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 | x0 \-> y1 => Not trivial, Not overlay, Proper, NW0, N1 7.04/23.03 | 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 | x0 \-> y1 => Not trivial, Not overlay, Proper, NW0, N1 7.06/23.05 | x0 \-> y1 => Not trivial, Not overlay, Proper, NW0, N2 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N1 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N2 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N3 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N4 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N5 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N6 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N7 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N8 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N9 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N10 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N11 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N12 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N13 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N14 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N15 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N16 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N17 7.06/23.05 => 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 => Not trivial, Overlay, Proper, NW0, N1 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N2 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N3 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N4 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N5 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N6 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N7 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N8 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N9 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N10 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N11 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N12 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N13 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N14 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N15 7.06/23.05 | x0 \-> y1 => Not trivial, Not overlay, Proper, NW0, N16 7.06/23.05 => Not trivial, Not overlay, Proper, NW0, N17 7.06/23.05 => Not trivial, Overlay, Proper, NW0, N18 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N19 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N20 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N21 7.06/23.06 | x0 \-> y1 => Not trivial, Not overlay, Proper, NW0, N22 7.06/23.06 => Not trivial, Overlay, Proper, NW0, N23 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N24 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N25 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N26 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N27 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N28 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N29 7.06/23.06 => Not trivial, Not overlay, Proper, NW0, N30 7.06/23.06 => 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 | 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_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