NO Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(b(a(a(b(x))))) -> b(x) b(a(b(a(a(a(b(x))))))) -> b(x) b(a(b(x))) -> b(a(a(a(b(x))))) b(a(a(b(b(x))))) -> b(x) b(a(a(a(b(b(b(x))))))) -> b(b(b(a(a(a(b(x))))))) b(a(a(a(b(a(b(x))))))) -> b(x) b(a(a(a(b(a(a(b(x)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))) b(a(a(a(b(a(a(a(b(x))))))))) -> b(x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Problem 1: Problem 1: Not CS-TRS Procedure: R is not a CS-TRS Problem 1: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR vNonEmpty x) (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(b(a(a(b(x))))) -> b(x) b(a(b(a(a(a(b(x))))))) -> b(x) b(a(b(x))) -> b(a(a(a(b(x))))) b(a(a(b(b(x))))) -> b(x) b(a(a(a(b(b(b(x))))))) -> b(b(b(a(a(a(b(x))))))) b(a(a(a(b(a(b(x))))))) -> b(x) b(a(a(a(b(a(a(b(x)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))) b(a(a(a(b(a(a(a(b(x))))))))) -> b(x) ) ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Huet Levy Ordered by Num of Vars and Symbs Procedure: -> Rules: b(b(a(a(b(x))))) -> b(x) b(a(b(a(a(a(b(x))))))) -> b(x) b(a(b(x))) -> b(a(a(a(b(x))))) b(a(a(b(b(x))))) -> b(x) b(a(a(a(b(b(b(x))))))) -> b(b(b(a(a(a(b(x))))))) b(a(a(a(b(a(b(x))))))) -> b(x) b(a(a(a(b(a(a(b(x)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))) b(a(a(a(b(a(a(a(b(x))))))))) -> b(x) -> Vars: x, x, x, x, x, x, x, x -> Rlps: (rule: b(b(a(a(b(x))))) -> b(x), id: 1, possubterms: b(b(a(a(b(x)))))->[], b(a(a(b(x))))->[1], a(a(b(x)))->[1, 1], a(b(x))->[1, 1, 1], b(x)->[1, 1, 1, 1]) (rule: b(a(b(a(a(a(b(x))))))) -> b(x), id: 2, possubterms: b(a(b(a(a(a(b(x)))))))->[], a(b(a(a(a(b(x))))))->[1], b(a(a(a(b(x)))))->[1, 1], a(a(a(b(x))))->[1, 1, 1], a(a(b(x)))->[1, 1, 1, 1], a(b(x))->[1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1]) (rule: b(a(b(x))) -> b(a(a(a(b(x))))), id: 3, possubterms: b(a(b(x)))->[], a(b(x))->[1], b(x)->[1, 1]) (rule: b(a(a(b(b(x))))) -> b(x), id: 4, possubterms: b(a(a(b(b(x)))))->[], a(a(b(b(x))))->[1], a(b(b(x)))->[1, 1], b(b(x))->[1, 1, 1], b(x)->[1, 1, 1, 1]) (rule: b(a(a(a(b(b(b(x))))))) -> b(b(b(a(a(a(b(x))))))), id: 5, possubterms: b(a(a(a(b(b(b(x)))))))->[], a(a(a(b(b(b(x))))))->[1], a(a(b(b(b(x)))))->[1, 1], a(b(b(b(x))))->[1, 1, 1], b(b(b(x)))->[1, 1, 1, 1], b(b(x))->[1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1]) (rule: b(a(a(a(b(a(b(x))))))) -> b(x), id: 6, possubterms: b(a(a(a(b(a(b(x)))))))->[], a(a(a(b(a(b(x))))))->[1], a(a(b(a(b(x)))))->[1, 1], a(b(a(b(x))))->[1, 1, 1], b(a(b(x)))->[1, 1, 1, 1], a(b(x))->[1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1]) (rule: b(a(a(a(b(a(a(b(x)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), id: 7, possubterms: b(a(a(a(b(a(a(b(x))))))))->[], a(a(a(b(a(a(b(x)))))))->[1], a(a(b(a(a(b(x))))))->[1, 1], a(b(a(a(b(x)))))->[1, 1, 1], b(a(a(b(x))))->[1, 1, 1, 1], a(a(b(x)))->[1, 1, 1, 1, 1], a(b(x))->[1, 1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1, 1]) (rule: b(a(a(a(b(a(a(a(b(x))))))))) -> b(x), id: 8, possubterms: b(a(a(a(b(a(a(a(b(x)))))))))->[], a(a(a(b(a(a(a(b(x))))))))->[1], a(a(b(a(a(a(b(x)))))))->[1, 1], a(b(a(a(a(b(x))))))->[1, 1, 1], b(a(a(a(b(x)))))->[1, 1, 1, 1], a(a(a(b(x))))->[1, 1, 1, 1, 1], a(a(b(x)))->[1, 1, 1, 1, 1, 1], a(b(x))->[1, 1, 1, 1, 1, 1, 1], b(x)->[1, 1, 1, 1, 1, 1, 1, 1]) -> Unifications: (R1 unifies with R4 at p: [1], l: b(b(a(a(b(x))))), lp: b(a(a(b(x)))), sig: {x -> b(x')}, l': b(a(a(b(b(x'))))), r: b(x), r': b(x')) (R1 unifies with R1 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(x), r': b(x')) (R1 unifies with R2 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(x), r': b(x')) (R1 unifies with R3 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(x), r': b(a(a(a(b(x')))))) (R1 unifies with R4 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(x), r': b(x')) (R1 unifies with R5 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(x), r': b(b(b(a(a(a(b(x')))))))) (R1 unifies with R6 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(x), r': b(x')) (R1 unifies with R7 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(x), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R1 unifies with R8 at p: [1,1,1,1], l: b(b(a(a(b(x))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(x), r': b(x')) (R2 unifies with R5 at p: [1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(a(a(a(b(x))))), sig: {x -> b(b(x'))}, l': b(a(a(a(b(b(b(x'))))))), r: b(x), r': b(b(b(a(a(a(b(x')))))))) (R2 unifies with R6 at p: [1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(a(a(a(b(x))))), sig: {x -> a(b(x'))}, l': b(a(a(a(b(a(b(x'))))))), r: b(x), r': b(x')) (R2 unifies with R7 at p: [1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(a(a(a(b(x))))), sig: {x -> a(a(b(x')))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(x), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R2 unifies with R8 at p: [1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(a(a(a(b(x))))), sig: {x -> a(a(a(b(x'))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(x), r': b(x')) (R2 unifies with R1 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(x), r': b(x')) (R2 unifies with R2 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(x), r': b(x')) (R2 unifies with R3 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(x), r': b(a(a(a(b(x')))))) (R2 unifies with R4 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(x), r': b(x')) (R2 unifies with R5 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(x), r': b(b(b(a(a(a(b(x')))))))) (R2 unifies with R6 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(x), r': b(x')) (R2 unifies with R7 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(x), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R2 unifies with R8 at p: [1,1,1,1,1,1], l: b(a(b(a(a(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(x), r': b(x')) (R3 unifies with R2 at p: [], l: b(a(b(x))), lp: b(a(b(x))), sig: {x -> a(a(a(b(x'))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(a(a(a(b(x))))), r': b(x')) (R3 unifies with R1 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(a(a(a(b(x))))), r': b(x')) (R3 unifies with R2 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(a(a(a(b(x))))), r': b(x')) (R3 unifies with R3 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(a(a(a(b(x))))), r': b(a(a(a(b(x')))))) (R3 unifies with R4 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(a(a(a(b(x))))), r': b(x')) (R3 unifies with R5 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(a(a(a(b(x))))), r': b(b(b(a(a(a(b(x')))))))) (R3 unifies with R6 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(a(a(a(b(x))))), r': b(x')) (R3 unifies with R7 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(a(a(a(b(x))))), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R3 unifies with R8 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(a(a(a(b(x))))), r': b(x')) (R4 unifies with R1 at p: [1,1,1], l: b(a(a(b(b(x))))), lp: b(b(x)), sig: {x -> a(a(b(x')))}, l': b(b(a(a(b(x'))))), r: b(x), r': b(x')) (R4 unifies with R1 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(x), r': b(x')) (R4 unifies with R2 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(x), r': b(x')) (R4 unifies with R3 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(x), r': b(a(a(a(b(x')))))) (R4 unifies with R4 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(x), r': b(x')) (R4 unifies with R5 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(x), r': b(b(b(a(a(a(b(x')))))))) (R4 unifies with R6 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(x), r': b(x')) (R4 unifies with R7 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(x), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R4 unifies with R8 at p: [1,1,1,1], l: b(a(a(b(b(x))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(x), r': b(x')) (R5 unifies with R1 at p: [1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(b(x)), sig: {x -> a(a(b(x')))}, l': b(b(a(a(b(x'))))), r: b(b(b(a(a(a(b(x))))))), r': b(x')) (R5 unifies with R1 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(b(b(a(a(a(b(x))))))), r': b(x')) (R5 unifies with R2 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(b(b(a(a(a(b(x))))))), r': b(x')) (R5 unifies with R3 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(b(b(a(a(a(b(x))))))), r': b(a(a(a(b(x')))))) (R5 unifies with R4 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(b(b(a(a(a(b(x))))))), r': b(x')) (R5 unifies with R5 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(b(b(a(a(a(b(x))))))), r': b(b(b(a(a(a(b(x')))))))) (R5 unifies with R6 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(b(b(a(a(a(b(x))))))), r': b(x')) (R5 unifies with R7 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(b(b(a(a(a(b(x))))))), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R5 unifies with R8 at p: [1,1,1,1,1,1], l: b(a(a(a(b(b(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(b(b(a(a(a(b(x))))))), r': b(x')) (R6 unifies with R2 at p: [1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(a(b(x))), sig: {x -> a(a(a(b(x'))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(x), r': b(x')) (R6 unifies with R3 at p: [1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(a(b(x))), sig: {x -> x'}, l': b(a(b(x'))), r: b(x), r': b(a(a(a(b(x')))))) (R6 unifies with R1 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(x), r': b(x')) (R6 unifies with R2 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(x), r': b(x')) (R6 unifies with R3 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(x), r': b(a(a(a(b(x')))))) (R6 unifies with R4 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(x), r': b(x')) (R6 unifies with R5 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(x), r': b(b(b(a(a(a(b(x')))))))) (R6 unifies with R6 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(x), r': b(x')) (R6 unifies with R7 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(x), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R6 unifies with R8 at p: [1,1,1,1,1,1], l: b(a(a(a(b(a(b(x))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(x), r': b(x')) (R7 unifies with R4 at p: [1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(a(a(b(x)))), sig: {x -> b(x')}, l': b(a(a(b(b(x'))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(x')) (R7 unifies with R1 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(x')) (R7 unifies with R2 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(x')) (R7 unifies with R3 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(a(a(a(b(x')))))) (R7 unifies with R4 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(x')) (R7 unifies with R5 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(b(b(a(a(a(b(x')))))))) (R7 unifies with R6 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(x')) (R7 unifies with R7 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R7 unifies with R8 at p: [1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(b(x)))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))), r': b(x')) (R8 unifies with R5 at p: [1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(a(a(a(b(x))))), sig: {x -> b(b(x'))}, l': b(a(a(a(b(b(b(x'))))))), r: b(x), r': b(b(b(a(a(a(b(x')))))))) (R8 unifies with R6 at p: [1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(a(a(a(b(x))))), sig: {x -> a(b(x'))}, l': b(a(a(a(b(a(b(x'))))))), r: b(x), r': b(x')) (R8 unifies with R7 at p: [1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(a(a(a(b(x))))), sig: {x -> a(a(b(x')))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(x), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R8 unifies with R8 at p: [1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(a(a(a(b(x))))), sig: {x -> a(a(a(b(x'))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(x), r': b(x')) (R8 unifies with R1 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> b(a(a(b(x'))))}, l': b(b(a(a(b(x'))))), r: b(x), r': b(x')) (R8 unifies with R2 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(b(a(a(a(b(x'))))))}, l': b(a(b(a(a(a(b(x'))))))), r: b(x), r': b(x')) (R8 unifies with R3 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: b(x), r': b(a(a(a(b(x')))))) (R8 unifies with R4 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(b(b(x'))))}, l': b(a(a(b(b(x'))))), r: b(x), r': b(x')) (R8 unifies with R5 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(a(b(b(b(x'))))))}, l': b(a(a(a(b(b(b(x'))))))), r: b(x), r': b(b(b(a(a(a(b(x')))))))) (R8 unifies with R6 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(a(b(a(b(x'))))))}, l': b(a(a(a(b(a(b(x'))))))), r: b(x), r': b(x')) (R8 unifies with R7 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(b(x')))))))}, l': b(a(a(a(b(a(a(b(x')))))))), r: b(x), r': b(a(a(b(a(a(b(a(a(a(b(b(x'))))))))))))) (R8 unifies with R8 at p: [1,1,1,1,1,1,1,1], l: b(a(a(a(b(a(a(a(b(x))))))))), lp: b(x), sig: {x -> a(a(a(b(a(a(a(b(x'))))))))}, l': b(a(a(a(b(a(a(a(b(x'))))))))), r: b(x), r': b(x')) -> Critical pairs info: => Trivial, Not overlay, Proper, NW0, N1 => Not trivial, Not overlay, Proper, NW0, N2 => Not trivial, Not overlay, Proper, NW0, N3 => Not trivial, Overlay, Proper, NW0, N4 => Not trivial, Not overlay, Proper, NW0, N5 => Not trivial, Not overlay, Proper, NW0, N6 => Not trivial, Not overlay, Proper, NW0, N7 => Trivial, Not overlay, Proper, NW0, N8 => Not trivial, Not overlay, Proper, NW0, N9 => Not trivial, Not overlay, Proper, NW0, N10 => Not trivial, Not overlay, Proper, NW0, N11 => Not trivial, Not overlay, Proper, NW0, N12 => Not trivial, Not overlay, Proper, NW0, N13 => Not trivial, Not overlay, Proper, NW0, N14 => Not trivial, Not overlay, Proper, NW0, N15 => Not trivial, Not overlay, Proper, NW0, N16 => Not trivial, Not overlay, Proper, NW0, N17 => Not trivial, Not overlay, Proper, NW0, N18 => Not trivial, Not overlay, Proper, NW0, N19 => Not trivial, Not overlay, Proper, NW0, N20 => Not trivial, Not overlay, Proper, NW0, N21 => Not trivial, Not overlay, Proper, NW0, N22 => Not trivial, Not overlay, Proper, NW0, N23 => Not trivial, Not overlay, Proper, NW0, N24 => Not trivial, Not overlay, Proper, NW0, N25 => Trivial, Not overlay, Proper, NW0, N26 => Not trivial, Not overlay, Proper, NW0, N27 => Not trivial, Not overlay, Proper, NW0, N28 => Trivial, Not overlay, Proper, NW0, N29 => Not trivial, Not overlay, Proper, NW0, N30 => Not trivial, Not overlay, Proper, NW0, N31 => Not trivial, Not overlay, Proper, NW0, N32 => Not trivial, Not overlay, Proper, NW0, N33 => Trivial, Not overlay, Proper, NW0, N34 => Not trivial, Not overlay, Proper, NW0, N35 => Not trivial, Not overlay, Proper, NW0, N36 => Not trivial, Not overlay, Proper, NW0, N37 => Not trivial, Not overlay, Proper, NW0, N38 => Not trivial, Not overlay, Proper, NW0, N39 => Not trivial, Not overlay, Proper, NW0, N40 => Not trivial, Not overlay, Proper, NW0, N41 => Not trivial, Not overlay, Proper, NW0, N42 => Not trivial, Not overlay, Proper, NW0, N43 => Not trivial, Not overlay, Proper, NW0, N44 => Not trivial, Not overlay, Proper, NW0, N45 => Not trivial, Not overlay, Proper, NW0, N46 => Not trivial, Not overlay, Proper, NW0, N47 => Not trivial, Not overlay, Proper, NW0, N48 => Not trivial, Not overlay, Proper, NW0, N49 => Not trivial, Not overlay, Proper, NW0, N50 => Trivial, Not overlay, Proper, NW0, N51 => Not trivial, Not overlay, Proper, NW0, N52 => Not trivial, Not overlay, Proper, NW0, N53 => Trivial, Not overlay, Proper, NW0, N54 => Not trivial, Not overlay, Proper, NW0, N55 => Not trivial, Not overlay, Proper, NW0, N56 => Not trivial, Not overlay, Proper, NW0, N57 => Not trivial, Not overlay, Proper, NW0, N58 => Not trivial, Not overlay, Proper, NW0, N59 => Not trivial, Not overlay, Proper, NW0, N60 => Not trivial, Not overlay, Proper, NW0, N61 => Not trivial, Not overlay, Proper, NW0, N62 => Trivial, Not overlay, Proper, NW0, N63 => Not trivial, Not overlay, Proper, NW0, N64 => Not trivial, Not overlay, Proper, NW0, N65 => Not trivial, Not overlay, Proper, NW0, N66 => Not trivial, Not overlay, Proper, NW0, N67 => Trivial, Not overlay, Proper, NW0, N68 => Not trivial, Not overlay, Proper, NW0, N69 => Not trivial, Not overlay, Proper, NW0, N70 => Not trivial, Not overlay, Proper, NW0, N71 => Not trivial, Not overlay, Proper, NW0, N72 => Not trivial, Not overlay, Proper, NW0, N73 => Not trivial, Not overlay, Proper, NW0, N74 => Not trivial, Not overlay, Proper, NW0, N75 => Not trivial, Not overlay, Proper, NW0, N76 => Not trivial, Not overlay, Proper, NW0, N77 => Trivial, Not overlay, Proper, NW0, N78 => Not trivial, Not overlay, Proper, NW0, N79 -> 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: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Confluence Problem: (VAR x x') (REPLACEMENT-MAP (b 1) (a 1) (fSNonEmpty) ) (RULES b(b(a(a(b(x))))) -> b(x) b(a(b(a(a(a(b(x))))))) -> b(x) b(a(b(x))) -> b(a(a(a(b(x))))) b(a(a(b(b(x))))) -> b(x) b(a(a(a(b(b(b(x))))))) -> b(b(b(a(a(a(b(x))))))) b(a(a(a(b(a(b(x))))))) -> b(x) b(a(a(a(b(a(a(b(x)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))) b(a(a(a(b(a(a(a(b(x))))))))) -> b(x) ) Critical Pairs: => Not trivial, Not overlay, Proper, NW0, N45 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: No Convergence InfChecker Procedure: Infeasible convergence? YES Problem 1: Infeasibility Problem: [(VAR vNonEmpty x x1 vNonEmpty z0) (STRATEGY CONTEXTSENSITIVE (b 1) (a 1) (c_x1) (fSNonEmpty) ) (RULES b(b(a(a(b(x))))) -> b(x) b(a(b(a(a(a(b(x))))))) -> b(x) b(a(b(x))) -> b(a(a(a(b(x))))) b(a(a(b(b(x))))) -> b(x) b(a(a(a(b(b(b(x))))))) -> b(b(b(a(a(a(b(x))))))) b(a(a(a(b(a(b(x))))))) -> b(x) b(a(a(a(b(a(a(b(x)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))) b(a(a(a(b(a(a(a(b(x))))))))) -> b(x) )] Infeasibility Conditions: b(a(b(a(a(b(a(a(b(a(a(a(b(b(c_x1)))))))))))))) ->* z0, b(a(a(a(b(a(a(a(b(a(a(b(c_x1)))))))))))) ->* z0 Problem 1: Obtaining a model using AGES: -> Theory (Usable Rules): b(b(a(a(b(x))))) -> b(x) b(a(b(a(a(a(b(x))))))) -> b(x) b(a(b(x))) -> b(a(a(a(b(x))))) b(a(a(b(b(x))))) -> b(x) b(a(a(a(b(b(b(x))))))) -> b(b(b(a(a(a(b(x))))))) b(a(a(a(b(a(b(x))))))) -> b(x) b(a(a(a(b(a(a(b(x)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x)))))))))))) b(a(a(a(b(a(a(a(b(x))))))))) -> b(x) -> AGES Output: The problem is infeasible. The problem is not confluent.