(VAR x1 )
(RULES 
        a12(a12(x1)) -> x1
        a13(a13(x1)) -> x1
        a14(a14(x1)) -> x1
        a15(a15(x1)) -> x1
        a16(a16(x1)) -> x1
        a23(a23(x1)) -> x1
        a24(a24(x1)) -> x1
        a25(a25(x1)) -> x1
        a26(a26(x1)) -> x1
        a34(a34(x1)) -> x1
        a35(a35(x1)) -> x1
        a36(a36(x1)) -> x1
        a45(a45(x1)) -> x1
        a46(a46(x1)) -> x1
        a56(a56(x1)) -> x1
        a13(x1) -> a12(a23(a12(x1)))
        a14(x1) -> a12(a23(a34(a23(a12(x1)))))
        a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
        a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
        a24(x1) -> a23(a34(a23(x1)))
        a25(x1) -> a23(a34(a45(a34(a23(x1)))))
        a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
        a35(x1) -> a34(a45(a34(x1)))
        a36(x1) -> a34(a45(a56(a45(a34(x1)))))
        a46(x1) -> a45(a56(a45(x1)))
        a12(a23(a12(a23(a12(a23(x1)))))) -> x1
        a23(a34(a23(a34(a23(a34(x1)))))) -> x1
        a34(a45(a34(a45(a34(a45(x1)))))) -> x1
        a45(a56(a45(a56(a45(a56(x1)))))) -> x1
        a12(a34(x1)) -> a34(a12(x1))
        a12(a45(x1)) -> a45(a12(x1))
        a12(a56(x1)) -> a56(a12(x1))
        a23(a45(x1)) -> a45(a23(x1))
        a23(a56(x1)) -> a56(a23(x1))
        a34(a56(x1)) -> a56(a34(x1))
        
)