NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (0 1) (1 1) (2 1) (4 1) (5 1) (3 1) (fSNonEmpty) ) (RULES 0(1(5(5(5(3(5(x))))))) -> 5(3(2(5(1(0(1(2(0(5(x)))))))))) 0(2(5(3(4(x))))) -> 3(2(4(3(1(5(1(1(3(4(x)))))))))) 0(4(4(5(5(5(x)))))) -> 0(4(4(4(3(3(4(1(3(1(x)))))))))) 1(2(4(5(2(4(x)))))) -> 3(3(5(3(0(4(0(3(1(3(x)))))))))) 2(5(0(4(x)))) -> 4(4(3(2(4(4(5(1(0(0(x)))))))))) 2(5(5(3(4(x))))) -> 4(5(4(3(1(4(0(2(4(4(x)))))))))) 2(5(5(x))) -> 4(2(5(4(4(0(0(1(1(2(x)))))))))) 4(1(5(5(0(4(x)))))) -> 1(0(3(0(4(2(4(4(3(4(x)))))))))) 4(2(5(5(1(5(x)))))) -> 2(3(4(2(1(1(3(4(2(5(x)))))))))) 4(4(5(2(4(2(2(x))))))) -> 4(0(5(5(4(5(1(2(2(1(x)))))))))) 4(5(2(4(x)))) -> 4(1(5(5(2(0(3(1(3(3(x)))))))))) 4(5(5(5(x)))) -> 1(5(1(2(0(3(2(1(0(5(x)))))))))) 5(2(4(x))) -> 0(5(0(2(3(3(4(2(4(2(x)))))))))) 5(2(5(5(0(4(x)))))) -> 0(4(2(3(3(5(2(1(4(4(x)))))))))) 5(5(2(4(5(0(x)))))) -> 2(1(1(4(2(4(0(4(2(0(x)))))))))) 5(5(2(x))) -> 0(1(3(2(3(0(3(2(5(3(x)))))))))) 5(5(5(1(4(x))))) -> 3(3(0(5(0(4(3(4(4(0(x)))))))))) 5(5(5(x))) -> 5(3(4(1(0(1(4(5(0(0(x)))))))))) 5(5(3(x))) -> 0(3(5(4(4(1(0(1(5(0(x)))))))))) 5(5(x)) -> 0(5(4(0(2(5(4(5(2(1(x)))))))))) 5(5(x)) -> 3(4(1(1(1(1(4(4(0(4(x)))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (0 1) (1 1) (2 1) (4 1) (5 1) (3 1) (fSNonEmpty) ) (RULES 0(1(5(5(5(3(5(x))))))) -> 5(3(2(5(1(0(1(2(0(5(x)))))))))) 0(2(5(3(4(x))))) -> 3(2(4(3(1(5(1(1(3(4(x)))))))))) 0(4(4(5(5(5(x)))))) -> 0(4(4(4(3(3(4(1(3(1(x)))))))))) 1(2(4(5(2(4(x)))))) -> 3(3(5(3(0(4(0(3(1(3(x)))))))))) 2(5(0(4(x)))) -> 4(4(3(2(4(4(5(1(0(0(x)))))))))) 2(5(5(3(4(x))))) -> 4(5(4(3(1(4(0(2(4(4(x)))))))))) 2(5(5(x))) -> 4(2(5(4(4(0(0(1(1(2(x)))))))))) 4(1(5(5(0(4(x)))))) -> 1(0(3(0(4(2(4(4(3(4(x)))))))))) 4(2(5(5(1(5(x)))))) -> 2(3(4(2(1(1(3(4(2(5(x)))))))))) 4(4(5(2(4(2(2(x))))))) -> 4(0(5(5(4(5(1(2(2(1(x)))))))))) 4(5(2(4(x)))) -> 4(1(5(5(2(0(3(1(3(3(x)))))))))) 4(5(5(5(x)))) -> 1(5(1(2(0(3(2(1(0(5(x)))))))))) 5(2(4(x))) -> 0(5(0(2(3(3(4(2(4(2(x)))))))))) 5(2(5(5(0(4(x)))))) -> 0(4(2(3(3(5(2(1(4(4(x)))))))))) 5(5(2(4(5(0(x)))))) -> 2(1(1(4(2(4(0(4(2(0(x)))))))))) 5(5(2(x))) -> 0(1(3(2(3(0(3(2(5(3(x)))))))))) 5(5(5(1(4(x))))) -> 3(3(0(5(0(4(3(4(4(0(x)))))))))) 5(5(5(x))) -> 5(3(4(1(0(1(4(5(0(0(x)))))))))) 5(5(3(x))) -> 0(3(5(4(4(1(0(1(5(0(x)))))))))) 5(5(x)) -> 0(5(4(0(2(5(4(5(2(1(x)))))))))) 5(5(x)) -> 3(4(1(1(1(1(4(4(0(4(x)))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: 0(1(5(5(5(3(5(x))))))) -> 5(3(2(5(1(0(1(2(0(5(x)))))))))) 0(2(5(3(4(x))))) -> 3(2(4(3(1(5(1(1(3(4(x)))))))))) 0(4(4(5(5(5(x)))))) -> 0(4(4(4(3(3(4(1(3(1(x)))))))))) 1(2(4(5(2(4(x)))))) -> 3(3(5(3(0(4(0(3(1(3(x)))))))))) 2(5(0(4(x)))) -> 4(4(3(2(4(4(5(1(0(0(x)))))))))) 2(5(5(3(4(x))))) -> 4(5(4(3(1(4(0(2(4(4(x)))))))))) 2(5(5(x))) -> 4(2(5(4(4(0(0(1(1(2(x)))))))))) 4(1(5(5(0(4(x)))))) -> 1(0(3(0(4(2(4(4(3(4(x)))))))))) 4(2(5(5(1(5(x)))))) -> 2(3(4(2(1(1(3(4(2(5(x)))))))))) 4(4(5(2(4(2(2(x))))))) -> 4(0(5(5(4(5(1(2(2(1(x)))))))))) 4(5(2(4(x)))) -> 4(1(5(5(2(0(3(1(3(3(x)))))))))) 4(5(5(5(x)))) -> 1(5(1(2(0(3(2(1(0(5(x)))))))))) 5(2(4(x))) -> 0(5(0(2(3(3(4(2(4(2(x)))))))))) 5(2(5(5(0(4(x)))))) -> 0(4(2(3(3(5(2(1(4(4(x)))))))))) 5(5(2(4(5(0(x)))))) -> 2(1(1(4(2(4(0(4(2(0(x)))))))))) 5(5(2(x))) -> 0(1(3(2(3(0(3(2(5(3(x)))))))))) 5(5(5(1(4(x))))) -> 3(3(0(5(0(4(3(4(4(0(x)))))))))) 5(5(5(x))) -> 5(3(4(1(0(1(4(5(0(0(x)))))))))) 5(5(3(x))) -> 0(3(5(4(4(1(0(1(5(0(x)))))))))) 5(5(x)) -> 0(5(4(0(2(5(4(5(2(1(x)))))))))) 5(5(x)) -> 3(4(1(1(1(1(4(4(0(4(x)))))))))) -> Vars: x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x -> Rlps: (rule: 0(1(5(5(5(3(5(x))))))) -> 5(3(2(5(1(0(1(2(0(5(x)))))))))), id: 1, possubterms: 0(1(5(5(5(3(5(x)))))))->[], 1(5(5(5(3(5(x))))))->[1], 5(5(5(3(5(x)))))->[1, 1], 5(5(3(5(x))))->[1, 1, 1], 5(3(5(x)))->[1, 1, 1, 1], 3(5(x))->[1, 1, 1, 1, 1], 5(x)->[1, 1, 1, 1, 1, 1]) (rule: 0(2(5(3(4(x))))) -> 3(2(4(3(1(5(1(1(3(4(x)))))))))), id: 2, possubterms: 0(2(5(3(4(x)))))->[], 2(5(3(4(x))))->[1], 5(3(4(x)))->[1, 1], 3(4(x))->[1, 1, 1], 4(x)->[1, 1, 1, 1]) (rule: 0(4(4(5(5(5(x)))))) -> 0(4(4(4(3(3(4(1(3(1(x)))))))))), id: 3, possubterms: 0(4(4(5(5(5(x))))))->[], 4(4(5(5(5(x)))))->[1], 4(5(5(5(x))))->[1, 1], 5(5(5(x)))->[1, 1, 1], 5(5(x))->[1, 1, 1, 1], 5(x)->[1, 1, 1, 1, 1]) (rule: 1(2(4(5(2(4(x)))))) -> 3(3(5(3(0(4(0(3(1(3(x)))))))))), id: 4, possubterms: 1(2(4(5(2(4(x))))))->[], 2(4(5(2(4(x)))))->[1], 4(5(2(4(x))))->[1, 1], 5(2(4(x)))->[1, 1, 1], 2(4(x))->[1, 1, 1, 1], 4(x)->[1, 1, 1, 1, 1]) (rule: 2(5(0(4(x)))) -> 4(4(3(2(4(4(5(1(0(0(x)))))))))), id: 5, possubterms: 2(5(0(4(x))))->[], 5(0(4(x)))->[1], 0(4(x))->[1, 1], 4(x)->[1, 1, 1]) (rule: 2(5(5(3(4(x))))) -> 4(5(4(3(1(4(0(2(4(4(x)))))))))), id: 6, possubterms: 2(5(5(3(4(x)))))->[], 5(5(3(4(x))))->[1], 5(3(4(x)))->[1, 1], 3(4(x))->[1, 1, 1], 4(x)->[1, 1, 1, 1]) (rule: 2(5(5(x))) -> 4(2(5(4(4(0(0(1(1(2(x)))))))))), id: 7, possubterms: 2(5(5(x)))->[], 5(5(x))->[1], 5(x)->[1, 1]) (rule: 4(1(5(5(0(4(x)))))) -> 1(0(3(0(4(2(4(4(3(4(x)))))))))), id: 8, possubterms: 4(1(5(5(0(4(x))))))->[], 1(5(5(0(4(x)))))->[1], 5(5(0(4(x))))->[1, 1], 5(0(4(x)))->[1, 1, 1], 0(4(x))->[1, 1, 1, 1], 4(x)->[1, 1, 1, 1, 1]) (rule: 4(2(5(5(1(5(x)))))) -> 2(3(4(2(1(1(3(4(2(5(x)))))))))), id: 9, possubterms: 4(2(5(5(1(5(x))))))->[], 2(5(5(1(5(x)))))->[1], 5(5(1(5(x))))->[1, 1], 5(1(5(x)))->[1, 1, 1], 1(5(x))->[1, 1, 1, 1], 5(x)->[1, 1, 1, 1, 1]) (rule: 4(4(5(2(4(2(2(x))))))) -> 4(0(5(5(4(5(1(2(2(1(x)))))))))), id: 10, possubterms: 4(4(5(2(4(2(2(x)))))))->[], 4(5(2(4(2(2(x))))))->[1], 5(2(4(2(2(x)))))->[1, 1], 2(4(2(2(x))))->[1, 1, 1], 4(2(2(x)))->[1, 1, 1, 1], 2(2(x))->[1, 1, 1, 1, 1], 2(x)->[1, 1, 1, 1, 1, 1]) (rule: 4(5(2(4(x)))) -> 4(1(5(5(2(0(3(1(3(3(x)))))))))), id: 11, possubterms: 4(5(2(4(x))))->[], 5(2(4(x)))->[1], 2(4(x))->[1, 1], 4(x)->[1, 1, 1]) (rule: 4(5(5(5(x)))) -> 1(5(1(2(0(3(2(1(0(5(x)))))))))), id: 12, possubterms: 4(5(5(5(x))))->[], 5(5(5(x)))->[1], 5(5(x))->[1, 1], 5(x)->[1, 1, 1]) (rule: 5(2(4(x))) -> 0(5(0(2(3(3(4(2(4(2(x)))))))))), id: 13, possubterms: 5(2(4(x)))->[], 2(4(x))->[1], 4(x)->[1, 1]) (rule: 5(2(5(5(0(4(x)))))) -> 0(4(2(3(3(5(2(1(4(4(x)))))))))), id: 14, possubterms: 5(2(5(5(0(4(x))))))->[], 2(5(5(0(4(x)))))->[1], 5(5(0(4(x))))->[1, 1], 5(0(4(x)))->[1, 1, 1], 0(4(x))->[1, 1, 1, 1], 4(x)->[1, 1, 1, 1, 1]) (rule: 5(5(2(4(5(0(x)))))) -> 2(1(1(4(2(4(0(4(2(0(x)))))))))), id: 15, possubterms: 5(5(2(4(5(0(x))))))->[], 5(2(4(5(0(x)))))->[1], 2(4(5(0(x))))->[1, 1], 4(5(0(x)))->[1, 1, 1], 5(0(x))->[1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1]) (rule: 5(5(2(x))) -> 0(1(3(2(3(0(3(2(5(3(x)))))))))), id: 16, possubterms: 5(5(2(x)))->[], 5(2(x))->[1], 2(x)->[1, 1]) (rule: 5(5(5(1(4(x))))) -> 3(3(0(5(0(4(3(4(4(0(x)))))))))), id: 17, possubterms: 5(5(5(1(4(x)))))->[], 5(5(1(4(x))))->[1], 5(1(4(x)))->[1, 1], 1(4(x))->[1, 1, 1], 4(x)->[1, 1, 1, 1]) (rule: 5(5(5(x))) -> 5(3(4(1(0(1(4(5(0(0(x)))))))))), id: 18, possubterms: 5(5(5(x)))->[], 5(5(x))->[1], 5(x)->[1, 1]) (rule: 5(5(3(x))) -> 0(3(5(4(4(1(0(1(5(0(x)))))))))), id: 19, possubterms: 5(5(3(x)))->[], 5(3(x))->[1], 3(x)->[1, 1]) (rule: 5(5(x)) -> 0(5(4(0(2(5(4(5(2(1(x)))))))))), id: 20, possubterms: 5(5(x))->[], 5(x)->[1]) (rule: 5(5(x)) -> 3(4(1(1(1(1(4(4(0(4(x)))))))))), id: 21, possubterms: 5(5(x))->[], 5(x)->[1]) -> Unifications: (R1 unifies with R18 at p: [1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(5(5(3(5(x))))), sig: {x' -> 3(5(x))}, l': 5(5(5(x'))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R1 unifies with R20 at p: [1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(5(5(3(5(x))))), sig: {x' -> 5(3(5(x)))}, l': 5(5(x')), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R1 unifies with R21 at p: [1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(5(5(3(5(x))))), sig: {x' -> 5(3(5(x)))}, l': 5(5(x')), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R1 unifies with R19 at p: [1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(5(3(5(x)))), sig: {x' -> 5(x)}, l': 5(5(3(x'))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R1 unifies with R20 at p: [1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(5(3(5(x)))), sig: {x' -> 3(5(x))}, l': 5(5(x')), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R1 unifies with R21 at p: [1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(5(3(5(x)))), sig: {x' -> 3(5(x))}, l': 5(5(x')), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R1 unifies with R13 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R1 unifies with R14 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R1 unifies with R15 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R1 unifies with R16 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R1 unifies with R17 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R1 unifies with R18 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R1 unifies with R19 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R1 unifies with R20 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R1 unifies with R21 at p: [1,1,1,1,1,1], l: 0(1(5(5(5(3(5(x))))))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 5(3(2(5(1(0(1(2(0(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R2 unifies with R8 at p: [1,1,1,1], l: 0(2(5(3(4(x))))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 3(2(4(3(1(5(1(1(3(4(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R2 unifies with R9 at p: [1,1,1,1], l: 0(2(5(3(4(x))))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 3(2(4(3(1(5(1(1(3(4(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R2 unifies with R10 at p: [1,1,1,1], l: 0(2(5(3(4(x))))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 3(2(4(3(1(5(1(1(3(4(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R2 unifies with R11 at p: [1,1,1,1], l: 0(2(5(3(4(x))))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 3(2(4(3(1(5(1(1(3(4(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R2 unifies with R12 at p: [1,1,1,1], l: 0(2(5(3(4(x))))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 3(2(4(3(1(5(1(1(3(4(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R3 unifies with R12 at p: [1,1], l: 0(4(4(5(5(5(x)))))), lp: 4(5(5(5(x)))), sig: {x -> x'}, l': 4(5(5(5(x')))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R3 unifies with R17 at p: [1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(5(x))), sig: {x -> 1(4(x'))}, l': 5(5(5(1(4(x'))))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R3 unifies with R18 at p: [1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(5(x))), sig: {x -> x'}, l': 5(5(5(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R3 unifies with R20 at p: [1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(5(x))), sig: {x' -> 5(x)}, l': 5(5(x')), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R3 unifies with R21 at p: [1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(5(x))), sig: {x' -> 5(x)}, l': 5(5(x')), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R3 unifies with R15 at p: [1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(x)), sig: {x -> 2(4(5(0(x'))))}, l': 5(5(2(4(5(0(x')))))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R3 unifies with R16 at p: [1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(x)), sig: {x -> 2(x')}, l': 5(5(2(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R3 unifies with R17 at p: [1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(x)), sig: {x -> 5(1(4(x')))}, l': 5(5(5(1(4(x'))))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R3 unifies with R18 at p: [1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(x)), sig: {x -> 5(x')}, l': 5(5(5(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R3 unifies with R19 at p: [1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(x)), sig: {x -> 3(x')}, l': 5(5(3(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R3 unifies with R20 at p: [1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R3 unifies with R21 at p: [1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R3 unifies with R13 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R3 unifies with R14 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R3 unifies with R15 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R3 unifies with R16 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R3 unifies with R17 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R3 unifies with R18 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R3 unifies with R19 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R3 unifies with R20 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R3 unifies with R21 at p: [1,1,1,1,1], l: 0(4(4(5(5(5(x)))))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 0(4(4(4(3(3(4(1(3(1(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R4 unifies with R11 at p: [1,1], l: 1(2(4(5(2(4(x)))))), lp: 4(5(2(4(x)))), sig: {x -> x'}, l': 4(5(2(4(x')))), r: 3(3(5(3(0(4(0(3(1(3(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R4 unifies with R13 at p: [1,1,1], l: 1(2(4(5(2(4(x)))))), lp: 5(2(4(x))), sig: {x -> x'}, l': 5(2(4(x'))), r: 3(3(5(3(0(4(0(3(1(3(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R4 unifies with R8 at p: [1,1,1,1,1], l: 1(2(4(5(2(4(x)))))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 3(3(5(3(0(4(0(3(1(3(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R4 unifies with R9 at p: [1,1,1,1,1], l: 1(2(4(5(2(4(x)))))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 3(3(5(3(0(4(0(3(1(3(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R4 unifies with R10 at p: [1,1,1,1,1], l: 1(2(4(5(2(4(x)))))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 3(3(5(3(0(4(0(3(1(3(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R4 unifies with R11 at p: [1,1,1,1,1], l: 1(2(4(5(2(4(x)))))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 3(3(5(3(0(4(0(3(1(3(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R4 unifies with R12 at p: [1,1,1,1,1], l: 1(2(4(5(2(4(x)))))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 3(3(5(3(0(4(0(3(1(3(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R5 unifies with R3 at p: [1,1], l: 2(5(0(4(x)))), lp: 0(4(x)), sig: {x -> 4(5(5(5(x'))))}, l': 0(4(4(5(5(5(x')))))), r: 4(4(3(2(4(4(5(1(0(0(x)))))))))), r': 0(4(4(4(3(3(4(1(3(1(x'))))))))))) (R5 unifies with R8 at p: [1,1,1], l: 2(5(0(4(x)))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 4(4(3(2(4(4(5(1(0(0(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R5 unifies with R9 at p: [1,1,1], l: 2(5(0(4(x)))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 4(4(3(2(4(4(5(1(0(0(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R5 unifies with R10 at p: [1,1,1], l: 2(5(0(4(x)))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 4(4(3(2(4(4(5(1(0(0(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R5 unifies with R11 at p: [1,1,1], l: 2(5(0(4(x)))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 4(4(3(2(4(4(5(1(0(0(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R5 unifies with R12 at p: [1,1,1], l: 2(5(0(4(x)))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 4(4(3(2(4(4(5(1(0(0(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R6 unifies with R19 at p: [1], l: 2(5(5(3(4(x))))), lp: 5(5(3(4(x)))), sig: {x' -> 4(x)}, l': 5(5(3(x'))), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R6 unifies with R20 at p: [1], l: 2(5(5(3(4(x))))), lp: 5(5(3(4(x)))), sig: {x' -> 3(4(x))}, l': 5(5(x')), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R6 unifies with R21 at p: [1], l: 2(5(5(3(4(x))))), lp: 5(5(3(4(x)))), sig: {x' -> 3(4(x))}, l': 5(5(x')), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R6 unifies with R8 at p: [1,1,1,1], l: 2(5(5(3(4(x))))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R6 unifies with R9 at p: [1,1,1,1], l: 2(5(5(3(4(x))))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R6 unifies with R10 at p: [1,1,1,1], l: 2(5(5(3(4(x))))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R6 unifies with R11 at p: [1,1,1,1], l: 2(5(5(3(4(x))))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R6 unifies with R12 at p: [1,1,1,1], l: 2(5(5(3(4(x))))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 4(5(4(3(1(4(0(2(4(4(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R7 unifies with R6 at p: [], l: 2(5(5(x))), lp: 2(5(5(x))), sig: {x -> 3(4(x'))}, l': 2(5(5(3(4(x'))))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 4(5(4(3(1(4(0(2(4(4(x'))))))))))) (R7 unifies with R15 at p: [1], l: 2(5(5(x))), lp: 5(5(x)), sig: {x -> 2(4(5(0(x'))))}, l': 5(5(2(4(5(0(x')))))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R7 unifies with R16 at p: [1], l: 2(5(5(x))), lp: 5(5(x)), sig: {x -> 2(x')}, l': 5(5(2(x'))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R7 unifies with R17 at p: [1], l: 2(5(5(x))), lp: 5(5(x)), sig: {x -> 5(1(4(x')))}, l': 5(5(5(1(4(x'))))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R7 unifies with R18 at p: [1], l: 2(5(5(x))), lp: 5(5(x)), sig: {x -> 5(x')}, l': 5(5(5(x'))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R7 unifies with R19 at p: [1], l: 2(5(5(x))), lp: 5(5(x)), sig: {x -> 3(x')}, l': 5(5(3(x'))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R7 unifies with R20 at p: [1], l: 2(5(5(x))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R7 unifies with R21 at p: [1], l: 2(5(5(x))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R7 unifies with R13 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R7 unifies with R14 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R7 unifies with R15 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R7 unifies with R16 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R7 unifies with R17 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R7 unifies with R18 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R7 unifies with R19 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R7 unifies with R20 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R7 unifies with R21 at p: [1,1], l: 2(5(5(x))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 4(2(5(4(4(0(0(1(1(2(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R8 unifies with R20 at p: [1,1], l: 4(1(5(5(0(4(x)))))), lp: 5(5(0(4(x)))), sig: {x' -> 0(4(x))}, l': 5(5(x')), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R8 unifies with R21 at p: [1,1], l: 4(1(5(5(0(4(x)))))), lp: 5(5(0(4(x)))), sig: {x' -> 0(4(x))}, l': 5(5(x')), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R8 unifies with R3 at p: [1,1,1,1], l: 4(1(5(5(0(4(x)))))), lp: 0(4(x)), sig: {x -> 4(5(5(5(x'))))}, l': 0(4(4(5(5(5(x')))))), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 0(4(4(4(3(3(4(1(3(1(x'))))))))))) (R8 unifies with R8 at p: [1,1,1,1,1], l: 4(1(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R8 unifies with R9 at p: [1,1,1,1,1], l: 4(1(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R8 unifies with R10 at p: [1,1,1,1,1], l: 4(1(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R8 unifies with R11 at p: [1,1,1,1,1], l: 4(1(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R8 unifies with R12 at p: [1,1,1,1,1], l: 4(1(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 1(0(3(0(4(2(4(4(3(4(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R9 unifies with R7 at p: [1], l: 4(2(5(5(1(5(x)))))), lp: 2(5(5(1(5(x))))), sig: {x' -> 1(5(x))}, l': 2(5(5(x'))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 4(2(5(4(4(0(0(1(1(2(x'))))))))))) (R9 unifies with R20 at p: [1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(5(1(5(x)))), sig: {x' -> 1(5(x))}, l': 5(5(x')), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R9 unifies with R21 at p: [1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(5(1(5(x)))), sig: {x' -> 1(5(x))}, l': 5(5(x')), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R9 unifies with R13 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R9 unifies with R14 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R9 unifies with R15 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R9 unifies with R16 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R9 unifies with R17 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R9 unifies with R18 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R9 unifies with R19 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R9 unifies with R20 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R9 unifies with R21 at p: [1,1,1,1,1], l: 4(2(5(5(1(5(x)))))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 2(3(4(2(1(1(3(4(2(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R10 unifies with R11 at p: [1], l: 4(4(5(2(4(2(2(x))))))), lp: 4(5(2(4(2(2(x)))))), sig: {x' -> 2(2(x))}, l': 4(5(2(4(x')))), r: 4(0(5(5(4(5(1(2(2(1(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R10 unifies with R13 at p: [1,1], l: 4(4(5(2(4(2(2(x))))))), lp: 5(2(4(2(2(x))))), sig: {x' -> 2(2(x))}, l': 5(2(4(x'))), r: 4(0(5(5(4(5(1(2(2(1(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R10 unifies with R5 at p: [1,1,1,1,1,1], l: 4(4(5(2(4(2(2(x))))))), lp: 2(x), sig: {x -> 5(0(4(x')))}, l': 2(5(0(4(x')))), r: 4(0(5(5(4(5(1(2(2(1(x)))))))))), r': 4(4(3(2(4(4(5(1(0(0(x'))))))))))) (R10 unifies with R6 at p: [1,1,1,1,1,1], l: 4(4(5(2(4(2(2(x))))))), lp: 2(x), sig: {x -> 5(5(3(4(x'))))}, l': 2(5(5(3(4(x'))))), r: 4(0(5(5(4(5(1(2(2(1(x)))))))))), r': 4(5(4(3(1(4(0(2(4(4(x'))))))))))) (R10 unifies with R7 at p: [1,1,1,1,1,1], l: 4(4(5(2(4(2(2(x))))))), lp: 2(x), sig: {x -> 5(5(x'))}, l': 2(5(5(x'))), r: 4(0(5(5(4(5(1(2(2(1(x)))))))))), r': 4(2(5(4(4(0(0(1(1(2(x'))))))))))) (R11 unifies with R13 at p: [1], l: 4(5(2(4(x)))), lp: 5(2(4(x))), sig: {x -> x'}, l': 5(2(4(x'))), r: 4(1(5(5(2(0(3(1(3(3(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R11 unifies with R8 at p: [1,1,1], l: 4(5(2(4(x)))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 4(1(5(5(2(0(3(1(3(3(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R11 unifies with R9 at p: [1,1,1], l: 4(5(2(4(x)))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 4(1(5(5(2(0(3(1(3(3(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R11 unifies with R10 at p: [1,1,1], l: 4(5(2(4(x)))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 4(1(5(5(2(0(3(1(3(3(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R11 unifies with R11 at p: [1,1,1], l: 4(5(2(4(x)))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 4(1(5(5(2(0(3(1(3(3(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R11 unifies with R12 at p: [1,1,1], l: 4(5(2(4(x)))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 4(1(5(5(2(0(3(1(3(3(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R12 unifies with R17 at p: [1], l: 4(5(5(5(x)))), lp: 5(5(5(x))), sig: {x -> 1(4(x'))}, l': 5(5(5(1(4(x'))))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R12 unifies with R18 at p: [1], l: 4(5(5(5(x)))), lp: 5(5(5(x))), sig: {x -> x'}, l': 5(5(5(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R12 unifies with R20 at p: [1], l: 4(5(5(5(x)))), lp: 5(5(5(x))), sig: {x' -> 5(x)}, l': 5(5(x')), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R12 unifies with R21 at p: [1], l: 4(5(5(5(x)))), lp: 5(5(5(x))), sig: {x' -> 5(x)}, l': 5(5(x')), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R12 unifies with R15 at p: [1,1], l: 4(5(5(5(x)))), lp: 5(5(x)), sig: {x -> 2(4(5(0(x'))))}, l': 5(5(2(4(5(0(x')))))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R12 unifies with R16 at p: [1,1], l: 4(5(5(5(x)))), lp: 5(5(x)), sig: {x -> 2(x')}, l': 5(5(2(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R12 unifies with R17 at p: [1,1], l: 4(5(5(5(x)))), lp: 5(5(x)), sig: {x -> 5(1(4(x')))}, l': 5(5(5(1(4(x'))))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R12 unifies with R18 at p: [1,1], l: 4(5(5(5(x)))), lp: 5(5(x)), sig: {x -> 5(x')}, l': 5(5(5(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R12 unifies with R19 at p: [1,1], l: 4(5(5(5(x)))), lp: 5(5(x)), sig: {x -> 3(x')}, l': 5(5(3(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R12 unifies with R20 at p: [1,1], l: 4(5(5(5(x)))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R12 unifies with R21 at p: [1,1], l: 4(5(5(5(x)))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R12 unifies with R13 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R12 unifies with R14 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R12 unifies with R15 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R12 unifies with R16 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R12 unifies with R17 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R12 unifies with R18 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R12 unifies with R19 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R12 unifies with R20 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R12 unifies with R21 at p: [1,1,1], l: 4(5(5(5(x)))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 1(5(1(2(0(3(2(1(0(5(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R13 unifies with R8 at p: [1,1], l: 5(2(4(x))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 0(5(0(2(3(3(4(2(4(2(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R13 unifies with R9 at p: [1,1], l: 5(2(4(x))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 0(5(0(2(3(3(4(2(4(2(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R13 unifies with R10 at p: [1,1], l: 5(2(4(x))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 0(5(0(2(3(3(4(2(4(2(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R13 unifies with R11 at p: [1,1], l: 5(2(4(x))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 0(5(0(2(3(3(4(2(4(2(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R13 unifies with R12 at p: [1,1], l: 5(2(4(x))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 0(5(0(2(3(3(4(2(4(2(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R14 unifies with R7 at p: [1], l: 5(2(5(5(0(4(x)))))), lp: 2(5(5(0(4(x))))), sig: {x' -> 0(4(x))}, l': 2(5(5(x'))), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 4(2(5(4(4(0(0(1(1(2(x'))))))))))) (R14 unifies with R20 at p: [1,1], l: 5(2(5(5(0(4(x)))))), lp: 5(5(0(4(x)))), sig: {x' -> 0(4(x))}, l': 5(5(x')), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R14 unifies with R21 at p: [1,1], l: 5(2(5(5(0(4(x)))))), lp: 5(5(0(4(x)))), sig: {x' -> 0(4(x))}, l': 5(5(x')), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R14 unifies with R3 at p: [1,1,1,1], l: 5(2(5(5(0(4(x)))))), lp: 0(4(x)), sig: {x -> 4(5(5(5(x'))))}, l': 0(4(4(5(5(5(x')))))), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 0(4(4(4(3(3(4(1(3(1(x'))))))))))) (R14 unifies with R8 at p: [1,1,1,1,1], l: 5(2(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R14 unifies with R9 at p: [1,1,1,1,1], l: 5(2(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R14 unifies with R10 at p: [1,1,1,1,1], l: 5(2(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R14 unifies with R11 at p: [1,1,1,1,1], l: 5(2(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R14 unifies with R12 at p: [1,1,1,1,1], l: 5(2(5(5(0(4(x)))))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 0(4(2(3(3(5(2(1(4(4(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R15 unifies with R13 at p: [1], l: 5(5(2(4(5(0(x)))))), lp: 5(2(4(5(0(x))))), sig: {x' -> 5(0(x))}, l': 5(2(4(x'))), r: 2(1(1(4(2(4(0(4(2(0(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R15 unifies with R1 at p: [1,1,1,1,1], l: 5(5(2(4(5(0(x)))))), lp: 0(x), sig: {x -> 1(5(5(5(3(5(x'))))))}, l': 0(1(5(5(5(3(5(x'))))))), r: 2(1(1(4(2(4(0(4(2(0(x)))))))))), r': 5(3(2(5(1(0(1(2(0(5(x'))))))))))) (R15 unifies with R2 at p: [1,1,1,1,1], l: 5(5(2(4(5(0(x)))))), lp: 0(x), sig: {x -> 2(5(3(4(x'))))}, l': 0(2(5(3(4(x'))))), r: 2(1(1(4(2(4(0(4(2(0(x)))))))))), r': 3(2(4(3(1(5(1(1(3(4(x'))))))))))) (R15 unifies with R3 at p: [1,1,1,1,1], l: 5(5(2(4(5(0(x)))))), lp: 0(x), sig: {x -> 4(4(5(5(5(x')))))}, l': 0(4(4(5(5(5(x')))))), r: 2(1(1(4(2(4(0(4(2(0(x)))))))))), r': 0(4(4(4(3(3(4(1(3(1(x'))))))))))) (R16 unifies with R15 at p: [], l: 5(5(2(x))), lp: 5(5(2(x))), sig: {x -> 4(5(0(x')))}, l': 5(5(2(4(5(0(x')))))), r: 0(1(3(2(3(0(3(2(5(3(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R16 unifies with R13 at p: [1], l: 5(5(2(x))), lp: 5(2(x)), sig: {x -> 4(x')}, l': 5(2(4(x'))), r: 0(1(3(2(3(0(3(2(5(3(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R16 unifies with R14 at p: [1], l: 5(5(2(x))), lp: 5(2(x)), sig: {x -> 5(5(0(4(x'))))}, l': 5(2(5(5(0(4(x')))))), r: 0(1(3(2(3(0(3(2(5(3(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R16 unifies with R5 at p: [1,1], l: 5(5(2(x))), lp: 2(x), sig: {x -> 5(0(4(x')))}, l': 2(5(0(4(x')))), r: 0(1(3(2(3(0(3(2(5(3(x)))))))))), r': 4(4(3(2(4(4(5(1(0(0(x'))))))))))) (R16 unifies with R6 at p: [1,1], l: 5(5(2(x))), lp: 2(x), sig: {x -> 5(5(3(4(x'))))}, l': 2(5(5(3(4(x'))))), r: 0(1(3(2(3(0(3(2(5(3(x)))))))))), r': 4(5(4(3(1(4(0(2(4(4(x'))))))))))) (R16 unifies with R7 at p: [1,1], l: 5(5(2(x))), lp: 2(x), sig: {x -> 5(5(x'))}, l': 2(5(5(x'))), r: 0(1(3(2(3(0(3(2(5(3(x)))))))))), r': 4(2(5(4(4(0(0(1(1(2(x'))))))))))) (R17 unifies with R20 at p: [1], l: 5(5(5(1(4(x))))), lp: 5(5(1(4(x)))), sig: {x' -> 1(4(x))}, l': 5(5(x')), r: 3(3(0(5(0(4(3(4(4(0(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R17 unifies with R21 at p: [1], l: 5(5(5(1(4(x))))), lp: 5(5(1(4(x)))), sig: {x' -> 1(4(x))}, l': 5(5(x')), r: 3(3(0(5(0(4(3(4(4(0(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R17 unifies with R8 at p: [1,1,1,1], l: 5(5(5(1(4(x))))), lp: 4(x), sig: {x -> 1(5(5(0(4(x')))))}, l': 4(1(5(5(0(4(x')))))), r: 3(3(0(5(0(4(3(4(4(0(x)))))))))), r': 1(0(3(0(4(2(4(4(3(4(x'))))))))))) (R17 unifies with R9 at p: [1,1,1,1], l: 5(5(5(1(4(x))))), lp: 4(x), sig: {x -> 2(5(5(1(5(x')))))}, l': 4(2(5(5(1(5(x')))))), r: 3(3(0(5(0(4(3(4(4(0(x)))))))))), r': 2(3(4(2(1(1(3(4(2(5(x'))))))))))) (R17 unifies with R10 at p: [1,1,1,1], l: 5(5(5(1(4(x))))), lp: 4(x), sig: {x -> 4(5(2(4(2(2(x'))))))}, l': 4(4(5(2(4(2(2(x'))))))), r: 3(3(0(5(0(4(3(4(4(0(x)))))))))), r': 4(0(5(5(4(5(1(2(2(1(x'))))))))))) (R17 unifies with R11 at p: [1,1,1,1], l: 5(5(5(1(4(x))))), lp: 4(x), sig: {x -> 5(2(4(x')))}, l': 4(5(2(4(x')))), r: 3(3(0(5(0(4(3(4(4(0(x)))))))))), r': 4(1(5(5(2(0(3(1(3(3(x'))))))))))) (R17 unifies with R12 at p: [1,1,1,1], l: 5(5(5(1(4(x))))), lp: 4(x), sig: {x -> 5(5(5(x')))}, l': 4(5(5(5(x')))), r: 3(3(0(5(0(4(3(4(4(0(x)))))))))), r': 1(5(1(2(0(3(2(1(0(5(x'))))))))))) (R18 unifies with R17 at p: [], l: 5(5(5(x))), lp: 5(5(5(x))), sig: {x -> 1(4(x'))}, l': 5(5(5(1(4(x'))))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R18 unifies with R15 at p: [1], l: 5(5(5(x))), lp: 5(5(x)), sig: {x -> 2(4(5(0(x'))))}, l': 5(5(2(4(5(0(x')))))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R18 unifies with R16 at p: [1], l: 5(5(5(x))), lp: 5(5(x)), sig: {x -> 2(x')}, l': 5(5(2(x'))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R18 unifies with R17 at p: [1], l: 5(5(5(x))), lp: 5(5(x)), sig: {x -> 5(1(4(x')))}, l': 5(5(5(1(4(x'))))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R18 unifies with R18 at p: [1], l: 5(5(5(x))), lp: 5(5(x)), sig: {x -> 5(x')}, l': 5(5(5(x'))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R18 unifies with R19 at p: [1], l: 5(5(5(x))), lp: 5(5(x)), sig: {x -> 3(x')}, l': 5(5(3(x'))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R18 unifies with R20 at p: [1], l: 5(5(5(x))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R18 unifies with R21 at p: [1], l: 5(5(5(x))), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R18 unifies with R13 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R18 unifies with R14 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R18 unifies with R15 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R18 unifies with R16 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R18 unifies with R17 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R18 unifies with R18 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R18 unifies with R19 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R18 unifies with R20 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R18 unifies with R21 at p: [1,1], l: 5(5(5(x))), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 5(3(4(1(0(1(4(5(0(0(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R20 unifies with R15 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 2(4(5(0(x'))))}, l': 5(5(2(4(5(0(x')))))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R20 unifies with R16 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 2(x')}, l': 5(5(2(x'))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R20 unifies with R17 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 5(1(4(x')))}, l': 5(5(5(1(4(x'))))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R20 unifies with R18 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 5(x')}, l': 5(5(5(x'))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R20 unifies with R19 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 3(x')}, l': 5(5(3(x'))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R20 unifies with R13 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R20 unifies with R14 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R20 unifies with R15 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R20 unifies with R16 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R20 unifies with R17 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R20 unifies with R18 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R20 unifies with R19 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R20 unifies with R20 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R20 unifies with R21 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 0(5(4(0(2(5(4(5(2(1(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) (R21 unifies with R15 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 2(4(5(0(x'))))}, l': 5(5(2(4(5(0(x')))))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R21 unifies with R16 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 2(x')}, l': 5(5(2(x'))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R21 unifies with R17 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 5(1(4(x')))}, l': 5(5(5(1(4(x'))))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R21 unifies with R18 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 5(x')}, l': 5(5(5(x'))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R21 unifies with R19 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> 3(x')}, l': 5(5(3(x'))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R21 unifies with R20 at p: [], l: 5(5(x)), lp: 5(5(x)), sig: {x -> x'}, l': 5(5(x')), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R21 unifies with R13 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 2(4(x'))}, l': 5(2(4(x'))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(5(0(2(3(3(4(2(4(2(x'))))))))))) (R21 unifies with R14 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 2(5(5(0(4(x')))))}, l': 5(2(5(5(0(4(x')))))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(4(2(3(3(5(2(1(4(4(x'))))))))))) (R21 unifies with R15 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(2(4(5(0(x')))))}, l': 5(5(2(4(5(0(x')))))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 2(1(1(4(2(4(0(4(2(0(x'))))))))))) (R21 unifies with R16 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(2(x'))}, l': 5(5(2(x'))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(1(3(2(3(0(3(2(5(3(x'))))))))))) (R21 unifies with R17 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(5(1(4(x'))))}, l': 5(5(5(1(4(x'))))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 3(3(0(5(0(4(3(4(4(0(x'))))))))))) (R21 unifies with R18 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(5(x'))}, l': 5(5(5(x'))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 5(3(4(1(0(1(4(5(0(0(x'))))))))))) (R21 unifies with R19 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(3(x'))}, l': 5(5(3(x'))), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(3(5(4(4(1(0(1(5(0(x'))))))))))) (R21 unifies with R20 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 0(5(4(0(2(5(4(5(2(1(x'))))))))))) (R21 unifies with R21 at p: [1], l: 5(5(x)), lp: 5(x), sig: {x -> 5(x')}, l': 5(5(x')), r: 3(4(1(1(1(1(4(4(0(4(x)))))))))), r': 3(4(1(1(1(1(4(4(0(4(x'))))))))))) -> Critical pairs info: <5(5(2(4(5(3(2(4(3(1(5(1(1(3(4(x'))))))))))))))),2(1(1(4(2(4(0(4(2(0(2(5(3(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N1 <0(3(5(4(4(1(0(1(5(0(x')))))))))),0(5(4(0(2(5(4(5(2(1(3(x')))))))))))> => Not trivial, Overlay, Proper, NW0, N2 <5(5(5(1(1(0(3(0(4(2(4(4(3(4(x')))))))))))))),3(3(0(5(0(4(3(4(4(0(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N3 <4(5(5(3(3(0(5(0(4(3(4(4(0(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N4 <0(1(3(4(1(1(1(1(4(4(0(4(5(3(5(x))))))))))))))),5(3(2(5(1(0(1(2(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N5 <4(1(0(5(4(0(2(5(4(5(2(1(0(4(x)))))))))))))),1(0(3(0(4(2(4(4(3(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N6 <5(0(3(5(4(4(1(0(1(5(0(x'))))))))))),5(3(4(1(0(1(4(5(0(0(3(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N7 <5(3(4(1(1(1(1(4(4(0(4(x'))))))))))),5(3(4(1(0(1(4(5(0(0(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N8 <0(2(5(3(4(1(5(5(2(0(3(1(3(3(x')))))))))))))),3(2(4(3(1(5(1(1(3(4(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N9 <0(1(3(2(3(0(3(2(5(3(x')))))))))),0(5(4(0(2(5(4(5(2(1(2(x')))))))))))> => Not trivial, Overlay, Proper, NW0, N10 <2(5(3(4(1(1(1(1(4(4(0(4(x')))))))))))),4(2(5(4(4(0(0(1(1(2(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N11 <0(5(4(0(2(5(4(5(2(1(x')))))))))),3(4(1(1(1(1(4(4(0(4(x'))))))))))> => Not trivial, Overlay, Proper, NW0, N12 <0(4(4(3(4(1(1(1(1(4(4(0(4(5(x)))))))))))))),0(4(4(4(3(3(4(1(3(1(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N13 <0(4(4(5(5(0(5(4(0(2(5(4(5(2(1(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N14 <4(5(5(2(1(1(4(2(4(0(4(2(0(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N15 <0(3(5(4(4(1(0(1(5(0(x')))))))))),3(4(1(1(1(1(4(4(0(4(3(x')))))))))))> => Not trivial, Overlay, Proper, NW0, N16 <5(3(4(1(0(1(4(5(0(0(x')))))))))),0(5(4(0(2(5(4(5(2(1(5(x')))))))))))> => Not trivial, Overlay, Proper, NW0, N17 <2(5(0(1(5(1(2(0(3(2(1(0(5(x'))))))))))))),4(4(3(2(4(4(5(1(0(0(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N18 <4(1(5(5(0(4(1(5(5(2(0(3(1(3(3(x'))))))))))))))),1(0(3(0(4(2(4(4(3(4(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N19 <2(5(0(4(1(5(5(2(0(3(1(3(3(x'))))))))))))),4(4(3(2(4(4(5(1(0(0(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N20 <4(2(3(4(1(1(1(1(4(4(0(4(1(5(x)))))))))))))),2(3(4(2(1(1(3(4(2(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N21 <4(1(5(5(0(4(4(4(3(3(4(1(3(1(x')))))))))))))),1(0(3(0(4(2(4(4(3(4(4(5(5(5(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N22 <0(4(4(5(5(3(4(1(0(1(4(5(0(0(x')))))))))))))),0(4(4(4(3(3(4(1(3(1(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N23 <5(3(3(0(5(0(4(3(4(4(0(x'))))))))))),3(4(1(1(1(1(4(4(0(4(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N24 <0(4(4(5(3(4(1(0(1(4(5(0(0(x'))))))))))))),0(4(4(4(3(3(4(1(3(1(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N25 <5(0(3(5(4(4(1(0(1(5(0(x'))))))))))),3(4(1(1(1(1(4(4(0(4(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N26 <4(5(3(4(1(1(1(1(4(4(0(4(x')))))))))))),1(5(1(2(0(3(2(1(0(5(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N27 <4(2(5(5(1(0(5(0(2(3(3(4(2(4(2(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N28 <2(5(0(1(0(3(0(4(2(4(4(3(4(x'))))))))))))),4(4(3(2(4(4(5(1(0(0(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N29 <2(5(5(3(4(1(5(5(2(0(3(1(3(3(x')))))))))))))),4(5(4(3(1(4(0(2(4(4(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N30 <0(4(4(5(5(3(3(0(5(0(4(3(4(4(0(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N31 <1(2(4(5(2(1(5(1(2(0(3(2(1(0(5(x'))))))))))))))),3(3(5(3(0(4(0(3(1(3(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N32 <0(1(5(3(4(1(0(1(4(5(0(0(3(5(x)))))))))))))),5(3(2(5(1(0(1(2(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N33 <0(4(4(5(0(3(5(4(4(1(0(1(5(0(x')))))))))))))),0(4(4(4(3(3(4(1(3(1(3(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N34 <2(5(3(3(0(5(0(4(3(4(4(0(x')))))))))))),4(2(5(4(4(0(0(1(1(2(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N35 <5(0(4(2(3(3(5(2(1(4(4(x'))))))))))),0(1(3(2(3(0(3(2(5(3(5(5(0(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N36 <5(0(4(2(3(3(5(2(1(4(4(x'))))))))))),0(5(4(0(2(5(4(5(2(1(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N37 <2(3(4(1(1(1(1(4(4(0(4(x'))))))))))),4(2(5(4(4(0(0(1(1(2(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N38 <4(3(4(1(1(1(1(4(4(0(4(5(x)))))))))))),1(5(1(2(0(3(2(1(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N39 <2(5(5(3(4(0(5(5(4(5(1(2(2(1(x')))))))))))))),4(5(4(3(1(4(0(2(4(4(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N40 <5(2(1(1(4(2(4(0(4(2(0(x'))))))))))),3(4(1(1(1(1(4(4(0(4(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N41 <4(5(2(4(1(5(5(2(0(3(1(3(3(x'))))))))))))),4(1(5(5(2(0(3(1(3(3(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N42 <5(2(5(5(0(4(0(5(5(4(5(1(2(2(1(x'))))))))))))))),0(4(2(3(3(5(2(1(4(4(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N43 <5(5(5(1(2(3(4(2(1(1(3(4(2(5(x')))))))))))))),3(3(0(5(0(4(3(4(4(0(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N44 <4(0(5(0(2(3(3(4(2(4(2(x'))))))))))),4(1(5(5(2(0(3(1(3(3(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N45 <0(1(5(5(5(3(0(5(0(2(3(3(4(2(4(2(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N46 <5(3(3(0(5(0(4(3(4(4(0(x'))))))))))),0(5(4(0(2(5(4(5(2(1(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N47 <4(4(0(5(0(2(3(3(4(2(4(2(2(2(x)))))))))))))),4(0(5(5(4(5(1(2(2(1(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N48 <4(5(5(0(1(3(2(3(0(3(2(5(3(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N49 <2(5(5(3(1(0(3(0(4(2(4(4(3(4(x')))))))))))))),4(5(4(3(1(4(0(2(4(4(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N50 <2(5(3(4(1(0(1(4(5(0(0(x'))))))))))),4(2(5(4(4(0(0(1(1(2(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N51 <0(1(5(0(5(4(0(2(5(4(5(2(1(3(5(x))))))))))))))),5(3(2(5(1(0(1(2(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N52 <4(2(5(5(1(0(3(5(4(4(1(0(1(5(0(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N53 <4(1(3(4(1(1(1(1(4(4(0(4(0(4(x)))))))))))))),1(0(3(0(4(2(4(4(3(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N54 <4(5(3(3(0(5(0(4(3(4(4(0(x')))))))))))),1(5(1(2(0(3(2(1(0(5(5(1(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N55 <0(4(4(5(3(3(0(5(0(4(3(4(4(0(x')))))))))))))),0(4(4(4(3(3(4(1(3(1(5(1(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N56 <5(5(3(3(0(5(0(4(3(4(4(0(x')))))))))))),5(3(4(1(0(1(4(5(0(0(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N57 <5(0(5(0(2(3(3(4(2(4(2(x'))))))))))),0(5(4(0(2(5(4(5(2(1(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N58 <4(1(5(5(0(1(0(3(0(4(2(4(4(3(4(x'))))))))))))))),1(0(3(0(4(2(4(4(3(4(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N59 <5(0(5(0(2(3(3(4(2(4(2(x'))))))))))),3(4(1(1(1(1(4(4(0(4(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N60 <5(5(2(4(5(5(3(2(5(1(0(1(2(0(5(x'))))))))))))))),2(1(1(4(2(4(0(4(2(0(1(5(5(5(3(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N61 <5(5(0(3(5(4(4(1(0(1(5(0(x')))))))))))),5(3(4(1(0(1(4(5(0(0(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N62 <2(0(1(3(2(3(0(3(2(5(3(x'))))))))))),4(2(5(4(4(0(0(1(1(2(2(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N63 <2(1(1(4(2(4(0(4(2(0(x')))))))))),0(5(4(0(2(5(4(5(2(1(2(4(5(0(x'))))))))))))))> => Not trivial, Overlay, Proper, NW0, N64 <2(5(0(4(0(5(5(4(5(1(2(2(1(x'))))))))))))),4(4(3(2(4(4(5(1(0(0(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N65 <0(4(4(5(5(2(1(1(4(2(4(0(4(2(0(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N66 <1(2(4(1(5(5(2(0(3(1(3(3(x')))))))))))),3(3(5(3(0(4(0(3(1(3(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N67 <5(5(2(1(1(4(2(4(0(4(2(0(x')))))))))))),5(3(4(1(0(1(4(5(0(0(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N68 <0(1(5(3(4(1(1(1(1(4(4(0(4(3(5(x))))))))))))))),5(3(2(5(1(0(1(2(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N69 <0(4(4(5(0(5(4(0(2(5(4(5(2(1(x')))))))))))))),0(4(4(4(3(3(4(1(3(1(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N70 <3(3(0(5(0(4(3(4(4(0(x')))))))))),3(4(1(1(1(1(4(4(0(4(5(1(4(x')))))))))))))> => Not trivial, Overlay, Proper, NW0, N71 <5(5(5(3(4(1(0(1(4(5(0(0(x')))))))))))),5(3(4(1(0(1(4(5(0(0(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N72 <5(5(4(5(4(3(1(4(0(2(4(4(x')))))))))))),0(1(3(2(3(0(3(2(5(3(5(5(3(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N73 <4(2(5(5(1(3(4(1(1(1(1(4(4(0(4(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N74 <3(3(0(5(0(4(3(4(4(0(x')))))))))),0(5(4(0(2(5(4(5(2(1(5(1(4(x')))))))))))))> => Not trivial, Overlay, Proper, NW0, N75 <0(4(4(5(5(0(5(0(2(3(3(4(2(4(2(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N76 <4(1(5(5(0(2(3(4(2(1(1(3(4(2(5(x'))))))))))))))),1(0(3(0(4(2(4(4(3(4(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N77 <5(2(4(1(5(5(2(0(3(1(3(3(x')))))))))))),0(5(0(2(3(3(4(2(4(2(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N78 <5(2(5(5(0(2(3(4(2(1(1(3(4(2(5(x'))))))))))))))),0(4(2(3(3(5(2(1(4(4(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N79 <5(4(2(5(4(4(0(0(1(1(2(0(4(x))))))))))))),0(4(2(3(3(5(2(1(4(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N80 <5(0(3(5(4(4(1(0(1(5(0(x'))))))))))),0(5(4(0(2(5(4(5(2(1(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N81 <5(5(3(4(1(1(1(1(4(4(0(4(x')))))))))))),5(3(4(1(0(1(4(5(0(0(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N82 <0(1(5(5(5(3(0(5(4(0(2(5(4(5(2(1(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N83 <0(2(5(3(1(0(3(0(4(2(4(4(3(4(x')))))))))))))),3(2(4(3(1(5(1(1(3(4(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N84 <2(0(5(4(0(2(5(4(5(2(1(3(4(x))))))))))))),4(5(4(3(1(4(0(2(4(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N85 <4(1(5(5(0(4(0(5(5(4(5(1(2(2(1(x'))))))))))))))),1(0(3(0(4(2(4(4(3(4(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N86 <2(5(5(3(4(1(0(1(4(5(0(0(x')))))))))))),4(2(5(4(4(0(0(1(1(2(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N87 <5(0(5(4(0(2(5(4(5(2(1(x'))))))))))),5(3(4(1(0(1(4(5(0(0(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N88 <5(5(4(2(5(4(4(0(0(1(1(2(x')))))))))))),0(1(3(2(3(0(3(2(5(3(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N89 <0(1(5(5(5(3(3(3(0(5(0(4(3(4(4(0(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N90 <4(2(5(5(1(0(1(3(2(3(0(3(2(5(3(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N91 <5(2(0(5(4(0(2(5(4(5(2(1(0(4(x)))))))))))))),0(4(2(3(3(5(2(1(4(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N92 <1(2(4(5(2(1(0(3(0(4(2(4(4(3(4(x'))))))))))))))),3(3(5(3(0(4(0(3(1(3(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N93 <0(2(5(3(2(3(4(2(1(1(3(4(2(5(x')))))))))))))),3(2(4(3(1(5(1(1(3(4(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N94 <5(5(2(4(5(0(4(4(4(3(3(4(1(3(1(x'))))))))))))))),2(1(1(4(2(4(0(4(2(0(4(4(5(5(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N95 <0(4(4(3(3(0(5(0(4(3(4(4(0(x'))))))))))))),0(4(4(4(3(3(4(1(3(1(1(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N96 <4(4(5(2(4(2(4(2(5(4(4(0(0(1(1(2(x')))))))))))))))),4(0(5(5(4(5(1(2(2(1(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N97 <2(0(3(5(4(4(1(0(1(5(0(x'))))))))))),4(2(5(4(4(0(0(1(1(2(3(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N98 <4(5(2(2(3(4(2(1(1(3(4(2(5(x'))))))))))))),4(1(5(5(2(0(3(1(3(3(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N99 <2(5(0(4(4(4(3(3(4(1(3(1(x')))))))))))),4(4(3(2(4(4(5(1(0(0(4(5(5(5(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N100 <2(1(1(4(2(4(0(4(2(0(x')))))))))),0(1(3(2(3(0(3(2(5(3(4(5(0(x')))))))))))))> => Not trivial, Overlay, Proper, NW0, N101 <5(5(0(4(2(3(3(5(2(1(4(4(x')))))))))))),5(3(4(1(0(1(4(5(0(0(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N102 <5(0(5(4(0(2(5(4(5(2(1(1(4(x))))))))))))),3(3(0(5(0(4(3(4(4(0(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N103 <2(5(0(5(4(0(2(5(4(5(2(1(x')))))))))))),4(2(5(4(4(0(0(1(1(2(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N104 <5(5(4(4(3(2(4(4(5(1(0(0(x')))))))))))),0(1(3(2(3(0(3(2(5(3(5(0(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N105 <4(4(2(5(4(4(0(0(1(1(2(1(5(x))))))))))))),2(3(4(2(1(1(3(4(2(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N106 <0(1(3(2(3(0(3(2(5(3(x')))))))))),3(4(1(1(1(1(4(4(0(4(2(x')))))))))))> => Not trivial, Overlay, Proper, NW0, N107 <5(0(4(2(3(3(5(2(1(4(4(x'))))))))))),3(4(1(1(1(1(4(4(0(4(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N108 <4(2(5(5(1(3(3(0(5(0(4(3(4(4(0(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(5(5(1(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N109 <5(2(5(5(0(4(4(4(3(3(4(1(3(1(x')))))))))))))),0(4(2(3(3(5(2(1(4(4(4(5(5(5(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N110 <0(4(4(5(5(5(3(4(1(0(1(4(5(0(0(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N111 <4(5(0(5(4(0(2(5(4(5(2(1(x')))))))))))),1(5(1(2(0(3(2(1(0(5(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N112 <0(1(5(5(5(3(2(1(1(4(2(4(0(4(2(0(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N113 <5(5(3(4(1(0(1(4(5(0(0(x'))))))))))),3(4(1(1(1(1(4(4(0(4(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N114 <2(5(0(1(3(2(3(0(3(2(5(3(x')))))))))))),4(2(5(4(4(0(0(1(1(2(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N115 <5(2(1(0(3(0(4(2(4(4(3(4(x')))))))))))),0(5(0(2(3(3(4(2(4(2(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N116 <5(2(5(5(0(1(5(1(2(0(3(2(1(0(5(x'))))))))))))))),0(4(2(3(3(5(2(1(4(4(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N117 <4(5(0(3(5(4(4(1(0(1(5(0(x')))))))))))),1(5(1(2(0(3(2(1(0(5(3(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N118 <4(5(3(4(1(0(1(4(5(0(0(x'))))))))))),1(5(1(2(0(3(2(1(0(5(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N119 <0(4(4(5(3(4(1(1(1(1(4(4(0(4(x')))))))))))))),0(4(4(4(3(3(4(1(3(1(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N120 <5(2(2(3(4(2(1(1(3(4(2(5(x')))))))))))),0(5(0(2(3(3(4(2(4(2(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N121 <0(4(4(5(5(0(4(2(3(3(5(2(1(4(4(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N122 <0(4(4(5(0(1(3(2(3(0(3(2(5(3(x')))))))))))))),0(4(4(4(3(3(4(1(3(1(2(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N123 <5(3(4(1(1(1(1(4(4(0(4(x'))))))))))),0(5(4(0(2(5(4(5(2(1(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N124 <4(2(0(5(4(0(2(5(4(5(2(1(1(5(x)))))))))))))),2(3(4(2(1(1(3(4(2(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N125 <4(5(5(0(4(2(3(3(5(2(1(4(4(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N126 <5(5(0(1(3(2(3(0(3(2(5(3(x')))))))))))),5(3(4(1(0(1(4(5(0(0(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N127 <2(0(5(4(0(2(5(4(5(2(1(x'))))))))))),4(2(5(4(4(0(0(1(1(2(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N128 <5(0(1(3(2(3(0(3(2(5(3(x'))))))))))),3(4(1(1(1(1(4(4(0(4(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N129 <5(0(5(0(2(3(3(4(2(4(2(x'))))))))))),0(1(3(2(3(0(3(2(5(3(4(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N130 <4(2(5(5(1(2(1(1(4(2(4(0(4(2(0(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N131 <5(3(4(1(0(1(4(5(0(0(x')))))))))),3(4(1(1(1(1(4(4(0(4(5(x')))))))))))> => Not trivial, Overlay, Proper, NW0, N132 <0(4(4(0(5(4(0(2(5(4(5(2(1(5(x)))))))))))))),0(4(4(4(3(3(4(1(3(1(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N133 <4(5(4(3(1(4(0(2(4(4(x')))))))))),4(2(5(4(4(0(0(1(1(2(3(4(x'))))))))))))> => Not trivial, Overlay, Proper, NW0, N134 <5(2(3(4(1(1(1(1(4(4(0(4(0(4(x)))))))))))))),0(4(2(3(3(5(2(1(4(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N135 <5(3(4(1(1(1(1(4(4(0(4(x'))))))))))),3(4(1(1(1(1(4(4(0(4(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N136 <2(3(4(1(1(1(1(4(4(0(4(3(4(x))))))))))))),4(5(4(3(1(4(0(2(4(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N137 <5(3(4(1(1(1(1(4(4(0(4(1(4(x))))))))))))),3(3(0(5(0(4(3(4(4(0(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N138 <5(5(0(5(0(2(3(3(4(2(4(2(x')))))))))))),5(3(4(1(0(1(4(5(0(0(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N139 <4(5(5(3(4(1(1(1(1(4(4(0(4(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N140 <5(0(1(3(2(3(0(3(2(5(3(x'))))))))))),0(5(4(0(2(5(4(5(2(1(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N141 <4(0(5(4(0(2(5(4(5(2(1(5(x)))))))))))),1(5(1(2(0(3(2(1(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N142 <5(5(3(4(1(0(1(4(5(0(0(x'))))))))))),5(3(4(1(0(1(4(5(0(0(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N143 <0(1(5(0(3(5(4(4(1(0(1(5(0(5(x)))))))))))))),5(3(2(5(1(0(1(2(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N144 <2(0(3(5(4(4(1(0(1(5(0(4(x)))))))))))),4(5(4(3(1(4(0(2(4(4(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N145 <5(2(5(5(0(4(1(5(5(2(0(3(1(3(3(x'))))))))))))))),0(4(2(3(3(5(2(1(4(4(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N146 <4(5(2(4(0(5(5(4(5(1(2(2(1(x'))))))))))))),4(1(5(5(2(0(3(1(3(3(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N147 <2(5(0(5(0(2(3(3(4(2(4(2(x')))))))))))),4(2(5(4(4(0(0(1(1(2(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N148 <3(3(0(5(0(4(3(4(4(0(x')))))))))),5(3(4(1(0(1(4(5(0(0(1(4(x'))))))))))))> => Not trivial, Overlay, Proper, NW0, N149 <2(3(3(0(5(0(4(3(4(4(0(x'))))))))))),4(2(5(4(4(0(0(1(1(2(5(1(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N150 <4(4(5(2(4(2(4(4(3(2(4(4(5(1(0(0(x')))))))))))))))),4(0(5(5(4(5(1(2(2(1(5(0(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N151 <4(5(2(1(1(4(2(4(0(4(2(0(x')))))))))))),1(5(1(2(0(3(2(1(0(5(2(4(5(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N152 <5(5(3(4(1(0(1(4(5(0(0(x'))))))))))),0(5(4(0(2(5(4(5(2(1(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N153 <4(2(5(5(1(5(3(4(1(0(1(4(5(0(0(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N154 <4(5(5(0(5(4(0(2(5(4(5(2(1(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N155 <1(2(4(5(2(4(1(5(5(2(0(3(1(3(3(x'))))))))))))))),3(3(5(3(0(4(0(3(1(3(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N156 <0(1(5(5(5(3(0(4(2(3(3(5(2(1(4(4(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N157 <2(2(1(1(4(2(4(0(4(2(0(x'))))))))))),4(2(5(4(4(0(0(1(1(2(2(4(5(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N158 <2(5(0(3(5(4(4(1(0(1(5(0(x')))))))))))),4(2(5(4(4(0(0(1(1(2(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N159 <0(1(5(5(5(3(3(4(1(1(1(1(4(4(0(4(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N160 <4(5(2(1(5(1(2(0(3(2(1(0(5(x'))))))))))))),4(1(5(5(2(0(3(1(3(3(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N161 <0(4(4(5(5(0(3(5(4(4(1(0(1(5(0(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N162 <5(0(1(3(2(3(0(3(2(5(3(x'))))))))))),5(3(4(1(0(1(4(5(0(0(2(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N163 <2(5(5(3(1(5(1(2(0(3(2(1(0(5(x')))))))))))))),4(5(4(3(1(4(0(2(4(4(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N164 <5(5(5(1(1(5(1(2(0(3(2(1(0(5(x')))))))))))))),3(3(0(5(0(4(3(4(4(0(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N165 <5(3(3(0(5(0(4(3(4(4(0(x'))))))))))),5(3(4(1(0(1(4(5(0(0(5(1(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N166 <0(2(5(3(1(5(1(2(0(3(2(1(0(5(x')))))))))))))),3(2(4(3(1(5(1(1(3(4(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N167 <5(0(5(4(0(2(5(4(5(2(1(x'))))))))))),3(4(1(1(1(1(4(4(0(4(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N168 <1(2(4(5(2(4(0(5(5(4(5(1(2(2(1(x'))))))))))))))),3(3(5(3(0(4(0(3(1(3(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N169 <2(5(0(4(2(3(3(5(2(1(4(4(x')))))))))))),4(2(5(4(4(0(0(1(1(2(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N170 <4(5(5(3(4(1(0(1(4(5(0(0(x')))))))))))),1(5(1(2(0(3(2(1(0(5(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N171 <0(1(5(5(5(3(0(3(5(4(4(1(0(1(5(0(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N172 <4(2(5(5(1(0(5(4(0(2(5(4(5(2(1(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N173 <5(5(5(1(4(0(5(5(4(5(1(2(2(1(x')))))))))))))),3(3(0(5(0(4(3(4(4(0(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N174 <0(4(4(5(5(3(4(1(1(1(1(4(4(0(4(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N175 <0(2(5(3(4(0(5(5(4(5(1(2(2(1(x')))))))))))))),3(2(4(3(1(5(1(1(3(4(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N176 <4(5(5(0(3(5(4(4(1(0(1(5(0(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N177 <4(2(5(5(1(0(4(2(3(3(5(2(1(4(4(x'))))))))))))))),2(3(4(2(1(1(3(4(2(5(2(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N178 <1(2(4(0(5(0(2(3(3(4(2(4(2(x'))))))))))))),3(3(5(3(0(4(0(3(1(3(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N179 <5(2(1(1(4(2(4(0(4(2(0(x'))))))))))),5(3(4(1(0(1(4(5(0(0(2(4(5(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N180 <5(2(1(1(4(2(4(0(4(2(0(x'))))))))))),0(5(4(0(2(5(4(5(2(1(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N181 <5(2(1(5(1(2(0(3(2(1(0(5(x')))))))))))),0(5(0(2(3(3(4(2(4(2(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N182 <1(2(4(5(2(2(3(4(2(1(1(3(4(2(5(x'))))))))))))))),3(3(5(3(0(4(0(3(1(3(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N183 <0(1(0(5(4(0(2(5(4(5(2(1(5(3(5(x))))))))))))))),5(3(2(5(1(0(1(2(0(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N184 <5(2(5(5(0(1(0(3(0(4(2(4(4(3(4(x'))))))))))))))),0(4(2(3(3(5(2(1(4(4(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N185 <2(1(1(4(2(4(0(4(2(0(x')))))))))),3(4(1(1(1(1(4(4(0(4(2(4(5(0(x'))))))))))))))> => Not trivial, Overlay, Proper, NW0, N186 <4(1(5(5(0(1(5(1(2(0(3(2(1(0(5(x'))))))))))))))),1(0(3(0(4(2(4(4(3(4(5(5(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N187 <4(3(3(0(5(0(4(3(4(4(0(x'))))))))))),1(5(1(2(0(3(2(1(0(5(1(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N188 <0(4(1(5(1(2(0(3(2(1(0(5(x')))))))))))),0(4(4(4(3(3(4(1(3(1(x'))))))))))> => Not trivial, Not overlay, Proper, NW0, N189 <5(5(5(1(4(1(5(5(2(0(3(1(3(3(x')))))))))))))),3(3(0(5(0(4(3(4(4(0(5(2(4(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N190 <2(5(0(2(3(4(2(1(1(3(4(2(5(x'))))))))))))),4(4(3(2(4(4(5(1(0(0(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N191 <5(0(5(0(2(3(3(4(2(4(2(5(0(x))))))))))))),2(1(1(4(2(4(0(4(2(0(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N192 <4(5(0(1(3(2(3(0(3(2(5(3(x')))))))))))),1(5(1(2(0(3(2(1(0(5(2(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N193 <0(4(4(5(5(0(1(3(2(3(0(3(2(5(3(x'))))))))))))))),0(4(4(4(3(3(4(1(3(1(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N194 <5(0(5(4(0(2(5(4(5(2(1(x'))))))))))),0(5(4(0(2(5(4(5(2(1(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N195 <4(5(5(5(3(4(1(0(1(4(5(0(0(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N196 <4(5(5(0(5(0(2(3(3(4(2(4(2(x'))))))))))))),1(5(1(2(0(3(2(1(0(5(2(4(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N197 <4(4(1(5(5(2(0(3(1(3(3(2(2(x))))))))))))),4(0(5(5(4(5(1(2(2(1(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N198 <4(4(5(2(4(2(4(5(4(3(1(4(0(2(4(4(x')))))))))))))))),4(0(5(5(4(5(1(2(2(1(5(5(3(4(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N199 <0(1(5(5(5(3(0(1(3(2(3(0(3(2(5(3(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(5(2(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N200 <5(5(0(5(4(0(2(5(4(5(2(1(x')))))))))))),5(3(4(1(0(1(4(5(0(0(5(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N201 <5(2(4(0(5(5(4(5(1(2(2(1(x')))))))))))),0(5(0(2(3(3(4(2(4(2(4(5(2(4(2(2(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N202 <0(1(5(5(5(3(5(3(4(1(0(1(4(5(0(0(x')))))))))))))))),5(3(2(5(1(0(1(2(0(5(5(5(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N203 <4(5(2(1(0(3(0(4(2(4(4(3(4(x'))))))))))))),4(1(5(5(2(0(3(1(3(3(1(5(5(0(4(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N204 <2(5(2(1(1(4(2(4(0(4(2(0(x')))))))))))),4(2(5(4(4(0(0(1(1(2(5(2(4(5(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N205 <0(4(4(5(2(1(1(4(2(4(0(4(2(0(x')))))))))))))),0(4(4(4(3(3(4(1(3(1(2(4(5(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N206 <2(5(5(3(2(3(4(2(1(1(3(4(2(5(x')))))))))))))),4(5(4(3(1(4(0(2(4(4(2(5(5(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N207 -> Problem conclusions: Left linear, Right linear, Linear Not weakly orthogonal, Not almost orthogonal, Not orthogonal Not Huet-Levy confluent, Not Newman confluent R is a TRS Problem 1: No Convergence Brute Force Procedure: -> Rewritings: s: 5(5(2(4(5(3(2(4(3(1(5(1(1(3(4(x'))))))))))))))) Nodes: [0,1,2,3,4] Edges: [(0,1),(0,2),(0,3),(0,4)] ID: 0 => ('5(5(2(4(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))))', D0) ID: 1 => ('5(0(5(0(2(3(3(4(2(4(2(5(3(2(4(3(1(5(1(1(3(4(x'))))))))))))))))))))))', D1, R13, P[1], S{x16 -> 5(3(2(4(3(1(5(1(1(3(4(x')))))))))))}), NR: '0(5(0(2(3(3(4(2(4(2(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))))))))))' ID: 2 => ('0(1(3(2(3(0(3(2(5(3(4(5(3(2(4(3(1(5(1(1(3(4(x'))))))))))))))))))))))', D1, R16, P[], S{x19 -> 4(5(3(2(4(3(1(5(1(1(3(4(x'))))))))))))}), NR: '0(1(3(2(3(0(3(2(5(3(4(5(3(2(4(3(1(5(1(1(3(4(x'))))))))))))))))))))))' ID: 3 => ('0(5(4(0(2(5(4(5(2(1(2(4(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))))))))))))', D1, R20, P[], S{x23 -> 2(4(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))}), NR: '0(5(4(0(2(5(4(5(2(1(2(4(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))))))))))))' ID: 4 => ('3(4(1(1(1(1(4(4(0(4(2(4(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))))))))))))', D1, R21, P[], S{x24 -> 2(4(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))}), NR: '3(4(1(1(1(1(4(4(0(4(2(4(5(3(2(4(3(1(5(1(1(3(4(x')))))))))))))))))))))))' t: 2(1(1(4(2(4(0(4(2(0(2(5(3(4(x')))))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('2(1(1(4(2(4(0(4(2(0(2(5(3(4(x'))))))))))))))', D0) ID: 1 => ('2(1(1(4(2(4(0(4(2(3(2(4(3(1(5(1(1(3(4(x')))))))))))))))))))', D1, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> x'}), NR: '3(2(4(3(1(5(1(1(3(4(x'))))))))))' 5(5(2(4(5(3(2(4(3(1(5(1(1(3(4(x'))))))))))))))) ->* no union *<- 2(1(1(4(2(4(0(4(2(0(2(5(3(4(x')))))))))))))) "Not joinable" The problem is not confluent.