Input TRS:
    1: \\(x,x) -> e()
    2: /(x,x) -> e()
    3: .(e(),x) -> x
    4: .(x,e()) -> x
    5: \\(e(),x) -> x
    6: /(x,e()) -> x
    7: .(x,\\(x,y)) -> y
    8: .(/(y,x),x) -> y
    9: \\(x,.(x,y)) -> y
    10: /(.(y,x),x) -> y
    11: /(x,\\(y,x)) -> y
    12: \\(/(x,y),x) -> y
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 4 8 1 3 5 10 7 12 11 9 6 2
     /(x1,x2)	weight: (/ 80649 4) + x1 + 2 * x2
     \\(x1,x2)	weight: (/ 35421 4) + x1 + 2 * x2
     .(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
     e()	weight: 0
Number of strict rules: 0
YES