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