Vampire---5.0.1.UNS-Ref.s

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

% Computer : n010.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:16:09 AM UTC 2026

% Result   : Unsatisfiable 148.45s 31.54s
% Output   : Refutation 218.93s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  107
%            Number of leaves      :   19
% Syntax   : Number of formulae    : 1133 (1133 unt;   6 def)
%            Number of atoms       : 1133 (1132 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    3 (   3   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   2 avg)
%            Maximal term depth    :    8 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :   15 (  15 usr;   9 con; 0-2 aty)
%            Number of variables   :  924 ( 924   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
    ! [X0] : product(X0,one) = X0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos01) ).

fof(f2,negated_conjecture,
    ! [X0] : product(one,X0) = X0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos02) ).

fof(f3,axiom,
    ! [X0,X1] : product(X0,difference(X0,X1)) = X1,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos03) ).

fof(f4,axiom,
    ! [X0,X1] : difference(X0,product(X0,X1)) = X1,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos04) ).

fof(f5,axiom,
    ! [X0,X1] : quotient(product(X0,X1),X1) = X0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos05) ).

fof(f6,axiom,
    ! [X0,X1] : product(quotient(X0,X1),X1) = X0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos06) ).

fof(f7,axiom,
    ! [X2,X0,X1] : difference(X0,product(product(X0,X1),X2)) = quotient(product(X1,product(X2,X0)),X0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos07) ).

fof(f8,axiom,
    ! [X2,X0,X1] : difference(product(X0,X1),product(X0,product(X1,X2))) = quotient(quotient(product(X2,product(X0,X1)),X1),X0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos08) ).

fof(f9,negated_conjecture,
    ! [X0] : i(X0) = difference(X0,one),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos09) ).

fof(f10,negated_conjecture,
    ! [X0] : j(X0) = quotient(one,X0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos10) ).

fof(f11,negated_conjecture,
    ! [X0] : product(i(X0),X0) = product(X0,j(X0)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos11) ).

fof(f12,axiom,
    ! [X0] : eta(X0) = product(i(X0),X0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos12) ).

fof(f13,plain,
    ! [X0] : product(i(X0),X0) = eta(X0),
    inference(reorient_equations,[],[f12]) ).

fof(f14,negated_conjecture,
    product(i(i(x0)),x1) != product(eta(x0),product(x0,x1)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).

fof(f15,plain,
    ! [X0] : eta(X0) = product(difference(X0,one),X0),
    inference(definition_unfolding,[],[f13,f9]) ).

fof(f16,plain,
    ! [X0] : product(difference(X0,one),X0) = product(X0,quotient(one,X0)),
    inference(definition_unfolding,[],[f11,f9,f10]) ).

fof(f17,plain,
    product(difference(difference(x0,one),one),x1) != product(product(difference(x0,one),x0),product(x0,x1)),
    inference(definition_unfolding,[],[f14,f9,f9,f15]) ).

fof(f18,definition,
    sF0 = difference(x0,one),
    introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).

fof(f19,plain,
    difference(x0,one) = sF0,
    inference(reorient_equations,[],[f18]) ).

fof(f20,definition,
    sF1 = difference(sF0,one),
    introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).

fof(f21,plain,
    difference(sF0,one) = sF1,
    inference(reorient_equations,[],[f20]) ).

fof(f22,definition,
    sF2 = product(sF1,x1),
    introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).

fof(f23,plain,
    product(sF1,x1) = sF2,
    inference(reorient_equations,[],[f22]) ).

fof(f24,definition,
    sF3 = product(sF0,x0),
    introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).

fof(f25,plain,
    product(sF0,x0) = sF3,
    inference(reorient_equations,[],[f24]) ).

fof(f26,definition,
    sF4 = product(x0,x1),
    introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).

fof(f27,plain,
    product(x0,x1) = sF4,
    inference(reorient_equations,[],[f26]) ).

fof(f28,definition,
    sF5 = product(sF3,sF4),
    introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).

fof(f29,plain,
    product(sF3,sF4) = sF5,
    inference(reorient_equations,[],[f28]) ).

fof(f30,plain,
    sF2 != sF5,
    inference(definition_folding,[],[f17,f29,f27,f25,f19,f23,f21,f19]) ).

fof(f31,plain,
    ! [X2,X0,X1] : difference(product(X0,X1),product(X0,product(X1,X2))) = quotient(difference(X1,product(product(X1,X2),X0)),X0),
    inference(backward_demodulation,[],[f8,f7]) ).

fof(f32,plain,
    one = product(x0,sF0),
    inference(superposition,[],[f3,f19]) ).

fof(f33,plain,
    x1 = difference(x0,sF4),
    inference(superposition,[],[f4,f27]) ).

fof(f34,plain,
    product(sF0,x0) = product(x0,quotient(one,x0)),
    inference(superposition,[],[f16,f19]) ).

fof(f36,plain,
    sF3 = product(x0,quotient(one,x0)),
    inference(forward_demodulation,[],[f34,f25]) ).

fof(f37,plain,
    product(sF0,quotient(one,sF0)) = product(sF1,sF0),
    inference(superposition,[],[f16,f21]) ).

fof(f38,plain,
    one = product(sF0,sF1),
    inference(superposition,[],[f3,f21]) ).

fof(f39,plain,
    x0 = difference(sF0,sF3),
    inference(superposition,[],[f4,f25]) ).

fof(f40,plain,
    x1 = difference(sF1,sF2),
    inference(superposition,[],[f4,f23]) ).

fof(f41,plain,
    sF4 = difference(sF3,sF5),
    inference(superposition,[],[f4,f29]) ).

fof(f42,plain,
    ! [X2,X0,X1] : difference(product(X1,X2),product(X1,X0)) = quotient(difference(X2,product(X0,X1)),X1),
    inference(superposition,[],[f31,f3]) ).

fof(f50,plain,
    ! [X0] : one = difference(X0,X0),
    inference(superposition,[],[f4,f1]) ).

fof(f62,plain,
    ! [X0] : difference(one,X0) = X0,
    inference(superposition,[],[f3,f2]) ).

fof(f63,plain,
    ! [X2,X0,X1] : difference(difference(X1,X0),product(product(difference(X1,X0),X2),X1)) = quotient(product(X2,X0),difference(X1,X0)),
    inference(superposition,[],[f7,f3]) ).

fof(f68,plain,
    ! [X0] : difference(x0,product(product(x0,X0),sF0)) = quotient(product(X0,sF3),x0),
    inference(superposition,[],[f7,f25]) ).

fof(f79,plain,
    ! [X0,X1] : quotient(X0,difference(X1,X0)) = X1,
    inference(superposition,[],[f5,f3]) ).

fof(f80,plain,
    ! [X0] : quotient(X0,one) = X0,
    inference(superposition,[],[f5,f1]) ).

fof(f82,plain,
    ! [X0] : difference(X0,one) = quotient(product(X0,quotient(one,X0)),X0),
    inference(superposition,[],[f5,f16]) ).

fof(f84,plain,
    sF0 = quotient(sF3,x0),
    inference(superposition,[],[f5,f25]) ).

fof(f86,plain,
    sF3 = quotient(sF5,sF4),
    inference(superposition,[],[f5,f29]) ).

fof(f87,plain,
    ! [X2,X0,X1] : difference(product(difference(X1,X0),X2),product(difference(X1,X0),X1)) = quotient(difference(X2,X0),difference(X1,X0)),
    inference(superposition,[],[f42,f3]) ).

fof(f89,plain,
    ! [X0,X1] : difference(product(X0,X1),product(X0,one)) = quotient(difference(X1,X0),X0),
    inference(superposition,[],[f42,f2]) ).

fof(f92,plain,
    ! [X0] : difference(product(x0,X0),product(x0,sF0)) = quotient(difference(X0,sF3),x0),
    inference(superposition,[],[f42,f25]) ).

fof(f96,plain,
    ! [X0,X1] : quotient(one,X0) = difference(product(X0,product(X1,X0)),product(X0,X1)),
    inference(superposition,[],[f42,f50]) ).

fof(f98,plain,
    ! [X0] : quotient(difference(X0,sF3),x0) = difference(product(x0,X0),one),
    inference(forward_demodulation,[],[f92,f32]) ).

fof(f100,plain,
    ! [X0,X1] : quotient(difference(X1,X0),X0) = difference(product(X0,X1),X0),
    inference(forward_demodulation,[],[f89,f1]) ).

fof(f105,plain,
    x0 = quotient(one,sF0),
    inference(superposition,[],[f79,f19]) ).

fof(f106,plain,
    sF0 = quotient(one,sF1),
    inference(superposition,[],[f79,f21]) ).

fof(f107,plain,
    product(sF0,x0) = product(sF1,sF0),
    inference(backward_demodulation,[],[f37,f105]) ).

fof(f108,plain,
    sF3 = product(sF1,sF0),
    inference(forward_demodulation,[],[f107,f25]) ).

fof(f109,plain,
    ! [X0] : difference(product(sF0,X0),product(sF0,sF1)) = quotient(difference(X0,sF3),sF0),
    inference(superposition,[],[f42,f108]) ).

fof(f110,plain,
    sF1 = quotient(sF3,sF0),
    inference(superposition,[],[f5,f108]) ).

fof(f112,plain,
    sF0 = difference(sF1,sF3),
    inference(superposition,[],[f4,f108]) ).

fof(f113,plain,
    ! [X0] : quotient(difference(X0,sF3),sF0) = difference(product(sF0,X0),one),
    inference(forward_demodulation,[],[f109,f38]) ).

fof(f116,plain,
    ! [X2,X0,X1] : product(X1,product(X2,X0)) = product(difference(X0,product(product(X0,X1),X2)),X0),
    inference(superposition,[],[f6,f7]) ).

fof(f117,plain,
    ! [X2,X0,X1] : difference(X1,product(X2,X0)) = product(difference(product(X0,X1),product(X0,X2)),X0),
    inference(superposition,[],[f6,f42]) ).

fof(f120,plain,
    ! [X2,X0,X1] : difference(product(X1,X2),product(X1,quotient(X0,X1))) = quotient(difference(X2,X0),X1),
    inference(superposition,[],[f42,f6]) ).

fof(f121,plain,
    ! [X2,X0,X1] : difference(X1,product(product(X1,X2),quotient(X0,X1))) = quotient(product(X2,X0),X1),
    inference(superposition,[],[f7,f6]) ).

fof(f122,plain,
    ! [X0,X1] : difference(quotient(X0,X1),X0) = X1,
    inference(superposition,[],[f4,f6]) ).

fof(f124,plain,
    ! [X2,X0,X1] : quotient(X0,X1) = difference(X1,product(product(X1,quotient(X0,product(X2,X1))),X2)),
    inference(superposition,[],[f7,f6]) ).

fof(f125,plain,
    ! [X2,X0,X1] : difference(difference(X1,X0),product(X2,X1)) = product(difference(X0,product(X1,X2)),X1),
    inference(superposition,[],[f117,f3]) ).

fof(f132,plain,
    ! [X0] : difference(x0,product(X0,sF0)) = product(difference(sF3,product(sF0,X0)),sF0),
    inference(superposition,[],[f117,f25]) ).

fof(f134,plain,
    ! [X0] : difference(sF0,product(X0,sF1)) = product(difference(sF3,product(sF1,X0)),sF1),
    inference(superposition,[],[f117,f108]) ).

fof(f136,plain,
    ! [X2,X0,X1] : difference(X1,product(difference(X2,X0),X2)) = product(difference(product(X2,X1),X0),X2),
    inference(superposition,[],[f117,f3]) ).

fof(f143,plain,
    ! [X0] : difference(X0,product(x0,sF0)) = product(difference(product(sF0,X0),sF3),sF0),
    inference(superposition,[],[f117,f25]) ).

fof(f145,plain,
    ! [X0] : difference(X0,product(sF0,sF1)) = product(difference(product(sF1,X0),sF3),sF1),
    inference(superposition,[],[f117,f108]) ).

fof(f158,plain,
    ! [X0] : difference(X0,one) = product(difference(product(sF1,X0),sF3),sF1),
    inference(forward_demodulation,[],[f145,f38]) ).

fof(f159,plain,
    ! [X0] : difference(X0,one) = product(difference(product(sF0,X0),sF3),sF0),
    inference(forward_demodulation,[],[f143,f32]) ).

fof(f163,plain,
    ! [X2,X0,X1] : quotient(difference(X2,X0),difference(X1,X0)) = product(difference(product(X1,product(difference(X1,X0),X2)),X0),X1),
    inference(backward_demodulation,[],[f87,f136]) ).

fof(f166,plain,
    ! [X2,X0,X1] : quotient(product(X2,X0),difference(X1,X0)) = product(difference(X0,product(X1,product(difference(X1,X0),X2))),X1),
    inference(backward_demodulation,[],[f63,f125]) ).

fof(f173,plain,
    ! [X0] : quotient(product(X0,one),sF0) = product(difference(one,product(x0,product(sF0,X0))),x0),
    inference(superposition,[],[f166,f19]) ).

fof(f174,plain,
    ! [X0] : quotient(product(X0,one),sF1) = product(difference(one,product(sF0,product(sF1,X0))),sF0),
    inference(superposition,[],[f166,f21]) ).

fof(f189,plain,
    ! [X2,X0,X1] : difference(X1,product(X2,product(difference(X2,X1),X0))) = quotient(quotient(product(X0,X1),difference(X2,X1)),X2),
    inference(superposition,[],[f5,f166]) ).

fof(f203,plain,
    ! [X0] : quotient(product(X0,one),sF1) = product(product(sF0,product(sF1,X0)),sF0),
    inference(forward_demodulation,[],[f174,f62]) ).

fof(f204,plain,
    ! [X0] : quotient(product(X0,one),sF0) = product(product(x0,product(sF0,X0)),x0),
    inference(forward_demodulation,[],[f173,f62]) ).

fof(f213,plain,
    ! [X0] : product(product(sF0,product(sF1,X0)),sF0) = quotient(X0,sF1),
    inference(forward_demodulation,[],[f203,f1]) ).

fof(f214,plain,
    ! [X0] : product(product(x0,product(sF0,X0)),x0) = quotient(X0,sF0),
    inference(forward_demodulation,[],[f204,f1]) ).

fof(f222,plain,
    ! [X2,X0,X1] : product(difference(X1,X0),product(X2,X1)) = product(difference(X1,product(X0,X2)),X1),
    inference(superposition,[],[f116,f3]) ).

fof(f242,plain,
    ! [X2,X3,X0,X1] : difference(product(X2,X3),product(X2,difference(X2,product(product(X2,X0),X1)))) = quotient(difference(X3,product(X0,product(X1,X2))),X2),
    inference(superposition,[],[f42,f116]) ).

fof(f249,plain,
    ! [X2,X3,X0,X1] : quotient(difference(X3,product(X0,product(X1,X2))),X2) = difference(product(X2,X3),product(product(X2,X0),X1)),
    inference(forward_demodulation,[],[f242,f3]) ).

fof(f287,plain,
    ! [X2,X0,X1] : quotient(product(difference(X1,X0),X2),X1) = difference(X1,product(X0,quotient(X2,X1))),
    inference(superposition,[],[f121,f3]) ).

fof(f293,plain,
    ! [X2,X0,X1] : quotient(product(X1,X2),quotient(X0,X1)) = difference(quotient(X0,X1),product(X0,quotient(X2,quotient(X0,X1)))),
    inference(superposition,[],[f121,f6]) ).

fof(f308,plain,
    ! [X2,X0,X1] : product(product(X2,X0),quotient(X1,X2)) = product(X2,quotient(product(X0,X1),X2)),
    inference(superposition,[],[f3,f121]) ).

fof(f324,plain,
    quotient(one,x0) = difference(x0,sF3),
    inference(superposition,[],[f4,f36]) ).

fof(f329,plain,
    ! [X0] : difference(X0,product(quotient(one,x0),x0)) = product(difference(product(x0,X0),sF3),x0),
    inference(superposition,[],[f117,f36]) ).

fof(f330,plain,
    ! [X0] : difference(X0,one) = product(difference(product(x0,X0),sF3),x0),
    inference(forward_demodulation,[],[f329,f6]) ).

fof(f339,plain,
    ! [X0] : difference(difference(x0,X0),one) = product(difference(X0,sF3),x0),
    inference(superposition,[],[f330,f3]) ).

fof(f343,plain,
    ! [X0] : difference(product(x0,X0),sF3) = quotient(difference(X0,one),x0),
    inference(superposition,[],[f5,f330]) ).

fof(f380,plain,
    quotient(one,sF0) = difference(product(sF0,sF3),one),
    inference(superposition,[],[f113,f50]) ).

fof(f383,plain,
    ! [X0] : difference(X0,sF3) = product(difference(product(sF0,X0),one),sF0),
    inference(superposition,[],[f6,f113]) ).

fof(f386,plain,
    x0 = difference(product(sF0,sF3),one),
    inference(forward_demodulation,[],[f380,f105]) ).

fof(f389,plain,
    difference(sF0,one) = product(difference(one,sF3),x0),
    inference(superposition,[],[f339,f19]) ).

fof(f398,plain,
    difference(sF0,one) = product(sF3,x0),
    inference(forward_demodulation,[],[f389,f62]) ).

fof(f400,plain,
    sF1 = product(sF3,x0),
    inference(forward_demodulation,[],[f398,f21]) ).

fof(f401,plain,
    x0 = difference(sF3,sF1),
    inference(superposition,[],[f4,f400]) ).

fof(f402,plain,
    sF3 = quotient(sF1,x0),
    inference(superposition,[],[f5,f400]) ).

fof(f403,plain,
    ! [X0] : difference(x0,product(product(x0,X0),sF3)) = quotient(product(X0,sF1),x0),
    inference(superposition,[],[f7,f400]) ).

fof(f405,plain,
    ! [X0] : difference(x0,product(X0,sF3)) = product(difference(sF1,product(sF3,X0)),sF3),
    inference(superposition,[],[f117,f400]) ).

fof(f422,plain,
    ! [X0] : product(sF4,quotient(X0,x0)) = product(x0,quotient(product(x1,X0),x0)),
    inference(superposition,[],[f308,f27]) ).

fof(f423,plain,
    ! [X0] : product(sF3,quotient(X0,sF0)) = product(sF0,quotient(product(x0,X0),sF0)),
    inference(superposition,[],[f308,f25]) ).

fof(f425,plain,
    ! [X0] : product(sF3,quotient(X0,sF1)) = product(sF1,quotient(product(sF0,X0),sF1)),
    inference(superposition,[],[f308,f108]) ).

fof(f427,plain,
    ! [X0] : product(sF3,quotient(product(x0,X0),sF3)) = product(sF1,quotient(X0,sF3)),
    inference(superposition,[],[f308,f400]) ).

fof(f431,plain,
    ! [X0] : product(product(x0,X0),difference(x0,sF3)) = product(x0,quotient(product(X0,one),x0)),
    inference(superposition,[],[f308,f324]) ).

fof(f436,plain,
    ! [X0] : product(product(x0,X0),sF3) = product(x0,quotient(product(X0,sF1),x0)),
    inference(superposition,[],[f308,f402]) ).

fof(f448,plain,
    ! [X0] : product(product(x0,X0),difference(x0,sF3)) = product(x0,quotient(X0,x0)),
    inference(forward_demodulation,[],[f431,f1]) ).

fof(f462,plain,
    ! [X0] : quotient(difference(X0,one),sF0) = product(difference(product(x0,product(sF0,X0)),one),x0),
    inference(superposition,[],[f163,f19]) ).

fof(f463,plain,
    ! [X0] : quotient(difference(X0,one),sF1) = product(difference(product(sF0,product(sF1,X0)),one),sF0),
    inference(superposition,[],[f163,f21]) ).

fof(f502,plain,
    ! [X0] : difference(product(sF1,X0),sF3) = quotient(difference(X0,one),sF1),
    inference(forward_demodulation,[],[f463,f383]) ).

fof(f515,plain,
    quotient(one,x0) = difference(product(x0,sF3),one),
    inference(superposition,[],[f98,f50]) ).

fof(f517,plain,
    difference(product(x0,sF1),one) = quotient(sF0,x0),
    inference(superposition,[],[f98,f112]) ).

fof(f519,plain,
    ! [X0] : difference(X0,sF3) = product(difference(product(x0,X0),one),x0),
    inference(superposition,[],[f6,f98]) ).

fof(f520,plain,
    ! [X0] : difference(product(sF0,X0),sF3) = quotient(difference(X0,one),sF0),
    inference(backward_demodulation,[],[f462,f519]) ).

fof(f522,plain,
    difference(x0,sF3) = difference(product(x0,sF3),one),
    inference(forward_demodulation,[],[f515,f324]) ).

fof(f542,plain,
    ! [X0,X1] : quotient(one,X1) = difference(product(X1,product(difference(X1,X0),X1)),X0),
    inference(superposition,[],[f96,f3]) ).

fof(f543,plain,
    ! [X0] : quotient(one,X0) = difference(product(X0,product(one,X0)),X0),
    inference(superposition,[],[f96,f1]) ).

fof(f574,plain,
    ! [X0] : quotient(one,X0) = difference(product(X0,X0),X0),
    inference(forward_demodulation,[],[f543,f2]) ).

fof(f628,plain,
    ! [X0,X1] : product(X0,product(difference(X0,X1),X0)) = quotient(X1,quotient(one,X0)),
    inference(superposition,[],[f79,f542]) ).

fof(f695,plain,
    quotient(x0,sF0) = product(product(x0,sF3),x0),
    inference(superposition,[],[f214,f25]) ).

fof(f696,plain,
    ! [X0] : quotient(difference(sF0,X0),sF0) = product(product(x0,X0),x0),
    inference(superposition,[],[f214,f3]) ).

fof(f719,plain,
    ! [X0] : product(difference(one,product(x0,X0)),x0) = difference(sF0,product(X0,x0)),
    inference(superposition,[],[f125,f19]) ).

fof(f720,plain,
    ! [X0] : product(difference(one,product(sF0,X0)),sF0) = difference(sF1,product(X0,sF0)),
    inference(superposition,[],[f125,f21]) ).

fof(f725,plain,
    ! [X0,X1] : product(difference(X1,product(X0,one)),X0) = difference(difference(X0,X1),X0),
    inference(superposition,[],[f125,f2]) ).

fof(f728,plain,
    ! [X0,X1] : product(difference(X1,product(X0,difference(X0,one))),X0) = difference(difference(X0,X1),product(X0,quotient(one,X0))),
    inference(superposition,[],[f125,f16]) ).

fof(f734,plain,
    ! [X2,X0,X1] : difference(difference(X1,X2),X0) = product(difference(X2,product(X1,quotient(X0,X1))),X1),
    inference(superposition,[],[f125,f6]) ).

fof(f736,plain,
    ! [X0] : product(difference(X0,product(x0,sF0)),x0) = difference(difference(x0,X0),sF3),
    inference(superposition,[],[f125,f25]) ).

fof(f752,plain,
    ! [X0] : difference(difference(x0,X0),sF3) = product(difference(X0,one),x0),
    inference(forward_demodulation,[],[f736,f32]) ).

fof(f754,plain,
    ! [X0,X1] : difference(difference(X0,X1),product(X0,quotient(one,X0))) = product(difference(X1,one),X0),
    inference(forward_demodulation,[],[f728,f3]) ).

fof(f755,plain,
    ! [X0,X1] : product(difference(X1,X0),X0) = difference(difference(X0,X1),X0),
    inference(forward_demodulation,[],[f725,f1]) ).

fof(f758,plain,
    ! [X0] : difference(sF1,product(X0,sF0)) = product(product(sF0,X0),sF0),
    inference(forward_demodulation,[],[f720,f62]) ).

fof(f759,plain,
    ! [X0] : product(product(x0,X0),x0) = difference(sF0,product(X0,x0)),
    inference(forward_demodulation,[],[f719,f62]) ).

fof(f773,plain,
    product(product(sF0,one),sF0) = difference(sF1,sF0),
    inference(superposition,[],[f758,f2]) ).

fof(f778,plain,
    ! [X0] : product(product(sF0,quotient(X0,sF0)),sF0) = difference(sF1,X0),
    inference(superposition,[],[f758,f6]) ).

fof(f787,plain,
    ! [X0] : product(X0,sF0) = product(sF1,product(product(sF0,X0),sF0)),
    inference(superposition,[],[f3,f758]) ).

fof(f793,plain,
    difference(sF1,sF0) = product(sF0,sF0),
    inference(forward_demodulation,[],[f773,f1]) ).

fof(f799,plain,
    product(product(x0,one),x0) = difference(sF0,x0),
    inference(superposition,[],[f759,f2]) ).

fof(f800,plain,
    ! [X0] : product(product(x0,product(x0,product(sF0,X0))),x0) = difference(sF0,quotient(X0,sF0)),
    inference(superposition,[],[f759,f214]) ).

fof(f807,plain,
    ! [X0] : difference(sF0,X0) = product(product(x0,quotient(X0,x0)),x0),
    inference(superposition,[],[f759,f6]) ).

fof(f809,plain,
    product(product(x0,sF3),x0) = difference(sF0,sF1),
    inference(superposition,[],[f759,f400]) ).

fof(f817,plain,
    ! [X0] : product(X0,x0) = product(sF0,product(product(x0,X0),x0)),
    inference(superposition,[],[f3,f759]) ).

fof(f821,plain,
    quotient(x0,sF0) = difference(sF0,sF1),
    inference(backward_demodulation,[],[f695,f809]) ).

fof(f825,plain,
    difference(sF0,x0) = product(x0,x0),
    inference(forward_demodulation,[],[f799,f1]) ).

fof(f834,plain,
    ! [X0,X1] : difference(sF0,product(X0,product(X1,x0))) = product(product(x0,difference(x0,product(product(x0,X0),X1))),x0),
    inference(superposition,[],[f807,f7]) ).

fof(f841,plain,
    ! [X0] : product(x0,quotient(X0,x0)) = quotient(difference(sF0,X0),x0),
    inference(superposition,[],[f5,f807]) ).

fof(f851,plain,
    ! [X0,X1] : difference(sF0,product(X0,product(X1,x0))) = product(product(product(x0,X0),X1),x0),
    inference(forward_demodulation,[],[f834,f3]) ).

fof(f858,plain,
    ! [X0] : product(difference(x0,X0),x0) = product(sF0,product(X0,x0)),
    inference(superposition,[],[f817,f3]) ).

fof(f859,plain,
    product(one,x0) = product(sF0,product(x0,x0)),
    inference(superposition,[],[f817,f1]) ).

fof(f860,plain,
    ! [X0] : product(sF0,quotient(X0,sF0)) = product(product(sF0,X0),x0),
    inference(superposition,[],[f817,f214]) ).

fof(f881,plain,
    x0 = product(sF0,product(x0,x0)),
    inference(forward_demodulation,[],[f859,f2]) ).

fof(f938,plain,
    ! [X0] : product(product(product(x0,X0),x0),sF0) = product(sF1,product(product(X0,x0),sF0)),
    inference(superposition,[],[f787,f817]) ).

fof(f939,plain,
    ! [X0] : product(difference(sF0,X0),sF0) = product(sF1,product(X0,sF0)),
    inference(superposition,[],[f787,f3]) ).

fof(f949,plain,
    ! [X0,X1] : difference(X1,product(product(product(sF0,X0),sF0),sF1)) = product(difference(product(sF1,X1),product(X0,sF0)),sF1),
    inference(superposition,[],[f117,f787]) ).

fof(f1037,plain,
    product(sF1,product(x0,sF0)) = product(product(x0,x0),sF0),
    inference(superposition,[],[f939,f825]) ).

fof(f1043,plain,
    product(sF1,one) = product(product(x0,x0),sF0),
    inference(forward_demodulation,[],[f1037,f32]) ).

fof(f1045,plain,
    sF1 = product(product(x0,x0),sF0),
    inference(forward_demodulation,[],[f1043,f1]) ).

fof(f1063,plain,
    x0 = product(difference(sF0,sF1),sF0),
    inference(superposition,[],[f6,f821]) ).

fof(f1064,plain,
    x0 = product(sF1,product(sF1,sF0)),
    inference(forward_demodulation,[],[f1063,f939]) ).

fof(f1065,plain,
    x0 = product(sF1,sF3),
    inference(forward_demodulation,[],[f1064,f108]) ).

fof(f1066,plain,
    sF3 = difference(sF1,x0),
    inference(superposition,[],[f4,f1065]) ).

fof(f1067,plain,
    sF1 = quotient(x0,sF3),
    inference(superposition,[],[f5,f1065]) ).

fof(f1068,plain,
    ! [X0] : difference(sF3,product(product(sF3,X0),sF1)) = quotient(product(X0,x0),sF3),
    inference(superposition,[],[f7,f1065]) ).

fof(f1071,plain,
    quotient(one,sF3) = difference(product(sF3,x0),product(sF3,sF1)),
    inference(superposition,[],[f96,f1065]) ).

fof(f1072,plain,
    ! [X0] : difference(sF3,product(X0,sF1)) = product(difference(x0,product(sF1,X0)),sF1),
    inference(superposition,[],[f117,f1065]) ).

fof(f1074,plain,
    ! [X0] : product(difference(X0,product(sF3,sF1)),sF3) = difference(difference(sF3,X0),x0),
    inference(superposition,[],[f125,f1065]) ).

fof(f1076,plain,
    quotient(one,sF3) = difference(sF1,product(sF3,sF1)),
    inference(forward_demodulation,[],[f1071,f400]) ).

fof(f1101,plain,
    product(difference(sF0,one),sF1) = difference(product(sF0,sF0),product(sF1,quotient(one,sF1))),
    inference(superposition,[],[f754,f793]) ).

fof(f1102,plain,
    product(difference(sF3,one),sF1) = difference(sF0,product(sF1,quotient(one,sF1))),
    inference(superposition,[],[f754,f112]) ).

fof(f1125,plain,
    product(difference(sF3,one),sF1) = difference(sF0,product(sF1,sF0)),
    inference(forward_demodulation,[],[f1102,f106]) ).

fof(f1126,plain,
    product(difference(sF0,one),sF1) = difference(product(sF0,sF0),product(sF1,sF0)),
    inference(forward_demodulation,[],[f1101,f106]) ).

fof(f1152,plain,
    difference(sF0,sF3) = product(difference(sF3,one),sF1),
    inference(forward_demodulation,[],[f1125,f108]) ).

fof(f1153,plain,
    product(difference(sF0,one),sF1) = difference(product(sF0,sF0),sF3),
    inference(forward_demodulation,[],[f1126,f108]) ).

fof(f1170,plain,
    x0 = product(difference(sF3,one),sF1),
    inference(forward_demodulation,[],[f1152,f39]) ).

fof(f1171,plain,
    difference(product(sF0,sF0),sF3) = product(sF1,sF1),
    inference(forward_demodulation,[],[f1153,f21]) ).

fof(f1185,plain,
    difference(product(x0,product(sF0,sF0)),one) = quotient(product(sF1,sF1),x0),
    inference(superposition,[],[f98,f1171]) ).

fof(f1203,plain,
    ! [X0] : product(sF0,quotient(X0,sF0)) = quotient(difference(sF1,X0),sF0),
    inference(superposition,[],[f5,f778]) ).

fof(f1240,plain,
    difference(sF0,sF1) = product(difference(sF3,sF1),sF1),
    inference(superposition,[],[f755,f112]) ).

fof(f1241,plain,
    difference(x0,sF3) = product(difference(sF1,sF3),sF3),
    inference(superposition,[],[f755,f401]) ).

fof(f1245,plain,
    ! [X0,X1] : difference(X1,X0) = quotient(X1,product(difference(X0,X1),X1)),
    inference(superposition,[],[f79,f755]) ).

fof(f1246,plain,
    ! [X0,X1] : product(difference(X1,X0),product(difference(X0,X1),X1)) = X1,
    inference(superposition,[],[f3,f755]) ).

fof(f1253,plain,
    difference(x0,sF3) = product(sF0,sF3),
    inference(forward_demodulation,[],[f1241,f112]) ).

fof(f1254,plain,
    product(x0,sF1) = difference(sF0,sF1),
    inference(forward_demodulation,[],[f1240,f401]) ).

fof(f1262,plain,
    quotient(one,x0) = product(sF0,sF3),
    inference(backward_demodulation,[],[f324,f1253]) ).

fof(f1267,plain,
    ! [X0] : product(x0,quotient(X0,x0)) = product(product(x0,X0),product(sF0,sF3)),
    inference(backward_demodulation,[],[f448,f1253]) ).

fof(f1270,plain,
    product(sF0,sF3) = difference(product(x0,sF3),one),
    inference(backward_demodulation,[],[f522,f1253]) ).

fof(f1282,plain,
    difference(product(sF0,x0),one) = quotient(product(sF0,sF3),sF0),
    inference(superposition,[],[f113,f1253]) ).

fof(f1286,plain,
    ! [X0] : quotient(product(X0,sF3),product(sF0,sF3)) = product(difference(sF3,product(x0,product(product(sF0,sF3),X0))),x0),
    inference(superposition,[],[f166,f1253]) ).

fof(f1290,plain,
    difference(sF3,one) = quotient(product(sF0,sF3),sF0),
    inference(forward_demodulation,[],[f1282,f25]) ).

fof(f1359,plain,
    ! [X0] : product(difference(X0,one),product(X0,X0)) = X0,
    inference(superposition,[],[f1246,f62]) ).

fof(f1456,plain,
    ! [X0] : difference(difference(sF1,X0),one) = product(difference(X0,sF3),sF1),
    inference(superposition,[],[f158,f3]) ).

fof(f1546,plain,
    product(product(sF0,x0),sF0) = quotient(sF3,sF1),
    inference(superposition,[],[f213,f1065]) ).

fof(f1547,plain,
    ! [X0] : product(product(sF0,X0),sF0) = quotient(difference(sF1,X0),sF1),
    inference(superposition,[],[f213,f3]) ).

fof(f1549,plain,
    ! [X0] : product(product(sF1,X0),sF0) = product(sF1,quotient(X0,sF1)),
    inference(superposition,[],[f787,f213]) ).

fof(f1552,plain,
    ! [X0] : product(sF0,product(sF1,X0)) = quotient(quotient(X0,sF1),sF0),
    inference(superposition,[],[f5,f213]) ).

fof(f1563,plain,
    product(sF3,sF0) = quotient(sF3,sF1),
    inference(forward_demodulation,[],[f1546,f25]) ).

fof(f1579,plain,
    ! [X0] : product(product(sF0,product(product(x0,X0),x0)),sF0) = difference(sF1,difference(sF0,X0)),
    inference(superposition,[],[f778,f696]) ).

fof(f1581,plain,
    ! [X0] : difference(sF0,X0) = product(product(product(x0,X0),x0),sF0),
    inference(superposition,[],[f6,f696]) ).

fof(f1582,plain,
    ! [X0] : difference(sF0,X0) = product(sF1,product(product(X0,x0),sF0)),
    inference(backward_demodulation,[],[f938,f1581]) ).

fof(f1583,plain,
    ! [X0] : product(product(X0,x0),sF0) = difference(sF1,difference(sF0,X0)),
    inference(forward_demodulation,[],[f1579,f817]) ).

fof(f1595,plain,
    product(product(sF0,x0),sF0) = difference(sF1,one),
    inference(superposition,[],[f758,f32]) ).

fof(f1604,plain,
    ! [X0] : product(difference(X0,product(sF0,x0)),sF0) = difference(difference(sF0,X0),one),
    inference(superposition,[],[f125,f32]) ).

fof(f1605,plain,
    ! [X0] : product(x0,quotient(product(sF0,X0),x0)) = product(one,quotient(X0,x0)),
    inference(superposition,[],[f308,f32]) ).

fof(f1606,plain,
    ! [X0] : quotient(X0,x0) = product(x0,quotient(product(sF0,X0),x0)),
    inference(forward_demodulation,[],[f1605,f2]) ).

fof(f1607,plain,
    ! [X0] : difference(difference(sF0,X0),one) = product(difference(X0,sF3),sF0),
    inference(forward_demodulation,[],[f1604,f25]) ).

fof(f1614,plain,
    product(sF3,sF0) = difference(sF1,one),
    inference(forward_demodulation,[],[f1595,f25]) ).

fof(f1622,plain,
    product(difference(one,sF3),sF1) = difference(product(sF3,sF0),one),
    inference(superposition,[],[f1456,f1614]) ).

fof(f1638,plain,
    product(sF3,sF1) = difference(product(sF3,sF0),one),
    inference(forward_demodulation,[],[f1622,f62]) ).

fof(f1645,plain,
    difference(product(x0,sF1),one) = product(difference(sF1,sF3),sF0),
    inference(superposition,[],[f1607,f1254]) ).

fof(f1663,plain,
    difference(product(x0,sF1),one) = product(sF0,sF0),
    inference(forward_demodulation,[],[f1645,f112]) ).

fof(f1669,plain,
    quotient(sF0,x0) = product(sF0,sF0),
    inference(backward_demodulation,[],[f517,f1663]) ).

fof(f1729,plain,
    ! [X2,X3,X0,X1] : difference(X1,product(X2,product(X3,X0))) = product(difference(product(X0,X1),product(product(X0,X2),X3)),X0),
    inference(superposition,[],[f6,f249]) ).

fof(f1775,plain,
    ! [X0] : difference(X0,one) = quotient(X0,product(X0,X0)),
    inference(superposition,[],[f5,f1359]) ).

fof(f1822,plain,
    ! [X0] : quotient(X0,sF0) = difference(sF0,product(product(sF0,quotient(X0,sF1)),product(x0,x0))),
    inference(superposition,[],[f124,f1045]) ).

fof(f1859,plain,
    ! [X2,X0,X1] : product(X1,quotient(X0,X1)) = product(product(X1,quotient(X0,product(X2,X1))),X2),
    inference(superposition,[],[f3,f124]) ).

fof(f1928,plain,
    ! [X0] : quotient(X0,sF0) = product(product(product(x0,product(sF0,quotient(X0,sF1))),x0),x0),
    inference(forward_demodulation,[],[f1822,f851]) ).

fof(f1958,plain,
    ! [X0] : quotient(X0,sF0) = product(quotient(quotient(X0,sF1),sF0),x0),
    inference(forward_demodulation,[],[f1928,f214]) ).

fof(f1968,plain,
    ! [X0] : quotient(X0,sF0) = product(product(sF0,product(sF1,X0)),x0),
    inference(forward_demodulation,[],[f1958,f1552]) ).

fof(f1971,plain,
    ! [X0] : quotient(X0,sF0) = product(sF0,quotient(product(sF1,X0),sF0)),
    inference(forward_demodulation,[],[f1968,f860]) ).

fof(f1977,plain,
    quotient(one,x0) = product(x0,quotient(sF0,x0)),
    inference(superposition,[],[f841,f50]) ).

fof(f1995,plain,
    quotient(one,x0) = product(x0,product(sF0,sF0)),
    inference(forward_demodulation,[],[f1977,f1669]) ).

fof(f2006,plain,
    product(sF0,sF3) = product(x0,product(sF0,sF0)),
    inference(forward_demodulation,[],[f1995,f1262]) ).

fof(f2011,plain,
    difference(product(sF0,sF3),one) = quotient(product(sF1,sF1),x0),
    inference(backward_demodulation,[],[f1185,f2006]) ).

fof(f2012,plain,
    x0 = quotient(product(sF1,sF1),x0),
    inference(forward_demodulation,[],[f2011,f386]) ).

fof(f2015,plain,
    product(x0,x0) = product(sF1,sF1),
    inference(superposition,[],[f6,f2012]) ).

fof(f2017,plain,
    x0 = product(sF0,product(sF1,sF1)),
    inference(backward_demodulation,[],[f881,f2015]) ).

fof(f2050,plain,
    difference(x0,one) = quotient(x0,product(sF1,sF1)),
    inference(superposition,[],[f1775,f2015]) ).

fof(f2055,plain,
    ! [X0] : quotient(product(X0,product(sF1,sF1)),x0) = difference(x0,product(product(x0,X0),x0)),
    inference(superposition,[],[f7,f2015]) ).

fof(f2063,plain,
    ! [X0] : product(x0,quotient(product(x0,X0),x0)) = product(product(sF1,sF1),quotient(X0,x0)),
    inference(superposition,[],[f308,f2015]) ).

fof(f2069,plain,
    sF0 = quotient(x0,product(sF1,sF1)),
    inference(forward_demodulation,[],[f2050,f19]) ).

fof(f2108,plain,
    quotient(product(sF0,sF3),sF0) = difference(sF0,product(product(sF0,x0),sF0)),
    inference(superposition,[],[f7,f2006]) ).

fof(f2125,plain,
    quotient(product(sF0,sF3),sF0) = difference(sF0,product(sF3,sF0)),
    inference(forward_demodulation,[],[f2108,f25]) ).

fof(f2135,plain,
    difference(sF3,one) = difference(sF0,product(sF3,sF0)),
    inference(forward_demodulation,[],[f2125,f1290]) ).

fof(f2152,plain,
    difference(sF3,one) = quotient(x0,sF1),
    inference(superposition,[],[f5,f1170]) ).

fof(f2178,plain,
    ! [X0] : difference(sF0,product(x0,product(sF0,X0))) = product(sF1,product(quotient(X0,sF0),sF0)),
    inference(superposition,[],[f1582,f214]) ).

fof(f2181,plain,
    ! [X0] : difference(sF0,difference(x0,X0)) = product(sF1,product(product(sF0,product(X0,x0)),sF0)),
    inference(superposition,[],[f1582,f858]) ).

fof(f2186,plain,
    ! [X0] : product(sF1,product(X0,sF0)) = difference(sF0,quotient(X0,x0)),
    inference(superposition,[],[f1582,f6]) ).

fof(f2192,plain,
    ! [X0] : product(product(sF0,difference(sF0,X0)),sF0) = quotient(product(product(X0,x0),sF0),sF1),
    inference(superposition,[],[f213,f1582]) ).

fof(f2215,plain,
    ! [X0] : product(X0,sF0) = quotient(product(product(X0,x0),sF0),sF1),
    inference(forward_demodulation,[],[f2192,f3]) ).

fof(f2222,plain,
    ! [X0] : product(product(X0,x0),sF0) = difference(sF0,difference(x0,X0)),
    inference(forward_demodulation,[],[f2181,f787]) ).

fof(f2224,plain,
    ! [X0] : product(sF1,X0) = difference(sF0,product(x0,product(sF0,X0))),
    inference(forward_demodulation,[],[f2178,f6]) ).

fof(f2240,plain,
    ! [X0] : product(sF1,difference(sF0,X0)) = difference(sF0,product(x0,X0)),
    inference(superposition,[],[f2224,f3]) ).

fof(f2250,plain,
    ! [X0] : product(x0,product(sF0,X0)) = product(sF0,product(sF1,X0)),
    inference(superposition,[],[f3,f2224]) ).

fof(f2270,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = product(product(x0,product(sF0,product(sF1,X0))),x0),
    inference(backward_demodulation,[],[f800,f2250]) ).

fof(f2297,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = product(product(sF0,product(sF1,product(sF1,X0))),x0),
    inference(forward_demodulation,[],[f2270,f2250]) ).

fof(f2306,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = product(sF0,quotient(product(sF1,product(sF1,X0)),sF0)),
    inference(forward_demodulation,[],[f2297,f860]) ).

fof(f2308,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = quotient(product(sF1,X0),sF0),
    inference(forward_demodulation,[],[f2306,f1971]) ).

fof(f2325,plain,
    ! [X0] : product(x0,X0) = product(sF0,product(sF1,difference(sF0,X0))),
    inference(superposition,[],[f3,f2240]) ).

fof(f2406,plain,
    ! [X0] : quotient(X0,x0) = product(sF0,product(sF1,product(X0,sF0))),
    inference(superposition,[],[f3,f2186]) ).

fof(f2519,plain,
    ! [X2,X0,X1] : product(X0,quotient(X1,product(X2,X0))) = quotient(product(X0,quotient(X1,X0)),X2),
    inference(superposition,[],[f5,f1859]) ).

fof(f2538,plain,
    ! [X0] : difference(X0,one) = product(X0,quotient(one,product(X0,X0))),
    inference(backward_demodulation,[],[f82,f2519]) ).

fof(f2582,plain,
    ! [X0] : quotient(one,product(X0,X0)) = difference(X0,difference(X0,one)),
    inference(superposition,[],[f4,f2538]) ).

fof(f2676,plain,
    quotient(one,product(sF1,sF1)) = difference(x0,difference(x0,one)),
    inference(superposition,[],[f2582,f2015]) ).

fof(f2684,plain,
    difference(x0,sF0) = quotient(one,product(sF1,sF1)),
    inference(forward_demodulation,[],[f2676,f19]) ).

fof(f2687,plain,
    difference(x0,sF0) = difference(sF1,difference(sF1,one)),
    inference(forward_demodulation,[],[f2684,f2582]) ).

fof(f2690,plain,
    difference(x0,sF0) = difference(sF1,product(sF3,sF0)),
    inference(forward_demodulation,[],[f2687,f1614]) ).

fof(f2691,plain,
    difference(x0,sF0) = product(product(sF0,sF3),sF0),
    inference(forward_demodulation,[],[f2690,f758]) ).

fof(f2706,plain,
    product(sF0,sF3) = quotient(difference(x0,sF0),sF0),
    inference(superposition,[],[f5,f2691]) ).

fof(f2718,plain,
    product(sF0,sF3) = difference(product(sF0,x0),sF0),
    inference(forward_demodulation,[],[f2706,f100]) ).

fof(f2720,plain,
    product(sF0,sF3) = difference(sF3,sF0),
    inference(forward_demodulation,[],[f2718,f25]) ).

fof(f2722,plain,
    sF0 = product(sF3,product(sF0,sF3)),
    inference(superposition,[],[f3,f2720]) ).

fof(f2727,plain,
    difference(product(sF0,sF3),sF3) = product(difference(sF0,sF3),sF3),
    inference(superposition,[],[f755,f2720]) ).

fof(f2732,plain,
    product(x0,sF3) = difference(product(sF0,sF3),sF3),
    inference(forward_demodulation,[],[f2727,f39]) ).

fof(f2803,plain,
    ! [X2,X0,X1] : quotient(X0,X1) = difference(product(X1,quotient(product(X2,X1),X0)),product(X1,X2)),
    inference(superposition,[],[f42,f122]) ).

fof(f2814,plain,
    ! [X0,X1] : difference(product(product(X1,X0),X1),product(X1,X0)) = quotient(X0,product(X1,X0)),
    inference(superposition,[],[f100,f4]) ).

fof(f2827,plain,
    ! [X0,X1] : quotient(X0,X1) = difference(product(X1,quotient(X1,X0)),X1),
    inference(superposition,[],[f100,f122]) ).

fof(f2841,plain,
    difference(product(sF3,sF1),sF3) = quotient(sF0,sF3),
    inference(superposition,[],[f100,f112]) ).

fof(f2842,plain,
    quotient(x0,sF1) = difference(product(sF1,sF3),sF1),
    inference(superposition,[],[f100,f401]) ).

fof(f2843,plain,
    quotient(product(sF0,sF3),sF0) = difference(product(sF0,sF3),sF0),
    inference(superposition,[],[f100,f2720]) ).

fof(f2862,plain,
    difference(sF3,one) = difference(product(sF0,sF3),sF0),
    inference(forward_demodulation,[],[f2843,f1290]) ).

fof(f2863,plain,
    difference(x0,sF1) = quotient(x0,sF1),
    inference(forward_demodulation,[],[f2842,f1065]) ).

fof(f2882,plain,
    difference(sF3,one) = difference(x0,sF1),
    inference(forward_demodulation,[],[f2863,f2152]) ).

fof(f2900,plain,
    product(difference(sF1,one),x0) = difference(difference(sF3,one),sF3),
    inference(superposition,[],[f752,f2882]) ).

fof(f2902,plain,
    product(difference(sF1,sF3),x0) = difference(difference(sF3,one),one),
    inference(superposition,[],[f339,f2882]) ).

fof(f2903,plain,
    sF1 = product(x0,difference(sF3,one)),
    inference(superposition,[],[f3,f2882]) ).

fof(f2916,plain,
    product(sF0,x0) = difference(difference(sF3,one),one),
    inference(forward_demodulation,[],[f2902,f112]) ).

fof(f2918,plain,
    product(difference(sF1,one),x0) = product(difference(one,sF3),sF3),
    inference(forward_demodulation,[],[f2900,f755]) ).

fof(f2923,plain,
    sF3 = difference(difference(sF3,one),one),
    inference(forward_demodulation,[],[f2916,f25]) ).

fof(f2924,plain,
    product(sF3,sF3) = product(difference(sF1,one),x0),
    inference(forward_demodulation,[],[f2918,f62]) ).

fof(f2926,plain,
    product(sF3,sF3) = product(product(sF3,sF0),x0),
    inference(forward_demodulation,[],[f2924,f1614]) ).

fof(f2930,plain,
    quotient(one,sF3) = difference(sF3,one),
    inference(superposition,[],[f79,f2923]) ).

fof(f2944,plain,
    difference(sF1,product(sF3,sF1)) = difference(sF3,one),
    inference(backward_demodulation,[],[f1076,f2930]) ).

fof(f3196,plain,
    ! [X0] : product(product(x0,X0),sF0) = product(x0,quotient(product(X0,sF3),x0)),
    inference(superposition,[],[f308,f84]) ).

fof(f3290,plain,
    ! [X0] : product(X0,product(sF0,sF3)) = product(x0,quotient(difference(x0,X0),x0)),
    inference(superposition,[],[f1267,f3]) ).

fof(f3295,plain,
    ! [X0] : difference(sF3,product(product(sF3,product(x0,X0)),sF0)) = quotient(product(x0,quotient(X0,x0)),sF3),
    inference(superposition,[],[f7,f1267]) ).

fof(f3311,plain,
    ! [X0] : product(x0,quotient(X0,product(sF3,x0))) = difference(sF3,product(product(sF3,product(x0,X0)),sF0)),
    inference(forward_demodulation,[],[f3295,f2519]) ).

fof(f3320,plain,
    ! [X0] : product(x0,quotient(X0,sF1)) = difference(sF3,product(product(sF3,product(x0,X0)),sF0)),
    inference(forward_demodulation,[],[f3311,f400]) ).

fof(f3343,plain,
    ! [X0] : difference(sF0,difference(x0,X0)) = product(product(X0,product(sF0,sF3)),x0),
    inference(superposition,[],[f807,f3290]) ).

fof(f3346,plain,
    ! [X0] : product(quotient(difference(x0,X0),x0),x0) = product(sF0,product(product(X0,product(sF0,sF3)),x0)),
    inference(superposition,[],[f817,f3290]) ).

fof(f3366,plain,
    ! [X0] : difference(x0,X0) = product(sF0,product(product(X0,product(sF0,sF3)),x0)),
    inference(forward_demodulation,[],[f3346,f6]) ).

fof(f3368,plain,
    ! [X0] : product(product(X0,x0),sF0) = product(product(X0,product(sF0,sF3)),x0),
    inference(forward_demodulation,[],[f3343,f2222]) ).

fof(f3378,plain,
    ! [X0] : difference(x0,X0) = product(sF0,product(product(X0,x0),sF0)),
    inference(backward_demodulation,[],[f3366,f3368]) ).

fof(f3403,plain,
    ! [X0] : product(sF0,product(X0,sF0)) = difference(x0,quotient(X0,x0)),
    inference(superposition,[],[f3378,f6]) ).

fof(f3699,plain,
    ! [X0] : difference(x0,product(sF0,X0)) = product(sF0,product(product(sF0,quotient(X0,sF0)),sF0)),
    inference(superposition,[],[f3378,f860]) ).

fof(f3723,plain,
    ! [X0] : difference(x0,product(sF0,X0)) = product(sF0,difference(sF1,X0)),
    inference(forward_demodulation,[],[f3699,f778]) ).

fof(f3752,plain,
    quotient(sF3,sF1) = difference(product(sF1,difference(sF3,one)),sF3),
    inference(superposition,[],[f502,f2923]) ).

fof(f3768,plain,
    product(sF3,sF0) = difference(product(sF1,difference(sF3,one)),sF3),
    inference(forward_demodulation,[],[f3752,f1563]) ).

fof(f3782,plain,
    difference(sF0,product(sF3,sF0)) = product(sF1,product(product(sF3,sF3),sF0)),
    inference(superposition,[],[f1582,f2926]) ).

fof(f3783,plain,
    product(product(x0,product(sF3,sF0)),x0) = difference(sF0,product(sF3,sF3)),
    inference(superposition,[],[f759,f2926]) ).

fof(f3799,plain,
    difference(sF3,one) = product(sF1,product(product(sF3,sF3),sF0)),
    inference(forward_demodulation,[],[f3782,f2135]) ).

fof(f3858,plain,
    quotient(difference(sF3,one),sF0) = product(product(x0,product(sF3,sF0)),x0),
    inference(superposition,[],[f696,f2135]) ).

fof(f3862,plain,
    product(sF3,sF0) = product(sF0,difference(sF3,one)),
    inference(superposition,[],[f3,f2135]) ).

fof(f3879,plain,
    quotient(difference(sF3,one),sF0) = difference(sF0,product(sF3,sF3)),
    inference(forward_demodulation,[],[f3858,f3783]) ).

fof(f3887,plain,
    difference(product(sF0,sF3),sF3) = difference(sF0,product(sF3,sF3)),
    inference(forward_demodulation,[],[f3879,f520]) ).

fof(f3893,plain,
    product(x0,sF3) = difference(sF0,product(sF3,sF3)),
    inference(forward_demodulation,[],[f3887,f2732]) ).

fof(f3898,plain,
    difference(product(x0,sF3),one) = product(difference(product(sF3,sF3),sF3),sF0),
    inference(superposition,[],[f1607,f3893]) ).

fof(f3901,plain,
    product(sF1,product(product(sF3,sF3),sF0)) = product(product(x0,sF3),sF0),
    inference(superposition,[],[f939,f3893]) ).

fof(f3917,plain,
    difference(sF3,one) = product(product(x0,sF3),sF0),
    inference(forward_demodulation,[],[f3901,f3799]) ).

fof(f3918,plain,
    difference(product(x0,sF3),one) = product(quotient(one,sF3),sF0),
    inference(forward_demodulation,[],[f3898,f574]) ).

fof(f3921,plain,
    difference(product(x0,sF3),one) = product(difference(sF3,one),sF0),
    inference(forward_demodulation,[],[f3918,f2930]) ).

fof(f3924,plain,
    product(sF0,sF3) = product(difference(sF3,one),sF0),
    inference(forward_demodulation,[],[f3921,f1270]) ).

fof(f3927,plain,
    product(x0,product(sF3,sF0)) = product(sF0,product(sF1,difference(sF3,one))),
    inference(superposition,[],[f2250,f3862]) ).

fof(f3956,plain,
    product(sF3,sF1) = product(sF1,difference(sF3,one)),
    inference(superposition,[],[f3,f2944]) ).

fof(f3959,plain,
    ! [X0] : product(difference(product(sF3,sF1),product(sF1,X0)),sF1) = difference(difference(sF3,one),product(X0,sF1)),
    inference(superposition,[],[f125,f2944]) ).

fof(f3961,plain,
    ! [X0] : quotient(product(X0,product(sF3,sF1)),difference(sF3,one)) = product(difference(product(sF3,sF1),product(sF1,product(difference(sF3,one),X0))),sF1),
    inference(superposition,[],[f166,f2944]) ).

fof(f3968,plain,
    ! [X0] : quotient(product(X0,product(sF3,sF1)),difference(sF3,one)) = difference(difference(sF3,one),product(product(difference(sF3,one),X0),sF1)),
    inference(backward_demodulation,[],[f3961,f3959]) ).

fof(f3969,plain,
    product(x0,product(sF3,sF0)) = product(sF0,product(sF3,sF1)),
    inference(backward_demodulation,[],[f3927,f3956]) ).

fof(f3970,plain,
    product(sF3,sF0) = difference(product(sF3,sF1),sF3),
    inference(backward_demodulation,[],[f3768,f3956]) ).

fof(f3980,plain,
    product(sF3,sF0) = quotient(sF0,sF3),
    inference(backward_demodulation,[],[f2841,f3970]) ).

fof(f4085,plain,
    ! [X0,X1] : difference(X1,product(sF1,product(X0,sF0))) = product(difference(product(sF0,X1),X0),sF0),
    inference(superposition,[],[f136,f939]) ).

fof(f4236,plain,
    ! [X0] : quotient(X0,x0) = difference(product(x0,quotient(one,X0)),sF3),
    inference(superposition,[],[f343,f122]) ).

fof(f4391,plain,
    ! [X0] : difference(product(sF1,sF1),product(sF1,X0)) = product(product(sF0,product(X0,sF1)),sF0),
    inference(superposition,[],[f42,f1547]) ).

fof(f4395,plain,
    ! [X0] : difference(sF1,X0) = product(product(product(sF0,X0),sF0),sF1),
    inference(superposition,[],[f6,f1547]) ).

fof(f4397,plain,
    ! [X0,X1] : product(difference(product(sF1,X1),product(X0,sF0)),sF1) = difference(X1,difference(sF1,X0)),
    inference(backward_demodulation,[],[f949,f4395]) ).

fof(f4431,plain,
    ! [X0] : product(product(x0,X0),sF0) = quotient(difference(sF0,X0),sF1),
    inference(superposition,[],[f213,f2325]) ).

fof(f4885,plain,
    difference(product(sF5,sF3),sF5) = quotient(sF4,sF5),
    inference(superposition,[],[f2814,f29]) ).

fof(f5096,plain,
    ! [X2,X0,X1] : product(difference(X1,X0),X1) = product(difference(X1,X2),product(difference(X2,X0),X1)),
    inference(superposition,[],[f222,f3]) ).

fof(f5098,plain,
    ! [X0,X1] : product(difference(X1,X0),X1) = product(difference(X1,one),product(X0,X1)),
    inference(superposition,[],[f222,f2]) ).

fof(f5112,plain,
    ! [X0,X1] : product(difference(X1,difference(X0,one)),product(X0,X1)) = product(difference(X1,product(X0,quotient(one,X0))),X1),
    inference(superposition,[],[f222,f16]) ).

fof(f5126,plain,
    ! [X2,X0,X1] : product(difference(X1,X0),X1) = product(difference(X1,quotient(X0,X2)),product(X2,X1)),
    inference(superposition,[],[f222,f6]) ).

fof(f5176,plain,
    ! [X0,X1] : product(sF0,product(product(X0,X1),x0)) = product(difference(x0,X0),product(X1,x0)),
    inference(superposition,[],[f858,f222]) ).

fof(f5255,plain,
    ! [X0,X1] : product(difference(X1,difference(X0,one)),product(X0,X1)) = product(difference(X1,X0),product(quotient(one,X0),X1)),
    inference(forward_demodulation,[],[f5112,f222]) ).

fof(f5410,plain,
    product(difference(x0,sF3),product(quotient(one,sF3),x0)) = product(difference(x0,difference(sF3,one)),sF1),
    inference(superposition,[],[f5255,f400]) ).

fof(f5439,plain,
    product(difference(x0,difference(sF3,one)),sF1) = product(sF0,product(product(sF3,quotient(one,sF3)),x0)),
    inference(forward_demodulation,[],[f5410,f5176]) ).

fof(f5500,plain,
    product(difference(x0,difference(sF3,one)),sF1) = product(sF0,product(product(sF3,difference(sF3,one)),x0)),
    inference(forward_demodulation,[],[f5439,f2930]) ).

fof(f5550,plain,
    product(sF0,product(one,x0)) = product(difference(x0,difference(sF3,one)),sF1),
    inference(forward_demodulation,[],[f5500,f3]) ).

fof(f5590,plain,
    product(sF0,x0) = product(difference(x0,difference(sF3,one)),sF1),
    inference(forward_demodulation,[],[f5550,f2]) ).

fof(f5622,plain,
    sF3 = product(difference(x0,difference(sF3,one)),sF1),
    inference(forward_demodulation,[],[f5590,f25]) ).

fof(f5698,plain,
    quotient(sF3,sF1) = difference(x0,difference(sF3,one)),
    inference(superposition,[],[f5,f5622]) ).

fof(f5700,plain,
    ! [X0] : difference(product(sF1,X0),product(sF1,difference(x0,difference(sF3,one)))) = quotient(difference(X0,sF3),sF1),
    inference(superposition,[],[f42,f5622]) ).

fof(f5715,plain,
    product(sF3,sF0) = difference(x0,difference(sF3,one)),
    inference(forward_demodulation,[],[f5698,f1563]) ).

fof(f5724,plain,
    ! [X0] : difference(product(sF1,X0),product(sF1,product(sF3,sF0))) = quotient(difference(X0,sF3),sF1),
    inference(backward_demodulation,[],[f5700,f5715]) ).

fof(f5747,plain,
    ! [X0] : product(difference(product(sF0,product(sF1,X0)),sF3),sF0) = quotient(difference(X0,sF3),sF1),
    inference(forward_demodulation,[],[f5724,f4085]) ).

fof(f5757,plain,
    ! [X0] : difference(product(sF1,X0),one) = quotient(difference(X0,sF3),sF1),
    inference(forward_demodulation,[],[f5747,f159]) ).

fof(f5772,plain,
    difference(product(sF3,sF0),one) = product(difference(difference(sF3,one),sF3),x0),
    inference(superposition,[],[f339,f5715]) ).

fof(f5774,plain,
    difference(sF3,one) = product(x0,product(sF3,sF0)),
    inference(superposition,[],[f3,f5715]) ).

fof(f5789,plain,
    difference(sF3,one) = product(sF0,product(sF3,sF1)),
    inference(backward_demodulation,[],[f3969,f5774]) ).

fof(f5791,plain,
    difference(product(sF3,sF0),one) = product(product(difference(one,sF3),sF3),x0),
    inference(forward_demodulation,[],[f5772,f755]) ).

fof(f5820,plain,
    difference(product(sF3,sF0),one) = product(product(sF3,sF3),x0),
    inference(forward_demodulation,[],[f5791,f62]) ).

fof(f5832,plain,
    product(sF3,sF1) = product(product(sF3,sF3),x0),
    inference(forward_demodulation,[],[f5820,f1638]) ).

fof(f5874,plain,
    ! [X0] : product(difference(x0,X0),x0) = product(x1,product(difference(sF4,X0),x0)),
    inference(superposition,[],[f5096,f33]) ).

fof(f5883,plain,
    ! [X0] : product(difference(sF0,X0),sF0) = product(x0,product(difference(sF3,X0),sF0)),
    inference(superposition,[],[f5096,f39]) ).

fof(f5887,plain,
    ! [X0] : product(difference(sF1,X0),sF1) = product(sF3,product(difference(x0,X0),sF1)),
    inference(superposition,[],[f5096,f1066]) ).

fof(f5889,plain,
    ! [X0] : product(difference(sF1,X0),sF1) = product(sF0,product(difference(sF3,X0),sF1)),
    inference(superposition,[],[f5096,f112]) ).

fof(f5890,plain,
    ! [X0] : product(difference(sF3,X0),sF3) = product(x0,product(difference(sF1,X0),sF3)),
    inference(superposition,[],[f5096,f401]) ).

fof(f6032,plain,
    ! [X0] : product(sF1,product(X0,sF0)) = product(x0,product(difference(sF3,X0),sF0)),
    inference(forward_demodulation,[],[f5883,f939]) ).

fof(f6041,plain,
    ! [X0] : product(sF0,product(X0,x0)) = product(x1,product(difference(sF4,X0),x0)),
    inference(forward_demodulation,[],[f5874,f858]) ).

fof(f6192,plain,
    ! [X0] : product(x1,product(X0,x0)) = product(sF0,product(product(sF4,X0),x0)),
    inference(superposition,[],[f6041,f4]) ).

fof(f6283,plain,
    ! [X0] : quotient(X0,sF1) = difference(product(sF1,quotient(sF3,X0)),one),
    inference(superposition,[],[f5757,f122]) ).

fof(f6442,plain,
    ! [X0] : product(x0,product(X0,sF0)) = product(sF1,product(product(sF3,X0),sF0)),
    inference(superposition,[],[f6032,f4]) ).

fof(f6508,plain,
    product(x0,product(sF4,sF0)) = product(sF1,product(sF5,sF0)),
    inference(superposition,[],[f6442,f29]) ).

fof(f6570,plain,
    quotient(one,x0) = difference(product(x0,product(product(sF4,sF0),x0)),product(sF1,product(sF5,sF0))),
    inference(superposition,[],[f96,f6508]) ).

fof(f6589,plain,
    quotient(one,x0) = product(difference(product(sF0,product(x0,product(product(sF4,sF0),x0))),sF5),sF0),
    inference(forward_demodulation,[],[f6570,f4085]) ).

fof(f6601,plain,
    product(sF0,sF3) = product(difference(product(sF0,product(x0,product(product(sF4,sF0),x0))),sF5),sF0),
    inference(forward_demodulation,[],[f6589,f1262]) ).

fof(f6691,plain,
    ! [X2,X0,X1] : product(difference(X1,X2),X1) = product(difference(X1,quotient(X2,quotient(X0,X1))),X0),
    inference(superposition,[],[f5126,f6]) ).

fof(f6706,plain,
    ! [X0] : product(difference(x0,X0),x0) = product(difference(x0,quotient(X0,sF0)),sF3),
    inference(superposition,[],[f5126,f25]) ).

fof(f6707,plain,
    ! [X0] : product(difference(sF1,X0),sF1) = product(difference(sF1,quotient(X0,sF0)),one),
    inference(superposition,[],[f5126,f38]) ).

fof(f6715,plain,
    ! [X0] : product(difference(sF0,X0),sF0) = product(difference(sF0,quotient(X0,sF1)),sF3),
    inference(superposition,[],[f5126,f108]) ).

fof(f6718,plain,
    ! [X0] : product(difference(x0,X0),x0) = product(difference(x0,quotient(X0,sF3)),sF1),
    inference(superposition,[],[f5126,f400]) ).

fof(f6754,plain,
    ! [X0] : product(sF0,product(X0,x0)) = product(difference(x0,quotient(X0,sF3)),sF1),
    inference(forward_demodulation,[],[f6718,f858]) ).

fof(f6755,plain,
    ! [X0] : product(sF1,product(X0,sF0)) = product(difference(sF0,quotient(X0,sF1)),sF3),
    inference(forward_demodulation,[],[f6715,f939]) ).

fof(f6757,plain,
    ! [X0] : product(difference(sF1,X0),sF1) = difference(sF1,quotient(X0,sF0)),
    inference(forward_demodulation,[],[f6707,f1]) ).

fof(f6758,plain,
    ! [X0] : product(sF0,product(X0,x0)) = product(difference(x0,quotient(X0,sF0)),sF3),
    inference(forward_demodulation,[],[f6706,f858]) ).

fof(f6833,plain,
    ! [X0] : product(difference(sF1,difference(sF1,X0)),sF1) = difference(sF1,product(sF0,quotient(X0,sF0))),
    inference(superposition,[],[f6757,f1203]) ).

fof(f6879,plain,
    product(sF1,difference(sF0,product(sF3,sF0))) = difference(sF0,difference(sF3,one)),
    inference(superposition,[],[f2240,f5774]) ).

fof(f6916,plain,
    product(sF1,difference(sF3,one)) = difference(sF0,difference(sF3,one)),
    inference(forward_demodulation,[],[f6879,f2135]) ).

fof(f6926,plain,
    product(sF3,sF1) = difference(sF0,difference(sF3,one)),
    inference(forward_demodulation,[],[f6916,f3956]) ).

fof(f7042,plain,
    ! [X0] : product(sF0,product(product(X0,sF0),x0)) = product(difference(x0,X0),sF3),
    inference(superposition,[],[f6758,f5]) ).

fof(f7108,plain,
    ! [X0] : product(difference(x0,product(sF0,product(sF1,X0))),sF3) = product(sF0,product(quotient(X0,sF1),x0)),
    inference(superposition,[],[f7042,f213]) ).

fof(f7134,plain,
    ! [X0] : product(product(X0,sF0),x0) = difference(sF0,product(difference(x0,X0),sF3)),
    inference(superposition,[],[f4,f7042]) ).

fof(f7170,plain,
    ! [X0] : product(sF0,product(quotient(X0,sF1),x0)) = product(product(sF0,difference(sF1,product(sF1,X0))),sF3),
    inference(forward_demodulation,[],[f7108,f3723]) ).

fof(f7195,plain,
    ! [X0] : product(product(sF0,X0),sF3) = product(sF0,product(quotient(X0,sF1),x0)),
    inference(forward_demodulation,[],[f7170,f4]) ).

fof(f7221,plain,
    ! [X0] : product(sF0,product(X0,x0)) = product(product(sF0,product(X0,sF1)),sF3),
    inference(superposition,[],[f7195,f5]) ).

fof(f7237,plain,
    ! [X0] : product(quotient(X0,sF1),x0) = difference(sF0,product(product(sF0,X0),sF3)),
    inference(superposition,[],[f4,f7195]) ).

fof(f7359,plain,
    ! [X2,X3,X0,X1] : difference(difference(X1,X0),product(X2,product(X3,X1))) = product(difference(X0,product(product(X1,X2),X3)),X1),
    inference(superposition,[],[f1729,f3]) ).

fof(f7487,plain,
    ! [X0,X1] : difference(X0,product(sF0,product(X1,sF1))) = product(difference(product(sF1,X0),product(sF3,X1)),sF1),
    inference(superposition,[],[f1729,f108]) ).

fof(f7488,plain,
    ! [X0,X1] : difference(X0,product(sF3,product(X1,sF1))) = product(difference(product(sF1,X0),product(x0,X1)),sF1),
    inference(superposition,[],[f1729,f1065]) ).

fof(f7784,plain,
    ! [X0] : difference(X0,product(sF3,product(x0,sF3))) = product(difference(product(sF3,X0),product(sF3,sF1)),sF3),
    inference(superposition,[],[f1729,f5832]) ).

fof(f7816,plain,
    ! [X0] : difference(X0,product(sF3,product(x0,sF3))) = difference(difference(sF3,product(sF3,X0)),x0),
    inference(forward_demodulation,[],[f7784,f1074]) ).

fof(f7821,plain,
    ! [X0] : difference(X0,x0) = difference(X0,product(sF3,product(x0,sF3))),
    inference(forward_demodulation,[],[f7816,f4]) ).

fof(f7837,plain,
    product(x0,sF3) = difference(sF3,x0),
    inference(superposition,[],[f4,f7821]) ).

fof(f8227,plain,
    ! [X0,X1] : difference(X0,product(product(sF0,sF3),product(X1,sF3))) = product(difference(product(sF3,X0),product(sF0,X1)),sF3),
    inference(superposition,[],[f1729,f2722]) ).

fof(f8257,plain,
    ! [X2,X0,X1] : difference(X0,product(X1,quotient(X2,X1))) = quotient(difference(difference(X1,X0),X2),X1),
    inference(superposition,[],[f120,f3]) ).

fof(f8323,plain,
    ! [X0] : quotient(difference(sF0,X0),sF1) = difference(sF3,product(sF1,quotient(X0,sF1))),
    inference(superposition,[],[f120,f108]) ).

fof(f8324,plain,
    ! [X0] : quotient(difference(sF3,X0),sF1) = difference(x0,product(sF1,quotient(X0,sF1))),
    inference(superposition,[],[f120,f1065]) ).

fof(f8340,plain,
    ! [X0,X1] : quotient(difference(X1,product(sF1,X0)),sF0) = difference(product(sF0,X1),product(sF0,difference(sF0,quotient(X0,sF0)))),
    inference(superposition,[],[f120,f2308]) ).

fof(f8354,plain,
    ! [X0,X1] : difference(product(sF1,X1),product(sF1,product(product(sF0,X0),sF0))) = quotient(difference(X1,difference(sF1,X0)),sF1),
    inference(superposition,[],[f120,f1547]) ).

fof(f8433,plain,
    ! [X0,X1] : quotient(difference(X1,difference(sF1,X0)),sF1) = product(difference(product(sF0,product(sF1,X1)),product(sF0,X0)),sF0),
    inference(forward_demodulation,[],[f8354,f4085]) ).

fof(f8436,plain,
    ! [X0,X1] : quotient(difference(X1,product(sF1,X0)),sF0) = difference(product(sF0,X1),quotient(X0,sF0)),
    inference(forward_demodulation,[],[f8340,f3]) ).

fof(f8446,plain,
    ! [X0] : product(product(x0,X0),sF0) = difference(sF3,product(sF1,quotient(X0,sF1))),
    inference(forward_demodulation,[],[f8323,f4431]) ).

fof(f8478,plain,
    ! [X0,X1] : difference(product(sF1,X1),product(X0,sF0)) = quotient(difference(X1,difference(sF1,X0)),sF1),
    inference(forward_demodulation,[],[f8433,f117]) ).

fof(f8626,plain,
    ! [X0] : quotient(product(sF0,X0),x0) = difference(x0,quotient(X0,x0)),
    inference(superposition,[],[f4,f1606]) ).

fof(f8655,plain,
    ! [X0] : product(sF0,product(X0,sF0)) = quotient(product(sF0,X0),x0),
    inference(forward_demodulation,[],[f8626,f3403]) ).

fof(f9296,plain,
    ! [X0,X1] : product(difference(X1,one),X0) = product(difference(X1,quotient(X0,X1)),X1),
    inference(superposition,[],[f5098,f6]) ).

fof(f10151,plain,
    quotient(product(x1,sF1),x0) = difference(x0,product(sF4,sF3)),
    inference(superposition,[],[f403,f27]) ).

fof(f10161,plain,
    ! [X0] : difference(product(sF3,x0),product(sF3,product(x0,X0))) = quotient(quotient(product(X0,sF1),x0),sF3),
    inference(superposition,[],[f42,f403]) ).

fof(f10181,plain,
    ! [X0] : difference(sF1,product(sF3,product(x0,X0))) = quotient(quotient(product(X0,sF1),x0),sF3),
    inference(forward_demodulation,[],[f10161,f400]) ).

fof(f10231,plain,
    ! [X0] : difference(difference(sF3,X0),one) = product(difference(X0,product(sF3,difference(sF3,one))),sF3),
    inference(superposition,[],[f734,f2930]) ).

fof(f10274,plain,
    ! [X0,X1] : difference(difference(X0,one),X1) = product(product(X0,quotient(X1,X0)),X0),
    inference(superposition,[],[f734,f62]) ).

fof(f10385,plain,
    ! [X0] : difference(difference(sF3,X0),one) = product(difference(X0,one),sF3),
    inference(forward_demodulation,[],[f10231,f3]) ).

fof(f10472,plain,
    ! [X0] : difference(sF3,X0) = quotient(one,product(difference(X0,one),sF3)),
    inference(superposition,[],[f79,f10385]) ).

fof(f11790,plain,
    product(sF1,quotient(x1,sF1)) = product(sF2,sF0),
    inference(superposition,[],[f1549,f23]) ).

fof(f12117,plain,
    ! [X0,X1] : difference(X1,quotient(X1,X0)) = quotient(X1,product(X0,X1)),
    inference(superposition,[],[f1245,f122]) ).

fof(f12388,plain,
    ! [X0,X1] : quotient(difference(X1,X0),X0) = difference(difference(X1,X0),quotient(difference(X1,X0),X1)),
    inference(superposition,[],[f12117,f3]) ).

fof(f12542,plain,
    ! [X0,X1] : difference(product(X0,X1),X0) = difference(difference(X1,X0),quotient(difference(X1,X0),X1)),
    inference(forward_demodulation,[],[f12388,f100]) ).

fof(f12697,plain,
    ! [X0,X1] : quotient(difference(X1,X0),X1) = product(difference(X1,X0),difference(product(X0,X1),X0)),
    inference(superposition,[],[f3,f12542]) ).

fof(f12972,plain,
    ! [X0,X1] : quotient(X0,quotient(X1,X0)) = product(X0,difference(product(X1,quotient(X1,X0)),X1)),
    inference(superposition,[],[f12697,f122]) ).

fof(f13231,plain,
    ! [X0,X1] : product(X0,quotient(X0,X1)) = quotient(X0,quotient(X1,X0)),
    inference(forward_demodulation,[],[f12972,f2827]) ).

fof(f15443,plain,
    ! [X0] : difference(product(sF1,product(sF3,quotient(sF3,X0))),one) = quotient(quotient(X0,sF3),sF1),
    inference(superposition,[],[f5757,f2827]) ).

fof(f15972,plain,
    ! [X0] : product(difference(x0,X0),sF1) = product(sF0,product(product(X0,sF3),x0)),
    inference(superposition,[],[f6754,f5]) ).

fof(f16084,plain,
    ! [X0] : product(sF0,product(sF1,product(product(X0,sF3),x0))) = product(x0,product(difference(x0,X0),sF1)),
    inference(superposition,[],[f2250,f15972]) ).

fof(f16089,plain,
    ! [X0] : difference(sF0,product(difference(x0,X0),sF1)) = product(product(X0,sF3),x0),
    inference(superposition,[],[f4,f15972]) ).

fof(f16184,plain,
    product(product(sF4,sF3),x0) = difference(sF0,product(x1,sF1)),
    inference(superposition,[],[f16089,f33]) ).

fof(f16185,plain,
    ! [X0] : difference(sF0,product(X0,sF1)) = product(product(product(x0,X0),sF3),x0),
    inference(superposition,[],[f16089,f4]) ).

fof(f16438,plain,
    ! [X0] : quotient(X0,sF0) = product(sF0,product(sF1,product(X0,sF1))),
    inference(superposition,[],[f1552,f5]) ).

fof(f16444,plain,
    ! [X0,X1] : product(sF0,product(sF1,difference(difference(sF1,X0),X1))) = quotient(difference(X0,product(sF1,quotient(X1,sF1))),sF0),
    inference(superposition,[],[f1552,f8257]) ).

fof(f16453,plain,
    ! [X0] : product(difference(sF1,quotient(X0,sF1)),sF1) = difference(sF1,product(sF0,product(sF1,X0))),
    inference(superposition,[],[f6757,f1552]) ).

fof(f16471,plain,
    ! [X0] : product(difference(sF1,one),X0) = difference(sF1,product(sF0,product(sF1,X0))),
    inference(forward_demodulation,[],[f16453,f9296]) ).

fof(f16479,plain,
    ! [X0,X1] : product(sF0,product(sF1,difference(difference(sF1,X0),X1))) = difference(product(sF0,X0),quotient(quotient(X1,sF1),sF0)),
    inference(forward_demodulation,[],[f16444,f8436]) ).

fof(f16493,plain,
    ! [X0] : product(product(sF3,sF0),X0) = difference(sF1,product(sF0,product(sF1,X0))),
    inference(forward_demodulation,[],[f16471,f1614]) ).

fof(f16499,plain,
    ! [X0,X1] : product(sF0,product(sF1,difference(difference(sF1,X0),X1))) = difference(product(sF0,X0),product(sF0,product(sF1,X1))),
    inference(forward_demodulation,[],[f16479,f1552]) ).

fof(f18325,plain,
    ! [X0] : product(difference(x0,X0),x0) = product(difference(x0,quotient(X0,product(sF0,sF3))),one),
    inference(superposition,[],[f6691,f1262]) ).

fof(f18402,plain,
    ! [X0] : product(sF1,product(quotient(X0,quotient(sF0,sF3)),sF0)) = product(x0,product(difference(sF3,X0),sF3)),
    inference(superposition,[],[f6032,f6691]) ).

fof(f18405,plain,
    ! [X2,X0,X1] : quotient(product(difference(X0,X1),X0),X2) = difference(X0,quotient(X1,quotient(X2,X0))),
    inference(superposition,[],[f5,f6691]) ).

fof(f18429,plain,
    ! [X0,X1] : product(difference(X0,X1),X0) = difference(X0,quotient(X1,quotient(one,X0))),
    inference(superposition,[],[f1,f6691]) ).

fof(f18468,plain,
    ! [X0] : product(x0,product(difference(sF3,X0),sF3)) = product(sF1,product(quotient(X0,product(sF3,sF0)),sF0)),
    inference(forward_demodulation,[],[f18402,f3980]) ).

fof(f18509,plain,
    ! [X0] : product(difference(x0,X0),x0) = difference(x0,quotient(X0,product(sF0,sF3))),
    inference(forward_demodulation,[],[f18325,f1]) ).

fof(f18543,plain,
    ! [X0] : product(sF0,product(X0,x0)) = difference(x0,quotient(X0,product(sF0,sF3))),
    inference(forward_demodulation,[],[f18509,f858]) ).

fof(f18741,plain,
    product(product(sF4,sF0),x0) = difference(sF0,product(x1,sF3)),
    inference(superposition,[],[f7134,f33]) ).

fof(f19168,plain,
    ! [X0] : product(x0,quotient(X0,x0)) = product(sF4,quotient(difference(x1,X0),x0)),
    inference(superposition,[],[f422,f3]) ).

fof(f19423,plain,
    ! [X0] : difference(product(sF1,sF0),product(sF1,X0)) = product(product(x0,product(X0,sF1)),sF0),
    inference(superposition,[],[f42,f4431]) ).

fof(f19427,plain,
    ! [X0] : difference(sF0,X0) = product(product(product(x0,X0),sF0),sF1),
    inference(superposition,[],[f6,f4431]) ).

fof(f19435,plain,
    ! [X0] : product(difference(sF1,one),difference(sF0,X0)) = product(difference(sF1,product(product(x0,X0),sF0)),sF1),
    inference(superposition,[],[f9296,f4431]) ).

fof(f19439,plain,
    ! [X0] : product(difference(sF1,one),difference(sF0,X0)) = product(difference(sF1,product(x0,X0)),product(sF0,sF1)),
    inference(forward_demodulation,[],[f19435,f222]) ).

fof(f19446,plain,
    ! [X0] : difference(sF3,product(sF1,X0)) = product(product(x0,product(X0,sF1)),sF0),
    inference(forward_demodulation,[],[f19423,f108]) ).

fof(f19468,plain,
    ! [X0] : product(difference(sF1,one),difference(sF0,X0)) = product(difference(sF1,product(x0,X0)),one),
    inference(forward_demodulation,[],[f19439,f38]) ).

fof(f19482,plain,
    ! [X0] : difference(sF1,product(x0,X0)) = product(difference(sF1,one),difference(sF0,X0)),
    inference(forward_demodulation,[],[f19468,f1]) ).

fof(f19490,plain,
    ! [X0] : difference(sF1,product(x0,X0)) = product(product(sF3,sF0),difference(sF0,X0)),
    inference(forward_demodulation,[],[f19482,f1614]) ).

fof(f19497,plain,
    ! [X0] : product(sF3,quotient(product(product(X0,x0),sF0),sF1)) = product(sF1,quotient(difference(x0,X0),sF1)),
    inference(superposition,[],[f425,f3378]) ).

fof(f19512,plain,
    ! [X0] : product(sF1,quotient(X0,sF1)) = product(sF3,quotient(difference(sF0,X0),sF1)),
    inference(superposition,[],[f425,f3]) ).

fof(f19566,plain,
    ! [X0] : product(sF1,quotient(X0,sF1)) = product(sF3,product(product(x0,X0),sF0)),
    inference(forward_demodulation,[],[f19512,f4431]) ).

fof(f19579,plain,
    ! [X0] : product(sF1,quotient(difference(x0,X0),sF1)) = product(sF3,product(X0,sF0)),
    inference(forward_demodulation,[],[f19497,f2215]) ).

fof(f19638,plain,
    product(sF1,quotient(x1,sF1)) = product(sF3,product(sF4,sF0)),
    inference(superposition,[],[f19566,f27]) ).

fof(f19645,plain,
    ! [X0] : product(sF1,quotient(quotient(X0,product(sF0,x0)),sF1)) = product(sF3,product(x0,quotient(X0,x0))),
    inference(superposition,[],[f19566,f1859]) ).

fof(f19650,plain,
    ! [X0] : quotient(product(sF1,quotient(X0,sF1)),sF0) = difference(sF0,product(product(sF0,sF3),product(x0,X0))),
    inference(superposition,[],[f7,f19566]) ).

fof(f19683,plain,
    ! [X0] : product(sF1,quotient(X0,product(sF0,sF1))) = difference(sF0,product(product(sF0,sF3),product(x0,X0))),
    inference(forward_demodulation,[],[f19650,f2519]) ).

fof(f19687,plain,
    ! [X0] : product(sF3,product(x0,quotient(X0,x0))) = product(sF1,quotient(quotient(X0,sF3),sF1)),
    inference(forward_demodulation,[],[f19645,f25]) ).

fof(f19692,plain,
    product(sF2,sF0) = product(sF3,product(sF4,sF0)),
    inference(forward_demodulation,[],[f19638,f11790]) ).

fof(f19706,plain,
    ! [X0] : product(sF1,quotient(X0,one)) = difference(sF0,product(product(sF0,sF3),product(x0,X0))),
    inference(forward_demodulation,[],[f19683,f38]) ).

fof(f19722,plain,
    ! [X0] : product(sF1,X0) = difference(sF0,product(product(sF0,sF3),product(x0,X0))),
    inference(forward_demodulation,[],[f19706,f80]) ).

fof(f19872,plain,
    ! [X0] : product(sF1,difference(x0,X0)) = difference(sF0,product(product(sF0,sF3),X0)),
    inference(superposition,[],[f19722,f3]) ).

fof(f19887,plain,
    ! [X0] : product(sF0,product(sF1,X0)) = product(product(sF0,sF3),product(x0,X0)),
    inference(superposition,[],[f3,f19722]) ).

fof(f20658,plain,
    ! [X2,X0,X1] : quotient(product(X0,X1),X2) = difference(X1,quotient(product(X1,X0),quotient(X2,X1))),
    inference(superposition,[],[f18405,f4]) ).

fof(f20753,plain,
    ! [X0,X1] : difference(x0,quotient(X0,quotient(X1,x0))) = quotient(product(sF0,product(X0,x0)),X1),
    inference(superposition,[],[f18405,f858]) ).

fof(f22837,plain,
    ! [X2,X0,X1] : quotient(product(X1,X2),product(X0,X2)) = difference(X2,quotient(product(X2,X1),X0)),
    inference(superposition,[],[f20658,f5]) ).

fof(f22902,plain,
    ! [X2,X0,X1] : product(X1,quotient(product(X0,X1),X2)) = quotient(product(X1,X0),quotient(X2,X1)),
    inference(superposition,[],[f3,f20658]) ).

fof(f22954,plain,
    ! [X2,X0,X1] : difference(quotient(X0,X1),product(X0,quotient(X2,quotient(X0,X1)))) = product(X1,quotient(product(X2,X1),X0)),
    inference(backward_demodulation,[],[f293,f22902]) ).

fof(f23026,plain,
    ! [X0] : product(difference(sF3,product(x0,product(product(sF0,sF3),X0))),x0) = difference(sF3,quotient(product(sF3,X0),sF0)),
    inference(backward_demodulation,[],[f1286,f22837]) ).

fof(f23410,plain,
    ! [X0] : quotient(one,product(X0,sF1)) = difference(sF1,quotient(product(sF1,sF0),X0)),
    inference(superposition,[],[f22837,f38]) ).

fof(f23451,plain,
    ! [X0] : quotient(product(X0,sF0),difference(sF3,one)) = difference(sF0,quotient(product(sF0,X0),product(x0,sF3))),
    inference(superposition,[],[f22837,f3917]) ).

fof(f23523,plain,
    ! [X0] : quotient(product(X0,product(sF1,sF1)),x0) = difference(product(sF1,sF1),quotient(product(product(sF1,sF1),X0),sF0)),
    inference(superposition,[],[f22837,f2017]) ).

fof(f23525,plain,
    ! [X0] : quotient(product(X0,product(sF3,sF1)),difference(sF3,one)) = difference(product(sF3,sF1),quotient(product(product(sF3,sF1),X0),sF0)),
    inference(superposition,[],[f22837,f5789]) ).

fof(f23586,plain,
    ! [X0] : difference(x0,product(product(x0,X0),x0)) = difference(product(sF1,sF1),quotient(product(product(sF1,sF1),X0),sF0)),
    inference(forward_demodulation,[],[f23523,f2055]) ).

fof(f23625,plain,
    ! [X0] : quotient(one,product(X0,sF1)) = difference(sF1,quotient(sF3,X0)),
    inference(forward_demodulation,[],[f23410,f108]) ).

fof(f25686,plain,
    ! [X0] : product(product(sF0,X0),product(sF0,sF3)) = product(x0,quotient(product(sF0,difference(sF1,X0)),x0)),
    inference(superposition,[],[f3290,f3723]) ).

fof(f25726,plain,
    ! [X0] : product(product(sF0,X0),product(sF0,sF3)) = product(x0,product(sF0,product(difference(sF1,X0),sF0))),
    inference(forward_demodulation,[],[f25686,f8655]) ).

fof(f25754,plain,
    ! [X0] : product(product(sF0,X0),product(sF0,sF3)) = product(sF0,product(sF1,product(difference(sF1,X0),sF0))),
    inference(forward_demodulation,[],[f25726,f2250]) ).

fof(f25767,plain,
    ! [X0] : product(product(sF0,X0),product(sF0,sF3)) = quotient(difference(sF1,X0),x0),
    inference(forward_demodulation,[],[f25754,f2406]) ).

fof(f26107,plain,
    ! [X0] : product(sF0,product(X0,sF1)) = quotient(product(sF0,product(X0,x0)),sF3),
    inference(superposition,[],[f5,f7221]) ).

fof(f26143,plain,
    ! [X0] : product(sF0,product(X0,sF1)) = difference(x0,quotient(X0,quotient(sF3,x0))),
    inference(forward_demodulation,[],[f26107,f20753]) ).

fof(f26163,plain,
    ! [X0] : product(sF0,product(X0,sF1)) = difference(x0,quotient(X0,sF0)),
    inference(forward_demodulation,[],[f26143,f84]) ).

fof(f26238,plain,
    ! [X0] : difference(x0,X0) = product(sF0,product(product(X0,sF0),sF1)),
    inference(superposition,[],[f26163,f5]) ).

fof(f26241,plain,
    ! [X0] : difference(x0,difference(sF0,quotient(X0,sF0))) = product(sF0,product(product(sF1,X0),sF1)),
    inference(superposition,[],[f26163,f2308]) ).

fof(f26249,plain,
    ! [X0] : difference(x0,product(product(x0,X0),x0)) = product(sF0,product(difference(sF0,X0),sF1)),
    inference(superposition,[],[f26163,f696]) ).

fof(f26259,plain,
    ! [X0] : product(quotient(X0,sF0),product(sF0,sF3)) = product(x0,quotient(product(sF0,product(X0,sF1)),x0)),
    inference(superposition,[],[f3290,f26163]) ).

fof(f26293,plain,
    ! [X0] : product(quotient(X0,sF0),product(sF0,sF3)) = product(x0,product(sF0,product(product(X0,sF1),sF0))),
    inference(forward_demodulation,[],[f26259,f8655]) ).

fof(f26303,plain,
    ! [X0] : difference(product(sF1,sF1),quotient(product(product(sF1,sF1),X0),sF0)) = product(sF0,product(difference(sF0,X0),sF1)),
    inference(backward_demodulation,[],[f23586,f26249]) ).

fof(f26324,plain,
    ! [X0] : product(quotient(X0,sF0),product(sF0,sF3)) = product(sF0,product(sF1,product(product(X0,sF1),sF0))),
    inference(forward_demodulation,[],[f26293,f2250]) ).

fof(f26333,plain,
    ! [X0] : quotient(product(X0,sF1),x0) = product(quotient(X0,sF0),product(sF0,sF3)),
    inference(forward_demodulation,[],[f26324,f2406]) ).

fof(f26381,plain,
    ! [X0] : difference(sF0,difference(x0,X0)) = product(product(X0,sF0),sF1),
    inference(superposition,[],[f4,f26238]) ).

fof(f26420,plain,
    ! [X0] : product(product(X0,x0),sF0) = product(product(X0,sF0),sF1),
    inference(backward_demodulation,[],[f2222,f26381]) ).

fof(f26461,plain,
    ! [X0] : difference(sF0,X0) = product(sF1,product(product(X0,sF0),sF1)),
    inference(backward_demodulation,[],[f1582,f26420]) ).

fof(f26462,plain,
    ! [X0] : difference(sF1,difference(sF0,X0)) = product(product(X0,sF0),sF1),
    inference(backward_demodulation,[],[f1583,f26420]) ).

fof(f26661,plain,
    ! [X0] : product(X0,sF0) = product(product(quotient(X0,x0),sF0),sF1),
    inference(superposition,[],[f26420,f6]) ).

fof(f26979,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = product(sF1,product(X0,sF1)),
    inference(superposition,[],[f26461,f6]) ).

fof(f27049,plain,
    ! [X0] : quotient(product(sF1,X0),sF0) = product(sF1,product(X0,sF1)),
    inference(backward_demodulation,[],[f2308,f26979]) ).

fof(f27059,plain,
    ! [X0] : product(sF0,product(product(sF1,X0),sF1)) = difference(x0,product(sF1,product(X0,sF1))),
    inference(backward_demodulation,[],[f26241,f26979]) ).

fof(f27705,plain,
    ! [X0] : quotient(product(sF0,product(difference(sF0,X0),sF1)),x0) = difference(product(x0,x0),product(x0,product(x0,X0))),
    inference(superposition,[],[f42,f26249]) ).

fof(f27737,plain,
    ! [X0] : difference(product(sF1,sF1),product(x0,product(x0,X0))) = quotient(product(sF0,product(difference(sF0,X0),sF1)),x0),
    inference(forward_demodulation,[],[f27705,f2015]) ).

fof(f27771,plain,
    ! [X0] : difference(product(sF1,sF1),product(x0,product(x0,X0))) = product(sF0,product(product(difference(sF0,X0),sF1),sF0)),
    inference(forward_demodulation,[],[f27737,f8655]) ).

fof(f27849,plain,
    ! [X0] : quotient(one,product(X0,sF3)) = difference(sF3,quotient(one,X0)),
    inference(superposition,[],[f10472,f122]) ).

fof(f28326,plain,
    ! [X0] : product(x0,product(product(sF0,sF3),X0)) = product(sF0,product(sF1,product(sF1,difference(x0,X0)))),
    inference(superposition,[],[f2325,f19872]) ).

fof(f28330,plain,
    ! [X0] : quotient(product(X0,sF0),difference(product(sF0,sF3),sF0)) = product(product(sF1,difference(x0,product(difference(product(sF0,sF3),sF0),X0))),product(sF0,sF3)),
    inference(superposition,[],[f166,f19872]) ).

fof(f28332,plain,
    ! [X0] : difference(difference(product(sF0,sF3),sF0),X0) = product(product(sF1,difference(x0,quotient(X0,product(sF0,sF3)))),product(sF0,sF3)),
    inference(superposition,[],[f734,f19872]) ).

fof(f28361,plain,
    ! [X0] : difference(difference(product(sF0,sF3),sF0),X0) = product(product(sF1,product(sF0,product(X0,x0))),product(sF0,sF3)),
    inference(forward_demodulation,[],[f28332,f18543]) ).

fof(f28362,plain,
    ! [X0] : quotient(product(X0,sF0),difference(sF3,one)) = product(product(sF1,difference(x0,product(difference(sF3,one),X0))),product(sF0,sF3)),
    inference(forward_demodulation,[],[f28330,f2862]) ).

fof(f28382,plain,
    ! [X0] : difference(difference(sF3,one),X0) = product(product(sF1,product(sF0,product(X0,x0))),product(sF0,sF3)),
    inference(forward_demodulation,[],[f28361,f2862]) ).

fof(f29177,plain,
    ! [X0] : quotient(product(sF3,X0),difference(sF3,one)) = product(sF3,quotient(product(X0,sF3),one)),
    inference(superposition,[],[f22902,f2930]) ).

fof(f29227,plain,
    ! [X0] : quotient(product(x0,X0),sF3) = product(x0,quotient(product(X0,x0),sF1)),
    inference(superposition,[],[f22902,f402]) ).

fof(f29354,plain,
    ! [X0] : quotient(product(sF3,X0),difference(sF3,one)) = product(sF3,product(X0,sF3)),
    inference(forward_demodulation,[],[f29177,f80]) ).

fof(f30377,plain,
    ! [X0,X1] : quotient(X1,product(sF0,sF3)) = difference(product(product(sF0,sF3),quotient(product(x0,quotient(X0,x0)),X1)),product(product(sF0,sF3),product(x0,X0))),
    inference(superposition,[],[f2803,f1267]) ).

fof(f30577,plain,
    ! [X0] : quotient(X0,difference(sF3,one)) = difference(product(difference(sF3,one),quotient(product(sF0,difference(sF3,one)),X0)),product(sF0,sF3)),
    inference(superposition,[],[f2803,f3924]) ).

fof(f30755,plain,
    ! [X0] : quotient(X0,difference(sF3,one)) = difference(product(difference(sF3,one),quotient(product(sF3,sF0),X0)),product(sF0,sF3)),
    inference(forward_demodulation,[],[f30577,f3862]) ).

fof(f30946,plain,
    ! [X0,X1] : quotient(X1,product(sF0,sF3)) = difference(product(product(sF0,sF3),quotient(product(x0,quotient(X0,x0)),X1)),product(sF0,product(sF1,X0))),
    inference(forward_demodulation,[],[f30377,f19887]) ).

fof(f31075,plain,
    ! [X0,X1] : quotient(X1,product(sF0,sF3)) = difference(product(product(sF0,sF3),product(x0,quotient(X0,product(X1,x0)))),product(sF0,product(sF1,X0))),
    inference(forward_demodulation,[],[f30946,f2519]) ).

fof(f31150,plain,
    ! [X0,X1] : quotient(X1,product(sF0,sF3)) = difference(product(sF0,product(sF1,quotient(X0,product(X1,x0)))),product(sF0,product(sF1,X0))),
    inference(forward_demodulation,[],[f31075,f19887]) ).

fof(f31191,plain,
    ! [X0,X1] : quotient(X1,product(sF0,sF3)) = product(sF0,product(sF1,difference(difference(sF1,product(sF1,quotient(X0,product(X1,x0)))),X0))),
    inference(forward_demodulation,[],[f31150,f16499]) ).

fof(f31208,plain,
    ! [X0,X1] : quotient(X1,product(sF0,sF3)) = product(sF0,product(sF1,difference(quotient(X0,product(X1,x0)),X0))),
    inference(forward_demodulation,[],[f31191,f4]) ).

fof(f31214,plain,
    ! [X1] : quotient(X1,product(sF0,sF3)) = product(sF0,product(sF1,product(X1,x0))),
    inference(forward_demodulation,[],[f31208,f122]) ).

fof(f31226,plain,
    ! [X0] : quotient(product(X0,sF3),product(sF0,sF3)) = product(x0,product(difference(x0,X0),sF1)),
    inference(backward_demodulation,[],[f16084,f31214]) ).

fof(f31232,plain,
    ! [X0] : product(x0,product(difference(x0,X0),sF1)) = difference(sF3,quotient(product(sF3,X0),sF0)),
    inference(forward_demodulation,[],[f31226,f22837]) ).

fof(f31238,plain,
    ! [X0] : product(difference(sF3,product(x0,product(product(sF0,sF3),X0))),x0) = product(x0,product(difference(x0,X0),sF1)),
    inference(backward_demodulation,[],[f23026,f31232]) ).

fof(f31424,plain,
    ! [X0] : difference(sF0,difference(sF1,X0)) = product(difference(sF3,product(X0,sF0)),sF1),
    inference(superposition,[],[f4397,f108]) ).

fof(f31425,plain,
    ! [X0] : difference(sF3,difference(sF1,X0)) = product(difference(x0,product(X0,sF0)),sF1),
    inference(superposition,[],[f4397,f1065]) ).

fof(f32216,plain,
    ! [X0] : product(sF1,difference(x0,product(X0,x0))) = product(product(product(x0,product(sF0,sF3)),X0),x0),
    inference(superposition,[],[f19872,f851]) ).

fof(f32234,plain,
    ! [X0,X1] : product(X0,product(X1,x0)) = product(sF0,product(product(product(x0,X0),X1),x0)),
    inference(superposition,[],[f3,f851]) ).

fof(f32270,plain,
    ! [X0] : product(sF1,difference(x0,product(X0,x0))) = product(product(product(sF0,product(sF1,sF3)),X0),x0),
    inference(forward_demodulation,[],[f32216,f2250]) ).

fof(f32334,plain,
    ! [X0] : product(sF1,difference(x0,product(X0,x0))) = product(product(product(sF0,x0),X0),x0),
    inference(forward_demodulation,[],[f32270,f1065]) ).

fof(f32380,plain,
    ! [X0] : product(product(sF3,X0),x0) = product(sF1,difference(x0,product(X0,x0))),
    inference(forward_demodulation,[],[f32334,f25]) ).

fof(f32439,plain,
    ! [X0] : product(sF0,product(product(sF1,X0),x0)) = product(difference(sF3,one),product(X0,x0)),
    inference(superposition,[],[f32234,f2903]) ).

fof(f32661,plain,
    ! [X0] : difference(x0,product(X0,x0)) = difference(sF1,product(product(sF3,X0),x0)),
    inference(superposition,[],[f4,f32380]) ).

fof(f32824,plain,
    ! [X0] : difference(sF1,product(X0,x0)) = difference(x0,product(difference(sF3,X0),x0)),
    inference(superposition,[],[f32661,f3]) ).

fof(f32930,plain,
    ! [X0] : difference(sF1,product(quotient(X0,quotient(one,sF3)),x0)) = difference(x0,product(product(difference(sF3,X0),sF3),x0)),
    inference(superposition,[],[f32824,f18429]) ).

fof(f32935,plain,
    ! [X0] : difference(sF1,product(quotient(X0,quotient(x0,sF3)),x0)) = difference(x0,product(difference(sF3,X0),sF3)),
    inference(superposition,[],[f32824,f6691]) ).

fof(f32946,plain,
    ! [X0] : product(difference(sF3,X0),x0) = product(x0,difference(sF1,product(X0,x0))),
    inference(superposition,[],[f3,f32824]) ).

fof(f32980,plain,
    ! [X0] : product(difference(product(sF3,x0),X0),sF3) = difference(sF1,product(quotient(X0,quotient(x0,sF3)),x0)),
    inference(forward_demodulation,[],[f32935,f136]) ).

fof(f32985,plain,
    ! [X0] : difference(x0,product(product(difference(sF3,X0),sF3),x0)) = difference(sF1,product(quotient(X0,difference(sF3,one)),x0)),
    inference(forward_demodulation,[],[f32930,f2930]) ).

fof(f33000,plain,
    ! [X0] : product(difference(product(sF3,x0),X0),sF3) = difference(sF1,product(quotient(X0,sF1),x0)),
    inference(forward_demodulation,[],[f32980,f1067]) ).

fof(f33012,plain,
    ! [X0] : product(difference(sF1,X0),sF3) = difference(sF1,product(quotient(X0,sF1),x0)),
    inference(forward_demodulation,[],[f33000,f400]) ).

fof(f33057,plain,
    ! [X0] : difference(sF1,product(X0,x0)) = product(difference(sF1,product(X0,sF1)),sF3),
    inference(superposition,[],[f33012,f5]) ).

fof(f33881,plain,
    difference(sF0,product(x1,sF1)) = product(difference(sF3,sF2),sF1),
    inference(superposition,[],[f134,f23]) ).

fof(f33898,plain,
    ! [X0] : product(sF0,product(difference(sF3,product(sF1,X0)),x0)) = product(product(sF0,difference(sF0,product(X0,sF1))),sF3),
    inference(superposition,[],[f7221,f134]) ).

fof(f33921,plain,
    ! [X0] : product(difference(sF1,difference(sF3,product(sF1,X0))),sF1) = product(difference(sF1,one),difference(sF0,product(X0,sF1))),
    inference(superposition,[],[f5098,f134]) ).

fof(f33934,plain,
    ! [X0] : product(difference(sF1,difference(sF3,product(sF1,X0))),sF1) = product(product(sF3,sF0),difference(sF0,product(X0,sF1))),
    inference(forward_demodulation,[],[f33921,f1614]) ).

fof(f33939,plain,
    ! [X0] : product(product(X0,sF1),sF3) = product(sF0,product(difference(sF3,product(sF1,X0)),x0)),
    inference(forward_demodulation,[],[f33898,f3]) ).

fof(f33955,plain,
    product(product(sF4,sF3),x0) = product(difference(sF3,sF2),sF1),
    inference(forward_demodulation,[],[f33881,f16184]) ).

fof(f33966,plain,
    ! [X0] : product(difference(sF1,difference(sF3,product(sF1,X0))),sF1) = difference(sF1,product(x0,product(X0,sF1))),
    inference(forward_demodulation,[],[f33934,f19490]) ).

fof(f35566,plain,
    ! [X0] : quotient(product(product(sF1,sF1),X0),sF0) = product(product(sF1,sF1),quotient(product(X0,product(sF1,sF1)),x0)),
    inference(superposition,[],[f22902,f2069]) ).

fof(f35567,plain,
    ! [X0] : quotient(product(product(sF1,sF1),X0),sF0) = product(x0,quotient(product(x0,product(X0,product(sF1,sF1))),x0)),
    inference(forward_demodulation,[],[f35566,f2063]) ).

fof(f36769,plain,
    ! [X0] : difference(x0,product(product(product(x0,X0),x0),sF0)) = product(difference(sF3,product(X0,x0)),sF0),
    inference(superposition,[],[f132,f817]) ).

fof(f36877,plain,
    ! [X0] : product(difference(sF3,product(X0,x0)),sF0) = difference(x0,product(product(product(x0,X0),sF0),sF1)),
    inference(forward_demodulation,[],[f36769,f26420]) ).

fof(f36906,plain,
    ! [X0] : difference(x0,difference(sF0,X0)) = product(difference(sF3,product(X0,x0)),sF0),
    inference(forward_demodulation,[],[f36877,f19427]) ).

fof(f37427,plain,
    ! [X0] : difference(one,product(sF1,product(product(sF3,sF0),X0))) = quotient(quotient(product(X0,one),product(sF3,sF0)),sF1),
    inference(superposition,[],[f189,f1614]) ).

fof(f37434,plain,
    ! [X0] : difference(product(sF3,sF1),product(sF1,product(difference(sF3,one),X0))) = quotient(quotient(product(X0,product(sF3,sF1)),difference(sF3,one)),sF1),
    inference(superposition,[],[f189,f2944]) ).

fof(f37518,plain,
    ! [X0] : difference(one,product(sF1,product(product(sF3,sF0),X0))) = quotient(quotient(X0,product(sF3,sF0)),sF1),
    inference(forward_demodulation,[],[f37427,f1]) ).

fof(f37608,plain,
    ! [X0] : product(sF1,product(product(sF3,sF0),X0)) = quotient(quotient(X0,product(sF3,sF0)),sF1),
    inference(forward_demodulation,[],[f37518,f62]) ).

fof(f45844,plain,
    ! [X0] : product(difference(sF3,difference(sF1,product(X0,sF1))),sF3) = product(difference(sF3,one),difference(sF1,product(X0,x0))),
    inference(superposition,[],[f5098,f33057]) ).

fof(f46118,plain,
    product(sF0,product(difference(sF3,sF2),x0)) = product(product(sF0,product(product(sF4,sF3),x0)),sF3),
    inference(superposition,[],[f7221,f33955]) ).

fof(f46163,plain,
    product(sF0,product(difference(sF3,sF2),x0)) = product(product(x1,product(sF3,x0)),sF3),
    inference(forward_demodulation,[],[f46118,f6192]) ).

fof(f46169,plain,
    product(sF0,product(difference(sF3,sF2),x0)) = product(product(x1,sF1),sF3),
    inference(forward_demodulation,[],[f46163,f400]) ).

fof(f53098,plain,
    ! [X0] : product(product(sF1,sF1),quotient(product(X0,product(sF1,sF1)),x0)) = difference(sF0,product(x0,quotient(X0,sF0))),
    inference(superposition,[],[f22954,f2069]) ).

fof(f53112,plain,
    ! [X0] : product(x0,quotient(product(X0,x0),sF1)) = difference(sF3,product(sF1,quotient(X0,sF3))),
    inference(superposition,[],[f22954,f402]) ).

fof(f53214,plain,
    ! [X0] : quotient(product(x0,X0),sF3) = difference(sF3,product(sF1,quotient(X0,sF3))),
    inference(forward_demodulation,[],[f53112,f29227]) ).

fof(f53224,plain,
    ! [X0] : product(sF1,difference(sF0,quotient(X0,sF0))) = product(product(sF1,sF1),quotient(product(X0,product(sF1,sF1)),x0)),
    inference(forward_demodulation,[],[f53098,f2240]) ).

fof(f53282,plain,
    ! [X0] : product(sF1,difference(sF0,quotient(X0,sF0))) = product(x0,quotient(product(x0,product(X0,product(sF1,sF1))),x0)),
    inference(forward_demodulation,[],[f53224,f2063]) ).

fof(f53323,plain,
    ! [X0] : product(sF1,product(sF1,product(X0,sF1))) = product(x0,quotient(product(x0,product(X0,product(sF1,sF1))),x0)),
    inference(forward_demodulation,[],[f53282,f26979]) ).

fof(f53334,plain,
    ! [X0] : quotient(product(product(sF1,sF1),X0),sF0) = product(sF1,product(sF1,product(X0,sF1))),
    inference(backward_demodulation,[],[f35567,f53323]) ).

fof(f53340,plain,
    ! [X0] : product(sF0,product(difference(sF0,X0),sF1)) = difference(product(sF1,sF1),product(sF1,product(sF1,product(X0,sF1)))),
    inference(backward_demodulation,[],[f26303,f53334]) ).

fof(f53342,plain,
    ! [X0] : product(sF0,product(difference(sF0,X0),sF1)) = product(product(sF0,product(product(sF1,product(X0,sF1)),sF1)),sF0),
    inference(forward_demodulation,[],[f53340,f4391]) ).

fof(f53483,plain,
    ! [X0] : product(difference(sF0,X0),sF3) = product(sF1,product(product(X0,sF1),sF0)),
    inference(superposition,[],[f6755,f5]) ).

fof(f54853,plain,
    ! [X0] : difference(sF3,product(sF1,product(product(sF0,X0),sF0))) = product(product(x0,difference(sF1,X0)),sF0),
    inference(superposition,[],[f8446,f1547]) ).

fof(f54912,plain,
    ! [X0] : product(product(x0,difference(sF1,X0)),sF0) = product(difference(product(sF0,sF3),product(sF0,X0)),sF0),
    inference(forward_demodulation,[],[f54853,f4085]) ).

fof(f54936,plain,
    ! [X0] : difference(sF3,product(X0,sF0)) = product(product(x0,difference(sF1,X0)),sF0),
    inference(forward_demodulation,[],[f54912,f117]) ).

fof(f54999,plain,
    ! [X0] : product(x0,difference(sF1,X0)) = quotient(difference(sF3,product(X0,sF0)),sF0),
    inference(superposition,[],[f5,f54936]) ).

fof(f55042,plain,
    ! [X0] : product(x0,difference(sF1,X0)) = difference(product(sF0,sF3),product(sF0,X0)),
    inference(forward_demodulation,[],[f54999,f42]) ).

fof(f55765,plain,
    ! [X0] : product(difference(sF0,product(product(sF0,sF3),X0)),product(sF0,sF3)) = difference(difference(sF3,one),product(X0,product(sF0,sF3))),
    inference(superposition,[],[f125,f2862]) ).

fof(f55769,plain,
    ! [X0] : difference(sF0,product(product(sF0,sF3),product(difference(sF3,one),X0))) = quotient(quotient(product(X0,sF0),difference(sF3,one)),product(sF0,sF3)),
    inference(superposition,[],[f189,f2862]) ).

fof(f55788,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = quotient(quotient(product(X0,sF0),difference(sF3,one)),product(sF0,sF3)),
    inference(forward_demodulation,[],[f55769,f19872]) ).

fof(f55791,plain,
    ! [X0] : product(difference(sF0,product(product(sF0,sF3),X0)),product(sF0,sF3)) = product(difference(one,product(product(sF3,X0),sF0)),sF3),
    inference(forward_demodulation,[],[f55765,f7359]) ).

fof(f55804,plain,
    ! [X0] : product(difference(sF0,product(product(sF0,sF3),X0)),product(sF0,sF3)) = product(product(product(sF3,X0),sF0),sF3),
    inference(forward_demodulation,[],[f55791,f62]) ).

fof(f55814,plain,
    ! [X0] : product(product(product(sF3,X0),sF0),sF3) = product(product(sF1,difference(x0,X0)),product(sF0,sF3)),
    inference(forward_demodulation,[],[f55804,f19872]) ).

fof(f55821,plain,
    ! [X0] : quotient(product(X0,sF0),difference(sF3,one)) = product(product(product(sF3,product(difference(sF3,one),X0)),sF0),sF3),
    inference(backward_demodulation,[],[f28362,f55814]) ).

fof(f56176,plain,
    difference(x0,product(sF4,sF3)) = product(difference(sF1,sF5),sF3),
    inference(superposition,[],[f405,f29]) ).

fof(f56256,plain,
    quotient(product(x1,sF1),x0) = product(difference(sF1,sF5),sF3),
    inference(backward_demodulation,[],[f10151,f56176]) ).

fof(f56340,plain,
    product(difference(x0,one),product(x1,sF1)) = product(difference(x0,product(difference(sF1,sF5),sF3)),x0),
    inference(superposition,[],[f9296,f56256]) ).

fof(f56348,plain,
    product(difference(x0,one),product(x1,sF1)) = product(difference(x0,difference(sF1,sF5)),product(sF3,x0)),
    inference(forward_demodulation,[],[f56340,f222]) ).

fof(f56362,plain,
    product(difference(x0,one),product(x1,sF1)) = product(sF0,product(product(difference(sF1,sF5),sF3),x0)),
    inference(forward_demodulation,[],[f56348,f5176]) ).

fof(f56372,plain,
    product(difference(x0,one),product(x1,sF1)) = product(difference(x0,difference(sF1,sF5)),sF1),
    inference(forward_demodulation,[],[f56362,f15972]) ).

fof(f56378,plain,
    product(sF0,product(x1,sF1)) = product(difference(x0,difference(sF1,sF5)),sF1),
    inference(forward_demodulation,[],[f56372,f19]) ).

fof(f56394,plain,
    difference(x0,difference(sF1,sF5)) = quotient(product(sF0,product(x1,sF1)),sF1),
    inference(superposition,[],[f5,f56378]) ).

fof(f56437,plain,
    difference(x0,difference(sF1,sF5)) = difference(sF1,product(product(sF1,sF0),x1)),
    inference(forward_demodulation,[],[f56394,f7]) ).

fof(f56453,plain,
    difference(x0,difference(sF1,sF5)) = difference(sF1,product(sF3,x1)),
    inference(forward_demodulation,[],[f56437,f108]) ).

fof(f56519,plain,
    difference(sF1,sF5) = product(x0,difference(sF1,product(sF3,x1))),
    inference(superposition,[],[f3,f56453]) ).

fof(f56945,plain,
    ! [X0] : quotient(product(product(sF3,sF1),X0),sF0) = difference(sF0,product(difference(sF3,one),quotient(X0,sF0))),
    inference(superposition,[],[f287,f6926]) ).

fof(f57035,plain,
    ! [X0,X1] : quotient(difference(X0,X1),X0) = difference(X0,product(X1,quotient(one,X0))),
    inference(superposition,[],[f287,f1]) ).

fof(f57456,plain,
    ! [X0,X1] : difference(product(quotient(one,X0),X0),product(quotient(one,X0),X1)) = quotient(quotient(difference(X0,X1),X0),quotient(one,X0)),
    inference(superposition,[],[f42,f57035]) ).

fof(f57459,plain,
    ! [X0,X1] : product(X1,quotient(one,X0)) = product(X0,quotient(difference(X0,X1),X0)),
    inference(superposition,[],[f3,f57035]) ).

fof(f57572,plain,
    ! [X0,X1] : quotient(quotient(difference(X0,X1),X0),quotient(one,X0)) = difference(one,product(quotient(one,X0),X1)),
    inference(forward_demodulation,[],[f57456,f6]) ).

fof(f57655,plain,
    ! [X0,X1] : product(quotient(one,X0),X1) = quotient(quotient(difference(X0,X1),X0),quotient(one,X0)),
    inference(forward_demodulation,[],[f57572,f62]) ).

fof(f59639,plain,
    ! [X0] : product(sF0,product(sF1,X0)) = product(sF1,product(product(sF3,sF0),X0)),
    inference(superposition,[],[f3,f16493]) ).

fof(f59668,plain,
    ! [X0] : product(sF0,product(sF1,X0)) = quotient(quotient(X0,product(sF3,sF0)),sF1),
    inference(backward_demodulation,[],[f37608,f59639]) ).

fof(f64036,plain,
    product(sF3,quotient(x1,sF0)) = product(sF0,quotient(sF4,sF0)),
    inference(superposition,[],[f423,f27]) ).

fof(f64041,plain,
    ! [X0] : product(sF0,quotient(X0,sF0)) = product(sF3,quotient(difference(x0,X0),sF0)),
    inference(superposition,[],[f423,f3]) ).

fof(f64059,plain,
    ! [X0] : product(sF0,product(quotient(product(x0,X0),sF0),sF0)) = quotient(product(sF3,quotient(X0,sF0)),x0),
    inference(superposition,[],[f8655,f423]) ).

fof(f64065,plain,
    ! [X0] : product(product(sF3,quotient(X0,sF0)),sF0) = difference(difference(sF0,one),product(x0,X0)),
    inference(superposition,[],[f10274,f423]) ).

fof(f64122,plain,
    ! [X0] : difference(sF1,product(x0,X0)) = product(product(sF3,quotient(X0,sF0)),sF0),
    inference(forward_demodulation,[],[f64065,f21]) ).

fof(f64125,plain,
    ! [X0] : product(sF0,product(x0,X0)) = quotient(product(sF3,quotient(X0,sF0)),x0),
    inference(forward_demodulation,[],[f64059,f6]) ).

fof(f64313,plain,
    ! [X0] : product(product(sF0,product(sF3,quotient(X0,sF0))),sF0) = difference(sF1,difference(sF1,product(x0,X0))),
    inference(superposition,[],[f758,f64122]) ).

fof(f64315,plain,
    ! [X0,X1] : difference(X1,difference(sF1,product(sF3,quotient(X0,sF0)))) = product(difference(product(sF1,X1),difference(sF1,product(x0,X0))),sF1),
    inference(superposition,[],[f4397,f64122]) ).

fof(f68044,plain,
    quotient(difference(sF3,sF2),sF0) = product(sF0,product(sF1,product(product(sF4,sF3),x0))),
    inference(superposition,[],[f16438,f33955]) ).

fof(f68180,plain,
    quotient(difference(sF3,sF2),sF0) = quotient(product(sF4,sF3),product(sF0,sF3)),
    inference(forward_demodulation,[],[f68044,f31214]) ).

fof(f68232,plain,
    quotient(difference(sF3,sF2),sF0) = difference(sF3,quotient(product(sF3,sF4),sF0)),
    inference(forward_demodulation,[],[f68180,f22837]) ).

fof(f68263,plain,
    quotient(difference(sF3,sF2),sF0) = product(x0,product(difference(x0,sF4),sF1)),
    inference(forward_demodulation,[],[f68232,f31232]) ).

fof(f68282,plain,
    quotient(difference(sF3,sF2),sF0) = product(x0,product(x1,sF1)),
    inference(forward_demodulation,[],[f68263,f33]) ).

fof(f68312,plain,
    difference(sF1,product(x0,difference(sF3,sF2))) = product(product(sF3,product(x0,product(x1,sF1))),sF0),
    inference(superposition,[],[f64122,f68282]) ).

fof(f68612,plain,
    ! [X0] : product(x0,product(difference(sF1,X0),sF1)) = product(sF0,product(sF1,product(difference(sF3,X0),sF1))),
    inference(superposition,[],[f2250,f5889]) ).

fof(f68687,plain,
    ! [X0] : product(x0,product(difference(sF1,X0),sF1)) = quotient(difference(sF3,X0),sF0),
    inference(forward_demodulation,[],[f68612,f16438]) ).

fof(f69029,plain,
    ! [X0] : product(difference(sF3,product(sF0,X0)),x0) = product(x0,difference(sF1,product(sF0,quotient(X0,sF0)))),
    inference(superposition,[],[f32946,f860]) ).

fof(f69036,plain,
    ! [X0] : product(difference(sF3,product(x0,quotient(X0,x0))),x0) = product(x0,difference(sF1,difference(difference(x0,one),X0))),
    inference(superposition,[],[f32946,f10274]) ).

fof(f69060,plain,
    ! [X0] : product(x0,difference(sF1,X0)) = product(difference(sF3,quotient(X0,x0)),x0),
    inference(superposition,[],[f32946,f6]) ).

fof(f69069,plain,
    ! [X0] : product(product(difference(sF3,X0),x0),sF0) = difference(sF3,product(product(X0,x0),sF0)),
    inference(superposition,[],[f54936,f32946]) ).

fof(f69144,plain,
    ! [X0] : product(product(difference(sF3,X0),x0),sF0) = difference(sF3,product(product(X0,sF0),sF1)),
    inference(forward_demodulation,[],[f69069,f26420]) ).

fof(f69162,plain,
    ! [X0] : product(difference(sF3,product(x0,quotient(X0,x0))),x0) = product(x0,difference(sF1,difference(sF0,X0))),
    inference(forward_demodulation,[],[f69036,f19]) ).

fof(f69169,plain,
    ! [X0] : product(difference(sF3,product(sF0,X0)),x0) = product(x0,product(difference(sF1,difference(sF1,X0)),sF1)),
    inference(forward_demodulation,[],[f69029,f6833]) ).

fof(f69180,plain,
    ! [X0] : product(product(difference(sF3,X0),sF0),sF1) = difference(sF3,product(product(X0,sF0),sF1)),
    inference(forward_demodulation,[],[f69144,f26420]) ).

fof(f69191,plain,
    ! [X0] : product(x0,product(product(X0,sF0),sF1)) = product(difference(sF3,product(x0,quotient(X0,x0))),x0),
    inference(forward_demodulation,[],[f69162,f26462]) ).

fof(f69198,plain,
    ! [X0] : product(difference(sF3,product(sF0,X0)),x0) = quotient(difference(sF3,difference(sF1,X0)),sF0),
    inference(forward_demodulation,[],[f69169,f68687]) ).

fof(f69210,plain,
    ! [X0] : difference(difference(x0,sF3),X0) = product(x0,product(product(X0,sF0),sF1)),
    inference(forward_demodulation,[],[f69191,f734]) ).

fof(f69226,plain,
    ! [X0] : difference(product(sF0,sF3),X0) = product(x0,product(product(X0,sF0),sF1)),
    inference(forward_demodulation,[],[f69210,f1253]) ).

fof(f69301,plain,
    ! [X0] : product(x0,difference(sF1,product(sF3,quotient(X0,sF0)))) = product(difference(sF3,product(sF0,product(x0,X0))),x0),
    inference(superposition,[],[f69060,f64125]) ).

fof(f69331,plain,
    ! [X0] : difference(sF3,quotient(X0,x0)) = quotient(product(x0,difference(sF1,X0)),x0),
    inference(superposition,[],[f5,f69060]) ).

fof(f73801,plain,
    ! [X0] : quotient(product(X0,sF1),x0) = difference(product(x0,difference(sF1,quotient(sF3,X0))),sF3),
    inference(superposition,[],[f4236,f23625]) ).

fof(f75369,plain,
    product(sF3,product(sF4,sF3)) = quotient(sF5,quotient(one,sF3)),
    inference(superposition,[],[f628,f41]) ).

fof(f75373,plain,
    ! [X0,X1] : product(X0,product(difference(X0,one),X1)) = quotient(quotient(X1,X0),quotient(one,X0)),
    inference(superposition,[],[f628,f9296]) ).

fof(f75428,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(product(sF0,sF3),X0),product(sF0,sF3)))) = difference(sF0,quotient(X0,quotient(one,product(sF0,sF3)))),
    inference(superposition,[],[f19872,f628]) ).

fof(f75553,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(product(sF0,sF3),X0),product(sF0,sF3)))) = difference(sF0,quotient(X0,difference(sF3,quotient(one,sF0)))),
    inference(forward_demodulation,[],[f75428,f27849]) ).

fof(f75578,plain,
    ! [X0,X1] : product(quotient(one,X0),X1) = product(X0,product(difference(X0,one),difference(X0,X1))),
    inference(backward_demodulation,[],[f57655,f75373]) ).

fof(f75590,plain,
    product(sF3,product(sF4,sF3)) = quotient(sF5,difference(sF3,one)),
    inference(forward_demodulation,[],[f75369,f2930]) ).

fof(f75787,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(product(sF0,sF3),X0),product(sF0,sF3)))) = difference(sF0,quotient(X0,difference(sF3,x0))),
    inference(forward_demodulation,[],[f75553,f105]) ).

fof(f75957,plain,
    ! [X0] : difference(sF0,quotient(X0,product(x0,sF3))) = product(sF1,difference(x0,product(difference(product(sF0,sF3),X0),product(sF0,sF3)))),
    inference(forward_demodulation,[],[f75787,f7837]) ).

fof(f76067,plain,
    ! [X0] : difference(sF0,quotient(X0,product(x0,sF3))) = product(sF1,product(difference(product(product(sF0,sF3),x0),X0),product(sF0,sF3))),
    inference(forward_demodulation,[],[f75957,f136]) ).

fof(f76137,plain,
    ! [X0] : difference(sF0,quotient(X0,product(x0,sF3))) = product(sF1,product(difference(product(sF0,quotient(sF3,sF0)),X0),product(sF0,sF3))),
    inference(forward_demodulation,[],[f76067,f860]) ).

fof(f76183,plain,
    ! [X0] : difference(sF0,quotient(X0,product(x0,sF3))) = product(sF1,product(difference(product(sF0,sF1),X0),product(sF0,sF3))),
    inference(forward_demodulation,[],[f76137,f110]) ).

fof(f76226,plain,
    ! [X0] : difference(sF0,quotient(X0,product(x0,sF3))) = product(sF1,product(difference(one,X0),product(sF0,sF3))),
    inference(forward_demodulation,[],[f76183,f38]) ).

fof(f76254,plain,
    ! [X0] : difference(sF0,quotient(X0,product(x0,sF3))) = product(sF1,product(X0,product(sF0,sF3))),
    inference(forward_demodulation,[],[f76226,f62]) ).

fof(f76275,plain,
    ! [X0] : quotient(product(X0,sF0),difference(sF3,one)) = product(sF1,product(product(sF0,X0),product(sF0,sF3))),
    inference(backward_demodulation,[],[f23451,f76254]) ).

fof(f76285,plain,
    ! [X0] : quotient(product(X0,sF0),difference(sF3,one)) = product(sF1,quotient(difference(sF1,X0),x0)),
    inference(forward_demodulation,[],[f76275,f25767]) ).

fof(f76292,plain,
    ! [X0] : product(product(product(sF3,product(difference(sF3,one),X0)),sF0),sF3) = product(sF1,quotient(difference(sF1,X0),x0)),
    inference(backward_demodulation,[],[f55821,f76285]) ).

fof(f76293,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = quotient(product(sF1,quotient(difference(sF1,X0),x0)),product(sF0,sF3)),
    inference(backward_demodulation,[],[f55788,f76285]) ).

fof(f78647,plain,
    ! [X0] : difference(product(sF0,sF3),product(x0,difference(sF1,X0))) = product(x0,product(difference(sF3,product(X0,sF0)),sF1)),
    inference(superposition,[],[f69226,f54936]) ).

fof(f78805,plain,
    ! [X0] : difference(product(sF0,sF3),product(x0,difference(sF1,X0))) = product(x0,difference(sF0,difference(sF1,X0))),
    inference(forward_demodulation,[],[f78647,f31424]) ).

fof(f80716,plain,
    ! [X0] : difference(sF0,difference(sF1,product(sF3,quotient(X0,sF0)))) = product(difference(sF3,difference(sF1,product(x0,X0))),sF1),
    inference(superposition,[],[f31424,f64122]) ).

fof(f81551,plain,
    ! [X0] : product(x0,quotient(difference(x0,X0),sF1)) = difference(sF3,product(product(sF3,X0),sF0)),
    inference(superposition,[],[f3320,f3]) ).

fof(f81566,plain,
    ! [X0] : product(product(sF3,product(x0,X0)),sF0) = product(sF3,product(x0,quotient(X0,sF1))),
    inference(superposition,[],[f3,f3320]) ).

fof(f81617,plain,
    difference(sF1,product(x0,difference(sF3,sF2))) = product(sF3,product(x0,quotient(product(x1,sF1),sF1))),
    inference(backward_demodulation,[],[f68312,f81566]) ).

fof(f81669,plain,
    difference(sF1,product(x0,difference(sF3,sF2))) = product(sF3,product(x0,x1)),
    inference(forward_demodulation,[],[f81617,f5]) ).

fof(f81706,plain,
    product(sF3,sF4) = difference(sF1,product(x0,difference(sF3,sF2))),
    inference(forward_demodulation,[],[f81669,f27]) ).

fof(f81732,plain,
    sF5 = difference(sF1,product(x0,difference(sF3,sF2))),
    inference(forward_demodulation,[],[f81706,f29]) ).

fof(f81803,plain,
    product(x0,difference(sF3,sF2)) = product(sF1,sF5),
    inference(superposition,[],[f3,f81732]) ).

fof(f81889,plain,
    quotient(product(difference(sF3,sF2),sF3),x0) = difference(x0,product(product(sF1,sF5),sF0)),
    inference(superposition,[],[f68,f81803]) ).

fof(f81963,plain,
    quotient(product(difference(sF3,sF2),sF3),x0) = difference(x0,product(sF1,quotient(sF5,sF1))),
    inference(forward_demodulation,[],[f81889,f1549]) ).

fof(f81972,plain,
    quotient(product(difference(sF3,sF2),sF3),x0) = quotient(difference(sF3,sF5),sF1),
    inference(forward_demodulation,[],[f81963,f8324]) ).

fof(f81977,plain,
    quotient(product(difference(sF3,sF2),sF3),x0) = quotient(sF4,sF1),
    inference(forward_demodulation,[],[f81972,f41]) ).

fof(f81979,plain,
    quotient(sF4,sF1) = difference(sF3,quotient(sF2,quotient(x0,sF3))),
    inference(forward_demodulation,[],[f81977,f18405]) ).

fof(f81981,plain,
    quotient(sF4,sF1) = difference(sF3,quotient(sF2,sF1)),
    inference(forward_demodulation,[],[f81979,f1067]) ).

fof(f82055,plain,
    product(difference(sF1,quotient(sF2,sF1)),sF1) = product(sF0,product(quotient(sF4,sF1),sF1)),
    inference(superposition,[],[f5889,f81981]) ).

fof(f82059,plain,
    product(difference(sF3,sF2),sF3) = product(quotient(sF4,sF1),product(sF1,sF3)),
    inference(superposition,[],[f5126,f81981]) ).

fof(f82060,plain,
    quotient(sF2,sF1) = product(sF3,quotient(sF4,sF1)),
    inference(superposition,[],[f3,f81981]) ).

fof(f82093,plain,
    product(difference(sF3,sF2),sF3) = product(quotient(sF4,sF1),x0),
    inference(forward_demodulation,[],[f82059,f1065]) ).

fof(f82095,plain,
    product(sF0,sF4) = product(difference(sF1,quotient(sF2,sF1)),sF1),
    inference(forward_demodulation,[],[f82055,f6]) ).

fof(f82097,plain,
    product(sF0,sF4) = product(difference(sF1,one),sF2),
    inference(forward_demodulation,[],[f82095,f9296]) ).

fof(f82099,plain,
    product(sF0,sF4) = product(product(sF3,sF0),sF2),
    inference(forward_demodulation,[],[f82097,f1614]) ).

fof(f82102,plain,
    ! [X0] : difference(X0,product(sF0,product(sF2,sF3))) = product(difference(product(sF3,X0),product(sF0,sF4)),sF3),
    inference(superposition,[],[f1729,f82099]) ).

fof(f82190,plain,
    ! [X0] : difference(sF3,product(product(sF0,quotient(X0,sF0)),sF0)) = product(x0,quotient(difference(x0,quotient(difference(x0,X0),sF0)),sF1)),
    inference(superposition,[],[f81551,f64041]) ).

fof(f82191,plain,
    product(x0,quotient(difference(x0,quotient(x1,sF0)),sF1)) = difference(sF3,product(product(sF0,quotient(sF4,sF0)),sF0)),
    inference(superposition,[],[f81551,f64036]) ).

fof(f82194,plain,
    difference(sF3,product(sF5,sF0)) = product(x0,quotient(difference(x0,sF4),sF1)),
    inference(superposition,[],[f81551,f29]) ).

fof(f82206,plain,
    ! [X0] : difference(sF3,difference(sF1,product(x0,X0))) = product(x0,quotient(difference(x0,quotient(X0,sF0)),sF1)),
    inference(superposition,[],[f81551,f64122]) ).

fof(f82259,plain,
    ! [X0] : difference(sF3,difference(sF1,product(x0,X0))) = product(x0,quotient(product(sF0,product(X0,sF1)),sF1)),
    inference(forward_demodulation,[],[f82206,f26163]) ).

fof(f82269,plain,
    difference(sF3,product(sF5,sF0)) = product(x0,quotient(x1,sF1)),
    inference(forward_demodulation,[],[f82194,f33]) ).

fof(f82271,plain,
    product(x0,quotient(difference(x0,quotient(x1,sF0)),sF1)) = difference(sF3,difference(difference(sF0,one),sF4)),
    inference(forward_demodulation,[],[f82191,f10274]) ).

fof(f82272,plain,
    ! [X0] : difference(sF3,product(product(sF0,quotient(X0,sF0)),sF0)) = product(x0,quotient(product(sF0,product(difference(x0,X0),sF1)),sF1)),
    inference(forward_demodulation,[],[f82190,f26163]) ).

fof(f82296,plain,
    ! [X0] : difference(sF3,difference(sF1,product(x0,X0))) = product(x0,difference(sF1,product(product(sF1,sF0),X0))),
    inference(forward_demodulation,[],[f82259,f7]) ).

fof(f82305,plain,
    difference(sF3,difference(sF1,sF4)) = product(x0,quotient(difference(x0,quotient(x1,sF0)),sF1)),
    inference(forward_demodulation,[],[f82271,f21]) ).

fof(f82306,plain,
    ! [X0] : difference(sF3,product(product(sF0,quotient(X0,sF0)),sF0)) = product(x0,difference(sF1,product(product(sF1,sF0),difference(x0,X0)))),
    inference(forward_demodulation,[],[f82272,f7]) ).

fof(f82326,plain,
    ! [X0] : difference(sF3,difference(sF1,product(x0,X0))) = product(x0,difference(sF1,product(sF3,X0))),
    inference(forward_demodulation,[],[f82296,f108]) ).

fof(f82335,plain,
    difference(sF3,difference(sF1,sF4)) = product(x0,quotient(product(sF0,product(x1,sF1)),sF1)),
    inference(forward_demodulation,[],[f82305,f26163]) ).

fof(f82336,plain,
    ! [X0] : difference(sF3,product(product(sF0,quotient(X0,sF0)),sF0)) = product(x0,difference(sF1,product(sF3,difference(x0,X0)))),
    inference(forward_demodulation,[],[f82306,f108]) ).

fof(f82354,plain,
    ! [X0] : difference(sF0,difference(sF1,product(sF3,quotient(X0,sF0)))) = product(product(x0,difference(sF1,product(sF3,X0))),sF1),
    inference(backward_demodulation,[],[f80716,f82326]) ).

fof(f82361,plain,
    difference(sF3,difference(sF1,sF4)) = product(x0,difference(sF1,product(product(sF1,sF0),x1))),
    inference(forward_demodulation,[],[f82335,f7]) ).

fof(f82362,plain,
    ! [X0] : difference(sF3,difference(difference(sF0,one),X0)) = product(x0,difference(sF1,product(sF3,difference(x0,X0)))),
    inference(forward_demodulation,[],[f82336,f10274]) ).

fof(f82378,plain,
    product(x0,difference(sF1,product(sF3,x1))) = difference(sF3,difference(sF1,sF4)),
    inference(forward_demodulation,[],[f82361,f108]) ).

fof(f82379,plain,
    ! [X0] : difference(sF3,difference(sF1,X0)) = product(x0,difference(sF1,product(sF3,difference(x0,X0)))),
    inference(forward_demodulation,[],[f82362,f21]) ).

fof(f82392,plain,
    difference(sF1,sF5) = difference(sF3,difference(sF1,sF4)),
    inference(forward_demodulation,[],[f82378,f56519]) ).

fof(f82468,plain,
    ! [X0] : difference(sF1,product(sF3,difference(x0,X0))) = difference(x0,difference(sF3,difference(sF1,X0))),
    inference(superposition,[],[f4,f82379]) ).

fof(f83215,plain,
    ! [X0] : difference(x0,difference(sF3,X0)) = difference(sF1,product(sF3,difference(x0,product(sF1,X0)))),
    inference(superposition,[],[f82468,f4]) ).

fof(f83449,plain,
    ! [X0] : difference(x0,product(difference(x0,product(sF1,X0)),sF3)) = product(difference(x0,difference(sF3,X0)),sF3),
    inference(superposition,[],[f405,f83215]) ).

fof(f83460,plain,
    ! [X0] : product(sF3,difference(x0,product(sF1,X0))) = product(sF1,difference(x0,difference(sF3,X0))),
    inference(superposition,[],[f3,f83215]) ).

fof(f83750,plain,
    ! [X0] : product(sF3,difference(x0,quotient(X0,quotient(one,sF1)))) = product(sF1,difference(x0,difference(sF3,product(difference(sF1,X0),sF1)))),
    inference(superposition,[],[f83460,f628]) ).

fof(f83769,plain,
    ! [X0] : difference(x0,product(sF1,X0)) = difference(sF3,product(sF1,difference(x0,difference(sF3,X0)))),
    inference(superposition,[],[f4,f83460]) ).

fof(f83833,plain,
    ! [X0] : product(sF3,difference(x0,quotient(X0,quotient(one,sF1)))) = product(sF1,difference(x0,product(difference(product(sF1,sF3),X0),sF1))),
    inference(forward_demodulation,[],[f83750,f136]) ).

fof(f83868,plain,
    ! [X0] : product(sF3,difference(x0,quotient(X0,quotient(one,sF1)))) = product(sF1,difference(x0,product(difference(x0,X0),sF1))),
    inference(forward_demodulation,[],[f83833,f1065]) ).

fof(f83897,plain,
    ! [X0] : product(sF3,difference(x0,quotient(X0,sF0))) = product(sF1,difference(x0,product(difference(x0,X0),sF1))),
    inference(forward_demodulation,[],[f83868,f106]) ).

fof(f83915,plain,
    ! [X0] : product(sF3,product(sF0,product(X0,sF1))) = product(sF1,difference(x0,product(difference(x0,X0),sF1))),
    inference(forward_demodulation,[],[f83897,f26163]) ).

fof(f86128,plain,
    ! [X0] : product(x0,product(difference(x0,product(product(x0,X0),sF0)),sF1)) = difference(sF3,quotient(product(sF1,quotient(X0,sF1)),sF0)),
    inference(superposition,[],[f31232,f19566]) ).

fof(f86129,plain,
    product(x0,product(difference(x0,product(sF4,sF0)),sF1)) = difference(sF3,quotient(product(sF2,sF0),sF0)),
    inference(superposition,[],[f31232,f19692]) ).

fof(f86158,plain,
    ! [X0] : product(x0,product(difference(x0,product(X0,sF0)),sF1)) = difference(sF3,difference(sF0,product(product(sF0,sF3),X0))),
    inference(superposition,[],[f31232,f7]) ).

fof(f86166,plain,
    ! [X0] : product(sF1,product(quotient(product(sF3,X0),sF0),sF0)) = product(x0,product(product(x0,product(difference(x0,X0),sF1)),sF0)),
    inference(superposition,[],[f6032,f31232]) ).

fof(f86198,plain,
    ! [X0] : product(sF1,product(quotient(product(sF3,X0),sF0),sF0)) = product(x0,difference(sF3,product(sF1,difference(x0,X0)))),
    inference(forward_demodulation,[],[f86166,f19446]) ).

fof(f86205,plain,
    ! [X0] : difference(sF3,product(sF1,difference(x0,X0))) = product(x0,product(difference(x0,product(X0,sF0)),sF1)),
    inference(forward_demodulation,[],[f86158,f19872]) ).

fof(f86234,plain,
    difference(sF3,sF2) = product(x0,product(difference(x0,product(sF4,sF0)),sF1)),
    inference(forward_demodulation,[],[f86129,f5]) ).

fof(f86235,plain,
    ! [X0] : product(x0,product(difference(x0,product(product(x0,X0),sF0)),sF1)) = difference(sF3,product(sF1,quotient(X0,product(sF0,sF1)))),
    inference(forward_demodulation,[],[f86128,f2519]) ).

fof(f86243,plain,
    ! [X0] : product(sF1,product(sF3,X0)) = product(x0,difference(sF3,product(sF1,difference(x0,X0)))),
    inference(forward_demodulation,[],[f86198,f6]) ).

fof(f86250,plain,
    ! [X0] : difference(sF3,product(sF1,difference(x0,X0))) = product(x0,difference(sF3,difference(sF1,X0))),
    inference(forward_demodulation,[],[f86205,f31425]) ).

fof(f86275,plain,
    difference(sF3,sF2) = product(x0,difference(sF3,difference(sF1,sF4))),
    inference(forward_demodulation,[],[f86234,f31425]) ).

fof(f86276,plain,
    ! [X0] : product(x0,product(difference(x0,product(product(x0,X0),sF0)),sF1)) = difference(sF3,product(sF1,quotient(X0,one))),
    inference(forward_demodulation,[],[f86235,f38]) ).

fof(f86288,plain,
    ! [X0] : product(sF1,product(sF3,X0)) = product(x0,product(x0,difference(sF3,difference(sF1,X0)))),
    inference(backward_demodulation,[],[f86243,f86250]) ).

fof(f86293,plain,
    ! [X0] : difference(x0,product(sF1,X0)) = product(x0,difference(sF3,difference(sF1,difference(sF3,X0)))),
    inference(backward_demodulation,[],[f83769,f86250]) ).

fof(f86312,plain,
    difference(sF3,sF2) = product(x0,difference(sF1,sF5)),
    inference(forward_demodulation,[],[f86275,f82392]) ).

fof(f86313,plain,
    ! [X0] : difference(sF3,product(sF1,X0)) = product(x0,product(difference(x0,product(product(x0,X0),sF0)),sF1)),
    inference(forward_demodulation,[],[f86276,f80]) ).

fof(f86335,plain,
    ! [X0] : difference(sF3,product(sF1,X0)) = product(x0,difference(sF3,difference(sF1,product(x0,X0)))),
    inference(forward_demodulation,[],[f86313,f31425]) ).

fof(f86349,plain,
    ! [X0] : difference(sF3,product(sF1,X0)) = product(x0,product(x0,difference(sF1,product(sF3,X0)))),
    inference(forward_demodulation,[],[f86335,f82326]) ).

fof(f86371,plain,
    difference(sF3,product(sF5,sF0)) = product(difference(sF3,sF2),sF0),
    inference(superposition,[],[f54936,f86312]) ).

fof(f86375,plain,
    difference(x0,product(difference(sF3,sF2),sF3)) = quotient(product(difference(sF1,sF5),sF1),x0),
    inference(superposition,[],[f403,f86312]) ).

fof(f86378,plain,
    product(sF0,product(difference(sF3,sF2),x0)) = product(difference(sF1,sF5),x0),
    inference(superposition,[],[f817,f86312]) ).

fof(f86444,plain,
    product(product(x1,sF1),sF3) = product(difference(sF1,sF5),x0),
    inference(forward_demodulation,[],[f86378,f46169]) ).

fof(f86447,plain,
    difference(x0,product(difference(sF3,sF2),sF3)) = difference(sF1,quotient(sF5,quotient(x0,sF1))),
    inference(forward_demodulation,[],[f86375,f18405]) ).

fof(f86450,plain,
    product(difference(sF3,sF2),sF0) = product(x0,quotient(x1,sF1)),
    inference(forward_demodulation,[],[f86371,f82269]) ).

fof(f86476,plain,
    difference(x0,product(difference(sF3,sF2),sF3)) = difference(sF1,quotient(sF5,difference(sF3,one))),
    inference(forward_demodulation,[],[f86447,f2152]) ).

fof(f86486,plain,
    difference(x0,product(difference(sF3,sF2),sF3)) = difference(sF1,product(sF3,product(sF4,sF3))),
    inference(forward_demodulation,[],[f86476,f75590]) ).

fof(f86490,plain,
    product(difference(product(sF3,x0),sF2),sF3) = difference(sF1,product(sF3,product(sF4,sF3))),
    inference(forward_demodulation,[],[f86486,f136]) ).

fof(f86493,plain,
    product(difference(sF1,sF2),sF3) = difference(sF1,product(sF3,product(sF4,sF3))),
    inference(forward_demodulation,[],[f86490,f400]) ).

fof(f86495,plain,
    product(x1,sF3) = difference(sF1,product(sF3,product(sF4,sF3))),
    inference(forward_demodulation,[],[f86493,f40]) ).

fof(f86572,plain,
    product(difference(x0,sF5),x0) = product(difference(x0,sF1),product(product(x1,sF1),sF3)),
    inference(superposition,[],[f5096,f86444]) ).

fof(f86645,plain,
    product(difference(x0,sF5),x0) = product(difference(sF3,one),product(product(x1,sF1),sF3)),
    inference(forward_demodulation,[],[f86572,f2882]) ).

fof(f86661,plain,
    product(difference(x0,sF5),x0) = product(difference(sF3,product(x1,sF1)),sF3),
    inference(forward_demodulation,[],[f86645,f5098]) ).

fof(f86667,plain,
    product(difference(x0,sF5),x0) = product(difference(sF3,x1),product(sF1,sF3)),
    inference(forward_demodulation,[],[f86661,f222]) ).

fof(f86671,plain,
    product(difference(x0,sF5),x0) = product(difference(sF3,x1),x0),
    inference(forward_demodulation,[],[f86667,f1065]) ).

fof(f86672,plain,
    product(sF0,product(sF5,x0)) = product(difference(sF3,x1),x0),
    inference(forward_demodulation,[],[f86671,f858]) ).

fof(f86674,plain,
    difference(sF3,product(x1,quotient(x0,sF3))) = quotient(product(sF0,product(sF5,x0)),sF3),
    inference(superposition,[],[f287,f86672]) ).

fof(f86688,plain,
    difference(sF3,x1) = quotient(product(sF0,product(sF5,x0)),x0),
    inference(superposition,[],[f5,f86672]) ).

fof(f86748,plain,
    difference(sF3,x1) = difference(x0,product(product(x0,sF0),sF5)),
    inference(forward_demodulation,[],[f86688,f7]) ).

fof(f86760,plain,
    difference(sF3,product(x1,quotient(x0,sF3))) = difference(x0,quotient(sF5,quotient(sF3,x0))),
    inference(forward_demodulation,[],[f86674,f20753]) ).

fof(f86774,plain,
    difference(sF3,x1) = difference(x0,product(one,sF5)),
    inference(forward_demodulation,[],[f86748,f32]) ).

fof(f86779,plain,
    difference(sF3,product(x1,quotient(x0,sF3))) = difference(x0,quotient(sF5,sF0)),
    inference(forward_demodulation,[],[f86760,f84]) ).

fof(f86787,plain,
    difference(sF3,x1) = difference(x0,sF5),
    inference(forward_demodulation,[],[f86774,f2]) ).

fof(f86790,plain,
    difference(sF3,product(x1,quotient(x0,sF3))) = product(sF0,product(sF5,sF1)),
    inference(forward_demodulation,[],[f86779,f26163]) ).

fof(f86793,plain,
    difference(sF3,product(x1,sF1)) = product(sF0,product(sF5,sF1)),
    inference(forward_demodulation,[],[f86790,f1067]) ).

fof(f86801,plain,
    product(product(sF5,sF3),x0) = difference(sF0,product(difference(sF3,x1),sF1)),
    inference(superposition,[],[f16089,f86787]) ).

fof(f87040,plain,
    difference(product(sF1,sF3),product(sF1,x1)) = quotient(product(sF0,product(sF5,sF1)),sF1),
    inference(superposition,[],[f42,f86793]) ).

fof(f87074,plain,
    difference(product(sF1,sF3),product(sF1,x1)) = difference(sF1,product(product(sF1,sF0),sF5)),
    inference(forward_demodulation,[],[f87040,f7]) ).

fof(f87083,plain,
    difference(product(sF1,sF3),product(sF1,x1)) = difference(sF1,product(sF3,sF5)),
    inference(forward_demodulation,[],[f87074,f108]) ).

fof(f87087,plain,
    difference(sF1,product(sF3,sF5)) = difference(product(sF1,sF3),sF2),
    inference(forward_demodulation,[],[f87083,f23]) ).

fof(f87089,plain,
    difference(x0,sF2) = difference(sF1,product(sF3,sF5)),
    inference(forward_demodulation,[],[f87087,f1065]) ).

fof(f87103,plain,
    product(sF3,sF5) = product(sF1,difference(x0,sF2)),
    inference(superposition,[],[f3,f87089]) ).

fof(f87243,plain,
    difference(sF0,product(difference(x0,sF2),sF1)) = product(difference(sF3,product(sF3,sF5)),sF1),
    inference(superposition,[],[f134,f87103]) ).

fof(f87313,plain,
    product(sF5,sF1) = difference(sF0,product(difference(x0,sF2),sF1)),
    inference(forward_demodulation,[],[f87243,f4]) ).

fof(f87323,plain,
    product(sF5,sF1) = product(product(sF2,sF3),x0),
    inference(forward_demodulation,[],[f87313,f16089]) ).

fof(f88058,plain,
    ! [X0] : difference(X0,difference(sF1,difference(sF3,sF2))) = product(difference(product(sF1,X0),product(x0,quotient(x1,sF1))),sF1),
    inference(superposition,[],[f4397,f86450]) ).

fof(f88124,plain,
    ! [X0] : difference(X0,difference(sF1,difference(sF3,sF2))) = difference(X0,product(sF3,product(quotient(x1,sF1),sF1))),
    inference(forward_demodulation,[],[f88058,f7488]) ).

fof(f88142,plain,
    ! [X0] : difference(X0,product(sF3,x1)) = difference(X0,difference(sF1,difference(sF3,sF2))),
    inference(forward_demodulation,[],[f88124,f6]) ).

fof(f88189,plain,
    difference(sF1,difference(sF3,sF2)) = difference(one,product(sF3,x1)),
    inference(superposition,[],[f62,f88142]) ).

fof(f88308,plain,
    product(sF3,x1) = difference(sF1,difference(sF3,sF2)),
    inference(forward_demodulation,[],[f88189,f62]) ).

fof(f89557,plain,
    difference(x0,product(sF1,sF2)) = product(x0,difference(sF3,product(sF3,x1))),
    inference(superposition,[],[f86293,f88308]) ).

fof(f89561,plain,
    ! [X0] : difference(x0,product(difference(x0,product(sF1,X0)),sF3)) = quotient(product(difference(sF3,difference(sF1,difference(sF3,X0))),sF1),x0),
    inference(superposition,[],[f403,f86293]) ).

fof(f89641,plain,
    ! [X0] : product(difference(x0,difference(sF3,X0)),sF3) = quotient(product(difference(sF3,difference(sF1,difference(sF3,X0))),sF1),x0),
    inference(forward_demodulation,[],[f89561,f83449]) ).

fof(f89645,plain,
    product(x0,x1) = difference(x0,product(sF1,sF2)),
    inference(forward_demodulation,[],[f89557,f4]) ).

fof(f89699,plain,
    sF4 = difference(x0,product(sF1,sF2)),
    inference(forward_demodulation,[],[f89645,f27]) ).

fof(f89841,plain,
    product(difference(sF1,product(sF1,sF2)),sF1) = product(sF3,product(sF4,sF1)),
    inference(superposition,[],[f5887,f89699]) ).

fof(f89846,plain,
    product(sF0,quotient(product(sF1,sF2),sF0)) = product(sF3,quotient(sF4,sF0)),
    inference(superposition,[],[f64041,f89699]) ).

fof(f89899,plain,
    product(sF3,quotient(sF4,sF0)) = product(sF0,product(sF1,product(sF2,sF1))),
    inference(forward_demodulation,[],[f89846,f27049]) ).

fof(f89904,plain,
    product(sF3,product(sF4,sF1)) = product(difference(sF1,sF1),product(sF2,sF1)),
    inference(forward_demodulation,[],[f89841,f222]) ).

fof(f89915,plain,
    quotient(sF2,sF0) = product(sF3,quotient(sF4,sF0)),
    inference(forward_demodulation,[],[f89899,f16438]) ).

fof(f89917,plain,
    product(sF3,product(sF4,sF1)) = product(one,product(sF2,sF1)),
    inference(forward_demodulation,[],[f89904,f50]) ).

fof(f89924,plain,
    product(sF2,sF1) = product(sF3,product(sF4,sF1)),
    inference(forward_demodulation,[],[f89917,f2]) ).

fof(f90018,plain,
    difference(sF3,quotient(sF2,sF0)) = quotient(sF4,sF0),
    inference(superposition,[],[f4,f89915]) ).

fof(f90107,plain,
    product(difference(sF3,sF2),sF3) = product(quotient(sF4,sF0),product(sF0,sF3)),
    inference(superposition,[],[f5126,f90018]) ).

fof(f90143,plain,
    product(difference(sF3,sF2),sF3) = quotient(product(sF4,sF1),x0),
    inference(forward_demodulation,[],[f90107,f26333]) ).

fof(f90239,plain,
    product(x0,product(product(sF4,sF1),sF0)) = product(sF1,product(product(sF2,sF1),sF0)),
    inference(superposition,[],[f6442,f89924]) ).

fof(f90294,plain,
    product(x0,product(product(sF4,sF1),sF0)) = product(difference(sF0,sF2),sF3),
    inference(forward_demodulation,[],[f90239,f53483]) ).

fof(f95279,plain,
    ! [X0] : product(sF3,quotient(X0,sF3)) = product(sF1,quotient(difference(x0,X0),sF3)),
    inference(superposition,[],[f427,f3]) ).

fof(f97747,plain,
    product(difference(sF3,sF2),sF3) = product(x0,product(x1,sF3)),
    inference(superposition,[],[f5890,f40]) ).

fof(f97781,plain,
    ! [X0] : difference(x0,product(product(difference(sF3,X0),sF3),x0)) = product(sF0,product(difference(sF0,product(difference(sF1,X0),sF3)),sF1)),
    inference(superposition,[],[f26249,f5890]) ).

fof(f97847,plain,
    ! [X0] : difference(sF1,product(quotient(X0,difference(sF3,one)),x0)) = product(sF0,product(difference(sF0,product(difference(sF1,X0),sF3)),sF1)),
    inference(forward_demodulation,[],[f97781,f32985]) ).

fof(f97874,plain,
    product(quotient(sF4,sF1),x0) = product(x0,product(x1,sF3)),
    inference(backward_demodulation,[],[f82093,f97747]) ).

fof(f97898,plain,
    quotient(product(sF4,sF1),x0) = product(x0,product(x1,sF3)),
    inference(backward_demodulation,[],[f90143,f97747]) ).

fof(f98102,plain,
    product(product(sF3,quotient(sF4,sF1)),x0) = product(sF1,difference(x0,product(x0,product(x1,sF3)))),
    inference(superposition,[],[f32380,f97874]) ).

fof(f98161,plain,
    product(product(sF3,quotient(sF4,sF1)),x0) = product(sF1,product(x1,sF3)),
    inference(forward_demodulation,[],[f98102,f4]) ).

fof(f98178,plain,
    product(quotient(sF2,sF1),x0) = product(sF1,product(x1,sF3)),
    inference(forward_demodulation,[],[f98161,f82060]) ).

fof(f98541,plain,
    quotient(sF2,sF1) = quotient(product(sF1,product(x1,sF3)),x0),
    inference(superposition,[],[f5,f98178]) ).

fof(f98608,plain,
    product(product(sF4,sF1),sF0) = product(product(product(x0,product(x1,sF3)),sF0),sF1),
    inference(superposition,[],[f26661,f97898]) ).

fof(f98639,plain,
    difference(sF0,product(x1,sF3)) = product(product(sF4,sF1),sF0),
    inference(forward_demodulation,[],[f98608,f19427]) ).

fof(f98652,plain,
    product(product(sF4,sF0),x0) = product(product(sF4,sF1),sF0),
    inference(forward_demodulation,[],[f98639,f18741]) ).

fof(f98664,plain,
    product(x0,product(product(sF4,sF0),x0)) = product(difference(sF0,sF2),sF3),
    inference(backward_demodulation,[],[f90294,f98652]) ).

fof(f98673,plain,
    product(sF0,sF3) = product(difference(product(sF0,product(difference(sF0,sF2),sF3)),sF5),sF0),
    inference(backward_demodulation,[],[f6601,f98664]) ).

fof(f100947,plain,
    product(sF3,product(product(sF4,sF3),sF0)) = product(sF1,quotient(product(difference(sF1,sF5),sF3),sF1)),
    inference(superposition,[],[f19579,f56176]) ).

fof(f101000,plain,
    product(sF3,product(product(sF4,sF3),sF0)) = product(sF1,difference(sF1,product(sF5,quotient(sF3,sF1)))),
    inference(forward_demodulation,[],[f100947,f287]) ).

fof(f101023,plain,
    product(sF3,product(product(sF4,sF3),sF0)) = product(sF5,quotient(sF3,sF1)),
    inference(forward_demodulation,[],[f101000,f3]) ).

fof(f101036,plain,
    product(sF5,product(sF3,sF0)) = product(sF3,product(product(sF4,sF3),sF0)),
    inference(forward_demodulation,[],[f101023,f1563]) ).

fof(f101058,plain,
    quotient(product(sF5,product(sF3,sF0)),sF0) = difference(sF0,product(product(sF0,sF3),product(sF4,sF3))),
    inference(superposition,[],[f7,f101036]) ).

fof(f101108,plain,
    quotient(product(sF5,product(sF3,sF0)),sF0) = product(difference(product(sF3,sF0),product(sF0,sF4)),sF3),
    inference(forward_demodulation,[],[f101058,f8227]) ).

fof(f101121,plain,
    quotient(product(sF5,product(sF3,sF0)),sF0) = difference(sF0,product(sF0,product(sF2,sF3))),
    inference(forward_demodulation,[],[f101108,f82102]) ).

fof(f101133,plain,
    product(sF2,sF3) = quotient(product(sF5,product(sF3,sF0)),sF0),
    inference(forward_demodulation,[],[f101121,f4]) ).

fof(f101141,plain,
    product(sF2,sF3) = difference(sF0,product(product(sF0,sF5),sF3)),
    inference(forward_demodulation,[],[f101133,f7]) ).

fof(f101144,plain,
    product(quotient(sF5,sF1),x0) = product(sF2,sF3),
    inference(forward_demodulation,[],[f101141,f7237]) ).

fof(f101160,plain,
    quotient(sF5,sF1) = quotient(product(sF2,sF3),x0),
    inference(superposition,[],[f5,f101144]) ).

fof(f102505,plain,
    product(product(x0,sF2),sF0) = product(x0,quotient(sF5,sF1)),
    inference(superposition,[],[f3196,f101160]) ).

fof(f102784,plain,
    ! [X0] : difference(X0,difference(sF1,product(x0,sF2))) = product(difference(product(sF1,X0),product(x0,quotient(sF5,sF1))),sF1),
    inference(superposition,[],[f4397,f102505]) ).

fof(f102850,plain,
    ! [X0] : difference(X0,difference(sF1,product(x0,sF2))) = difference(X0,product(sF3,product(quotient(sF5,sF1),sF1))),
    inference(forward_demodulation,[],[f102784,f7488]) ).

fof(f102865,plain,
    ! [X0] : difference(X0,product(sF3,sF5)) = difference(X0,difference(sF1,product(x0,sF2))),
    inference(forward_demodulation,[],[f102850,f6]) ).

fof(f102967,plain,
    difference(sF1,product(sF3,difference(x0,product(x0,sF2)))) = difference(x0,difference(sF3,product(sF3,sF5))),
    inference(superposition,[],[f82468,f102865]) ).

fof(f102984,plain,
    difference(x0,sF5) = difference(sF1,product(sF3,difference(x0,product(x0,sF2)))),
    inference(forward_demodulation,[],[f102967,f4]) ).

fof(f103066,plain,
    difference(x0,sF5) = difference(sF1,product(sF3,sF2)),
    inference(forward_demodulation,[],[f102984,f4]) ).

fof(f103129,plain,
    difference(sF3,x1) = difference(sF1,product(sF3,sF2)),
    inference(forward_demodulation,[],[f103066,f86787]) ).

fof(f103187,plain,
    ! [X0] : difference(X0,product(difference(sF3,x1),sF1)) = product(difference(product(sF1,X0),product(sF3,sF2)),sF1),
    inference(superposition,[],[f136,f103129]) ).

fof(f103216,plain,
    ! [X0] : difference(X0,product(difference(sF3,x1),sF1)) = difference(X0,product(sF0,product(sF2,sF1))),
    inference(forward_demodulation,[],[f103187,f7487]) ).

fof(f103244,plain,
    product(product(sF5,sF3),x0) = difference(sF0,product(sF0,product(sF2,sF1))),
    inference(backward_demodulation,[],[f86801,f103216]) ).

fof(f103298,plain,
    product(sF2,sF1) = product(product(sF5,sF3),x0),
    inference(forward_demodulation,[],[f103244,f4]) ).

fof(f103325,plain,
    product(sF5,sF3) = quotient(product(sF2,sF1),x0),
    inference(superposition,[],[f5,f103298]) ).

fof(f103810,plain,
    product(sF1,product(product(sF2,sF1),sF0)) = difference(sF0,product(sF5,sF3)),
    inference(superposition,[],[f2186,f103325]) ).

fof(f103847,plain,
    product(difference(sF0,sF2),sF3) = difference(sF0,product(sF5,sF3)),
    inference(forward_demodulation,[],[f103810,f53483]) ).

fof(f103974,plain,
    product(sF5,sF3) = product(sF0,product(difference(sF0,sF2),sF3)),
    inference(superposition,[],[f3,f103847]) ).

fof(f104009,plain,
    product(sF0,sF3) = product(difference(product(sF5,sF3),sF5),sF0),
    inference(backward_demodulation,[],[f98673,f103974]) ).

fof(f104025,plain,
    product(sF0,sF3) = product(quotient(sF4,sF5),sF0),
    inference(forward_demodulation,[],[f104009,f4885]) ).

fof(f104050,plain,
    quotient(product(sF0,sF3),sF0) = quotient(sF4,sF5),
    inference(superposition,[],[f5,f104025]) ).

fof(f104102,plain,
    difference(sF3,one) = quotient(sF4,sF5),
    inference(forward_demodulation,[],[f104050,f1290]) ).

fof(f104319,plain,
    product(sF5,quotient(sF5,sF4)) = quotient(sF5,difference(sF3,one)),
    inference(superposition,[],[f13231,f104102]) ).

fof(f104326,plain,
    product(sF3,product(sF4,sF3)) = product(sF5,quotient(sF5,sF4)),
    inference(forward_demodulation,[],[f104319,f75590]) ).

fof(f104345,plain,
    product(sF3,product(sF4,sF3)) = product(sF5,sF3),
    inference(forward_demodulation,[],[f104326,f86]) ).

fof(f104352,plain,
    product(x1,sF3) = difference(sF1,product(sF5,sF3)),
    inference(backward_demodulation,[],[f86495,f104345]) ).

fof(f104684,plain,
    product(sF5,sF3) = product(sF1,product(x1,sF3)),
    inference(superposition,[],[f3,f104352]) ).

fof(f104728,plain,
    quotient(sF2,sF1) = quotient(product(sF5,sF3),x0),
    inference(backward_demodulation,[],[f98541,f104684]) ).

fof(f108702,plain,
    product(product(x0,sF5),sF0) = product(x0,quotient(sF2,sF1)),
    inference(superposition,[],[f3196,f104728]) ).

fof(f108771,plain,
    ! [X0] : difference(X0,difference(sF1,product(x0,sF5))) = product(difference(product(sF1,X0),product(x0,quotient(sF2,sF1))),sF1),
    inference(superposition,[],[f4397,f108702]) ).

fof(f108838,plain,
    ! [X0] : difference(X0,difference(sF1,product(x0,sF5))) = difference(X0,product(sF3,product(quotient(sF2,sF1),sF1))),
    inference(forward_demodulation,[],[f108771,f7488]) ).

fof(f108854,plain,
    ! [X0] : difference(X0,product(sF3,sF2)) = difference(X0,difference(sF1,product(x0,sF5))),
    inference(forward_demodulation,[],[f108838,f6]) ).

fof(f108895,plain,
    difference(one,product(sF3,sF2)) = difference(sF1,product(x0,sF5)),
    inference(superposition,[],[f62,f108854]) ).

fof(f109025,plain,
    product(sF3,sF2) = difference(sF1,product(x0,sF5)),
    inference(forward_demodulation,[],[f108895,f62]) ).

fof(f109175,plain,
    product(product(sF3,sF2),sF1) = product(difference(sF1,x0),product(sF5,sF1)),
    inference(superposition,[],[f222,f109025]) ).

fof(f109214,plain,
    product(product(sF3,sF2),sF1) = product(sF3,product(sF5,sF1)),
    inference(forward_demodulation,[],[f109175,f1066]) ).

fof(f109552,plain,
    ! [X0] : difference(X0,product(sF2,product(sF1,sF3))) = product(difference(product(sF3,X0),product(sF3,product(sF5,sF1))),sF3),
    inference(superposition,[],[f1729,f109214]) ).

fof(f109624,plain,
    ! [X0] : difference(X0,product(product(sF5,sF1),sF3)) = difference(X0,product(sF2,product(sF1,sF3))),
    inference(forward_demodulation,[],[f109552,f117]) ).

fof(f109645,plain,
    ! [X0] : difference(X0,product(product(sF5,sF1),sF3)) = difference(X0,product(sF2,x0)),
    inference(forward_demodulation,[],[f109624,f1065]) ).

fof(f109740,plain,
    product(x0,quotient(product(product(sF5,sF1),sF3),x0)) = product(sF4,quotient(difference(x1,product(sF2,x0)),x0)),
    inference(superposition,[],[f19168,f109645]) ).

fof(f109803,plain,
    product(x0,quotient(product(product(sF5,sF1),sF3),x0)) = product(x0,quotient(product(sF2,x0),x0)),
    inference(forward_demodulation,[],[f109740,f19168]) ).

fof(f109884,plain,
    product(x0,sF2) = product(x0,quotient(product(product(sF5,sF1),sF3),x0)),
    inference(forward_demodulation,[],[f109803,f5]) ).

fof(f109949,plain,
    product(x0,sF2) = product(product(x0,product(sF5,sF1)),sF0),
    inference(forward_demodulation,[],[f109884,f3196]) ).

fof(f109982,plain,
    difference(sF3,product(sF1,sF5)) = product(x0,sF2),
    inference(forward_demodulation,[],[f109949,f19446]) ).

fof(f110033,plain,
    product(sF1,sF5) = product(sF3,product(x0,sF2)),
    inference(superposition,[],[f3,f109982]) ).

fof(f110225,plain,
    difference(sF2,product(product(sF2,sF3),x0)) = quotient(product(sF1,sF5),sF2),
    inference(superposition,[],[f7,f110033]) ).

fof(f110278,plain,
    difference(sF2,product(sF5,sF1)) = quotient(product(sF1,sF5),sF2),
    inference(forward_demodulation,[],[f110225,f87323]) ).

fof(f110303,plain,
    quotient(sF2,sF5) = difference(product(sF5,difference(sF2,product(sF5,sF1))),product(sF5,sF1)),
    inference(superposition,[],[f2803,f110278]) ).

fof(f118197,plain,
    ! [X0] : product(sF1,product(quotient(X0,product(sF3,sF0)),sF0)) = product(difference(sF0,product(sF0,product(sF1,X0))),sF3),
    inference(superposition,[],[f6755,f59668]) ).

fof(f118230,plain,
    ! [X0] : product(sF1,product(quotient(X0,product(sF3,sF0)),sF0)) = product(product(sF1,X0),sF3),
    inference(forward_demodulation,[],[f118197,f4]) ).

fof(f118264,plain,
    ! [X0] : product(x0,product(difference(sF3,X0),sF3)) = product(product(sF1,X0),sF3),
    inference(backward_demodulation,[],[f18468,f118230]) ).

fof(f118401,plain,
    ! [X0] : product(sF1,quotient(product(difference(sF3,X0),sF3),sF3)) = product(sF3,quotient(product(product(sF1,X0),sF3),sF3)),
    inference(superposition,[],[f427,f118264]) ).

fof(f118403,plain,
    ! [X0] : product(product(difference(sF3,X0),sF3),x0) = product(sF0,product(product(product(sF1,X0),sF3),x0)),
    inference(superposition,[],[f817,f118264]) ).

fof(f118493,plain,
    ! [X0] : product(difference(x0,product(sF1,X0)),sF1) = product(product(difference(sF3,X0),sF3),x0),
    inference(forward_demodulation,[],[f118403,f15972]) ).

fof(f118495,plain,
    ! [X0] : product(sF3,product(sF1,X0)) = product(sF1,quotient(product(difference(sF3,X0),sF3),sF3)),
    inference(forward_demodulation,[],[f118401,f5]) ).

fof(f118573,plain,
    ! [X0] : difference(sF3,product(X0,sF1)) = product(product(difference(sF3,X0),sF3),x0),
    inference(forward_demodulation,[],[f118493,f1072]) ).

fof(f118574,plain,
    ! [X0] : product(sF1,difference(sF3,X0)) = product(sF3,product(sF1,X0)),
    inference(forward_demodulation,[],[f118495,f5]) ).

fof(f118624,plain,
    ! [X0] : difference(sF1,product(quotient(X0,difference(sF3,one)),x0)) = difference(x0,difference(sF3,product(X0,sF1))),
    inference(backward_demodulation,[],[f32985,f118573]) ).

fof(f118707,plain,
    ! [X0] : product(sF0,product(difference(sF0,product(difference(sF1,X0),sF3)),sF1)) = difference(x0,difference(sF3,product(X0,sF1))),
    inference(backward_demodulation,[],[f97847,f118624]) ).

fof(f118758,plain,
    ! [X0] : product(sF3,difference(sF0,X0)) = product(sF1,difference(sF3,product(product(X0,sF0),sF1))),
    inference(superposition,[],[f118574,f26461]) ).

fof(f118783,plain,
    ! [X0] : product(sF1,difference(sF3,product(difference(sF1,X0),sF1))) = product(sF3,quotient(X0,quotient(one,sF1))),
    inference(superposition,[],[f118574,f628]) ).

fof(f118786,plain,
    ! [X0] : product(sF3,X0) = product(sF1,difference(sF3,difference(sF1,X0))),
    inference(superposition,[],[f118574,f3]) ).

fof(f118867,plain,
    ! [X0] : product(sF3,quotient(X0,sF0)) = product(sF1,difference(sF3,product(difference(sF1,X0),sF1))),
    inference(forward_demodulation,[],[f118783,f106]) ).

fof(f118876,plain,
    ! [X0] : product(sF3,difference(sF0,X0)) = product(sF1,product(product(difference(sF3,X0),sF0),sF1)),
    inference(forward_demodulation,[],[f118758,f69180]) ).

fof(f118904,plain,
    ! [X0] : product(sF3,quotient(X0,sF0)) = product(sF1,product(difference(product(sF1,sF3),X0),sF1)),
    inference(forward_demodulation,[],[f118867,f136]) ).

fof(f118909,plain,
    ! [X0] : product(sF3,difference(sF0,X0)) = difference(sF0,difference(sF3,X0)),
    inference(forward_demodulation,[],[f118876,f26461]) ).

fof(f118924,plain,
    ! [X0] : product(sF3,quotient(X0,sF0)) = product(sF1,product(difference(x0,X0),sF1)),
    inference(forward_demodulation,[],[f118904,f1065]) ).

fof(f119115,plain,
    ! [X0] : product(product(sF0,product(sF3,X0)),sF0) = quotient(difference(sF3,difference(sF1,X0)),sF1),
    inference(superposition,[],[f213,f118786]) ).

fof(f119126,plain,
    ! [X0] : difference(sF1,product(sF3,X0)) = difference(sF3,difference(sF1,X0)),
    inference(superposition,[],[f4,f118786]) ).

fof(f119185,plain,
    ! [X0] : product(difference(sF3,product(sF0,X0)),x0) = quotient(difference(sF1,product(sF3,X0)),sF0),
    inference(backward_demodulation,[],[f69198,f119126]) ).

fof(f119231,plain,
    ! [X0] : difference(sF3,product(sF1,difference(x0,X0))) = product(x0,difference(sF1,product(sF3,X0))),
    inference(backward_demodulation,[],[f86250,f119126]) ).

fof(f119233,plain,
    ! [X0] : product(sF1,product(sF3,X0)) = product(x0,product(x0,difference(sF1,product(sF3,X0)))),
    inference(backward_demodulation,[],[f86288,f119126]) ).

fof(f119290,plain,
    ! [X0] : product(difference(sF3,one),difference(sF1,product(X0,x0))) = product(difference(sF1,product(sF3,product(X0,sF1))),sF3),
    inference(backward_demodulation,[],[f45844,f119126]) ).

fof(f119301,plain,
    ! [X0] : difference(sF1,product(sF3,product(x0,X0))) = product(x0,difference(sF1,product(sF3,X0))),
    inference(backward_demodulation,[],[f82326,f119126]) ).

fof(f119320,plain,
    ! [X0] : difference(x0,product(sF1,X0)) = product(x0,difference(sF1,product(sF3,difference(sF3,X0)))),
    inference(backward_demodulation,[],[f86293,f119126]) ).

fof(f119343,plain,
    ! [X0] : product(difference(x0,difference(sF3,X0)),sF3) = quotient(product(difference(sF1,product(sF3,difference(sF3,X0))),sF1),x0),
    inference(backward_demodulation,[],[f89641,f119126]) ).

fof(f119398,plain,
    ! [X0] : difference(product(sF1,sF3),product(X0,sF0)) = product(product(sF0,product(sF3,X0)),sF0),
    inference(forward_demodulation,[],[f119115,f8478]) ).

fof(f119470,plain,
    ! [X0] : product(difference(x0,difference(sF3,X0)),sF3) = difference(sF1,quotient(product(sF3,difference(sF3,X0)),quotient(x0,sF1))),
    inference(forward_demodulation,[],[f119343,f18405]) ).

fof(f119493,plain,
    ! [X0] : difference(x0,product(sF1,X0)) = product(x0,difference(sF1,X0)),
    inference(forward_demodulation,[],[f119320,f3]) ).

fof(f119509,plain,
    ! [X0] : quotient(quotient(product(X0,sF1),x0),sF3) = product(x0,difference(sF1,product(sF3,X0))),
    inference(backward_demodulation,[],[f10181,f119301]) ).

fof(f119513,plain,
    ! [X0] : product(difference(sF3,one),difference(sF1,product(X0,x0))) = difference(x0,product(product(X0,sF1),sF3)),
    inference(forward_demodulation,[],[f119290,f405]) ).

fof(f119522,plain,
    ! [X0] : difference(sF3,product(sF1,X0)) = product(sF1,product(sF3,X0)),
    inference(backward_demodulation,[],[f86349,f119233]) ).

fof(f119528,plain,
    ! [X0] : product(sF0,quotient(product(sF3,X0),sF0)) = product(difference(sF3,product(sF0,X0)),x0),
    inference(forward_demodulation,[],[f119185,f1203]) ).

fof(f119535,plain,
    ! [X0] : difference(x0,product(X0,sF0)) = product(product(sF0,product(sF3,X0)),sF0),
    inference(forward_demodulation,[],[f119398,f1065]) ).

fof(f119577,plain,
    ! [X0] : product(difference(x0,difference(sF3,X0)),sF3) = difference(sF1,quotient(product(sF3,difference(sF3,X0)),difference(sF3,one))),
    inference(forward_demodulation,[],[f119470,f2152]) ).

fof(f119585,plain,
    ! [X0] : difference(sF3,product(X0,sF1)) = product(product(x0,difference(sF1,X0)),sF1),
    inference(backward_demodulation,[],[f1072,f119493]) ).

fof(f119629,plain,
    ! [X0] : product(sF3,product(x0,difference(sF1,X0))) = product(sF1,difference(x0,difference(sF3,X0))),
    inference(backward_demodulation,[],[f83460,f119493]) ).

fof(f119699,plain,
    ! [X0] : product(sF0,product(product(sF1,X0),sF1)) = product(x0,difference(sF1,product(X0,sF1))),
    inference(backward_demodulation,[],[f27059,f119493]) ).

fof(f119769,plain,
    ! [X0] : difference(sF0,product(X0,sF1)) = product(product(sF1,product(sF3,X0)),sF1),
    inference(backward_demodulation,[],[f134,f119522]) ).

fof(f119799,plain,
    ! [X0] : product(product(X0,sF1),sF3) = product(sF0,product(product(sF1,product(sF3,X0)),x0)),
    inference(backward_demodulation,[],[f33939,f119522]) ).

fof(f119800,plain,
    ! [X0] : difference(sF1,product(x0,product(X0,sF1))) = product(difference(sF1,product(sF1,product(sF3,X0))),sF1),
    inference(backward_demodulation,[],[f33966,f119522]) ).

fof(f119833,plain,
    ! [X0] : product(x0,difference(sF1,product(sF3,X0))) = product(sF1,product(sF3,difference(x0,X0))),
    inference(backward_demodulation,[],[f119231,f119522]) ).

fof(f119846,plain,
    ! [X0] : quotient(product(x0,X0),sF3) = product(sF1,product(sF3,quotient(X0,sF3))),
    inference(backward_demodulation,[],[f53214,f119522]) ).

fof(f119859,plain,
    ! [X0] : product(x0,difference(sF1,product(sF3,quotient(X0,sF0)))) = product(sF0,quotient(product(sF3,product(x0,X0)),sF0)),
    inference(backward_demodulation,[],[f69301,f119528]) ).

fof(f119879,plain,
    ! [X0] : difference(x0,product(quotient(X0,sF0),sF0)) = difference(sF1,difference(sF1,product(x0,X0))),
    inference(backward_demodulation,[],[f64313,f119535]) ).

fof(f119912,plain,
    ! [X0] : difference(sF1,product(sF3,product(difference(sF3,X0),sF3))) = product(difference(x0,difference(sF3,X0)),sF3),
    inference(forward_demodulation,[],[f119577,f29354]) ).

fof(f119972,plain,
    ! [X0] : difference(sF3,product(product(sF3,X0),sF1)) = difference(sF0,difference(sF1,product(sF3,quotient(X0,sF0)))),
    inference(backward_demodulation,[],[f82354,f119585]) ).

fof(f120020,plain,
    ! [X0] : quotient(quotient(product(X0,sF1),x0),sF3) = product(sF1,product(sF3,difference(x0,X0))),
    inference(backward_demodulation,[],[f119509,f119833]) ).

fof(f120060,plain,
    ! [X0] : difference(sF1,product(x0,product(X0,sF1))) = product(difference(sF1,sF1),product(product(sF3,X0),sF1)),
    inference(forward_demodulation,[],[f119800,f222]) ).

fof(f120067,plain,
    ! [X0] : product(sF0,quotient(product(sF3,product(x0,X0)),sF0)) = product(sF1,product(sF3,difference(x0,quotient(X0,sF0)))),
    inference(forward_demodulation,[],[f119859,f119833]) ).

fof(f120073,plain,
    ! [X0] : difference(x0,X0) = difference(sF1,difference(sF1,product(x0,X0))),
    inference(forward_demodulation,[],[f119879,f6]) ).

fof(f120090,plain,
    ! [X0] : difference(sF1,quotient(X0,quotient(one,sF3))) = product(difference(x0,difference(sF3,X0)),sF3),
    inference(forward_demodulation,[],[f119912,f628]) ).

fof(f120114,plain,
    ! [X0] : quotient(product(X0,x0),sF3) = difference(sF0,difference(sF1,product(sF3,quotient(X0,sF0)))),
    inference(forward_demodulation,[],[f119972,f1068]) ).

fof(f120140,plain,
    ! [X0] : difference(sF1,product(x0,product(X0,sF1))) = product(one,product(product(sF3,X0),sF1)),
    inference(forward_demodulation,[],[f120060,f50]) ).

fof(f120155,plain,
    ! [X0] : product(sF0,quotient(product(sF3,product(x0,X0)),sF0)) = product(sF1,product(sF3,product(sF0,product(X0,sF1)))),
    inference(forward_demodulation,[],[f120067,f26163]) ).

fof(f120165,plain,
    ! [X0] : difference(sF1,quotient(X0,difference(sF3,one))) = product(difference(x0,difference(sF3,X0)),sF3),
    inference(forward_demodulation,[],[f120090,f2930]) ).

fof(f120185,plain,
    ! [X0] : product(product(sF3,X0),sF1) = difference(sF1,product(x0,product(X0,sF1))),
    inference(forward_demodulation,[],[f120140,f2]) ).

fof(f120227,plain,
    ! [X0] : difference(x0,product(difference(sF0,X0),sF3)) = product(x0,difference(sF1,product(product(X0,sF1),sF0))),
    inference(superposition,[],[f119493,f53483]) ).

fof(f120273,plain,
    ! [X0] : difference(product(x0,difference(sF1,X0)),sF3) = product(difference(product(sF1,X0),one),x0),
    inference(superposition,[],[f752,f119493]) ).

fof(f120290,plain,
    ! [X0] : product(sF1,X0) = product(x0,product(x0,difference(sF1,X0))),
    inference(superposition,[],[f3,f119493]) ).

fof(f120312,plain,
    ! [X0] : product(product(sF1,X0),quotient(one,x0)) = product(x0,quotient(product(x0,difference(sF1,X0)),x0)),
    inference(superposition,[],[f57459,f119493]) ).

fof(f120315,plain,
    ! [X0] : product(x0,difference(sF3,quotient(X0,x0))) = product(product(sF1,X0),quotient(one,x0)),
    inference(forward_demodulation,[],[f120312,f69331]) ).

fof(f120340,plain,
    ! [X0] : quotient(product(X0,sF1),x0) = product(difference(product(sF1,quotient(sF3,X0)),one),x0),
    inference(backward_demodulation,[],[f73801,f120273]) ).

fof(f120379,plain,
    ! [X0] : difference(x0,product(difference(sF0,X0),sF3)) = product(x0,product(product(sF0,product(X0,sF1)),sF0)),
    inference(forward_demodulation,[],[f120227,f758]) ).

fof(f120383,plain,
    ! [X0] : product(product(sF1,X0),product(sF0,sF3)) = product(x0,difference(sF3,quotient(X0,x0))),
    inference(forward_demodulation,[],[f120315,f1262]) ).

fof(f120398,plain,
    ! [X0] : quotient(product(X0,sF1),x0) = product(quotient(X0,sF1),x0),
    inference(forward_demodulation,[],[f120340,f6283]) ).

fof(f120433,plain,
    ! [X0] : difference(difference(sF3,one),X0) = product(x0,difference(sF3,quotient(product(sF0,product(X0,x0)),x0))),
    inference(backward_demodulation,[],[f28382,f120383]) ).

fof(f120466,plain,
    ! [X0] : difference(x0,product(product(x0,X0),sF3)) = product(quotient(X0,sF1),x0),
    inference(backward_demodulation,[],[f403,f120398]) ).

fof(f120467,plain,
    ! [X0] : product(product(x0,X0),sF3) = product(x0,product(quotient(X0,sF1),x0)),
    inference(backward_demodulation,[],[f436,f120398]) ).

fof(f120503,plain,
    ! [X0] : quotient(product(quotient(X0,sF1),x0),sF3) = product(sF1,product(sF3,difference(x0,X0))),
    inference(backward_demodulation,[],[f120020,f120398]) ).

fof(f120561,plain,
    ! [X0] : difference(difference(sF3,one),X0) = product(x0,difference(sF3,difference(x0,product(product(x0,sF0),X0)))),
    inference(forward_demodulation,[],[f120433,f7]) ).

fof(f120597,plain,
    ! [X0] : difference(difference(sF3,one),X0) = product(x0,difference(sF3,difference(x0,product(one,X0)))),
    inference(forward_demodulation,[],[f120561,f32]) ).

fof(f120621,plain,
    ! [X0] : difference(difference(sF3,one),X0) = product(x0,difference(sF3,difference(x0,X0))),
    inference(forward_demodulation,[],[f120597,f2]) ).

fof(f120733,plain,
    ! [X0] : difference(sF1,difference(sF1,X0)) = difference(x0,difference(x0,X0)),
    inference(superposition,[],[f120073,f3]) ).

fof(f120754,plain,
    ! [X0] : difference(sF1,product(x0,X0)) = product(sF1,difference(x0,X0)),
    inference(superposition,[],[f3,f120073]) ).

fof(f120758,plain,
    ! [X0,X1] : difference(X1,product(difference(x0,X0),sF1)) = product(difference(product(sF1,X1),difference(sF1,product(x0,X0))),sF1),
    inference(superposition,[],[f136,f120073]) ).

fof(f120788,plain,
    ! [X0,X1] : difference(X1,product(difference(x0,X0),sF1)) = difference(X1,difference(sF1,product(sF3,quotient(X0,sF0)))),
    inference(backward_demodulation,[],[f64315,f120758]) ).

fof(f120853,plain,
    ! [X0] : product(product(sF3,X0),sF1) = product(sF1,difference(x0,product(X0,sF1))),
    inference(backward_demodulation,[],[f120185,f120754]) ).

fof(f120967,plain,
    ! [X0] : quotient(product(X0,x0),sF3) = difference(sF0,product(difference(x0,X0),sF1)),
    inference(backward_demodulation,[],[f120114,f120788]) ).

fof(f120982,plain,
    ! [X0] : product(sF3,product(sF0,product(X0,sF1))) = product(product(sF3,difference(x0,X0)),sF1),
    inference(backward_demodulation,[],[f83915,f120853]) ).

fof(f121060,plain,
    ! [X0] : quotient(product(X0,x0),sF3) = product(product(X0,sF3),x0),
    inference(forward_demodulation,[],[f120967,f16089]) ).

fof(f121133,plain,
    ! [X0] : product(product(quotient(X0,sF1),sF3),x0) = product(sF1,product(sF3,difference(x0,X0))),
    inference(backward_demodulation,[],[f120503,f121060]) ).

fof(f121312,plain,
    ! [X0] : difference(x0,product(sF0,product(X0,sF1))) = difference(sF1,difference(sF1,quotient(X0,sF0))),
    inference(superposition,[],[f120733,f26163]) ).

fof(f121412,plain,
    ! [X0] : difference(x0,product(sF0,product(X0,sF1))) = difference(sF1,product(difference(sF1,X0),sF1)),
    inference(forward_demodulation,[],[f121312,f6757]) ).

fof(f121468,plain,
    ! [X0] : difference(x0,product(sF0,product(X0,sF1))) = product(difference(product(sF1,sF1),X0),sF1),
    inference(forward_demodulation,[],[f121412,f136]) ).

fof(f121507,plain,
    ! [X0] : product(sF0,difference(sF1,product(X0,sF1))) = product(difference(product(sF1,sF1),X0),sF1),
    inference(forward_demodulation,[],[f121468,f3723]) ).

fof(f121629,plain,
    ! [X0] : product(difference(sF1,x0),product(X0,sF1)) = product(product(sF1,difference(x0,X0)),sF1),
    inference(superposition,[],[f222,f120754]) ).

fof(f121636,plain,
    ! [X0] : product(x0,X0) = product(sF1,product(sF1,difference(x0,X0))),
    inference(superposition,[],[f3,f120754]) ).

fof(f121647,plain,
    ! [X0] : quotient(product(x0,X0),quotient(one,sF1)) = product(sF1,product(product(sF1,difference(x0,X0)),sF1)),
    inference(superposition,[],[f628,f120754]) ).

fof(f121667,plain,
    ! [X0] : quotient(product(x0,X0),sF0) = product(sF1,product(product(sF1,difference(x0,X0)),sF1)),
    inference(forward_demodulation,[],[f121647,f106]) ).

fof(f121671,plain,
    ! [X0] : product(x0,product(product(sF0,sF3),X0)) = product(sF0,product(x0,X0)),
    inference(backward_demodulation,[],[f28326,f121636]) ).

fof(f121679,plain,
    ! [X0] : product(sF3,product(X0,sF1)) = product(product(sF1,difference(x0,X0)),sF1),
    inference(forward_demodulation,[],[f121629,f1066]) ).

fof(f121758,plain,
    ! [X0] : product(x0,product(difference(x0,X0),sF1)) = product(difference(sF3,product(sF0,product(x0,X0))),x0),
    inference(backward_demodulation,[],[f31238,f121671]) ).

fof(f121763,plain,
    ! [X0] : quotient(product(x0,X0),sF0) = product(sF1,product(sF3,product(X0,sF1))),
    inference(backward_demodulation,[],[f121667,f121679]) ).

fof(f121812,plain,
    ! [X0] : product(x0,product(difference(x0,X0),sF1)) = product(sF0,quotient(product(sF3,product(x0,X0)),sF0)),
    inference(forward_demodulation,[],[f121758,f119528]) ).

fof(f121853,plain,
    ! [X0] : product(x0,product(difference(x0,X0),sF1)) = product(sF1,product(sF3,product(sF0,product(X0,sF1)))),
    inference(backward_demodulation,[],[f120155,f121812]) ).

fof(f121926,plain,
    ! [X0] : product(sF1,product(sF1,X0)) = product(x0,product(x0,X0)),
    inference(superposition,[],[f120290,f4]) ).

fof(f122053,plain,
    ! [X0] : product(sF0,product(product(difference(sF0,X0),sF1),sF0)) = difference(product(sF1,sF1),product(sF1,product(sF1,X0))),
    inference(backward_demodulation,[],[f27771,f121926]) ).

fof(f122163,plain,
    ! [X0] : product(sF0,product(product(difference(sF0,X0),sF1),sF0)) = product(product(sF0,product(product(sF1,X0),sF1)),sF0),
    inference(forward_demodulation,[],[f122053,f4391]) ).

fof(f122248,plain,
    ! [X0] : product(sF0,product(difference(sF0,X0),sF1)) = product(sF0,product(product(difference(sF0,product(X0,sF1)),sF1),sF0)),
    inference(backward_demodulation,[],[f53342,f122163]) ).

fof(f123062,plain,
    ! [X0] : product(sF3,quotient(product(product(x0,X0),sF3),sF3)) = product(sF1,quotient(product(quotient(X0,sF1),x0),sF3)),
    inference(superposition,[],[f95279,f120466]) ).

fof(f123111,plain,
    ! [X0] : product(sF3,quotient(product(product(x0,X0),sF3),sF3)) = product(sF1,product(product(quotient(X0,sF1),sF3),x0)),
    inference(forward_demodulation,[],[f123062,f121060]) ).

fof(f123175,plain,
    ! [X0] : product(sF3,quotient(product(product(x0,X0),sF3),sF3)) = product(sF1,product(sF1,product(sF3,difference(x0,X0)))),
    inference(forward_demodulation,[],[f123111,f121133]) ).

fof(f123230,plain,
    ! [X0] : product(sF3,product(x0,X0)) = product(sF1,product(sF1,product(sF3,difference(x0,X0)))),
    inference(forward_demodulation,[],[f123175,f5]) ).

fof(f123394,plain,
    ! [X0] : product(quotient(one,sF3),difference(sF1,X0)) = product(sF3,product(difference(sF3,one),difference(sF1,product(sF3,X0)))),
    inference(superposition,[],[f75578,f119126]) ).

fof(f123395,plain,
    ! [X0] : product(sF3,product(difference(sF3,one),difference(sF1,product(sF3,X0)))) = product(difference(sF3,one),difference(sF1,X0)),
    inference(forward_demodulation,[],[f123394,f2930]) ).

fof(f123989,plain,
    ! [X0] : difference(sF3,difference(sF0,X0)) = product(sF1,product(sF3,product(product(X0,sF0),sF1))),
    inference(superposition,[],[f119522,f26461]) ).

fof(f124027,plain,
    ! [X0] : product(difference(product(sF1,X0),one),sF3) = difference(product(sF1,product(sF3,X0)),one),
    inference(superposition,[],[f10385,f119522]) ).

fof(f124078,plain,
    ! [X0] : quotient(quotient(X0,sF3),sF1) = product(difference(product(sF1,quotient(sF3,X0)),one),sF3),
    inference(backward_demodulation,[],[f15443,f124027]) ).

fof(f124113,plain,
    ! [X0] : difference(sF3,difference(sF0,X0)) = quotient(product(x0,product(X0,sF0)),sF0),
    inference(forward_demodulation,[],[f123989,f121763]) ).

fof(f124131,plain,
    ! [X0] : quotient(quotient(X0,sF3),sF1) = product(quotient(X0,sF1),sF3),
    inference(forward_demodulation,[],[f124078,f6283]) ).

fof(f124157,plain,
    ! [X0] : difference(sF0,product(product(sF0,x0),X0)) = difference(sF3,difference(sF0,X0)),
    inference(forward_demodulation,[],[f124113,f7]) ).

fof(f124165,plain,
    ! [X0] : product(sF3,product(x0,quotient(X0,x0))) = product(sF1,product(quotient(X0,sF1),sF3)),
    inference(backward_demodulation,[],[f19687,f124131]) ).

fof(f124190,plain,
    ! [X0] : difference(sF0,product(sF3,X0)) = difference(sF3,difference(sF0,X0)),
    inference(forward_demodulation,[],[f124157,f25]) ).

fof(f124660,plain,
    ! [X0] : difference(sF0,product(sF3,product(difference(x0,X0),sF1))) = difference(sF3,product(product(X0,sF3),x0)),
    inference(superposition,[],[f124190,f16089]) ).

fof(f124684,plain,
    ! [X0] : difference(sF3,X0) = difference(sF0,product(sF3,product(sF0,X0))),
    inference(superposition,[],[f124190,f4]) ).

fof(f124760,plain,
    ! [X0] : difference(sF0,product(difference(sF1,X0),sF1)) = difference(sF3,product(product(X0,sF3),x0)),
    inference(forward_demodulation,[],[f124660,f5887]) ).

fof(f124790,plain,
    ! [X0] : product(difference(product(sF1,sF0),X0),sF1) = difference(sF3,product(product(X0,sF3),x0)),
    inference(forward_demodulation,[],[f124760,f136]) ).

fof(f124814,plain,
    ! [X0] : product(difference(sF3,X0),sF1) = difference(sF3,product(product(X0,sF3),x0)),
    inference(forward_demodulation,[],[f124790,f108]) ).

fof(f124880,plain,
    ! [X0] : product(difference(sF3,X0),sF0) = product(sF1,product(product(sF3,product(sF0,X0)),sF0)),
    inference(superposition,[],[f939,f124684]) ).

fof(f124893,plain,
    ! [X0] : product(sF0,difference(sF3,X0)) = product(sF3,product(sF0,X0)),
    inference(superposition,[],[f3,f124684]) ).

fof(f124958,plain,
    ! [X0] : product(sF0,difference(sF3,product(X0,sF1))) = product(product(sF3,difference(x0,X0)),sF1),
    inference(backward_demodulation,[],[f120982,f124893]) ).

fof(f124960,plain,
    ! [X0] : product(x0,product(difference(x0,X0),sF1)) = product(sF1,product(sF0,difference(sF3,product(X0,sF1)))),
    inference(backward_demodulation,[],[f121853,f124893]) ).

fof(f125028,plain,
    ! [X0] : product(difference(sF3,X0),sF0) = product(x0,product(product(sF0,X0),sF0)),
    inference(forward_demodulation,[],[f124880,f6442]) ).

fof(f125121,plain,
    ! [X0] : product(difference(sF3,product(X0,sF1)),sF0) = difference(x0,product(difference(sF0,X0),sF3)),
    inference(backward_demodulation,[],[f120379,f125028]) ).

fof(f125414,plain,
    ! [X0] : product(sF3,difference(x0,X0)) = product(sF0,difference(sF3,product(product(X0,sF0),sF1))),
    inference(superposition,[],[f124893,f26238]) ).

fof(f125545,plain,
    ! [X0] : product(sF3,difference(x0,X0)) = product(sF0,product(product(difference(sF3,X0),sF0),sF1)),
    inference(forward_demodulation,[],[f125414,f69180]) ).

fof(f125573,plain,
    ! [X0] : product(sF3,difference(x0,X0)) = difference(x0,difference(sF3,X0)),
    inference(forward_demodulation,[],[f125545,f26238]) ).

fof(f125595,plain,
    ! [X0] : product(sF3,product(x0,difference(sF1,X0))) = product(sF1,product(sF3,difference(x0,X0))),
    inference(backward_demodulation,[],[f119629,f125573]) ).

fof(f125629,plain,
    ! [X0] : difference(sF1,quotient(X0,difference(sF3,one))) = product(product(sF3,difference(x0,X0)),sF3),
    inference(backward_demodulation,[],[f120165,f125573]) ).

fof(f125648,plain,
    ! [X0] : product(sF0,product(difference(sF0,product(difference(sF1,X0),sF3)),sF1)) = product(sF3,difference(x0,product(X0,sF1))),
    inference(backward_demodulation,[],[f118707,f125573]) ).

fof(f125825,plain,
    ! [X0] : product(difference(sF3,product(sF3,quotient(X0,sF3))),sF1) = difference(sF3,product(difference(difference(sF3,one),X0),x0)),
    inference(superposition,[],[f124814,f10274]) ).

fof(f125857,plain,
    ! [X0] : difference(x0,difference(sF0,product(X0,sF3))) = product(product(difference(sF3,X0),sF1),sF0),
    inference(superposition,[],[f36906,f124814]) ).

fof(f125865,plain,
    ! [X0] : product(product(X0,sF3),x0) = product(sF3,product(difference(sF3,X0),sF1)),
    inference(superposition,[],[f3,f124814]) ).

fof(f125927,plain,
    ! [X0] : product(quotient(X0,sF3),sF1) = difference(sF3,product(difference(difference(sF3,one),X0),x0)),
    inference(forward_demodulation,[],[f125825,f4]) ).

fof(f127914,plain,
    ! [X0] : product(product(difference(sF3,X0),sF0),x0) = difference(sF0,product(product(sF3,difference(x0,X0)),sF3)),
    inference(superposition,[],[f7134,f125573]) ).

fof(f127920,plain,
    ! [X0] : product(sF3,quotient(difference(sF3,X0),sF3)) = product(sF1,quotient(product(sF3,difference(x0,X0)),sF3)),
    inference(superposition,[],[f95279,f125573]) ).

fof(f127921,plain,
    ! [X0] : product(sF1,product(product(sF3,difference(x0,X0)),sF1)) = product(sF3,quotient(difference(sF3,X0),sF0)),
    inference(superposition,[],[f118924,f125573]) ).

fof(f127924,plain,
    ! [X0] : product(x0,difference(sF3,X0)) = product(sF1,product(sF1,product(sF3,difference(x0,X0)))),
    inference(superposition,[],[f121636,f125573]) ).

fof(f127960,plain,
    ! [X0] : product(sF3,product(x0,X0)) = product(x0,difference(sF3,X0)),
    inference(forward_demodulation,[],[f127924,f123230]) ).

fof(f127963,plain,
    ! [X0] : product(sF1,product(sF0,difference(sF3,product(X0,sF1)))) = product(sF3,quotient(difference(sF3,X0),sF0)),
    inference(forward_demodulation,[],[f127921,f124958]) ).

fof(f127964,plain,
    ! [X0] : product(X0,quotient(one,sF3)) = product(sF1,quotient(product(sF3,difference(x0,X0)),sF3)),
    inference(forward_demodulation,[],[f127920,f57459]) ).

fof(f128066,plain,
    ! [X0] : difference(difference(sF3,one),X0) = product(sF3,product(x0,difference(x0,X0))),
    inference(backward_demodulation,[],[f120621,f127960]) ).

fof(f128087,plain,
    ! [X0] : product(sF3,product(x0,quotient(X0,x0))) = product(product(sF1,X0),product(sF0,sF3)),
    inference(backward_demodulation,[],[f120383,f127960]) ).

fof(f128119,plain,
    ! [X0] : product(x0,product(difference(x0,X0),sF1)) = product(sF3,quotient(difference(sF3,X0),sF0)),
    inference(backward_demodulation,[],[f124960,f127963]) ).

fof(f128120,plain,
    ! [X0] : product(X0,difference(sF3,one)) = product(sF1,quotient(product(sF3,difference(x0,X0)),sF3)),
    inference(forward_demodulation,[],[f127964,f2930]) ).

fof(f128269,plain,
    ! [X0] : product(product(sF1,X0),product(sF0,sF3)) = product(sF1,product(quotient(X0,sF1),sF3)),
    inference(forward_demodulation,[],[f128087,f124165]) ).

fof(f128279,plain,
    ! [X0] : product(sF3,X0) = difference(difference(sF3,one),X0),
    inference(forward_demodulation,[],[f128066,f3]) ).

fof(f128300,plain,
    ! [X0] : difference(sF3,quotient(product(sF3,X0),sF0)) = product(sF3,quotient(difference(sF3,X0),sF0)),
    inference(backward_demodulation,[],[f31232,f128119]) ).

fof(f128441,plain,
    ! [X0] : product(quotient(X0,sF3),sF1) = difference(sF3,product(product(sF3,X0),x0)),
    inference(backward_demodulation,[],[f125927,f128279]) ).

fof(f128473,plain,
    ! [X0] : quotient(product(X0,product(sF3,sF1)),difference(sF3,one)) = product(sF3,product(product(difference(sF3,one),X0),sF1)),
    inference(backward_demodulation,[],[f3968,f128279]) ).

fof(f128678,plain,
    ! [X0] : difference(product(sF3,sF1),product(sF1,product(difference(sF3,one),X0))) = quotient(product(sF3,product(product(difference(sF3,one),X0),sF1)),sF1),
    inference(backward_demodulation,[],[f37434,f128473]) ).

fof(f128679,plain,
    ! [X0] : difference(product(sF3,sF1),quotient(product(product(sF3,sF1),X0),sF0)) = product(sF3,product(product(difference(sF3,one),X0),sF1)),
    inference(backward_demodulation,[],[f23525,f128473]) ).

fof(f128776,plain,
    ! [X0] : difference(product(sF3,sF1),product(sF1,product(difference(sF3,one),X0))) = difference(sF1,product(product(sF1,sF3),product(difference(sF3,one),X0))),
    inference(forward_demodulation,[],[f128678,f7]) ).

fof(f128827,plain,
    ! [X0] : difference(sF1,product(x0,product(difference(sF3,one),X0))) = difference(product(sF3,sF1),product(sF1,product(difference(sF3,one),X0))),
    inference(forward_demodulation,[],[f128776,f1065]) ).

fof(f128849,plain,
    ! [X0] : difference(product(sF3,sF1),product(sF1,product(difference(sF3,one),X0))) = product(sF1,difference(x0,product(difference(sF3,one),X0))),
    inference(forward_demodulation,[],[f128827,f120754]) ).

fof(f128884,plain,
    ! [X0] : difference(one,product(sF3,quotient(X0,sF3))) = quotient(product(sF3,X0),sF3),
    inference(superposition,[],[f8257,f128279]) ).

fof(f128889,plain,
    ! [X0] : product(sF3,product(X0,sF3)) = product(difference(one,product(sF3,X0)),sF3),
    inference(superposition,[],[f125,f128279]) ).

fof(f128942,plain,
    ! [X0] : product(sF3,product(difference(sF3,one),X0)) = X0,
    inference(superposition,[],[f4,f128279]) ).

fof(f129008,plain,
    ! [X0] : product(product(X0,sF0),sF3) = product(sF1,quotient(difference(sF1,X0),x0)),
    inference(backward_demodulation,[],[f76292,f128942]) ).

fof(f129038,plain,
    ! [X0] : difference(sF1,product(sF3,X0)) = product(difference(sF3,one),difference(sF1,X0)),
    inference(backward_demodulation,[],[f123395,f128942]) ).

fof(f129115,plain,
    ! [X0] : product(product(sF3,X0),sF3) = product(sF3,product(X0,sF3)),
    inference(forward_demodulation,[],[f128889,f62]) ).

fof(f129120,plain,
    ! [X0] : product(sF3,quotient(X0,sF3)) = quotient(product(sF3,X0),sF3),
    inference(forward_demodulation,[],[f128884,f62]) ).

fof(f129157,plain,
    ! [X0] : difference(sF1,product(sF3,product(X0,x0))) = difference(x0,product(product(X0,sF1),sF3)),
    inference(backward_demodulation,[],[f119513,f129038]) ).

fof(f129197,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = quotient(product(product(X0,sF0),sF3),product(sF0,sF3)),
    inference(backward_demodulation,[],[f76293,f129008]) ).

fof(f129319,plain,
    ! [X0] : product(product(difference(sF3,X0),sF0),x0) = difference(sF0,product(sF3,product(difference(x0,X0),sF3))),
    inference(backward_demodulation,[],[f127914,f129115]) ).

fof(f129320,plain,
    ! [X0] : difference(sF1,quotient(X0,difference(sF3,one))) = product(sF3,product(difference(x0,X0),sF3)),
    inference(backward_demodulation,[],[f125629,f129115]) ).

fof(f129331,plain,
    ! [X0] : product(X0,difference(sF3,one)) = product(sF1,product(sF3,quotient(difference(x0,X0),sF3))),
    inference(backward_demodulation,[],[f128120,f129120]) ).

fof(f129393,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = difference(sF3,quotient(product(sF3,product(X0,sF0)),sF0)),
    inference(forward_demodulation,[],[f129197,f22837]) ).

fof(f129490,plain,
    ! [X0] : product(X0,difference(sF3,one)) = quotient(product(x0,difference(x0,X0)),sF3),
    inference(forward_demodulation,[],[f129331,f119846]) ).

fof(f129517,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = product(sF3,quotient(difference(sF3,product(X0,sF0)),sF0)),
    inference(forward_demodulation,[],[f129393,f128300]) ).

fof(f129564,plain,
    ! [X0] : quotient(X0,sF3) = product(X0,difference(sF3,one)),
    inference(forward_demodulation,[],[f129490,f3]) ).

fof(f129583,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = product(sF3,difference(product(sF0,sF3),product(sF0,X0))),
    inference(forward_demodulation,[],[f129517,f42]) ).

fof(f129824,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = product(sF3,product(x0,difference(sF1,X0))),
    inference(forward_demodulation,[],[f129583,f55042]) ).

fof(f129977,plain,
    ! [X0] : product(sF1,difference(x0,product(difference(sF3,one),X0))) = product(sF1,product(sF3,difference(x0,X0))),
    inference(forward_demodulation,[],[f129824,f125595]) ).

fof(f130045,plain,
    ! [X0] : difference(product(sF3,sF1),product(sF1,product(difference(sF3,one),X0))) = product(sF1,product(sF3,difference(x0,X0))),
    inference(backward_demodulation,[],[f128849,f129977]) ).

fof(f130216,plain,
    ! [X0] : difference(difference(difference(sF3,one),one),X0) = quotient(product(difference(sF3,one),quotient(X0,difference(sF3,one))),sF3),
    inference(superposition,[],[f10274,f129564]) ).

fof(f130420,plain,
    ! [X0] : difference(difference(difference(sF3,one),one),X0) = product(difference(sF3,one),quotient(X0,product(sF3,difference(sF3,one)))),
    inference(forward_demodulation,[],[f130216,f2519]) ).

fof(f130610,plain,
    ! [X0] : difference(difference(difference(sF3,one),one),X0) = product(difference(sF3,one),quotient(X0,one)),
    inference(forward_demodulation,[],[f130420,f3]) ).

fof(f130758,plain,
    ! [X0] : product(difference(sF3,one),X0) = difference(difference(difference(sF3,one),one),X0),
    inference(forward_demodulation,[],[f130610,f80]) ).

fof(f130878,plain,
    ! [X0] : product(difference(sF3,one),X0) = difference(product(sF3,one),X0),
    inference(forward_demodulation,[],[f130758,f128279]) ).

fof(f130968,plain,
    ! [X0] : difference(sF3,X0) = product(difference(sF3,one),X0),
    inference(forward_demodulation,[],[f130878,f1]) ).

fof(f131090,plain,
    ! [X0] : difference(product(sF3,sF1),quotient(product(product(sF3,sF1),X0),sF0)) = product(sF3,product(difference(sF3,X0),sF1)),
    inference(backward_demodulation,[],[f128679,f130968]) ).

fof(f131107,plain,
    ! [X0] : product(sF1,product(sF3,difference(x0,X0))) = difference(product(sF3,sF1),product(sF1,difference(sF3,X0))),
    inference(backward_demodulation,[],[f130045,f130968]) ).

fof(f131125,plain,
    ! [X0] : product(sF0,product(product(sF1,X0),x0)) = difference(sF3,product(X0,x0)),
    inference(backward_demodulation,[],[f32439,f130968]) ).

fof(f131192,plain,
    ! [X0] : quotient(product(product(sF3,sF1),X0),sF0) = difference(sF0,difference(sF3,quotient(X0,sF0))),
    inference(backward_demodulation,[],[f56945,f130968]) ).

fof(f131197,plain,
    ! [X0] : quotient(X0,difference(sF3,one)) = difference(difference(sF3,quotient(product(sF3,sF0),X0)),product(sF0,sF3)),
    inference(backward_demodulation,[],[f30755,f130968]) ).

fof(f131280,plain,
    ! [X0] : quotient(X0,difference(sF3,one)) = product(difference(quotient(product(sF3,sF0),X0),product(sF3,sF0)),sF3),
    inference(forward_demodulation,[],[f131197,f125]) ).

fof(f131283,plain,
    ! [X0] : quotient(product(product(sF3,sF1),X0),sF0) = product(sF3,difference(sF0,quotient(X0,sF0))),
    inference(forward_demodulation,[],[f131192,f118909]) ).

fof(f131316,plain,
    ! [X0] : product(product(X0,sF1),sF3) = difference(sF3,product(product(sF3,X0),x0)),
    inference(backward_demodulation,[],[f119799,f131125]) ).

fof(f131352,plain,
    ! [X0] : product(product(X0,sF3),x0) = difference(product(sF3,sF1),quotient(product(product(sF3,sF1),X0),sF0)),
    inference(forward_demodulation,[],[f131090,f125865]) ).

fof(f131433,plain,
    ! [X0] : product(X0,sF3) = quotient(X0,difference(sF3,one)),
    inference(forward_demodulation,[],[f131280,f122]) ).

fof(f131434,plain,
    ! [X0] : quotient(product(product(sF3,sF1),X0),sF0) = product(sF3,product(sF1,product(X0,sF1))),
    inference(forward_demodulation,[],[f131283,f26979]) ).

fof(f131455,plain,
    ! [X0] : product(quotient(X0,sF3),sF1) = product(product(X0,sF1),sF3),
    inference(backward_demodulation,[],[f128441,f131316]) ).

fof(f131541,plain,
    ! [X0] : difference(sF1,product(X0,sF3)) = product(sF3,product(difference(x0,X0),sF3)),
    inference(backward_demodulation,[],[f129320,f131433]) ).

fof(f131575,plain,
    ! [X0] : quotient(product(product(sF3,sF1),X0),sF0) = product(sF1,difference(sF3,product(X0,sF1))),
    inference(forward_demodulation,[],[f131434,f118574]) ).

fof(f131687,plain,
    ! [X0] : product(product(difference(sF3,X0),sF0),x0) = difference(sF0,difference(sF1,product(X0,sF3))),
    inference(backward_demodulation,[],[f129319,f131541]) ).

fof(f131733,plain,
    ! [X0] : product(product(X0,sF3),x0) = difference(product(sF3,sF1),product(sF1,difference(sF3,product(X0,sF1)))),
    inference(backward_demodulation,[],[f131352,f131575]) ).

fof(f131826,plain,
    ! [X0] : product(product(X0,sF3),x0) = product(sF1,product(sF3,difference(x0,product(X0,sF1)))),
    inference(forward_demodulation,[],[f131733,f131107]) ).

fof(f132096,plain,
    ! [X0] : product(product(product(x0,difference(sF3,one)),X0),x0) = difference(sF0,difference(sF3,product(X0,x0))),
    inference(superposition,[],[f851,f130968]) ).

fof(f132224,plain,
    ! [X0] : product(product(product(x0,difference(sF3,one)),X0),x0) = product(sF3,difference(sF0,product(X0,x0))),
    inference(forward_demodulation,[],[f132096,f118909]) ).

fof(f132411,plain,
    ! [X0] : product(product(product(x0,difference(sF3,one)),X0),x0) = product(sF3,product(product(x0,X0),x0)),
    inference(forward_demodulation,[],[f132224,f759]) ).

fof(f132578,plain,
    ! [X0] : product(sF3,product(product(x0,X0),x0)) = product(product(product(sF3,product(x0,one)),X0),x0),
    inference(forward_demodulation,[],[f132411,f127960]) ).

fof(f132764,plain,
    ! [X0] : product(sF3,product(product(x0,X0),x0)) = product(product(product(sF3,x0),X0),x0),
    inference(forward_demodulation,[],[f132578,f1]) ).

fof(f132889,plain,
    ! [X0] : product(product(sF1,X0),x0) = product(sF3,product(product(x0,X0),x0)),
    inference(forward_demodulation,[],[f132764,f400]) ).

fof(f133205,plain,
    ! [X0] : product(x0,product(product(product(x0,X0),x0),sF0)) = product(sF1,product(product(product(sF1,X0),x0),sF0)),
    inference(superposition,[],[f6442,f132889]) ).

fof(f133273,plain,
    ! [X0] : product(sF1,product(product(product(sF1,X0),sF0),sF1)) = product(x0,product(product(product(x0,X0),x0),sF0)),
    inference(forward_demodulation,[],[f133205,f26420]) ).

fof(f133323,plain,
    ! [X0] : product(sF1,product(product(product(sF1,X0),sF0),sF1)) = product(x0,product(product(product(x0,X0),sF0),sF1)),
    inference(forward_demodulation,[],[f133273,f26420]) ).

fof(f133367,plain,
    ! [X0] : difference(product(sF0,sF3),product(x0,X0)) = product(sF1,product(product(product(sF1,X0),sF0),sF1)),
    inference(forward_demodulation,[],[f133323,f69226]) ).

fof(f133393,plain,
    ! [X0] : difference(sF0,product(sF1,X0)) = difference(product(sF0,sF3),product(x0,X0)),
    inference(forward_demodulation,[],[f133367,f26461]) ).

fof(f133414,plain,
    ! [X0] : product(x0,difference(sF0,difference(sF1,X0))) = difference(sF0,product(sF1,difference(sF1,X0))),
    inference(backward_demodulation,[],[f78805,f133393]) ).

fof(f133433,plain,
    ! [X0] : difference(sF0,X0) = product(x0,difference(sF0,difference(sF1,X0))),
    inference(forward_demodulation,[],[f133414,f3]) ).

fof(f133507,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = product(x0,difference(sF0,product(difference(sF1,X0),sF1))),
    inference(superposition,[],[f133433,f6757]) ).

fof(f133543,plain,
    ! [X0] : difference(x0,product(difference(sF0,X0),sF3)) = product(quotient(difference(sF0,difference(sF1,X0)),sF1),x0),
    inference(superposition,[],[f120466,f133433]) ).

fof(f133547,plain,
    ! [X0] : difference(x0,difference(sF0,X0)) = difference(sF0,difference(sF1,X0)),
    inference(superposition,[],[f4,f133433]) ).

fof(f133658,plain,
    ! [X0] : product(product(difference(sF3,X0),sF1),sF0) = difference(sF0,difference(sF1,product(X0,sF3))),
    inference(backward_demodulation,[],[f125857,f133547]) ).

fof(f133692,plain,
    ! [X0] : difference(x0,product(difference(sF0,X0),sF3)) = product(difference(product(sF1,sF0),product(X0,sF0)),x0),
    inference(forward_demodulation,[],[f133543,f8478]) ).

fof(f133768,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = product(x0,product(difference(product(sF1,sF0),X0),sF1)),
    inference(forward_demodulation,[],[f133507,f136]) ).

fof(f133801,plain,
    ! [X0] : product(product(difference(sF3,X0),sF0),x0) = product(product(difference(sF3,X0),sF1),sF0),
    inference(forward_demodulation,[],[f133658,f131687]) ).

fof(f133808,plain,
    ! [X0] : product(difference(sF3,product(X0,sF0)),x0) = difference(x0,product(difference(sF0,X0),sF3)),
    inference(forward_demodulation,[],[f133692,f108]) ).

fof(f133855,plain,
    ! [X0] : difference(sF0,quotient(X0,sF0)) = product(x0,product(difference(sF3,X0),sF1)),
    inference(forward_demodulation,[],[f133768,f108]) ).

fof(f133900,plain,
    ! [X0] : product(difference(sF3,product(X0,sF0)),x0) = product(difference(sF3,product(X0,sF1)),sF0),
    inference(backward_demodulation,[],[f125121,f133808]) ).

fof(f133922,plain,
    ! [X0] : product(sF1,product(X0,sF1)) = product(x0,product(difference(sF3,X0),sF1)),
    inference(forward_demodulation,[],[f133855,f26979]) ).

fof(f136376,plain,
    ! [X0] : product(x0,quotient(product(difference(sF3,X0),sF1),x0)) = product(product(sF1,product(X0,sF1)),product(sF0,sF3)),
    inference(superposition,[],[f1267,f133922]) ).

fof(f136396,plain,
    ! [X0] : product(difference(sF3,X0),sF1) = difference(x0,product(sF1,product(X0,sF1))),
    inference(superposition,[],[f4,f133922]) ).

fof(f136460,plain,
    ! [X0] : product(difference(sF3,X0),sF1) = product(x0,difference(sF1,product(X0,sF1))),
    inference(forward_demodulation,[],[f136396,f119493]) ).

fof(f136478,plain,
    ! [X0] : product(x0,quotient(product(difference(sF3,X0),sF1),x0)) = product(sF1,product(quotient(product(X0,sF1),sF1),sF3)),
    inference(forward_demodulation,[],[f136376,f128269]) ).

fof(f136529,plain,
    ! [X0] : product(difference(sF3,X0),sF1) = product(sF0,product(product(sF1,X0),sF1)),
    inference(backward_demodulation,[],[f119699,f136460]) ).

fof(f136538,plain,
    ! [X0] : product(sF1,product(X0,sF3)) = product(x0,quotient(product(difference(sF3,X0),sF1),x0)),
    inference(forward_demodulation,[],[f136478,f5]) ).

fof(f136573,plain,
    ! [X0] : product(sF0,product(product(difference(sF0,X0),sF1),sF0)) = product(product(difference(sF3,X0),sF1),sF0),
    inference(backward_demodulation,[],[f122163,f136529]) ).

fof(f136585,plain,
    ! [X0] : product(sF1,product(X0,sF3)) = product(x0,product(quotient(difference(sF3,X0),sF1),x0)),
    inference(forward_demodulation,[],[f136538,f120398]) ).

fof(f136609,plain,
    ! [X0] : product(product(difference(sF3,X0),sF0),x0) = product(sF0,product(product(difference(sF0,X0),sF1),sF0)),
    inference(forward_demodulation,[],[f136573,f133801]) ).

fof(f136610,plain,
    ! [X0] : product(sF1,product(X0,sF3)) = product(product(x0,difference(sF3,X0)),sF3),
    inference(forward_demodulation,[],[f136585,f120467]) ).

fof(f136623,plain,
    ! [X0] : product(sF0,product(difference(sF0,X0),sF1)) = product(product(difference(sF3,product(X0,sF1)),sF0),x0),
    inference(backward_demodulation,[],[f122248,f136609]) ).

fof(f136624,plain,
    ! [X0] : product(sF1,product(X0,sF3)) = product(product(sF3,product(x0,X0)),sF3),
    inference(forward_demodulation,[],[f136610,f127960]) ).

fof(f136631,plain,
    ! [X0] : product(sF0,product(difference(sF0,X0),sF1)) = product(product(difference(sF3,product(X0,sF0)),x0),x0),
    inference(forward_demodulation,[],[f136623,f133900]) ).

fof(f136632,plain,
    ! [X0] : product(sF1,product(X0,sF3)) = product(sF3,product(product(x0,X0),sF3)),
    inference(forward_demodulation,[],[f136624,f129115]) ).

fof(f136972,plain,
    ! [X0] : difference(x0,product(product(product(x0,X0),sF3),x0)) = difference(sF1,product(product(sF1,product(X0,sF3)),x0)),
    inference(superposition,[],[f32661,f136632]) ).

fof(f137047,plain,
    ! [X0] : difference(x0,difference(sF0,product(X0,sF1))) = difference(sF1,product(product(sF1,product(X0,sF3)),x0)),
    inference(forward_demodulation,[],[f136972,f16185]) ).

fof(f137118,plain,
    ! [X0] : difference(sF0,difference(sF1,product(X0,sF1))) = difference(sF1,product(product(sF1,product(X0,sF3)),x0)),
    inference(forward_demodulation,[],[f137047,f133547]) ).

fof(f137676,plain,
    ! [X0] : difference(x0,X0) = difference(sF0,difference(sF1,product(sF0,X0))),
    inference(superposition,[],[f133547,f4]) ).

fof(f137918,plain,
    ! [X0] : difference(x0,product(difference(sF3,X0),sF1)) = difference(sF0,difference(sF1,product(difference(sF1,X0),sF1))),
    inference(superposition,[],[f137676,f5889]) ).

fof(f138114,plain,
    ! [X0] : difference(x0,product(difference(sF3,X0),sF1)) = difference(sF0,product(difference(product(sF1,sF1),X0),sF1)),
    inference(forward_demodulation,[],[f137918,f136]) ).

fof(f138196,plain,
    ! [X0] : difference(x0,product(difference(sF3,X0),sF1)) = difference(sF0,product(sF0,difference(sF1,product(X0,sF1)))),
    inference(forward_demodulation,[],[f138114,f121507]) ).

fof(f138233,plain,
    ! [X0] : difference(sF1,product(X0,sF1)) = difference(x0,product(difference(sF3,X0),sF1)),
    inference(forward_demodulation,[],[f138196,f4]) ).

fof(f138319,plain,
    ! [X0] : difference(sF1,product(product(sF1,X0),sF1)) = difference(x0,product(product(sF1,product(sF3,X0)),sF1)),
    inference(superposition,[],[f138233,f119522]) ).

fof(f138337,plain,
    ! [X0] : difference(x0,product(X0,sF1)) = difference(sF1,product(product(sF3,X0),sF1)),
    inference(superposition,[],[f138233,f4]) ).

fof(f138445,plain,
    ! [X0] : difference(x0,difference(sF0,product(X0,sF1))) = difference(sF1,product(product(sF1,X0),sF1)),
    inference(forward_demodulation,[],[f138319,f119769]) ).

fof(f138481,plain,
    ! [X0] : difference(sF0,difference(sF1,product(X0,sF1))) = difference(sF1,product(product(sF1,X0),sF1)),
    inference(forward_demodulation,[],[f138445,f133547]) ).

fof(f138670,plain,
    ! [X0] : difference(x0,product(quotient(product(x0,X0),sF3),sF1)) = difference(sF1,product(product(sF1,quotient(X0,sF3)),sF1)),
    inference(superposition,[],[f138337,f427]) ).

fof(f138769,plain,
    ! [X0] : difference(x0,product(quotient(product(x0,X0),sF3),sF1)) = difference(sF0,difference(sF1,product(quotient(X0,sF3),sF1))),
    inference(forward_demodulation,[],[f138670,f138481]) ).

fof(f138814,plain,
    ! [X0] : difference(x0,product(quotient(product(x0,X0),sF3),sF1)) = difference(sF0,difference(sF1,product(product(X0,sF1),sF3))),
    inference(forward_demodulation,[],[f138769,f131455]) ).

fof(f138849,plain,
    ! [X0] : product(product(difference(sF3,product(X0,sF1)),sF0),x0) = difference(x0,product(quotient(product(x0,X0),sF3),sF1)),
    inference(forward_demodulation,[],[f138814,f131687]) ).

fof(f138872,plain,
    ! [X0] : product(product(difference(sF3,product(X0,sF1)),sF0),x0) = difference(x0,product(product(product(x0,X0),sF1),sF3)),
    inference(forward_demodulation,[],[f138849,f131455]) ).

fof(f138891,plain,
    ! [X0] : difference(sF1,product(sF3,product(product(x0,X0),x0))) = product(product(difference(sF3,product(X0,sF1)),sF0),x0),
    inference(forward_demodulation,[],[f138872,f129157]) ).

fof(f138900,plain,
    ! [X0] : difference(sF1,product(sF3,product(product(x0,X0),x0))) = product(product(difference(sF3,product(X0,sF0)),x0),x0),
    inference(forward_demodulation,[],[f138891,f133900]) ).

fof(f138906,plain,
    ! [X0] : product(sF0,product(difference(sF0,X0),sF1)) = difference(sF1,product(sF3,product(product(x0,X0),x0))),
    inference(forward_demodulation,[],[f138900,f136631]) ).

fof(f138909,plain,
    ! [X0] : difference(sF1,product(product(sF1,X0),x0)) = product(sF0,product(difference(sF0,X0),sF1)),
    inference(forward_demodulation,[],[f138906,f132889]) ).

fof(f138915,plain,
    ! [X0] : difference(sF0,difference(sF1,product(X0,sF1))) = product(sF0,product(difference(sF0,product(X0,sF3)),sF1)),
    inference(backward_demodulation,[],[f137118,f138909]) ).

fof(f138927,plain,
    ! [X0] : product(sF3,difference(x0,product(X0,sF1))) = difference(sF0,difference(sF1,product(difference(sF1,X0),sF1))),
    inference(backward_demodulation,[],[f125648,f138915]) ).

fof(f138935,plain,
    ! [X0] : product(sF3,difference(x0,product(X0,sF1))) = difference(sF0,product(difference(product(sF1,sF1),X0),sF1)),
    inference(forward_demodulation,[],[f138927,f136]) ).

fof(f138937,plain,
    ! [X0] : product(sF3,difference(x0,product(X0,sF1))) = difference(sF0,product(sF0,difference(sF1,product(X0,sF1)))),
    inference(forward_demodulation,[],[f138935,f121507]) ).

fof(f138941,plain,
    ! [X0] : difference(sF1,product(X0,sF1)) = product(sF3,difference(x0,product(X0,sF1))),
    inference(forward_demodulation,[],[f138937,f4]) ).

fof(f138943,plain,
    ! [X0] : product(product(X0,sF3),x0) = product(sF1,difference(sF1,product(X0,sF1))),
    inference(backward_demodulation,[],[f131826,f138941]) ).

fof(f138999,plain,
    ! [X0] : product(X0,sF1) = product(product(X0,sF3),x0),
    inference(forward_demodulation,[],[f138943,f3]) ).

fof(f139208,plain,
    product(sF2,sF1) = product(sF5,sF1),
    inference(backward_demodulation,[],[f103298,f138999]) ).

fof(f139373,plain,
    quotient(sF2,sF5) = difference(product(sF5,difference(sF2,product(sF2,sF1))),product(sF2,sF1)),
    inference(backward_demodulation,[],[f110303,f139208]) ).

fof(f140567,plain,
    quotient(sF2,sF5) = difference(product(sF5,sF1),product(sF2,sF1)),
    inference(forward_demodulation,[],[f139373,f4]) ).

fof(f141449,plain,
    difference(product(sF2,sF1),product(sF2,sF1)) = quotient(sF2,sF5),
    inference(forward_demodulation,[],[f140567,f139208]) ).

fof(f143558,plain,
    one = quotient(sF2,sF5),
    inference(forward_demodulation,[],[f141449,f50]) ).

fof(f155917,plain,
    sF5 = difference(one,sF2),
    inference(superposition,[],[f122,f143558]) ).

fof(f155945,plain,
    sF2 = sF5,
    inference(forward_demodulation,[],[f155917,f62]) ).

fof(f155969,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f155945,f30]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04  % Problem  : GRP765-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.08  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.43  % Computer : n010.cluster.edu
% 0.16/0.43  % Model    : x86_64 x86_64
% 0.16/0.43  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43  % Memory   : 8046.5625MB
% 0.16/0.43  % OS       : Linux 6.8.0-71-generic
% 0.16/0.43  % CPULimit : 300
% 0.16/0.43  % WCLimit  : 300
% 0.16/0.43  % DateTime : Sun Sep 27 10:43:17 UTC 2026
% 0.16/0.43  % CPUTime  : 
% 0.16/0.43  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.49  Running first-order theorem proving
% 0.22/0.49  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 146.66/21.47  % (774101)Detected a unit-equality problem, will run specialized UEQ schedule.
% 146.66/21.47  % (774109)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3056954635:i=136:bd=preordered:ins=2:av=off_3000 on theBenchmark for (3000ds/136Mi)
% 146.66/21.47  % (774109)Instruction limit reached! 
% 146.66/21.47  % (774109)------------------------------
% 146.66/21.47  % (774109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.66/21.47  % (774109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.66/21.47  % (774109)CaDiCaL version: 2.1.3
% 146.66/21.47  % (774109)Termination reason: Instruction limit
% 146.66/21.47  % (774109)Termination phase: Saturation
% 146.66/21.47  % (774109)Time elapsed: 0.047 s
% 146.66/21.47  % (774109)Peak memory usage: 89 MB
% 146.66/21.47  % (774109)Instructions burned: 137 (million)
% 146.66/21.47  % (774110)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3307841707:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_3000 on theBenchmark for (3000ds/181Mi)
% 146.66/21.47  % (774112)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1313042325:i=1187:sd=4:av=off:ss=axioms:sgt=32_3000 on theBenchmark for (3000ds/1187Mi)
% 146.66/21.47  % (774111)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1630401131:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_3000 on theBenchmark for (3000ds/257Mi)
% 146.66/21.47  % (774108)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=897368811:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_3000 on theBenchmark for (3000ds/130716Mi)
% 146.66/21.47  % (774107)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=1338998962:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/130792Mi)
% 146.66/21.47  % (774106)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=4124594327:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_3000 on theBenchmark for (3000ds/138329Mi)
% 146.66/21.47  % (774115)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3238391651:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 146.66/21.47  % (774110)Instruction limit reached! 
% 146.66/21.47  % (774110)------------------------------
% 146.66/21.47  % (774110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.66/21.47  % (774110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.66/21.47  % (774110)CaDiCaL version: 2.1.3
% 146.66/21.47  % (774110)Termination reason: Instruction limit
% 146.66/21.47  % (774110)Termination phase: Saturation
% 146.66/21.47  % (774110)Time elapsed: 0.178 s
% 146.66/21.47  % (774110)Peak memory usage: 89 MB
% 146.66/21.47  % (774110)Instructions burned: 181 (million)
% 146.66/21.47  % (774111)Instruction limit reached! 
% 146.66/21.47  % (774111)------------------------------
% 146.66/21.47  % (774111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.66/21.47  % (774111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.66/21.47  % (774111)CaDiCaL version: 2.1.3
% 146.66/21.47  % (774111)Termination reason: Instruction limit
% 146.66/21.47  % (774111)Termination phase: Saturation
% 146.66/21.47  % (774111)Time elapsed: 0.257 s
% 146.66/21.47  % (774111)Peak memory usage: 90 MB
% 146.66/21.47  % (774111)Instructions burned: 257 (million)
% 146.66/21.47  % (774123)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3711149405:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 146.66/21.47  % (774124)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=396634828:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 146.66/21.47  % (774124)Instruction limit reached! 
% 146.66/21.47  % (774124)------------------------------
% 146.66/21.47  % (774124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.66/21.47  % (774124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.66/21.47  % (774124)CaDiCaL version: 2.1.3
% 146.66/21.47  % (774124)Termination reason: Instruction limit
% 146.66/21.47  % (774124)Termination phase: Saturation
% 146.66/21.47  % (774124)Time elapsed: 0.197 s
% 146.66/21.47  % (774124)Peak memory usage: 90 MB
% 146.66/21.47  % (774124)Instructions burned: 215 (million)
% 203.05/29.36  % (774127)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=1041321319:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/317Mi)
% 203.05/29.36  % (774112)Instruction limit reached! 
% 203.05/29.36  % (774112)------------------------------
% 203.05/29.36  % (774112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.05/29.36  % (774112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.05/29.36  % (774112)CaDiCaL version: 2.1.3
% 203.05/29.36  % (774112)Termination reason: Instruction limit
% 203.05/29.36  % (774112)Termination phase: Saturation
% 203.05/29.36  % (774112)Time elapsed: 1.108 s
% 203.05/29.36  % (774112)Peak memory usage: 99 MB
% 203.05/29.36  % (774112)Instructions burned: 1187 (million)
% 203.05/29.36  % (774127)Instruction limit reached! 
% 203.05/29.36  % (774127)------------------------------
% 203.05/29.36  % (774127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.05/29.36  % (774127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.05/29.36  % (774127)CaDiCaL version: 2.1.3
% 203.05/29.36  % (774127)Termination reason: Instruction limit
% 203.05/29.36  % (774127)Termination phase: Saturation
% 203.05/29.36  % (774127)Time elapsed: 0.180 s
% 203.05/29.36  % (774127)Peak memory usage: 94 MB
% 203.05/29.36  % (774127)Instructions burned: 319 (million)
% 203.05/29.36  % (774131)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1534866988:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2985 on theBenchmark for (2985ds/2836Mi)
% 203.05/29.36  % (774130)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=3066773884:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/12125Mi)
% 203.05/29.36  % (774115)Instruction limit reached! 
% 203.05/29.36  % (774115)------------------------------
% 203.05/29.36  % (774115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.05/29.36  % (774115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.05/29.36  % (774115)CaDiCaL version: 2.1.3
% 203.05/29.36  % (774115)Termination reason: Instruction limit
% 203.05/29.36  % (774115)Termination phase: Saturation
% 203.05/29.36  % (774115)Time elapsed: 1.746 s
% 203.05/29.36  % (774115)Peak memory usage: 141 MB
% 203.05/29.36  % (774115)Instructions burned: 2051 (million)
% 203.05/29.36  % (774137)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2400355062:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2978 on theBenchmark for (2978ds/14534Mi)
% 203.05/29.36  % (774131)Instruction limit reached! 
% 203.05/29.36  % (774131)------------------------------
% 203.05/29.36  % (774131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.05/29.36  % (774131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.05/29.36  % (774131)CaDiCaL version: 2.1.3
% 203.05/29.36  % (774131)Termination reason: Instruction limit
% 203.05/29.36  % (774131)Termination phase: Saturation
% 203.05/29.36  % (774131)Time elapsed: 1.719 s
% 203.05/29.36  % (774131)Peak memory usage: 136 MB
% 203.05/29.36  % (774131)Instructions burned: 2837 (million)
% 203.05/29.36  % (774139)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=1335194075:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2966 on theBenchmark for (2966ds/11832Mi)
% 203.05/29.36  % (774123)Instruction limit reached! 
% 203.05/29.36  % (774123)------------------------------
% 203.05/29.36  % (774123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.05/29.36  % (774123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.05/29.36  % (774123)CaDiCaL version: 2.1.3
% 203.05/29.36  % (774123)Termination reason: Instruction limit
% 203.05/29.36  % (774123)Termination phase: Saturation
% 203.05/29.36  % (774123)Time elapsed: 4.935 s
% 203.05/29.36  % (774123)Peak memory usage: 170 MB
% 203.05/29.36  % (774123)Instructions burned: 4948 (million)
% 203.05/29.36  % (774147)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=4102098888:i=2279:fgj=on:bd=all_2943 on theBenchmark for (2943ds/2279Mi)
% 203.05/29.36  % (774147)Instruction limit reached! 
% 203.05/29.36  % (774147)------------------------------
% 203.05/29.36  % (774147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774147)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774147)Termination reason: Instruction limit
% 148.45/31.54  % (774147)Termination phase: Saturation
% 148.45/31.54  % (774147)Time elapsed: 2.256 s
% 148.45/31.54  % (774147)Peak memory usage: 138 MB
% 148.45/31.54  % (774147)Instructions burned: 2280 (million)
% 148.45/31.54  % (774151)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=3922651311:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2917 on theBenchmark for (2917ds/6225Mi)
% 148.45/31.54  % (774139)Instruction limit reached! 
% 148.45/31.54  % (774139)------------------------------
% 148.45/31.54  % (774139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774139)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774139)Termination reason: Instruction limit
% 148.45/31.54  % (774139)Termination phase: Saturation
% 148.45/31.54  % (774139)Time elapsed: 6.934 s
% 148.45/31.54  % (774139)Peak memory usage: 240 MB
% 148.45/31.54  % (774139)Instructions burned: 11833 (million)
% 148.45/31.54  % (774154)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=3965895721:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2894 on theBenchmark for (2894ds/21755Mi)
% 148.45/31.54  % (774130)Instruction limit reached! 
% 148.45/31.54  % (774130)------------------------------
% 148.45/31.54  % (774130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774130)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774130)Termination reason: Instruction limit
% 148.45/31.54  % (774130)Termination phase: Saturation
% 148.45/31.54  % (774130)Time elapsed: 12.183 s
% 148.45/31.54  % (774130)Peak memory usage: 245 MB
% 148.45/31.54  % (774130)Instructions burned: 12125 (million)
% 148.45/31.54  % (774159)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=1387895712:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2861 on theBenchmark for (2861ds/16427Mi)
% 148.45/31.54  % (774151)Instruction limit reached! 
% 148.45/31.54  % (774151)------------------------------
% 148.45/31.54  % (774151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774151)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774151)Termination reason: Instruction limit
% 148.45/31.54  % (774151)Termination phase: Saturation
% 148.45/31.54  % (774151)Time elapsed: 6.389 s
% 148.45/31.54  % (774151)Peak memory usage: 165 MB
% 148.45/31.54  % (774151)Instructions burned: 6225 (million)
% 148.45/31.54  % (774161)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=3555681542:i=9356:fgj=on:bd=preordered:av=off_2850 on theBenchmark for (2850ds/9356Mi)
% 148.45/31.54  % (774137)Instruction limit reached! 
% 148.45/31.54  % (774137)------------------------------
% 148.45/31.54  % (774137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774137)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774137)Termination reason: Instruction limit
% 148.45/31.54  % (774137)Termination phase: Saturation
% 148.45/31.54  % (774137)Time elapsed: 15.510 s
% 148.45/31.54  % (774137)Peak memory usage: 258 MB
% 148.45/31.54  % (774137)Instructions burned: 14534 (million)
% 148.45/31.54  % (774163)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=2662479481:i=2070:kws=inv_precedence:slsql=off:bd=all_2819 on theBenchmark for (2819ds/2070Mi)
% 148.45/31.54  % (774163)Instruction limit reached! 
% 148.45/31.54  % (774163)------------------------------
% 148.45/31.54  % (774163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774163)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774163)Termination reason: Instruction limit
% 148.45/31.54  % (774163)Termination phase: Saturation
% 148.45/31.54  % (774163)Time elapsed: 2.094 s
% 148.45/31.54  % (774163)Peak memory usage: 130 MB
% 148.45/31.54  % (774163)Instructions burned: 2070 (million)
% 148.45/31.54  % (774167)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=3100958534:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2796 on theBenchmark for (2796ds/6461Mi)
% 148.45/31.54  % (774161)Instruction limit reached! 
% 148.45/31.54  % (774161)------------------------------
% 148.45/31.54  % (774161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774161)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774161)Termination reason: Instruction limit
% 148.45/31.54  % (774161)Termination phase: Saturation
% 148.45/31.54  % (774161)Time elapsed: 8.540 s
% 148.45/31.54  % (774161)Peak memory usage: 383 MB
% 148.45/31.54  % (774161)Instructions burned: 9357 (million)
% 148.45/31.54  % (774169)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=2039696140:i=2310:bd=all:ss=included_2761 on theBenchmark for (2761ds/2310Mi)
% 148.45/31.54  % (774154)Instruction limit reached! 
% 148.45/31.54  % (774154)------------------------------
% 148.45/31.54  % (774154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774154)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774154)Termination reason: Instruction limit
% 148.45/31.54  % (774154)Termination phase: Saturation
% 148.45/31.54  % (774154)Time elapsed: 14.352 s
% 148.45/31.54  % (774154)Peak memory usage: 291 MB
% 148.45/31.54  % (774154)Instructions burned: 21755 (million)
% 148.45/31.54  % (774171)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=2081374884:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2748 on theBenchmark for (2748ds/2616Mi)
% 148.45/31.54  % (774169)Instruction limit reached! 
% 148.45/31.54  % (774169)------------------------------
% 148.45/31.54  % (774169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774169)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774169)Termination reason: Instruction limit
% 148.45/31.54  % (774169)Termination phase: Saturation
% 148.45/31.54  % (774169)Time elapsed: 2.235 s
% 148.45/31.54  % (774169)Peak memory usage: 108 MB
% 148.45/31.54  % (774169)Instructions burned: 2311 (million)
% 148.45/31.54  % (774171)Instruction limit reached! 
% 148.45/31.54  % (774171)------------------------------
% 148.45/31.54  % (774171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774171)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774171)Termination reason: Instruction limit
% 148.45/31.54  % (774171)Termination phase: Saturation
% 148.45/31.54  % (774171)Time elapsed: 1.298 s
% 148.45/31.54  % (774171)Peak memory usage: 127 MB
% 148.45/31.54  % (774171)Instructions burned: 2617 (million)
% 148.45/31.54  % (774173)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=2138568184:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2736 on theBenchmark for (2736ds/30521Mi)
% 148.45/31.54  % (774175)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=2784661896:i=3258:fgj=on:bd=all:ins=1_2733 on theBenchmark for (2733ds/3258Mi)
% 148.45/31.54  % (774167)Instruction limit reached! 
% 148.45/31.54  % (774167)------------------------------
% 148.45/31.54  % (774167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774167)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774167)Termination reason: Instruction limit
% 148.45/31.54  % (774167)Termination phase: Saturation
% 148.45/31.54  % (774167)Time elapsed: 6.422 s
% 148.45/31.54  % (774167)Peak memory usage: 173 MB
% 148.45/31.54  % (774167)Instructions burned: 6462 (million)
% 148.45/31.54  % (774273)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=1095184124:i=5037:kws=precedence_2728 on theBenchmark for (2728ds/5037Mi)
% 148.45/31.54  % (774175)Instruction limit reached! 
% 148.45/31.54  % (774175)------------------------------
% 148.45/31.54  % (774175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774175)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774175)Termination reason: Instruction limit
% 148.45/31.54  % (774175)Termination phase: Saturation
% 148.45/31.54  % (774175)Time elapsed: 1.728 s
% 148.45/31.54  % (774175)Peak memory usage: 149 MB
% 148.45/31.54  % (774175)Instructions burned: 3259 (million)
% 148.45/31.54  % (774332)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=164457602:i=65240_2714 on theBenchmark for (2714ds/65240Mi)
% 148.45/31.54  % (774159)Instruction limit reached! 
% 148.45/31.54  % (774159)------------------------------
% 148.45/31.54  % (774159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774159)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774159)Termination reason: Instruction limit
% 148.45/31.54  % (774159)Termination phase: Saturation
% 148.45/31.54  % (774159)Time elapsed: 15.521 s
% 148.45/31.54  % (774159)Peak memory usage: 268 MB
% 148.45/31.54  % (774159)Instructions burned: 16428 (million)
% 148.45/31.54  % (774334)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=1221475265:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2702 on theBenchmark for (2702ds/16502Mi)
% 148.45/31.54  % (774273)Instruction limit reached! 
% 148.45/31.54  % (774273)------------------------------
% 148.45/31.54  % (774273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/31.54  % (774273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/31.54  % (774273)CaDiCaL version: 2.1.3
% 148.45/31.54  % (774273)Termination reason: Instruction limit
% 148.45/31.54  % (774273)Termination phase: Saturation
% 148.45/31.54  % (774273)Time elapsed: 2.993 s
% 148.45/31.54  % (774273)Peak memory usage: 171 MB
% 148.45/31.54  % (774273)Instructions burned: 5037 (million)
% 148.45/31.54  % (774108)First to succeed.
% 148.45/31.54  % (774108)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-774101"
% 148.45/31.54  % (774336)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=1312146042:i=7623:bd=preordered:er=filter_2697 on theBenchmark for (2697ds/7623Mi)
% 148.45/31.54  % (774108)Refutation found. Thanks to Tanya!
% 148.45/31.54  % SZS status Unsatisfiable for theBenchmark
% 148.45/31.54  % SZS output start Proof for theBenchmark
% See solution above
% 218.93/31.75  % (774108)------------------------------
% 218.93/31.75  % (774108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 218.93/31.75  % (774108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.93/31.75  % (774108)CaDiCaL version: 2.1.3
% 218.93/31.75  % (774108)Termination reason: Refutation
% 218.93/31.75  % (774108)Time elapsed: 30.141 s
% 218.93/31.75  % (774108)Peak memory usage: 384 MB
% 218.93/31.75  % (774108)Instructions burned: 29425 (million)
% 218.93/31.75  % (774108)------------------------------
% 218.93/31.75  % (774108)------------------------------
% 218.93/31.75  % (774101)Success in time 30.745 s
% 218.93/31.75  % Vampire exiting
%------------------------------------------------------------------------------