0.004/0.004 NO 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty x y z) 0.004/0.004 (REPLACEMENT-MAP 0.004/0.004 (F 1, 2) 0.004/0.004 (a) 0.004/0.004 (C) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 (fSNonEmpty) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 F(x,x) -> C 0.004/0.004 F(x,y) -> F(x,y) | x ->*<- z, z ->*<- y 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Inlining of Conditions Processor [STERN17]: 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR vNonEmpty x y z) 0.004/0.004 (REPLACEMENT-MAP 0.004/0.004 (F 1, 2) 0.004/0.004 (a) 0.004/0.004 (C) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 (fSNonEmpty) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 F(x,x) -> C 0.004/0.004 F(x,y) -> F(x,y) | x ->*<- z, z ->*<- y 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Clean CTRS Processor: 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR x) 0.004/0.004 (REPLACEMENT-MAP 0.004/0.004 (F 1, 2) 0.004/0.004 (a) 0.004/0.004 (C) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 (fSNonEmpty) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 F(x,x) -> C 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 CRule InfChecker Info: 0.004/0.004 F(x,x) -> C 0.004/0.004 Rule remains 0.004/0.004 Proof: 0.004/0.004 NO_CONDS 0.004/0.004 0.004/0.004 CRule InfChecker Info: 0.004/0.004 F(x,y) -> F(x,y) | x ->*<- z, z ->*<- y 0.004/0.004 Rule deleted 0.004/0.004 Proof: 0.004/0.004 SAME_LHS_AND_RHS 0.004/0.004 0.004/0.004 CRule InfChecker Info: 0.004/0.004 a -> b 0.004/0.004 Rule remains 0.004/0.004 Proof: 0.004/0.004 NO_CONDS 0.004/0.004 0.004/0.004 CRule InfChecker Info: 0.004/0.004 a -> c 0.004/0.004 Rule remains 0.004/0.004 Proof: 0.004/0.004 NO_CONDS 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Transform No Conds CTRS Processor: 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR x) 0.004/0.004 (REPLACEMENT-MAP 0.004/0.004 (F 1, 2) 0.004/0.004 (a) 0.004/0.004 (C) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 (fSNonEmpty) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 F(x,x) -> C 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Resulting R: 0.004/0.004 (VAR x) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (F 1 2) 0.004/0.004 (a) 0.004/0.004 (C) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 (fSNonEmpty) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 F(x,x) -> C 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 CleanTRS Processor: 0.004/0.004 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (VAR x) 0.004/0.004 (REPLACEMENT-MAP 0.004/0.004 (F 1, 2) 0.004/0.004 (a) 0.004/0.004 (C) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 (fSNonEmpty) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 F(x,x) -> C 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 0.004/0.004 Modular Confluence Combinations Decomposition Processor: 0.004/0.004 0.004/0.004 TRS combination: 0.004/0.004 {F(x,x) -> C} 0.004/0.004 {a -> b 0.004/0.004 a -> c} 0.004/0.004 Disjoint 0.004/0.004 Constructor-sharing 0.004/0.004 Not left linear 0.004/0.004 Layer-preserving 0.004/0.004 TRS1 0.004/0.004 Just (VAR x) 0.004/0.004 (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (F 1 2) 0.004/0.004 (C) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 F(x,x) -> C 0.004/0.004 ) 0.004/0.004 0.004/0.004 TRS2 0.004/0.004 Just (STRATEGY CONTEXTSENSITIVE 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 Confluence Problem: 0.004/0.004 (REPLACEMENT-MAP 0.004/0.004 (a) 0.004/0.004 (b) 0.004/0.004 (c) 0.004/0.004 ) 0.004/0.004 (RULES 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 ) 0.004/0.004 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.004/0.004 0.004/0.004 Huet Levy Processor: 0.004/0.004 -> Rules: 0.004/0.004 a -> b 0.004/0.004 a -> c 0.004/0.004 -> Vars: 0.004/0.004 0.004/0.004 0.004/0.004 -> Rlps: 0.004/0.004 (rule: a -> b, id: 1, possubterms: a->[]) 0.004/0.004 (rule: a -> c, id: 2, possubterms: a->[]) 0.004/0.004 0.004/0.004 -> Unifications: 0.004/0.004 (R2 unifies with R1 at p: [], l: a, lp: a, sig: {}, l': a, r: c, r': b) 0.004/0.004 0.004/0.004 -> Critical pairs info: 0.004/0.004 => Not trivial, Overlay, NW0, N1 0.004/0.004 0.004/0.004 -> Problem conclusions: 0.004/0.004 Left linear, Right linear, Linear 0.004/0.004 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.004/0.004 Not Huet-Levy confluent, Not Newman confluent 0.004/0.004 R is a TRS 0.004/0.004 0.004/0.004 0.004/0.004 Problem 1: 0.004/0.004 Different Normal CP Terms Processor: 0.004/0.004 => Not trivial, Overlay, NW0, N1, Normal and not trivial cp 0.004/0.004 0.004/0.004 The problem is not joinable. 0.004/0.004 0.02user 0.00system 0:00.04elapsed 56%CPU (0avgtext+0avgdata 9604maxresident)k 0.004/0.004 0inputs+0outputs (0major+1857minor)pagefaults 0swaps