0.01/0.01 NO 0.01/0.01 0.01/0.01 Problem 1: 0.01/0.01 0.01/0.01 0.01/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.01/0.01 Confluence Problem: 0.01/0.01 (VAR vNonEmpty:S v_NonEmpty:S:S x:S:S) 0.01/0.01 (STRATEGY CONTEXTSENSITIVE 0.01/0.01 (*top*_0 1) 0.01/0.01 (f_0 1) 0.01/0.01 (f_1 1) 0.01/0.01 (g_0 1) 0.01/0.01 (b_0) 0.01/0.01 (fSNonEmpty) 0.01/0.01 (g_1 1) 0.01/0.01 ) 0.01/0.01 (RULES 0.01/0.01 *top*_0(f_0(f_1(f_0(g_0(x:S:S))))) -> *top*_0(f_0(x:S:S)) 0.01/0.01 *top*_0(f_1(f_0(g_0(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(f_1(f_0(g_1(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(g_1(b_0)) -> *top*_0(f_0(g_1(b_0))) 0.01/0.01 f_0(f_0(f_1(f_0(g_0(x:S:S))))) -> f_1(f_0(x:S:S)) 0.01/0.01 f_0(f_1(f_0(g_0(x:S:S)))) -> f_1(x:S:S) 0.01/0.01 f_0(f_1(f_0(g_1(x:S:S)))) -> f_0(x:S:S) 0.01/0.01 f_0(g_1(b_0)) -> f_1(f_0(g_1(b_0))) 0.01/0.01 f_1(f_0(g_0(x:S:S))) -> x:S:S 0.01/0.01 g_0(f_0(f_1(f_0(g_0(x:S:S))))) -> g_0(f_0(x:S:S)) 0.01/0.01 g_0(f_1(f_0(g_0(x:S:S)))) -> g_0(x:S:S) 0.01/0.01 g_0(f_1(f_0(g_1(x:S:S)))) -> g_1(x:S:S) 0.01/0.01 g_0(g_1(b_0)) -> g_0(f_0(g_1(b_0))) 0.01/0.01 ) 0.01/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.01/0.01 0.01/0.01 0.01/0.01 Problem 1: 0.01/0.01 0.01/0.01 CleanTRS Processor: 0.01/0.01 0.01/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.01/0.01 Confluence Problem: 0.01/0.01 (VAR vNonEmpty:S v_NonEmpty:S:S x:S:S) 0.01/0.01 (STRATEGY CONTEXTSENSITIVE 0.01/0.01 (*top*_0 1) 0.01/0.01 (f_0 1) 0.01/0.01 (f_1 1) 0.01/0.01 (g_0 1) 0.01/0.01 (b_0) 0.01/0.01 (fSNonEmpty) 0.01/0.01 (g_1 1) 0.01/0.01 ) 0.01/0.01 (RULES 0.01/0.01 *top*_0(f_0(f_1(f_0(g_0(x:S:S))))) -> *top*_0(f_0(x:S:S)) 0.01/0.01 *top*_0(f_1(f_0(g_0(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(f_1(f_0(g_1(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(g_1(b_0)) -> *top*_0(f_0(g_1(b_0))) 0.01/0.01 f_0(f_0(f_1(f_0(g_0(x:S:S))))) -> f_1(f_0(x:S:S)) 0.01/0.01 f_0(f_1(f_0(g_0(x:S:S)))) -> f_1(x:S:S) 0.01/0.01 f_0(f_1(f_0(g_1(x:S:S)))) -> f_0(x:S:S) 0.01/0.01 f_0(g_1(b_0)) -> f_1(f_0(g_1(b_0))) 0.01/0.01 f_1(f_0(g_0(x:S:S))) -> x:S:S 0.01/0.01 g_0(f_0(f_1(f_0(g_0(x:S:S))))) -> g_0(f_0(x:S:S)) 0.01/0.01 g_0(f_1(f_0(g_0(x:S:S)))) -> g_0(x:S:S) 0.01/0.01 g_0(f_1(f_0(g_1(x:S:S)))) -> g_1(x:S:S) 0.01/0.01 g_0(g_1(b_0)) -> g_0(f_0(g_1(b_0))) 0.01/0.01 ) 0.01/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.01/0.01 0.01/0.01 0.01/0.01 Problem 1: 0.01/0.01 0.01/0.01 Modular Confluence Combinations Decomposition Processor: 0.01/0.01 0.01/0.01 No usable combinations 0.01/0.01 0.01/0.01 Problem 1: 0.01/0.01 Not CS-TRS Processor: 0.01/0.01 R is not a CS-TRS 0.01/0.01 0.01/0.01 Problem 1: 0.01/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.01/0.01 Confluence Problem: 0.01/0.01 (VAR vNonEmpty:S v_NonEmpty:S:S x:S:S) 0.01/0.01 (STRATEGY CONTEXTSENSITIVE 0.01/0.01 (*top*_0 1) 0.01/0.01 (f_0 1) 0.01/0.01 (f_1 1) 0.01/0.01 (g_0 1) 0.01/0.01 (b_0) 0.01/0.01 (fSNonEmpty) 0.01/0.01 (g_1 1) 0.01/0.01 ) 0.01/0.01 (RULES 0.01/0.01 *top*_0(f_0(f_1(f_0(g_0(x:S:S))))) -> *top*_0(f_0(x:S:S)) 0.01/0.01 *top*_0(f_1(f_0(g_0(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(f_1(f_0(g_1(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(g_1(b_0)) -> *top*_0(f_0(g_1(b_0))) 0.01/0.01 f_0(f_0(f_1(f_0(g_0(x:S:S))))) -> f_1(f_0(x:S:S)) 0.01/0.01 f_0(f_1(f_0(g_0(x:S:S)))) -> f_1(x:S:S) 0.01/0.01 f_0(f_1(f_0(g_1(x:S:S)))) -> f_0(x:S:S) 0.01/0.01 f_0(g_1(b_0)) -> f_1(f_0(g_1(b_0))) 0.01/0.01 f_1(f_0(g_0(x:S:S))) -> x:S:S 0.01/0.01 g_0(f_0(f_1(f_0(g_0(x:S:S))))) -> g_0(f_0(x:S:S)) 0.01/0.01 g_0(f_1(f_0(g_0(x:S:S)))) -> g_0(x:S:S) 0.01/0.01 g_0(f_1(f_0(g_1(x:S:S)))) -> g_1(x:S:S) 0.01/0.01 g_0(g_1(b_0)) -> g_0(f_0(g_1(b_0))) 0.01/0.01 ) 0.01/0.01 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.01/0.01 0.01/0.01 Huet Levy Processor: 0.01/0.01 -> Rules: 0.01/0.01 *top*_0(f_0(f_1(f_0(g_0(x:S:S))))) -> *top*_0(f_0(x:S:S)) 0.01/0.01 *top*_0(f_1(f_0(g_0(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(f_1(f_0(g_1(x:S:S)))) -> *top*_0(x:S:S) 0.01/0.01 *top*_0(g_1(b_0)) -> *top*_0(f_0(g_1(b_0))) 0.01/0.01 f_0(f_0(f_1(f_0(g_0(x:S:S))))) -> f_1(f_0(x:S:S)) 0.01/0.01 f_0(f_1(f_0(g_0(x:S:S)))) -> f_1(x:S:S) 0.01/0.01 f_0(f_1(f_0(g_1(x:S:S)))) -> f_0(x:S:S) 0.01/0.01 f_0(g_1(b_0)) -> f_1(f_0(g_1(b_0))) 0.01/0.01 f_1(f_0(g_0(x:S:S))) -> x:S:S 0.01/0.01 g_0(f_0(f_1(f_0(g_0(x:S:S))))) -> g_0(f_0(x:S:S)) 0.01/0.01 g_0(f_1(f_0(g_0(x:S:S)))) -> g_0(x:S:S) 0.01/0.01 g_0(f_1(f_0(g_1(x:S:S)))) -> g_1(x:S:S) 0.01/0.01 g_0(g_1(b_0)) -> g_0(f_0(g_1(b_0))) 0.01/0.01 -> Vars: 0.01/0.01 x:S, x:S, x:S, x:S, x:S, x:S, x:S, x:S, x:S, x:S 0.01/0.01 -> FVars: 0.01/0.01 x3, x4, x5, x6, x7, x8, x9, x10, x11, x12 0.01/0.01 -> PVars: 0.01/0.01 x:S: [x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] 0.01/0.01 0.01/0.01 -> Rlps: 0.01/0.01 (rule: *top*_0(f_0(f_1(f_0(g_0(x3:S))))) -> *top*_0(f_0(x3:S)), id: 1, possubterms: *top*_0(f_0(f_1(f_0(g_0(x3:S)))))->[], f_0(f_1(f_0(g_0(x3:S))))->[1], f_1(f_0(g_0(x3:S)))->[1, 1], f_0(g_0(x3:S))->[1, 1, 1], g_0(x3:S)->[1, 1, 1, 1]) 0.01/0.01 (rule: *top*_0(f_1(f_0(g_0(x4:S)))) -> *top*_0(x4:S), id: 2, possubterms: *top*_0(f_1(f_0(g_0(x4:S))))->[], f_1(f_0(g_0(x4:S)))->[1], f_0(g_0(x4:S))->[1, 1], g_0(x4:S)->[1, 1, 1]) 0.01/0.01 (rule: *top*_0(f_1(f_0(g_1(x5:S)))) -> *top*_0(x5:S), id: 3, possubterms: *top*_0(f_1(f_0(g_1(x5:S))))->[], f_1(f_0(g_1(x5:S)))->[1], f_0(g_1(x5:S))->[1, 1], g_1(x5:S)->[1, 1, 1]) 0.01/0.01 (rule: *top*_0(g_1(b_0)) -> *top*_0(f_0(g_1(b_0))), id: 4, possubterms: *top*_0(g_1(b_0))->[], g_1(b_0)->[1], b_0->[1, 1]) 0.01/0.01 (rule: f_0(f_0(f_1(f_0(g_0(x6:S))))) -> f_1(f_0(x6:S)), id: 5, possubterms: f_0(f_0(f_1(f_0(g_0(x6:S)))))->[], f_0(f_1(f_0(g_0(x6:S))))->[1], f_1(f_0(g_0(x6:S)))->[1, 1], f_0(g_0(x6:S))->[1, 1, 1], g_0(x6:S)->[1, 1, 1, 1]) 0.01/0.01 (rule: f_0(f_1(f_0(g_0(x7:S)))) -> f_1(x7:S), id: 6, possubterms: f_0(f_1(f_0(g_0(x7:S))))->[], f_1(f_0(g_0(x7:S)))->[1], f_0(g_0(x7:S))->[1, 1], g_0(x7:S)->[1, 1, 1]) 0.01/0.01 (rule: f_0(f_1(f_0(g_1(x8:S)))) -> f_0(x8:S), id: 7, possubterms: f_0(f_1(f_0(g_1(x8:S))))->[], f_1(f_0(g_1(x8:S)))->[1], f_0(g_1(x8:S))->[1, 1], g_1(x8:S)->[1, 1, 1]) 0.01/0.01 (rule: f_0(g_1(b_0)) -> f_1(f_0(g_1(b_0))), id: 8, possubterms: f_0(g_1(b_0))->[], g_1(b_0)->[1], b_0->[1, 1]) 0.01/0.01 (rule: f_1(f_0(g_0(x9:S))) -> x9:S, id: 9, possubterms: f_1(f_0(g_0(x9:S)))->[], f_0(g_0(x9:S))->[1], g_0(x9:S)->[1, 1]) 0.01/0.01 (rule: g_0(f_0(f_1(f_0(g_0(x10:S))))) -> g_0(f_0(x10:S)), id: 10, possubterms: g_0(f_0(f_1(f_0(g_0(x10:S)))))->[], f_0(f_1(f_0(g_0(x10:S))))->[1], f_1(f_0(g_0(x10:S)))->[1, 1], f_0(g_0(x10:S))->[1, 1, 1], g_0(x10:S)->[1, 1, 1, 1]) 0.01/0.01 (rule: g_0(f_1(f_0(g_0(x11:S)))) -> g_0(x11:S), id: 11, possubterms: g_0(f_1(f_0(g_0(x11:S))))->[], f_1(f_0(g_0(x11:S)))->[1], f_0(g_0(x11:S))->[1, 1], g_0(x11:S)->[1, 1, 1]) 0.01/0.01 (rule: g_0(f_1(f_0(g_1(x12:S)))) -> g_1(x12:S), id: 12, possubterms: g_0(f_1(f_0(g_1(x12:S))))->[], f_1(f_0(g_1(x12:S)))->[1], f_0(g_1(x12:S))->[1, 1], g_1(x12:S)->[1, 1, 1]) 0.01/0.01 (rule: g_0(g_1(b_0)) -> g_0(f_0(g_1(b_0))), id: 13, possubterms: g_0(g_1(b_0))->[], g_1(b_0)->[1], b_0->[1, 1]) 0.01/0.01 0.01/0.01 -> Unifications: 0.01/0.01 (R1 unifies with R6 at p: [1], l: *top*_0(f_0(f_1(f_0(g_0(x3:S))))), lp: f_0(f_1(f_0(g_0(x3:S)))), sig: {x3:S -> x:S:S}, l': f_0(f_1(f_0(g_0(x:S:S)))), r: *top*_0(f_0(x3:S)), r': f_1(x:S:S)) 0.01/0.01 (R1 unifies with R9 at p: [1,1], l: *top*_0(f_0(f_1(f_0(g_0(x3:S))))), lp: f_1(f_0(g_0(x3:S))), sig: {x3:S -> x:S:S}, l': f_1(f_0(g_0(x:S:S))), r: *top*_0(f_0(x3:S)), r': x:S:S) 0.01/0.01 (R1 unifies with R10 at p: [1,1,1,1], l: *top*_0(f_0(f_1(f_0(g_0(x3:S))))), lp: g_0(x3:S), sig: {x3:S -> f_0(f_1(f_0(g_0(x:S:S))))}, l': g_0(f_0(f_1(f_0(g_0(x:S:S))))), r: *top*_0(f_0(x3:S)), r': g_0(f_0(x:S:S))) 0.01/0.01 (R1 unifies with R11 at p: [1,1,1,1], l: *top*_0(f_0(f_1(f_0(g_0(x3:S))))), lp: g_0(x3:S), sig: {x3:S -> f_1(f_0(g_0(x:S:S)))}, l': g_0(f_1(f_0(g_0(x:S:S)))), r: *top*_0(f_0(x3:S)), r': g_0(x:S:S)) 0.01/0.01 (R1 unifies with R12 at p: [1,1,1,1], l: *top*_0(f_0(f_1(f_0(g_0(x3:S))))), lp: g_0(x3:S), sig: {x3:S -> f_1(f_0(g_1(x:S:S)))}, l': g_0(f_1(f_0(g_1(x:S:S)))), r: *top*_0(f_0(x3:S)), r': g_1(x:S:S)) 0.01/0.01 (R1 unifies with R13 at p: [1,1,1,1], l: *top*_0(f_0(f_1(f_0(g_0(x3:S))))), lp: g_0(x3:S), sig: {x3:S -> g_1(b_0)}, l': g_0(g_1(b_0)), r: *top*_0(f_0(x3:S)), r': g_0(f_0(g_1(b_0)))) 0.01/0.01 (R2 unifies with R9 at p: [1], l: *top*_0(f_1(f_0(g_0(x4:S)))), lp: f_1(f_0(g_0(x4:S))), sig: {x4:S -> x:S:S}, l': f_1(f_0(g_0(x:S:S))), r: *top*_0(x4:S), r': x:S:S) 0.01/0.01 (R2 unifies with R10 at p: [1,1,1], l: *top*_0(f_1(f_0(g_0(x4:S)))), lp: g_0(x4:S), sig: {x4:S -> f_0(f_1(f_0(g_0(x:S:S))))}, l': g_0(f_0(f_1(f_0(g_0(x:S:S))))), r: *top*_0(x4:S), r': g_0(f_0(x:S:S))) 0.01/0.01 (R2 unifies with R11 at p: [1,1,1], l: *top*_0(f_1(f_0(g_0(x4:S)))), lp: g_0(x4:S), sig: {x4:S -> f_1(f_0(g_0(x:S:S)))}, l': g_0(f_1(f_0(g_0(x:S:S)))), r: *top*_0(x4:S), r': g_0(x:S:S)) 0.01/0.01 (R2 unifies with R12 at p: [1,1,1], l: *top*_0(f_1(f_0(g_0(x4:S)))), lp: g_0(x4:S), sig: {x4:S -> f_1(f_0(g_1(x:S:S)))}, l': g_0(f_1(f_0(g_1(x:S:S)))), r: *top*_0(x4:S), r': g_1(x:S:S)) 0.01/0.01 (R2 unifies with R13 at p: [1,1,1], l: *top*_0(f_1(f_0(g_0(x4:S)))), lp: g_0(x4:S), sig: {x4:S -> g_1(b_0)}, l': g_0(g_1(b_0)), r: *top*_0(x4:S), r': g_0(f_0(g_1(b_0)))) 0.01/0.01 (R3 unifies with R8 at p: [1,1], l: *top*_0(f_1(f_0(g_1(x5:S)))), lp: f_0(g_1(x5:S)), sig: {x5:S -> b_0}, l': f_0(g_1(b_0)), r: *top*_0(x5:S), r': f_1(f_0(g_1(b_0)))) 0.01/0.01 (R5 unifies with R6 at p: [1], l: f_0(f_0(f_1(f_0(g_0(x6:S))))), lp: f_0(f_1(f_0(g_0(x6:S)))), sig: {x6:S -> x:S:S}, l': f_0(f_1(f_0(g_0(x:S:S)))), r: f_1(f_0(x6:S)), r': f_1(x:S:S)) 0.01/0.01 (R5 unifies with R9 at p: [1,1], l: f_0(f_0(f_1(f_0(g_0(x6:S))))), lp: f_1(f_0(g_0(x6:S))), sig: {x6:S -> x:S:S}, l': f_1(f_0(g_0(x:S:S))), r: f_1(f_0(x6:S)), r': x:S:S) 0.01/0.01 (R5 unifies with R10 at p: [1,1,1,1], l: f_0(f_0(f_1(f_0(g_0(x6:S))))), lp: g_0(x6:S), sig: {x6:S -> f_0(f_1(f_0(g_0(x:S:S))))}, l': g_0(f_0(f_1(f_0(g_0(x:S:S))))), r: f_1(f_0(x6:S)), r': g_0(f_0(x:S:S))) 0.01/0.01 (R5 unifies with R11 at p: [1,1,1,1], l: f_0(f_0(f_1(f_0(g_0(x6:S))))), lp: g_0(x6:S), sig: {x6:S -> f_1(f_0(g_0(x:S:S)))}, l': g_0(f_1(f_0(g_0(x:S:S)))), r: f_1(f_0(x6:S)), r': g_0(x:S:S)) 0.01/0.01 (R5 unifies with R12 at p: [1,1,1,1], l: f_0(f_0(f_1(f_0(g_0(x6:S))))), lp: g_0(x6:S), sig: {x6:S -> f_1(f_0(g_1(x:S:S)))}, l': g_0(f_1(f_0(g_1(x:S:S)))), r: f_1(f_0(x6:S)), r': g_1(x:S:S)) 0.01/0.01 (R5 unifies with R13 at p: [1,1,1,1], l: f_0(f_0(f_1(f_0(g_0(x6:S))))), lp: g_0(x6:S), sig: {x6:S -> g_1(b_0)}, l': g_0(g_1(b_0)), r: f_1(f_0(x6:S)), r': g_0(f_0(g_1(b_0)))) 0.01/0.01 (R6 unifies with R9 at p: [1], l: f_0(f_1(f_0(g_0(x7:S)))), lp: f_1(f_0(g_0(x7:S))), sig: {x7:S -> x:S:S}, l': f_1(f_0(g_0(x:S:S))), r: f_1(x7:S), r': x:S:S) 0.01/0.01 (R6 unifies with R10 at p: [1,1,1], l: f_0(f_1(f_0(g_0(x7:S)))), lp: g_0(x7:S), sig: {x7:S -> f_0(f_1(f_0(g_0(x:S:S))))}, l': g_0(f_0(f_1(f_0(g_0(x:S:S))))), r: f_1(x7:S), r': g_0(f_0(x:S:S))) 0.01/0.01 (R6 unifies with R11 at p: [1,1,1], l: f_0(f_1(f_0(g_0(x7:S)))), lp: g_0(x7:S), sig: {x7:S -> f_1(f_0(g_0(x:S:S)))}, l': g_0(f_1(f_0(g_0(x:S:S)))), r: f_1(x7:S), r': g_0(x:S:S)) 0.01/0.01 (R6 unifies with R12 at p: [1,1,1], l: f_0(f_1(f_0(g_0(x7:S)))), lp: g_0(x7:S), sig: {x7:S -> f_1(f_0(g_1(x:S:S)))}, l': g_0(f_1(f_0(g_1(x:S:S)))), r: f_1(x7:S), r': g_1(x:S:S)) 0.01/0.01 (R6 unifies with R13 at p: [1,1,1], l: f_0(f_1(f_0(g_0(x7:S)))), lp: g_0(x7:S), sig: {x7:S -> g_1(b_0)}, l': g_0(g_1(b_0)), r: f_1(x7:S), r': g_0(f_0(g_1(b_0)))) 0.01/0.01 (R7 unifies with R8 at p: [1,1], l: f_0(f_1(f_0(g_1(x8:S)))), lp: f_0(g_1(x8:S)), sig: {x8:S -> b_0}, l': f_0(g_1(b_0)), r: f_0(x8:S), r': f_1(f_0(g_1(b_0)))) 0.01/0.01 (R9 unifies with R10 at p: [1,1], l: f_1(f_0(g_0(x9:S))), lp: g_0(x9:S), sig: {x9:S -> f_0(f_1(f_0(g_0(x:S:S))))}, l': g_0(f_0(f_1(f_0(g_0(x:S:S))))), r: x9:S, r': g_0(f_0(x:S:S))) 0.01/0.01 (R9 unifies with R11 at p: [1,1], l: f_1(f_0(g_0(x9:S))), lp: g_0(x9:S), sig: {x9:S -> f_1(f_0(g_0(x:S:S)))}, l': g_0(f_1(f_0(g_0(x:S:S)))), r: x9:S, r': g_0(x:S:S)) 0.01/0.01 (R9 unifies with R12 at p: [1,1], l: f_1(f_0(g_0(x9:S))), lp: g_0(x9:S), sig: {x9:S -> f_1(f_0(g_1(x:S:S)))}, l': g_0(f_1(f_0(g_1(x:S:S)))), r: x9:S, r': g_1(x:S:S)) 0.01/0.01 (R9 unifies with R13 at p: [1,1], l: f_1(f_0(g_0(x9:S))), lp: g_0(x9:S), sig: {x9:S -> g_1(b_0)}, l': g_0(g_1(b_0)), r: x9:S, r': g_0(f_0(g_1(b_0)))) 0.01/0.01 (R10 unifies with R6 at p: [1], l: g_0(f_0(f_1(f_0(g_0(x10:S))))), lp: f_0(f_1(f_0(g_0(x10:S)))), sig: {x10:S -> x:S:S}, l': f_0(f_1(f_0(g_0(x:S:S)))), r: g_0(f_0(x10:S)), r': f_1(x:S:S)) 0.01/0.01 (R10 unifies with R9 at p: [1,1], l: g_0(f_0(f_1(f_0(g_0(x10:S))))), lp: f_1(f_0(g_0(x10:S))), sig: {x10:S -> x:S:S}, l': f_1(f_0(g_0(x:S:S))), r: g_0(f_0(x10:S)), r': x:S:S) 0.01/0.01 (R10 unifies with R10 at p: [1,1,1,1], l: g_0(f_0(f_1(f_0(g_0(x10:S))))), lp: g_0(x10:S), sig: {x10:S -> f_0(f_1(f_0(g_0(x:S:S))))}, l': g_0(f_0(f_1(f_0(g_0(x:S:S))))), r: g_0(f_0(x10:S)), r': g_0(f_0(x:S:S))) 0.01/0.01 (R10 unifies with R11 at p: [1,1,1,1], l: g_0(f_0(f_1(f_0(g_0(x10:S))))), lp: g_0(x10:S), sig: {x10:S -> f_1(f_0(g_0(x:S:S)))}, l': g_0(f_1(f_0(g_0(x:S:S)))), r: g_0(f_0(x10:S)), r': g_0(x:S:S)) 0.01/0.01 (R10 unifies with R12 at p: [1,1,1,1], l: g_0(f_0(f_1(f_0(g_0(x10:S))))), lp: g_0(x10:S), sig: {x10:S -> f_1(f_0(g_1(x:S:S)))}, l': g_0(f_1(f_0(g_1(x:S:S)))), r: g_0(f_0(x10:S)), r': g_1(x:S:S)) 0.01/0.01 (R10 unifies with R13 at p: [1,1,1,1], l: g_0(f_0(f_1(f_0(g_0(x10:S))))), lp: g_0(x10:S), sig: {x10:S -> g_1(b_0)}, l': g_0(g_1(b_0)), r: g_0(f_0(x10:S)), r': g_0(f_0(g_1(b_0)))) 0.01/0.01 (R11 unifies with R9 at p: [1], l: g_0(f_1(f_0(g_0(x11:S)))), lp: f_1(f_0(g_0(x11:S))), sig: {x11:S -> x:S:S}, l': f_1(f_0(g_0(x:S:S))), r: g_0(x11:S), r': x:S:S) 0.01/0.01 (R11 unifies with R10 at p: [1,1,1], l: g_0(f_1(f_0(g_0(x11:S)))), lp: g_0(x11:S), sig: {x11:S -> f_0(f_1(f_0(g_0(x:S:S))))}, l': g_0(f_0(f_1(f_0(g_0(x:S:S))))), r: g_0(x11:S), r': g_0(f_0(x:S:S))) 0.01/0.01 (R11 unifies with R11 at p: [1,1,1], l: g_0(f_1(f_0(g_0(x11:S)))), lp: g_0(x11:S), sig: {x11:S -> f_1(f_0(g_0(x:S:S)))}, l': g_0(f_1(f_0(g_0(x:S:S)))), r: g_0(x11:S), r': g_0(x:S:S)) 0.01/0.01 (R11 unifies with R12 at p: [1,1,1], l: g_0(f_1(f_0(g_0(x11:S)))), lp: g_0(x11:S), sig: {x11:S -> f_1(f_0(g_1(x:S:S)))}, l': g_0(f_1(f_0(g_1(x:S:S)))), r: g_0(x11:S), r': g_1(x:S:S)) 0.01/0.01 (R11 unifies with R13 at p: [1,1,1], l: g_0(f_1(f_0(g_0(x11:S)))), lp: g_0(x11:S), sig: {x11:S -> g_1(b_0)}, l': g_0(g_1(b_0)), r: g_0(x11:S), r': g_0(f_0(g_1(b_0)))) 0.01/0.01 (R12 unifies with R8 at p: [1,1], l: g_0(f_1(f_0(g_1(x12:S)))), lp: f_0(g_1(x12:S)), sig: {x12:S -> b_0}, l': f_0(g_1(b_0)), r: g_1(x12:S), r': f_1(f_0(g_1(b_0)))) 0.01/0.01 0.01/0.01 -> Critical pairs info: 0.01/0.01 <*top*_0(f_1(f_1(f_0(g_1(b_0))))),*top*_0(b_0)> => Not trivial, Not overlay, NW0, N1 0.01/0.01 <*top*_0(f_0(f_1(f_0(g_0(f_0(x:S:S)))))),*top*_0(f_0(f_0(f_1(f_0(g_0(x:S:S))))))> => Not trivial, Not overlay, NW0, N2 0.01/0.01 => Trivial, Not overlay, NW0, N3 0.01/0.01 <*top*_0(f_0(f_1(f_0(g_0(f_0(g_1(b_0))))))),*top*_0(f_0(g_1(b_0)))> => Not trivial, Not overlay, NW0, N4 0.01/0.01 => Not trivial, Not overlay, NW0, N5 0.01/0.01 => Not trivial, Not overlay, NW0, N6 0.01/0.01 => Not trivial, Not overlay, NW0, N7 0.01/0.01 => Trivial, Not overlay, NW0, N8 0.01/0.01 => Not trivial, Not overlay, NW0, N9 0.01/0.01 => Not trivial, Not overlay, NW0, N10 0.01/0.01 <*top*_0(f_0(f_1(f_0(g_0(x:S:S))))),*top*_0(f_0(f_1(f_0(g_0(x:S:S)))))> => Trivial, Not overlay, NW0, N11 0.01/0.01 => Not trivial, Not overlay, NW0, N12 0.01/0.01 => Trivial, Not overlay, NW0, N13 0.01/0.01 <*top*_0(f_1(f_0(g_0(f_0(x:S:S))))),*top*_0(f_0(f_1(f_0(g_0(x:S:S)))))> => Not trivial, Not overlay, NW0, N14 0.01/0.01 => Not trivial, Not overlay, NW0, N15 0.01/0.01 => Not trivial, Not overlay, NW0, N16 0.01/0.01 => Trivial, Not overlay, NW0, N17 0.01/0.01 <*top*_0(f_1(f_0(g_1(x:S:S)))),*top*_0(f_1(f_0(g_1(x:S:S))))> => Trivial, Not overlay, NW0, N18 0.01/0.01 => Not trivial, Not overlay, NW0, N19 0.01/0.01 => Not trivial, Not overlay, NW0, N20 0.01/0.01 => Not trivial, Not overlay, NW0, N21 0.01/0.01 <*top*_0(f_1(f_0(g_0(f_0(g_1(b_0)))))),*top*_0(g_1(b_0))> => Not trivial, Not overlay, NW0, N22 0.01/0.01 => Not trivial, Not overlay, NW0, N23 0.01/0.01 <*top*_0(f_1(f_0(g_0(x:S:S)))),*top*_0(f_1(f_0(g_0(x:S:S))))> => Trivial, Not overlay, NW0, N24 0.01/0.01 => Not trivial, Not overlay, NW0, N25 0.01/0.01 => Not trivial, Not overlay, NW0, N26 0.01/0.01 => Not trivial, Not overlay, NW0, N27 0.01/0.01 <*top*_0(f_0(f_1(f_0(g_1(x:S:S))))),*top*_0(f_0(f_1(f_0(g_1(x:S:S)))))> => Trivial, Not overlay, NW0, N28 0.01/0.01 => Not trivial, Not overlay, NW0, N29 0.01/0.01 => Trivial, Not overlay, NW0, N30 0.01/0.01 <*top*_0(f_1(x:S:S)),*top*_0(f_0(x:S:S))> => Not trivial, Not overlay, NW0, N31 0.01/0.01 => Trivial, Not overlay, NW0, N32 0.01/0.01 => Trivial, Not overlay, NW0, N33 0.01/0.01 <*top*_0(f_0(x:S:S)),*top*_0(f_0(x:S:S))> => Trivial, Not overlay, NW0, N34 0.01/0.01 => Not trivial, Not overlay, NW0, N35 0.01/0.01 => Not trivial, Not overlay, NW0, N36 0.01/0.01 => Not trivial, Not overlay, NW0, N37 0.01/0.01 <*top*_0(x:S:S),*top*_0(x:S:S)> => Trivial, Not overlay, NW0, N38 0.01/0.01 => Trivial, Not overlay, NW0, N39 0.01/0.01 => Not trivial, Not overlay, NW0, N40 0.01/0.01 0.01/0.01 -> Problem conclusions: 0.01/0.01 Left linear, Right linear, Linear 0.01/0.01 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.01/0.01 Not Huet-Levy confluent, Not Newman confluent 0.01/0.01 R is a TRS 0.01/0.01 0.01/0.01 0.01/0.01 Problem 1: 0.01/0.01 Different Normal CP Terms Processor: 0.01/0.01 => Not trivial, Not overlay, NW0, N7, Normal and not trivial cp 0.01/0.01 0.01/0.01 The problem is not joinable. 0.01/0.01 0.08user 0.00system 0:00.10elapsed 87%CPU (0avgtext+0avgdata 11100maxresident)k 0.01/0.01 1904inputs+0outputs (9major+1177minor)pagefaults 0swaps