7.04/23.03	NO
7.04/23.03	
7.04/23.03	Problem 1: 
7.04/23.03	
7.04/23.03	
7.04/23.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.04/23.03	Confluence Problem:
7.04/23.03	(VAR vNonEmpty x x0 y z)
7.04/23.03	(REPLACEMENT-MAP
7.04/23.03	(*top*_0 1)
7.04/23.03	(f_0 1, 2)
7.04/23.03	(f_1)
7.04/23.03	(a_1)
7.04/23.03	(c_0)
7.04/23.03	(fSNonEmpty)
7.04/23.03	)
7.04/23.03	(RULES
7.04/23.03	*top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.04/23.03	f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	f_1(f_0(x,y),z) -> c_0
7.04/23.03	f_1(f_1(x,y),z) -> c_0
7.04/23.03	f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.04/23.03	f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.04/23.03	f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.04/23.03	f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.04/23.03	)
7.04/23.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.04/23.03	
7.04/23.03	
7.04/23.03	Problem 1: 
7.04/23.03	
7.04/23.03	Problem 1: 
7.04/23.03	CS-TRS Procedure:
7.04/23.03	R is a CS-TRS
7.04/23.03	
7.04/23.03	Problem 1: 
7.04/23.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.04/23.03	Confluence Problem:
7.04/23.03	(VAR vNonEmpty x x0 y z)
7.04/23.03	(REPLACEMENT-MAP
7.04/23.03	(*top*_0 1)
7.04/23.03	(f_0 1, 2)
7.04/23.03	(f_1)
7.04/23.03	(a_1)
7.04/23.03	(c_0)
7.04/23.03	(fSNonEmpty)
7.04/23.03	)
7.04/23.03	(RULES
7.04/23.03	*top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.04/23.03	f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	f_1(f_0(x,y),z) -> c_0
7.04/23.03	f_1(f_1(x,y),z) -> c_0
7.04/23.03	f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.04/23.03	f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.04/23.03	f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.04/23.03	f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.04/23.03	)
7.04/23.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.04/23.03	
7.04/23.03	LH u-Critical Pairs Procedure [JLAMP21-Def12]:
7.04/23.03	->LH u-Critical Pair:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Var x => x0
7.04/23.03	 Var y => y1
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 s => f_0(a_1,y1)
7.04/23.03	 t => f_1(f_0(a_1,a_1),x0)
7.04/23.03	 C => x0 \-> y1 
7.04/23.03	 NW => 2 
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Var x => x0
7.04/23.03	 Var y => y1
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 s => f_0(y1,a_1)
7.04/23.03	 t => f_1(x0,f_0(a_1,a_1))
7.04/23.03	 C => x0 \-> y1 
7.04/23.03	 NW => 2 
7.04/23.03	
7.04/23.03	
7.04/23.03	Problem 1: 
7.04/23.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.04/23.03	Confluence Problem:
7.04/23.03	(VAR vNonEmpty x x0 y z y1)
7.04/23.03	(REPLACEMENT-MAP
7.04/23.03	(*top*_0 1)
7.04/23.03	(f_0 1, 2)
7.04/23.03	(f_1)
7.04/23.03	(a_1)
7.04/23.03	(c_0)
7.04/23.03	(fSNonEmpty)
7.04/23.03	)
7.04/23.03	(RULES
7.04/23.03	*top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.04/23.03	f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	f_1(f_0(x,y),z) -> c_0
7.04/23.03	f_1(f_1(x,y),z) -> c_0
7.04/23.03	f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.04/23.03	f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.04/23.03	f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.04/23.03	f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.04/23.03	)
7.04/23.03	Critical Pairs:
7.04/23.03	<f_0(a_1,y1),f_1(f_0(a_1,a_1),x0)> | x0 \-> y1  =>  Not trivial, Not overlay, Proper, NW0, N1
7.04/23.03	<f_0(y1,a_1),f_1(x0,f_0(a_1,a_1))> | x0 \-> y1  =>  Not trivial, Not overlay, Proper, NW0, N2
7.04/23.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.04/23.03	
7.04/23.03	LH u-Critical Pair Instances Procedure [JLAMP21]:
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 1 (l' :-> r') => *top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> *top*_0(a_1)}
7.04/23.03	 s => f_0(a_1,*top*_0(f_0(a_1,a_1)))
7.04/23.03	 t => f_1(f_0(a_1,a_1),*top*_0(a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 2 (l' :-> r') => f_0(a_1,x0') -> f_1(f_0(a_1,a_1),x0')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_0(a_1,x0')}
7.04/23.03	 s => f_0(a_1,f_1(f_0(a_1,a_1),x0'))
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_0(a_1,x0'))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 3 (l' :-> r') => f_0(x0',a_1) -> f_1(x0',f_0(a_1,a_1))
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_0(x0',a_1)}
7.04/23.03	 s => f_0(a_1,f_1(x0',f_0(a_1,a_1)))
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_0(x0',a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 4 (l' :-> r') => f_1(f_0(x',y'),z') -> c_0
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_1(f_0(x',y'),z')}
7.04/23.03	 s => f_0(a_1,c_0)
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_1(f_0(x',y'),z'))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 5 (l' :-> r') => f_1(f_1(x',y'),z') -> c_0
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_1(f_1(x',y'),z')}
7.04/23.03	 s => f_0(a_1,c_0)
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_1(f_1(x',y'),z'))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 6 (l' :-> r') => f_1(x',f_0(y',z')) -> f_1(f_0(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_0(y',z'))}
7.04/23.03	 s => f_0(a_1,f_1(f_0(x',y'),z'))
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_1(x',f_0(y',z')))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 7 (l' :-> r') => f_1(x',f_0(y',z')) -> f_1(f_1(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_0(y',z'))}
7.04/23.03	 s => f_0(a_1,f_1(f_1(x',y'),z'))
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_1(x',f_0(y',z')))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 8 (l' :-> r') => f_1(x',f_1(y',z')) -> f_1(f_0(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_1(y',z'))}
7.04/23.03	 s => f_0(a_1,f_1(f_0(x',y'),z'))
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_1(x',f_1(y',z')))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 2 (l :-> r) => f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.04/23.03	 Rule 9 (l' :-> r') => f_1(x',f_1(y',z')) -> f_1(f_1(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [2]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_1(y',z'))}
7.04/23.03	 s => f_0(a_1,f_1(f_1(x',y'),z'))
7.04/23.03	 t => f_1(f_0(a_1,a_1),f_1(x',f_1(y',z')))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 1 (l' :-> r') => *top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> *top*_0(a_1)}
7.04/23.03	 s => f_0(*top*_0(f_0(a_1,a_1)),a_1)
7.04/23.03	 t => f_1(*top*_0(a_1),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 2 (l' :-> r') => f_0(a_1,x0') -> f_1(f_0(a_1,a_1),x0')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_0(a_1,x0')}
7.04/23.03	 s => f_0(f_1(f_0(a_1,a_1),x0'),a_1)
7.04/23.03	 t => f_1(f_0(a_1,x0'),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 3 (l' :-> r') => f_0(x0',a_1) -> f_1(x0',f_0(a_1,a_1))
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_0(x0',a_1)}
7.04/23.03	 s => f_0(f_1(x0',f_0(a_1,a_1)),a_1)
7.04/23.03	 t => f_1(f_0(x0',a_1),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 4 (l' :-> r') => f_1(f_0(x',y'),z') -> c_0
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_1(f_0(x',y'),z')}
7.04/23.03	 s => f_0(c_0,a_1)
7.04/23.03	 t => f_1(f_1(f_0(x',y'),z'),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 5 (l' :-> r') => f_1(f_1(x',y'),z') -> c_0
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_1(f_1(x',y'),z')}
7.04/23.03	 s => f_0(c_0,a_1)
7.04/23.03	 t => f_1(f_1(f_1(x',y'),z'),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 6 (l' :-> r') => f_1(x',f_0(y',z')) -> f_1(f_0(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_0(y',z'))}
7.04/23.03	 s => f_0(f_1(f_0(x',y'),z'),a_1)
7.04/23.03	 t => f_1(f_1(x',f_0(y',z')),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 7 (l' :-> r') => f_1(x',f_0(y',z')) -> f_1(f_1(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_0(y',z'))}
7.04/23.03	 s => f_0(f_1(f_1(x',y'),z'),a_1)
7.04/23.03	 t => f_1(f_1(x',f_0(y',z')),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 8 (l' :-> r') => f_1(x',f_1(y',z')) -> f_1(f_0(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_1(y',z'))}
7.04/23.03	 s => f_0(f_1(f_0(x',y'),z'),a_1)
7.04/23.03	 t => f_1(f_1(x',f_1(y',z')),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	->LH u-Critical Pair Instance:
7.04/23.03	 Rule 3 (l :-> r) => f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.04/23.03	 Rule 9 (l' :-> r') => f_1(x',f_1(y',z')) -> f_1(f_1(x',y'),z')
7.04/23.03	 Var => x0
7.04/23.03	 Pos x0 in l => [1]
7.04/23.03	 Sigma => {x0 -> f_1(x',f_1(y',z'))}
7.04/23.03	 s => f_0(f_1(f_1(x',y'),z'),a_1)
7.04/23.03	 t => f_1(f_1(x',f_1(y',z')),f_0(a_1,a_1))
7.04/23.03	 NW => 0
7.04/23.03	
7.04/23.03	
7.04/23.03	Problem 1: 
7.04/23.03	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.04/23.03	Confluence Problem:
7.04/23.03	(VAR vNonEmpty x x0 y z y1)
7.04/23.03	(REPLACEMENT-MAP
7.04/23.03	(*top*_0 1)
7.04/23.03	(f_0 1, 2)
7.04/23.03	(f_1)
7.04/23.03	(a_1)
7.04/23.03	(c_0)
7.04/23.03	(fSNonEmpty)
7.06/23.05	)
7.06/23.05	(RULES
7.06/23.05	*top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.06/23.05	f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.06/23.05	f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.06/23.05	f_1(f_0(x,y),z) -> c_0
7.06/23.05	f_1(f_1(x,y),z) -> c_0
7.06/23.05	f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.06/23.05	f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.06/23.05	f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.06/23.05	f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.06/23.05	)
7.06/23.05	Critical Pairs:
7.06/23.05	<f_0(a_1,y1),f_1(f_0(a_1,a_1),x0)> | x0 \-> y1  =>  Not trivial, Not overlay, Proper, NW0, N1
7.06/23.05	<f_0(y1,a_1),f_1(x0,f_0(a_1,a_1))> | x0 \-> y1  =>  Not trivial, Not overlay, Proper, NW0, N2
7.06/23.05	<f_0(a_1,*top*_0(f_0(a_1,a_1))),f_1(f_0(a_1,a_1),*top*_0(a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N1
7.06/23.05	<f_0(a_1,f_1(f_0(a_1,a_1),x0')),f_1(f_0(a_1,a_1),f_0(a_1,x0'))>   =>  Not trivial, Not overlay, Proper, NW0, N2
7.06/23.05	<f_0(a_1,f_1(x0',f_0(a_1,a_1))),f_1(f_0(a_1,a_1),f_0(x0',a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N3
7.06/23.05	<f_0(a_1,c_0),f_1(f_0(a_1,a_1),f_1(f_0(x',y'),z'))>   =>  Not trivial, Not overlay, Proper, NW0, N4
7.06/23.05	<f_0(a_1,c_0),f_1(f_0(a_1,a_1),f_1(f_1(x',y'),z'))>   =>  Not trivial, Not overlay, Proper, NW0, N5
7.06/23.05	<f_0(a_1,f_1(f_0(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_0(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N6
7.06/23.05	<f_0(a_1,f_1(f_1(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_0(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N7
7.06/23.05	<f_0(a_1,f_1(f_0(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_1(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N8
7.06/23.05	<f_0(a_1,f_1(f_1(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_1(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N9
7.06/23.05	<f_0(*top*_0(f_0(a_1,a_1)),a_1),f_1(*top*_0(a_1),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N10
7.06/23.05	<f_0(f_1(f_0(a_1,a_1),x0'),a_1),f_1(f_0(a_1,x0'),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N11
7.06/23.05	<f_0(f_1(x0',f_0(a_1,a_1)),a_1),f_1(f_0(x0',a_1),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N12
7.06/23.05	<f_0(c_0,a_1),f_1(f_1(f_0(x',y'),z'),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N13
7.06/23.05	<f_0(c_0,a_1),f_1(f_1(f_1(x',y'),z'),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N14
7.06/23.05	<f_0(f_1(f_0(x',y'),z'),a_1),f_1(f_1(x',f_0(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N15
7.06/23.05	<f_0(f_1(f_1(x',y'),z'),a_1),f_1(f_1(x',f_0(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N16
7.06/23.05	<f_0(f_1(f_0(x',y'),z'),a_1),f_1(f_1(x',f_1(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N17
7.06/23.05	<f_0(f_1(f_1(x',y'),z'),a_1),f_1(f_1(x',f_1(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N18
7.06/23.05	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.06/23.05	
7.06/23.05	Huet Levy Ordered by Num of Vars and Symbs Procedure:
7.06/23.05	-> Rules:
7.06/23.05	 *top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.06/23.05	 f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.06/23.05	 f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.06/23.05	 f_1(f_0(x,y),z) -> c_0
7.06/23.05	 f_1(f_1(x,y),z) -> c_0
7.06/23.05	 f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.06/23.05	 f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.06/23.05	 f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.06/23.05	 f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.06/23.05	-> Vars:
7.06/23.05	 x0, x0, x, y, z, x, y, z, x, y, z, x, y, z, x, y, z, x, y, z
7.06/23.05	-> UVars:
7.06/23.05	 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
7.06/23.05	 (UV-RuleId: 2, UV-LActive: [x0], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [x0])
7.06/23.05	 (UV-RuleId: 3, UV-LActive: [x0], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [x0])
7.06/23.05	 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x, y, z], UV-RFrozen: [])
7.06/23.05	 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x, y, z], UV-RFrozen: [])
7.06/23.05	 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x, y, z], UV-RFrozen: [x, y, z])
7.06/23.05	 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x, y, z], UV-RFrozen: [x, y, z])
7.06/23.05	 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x, y, z], UV-RFrozen: [x, y, z])
7.06/23.05	 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x, y, z], UV-RFrozen: [x, y, z])
7.06/23.05	
7.06/23.05	-> Rlps:
7.06/23.05	 (rule: *top*_0(a_1) -> *top*_0(f_0(a_1,a_1)), id: 1, possubterms: *top*_0(a_1)->[], a_1->[1])
7.06/23.05	 (rule: f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0), id: 2, possubterms: f_0(a_1,x0)->[], a_1->[1])
7.06/23.05	 (rule: f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1)), id: 3, possubterms: f_0(x0,a_1)->[], a_1->[2])
7.06/23.05	 (rule: f_1(f_0(x,y),z) -> c_0, id: 4, possubterms: f_1(f_0(x,y),z)->[])
7.06/23.05	 (rule: f_1(f_1(x,y),z) -> c_0, id: 5, possubterms: f_1(f_1(x,y),z)->[])
7.06/23.05	 (rule: f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z), id: 6, possubterms: f_1(x,f_0(y,z))->[])
7.06/23.05	 (rule: f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z), id: 7, possubterms: f_1(x,f_0(y,z))->[])
7.06/23.05	 (rule: f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z), id: 8, possubterms: f_1(x,f_1(y,z))->[])
7.06/23.05	 (rule: f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z), id: 9, possubterms: f_1(x,f_1(y,z))->[])
7.06/23.05	
7.06/23.05	-> Unifications:
7.06/23.05	(R3 unifies with R2 at p: [], l: f_0(x0,a_1), lp: f_0(x0,a_1), sig: {x0 -> a_1,x0' -> a_1}, l': f_0(a_1,x0'), r: f_1(x0,f_0(a_1,a_1)), r': f_1(f_0(a_1,a_1),x0'))
7.06/23.05	(R6 unifies with R4 at p: [], l: f_1(x,f_0(y,z)), lp: f_1(x,f_0(y,z)), sig: {x -> f_0(x',y'),z' -> f_0(y,z)}, l': f_1(f_0(x',y'),z'), r: f_1(f_0(x,y),z), r': c_0)
7.06/23.05	(R6 unifies with R5 at p: [], l: f_1(x,f_0(y,z)), lp: f_1(x,f_0(y,z)), sig: {x -> f_1(x',y'),z' -> f_0(y,z)}, l': f_1(f_1(x',y'),z'), r: f_1(f_0(x,y),z), r': c_0)
7.06/23.05	(R7 unifies with R4 at p: [], l: f_1(x,f_0(y,z)), lp: f_1(x,f_0(y,z)), sig: {x -> f_0(x',y'),z' -> f_0(y,z)}, l': f_1(f_0(x',y'),z'), r: f_1(f_1(x,y),z), r': c_0)
7.06/23.05	(R7 unifies with R5 at p: [], l: f_1(x,f_0(y,z)), lp: f_1(x,f_0(y,z)), sig: {x -> f_1(x',y'),z' -> f_0(y,z)}, l': f_1(f_1(x',y'),z'), r: f_1(f_1(x,y),z), r': c_0)
7.06/23.05	(R7 unifies with R6 at p: [], l: f_1(x,f_0(y,z)), lp: f_1(x,f_0(y,z)), sig: {x -> x',y -> y',z -> z'}, l': f_1(x',f_0(y',z')), r: f_1(f_1(x,y),z), r': f_1(f_0(x',y'),z'))
7.06/23.05	(R8 unifies with R4 at p: [], l: f_1(x,f_1(y,z)), lp: f_1(x,f_1(y,z)), sig: {x -> f_0(x',y'),z' -> f_1(y,z)}, l': f_1(f_0(x',y'),z'), r: f_1(f_0(x,y),z), r': c_0)
7.06/23.05	(R8 unifies with R5 at p: [], l: f_1(x,f_1(y,z)), lp: f_1(x,f_1(y,z)), sig: {x -> f_1(x',y'),z' -> f_1(y,z)}, l': f_1(f_1(x',y'),z'), r: f_1(f_0(x,y),z), r': c_0)
7.06/23.05	(R9 unifies with R4 at p: [], l: f_1(x,f_1(y,z)), lp: f_1(x,f_1(y,z)), sig: {x -> f_0(x',y'),z' -> f_1(y,z)}, l': f_1(f_0(x',y'),z'), r: f_1(f_1(x,y),z), r': c_0)
7.06/23.05	(R9 unifies with R5 at p: [], l: f_1(x,f_1(y,z)), lp: f_1(x,f_1(y,z)), sig: {x -> f_1(x',y'),z' -> f_1(y,z)}, l': f_1(f_1(x',y'),z'), r: f_1(f_1(x,y),z), r': c_0)
7.06/23.05	(R9 unifies with R8 at p: [], l: f_1(x,f_1(y,z)), lp: f_1(x,f_1(y,z)), sig: {x -> x',y -> y',z -> z'}, l': f_1(x',f_1(y',z')), r: f_1(f_1(x,y),z), r': f_1(f_0(x',y'),z'))
7.06/23.05	
7.06/23.05	-> Critical pairs info:
7.06/23.05	<c_0,f_1(f_1(f_1(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N1
7.06/23.05	<f_1(f_0(a_1,a_1),a_1),f_1(a_1,f_0(a_1,a_1))>   =>  Not trivial, Overlay, Proper, NW0, N2
7.06/23.05	<c_0,f_1(f_1(f_1(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N3
7.06/23.05	<f_0(*top*_0(f_0(a_1,a_1)),a_1),f_1(*top*_0(a_1),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N4
7.06/23.05	<c_0,f_1(f_0(f_0(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N5
7.06/23.05	<c_0,f_1(f_1(f_0(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N6
7.06/23.05	<c_0,f_1(f_0(f_1(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N7
7.06/23.05	<f_0(a_1,*top*_0(f_0(a_1,a_1))),f_1(f_0(a_1,a_1),*top*_0(a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N8
7.06/23.05	<c_0,f_1(f_0(f_0(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N9
7.06/23.05	<c_0,f_1(f_1(f_0(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N10
7.06/23.05	<c_0,f_1(f_0(f_1(x',y'),y),z)>   =>  Not trivial, Overlay, Proper, NW0, N11
7.06/23.05	<f_0(a_1,f_1(f_0(a_1,a_1),x0')),f_1(f_0(a_1,a_1),f_0(a_1,x0'))>   =>  Not trivial, Not overlay, Proper, NW0, N12
7.06/23.05	<f_0(a_1,f_1(x0',f_0(a_1,a_1))),f_1(f_0(a_1,a_1),f_0(x0',a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N13
7.06/23.05	<f_0(f_1(x0',f_0(a_1,a_1)),a_1),f_1(f_0(x0',a_1),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N14
7.06/23.05	<f_0(f_1(f_0(a_1,a_1),x0'),a_1),f_1(f_0(a_1,x0'),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N15
7.06/23.05	<f_0(y1,a_1),f_1(x0,f_0(a_1,a_1))> | x0 \-> y1  =>  Not trivial, Not overlay, Proper, NW0, N16
7.06/23.05	<f_0(c_0,a_1),f_1(f_1(f_0(x',y'),z'),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N17
7.06/23.05	<f_1(f_0(x',y'),z'),f_1(f_1(x',y'),z')>   =>  Not trivial, Overlay, Proper, NW0, N18
7.06/23.06	<f_0(a_1,c_0),f_1(f_0(a_1,a_1),f_1(f_0(x',y'),z'))>   =>  Not trivial, Not overlay, Proper, NW0, N19
7.06/23.06	<f_0(a_1,c_0),f_1(f_0(a_1,a_1),f_1(f_1(x',y'),z'))>   =>  Not trivial, Not overlay, Proper, NW0, N20
7.06/23.06	<f_0(c_0,a_1),f_1(f_1(f_1(x',y'),z'),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N21
7.06/23.06	<f_0(a_1,y1),f_1(f_0(a_1,a_1),x0)> | x0 \-> y1  =>  Not trivial, Not overlay, Proper, NW0, N22
7.06/23.06	<f_1(f_0(x',y'),z'),f_1(f_1(x',y'),z')>   =>  Not trivial, Overlay, Proper, NW0, N23
7.06/23.06	<f_0(f_1(f_1(x',y'),z'),a_1),f_1(f_1(x',f_1(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N24
7.06/23.06	<f_0(f_1(f_0(x',y'),z'),a_1),f_1(f_1(x',f_0(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N25
7.06/23.06	<f_0(a_1,f_1(f_0(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_1(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N26
7.06/23.06	<f_0(a_1,f_1(f_1(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_0(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N27
7.06/23.06	<f_0(f_1(f_1(x',y'),z'),a_1),f_1(f_1(x',f_0(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N28
7.06/23.06	<f_0(f_1(f_0(x',y'),z'),a_1),f_1(f_1(x',f_1(y',z')),f_0(a_1,a_1))>   =>  Not trivial, Not overlay, Proper, NW0, N29
7.06/23.06	<f_0(a_1,f_1(f_0(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_0(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N30
7.06/23.06	<f_0(a_1,f_1(f_1(x',y'),z')),f_1(f_0(a_1,a_1),f_1(x',f_1(y',z')))>   =>  Not trivial, Not overlay, Proper, NW0, N31
7.06/23.06	
7.06/23.06	-> Problem conclusions:
7.06/23.06	 Left linear, Right linear, Linear
7.06/23.06	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
7.06/23.06	 Not Huet-Levy confluent, Not Newman confluent
7.06/23.06	 R is a CS-TRS, Not left-homogeneous u-replacing variables
7.06/23.06	
7.06/23.06	
7.06/23.06	Problem 1: 
7.06/23.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.06/23.06	Confluence Problem:
7.06/23.06	(VAR x x0 y z y1 x' x0' y' z')
7.06/23.06	(REPLACEMENT-MAP
7.06/23.06	(*top*_0 1)
7.06/23.06	(f_0 1, 2)
7.06/23.06	(f_1)
7.06/23.06	(a_1)
7.06/23.06	(c_0)
7.06/23.06	(fSNonEmpty)
7.06/23.06	)
7.06/23.06	(RULES
7.06/23.06	*top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.06/23.06	f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.06/23.06	f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.06/23.06	f_1(f_0(x,y),z) -> c_0
7.06/23.06	f_1(f_1(x,y),z) -> c_0
7.06/23.06	f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.06/23.06	f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.06/23.06	f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.06/23.06	f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.06/23.06	)
7.06/23.06	Critical Pairs:
7.06/23.06	<f_0(y1,a_1),f_1(x0,f_0(a_1,a_1))> | x0 \-> y1  =>  Not trivial, Not overlay, Proper, NW0, N16
7.06/23.06	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
7.06/23.06	
7.06/23.06	No Convergence (JLAMP22,Prop56) InfChecker Procedure:
7.06/23.06	 
7.06/23.06	Substitution: {x0 -> f_1(c_x,f_0(c_y,c_z)), y1 -> f_1(f_1(c_x,c_y),c_z)} 
7.06/23.06	LHCP after substitution: <f_0(f_1(f_1(c_x,c_y),c_z),a_1),f_1(f_1(c_x,f_0(c_y,c_z)),f_0(a_1,a_1))> | f_1(c_x,f_0(c_y,c_z)) \-> f_1(f_1(c_x,c_y),c_z) 
7.06/23.06	Try number: 1
7.06/23.06	Infeasible convergence?
7.06/23.06	YES
7.06/23.06	
7.06/23.06	Problem 1: 
7.06/23.06	
7.06/23.06	Infeasibility Problem:
7.06/23.06	[(VAR vNonEmpty x x0 y z y1 x1 x01 z1 vNonEmpty)
7.06/23.06	(STRATEGY CONTEXTSENSITIVE
7.06/23.06	(f_0 1 2)
7.06/23.06	(f_1)
7.06/23.06	(*top*_0 1)
7.06/23.06	(a_1)
7.06/23.06	(c_0)
7.06/23.06	(c_x)
7.06/23.06	(c_y)
7.06/23.06	(c_z)
7.06/23.06	(c_z0)
7.06/23.06	(fSNonEmpty)
7.06/23.06	)
7.06/23.06	(RULES
7.06/23.06	f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.06/23.06	f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.06/23.06	f_1(f_0(x,y),z) -> c_0
7.06/23.06	f_1(f_1(x,y),z) -> c_0
7.06/23.06	f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.06/23.06	f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.06/23.06	f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.06/23.06	f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.06/23.06	*top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.06/23.06	)]
7.06/23.06	Infeasibility Conditions:
7.06/23.06	f_1(c_x,f_0(c_y,c_z)) \-> f_1(f_1(c_x,c_y),c_z), f_0(f_1(f_1(c_x,c_y),c_z),a_1) \->* c_z0, f_1(f_1(c_x,f_0(c_y,c_z)),f_0(a_1,a_1)) \->* c_z0
7.06/23.06	
7.06/23.06	Problem 1: 
7.06/23.06	
7.06/23.06	Obtaining a model using Mace4:
7.06/23.06	
7.06/23.06	 -> Usable Rules:
7.06/23.06	f_0(a_1,x0) -> f_1(f_0(a_1,a_1),x0)
7.06/23.06	f_0(x0,a_1) -> f_1(x0,f_0(a_1,a_1))
7.06/23.06	f_1(f_0(x,y),z) -> c_0
7.06/23.06	f_1(f_1(x,y),z) -> c_0
7.06/23.06	f_1(x,f_0(y,z)) -> f_1(f_0(x,y),z)
7.06/23.06	f_1(x,f_0(y,z)) -> f_1(f_1(x,y),z)
7.06/23.06	f_1(x,f_1(y,z)) -> f_1(f_0(x,y),z)
7.06/23.06	f_1(x,f_1(y,z)) -> f_1(f_1(x,y),z)
7.06/23.06	*top*_0(a_1) -> *top*_0(f_0(a_1,a_1))
7.06/23.06	
7.06/23.06	 -> Mace4 Output:
7.06/23.06	============================== Mace4 =================================
7.06/23.06	Mace4 (64) version 2009-11A, November 2009.
7.06/23.06	Process 5326 was started by sandbox2 on n088.star.cs.uiowa.edu,
7.06/23.06	Wed Jul 13 08:39:02 2022
7.06/23.06	The command was "./mace4 -c -f /tmp/mace45308.in".
7.06/23.06	============================== end of head ===========================
7.06/23.06	
7.06/23.06	============================== INPUT =================================
7.06/23.06	
7.06/23.06	% Reading from file /tmp/mace45308.in
7.06/23.06	
7.06/23.06	assign(max_seconds,10).
7.06/23.06	
7.06/23.06	formulas(assumptions).
7.06/23.06	\->(x1,y) -> \->(f_0(x1,x2),f_0(y,x2)) # label(cscongruence).
7.06/23.06	\->(x2,y) -> \->(f_0(x1,x2),f_0(x1,y)) # label(cscongruence).
7.06/23.06	\->(x1,y) -> \->(*top*_0(x1),*top*_0(y)) # label(cscongruence).
7.06/23.06	\->(f_0(a_1,x2),f_1(f_0(a_1,a_1),x2)) # label(csreplacement).
7.06/23.06	\->(f_0(x2,a_1),f_1(x2,f_0(a_1,a_1))) # label(csreplacement).
7.06/23.06	\->(f_1(f_0(x1,x3),x4),c_0) # label(csreplacement).
7.06/23.06	\->(f_1(f_1(x1,x3),x4),c_0) # label(csreplacement).
7.06/23.06	\->(f_1(x1,f_0(x3,x4)),f_1(f_0(x1,x3),x4)) # label(csreplacement).
7.06/23.06	\->(f_1(x1,f_0(x3,x4)),f_1(f_1(x1,x3),x4)) # label(csreplacement).
7.06/23.06	\->(f_1(x1,f_1(x3,x4)),f_1(f_0(x1,x3),x4)) # label(csreplacement).
7.06/23.06	\->(f_1(x1,f_1(x3,x4)),f_1(f_1(x1,x3),x4)) # label(csreplacement).
7.06/23.06	\->(*top*_0(a_1),*top*_0(f_0(a_1,a_1))) # label(csreplacement).
7.06/23.06	\->*(x,x) # label(csreflexivity).
7.06/23.06	\->(x,y) & \->*(y,z) -> \->*(x,z) # label(cstransitivity).
7.06/23.06	end_of_list.
7.06/23.06	
7.06/23.06	formulas(goals).
7.06/23.06	\->(f_1(c_x,f_0(c_y,c_z)),f_1(f_1(c_x,c_y),c_z)) & \->*(f_0(f_1(f_1(c_x,c_y),c_z),a_1),c_z0) & \->*(f_1(f_1(c_x,f_0(c_y,c_z)),f_0(a_1,a_1)),c_z0) # label(goal).
7.06/23.06	end_of_list.
7.06/23.06	
7.06/23.06	============================== end of input ==========================
7.06/23.06	
7.06/23.06	============================== PROCESS NON-CLAUSAL FORMULAS ==========
7.06/23.06	
7.06/23.06	% Formulas that are not ordinary clauses:
7.06/23.06	1 \->(x1,y) -> \->(f_0(x1,x2),f_0(y,x2)) # label(cscongruence) # label(non_clause).  [assumption].
7.06/23.06	2 \->(x2,y) -> \->(f_0(x1,x2),f_0(x1,y)) # label(cscongruence) # label(non_clause).  [assumption].
7.06/23.06	3 \->(x1,y) -> \->(*top*_0(x1),*top*_0(y)) # label(cscongruence) # label(non_clause).  [assumption].
7.06/23.06	4 \->(x,y) & \->*(y,z) -> \->*(x,z) # label(cstransitivity) # label(non_clause).  [assumption].
7.06/23.06	5 \->(f_1(c_x,f_0(c_y,c_z)),f_1(f_1(c_x,c_y),c_z)) & \->*(f_0(f_1(f_1(c_x,c_y),c_z),a_1),c_z0) & \->*(f_1(f_1(c_x,f_0(c_y,c_z)),f_0(a_1,a_1)),c_z0) # label(goal) # label(non_clause) # label(goal).  [goal].
7.06/23.06	
7.06/23.06	============================== end of process non-clausal formulas ===
7.06/23.06	
7.06/23.06	============================== CLAUSES FOR SEARCH ====================
7.06/23.06	
7.06/23.06	formulas(mace4_clauses).
7.06/23.06	-\->(x,y) | \->(f_0(x,z),f_0(y,z)) # label(cscongruence).
7.06/23.06	-\->(x,y) | \->(f_0(z,x),f_0(z,y)) # label(cscongruence).
7.06/23.06	-\->(x,y) | \->(*top*_0(x),*top*_0(y)) # label(cscongruence).
7.06/23.06	\->(f_0(a_1,x),f_1(f_0(a_1,a_1),x)) # label(csreplacement).
7.06/23.06	\->(f_0(x,a_1),f_1(x,f_0(a_1,a_1))) # label(csreplacement).
7.06/23.06	\->(f_1(f_0(x,y),z),c_0) # label(csreplacement).
7.06/23.06	\->(f_1(f_1(x,y),z),c_0) # label(csreplacement).
7.06/23.06	\->(f_1(x,f_0(y,z)),f_1(f_0(x,y),z)) # label(csreplacement).
7.06/23.06	\->(f_1(x,f_0(y,z)),f_1(f_1(x,y),z)) # label(csreplacement).
7.06/23.06	\->(f_1(x,f_1(y,z)),f_1(f_0(x,y),z)) # label(csreplacement).
7.06/23.06	\->(f_1(x,f_1(y,z)),f_1(f_1(x,y),z)) # label(csreplacement).
7.06/23.06	\->(*top*_0(a_1),*top*_0(f_0(a_1,a_1))) # label(csreplacement).
7.06/23.06	\->*(x,x) # label(csreflexivity).
7.06/23.06	-\->(x,y) | -\->*(y,z) | \->*(x,z) # label(cstransitivity).
7.06/23.06	-\->(f_1(c_x,f_0(c_y,c_z)),f_1(f_1(c_x,c_y),c_z)) | -\->*(f_0(f_1(f_1(c_x,c_y),c_z),a_1),c_z0) | -\->*(f_1(f_1(c_x,f_0(c_y,c_z)),f_0(a_1,a_1)),c_z0) # label(goal).
7.06/23.06	end_of_list.
7.06/23.06	
7.06/23.06	============================== end of clauses for search =============
7.06/23.06	
7.06/23.06	% There are no natural numbers in the input.
7.06/23.06	
7.06/23.06	============================== DOMAIN SIZE 2 =========================
7.06/23.06	
7.06/23.06	============================== MODEL =================================
7.06/23.06	
7.06/23.06	interpretation( 2, [number=1, seconds=0], [
7.06/23.06	
7.06/23.06	        function(c_z0, [ 0 ]),
7.06/23.06	
7.06/23.06	        function(a_1, [ 0 ]),
7.06/23.06	
7.06/23.06	        function(c_0, [ 1 ]),
7.06/23.06	
7.06/23.06	        function(c_x, [ 0 ]),
7.06/23.06	
7.06/23.06	        function(c_y, [ 0 ]),
7.06/23.06	
7.06/23.06	        function(c_z, [ 0 ]),
7.06/23.06	
7.06/23.06	        function(*top*_0(_), [ 0, 0 ]),
7.06/23.06	
7.06/23.06	        function(f_0(_,_), [
7.06/23.06				   0, 0,
7.06/23.06				   0, 0 ]),
7.06/23.06	
7.06/23.06	        function(f_1(_,_), [
7.06/23.06				   1, 1,
7.06/23.06				   1, 1 ]),
7.06/23.06	
7.06/23.06	        relation(\->*(_,_), [
7.06/23.06				   1, 1,
7.06/23.06				   0, 1 ]),
7.06/23.06	
7.06/23.06	        relation(\->(_,_), [
7.06/23.06				   1, 1,
7.06/23.06				   0, 1 ])
7.06/23.06	]).
7.06/23.06	
7.06/23.06	============================== end of model ==========================
7.06/23.06	
7.06/23.06	============================== STATISTICS ============================
7.06/23.06	
7.06/23.06	For domain size 2.
7.06/23.06	
7.06/23.06	Current CPU time: 0.00 seconds (total CPU time: 0.04 seconds).
7.06/23.06	Ground clauses: seen=84, kept=80.
7.06/23.06	Selections=5799, assignments=11587, propagations=3676, current_models=1.
7.06/23.06	Rewrite_terms=290565, rewrite_bools=144525, indexes=35258.
7.06/23.06	Rules_from_neg_clauses=365, cross_offs=365.
7.06/23.06	
7.06/23.06	============================== end of statistics =====================
7.06/23.06	
7.06/23.06	User_CPU=0.04, System_CPU=0.01, Wall_clock=1.
7.06/23.06	
7.06/23.06	Exiting with 1 model.
7.06/23.06	
7.06/23.06	Process 5326 exit (max_models) Wed Jul 13 08:39:03 2022
7.06/23.06	The process finished Wed Jul 13 08:39:03 2022
7.06/23.06	
7.06/23.06	
7.06/23.06	Mace4 cooked interpretation:
7.06/23.06	
7.06/23.06	
7.06/23.06	
7.06/23.06	The problem is infeasible.
7.06/23.06	
7.06/23.06	
7.06/23.06	The problem is not confluent.
7.06/41.60	EOF