%------------------------------------------------------------------------------
NAME            Unknown

MODE            PROOF

SORTS           ANY

SIGNATURE       a: -> ANY
                asoc: ANY ANY ANY -> ANY
                b: -> ANY
                c: -> ANY
                d: -> ANY
                e: -> ANY
                i: ANY -> ANY
                mult: ANY ANY -> ANY
                op_l: ANY ANY ANY -> ANY
                op_r: ANY ANY ANY -> ANY
                op_t: ANY ANY -> ANY
                rd: ANY ANY -> ANY
                unit: -> ANY

ORDERING        KBO
                i=1, mult=1, op_t=1, rd=1, asoc=1, op_l=1, op_r=1, unit=1, e=1, d=1, c=1, b=1, a=1
                i > rd > mult > op_t > asoc > op_l > op_r > unit > e > d > c > b > a

VARIABLES       E,D,C,B,A: ANY

EQUATIONS       mult(unit, A) = A   % sos
                mult(A, unit) = A   % sos
                mult(A, i(A)) = unit   % sos
                mult(i(A), A) = unit   % sos
                i(mult(A, B)) = mult(i(A), i(B))   % sos
                mult(i(A), mult(A, B)) = B   % sos
                rd(mult(A, B), B) = A   % sos
                mult(rd(A, B), B) = A   % sos
                mult(mult(A, mult(B, A)), C) = mult(A, mult(B, mult(A, C)))   % sos
                mult(mult(A, B), C) = mult(mult(A, mult(B, C)), asoc(A, B, C))   % sos
                op_l(A, B, C) = mult(i(mult(C, B)), mult(C, mult(B, A)))   % sos
                op_r(A, B, C) = rd(mult(mult(A, B), C), mult(B, C))   % sos
                op_t(A, B) = mult(i(B), mult(A, B))   % sos
                op_r(op_r(A, B, C), D, E) = op_r(op_r(A, D, E), B, C)   % sos
                op_l(op_r(A, B, C), D, E) = op_r(op_l(A, D, E), B, C)   % sos
                op_l(op_l(A, B, C), D, E) = op_l(op_l(A, D, E), B, C)   % sos
                op_t(op_r(A, B, C), D) = op_r(op_t(A, D), B, C)   % sos
                op_t(op_l(A, B, C), D) = op_l(op_t(A, D), B, C)   % sos
                op_t(op_t(A, B), C) = op_t(op_t(A, C), B)   % sos

CONCLUSION      asoc(asoc(a, b, c), d, e) = unit   % goals
%------------------------------------------------------------------------------
