21.063/21.063	NO
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	Confluence Problem:
21.063/21.063	(VAR vNonEmpty w x y z)
21.063/21.063	(REPLACEMENT-MAP
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1, 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Inlining of Conditions Processor [STERN17]:
21.063/21.063	
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	Confluence Problem:
21.063/21.063	(VAR vNonEmpty w x y z)
21.063/21.063	(REPLACEMENT-MAP
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1, 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Clean CTRS Processor:
21.063/21.063	
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	Confluence Problem:
21.063/21.063	(VAR w x y z)
21.063/21.063	(REPLACEMENT-MAP
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1, 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	
21.063/21.063	CRule InfChecker Info:
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	Rule remains
21.063/21.063	Proof:
21.063/21.063	NO
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Infeasibility Problem:
21.063/21.063	[(VAR vNonEmpty w x y z vNonEmpty x y z)
21.063/21.063	(STRATEGY CONTEXTSENSITIVE
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)]
21.063/21.063	
21.063/21.063	Infeasibility Conditions:
21.063/21.063	iadd(z) ->* tp2(x,y)
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Obtaining a proof using Prover9:
21.063/21.063	
21.063/21.063	 -> Prover9 Output:
21.063/21.063	============================== Prover9 ===============================
21.063/21.063	Prover9 (64) version 2009-11A, November 2009.
21.063/21.063	Process 11463 was started by ubuntu on ubuntu,
21.063/21.063	Wed Mar  9 09:16:58 2022
21.063/21.063	The command was "./prover9 -f /tmp/prover911456-0.in".
21.063/21.063	============================== end of head ===========================
21.063/21.063	
21.063/21.063	============================== INPUT =================================
21.063/21.063	
21.063/21.063	% Reading from file /tmp/prover911456-0.in
21.063/21.063	
21.063/21.063	assign(max_seconds,20).
21.063/21.063	
21.063/21.063	formulas(assumptions).
21.063/21.063	->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.063/21.063	->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.063/21.063	->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement).
21.063/21.063	->_s0(iadd(x3),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(x2,0)) # label(replacement).
21.063/21.063	->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement).
21.063/21.063	->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(x,x) # label(reflexivity).
21.063/21.063	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(goals).
21.063/21.063	(exists x6 exists x7 exists x8 ->*_s0(iadd(x8),tp2(x6,x7))) # label(goal).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of input ==========================
21.063/21.063	
21.063/21.063	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.063/21.063	
21.063/21.063	% Formulas that are not ordinary clauses:
21.063/21.063	1 ->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	2 ->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	3 ->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	4 ->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	5 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	6 ->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	7 ->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	8 ->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	9 ->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	10 ->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	11 ->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	12 ->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 exists x8 ->*_s0(iadd(x8),tp2(x6,x7))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	
21.063/21.063	============================== end of process non-clausal formulas ===
21.063/21.063	
21.063/21.063	============================== PROCESS INITIAL CLAUSES ===============
21.063/21.063	
21.063/21.063	% Clauses before input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	-->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	-->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	-->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	-->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	-->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) # label(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== PREDICATE ELIMINATION =================
21.063/21.063	
21.063/21.063	No predicates eliminated.
21.063/21.063	
21.063/21.063	============================== end predicate elimination =============
21.063/21.063	
21.063/21.063	Auto_denials:
21.063/21.063	  % copying label goal to answer in negative clause
21.063/21.063	
21.063/21.063	Term ordering decisions:
21.063/21.063	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
21.063/21.063	Function symbol precedence:  function_order([ 0, tp2, s, iadd, imult, tp1, itwice, iquad ]).
21.063/21.063	After inverse_order:  (no changes).
21.063/21.063	Unfolding symbols: (none).
21.063/21.063	
21.063/21.063	Auto_inference settings:
21.063/21.063	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
21.063/21.063	  % clear(ordered_res).  % (HNE depth_diff=-9)
21.063/21.063	  % set(ur_resolution).  % (HNE depth_diff=-9)
21.063/21.063	    % set(ur_resolution) -> set(pos_ur_resolution).
21.063/21.063	    % set(ur_resolution) -> set(neg_ur_resolution).
21.063/21.063	
21.063/21.063	Auto_process settings:  (no changes).
21.063/21.063	
21.063/21.063	kept:      15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	kept:      16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	kept:      17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	kept:      18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	kept:      19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	kept:      20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	kept:      21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	kept:      22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	kept:      23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	kept:      24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	kept:      27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	kept:      28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	kept:      29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	kept:      30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	kept:      31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	kept:      32 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	
21.063/21.063	============================== end of process initial clauses ========
21.063/21.063	
21.063/21.063	============================== CLAUSES FOR SEARCH ====================
21.063/21.063	
21.063/21.063	% Clauses after input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of clauses for search =============
21.063/21.063	
21.063/21.063	============================== SEARCH ================================
21.063/21.063	
21.063/21.063	% Starting search at 0.00 seconds.
21.063/21.063	
21.063/21.063	given #1 (I,wt=8): 15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	
21.063/21.063	given #2 (I,wt=8): 16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	
21.063/21.063	given #3 (I,wt=8): 17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	
21.063/21.063	given #4 (I,wt=8): 18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	
21.063/21.063	given #5 (I,wt=8): 19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	
21.063/21.063	given #6 (I,wt=8): 20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	
21.063/21.063	given #7 (I,wt=10): 21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	
21.063/21.063	given #8 (I,wt=10): 22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	
21.063/21.063	given #9 (I,wt=6): 24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #10 (I,wt=6): 25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #11 (I,wt=6): 26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #12 (I,wt=15): 28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	
21.063/21.063	given #13 (I,wt=3): 30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	
21.063/21.063	given #14 (I,wt=9): 31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	
21.063/21.063	============================== PROOF =================================
21.063/21.063	
21.063/21.063	% Proof 1 at 0.00 (+ 0.01) seconds: goal.
21.063/21.063	% Length of proof is 8.
21.063/21.063	% Level of proof is 3.
21.063/21.063	% Maximum clause weight is 9.000.
21.063/21.063	% Given clauses 14.
21.063/21.063	
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 exists x8 ->*_s0(iadd(x8),tp2(x6,x7))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(iadd(x),tp2(y,z)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	59 ->*_s0(iadd(x),tp2(0,x)).  [ur(31,a,24,a,b,30,a)].
21.063/21.063	60 $F # answer(goal).  [resolve(59,a,32,a)].
21.063/21.063	
21.063/21.063	============================== end of proof ==========================
21.063/21.063	
21.063/21.063	============================== STATISTICS ============================
21.063/21.063	
21.063/21.063	Given=14. Generated=45. Kept=45. proofs=1.
21.063/21.063	Usable=14. Sos=25. Demods=0. Limbo=2, Disabled=21. Hints=0.
21.063/21.063	Kept_by_rule=0, Deleted_by_rule=0.
21.063/21.063	Forward_subsumed=0. Back_subsumed=3.
21.063/21.063	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
21.063/21.063	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
21.063/21.063	Demod_attempts=0. Demod_rewrites=0.
21.063/21.063	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
21.063/21.063	Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=19.
21.063/21.063	Megabytes=0.13.
21.063/21.063	User_CPU=0.00, System_CPU=0.01, Wall_clock=0.
21.063/21.063	
21.063/21.063	============================== end of statistics =====================
21.063/21.063	
21.063/21.063	============================== end of search =========================
21.063/21.063	
21.063/21.063	THEOREM PROVED
21.063/21.063	
21.063/21.063	Exiting with 1 proof.
21.063/21.063	
21.063/21.063	Process 11463 exit (max_proofs) Wed Mar  9 09:16:58 2022
21.063/21.063	
21.063/21.063	
21.063/21.063	The problem is feasible.
21.063/21.063	
21.063/21.063	
21.063/21.063	CRule InfChecker Info:
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	Rule remains
21.063/21.063	Proof:
21.063/21.063	NO_CONDS
21.063/21.063	
21.063/21.063	CRule InfChecker Info:
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	Rule remains
21.063/21.063	Proof:
21.063/21.063	NO_CONDS
21.063/21.063	
21.063/21.063	CRule InfChecker Info:
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	Rule remains
21.063/21.063	Proof:
21.063/21.063	NO_CONDS
21.063/21.063	
21.063/21.063	CRule InfChecker Info:
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	Rule remains
21.063/21.063	Proof:
21.063/21.063	NO
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Infeasibility Problem:
21.063/21.063	[(VAR vNonEmpty w x y z vNonEmpty w x y z)
21.063/21.063	(STRATEGY CONTEXTSENSITIVE
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)]
21.063/21.063	
21.063/21.063	Infeasibility Conditions:
21.063/21.063	iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Obtaining a proof using Prover9:
21.063/21.063	
21.063/21.063	 -> Prover9 Output:
21.063/21.063	============================== Prover9 ===============================
21.063/21.063	Prover9 (64) version 2009-11A, November 2009.
21.063/21.063	Process 11485 was started by ubuntu on ubuntu,
21.063/21.063	Wed Mar  9 09:16:58 2022
21.063/21.063	The command was "./prover9 -f /tmp/prover911478-0.in".
21.063/21.063	============================== end of head ===========================
21.063/21.063	
21.063/21.063	============================== INPUT =================================
21.063/21.063	
21.063/21.063	% Reading from file /tmp/prover911478-0.in
21.063/21.063	
21.063/21.063	assign(max_seconds,20).
21.063/21.063	
21.063/21.063	formulas(assumptions).
21.063/21.063	->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.063/21.063	->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.063/21.063	->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement).
21.063/21.063	->_s0(iadd(x3),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(x2,0)) # label(replacement).
21.063/21.063	->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement).
21.063/21.063	->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(x,x) # label(reflexivity).
21.063/21.063	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(goals).
21.063/21.063	(exists x6 exists x7 exists x8 exists x9 (->*_s0(iadd(x9),tp2(x6,x8)) & ->*_s0(imult(x6),tp2(x7,s(x8))))) # label(goal).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of input ==========================
21.063/21.063	
21.063/21.063	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.063/21.063	
21.063/21.063	% Formulas that are not ordinary clauses:
21.063/21.063	1 ->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	2 ->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	3 ->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	4 ->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	5 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	6 ->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	7 ->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	8 ->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	9 ->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	10 ->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	11 ->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	12 ->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 exists x8 exists x9 (->*_s0(iadd(x9),tp2(x6,x8)) & ->*_s0(imult(x6),tp2(x7,s(x8))))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	
21.063/21.063	============================== end of process non-clausal formulas ===
21.063/21.063	
21.063/21.063	============================== PROCESS INITIAL CLAUSES ===============
21.063/21.063	
21.063/21.063	% Clauses before input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	-->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	-->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	-->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	-->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	-->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) # label(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== PREDICATE ELIMINATION =================
21.063/21.063	
21.063/21.063	No predicates eliminated.
21.063/21.063	
21.063/21.063	============================== end predicate elimination =============
21.063/21.063	
21.063/21.063	Auto_denials:
21.063/21.063	  % copying label goal to answer in negative clause
21.063/21.063	
21.063/21.063	Term ordering decisions:
21.063/21.063	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
21.063/21.063	Function symbol precedence:  function_order([ 0, tp2, s, iadd, imult, tp1, itwice, iquad ]).
21.063/21.063	After inverse_order:  (no changes).
21.063/21.063	Unfolding symbols: (none).
21.063/21.063	
21.063/21.063	Auto_inference settings:
21.063/21.063	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
21.063/21.063	  % clear(ordered_res).  % (HNE depth_diff=-9)
21.063/21.063	  % set(ur_resolution).  % (HNE depth_diff=-9)
21.063/21.063	    % set(ur_resolution) -> set(pos_ur_resolution).
21.063/21.063	    % set(ur_resolution) -> set(neg_ur_resolution).
21.063/21.063	
21.063/21.063	Auto_process settings:
21.063/21.063	  % set(unit_deletion).  % (Horn set with negative nonunits)
21.063/21.063	
21.063/21.063	kept:      15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	kept:      16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	kept:      17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	kept:      18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	kept:      19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	kept:      20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	kept:      21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	kept:      22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	kept:      23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	kept:      24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	kept:      27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	kept:      28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	kept:      29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	kept:      30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	kept:      31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	kept:      32 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	
21.063/21.063	============================== end of process initial clauses ========
21.063/21.063	
21.063/21.063	============================== CLAUSES FOR SEARCH ====================
21.063/21.063	
21.063/21.063	% Clauses after input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of clauses for search =============
21.063/21.063	
21.063/21.063	============================== SEARCH ================================
21.063/21.063	
21.063/21.063	% Starting search at 0.00 seconds.
21.063/21.063	
21.063/21.063	given #1 (I,wt=8): 15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	
21.063/21.063	given #2 (I,wt=8): 16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	
21.063/21.063	given #3 (I,wt=8): 17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	
21.063/21.063	given #4 (I,wt=8): 18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	
21.063/21.063	given #5 (I,wt=8): 19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	
21.063/21.063	given #6 (I,wt=8): 20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	
21.063/21.063	given #7 (I,wt=10): 21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	
21.063/21.063	given #8 (I,wt=10): 22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	
21.063/21.063	given #9 (I,wt=14): 23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	
21.063/21.063	given #10 (I,wt=6): 24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #11 (I,wt=6): 25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #12 (I,wt=6): 26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #13 (I,wt=15): 28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	
21.063/21.063	given #14 (I,wt=11): 29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	
21.063/21.063	given #15 (I,wt=3): 30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	
21.063/21.063	given #16 (I,wt=9): 31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	
21.063/21.063	given #17 (I,wt=13): 32 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	
21.063/21.063	given #18 (A,wt=10): 33 ->_s0(tp2(x,iadd(y)),tp2(x,tp2(0,y))).  [ur(22,a,24,a)].
21.063/21.063	
21.063/21.063	given #19 (F,wt=16): 60 -->*_s0(imult(x),tp2(y,s(z))) | -->_s0(iadd(u),w) | -->*_s0(w,tp2(x,z)) # answer(goal).  [resolve(32,a,31,c)].
21.063/21.063	
21.063/21.063	============================== PROOF =================================
21.063/21.063	
21.063/21.063	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
21.063/21.063	% Length of proof is 11.
21.063/21.063	% Level of proof is 4.
21.063/21.063	% Maximum clause weight is 16.000.
21.063/21.063	% Given clauses 19.
21.063/21.063	
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 exists x8 exists x9 (->*_s0(iadd(x9),tp2(x6,x8)) & ->*_s0(imult(x6),tp2(x7,s(x8))))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	58 ->*_s0(imult(0),tp2(0,x)).  [ur(31,a,25,a,b,30,a)].
21.063/21.063	60 -->*_s0(imult(x),tp2(y,s(z))) | -->_s0(iadd(u),w) | -->*_s0(w,tp2(x,z)) # answer(goal).  [resolve(32,a,31,c)].
21.063/21.063	76 -->*_s0(imult(0),tp2(x,s(y))) # answer(goal).  [ur(60,b,24,a,c,30,a)].
21.063/21.063	77 $F # answer(goal).  [resolve(76,a,58,a)].
21.063/21.063	
21.063/21.063	============================== end of proof ==========================
21.063/21.063	
21.063/21.063	============================== STATISTICS ============================
21.063/21.063	
21.063/21.063	Given=19. Generated=63. Kept=62. proofs=1.
21.063/21.063	Usable=19. Sos=36. Demods=0. Limbo=5, Disabled=19. Hints=0.
21.063/21.063	Kept_by_rule=0, Deleted_by_rule=0.
21.063/21.063	Forward_subsumed=1. Back_subsumed=1.
21.063/21.063	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
21.063/21.063	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
21.063/21.063	Demod_attempts=0. Demod_rewrites=0.
21.063/21.063	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
21.063/21.063	Nonunit_fsub_feature_tests=13. Nonunit_bsub_feature_tests=22.
21.063/21.063	Megabytes=0.18.
21.063/21.063	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.063/21.063	
21.063/21.063	============================== end of statistics =====================
21.063/21.063	
21.063/21.063	============================== end of search =========================
21.063/21.063	
21.063/21.063	THEOREM PROVED
21.063/21.063	
21.063/21.063	Exiting with 1 proof.
21.063/21.063	
21.063/21.063	Process 11485 exit (max_proofs) Wed Mar  9 09:16:58 2022
21.063/21.063	
21.063/21.063	
21.063/21.063	The problem is feasible.
21.063/21.063	
21.063/21.063	
21.063/21.063	CRule InfChecker Info:
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	Rule remains
21.063/21.063	Proof:
21.063/21.063	NO
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Infeasibility Problem:
21.063/21.063	[(VAR vNonEmpty w x y z vNonEmpty x y z)
21.063/21.063	(STRATEGY CONTEXTSENSITIVE
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)]
21.063/21.063	
21.063/21.063	Infeasibility Conditions:
21.063/21.063	itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Obtaining a proof using Prover9:
21.063/21.063	
21.063/21.063	 -> Prover9 Output:
21.063/21.063	============================== Prover9 ===============================
21.063/21.063	Prover9 (64) version 2009-11A, November 2009.
21.063/21.063	Process 11507 was started by ubuntu on ubuntu,
21.063/21.063	Wed Mar  9 09:16:58 2022
21.063/21.063	The command was "./prover9 -f /tmp/prover911500-0.in".
21.063/21.063	============================== end of head ===========================
21.063/21.063	
21.063/21.063	============================== INPUT =================================
21.063/21.063	
21.063/21.063	% Reading from file /tmp/prover911500-0.in
21.063/21.063	
21.063/21.063	assign(max_seconds,20).
21.063/21.063	
21.063/21.063	formulas(assumptions).
21.063/21.063	->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.063/21.063	->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.063/21.063	->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement).
21.063/21.063	->_s0(iadd(x3),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(x2,0)) # label(replacement).
21.063/21.063	->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement).
21.063/21.063	->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(x,x) # label(reflexivity).
21.063/21.063	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(goals).
21.063/21.063	(exists x6 exists x7 exists x8 (->*_s0(itwice(x7),tp1(x8)) & ->*_s0(itwice(x8),tp1(x6)))) # label(goal).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of input ==========================
21.063/21.063	
21.063/21.063	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.063/21.063	
21.063/21.063	% Formulas that are not ordinary clauses:
21.063/21.063	1 ->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	2 ->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	3 ->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	4 ->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	5 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	6 ->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	7 ->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	8 ->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	9 ->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	10 ->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	11 ->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	12 ->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 exists x8 (->*_s0(itwice(x7),tp1(x8)) & ->*_s0(itwice(x8),tp1(x6)))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	
21.063/21.063	============================== end of process non-clausal formulas ===
21.063/21.063	
21.063/21.063	============================== PROCESS INITIAL CLAUSES ===============
21.063/21.063	
21.063/21.063	% Clauses before input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	-->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	-->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	-->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	-->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	-->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	-->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) # label(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== PREDICATE ELIMINATION =================
21.063/21.063	
21.063/21.063	No predicates eliminated.
21.063/21.063	
21.063/21.063	============================== end predicate elimination =============
21.063/21.063	
21.063/21.063	Auto_denials:
21.063/21.063	  % copying label goal to answer in negative clause
21.063/21.063	
21.063/21.063	Term ordering decisions:
21.063/21.063	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
21.063/21.063	Function symbol precedence:  function_order([ 0, tp2, s, iadd, imult, tp1, itwice, iquad ]).
21.063/21.063	After inverse_order:  (no changes).
21.063/21.063	Unfolding symbols: (none).
21.063/21.063	
21.063/21.063	Auto_inference settings:
21.063/21.063	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
21.063/21.063	  % clear(ordered_res).  % (HNE depth_diff=-9)
21.063/21.063	  % set(ur_resolution).  % (HNE depth_diff=-9)
21.063/21.063	    % set(ur_resolution) -> set(pos_ur_resolution).
21.063/21.063	    % set(ur_resolution) -> set(neg_ur_resolution).
21.063/21.063	
21.063/21.063	Auto_process settings:
21.063/21.063	  % set(unit_deletion).  % (Horn set with negative nonunits)
21.063/21.063	
21.063/21.063	kept:      15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	kept:      16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	kept:      17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	kept:      18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	kept:      19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	kept:      20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	kept:      21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	kept:      22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	kept:      23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	kept:      24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	kept:      27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	kept:      28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	kept:      29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	kept:      30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	kept:      31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	kept:      32 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	
21.063/21.063	============================== end of process initial clauses ========
21.063/21.063	
21.063/21.063	============================== CLAUSES FOR SEARCH ====================
21.063/21.063	
21.063/21.063	% Clauses after input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of clauses for search =============
21.063/21.063	
21.063/21.063	============================== SEARCH ================================
21.063/21.063	
21.063/21.063	% Starting search at 0.00 seconds.
21.063/21.063	
21.063/21.063	given #1 (I,wt=8): 15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	
21.063/21.063	given #2 (I,wt=8): 16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	
21.063/21.063	given #3 (I,wt=8): 17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	
21.063/21.063	given #4 (I,wt=8): 18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	
21.063/21.063	given #5 (I,wt=8): 19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	
21.063/21.063	given #6 (I,wt=8): 20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	
21.063/21.063	given #7 (I,wt=10): 21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	
21.063/21.063	given #8 (I,wt=10): 22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	
21.063/21.063	given #9 (I,wt=14): 23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	
21.063/21.063	given #10 (I,wt=6): 24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #11 (I,wt=6): 25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #12 (I,wt=6): 26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #13 (I,wt=22): 27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	
21.063/21.063	given #14 (I,wt=11): 29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	
21.063/21.063	given #15 (I,wt=3): 30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	
21.063/21.063	given #16 (I,wt=9): 31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	
21.063/21.063	given #17 (I,wt=10): 32 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	
21.063/21.063	given #18 (A,wt=10): 33 ->_s0(tp2(x,iadd(y)),tp2(x,tp2(0,y))).  [ur(22,a,24,a)].
21.063/21.063	
21.063/21.063	given #19 (F,wt=13): 60 -->*_s0(itwice(x),tp1(y)) | -->_s0(itwice(z),u) | -->*_s0(u,tp1(x)) # answer(goal).  [resolve(32,a,31,c)].
21.063/21.063	
21.063/21.063	given #20 (F,wt=10): 74 -->*_s0(itwice(x),tp1(y)) | -->_s0(itwice(z),tp1(x)) # answer(goal).  [resolve(60,c,30,a)].
21.063/21.063	
21.063/21.063	given #21 (F,wt=11): 76 -->*_s0(itwice(x),tp1(y)) | -->*_s0(iadd(z),tp2(x,x)) # answer(goal).  [resolve(74,b,29,b)].
21.063/21.063	
21.063/21.063	given #22 (F,wt=13): 61 -->*_s0(itwice(x),tp1(y)) | -->_s0(itwice(y),z) | -->*_s0(z,tp1(u)) # answer(goal).  [resolve(32,b,31,c)].
21.063/21.063	
21.063/21.063	given #23 (T,wt=6): 57 ->*_s0(imult(0),tp2(x,0)).  [ur(31,a,26,a,b,30,a)].
21.063/21.063	
21.063/21.063	given #24 (T,wt=6): 58 ->*_s0(imult(0),tp2(0,x)).  [ur(31,a,25,a,b,30,a)].
21.063/21.063	
21.063/21.063	given #25 (T,wt=6): 59 ->*_s0(iadd(x),tp2(0,x)).  [ur(31,a,24,a,b,30,a)].
21.063/21.063	
21.063/21.063	given #26 (T,wt=5): 84 ->_s0(itwice(0),tp1(0)).  [ur(29,a,59,a)].
21.063/21.063	
21.063/21.063	============================== PROOF =================================
21.063/21.063	
21.063/21.063	% Proof 1 at 0.01 (+ 0.00) seconds: goal.
21.063/21.063	% Length of proof is 15.
21.063/21.063	% Level of proof is 6.
21.063/21.063	% Maximum clause weight is 13.000.
21.063/21.063	% Given clauses 26.
21.063/21.063	
21.063/21.063	12 ->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 exists x8 (->*_s0(itwice(x7),tp1(x8)) & ->*_s0(itwice(x8),tp1(x6)))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	59 ->*_s0(iadd(x),tp2(0,x)).  [ur(31,a,24,a,b,30,a)].
21.063/21.063	60 -->*_s0(itwice(x),tp1(y)) | -->_s0(itwice(z),u) | -->*_s0(u,tp1(x)) # answer(goal).  [resolve(32,a,31,c)].
21.063/21.063	74 -->*_s0(itwice(x),tp1(y)) | -->_s0(itwice(z),tp1(x)) # answer(goal).  [resolve(60,c,30,a)].
21.063/21.063	76 -->*_s0(itwice(x),tp1(y)) | -->*_s0(iadd(z),tp2(x,x)) # answer(goal).  [resolve(74,b,29,b)].
21.063/21.063	83 -->*_s0(itwice(0),tp1(x)) # answer(goal).  [resolve(59,a,76,b)].
21.063/21.063	84 ->_s0(itwice(0),tp1(0)).  [ur(29,a,59,a)].
21.063/21.063	89 $F # answer(goal).  [ur(31,a,84,a,b,30,a),unit_del(a,83)].
21.063/21.063	
21.063/21.063	============================== end of proof ==========================
21.063/21.063	
21.063/21.063	============================== STATISTICS ============================
21.063/21.063	
21.063/21.063	Given=26. Generated=79. Kept=74. proofs=1.
21.063/21.063	Usable=26. Sos=45. Demods=0. Limbo=2, Disabled=19. Hints=0.
21.063/21.063	Kept_by_rule=0, Deleted_by_rule=0.
21.063/21.063	Forward_subsumed=4. Back_subsumed=1.
21.063/21.063	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
21.063/21.063	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
21.063/21.063	Demod_attempts=0. Demod_rewrites=0.
21.063/21.063	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
21.063/21.063	Nonunit_fsub_feature_tests=38. Nonunit_bsub_feature_tests=61.
21.063/21.063	Megabytes=0.19.
21.063/21.063	User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
21.063/21.063	
21.063/21.063	============================== end of statistics =====================
21.063/21.063	
21.063/21.063	============================== end of search =========================
21.063/21.063	
21.063/21.063	THEOREM PROVED
21.063/21.063	
21.063/21.063	Exiting with 1 proof.
21.063/21.063	
21.063/21.063	Process 11507 exit (max_proofs) Wed Mar  9 09:16:58 2022
21.063/21.063	
21.063/21.063	
21.063/21.063	The problem is feasible.
21.063/21.063	
21.063/21.063	
21.063/21.063	CRule InfChecker Info:
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	Rule remains
21.063/21.063	Proof:
21.063/21.063	NO
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Infeasibility Problem:
21.063/21.063	[(VAR vNonEmpty w x y z vNonEmpty x y)
21.063/21.063	(STRATEGY CONTEXTSENSITIVE
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)]
21.063/21.063	
21.063/21.063	Infeasibility Conditions:
21.063/21.063	iadd(y) ->* tp2(x,x)
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Obtaining a proof using Prover9:
21.063/21.063	
21.063/21.063	 -> Prover9 Output:
21.063/21.063	============================== Prover9 ===============================
21.063/21.063	Prover9 (64) version 2009-11A, November 2009.
21.063/21.063	Process 11529 was started by ubuntu on ubuntu,
21.063/21.063	Wed Mar  9 09:16:58 2022
21.063/21.063	The command was "./prover9 -f /tmp/prover911522-0.in".
21.063/21.063	============================== end of head ===========================
21.063/21.063	
21.063/21.063	============================== INPUT =================================
21.063/21.063	
21.063/21.063	% Reading from file /tmp/prover911522-0.in
21.063/21.063	
21.063/21.063	assign(max_seconds,20).
21.063/21.063	
21.063/21.063	formulas(assumptions).
21.063/21.063	->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence).
21.063/21.063	->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.063/21.063	->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.063/21.063	->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement).
21.063/21.063	->_s0(iadd(x3),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(0,x3)) # label(replacement).
21.063/21.063	->_s0(imult(0),tp2(x2,0)) # label(replacement).
21.063/21.063	->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement).
21.063/21.063	->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement).
21.063/21.063	->*_s0(x,x) # label(reflexivity).
21.063/21.063	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(goals).
21.063/21.063	(exists x6 exists x7 ->*_s0(iadd(x7),tp2(x6,x6))) # label(goal).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of input ==========================
21.063/21.063	
21.063/21.063	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.063/21.063	
21.063/21.063	% Formulas that are not ordinary clauses:
21.063/21.063	1 ->_s0(x1,y) -> ->_s0(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	2 ->_s0(x1,y) -> ->_s0(imult(x1),imult(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	3 ->_s0(x1,y) -> ->_s0(iquad(x1),iquad(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	4 ->_s0(x1,y) -> ->_s0(itwice(x1),itwice(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	5 ->_s0(x1,y) -> ->_s0(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	6 ->_s0(x1,y) -> ->_s0(tp1(x1),tp1(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	7 ->_s0(x1,y) -> ->_s0(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	8 ->_s0(x2,y) -> ->_s0(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	9 ->*_s0(iadd(x4),tp2(x2,x3)) -> ->_s0(iadd(s(x4)),tp2(s(x2),x3)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	10 ->*_s0(iadd(x4),tp2(x1,x3)) & ->*_s0(imult(x1),tp2(x2,s(x3))) -> ->_s0(imult(s(x4)),tp2(s(x2),s(x3))) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	11 ->*_s0(itwice(x3),tp1(x4)) & ->*_s0(itwice(x4),tp1(x2)) -> ->_s0(iquad(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	12 ->*_s0(iadd(x3),tp2(x2,x2)) -> ->_s0(itwice(x3),tp1(x2)) # label(replacement) # label(non_clause).  [assumption].
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 ->*_s0(iadd(x7),tp2(x6,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	
21.063/21.063	============================== end of process non-clausal formulas ===
21.063/21.063	
21.063/21.063	============================== PROCESS INITIAL CLAUSES ===============
21.063/21.063	
21.063/21.063	% Clauses before input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	-->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	-->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	-->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	-->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	-->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	-->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	-->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	-->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	-->*_s0(iadd(x),tp2(y,y)) # label(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== PREDICATE ELIMINATION =================
21.063/21.063	
21.063/21.063	No predicates eliminated.
21.063/21.063	
21.063/21.063	============================== end predicate elimination =============
21.063/21.063	
21.063/21.063	Auto_denials:
21.063/21.063	  % copying label goal to answer in negative clause
21.063/21.063	
21.063/21.063	Term ordering decisions:
21.063/21.063	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
21.063/21.063	Function symbol precedence:  function_order([ 0, tp2, s, iadd, imult, tp1, itwice, iquad ]).
21.063/21.063	After inverse_order:  (no changes).
21.063/21.063	Unfolding symbols: (none).
21.063/21.063	
21.063/21.063	Auto_inference settings:
21.063/21.063	  % set(neg_binary_resolution).  % (HNE depth_diff=-9)
21.063/21.063	  % clear(ordered_res).  % (HNE depth_diff=-9)
21.063/21.063	  % set(ur_resolution).  % (HNE depth_diff=-9)
21.063/21.063	    % set(ur_resolution) -> set(pos_ur_resolution).
21.063/21.063	    % set(ur_resolution) -> set(neg_ur_resolution).
21.063/21.063	
21.063/21.063	Auto_process settings:  (no changes).
21.063/21.063	
21.063/21.063	kept:      15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	kept:      16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	kept:      17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	kept:      18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	kept:      19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	kept:      20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	kept:      21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	kept:      22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	kept:      23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	kept:      24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	kept:      26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	kept:      27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	kept:      28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	kept:      29 -->*_s0(iadd(x),tp2(y,y)) | ->_s0(itwice(x),tp1(y)) # label(replacement).  [clausify(12)].
21.063/21.063	kept:      30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	kept:      31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	kept:      32 -->*_s0(iadd(x),tp2(y,y)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	
21.063/21.063	============================== end of process initial clauses ========
21.063/21.063	
21.063/21.063	============================== CLAUSES FOR SEARCH ====================
21.063/21.063	
21.063/21.063	% Clauses after input processing:
21.063/21.063	
21.063/21.063	formulas(usable).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(sos).
21.063/21.063	15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(iadd(x),tp2(y,y)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(demodulators).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of clauses for search =============
21.063/21.063	
21.063/21.063	============================== SEARCH ================================
21.063/21.063	
21.063/21.063	% Starting search at 0.00 seconds.
21.063/21.063	
21.063/21.063	given #1 (I,wt=8): 15 -->_s0(x,y) | ->_s0(iadd(x),iadd(y)) # label(congruence).  [clausify(1)].
21.063/21.063	
21.063/21.063	given #2 (I,wt=8): 16 -->_s0(x,y) | ->_s0(imult(x),imult(y)) # label(congruence).  [clausify(2)].
21.063/21.063	
21.063/21.063	given #3 (I,wt=8): 17 -->_s0(x,y) | ->_s0(iquad(x),iquad(y)) # label(congruence).  [clausify(3)].
21.063/21.063	
21.063/21.063	given #4 (I,wt=8): 18 -->_s0(x,y) | ->_s0(itwice(x),itwice(y)) # label(congruence).  [clausify(4)].
21.063/21.063	
21.063/21.063	given #5 (I,wt=8): 19 -->_s0(x,y) | ->_s0(s(x),s(y)) # label(congruence).  [clausify(5)].
21.063/21.063	
21.063/21.063	given #6 (I,wt=8): 20 -->_s0(x,y) | ->_s0(tp1(x),tp1(y)) # label(congruence).  [clausify(6)].
21.063/21.063	
21.063/21.063	given #7 (I,wt=10): 21 -->_s0(x,y) | ->_s0(tp2(x,z),tp2(y,z)) # label(congruence).  [clausify(7)].
21.063/21.063	
21.063/21.063	given #8 (I,wt=10): 22 -->_s0(x,y) | ->_s0(tp2(z,x),tp2(z,y)) # label(congruence).  [clausify(8)].
21.063/21.063	
21.063/21.063	given #9 (I,wt=14): 23 -->*_s0(iadd(x),tp2(y,z)) | ->_s0(iadd(s(x)),tp2(s(y),z)) # label(replacement).  [clausify(9)].
21.063/21.063	
21.063/21.063	given #10 (I,wt=6): 24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #11 (I,wt=6): 25 ->_s0(imult(0),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #12 (I,wt=6): 26 ->_s0(imult(0),tp2(x,0)) # label(replacement).  [assumption].
21.063/21.063	
21.063/21.063	given #13 (I,wt=22): 27 -->*_s0(iadd(x),tp2(y,z)) | -->*_s0(imult(y),tp2(u,s(z))) | ->_s0(imult(s(x)),tp2(s(u),s(z))) # label(replacement).  [clausify(10)].
21.063/21.063	
21.063/21.063	given #14 (I,wt=15): 28 -->*_s0(itwice(x),tp1(y)) | -->*_s0(itwice(y),tp1(z)) | ->_s0(iquad(x),tp1(z)) # label(replacement).  [clausify(11)].
21.063/21.063	
21.063/21.063	given #15 (I,wt=3): 30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	
21.063/21.063	given #16 (I,wt=9): 31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	
21.063/21.063	============================== PROOF =================================
21.063/21.063	
21.063/21.063	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
21.063/21.063	% Length of proof is 8.
21.063/21.063	% Level of proof is 3.
21.063/21.063	% Maximum clause weight is 9.000.
21.063/21.063	% Given clauses 16.
21.063/21.063	
21.063/21.063	13 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	14 (exists x6 exists x7 ->*_s0(iadd(x7),tp2(x6,x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	24 ->_s0(iadd(x),tp2(0,x)) # label(replacement).  [assumption].
21.063/21.063	30 ->*_s0(x,x) # label(reflexivity).  [assumption].
21.063/21.063	31 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(13)].
21.063/21.063	32 -->*_s0(iadd(x),tp2(y,y)) # label(goal) # answer(goal).  [deny(14)].
21.063/21.063	59 ->*_s0(iadd(x),tp2(0,x)).  [ur(31,a,24,a,b,30,a)].
21.063/21.063	60 $F # answer(goal).  [resolve(59,a,32,a)].
21.063/21.063	
21.063/21.063	============================== end of proof ==========================
21.063/21.063	
21.063/21.063	============================== STATISTICS ============================
21.063/21.063	
21.063/21.063	Given=16. Generated=45. Kept=45. proofs=1.
21.063/21.063	Usable=16. Sos=25. Demods=0. Limbo=2, Disabled=19. Hints=0.
21.063/21.063	Kept_by_rule=0, Deleted_by_rule=0.
21.063/21.063	Forward_subsumed=0. Back_subsumed=1.
21.063/21.063	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
21.063/21.063	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
21.063/21.063	Demod_attempts=0. Demod_rewrites=0.
21.063/21.063	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
21.063/21.063	Nonunit_fsub_feature_tests=1. Nonunit_bsub_feature_tests=19.
21.063/21.063	Megabytes=0.14.
21.063/21.063	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.063/21.063	
21.063/21.063	============================== end of statistics =====================
21.063/21.063	
21.063/21.063	============================== end of search =========================
21.063/21.063	
21.063/21.063	THEOREM PROVED
21.063/21.063	
21.063/21.063	Exiting with 1 proof.
21.063/21.063	
21.063/21.063	Process 11529 exit (max_proofs) Wed Mar  9 09:16:58 2022
21.063/21.063	
21.063/21.063	
21.063/21.063	The problem is feasible.
21.063/21.063	
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	Confluence Problem:
21.063/21.063	(VAR w x y z)
21.063/21.063	(REPLACEMENT-MAP
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1, 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	
21.063/21.063	Critical Pairs Processor:
21.063/21.063	-> Rules:
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	-> Vars:
21.063/21.063	"w", "x", "y", "z"
21.063/21.063	
21.063/21.063	-> Rlps:
21.063/21.063	crule: iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y), id: 1, possubterms: iadd(s(z))-> [], s(z)-> [1]
21.063/21.063	crule: iadd(y) -> tp2(0,y), id: 2, possubterms: iadd(y)-> []
21.063/21.063	crule: imult(0) -> tp2(0,y), id: 3, possubterms: imult(0)-> [], 0-> [1]
21.063/21.063	crule: imult(0) -> tp2(x,0), id: 4, possubterms: imult(0)-> [], 0-> [1]
21.063/21.063	crule: imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y)), id: 5, possubterms: imult(s(z))-> [], s(z)-> [1]
21.063/21.063	crule: iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x), id: 6, possubterms: iquad(y)-> []
21.063/21.063	crule: itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x), id: 7, possubterms: itwice(y)-> []
21.063/21.063	
21.063/21.063	-> Unifications:
21.063/21.063	R2 unifies with  R1 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.063/21.063	R4 unifies with  R3 at  p: [], l: imult(0), lp: imult(0), conds: {}, sig: {}, l': imult(0), r: tp2(x,0), r': tp2(0,y)
21.063/21.063	
21.063/21.063	-> Critical pairs info:
21.063/21.063	<tp2(0,y),tp2(x,0)>   =>  Not trivial, Overlay, NW2, N1
21.063/21.063	<tp2(s(x),y'),tp2(0,s(z))> | iadd(z) ->* tp2(x,y')  =>  Not trivial, Overlay, NW2, N2
21.063/21.063	
21.063/21.063	-> Problem conclusions:
21.063/21.063	 Left linear, Right linear, Linear
21.063/21.063	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
21.063/21.063	 CTRS Type: 4
21.063/21.063	 Not deterministic, Maybe strongly deterministic
21.063/21.063	 Oriented CTRS, Not properly oriented CTRS, Not join CTRS, Not semiequational CTRS
21.063/21.063	 Maybe right-stable CTRS, Overlay CTRS
21.063/21.063	 Maybe normal CTRS, Maybe almost normal CTRS
21.063/21.063	 Maybe terminating CTRS, Maybe operational terminating CTRS, Maybe joinable CCPs
21.063/21.063	 Maybe level confluent
21.063/21.063	 Maybe confluent
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	Confluence Problem:
21.063/21.063	(VAR w x y z x y z)
21.063/21.063	(REPLACEMENT-MAP
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1, 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)
21.063/21.063	Critical Pairs:
21.063/21.063	<tp2(0,y),tp2(x,0)>   =>  Not trivial, Overlay, NW2, N1
21.063/21.063	<tp2(s(x),y'),tp2(0,s(z))> | iadd(z) ->* tp2(x,y')  =>  Not trivial, Overlay, NW2, N2
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	
21.063/21.063	Conditional Critical Pairs Distributor Processor
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	Confluence Problem:
21.063/21.063	(VAR w x y z x y z)
21.063/21.063	(REPLACEMENT-MAP
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1, 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)
21.063/21.063	Critical Pairs:
21.063/21.063	<tp2(0,y),tp2(x,0)>   =>  Not trivial, Overlay, NW2, N1
21.063/21.063	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
21.063/21.063	
21.063/21.063	Infeasible Convergence No Conditions CCP Processor:
21.063/21.063	Infeasible convergence?
21.063/21.063	YES
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Infeasibility Problem:
21.063/21.063	[(VAR vNonEmpty w x y z vNonEmpty z)
21.063/21.063	(STRATEGY CONTEXTSENSITIVE
21.063/21.063	(iadd 1)
21.063/21.063	(imult 1)
21.063/21.063	(iquad 1)
21.063/21.063	(itwice 1)
21.063/21.063	(0)
21.063/21.063	(c_x)
21.063/21.063	(c_y)
21.063/21.063	(fSNonEmpty)
21.063/21.063	(s 1)
21.063/21.063	(tp1 1)
21.063/21.063	(tp2 1 2)
21.063/21.063	)
21.063/21.063	(RULES
21.063/21.063	iadd(s(z)) -> tp2(s(x),y) | iadd(z) ->* tp2(x,y)
21.063/21.063	iadd(y) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(0,y)
21.063/21.063	imult(0) -> tp2(x,0)
21.063/21.063	imult(s(z)) -> tp2(s(x),s(y)) | iadd(z) ->* tp2(w,y), imult(w) ->* tp2(x,s(y))
21.063/21.063	iquad(y) -> tp1(x) | itwice(y) ->* tp1(z), itwice(z) ->* tp1(x)
21.063/21.063	itwice(y) -> tp1(x) | iadd(y) ->* tp2(x,x)
21.063/21.063	)]
21.063/21.063	
21.063/21.063	Infeasibility Conditions:
21.063/21.063	tp2(0,c_y) ->* z, tp2(c_x,0) ->* z
21.063/21.063	
21.063/21.063	Problem 1:
21.063/21.063	
21.063/21.063	Obtaining a model using Mace4:
21.063/21.063	
21.063/21.063	 -> Usable Rules:
21.063/21.063	Empty
21.063/21.063	
21.063/21.063	 -> Mace4 Output:
21.063/21.063	============================== Mace4 =================================
21.063/21.063	Mace4 (64) version 2009-11A, November 2009.
21.063/21.063	Process 11550 was started by ubuntu on ubuntu,
21.063/21.063	Wed Mar  9 09:16:58 2022
21.063/21.063	The command was "./mace4 -c -f /tmp/mace411532-2.in".
21.063/21.063	============================== end of head ===========================
21.063/21.063	
21.063/21.063	============================== INPUT =================================
21.063/21.063	
21.063/21.063	% Reading from file /tmp/mace411532-2.in
21.063/21.063	
21.063/21.063	assign(max_seconds,20).
21.063/21.063	
21.063/21.063	formulas(assumptions).
21.063/21.063	->(x1,y) -> ->(iadd(x1),iadd(y)) # label(congruence).
21.063/21.063	->(x1,y) -> ->(imult(x1),imult(y)) # label(congruence).
21.063/21.063	->(x1,y) -> ->(iquad(x1),iquad(y)) # label(congruence).
21.063/21.063	->(x1,y) -> ->(itwice(x1),itwice(y)) # label(congruence).
21.063/21.063	->(x1,y) -> ->(s(x1),s(y)) # label(congruence).
21.063/21.063	->(x1,y) -> ->(tp1(x1),tp1(y)) # label(congruence).
21.063/21.063	->(x1,y) -> ->(tp2(x1,x2),tp2(y,x2)) # label(congruence).
21.063/21.063	->(x2,y) -> ->(tp2(x1,x2),tp2(x1,y)) # label(congruence).
21.063/21.063	->*(x,x) # label(reflexivity).
21.063/21.063	->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	formulas(goals).
21.063/21.063	(exists x6 (->*(tp2(0,c_y),x6) & ->*(tp2(c_x,0),x6))) # label(goal).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of input ==========================
21.063/21.063	
21.063/21.063	============================== PROCESS NON-CLAUSAL FORMULAS ==========
21.063/21.063	
21.063/21.063	% Formulas that are not ordinary clauses:
21.063/21.063	1 ->(x1,y) -> ->(iadd(x1),iadd(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	2 ->(x1,y) -> ->(imult(x1),imult(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	3 ->(x1,y) -> ->(iquad(x1),iquad(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	4 ->(x1,y) -> ->(itwice(x1),itwice(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	5 ->(x1,y) -> ->(s(x1),s(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	6 ->(x1,y) -> ->(tp1(x1),tp1(y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	7 ->(x1,y) -> ->(tp2(x1,x2),tp2(y,x2)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	8 ->(x2,y) -> ->(tp2(x1,x2),tp2(x1,y)) # label(congruence) # label(non_clause).  [assumption].
21.063/21.063	9 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause).  [assumption].
21.063/21.063	10 (exists x6 (->*(tp2(0,c_y),x6) & ->*(tp2(c_x,0),x6))) # label(goal) # label(non_clause) # label(goal).  [goal].
21.063/21.063	
21.063/21.063	============================== end of process non-clausal formulas ===
21.063/21.063	
21.063/21.063	============================== CLAUSES FOR SEARCH ====================
21.063/21.063	
21.063/21.063	formulas(mace4_clauses).
21.063/21.063	-->(x,y) | ->(iadd(x),iadd(y)) # label(congruence).
21.063/21.063	-->(x,y) | ->(imult(x),imult(y)) # label(congruence).
21.063/21.063	-->(x,y) | ->(iquad(x),iquad(y)) # label(congruence).
21.063/21.063	-->(x,y) | ->(itwice(x),itwice(y)) # label(congruence).
21.063/21.063	-->(x,y) | ->(s(x),s(y)) # label(congruence).
21.063/21.063	-->(x,y) | ->(tp1(x),tp1(y)) # label(congruence).
21.063/21.063	-->(x,y) | ->(tp2(x,z),tp2(y,z)) # label(congruence).
21.063/21.063	-->(x,y) | ->(tp2(z,x),tp2(z,y)) # label(congruence).
21.063/21.063	->*(x,x) # label(reflexivity).
21.063/21.063	-->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity).
21.063/21.063	-->*(tp2(0,c_y),x) | -->*(tp2(c_x,0),x) # label(goal).
21.063/21.063	end_of_list.
21.063/21.063	
21.063/21.063	============================== end of clauses for search =============
21.063/21.063	
21.063/21.063	% There are no natural numbers in the input.
21.063/21.063	
21.063/21.063	============================== DOMAIN SIZE 2 =========================
21.063/21.063	
21.063/21.063	============================== MODEL =================================
21.063/21.063	
21.063/21.063	interpretation( 2, [number=1, seconds=0], [
21.063/21.063	
21.063/21.063	        function(0, [ 0 ]),
21.063/21.063	
21.063/21.063	        function(c_x, [ 0 ]),
21.063/21.063	
21.063/21.063	        function(c_y, [ 1 ]),
21.063/21.063	
21.063/21.063	        function(s(_), [ 0, 0 ]),
21.063/21.063	
21.063/21.063	        function(tp1(_), [ 0, 0 ]),
21.063/21.063	
21.063/21.063	        function(iadd(_), [ 0, 0 ]),
21.063/21.063	
21.063/21.063	        function(imult(_), [ 0, 0 ]),
21.063/21.063	
21.063/21.063	        function(iquad(_), [ 0, 0 ]),
21.063/21.063	
21.063/21.063	        function(itwice(_), [ 0, 0 ]),
21.063/21.063	
21.063/21.063	        function(tp2(_,_), [
21.063/21.063				   0, 1,
21.063/21.063				   0, 0 ]),
21.063/21.063	
21.063/21.063	        relation(->*(_,_), [
21.063/21.063				   1, 0,
21.063/21.063				   0, 1 ]),
21.063/21.063	
21.063/21.063	        relation(->(_,_), [
21.063/21.063				   0, 0,
21.063/21.063				   0, 0 ])
21.063/21.063	]).
21.063/21.063	
21.063/21.063	============================== end of model ==========================
21.063/21.063	
21.063/21.063	============================== STATISTICS ============================
21.063/21.063	
21.063/21.063	For domain size 2.
21.063/21.063	
21.063/21.063	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
21.063/21.063	Ground clauses: seen=52, kept=48.
21.063/21.063	Selections=146, assignments=274, propagations=8, current_models=1.
21.063/21.063	Rewrite_terms=1046, rewrite_bools=322, indexes=338.
21.063/21.063	Rules_from_neg_clauses=1, cross_offs=1.
21.063/21.063	
21.063/21.063	============================== end of statistics =====================
21.063/21.063	
21.063/21.063	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
21.063/21.063	
21.063/21.063	Exiting with 1 model.
21.063/21.063	
21.063/21.063	Process 11550 exit (max_models) Wed Mar  9 09:16:58 2022
21.063/21.063	The process finished Wed Mar  9 09:16:58 2022
21.063/21.063	
21.063/21.063	
21.063/21.063	Mace4 cooked interpretation:
21.063/21.063	
21.063/21.063	
21.063/21.063	
21.063/21.063	The problem is infeasible.
21.063/21.063	
21.063/21.063	
21.063/21.063	The problem is not joinable.
21.063/21.063	33.54user 1.59system 0:21.63elapsed 162%CPU (0avgtext+0avgdata 446252maxresident)k
21.063/21.063	8inputs+0outputs (0major+174683minor)pagefaults 0swaps