MAYBE
Input TRS:
    1: f(x,f(y,z)) -> f(f(x,y),f(x,z))
    2: f(f(x,y),z) -> f(f(x,z),f(y,z))
    3: f(f(x,y),f(y,z)) -> y
Infeasibility test:
    f(a(),a()) --> x
    a() --> x
Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ...failed.