0.17/0.80 YES 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 Confluence Problem: 0.17/0.80 (VAR x) 0.17/0.80 (REPLACEMENT-MAP 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h 1) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 Not CS-TRS Procedure: 0.17/0.80 R is not a CS-TRS 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 CSR Converter From Canonical u-Replacement Map Procedure [CSUR20]: 0.17/0.80 0.17/0.80 Original Replacement Map: 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h 1) 0.17/0.80 0.17/0.80 New Replacement Map: 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 0.17/0.80 New problem: 0.17/0.80 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 Confluence Problem: 0.17/0.80 (VAR x) 0.17/0.80 (REPLACEMENT-MAP 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 Termination Procedure: 0.17/0.80 Terminating? 0.17/0.80 YES 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 (VAR vu95NonEmpty x) 0.17/0.80 (STRATEGY CONTEXTSENSITIVE 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 (fSNonEmpty) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 Dependency Pairs Processor: 0.17/0.80 -> Pairs: 0.17/0.80 F(g(h(x))) -> F(h(g(x))) 0.17/0.80 F(g(h(x))) -> G(f(h(g(x)))) 0.17/0.80 F(g(h(x))) -> H(g(x)) 0.17/0.80 H(x) -> x 0.17/0.80 -> Rules: 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 -> Unhiding Rules: 0.17/0.80 g(x) -> G(x) 0.17/0.80 g(x2) -> x2 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 SCC Processor: 0.17/0.80 -> Pairs: 0.17/0.80 F(g(h(x))) -> F(h(g(x))) 0.17/0.80 F(g(h(x))) -> G(f(h(g(x)))) 0.17/0.80 F(g(h(x))) -> H(g(x)) 0.17/0.80 H(x) -> x 0.17/0.80 -> Rules: 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 -> Unhiding rules: 0.17/0.80 g(x) -> G(x) 0.17/0.80 g(x2) -> x2 0.17/0.80 ->Strongly Connected Components: 0.17/0.80 ->->Cycle: 0.17/0.80 ->->-> Pairs: 0.17/0.80 F(g(h(x))) -> F(h(g(x))) 0.17/0.80 ->->-> Rules: 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ->->-> Unhiding rules: 0.17/0.80 Empty 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 Reduction Triple Processor: 0.17/0.80 -> Pairs: 0.17/0.80 F(g(h(x))) -> F(h(g(x))) 0.17/0.80 -> Rules: 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 -> Unhiding rules: 0.17/0.80 Empty 0.17/0.80 -> Usable rules: 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ->Interpretation type: 0.17/0.80 Linear 0.17/0.80 ->Coefficients: 0.17/0.80 Natural Numbers 0.17/0.80 ->Dimension: 0.17/0.80 1 0.17/0.80 ->Bound: 0.17/0.80 2 0.17/0.80 ->Interpretation: 0.17/0.80 0.17/0.80 [f](X) = 0 0.17/0.80 [g](X) = 2.X 0.17/0.80 [h](X) = 2.X + 2 0.17/0.80 [fSNonEmpty] = 0 0.17/0.80 [F](X) = 2.X 0.17/0.80 [G](X) = 0 0.17/0.80 [H](X) = 0 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 0.17/0.80 Basic Processor: 0.17/0.80 -> Pairs: 0.17/0.80 Empty 0.17/0.80 -> Rules: 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 -> Unhiding rules: 0.17/0.80 Empty 0.17/0.80 -> Result: 0.17/0.80 Set P is empty 0.17/0.80 0.17/0.80 The problem is finite. 0.17/0.80 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 Confluence Problem: 0.17/0.80 (VAR x) 0.17/0.80 (REPLACEMENT-MAP 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 Terminating:"YES" 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 0.17/0.80 Huet Levy NW Procedure: 0.17/0.80 -> Rules: 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 -> Vars: 0.17/0.80 x, x, x, x 0.17/0.80 -> UVars: 0.17/0.80 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: [x]) 0.17/0.80 (UV-RuleId: 2, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) 0.17/0.80 (UV-RuleId: 3, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: []) 0.17/0.80 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [x], UV-LFrozen: [x], UV-RFrozen: []) 0.17/0.80 0.17/0.80 -> Rlps: 0.17/0.80 (rule: f(g(h(x))) -> g(f(h(g(x)))), id: 1, possubterms: f(g(h(x)))->[], g(h(x))->[1], h(x)->[1, 1]) 0.17/0.80 (rule: f(x) -> x, id: 2, possubterms: f(x)->[]) 0.17/0.80 (rule: g(x) -> x, id: 3, possubterms: g(x)->[]) 0.17/0.80 (rule: h(x) -> x, id: 4, possubterms: h(x)->[]) 0.17/0.80 0.17/0.80 -> Unifications: 0.17/0.80 (R1 unifies with R3 at p: [1], l: f(g(h(x))), lp: g(h(x)), sig: {x' -> h(x)}, l': g(x'), r: g(f(h(g(x)))), r': x') 0.17/0.80 (R1 unifies with R4 at p: [1,1], l: f(g(h(x))), lp: h(x), sig: {x -> x'}, l': h(x'), r: g(f(h(g(x)))), r': x') 0.17/0.80 (R2 unifies with R1 at p: [], l: f(x), lp: f(x), sig: {x -> g(h(x'))}, l': f(g(h(x'))), r: x, r': g(f(h(g(x'))))) 0.17/0.80 0.17/0.80 -> Critical pairs info: 0.17/0.80 => Not trivial, Not overlay, Proper, NW0, N1 0.17/0.80 => Not trivial, Overlay, Proper, NW0, N2 0.17/0.80 => Not trivial, Not overlay, Proper, NW0, N3 0.17/0.80 0.17/0.80 -> Problem conclusions: 0.17/0.80 Left linear, Right linear, Linear 0.17/0.80 Not weakly orthogonal, Not almost orthogonal, Not orthogonal, Not strongly orthogonal 0.17/0.80 Not Huet-Levy confluent, Not Newman confluent 0.17/0.80 R is a CS-TRS, Left-homogeneous u-replacing variables 0.17/0.80 Maybe confluent 0.17/0.80 0.17/0.80 0.17/0.80 Problem 1: 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 Confluence Problem: 0.17/0.80 (VAR x x') 0.17/0.80 (REPLACEMENT-MAP 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 Critical Pairs: 0.17/0.80 => Not trivial, Not overlay, Proper, NW0, N1 0.17/0.80 => Not trivial, Overlay, Proper, NW0, N2 0.17/0.80 => Not trivial, Not overlay, Proper, NW0, N3 0.17/0.80 Terminating:"YES" 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 0.17/0.80 Critical Pairs Distributor Processor: 0.17/0.80 0.17/0.80 0.17/0.80 0.17/0.80 The problem is decomposed in 3 subproblems. 0.17/0.80 0.17/0.80 Problem 1.1: 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 Confluence Problem: 0.17/0.80 (VAR x x') 0.17/0.80 (REPLACEMENT-MAP 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 Critical Pairs: 0.17/0.80 => Not trivial, Not overlay, Proper, NW0, N1 0.17/0.80 Terminating:"YES" 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 0.17/0.80 Huet Brute Force Joinability Procedure: 0.17/0.80 -> Rewritings: 0.17/0.80 s: f(g(x')) 0.17/0.80 Nodes: [0,1,2,3] 0.17/0.80 Edges: [(0,1),(0,2),(1,3),(2,3)] 0.17/0.80 ID: 0 => ('f(g(x'))', D0) 0.17/0.80 ID: 1 => ('g(x')', D1, R2, P[], S{x3 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 2 => ('f(x')', D1, R3, P[1], S{x4 -> x'}), NR: 'x'' 0.17/0.80 ID: 3 => ('x'', D2, R3, P[], S{x4 -> x'}), NR: 'x'' 0.17/0.80 t: g(f(h(g(x')))) 0.17/0.80 Nodes: [0,1,2,3,4,5,6,7,8,9,10] 0.17/0.80 Edges: [(0,1),(0,2),(0,3),(1,4),(1,5),(2,4),(2,6),(3,5),(3,6),(3,7),(4,8),(5,8),(5,8),(6,8),(6,9),(7,8),(7,9),(8,10),(9,10)] 0.17/0.80 ID: 0 => ('g(f(h(g(x'))))', D0) 0.17/0.80 ID: 1 => ('g(h(g(x')))', D1, R2, P[1], S{x3 -> h(g(x'))}), NR: 'h(g(x'))' 0.17/0.80 ID: 2 => ('f(h(g(x')))', D1, R3, P[], S{x4 -> f(h(g(x')))}), NR: 'f(h(g(x')))' 0.17/0.80 ID: 3 => ('g(f(g(x')))', D1, R4, P[1, 1], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 4 => ('h(g(x'))', D2, R3, P[], S{x4 -> h(g(x'))}), NR: 'h(g(x'))' 0.17/0.80 ID: 5 => ('g(g(x'))', D2, R4, P[1], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 6 => ('f(g(x'))', D2, R4, P[1], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 7 => ('g(f(x'))', D2, R3, P[1, 1], S{x4 -> x'}), NR: 'x'' 0.17/0.80 ID: 8 => ('g(x')', D3, R4, P[], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 9 => ('f(x')', D3, R3, P[1], S{x4 -> x'}), NR: 'x'' 0.17/0.80 ID: 10 => ('x'', D4, R3, P[], S{x4 -> x'}), NR: 'x'' 0.17/0.80 SNodesPath: f(g(x')) 0.17/0.80 TNodesPath: 0.17/0.80 f(g(x')) ->* f(g(x')) *<- g(f(h(g(x')))) 0.17/0.80 "Joinable" 0.17/0.80 0.17/0.80 The problem is confluent. 0.17/0.80 0.17/0.80 Problem 1.2: 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 Confluence Problem: 0.17/0.80 (VAR x x') 0.17/0.80 (REPLACEMENT-MAP 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 Critical Pairs: 0.17/0.80 => Not trivial, Overlay, Proper, NW0, N2 0.17/0.80 Terminating:"YES" 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 0.17/0.80 Huet Brute Force Joinability Procedure: 0.17/0.80 -> Rewritings: 0.17/0.80 s: g(f(h(g(x')))) 0.17/0.80 Nodes: [0,1,2,3,4,5,6,7,8,9,10] 0.17/0.80 Edges: [(0,1),(0,2),(0,3),(1,4),(1,5),(2,4),(2,6),(3,5),(3,6),(3,7),(4,8),(5,8),(5,8),(6,8),(6,9),(7,8),(7,9),(8,10),(9,10)] 0.17/0.80 ID: 0 => ('g(f(h(g(x'))))', D0) 0.17/0.80 ID: 1 => ('g(h(g(x')))', D1, R2, P[1], S{x3 -> h(g(x'))}), NR: 'h(g(x'))' 0.17/0.80 ID: 2 => ('f(h(g(x')))', D1, R3, P[], S{x4 -> f(h(g(x')))}), NR: 'f(h(g(x')))' 0.17/0.80 ID: 3 => ('g(f(g(x')))', D1, R4, P[1, 1], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 4 => ('h(g(x'))', D2, R3, P[], S{x4 -> h(g(x'))}), NR: 'h(g(x'))' 0.17/0.80 ID: 5 => ('g(g(x'))', D2, R4, P[1], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 6 => ('f(g(x'))', D2, R4, P[1], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 7 => ('g(f(x'))', D2, R3, P[1, 1], S{x4 -> x'}), NR: 'x'' 0.17/0.80 ID: 8 => ('g(x')', D3, R4, P[], S{x5 -> g(x')}), NR: 'g(x')' 0.17/0.80 ID: 9 => ('f(x')', D3, R3, P[1], S{x4 -> x'}), NR: 'x'' 0.17/0.80 ID: 10 => ('x'', D4, R3, P[], S{x4 -> x'}), NR: 'x'' 0.17/0.80 t: g(h(x')) 0.17/0.80 Nodes: [0,1,2,3] 0.17/0.80 Edges: [(0,1),(0,2),(1,3),(2,3)] 0.17/0.80 ID: 0 => ('g(h(x'))', D0) 0.17/0.80 ID: 1 => ('h(x')', D1, R3, P[], S{x4 -> h(x')}), NR: 'h(x')' 0.17/0.80 ID: 2 => ('g(x')', D1, R4, P[1], S{x5 -> x'}), NR: 'x'' 0.17/0.80 ID: 3 => ('x'', D2, R4, P[], S{x5 -> x'}), NR: 'x'' 0.17/0.80 SNodesPath: g(f(h(g(x')))) -> g(h(g(x'))) -> h(g(x')) -> g(x') 0.17/0.80 TNodesPath: 0.17/0.80 g(f(h(g(x')))) ->* g(x') *<- g(h(x')) 0.17/0.80 "Joinable" 0.17/0.80 0.17/0.80 The problem is confluent. 0.17/0.80 0.17/0.80 Problem 1.3: 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 Confluence Problem: 0.17/0.80 (VAR x x') 0.17/0.80 (REPLACEMENT-MAP 0.17/0.80 (f 1) 0.17/0.80 (g 1) 0.17/0.80 (h) 0.17/0.80 ) 0.17/0.80 (RULES 0.17/0.80 f(g(h(x))) -> g(f(h(g(x)))) 0.17/0.80 f(x) -> x 0.17/0.80 g(x) -> x 0.17/0.80 h(x) -> x 0.17/0.80 ) 0.17/0.80 0.17/0.80 Critical Pairs: 0.17/0.80 => Not trivial, Not overlay, Proper, NW0, N3 0.17/0.80 Terminating:"YES" 0.17/0.80 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.17/0.80 0.17/0.80 Huet Brute Force Joinability Procedure: 0.17/0.80 -> Rewritings: 0.17/0.80 s: f(h(x)) 0.17/0.80 Nodes: [0,1,2,3] 0.17/0.80 Edges: [(0,1),(0,2),(1,3),(2,3)] 0.17/0.80 ID: 0 => ('f(h(x))', D0) 0.17/0.80 ID: 1 => ('h(x)', D1, R2, P[], S{x3 -> h(x)}), NR: 'h(x)' 0.17/0.80 ID: 2 => ('f(x)', D1, R4, P[1], S{x5 -> x}), NR: 'x' 0.17/0.80 ID: 3 => ('x', D2, R4, P[], S{x5 -> x}), NR: 'x' 0.17/0.80 t: g(f(h(g(x)))) 0.17/0.80 Nodes: [0,1,2,3,4,5,6,7,8,9,10] 0.17/0.80 Edges: [(0,1),(0,2),(0,3),(1,4),(1,5),(2,4),(2,6),(3,5),(3,6),(3,7),(4,8),(5,8),(5,8),(6,8),(6,9),(7,8),(7,9),(8,10),(9,10)] 0.17/0.80 ID: 0 => ('g(f(h(g(x))))', D0) 0.17/0.80 ID: 1 => ('g(h(g(x)))', D1, R2, P[1], S{x3 -> h(g(x))}), NR: 'h(g(x))' 0.17/0.80 ID: 2 => ('f(h(g(x)))', D1, R3, P[], S{x4 -> f(h(g(x)))}), NR: 'f(h(g(x)))' 0.17/0.80 ID: 3 => ('g(f(g(x)))', D1, R4, P[1, 1], S{x5 -> g(x)}), NR: 'g(x)' 0.17/0.80 ID: 4 => ('h(g(x))', D2, R3, P[], S{x4 -> h(g(x))}), NR: 'h(g(x))' 0.17/0.80 ID: 5 => ('g(g(x))', D2, R4, P[1], S{x5 -> g(x)}), NR: 'g(x)' 0.17/0.80 ID: 6 => ('f(g(x))', D2, R4, P[1], S{x5 -> g(x)}), NR: 'g(x)' 0.17/0.80 ID: 7 => ('g(f(x))', D2, R3, P[1, 1], S{x4 -> x}), NR: 'x' 0.17/0.80 ID: 8 => ('g(x)', D3, R4, P[], S{x5 -> g(x)}), NR: 'g(x)' 0.17/0.80 ID: 9 => ('f(x)', D3, R3, P[1], S{x4 -> x}), NR: 'x' 0.17/0.80 ID: 10 => ('x', D4, R3, P[], S{x4 -> x}), NR: 'x' 0.17/0.80 SNodesPath: 0.17/0.80 TNodesPath: 0.17/0.80 f(h(x)) ->* f(x) *<- g(f(h(g(x)))) 0.17/0.80 "Joinable" 0.17/0.80 0.17/0.80 The problem is confluent. 0.17/60.88 EOF