Vampire---5.0.1.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : GRP689-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n017.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 10:15:37 AM UTC 2026

% Result   : Unsatisfiable 51.24s 8.19s
% Output   : Refutation 51.74s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
    ! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).

fof(f2,negated_conjecture,
    ! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).

fof(f3,negated_conjecture,
    ! [X0,X1] : mult(rd(X0,X1),X1) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).

fof(f4,negated_conjecture,
    ! [X0,X1] : rd(mult(X0,X1),X1) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).

fof(f5,negated_conjecture,
    ! [X0] : mult(X0,unit) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).

fof(f6,negated_conjecture,
    ! [X0] : mult(unit,X0) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).

fof(f7,axiom,
    ! [X2,X0,X1] : mult(X0,mult(X1,mult(X0,X2))) = mult(mult(X0,mult(X1,X0)),X2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).

fof(f8,negated_conjecture,
    ! [X0,X1] : mult(i(X0),mult(X0,X1)) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).

fof(f9,negated_conjecture,
    ! [X0,X1] : i(mult(X0,X1)) = mult(i(X0),i(X1)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c09) ).

fof(f10,axiom,
    mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).

fof(f11,plain,
    unit = mult(op_c,mult(op_c,mult(op_c,op_c))),
    inference(reorient_equations,[],[f10]) ).

fof(f12,axiom,
    mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,op_d)))))))) = unit,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).

fof(f13,plain,
    unit = mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,mult(op_d,op_d)))))))),
    inference(reorient_equations,[],[f12]) ).

fof(f14,negated_conjecture,
    mult(op_c,op_d) != mult(op_d,op_c),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).

fof(f15,definition,
    sF0 = mult(op_c,op_c),
    introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).

fof(f16,plain,
    mult(op_c,op_c) = sF0,
    inference(reorient_equations,[],[f15]) ).

fof(f17,definition,
    sF1 = mult(op_c,sF0),
    introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).

fof(f18,plain,
    mult(op_c,sF0) = sF1,
    inference(reorient_equations,[],[f17]) ).

fof(f19,definition,
    sF2 = mult(op_c,sF1),
    introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).

fof(f20,plain,
    mult(op_c,sF1) = sF2,
    inference(reorient_equations,[],[f19]) ).

fof(f21,plain,
    unit = sF2,
    inference(definition_folding,[],[f11,f20,f18,f16]) ).

fof(f22,definition,
    sF3 = mult(op_d,op_d),
    introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).

fof(f23,plain,
    mult(op_d,op_d) = sF3,
    inference(reorient_equations,[],[f22]) ).

fof(f24,definition,
    sF4 = mult(op_d,sF3),
    introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).

fof(f25,plain,
    mult(op_d,sF3) = sF4,
    inference(reorient_equations,[],[f24]) ).

fof(f26,definition,
    sF5 = mult(op_d,sF4),
    introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).

fof(f27,plain,
    mult(op_d,sF4) = sF5,
    inference(reorient_equations,[],[f26]) ).

fof(f28,definition,
    sF6 = mult(op_d,sF5),
    introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).

fof(f29,plain,
    mult(op_d,sF5) = sF6,
    inference(reorient_equations,[],[f28]) ).

fof(f30,definition,
    sF7 = mult(op_d,sF6),
    introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).

fof(f31,plain,
    mult(op_d,sF6) = sF7,
    inference(reorient_equations,[],[f30]) ).

fof(f32,definition,
    sF8 = mult(op_d,sF7),
    introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).

fof(f33,plain,
    mult(op_d,sF7) = sF8,
    inference(reorient_equations,[],[f32]) ).

fof(f34,definition,
    sF9 = mult(op_d,sF8),
    introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).

fof(f35,plain,
    mult(op_d,sF8) = sF9,
    inference(reorient_equations,[],[f34]) ).

fof(f36,definition,
    sF10 = mult(op_d,sF9),
    introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).

fof(f37,plain,
    mult(op_d,sF9) = sF10,
    inference(reorient_equations,[],[f36]) ).

fof(f38,plain,
    unit = sF10,
    inference(definition_folding,[],[f13,f37,f35,f33,f31,f29,f27,f25,f23]) ).

fof(f39,definition,
    sF11 = mult(op_c,op_d),
    introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).

fof(f40,plain,
    mult(op_c,op_d) = sF11,
    inference(reorient_equations,[],[f39]) ).

fof(f41,definition,
    sF12 = mult(op_d,op_c),
    introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).

fof(f42,plain,
    mult(op_d,op_c) = sF12,
    inference(reorient_equations,[],[f41]) ).

fof(f43,plain,
    sF11 != sF12,
    inference(definition_folding,[],[f14,f42,f40]) ).

fof(f44,plain,
    unit = mult(op_c,sF1),
    inference(forward_demodulation,[],[f20,f21]) ).

fof(f45,plain,
    unit = mult(op_d,sF9),
    inference(forward_demodulation,[],[f37,f38]) ).

fof(f46,plain,
    ! [X2,X3,X0,X1] : mult(X2,mult(mult(X0,mult(X1,X0)),mult(X2,X3))) = mult(mult(X2,mult(X0,mult(X1,mult(X0,X2)))),X3),
    inference(superposition,[],[f7,f7]) ).

fof(f49,plain,
    ! [X2,X3,X0,X1] : mult(mult(X2,mult(X0,mult(X1,mult(X0,X2)))),X3) = mult(X2,mult(X0,mult(X1,mult(X0,mult(X2,X3))))),
    inference(forward_demodulation,[],[f46,f7]) ).

fof(f51,plain,
    ! [X0] : mult(op_d,mult(op_c,mult(op_d,X0))) = mult(mult(op_d,sF11),X0),
    inference(superposition,[],[f7,f40]) ).

fof(f52,plain,
    ! [X0] : mult(op_c,mult(op_d,mult(op_c,X0))) = mult(mult(op_c,sF12),X0),
    inference(superposition,[],[f7,f42]) ).

fof(f58,plain,
    op_c = ld(op_d,sF12),
    inference(superposition,[],[f2,f42]) ).

fof(f60,plain,
    ! [X0] : mult(op_c,mult(op_c,mult(op_c,X0))) = mult(mult(op_c,sF0),X0),
    inference(superposition,[],[f7,f16]) ).

fof(f61,plain,
    ! [X0] : mult(op_c,mult(op_c,mult(op_c,X0))) = mult(sF1,X0),
    inference(forward_demodulation,[],[f60,f18]) ).

fof(f62,plain,
    op_d = ld(op_d,sF3),
    inference(superposition,[],[f2,f23]) ).

fof(f63,plain,
    ! [X0] : mult(op_d,mult(op_d,mult(op_d,X0))) = mult(mult(op_d,sF3),X0),
    inference(superposition,[],[f7,f23]) ).

fof(f64,plain,
    ! [X0] : mult(op_d,mult(op_d,mult(op_d,X0))) = mult(sF4,X0),
    inference(forward_demodulation,[],[f63,f25]) ).

fof(f65,plain,
    sF8 = ld(op_d,sF9),
    inference(superposition,[],[f2,f35]) ).

fof(f68,plain,
    ! [X0] : mult(sF0,mult(op_c,mult(sF0,X0))) = mult(mult(sF0,sF1),X0),
    inference(superposition,[],[f7,f18]) ).

fof(f69,plain,
    sF4 = ld(op_d,sF5),
    inference(superposition,[],[f2,f27]) ).

fof(f70,plain,
    ! [X0] : mult(sF4,mult(op_d,mult(sF4,X0))) = mult(mult(sF4,sF5),X0),
    inference(superposition,[],[f7,f27]) ).

fof(f71,plain,
    sF3 = ld(op_d,sF4),
    inference(superposition,[],[f2,f25]) ).

fof(f73,plain,
    sF5 = ld(op_d,sF6),
    inference(superposition,[],[f2,f29]) ).

fof(f74,plain,
    ! [X0] : mult(sF5,mult(op_d,mult(sF5,X0))) = mult(mult(sF5,sF6),X0),
    inference(superposition,[],[f7,f29]) ).

fof(f75,plain,
    sF7 = ld(op_d,sF8),
    inference(superposition,[],[f2,f33]) ).

fof(f77,plain,
    sF6 = ld(op_d,sF7),
    inference(superposition,[],[f2,f31]) ).

fof(f78,plain,
    ! [X0] : mult(sF6,mult(op_d,mult(sF6,X0))) = mult(mult(sF6,sF7),X0),
    inference(superposition,[],[f7,f31]) ).

fof(f80,plain,
    ! [X0] : unit = ld(X0,X0),
    inference(superposition,[],[f2,f5]) ).

fof(f87,plain,
    ! [X0,X1] : mult(X0,mult(unit,mult(X0,X1))) = mult(mult(X0,X0),X1),
    inference(superposition,[],[f7,f6]) ).

fof(f91,plain,
    ! [X0,X1] : mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1)),
    inference(forward_demodulation,[],[f87,f6]) ).

fof(f95,plain,
    ! [X2,X0,X1] : mult(X1,mult(rd(X0,X1),mult(X1,X2))) = mult(mult(X1,X0),X2),
    inference(superposition,[],[f7,f3]) ).

fof(f97,plain,
    ! [X0,X1] : ld(X1,X0) = mult(i(X1),X0),
    inference(superposition,[],[f8,f1]) ).

fof(f115,plain,
    ! [X0,X1] : mult(X1,X0) = ld(i(X1),X0),
    inference(superposition,[],[f2,f8]) ).

fof(f117,plain,
    ! [X0,X1] : i(mult(X0,X1)) = ld(X0,i(X1)),
    inference(backward_demodulation,[],[f9,f97]) ).

fof(f136,plain,
    sF9 = ld(op_d,unit),
    inference(superposition,[],[f2,f45]) ).

fof(f139,plain,
    ! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
    inference(superposition,[],[f4,f1]) ).

fof(f141,plain,
    ! [X2,X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,mult(X1,mult(X0,X2))),X2),
    inference(superposition,[],[f4,f7]) ).

fof(f142,plain,
    ! [X0] : unit = rd(X0,X0),
    inference(superposition,[],[f4,f6]) ).

fof(f157,plain,
    ! [X0] : mult(sF1,mult(op_c,mult(sF1,X0))) = mult(mult(sF1,unit),X0),
    inference(superposition,[],[f7,f44]) ).

fof(f158,plain,
    ! [X0] : mult(sF1,X0) = mult(sF1,mult(op_c,mult(sF1,X0))),
    inference(forward_demodulation,[],[f157,f5]) ).

fof(f169,plain,
    ! [X0] : mult(op_d,mult(op_d,X0)) = mult(sF4,ld(op_d,X0)),
    inference(superposition,[],[f64,f1]) ).

fof(f171,plain,
    ! [X0] : mult(op_d,mult(sF4,X0)) = mult(sF4,mult(op_d,X0)),
    inference(superposition,[],[f64,f64]) ).

fof(f173,plain,
    ! [X0] : mult(op_d,mult(op_d,X0)) = ld(op_d,mult(sF4,X0)),
    inference(superposition,[],[f2,f64]) ).

fof(f175,plain,
    ! [X0] : mult(mult(sF4,sF5),X0) = mult(sF4,mult(sF4,mult(op_d,X0))),
    inference(backward_demodulation,[],[f70,f171]) ).

fof(f179,plain,
    ! [X0] : mult(sF4,ld(op_d,X0)) = ld(op_d,mult(sF4,X0)),
    inference(backward_demodulation,[],[f173,f169]) ).

fof(f194,plain,
    ! [X0,X1] : i(X1) = mult(X0,i(mult(X0,X1))),
    inference(superposition,[],[f1,f117]) ).

fof(f195,plain,
    ! [X0,X1] : i(ld(X1,X0)) = mult(X1,i(X0)),
    inference(superposition,[],[f194,f1]) ).

fof(f196,plain,
    ! [X0] : i(unit) = mult(X0,i(X0)),
    inference(superposition,[],[f194,f5]) ).

fof(f199,plain,
    ! [X0,X1] : i(X1) = mult(rd(X0,X1),i(X0)),
    inference(superposition,[],[f194,f3]) ).

fof(f203,plain,
    i(sF0) = mult(op_c,i(sF1)),
    inference(superposition,[],[f194,f18]) ).

fof(f205,plain,
    i(op_c) = mult(op_d,i(sF12)),
    inference(superposition,[],[f194,f42]) ).

fof(f240,plain,
    ! [X0] : mult(op_c,mult(op_c,X0)) = mult(sF1,ld(op_c,X0)),
    inference(superposition,[],[f61,f1]) ).

fof(f243,plain,
    ! [X0] : mult(op_c,mult(sF1,X0)) = mult(sF1,mult(op_c,X0)),
    inference(superposition,[],[f61,f61]) ).

fof(f246,plain,
    ! [X0] : mult(op_c,mult(op_c,X0)) = ld(op_c,mult(sF1,X0)),
    inference(superposition,[],[f2,f61]) ).

fof(f248,plain,
    ! [X0] : mult(sF1,X0) = mult(sF1,mult(sF1,mult(op_c,X0))),
    inference(backward_demodulation,[],[f158,f243]) ).

fof(f253,plain,
    ! [X0] : mult(sF1,ld(op_c,X0)) = ld(op_c,mult(sF1,X0)),
    inference(backward_demodulation,[],[f246,f240]) ).

fof(f265,plain,
    ! [X0] : ld(op_c,X0) = mult(sF1,ld(op_c,ld(sF1,X0))),
    inference(superposition,[],[f253,f1]) ).

fof(f291,plain,
    ! [X0] : ld(op_d,X0) = mult(sF4,ld(op_d,ld(sF4,X0))),
    inference(superposition,[],[f179,f1]) ).

fof(f292,plain,
    ld(op_d,sF4) = mult(sF4,ld(op_d,unit)),
    inference(superposition,[],[f179,f5]) ).

fof(f297,plain,
    ld(op_d,sF4) = mult(sF4,sF9),
    inference(forward_demodulation,[],[f292,f136]) ).

fof(f299,plain,
    sF3 = mult(sF4,sF9),
    inference(forward_demodulation,[],[f297,f71]) ).

fof(f301,plain,
    ld(op_d,sF3) = mult(sF4,ld(op_d,sF9)),
    inference(superposition,[],[f179,f299]) ).

fof(f305,plain,
    ! [X0] : mult(sF9,mult(sF4,mult(sF9,X0))) = mult(mult(sF9,sF3),X0),
    inference(superposition,[],[f7,f299]) ).

fof(f306,plain,
    ld(op_d,sF3) = mult(sF4,sF8),
    inference(forward_demodulation,[],[f301,f65]) ).

fof(f307,plain,
    op_d = mult(sF4,sF8),
    inference(forward_demodulation,[],[f306,f62]) ).

fof(f308,plain,
    mult(sF4,ld(op_d,sF8)) = ld(op_d,op_d),
    inference(superposition,[],[f179,f307]) ).

fof(f313,plain,
    unit = mult(sF4,ld(op_d,sF8)),
    inference(forward_demodulation,[],[f308,f80]) ).

fof(f314,plain,
    unit = mult(sF4,sF7),
    inference(forward_demodulation,[],[f313,f75]) ).

fof(f320,plain,
    ! [X0] : mult(sF1,ld(op_c,X0)) = mult(sF1,mult(sF1,X0)),
    inference(superposition,[],[f248,f1]) ).

fof(f326,plain,
    ! [X0] : mult(sF1,mult(op_c,X0)) = ld(sF1,mult(sF1,X0)),
    inference(superposition,[],[f2,f248]) ).

fof(f328,plain,
    ! [X0] : mult(sF1,mult(op_c,X0)) = X0,
    inference(forward_demodulation,[],[f326,f2]) ).

fof(f335,plain,
    ! [X0] : mult(op_c,mult(op_c,X0)) = mult(sF1,mult(sF1,X0)),
    inference(backward_demodulation,[],[f240,f320]) ).

fof(f336,plain,
    ! [X0] : ld(op_c,X0) = mult(sF1,mult(sF1,ld(sF1,X0))),
    inference(backward_demodulation,[],[f265,f320]) ).

fof(f339,plain,
    ! [X0] : mult(op_c,mult(sF1,X0)) = X0,
    inference(backward_demodulation,[],[f243,f328]) ).

fof(f341,plain,
    ! [X0] : mult(sF1,X0) = ld(op_c,X0),
    inference(forward_demodulation,[],[f336,f1]) ).

fof(f358,plain,
    ! [X0] : op_c = rd(X0,mult(sF1,X0)),
    inference(superposition,[],[f139,f341]) ).

fof(f365,plain,
    ! [X0] : mult(op_c,X0) = ld(sF1,X0),
    inference(superposition,[],[f339,f1]) ).

fof(f377,plain,
    ! [X0] : sF1 = rd(X0,mult(op_c,X0)),
    inference(superposition,[],[f139,f365]) ).

fof(f381,plain,
    ld(op_d,unit) = mult(sF4,ld(op_d,sF7)),
    inference(superposition,[],[f179,f314]) ).

fof(f387,plain,
    ld(op_d,unit) = mult(sF4,sF6),
    inference(forward_demodulation,[],[f381,f77]) ).

fof(f388,plain,
    sF9 = mult(sF4,sF6),
    inference(forward_demodulation,[],[f387,f136]) ).

fof(f389,plain,
    ld(op_d,sF9) = mult(sF4,ld(op_d,sF6)),
    inference(superposition,[],[f179,f388]) ).

fof(f394,plain,
    ld(op_d,sF9) = mult(sF4,sF5),
    inference(forward_demodulation,[],[f389,f73]) ).

fof(f395,plain,
    sF8 = mult(sF4,sF5),
    inference(forward_demodulation,[],[f394,f65]) ).

fof(f396,plain,
    ! [X0] : mult(sF8,X0) = mult(sF4,mult(sF4,mult(op_d,X0))),
    inference(backward_demodulation,[],[f175,f395]) ).

fof(f397,plain,
    ld(op_d,sF8) = mult(sF4,ld(op_d,sF5)),
    inference(superposition,[],[f179,f395]) ).

fof(f401,plain,
    ! [X0] : mult(sF5,mult(sF4,mult(sF5,X0))) = mult(mult(sF5,sF8),X0),
    inference(superposition,[],[f7,f395]) ).

fof(f402,plain,
    ld(op_d,sF8) = mult(sF4,sF4),
    inference(forward_demodulation,[],[f397,f69]) ).

fof(f403,plain,
    sF7 = mult(sF4,sF4),
    inference(forward_demodulation,[],[f402,f75]) ).

fof(f404,plain,
    ld(op_d,sF7) = mult(sF4,ld(op_d,sF4)),
    inference(superposition,[],[f179,f403]) ).

fof(f408,plain,
    ! [X0] : mult(sF4,mult(sF4,mult(sF4,X0))) = mult(mult(sF4,sF7),X0),
    inference(superposition,[],[f7,f403]) ).

fof(f409,plain,
    ! [X0] : mult(unit,X0) = mult(sF4,mult(sF4,mult(sF4,X0))),
    inference(forward_demodulation,[],[f408,f314]) ).

fof(f410,plain,
    ld(op_d,sF7) = mult(sF4,sF3),
    inference(forward_demodulation,[],[f404,f71]) ).

fof(f411,plain,
    ! [X0] : mult(sF4,mult(sF4,mult(sF4,X0))) = X0,
    inference(forward_demodulation,[],[f409,f6]) ).

fof(f412,plain,
    sF6 = mult(sF4,sF3),
    inference(forward_demodulation,[],[f410,f77]) ).

fof(f413,plain,
    ld(op_d,sF6) = mult(sF4,ld(op_d,sF3)),
    inference(superposition,[],[f179,f412]) ).

fof(f417,plain,
    ! [X0] : mult(sF3,mult(sF4,mult(sF3,X0))) = mult(mult(sF3,sF6),X0),
    inference(superposition,[],[f7,f412]) ).

fof(f418,plain,
    ld(op_d,sF6) = mult(sF4,op_d),
    inference(forward_demodulation,[],[f413,f62]) ).

fof(f419,plain,
    sF5 = mult(sF4,op_d),
    inference(forward_demodulation,[],[f418,f73]) ).

fof(f424,plain,
    ! [X0] : mult(op_d,mult(sF4,mult(op_d,X0))) = mult(mult(op_d,sF5),X0),
    inference(superposition,[],[f7,f419]) ).

fof(f425,plain,
    ! [X0] : mult(sF6,X0) = mult(op_d,mult(sF4,mult(op_d,X0))),
    inference(forward_demodulation,[],[f424,f29]) ).

fof(f427,plain,
    ! [X0] : mult(sF6,X0) = mult(sF4,mult(op_d,mult(op_d,X0))),
    inference(forward_demodulation,[],[f425,f171]) ).

fof(f429,plain,
    ! [X0] : mult(sF6,X0) = mult(sF4,mult(sF4,ld(op_d,X0))),
    inference(forward_demodulation,[],[f427,f169]) ).

fof(f445,plain,
    ! [X0] : mult(sF6,mult(sF4,X0)) = mult(sF4,mult(sF4,mult(sF4,ld(op_d,X0)))),
    inference(superposition,[],[f429,f179]) ).

fof(f446,plain,
    ! [X0] : mult(sF4,mult(sF4,X0)) = mult(sF6,mult(op_d,X0)),
    inference(superposition,[],[f429,f2]) ).

fof(f449,plain,
    ! [X0] : i(mult(sF4,ld(op_d,X0))) = mult(sF4,i(mult(sF6,X0))),
    inference(superposition,[],[f194,f429]) ).

fof(f451,plain,
    ! [X0] : mult(sF4,ld(op_d,X0)) = ld(sF4,mult(sF6,X0)),
    inference(superposition,[],[f2,f429]) ).

fof(f454,plain,
    ! [X0] : mult(mult(sF6,sF7),X0) = mult(sF4,mult(sF4,mult(sF6,X0))),
    inference(backward_demodulation,[],[f78,f446]) ).

fof(f455,plain,
    ! [X0] : ld(op_d,X0) = mult(sF6,mult(sF4,X0)),
    inference(forward_demodulation,[],[f445,f411]) ).

fof(f459,plain,
    ! [X0] : ld(op_d,mult(sF4,ld(op_d,X0))) = mult(sF6,mult(sF6,X0)),
    inference(superposition,[],[f455,f429]) ).

fof(f460,plain,
    ld(op_d,op_d) = mult(sF6,sF5),
    inference(superposition,[],[f455,f419]) ).

fof(f461,plain,
    ld(op_d,sF3) = mult(sF6,sF6),
    inference(superposition,[],[f455,f412]) ).

fof(f462,plain,
    ld(op_d,sF4) = mult(sF6,sF7),
    inference(superposition,[],[f455,f403]) ).

fof(f463,plain,
    ld(op_d,sF5) = mult(sF6,sF8),
    inference(superposition,[],[f455,f395]) ).

fof(f464,plain,
    ld(op_d,sF6) = mult(sF6,sF9),
    inference(superposition,[],[f455,f388]) ).

fof(f466,plain,
    ld(op_d,sF8) = mult(sF6,op_d),
    inference(superposition,[],[f455,f307]) ).

fof(f467,plain,
    ld(op_d,sF9) = mult(sF6,sF3),
    inference(superposition,[],[f455,f299]) ).

fof(f468,plain,
    ! [X0] : mult(sF6,X0) = ld(op_d,ld(sF4,X0)),
    inference(superposition,[],[f455,f1]) ).

fof(f469,plain,
    ld(op_d,unit) = mult(sF6,sF4),
    inference(superposition,[],[f455,f5]) ).

fof(f471,plain,
    ! [X0] : mult(sF6,mult(sF4,mult(sF6,X0))) = mult(ld(op_d,sF6),X0),
    inference(superposition,[],[f7,f455]) ).

fof(f474,plain,
    ! [X0] : mult(sF4,X0) = ld(sF6,ld(op_d,X0)),
    inference(superposition,[],[f2,f455]) ).

fof(f477,plain,
    ! [X0] : mult(sF5,X0) = mult(sF6,mult(sF4,mult(sF6,X0))),
    inference(forward_demodulation,[],[f471,f73]) ).

fof(f479,plain,
    sF9 = mult(sF6,sF4),
    inference(forward_demodulation,[],[f469,f136]) ).

fof(f480,plain,
    ! [X0] : ld(op_d,X0) = mult(sF4,mult(sF6,X0)),
    inference(backward_demodulation,[],[f291,f468]) ).

fof(f481,plain,
    sF8 = mult(sF6,sF3),
    inference(forward_demodulation,[],[f467,f65]) ).

fof(f482,plain,
    sF7 = mult(sF6,op_d),
    inference(forward_demodulation,[],[f466,f75]) ).

fof(f484,plain,
    sF5 = mult(sF6,sF9),
    inference(forward_demodulation,[],[f464,f73]) ).

fof(f485,plain,
    sF4 = mult(sF6,sF8),
    inference(forward_demodulation,[],[f463,f69]) ).

fof(f486,plain,
    sF3 = mult(sF6,sF7),
    inference(forward_demodulation,[],[f462,f71]) ).

fof(f487,plain,
    op_d = mult(sF6,sF6),
    inference(forward_demodulation,[],[f461,f62]) ).

fof(f488,plain,
    unit = mult(sF6,sF5),
    inference(forward_demodulation,[],[f460,f80]) ).

fof(f489,plain,
    ! [X0] : mult(sF4,ld(op_d,ld(op_d,X0))) = mult(sF6,mult(sF6,X0)),
    inference(forward_demodulation,[],[f459,f179]) ).

fof(f491,plain,
    ! [X0] : mult(sF5,X0) = ld(op_d,mult(sF6,X0)),
    inference(forward_demodulation,[],[f477,f455]) ).

fof(f493,plain,
    ! [X0] : mult(mult(sF6,sF7),X0) = mult(sF4,ld(op_d,X0)),
    inference(backward_demodulation,[],[f454,f480]) ).

fof(f497,plain,
    ! [X0] : mult(sF3,X0) = mult(sF4,ld(op_d,X0)),
    inference(forward_demodulation,[],[f493,f486]) ).

fof(f498,plain,
    ! [X0] : mult(op_d,mult(op_d,X0)) = mult(sF3,X0),
    inference(backward_demodulation,[],[f169,f497]) ).

fof(f500,plain,
    ! [X0] : mult(sF3,X0) = ld(op_d,mult(sF4,X0)),
    inference(backward_demodulation,[],[f179,f497]) ).

fof(f502,plain,
    ! [X0] : mult(sF6,X0) = mult(sF4,mult(sF3,X0)),
    inference(backward_demodulation,[],[f429,f497]) ).

fof(f503,plain,
    ! [X0] : mult(sF4,i(mult(sF6,X0))) = i(mult(sF3,X0)),
    inference(backward_demodulation,[],[f449,f497]) ).

fof(f505,plain,
    ! [X0] : mult(sF3,X0) = ld(sF4,mult(sF6,X0)),
    inference(backward_demodulation,[],[f451,f497]) ).

fof(f507,plain,
    ! [X0] : mult(sF6,mult(sF6,X0)) = mult(sF3,ld(op_d,X0)),
    inference(backward_demodulation,[],[f489,f497]) ).

fof(f508,plain,
    ! [X0] : mult(mult(sF3,sF6),X0) = mult(sF3,mult(sF6,X0)),
    inference(backward_demodulation,[],[f417,f502]) ).

fof(f509,plain,
    ! [X0] : ld(op_d,ld(op_d,X0)) = mult(sF5,mult(sF4,X0)),
    inference(superposition,[],[f491,f455]) ).

fof(f514,plain,
    ! [X0] : mult(op_d,mult(sF5,X0)) = mult(sF6,X0),
    inference(superposition,[],[f1,f491]) ).

fof(f515,plain,
    ! [X0] : mult(mult(sF5,sF6),X0) = mult(sF5,mult(sF6,X0)),
    inference(backward_demodulation,[],[f74,f514]) ).

fof(f518,plain,
    ! [X0] : mult(sF4,mult(sF6,X0)) = ld(sF6,mult(sF5,X0)),
    inference(superposition,[],[f474,f491]) ).

fof(f519,plain,
    ! [X0] : mult(sF4,mult(op_d,X0)) = ld(sF6,X0),
    inference(superposition,[],[f474,f2]) ).

fof(f520,plain,
    ! [X0] : mult(sF4,i(X0)) = ld(sF6,i(mult(op_d,X0))),
    inference(superposition,[],[f474,f117]) ).

fof(f523,plain,
    ! [X0] : mult(sF4,i(X0)) = i(mult(sF6,mult(op_d,X0))),
    inference(forward_demodulation,[],[f520,f117]) ).

fof(f525,plain,
    ! [X0] : mult(sF8,X0) = mult(sF4,ld(sF6,X0)),
    inference(backward_demodulation,[],[f396,f519]) ).

fof(f526,plain,
    ! [X0] : mult(op_d,mult(sF4,X0)) = ld(sF6,X0),
    inference(backward_demodulation,[],[f171,f519]) ).

fof(f527,plain,
    ! [X0] : ld(op_d,X0) = ld(sF6,mult(sF5,X0)),
    inference(forward_demodulation,[],[f518,f480]) ).

fof(f528,plain,
    ! [X0] : mult(sF4,i(X0)) = i(mult(sF4,mult(sF4,X0))),
    inference(forward_demodulation,[],[f523,f446]) ).

fof(f529,plain,
    mult(sF5,sF6) = ld(op_d,op_d),
    inference(superposition,[],[f491,f487]) ).

fof(f533,plain,
    ! [X0] : mult(sF6,mult(sF6,mult(sF6,X0))) = mult(mult(sF6,op_d),X0),
    inference(superposition,[],[f7,f487]) ).

fof(f534,plain,
    ! [X0] : mult(sF7,X0) = mult(sF6,mult(sF6,mult(sF6,X0))),
    inference(forward_demodulation,[],[f533,f482]) ).

fof(f535,plain,
    unit = mult(sF5,sF6),
    inference(forward_demodulation,[],[f529,f80]) ).

fof(f536,plain,
    ! [X0] : mult(sF7,X0) = mult(sF3,ld(op_d,mult(sF6,X0))),
    inference(forward_demodulation,[],[f534,f507]) ).

fof(f537,plain,
    ! [X0] : mult(unit,X0) = mult(sF5,mult(sF6,X0)),
    inference(backward_demodulation,[],[f515,f535]) ).

fof(f538,plain,
    ! [X0] : mult(sF7,X0) = mult(sF3,mult(sF5,X0)),
    inference(forward_demodulation,[],[f536,f491]) ).

fof(f539,plain,
    ! [X0] : mult(sF5,mult(sF6,X0)) = X0,
    inference(forward_demodulation,[],[f537,f6]) ).

fof(f543,plain,
    ld(op_d,sF7) = mult(sF5,op_d),
    inference(superposition,[],[f491,f482]) ).

fof(f546,plain,
    op_d = ld(sF6,sF7),
    inference(superposition,[],[f2,f482]) ).

fof(f547,plain,
    ! [X0] : mult(op_d,mult(sF6,mult(op_d,X0))) = mult(mult(op_d,sF7),X0),
    inference(superposition,[],[f7,f482]) ).

fof(f548,plain,
    ! [X0] : mult(sF8,X0) = mult(op_d,mult(sF6,mult(op_d,X0))),
    inference(forward_demodulation,[],[f547,f33]) ).

fof(f549,plain,
    sF6 = mult(sF5,op_d),
    inference(forward_demodulation,[],[f543,f77]) ).

fof(f550,plain,
    ! [X0] : mult(sF8,X0) = mult(op_d,mult(sF4,mult(sF4,X0))),
    inference(forward_demodulation,[],[f548,f446]) ).

fof(f551,plain,
    ! [X0] : mult(sF8,X0) = ld(sF6,mult(sF4,X0)),
    inference(forward_demodulation,[],[f550,f526]) ).

fof(f556,plain,
    mult(sF8,sF3) = ld(sF6,sF6),
    inference(superposition,[],[f551,f412]) ).

fof(f557,plain,
    ld(sF6,sF7) = mult(sF8,sF4),
    inference(superposition,[],[f551,f403]) ).

fof(f558,plain,
    mult(sF8,sF5) = ld(sF6,sF8),
    inference(superposition,[],[f551,f395]) ).

fof(f559,plain,
    mult(sF8,sF6) = ld(sF6,sF9),
    inference(superposition,[],[f551,f388]) ).

fof(f563,plain,
    ! [X0] : ld(sF6,X0) = mult(sF8,ld(sF4,X0)),
    inference(superposition,[],[f551,f1]) ).

fof(f567,plain,
    ! [X0] : mult(sF4,X0) = mult(sF6,mult(sF8,X0)),
    inference(superposition,[],[f1,f551]) ).

fof(f571,plain,
    op_d = mult(sF8,sF4),
    inference(forward_demodulation,[],[f557,f546]) ).

fof(f572,plain,
    unit = mult(sF8,sF3),
    inference(forward_demodulation,[],[f556,f80]) ).

fof(f576,plain,
    ! [X0] : mult(sF4,mult(sF8,mult(sF4,X0))) = mult(mult(sF4,op_d),X0),
    inference(superposition,[],[f7,f571]) ).

fof(f577,plain,
    ! [X0] : mult(sF5,X0) = mult(sF4,mult(sF8,mult(sF4,X0))),
    inference(forward_demodulation,[],[f576,f419]) ).

fof(f584,plain,
    ! [X0] : mult(op_d,mult(sF5,mult(op_d,X0))) = mult(mult(op_d,sF6),X0),
    inference(superposition,[],[f7,f549]) ).

fof(f585,plain,
    ! [X0] : mult(sF7,X0) = mult(op_d,mult(sF5,mult(op_d,X0))),
    inference(forward_demodulation,[],[f584,f31]) ).

fof(f586,plain,
    ! [X0] : mult(sF7,X0) = mult(sF6,mult(op_d,X0)),
    inference(forward_demodulation,[],[f585,f514]) ).

fof(f587,plain,
    ! [X0] : mult(sF7,X0) = mult(sF4,mult(sF4,X0)),
    inference(backward_demodulation,[],[f446,f586]) ).

fof(f588,plain,
    ! [X0] : mult(sF4,i(X0)) = i(mult(sF7,X0)),
    inference(backward_demodulation,[],[f528,f587]) ).

fof(f595,plain,
    mult(sF7,op_c) = mult(sF6,sF12),
    inference(superposition,[],[f586,f42]) ).

fof(f596,plain,
    mult(sF6,sF3) = mult(sF7,op_d),
    inference(superposition,[],[f586,f23]) ).

fof(f597,plain,
    mult(sF6,sF4) = mult(sF7,sF3),
    inference(superposition,[],[f586,f25]) ).

fof(f600,plain,
    mult(sF6,sF7) = mult(sF7,sF6),
    inference(superposition,[],[f586,f31]) ).

fof(f601,plain,
    mult(sF6,sF8) = mult(sF7,sF7),
    inference(superposition,[],[f586,f33]) ).

fof(f602,plain,
    mult(sF7,sF8) = mult(sF6,sF9),
    inference(superposition,[],[f586,f35]) ).

fof(f608,plain,
    ! [X0] : mult(sF6,mult(op_d,mult(sF6,X0))) = mult(mult(sF7,sF6),X0),
    inference(superposition,[],[f7,f586]) ).

fof(f611,plain,
    ! [X0] : mult(op_d,X0) = ld(sF6,mult(sF7,X0)),
    inference(superposition,[],[f2,f586]) ).

fof(f614,plain,
    ! [X0] : mult(mult(sF7,sF6),X0) = mult(sF7,mult(sF6,X0)),
    inference(forward_demodulation,[],[f608,f586]) ).

fof(f617,plain,
    sF5 = mult(sF7,sF8),
    inference(forward_demodulation,[],[f602,f484]) ).

fof(f618,plain,
    sF4 = mult(sF7,sF7),
    inference(forward_demodulation,[],[f601,f485]) ).

fof(f619,plain,
    sF3 = mult(sF7,sF6),
    inference(forward_demodulation,[],[f600,f486]) ).

fof(f622,plain,
    sF9 = mult(sF7,sF3),
    inference(forward_demodulation,[],[f597,f479]) ).

fof(f623,plain,
    sF8 = mult(sF7,op_d),
    inference(forward_demodulation,[],[f596,f481]) ).

fof(f626,plain,
    ! [X0] : mult(sF3,X0) = mult(sF7,mult(sF6,X0)),
    inference(backward_demodulation,[],[f614,f619]) ).

fof(f634,plain,
    ld(op_d,sF4) = mult(sF5,sF8),
    inference(superposition,[],[f491,f485]) ).

fof(f638,plain,
    ! [X0] : mult(sF8,mult(sF6,mult(sF8,X0))) = mult(mult(sF8,sF4),X0),
    inference(superposition,[],[f7,f485]) ).

fof(f639,plain,
    ! [X0] : mult(op_d,X0) = mult(sF8,mult(sF6,mult(sF8,X0))),
    inference(forward_demodulation,[],[f638,f571]) ).

fof(f640,plain,
    sF3 = mult(sF5,sF8),
    inference(forward_demodulation,[],[f634,f71]) ).

fof(f641,plain,
    ! [X0] : mult(op_d,X0) = mult(sF8,mult(sF4,X0)),
    inference(forward_demodulation,[],[f639,f567]) ).

fof(f642,plain,
    ! [X0] : mult(sF3,X0) = mult(sF5,mult(sF4,mult(sF5,X0))),
    inference(backward_demodulation,[],[f401,f640]) ).

fof(f644,plain,
    ! [X0] : mult(sF5,X0) = mult(sF4,mult(op_d,X0)),
    inference(backward_demodulation,[],[f577,f641]) ).

fof(f645,plain,
    ! [X0] : mult(sF5,X0) = ld(sF6,X0),
    inference(backward_demodulation,[],[f519,f644]) ).

fof(f646,plain,
    ! [X0] : mult(sF5,X0) = mult(sF8,ld(sF4,X0)),
    inference(backward_demodulation,[],[f563,f645]) ).

fof(f647,plain,
    ! [X0] : mult(sF8,X0) = mult(sF4,mult(sF5,X0)),
    inference(backward_demodulation,[],[f525,f645]) ).

fof(f648,plain,
    ! [X0] : mult(op_d,mult(sF4,X0)) = mult(sF5,X0),
    inference(backward_demodulation,[],[f526,f645]) ).

fof(f651,plain,
    ! [X0] : ld(op_d,X0) = mult(sF5,mult(sF5,X0)),
    inference(backward_demodulation,[],[f527,f645]) ).

fof(f652,plain,
    ! [X0] : mult(sF8,X0) = mult(sF5,mult(sF4,X0)),
    inference(backward_demodulation,[],[f551,f645]) ).

fof(f653,plain,
    ! [X0] : mult(op_d,X0) = mult(sF5,mult(sF7,X0)),
    inference(backward_demodulation,[],[f611,f645]) ).

fof(f659,plain,
    op_d = mult(sF5,sF7),
    inference(backward_demodulation,[],[f546,f645]) ).

fof(f660,plain,
    mult(sF5,sF8) = mult(sF8,sF5),
    inference(backward_demodulation,[],[f558,f645]) ).

fof(f661,plain,
    mult(sF8,sF6) = mult(sF5,sF9),
    inference(backward_demodulation,[],[f559,f645]) ).

fof(f662,plain,
    sF3 = mult(sF8,sF5),
    inference(forward_demodulation,[],[f660,f640]) ).

fof(f666,plain,
    ! [X0] : mult(sF8,X0) = ld(op_d,ld(op_d,X0)),
    inference(backward_demodulation,[],[f509,f652]) ).

fof(f667,plain,
    ! [X0] : mult(sF3,X0) = mult(sF8,mult(sF5,X0)),
    inference(backward_demodulation,[],[f642,f652]) ).

fof(f673,plain,
    ! [X0] : sF6 = rd(X0,mult(sF5,X0)),
    inference(superposition,[],[f139,f645]) ).

fof(f674,plain,
    ! [X0] : mult(sF6,mult(sF5,X0)) = X0,
    inference(superposition,[],[f1,f645]) ).

fof(f676,plain,
    ! [X0] : i(mult(sF6,X0)) = mult(sF5,i(X0)),
    inference(superposition,[],[f117,f645]) ).

fof(f679,plain,
    ! [X0] : i(mult(sF3,X0)) = mult(sF4,mult(sF5,i(X0))),
    inference(backward_demodulation,[],[f503,f676]) ).

fof(f680,plain,
    ! [X0] : i(mult(sF3,X0)) = mult(sF8,i(X0)),
    inference(forward_demodulation,[],[f679,f647]) ).

fof(f696,plain,
    ! [X0] : mult(mult(sF5,sF3),X0) = mult(sF5,mult(sF8,mult(sF5,X0))),
    inference(superposition,[],[f7,f662]) ).

fof(f697,plain,
    ! [X0] : mult(mult(sF5,sF3),X0) = mult(sF5,mult(sF3,X0)),
    inference(forward_demodulation,[],[f696,f667]) ).

fof(f705,plain,
    ! [X0] : mult(sF7,mult(sF5,mult(sF7,X0))) = mult(mult(sF7,op_d),X0),
    inference(superposition,[],[f7,f659]) ).

fof(f706,plain,
    ! [X0] : mult(sF8,X0) = mult(sF7,mult(sF5,mult(sF7,X0))),
    inference(forward_demodulation,[],[f705,f623]) ).

fof(f707,plain,
    ! [X0] : mult(sF8,X0) = mult(sF7,mult(op_d,X0)),
    inference(forward_demodulation,[],[f706,f653]) ).

fof(f726,plain,
    ! [X0] : mult(sF4,X0) = ld(sF5,mult(sF8,X0)),
    inference(superposition,[],[f2,f652]) ).

fof(f748,plain,
    ! [X0] : ld(sF4,X0) = ld(sF8,mult(sF5,X0)),
    inference(superposition,[],[f2,f646]) ).

fof(f758,plain,
    ! [X0] : ld(op_d,X0) = mult(sF8,mult(op_d,X0)),
    inference(superposition,[],[f666,f2]) ).

fof(f770,plain,
    ! [X0] : mult(sF8,mult(sF5,mult(sF8,X0))) = mult(mult(sF8,sF3),X0),
    inference(superposition,[],[f7,f640]) ).

fof(f771,plain,
    ! [X0] : mult(unit,X0) = mult(sF8,mult(sF5,mult(sF8,X0))),
    inference(forward_demodulation,[],[f770,f572]) ).

fof(f772,plain,
    ! [X0] : mult(unit,X0) = mult(sF3,mult(sF8,X0)),
    inference(forward_demodulation,[],[f771,f667]) ).

fof(f773,plain,
    ! [X0] : mult(sF3,mult(sF8,X0)) = X0,
    inference(forward_demodulation,[],[f772,f6]) ).

fof(f780,plain,
    sF7 = ld(sF6,sF3),
    inference(superposition,[],[f2,f486]) ).

fof(f781,plain,
    ! [X0] : mult(sF7,mult(sF6,mult(sF7,X0))) = mult(mult(sF7,sF3),X0),
    inference(superposition,[],[f7,f486]) ).

fof(f782,plain,
    ! [X0] : mult(sF9,X0) = mult(sF7,mult(sF6,mult(sF7,X0))),
    inference(forward_demodulation,[],[f781,f622]) ).

fof(f783,plain,
    sF7 = mult(sF5,sF3),
    inference(forward_demodulation,[],[f780,f645]) ).

fof(f785,plain,
    ! [X0] : mult(sF9,X0) = mult(sF3,mult(sF7,X0)),
    inference(forward_demodulation,[],[f782,f626]) ).

fof(f786,plain,
    ! [X0] : mult(sF7,X0) = mult(sF5,mult(sF3,X0)),
    inference(backward_demodulation,[],[f697,f783]) ).

fof(f800,plain,
    ! [X0] : mult(sF3,mult(op_d,X0)) = mult(sF7,mult(sF7,X0)),
    inference(superposition,[],[f626,f586]) ).

fof(f802,plain,
    mult(sF3,sF6) = mult(sF7,op_d),
    inference(superposition,[],[f626,f487]) ).

fof(f803,plain,
    mult(sF7,sF3) = mult(sF3,sF7),
    inference(superposition,[],[f626,f486]) ).

fof(f811,plain,
    ! [X0] : mult(sF6,X0) = ld(sF7,mult(sF3,X0)),
    inference(superposition,[],[f2,f626]) ).

fof(f819,plain,
    sF9 = mult(sF3,sF7),
    inference(forward_demodulation,[],[f803,f622]) ).

fof(f820,plain,
    sF8 = mult(sF3,sF6),
    inference(forward_demodulation,[],[f802,f623]) ).

fof(f826,plain,
    ! [X0] : mult(sF8,X0) = mult(sF3,mult(sF6,X0)),
    inference(backward_demodulation,[],[f508,f820]) ).

fof(f837,plain,
    ld(op_d,sF5) = mult(sF5,sF9),
    inference(superposition,[],[f491,f484]) ).

fof(f840,plain,
    sF9 = ld(sF6,sF5),
    inference(superposition,[],[f2,f484]) ).

fof(f842,plain,
    sF9 = mult(sF5,sF5),
    inference(forward_demodulation,[],[f840,f645]) ).

fof(f843,plain,
    sF4 = mult(sF5,sF9),
    inference(forward_demodulation,[],[f837,f69]) ).

fof(f846,plain,
    sF4 = mult(sF8,sF6),
    inference(backward_demodulation,[],[f661,f843]) ).

fof(f895,plain,
    ! [X0] : mult(sF6,mult(sF8,mult(sF6,X0))) = mult(mult(sF6,sF4),X0),
    inference(superposition,[],[f7,f846]) ).

fof(f896,plain,
    ! [X0] : mult(sF9,X0) = mult(sF6,mult(sF8,mult(sF6,X0))),
    inference(forward_demodulation,[],[f895,f479]) ).

fof(f897,plain,
    ! [X0] : mult(sF9,X0) = mult(sF4,mult(sF6,X0)),
    inference(forward_demodulation,[],[f896,f567]) ).

fof(f898,plain,
    ! [X0] : mult(sF9,X0) = ld(op_d,X0),
    inference(backward_demodulation,[],[f480,f897]) ).

fof(f904,plain,
    ! [X0] : mult(sF6,mult(sF6,X0)) = mult(sF3,mult(sF9,X0)),
    inference(backward_demodulation,[],[f507,f898]) ).

fof(f907,plain,
    ! [X0] : mult(sF9,X0) = mult(sF5,mult(sF5,X0)),
    inference(backward_demodulation,[],[f651,f898]) ).

fof(f908,plain,
    ! [X0] : mult(sF8,X0) = ld(op_d,mult(sF9,X0)),
    inference(backward_demodulation,[],[f666,f898]) ).

fof(f913,plain,
    ! [X0] : mult(sF9,X0) = mult(sF8,mult(op_d,X0)),
    inference(backward_demodulation,[],[f758,f898]) ).

fof(f918,plain,
    ! [X0] : mult(sF3,X0) = mult(sF9,mult(sF4,X0)),
    inference(backward_demodulation,[],[f500,f898]) ).

fof(f920,plain,
    ! [X0] : mult(sF5,X0) = mult(sF9,mult(sF6,X0)),
    inference(backward_demodulation,[],[f491,f898]) ).

fof(f924,plain,
    op_d = mult(sF9,sF3),
    inference(backward_demodulation,[],[f62,f898]) ).

fof(f931,plain,
    op_c = mult(sF9,sF12),
    inference(backward_demodulation,[],[f58,f898]) ).

fof(f935,plain,
    ! [X0] : mult(op_d,X0) = mult(sF9,mult(sF4,mult(sF9,X0))),
    inference(backward_demodulation,[],[f305,f924]) ).

fof(f936,plain,
    ! [X0] : mult(sF8,X0) = mult(sF9,mult(sF9,X0)),
    inference(forward_demodulation,[],[f908,f898]) ).

fof(f940,plain,
    ! [X0] : mult(op_d,X0) = mult(sF3,mult(sF9,X0)),
    inference(forward_demodulation,[],[f935,f918]) ).

fof(f941,plain,
    ! [X0] : mult(op_d,X0) = mult(sF6,mult(sF6,X0)),
    inference(backward_demodulation,[],[f904,f940]) ).

fof(f944,plain,
    ! [X0] : op_d = rd(X0,mult(sF9,X0)),
    inference(superposition,[],[f139,f898]) ).

fof(f946,plain,
    ! [X0] : mult(sF9,mult(op_d,X0)) = X0,
    inference(superposition,[],[f2,f898]) ).

fof(f983,plain,
    ! [X0] : i(mult(sF5,X0)) = mult(sF4,i(mult(sF8,X0))),
    inference(superposition,[],[f194,f647]) ).

fof(f1038,plain,
    ! [X0] : mult(op_d,mult(sF4,mult(op_d,X0))) = mult(mult(sF5,op_d),X0),
    inference(superposition,[],[f7,f648]) ).

fof(f1045,plain,
    ! [X0] : mult(sF6,X0) = mult(op_d,mult(sF4,mult(op_d,X0))),
    inference(forward_demodulation,[],[f1038,f549]) ).

fof(f1058,plain,
    ! [X0] : mult(sF6,X0) = mult(sF5,mult(op_d,X0)),
    inference(forward_demodulation,[],[f1045,f648]) ).

fof(f1164,plain,
    ! [X0] : mult(sF3,X0) = ld(sF5,mult(sF7,X0)),
    inference(superposition,[],[f2,f786]) ).

fof(f1177,plain,
    mult(sF7,sF8) = mult(sF3,sF3),
    inference(superposition,[],[f626,f481]) ).

fof(f1184,plain,
    sF5 = mult(sF3,sF3),
    inference(forward_demodulation,[],[f1177,f617]) ).

fof(f1228,plain,
    ! [X0] : ld(sF5,X0) = mult(sF4,ld(sF8,X0)),
    inference(superposition,[],[f726,f1]) ).

fof(f1353,plain,
    ! [X0] : mult(sF6,X0) = ld(sF9,mult(sF5,X0)),
    inference(superposition,[],[f2,f920]) ).

fof(f1374,plain,
    ! [X0] : mult(sF6,ld(sF3,X0)) = ld(sF7,X0),
    inference(superposition,[],[f811,f1]) ).

fof(f1399,plain,
    ! [X0] : mult(sF6,mult(sF3,X0)) = ld(sF9,mult(sF7,X0)),
    inference(superposition,[],[f1353,f786]) ).

fof(f1406,plain,
    ! [X0] : mult(sF6,ld(sF5,X0)) = ld(sF9,X0),
    inference(superposition,[],[f1353,f1]) ).

fof(f1450,plain,
    ! [X0] : mult(sF6,X0) = mult(sF4,ld(sF8,X0)),
    inference(superposition,[],[f567,f1]) ).

fof(f1452,plain,
    ! [X0] : mult(sF6,i(X0)) = mult(sF4,i(mult(sF8,X0))),
    inference(superposition,[],[f567,f194]) ).

fof(f1465,plain,
    ! [X0] : mult(sF6,i(X0)) = i(mult(sF5,X0)),
    inference(backward_demodulation,[],[f983,f1452]) ).

fof(f1467,plain,
    ! [X0] : mult(sF6,X0) = ld(sF5,X0),
    inference(backward_demodulation,[],[f1228,f1450]) ).

fof(f1482,plain,
    ! [X0] : mult(sF6,mult(sF6,X0)) = ld(sF9,X0),
    inference(backward_demodulation,[],[f1406,f1467]) ).

fof(f1487,plain,
    ! [X0] : mult(sF3,X0) = mult(sF6,mult(sF7,X0)),
    inference(backward_demodulation,[],[f1164,f1467]) ).

fof(f1498,plain,
    ! [X0] : mult(op_d,X0) = ld(sF9,X0),
    inference(forward_demodulation,[],[f1482,f941]) ).

fof(f1506,plain,
    ! [X0] : mult(op_d,mult(sF7,X0)) = mult(sF6,mult(sF3,X0)),
    inference(backward_demodulation,[],[f1399,f1498]) ).

fof(f1516,plain,
    ! [X0] : sF9 = rd(X0,mult(op_d,X0)),
    inference(superposition,[],[f139,f1498]) ).

fof(f1522,plain,
    ! [X0] : sF5 = rd(X0,mult(sF6,X0)),
    inference(superposition,[],[f139,f1467]) ).

fof(f1526,plain,
    ! [X0] : mult(sF3,mult(sF6,X0)) = mult(sF6,mult(sF3,X0)),
    inference(superposition,[],[f1487,f626]) ).

fof(f1528,plain,
    ! [X0] : mult(sF6,mult(sF8,X0)) = mult(sF3,mult(op_d,X0)),
    inference(superposition,[],[f1487,f707]) ).

fof(f1556,plain,
    ! [X0] : mult(sF4,X0) = mult(sF3,mult(op_d,X0)),
    inference(forward_demodulation,[],[f1528,f567]) ).

fof(f1558,plain,
    ! [X0] : mult(sF8,X0) = mult(sF6,mult(sF3,X0)),
    inference(forward_demodulation,[],[f1526,f826]) ).

fof(f1564,plain,
    ! [X0] : mult(sF4,X0) = mult(sF7,mult(sF7,X0)),
    inference(backward_demodulation,[],[f800,f1556]) ).

fof(f1565,plain,
    ! [X0] : mult(sF8,X0) = mult(op_d,mult(sF7,X0)),
    inference(backward_demodulation,[],[f1506,f1558]) ).

fof(f1617,plain,
    ! [X0] : mult(sF6,X0) = ld(sF3,mult(sF8,X0)),
    inference(superposition,[],[f2,f826]) ).

fof(f1701,plain,
    ! [X0] : ld(sF4,X0) = mult(sF3,ld(sF6,X0)),
    inference(superposition,[],[f505,f1]) ).

fof(f1710,plain,
    ! [X0] : ld(sF4,X0) = mult(sF3,mult(sF5,X0)),
    inference(forward_demodulation,[],[f1701,f645]) ).

fof(f1722,plain,
    ! [X0] : mult(sF7,X0) = ld(sF4,X0),
    inference(forward_demodulation,[],[f1710,f538]) ).

fof(f1727,plain,
    ! [X0] : mult(sF7,X0) = ld(sF8,mult(sF5,X0)),
    inference(backward_demodulation,[],[f748,f1722]) ).

fof(f1760,plain,
    ! [X0] : ld(sF8,X0) = mult(sF7,ld(sF5,X0)),
    inference(superposition,[],[f1727,f1]) ).

fof(f1767,plain,
    ! [X0] : mult(sF7,mult(sF6,X0)) = ld(sF8,X0),
    inference(forward_demodulation,[],[f1760,f1467]) ).

fof(f1779,plain,
    ! [X0] : mult(sF3,X0) = ld(sF8,X0),
    inference(forward_demodulation,[],[f1767,f626]) ).

fof(f1794,plain,
    ! [X0] : sF8 = rd(X0,mult(sF3,X0)),
    inference(superposition,[],[f139,f1779]) ).

fof(f1807,plain,
    ! [X0] : mult(sF4,X0) = mult(sF6,ld(sF3,X0)),
    inference(superposition,[],[f502,f1]) ).

fof(f1826,plain,
    ! [X0] : mult(sF4,X0) = ld(sF7,X0),
    inference(backward_demodulation,[],[f1374,f1807]) ).

fof(f1852,plain,
    ! [X0] : sF7 = rd(X0,mult(sF4,X0)),
    inference(superposition,[],[f139,f1826]) ).

fof(f2060,plain,
    ! [X0] : ld(sF3,X0) = mult(sF6,ld(sF8,X0)),
    inference(superposition,[],[f1617,f1]) ).

fof(f2067,plain,
    ! [X0] : ld(sF3,X0) = mult(sF6,mult(sF3,X0)),
    inference(forward_demodulation,[],[f2060,f1779]) ).

fof(f2077,plain,
    ! [X0] : mult(sF8,X0) = ld(sF3,X0),
    inference(forward_demodulation,[],[f2067,f1558]) ).

fof(f2094,plain,
    ! [X0] : sF3 = rd(X0,mult(sF8,X0)),
    inference(superposition,[],[f139,f2077]) ).

fof(f2162,plain,
    mult(op_d,sF12) = mult(sF3,op_c),
    inference(superposition,[],[f498,f42]) ).

fof(f2329,plain,
    mult(sF9,op_c) = mult(sF8,sF12),
    inference(superposition,[],[f913,f42]) ).

fof(f3837,plain,
    ! [X0] : i(i(X0)) = X0,
    inference(superposition,[],[f3,f199]) ).

fof(f3840,plain,
    ! [X0,X1] : rd(X1,X0) = rd(i(X0),i(X1)),
    inference(superposition,[],[f4,f199]) ).

fof(f3842,plain,
    ! [X2,X0,X1] : mult(i(X1),mult(rd(X1,X0),mult(i(X1),X2))) = mult(mult(i(X1),i(X0)),X2),
    inference(superposition,[],[f7,f199]) ).

fof(f3843,plain,
    ! [X2,X0,X1] : mult(i(X1),mult(rd(X1,X0),mult(i(X1),X2))) = mult(ld(X1,i(X0)),X2),
    inference(forward_demodulation,[],[f3842,f97]) ).

fof(f3941,plain,
    ! [X2,X0,X1] : mult(i(mult(X1,X0)),X2) = mult(i(X1),mult(rd(X1,X0),mult(i(X1),X2))),
    inference(forward_demodulation,[],[f3843,f117]) ).

fof(f4026,plain,
    ! [X2,X0,X1] : mult(i(mult(X1,X0)),X2) = ld(X1,mult(rd(X1,X0),mult(i(X1),X2))),
    inference(forward_demodulation,[],[f3941,f97]) ).

fof(f4027,plain,
    ! [X2,X0,X1] : mult(i(mult(X1,X0)),X2) = ld(X1,mult(rd(X1,X0),ld(X1,X2))),
    inference(forward_demodulation,[],[f4026,f97]) ).

fof(f4028,plain,
    ! [X2,X0,X1] : ld(mult(X1,X0),X2) = ld(X1,mult(rd(X1,X0),ld(X1,X2))),
    inference(forward_demodulation,[],[f4027,f97]) ).

fof(f4040,plain,
    ! [X0,X1] : i(X1) = mult(rd(i(X0),X1),X0),
    inference(superposition,[],[f199,f3837]) ).

fof(f4070,plain,
    ! [X0] : mult(op_c,mult(X0,op_c)) = rd(mult(op_c,mult(X0,unit)),sF1),
    inference(superposition,[],[f141,f44]) ).

fof(f4085,plain,
    ! [X0] : mult(op_d,mult(X0,op_d)) = rd(mult(op_d,mult(X0,unit)),sF9),
    inference(superposition,[],[f141,f45]) ).

fof(f4138,plain,
    ! [X0] : mult(sF6,mult(X0,sF6)) = rd(mult(sF6,mult(X0,unit)),sF5),
    inference(superposition,[],[f141,f488]) ).

fof(f4374,plain,
    ! [X0] : mult(sF6,mult(X0,sF6)) = rd(mult(sF6,X0),sF5),
    inference(forward_demodulation,[],[f4138,f5]) ).

fof(f4379,plain,
    ! [X0] : mult(op_d,mult(X0,op_d)) = rd(mult(op_d,X0),sF9),
    inference(forward_demodulation,[],[f4085,f5]) ).

fof(f4380,plain,
    ! [X0] : mult(op_c,mult(X0,op_c)) = rd(mult(op_c,X0),sF1),
    inference(forward_demodulation,[],[f4070,f5]) ).

fof(f4561,plain,
    mult(op_d,mult(op_c,op_d)) = rd(sF12,sF9),
    inference(superposition,[],[f4379,f42]) ).

fof(f4594,plain,
    mult(op_d,sF11) = rd(sF12,sF9),
    inference(forward_demodulation,[],[f4561,f40]) ).

fof(f4608,plain,
    mult(op_c,mult(sF0,op_c)) = rd(sF1,sF1),
    inference(superposition,[],[f4380,f18]) ).

fof(f4611,plain,
    mult(op_c,mult(unit,op_c)) = rd(op_c,sF1),
    inference(superposition,[],[f4380,f5]) ).

fof(f4624,plain,
    mult(op_c,op_c) = rd(op_c,sF1),
    inference(forward_demodulation,[],[f4611,f6]) ).

fof(f4627,plain,
    unit = mult(op_c,mult(sF0,op_c)),
    inference(forward_demodulation,[],[f4608,f142]) ).

fof(f4632,plain,
    sF0 = rd(op_c,sF1),
    inference(forward_demodulation,[],[f4624,f16]) ).

fof(f4635,plain,
    op_c = mult(sF0,sF1),
    inference(superposition,[],[f3,f4632]) ).

fof(f4636,plain,
    ! [X0] : mult(op_c,X0) = mult(sF0,mult(op_c,mult(sF0,X0))),
    inference(backward_demodulation,[],[f68,f4635]) ).

fof(f4638,plain,
    ! [X0] : mult(op_c,ld(sF0,X0)) = mult(sF0,mult(op_c,X0)),
    inference(superposition,[],[f4636,f1]) ).

fof(f4819,plain,
    i(sF9) = mult(mult(op_d,sF11),i(sF12)),
    inference(superposition,[],[f199,f4594]) ).

fof(f4925,plain,
    mult(sF4,op_c) = mult(sF3,sF12),
    inference(superposition,[],[f1556,f42]) ).

fof(f5129,plain,
    ! [X2,X0,X1] : i(mult(X2,ld(X0,X1))) = ld(X2,mult(X0,i(X1))),
    inference(superposition,[],[f117,f195]) ).

fof(f5380,plain,
    ! [X0,X1] : i(X0) = rd(X1,mult(X0,X1)),
    inference(superposition,[],[f139,f115]) ).

fof(f5387,plain,
    sF1 = i(op_c),
    inference(backward_demodulation,[],[f377,f5380]) ).

fof(f5388,plain,
    sF9 = i(op_d),
    inference(backward_demodulation,[],[f1516,f5380]) ).

fof(f5389,plain,
    op_c = i(sF1),
    inference(backward_demodulation,[],[f358,f5380]) ).

fof(f5390,plain,
    sF8 = i(sF3),
    inference(backward_demodulation,[],[f1794,f5380]) ).

fof(f5391,plain,
    sF7 = i(sF4),
    inference(backward_demodulation,[],[f1852,f5380]) ).

fof(f5392,plain,
    sF6 = i(sF5),
    inference(backward_demodulation,[],[f673,f5380]) ).

fof(f5393,plain,
    sF5 = i(sF6),
    inference(backward_demodulation,[],[f1522,f5380]) ).

fof(f5395,plain,
    sF3 = i(sF8),
    inference(backward_demodulation,[],[f2094,f5380]) ).

fof(f5396,plain,
    op_d = i(sF9),
    inference(backward_demodulation,[],[f944,f5380]) ).

fof(f5424,plain,
    op_d = mult(mult(op_d,sF11),i(sF12)),
    inference(backward_demodulation,[],[f4819,f5396]) ).

fof(f5488,plain,
    mult(op_c,op_c) = i(sF0),
    inference(backward_demodulation,[],[f203,f5389]) ).

fof(f5493,plain,
    sF1 = mult(op_d,i(sF12)),
    inference(backward_demodulation,[],[f205,f5387]) ).

fof(f5566,plain,
    sF0 = i(sF0),
    inference(forward_demodulation,[],[f5488,f16]) ).

fof(f5573,plain,
    ! [X0] : i(X0) = mult(rd(sF3,X0),sF8),
    inference(superposition,[],[f199,f5390]) ).

fof(f5574,plain,
    ! [X0] : i(mult(X0,sF3)) = ld(X0,sF8),
    inference(superposition,[],[f117,f5390]) ).

fof(f5577,plain,
    ! [X0] : i(X0) = mult(rd(sF4,X0),sF7),
    inference(superposition,[],[f199,f5391]) ).

fof(f5578,plain,
    ! [X0] : i(mult(X0,sF4)) = ld(X0,sF7),
    inference(superposition,[],[f117,f5391]) ).

fof(f5581,plain,
    ! [X0] : i(X0) = mult(rd(op_d,X0),sF9),
    inference(superposition,[],[f199,f5388]) ).

fof(f5582,plain,
    ! [X0] : i(mult(X0,op_d)) = ld(X0,sF9),
    inference(superposition,[],[f117,f5388]) ).

fof(f5585,plain,
    ! [X0] : i(X0) = mult(rd(sF6,X0),sF5),
    inference(superposition,[],[f199,f5393]) ).

fof(f5586,plain,
    ! [X0] : i(mult(X0,sF6)) = ld(X0,sF5),
    inference(superposition,[],[f117,f5393]) ).

fof(f5590,plain,
    ! [X0] : i(mult(X0,sF5)) = ld(X0,sF6),
    inference(superposition,[],[f117,f5392]) ).

fof(f5595,plain,
    ! [X0] : mult(sF0,X0) = ld(sF0,X0),
    inference(superposition,[],[f115,f5566]) ).

fof(f5597,plain,
    ! [X0] : i(X0) = mult(rd(sF0,X0),sF0),
    inference(superposition,[],[f199,f5566]) ).

fof(f5598,plain,
    ! [X0] : i(mult(X0,sF0)) = ld(X0,sF0),
    inference(superposition,[],[f117,f5566]) ).

fof(f5600,plain,
    ! [X0] : mult(op_c,mult(sF0,X0)) = mult(sF0,mult(op_c,X0)),
    inference(backward_demodulation,[],[f4638,f5595]) ).

fof(f5601,plain,
    unit = mult(sF0,mult(op_c,op_c)),
    inference(backward_demodulation,[],[f4627,f5600]) ).

fof(f5607,plain,
    unit = mult(sF0,sF0),
    inference(forward_demodulation,[],[f5601,f16]) ).

fof(f5611,plain,
    ! [X0] : i(mult(X0,sF8)) = ld(X0,sF3),
    inference(superposition,[],[f117,f5395]) ).

fof(f5619,plain,
    ! [X0] : i(mult(X0,sF1)) = ld(X0,op_c),
    inference(superposition,[],[f117,f5389]) ).

fof(f5622,plain,
    ! [X0] : i(X0) = mult(rd(op_c,X0),sF1),
    inference(superposition,[],[f199,f5387]) ).

fof(f5629,plain,
    ! [X0] : mult(sF0,mult(sF0,X0)) = X0,
    inference(superposition,[],[f2,f5595]) ).

fof(f5630,plain,
    ! [X0] : i(mult(sF0,X0)) = mult(sF0,i(X0)),
    inference(superposition,[],[f117,f5595]) ).

fof(f5635,plain,
    ! [X0] : i(X0) = ld(rd(X0,sF3),sF8),
    inference(superposition,[],[f5574,f3]) ).

fof(f5643,plain,
    i(unit) = ld(sF8,sF8),
    inference(superposition,[],[f5574,f572]) ).

fof(f5659,plain,
    ! [X0,X1] : mult(mult(X0,sF3),X1) = ld(ld(X0,sF8),X1),
    inference(superposition,[],[f115,f5574]) ).

fof(f5662,plain,
    ! [X0,X1] : i(mult(X1,mult(X0,sF3))) = ld(X1,ld(X0,sF8)),
    inference(superposition,[],[f117,f5574]) ).

fof(f5679,plain,
    unit = i(unit),
    inference(forward_demodulation,[],[f5643,f80]) ).

fof(f5689,plain,
    ! [X0] : unit = mult(X0,i(X0)),
    inference(backward_demodulation,[],[f196,f5679]) ).

fof(f5709,plain,
    ! [X0] : i(mult(X0,unit)) = ld(X0,unit),
    inference(superposition,[],[f117,f5679]) ).

fof(f5710,plain,
    ! [X0] : i(X0) = ld(X0,unit),
    inference(forward_demodulation,[],[f5709,f5]) ).

fof(f5801,plain,
    ! [X0] : rd(X0,sF3) = rd(sF8,i(X0)),
    inference(superposition,[],[f139,f5635]) ).

fof(f5823,plain,
    ! [X0] : i(X0) = ld(rd(X0,sF4),sF7),
    inference(superposition,[],[f5578,f3]) ).

fof(f5892,plain,
    ! [X0] : rd(X0,sF4) = rd(sF7,i(X0)),
    inference(superposition,[],[f139,f5823]) ).

fof(f5914,plain,
    ! [X0] : i(X0) = ld(rd(X0,op_d),sF9),
    inference(superposition,[],[f5582,f3]) ).

fof(f5943,plain,
    ! [X0,X1] : i(mult(X1,mult(X0,op_d))) = ld(X1,ld(X0,sF9)),
    inference(superposition,[],[f117,f5582]) ).

fof(f5989,plain,
    ! [X0] : rd(X0,op_d) = rd(sF9,i(X0)),
    inference(superposition,[],[f139,f5914]) ).

fof(f6022,plain,
    ! [X0] : rd(sF3,X0) = rd(i(X0),sF8),
    inference(superposition,[],[f4,f5573]) ).

fof(f6051,plain,
    rd(sF3,sF0) = rd(sF0,sF8),
    inference(superposition,[],[f6022,f5566]) ).

fof(f6187,plain,
    rd(sF0,sF3) = rd(sF8,sF0),
    inference(superposition,[],[f5801,f5566]) ).

fof(f6234,plain,
    rd(sF0,sF4) = rd(sF7,sF0),
    inference(superposition,[],[f5892,f5566]) ).

fof(f6278,plain,
    ! [X0] : rd(i(X0),sF9) = rd(op_d,X0),
    inference(superposition,[],[f4,f5581]) ).

fof(f6306,plain,
    ! [X0] : rd(X0,sF9) = rd(op_d,i(X0)),
    inference(superposition,[],[f6278,f3837]) ).

fof(f6309,plain,
    rd(op_d,sF0) = rd(sF0,sF9),
    inference(superposition,[],[f6278,f5566]) ).

fof(f6622,plain,
    ! [X0] : rd(sF4,X0) = rd(i(X0),sF7),
    inference(superposition,[],[f4,f5577]) ).

fof(f6655,plain,
    ! [X0] : rd(sF4,i(X0)) = rd(X0,sF7),
    inference(superposition,[],[f6622,f3837]) ).

fof(f6658,plain,
    rd(sF4,sF0) = rd(sF0,sF7),
    inference(superposition,[],[f6622,f5566]) ).

fof(f6913,plain,
    ! [X0] : i(X0) = ld(rd(X0,sF6),sF5),
    inference(superposition,[],[f5586,f3]) ).

fof(f6937,plain,
    ! [X0,X1] : mult(mult(X0,sF6),X1) = ld(ld(X0,sF5),X1),
    inference(superposition,[],[f115,f5586]) ).

fof(f6990,plain,
    ! [X0] : rd(X0,sF6) = rd(sF5,i(X0)),
    inference(superposition,[],[f139,f6913]) ).

fof(f7034,plain,
    ! [X0] : rd(sF5,X0) = rd(i(X0),sF6),
    inference(superposition,[],[f6990,f3837]) ).

fof(f7119,plain,
    ! [X0] : rd(sF6,X0) = rd(i(X0),sF5),
    inference(superposition,[],[f4,f5585]) ).

fof(f7137,plain,
    ! [X0] : rd(sF6,mult(sF5,X0)) = rd(mult(sF6,i(X0)),sF5),
    inference(superposition,[],[f7119,f1465]) ).

fof(f7157,plain,
    ! [X0] : rd(sF6,i(X0)) = rd(X0,sF5),
    inference(superposition,[],[f7119,f3837]) ).

fof(f7180,plain,
    ! [X0] : rd(sF6,mult(sF5,X0)) = mult(sF6,mult(i(X0),sF6)),
    inference(forward_demodulation,[],[f7137,f4374]) ).

fof(f7189,plain,
    ! [X0] : rd(sF6,mult(sF5,X0)) = mult(sF6,ld(X0,sF6)),
    inference(forward_demodulation,[],[f7180,f97]) ).

fof(f7625,plain,
    rd(op_c,op_d) = rd(sF9,sF1),
    inference(superposition,[],[f5989,f5387]) ).

fof(f7627,plain,
    rd(sF0,op_d) = rd(sF9,sF0),
    inference(superposition,[],[f5989,f5566]) ).

fof(f7868,plain,
    ! [X0,X1] : mult(mult(X0,sF5),X1) = ld(ld(X0,sF6),X1),
    inference(superposition,[],[f115,f5590]) ).

fof(f7881,plain,
    ! [X0] : rd(mult(X0,sF5),sF6) = rd(sF5,ld(X0,sF6)),
    inference(superposition,[],[f6990,f5590]) ).

fof(f8400,plain,
    ! [X0] : mult(sF0,mult(X0,sF0)) = rd(mult(sF0,mult(X0,unit)),sF0),
    inference(superposition,[],[f141,f5607]) ).

fof(f8409,plain,
    ! [X0] : mult(sF0,mult(X0,sF0)) = rd(mult(sF0,X0),sF0),
    inference(forward_demodulation,[],[f8400,f5]) ).

fof(f8527,plain,
    ! [X0,X1] : mult(mult(X0,sF8),X1) = ld(ld(X0,sF3),X1),
    inference(superposition,[],[f115,f5611]) ).

fof(f8825,plain,
    ! [X0,X1] : mult(mult(i(X0),sF3),X1) = ld(mult(X0,sF8),X1),
    inference(superposition,[],[f5659,f115]) ).

fof(f8840,plain,
    ! [X0,X1] : mult(ld(X0,sF8),i(X1)) = i(mult(mult(X0,sF3),X1)),
    inference(superposition,[],[f195,f5659]) ).

fof(f8842,plain,
    ! [X0,X1] : mult(ld(X0,sF8),mult(mult(X0,sF3),X1)) = X1,
    inference(superposition,[],[f1,f5659]) ).

fof(f8843,plain,
    ! [X0,X1] : mult(mult(X0,sF3),mult(ld(X0,sF8),X1)) = X1,
    inference(superposition,[],[f2,f5659]) ).

fof(f8869,plain,
    ! [X0,X1] : ld(mult(X0,sF8),X1) = mult(ld(X0,sF3),X1),
    inference(forward_demodulation,[],[f8825,f97]) ).

fof(f9269,plain,
    ! [X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,mult(X1,unit)),i(X0)),
    inference(superposition,[],[f141,f5689]) ).

fof(f9402,plain,
    ! [X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,X1),i(X0)),
    inference(forward_demodulation,[],[f9269,f5]) ).

fof(f9500,plain,
    ! [X0,X1] : mult(mult(i(X0),sF6),X1) = ld(mult(X0,sF5),X1),
    inference(superposition,[],[f6937,f115]) ).

fof(f9552,plain,
    ! [X0,X1] : ld(mult(X0,sF5),X1) = mult(ld(X0,sF6),X1),
    inference(forward_demodulation,[],[f9500,f97]) ).

fof(f9667,plain,
    mult(sF5,i(sF12)) = mult(sF4,sF1),
    inference(superposition,[],[f644,f5493]) ).

fof(f9668,plain,
    mult(sF8,i(sF12)) = mult(sF7,sF1),
    inference(superposition,[],[f707,f5493]) ).

fof(f9669,plain,
    mult(sF9,i(sF12)) = mult(sF8,sF1),
    inference(superposition,[],[f913,f5493]) ).

fof(f9670,plain,
    mult(sF6,i(sF12)) = mult(sF5,sF1),
    inference(superposition,[],[f1058,f5493]) ).

fof(f9676,plain,
    i(sF12) = ld(op_d,sF1),
    inference(superposition,[],[f2,f5493]) ).

fof(f9679,plain,
    i(sF12) = mult(sF9,sF1),
    inference(forward_demodulation,[],[f9676,f898]) ).

fof(f9723,plain,
    ! [X0,X1] : mult(ld(X0,sF6),mult(mult(X0,sF5),X1)) = X1,
    inference(superposition,[],[f1,f7868]) ).

fof(f9726,plain,
    ! [X0,X1] : i(mult(ld(X0,sF6),X1)) = mult(mult(X0,sF5),i(X1)),
    inference(superposition,[],[f117,f7868]) ).

fof(f10362,plain,
    ! [X0,X1] : mult(mult(i(X0),sF8),X1) = ld(mult(X0,sF3),X1),
    inference(superposition,[],[f8527,f115]) ).

fof(f10422,plain,
    ! [X0,X1] : mult(ld(X0,sF8),X1) = ld(mult(X0,sF3),X1),
    inference(forward_demodulation,[],[f10362,f97]) ).

fof(f10727,plain,
    ! [X2,X0,X1] : ld(ld(X0,X1),X2) = mult(mult(X0,i(X1)),X2),
    inference(superposition,[],[f97,f195]) ).

fof(f10777,plain,
    ! [X0,X1] : i(X0) = rd(ld(X0,X1),X1),
    inference(superposition,[],[f4,f97]) ).

fof(f10779,plain,
    ! [X2,X0,X1] : mult(X1,mult(i(X0),mult(X1,X2))) = mult(mult(X1,ld(X0,X1)),X2),
    inference(superposition,[],[f7,f97]) ).

fof(f10807,plain,
    ! [X2,X0,X1] : mult(mult(X1,ld(X0,X1)),X2) = mult(X1,ld(X0,mult(X1,X2))),
    inference(forward_demodulation,[],[f10779,f97]) ).

fof(f11240,plain,
    sF1 = ld(sF0,op_c),
    inference(superposition,[],[f2,f4635]) ).

fof(f11243,plain,
    sF1 = mult(sF0,op_c),
    inference(forward_demodulation,[],[f11240,f5595]) ).

fof(f11253,plain,
    ! [X0] : mult(op_c,mult(sF0,mult(op_c,X0))) = mult(mult(op_c,sF1),X0),
    inference(superposition,[],[f7,f11243]) ).

fof(f11254,plain,
    ! [X0] : mult(unit,X0) = mult(op_c,mult(sF0,mult(op_c,X0))),
    inference(forward_demodulation,[],[f11253,f44]) ).

fof(f11258,plain,
    ! [X0] : mult(unit,X0) = mult(sF0,mult(op_c,mult(op_c,X0))),
    inference(forward_demodulation,[],[f11254,f5600]) ).

fof(f11261,plain,
    ! [X0] : mult(unit,X0) = mult(sF0,mult(sF1,mult(sF1,X0))),
    inference(forward_demodulation,[],[f11258,f335]) ).

fof(f11262,plain,
    ! [X0] : mult(sF0,mult(sF1,mult(sF1,X0))) = X0,
    inference(forward_demodulation,[],[f11261,f6]) ).

fof(f11286,plain,
    ! [X0] : rd(i(X0),sF1) = rd(op_c,X0),
    inference(superposition,[],[f4,f5622]) ).

fof(f11341,plain,
    ! [X0] : rd(X0,sF1) = rd(op_c,i(X0)),
    inference(superposition,[],[f11286,f3837]) ).

fof(f11707,plain,
    ! [X0,X1] : rd(i(X0),X1) = rd(i(X1),X0),
    inference(superposition,[],[f4,f4040]) ).

fof(f11822,plain,
    ! [X0,X1] : rd(ld(X0,sF8),X1) = rd(i(X1),mult(X0,sF3)),
    inference(superposition,[],[f11707,f5574]) ).

fof(f11850,plain,
    ! [X0] : rd(sF0,X0) = rd(i(X0),sF0),
    inference(superposition,[],[f11707,f5566]) ).

fof(f13369,plain,
    ! [X0] : rd(sF0,i(X0)) = rd(X0,sF0),
    inference(superposition,[],[f11850,f3837]) ).

fof(f13419,plain,
    ! [X0] : rd(mult(X0,sF3),sF0) = rd(sF0,ld(X0,sF8)),
    inference(superposition,[],[f13369,f5574]) ).

fof(f14026,plain,
    ! [X0,X1] : mult(mult(i(X0),op_c),X1) = mult(i(X0),mult(rd(X0,sF1),mult(i(X0),X1))),
    inference(superposition,[],[f95,f11341]) ).

fof(f14129,plain,
    ! [X2,X0,X1] : mult(mult(X1,X2),ld(X1,X0)) = mult(X1,mult(rd(X2,X1),X0)),
    inference(superposition,[],[f95,f1]) ).

fof(f14132,plain,
    ! [X2,X0,X1] : mult(mult(X1,X2),i(mult(X1,X0))) = mult(X1,mult(rd(X2,X1),i(X0))),
    inference(superposition,[],[f95,f194]) ).

fof(f14133,plain,
    ! [X0,X1] : mult(mult(X0,X1),i(X0)) = mult(X0,mult(rd(X1,X0),unit)),
    inference(superposition,[],[f95,f5689]) ).

fof(f14178,plain,
    ! [X0] : mult(mult(op_d,X0),sF9) = mult(op_d,mult(rd(X0,op_d),unit)),
    inference(superposition,[],[f95,f45]) ).

fof(f14180,plain,
    ! [X0] : mult(mult(sF0,X0),sF0) = mult(sF0,mult(rd(X0,sF0),unit)),
    inference(superposition,[],[f95,f5607]) ).

fof(f14228,plain,
    ! [X0] : mult(mult(sF5,X0),sF6) = mult(sF5,mult(rd(X0,sF5),unit)),
    inference(superposition,[],[f95,f535]) ).

fof(f14243,plain,
    ! [X0] : mult(mult(sF6,X0),sF5) = mult(sF6,mult(rd(X0,sF6),unit)),
    inference(superposition,[],[f95,f488]) ).

fof(f14300,plain,
    ! [X2,X0,X1] : mult(rd(X1,X0),mult(X0,X2)) = ld(X0,mult(mult(X0,X1),X2)),
    inference(superposition,[],[f2,f95]) ).

fof(f14422,plain,
    ! [X0] : mult(mult(sF6,X0),sF5) = mult(sF6,rd(X0,sF6)),
    inference(forward_demodulation,[],[f14243,f5]) ).

fof(f14425,plain,
    ! [X0] : mult(mult(sF5,X0),sF6) = mult(sF5,rd(X0,sF5)),
    inference(forward_demodulation,[],[f14228,f5]) ).

fof(f14431,plain,
    ! [X0] : mult(mult(sF0,X0),sF0) = mult(sF0,rd(X0,sF0)),
    inference(forward_demodulation,[],[f14180,f5]) ).

fof(f14432,plain,
    ! [X0] : mult(mult(op_d,X0),sF9) = mult(op_d,rd(X0,op_d)),
    inference(forward_demodulation,[],[f14178,f5]) ).

fof(f14446,plain,
    ! [X0,X1] : mult(mult(X0,X1),i(X0)) = mult(X0,rd(X1,X0)),
    inference(forward_demodulation,[],[f14133,f5]) ).

fof(f14539,plain,
    ! [X0,X1] : mult(mult(i(X0),op_c),X1) = ld(X0,mult(rd(X0,sF1),mult(i(X0),X1))),
    inference(forward_demodulation,[],[f14026,f97]) ).

fof(f14676,plain,
    ! [X0,X1] : mult(mult(i(X0),op_c),X1) = ld(X0,mult(rd(X0,sF1),ld(X0,X1))),
    inference(forward_demodulation,[],[f14539,f97]) ).

fof(f14726,plain,
    ! [X0,X1] : mult(mult(i(X0),op_c),X1) = ld(mult(X0,sF1),X1),
    inference(forward_demodulation,[],[f14676,f4028]) ).

fof(f14759,plain,
    ! [X0,X1] : ld(mult(X0,sF1),X1) = mult(ld(X0,op_c),X1),
    inference(forward_demodulation,[],[f14726,f97]) ).

fof(f14800,plain,
    mult(op_d,rd(op_c,op_d)) = mult(sF12,sF9),
    inference(superposition,[],[f14432,f42]) ).

fof(f14839,plain,
    mult(sF12,sF9) = mult(op_d,rd(sF9,sF1)),
    inference(forward_demodulation,[],[f14800,f7625]) ).

fof(f15164,plain,
    ! [X0,X1] : rd(X1,X0) = i(rd(X0,X1)),
    inference(superposition,[],[f5380,f3]) ).

fof(f15171,plain,
    ! [X0,X1] : rd(X1,i(X0)) = i(rd(i(X1),X0)),
    inference(superposition,[],[f5380,f4040]) ).

fof(f15560,plain,
    ! [X0,X1] : rd(X1,i(X0)) = rd(X0,i(X1)),
    inference(backward_demodulation,[],[f15171,f15164]) ).

fof(f15587,plain,
    ! [X0,X1] : mult(X0,mult(X1,X0)) = rd(X0,i(mult(X0,X1))),
    inference(backward_demodulation,[],[f9402,f15560]) ).

fof(f15767,plain,
    ! [X2,X0,X1] : mult(rd(X1,X0),X2) = ld(rd(X0,X1),X2),
    inference(superposition,[],[f115,f15164]) ).

fof(f15930,plain,
    ! [X0,X1] : rd(X1,i(X0)) = mult(X1,mult(ld(X1,X0),X1)),
    inference(superposition,[],[f15587,f1]) ).

fof(f15932,plain,
    ! [X0] : mult(X0,mult(unit,X0)) = rd(X0,i(X0)),
    inference(superposition,[],[f15587,f5]) ).

fof(f15957,plain,
    ! [X0,X1] : mult(i(X0),mult(X1,i(X0))) = rd(i(X0),i(ld(X0,X1))),
    inference(superposition,[],[f15587,f97]) ).

fof(f16151,plain,
    ! [X0,X1] : i(mult(X0,mult(X1,X0))) = rd(i(mult(X0,X1)),X0),
    inference(superposition,[],[f15164,f15587]) ).

fof(f16160,plain,
    ! [X0,X1] : i(mult(X0,mult(X1,X0))) = rd(i(X0),mult(X0,X1)),
    inference(forward_demodulation,[],[f16151,f11707]) ).

fof(f16324,plain,
    ! [X0,X1] : mult(i(X0),mult(X1,i(X0))) = rd(ld(X0,X1),X0),
    inference(forward_demodulation,[],[f15957,f3840]) ).

fof(f16344,plain,
    ! [X0] : mult(X0,X0) = rd(X0,i(X0)),
    inference(forward_demodulation,[],[f15932,f6]) ).

fof(f16456,plain,
    ! [X0,X1] : ld(X0,mult(X1,i(X0))) = rd(ld(X0,X1),X0),
    inference(forward_demodulation,[],[f16324,f97]) ).

fof(f16554,plain,
    ! [X0,X1] : i(mult(X0,ld(X1,X0))) = rd(ld(X0,X1),X0),
    inference(forward_demodulation,[],[f16456,f5129]) ).

fof(f16893,plain,
    ! [X2,X0,X1] : mult(rd(X0,i(X1)),X2) = ld(rd(i(X0),X1),X2),
    inference(superposition,[],[f15767,f11707]) ).

fof(f17017,plain,
    ! [X2,X0,X1] : mult(rd(X0,X1),mult(rd(X1,X0),X2)) = X2,
    inference(superposition,[],[f2,f15767]) ).

fof(f17155,plain,
    ! [X2,X0,X1] : mult(rd(X0,i(X1)),X2) = mult(rd(X1,i(X0)),X2),
    inference(forward_demodulation,[],[f16893,f15767]) ).

fof(f18070,plain,
    ! [X0,X1] : rd(mult(sF3,X0),i(X1)) = rd(X1,mult(sF8,i(X0))),
    inference(superposition,[],[f15560,f680]) ).

fof(f18079,plain,
    ! [X0,X1] : rd(X1,ld(X0,sF8)) = rd(mult(X0,sF3),i(X1)),
    inference(superposition,[],[f15560,f5574]) ).

fof(f18581,plain,
    ! [X0,X1] : rd(X1,mult(X0,sF5)) = rd(ld(X0,sF6),i(X1)),
    inference(superposition,[],[f3840,f5590]) ).

fof(f18849,plain,
    ! [X0] : mult(sF1,mult(sF1,X0)) = ld(sF0,X0),
    inference(superposition,[],[f2,f11262]) ).

fof(f18852,plain,
    ! [X0,X1] : mult(mult(sF0,X1),mult(sF1,mult(sF1,X0))) = mult(sF0,mult(rd(X1,sF0),X0)),
    inference(superposition,[],[f95,f11262]) ).

fof(f18860,plain,
    ! [X0] : mult(sF0,X0) = mult(sF1,mult(sF1,X0)),
    inference(forward_demodulation,[],[f18849,f5595]) ).

fof(f18878,plain,
    ! [X0,X1] : mult(sF0,mult(rd(X1,sF0),X0)) = mult(mult(sF0,X1),mult(sF0,X0)),
    inference(backward_demodulation,[],[f18852,f18860]) ).

fof(f19693,plain,
    ! [X0,X1] : mult(ld(X0,X1),X0) = ld(X0,rd(X0,i(X1))),
    inference(superposition,[],[f2,f15930]) ).

fof(f20146,plain,
    ! [X0,X1] : ld(X1,rd(X1,X0)) = mult(ld(X1,i(X0)),X1),
    inference(superposition,[],[f19693,f3837]) ).

fof(f20153,plain,
    ! [X0] : mult(ld(X0,sF5),X0) = ld(X0,rd(X0,sF6)),
    inference(superposition,[],[f19693,f5392]) ).

fof(f20154,plain,
    ! [X0] : mult(ld(X0,sF6),X0) = ld(X0,rd(X0,sF5)),
    inference(superposition,[],[f19693,f5393]) ).

fof(f20161,plain,
    ! [X0,X1] : mult(ld(X1,X0),X1) = ld(X1,rd(X0,i(X1))),
    inference(superposition,[],[f19693,f15560]) ).

fof(f20300,plain,
    ! [X0,X1] : mult(i(mult(X1,X0)),X1) = ld(X1,rd(X1,X0)),
    inference(forward_demodulation,[],[f20146,f117]) ).

fof(f20372,plain,
    ! [X0,X1] : ld(mult(X1,X0),X1) = ld(X1,rd(X1,X0)),
    inference(forward_demodulation,[],[f20300,f97]) ).

fof(f20929,plain,
    ! [X0] : rd(rd(X0,sF5),mult(ld(X0,sF6),X0)) = X0,
    inference(superposition,[],[f139,f20154]) ).

fof(f22929,plain,
    ! [X0,X1] : mult(ld(mult(X0,sF5),X1),mult(X0,sF5)) = ld(mult(X0,sF5),rd(X1,ld(X0,sF6))),
    inference(superposition,[],[f20161,f5590]) ).

fof(f22998,plain,
    ! [X0,X1] : rd(X1,i(X0)) = mult(X0,mult(ld(X0,X1),X0)),
    inference(superposition,[],[f1,f20161]) ).

fof(f23097,plain,
    ! [X0,X1] : mult(ld(mult(X0,sF5),X1),mult(X0,sF5)) = mult(ld(X0,sF6),rd(X1,ld(X0,sF6))),
    inference(forward_demodulation,[],[f22929,f9552]) ).

fof(f23176,plain,
    ! [X0,X1] : mult(ld(X0,sF6),rd(X1,ld(X0,sF6))) = mult(mult(ld(X0,sF6),X1),mult(X0,sF5)),
    inference(forward_demodulation,[],[f23097,f9552]) ).

fof(f24134,plain,
    ld(sF9,rd(sF9,i(sF12))) = ld(mult(sF8,sF1),sF9),
    inference(superposition,[],[f20372,f9669]) ).

fof(f24147,plain,
    ! [X0,X1] : mult(X0,X1) = rd(X0,ld(X0,rd(X0,X1))),
    inference(superposition,[],[f139,f20372]) ).

fof(f24187,plain,
    ld(sF9,rd(sF9,i(sF12))) = mult(ld(sF8,op_c),sF9),
    inference(forward_demodulation,[],[f24134,f14759]) ).

fof(f24403,plain,
    ld(sF9,rd(sF9,i(sF12))) = mult(mult(sF3,op_c),sF9),
    inference(forward_demodulation,[],[f24187,f1779]) ).

fof(f24531,plain,
    mult(mult(sF3,op_c),sF9) = mult(ld(sF9,sF12),sF9),
    inference(forward_demodulation,[],[f24403,f19693]) ).

fof(f24633,plain,
    mult(mult(sF3,op_c),sF9) = mult(mult(op_d,sF12),sF9),
    inference(forward_demodulation,[],[f24531,f1498]) ).

fof(f24718,plain,
    mult(mult(sF3,op_c),sF9) = mult(op_d,rd(sF12,op_d)),
    inference(forward_demodulation,[],[f24633,f14432]) ).

fof(f25408,plain,
    ! [X0,X1] : rd(mult(X0,mult(X1,op_d)),op_d) = rd(sF9,ld(X0,ld(X1,sF9))),
    inference(superposition,[],[f5989,f5943]) ).

fof(f25867,plain,
    ! [X2,X3,X0,X1] : ld(ld(X2,ld(X0,X1)),X3) = mult(mult(X2,mult(X0,i(X1))),X3),
    inference(superposition,[],[f10727,f195]) ).

fof(f26862,plain,
    mult(sF3,rd(sF9,sF1)) = mult(op_d,mult(sF12,sF9)),
    inference(superposition,[],[f498,f14839]) ).

fof(f26867,plain,
    rd(sF9,sF1) = mult(sF9,mult(sF12,sF9)),
    inference(superposition,[],[f946,f14839]) ).

fof(f27437,plain,
    ! [X0,X1] : mult(i(X0),mult(i(X0),X1)) = ld(ld(i(X0),X0),X1),
    inference(superposition,[],[f10727,f91]) ).

fof(f27519,plain,
    ! [X0,X1] : ld(mult(X0,X0),X1) = mult(i(X0),mult(i(X0),X1)),
    inference(forward_demodulation,[],[f27437,f115]) ).

fof(f27560,plain,
    ! [X0,X1] : ld(mult(X0,X0),X1) = ld(X0,mult(i(X0),X1)),
    inference(forward_demodulation,[],[f27519,f97]) ).

fof(f27585,plain,
    ! [X0,X1] : ld(mult(X0,X0),X1) = ld(X0,ld(X0,X1)),
    inference(forward_demodulation,[],[f27560,f97]) ).

fof(f27668,plain,
    ! [X0,X1] : mult(X0,X0) = rd(X1,ld(X0,ld(X0,X1))),
    inference(superposition,[],[f139,f27585]) ).

fof(f27878,plain,
    ! [X0] : rd(sF5,mult(X0,sF1)) = rd(ld(X0,op_c),sF6),
    inference(superposition,[],[f7034,f5619]) ).

fof(f27880,plain,
    ! [X0] : rd(mult(X0,sF1),sF5) = rd(sF6,ld(X0,op_c)),
    inference(superposition,[],[f7157,f5619]) ).

fof(f27887,plain,
    ! [X0,X1] : rd(ld(X0,op_c),X1) = rd(i(X1),mult(X0,sF1)),
    inference(superposition,[],[f11707,f5619]) ).

fof(f29880,plain,
    ! [X2,X0,X1] : mult(mult(X1,sF3),mult(ld(X1,sF8),mult(X0,mult(ld(X1,sF8),mult(mult(X1,sF3),X2))))) = mult(mult(X0,mult(ld(X1,sF8),mult(X1,sF3))),X2),
    inference(superposition,[],[f49,f8843]) ).

fof(f30126,plain,
    ! [X2,X0,X1] : mult(X0,mult(ld(X1,sF8),mult(mult(X1,sF3),X2))) = mult(mult(X0,mult(ld(X1,sF8),mult(X1,sF3))),X2),
    inference(forward_demodulation,[],[f29880,f8843]) ).

fof(f30521,plain,
    ! [X2,X0,X1] : mult(X0,X2) = mult(mult(X0,mult(ld(X1,sF8),mult(X1,sF3))),X2),
    inference(forward_demodulation,[],[f30126,f8842]) ).

fof(f32141,plain,
    ! [X0,X1] : mult(X0,unit) = mult(X0,mult(ld(X1,sF8),mult(X1,sF3))),
    inference(superposition,[],[f5,f30521]) ).

fof(f32180,plain,
    ! [X0,X1] : mult(X0,mult(ld(X1,sF8),mult(X1,sF3))) = X0,
    inference(forward_demodulation,[],[f32141,f5]) ).

fof(f32479,plain,
    ! [X0,X1] : mult(ld(X1,sF8),mult(X0,ld(X1,sF8))) = rd(mult(ld(X1,sF8),X0),mult(X1,sF3)),
    inference(superposition,[],[f141,f32180]) ).

fof(f37323,plain,
    ! [X0] : rd(mult(X0,sF0),op_d) = rd(sF9,ld(X0,sF0)),
    inference(superposition,[],[f5989,f5598]) ).

fof(f37329,plain,
    ! [X0] : rd(mult(X0,sF0),sF9) = rd(op_d,ld(X0,sF0)),
    inference(superposition,[],[f6306,f5598]) ).

fof(f37331,plain,
    ! [X0] : rd(mult(X0,sF0),sF7) = rd(sF4,ld(X0,sF0)),
    inference(superposition,[],[f6655,f5598]) ).

fof(f45676,plain,
    ! [X0,X1] : mult(X1,ld(X0,X1)) = rd(X1,ld(X1,X0)),
    inference(superposition,[],[f24147,f139]) ).

fof(f45687,plain,
    ! [X0,X1] : mult(mult(X0,X1),X1) = rd(mult(X0,X1),ld(mult(X0,X1),X0)),
    inference(superposition,[],[f24147,f4]) ).

fof(f46089,plain,
    ! [X0,X1] : mult(mult(X0,X1),X1) = rd(mult(X0,X1),ld(X0,rd(X0,X1))),
    inference(forward_demodulation,[],[f45687,f20372]) ).

fof(f53421,plain,
    ! [X0,X1] : mult(X1,X1) = rd(mult(X1,X0),ld(X1,X0)),
    inference(superposition,[],[f27668,f2]) ).

fof(f54480,plain,
    ! [X2,X0,X1] : mult(X0,ld(mult(X0,X1),mult(X0,X2))) = mult(mult(X0,ld(X0,rd(X0,X1))),X2),
    inference(superposition,[],[f10807,f20372]) ).

fof(f54737,plain,
    ! [X2,X0,X1] : mult(rd(X0,X1),X2) = mult(X0,ld(mult(X0,X1),mult(X0,X2))),
    inference(forward_demodulation,[],[f54480,f1]) ).

fof(f57440,plain,
    ! [X2,X0,X1] : mult(rd(rd(X1,X0),i(X1)),X2) = mult(rd(X1,X0),ld(i(X0),mult(rd(X1,X0),X2))),
    inference(superposition,[],[f54737,f199]) ).

fof(f57922,plain,
    ! [X2,X0,X1] : ld(mult(X0,X1),mult(X0,X2)) = ld(X0,mult(rd(X0,X1),X2)),
    inference(superposition,[],[f2,f54737]) ).

fof(f58484,plain,
    ! [X2,X0,X1] : mult(rd(rd(X1,X0),i(X1)),X2) = mult(rd(X1,X0),mult(X0,mult(rd(X1,X0),X2))),
    inference(forward_demodulation,[],[f57440,f115]) ).

fof(f58760,plain,
    ! [X2,X0,X1] : mult(rd(X1,X0),mult(X0,mult(rd(X1,X0),X2))) = mult(rd(X1,i(rd(X1,X0))),X2),
    inference(forward_demodulation,[],[f58484,f17155]) ).

fof(f58903,plain,
    ! [X2,X0,X1] : mult(rd(X1,X0),mult(X0,mult(rd(X1,X0),X2))) = mult(rd(X1,rd(X0,X1)),X2),
    inference(forward_demodulation,[],[f58760,f15164]) ).

fof(f62663,plain,
    ! [X2,X0,X1] : mult(X0,ld(X1,X2)) = mult(X1,mult(rd(ld(X1,X0),X1),X2)),
    inference(superposition,[],[f14129,f1]) ).

fof(f65883,plain,
    i(mult(sF6,mult(i(sF12),sF6))) = rd(i(sF6),mult(sF5,sF1)),
    inference(superposition,[],[f16160,f9670]) ).

fof(f66056,plain,
    i(mult(sF6,mult(i(sF12),sF6))) = rd(ld(sF5,op_c),sF6),
    inference(forward_demodulation,[],[f65883,f27887]) ).

fof(f66343,plain,
    i(mult(sF6,mult(i(sF12),sF6))) = rd(sF5,mult(sF5,sF1)),
    inference(forward_demodulation,[],[f66056,f27878]) ).

fof(f66613,plain,
    rd(sF5,mult(sF5,sF1)) = mult(sF5,i(mult(i(sF12),sF6))),
    inference(forward_demodulation,[],[f66343,f676]) ).

fof(f66825,plain,
    rd(sF5,mult(sF5,sF1)) = mult(sF5,ld(i(sF12),sF5)),
    inference(forward_demodulation,[],[f66613,f5586]) ).

fof(f66969,plain,
    rd(sF5,mult(sF5,sF1)) = mult(sF5,mult(sF12,sF5)),
    inference(forward_demodulation,[],[f66825,f115]) ).

fof(f84089,plain,
    ! [X0,X1] : mult(rd(X0,X1),rd(X0,X1)) = rd(X0,ld(rd(X0,X1),X1)),
    inference(superposition,[],[f53421,f3]) ).

fof(f84628,plain,
    ! [X0,X1] : mult(rd(X0,X1),rd(X0,X1)) = rd(X0,mult(rd(X1,X0),X1)),
    inference(forward_demodulation,[],[f84089,f15767]) ).

fof(f85329,plain,
    ! [X0] : rd(X0,i(X0)) = mult(rd(X0,sF0),rd(X0,sF0)),
    inference(superposition,[],[f84628,f5597]) ).

fof(f85428,plain,
    ! [X0] : mult(X0,X0) = mult(rd(X0,sF0),rd(X0,sF0)),
    inference(forward_demodulation,[],[f85329,f16344]) ).

fof(f86131,plain,
    ! [X0] : rd(X0,sF0) = mult(rd(sF0,X0),mult(X0,X0)),
    inference(superposition,[],[f17017,f85428]) ).

fof(f86132,plain,
    ! [X0] : mult(X0,ld(sF0,rd(ld(sF0,X0),sF0))) = mult(sF0,mult(ld(sF0,X0),ld(sF0,X0))),
    inference(superposition,[],[f62663,f85428]) ).

fof(f86154,plain,
    ! [X0] : mult(rd(X0,sF0),rd(rd(X0,sF0),rd(X0,sF0))) = mult(mult(X0,X0),i(rd(X0,sF0))),
    inference(superposition,[],[f14446,f85428]) ).

fof(f86173,plain,
    ! [X0] : mult(rd(X0,sF0),rd(rd(X0,sF0),rd(X0,sF0))) = mult(X0,mult(X0,i(rd(X0,sF0)))),
    inference(forward_demodulation,[],[f86154,f91]) ).

fof(f86190,plain,
    ! [X0] : mult(X0,ld(sF0,rd(mult(sF0,X0),sF0))) = mult(sF0,mult(mult(sF0,X0),mult(sF0,X0))),
    inference(forward_demodulation,[],[f86132,f5595]) ).

fof(f86223,plain,
    ! [X0] : mult(rd(X0,sF0),rd(rd(X0,sF0),rd(X0,sF0))) = mult(X0,mult(X0,rd(sF0,X0))),
    inference(forward_demodulation,[],[f86173,f15164]) ).

fof(f86238,plain,
    ! [X0] : mult(X0,ld(sF0,rd(mult(sF0,X0),sF0))) = mult(sF0,mult(sF0,mult(rd(X0,sF0),X0))),
    inference(forward_demodulation,[],[f86190,f18878]) ).

fof(f86262,plain,
    ! [X0] : mult(rd(X0,sF0),unit) = mult(X0,mult(X0,rd(sF0,X0))),
    inference(forward_demodulation,[],[f86223,f142]) ).

fof(f86276,plain,
    ! [X0] : mult(rd(X0,sF0),X0) = mult(X0,ld(sF0,rd(mult(sF0,X0),sF0))),
    inference(forward_demodulation,[],[f86238,f5629]) ).

fof(f86294,plain,
    ! [X0] : rd(X0,sF0) = mult(X0,mult(X0,rd(sF0,X0))),
    inference(forward_demodulation,[],[f86262,f5]) ).

fof(f86306,plain,
    ! [X0] : mult(rd(X0,sF0),X0) = mult(X0,mult(sF0,rd(mult(sF0,X0),sF0))),
    inference(forward_demodulation,[],[f86276,f5595]) ).

fof(f86324,plain,
    ! [X0] : mult(rd(X0,sF0),X0) = mult(X0,mult(sF0,mult(sF0,mult(X0,sF0)))),
    inference(forward_demodulation,[],[f86306,f8409]) ).

fof(f86329,plain,
    ! [X0] : mult(X0,mult(X0,sF0)) = mult(rd(X0,sF0),X0),
    inference(forward_demodulation,[],[f86324,f5629]) ).

fof(f86357,plain,
    mult(rd(sF0,sF7),sF4) = mult(sF4,mult(sF4,sF0)),
    inference(superposition,[],[f86329,f6658]) ).

fof(f86387,plain,
    ! [X0] : rd(X0,sF0) = rd(mult(X0,mult(X0,sF0)),X0),
    inference(superposition,[],[f4,f86329]) ).

fof(f86577,plain,
    mult(sF7,sF0) = mult(rd(sF0,sF7),sF4),
    inference(forward_demodulation,[],[f86357,f587]) ).

fof(f86916,plain,
    rd(op_d,sF0) = rd(mult(sF3,sF0),op_d),
    inference(superposition,[],[f86387,f498]) ).

fof(f86922,plain,
    rd(sF7,sF0) = rd(mult(sF4,sF0),sF7),
    inference(superposition,[],[f86387,f1564]) ).

fof(f86924,plain,
    rd(sF9,sF0) = rd(mult(sF8,sF0),sF9),
    inference(superposition,[],[f86387,f936]) ).

fof(f87021,plain,
    rd(sF9,sF0) = rd(op_d,ld(sF8,sF0)),
    inference(forward_demodulation,[],[f86924,f37329]) ).

fof(f87023,plain,
    rd(sF7,sF0) = rd(sF4,ld(sF4,sF0)),
    inference(forward_demodulation,[],[f86922,f37331]) ).

fof(f87029,plain,
    rd(op_d,sF0) = rd(sF9,ld(sF3,sF0)),
    inference(forward_demodulation,[],[f86916,f37323]) ).

fof(f87104,plain,
    rd(sF9,sF0) = rd(op_d,mult(sF3,sF0)),
    inference(forward_demodulation,[],[f87021,f1779]) ).

fof(f87106,plain,
    rd(sF7,sF0) = mult(sF4,ld(sF0,sF4)),
    inference(forward_demodulation,[],[f87023,f45676]) ).

fof(f87112,plain,
    rd(op_d,sF0) = rd(sF9,mult(sF8,sF0)),
    inference(forward_demodulation,[],[f87029,f2077]) ).

fof(f87168,plain,
    rd(sF0,op_d) = rd(op_d,mult(sF3,sF0)),
    inference(forward_demodulation,[],[f87104,f7627]) ).

fof(f87170,plain,
    rd(sF7,sF0) = mult(sF4,mult(sF0,sF4)),
    inference(forward_demodulation,[],[f87106,f5595]) ).

fof(f87176,plain,
    rd(sF0,sF9) = rd(sF9,mult(sF8,sF0)),
    inference(forward_demodulation,[],[f87112,f6309]) ).

fof(f87225,plain,
    rd(sF0,sF4) = mult(sF4,mult(sF0,sF4)),
    inference(forward_demodulation,[],[f87170,f6234]) ).

fof(f87371,plain,
    rd(sF7,sF0) = mult(rd(sF0,sF7),sF4),
    inference(superposition,[],[f86131,f618]) ).

fof(f87383,plain,
    ! [X0] : mult(X0,mult(rd(sF0,X0),X0)) = rd(mult(X0,rd(X0,sF0)),X0),
    inference(superposition,[],[f141,f86131]) ).

fof(f87435,plain,
    ! [X0] : mult(X0,sF0) = rd(mult(X0,rd(X0,sF0)),X0),
    inference(forward_demodulation,[],[f87383,f3]) ).

fof(f87445,plain,
    rd(sF7,sF0) = mult(sF7,sF0),
    inference(forward_demodulation,[],[f87371,f86577]) ).

fof(f87502,plain,
    rd(sF0,sF4) = mult(sF7,sF0),
    inference(backward_demodulation,[],[f6234,f87445]) ).

fof(f87551,plain,
    mult(sF7,sF0) = mult(sF4,mult(sF0,sF4)),
    inference(backward_demodulation,[],[f87225,f87502]) ).

fof(f88473,plain,
    ! [X0] : ld(X0,rd(X0,sF0)) = mult(X0,rd(sF0,X0)),
    inference(superposition,[],[f2,f86294]) ).

fof(f88536,plain,
    rd(op_d,sF0) = mult(sF3,rd(sF0,op_d)),
    inference(superposition,[],[f498,f86294]) ).

fof(f88722,plain,
    rd(sF0,sF9) = mult(sF3,rd(sF0,op_d)),
    inference(forward_demodulation,[],[f88536,f6309]) ).

fof(f91715,plain,
    ! [X0] : mult(mult(sF7,sF0),X0) = mult(sF4,mult(sF0,mult(sF4,X0))),
    inference(superposition,[],[f7,f87551]) ).

fof(f91724,plain,
    i(mult(sF0,sF4)) = mult(sF4,i(mult(sF7,sF0))),
    inference(superposition,[],[f194,f87551]) ).

fof(f91751,plain,
    i(mult(sF0,sF4)) = mult(sF4,mult(sF4,i(sF0))),
    inference(forward_demodulation,[],[f91724,f588]) ).

fof(f91775,plain,
    i(mult(sF0,sF4)) = mult(sF7,i(sF0)),
    inference(forward_demodulation,[],[f91751,f587]) ).

fof(f91809,plain,
    mult(sF7,sF0) = i(mult(sF0,sF4)),
    inference(forward_demodulation,[],[f91775,f5566]) ).

fof(f91828,plain,
    mult(sF7,sF0) = mult(sF0,i(sF4)),
    inference(forward_demodulation,[],[f91809,f5630]) ).

fof(f91843,plain,
    mult(sF0,sF7) = mult(sF7,sF0),
    inference(forward_demodulation,[],[f91828,f5391]) ).

fof(f91864,plain,
    ! [X0] : mult(mult(sF0,sF7),X0) = mult(sF4,mult(sF0,mult(sF4,X0))),
    inference(backward_demodulation,[],[f91715,f91843]) ).

fof(f92230,plain,
    mult(sF9,sF0) = mult(sF3,mult(sF0,sF7)),
    inference(superposition,[],[f785,f91843]) ).

fof(f92234,plain,
    mult(sF8,sF0) = mult(op_d,mult(sF0,sF7)),
    inference(superposition,[],[f1565,f91843]) ).

fof(f92241,plain,
    ! [X0] : mult(sF0,mult(sF7,mult(sF0,X0))) = mult(mult(sF0,mult(sF0,sF7)),X0),
    inference(superposition,[],[f7,f91843]) ).

fof(f92273,plain,
    ! [X0] : mult(sF7,X0) = mult(sF0,mult(sF7,mult(sF0,X0))),
    inference(forward_demodulation,[],[f92241,f5629]) ).

fof(f92345,plain,
    ! [X0] : mult(sF7,mult(sF7,mult(sF0,X0))) = mult(sF0,mult(sF7,mult(sF7,X0))),
    inference(superposition,[],[f92273,f92273]) ).

fof(f92348,plain,
    mult(sF7,op_c) = mult(sF0,mult(sF7,sF1)),
    inference(superposition,[],[f92273,f11243]) ).

fof(f92454,plain,
    mult(sF6,sF12) = mult(sF0,mult(sF7,sF1)),
    inference(forward_demodulation,[],[f92348,f595]) ).

fof(f92455,plain,
    ! [X0] : mult(sF0,mult(sF4,X0)) = mult(sF7,mult(sF7,mult(sF0,X0))),
    inference(forward_demodulation,[],[f92345,f1564]) ).

fof(f92497,plain,
    ! [X0] : mult(sF0,mult(sF4,X0)) = mult(sF4,mult(sF0,X0)),
    inference(forward_demodulation,[],[f92455,f1564]) ).

fof(f92521,plain,
    ! [X0] : mult(mult(sF0,sF7),X0) = mult(sF0,mult(sF4,mult(sF4,X0))),
    inference(backward_demodulation,[],[f91864,f92497]) ).

fof(f92536,plain,
    ! [X0] : mult(mult(sF0,sF7),X0) = mult(sF0,mult(sF7,X0)),
    inference(forward_demodulation,[],[f92521,f587]) ).

fof(f92845,plain,
    i(mult(sF6,sF12)) = mult(sF0,i(mult(sF7,sF1))),
    inference(superposition,[],[f5630,f92454]) ).

fof(f92892,plain,
    i(mult(sF6,sF12)) = mult(sF0,mult(sF4,i(sF1))),
    inference(forward_demodulation,[],[f92845,f588]) ).

fof(f92908,plain,
    i(mult(sF6,sF12)) = mult(sF0,mult(sF4,op_c)),
    inference(forward_demodulation,[],[f92892,f5389]) ).

fof(f92921,plain,
    i(mult(sF6,sF12)) = mult(sF0,mult(sF3,sF12)),
    inference(forward_demodulation,[],[f92908,f4925]) ).

fof(f92934,plain,
    mult(sF5,i(sF12)) = mult(sF0,mult(sF3,sF12)),
    inference(forward_demodulation,[],[f92921,f676]) ).

fof(f92942,plain,
    mult(sF4,sF1) = mult(sF0,mult(sF3,sF12)),
    inference(forward_demodulation,[],[f92934,f9667]) ).

fof(f94469,plain,
    rd(mult(sF8,sF0),sF9) = mult(op_d,mult(mult(sF0,sF7),op_d)),
    inference(superposition,[],[f4379,f92234]) ).

fof(f94515,plain,
    rd(mult(sF8,sF0),sF9) = mult(op_d,mult(sF0,mult(sF7,op_d))),
    inference(forward_demodulation,[],[f94469,f92536]) ).

fof(f94541,plain,
    rd(mult(sF8,sF0),sF9) = mult(op_d,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f94515,f623]) ).

fof(f94558,plain,
    rd(op_d,ld(sF8,sF0)) = mult(op_d,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f94541,f37329]) ).

fof(f94570,plain,
    rd(op_d,mult(sF3,sF0)) = mult(op_d,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f94558,f1779]) ).

fof(f94579,plain,
    rd(sF0,op_d) = mult(op_d,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f94570,f87168]) ).

fof(f94594,plain,
    mult(sF0,sF8) = mult(sF9,rd(sF0,op_d)),
    inference(superposition,[],[f946,f94579]) ).

fof(f94597,plain,
    mult(sF3,rd(sF0,op_d)) = mult(sF4,mult(sF0,sF8)),
    inference(superposition,[],[f1556,f94579]) ).

fof(f94643,plain,
    mult(sF3,rd(sF0,op_d)) = mult(sF0,mult(sF4,sF8)),
    inference(forward_demodulation,[],[f94597,f92497]) ).

fof(f94668,plain,
    mult(sF0,op_d) = mult(sF3,rd(sF0,op_d)),
    inference(forward_demodulation,[],[f94643,f307]) ).

fof(f94693,plain,
    rd(sF0,sF9) = mult(sF0,op_d),
    inference(backward_demodulation,[],[f88722,f94668]) ).

fof(f94702,plain,
    rd(op_d,sF0) = mult(sF0,op_d),
    inference(backward_demodulation,[],[f6309,f94693]) ).

fof(f94706,plain,
    mult(sF0,op_d) = rd(sF9,mult(sF8,sF0)),
    inference(backward_demodulation,[],[f87176,f94693]) ).

fof(f94797,plain,
    mult(op_d,sF0) = rd(mult(op_d,mult(sF0,op_d)),op_d),
    inference(superposition,[],[f87435,f94702]) ).

fof(f94800,plain,
    mult(op_d,op_d) = mult(mult(sF0,op_d),mult(sF0,op_d)),
    inference(superposition,[],[f85428,f94702]) ).

fof(f94805,plain,
    rd(sF0,op_d) = i(mult(sF0,op_d)),
    inference(superposition,[],[f15164,f94702]) ).

fof(f94820,plain,
    rd(sF0,op_d) = mult(sF0,i(op_d)),
    inference(forward_demodulation,[],[f94805,f5630]) ).

fof(f94825,plain,
    mult(op_d,op_d) = mult(sF0,mult(rd(op_d,sF0),op_d)),
    inference(forward_demodulation,[],[f94800,f18878]) ).

fof(f94828,plain,
    mult(op_d,sF0) = rd(sF9,ld(op_d,ld(sF0,sF9))),
    inference(forward_demodulation,[],[f94797,f25408]) ).

fof(f94835,plain,
    mult(sF0,sF9) = rd(sF0,op_d),
    inference(forward_demodulation,[],[f94820,f5388]) ).

fof(f94839,plain,
    mult(op_d,op_d) = mult(sF0,mult(op_d,mult(op_d,sF0))),
    inference(forward_demodulation,[],[f94825,f86329]) ).

fof(f94841,plain,
    mult(op_d,sF0) = rd(sF9,mult(sF9,ld(sF0,sF9))),
    inference(forward_demodulation,[],[f94828,f898]) ).

fof(f94862,plain,
    mult(sF0,sF8) = mult(sF9,mult(sF0,sF9)),
    inference(backward_demodulation,[],[f94594,f94835]) ).

fof(f94889,plain,
    mult(op_d,op_d) = mult(sF0,mult(sF3,sF0)),
    inference(forward_demodulation,[],[f94839,f498]) ).

fof(f94891,plain,
    mult(op_d,sF0) = rd(sF9,mult(sF9,mult(sF0,sF9))),
    inference(forward_demodulation,[],[f94841,f5595]) ).

fof(f94905,plain,
    sF3 = mult(sF0,mult(sF3,sF0)),
    inference(forward_demodulation,[],[f94889,f23]) ).

fof(f94906,plain,
    mult(op_d,sF0) = rd(sF9,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f94891,f94862]) ).

fof(f95002,plain,
    mult(sF0,sF3) = mult(sF3,sF0),
    inference(superposition,[],[f5629,f94905]) ).

fof(f95014,plain,
    mult(sF0,i(sF3)) = i(mult(sF3,sF0)),
    inference(superposition,[],[f194,f94905]) ).

fof(f95016,plain,
    ! [X0] : mult(sF0,mult(rd(mult(sF3,sF0),sF0),X0)) = mult(sF3,ld(sF0,X0)),
    inference(superposition,[],[f14129,f94905]) ).

fof(f95025,plain,
    ! [X0] : ld(sF0,mult(rd(sF0,mult(sF3,sF0)),X0)) = ld(sF3,mult(sF0,X0)),
    inference(superposition,[],[f57922,f94905]) ).

fof(f95030,plain,
    ! [X0] : mult(sF8,mult(sF0,X0)) = ld(sF0,mult(rd(sF0,mult(sF3,sF0)),X0)),
    inference(forward_demodulation,[],[f95025,f2077]) ).

fof(f95039,plain,
    ! [X0] : mult(sF3,mult(sF0,X0)) = mult(sF0,mult(rd(mult(sF3,sF0),sF0),X0)),
    inference(forward_demodulation,[],[f95016,f5595]) ).

fof(f95041,plain,
    mult(sF0,i(sF3)) = mult(sF8,i(sF0)),
    inference(forward_demodulation,[],[f95014,f680]) ).

fof(f95073,plain,
    ! [X0] : mult(sF8,mult(sF0,X0)) = mult(sF0,mult(rd(sF0,mult(sF3,sF0)),X0)),
    inference(forward_demodulation,[],[f95030,f5595]) ).

fof(f95082,plain,
    ! [X0] : mult(sF3,mult(sF0,X0)) = mult(sF0,mult(sF3,X0)),
    inference(forward_demodulation,[],[f95039,f4]) ).

fof(f95084,plain,
    mult(sF8,sF0) = mult(sF0,i(sF3)),
    inference(forward_demodulation,[],[f95041,f5566]) ).

fof(f95096,plain,
    ! [X0] : mult(sF8,mult(sF0,X0)) = mult(sF0,mult(i(sF3),X0)),
    inference(forward_demodulation,[],[f95073,f5380]) ).

fof(f95114,plain,
    mult(sF9,sF0) = mult(sF0,mult(sF3,sF7)),
    inference(backward_demodulation,[],[f92230,f95082]) ).

fof(f95124,plain,
    mult(sF0,sF8) = mult(sF8,sF0),
    inference(forward_demodulation,[],[f95084,f5390]) ).

fof(f95134,plain,
    ! [X0] : mult(sF8,mult(sF0,X0)) = mult(sF0,ld(sF3,X0)),
    inference(forward_demodulation,[],[f95096,f97]) ).

fof(f95148,plain,
    mult(sF0,sF9) = mult(sF9,sF0),
    inference(forward_demodulation,[],[f95114,f819]) ).

fof(f95169,plain,
    mult(sF0,op_d) = rd(sF9,mult(sF0,sF8)),
    inference(backward_demodulation,[],[f94706,f95124]) ).

fof(f95185,plain,
    ! [X0] : mult(sF8,mult(sF0,X0)) = mult(sF0,mult(sF8,X0)),
    inference(forward_demodulation,[],[f95134,f2077]) ).

fof(f95225,plain,
    mult(sF0,op_d) = mult(op_d,sF0),
    inference(backward_demodulation,[],[f94906,f95169]) ).

fof(f95838,plain,
    ld(sF3,rd(sF3,sF0)) = ld(mult(sF0,sF3),sF3),
    inference(superposition,[],[f20372,f95002]) ).

fof(f95839,plain,
    mult(mult(sF0,sF3),sF0) = rd(mult(sF0,sF3),ld(sF3,rd(sF3,sF0))),
    inference(superposition,[],[f46089,f95002]) ).

fof(f95850,plain,
    mult(mult(sF0,sF3),sF0) = rd(mult(sF0,sF3),mult(sF3,rd(sF0,sF3))),
    inference(forward_demodulation,[],[f95839,f88473]) ).

fof(f95851,plain,
    ld(sF3,rd(sF3,sF0)) = mult(ld(sF0,sF8),sF3),
    inference(forward_demodulation,[],[f95838,f10422]) ).

fof(f95879,plain,
    mult(sF0,rd(sF3,sF0)) = rd(mult(sF0,sF3),mult(sF3,rd(sF0,sF3))),
    inference(forward_demodulation,[],[f95850,f14431]) ).

fof(f95880,plain,
    ld(sF3,rd(sF3,sF0)) = mult(mult(sF0,sF8),sF3),
    inference(forward_demodulation,[],[f95851,f5595]) ).

fof(f95901,plain,
    mult(sF0,rd(sF0,sF8)) = rd(mult(sF0,sF3),mult(sF3,rd(sF0,sF3))),
    inference(forward_demodulation,[],[f95879,f6051]) ).

fof(f95902,plain,
    mult(sF3,rd(sF0,sF3)) = mult(mult(sF0,sF8),sF3),
    inference(forward_demodulation,[],[f95880,f88473]) ).

fof(f96343,plain,
    ! [X0] : mult(mult(sF0,mult(sF0,sF9)),X0) = mult(sF0,mult(sF9,mult(sF0,X0))),
    inference(superposition,[],[f7,f95148]) ).

fof(f96375,plain,
    ! [X0] : mult(sF9,X0) = mult(sF0,mult(sF9,mult(sF0,X0))),
    inference(forward_demodulation,[],[f96343,f5629]) ).

fof(f96541,plain,
    mult(sF9,sF1) = mult(sF0,mult(sF9,op_c)),
    inference(superposition,[],[f96375,f4635]) ).

fof(f96567,plain,
    ! [X0] : mult(mult(sF9,mult(sF9,sF0)),X0) = mult(sF0,mult(sF9,mult(sF0,mult(sF9,mult(sF0,X0))))),
    inference(superposition,[],[f49,f96375]) ).

fof(f96607,plain,
    ! [X0] : mult(mult(sF9,mult(sF9,sF0)),X0) = mult(sF9,mult(sF9,mult(sF0,X0))),
    inference(forward_demodulation,[],[f96567,f96375]) ).

fof(f96650,plain,
    mult(sF9,sF1) = mult(sF0,mult(sF8,sF12)),
    inference(forward_demodulation,[],[f96541,f2329]) ).

fof(f96676,plain,
    ! [X0] : mult(mult(sF9,mult(sF9,sF0)),X0) = mult(sF8,mult(sF0,X0)),
    inference(forward_demodulation,[],[f96607,f936]) ).

fof(f96702,plain,
    i(sF12) = mult(sF0,mult(sF8,sF12)),
    inference(forward_demodulation,[],[f96650,f9679]) ).

fof(f96725,plain,
    ! [X0] : mult(mult(sF9,mult(sF9,sF0)),X0) = mult(sF0,mult(sF8,X0)),
    inference(forward_demodulation,[],[f96676,f95185]) ).

fof(f96748,plain,
    ! [X0] : mult(mult(sF8,sF0),X0) = mult(sF0,mult(sF8,X0)),
    inference(forward_demodulation,[],[f96725,f936]) ).

fof(f96756,plain,
    ! [X0] : mult(mult(sF0,sF8),X0) = mult(sF0,mult(sF8,X0)),
    inference(forward_demodulation,[],[f96748,f95124]) ).

fof(f96764,plain,
    mult(sF3,rd(sF0,sF3)) = mult(sF0,mult(sF8,sF3)),
    inference(backward_demodulation,[],[f95902,f96756]) ).

fof(f96769,plain,
    mult(sF0,unit) = mult(sF3,rd(sF0,sF3)),
    inference(forward_demodulation,[],[f96764,f572]) ).

fof(f96779,plain,
    sF0 = mult(sF3,rd(sF0,sF3)),
    inference(forward_demodulation,[],[f96769,f5]) ).

fof(f96788,plain,
    mult(sF0,rd(sF0,sF8)) = rd(mult(sF0,sF3),sF0),
    inference(backward_demodulation,[],[f95901,f96779]) ).

fof(f96794,plain,
    mult(sF0,rd(sF0,sF8)) = rd(sF0,ld(sF0,sF8)),
    inference(forward_demodulation,[],[f96788,f13419]) ).

fof(f96797,plain,
    mult(sF0,rd(sF0,sF8)) = mult(sF0,ld(sF8,sF0)),
    inference(forward_demodulation,[],[f96794,f45676]) ).

fof(f96800,plain,
    mult(sF0,rd(sF0,sF8)) = mult(sF0,mult(sF3,sF0)),
    inference(forward_demodulation,[],[f96797,f1779]) ).

fof(f96803,plain,
    mult(sF0,rd(sF0,sF8)) = mult(sF0,mult(sF0,sF3)),
    inference(forward_demodulation,[],[f96800,f95002]) ).

fof(f96806,plain,
    sF3 = mult(sF0,rd(sF0,sF8)),
    inference(forward_demodulation,[],[f96803,f5629]) ).

fof(f97173,plain,
    i(rd(sF0,sF8)) = mult(sF0,i(sF3)),
    inference(superposition,[],[f194,f96806]) ).

fof(f97200,plain,
    mult(sF0,sF8) = i(rd(sF0,sF8)),
    inference(forward_demodulation,[],[f97173,f5390]) ).

fof(f97253,plain,
    mult(sF0,sF8) = rd(sF8,sF0),
    inference(forward_demodulation,[],[f97200,f15164]) ).

fof(f97292,plain,
    mult(sF0,sF8) = rd(sF0,sF3),
    inference(backward_demodulation,[],[f6187,f97253]) ).

fof(f97643,plain,
    ! [X0] : mult(mult(sF3,sF0),X0) = mult(sF3,mult(mult(sF0,sF8),mult(sF3,X0))),
    inference(superposition,[],[f95,f97292]) ).

fof(f97664,plain,
    ! [X0] : mult(mult(sF3,sF0),X0) = mult(sF3,mult(sF0,mult(sF8,mult(sF3,X0)))),
    inference(forward_demodulation,[],[f97643,f96756]) ).

fof(f97682,plain,
    ! [X0] : mult(mult(sF3,sF0),X0) = mult(sF0,mult(sF3,mult(sF8,mult(sF3,X0)))),
    inference(forward_demodulation,[],[f97664,f95082]) ).

fof(f97696,plain,
    ! [X0] : mult(mult(sF3,sF0),X0) = mult(sF0,mult(sF3,X0)),
    inference(forward_demodulation,[],[f97682,f773]) ).

fof(f97704,plain,
    ! [X0] : mult(mult(sF0,sF3),X0) = mult(sF0,mult(sF3,X0)),
    inference(forward_demodulation,[],[f97696,f95002]) ).

fof(f98341,plain,
    ! [X0] : mult(sF0,mult(op_d,mult(sF0,X0))) = mult(mult(sF0,mult(sF0,op_d)),X0),
    inference(superposition,[],[f7,f95225]) ).

fof(f98374,plain,
    ! [X0] : mult(op_d,X0) = mult(sF0,mult(op_d,mult(sF0,X0))),
    inference(forward_demodulation,[],[f98341,f5629]) ).

fof(f98507,plain,
    ! [X0] : mult(sF0,mult(op_d,X0)) = mult(op_d,mult(sF0,X0)),
    inference(superposition,[],[f5629,f98374]) ).

fof(f98514,plain,
    ! [X0] : mult(op_d,mult(sF0,op_d)) = rd(mult(op_d,mult(op_d,X0)),mult(sF0,X0)),
    inference(superposition,[],[f141,f98374]) ).

fof(f98550,plain,
    ! [X0] : mult(op_d,mult(sF0,op_d)) = rd(mult(sF3,X0),mult(sF0,X0)),
    inference(forward_demodulation,[],[f98514,f498]) ).

fof(f98627,plain,
    ! [X0] : rd(mult(sF3,X0),mult(sF0,X0)) = mult(sF0,mult(op_d,op_d)),
    inference(forward_demodulation,[],[f98550,f98507]) ).

fof(f98675,plain,
    ! [X0] : mult(sF0,sF3) = rd(mult(sF3,X0),mult(sF0,X0)),
    inference(forward_demodulation,[],[f98627,f23]) ).

fof(f101042,plain,
    mult(sF0,sF3) = rd(mult(sF3,mult(sF8,sF12)),i(sF12)),
    inference(superposition,[],[f98675,f96702]) ).

fof(f101105,plain,
    mult(sF0,sF3) = rd(sF12,mult(sF8,i(mult(sF8,sF12)))),
    inference(forward_demodulation,[],[f101042,f18070]) ).

fof(f101149,plain,
    mult(sF0,sF3) = rd(sF12,i(sF12)),
    inference(forward_demodulation,[],[f101105,f194]) ).

fof(f101176,plain,
    mult(sF0,sF3) = mult(sF12,sF12),
    inference(forward_demodulation,[],[f101149,f16344]) ).

fof(f101213,plain,
    ! [X0] : mult(mult(sF0,sF3),X0) = mult(sF12,mult(sF12,X0)),
    inference(superposition,[],[f91,f101176]) ).

fof(f101214,plain,
    sF12 = ld(sF12,mult(sF0,sF3)),
    inference(superposition,[],[f2,f101176]) ).

fof(f101215,plain,
    sF12 = rd(mult(sF0,sF3),sF12),
    inference(superposition,[],[f4,f101176]) ).

fof(f101216,plain,
    ! [X0] : mult(sF12,mult(sF12,mult(sF12,X0))) = mult(mult(sF12,mult(sF0,sF3)),X0),
    inference(superposition,[],[f7,f101176]) ).

fof(f101220,plain,
    i(sF12) = mult(sF12,i(mult(sF0,sF3))),
    inference(superposition,[],[f194,f101176]) ).

fof(f101225,plain,
    mult(sF12,mult(sF0,sF3)) = rd(sF12,i(mult(sF0,sF3))),
    inference(superposition,[],[f15587,f101176]) ).

fof(f101226,plain,
    i(mult(sF12,mult(sF0,sF3))) = rd(i(sF12),mult(sF0,sF3)),
    inference(superposition,[],[f16160,f101176]) ).

fof(f101228,plain,
    mult(mult(sF0,sF3),sF12) = rd(mult(sF0,sF3),ld(sF12,rd(sF12,sF12))),
    inference(superposition,[],[f46089,f101176]) ).

fof(f101231,plain,
    ! [X0] : ld(sF12,mult(rd(sF12,sF12),X0)) = ld(mult(sF0,sF3),mult(sF12,X0)),
    inference(superposition,[],[f57922,f101176]) ).

fof(f101235,plain,
    ! [X0] : ld(sF12,mult(rd(sF12,sF12),X0)) = mult(ld(sF0,sF8),mult(sF12,X0)),
    inference(forward_demodulation,[],[f101231,f10422]) ).

fof(f101237,plain,
    mult(mult(sF0,sF3),sF12) = rd(mult(sF0,sF3),ld(sF12,unit)),
    inference(forward_demodulation,[],[f101228,f142]) ).

fof(f101239,plain,
    i(mult(sF12,mult(sF0,sF3))) = rd(ld(sF0,sF8),sF12),
    inference(forward_demodulation,[],[f101226,f11822]) ).

fof(f101240,plain,
    mult(sF12,mult(sF0,sF3)) = rd(sF12,mult(sF0,i(sF3))),
    inference(forward_demodulation,[],[f101225,f5630]) ).

fof(f101244,plain,
    i(sF12) = mult(sF12,mult(sF0,i(sF3))),
    inference(forward_demodulation,[],[f101220,f5630]) ).

fof(f101245,plain,
    ! [X0] : mult(sF0,mult(sF3,X0)) = mult(sF12,mult(sF12,X0)),
    inference(forward_demodulation,[],[f101213,f97704]) ).

fof(f101249,plain,
    ! [X0] : ld(sF12,mult(rd(sF12,sF12),X0)) = mult(mult(sF0,sF8),mult(sF12,X0)),
    inference(forward_demodulation,[],[f101235,f5595]) ).

fof(f101250,plain,
    mult(mult(sF0,sF3),sF12) = rd(mult(sF0,sF3),i(sF12)),
    inference(forward_demodulation,[],[f101237,f5710]) ).

fof(f101252,plain,
    i(mult(sF12,mult(sF0,sF3))) = rd(mult(sF0,sF8),sF12),
    inference(forward_demodulation,[],[f101239,f5595]) ).

fof(f101253,plain,
    mult(sF12,mult(sF0,sF3)) = rd(sF12,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f101240,f5390]) ).

fof(f101257,plain,
    i(sF12) = mult(sF12,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f101244,f5390]) ).

fof(f101258,plain,
    ! [X0] : mult(mult(sF12,mult(sF0,sF3)),X0) = mult(sF12,mult(sF0,mult(sF3,X0))),
    inference(backward_demodulation,[],[f101216,f101245]) ).

fof(f101265,plain,
    ! [X0] : mult(sF0,mult(sF8,mult(sF12,X0))) = ld(sF12,mult(rd(sF12,sF12),X0)),
    inference(forward_demodulation,[],[f101249,f96756]) ).

fof(f101266,plain,
    mult(mult(sF0,sF3),sF12) = rd(sF12,ld(sF0,sF8)),
    inference(forward_demodulation,[],[f101250,f18079]) ).

fof(f101268,plain,
    rd(mult(sF0,sF8),sF12) = ld(sF12,ld(sF0,sF8)),
    inference(forward_demodulation,[],[f101252,f5662]) ).

fof(f101278,plain,
    ! [X0] : mult(sF0,mult(sF8,mult(sF12,X0))) = ld(sF12,mult(unit,X0)),
    inference(forward_demodulation,[],[f101265,f142]) ).

fof(f101279,plain,
    mult(mult(sF0,sF3),sF12) = rd(sF12,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f101266,f5595]) ).

fof(f101281,plain,
    rd(mult(sF0,sF8),sF12) = ld(sF12,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f101268,f5595]) ).

fof(f101285,plain,
    ! [X0] : ld(sF12,X0) = mult(sF0,mult(sF8,mult(sF12,X0))),
    inference(forward_demodulation,[],[f101278,f6]) ).

fof(f101286,plain,
    mult(sF12,mult(sF0,sF3)) = mult(mult(sF0,sF3),sF12),
    inference(forward_demodulation,[],[f101279,f101253]) ).

fof(f101289,plain,
    mult(sF0,mult(sF3,sF12)) = mult(sF12,mult(sF0,sF3)),
    inference(forward_demodulation,[],[f101286,f97704]) ).

fof(f101290,plain,
    mult(sF4,sF1) = mult(sF12,mult(sF0,sF3)),
    inference(forward_demodulation,[],[f101289,f92942]) ).

fof(f101291,plain,
    ! [X0] : mult(mult(sF4,sF1),X0) = mult(sF12,mult(sF0,mult(sF3,X0))),
    inference(backward_demodulation,[],[f101258,f101290]) ).

fof(f101302,plain,
    mult(mult(mult(sF0,sF3),sF12),sF12) = rd(mult(mult(sF0,sF3),sF12),ld(mult(sF0,sF3),sF12)),
    inference(superposition,[],[f46089,f101215]) ).

fof(f101307,plain,
    mult(mult(sF0,sF3),mult(sF0,sF3)) = mult(mult(mult(sF0,sF3),sF12),sF12),
    inference(forward_demodulation,[],[f101302,f53421]) ).

fof(f101317,plain,
    mult(mult(sF0,sF3),mult(sF0,sF3)) = mult(mult(sF0,mult(sF3,sF12)),sF12),
    inference(forward_demodulation,[],[f101307,f97704]) ).

fof(f101324,plain,
    mult(mult(sF0,sF3),mult(sF0,sF3)) = mult(mult(sF4,sF1),sF12),
    inference(forward_demodulation,[],[f101317,f92942]) ).

fof(f101327,plain,
    mult(mult(sF4,sF1),sF12) = mult(sF0,mult(sF3,mult(sF0,sF3))),
    inference(forward_demodulation,[],[f101324,f97704]) ).

fof(f101330,plain,
    mult(mult(sF4,sF1),sF12) = mult(sF0,mult(sF0,mult(sF3,sF3))),
    inference(forward_demodulation,[],[f101327,f95082]) ).

fof(f101333,plain,
    mult(sF3,sF3) = mult(mult(sF4,sF1),sF12),
    inference(forward_demodulation,[],[f101330,f5629]) ).

fof(f101336,plain,
    sF5 = mult(mult(sF4,sF1),sF12),
    inference(forward_demodulation,[],[f101333,f1184]) ).

fof(f101346,plain,
    rd(ld(mult(sF0,sF3),sF12),mult(sF0,sF3)) = i(mult(mult(sF0,sF3),sF12)),
    inference(superposition,[],[f16554,f101214]) ).

fof(f101351,plain,
    mult(sF12,sF12) = rd(mult(sF12,mult(sF0,sF3)),sF12),
    inference(superposition,[],[f53421,f101214]) ).

fof(f101356,plain,
    mult(sF12,sF12) = rd(mult(sF4,sF1),sF12),
    inference(forward_demodulation,[],[f101351,f101290]) ).

fof(f101360,plain,
    rd(ld(mult(sF0,sF3),sF12),mult(sF0,sF3)) = mult(ld(sF0,sF8),i(sF12)),
    inference(forward_demodulation,[],[f101346,f8840]) ).

fof(f101366,plain,
    mult(sF0,sF3) = rd(mult(sF4,sF1),sF12),
    inference(forward_demodulation,[],[f101356,f101176]) ).

fof(f101370,plain,
    rd(ld(mult(sF0,sF3),sF12),mult(sF0,sF3)) = mult(mult(sF0,sF8),i(sF12)),
    inference(forward_demodulation,[],[f101360,f5595]) ).

fof(f101378,plain,
    mult(sF0,mult(sF8,i(sF12))) = rd(ld(mult(sF0,sF3),sF12),mult(sF0,sF3)),
    inference(forward_demodulation,[],[f101370,f96756]) ).

fof(f101384,plain,
    mult(sF0,mult(sF8,i(sF12))) = rd(mult(ld(sF0,sF8),sF12),mult(sF0,sF3)),
    inference(forward_demodulation,[],[f101378,f10422]) ).

fof(f101388,plain,
    mult(sF0,mult(sF8,i(sF12))) = mult(ld(sF0,sF8),mult(sF12,ld(sF0,sF8))),
    inference(forward_demodulation,[],[f101384,f32479]) ).

fof(f101390,plain,
    mult(sF0,mult(sF8,i(sF12))) = mult(mult(sF0,sF8),mult(sF12,mult(sF0,sF8))),
    inference(forward_demodulation,[],[f101388,f5595]) ).

fof(f101391,plain,
    mult(sF0,mult(sF8,i(sF12))) = mult(sF0,mult(sF8,mult(sF12,mult(sF0,sF8)))),
    inference(forward_demodulation,[],[f101390,f96756]) ).

fof(f101392,plain,
    mult(sF0,mult(sF8,i(sF12))) = ld(sF12,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f101391,f101285]) ).

fof(f101393,plain,
    mult(sF0,mult(sF7,sF1)) = ld(sF12,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f101392,f9668]) ).

fof(f101394,plain,
    mult(sF6,sF12) = ld(sF12,mult(sF0,sF8)),
    inference(forward_demodulation,[],[f101393,f92454]) ).

fof(f101395,plain,
    mult(sF6,sF12) = rd(mult(sF0,sF8),sF12),
    inference(backward_demodulation,[],[f101281,f101394]) ).

fof(f101396,plain,
    ! [X0] : mult(sF8,mult(sF0,mult(sF12,mult(sF0,mult(sF8,X0))))) = mult(mult(sF8,mult(sF0,i(sF12))),X0),
    inference(superposition,[],[f49,f101257]) ).

fof(f101408,plain,
    mult(i(sF12),i(sF12)) = mult(sF12,rd(mult(sF0,sF8),sF12)),
    inference(superposition,[],[f14446,f101257]) ).

fof(f101426,plain,
    mult(i(sF12),i(sF12)) = mult(sF12,mult(sF6,sF12)),
    inference(forward_demodulation,[],[f101408,f101395]) ).

fof(f101437,plain,
    ! [X0] : mult(sF8,mult(sF0,mult(sF12,mult(sF0,mult(sF8,X0))))) = ld(ld(sF8,ld(sF0,sF12)),X0),
    inference(forward_demodulation,[],[f101396,f25867]) ).

fof(f101445,plain,
    ld(sF12,i(sF12)) = mult(sF12,mult(sF6,sF12)),
    inference(forward_demodulation,[],[f101426,f97]) ).

fof(f101456,plain,
    ! [X0] : mult(sF8,mult(sF0,mult(sF12,mult(sF0,mult(sF8,X0))))) = ld(mult(sF3,ld(sF0,sF12)),X0),
    inference(forward_demodulation,[],[f101437,f1779]) ).

fof(f101462,plain,
    i(mult(sF12,sF12)) = mult(sF12,mult(sF6,sF12)),
    inference(forward_demodulation,[],[f101445,f117]) ).

fof(f101471,plain,
    ! [X0] : mult(sF8,mult(sF0,mult(sF12,mult(sF0,mult(sF8,X0))))) = ld(mult(sF3,mult(sF0,sF12)),X0),
    inference(forward_demodulation,[],[f101456,f5595]) ).

fof(f101475,plain,
    i(mult(sF0,sF3)) = mult(sF12,mult(sF6,sF12)),
    inference(forward_demodulation,[],[f101462,f101176]) ).

fof(f101479,plain,
    ! [X0] : mult(sF8,mult(sF0,mult(sF12,mult(sF0,mult(sF8,X0))))) = ld(mult(sF0,mult(sF3,sF12)),X0),
    inference(forward_demodulation,[],[f101471,f95082]) ).

fof(f101481,plain,
    mult(sF0,i(sF3)) = mult(sF12,mult(sF6,sF12)),
    inference(forward_demodulation,[],[f101475,f5630]) ).

fof(f101485,plain,
    ! [X0] : ld(mult(sF4,sF1),X0) = mult(sF8,mult(sF0,mult(sF12,mult(sF0,mult(sF8,X0))))),
    inference(forward_demodulation,[],[f101479,f92942]) ).

fof(f101486,plain,
    mult(sF0,sF8) = mult(sF12,mult(sF6,sF12)),
    inference(forward_demodulation,[],[f101481,f5390]) ).

fof(f101489,plain,
    ! [X0] : ld(mult(sF4,sF1),X0) = mult(sF0,mult(sF8,mult(sF12,mult(sF0,mult(sF8,X0))))),
    inference(forward_demodulation,[],[f101485,f95185]) ).

fof(f101493,plain,
    ! [X0] : ld(mult(sF4,sF1),X0) = ld(sF12,mult(sF0,mult(sF8,X0))),
    inference(forward_demodulation,[],[f101489,f101285]) ).

fof(f101496,plain,
    ! [X0] : mult(ld(sF4,op_c),X0) = ld(sF12,mult(sF0,mult(sF8,X0))),
    inference(forward_demodulation,[],[f101493,f14759]) ).

fof(f101498,plain,
    ! [X0] : mult(mult(sF7,op_c),X0) = ld(sF12,mult(sF0,mult(sF8,X0))),
    inference(forward_demodulation,[],[f101496,f1722]) ).

fof(f101500,plain,
    ! [X0] : mult(mult(sF6,sF12),X0) = ld(sF12,mult(sF0,mult(sF8,X0))),
    inference(forward_demodulation,[],[f101498,f595]) ).

fof(f101514,plain,
    ! [X0] : ld(sF12,mult(mult(sF0,sF8),X0)) = mult(rd(mult(sF6,sF12),sF12),mult(sF12,X0)),
    inference(superposition,[],[f14300,f101486]) ).

fof(f101515,plain,
    mult(mult(sF0,sF8),i(sF12)) = mult(sF12,rd(mult(sF6,sF12),sF12)),
    inference(superposition,[],[f14446,f101486]) ).

fof(f101518,plain,
    ld(mult(sF0,sF8),sF12) = ld(sF12,rd(sF12,mult(sF6,sF12))),
    inference(superposition,[],[f20372,f101486]) ).

fof(f101529,plain,
    ld(mult(sF0,sF8),sF12) = ld(sF12,i(sF6)),
    inference(forward_demodulation,[],[f101518,f5380]) ).

fof(f101532,plain,
    mult(sF12,sF6) = mult(mult(sF0,sF8),i(sF12)),
    inference(forward_demodulation,[],[f101515,f4]) ).

fof(f101533,plain,
    ! [X0] : mult(sF6,mult(sF12,X0)) = ld(sF12,mult(mult(sF0,sF8),X0)),
    inference(forward_demodulation,[],[f101514,f4]) ).

fof(f101544,plain,
    ld(mult(sF0,sF8),sF12) = i(mult(sF12,sF6)),
    inference(forward_demodulation,[],[f101529,f117]) ).

fof(f101547,plain,
    mult(sF12,sF6) = mult(sF0,mult(sF8,i(sF12))),
    inference(forward_demodulation,[],[f101532,f96756]) ).

fof(f101548,plain,
    ! [X0] : mult(sF6,mult(sF12,X0)) = ld(sF12,mult(sF0,mult(sF8,X0))),
    inference(forward_demodulation,[],[f101533,f96756]) ).

fof(f101557,plain,
    ld(sF12,sF5) = ld(mult(sF0,sF8),sF12),
    inference(forward_demodulation,[],[f101544,f5586]) ).

fof(f101560,plain,
    mult(sF12,sF6) = mult(sF0,mult(sF7,sF1)),
    inference(forward_demodulation,[],[f101547,f9668]) ).

fof(f101561,plain,
    ! [X0] : mult(mult(sF6,sF12),X0) = mult(sF6,mult(sF12,X0)),
    inference(backward_demodulation,[],[f101500,f101548]) ).

fof(f101568,plain,
    ld(sF12,sF5) = mult(ld(sF0,sF3),sF12),
    inference(forward_demodulation,[],[f101557,f8869]) ).

fof(f101571,plain,
    mult(sF6,sF12) = mult(sF12,sF6),
    inference(forward_demodulation,[],[f101560,f92454]) ).

fof(f101617,plain,
    ld(sF12,sF5) = mult(mult(sF0,sF3),sF12),
    inference(forward_demodulation,[],[f101568,f5595]) ).

fof(f101637,plain,
    ld(sF12,sF5) = mult(sF0,mult(sF3,sF12)),
    inference(forward_demodulation,[],[f101617,f97704]) ).

fof(f101651,plain,
    mult(sF4,sF1) = ld(sF12,sF5),
    inference(forward_demodulation,[],[f101637,f92942]) ).

fof(f101685,plain,
    i(sF12) = rd(mult(sF4,sF1),sF5),
    inference(superposition,[],[f10777,f101651]) ).

fof(f101690,plain,
    rd(sF5,i(sF12)) = mult(sF12,mult(mult(sF4,sF1),sF12)),
    inference(superposition,[],[f22998,f101651]) ).

fof(f101696,plain,
    ! [X0] : mult(sF5,ld(sF12,X0)) = mult(sF12,mult(rd(mult(sF4,sF1),sF12),X0)),
    inference(superposition,[],[f62663,f101651]) ).

fof(f101697,plain,
    ! [X0] : mult(sF5,ld(sF12,X0)) = mult(sF12,mult(mult(sF0,sF3),X0)),
    inference(forward_demodulation,[],[f101696,f101366]) ).

fof(f101702,plain,
    rd(sF5,i(sF12)) = mult(sF12,sF5),
    inference(forward_demodulation,[],[f101690,f101336]) ).

fof(f101706,plain,
    i(sF12) = rd(sF6,ld(sF4,op_c)),
    inference(forward_demodulation,[],[f101685,f27880]) ).

fof(f101715,plain,
    ! [X0] : mult(sF5,ld(sF12,X0)) = mult(sF12,mult(sF0,mult(sF3,X0))),
    inference(forward_demodulation,[],[f101697,f97704]) ).

fof(f101719,plain,
    rd(sF12,sF6) = mult(sF12,sF5),
    inference(forward_demodulation,[],[f101702,f6990]) ).

fof(f101723,plain,
    i(sF12) = rd(sF6,mult(sF7,op_c)),
    inference(forward_demodulation,[],[f101706,f1722]) ).

fof(f101731,plain,
    ! [X0] : mult(sF5,ld(sF12,X0)) = mult(mult(sF4,sF1),X0),
    inference(backward_demodulation,[],[f101291,f101715]) ).

fof(f101735,plain,
    i(sF12) = rd(sF6,mult(sF6,sF12)),
    inference(forward_demodulation,[],[f101723,f595]) ).

fof(f101867,plain,
    sF12 = mult(mult(sF12,sF5),sF6),
    inference(superposition,[],[f3,f101719]) ).

fof(f101869,plain,
    i(sF6) = mult(mult(sF12,sF5),i(sF12)),
    inference(superposition,[],[f199,f101719]) ).

fof(f101870,plain,
    rd(sF6,sF12) = i(mult(sF12,sF5)),
    inference(superposition,[],[f15164,f101719]) ).

fof(f101884,plain,
    ld(sF12,sF6) = rd(sF6,sF12),
    inference(forward_demodulation,[],[f101870,f5590]) ).

fof(f101885,plain,
    i(sF6) = mult(sF12,rd(sF5,sF12)),
    inference(forward_demodulation,[],[f101869,f14446]) ).

fof(f101898,plain,
    sF5 = mult(sF12,rd(sF5,sF12)),
    inference(forward_demodulation,[],[f101885,f5393]) ).

fof(f101922,plain,
    sF6 = mult(ld(sF12,sF6),sF12),
    inference(superposition,[],[f3,f101884]) ).

fof(f101933,plain,
    mult(rd(sF12,sF6),rd(sF12,sF6)) = rd(sF12,mult(ld(sF12,sF6),sF6)),
    inference(superposition,[],[f84628,f101884]) ).

fof(f101934,plain,
    rd(sF12,mult(ld(sF12,sF6),sF6)) = mult(mult(sF12,sF5),mult(sF12,sF5)),
    inference(forward_demodulation,[],[f101933,f101719]) ).

fof(f101977,plain,
    ld(sF12,mult(sF12,sF5)) = ld(mult(sF12,sF5),rd(mult(sF12,sF5),sF6)),
    inference(superposition,[],[f20372,f101867]) ).

fof(f101978,plain,
    mult(sF12,sF6) = rd(sF12,ld(mult(sF12,sF5),rd(mult(sF12,sF5),sF6))),
    inference(superposition,[],[f46089,f101867]) ).

fof(f101989,plain,
    mult(sF12,sF6) = rd(sF12,mult(ld(mult(sF12,sF5),sF5),mult(sF12,sF5))),
    inference(forward_demodulation,[],[f101978,f20153]) ).

fof(f101990,plain,
    ld(sF12,mult(sF12,sF5)) = mult(ld(mult(sF12,sF5),sF5),mult(sF12,sF5)),
    inference(forward_demodulation,[],[f101977,f20153]) ).

fof(f102008,plain,
    mult(sF12,sF6) = rd(sF12,mult(mult(ld(sF12,sF6),sF5),mult(sF12,sF5))),
    inference(forward_demodulation,[],[f101989,f9552]) ).

fof(f102009,plain,
    ld(sF12,mult(sF12,sF5)) = mult(mult(ld(sF12,sF6),sF5),mult(sF12,sF5)),
    inference(forward_demodulation,[],[f101990,f9552]) ).

fof(f102022,plain,
    mult(sF12,sF6) = rd(sF12,mult(ld(sF12,sF6),rd(sF5,ld(sF12,sF6)))),
    inference(forward_demodulation,[],[f102008,f23176]) ).

fof(f102023,plain,
    ld(sF12,mult(sF12,sF5)) = mult(ld(sF12,sF6),rd(sF5,ld(sF12,sF6))),
    inference(forward_demodulation,[],[f102009,f23176]) ).

fof(f102031,plain,
    mult(sF6,sF12) = rd(sF12,mult(ld(sF12,sF6),rd(sF5,ld(sF12,sF6)))),
    inference(forward_demodulation,[],[f102022,f101571]) ).

fof(f102032,plain,
    sF5 = mult(ld(sF12,sF6),rd(sF5,ld(sF12,sF6))),
    inference(forward_demodulation,[],[f102023,f2]) ).

fof(f102035,plain,
    mult(sF6,sF12) = rd(sF12,sF5),
    inference(backward_demodulation,[],[f102031,f102032]) ).

fof(f102056,plain,
    mult(ld(sF12,sF6),mult(sF12,ld(sF12,sF6))) = rd(ld(sF12,sF6),i(sF6)),
    inference(superposition,[],[f15587,f101922]) ).

fof(f102057,plain,
    i(mult(ld(sF12,sF6),mult(sF12,ld(sF12,sF6)))) = rd(i(ld(sF12,sF6)),sF6),
    inference(superposition,[],[f16160,f101922]) ).

fof(f102072,plain,
    rd(sF5,ld(sF12,sF6)) = i(mult(ld(sF12,sF6),mult(sF12,ld(sF12,sF6)))),
    inference(forward_demodulation,[],[f102057,f7034]) ).

fof(f102073,plain,
    rd(sF6,mult(sF12,sF5)) = mult(ld(sF12,sF6),mult(sF12,ld(sF12,sF6))),
    inference(forward_demodulation,[],[f102056,f18581]) ).

fof(f102087,plain,
    rd(sF5,ld(sF12,sF6)) = mult(mult(sF12,sF5),i(mult(sF12,ld(sF12,sF6)))),
    inference(forward_demodulation,[],[f102072,f9726]) ).

fof(f102088,plain,
    mult(ld(sF12,sF6),sF6) = rd(sF6,mult(sF12,sF5)),
    inference(forward_demodulation,[],[f102073,f1]) ).

fof(f102099,plain,
    rd(sF5,ld(sF12,sF6)) = mult(sF12,mult(rd(sF5,sF12),i(ld(sF12,sF6)))),
    inference(forward_demodulation,[],[f102087,f14132]) ).

fof(f102109,plain,
    rd(sF5,ld(sF12,sF6)) = mult(sF12,mult(rd(sF5,sF12),mult(sF12,i(sF6)))),
    inference(forward_demodulation,[],[f102099,f195]) ).

fof(f102115,plain,
    rd(sF5,ld(sF12,sF6)) = mult(mult(sF12,sF5),i(sF6)),
    inference(forward_demodulation,[],[f102109,f95]) ).

fof(f102116,plain,
    rd(sF5,ld(sF12,sF6)) = mult(mult(sF12,sF5),sF5),
    inference(forward_demodulation,[],[f102115,f5393]) ).

fof(f102261,plain,
    ld(sF12,sF5) = rd(sF5,sF12),
    inference(superposition,[],[f2,f101898]) ).

fof(f102293,plain,
    mult(sF4,sF1) = rd(sF5,sF12),
    inference(forward_demodulation,[],[f102261,f101651]) ).

fof(f102404,plain,
    ! [X0] : mult(mult(sF12,sF5),X0) = mult(sF12,mult(mult(sF4,sF1),mult(sF12,X0))),
    inference(superposition,[],[f95,f102293]) ).

fof(f102425,plain,
    ! [X0] : mult(mult(sF12,sF5),X0) = mult(sF12,mult(sF5,ld(sF12,mult(sF12,X0)))),
    inference(forward_demodulation,[],[f102404,f101731]) ).

fof(f102438,plain,
    ! [X0] : mult(mult(sF12,sF5),X0) = mult(sF12,mult(sF5,X0)),
    inference(forward_demodulation,[],[f102425,f2]) ).

fof(f102461,plain,
    rd(sF12,mult(ld(sF12,sF6),sF6)) = mult(sF12,mult(sF5,mult(sF12,sF5))),
    inference(backward_demodulation,[],[f101934,f102438]) ).

fof(f102464,plain,
    rd(sF5,ld(sF12,sF6)) = mult(sF12,mult(sF5,sF5)),
    inference(backward_demodulation,[],[f102116,f102438]) ).

fof(f102473,plain,
    mult(sF12,sF9) = rd(sF5,ld(sF12,sF6)),
    inference(forward_demodulation,[],[f102464,f842]) ).

fof(f102494,plain,
    sF12 = rd(mult(sF6,sF12),mult(ld(sF12,sF6),sF12)),
    inference(superposition,[],[f20929,f102035]) ).

fof(f102496,plain,
    sF12 = mult(mult(sF6,sF12),sF5),
    inference(superposition,[],[f3,f102035]) ).

fof(f102519,plain,
    sF12 = mult(sF6,rd(sF12,sF6)),
    inference(forward_demodulation,[],[f102496,f14422]) ).

fof(f102521,plain,
    sF12 = rd(mult(sF6,sF12),sF6),
    inference(forward_demodulation,[],[f102494,f101922]) ).

fof(f102532,plain,
    sF12 = mult(sF6,mult(sF12,sF5)),
    inference(forward_demodulation,[],[f102519,f101719]) ).

fof(f102637,plain,
    ! [X0] : mult(sF6,mult(sF12,mult(sF6,X0))) = mult(mult(sF6,mult(sF6,sF12)),X0),
    inference(superposition,[],[f95,f102521]) ).

fof(f102657,plain,
    ! [X0] : mult(mult(op_d,sF12),X0) = mult(sF6,mult(sF12,mult(sF6,X0))),
    inference(forward_demodulation,[],[f102637,f941]) ).

fof(f102666,plain,
    ! [X0] : mult(mult(sF3,op_c),X0) = mult(sF6,mult(sF12,mult(sF6,X0))),
    inference(forward_demodulation,[],[f102657,f2162]) ).

fof(f102719,plain,
    ! [X0] : mult(sF12,mult(rd(sF6,sF12),X0)) = mult(mult(sF6,sF12),ld(sF12,X0)),
    inference(superposition,[],[f14129,f101571]) ).

fof(f102740,plain,
    ! [X0] : mult(sF12,mult(rd(sF6,sF12),X0)) = mult(sF6,mult(sF12,ld(sF12,X0))),
    inference(forward_demodulation,[],[f102719,f101561]) ).

fof(f102756,plain,
    ! [X0] : mult(sF6,X0) = mult(sF12,mult(rd(sF6,sF12),X0)),
    inference(forward_demodulation,[],[f102740,f1]) ).

fof(f102770,plain,
    ! [X0] : mult(sF6,X0) = mult(sF12,mult(ld(sF12,sF6),X0)),
    inference(forward_demodulation,[],[f102756,f101884]) ).

fof(f102794,plain,
    ! [X0] : mult(sF12,X0) = mult(sF6,mult(mult(sF12,sF5),X0)),
    inference(superposition,[],[f102770,f9723]) ).

fof(f102890,plain,
    ! [X0] : mult(sF12,X0) = mult(sF6,mult(sF12,mult(sF5,X0))),
    inference(forward_demodulation,[],[f102794,f102438]) ).

fof(f102957,plain,
    ! [X0] : mult(mult(mult(sF6,sF12),sF6),X0) = mult(mult(sF6,sF12),mult(i(sF12),mult(mult(sF6,sF12),X0))),
    inference(superposition,[],[f95,f101735]) ).

fof(f102978,plain,
    ! [X0] : mult(mult(mult(sF6,sF12),sF6),X0) = mult(sF6,mult(sF12,mult(i(sF12),mult(mult(sF6,sF12),X0)))),
    inference(forward_demodulation,[],[f102957,f101561]) ).

fof(f102987,plain,
    ! [X0] : mult(mult(mult(sF6,sF12),sF6),X0) = mult(sF6,mult(sF12,ld(sF12,mult(mult(sF6,sF12),X0)))),
    inference(forward_demodulation,[],[f102978,f97]) ).

fof(f102994,plain,
    ! [X0] : mult(mult(mult(sF6,sF12),sF6),X0) = mult(sF6,mult(mult(sF6,sF12),X0)),
    inference(forward_demodulation,[],[f102987,f1]) ).

fof(f102999,plain,
    ! [X0] : mult(mult(mult(sF6,sF12),sF6),X0) = mult(sF6,mult(sF6,mult(sF12,X0))),
    inference(forward_demodulation,[],[f102994,f101561]) ).

fof(f103003,plain,
    ! [X0] : mult(op_d,mult(sF12,X0)) = mult(mult(mult(sF6,sF12),sF6),X0),
    inference(forward_demodulation,[],[f102999,f941]) ).

fof(f103006,plain,
    ! [X0] : mult(op_d,mult(sF12,X0)) = mult(mult(sF6,mult(sF12,sF6)),X0),
    inference(forward_demodulation,[],[f103003,f101561]) ).

fof(f103009,plain,
    ! [X0] : mult(op_d,mult(sF12,X0)) = mult(sF6,mult(sF12,mult(sF6,X0))),
    inference(forward_demodulation,[],[f103006,f7]) ).

fof(f103011,plain,
    ! [X0] : mult(mult(sF3,op_c),X0) = mult(op_d,mult(sF12,X0)),
    inference(backward_demodulation,[],[f102666,f103009]) ).

fof(f103028,plain,
    mult(op_d,rd(sF12,op_d)) = mult(op_d,mult(sF12,sF9)),
    inference(backward_demodulation,[],[f24718,f103011]) ).

fof(f103032,plain,
    mult(op_d,rd(sF12,op_d)) = mult(sF3,rd(sF9,sF1)),
    inference(forward_demodulation,[],[f103028,f26862]) ).

fof(f103130,plain,
    mult(sF5,sF12) = mult(sF12,sF5),
    inference(superposition,[],[f539,f102532]) ).

fof(f103147,plain,
    mult(sF6,i(sF12)) = i(mult(sF12,sF5)),
    inference(superposition,[],[f194,f102532]) ).

fof(f103149,plain,
    ! [X0] : mult(sF6,mult(rd(mult(sF12,sF5),sF6),X0)) = mult(sF12,ld(sF6,X0)),
    inference(superposition,[],[f14129,f102532]) ).

fof(f103172,plain,
    ! [X0] : mult(sF12,mult(sF5,X0)) = mult(sF6,mult(rd(mult(sF12,sF5),sF6),X0)),
    inference(forward_demodulation,[],[f103149,f645]) ).

fof(f103174,plain,
    mult(sF6,i(sF12)) = ld(sF12,sF6),
    inference(forward_demodulation,[],[f103147,f5590]) ).

fof(f103183,plain,
    rd(sF5,mult(sF5,sF1)) = mult(sF5,mult(sF5,sF12)),
    inference(backward_demodulation,[],[f66969,f103130]) ).

fof(f103186,plain,
    rd(sF6,mult(sF5,sF12)) = mult(ld(sF12,sF6),sF6),
    inference(backward_demodulation,[],[f102088,f103130]) ).

fof(f103189,plain,
    rd(sF12,mult(ld(sF12,sF6),sF6)) = mult(sF12,mult(sF5,mult(sF5,sF12))),
    inference(backward_demodulation,[],[f102461,f103130]) ).

fof(f103214,plain,
    ! [X0] : mult(sF12,mult(sF5,X0)) = mult(sF6,mult(rd(sF5,ld(sF12,sF6)),X0)),
    inference(forward_demodulation,[],[f103172,f7881]) ).

fof(f103216,plain,
    mult(sF5,sF1) = ld(sF12,sF6),
    inference(forward_demodulation,[],[f103174,f9670]) ).

fof(f103224,plain,
    mult(sF12,mult(sF9,sF12)) = rd(sF12,mult(ld(sF12,sF6),sF6)),
    inference(forward_demodulation,[],[f103189,f907]) ).

fof(f103225,plain,
    mult(sF6,ld(sF12,sF6)) = mult(ld(sF12,sF6),sF6),
    inference(forward_demodulation,[],[f103186,f7189]) ).

fof(f103226,plain,
    mult(sF9,sF12) = rd(sF5,mult(sF5,sF1)),
    inference(forward_demodulation,[],[f103183,f907]) ).

fof(f103238,plain,
    ! [X0] : mult(sF12,mult(sF5,X0)) = mult(sF6,mult(mult(sF12,sF9),X0)),
    inference(forward_demodulation,[],[f103214,f102473]) ).

fof(f103253,plain,
    mult(sF12,sF9) = rd(sF5,mult(sF5,sF1)),
    inference(backward_demodulation,[],[f102473,f103216]) ).

fof(f103293,plain,
    mult(sF12,mult(sF9,sF12)) = rd(sF12,mult(mult(sF5,sF1),sF6)),
    inference(forward_demodulation,[],[f103224,f103216]) ).

fof(f103294,plain,
    mult(mult(sF5,sF1),sF6) = mult(sF6,mult(sF5,sF1)),
    inference(forward_demodulation,[],[f103225,f103216]) ).

fof(f103295,plain,
    op_c = rd(sF5,mult(sF5,sF1)),
    inference(forward_demodulation,[],[f103226,f931]) ).

fof(f103325,plain,
    mult(sF12,mult(sF9,sF12)) = rd(sF12,mult(sF5,rd(sF1,sF5))),
    inference(forward_demodulation,[],[f103293,f14425]) ).

fof(f103326,plain,
    sF1 = mult(mult(sF5,sF1),sF6),
    inference(forward_demodulation,[],[f103294,f674]) ).

fof(f103327,plain,
    op_c = mult(sF12,sF9),
    inference(backward_demodulation,[],[f103253,f103295]) ).

fof(f103339,plain,
    mult(sF12,op_c) = rd(sF12,mult(sF5,rd(sF1,sF5))),
    inference(forward_demodulation,[],[f103325,f931]) ).

fof(f103340,plain,
    sF1 = mult(sF5,rd(sF1,sF5)),
    inference(forward_demodulation,[],[f103326,f14425]) ).

fof(f103346,plain,
    mult(sF9,op_c) = rd(sF9,sF1),
    inference(backward_demodulation,[],[f26867,f103327]) ).

fof(f103368,plain,
    ! [X0] : mult(sF6,mult(op_c,X0)) = mult(sF12,mult(sF5,X0)),
    inference(backward_demodulation,[],[f103238,f103327]) ).

fof(f103383,plain,
    mult(sF12,op_c) = rd(sF12,sF1),
    inference(backward_demodulation,[],[f103339,f103340]) ).

fof(f103391,plain,
    ! [X0] : mult(sF12,X0) = mult(sF6,mult(sF6,mult(op_c,X0))),
    inference(backward_demodulation,[],[f102890,f103368]) ).

fof(f103427,plain,
    mult(sF8,sF12) = rd(sF9,sF1),
    inference(forward_demodulation,[],[f103346,f2329]) ).

fof(f103442,plain,
    ! [X0] : mult(op_d,mult(op_c,X0)) = mult(sF12,X0),
    inference(forward_demodulation,[],[f103391,f941]) ).

fof(f103511,plain,
    mult(op_d,rd(sF12,op_d)) = mult(sF3,mult(sF8,sF12)),
    inference(backward_demodulation,[],[f103032,f103427]) ).

fof(f103536,plain,
    ! [X0] : mult(mult(op_c,sF12),X0) = mult(op_c,mult(sF12,X0)),
    inference(backward_demodulation,[],[f52,f103442]) ).

fof(f103539,plain,
    ! [X0] : mult(mult(op_d,sF11),X0) = mult(sF12,mult(op_d,X0)),
    inference(backward_demodulation,[],[f51,f103442]) ).

fof(f103558,plain,
    sF12 = mult(op_d,rd(sF12,op_d)),
    inference(forward_demodulation,[],[f103511,f773]) ).

fof(f103620,plain,
    op_d = mult(sF12,mult(op_d,i(sF12))),
    inference(backward_demodulation,[],[f5424,f103539]) ).

fof(f103730,plain,
    op_d = mult(sF12,sF1),
    inference(forward_demodulation,[],[f103620,f5493]) ).

fof(f104521,plain,
    sF12 = mult(mult(sF12,op_c),sF1),
    inference(superposition,[],[f3,f103383]) ).

fof(f104990,plain,
    mult(sF9,sF12) = rd(sF12,op_d),
    inference(superposition,[],[f946,f103558]) ).

fof(f105000,plain,
    ! [X0] : mult(rd(sF12,op_d),mult(op_d,mult(rd(sF12,op_d),X0))) = mult(mult(rd(sF12,op_d),sF12),X0),
    inference(superposition,[],[f7,f103558]) ).

fof(f105004,plain,
    mult(op_d,i(sF12)) = i(rd(sF12,op_d)),
    inference(superposition,[],[f194,f103558]) ).

fof(f105031,plain,
    mult(op_d,i(sF12)) = rd(op_d,sF12),
    inference(forward_demodulation,[],[f105004,f15164]) ).

fof(f105034,plain,
    ! [X0] : mult(mult(rd(sF12,op_d),sF12),X0) = mult(rd(sF12,rd(op_d,sF12)),X0),
    inference(forward_demodulation,[],[f105000,f58903]) ).

fof(f105040,plain,
    op_c = rd(sF12,op_d),
    inference(forward_demodulation,[],[f104990,f931]) ).

fof(f105052,plain,
    sF1 = rd(op_d,sF12),
    inference(forward_demodulation,[],[f105031,f5493]) ).

fof(f105073,plain,
    ! [X0] : mult(mult(op_c,sF12),X0) = mult(rd(sF12,rd(op_d,sF12)),X0),
    inference(backward_demodulation,[],[f105034,f105040]) ).

fof(f105089,plain,
    ! [X0] : mult(mult(op_c,sF12),X0) = mult(rd(sF12,sF1),X0),
    inference(forward_demodulation,[],[f105073,f105052]) ).

fof(f105104,plain,
    ! [X0] : mult(mult(op_c,sF12),X0) = mult(mult(sF12,op_c),X0),
    inference(forward_demodulation,[],[f105089,f103383]) ).

fof(f105114,plain,
    ! [X0] : mult(mult(sF12,op_c),X0) = mult(op_c,mult(sF12,X0)),
    inference(forward_demodulation,[],[f105104,f103536]) ).

fof(f105344,plain,
    sF12 = mult(op_c,mult(sF12,sF1)),
    inference(backward_demodulation,[],[f104521,f105114]) ).

fof(f105507,plain,
    mult(op_c,op_d) = sF12,
    inference(forward_demodulation,[],[f105344,f103730]) ).

fof(f105645,plain,
    sF11 = sF12,
    inference(forward_demodulation,[],[f105507,f40]) ).

fof(f105849,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f105645,f43]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP689-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39  % Computer : n017.cluster.edu
% 0.14/0.39  % Model    : x86_64 x86_64
% 0.14/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39  % Memory   : 8046.5625MB
% 0.14/0.39  % OS       : Linux 6.8.0-71-generic
% 0.14/0.39  % CPULimit : 300
% 0.14/0.39  % WCLimit  : 300
% 0.14/0.39  % DateTime : Sun Sep 27 10:31:35 UTC 2026
% 0.14/0.39  % CPUTime  : 
% 0.14/0.39  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.43  Running first-order theorem proving
% 0.14/0.43  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 51.24/8.19  % (2351260)Detected a unit-equality problem, will run specialized UEQ schedule.
% 51.24/8.19  % (2351289)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=241941627:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 51.24/8.19  % (2351291)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2570324697:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 51.24/8.19  % (2351285)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=2324033523:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 51.24/8.19  % (2351287)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3521745989:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 51.24/8.19  % (2351286)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2510086348:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 51.24/8.19  % (2351288)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1468703882:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 51.24/8.19  % (2351290)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=172222083:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 51.24/8.19  % (2351289)Instruction limit reached! 
% 51.24/8.19  % (2351289)------------------------------
% 51.24/8.19  % (2351289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351289)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351289)Termination reason: Instruction limit
% 51.24/8.19  % (2351289)Termination phase: Saturation
% 51.24/8.19  % (2351289)Time elapsed: 0.095 s
% 51.24/8.19  % (2351289)Peak memory usage: 89 MB
% 51.24/8.19  % (2351289)Instructions burned: 182 (million)
% 51.24/8.19  % (2351288)Instruction limit reached! 
% 51.24/8.19  % (2351288)------------------------------
% 51.24/8.19  % (2351288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351288)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351288)Termination reason: Instruction limit
% 51.24/8.19  % (2351288)Termination phase: Saturation
% 51.24/8.19  % (2351288)Time elapsed: 0.134 s
% 51.24/8.19  % (2351288)Peak memory usage: 88 MB
% 51.24/8.19  % (2351288)Instructions burned: 136 (million)
% 51.24/8.19  % (2351300)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=727284030:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 51.24/8.19  % (2351290)Instruction limit reached! 
% 51.24/8.19  % (2351290)------------------------------
% 51.24/8.19  % (2351290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351290)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351290)Termination reason: Instruction limit
% 51.24/8.19  % (2351290)Termination phase: Saturation
% 51.24/8.19  % (2351290)Time elapsed: 0.256 s
% 51.24/8.19  % (2351290)Peak memory usage: 90 MB
% 51.24/8.19  % (2351290)Instructions burned: 257 (million)
% 51.24/8.19  % (2351301)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2157459877:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 51.24/8.19  % (2351304)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=778398334:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 51.24/8.19  % (2351304)Instruction limit reached! 
% 51.24/8.19  % (2351304)------------------------------
% 51.24/8.19  % (2351304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351304)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351304)Termination reason: Instruction limit
% 51.24/8.19  % (2351304)Termination phase: Saturation
% 51.24/8.19  % (2351304)Time elapsed: 0.167 s
% 51.24/8.19  % (2351304)Peak memory usage: 90 MB
% 51.24/8.19  % (2351304)Instructions burned: 217 (million)
% 51.24/8.19  % (2351309)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=688498966:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 51.24/8.19  % (2351291)Instruction limit reached! 
% 51.24/8.19  % (2351291)------------------------------
% 51.24/8.19  % (2351291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351291)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351291)Termination reason: Instruction limit
% 51.24/8.19  % (2351291)Termination phase: Saturation
% 51.24/8.19  % (2351291)Time elapsed: 0.916 s
% 51.24/8.19  % (2351291)Peak memory usage: 99 MB
% 51.24/8.19  % (2351291)Instructions burned: 1187 (million)
% 51.24/8.19  % (2351312)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3562602578:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/12125Mi)
% 51.24/8.19  % (2351309)Instruction limit reached! 
% 51.24/8.19  % (2351309)------------------------------
% 51.24/8.19  % (2351309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351309)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351309)Termination reason: Instruction limit
% 51.24/8.19  % (2351309)Termination phase: Saturation
% 51.24/8.19  % (2351309)Time elapsed: 0.198 s
% 51.24/8.19  % (2351309)Peak memory usage: 93 MB
% 51.24/8.19  % (2351309)Instructions burned: 317 (million)
% 51.24/8.19  % (2351322)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=906221006:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2987 on theBenchmark for (2987ds/2836Mi)
% 51.24/8.19  % (2351300)Instruction limit reached! 
% 51.24/8.19  % (2351300)------------------------------
% 51.24/8.19  % (2351300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351300)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351300)Termination reason: Instruction limit
% 51.24/8.19  % (2351300)Termination phase: Saturation
% 51.24/8.19  % (2351300)Time elapsed: 1.496 s
% 51.24/8.19  % (2351300)Peak memory usage: 141 MB
% 51.24/8.19  % (2351300)Instructions burned: 2051 (million)
% 51.24/8.19  % (2351468)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=825658652:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2980 on theBenchmark for (2980ds/14534Mi)
% 51.24/8.19  % (2351301)Instruction limit reached! 
% 51.24/8.19  % (2351301)------------------------------
% 51.24/8.19  % (2351301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351301)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351301)Termination reason: Instruction limit
% 51.24/8.19  % (2351301)Termination phase: Saturation
% 51.24/8.19  % (2351301)Time elapsed: 2.311 s
% 51.24/8.19  % (2351301)Peak memory usage: 170 MB
% 51.24/8.19  % (2351301)Instructions burned: 4949 (million)
% 51.24/8.19  % (2351470)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=837436605:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/11832Mi)
% 51.24/8.19  % (2351322)Instruction limit reached! 
% 51.24/8.19  % (2351322)------------------------------
% 51.24/8.19  % (2351322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351322)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351322)Termination reason: Instruction limit
% 51.24/8.19  % (2351322)Termination phase: Saturation
% 51.24/8.19  % (2351322)Time elapsed: 1.965 s
% 51.24/8.19  % (2351322)Peak memory usage: 133 MB
% 51.24/8.19  % (2351322)Instructions burned: 2836 (million)
% 51.24/8.19  % (2351472)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=4211403335:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 51.24/8.19  % (2351472)Instruction limit reached! 
% 51.24/8.19  % (2351472)------------------------------
% 51.24/8.19  % (2351472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351472)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351472)Termination reason: Instruction limit
% 51.24/8.19  % (2351472)Termination phase: Saturation
% 51.24/8.19  % (2351472)Time elapsed: 1.417 s
% 51.24/8.19  % (2351472)Peak memory usage: 139 MB
% 51.24/8.19  % (2351472)Instructions burned: 2281 (million)
% 51.24/8.19  % (2351474)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=3952314263:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 51.24/8.19  % (2351312)Instruction limit reached! 
% 51.24/8.19  % (2351312)------------------------------
% 51.24/8.19  % (2351312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.24/8.19  % (2351312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.24/8.19  % (2351312)CaDiCaL version: 2.1.3
% 51.24/8.19  % (2351312)Termination reason: Instruction limit
% 51.24/8.19  % (2351312)Termination phase: Saturation
% 51.24/8.19  % (2351312)Time elapsed: 4.219 s
% 51.24/8.19  % (2351312)Peak memory usage: 243 MB
% 51.24/8.19  % (2351312)Instructions burned: 12126 (million)
% 51.24/8.19  % (2351476)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=972699877:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2945 on theBenchmark for (2945ds/21755Mi)
% 51.24/8.19  % (2351287)First to succeed.
% 51.24/8.19  % (2351287)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2351260"
% 51.24/8.19  % (2351287)Refutation found. Thanks to Tanya!
% 51.24/8.19  % SZS status Unsatisfiable for theBenchmark
% 51.24/8.19  % SZS output start Proof for theBenchmark
% See solution above
% 51.74/8.38  % (2351287)------------------------------
% 51.74/8.38  % (2351287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.74/8.38  % (2351287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.74/8.38  % (2351287)CaDiCaL version: 2.1.3
% 51.74/8.38  % (2351287)Termination reason: Refutation
% 51.74/8.38  % (2351287)Time elapsed: 6.706 s
% 51.74/8.38  % (2351287)Peak memory usage: 216 MB
% 51.74/8.38  % (2351287)Instructions burned: 10553 (million)
% 51.74/8.38  % (2351287)------------------------------
% 51.74/8.38  % (2351287)------------------------------
% 51.74/8.38  % (2351260)Success in time 7.201 s
% 51.74/8.38  % Vampire exiting
%------------------------------------------------------------------------------