NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (0 1) (1 1) (2 1) (3 1) (5 1) (4 1) (fSNonEmpty) ) (RULES 0(0(0(3(x)))) -> 4(2(4(0(2(5(3(3(4(5(x)))))))))) 0(2(1(x))) -> 0(4(0(1(4(5(1(5(0(1(x)))))))))) 0(2(3(1(3(x))))) -> 1(0(1(2(1(3(1(3(1(2(x)))))))))) 0(3(4(5(3(x))))) -> 2(0(2(5(1(2(4(4(5(5(x)))))))))) 0(5(2(1(3(x))))) -> 2(4(2(5(2(4(3(0(2(4(x)))))))))) 0(5(2(2(2(0(x)))))) -> 2(5(4(3(0(2(5(1(2(1(x)))))))))) 0(5(2(2(2(1(0(x))))))) -> 0(3(2(3(1(4(1(0(1(0(x)))))))))) 0(5(3(5(3(1(5(x))))))) -> 0(1(3(4(0(1(4(5(1(5(x)))))))))) 1(0(2(3(x)))) -> 1(1(2(5(4(1(2(4(3(2(x)))))))))) 1(1(3(x))) -> 1(2(1(2(2(2(5(1(4(2(x)))))))))) 1(1(5(1(4(4(3(x))))))) -> 1(0(3(4(4(1(0(2(5(5(x)))))))))) 1(3(2(3(0(5(3(x))))))) -> 1(4(0(1(5(4(0(3(2(5(x)))))))))) 1(3(5(3(x)))) -> 3(5(4(5(2(4(3(2(5(4(x)))))))))) 1(5(2(4(2(1(1(x))))))) -> 4(4(1(4(1(4(3(1(0(3(x)))))))))) 2(0(0(5(2(0(x)))))) -> 4(0(4(2(1(4(4(4(0(1(x)))))))))) 2(0(2(0(2(1(0(x))))))) -> 2(0(2(3(4(2(4(4(4(0(x)))))))))) 2(0(5(3(0(2(x)))))) -> 2(5(3(5(1(4(5(0(0(2(x)))))))))) 2(1(0(2(1(5(x)))))) -> 2(5(4(1(3(2(2(5(4(5(x)))))))))) 2(1(3(1(0(x))))) -> 0(1(4(5(1(5(5(2(3(0(x)))))))))) 2(4(5(5(1(3(5(x))))))) -> 2(1(2(1(4(4(4(3(4(4(x)))))))))) 3(0(0(5(5(2(1(x))))))) -> 0(2(4(3(2(3(2(1(0(3(x)))))))))) 3(1(5(2(3(0(5(x))))))) -> 5(3(4(0(4(5(2(0(0(4(x)))))))))) 5(1(5(1(0(2(x)))))) -> 4(5(0(0(4(3(1(1(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) (3 1) (5 1) (4 1) (fSNonEmpty) ) (RULES 0(0(0(3(x)))) -> 4(2(4(0(2(5(3(3(4(5(x)))))))))) 0(2(1(x))) -> 0(4(0(1(4(5(1(5(0(1(x)))))))))) 0(2(3(1(3(x))))) -> 1(0(1(2(1(3(1(3(1(2(x)))))))))) 0(3(4(5(3(x))))) -> 2(0(2(5(1(2(4(4(5(5(x)))))))))) 0(5(2(1(3(x))))) -> 2(4(2(5(2(4(3(0(2(4(x)))))))))) 0(5(2(2(2(0(x)))))) -> 2(5(4(3(0(2(5(1(2(1(x)))))))))) 0(5(2(2(2(1(0(x))))))) -> 0(3(2(3(1(4(1(0(1(0(x)))))))))) 0(5(3(5(3(1(5(x))))))) -> 0(1(3(4(0(1(4(5(1(5(x)))))))))) 1(0(2(3(x)))) -> 1(1(2(5(4(1(2(4(3(2(x)))))))))) 1(1(3(x))) -> 1(2(1(2(2(2(5(1(4(2(x)))))))))) 1(1(5(1(4(4(3(x))))))) -> 1(0(3(4(4(1(0(2(5(5(x)))))))))) 1(3(2(3(0(5(3(x))))))) -> 1(4(0(1(5(4(0(3(2(5(x)))))))))) 1(3(5(3(x)))) -> 3(5(4(5(2(4(3(2(5(4(x)))))))))) 1(5(2(4(2(1(1(x))))))) -> 4(4(1(4(1(4(3(1(0(3(x)))))))))) 2(0(0(5(2(0(x)))))) -> 4(0(4(2(1(4(4(4(0(1(x)))))))))) 2(0(2(0(2(1(0(x))))))) -> 2(0(2(3(4(2(4(4(4(0(x)))))))))) 2(0(5(3(0(2(x)))))) -> 2(5(3(5(1(4(5(0(0(2(x)))))))))) 2(1(0(2(1(5(x)))))) -> 2(5(4(1(3(2(2(5(4(5(x)))))))))) 2(1(3(1(0(x))))) -> 0(1(4(5(1(5(5(2(3(0(x)))))))))) 2(4(5(5(1(3(5(x))))))) -> 2(1(2(1(4(4(4(3(4(4(x)))))))))) 3(0(0(5(5(2(1(x))))))) -> 0(2(4(3(2(3(2(1(0(3(x)))))))))) 3(1(5(2(3(0(5(x))))))) -> 5(3(4(0(4(5(2(0(0(4(x)))))))))) 5(1(5(1(0(2(x)))))) -> 4(5(0(0(4(3(1(1(0(4(x)))))))))) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Procedure: -> Rules: 0(0(0(3(x)))) -> 4(2(4(0(2(5(3(3(4(5(x)))))))))) 0(2(1(x))) -> 0(4(0(1(4(5(1(5(0(1(x)))))))))) 0(2(3(1(3(x))))) -> 1(0(1(2(1(3(1(3(1(2(x)))))))))) 0(3(4(5(3(x))))) -> 2(0(2(5(1(2(4(4(5(5(x)))))))))) 0(5(2(1(3(x))))) -> 2(4(2(5(2(4(3(0(2(4(x)))))))))) 0(5(2(2(2(0(x)))))) -> 2(5(4(3(0(2(5(1(2(1(x)))))))))) 0(5(2(2(2(1(0(x))))))) -> 0(3(2(3(1(4(1(0(1(0(x)))))))))) 0(5(3(5(3(1(5(x))))))) -> 0(1(3(4(0(1(4(5(1(5(x)))))))))) 1(0(2(3(x)))) -> 1(1(2(5(4(1(2(4(3(2(x)))))))))) 1(1(3(x))) -> 1(2(1(2(2(2(5(1(4(2(x)))))))))) 1(1(5(1(4(4(3(x))))))) -> 1(0(3(4(4(1(0(2(5(5(x)))))))))) 1(3(2(3(0(5(3(x))))))) -> 1(4(0(1(5(4(0(3(2(5(x)))))))))) 1(3(5(3(x)))) -> 3(5(4(5(2(4(3(2(5(4(x)))))))))) 1(5(2(4(2(1(1(x))))))) -> 4(4(1(4(1(4(3(1(0(3(x)))))))))) 2(0(0(5(2(0(x)))))) -> 4(0(4(2(1(4(4(4(0(1(x)))))))))) 2(0(2(0(2(1(0(x))))))) -> 2(0(2(3(4(2(4(4(4(0(x)))))))))) 2(0(5(3(0(2(x)))))) -> 2(5(3(5(1(4(5(0(0(2(x)))))))))) 2(1(0(2(1(5(x)))))) -> 2(5(4(1(3(2(2(5(4(5(x)))))))))) 2(1(3(1(0(x))))) -> 0(1(4(5(1(5(5(2(3(0(x)))))))))) 2(4(5(5(1(3(5(x))))))) -> 2(1(2(1(4(4(4(3(4(4(x)))))))))) 3(0(0(5(5(2(1(x))))))) -> 0(2(4(3(2(3(2(1(0(3(x)))))))))) 3(1(5(2(3(0(5(x))))))) -> 5(3(4(0(4(5(2(0(0(4(x)))))))))) 5(1(5(1(0(2(x)))))) -> 4(5(0(0(4(3(1(1(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, x, x -> Rlps: (rule: 0(0(0(3(x)))) -> 4(2(4(0(2(5(3(3(4(5(x)))))))))), id: 1, possubterms: 0(0(0(3(x))))->[], 0(0(3(x)))->[1], 0(3(x))->[1, 1], 3(x)->[1, 1, 1]) (rule: 0(2(1(x))) -> 0(4(0(1(4(5(1(5(0(1(x)))))))))), id: 2, possubterms: 0(2(1(x)))->[], 2(1(x))->[1], 1(x)->[1, 1]) (rule: 0(2(3(1(3(x))))) -> 1(0(1(2(1(3(1(3(1(2(x)))))))))), id: 3, possubterms: 0(2(3(1(3(x)))))->[], 2(3(1(3(x))))->[1], 3(1(3(x)))->[1, 1], 1(3(x))->[1, 1, 1], 3(x)->[1, 1, 1, 1]) (rule: 0(3(4(5(3(x))))) -> 2(0(2(5(1(2(4(4(5(5(x)))))))))), id: 4, possubterms: 0(3(4(5(3(x)))))->[], 3(4(5(3(x))))->[1], 4(5(3(x)))->[1, 1], 5(3(x))->[1, 1, 1], 3(x)->[1, 1, 1, 1]) (rule: 0(5(2(1(3(x))))) -> 2(4(2(5(2(4(3(0(2(4(x)))))))))), id: 5, possubterms: 0(5(2(1(3(x)))))->[], 5(2(1(3(x))))->[1], 2(1(3(x)))->[1, 1], 1(3(x))->[1, 1, 1], 3(x)->[1, 1, 1, 1]) (rule: 0(5(2(2(2(0(x)))))) -> 2(5(4(3(0(2(5(1(2(1(x)))))))))), id: 6, possubterms: 0(5(2(2(2(0(x))))))->[], 5(2(2(2(0(x)))))->[1], 2(2(2(0(x))))->[1, 1], 2(2(0(x)))->[1, 1, 1], 2(0(x))->[1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1]) (rule: 0(5(2(2(2(1(0(x))))))) -> 0(3(2(3(1(4(1(0(1(0(x)))))))))), id: 7, possubterms: 0(5(2(2(2(1(0(x)))))))->[], 5(2(2(2(1(0(x))))))->[1], 2(2(2(1(0(x)))))->[1, 1], 2(2(1(0(x))))->[1, 1, 1], 2(1(0(x)))->[1, 1, 1, 1], 1(0(x))->[1, 1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1, 1]) (rule: 0(5(3(5(3(1(5(x))))))) -> 0(1(3(4(0(1(4(5(1(5(x)))))))))), id: 8, possubterms: 0(5(3(5(3(1(5(x)))))))->[], 5(3(5(3(1(5(x))))))->[1], 3(5(3(1(5(x)))))->[1, 1], 5(3(1(5(x))))->[1, 1, 1], 3(1(5(x)))->[1, 1, 1, 1], 1(5(x))->[1, 1, 1, 1, 1], 5(x)->[1, 1, 1, 1, 1, 1]) (rule: 1(0(2(3(x)))) -> 1(1(2(5(4(1(2(4(3(2(x)))))))))), id: 9, possubterms: 1(0(2(3(x))))->[], 0(2(3(x)))->[1], 2(3(x))->[1, 1], 3(x)->[1, 1, 1]) (rule: 1(1(3(x))) -> 1(2(1(2(2(2(5(1(4(2(x)))))))))), id: 10, possubterms: 1(1(3(x)))->[], 1(3(x))->[1], 3(x)->[1, 1]) (rule: 1(1(5(1(4(4(3(x))))))) -> 1(0(3(4(4(1(0(2(5(5(x)))))))))), id: 11, possubterms: 1(1(5(1(4(4(3(x)))))))->[], 1(5(1(4(4(3(x))))))->[1], 5(1(4(4(3(x)))))->[1, 1], 1(4(4(3(x))))->[1, 1, 1], 4(4(3(x)))->[1, 1, 1, 1], 4(3(x))->[1, 1, 1, 1, 1], 3(x)->[1, 1, 1, 1, 1, 1]) (rule: 1(3(2(3(0(5(3(x))))))) -> 1(4(0(1(5(4(0(3(2(5(x)))))))))), id: 12, possubterms: 1(3(2(3(0(5(3(x)))))))->[], 3(2(3(0(5(3(x))))))->[1], 2(3(0(5(3(x)))))->[1, 1], 3(0(5(3(x))))->[1, 1, 1], 0(5(3(x)))->[1, 1, 1, 1], 5(3(x))->[1, 1, 1, 1, 1], 3(x)->[1, 1, 1, 1, 1, 1]) (rule: 1(3(5(3(x)))) -> 3(5(4(5(2(4(3(2(5(4(x)))))))))), id: 13, possubterms: 1(3(5(3(x))))->[], 3(5(3(x)))->[1], 5(3(x))->[1, 1], 3(x)->[1, 1, 1]) (rule: 1(5(2(4(2(1(1(x))))))) -> 4(4(1(4(1(4(3(1(0(3(x)))))))))), id: 14, possubterms: 1(5(2(4(2(1(1(x)))))))->[], 5(2(4(2(1(1(x))))))->[1], 2(4(2(1(1(x)))))->[1, 1], 4(2(1(1(x))))->[1, 1, 1], 2(1(1(x)))->[1, 1, 1, 1], 1(1(x))->[1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1]) (rule: 2(0(0(5(2(0(x)))))) -> 4(0(4(2(1(4(4(4(0(1(x)))))))))), id: 15, possubterms: 2(0(0(5(2(0(x))))))->[], 0(0(5(2(0(x)))))->[1], 0(5(2(0(x))))->[1, 1], 5(2(0(x)))->[1, 1, 1], 2(0(x))->[1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1]) (rule: 2(0(2(0(2(1(0(x))))))) -> 2(0(2(3(4(2(4(4(4(0(x)))))))))), id: 16, possubterms: 2(0(2(0(2(1(0(x)))))))->[], 0(2(0(2(1(0(x))))))->[1], 2(0(2(1(0(x)))))->[1, 1], 0(2(1(0(x))))->[1, 1, 1], 2(1(0(x)))->[1, 1, 1, 1], 1(0(x))->[1, 1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1, 1]) (rule: 2(0(5(3(0(2(x)))))) -> 2(5(3(5(1(4(5(0(0(2(x)))))))))), id: 17, possubterms: 2(0(5(3(0(2(x))))))->[], 0(5(3(0(2(x)))))->[1], 5(3(0(2(x))))->[1, 1], 3(0(2(x)))->[1, 1, 1], 0(2(x))->[1, 1, 1, 1], 2(x)->[1, 1, 1, 1, 1]) (rule: 2(1(0(2(1(5(x)))))) -> 2(5(4(1(3(2(2(5(4(5(x)))))))))), id: 18, possubterms: 2(1(0(2(1(5(x))))))->[], 1(0(2(1(5(x)))))->[1], 0(2(1(5(x))))->[1, 1], 2(1(5(x)))->[1, 1, 1], 1(5(x))->[1, 1, 1, 1], 5(x)->[1, 1, 1, 1, 1]) (rule: 2(1(3(1(0(x))))) -> 0(1(4(5(1(5(5(2(3(0(x)))))))))), id: 19, possubterms: 2(1(3(1(0(x)))))->[], 1(3(1(0(x))))->[1], 3(1(0(x)))->[1, 1], 1(0(x))->[1, 1, 1], 0(x)->[1, 1, 1, 1]) (rule: 2(4(5(5(1(3(5(x))))))) -> 2(1(2(1(4(4(4(3(4(4(x)))))))))), id: 20, possubterms: 2(4(5(5(1(3(5(x)))))))->[], 4(5(5(1(3(5(x))))))->[1], 5(5(1(3(5(x)))))->[1, 1], 5(1(3(5(x))))->[1, 1, 1], 1(3(5(x)))->[1, 1, 1, 1], 3(5(x))->[1, 1, 1, 1, 1], 5(x)->[1, 1, 1, 1, 1, 1]) (rule: 3(0(0(5(5(2(1(x))))))) -> 0(2(4(3(2(3(2(1(0(3(x)))))))))), id: 21, possubterms: 3(0(0(5(5(2(1(x)))))))->[], 0(0(5(5(2(1(x))))))->[1], 0(5(5(2(1(x)))))->[1, 1], 5(5(2(1(x))))->[1, 1, 1], 5(2(1(x)))->[1, 1, 1, 1], 2(1(x))->[1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1]) (rule: 3(1(5(2(3(0(5(x))))))) -> 5(3(4(0(4(5(2(0(0(4(x)))))))))), id: 22, possubterms: 3(1(5(2(3(0(5(x)))))))->[], 1(5(2(3(0(5(x))))))->[1], 5(2(3(0(5(x)))))->[1, 1], 2(3(0(5(x))))->[1, 1, 1], 3(0(5(x)))->[1, 1, 1, 1], 0(5(x))->[1, 1, 1, 1, 1], 5(x)->[1, 1, 1, 1, 1, 1]) (rule: 5(1(5(1(0(2(x)))))) -> 4(5(0(0(4(3(1(1(0(4(x)))))))))), id: 23, possubterms: 5(1(5(1(0(2(x))))))->[], 1(5(1(0(2(x)))))->[1], 5(1(0(2(x))))->[1, 1], 1(0(2(x)))->[1, 1, 1], 0(2(x))->[1, 1, 1, 1], 2(x)->[1, 1, 1, 1, 1]) -> Unifications: (R1 unifies with R4 at p: [1,1], l: 0(0(0(3(x)))), lp: 0(3(x)), sig: {x -> 4(5(3(x')))}, l': 0(3(4(5(3(x'))))), r: 4(2(4(0(2(5(3(3(4(5(x)))))))))), r': 2(0(2(5(1(2(4(4(5(5(x'))))))))))) (R1 unifies with R21 at p: [1,1,1], l: 0(0(0(3(x)))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 4(2(4(0(2(5(3(3(4(5(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R1 unifies with R22 at p: [1,1,1], l: 0(0(0(3(x)))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 4(2(4(0(2(5(3(3(4(5(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R2 unifies with R18 at p: [1], l: 0(2(1(x))), lp: 2(1(x)), sig: {x -> 0(2(1(5(x'))))}, l': 2(1(0(2(1(5(x')))))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 2(5(4(1(3(2(2(5(4(5(x'))))))))))) (R2 unifies with R19 at p: [1], l: 0(2(1(x))), lp: 2(1(x)), sig: {x -> 3(1(0(x')))}, l': 2(1(3(1(0(x'))))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 0(1(4(5(1(5(5(2(3(0(x'))))))))))) (R2 unifies with R9 at p: [1,1], l: 0(2(1(x))), lp: 1(x), sig: {x -> 0(2(3(x')))}, l': 1(0(2(3(x')))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 1(1(2(5(4(1(2(4(3(2(x'))))))))))) (R2 unifies with R10 at p: [1,1], l: 0(2(1(x))), lp: 1(x), sig: {x -> 1(3(x'))}, l': 1(1(3(x'))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 1(2(1(2(2(2(5(1(4(2(x'))))))))))) (R2 unifies with R11 at p: [1,1], l: 0(2(1(x))), lp: 1(x), sig: {x -> 1(5(1(4(4(3(x'))))))}, l': 1(1(5(1(4(4(3(x'))))))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 1(0(3(4(4(1(0(2(5(5(x'))))))))))) (R2 unifies with R12 at p: [1,1], l: 0(2(1(x))), lp: 1(x), sig: {x -> 3(2(3(0(5(3(x'))))))}, l': 1(3(2(3(0(5(3(x'))))))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 1(4(0(1(5(4(0(3(2(5(x'))))))))))) (R2 unifies with R13 at p: [1,1], l: 0(2(1(x))), lp: 1(x), sig: {x -> 3(5(3(x')))}, l': 1(3(5(3(x')))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 3(5(4(5(2(4(3(2(5(4(x'))))))))))) (R2 unifies with R14 at p: [1,1], l: 0(2(1(x))), lp: 1(x), sig: {x -> 5(2(4(2(1(1(x'))))))}, l': 1(5(2(4(2(1(1(x'))))))), r: 0(4(0(1(4(5(1(5(0(1(x)))))))))), r': 4(4(1(4(1(4(3(1(0(3(x'))))))))))) (R3 unifies with R12 at p: [1,1,1], l: 0(2(3(1(3(x))))), lp: 1(3(x)), sig: {x -> 2(3(0(5(3(x')))))}, l': 1(3(2(3(0(5(3(x'))))))), r: 1(0(1(2(1(3(1(3(1(2(x)))))))))), r': 1(4(0(1(5(4(0(3(2(5(x'))))))))))) (R3 unifies with R13 at p: [1,1,1], l: 0(2(3(1(3(x))))), lp: 1(3(x)), sig: {x -> 5(3(x'))}, l': 1(3(5(3(x')))), r: 1(0(1(2(1(3(1(3(1(2(x)))))))))), r': 3(5(4(5(2(4(3(2(5(4(x'))))))))))) (R3 unifies with R21 at p: [1,1,1,1], l: 0(2(3(1(3(x))))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 1(0(1(2(1(3(1(3(1(2(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R3 unifies with R22 at p: [1,1,1,1], l: 0(2(3(1(3(x))))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 1(0(1(2(1(3(1(3(1(2(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R4 unifies with R21 at p: [1,1,1,1], l: 0(3(4(5(3(x))))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 2(0(2(5(1(2(4(4(5(5(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R4 unifies with R22 at p: [1,1,1,1], l: 0(3(4(5(3(x))))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 2(0(2(5(1(2(4(4(5(5(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R5 unifies with R19 at p: [1,1], l: 0(5(2(1(3(x))))), lp: 2(1(3(x))), sig: {x -> 1(0(x'))}, l': 2(1(3(1(0(x'))))), r: 2(4(2(5(2(4(3(0(2(4(x)))))))))), r': 0(1(4(5(1(5(5(2(3(0(x'))))))))))) (R5 unifies with R12 at p: [1,1,1], l: 0(5(2(1(3(x))))), lp: 1(3(x)), sig: {x -> 2(3(0(5(3(x')))))}, l': 1(3(2(3(0(5(3(x'))))))), r: 2(4(2(5(2(4(3(0(2(4(x)))))))))), r': 1(4(0(1(5(4(0(3(2(5(x'))))))))))) (R5 unifies with R13 at p: [1,1,1], l: 0(5(2(1(3(x))))), lp: 1(3(x)), sig: {x -> 5(3(x'))}, l': 1(3(5(3(x')))), r: 2(4(2(5(2(4(3(0(2(4(x)))))))))), r': 3(5(4(5(2(4(3(2(5(4(x'))))))))))) (R5 unifies with R21 at p: [1,1,1,1], l: 0(5(2(1(3(x))))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 2(4(2(5(2(4(3(0(2(4(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R5 unifies with R22 at p: [1,1,1,1], l: 0(5(2(1(3(x))))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 2(4(2(5(2(4(3(0(2(4(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R6 unifies with R15 at p: [1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 2(0(x)), sig: {x -> 0(5(2(0(x'))))}, l': 2(0(0(5(2(0(x')))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 4(0(4(2(1(4(4(4(0(1(x'))))))))))) (R6 unifies with R16 at p: [1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 2(0(x)), sig: {x -> 2(0(2(1(0(x')))))}, l': 2(0(2(0(2(1(0(x'))))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 2(0(2(3(4(2(4(4(4(0(x'))))))))))) (R6 unifies with R17 at p: [1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 2(0(x)), sig: {x -> 5(3(0(2(x'))))}, l': 2(0(5(3(0(2(x')))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 2(5(3(5(1(4(5(0(0(2(x'))))))))))) (R6 unifies with R1 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 0(0(3(x')))}, l': 0(0(0(3(x')))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 4(2(4(0(2(5(3(3(4(5(x'))))))))))) (R6 unifies with R2 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 2(1(x'))}, l': 0(2(1(x'))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R6 unifies with R3 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 2(3(1(3(x'))))}, l': 0(2(3(1(3(x'))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R6 unifies with R4 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 3(4(5(3(x'))))}, l': 0(3(4(5(3(x'))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 2(0(2(5(1(2(4(4(5(5(x'))))))))))) (R6 unifies with R5 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 5(2(1(3(x'))))}, l': 0(5(2(1(3(x'))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 2(4(2(5(2(4(3(0(2(4(x'))))))))))) (R6 unifies with R6 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 5(2(2(2(0(x')))))}, l': 0(5(2(2(2(0(x')))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 2(5(4(3(0(2(5(1(2(1(x'))))))))))) (R6 unifies with R7 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 5(2(2(2(1(0(x'))))))}, l': 0(5(2(2(2(1(0(x'))))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 0(3(2(3(1(4(1(0(1(0(x'))))))))))) (R6 unifies with R8 at p: [1,1,1,1,1], l: 0(5(2(2(2(0(x)))))), lp: 0(x), sig: {x -> 5(3(5(3(1(5(x'))))))}, l': 0(5(3(5(3(1(5(x'))))))), r: 2(5(4(3(0(2(5(1(2(1(x)))))))))), r': 0(1(3(4(0(1(4(5(1(5(x'))))))))))) (R7 unifies with R18 at p: [1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 2(1(0(x))), sig: {x -> 2(1(5(x')))}, l': 2(1(0(2(1(5(x')))))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 2(5(4(1(3(2(2(5(4(5(x'))))))))))) (R7 unifies with R9 at p: [1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 1(0(x)), sig: {x -> 2(3(x'))}, l': 1(0(2(3(x')))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 1(1(2(5(4(1(2(4(3(2(x'))))))))))) (R7 unifies with R1 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 0(0(3(x')))}, l': 0(0(0(3(x')))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 4(2(4(0(2(5(3(3(4(5(x'))))))))))) (R7 unifies with R2 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 2(1(x'))}, l': 0(2(1(x'))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R7 unifies with R3 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 2(3(1(3(x'))))}, l': 0(2(3(1(3(x'))))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R7 unifies with R4 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 3(4(5(3(x'))))}, l': 0(3(4(5(3(x'))))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 2(0(2(5(1(2(4(4(5(5(x'))))))))))) (R7 unifies with R5 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(2(1(3(x'))))}, l': 0(5(2(1(3(x'))))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 2(4(2(5(2(4(3(0(2(4(x'))))))))))) (R7 unifies with R6 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(2(2(2(0(x')))))}, l': 0(5(2(2(2(0(x')))))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 2(5(4(3(0(2(5(1(2(1(x'))))))))))) (R7 unifies with R7 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(2(2(2(1(0(x'))))))}, l': 0(5(2(2(2(1(0(x'))))))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 0(3(2(3(1(4(1(0(1(0(x'))))))))))) (R7 unifies with R8 at p: [1,1,1,1,1,1], l: 0(5(2(2(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(3(5(3(1(5(x'))))))}, l': 0(5(3(5(3(1(5(x'))))))), r: 0(3(2(3(1(4(1(0(1(0(x)))))))))), r': 0(1(3(4(0(1(4(5(1(5(x'))))))))))) (R8 unifies with R22 at p: [1,1,1,1], l: 0(5(3(5(3(1(5(x))))))), lp: 3(1(5(x))), sig: {x -> 2(3(0(5(x'))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 0(1(3(4(0(1(4(5(1(5(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R8 unifies with R14 at p: [1,1,1,1,1], l: 0(5(3(5(3(1(5(x))))))), lp: 1(5(x)), sig: {x -> 2(4(2(1(1(x')))))}, l': 1(5(2(4(2(1(1(x'))))))), r: 0(1(3(4(0(1(4(5(1(5(x)))))))))), r': 4(4(1(4(1(4(3(1(0(3(x'))))))))))) (R8 unifies with R23 at p: [1,1,1,1,1,1], l: 0(5(3(5(3(1(5(x))))))), lp: 5(x), sig: {x -> 1(5(1(0(2(x')))))}, l': 5(1(5(1(0(2(x')))))), r: 0(1(3(4(0(1(4(5(1(5(x)))))))))), r': 4(5(0(0(4(3(1(1(0(4(x'))))))))))) (R9 unifies with R3 at p: [1], l: 1(0(2(3(x)))), lp: 0(2(3(x))), sig: {x -> 1(3(x'))}, l': 0(2(3(1(3(x'))))), r: 1(1(2(5(4(1(2(4(3(2(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R9 unifies with R21 at p: [1,1,1], l: 1(0(2(3(x)))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 1(1(2(5(4(1(2(4(3(2(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R9 unifies with R22 at p: [1,1,1], l: 1(0(2(3(x)))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 1(1(2(5(4(1(2(4(3(2(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R10 unifies with R12 at p: [1], l: 1(1(3(x))), lp: 1(3(x)), sig: {x -> 2(3(0(5(3(x')))))}, l': 1(3(2(3(0(5(3(x'))))))), r: 1(2(1(2(2(2(5(1(4(2(x)))))))))), r': 1(4(0(1(5(4(0(3(2(5(x'))))))))))) (R10 unifies with R13 at p: [1], l: 1(1(3(x))), lp: 1(3(x)), sig: {x -> 5(3(x'))}, l': 1(3(5(3(x')))), r: 1(2(1(2(2(2(5(1(4(2(x)))))))))), r': 3(5(4(5(2(4(3(2(5(4(x'))))))))))) (R10 unifies with R21 at p: [1,1], l: 1(1(3(x))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 1(2(1(2(2(2(5(1(4(2(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R10 unifies with R22 at p: [1,1], l: 1(1(3(x))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 1(2(1(2(2(2(5(1(4(2(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R11 unifies with R21 at p: [1,1,1,1,1,1], l: 1(1(5(1(4(4(3(x))))))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 1(0(3(4(4(1(0(2(5(5(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R11 unifies with R22 at p: [1,1,1,1,1,1], l: 1(1(5(1(4(4(3(x))))))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 1(0(3(4(4(1(0(2(5(5(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R12 unifies with R8 at p: [1,1,1,1], l: 1(3(2(3(0(5(3(x))))))), lp: 0(5(3(x))), sig: {x -> 5(3(1(5(x'))))}, l': 0(5(3(5(3(1(5(x'))))))), r: 1(4(0(1(5(4(0(3(2(5(x)))))))))), r': 0(1(3(4(0(1(4(5(1(5(x'))))))))))) (R12 unifies with R21 at p: [1,1,1,1,1,1], l: 1(3(2(3(0(5(3(x))))))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 1(4(0(1(5(4(0(3(2(5(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R12 unifies with R22 at p: [1,1,1,1,1,1], l: 1(3(2(3(0(5(3(x))))))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 1(4(0(1(5(4(0(3(2(5(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R13 unifies with R21 at p: [1,1,1], l: 1(3(5(3(x)))), lp: 3(x), sig: {x -> 0(0(5(5(2(1(x'))))))}, l': 3(0(0(5(5(2(1(x'))))))), r: 3(5(4(5(2(4(3(2(5(4(x)))))))))), r': 0(2(4(3(2(3(2(1(0(3(x'))))))))))) (R13 unifies with R22 at p: [1,1,1], l: 1(3(5(3(x)))), lp: 3(x), sig: {x -> 1(5(2(3(0(5(x'))))))}, l': 3(1(5(2(3(0(5(x'))))))), r: 3(5(4(5(2(4(3(2(5(4(x)))))))))), r': 5(3(4(0(4(5(2(0(0(4(x'))))))))))) (R14 unifies with R10 at p: [1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(1(x)), sig: {x -> 3(x')}, l': 1(1(3(x'))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 1(2(1(2(2(2(5(1(4(2(x'))))))))))) (R14 unifies with R11 at p: [1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(1(x)), sig: {x -> 5(1(4(4(3(x')))))}, l': 1(1(5(1(4(4(3(x'))))))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 1(0(3(4(4(1(0(2(5(5(x'))))))))))) (R14 unifies with R9 at p: [1,1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(x), sig: {x -> 0(2(3(x')))}, l': 1(0(2(3(x')))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 1(1(2(5(4(1(2(4(3(2(x'))))))))))) (R14 unifies with R10 at p: [1,1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(x), sig: {x -> 1(3(x'))}, l': 1(1(3(x'))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 1(2(1(2(2(2(5(1(4(2(x'))))))))))) (R14 unifies with R11 at p: [1,1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(x), sig: {x -> 1(5(1(4(4(3(x'))))))}, l': 1(1(5(1(4(4(3(x'))))))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 1(0(3(4(4(1(0(2(5(5(x'))))))))))) (R14 unifies with R12 at p: [1,1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(x), sig: {x -> 3(2(3(0(5(3(x'))))))}, l': 1(3(2(3(0(5(3(x'))))))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 1(4(0(1(5(4(0(3(2(5(x'))))))))))) (R14 unifies with R13 at p: [1,1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(x), sig: {x -> 3(5(3(x')))}, l': 1(3(5(3(x')))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 3(5(4(5(2(4(3(2(5(4(x'))))))))))) (R14 unifies with R14 at p: [1,1,1,1,1,1], l: 1(5(2(4(2(1(1(x))))))), lp: 1(x), sig: {x -> 5(2(4(2(1(1(x'))))))}, l': 1(5(2(4(2(1(1(x'))))))), r: 4(4(1(4(1(4(3(1(0(3(x)))))))))), r': 4(4(1(4(1(4(3(1(0(3(x'))))))))))) (R15 unifies with R15 at p: [1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 2(0(x)), sig: {x -> 0(5(2(0(x'))))}, l': 2(0(0(5(2(0(x')))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 4(0(4(2(1(4(4(4(0(1(x'))))))))))) (R15 unifies with R16 at p: [1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 2(0(x)), sig: {x -> 2(0(2(1(0(x')))))}, l': 2(0(2(0(2(1(0(x'))))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 2(0(2(3(4(2(4(4(4(0(x'))))))))))) (R15 unifies with R17 at p: [1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 2(0(x)), sig: {x -> 5(3(0(2(x'))))}, l': 2(0(5(3(0(2(x')))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 2(5(3(5(1(4(5(0(0(2(x'))))))))))) (R15 unifies with R1 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 0(0(3(x')))}, l': 0(0(0(3(x')))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 4(2(4(0(2(5(3(3(4(5(x'))))))))))) (R15 unifies with R2 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 2(1(x'))}, l': 0(2(1(x'))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R15 unifies with R3 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 2(3(1(3(x'))))}, l': 0(2(3(1(3(x'))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R15 unifies with R4 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 3(4(5(3(x'))))}, l': 0(3(4(5(3(x'))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 2(0(2(5(1(2(4(4(5(5(x'))))))))))) (R15 unifies with R5 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 5(2(1(3(x'))))}, l': 0(5(2(1(3(x'))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 2(4(2(5(2(4(3(0(2(4(x'))))))))))) (R15 unifies with R6 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 5(2(2(2(0(x')))))}, l': 0(5(2(2(2(0(x')))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 2(5(4(3(0(2(5(1(2(1(x'))))))))))) (R15 unifies with R7 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 5(2(2(2(1(0(x'))))))}, l': 0(5(2(2(2(1(0(x'))))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 0(3(2(3(1(4(1(0(1(0(x'))))))))))) (R15 unifies with R8 at p: [1,1,1,1,1], l: 2(0(0(5(2(0(x)))))), lp: 0(x), sig: {x -> 5(3(5(3(1(5(x'))))))}, l': 0(5(3(5(3(1(5(x'))))))), r: 4(0(4(2(1(4(4(4(0(1(x)))))))))), r': 0(1(3(4(0(1(4(5(1(5(x'))))))))))) (R16 unifies with R2 at p: [1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(2(1(0(x)))), sig: {x' -> 0(x)}, l': 0(2(1(x'))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R16 unifies with R18 at p: [1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 2(1(0(x))), sig: {x -> 2(1(5(x')))}, l': 2(1(0(2(1(5(x')))))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 2(5(4(1(3(2(2(5(4(5(x'))))))))))) (R16 unifies with R9 at p: [1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 1(0(x)), sig: {x -> 2(3(x'))}, l': 1(0(2(3(x')))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 1(1(2(5(4(1(2(4(3(2(x'))))))))))) (R16 unifies with R1 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 0(0(3(x')))}, l': 0(0(0(3(x')))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 4(2(4(0(2(5(3(3(4(5(x'))))))))))) (R16 unifies with R2 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 2(1(x'))}, l': 0(2(1(x'))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R16 unifies with R3 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 2(3(1(3(x'))))}, l': 0(2(3(1(3(x'))))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R16 unifies with R4 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 3(4(5(3(x'))))}, l': 0(3(4(5(3(x'))))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 2(0(2(5(1(2(4(4(5(5(x'))))))))))) (R16 unifies with R5 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(2(1(3(x'))))}, l': 0(5(2(1(3(x'))))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 2(4(2(5(2(4(3(0(2(4(x'))))))))))) (R16 unifies with R6 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(2(2(2(0(x')))))}, l': 0(5(2(2(2(0(x')))))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 2(5(4(3(0(2(5(1(2(1(x'))))))))))) (R16 unifies with R7 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(2(2(2(1(0(x'))))))}, l': 0(5(2(2(2(1(0(x'))))))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 0(3(2(3(1(4(1(0(1(0(x'))))))))))) (R16 unifies with R8 at p: [1,1,1,1,1,1], l: 2(0(2(0(2(1(0(x))))))), lp: 0(x), sig: {x -> 5(3(5(3(1(5(x'))))))}, l': 0(5(3(5(3(1(5(x'))))))), r: 2(0(2(3(4(2(4(4(4(0(x)))))))))), r': 0(1(3(4(0(1(4(5(1(5(x'))))))))))) (R17 unifies with R2 at p: [1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 0(2(x)), sig: {x -> 1(x')}, l': 0(2(1(x'))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R17 unifies with R3 at p: [1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 0(2(x)), sig: {x -> 3(1(3(x')))}, l': 0(2(3(1(3(x'))))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R17 unifies with R15 at p: [1,1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 2(x), sig: {x -> 0(0(5(2(0(x')))))}, l': 2(0(0(5(2(0(x')))))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 4(0(4(2(1(4(4(4(0(1(x'))))))))))) (R17 unifies with R16 at p: [1,1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 2(x), sig: {x -> 0(2(0(2(1(0(x'))))))}, l': 2(0(2(0(2(1(0(x'))))))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 2(0(2(3(4(2(4(4(4(0(x'))))))))))) (R17 unifies with R17 at p: [1,1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 2(x), sig: {x -> 0(5(3(0(2(x')))))}, l': 2(0(5(3(0(2(x')))))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 2(5(3(5(1(4(5(0(0(2(x'))))))))))) (R17 unifies with R18 at p: [1,1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 2(x), sig: {x -> 1(0(2(1(5(x')))))}, l': 2(1(0(2(1(5(x')))))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 2(5(4(1(3(2(2(5(4(5(x'))))))))))) (R17 unifies with R19 at p: [1,1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 2(x), sig: {x -> 1(3(1(0(x'))))}, l': 2(1(3(1(0(x'))))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 0(1(4(5(1(5(5(2(3(0(x'))))))))))) (R17 unifies with R20 at p: [1,1,1,1,1], l: 2(0(5(3(0(2(x)))))), lp: 2(x), sig: {x -> 4(5(5(1(3(5(x'))))))}, l': 2(4(5(5(1(3(5(x'))))))), r: 2(5(3(5(1(4(5(0(0(2(x)))))))))), r': 2(1(2(1(4(4(4(3(4(4(x'))))))))))) (R18 unifies with R2 at p: [1,1], l: 2(1(0(2(1(5(x)))))), lp: 0(2(1(5(x)))), sig: {x' -> 5(x)}, l': 0(2(1(x'))), r: 2(5(4(1(3(2(2(5(4(5(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R18 unifies with R14 at p: [1,1,1,1], l: 2(1(0(2(1(5(x)))))), lp: 1(5(x)), sig: {x -> 2(4(2(1(1(x')))))}, l': 1(5(2(4(2(1(1(x'))))))), r: 2(5(4(1(3(2(2(5(4(5(x)))))))))), r': 4(4(1(4(1(4(3(1(0(3(x'))))))))))) (R18 unifies with R23 at p: [1,1,1,1,1], l: 2(1(0(2(1(5(x)))))), lp: 5(x), sig: {x -> 1(5(1(0(2(x')))))}, l': 5(1(5(1(0(2(x')))))), r: 2(5(4(1(3(2(2(5(4(5(x)))))))))), r': 4(5(0(0(4(3(1(1(0(4(x'))))))))))) (R19 unifies with R9 at p: [1,1,1], l: 2(1(3(1(0(x))))), lp: 1(0(x)), sig: {x -> 2(3(x'))}, l': 1(0(2(3(x')))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 1(1(2(5(4(1(2(4(3(2(x'))))))))))) (R19 unifies with R1 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 0(0(3(x')))}, l': 0(0(0(3(x')))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 4(2(4(0(2(5(3(3(4(5(x'))))))))))) (R19 unifies with R2 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 2(1(x'))}, l': 0(2(1(x'))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R19 unifies with R3 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 2(3(1(3(x'))))}, l': 0(2(3(1(3(x'))))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R19 unifies with R4 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 3(4(5(3(x'))))}, l': 0(3(4(5(3(x'))))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 2(0(2(5(1(2(4(4(5(5(x'))))))))))) (R19 unifies with R5 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 5(2(1(3(x'))))}, l': 0(5(2(1(3(x'))))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 2(4(2(5(2(4(3(0(2(4(x'))))))))))) (R19 unifies with R6 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 5(2(2(2(0(x')))))}, l': 0(5(2(2(2(0(x')))))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 2(5(4(3(0(2(5(1(2(1(x'))))))))))) (R19 unifies with R7 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 5(2(2(2(1(0(x'))))))}, l': 0(5(2(2(2(1(0(x'))))))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 0(3(2(3(1(4(1(0(1(0(x'))))))))))) (R19 unifies with R8 at p: [1,1,1,1], l: 2(1(3(1(0(x))))), lp: 0(x), sig: {x -> 5(3(5(3(1(5(x'))))))}, l': 0(5(3(5(3(1(5(x'))))))), r: 0(1(4(5(1(5(5(2(3(0(x)))))))))), r': 0(1(3(4(0(1(4(5(1(5(x'))))))))))) (R20 unifies with R13 at p: [1,1,1,1], l: 2(4(5(5(1(3(5(x))))))), lp: 1(3(5(x))), sig: {x -> 3(x')}, l': 1(3(5(3(x')))), r: 2(1(2(1(4(4(4(3(4(4(x)))))))))), r': 3(5(4(5(2(4(3(2(5(4(x'))))))))))) (R20 unifies with R23 at p: [1,1,1,1,1,1], l: 2(4(5(5(1(3(5(x))))))), lp: 5(x), sig: {x -> 1(5(1(0(2(x')))))}, l': 5(1(5(1(0(2(x')))))), r: 2(1(2(1(4(4(4(3(4(4(x)))))))))), r': 4(5(0(0(4(3(1(1(0(4(x'))))))))))) (R21 unifies with R18 at p: [1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 2(1(x)), sig: {x -> 0(2(1(5(x'))))}, l': 2(1(0(2(1(5(x')))))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 2(5(4(1(3(2(2(5(4(5(x'))))))))))) (R21 unifies with R19 at p: [1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 2(1(x)), sig: {x -> 3(1(0(x')))}, l': 2(1(3(1(0(x'))))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 0(1(4(5(1(5(5(2(3(0(x'))))))))))) (R21 unifies with R9 at p: [1,1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 1(x), sig: {x -> 0(2(3(x')))}, l': 1(0(2(3(x')))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 1(1(2(5(4(1(2(4(3(2(x'))))))))))) (R21 unifies with R10 at p: [1,1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 1(x), sig: {x -> 1(3(x'))}, l': 1(1(3(x'))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 1(2(1(2(2(2(5(1(4(2(x'))))))))))) (R21 unifies with R11 at p: [1,1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 1(x), sig: {x -> 1(5(1(4(4(3(x'))))))}, l': 1(1(5(1(4(4(3(x'))))))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 1(0(3(4(4(1(0(2(5(5(x'))))))))))) (R21 unifies with R12 at p: [1,1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 1(x), sig: {x -> 3(2(3(0(5(3(x'))))))}, l': 1(3(2(3(0(5(3(x'))))))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 1(4(0(1(5(4(0(3(2(5(x'))))))))))) (R21 unifies with R13 at p: [1,1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 1(x), sig: {x -> 3(5(3(x')))}, l': 1(3(5(3(x')))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 3(5(4(5(2(4(3(2(5(4(x'))))))))))) (R21 unifies with R14 at p: [1,1,1,1,1,1], l: 3(0(0(5(5(2(1(x))))))), lp: 1(x), sig: {x -> 5(2(4(2(1(1(x'))))))}, l': 1(5(2(4(2(1(1(x'))))))), r: 0(2(4(3(2(3(2(1(0(3(x)))))))))), r': 4(4(1(4(1(4(3(1(0(3(x'))))))))))) (R22 unifies with R5 at p: [1,1,1,1,1], l: 3(1(5(2(3(0(5(x))))))), lp: 0(5(x)), sig: {x -> 2(1(3(x')))}, l': 0(5(2(1(3(x'))))), r: 5(3(4(0(4(5(2(0(0(4(x)))))))))), r': 2(4(2(5(2(4(3(0(2(4(x'))))))))))) (R22 unifies with R6 at p: [1,1,1,1,1], l: 3(1(5(2(3(0(5(x))))))), lp: 0(5(x)), sig: {x -> 2(2(2(0(x'))))}, l': 0(5(2(2(2(0(x')))))), r: 5(3(4(0(4(5(2(0(0(4(x)))))))))), r': 2(5(4(3(0(2(5(1(2(1(x'))))))))))) (R22 unifies with R7 at p: [1,1,1,1,1], l: 3(1(5(2(3(0(5(x))))))), lp: 0(5(x)), sig: {x -> 2(2(2(1(0(x')))))}, l': 0(5(2(2(2(1(0(x'))))))), r: 5(3(4(0(4(5(2(0(0(4(x)))))))))), r': 0(3(2(3(1(4(1(0(1(0(x'))))))))))) (R22 unifies with R8 at p: [1,1,1,1,1], l: 3(1(5(2(3(0(5(x))))))), lp: 0(5(x)), sig: {x -> 3(5(3(1(5(x')))))}, l': 0(5(3(5(3(1(5(x'))))))), r: 5(3(4(0(4(5(2(0(0(4(x)))))))))), r': 0(1(3(4(0(1(4(5(1(5(x'))))))))))) (R22 unifies with R23 at p: [1,1,1,1,1,1], l: 3(1(5(2(3(0(5(x))))))), lp: 5(x), sig: {x -> 1(5(1(0(2(x')))))}, l': 5(1(5(1(0(2(x')))))), r: 5(3(4(0(4(5(2(0(0(4(x)))))))))), r': 4(5(0(0(4(3(1(1(0(4(x'))))))))))) (R23 unifies with R9 at p: [1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 1(0(2(x))), sig: {x -> 3(x')}, l': 1(0(2(3(x')))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 1(1(2(5(4(1(2(4(3(2(x'))))))))))) (R23 unifies with R2 at p: [1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 0(2(x)), sig: {x -> 1(x')}, l': 0(2(1(x'))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 0(4(0(1(4(5(1(5(0(1(x'))))))))))) (R23 unifies with R3 at p: [1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 0(2(x)), sig: {x -> 3(1(3(x')))}, l': 0(2(3(1(3(x'))))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 1(0(1(2(1(3(1(3(1(2(x'))))))))))) (R23 unifies with R15 at p: [1,1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 2(x), sig: {x -> 0(0(5(2(0(x')))))}, l': 2(0(0(5(2(0(x')))))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 4(0(4(2(1(4(4(4(0(1(x'))))))))))) (R23 unifies with R16 at p: [1,1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 2(x), sig: {x -> 0(2(0(2(1(0(x'))))))}, l': 2(0(2(0(2(1(0(x'))))))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 2(0(2(3(4(2(4(4(4(0(x'))))))))))) (R23 unifies with R17 at p: [1,1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 2(x), sig: {x -> 0(5(3(0(2(x')))))}, l': 2(0(5(3(0(2(x')))))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 2(5(3(5(1(4(5(0(0(2(x'))))))))))) (R23 unifies with R18 at p: [1,1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 2(x), sig: {x -> 1(0(2(1(5(x')))))}, l': 2(1(0(2(1(5(x')))))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 2(5(4(1(3(2(2(5(4(5(x'))))))))))) (R23 unifies with R19 at p: [1,1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 2(x), sig: {x -> 1(3(1(0(x'))))}, l': 2(1(3(1(0(x'))))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 0(1(4(5(1(5(5(2(3(0(x'))))))))))) (R23 unifies with R20 at p: [1,1,1,1,1], l: 5(1(5(1(0(2(x)))))), lp: 2(x), sig: {x -> 4(5(5(1(3(5(x'))))))}, l': 2(4(5(5(1(3(5(x'))))))), r: 4(5(0(0(4(3(1(1(0(4(x)))))))))), r': 2(1(2(1(4(4(4(3(4(4(x'))))))))))) -> Critical pairs info: <2(0(0(5(2(0(2(3(4(2(4(4(4(0(x')))))))))))))),4(0(4(2(1(4(4(4(0(1(2(0(2(1(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N1 <1(1(5(1(4(4(5(3(4(0(4(5(2(0(0(4(x')))))))))))))))),1(0(3(4(4(1(0(2(5(5(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N2 <5(1(5(1(0(4(0(4(2(1(4(4(4(0(1(x'))))))))))))))),4(5(0(0(4(3(1(1(0(4(0(0(5(2(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N3 <0(5(2(2(2(0(4(0(1(4(5(1(5(0(1(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(2(1(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N4 <0(5(2(2(2(1(2(0(2(5(1(2(4(4(5(5(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(3(4(5(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N5 <1(3(2(3(0(1(3(4(0(1(4(5(1(5(x')))))))))))))),1(4(0(1(5(4(0(3(2(5(5(3(1(5(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N6 <1(3(5(5(3(4(0(4(5(2(0(0(4(x'))))))))))))),3(5(4(5(2(4(3(2(5(4(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N7 <2(0(2(0(2(1(0(3(2(3(1(4(1(0(1(0(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(5(2(2(2(1(0(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N8 <2(0(2(0(2(1(2(0(2(5(1(2(4(4(5(5(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(3(4(5(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N9 <1(5(2(4(2(1(4(4(1(4(1(4(3(1(0(3(x')))))))))))))))),4(4(1(4(1(4(3(1(0(3(5(2(4(2(1(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N10 <0(5(2(2(2(1(2(4(2(5(2(4(3(0(2(4(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(5(2(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N11 <0(5(2(2(2(1(0(1(2(1(3(1(3(1(2(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(2(3(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N12 <3(0(0(5(5(2(1(0(3(4(4(1(0(2(5(5(x')))))))))))))))),0(2(4(3(2(3(2(1(0(3(1(5(1(4(4(3(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N13 <2(0(0(5(4(0(4(2(1(4(4(4(0(1(x')))))))))))))),4(0(4(2(1(4(4(4(0(1(0(5(2(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N14 <1(1(5(3(4(0(4(5(2(0(0(4(x')))))))))))),1(2(1(2(2(2(5(1(4(2(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N15 <2(1(3(1(2(0(2(5(1(2(4(4(5(5(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(3(4(5(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N16 <2(0(5(3(0(4(0(4(2(1(4(4(4(0(1(x'))))))))))))))),2(5(3(5(1(4(5(0(0(2(0(0(5(2(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N17 <2(0(5(3(0(2(5(4(1(3(2(2(5(4(5(x'))))))))))))))),2(5(3(5(1(4(5(0(0(2(1(0(2(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N18 <3(0(0(5(5(2(1(1(2(5(4(1(2(4(3(2(x')))))))))))))))),0(2(4(3(2(3(2(1(0(3(0(2(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N19 <0(5(2(2(4(0(4(2(1(4(4(4(0(1(x')))))))))))))),2(5(4(3(0(2(5(1(2(1(0(5(2(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N20 <2(1(3(1(2(4(2(5(2(4(3(0(2(4(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(5(2(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N21 <3(0(0(5(5(2(5(4(1(3(2(2(5(4(5(x'))))))))))))))),0(2(4(3(2(3(2(1(0(3(0(2(1(5(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N22 <0(5(2(1(4(0(1(5(4(0(3(2(5(x'))))))))))))),2(4(2(5(2(4(3(0(2(4(2(3(0(5(3(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N23 <1(5(2(4(2(1(1(4(0(1(5(4(0(3(2(5(x')))))))))))))))),4(4(1(4(1(4(3(1(0(3(3(2(3(0(5(3(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N24 <2(1(3(1(0(1(3(4(0(1(4(5(1(5(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(5(3(5(3(1(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N25 <0(5(2(2(2(2(5(4(3(0(2(5(1(2(1(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(5(2(2(2(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N26 <0(3(4(5(0(2(4(3(2(3(2(1(0(3(x')))))))))))))),2(0(2(5(1(2(4(4(5(5(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N27 <0(5(3(5(3(1(4(5(0(0(4(3(1(1(0(4(x')))))))))))))))),0(1(3(4(0(1(4(5(1(5(1(5(1(0(2(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N28 <5(1(5(1(0(2(1(2(1(4(4(4(3(4(4(x'))))))))))))))),4(5(0(0(4(3(1(1(0(4(4(5(5(1(3(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N29 <0(3(4(5(5(3(4(0(4(5(2(0(0(4(x')))))))))))))),2(0(2(5(1(2(4(4(5(5(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N30 <0(5(2(2(2(1(0(4(0(1(4(5(1(5(0(1(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(2(1(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N31 <3(0(0(5(5(2(3(5(4(5(2(4(3(2(5(4(x')))))))))))))))),0(2(4(3(2(3(2(1(0(3(3(5(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N32 <2(0(2(0(2(1(4(2(4(0(2(5(3(3(4(5(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(0(0(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N33 <2(0(5(3(0(2(5(3(5(1(4(5(0(0(2(x'))))))))))))))),2(5(3(5(1(4(5(0(0(2(0(5(3(0(2(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N34 <5(1(5(1(0(4(0(1(4(5(1(5(0(1(x')))))))))))))),4(5(0(0(4(3(1(1(0(4(1(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N35 <0(5(2(2(2(1(1(0(1(2(1(3(1(3(1(2(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(2(3(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N36 <5(1(5(1(1(2(5(4(1(2(4(3(2(x'))))))))))))),4(5(0(0(4(3(1(1(0(4(3(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N37 <0(0(0(5(3(4(0(4(5(2(0(0(4(x'))))))))))))),4(2(4(0(2(5(3(3(4(5(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N38 <2(0(2(0(2(1(2(5(4(3(0(2(5(1(2(1(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(5(2(2(2(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N39 <0(5(3(5(5(3(4(0(4(5(2(0(0(4(x')))))))))))))),0(1(3(4(0(1(4(5(1(5(2(3(0(5(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N40 <1(1(5(1(4(4(0(2(4(3(2(3(2(1(0(3(x')))))))))))))))),1(0(3(4(4(1(0(2(5(5(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N41 <3(1(5(2(3(2(5(4(3(0(2(5(1(2(1(x'))))))))))))))),5(3(4(0(4(5(2(0(0(4(2(2(2(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N42 <1(5(2(4(2(1(3(5(4(5(2(4(3(2(5(4(x')))))))))))))))),4(4(1(4(1(4(3(1(0(3(3(5(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N43 <2(0(5(3(0(0(1(4(5(1(5(5(2(3(0(x'))))))))))))))),2(5(3(5(1(4(5(0(0(2(1(3(1(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N44 <5(1(5(1(1(0(1(2(1(3(1(3(1(2(x')))))))))))))),4(5(0(0(4(3(1(1(0(4(3(1(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N45 <2(1(3(1(1(2(5(4(1(2(4(3(2(x'))))))))))))),0(1(4(5(1(5(5(2(3(0(2(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N46 <0(5(2(2(2(0(2(3(4(2(4(4(4(0(x')))))))))))))),2(5(4(3(0(2(5(1(2(1(2(0(2(1(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N47 <0(5(2(2(2(1(0(1(3(4(0(1(4(5(1(5(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(5(3(5(3(1(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N48 <1(5(2(4(2(1(2(1(2(2(2(5(1(4(2(x'))))))))))))))),4(4(1(4(1(4(3(1(0(3(3(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N49 <2(0(2(0(2(1(0(1(3(4(0(1(4(5(1(5(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(5(3(5(3(1(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N50 <0(5(2(2(2(0(1(3(4(0(1(4(5(1(5(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(5(3(5(3(1(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N51 <0(2(3(3(5(4(5(2(4(3(2(5(4(x'))))))))))))),1(0(1(2(1(3(1(3(1(2(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N52 <1(0(2(0(2(4(3(2(3(2(1(0(3(x'))))))))))))),1(1(2(5(4(1(2(4(3(2(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N53 <1(3(2(3(0(5(0(2(4(3(2(3(2(1(0(3(x')))))))))))))))),1(4(0(1(5(4(0(3(2(5(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N54 <0(5(2(1(5(3(4(0(4(5(2(0(0(4(x')))))))))))))),2(4(2(5(2(4(3(0(2(4(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N55 <0(0(1(4(5(1(5(5(2(3(0(x'))))))))))),0(4(0(1(4(5(1(5(0(1(3(1(0(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N56 <2(4(5(5(1(3(4(5(0(0(4(3(1(1(0(4(x')))))))))))))))),2(1(2(1(4(4(4(3(4(4(1(5(1(0(2(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N57 <0(0(0(0(2(4(3(2(3(2(1(0(3(x'))))))))))))),4(2(4(0(2(5(3(3(4(5(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N58 <5(1(5(1(0(2(5(4(1(3(2(2(5(4(5(x'))))))))))))))),4(5(0(0(4(3(1(1(0(4(1(0(2(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N59 <1(5(2(4(2(1(1(1(2(5(4(1(2(4(3(2(x')))))))))))))))),4(4(1(4(1(4(3(1(0(3(0(2(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N60 <3(1(5(2(3(0(4(5(0(0(4(3(1(1(0(4(x')))))))))))))))),5(3(4(0(4(5(2(0(0(4(1(5(1(0(2(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N61 <0(2(5(4(1(3(2(2(5(4(5(x'))))))))))),0(4(0(1(4(5(1(5(0(1(0(2(1(5(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N62 <1(3(5(0(2(4(3(2(3(2(1(0(3(x'))))))))))))),3(5(4(5(2(4(3(2(5(4(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N63 <2(1(3(1(2(5(4(3(0(2(5(1(2(1(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(5(2(2(2(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N64 <1(3(2(3(0(5(5(3(4(0(4(5(2(0(0(4(x')))))))))))))))),1(4(0(1(5(4(0(3(2(5(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N65 <0(5(2(2(2(2(4(2(5(2(4(3(0(2(4(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(5(2(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N66 <2(0(2(0(2(1(1(0(1(2(1(3(1(3(1(2(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(2(3(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N67 <3(1(5(2(3(0(1(3(4(0(1(4(5(1(5(x'))))))))))))))),5(3(4(0(4(5(2(0(0(4(3(5(3(1(5(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N68 <1(5(2(4(2(1(1(0(3(4(4(1(0(2(5(5(x')))))))))))))))),4(4(1(4(1(4(3(1(0(3(1(5(1(4(4(3(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N69 <2(0(0(5(2(2(5(4(3(0(2(5(1(2(1(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(5(2(2(2(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N70 <2(0(2(0(2(1(0(4(0(1(4(5(1(5(0(1(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(2(1(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N71 <1(5(2(4(2(1(1(2(1(2(2(2(5(1(4(2(x')))))))))))))))),4(4(1(4(1(4(3(1(0(3(1(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N72 <3(0(0(5(5(2(4(4(1(4(1(4(3(1(0(3(x')))))))))))))))),0(2(4(3(2(3(2(1(0(3(5(2(4(2(1(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N73 <0(5(2(2(2(1(1(2(5(4(1(2(4(3(2(x'))))))))))))))),0(3(2(3(1(4(1(0(1(0(2(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N74 <0(5(2(2(2(2(0(2(5(1(2(4(4(5(5(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(3(4(5(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N75 <0(5(2(2(2(0(3(2(3(1(4(1(0(1(0(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(5(2(2(2(1(0(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N76 <0(5(2(3(5(4(5(2(4(3(2(5(4(x'))))))))))))),2(4(2(5(2(4(3(0(2(4(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N77 <1(1(0(1(2(1(3(1(3(1(2(x'))))))))))),1(1(2(5(4(1(2(4(3(2(1(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N78 <0(2(1(0(3(4(4(1(0(2(5(5(x')))))))))))),0(4(0(1(4(5(1(5(0(1(1(5(1(4(4(3(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N79 <3(0(0(5(5(2(1(2(1(2(2(2(5(1(4(2(x')))))))))))))))),0(2(4(3(2(3(2(1(0(3(1(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N80 <2(0(2(0(4(0(1(4(5(1(5(0(1(0(x)))))))))))))),2(0(2(3(4(2(4(4(4(0(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N81 <0(2(1(4(0(1(5(4(0(3(2(5(x')))))))))))),0(4(0(1(4(5(1(5(0(1(3(2(3(0(5(3(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N82 <1(5(2(4(2(1(0(3(4(4(1(0(2(5(5(x'))))))))))))))),4(4(1(4(1(4(3(1(0(3(5(1(4(4(3(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N83 <2(1(0(2(1(4(5(0(0(4(3(1(1(0(4(x'))))))))))))))),2(5(4(1(3(2(2(5(4(5(1(5(1(0(2(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N84 <0(5(2(2(2(4(2(4(0(2(5(3(3(4(5(x'))))))))))))))),2(5(4(3(0(2(5(1(2(1(0(0(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N85 <1(1(4(0(1(5(4(0(3(2(5(x'))))))))))),1(2(1(2(2(2(5(1(4(2(2(3(0(5(3(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N86 <2(0(2(0(2(1(2(4(2(5(2(4(3(0(2(4(x')))))))))))))))),2(0(2(3(4(2(4(4(4(0(5(2(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N87 <2(0(5(3(1(0(1(2(1(3(1(3(1(2(x')))))))))))))),2(5(3(5(1(4(5(0(0(2(3(1(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N88 <5(1(5(1(0(2(5(3(5(1(4(5(0(0(2(x'))))))))))))))),4(5(0(0(4(3(1(1(0(4(0(5(3(0(2(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N89 <2(0(0(5(2(0(4(0(1(4(5(1(5(0(1(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(2(1(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N90 <2(0(2(0(2(5(4(1(3(2(2(5(4(5(x')))))))))))))),2(0(2(3(4(2(4(4(4(0(2(1(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N91 <2(1(3(1(0(3(2(3(1(4(1(0(1(0(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(5(2(2(2(1(0(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N92 <2(0(2(0(2(1(1(2(5(4(1(2(4(3(2(x'))))))))))))))),2(0(2(3(4(2(4(4(4(0(2(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N93 <2(0(5(3(0(2(1(2(1(4(4(4(3(4(4(x'))))))))))))))),2(5(3(5(1(4(5(0(0(2(4(5(5(1(3(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N94 <0(2(3(1(5(3(4(0(4(5(2(0(0(4(x')))))))))))))),1(0(1(2(1(3(1(3(1(2(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N95 <0(5(2(2(2(1(2(5(4(3(0(2(5(1(2(1(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(5(2(2(2(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N96 <2(0(5(3(0(4(0(1(4(5(1(5(0(1(x')))))))))))))),2(5(3(5(1(4(5(0(0(2(1(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N97 <1(0(2(5(3(4(0(4(5(2(0(0(4(x'))))))))))))),1(1(2(5(4(1(2(4(3(2(1(5(2(3(0(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N98 <0(5(3(5(3(4(4(1(4(1(4(3(1(0(3(x'))))))))))))))),0(1(3(4(0(1(4(5(1(5(2(4(2(1(1(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N99 <0(2(3(5(4(5(2(4(3(2(5(4(x')))))))))))),0(4(0(1(4(5(1(5(0(1(3(5(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N100 <3(0(0(5(5(2(1(4(0(1(5(4(0(3(2(5(x')))))))))))))))),0(2(4(3(2(3(2(1(0(3(3(2(3(0(5(3(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N101 <1(3(5(4(5(2(4(3(2(5(4(x'))))))))))),1(2(1(2(2(2(5(1(4(2(5(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N102 <2(1(0(4(0(1(4(5(1(5(0(1(5(x))))))))))))),2(5(4(1(3(2(2(5(4(5(x))))))))))> => Not trivial, Not overlay, Proper, NW0, N103 <5(1(5(1(0(0(1(4(5(1(5(5(2(3(0(x'))))))))))))))),4(5(0(0(4(3(1(1(0(4(1(3(1(0(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N104 <2(1(0(2(4(4(1(4(1(4(3(1(0(3(x')))))))))))))),2(5(4(1(3(2(2(5(4(5(2(4(2(1(1(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N105 <0(2(4(4(1(4(1(4(3(1(0(3(x')))))))))))),0(4(0(1(4(5(1(5(0(1(5(2(4(2(1(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N106 <0(5(2(2(2(1(4(2(4(0(2(5(3(3(4(5(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(0(0(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N107 <0(2(1(2(1(2(2(2(5(1(4(2(x')))))))))))),0(4(0(1(4(5(1(5(0(1(1(3(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N108 <3(0(0(5(5(0(1(4(5(1(5(5(2(3(0(x'))))))))))))))),0(2(4(3(2(3(2(1(0(3(3(1(0(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N109 <2(0(0(5(2(2(0(2(5(1(2(4(4(5(5(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(3(4(5(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N110 <2(1(3(1(0(4(0(1(4(5(1(5(0(1(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(2(1(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N111 <2(0(0(5(2(5(3(5(1(4(5(0(0(2(x')))))))))))))),4(0(4(2(1(4(4(4(0(1(5(3(0(2(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N112 <0(5(0(1(4(5(1(5(5(2(3(0(x')))))))))))),2(4(2(5(2(4(3(0(2(4(1(0(x'))))))))))))> => Not trivial, Not overlay, Proper, NW0, N113 <0(5(2(2(2(5(3(5(1(4(5(0(0(2(x')))))))))))))),2(5(4(3(0(2(5(1(2(1(5(3(0(2(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N114 <1(1(0(2(4(3(2(3(2(1(0(3(x')))))))))))),1(2(1(2(2(2(5(1(4(2(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N115 <0(5(2(2(2(1(0(3(2(3(1(4(1(0(1(0(x')))))))))))))))),0(3(2(3(1(4(1(0(1(0(5(2(2(2(1(0(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N116 <2(1(3(1(4(2(4(0(2(5(3(3(4(5(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(0(0(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N117 <2(0(0(5(2(0(1(3(4(0(1(4(5(1(5(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(5(3(5(3(1(5(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N118 <3(1(5(2(3(2(4(2(5(2(4(3(0(2(4(x'))))))))))))))),5(3(4(0(4(5(2(0(0(4(2(1(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N119 <5(1(5(1(0(2(0(2(3(4(2(4(4(4(0(x'))))))))))))))),4(5(0(0(4(3(1(1(0(4(0(2(0(2(1(0(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N120 <0(2(3(1(4(0(1(5(4(0(3(2(5(x'))))))))))))),1(0(1(2(1(3(1(3(1(2(2(3(0(5(3(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N121 <2(0(0(5(2(0(3(2(3(1(4(1(0(1(0(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(5(2(2(2(1(0(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N122 <2(1(3(1(1(0(1(2(1(3(1(3(1(2(x')))))))))))))),0(1(4(5(1(5(5(2(3(0(2(3(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N123 <2(0(0(5(2(1(0(1(2(1(3(1(3(1(2(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(2(3(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N124 <2(0(0(5(2(2(4(2(5(2(4(3(0(2(4(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(5(2(1(3(x'))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N125 <0(2(3(1(0(2(4(3(2(3(2(1(0(3(x')))))))))))))),1(0(1(2(1(3(1(3(1(2(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N126 <0(5(2(1(0(2(4(3(2(3(2(1(0(3(x')))))))))))))),2(4(2(5(2(4(3(0(2(4(0(0(5(5(2(1(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N127 <3(1(5(2(3(0(3(2(3(1(4(1(0(1(0(x'))))))))))))))),5(3(4(0(4(5(2(0(0(4(2(2(2(1(0(x')))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N128 <2(4(5(5(3(5(4(5(2(4(3(2(5(4(x')))))))))))))),2(1(2(1(4(4(4(3(4(4(3(x')))))))))))> => Not trivial, Not overlay, Proper, NW0, N129 <0(5(2(2(2(5(4(1(3(2(2(5(4(5(x')))))))))))))),0(3(2(3(1(4(1(0(1(0(2(1(5(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N130 <0(2(1(1(2(5(4(1(2(4(3(2(x')))))))))))),0(4(0(1(4(5(1(5(0(1(0(2(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N131 <0(0(2(0(2(5(1(2(4(4(5(5(x')))))))))))),4(2(4(0(2(5(3(3(4(5(4(5(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N132 <2(0(0(5(2(4(2(4(0(2(5(3(3(4(5(x'))))))))))))))),4(0(4(2(1(4(4(4(0(1(0(0(3(x')))))))))))))> => Not trivial, Not overlay, Proper, NW0, N133 <2(0(5(3(0(2(0(2(3(4(2(4(4(4(0(x'))))))))))))))),2(5(3(5(1(4(5(0(0(2(0(2(0(2(1(0(x'))))))))))))))))> => Not trivial, Not overlay, Proper, NW0, N134 -> 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: 2(0(0(5(2(0(2(3(4(2(4(4(4(0(x')))))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('2(0(0(5(2(0(2(3(4(2(4(4(4(0(x'))))))))))))))', D0) ID: 1 => ('4(0(4(2(1(4(4(4(0(1(2(3(4(2(4(4(4(0(x'))))))))))))))))))', D1, R15, P[], S{x18 -> 2(3(4(2(4(4(4(0(x'))))))))}), NR: '4(0(4(2(1(4(4(4(0(1(2(3(4(2(4(4(4(0(x'))))))))))))))))))' t: 4(0(4(2(1(4(4(4(0(1(2(0(2(1(0(x'))))))))))))))) Nodes: [0,1] Edges: [(0,1)] ID: 0 => ('4(0(4(2(1(4(4(4(0(1(2(0(2(1(0(x')))))))))))))))', D0) ID: 1 => ('4(0(4(2(1(4(4(4(0(1(2(0(4(0(1(4(5(1(5(0(1(0(x'))))))))))))))))))))))', D1, R2, P[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], S{x5 -> 0(x')}), NR: '0(4(0(1(4(5(1(5(0(1(0(x')))))))))))' 2(0(0(5(2(0(2(3(4(2(4(4(4(0(x')))))))))))))) ->* no union *<- 4(0(4(2(1(4(4(4(0(1(2(0(2(1(0(x'))))))))))))))) "Not joinable" The problem is not confluent.