9.023/9.023	NO
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	Confluence Problem:
9.023/9.023	(VAR vNonEmpty:S x:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Inlining of Conditions Processor [STERN17]:
9.023/9.023	
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	Confluence Problem:
9.023/9.023	(VAR vNonEmpty:S x:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Clean CTRS Processor:
9.023/9.023	
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	Confluence Problem:
9.023/9.023	(VAR x:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	
9.023/9.023	CRule InfChecker Info:
9.023/9.023	a -> c
9.023/9.023	Rule remains
9.023/9.023	Proof:
9.023/9.023	NO_CONDS
9.023/9.023	
9.023/9.023	CRule InfChecker Info:
9.023/9.023	a -> d
9.023/9.023	Rule remains
9.023/9.023	Proof:
9.023/9.023	NO_CONDS
9.023/9.023	
9.023/9.023	CRule InfChecker Info:
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	Rule remains
9.023/9.023	Proof:
9.023/9.023	NO
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Infeasibility Problem:
9.023/9.023	[(VAR vNonEmpty:S vNonEmpty:S:S x:S:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S:S) -> x:S:S | x:S:S ->* c
9.023/9.023	)]
9.023/9.023	
9.023/9.023	Infeasibility Conditions:
9.023/9.023	x:S:S ->* c
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Obtaining a proof using Prover9:
9.023/9.023	
9.023/9.023	 -> Prover9 Output:
9.023/9.023	============================== Prover9 ===============================
9.023/9.023	Prover9 (64) version 2009-11A, November 2009.
9.023/9.023	Process 48558 was started by ubuntu on ubuntu,
9.023/9.023	Wed Jul 14 10:47:54 2021
9.023/9.023	The command was "./prover9 -f /tmp/prover948549-0.in".
9.023/9.023	============================== end of head ===========================
9.023/9.023	
9.023/9.023	============================== INPUT =================================
9.023/9.023	
9.023/9.023	% Reading from file /tmp/prover948549-0.in
9.023/9.023	
9.023/9.023	assign(max_seconds,20).
9.023/9.023	
9.023/9.023	formulas(assumptions).
9.023/9.023	->*_s0(x,x) # label(reflexivity).
9.023/9.023	->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity).
9.023/9.023	->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence).
9.023/9.023	->_s0(a,c) # label(replacement).
9.023/9.023	->_s0(a,d) # label(replacement).
9.023/9.023	->*_s0(x2,c) -> ->_s0(f(x2),x2) # label(replacement).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	formulas(goals).
9.023/9.023	(exists x2 ->*_s0(x2,c)) # label(goal).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	============================== end of input ==========================
9.023/9.023	
9.023/9.023	============================== PROCESS NON-CLAUSAL FORMULAS ==========
9.023/9.023	
9.023/9.023	% Formulas that are not ordinary clauses:
9.023/9.023	1 ->_s0(x,y) & ->*_s0(y,z) -> ->*_s0(x,z) # label(transitivity) # label(non_clause).  [assumption].
9.023/9.023	2 ->_s0(x1,y) -> ->_s0(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
9.023/9.023	3 ->*_s0(x2,c) -> ->_s0(f(x2),x2) # label(replacement) # label(non_clause).  [assumption].
9.023/9.023	4 (exists x2 ->*_s0(x2,c)) # label(goal) # label(non_clause) # label(goal).  [goal].
9.023/9.023	
9.023/9.023	============================== end of process non-clausal formulas ===
9.023/9.023	
9.023/9.023	============================== PROCESS INITIAL CLAUSES ===============
9.023/9.023	
9.023/9.023	% Clauses before input processing:
9.023/9.023	
9.023/9.023	formulas(usable).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	formulas(sos).
9.023/9.023	->*_s0(x,x) # label(reflexivity).  [assumption].
9.023/9.023	-->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
9.023/9.023	-->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(2)].
9.023/9.023	->_s0(a,c) # label(replacement).  [assumption].
9.023/9.023	->_s0(a,d) # label(replacement).  [assumption].
9.023/9.023	-->*_s0(x,c) | ->_s0(f(x),x) # label(replacement).  [clausify(3)].
9.023/9.023	-->*_s0(x,c) # label(goal).  [deny(4)].
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	formulas(demodulators).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	============================== PREDICATE ELIMINATION =================
9.023/9.023	
9.023/9.023	No predicates eliminated.
9.023/9.023	
9.023/9.023	============================== end predicate elimination =============
9.023/9.023	
9.023/9.023	Auto_denials:
9.023/9.023	  % copying label goal to answer in negative clause
9.023/9.023	
9.023/9.023	Term ordering decisions:
9.023/9.023	Predicate symbol precedence:  predicate_order([ ->_s0, ->*_s0 ]).
9.023/9.023	Function symbol precedence:  function_order([ a, c, d, f ]).
9.023/9.023	After inverse_order:  (no changes).
9.023/9.023	Unfolding symbols: (none).
9.023/9.023	
9.023/9.023	Auto_inference settings:
9.023/9.023	  % set(neg_binary_resolution).  % (HNE depth_diff=-2)
9.023/9.023	  % clear(ordered_res).  % (HNE depth_diff=-2)
9.023/9.023	  % set(ur_resolution).  % (HNE depth_diff=-2)
9.023/9.023	    % set(ur_resolution) -> set(pos_ur_resolution).
9.023/9.023	    % set(ur_resolution) -> set(neg_ur_resolution).
9.023/9.023	
9.023/9.023	Auto_process settings:  (no changes).
9.023/9.023	
9.023/9.023	kept:      5 ->*_s0(x,x) # label(reflexivity).  [assumption].
9.023/9.023	kept:      6 -->_s0(x,y) | -->*_s0(y,z) | ->*_s0(x,z) # label(transitivity).  [clausify(1)].
9.023/9.023	kept:      7 -->_s0(x,y) | ->_s0(f(x),f(y)) # label(congruence).  [clausify(2)].
9.023/9.023	kept:      8 ->_s0(a,c) # label(replacement).  [assumption].
9.023/9.023	kept:      9 ->_s0(a,d) # label(replacement).  [assumption].
9.023/9.023	kept:      10 -->*_s0(x,c) | ->_s0(f(x),x) # label(replacement).  [clausify(3)].
9.023/9.023	kept:      11 -->*_s0(x,c) # label(goal) # answer(goal).  [deny(4)].
9.023/9.023	
9.023/9.023	============================== PROOF =================================
9.023/9.023	
9.023/9.023	% Proof 1 at 0.00 (+ 0.00) seconds: goal.
9.023/9.023	% Length of proof is 4.
9.023/9.023	% Level of proof is 2.
9.023/9.023	% Maximum clause weight is 3.000.
9.023/9.023	% Given clauses 0.
9.023/9.023	
9.023/9.023	4 (exists x2 ->*_s0(x2,c)) # label(goal) # label(non_clause) # label(goal).  [goal].
9.023/9.023	5 ->*_s0(x,x) # label(reflexivity).  [assumption].
9.023/9.023	11 -->*_s0(x,c) # label(goal) # answer(goal).  [deny(4)].
9.023/9.023	12 $F # answer(goal).  [resolve(11,a,5,a)].
9.023/9.023	
9.023/9.023	============================== end of proof ==========================
9.023/9.023	
9.023/9.023	============================== STATISTICS ============================
9.023/9.023	
9.023/9.023	Given=0. Generated=7. Kept=7. proofs=1.
9.023/9.023	Usable=0. Sos=0. Demods=0. Limbo=6, Disabled=7. Hints=0.
9.023/9.023	Kept_by_rule=0, Deleted_by_rule=0.
9.023/9.023	Forward_subsumed=0. Back_subsumed=0.
9.023/9.023	Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0.
9.023/9.023	New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=0.
9.023/9.023	Demod_attempts=0. Demod_rewrites=0.
9.023/9.023	Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0.
9.023/9.023	Nonunit_fsub_feature_tests=0. Nonunit_bsub_feature_tests=0.
9.023/9.023	Megabytes=0.04.
9.023/9.023	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
9.023/9.023	
9.023/9.023	============================== end of statistics =====================
9.023/9.023	
9.023/9.023	============================== end of search =========================
9.023/9.023	
9.023/9.023	THEOREM PROVED
9.023/9.023	
9.023/9.023	Exiting with 1 proof.
9.023/9.023	
9.023/9.023	Process 48558 exit (max_proofs) Wed Jul 14 10:47:54 2021
9.023/9.023	
9.023/9.023	
9.023/9.023	The problem is feasible.
9.023/9.023	
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	Confluence Problem:
9.023/9.023	(VAR x:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	
9.023/9.023	Critical Pairs Processor:
9.023/9.023	-> Rules:
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	-> Vars:
9.023/9.023	"x"
9.023/9.023	-> FVars:
9.023/9.023	"x2"
9.023/9.023	-> PVars:
9.023/9.023	"x": ["x2"]
9.023/9.023	
9.023/9.023	-> Rlps:
9.023/9.023	crule: a -> c, id: 1, possubterms: a-> []
9.023/9.023	crule: a -> d, id: 2, possubterms: a-> []
9.023/9.023	crule: f(x2:S) -> x2:S | x2:S ->* c, id: 3, possubterms: f(x2:S)-> []
9.023/9.023	
9.023/9.023	-> Unifications:
9.023/9.023	R2 unifies with  R1 at  p: [], l: a, lp: a, conds: {}, sig: {}, l': a, r: d, r': c
9.023/9.023	
9.023/9.023	-> Critical pairs info:
9.023/9.023	<c,d>   =>  Not trivial, Overlay, N1
9.023/9.023	
9.023/9.023	-> Problem conclusions:
9.023/9.023	 Left linear, Right linear, Linear
9.023/9.023	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
9.023/9.023	 CTRS Type: 1
9.023/9.023	 Deterministic, Strongly deterministic
9.023/9.023	 Oriented CTRS, Properly oriented CTRS, Not join CTRS
9.023/9.023	 Maybe right-stable CTRS, Overlay CTRS
9.023/9.023	 Maybe normal CTRS, Maybe almost normal CTRS
9.023/9.023	 Maybe terminating CTRS, Maybe joinable CCPs
9.023/9.023	 Maybe level confluent
9.023/9.023	 Maybe confluent
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	Confluence Problem:
9.023/9.023	(VAR x:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)
9.023/9.023	Critical Pairs:
9.023/9.023	<c,d>   =>  Not trivial, Overlay, N1
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	
9.023/9.023	Conditional Critical Pairs Distributor Processor
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	Confluence Problem:
9.023/9.023	(VAR x:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)
9.023/9.023	Critical Pairs:
9.023/9.023	<c,d>   =>  Not trivial, Overlay, N1
9.023/9.023	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
9.023/9.023	
9.023/9.023	InfChecker Different Ground and Normal No Conditions CCP Terms Processor:
9.023/9.023	Proof:
9.023/9.023	YES
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Infeasibility Problem:
9.023/9.023	[(VAR vNonEmpty:S x:S y:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)]
9.023/9.023	
9.023/9.023	Infeasibility Conditions:
9.023/9.023	c -> y:S
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Obtaining a model using Mace4:
9.023/9.023	
9.023/9.023	 -> Usable Rules:
9.023/9.023	Empty
9.023/9.023	
9.023/9.023	 -> Mace4 Output:
9.023/9.023	============================== Mace4 =================================
9.023/9.023	Mace4 (64) version 2009-11A, November 2009.
9.023/9.023	Process 48604 was started by ubuntu on ubuntu,
9.023/9.023	Wed Jul 14 10:47:54 2021
9.023/9.023	The command was "./mace4 -c -f /tmp/mace448572-2.in".
9.023/9.023	============================== end of head ===========================
9.023/9.023	
9.023/9.023	============================== INPUT =================================
9.023/9.023	
9.023/9.023	% Reading from file /tmp/mace448572-2.in
9.023/9.023	
9.023/9.023	assign(max_seconds,6).
9.023/9.023	
9.023/9.023	formulas(assumptions).
9.023/9.023	->(x1,y) -> ->(f(x1),f(y)) # label(congruence).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	formulas(goals).
9.023/9.023	(exists x2 ->(c,x2)) # label(goal).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	============================== end of input ==========================
9.023/9.023	
9.023/9.023	============================== PROCESS NON-CLAUSAL FORMULAS ==========
9.023/9.023	
9.023/9.023	% Formulas that are not ordinary clauses:
9.023/9.023	1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
9.023/9.023	2 (exists x2 ->(c,x2)) # label(goal) # label(non_clause) # label(goal).  [goal].
9.023/9.023	
9.023/9.023	============================== end of process non-clausal formulas ===
9.023/9.023	
9.023/9.023	============================== CLAUSES FOR SEARCH ====================
9.023/9.023	
9.023/9.023	formulas(mace4_clauses).
9.023/9.023	-->(x,y) | ->(f(x),f(y)) # label(congruence).
9.023/9.023	-->(c,x) # label(goal).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	============================== end of clauses for search =============
9.023/9.023	
9.023/9.023	% There are no natural numbers in the input.
9.023/9.023	
9.023/9.023	============================== DOMAIN SIZE 2 =========================
9.023/9.023	
9.023/9.023	============================== MODEL =================================
9.023/9.023	
9.023/9.023	interpretation( 2, [number=1, seconds=0], [
9.023/9.023	
9.023/9.023	        function(c, [ 0 ]),
9.023/9.023	
9.023/9.023	        function(f(_), [ 0, 0 ]),
9.023/9.023	
9.023/9.023	        relation(->(_,_), [
9.023/9.023				   0, 0,
9.023/9.023				   0, 0 ])
9.023/9.023	]).
9.023/9.023	
9.023/9.023	============================== end of model ==========================
9.023/9.023	
9.023/9.023	============================== STATISTICS ============================
9.023/9.023	
9.023/9.023	For domain size 2.
9.023/9.023	
9.023/9.023	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
9.023/9.023	Ground clauses: seen=6, kept=6.
9.023/9.023	Selections=3, assignments=3, propagations=4, current_models=1.
9.023/9.023	Rewrite_terms=10, rewrite_bools=8, indexes=2.
9.023/9.023	Rules_from_neg_clauses=0, cross_offs=0.
9.023/9.023	
9.023/9.023	============================== end of statistics =====================
9.023/9.023	
9.023/9.023	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
9.023/9.023	
9.023/9.023	Exiting with 1 model.
9.023/9.023	
9.023/9.023	Process 48604 exit (max_models) Wed Jul 14 10:47:54 2021
9.023/9.023	The process finished Wed Jul 14 10:47:54 2021
9.023/9.023	
9.023/9.023	
9.023/9.023	Mace4 cooked interpretation:
9.023/9.023	
9.023/9.023	
9.023/9.023	
9.023/9.023	The problem is infeasible.
9.023/9.023	YES
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Infeasibility Problem:
9.023/9.023	[(VAR vNonEmpty:S x:S)
9.023/9.023	(STRATEGY CONTEXTSENSITIVE
9.023/9.023	(a)
9.023/9.023	(f 1)
9.023/9.023	(c)
9.023/9.023	(d)
9.023/9.023	(fSNonEmpty)
9.023/9.023	)
9.023/9.023	(RULES
9.023/9.023	a -> c
9.023/9.023	a -> d
9.023/9.023	f(x:S) -> x:S | x:S ->* c
9.023/9.023	)]
9.023/9.023	
9.023/9.023	Infeasibility Conditions:
9.023/9.023	d -> x:S
9.023/9.023	
9.023/9.023	Problem 1:
9.023/9.023	
9.023/9.023	Obtaining a model using Mace4:
9.023/9.023	
9.023/9.023	 -> Usable Rules:
9.023/9.023	Empty
9.023/9.023	
9.023/9.023	 -> Mace4 Output:
9.023/9.023	============================== Mace4 =================================
9.023/9.023	Mace4 (64) version 2009-11A, November 2009.
9.023/9.023	Process 48637 was started by ubuntu on ubuntu,
9.023/9.023	Wed Jul 14 10:47:56 2021
9.023/9.023	The command was "./mace4 -c -f /tmp/mace448625-2.in".
9.023/9.023	============================== end of head ===========================
9.023/9.023	
9.023/9.023	============================== INPUT =================================
9.023/9.023	
9.023/9.023	% Reading from file /tmp/mace448625-2.in
9.023/9.023	
9.023/9.023	assign(max_seconds,6).
9.023/9.023	
9.023/9.023	formulas(assumptions).
9.023/9.023	->(x1,y) -> ->(f(x1),f(y)) # label(congruence).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	formulas(goals).
9.023/9.023	(exists x1 ->(d,x1)) # label(goal).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	============================== end of input ==========================
9.023/9.023	
9.023/9.023	============================== PROCESS NON-CLAUSAL FORMULAS ==========
9.023/9.023	
9.023/9.023	% Formulas that are not ordinary clauses:
9.023/9.023	1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause).  [assumption].
9.023/9.023	2 (exists x1 ->(d,x1)) # label(goal) # label(non_clause) # label(goal).  [goal].
9.023/9.023	
9.023/9.023	============================== end of process non-clausal formulas ===
9.023/9.023	
9.023/9.023	============================== CLAUSES FOR SEARCH ====================
9.023/9.023	
9.023/9.023	formulas(mace4_clauses).
9.023/9.023	-->(x,y) | ->(f(x),f(y)) # label(congruence).
9.023/9.023	-->(d,x) # label(goal).
9.023/9.023	end_of_list.
9.023/9.023	
9.023/9.023	============================== end of clauses for search =============
9.023/9.023	
9.023/9.023	% There are no natural numbers in the input.
9.023/9.023	
9.023/9.023	============================== DOMAIN SIZE 2 =========================
9.023/9.023	
9.023/9.023	============================== MODEL =================================
9.023/9.023	
9.023/9.023	interpretation( 2, [number=1, seconds=0], [
9.023/9.023	
9.023/9.023	        function(d, [ 0 ]),
9.023/9.023	
9.023/9.023	        function(f(_), [ 0, 0 ]),
9.023/9.023	
9.023/9.023	        relation(->(_,_), [
9.023/9.023				   0, 0,
9.023/9.023				   0, 0 ])
9.023/9.023	]).
9.023/9.023	
9.023/9.023	============================== end of model ==========================
9.023/9.023	
9.023/9.023	============================== STATISTICS ============================
9.023/9.023	
9.023/9.023	For domain size 2.
9.023/9.023	
9.023/9.023	Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds).
9.023/9.023	Ground clauses: seen=6, kept=6.
9.023/9.023	Selections=3, assignments=3, propagations=4, current_models=1.
9.023/9.023	Rewrite_terms=10, rewrite_bools=8, indexes=2.
9.023/9.023	Rules_from_neg_clauses=0, cross_offs=0.
9.023/9.023	
9.023/9.023	============================== end of statistics =====================
9.023/9.023	
9.023/9.023	User_CPU=0.00, System_CPU=0.00, Wall_clock=0.
9.023/9.023	
9.023/9.023	Exiting with 1 model.
9.023/9.023	
9.023/9.023	Process 48637 exit (max_models) Wed Jul 14 10:47:56 2021
9.023/9.023	The process finished Wed Jul 14 10:47:56 2021
9.023/9.023	
9.023/9.023	
9.023/9.023	Mace4 cooked interpretation:
9.023/9.023	
9.023/9.023	
9.023/9.023	
9.023/9.023	The problem is infeasible.
9.023/9.023	
9.023/9.023	
9.023/9.023	The problem is not joinable.
9.023/9.023	10.07user 0.47system 0:09.23elapsed 114%CPU (0avgtext+0avgdata 131084maxresident)k
9.023/9.023	0inputs+0outputs (0major+220667minor)pagefaults 0swaps