0.00/0.31 YES 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 Confluence Problem: 0.00/0.31 (VAR vNonEmpty:S x:S) 0.00/0.31 (STRATEGY CONTEXTSENSITIVE 0.00/0.31 (a 1) 0.00/0.31 (b 1) 0.00/0.31 (c 1) 0.00/0.31 (fSNonEmpty) 0.00/0.31 ) 0.00/0.31 (RULES 0.00/0.31 a(a(x:S)) -> a(b(a(x:S))) 0.00/0.31 b(a(b(x:S))) -> a(c(a(x:S))) 0.00/0.31 ) 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 CleanTRS Processor: 0.00/0.31 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 Confluence Problem: 0.00/0.31 (VAR vNonEmpty:S x:S) 0.00/0.31 (STRATEGY CONTEXTSENSITIVE 0.00/0.31 (a 1) 0.00/0.31 (b 1) 0.00/0.31 (c 1) 0.00/0.31 (fSNonEmpty) 0.00/0.31 ) 0.00/0.31 (RULES 0.00/0.31 a(a(x:S)) -> a(b(a(x:S))) 0.00/0.31 b(a(b(x:S))) -> a(c(a(x:S))) 0.00/0.31 ) 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 Modular Confluence Combinations Decomposition Processor: 0.00/0.31 0.00/0.31 No usable combinations 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 Termination Processor: 0.00/0.31 (STRATEGY CONTEXTSENSITIVE 0.00/0.31 (a 1) 0.00/0.31 (b 1) 0.00/0.31 (c 1) 0.00/0.31 (fSNonEmpty) 0.00/0.31 ) 0.00/0.31 Terminating? 0.00/0.31 YES 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 (VAR vu95NonEmpty:S vNonEmptyu58S:S xu58S:S) 0.00/0.31 (STRATEGY CONTEXTSENSITIVE 0.00/0.31 (a 1) 0.00/0.31 (b 1) 0.00/0.31 (c 1) 0.00/0.31 (fSNonEmpty) 0.00/0.31 ) 0.00/0.31 (RULES 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 ) 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 Dependency Pairs Processor: 0.00/0.31 -> Pairs: 0.00/0.31 A(a(xu58S:S)) -> A(b(a(xu58S:S))) 0.00/0.31 A(a(xu58S:S)) -> B(a(xu58S:S)) 0.00/0.31 B(a(b(xu58S:S))) -> A(c(a(xu58S:S))) 0.00/0.31 B(a(b(xu58S:S))) -> A(xu58S:S) 0.00/0.31 -> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 -> Unhiding Rules: 0.00/0.31 Empty 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 SCC Processor: 0.00/0.31 -> Pairs: 0.00/0.31 A(a(xu58S:S)) -> A(b(a(xu58S:S))) 0.00/0.31 A(a(xu58S:S)) -> B(a(xu58S:S)) 0.00/0.31 B(a(b(xu58S:S))) -> A(c(a(xu58S:S))) 0.00/0.31 B(a(b(xu58S:S))) -> A(xu58S:S) 0.00/0.31 -> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 -> Unhiding rules: 0.00/0.31 Empty 0.00/0.31 ->Strongly Connected Components: 0.00/0.31 ->->Cycle: 0.00/0.31 ->->-> Pairs: 0.00/0.31 A(a(xu58S:S)) -> A(b(a(xu58S:S))) 0.00/0.31 A(a(xu58S:S)) -> B(a(xu58S:S)) 0.00/0.31 B(a(b(xu58S:S))) -> A(xu58S:S) 0.00/0.31 ->->-> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 ->->-> Unhiding rules: 0.00/0.31 Empty 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 Reduction Triple Processor: 0.00/0.31 -> Pairs: 0.00/0.31 A(a(xu58S:S)) -> A(b(a(xu58S:S))) 0.00/0.31 A(a(xu58S:S)) -> B(a(xu58S:S)) 0.00/0.31 B(a(b(xu58S:S))) -> A(xu58S:S) 0.00/0.31 -> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 -> Unhiding rules: 0.00/0.31 Empty 0.00/0.31 -> Usable rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 ->Interpretation type: 0.00/0.31 Linear 0.00/0.31 ->Coefficients: 0.00/0.31 Natural Numbers 0.00/0.31 ->Dimension: 0.00/0.31 1 0.00/0.31 ->Bound: 0.00/0.31 2 0.00/0.31 ->Interpretation: 0.00/0.31 0.00/0.31 [a](X) = 2.X + 2 0.00/0.31 [b](X) = X 0.00/0.31 [c](X) = 0 0.00/0.31 [fSNonEmpty] = 0 0.00/0.31 [A](X) = 2.X + 2 0.00/0.31 [B](X) = 2.X 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 SCC Processor: 0.00/0.31 -> Pairs: 0.00/0.31 A(a(xu58S:S)) -> A(b(a(xu58S:S))) 0.00/0.31 B(a(b(xu58S:S))) -> A(xu58S:S) 0.00/0.31 -> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 -> Unhiding rules: 0.00/0.31 Empty 0.00/0.31 ->Strongly Connected Components: 0.00/0.31 ->->Cycle: 0.00/0.31 ->->-> Pairs: 0.00/0.31 A(a(xu58S:S)) -> A(b(a(xu58S:S))) 0.00/0.31 ->->-> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 ->->-> Unhiding rules: 0.00/0.31 Empty 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 Reduction Triple Processor: 0.00/0.31 -> Pairs: 0.00/0.31 A(a(xu58S:S)) -> A(b(a(xu58S:S))) 0.00/0.31 -> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 -> Unhiding rules: 0.00/0.31 Empty 0.00/0.31 -> Usable rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 ->Interpretation type: 0.00/0.31 Linear 0.00/0.31 ->Coefficients: 0.00/0.31 All rationals 0.00/0.31 ->Dimension: 0.00/0.31 1 0.00/0.31 ->Bound: 0.00/0.31 2 0.00/0.31 ->Interpretation: 0.00/0.31 0.00/0.31 [a](X) = 2.X + 2 0.00/0.31 [b](X) = 1/2.X + 1/2 0.00/0.31 [c](X) = 0 0.00/0.31 [fSNonEmpty] = 0 0.00/0.31 [A](X) = 2.X 0.00/0.31 [B](X) = 0 0.00/0.31 0.00/0.31 Problem 1: 0.00/0.31 0.00/0.31 Basic Processor: 0.00/0.31 -> Pairs: 0.00/0.31 Empty 0.00/0.31 -> Rules: 0.00/0.31 a(a(xu58S:S)) -> a(b(a(xu58S:S))) 0.00/0.31 b(a(b(xu58S:S))) -> a(c(a(xu58S:S))) 0.00/0.31 -> Unhiding rules: 0.00/0.31 Empty 0.00/0.31 -> Result: 0.00/0.31 Set P is empty 0.00/0.31 0.00/0.31 The problem is finite. 0.00/0.31 0.00/0.31 Problem 1.1: 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 Confluence Problem: 0.00/0.31 (VAR vNonEmpty:S x:S) 0.00/0.31 (STRATEGY CONTEXTSENSITIVE 0.00/0.31 (a 1) 0.00/0.31 (b 1) 0.00/0.31 (c 1) 0.00/0.31 (fSNonEmpty) 0.00/0.31 ) 0.00/0.31 (RULES 0.00/0.31 a(a(x:S)) -> a(b(a(x:S))) 0.00/0.31 b(a(b(x:S))) -> a(c(a(x:S))) 0.00/0.31 ) 0.00/0.31 Terminating:"YES" 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 0.00/0.31 Huet Levy Processor: 0.00/0.31 -> Rules: 0.00/0.31 a(a(x:S)) -> a(b(a(x:S))) 0.00/0.31 b(a(b(x:S))) -> a(c(a(x:S))) 0.00/0.31 -> Vars: 0.00/0.31 x, x 0.00/0.31 -> FVars: 0.00/0.31 x2, x3 0.00/0.31 -> PVars: 0.00/0.31 x: [x2, x3] 0.00/0.31 0.00/0.31 -> Rlps: 0.00/0.31 (rule: a(a(x2:S)) -> a(b(a(x2:S))), id: 1, possubterms: a(a(x2:S))->[], a(x2:S)->[1]) 0.00/0.31 (rule: b(a(b(x3:S))) -> a(c(a(x3:S))), id: 2, possubterms: b(a(b(x3:S)))->[], a(b(x3:S))->[1], b(x3:S)->[1, 1]) 0.00/0.31 0.00/0.31 -> Unifications: 0.00/0.31 (R1 unifies with R1 at p: [1], l: a(a(x2:S)), lp: a(x2:S), sig: {x2:S -> a(x:S)}, l': a(a(x:S)), r: a(b(a(x2:S))), r': a(b(a(x:S)))) 0.00/0.31 (R2 unifies with R2 at p: [1,1], l: b(a(b(x3:S))), lp: b(x3:S), sig: {x3:S -> a(b(x:S))}, l': b(a(b(x:S))), r: a(c(a(x3:S))), r': a(c(a(x:S)))) 0.00/0.31 0.00/0.31 -> Critical pairs info: 0.00/0.31 => Not trivial, Not overlay, N1 0.00/0.31 => Not trivial, Not overlay, N2 0.00/0.31 0.00/0.31 -> Problem conclusions: 0.00/0.31 Left linear, Right linear, Linear 0.00/0.31 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.00/0.31 Not Huet-Levy confluent, Not Newman confluent 0.00/0.31 R is a TRS 0.00/0.31 0.00/0.31 0.00/0.31 0.00/0.31 The problem is decomposed in 2 subproblems. 0.00/0.31 0.00/0.31 Problem 1.1.1: 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 Confluence Problem: 0.00/0.31 (VAR vNonEmpty:S x:S) 0.00/0.31 (STRATEGY CONTEXTSENSITIVE 0.00/0.31 (a 1) 0.00/0.31 (b 1) 0.00/0.31 (c 1) 0.00/0.31 (fSNonEmpty) 0.00/0.31 ) 0.00/0.31 (RULES 0.00/0.31 a(a(x:S)) -> a(b(a(x:S))) 0.00/0.31 b(a(b(x:S))) -> a(c(a(x:S))) 0.00/0.31 ) 0.00/0.31 Critical Pairs: 0.00/0.31 => Not trivial, Not overlay, N1 0.00/0.31 Terminating:"YES" 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 0.00/0.31 Huet Brute Force Joinability Processor: 0.00/0.31 -> Rewritings: 0.00/0.31 s: b(a(a(c(a(x:S))))) 0.00/0.31 Nodes: [0,1,2,3] 0.00/0.31 Edges: [(0,1),(1,2),(2,3)] 0.00/0.31 ID: 0 => ('b(a(a(c(a(x:S)))))', D0) 0.00/0.31 ID: 1 => ('b(a(b(a(c(a(x:S))))))', D1, R1, P[1], S{x2:S -> c(a(x:S))}), NR: 'a(b(a(c(a(x:S)))))' 0.00/0.31 ID: 2 => ('a(c(a(a(c(a(x:S))))))', D2, R2, P[], S{x3:S -> a(c(a(x:S)))}), NR: 'a(c(a(a(c(a(x:S))))))' 0.00/0.31 ID: 3 => ('a(c(a(b(a(c(a(x:S)))))))', D3, R1, P[1, 1], S{x2:S -> c(a(x:S))}), NR: 'a(b(a(c(a(x:S)))))' 0.00/0.31 t: a(c(a(a(b(x:S))))) 0.00/0.31 Nodes: [0,1,2,3] 0.00/0.31 Edges: [(0,1),(1,2),(2,3)] 0.00/0.31 ID: 0 => ('a(c(a(a(b(x:S)))))', D0) 0.00/0.31 ID: 1 => ('a(c(a(b(a(b(x:S))))))', D1, R1, P[1, 1], S{x2:S -> b(x:S)}), NR: 'a(b(a(b(x:S))))' 0.00/0.31 ID: 2 => ('a(c(a(a(c(a(x:S))))))', D2, R2, P[1, 1, 1], S{x3:S -> x:S}), NR: 'a(c(a(x:S)))' 0.00/0.31 ID: 3 => ('a(c(a(b(a(c(a(x:S)))))))', D3, R1, P[1, 1], S{x2:S -> c(a(x:S))}), NR: 'a(b(a(c(a(x:S)))))' 0.00/0.31 b(a(a(c(a(x:S))))) ->* a(c(a(a(c(a(x:S)))))) *<- a(c(a(a(b(x:S))))) 0.00/0.31 "Joinable" 0.00/0.31 0.00/0.31 The problem is joinable. 0.00/0.31 0.00/0.31 Problem 1.1.2: 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 Confluence Problem: 0.00/0.31 (VAR vNonEmpty:S x:S) 0.00/0.31 (STRATEGY CONTEXTSENSITIVE 0.00/0.31 (a 1) 0.00/0.31 (b 1) 0.00/0.31 (c 1) 0.00/0.31 (fSNonEmpty) 0.00/0.31 ) 0.00/0.31 (RULES 0.00/0.31 a(a(x:S)) -> a(b(a(x:S))) 0.00/0.31 b(a(b(x:S))) -> a(c(a(x:S))) 0.00/0.31 ) 0.00/0.31 Critical Pairs: 0.00/0.31 => Not trivial, Not overlay, N2 0.00/0.31 Terminating:"YES" 0.00/0.31 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.31 0.00/0.31 Huet Brute Force Joinability Processor: 0.00/0.31 -> Rewritings: 0.00/0.31 s: a(a(b(a(x:S)))) 0.00/0.31 Nodes: [0,1,2,3,4,5] 0.00/0.31 Edges: [(0,1),(1,2),(2,3),(2,4),(3,5),(4,5)] 0.00/0.31 ID: 0 => ('a(a(b(a(x:S))))', D0) 0.00/0.31 ID: 1 => ('a(b(a(b(a(x:S)))))', D1, R1, P[], S{x2:S -> b(a(x:S))}), NR: 'a(b(a(b(a(x:S)))))' 0.00/0.31 ID: 2 => ('a(a(c(a(a(x:S)))))', D2, R2, P[1], S{x3:S -> a(x:S)}), NR: 'a(c(a(a(x:S))))' 0.00/0.31 ID: 3 => ('a(b(a(c(a(a(x:S))))))', D3, R1, P[], S{x2:S -> c(a(a(x:S)))}), NR: 'a(b(a(c(a(a(x:S))))))' 0.00/0.31 ID: 4 => ('a(a(c(a(b(a(x:S))))))', D3, R1, P[1, 1, 1], S{x2:S -> x:S}), NR: 'a(b(a(x:S)))' 0.00/0.31 ID: 5 => ('a(b(a(c(a(b(a(x:S)))))))', D4, R1, P[1, 1, 1, 1], S{x2:S -> x:S}), NR: 'a(b(a(x:S)))' 0.00/0.31 t: a(b(a(a(x:S)))) 0.00/0.31 Nodes: [0,1,2,3,4,5] 0.00/0.31 Edges: [(0,1),(1,2),(2,3),(2,4),(3,5),(4,5)] 0.00/0.31 ID: 0 => ('a(b(a(a(x:S))))', D0) 0.00/0.31 ID: 1 => ('a(b(a(b(a(x:S)))))', D1, R1, P[1, 1], S{x2:S -> x:S}), NR: 'a(b(a(x:S)))' 0.00/0.31 ID: 2 => ('a(a(c(a(a(x:S)))))', D2, R2, P[1], S{x3:S -> a(x:S)}), NR: 'a(c(a(a(x:S))))' 0.00/0.31 ID: 3 => ('a(b(a(c(a(a(x:S))))))', D3, R1, P[], S{x2:S -> c(a(a(x:S)))}), NR: 'a(b(a(c(a(a(x:S))))))' 0.00/0.31 ID: 4 => ('a(a(c(a(b(a(x:S))))))', D3, R1, P[1, 1, 1], S{x2:S -> x:S}), NR: 'a(b(a(x:S)))' 0.00/0.31 ID: 5 => ('a(b(a(c(a(b(a(x:S)))))))', D4, R1, P[1, 1, 1, 1], S{x2:S -> x:S}), NR: 'a(b(a(x:S)))' 0.00/0.31 a(a(b(a(x:S)))) ->* a(b(a(b(a(x:S))))) *<- a(b(a(a(x:S)))) 0.00/0.31 "Joinable" 0.00/0.31 0.00/0.31 The problem is joinable. 0.00/10.26 EOF