0.00/0.01 NO 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 0.00/0.01 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR vNonEmpty X) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (c) 0.00/0.01 (f 1) 0.00/0.01 (h 1) 0.00/0.01 (d) 0.00/0.01 (fSNonEmpty) 0.00/0.01 (g) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 c(X) -> d(X) 0.00/0.01 f(f(X)) -> c(f(g(f(X)))) 0.00/0.01 h(X) -> c(d(X)) 0.00/0.01 ) 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 CS-TRS Procedure: 0.00/0.01 R is a CS-TRS 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR vNonEmpty X) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (c) 0.00/0.01 (f 1) 0.00/0.01 (h 1) 0.00/0.01 (d) 0.00/0.01 (fSNonEmpty) 0.00/0.01 (g) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 c(X) -> d(X) 0.00/0.01 f(f(X)) -> c(f(g(f(X)))) 0.00/0.01 h(X) -> c(d(X)) 0.00/0.01 ) 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 LH u-Critical Pair Instances Procedure [JLAMP21]: 0.00/0.01 ->LH u-Critical Pair Instance: 0.00/0.01 Rule 2 (l :-> r) => f(f(X)) -> c(f(g(f(X)))) 0.00/0.01 Rule 1 (l' :-> r') => c(X') -> d(X') 0.00/0.01 Var => X 0.00/0.01 Pos X in l => [1,1] 0.00/0.01 Sigma => {X -> c(X')} 0.00/0.01 s => f(f(d(X'))) 0.00/0.01 t => c(f(g(f(c(X'))))) 0.00/0.01 NW => 0 0.00/0.01 0.00/0.01 0.00/0.01 ->LH u-Critical Pair Instance: 0.00/0.01 Rule 2 (l :-> r) => f(f(X)) -> c(f(g(f(X)))) 0.00/0.01 Rule 2 (l' :-> r') => f(f(X')) -> c(f(g(f(X')))) 0.00/0.01 Var => X 0.00/0.01 Pos X in l => [1,1] 0.00/0.01 Sigma => {X -> f(f(X'))} 0.00/0.01 s => f(f(c(f(g(f(X')))))) 0.00/0.01 t => c(f(g(f(f(f(X')))))) 0.00/0.01 NW => 0 0.00/0.01 0.00/0.01 0.00/0.01 ->LH u-Critical Pair Instance: 0.00/0.01 Rule 2 (l :-> r) => f(f(X)) -> c(f(g(f(X)))) 0.00/0.01 Rule 3 (l' :-> r') => h(X') -> c(d(X')) 0.00/0.01 Var => X 0.00/0.01 Pos X in l => [1,1] 0.00/0.01 Sigma => {X -> h(X')} 0.00/0.01 s => f(f(c(d(X')))) 0.00/0.01 t => c(f(g(f(h(X'))))) 0.00/0.01 NW => 0 0.00/0.01 0.00/0.01 0.00/0.01 ->LH u-Critical Pair Instance: 0.00/0.01 Rule 3 (l :-> r) => h(X) -> c(d(X)) 0.00/0.01 Rule 1 (l' :-> r') => c(X') -> d(X') 0.00/0.01 Var => X 0.00/0.01 Pos X in l => [1] 0.00/0.01 Sigma => {X -> c(X')} 0.00/0.01 s => h(d(X')) 0.00/0.01 t => c(d(c(X'))) 0.00/0.01 NW => 0 0.00/0.01 0.00/0.01 0.00/0.01 ->LH u-Critical Pair Instance: 0.00/0.01 Rule 3 (l :-> r) => h(X) -> c(d(X)) 0.00/0.01 Rule 2 (l' :-> r') => f(f(X')) -> c(f(g(f(X')))) 0.00/0.01 Var => X 0.00/0.01 Pos X in l => [1] 0.00/0.01 Sigma => {X -> f(f(X'))} 0.00/0.01 s => h(c(f(g(f(X'))))) 0.00/0.01 t => c(d(f(f(X')))) 0.00/0.01 NW => 0 0.00/0.01 0.00/0.01 0.00/0.01 ->LH u-Critical Pair Instance: 0.00/0.01 Rule 3 (l :-> r) => h(X) -> c(d(X)) 0.00/0.01 Rule 3 (l' :-> r') => h(X') -> c(d(X')) 0.00/0.01 Var => X 0.00/0.01 Pos X in l => [1] 0.00/0.01 Sigma => {X -> h(X')} 0.00/0.01 s => h(c(d(X'))) 0.00/0.01 t => c(d(h(X'))) 0.00/0.01 NW => 0 0.00/0.01 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 Confluence Problem: 0.00/0.01 (VAR vNonEmpty X) 0.00/0.01 (REPLACEMENT-MAP 0.00/0.01 (c) 0.00/0.01 (f 1) 0.00/0.01 (h 1) 0.00/0.01 (d) 0.00/0.01 (fSNonEmpty) 0.00/0.01 (g) 0.00/0.01 ) 0.00/0.01 (RULES 0.00/0.01 c(X) -> d(X) 0.00/0.01 f(f(X)) -> c(f(g(f(X)))) 0.00/0.01 h(X) -> c(d(X)) 0.00/0.01 ) 0.00/0.01 Critical Pairs: 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N1 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N2 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N3 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N4 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N5 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N6 0.00/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.01 0.00/0.01 Huet Levy Procedure: 0.00/0.01 -> Rules: 0.00/0.01 c(X) -> d(X) 0.00/0.01 f(f(X)) -> c(f(g(f(X)))) 0.00/0.01 h(X) -> c(d(X)) 0.00/0.01 -> Vars: 0.00/0.01 X, X, X 0.00/0.01 -> UVars: 0.00/0.01 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X], UV-RFrozen: [X]) 0.00/0.01 (UV-RuleId: 2, UV-LActive: [X], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [X]) 0.00/0.01 (UV-RuleId: 3, UV-LActive: [X], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [X]) 0.00/0.01 0.00/0.01 -> Rlps: 0.00/0.01 (rule: c(X) -> d(X), id: 1, possubterms: c(X)->[]) 0.00/0.01 (rule: f(f(X)) -> c(f(g(f(X)))), id: 2, possubterms: f(f(X))->[], f(X)->[1]) 0.00/0.01 (rule: h(X) -> c(d(X)), id: 3, possubterms: h(X)->[]) 0.00/0.01 0.00/0.01 -> Unifications: 0.00/0.01 (R2 unifies with R2 at p: [1], l: f(f(X)), lp: f(X), sig: {X -> f(X')}, l': f(f(X')), r: c(f(g(f(X)))), r': c(f(g(f(X'))))) 0.00/0.01 0.00/0.01 -> Critical pairs info: 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N1 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N2 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N3 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N4 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N5 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N6 0.00/0.01 => Not trivial, Not overlay, Proper, NW0, N7 0.00/0.01 0.00/0.01 -> Problem conclusions: 0.00/0.01 Left linear, Right linear, Linear 0.00/0.01 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.00/0.01 Not Huet-Levy confluent, Not Newman confluent 0.00/0.01 R is a CS-TRS, Not left-homogeneous u-replacing variables 0.00/0.01 0.00/0.01 0.00/0.01 Problem 1: 0.00/0.01 No Convergence Brute Force Procedure: 0.00/0.01 -> Rewritings: 0.00/0.01 s: h(d(X')) 0.00/0.01 Nodes: [0,1,2] 0.00/0.01 Edges: [(0,1),(1,2)] 0.00/0.01 ID: 0 => ('h(d(X'))', D0) 0.00/0.01 ID: 1 => ('c(d(d(X')))', D1, R3, P[], S{x6 -> d(X')}), NR: 'c(d(d(X')))' 0.00/0.01 ID: 2 => ('d(d(d(X')))', D2, R1, P[], S{x4 -> d(d(X'))}), NR: 'd(d(d(X')))' 0.00/0.01 t: c(d(c(X'))) 0.00/0.01 Nodes: [0,1] 0.00/0.01 Edges: [(0,1)] 0.00/0.01 ID: 0 => ('c(d(c(X')))', D0) 0.00/0.01 ID: 1 => ('d(d(c(X')))', D1, R1, P[], S{x4 -> d(c(X'))}), NR: 'd(d(c(X')))' 0.00/0.01 h(d(X')) ->* no union *<- c(d(c(X'))) 0.00/0.01 "Not joinable" 0.00/0.01 0.00/0.01 The problem is not confluent. 0.00/0.01 EOF