0.00/0.08 NO 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 0.00/0.08 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 Confluence Problem: 0.00/0.08 (VAR vNonEmpty:S x:S) 0.00/0.08 (STRATEGY CONTEXTSENSITIVE 0.00/0.08 (0 1) 0.00/0.08 (1 1) 0.00/0.08 (2 1) 0.00/0.08 (fSNonEmpty) 0.00/0.08 ) 0.00/0.08 (RULES 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x:S))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(x:S)))))))))) 0.00/0.08 ) 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 0.00/0.08 CleanTRS Processor: 0.00/0.08 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 Confluence Problem: 0.00/0.08 (VAR vNonEmpty:S x:S) 0.00/0.08 (STRATEGY CONTEXTSENSITIVE 0.00/0.08 (0 1) 0.00/0.08 (1 1) 0.00/0.08 (2 1) 0.00/0.08 (fSNonEmpty) 0.00/0.08 ) 0.00/0.08 (RULES 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x:S))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(x:S)))))))))) 0.00/0.08 ) 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 0.00/0.08 Modular Confluence Combinations Decomposition Processor: 0.00/0.08 0.00/0.08 No usable combinations 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 Confluence Problem: 0.00/0.08 (VAR vNonEmpty:S x:S) 0.00/0.08 (STRATEGY CONTEXTSENSITIVE 0.00/0.08 (0 1) 0.00/0.08 (1 1) 0.00/0.08 (2 1) 0.00/0.08 (fSNonEmpty) 0.00/0.08 ) 0.00/0.08 (RULES 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x:S))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(x:S)))))))))) 0.00/0.08 ) 0.00/0.08 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.00/0.08 0.00/0.08 Huet Levy Processor: 0.00/0.08 -> Rules: 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x:S))))))))))))) 0.00/0.08 0(1(2(1(x:S)))) -> 1(2(1(1(0(1(2(0(1(2(x:S)))))))))) 0.00/0.08 -> Vars: 0.00/0.08 x, x, x, x, x, x 0.00/0.08 -> FVars: 0.00/0.08 x2, x3, x4, x5, x6, x7 0.00/0.08 -> PVars: 0.00/0.08 x: [x2, x3, x4, x5, x6, x7] 0.00/0.08 0.00/0.08 -> Rlps: 0.00/0.08 (rule: 0(1(2(1(x2:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x2:S))))))))))))))))))))))))), id: 1, possubterms: 0(1(2(1(x2:S))))->[], 1(2(1(x2:S)))->[1], 2(1(x2:S))->[1, 1], 1(x2:S)->[1, 1, 1]) 0.00/0.08 (rule: 0(1(2(1(x3:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x3:S)))))))))))))))))))))), id: 2, possubterms: 0(1(2(1(x3:S))))->[], 1(2(1(x3:S)))->[1], 2(1(x3:S))->[1, 1], 1(x3:S)->[1, 1, 1]) 0.00/0.08 (rule: 0(1(2(1(x4:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x4:S))))))))))))))))))), id: 3, possubterms: 0(1(2(1(x4:S))))->[], 1(2(1(x4:S)))->[1], 2(1(x4:S))->[1, 1], 1(x4:S)->[1, 1, 1]) 0.00/0.08 (rule: 0(1(2(1(x5:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x5:S)))))))))))))))), id: 4, possubterms: 0(1(2(1(x5:S))))->[], 1(2(1(x5:S)))->[1], 2(1(x5:S))->[1, 1], 1(x5:S)->[1, 1, 1]) 0.00/0.08 (rule: 0(1(2(1(x6:S)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x6:S))))))))))))), id: 5, possubterms: 0(1(2(1(x6:S))))->[], 1(2(1(x6:S)))->[1], 2(1(x6:S))->[1, 1], 1(x6:S)->[1, 1, 1]) 0.00/0.08 (rule: 0(1(2(1(x7:S)))) -> 1(2(1(1(0(1(2(0(1(2(x7:S)))))))))), id: 6, possubterms: 0(1(2(1(x7:S))))->[], 1(2(1(x7:S)))->[1], 2(1(x7:S))->[1, 1], 1(x7:S)->[1, 1, 1]) 0.00/0.08 0.00/0.08 -> Unifications: 0.00/0.08 (R2 unifies with R1 at p: [], l: 0(1(2(1(x3:S)))), lp: 0(1(2(1(x3:S)))), sig: {x3:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x3:S)))))))))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))))))) 0.00/0.08 (R3 unifies with R1 at p: [], l: 0(1(2(1(x4:S)))), lp: 0(1(2(1(x4:S)))), sig: {x4:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x4:S))))))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))))))) 0.00/0.08 (R3 unifies with R2 at p: [], l: 0(1(2(1(x4:S)))), lp: 0(1(2(1(x4:S)))), sig: {x4:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x4:S))))))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))) 0.00/0.08 (R4 unifies with R1 at p: [], l: 0(1(2(1(x5:S)))), lp: 0(1(2(1(x5:S)))), sig: {x5:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x5:S)))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))))))) 0.00/0.08 (R4 unifies with R2 at p: [], l: 0(1(2(1(x5:S)))), lp: 0(1(2(1(x5:S)))), sig: {x5:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x5:S)))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))) 0.00/0.08 (R4 unifies with R3 at p: [], l: 0(1(2(1(x5:S)))), lp: 0(1(2(1(x5:S)))), sig: {x5:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x5:S)))))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))) 0.00/0.08 (R5 unifies with R1 at p: [], l: 0(1(2(1(x6:S)))), lp: 0(1(2(1(x6:S)))), sig: {x6:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x6:S))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))))))) 0.00/0.08 (R5 unifies with R2 at p: [], l: 0(1(2(1(x6:S)))), lp: 0(1(2(1(x6:S)))), sig: {x6:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x6:S))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))) 0.00/0.08 (R5 unifies with R3 at p: [], l: 0(1(2(1(x6:S)))), lp: 0(1(2(1(x6:S)))), sig: {x6:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x6:S))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))) 0.00/0.08 (R5 unifies with R4 at p: [], l: 0(1(2(1(x6:S)))), lp: 0(1(2(1(x6:S)))), sig: {x6:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(0(1(2(x6:S))))))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))) 0.00/0.08 (R6 unifies with R1 at p: [], l: 0(1(2(1(x7:S)))), lp: 0(1(2(1(x7:S)))), sig: {x7:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(x7:S)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))))))) 0.00/0.08 (R6 unifies with R2 at p: [], l: 0(1(2(1(x7:S)))), lp: 0(1(2(1(x7:S)))), sig: {x7:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(x7:S)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))) 0.00/0.08 (R6 unifies with R3 at p: [], l: 0(1(2(1(x7:S)))), lp: 0(1(2(1(x7:S)))), sig: {x7:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(x7:S)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))) 0.00/0.08 (R6 unifies with R4 at p: [], l: 0(1(2(1(x7:S)))), lp: 0(1(2(1(x7:S)))), sig: {x7:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(x7:S)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))) 0.00/0.08 (R6 unifies with R5 at p: [], l: 0(1(2(1(x7:S)))), lp: 0(1(2(1(x7:S)))), sig: {x7:S -> x:S}, l': 0(1(2(1(x:S)))), r: 1(2(1(1(0(1(2(0(1(2(x7:S)))))))))), r': 1(2(1(1(0(1(2(0(1(2(0(1(2(x:S)))))))))))))) 0.00/0.08 0.00/0.08 -> Critical pairs info: 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(x:S))))))))))))),1(2(1(1(0(1(2(0(1(2(x:S))))))))))> => Not trivial, Overlay, N1 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))),1(2(1(1(0(1(2(0(1(2(x:S))))))))))> => Not trivial, Overlay, N2 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x:S)))))))))))))> => Not trivial, Overlay, N3 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(x:S))))))))))> => Not trivial, Overlay, N4 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x:S)))))))))))))> => Not trivial, Overlay, N5 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))> => Not trivial, Overlay, N6 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(x:S))))))))))> => Not trivial, Overlay, N7 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x:S)))))))))))))> => Not trivial, Overlay, N8 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))> => Not trivial, Overlay, N9 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))> => Not trivial, Overlay, N10 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(x:S))))))))))> => Not trivial, Overlay, N11 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(x:S)))))))))))))> => Not trivial, Overlay, N12 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))> => Not trivial, Overlay, N13 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S)))))))))))))))))))> => Not trivial, Overlay, N14 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))))),1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x:S))))))))))))))))))))))> => Not trivial, Overlay, N15 0.00/0.08 0.00/0.08 -> Problem conclusions: 0.00/0.08 Left linear, Right linear, Linear 0.00/0.08 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.00/0.08 Not Huet-Levy confluent, Not Newman confluent 0.00/0.08 R is a TRS 0.00/0.08 0.00/0.08 0.00/0.08 Problem 1: 0.00/0.08 Different Normal CP Terms Processor: 0.00/0.08 <1(2(1(1(0(1(2(0(1(2(0(1(2(x:S))))))))))))),1(2(1(1(0(1(2(0(1(2(x:S))))))))))> => Not trivial, Overlay, N1, Normal and not trivial cp 0.00/0.08 0.00/0.08 The problem is not joinable. 0.00/0.08 EOF