%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP764-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 : n004.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 51.16s 25.32s
% Output : Refutation 98.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 133
% Number of leaves : 20
% Syntax : Number of formulae : 843 ( 843 unt; 7 def)
% Number of atoms : 843 ( 842 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 : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-2 aty)
% Number of variables : 682 ( 682 !; 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(x0,product(eta(x0),x1)) != product(j(j(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(x0,product(product(difference(x0,one),x0),x1)) != product(quotient(one,quotient(one,x0)),x1),
inference(definition_unfolding,[],[f14,f15,f10,f10]) ).
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 = product(sF0,x0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f21,plain,
product(sF0,x0) = 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(x0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f25,plain,
product(x0,sF2) = sF3,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF4 = quotient(one,x0),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f27,plain,
quotient(one,x0) = sF4,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF5 = quotient(one,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f29,plain,
quotient(one,sF4) = sF5,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF6 = product(sF5,x1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f31,plain,
product(sF5,x1) = sF6,
inference(reorient_equations,[],[f30]) ).
fof(f32,plain,
sF3 != sF6,
inference(definition_folding,[],[f17,f31,f29,f27,f25,f23,f21,f19]) ).
fof(f36,plain,
product(sF0,x0) = product(x0,quotient(one,x0)),
inference(superposition,[],[f16,f19]) ).
fof(f37,plain,
product(sF0,x0) = product(x0,sF4),
inference(forward_demodulation,[],[f36,f27]) ).
fof(f38,plain,
sF1 = product(x0,sF4),
inference(forward_demodulation,[],[f37,f21]) ).
fof(f40,plain,
! [X0] : difference(sF1,product(x0,product(sF4,X0))) = quotient(quotient(product(X0,sF1),sF4),x0),
inference(superposition,[],[f8,f38]) ).
fof(f42,plain,
sF4 = difference(x0,sF1),
inference(superposition,[],[f4,f38]) ).
fof(f43,plain,
! [X2,X0,X1] : product(X1,product(X2,X0)) = product(product(X1,X2),quotient(quotient(product(X0,product(X1,X2)),X2),X1)),
inference(superposition,[],[f3,f8]) ).
fof(f44,plain,
one = product(x0,sF0),
inference(superposition,[],[f3,f19]) ).
fof(f45,plain,
! [X2,X0,X1] : quotient(quotient(product(difference(X2,X0),product(X1,X2)),X2),X1) = difference(product(X1,X2),product(X1,X0)),
inference(superposition,[],[f8,f3]) ).
fof(f46,plain,
! [X2,X0,X1] : difference(X0,product(X1,product(difference(X1,X0),X2))) = quotient(quotient(product(X2,X0),difference(X1,X0)),X1),
inference(superposition,[],[f8,f3]) ).
fof(f47,plain,
x0 = difference(sF0,sF1),
inference(superposition,[],[f4,f21]) ).
fof(f49,plain,
! [X0] : difference(sF1,product(sF0,product(x0,X0))) = quotient(quotient(product(X0,sF1),x0),sF0),
inference(superposition,[],[f8,f21]) ).
fof(f50,plain,
x1 = difference(sF1,sF2),
inference(superposition,[],[f4,f23]) ).
fof(f59,plain,
! [X0,X1] : quotient(X0,difference(X1,X0)) = X1,
inference(superposition,[],[f5,f3]) ).
fof(f60,plain,
! [X0] : difference(X0,one) = quotient(product(X0,quotient(one,X0)),X0),
inference(superposition,[],[f5,f16]) ).
fof(f63,plain,
sF0 = quotient(sF1,x0),
inference(superposition,[],[f5,f21]) ).
fof(f67,plain,
x0 = quotient(one,sF0),
inference(superposition,[],[f59,f19]) ).
fof(f70,plain,
! [X0] : quotient(X0,one) = X0,
inference(superposition,[],[f5,f1]) ).
fof(f71,plain,
! [X0] : one = difference(X0,X0),
inference(superposition,[],[f4,f1]) ).
fof(f72,plain,
! [X0,X1] : quotient(quotient(product(one,product(X1,X0)),X0),X1) = difference(product(X1,X0),product(X1,X0)),
inference(superposition,[],[f8,f1]) ).
fof(f77,plain,
! [X0,X1] : difference(product(X1,X0),product(X1,X0)) = quotient(quotient(product(X1,X0),X0),X1),
inference(forward_demodulation,[],[f72,f2]) ).
fof(f81,plain,
! [X0,X1] : difference(product(X1,X0),product(X1,X0)) = quotient(X1,X1),
inference(forward_demodulation,[],[f77,f5]) ).
fof(f84,plain,
! [X1] : one = quotient(X1,X1),
inference(forward_demodulation,[],[f81,f71]) ).
fof(f91,plain,
! [X0] : difference(one,X0) = X0,
inference(superposition,[],[f3,f2]) ).
fof(f101,plain,
! [X2,X0,X1] : quotient(product(difference(X1,X0),product(X2,X1)),X1) = difference(X1,product(X0,X2)),
inference(superposition,[],[f7,f3]) ).
fof(f113,plain,
! [X2,X0,X1] : product(product(X2,X0),X1) = product(X2,quotient(product(X0,product(X1,X2)),X2)),
inference(superposition,[],[f3,f7]) ).
fof(f123,plain,
! [X2,X0,X1] : difference(product(X1,X2),product(X1,X0)) = quotient(difference(X2,product(X0,X1)),X1),
inference(backward_demodulation,[],[f45,f101]) ).
fof(f129,plain,
one = product(sF4,x0),
inference(superposition,[],[f6,f27]) ).
fof(f135,plain,
! [X0,X1] : difference(quotient(X0,X1),X0) = X1,
inference(superposition,[],[f4,f6]) ).
fof(f148,plain,
! [X2,X0,X1] : difference(X0,product(X1,X2)) = quotient(difference(difference(X1,X0),product(X2,X1)),X1),
inference(superposition,[],[f123,f3]) ).
fof(f152,plain,
! [X2,X0,X1] : quotient(difference(X1,product(X2,quotient(X0,X1))),quotient(X0,X1)) = difference(X0,product(quotient(X0,X1),X2)),
inference(superposition,[],[f123,f6]) ).
fof(f155,plain,
! [X0] : quotient(difference(x0,product(X0,sF0)),sF0) = difference(sF1,product(sF0,X0)),
inference(superposition,[],[f123,f21]) ).
fof(f158,plain,
! [X2,X0,X1] : difference(product(X1,X2),X0) = quotient(difference(X2,product(difference(X1,X0),X1)),X1),
inference(superposition,[],[f123,f3]) ).
fof(f159,plain,
! [X0,X1] : quotient(difference(X1,product(one,X0)),X0) = difference(product(X0,X1),X0),
inference(superposition,[],[f123,f1]) ).
fof(f163,plain,
! [X0] : quotient(difference(X0,product(sF4,x0)),x0) = difference(product(x0,X0),sF1),
inference(superposition,[],[f123,f38]) ).
fof(f175,plain,
! [X0] : difference(product(x0,X0),sF1) = quotient(difference(X0,one),x0),
inference(forward_demodulation,[],[f163,f129]) ).
fof(f178,plain,
! [X0,X1] : difference(product(X0,X1),X0) = quotient(difference(X1,X0),X0),
inference(forward_demodulation,[],[f159,f2]) ).
fof(f190,plain,
! [X0] : difference(one,product(x0,product(sF0,X0))) = quotient(quotient(product(X0,one),sF0),x0),
inference(superposition,[],[f46,f19]) ).
fof(f214,plain,
! [X0] : difference(one,product(x0,product(sF0,X0))) = quotient(quotient(X0,sF0),x0),
inference(forward_demodulation,[],[f190,f1]) ).
fof(f222,plain,
! [X0] : product(x0,product(sF0,X0)) = quotient(quotient(X0,sF0),x0),
inference(forward_demodulation,[],[f214,f91]) ).
fof(f250,plain,
quotient(difference(sF4,one),x0) = difference(sF1,sF1),
inference(superposition,[],[f175,f38]) ).
fof(f258,plain,
one = quotient(difference(sF4,one),x0),
inference(forward_demodulation,[],[f250,f71]) ).
fof(f260,plain,
difference(sF4,one) = product(one,x0),
inference(superposition,[],[f6,f258]) ).
fof(f261,plain,
x0 = difference(sF4,one),
inference(forward_demodulation,[],[f260,f2]) ).
fof(f264,plain,
product(x0,sF4) = product(sF4,quotient(one,sF4)),
inference(superposition,[],[f16,f261]) ).
fof(f265,plain,
! [X0] : difference(one,product(sF4,product(x0,X0))) = quotient(quotient(product(X0,one),x0),sF4),
inference(superposition,[],[f46,f261]) ).
fof(f268,plain,
! [X0] : difference(one,product(sF4,product(x0,X0))) = quotient(quotient(X0,x0),sF4),
inference(forward_demodulation,[],[f265,f1]) ).
fof(f269,plain,
product(x0,sF4) = product(sF4,sF5),
inference(forward_demodulation,[],[f264,f29]) ).
fof(f270,plain,
! [X0] : product(sF4,product(x0,X0)) = quotient(quotient(X0,x0),sF4),
inference(forward_demodulation,[],[f268,f91]) ).
fof(f271,plain,
sF1 = product(sF4,sF5),
inference(forward_demodulation,[],[f269,f38]) ).
fof(f275,plain,
! [X0] : quotient(product(sF5,product(X0,sF4)),sF4) = difference(sF4,product(sF1,X0)),
inference(superposition,[],[f7,f271]) ).
fof(f277,plain,
sF5 = difference(sF4,sF1),
inference(superposition,[],[f4,f271]) ).
fof(f288,plain,
! [X0,X1] : product(X0,product(difference(X0,one),X1)) = quotient(quotient(product(X1,one),difference(X0,one)),X0),
inference(superposition,[],[f46,f91]) ).
fof(f289,plain,
! [X0,X1] : product(X0,product(difference(X0,one),X1)) = quotient(quotient(X1,difference(X0,one)),X0),
inference(forward_demodulation,[],[f288,f1]) ).
fof(f311,plain,
! [X0,X1] : quotient(X1,difference(X0,one)) = product(product(X0,product(difference(X0,one),X1)),X0),
inference(superposition,[],[f6,f289]) ).
fof(f335,plain,
sF4 = difference(sF5,one),
inference(superposition,[],[f135,f29]) ).
fof(f352,plain,
! [X0] : difference(x0,product(one,X0)) = quotient(product(sF0,product(X0,x0)),x0),
inference(superposition,[],[f101,f19]) ).
fof(f360,plain,
! [X2,X0,X1] : difference(X1,product(X2,quotient(X0,X1))) = quotient(product(difference(X1,X2),X0),X1),
inference(superposition,[],[f101,f6]) ).
fof(f369,plain,
! [X2,X0,X1] : product(difference(X0,X1),product(X2,X0)) = product(difference(X0,product(X1,X2)),X0),
inference(superposition,[],[f6,f101]) ).
fof(f374,plain,
! [X2,X0,X1] : difference(X0,product(quotient(X0,X1),X2)) = quotient(quotient(product(difference(X1,X2),X0),X1),quotient(X0,X1)),
inference(backward_demodulation,[],[f152,f360]) ).
fof(f379,plain,
! [X0] : difference(x0,X0) = quotient(product(sF0,product(X0,x0)),x0),
inference(forward_demodulation,[],[f352,f2]) ).
fof(f389,plain,
! [X0] : difference(x0,quotient(X0,x0)) = quotient(product(sF0,X0),x0),
inference(superposition,[],[f379,f6]) ).
fof(f392,plain,
! [X0] : product(sF0,product(X0,x0)) = product(difference(x0,X0),x0),
inference(superposition,[],[f6,f379]) ).
fof(f398,plain,
product(sF4,x0) = product(sF0,product(sF1,x0)),
inference(superposition,[],[f392,f42]) ).
fof(f399,plain,
! [X0] : product(X0,x0) = product(sF0,product(product(x0,X0),x0)),
inference(superposition,[],[f392,f4]) ).
fof(f418,plain,
one = product(sF0,product(sF1,x0)),
inference(forward_demodulation,[],[f398,f129]) ).
fof(f433,plain,
! [X0] : product(product(x0,X0),x0) = difference(sF0,product(X0,x0)),
inference(superposition,[],[f4,f399]) ).
fof(f437,plain,
product(product(x0,one),x0) = difference(sF0,x0),
inference(superposition,[],[f433,f2]) ).
fof(f440,plain,
! [X0] : product(product(x0,quotient(X0,x0)),x0) = difference(sF0,X0),
inference(superposition,[],[f433,f6]) ).
fof(f445,plain,
! [X0] : quotient(product(X0,product(x0,sF0)),sF0) = product(product(x0,product(sF0,X0)),x0),
inference(superposition,[],[f7,f433]) ).
fof(f450,plain,
! [X0] : quotient(product(X0,one),sF0) = product(product(x0,product(sF0,X0)),x0),
inference(forward_demodulation,[],[f445,f44]) ).
fof(f457,plain,
product(x0,x0) = difference(sF0,x0),
inference(forward_demodulation,[],[f437,f1]) ).
fof(f458,plain,
! [X0] : quotient(X0,sF0) = product(product(x0,product(sF0,X0)),x0),
inference(forward_demodulation,[],[f450,f1]) ).
fof(f469,plain,
product(product(x0,sF4),x0) = difference(sF0,one),
inference(superposition,[],[f440,f27]) ).
fof(f483,plain,
! [X0] : product(x0,quotient(X0,x0)) = quotient(difference(sF0,X0),x0),
inference(superposition,[],[f5,f440]) ).
fof(f492,plain,
product(sF1,x0) = difference(sF0,one),
inference(forward_demodulation,[],[f469,f38]) ).
fof(f498,plain,
product(sF0,quotient(one,sF0)) = product(product(sF1,x0),sF0),
inference(superposition,[],[f16,f492]) ).
fof(f505,plain,
product(sF0,x0) = product(product(sF1,x0),sF0),
inference(forward_demodulation,[],[f498,f67]) ).
fof(f507,plain,
sF1 = product(product(sF1,x0),sF0),
inference(forward_demodulation,[],[f505,f21]) ).
fof(f511,plain,
! [X0] : quotient(X0,x0) = product(x0,quotient(product(sF0,X0),x0)),
inference(superposition,[],[f483,f4]) ).
fof(f514,plain,
quotient(one,x0) = product(x0,quotient(sF0,x0)),
inference(superposition,[],[f483,f71]) ).
fof(f518,plain,
sF4 = product(x0,quotient(sF0,x0)),
inference(forward_demodulation,[],[f514,f27]) ).
fof(f527,plain,
difference(sF4,sF1) = quotient(difference(quotient(sF0,x0),one),x0),
inference(superposition,[],[f175,f518]) ).
fof(f531,plain,
! [X0] : quotient(product(quotient(sF0,x0),product(X0,x0)),x0) = difference(x0,product(sF4,X0)),
inference(superposition,[],[f7,f518]) ).
fof(f533,plain,
quotient(sF0,x0) = difference(x0,sF4),
inference(superposition,[],[f4,f518]) ).
fof(f535,plain,
sF5 = quotient(difference(quotient(sF0,x0),one),x0),
inference(forward_demodulation,[],[f527,f277]) ).
fof(f544,plain,
product(sF1,x0) = quotient(sF1,sF0),
inference(superposition,[],[f5,f507]) ).
fof(f545,plain,
sF0 = difference(product(sF1,x0),sF1),
inference(superposition,[],[f4,f507]) ).
fof(f546,plain,
sF0 = quotient(difference(x0,sF1),sF1),
inference(forward_demodulation,[],[f545,f178]) ).
fof(f551,plain,
sF0 = quotient(sF4,sF1),
inference(forward_demodulation,[],[f546,f42]) ).
fof(f553,plain,
sF1 = difference(sF0,sF4),
inference(superposition,[],[f135,f551]) ).
fof(f554,plain,
sF4 = product(sF0,sF1),
inference(superposition,[],[f6,f551]) ).
fof(f558,plain,
quotient(sF1,x0) = product(x0,quotient(sF4,x0)),
inference(superposition,[],[f483,f553]) ).
fof(f563,plain,
sF0 = product(x0,quotient(sF4,x0)),
inference(forward_demodulation,[],[f558,f63]) ).
fof(f622,plain,
! [X0] : difference(sF4,product(x0,product(quotient(sF0,x0),X0))) = quotient(quotient(product(X0,sF4),quotient(sF0,x0)),x0),
inference(superposition,[],[f46,f533]) ).
fof(f630,plain,
! [X0] : quotient(difference(X0,product(product(sF1,x0),sF0)),sF0) = difference(product(sF0,X0),one),
inference(superposition,[],[f123,f418]) ).
fof(f637,plain,
! [X0] : difference(product(sF0,X0),one) = quotient(difference(X0,sF1),sF0),
inference(forward_demodulation,[],[f630,f507]) ).
fof(f649,plain,
! [X0] : quotient(product(sF0,quotient(X0,difference(x0,one))),x0) = difference(x0,product(x0,product(difference(x0,one),X0))),
inference(superposition,[],[f389,f289]) ).
fof(f656,plain,
! [X0] : product(difference(x0,one),X0) = quotient(product(sF0,quotient(X0,difference(x0,one))),x0),
inference(forward_demodulation,[],[f649,f4]) ).
fof(f661,plain,
! [X0] : product(sF0,X0) = quotient(product(sF0,quotient(X0,sF0)),x0),
inference(forward_demodulation,[],[f656,f19]) ).
fof(f666,plain,
! [X0] : quotient(product(sF0,X0),x0) = product(sF0,product(X0,sF0)),
inference(superposition,[],[f661,f5]) ).
fof(f672,plain,
! [X0] : difference(x0,product(sF0,X0)) = quotient(product(sF0,product(sF0,quotient(X0,sF0))),x0),
inference(superposition,[],[f389,f661]) ).
fof(f675,plain,
! [X0] : product(product(sF0,X0),x0) = product(sF0,quotient(X0,sF0)),
inference(superposition,[],[f6,f661]) ).
fof(f682,plain,
! [X0] : difference(x0,X0) = product(sF0,product(product(X0,x0),sF0)),
inference(backward_demodulation,[],[f379,f666]) ).
fof(f684,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF0,product(product(sF0,quotient(X0,sF0)),sF0)),
inference(backward_demodulation,[],[f672,f666]) ).
fof(f686,plain,
! [X0] : difference(x0,quotient(X0,x0)) = product(sF0,product(X0,sF0)),
inference(backward_demodulation,[],[f389,f666]) ).
fof(f687,plain,
! [X0] : quotient(X0,x0) = product(x0,product(sF0,product(X0,sF0))),
inference(backward_demodulation,[],[f511,f666]) ).
fof(f712,plain,
! [X0] : quotient(X0,x0) = product(sF0,product(difference(sF0,X0),sF0)),
inference(superposition,[],[f666,f3]) ).
fof(f713,plain,
quotient(sF0,x0) = product(sF0,product(one,sF0)),
inference(superposition,[],[f666,f1]) ).
fof(f724,plain,
quotient(sF0,x0) = product(sF0,sF0),
inference(forward_demodulation,[],[f713,f2]) ).
fof(f733,plain,
! [X0] : difference(x0,product(sF4,X0)) = quotient(product(product(sF0,sF0),product(X0,x0)),x0),
inference(backward_demodulation,[],[f531,f724]) ).
fof(f735,plain,
difference(x0,sF4) = product(sF0,sF0),
inference(backward_demodulation,[],[f533,f724]) ).
fof(f736,plain,
sF5 = quotient(difference(product(sF0,sF0),one),x0),
inference(backward_demodulation,[],[f535,f724]) ).
fof(f737,plain,
! [X0] : difference(sF4,product(x0,product(product(sF0,sF0),X0))) = quotient(quotient(product(X0,sF4),product(sF0,sF0)),x0),
inference(backward_demodulation,[],[f622,f724]) ).
fof(f742,plain,
sF5 = quotient(quotient(difference(sF0,sF1),sF0),x0),
inference(forward_demodulation,[],[f736,f637]) ).
fof(f744,plain,
sF5 = product(x0,product(sF0,difference(sF0,sF1))),
inference(forward_demodulation,[],[f742,f222]) ).
fof(f745,plain,
sF5 = product(x0,sF1),
inference(forward_demodulation,[],[f744,f3]) ).
fof(f753,plain,
x0 = quotient(sF5,sF1),
inference(superposition,[],[f5,f745]) ).
fof(f754,plain,
sF1 = difference(x0,sF5),
inference(superposition,[],[f4,f745]) ).
fof(f793,plain,
! [X0,X1] : quotient(product(product(sF0,X0),X1),x0) = product(sF0,product(quotient(product(X0,product(X1,sF0)),sF0),sF0)),
inference(superposition,[],[f712,f7]) ).
fof(f809,plain,
! [X0,X1] : quotient(product(product(sF0,X0),X1),x0) = product(sF0,product(X0,product(X1,sF0))),
inference(forward_demodulation,[],[f793,f6]) ).
fof(f816,plain,
! [X0] : difference(x0,product(sF4,X0)) = product(sF0,product(sF0,product(product(X0,x0),sF0))),
inference(backward_demodulation,[],[f733,f809]) ).
fof(f821,plain,
! [X0] : difference(x0,product(sF4,X0)) = product(sF0,difference(x0,X0)),
inference(forward_demodulation,[],[f816,f682]) ).
fof(f899,plain,
! [X0] : product(product(X0,x0),sF0) = difference(sF0,difference(x0,X0)),
inference(superposition,[],[f4,f682]) ).
fof(f936,plain,
! [X0] : product(sF4,X0) = product(x0,product(sF0,difference(x0,X0))),
inference(superposition,[],[f3,f821]) ).
fof(f947,plain,
product(sF4,sF4) = product(x0,product(sF0,product(sF0,sF0))),
inference(superposition,[],[f936,f735]) ).
fof(f949,plain,
! [X0] : product(x0,product(sF0,X0)) = product(sF4,product(x0,X0)),
inference(superposition,[],[f936,f4]) ).
fof(f971,plain,
! [X0] : quotient(X0,sF0) = product(product(sF4,product(x0,X0)),x0),
inference(backward_demodulation,[],[f458,f949]) ).
fof(f972,plain,
! [X0] : quotient(quotient(X0,sF0),x0) = product(sF4,product(x0,X0)),
inference(backward_demodulation,[],[f222,f949]) ).
fof(f974,plain,
! [X0] : quotient(X0,x0) = product(sF4,product(x0,product(X0,sF0))),
inference(backward_demodulation,[],[f687,f949]) ).
fof(f982,plain,
product(sF4,sF4) = product(sF4,product(x0,product(sF0,sF0))),
inference(forward_demodulation,[],[f947,f949]) ).
fof(f993,plain,
quotient(sF0,x0) = product(sF4,sF4),
inference(forward_demodulation,[],[f982,f974]) ).
fof(f999,plain,
product(sF0,sF0) = product(sF4,sF4),
inference(forward_demodulation,[],[f993,f724]) ).
fof(f1034,plain,
product(x0,sF1) = product(sF4,product(x0,x0)),
inference(superposition,[],[f949,f21]) ).
fof(f1035,plain,
! [X0] : product(x0,product(X0,x0)) = product(sF4,product(x0,product(product(x0,X0),x0))),
inference(superposition,[],[f949,f399]) ).
fof(f1040,plain,
! [X0] : product(x0,X0) = product(sF4,product(x0,difference(sF0,X0))),
inference(superposition,[],[f949,f3]) ).
fof(f1062,plain,
sF5 = product(sF4,product(x0,x0)),
inference(forward_demodulation,[],[f1034,f745]) ).
fof(f1075,plain,
! [X0] : quotient(difference(product(x0,x0),product(X0,sF4)),sF4) = difference(sF5,product(sF4,X0)),
inference(superposition,[],[f123,f1062]) ).
fof(f1078,plain,
product(x0,x0) = difference(sF4,sF5),
inference(superposition,[],[f4,f1062]) ).
fof(f1088,plain,
product(x0,x0) = product(sF4,product(x0,product(x0,x0))),
inference(superposition,[],[f1040,f457]) ).
fof(f1100,plain,
! [X0] : difference(sF4,product(x0,X0)) = product(x0,difference(sF0,X0)),
inference(superposition,[],[f4,f1040]) ).
fof(f1101,plain,
! [X0] : quotient(quotient(product(X0,sF4),product(sF0,sF0)),x0) = product(x0,difference(sF0,product(product(sF0,sF0),X0))),
inference(backward_demodulation,[],[f737,f1100]) ).
fof(f1108,plain,
! [X0] : quotient(quotient(product(X0,sF4),product(sF0,sF0)),x0) = product(x0,quotient(product(sF0,product(X0,sF0)),sF0)),
inference(forward_demodulation,[],[f1101,f7]) ).
fof(f1116,plain,
! [X0] : difference(sF4,X0) = product(x0,difference(sF0,difference(x0,X0))),
inference(superposition,[],[f1100,f3]) ).
fof(f1117,plain,
difference(sF4,x0) = product(x0,difference(sF0,one)),
inference(superposition,[],[f1100,f1]) ).
fof(f1126,plain,
difference(sF4,x0) = product(x0,product(sF1,x0)),
inference(forward_demodulation,[],[f1117,f492]) ).
fof(f1127,plain,
! [X0] : difference(sF4,X0) = product(x0,product(product(X0,x0),sF0)),
inference(forward_demodulation,[],[f1116,f899]) ).
fof(f1139,plain,
! [X0] : product(product(sF4,X0),x0) = quotient(difference(x0,X0),sF0),
inference(superposition,[],[f971,f3]) ).
fof(f1142,plain,
! [X0] : product(product(x0,X0),x0) = quotient(difference(sF0,X0),sF0),
inference(superposition,[],[f971,f1040]) ).
fof(f1143,plain,
! [X0] : quotient(product(product(x0,X0),product(x0,sF4)),sF4) = difference(sF4,quotient(X0,sF0)),
inference(superposition,[],[f7,f971]) ).
fof(f1154,plain,
! [X0] : difference(sF4,quotient(X0,sF0)) = quotient(product(product(x0,X0),sF1),sF4),
inference(forward_demodulation,[],[f1143,f38]) ).
fof(f1158,plain,
! [X0] : difference(sF1,product(sF0,X0)) = product(product(sF4,product(X0,sF0)),x0),
inference(backward_demodulation,[],[f155,f1139]) ).
fof(f1168,plain,
! [X0] : quotient(product(sF0,product(X0,sF0)),sF0) = product(product(sF4,quotient(X0,x0)),x0),
inference(superposition,[],[f1139,f686]) ).
fof(f1179,plain,
! [X0] : difference(x0,X0) = product(product(product(sF4,X0),x0),sF0),
inference(superposition,[],[f6,f1139]) ).
fof(f1184,plain,
! [X0] : quotient(quotient(product(X0,sF4),product(sF0,sF0)),x0) = product(x0,product(product(sF4,quotient(X0,x0)),x0)),
inference(backward_demodulation,[],[f1108,f1168]) ).
fof(f1255,plain,
! [X2,X0,X1] : product(X1,product(X2,quotient(X0,product(X1,X2)))) = product(product(X1,X2),quotient(quotient(X0,X2),X1)),
inference(superposition,[],[f43,f6]) ).
fof(f1343,plain,
! [X0,X1] : difference(X1,product(X0,one)) = quotient(difference(difference(X0,X1),X0),X0),
inference(superposition,[],[f148,f2]) ).
fof(f1350,plain,
! [X2,X0,X1] : difference(X1,product(X2,quotient(X0,X2))) = quotient(difference(difference(X2,X1),X0),X2),
inference(superposition,[],[f148,f6]) ).
fof(f1371,plain,
! [X2,X0,X1] : difference(difference(X1,X0),product(X2,X1)) = product(difference(X0,product(X1,X2)),X1),
inference(superposition,[],[f6,f148]) ).
fof(f1408,plain,
! [X0,X1] : difference(X1,X0) = quotient(difference(difference(X0,X1),X0),X0),
inference(forward_demodulation,[],[f1343,f1]) ).
fof(f1476,plain,
difference(sF1,x0) = quotient(difference(sF4,x0),x0),
inference(superposition,[],[f1408,f42]) ).
fof(f1478,plain,
difference(sF5,x0) = quotient(difference(sF1,x0),x0),
inference(superposition,[],[f1408,f754]) ).
fof(f1483,plain,
difference(sF4,sF0) = quotient(difference(sF1,sF0),sF0),
inference(superposition,[],[f1408,f553]) ).
fof(f1601,plain,
! [X2,X3,X0,X1] : difference(product(X2,X3),product(product(X2,X0),X1)) = quotient(difference(X3,product(quotient(product(X0,product(X1,X2)),X2),X2)),X2),
inference(superposition,[],[f158,f7]) ).
fof(f1610,plain,
! [X0] : difference(product(x0,X0),one) = quotient(difference(X0,product(sF0,x0)),x0),
inference(superposition,[],[f158,f19]) ).
fof(f1645,plain,
! [X2,X0,X1] : product(difference(product(X0,X1),X2),X0) = difference(X1,product(difference(X0,X2),X0)),
inference(superposition,[],[f6,f158]) ).
fof(f1684,plain,
! [X0] : difference(product(x0,X0),one) = quotient(difference(X0,sF1),x0),
inference(forward_demodulation,[],[f1610,f21]) ).
fof(f1688,plain,
! [X2,X3,X0,X1] : difference(product(X2,X3),product(product(X2,X0),X1)) = quotient(difference(X3,product(X0,product(X1,X2))),X2),
inference(forward_demodulation,[],[f1601,f6]) ).
fof(f1735,plain,
difference(sF1,one) = quotient(difference(sF4,sF1),x0),
inference(superposition,[],[f1684,f38]) ).
fof(f1749,plain,
difference(sF1,one) = quotient(sF5,x0),
inference(forward_demodulation,[],[f1735,f277]) ).
fof(f1777,plain,
! [X0] : difference(x0,product(X0,sF4)) = quotient(product(difference(x0,X0),one),x0),
inference(superposition,[],[f101,f129]) ).
fof(f1782,plain,
! [X0] : quotient(difference(x0,X0),x0) = difference(x0,product(X0,sF4)),
inference(forward_demodulation,[],[f1777,f1]) ).
fof(f1800,plain,
! [X0] : product(sF0,product(product(X0,sF4),x0)) = product(quotient(difference(x0,X0),x0),x0),
inference(superposition,[],[f392,f1782]) ).
fof(f1807,plain,
! [X0] : product(X0,sF4) = product(x0,quotient(difference(x0,X0),x0)),
inference(superposition,[],[f3,f1782]) ).
fof(f1810,plain,
! [X0] : difference(x0,X0) = product(sF0,product(product(X0,sF4),x0)),
inference(forward_demodulation,[],[f1800,f6]) ).
fof(f1830,plain,
! [X0] : product(product(sF4,X0),sF4) = product(x0,quotient(product(sF0,difference(x0,X0)),x0)),
inference(superposition,[],[f1807,f821]) ).
fof(f1832,plain,
! [X0] : product(quotient(X0,x0),sF4) = product(x0,quotient(product(sF0,product(X0,sF0)),x0)),
inference(superposition,[],[f1807,f686]) ).
fof(f1834,plain,
product(x0,quotient(sF4,x0)) = product(sF1,sF4),
inference(superposition,[],[f1807,f42]) ).
fof(f1837,plain,
! [X0] : product(x0,quotient(X0,x0)) = product(product(x0,X0),sF4),
inference(superposition,[],[f1807,f4]) ).
fof(f1841,plain,
! [X0] : difference(sF0,difference(x0,X0)) = product(product(X0,sF4),x0),
inference(superposition,[],[f440,f1807]) ).
fof(f1853,plain,
! [X0,X1] : quotient(difference(X1,product(quotient(difference(x0,X0),x0),x0)),x0) = difference(product(x0,X1),product(X0,sF4)),
inference(superposition,[],[f123,f1807]) ).
fof(f1854,plain,
! [X0,X1] : difference(product(x0,X1),product(X0,sF4)) = quotient(difference(X1,difference(x0,X0)),x0),
inference(forward_demodulation,[],[f1853,f6]) ).
fof(f1857,plain,
! [X0] : product(product(X0,x0),sF0) = product(product(X0,sF4),x0),
inference(backward_demodulation,[],[f899,f1841]) ).
fof(f1865,plain,
sF0 = product(sF1,sF4),
inference(forward_demodulation,[],[f1834,f563]) ).
fof(f1867,plain,
! [X0] : product(quotient(X0,x0),sF4) = product(x0,product(sF0,product(product(X0,sF0),sF0))),
inference(forward_demodulation,[],[f1832,f666]) ).
fof(f1868,plain,
! [X0] : product(product(sF4,X0),sF4) = product(x0,product(sF0,product(difference(x0,X0),sF0))),
inference(forward_demodulation,[],[f1830,f666]) ).
fof(f1873,plain,
! [X0] : difference(sF5,product(sF4,X0)) = quotient(quotient(difference(x0,difference(x0,X0)),x0),sF4),
inference(backward_demodulation,[],[f1075,f1854]) ).
fof(f1886,plain,
! [X0] : difference(sF4,X0) = product(x0,product(product(X0,sF4),x0)),
inference(backward_demodulation,[],[f1127,f1857]) ).
fof(f1891,plain,
! [X0] : difference(x0,X0) = product(product(product(sF4,X0),sF4),x0),
inference(backward_demodulation,[],[f1179,f1857]) ).
fof(f1903,plain,
! [X0] : product(quotient(X0,x0),sF4) = product(sF4,product(x0,product(product(X0,sF0),sF0))),
inference(forward_demodulation,[],[f1867,f949]) ).
fof(f1904,plain,
! [X0] : product(product(sF4,X0),sF4) = product(sF4,product(x0,product(difference(x0,X0),sF0))),
inference(forward_demodulation,[],[f1868,f949]) ).
fof(f1906,plain,
! [X0] : difference(sF5,product(sF4,X0)) = product(sF4,product(x0,difference(x0,difference(x0,X0)))),
inference(forward_demodulation,[],[f1873,f270]) ).
fof(f1920,plain,
! [X0] : product(quotient(X0,x0),sF4) = quotient(product(X0,sF0),x0),
inference(forward_demodulation,[],[f1903,f974]) ).
fof(f1921,plain,
! [X0] : quotient(difference(x0,X0),x0) = product(product(sF4,X0),sF4),
inference(forward_demodulation,[],[f1904,f974]) ).
fof(f1923,plain,
! [X0] : difference(sF5,product(sF4,X0)) = product(sF4,difference(x0,X0)),
inference(forward_demodulation,[],[f1906,f3]) ).
fof(f1930,plain,
! [X0] : difference(x0,product(X0,sF4)) = product(product(sF4,X0),sF4),
inference(backward_demodulation,[],[f1782,f1921]) ).
fof(f1936,plain,
! [X0] : product(X0,sF4) = product(x0,product(product(sF4,X0),sF4)),
inference(backward_demodulation,[],[f1807,f1921]) ).
fof(f1954,plain,
! [X0] : product(x0,product(X0,x0)) = difference(sF4,quotient(X0,sF4)),
inference(superposition,[],[f1886,f6]) ).
fof(f1957,plain,
difference(sF4,sF0) = product(x0,product(sF0,quotient(sF4,sF0))),
inference(superposition,[],[f1886,f675]) ).
fof(f1964,plain,
! [X0] : difference(x0,difference(sF4,X0)) = product(product(X0,sF4),x0),
inference(superposition,[],[f4,f1886]) ).
fof(f1976,plain,
difference(sF4,sF0) = product(sF4,product(x0,quotient(sF4,sF0))),
inference(forward_demodulation,[],[f1957,f949]) ).
fof(f1988,plain,
sF4 = difference(sF1,sF0),
inference(superposition,[],[f4,f1865]) ).
fof(f1989,plain,
sF1 = quotient(sF0,sF4),
inference(superposition,[],[f5,f1865]) ).
fof(f1996,plain,
difference(sF4,sF0) = quotient(sF4,sF0),
inference(backward_demodulation,[],[f1483,f1988]) ).
fof(f1998,plain,
quotient(sF4,sF0) = product(sF4,product(x0,quotient(sF4,sF0))),
inference(backward_demodulation,[],[f1976,f1996]) ).
fof(f2059,plain,
! [X0] : quotient(product(X0,product(sF4,x0)),x0) = product(product(sF4,product(x0,X0)),sF4),
inference(superposition,[],[f7,f1930]) ).
fof(f2065,plain,
! [X0] : quotient(product(X0,one),x0) = product(product(sF4,product(x0,X0)),sF4),
inference(forward_demodulation,[],[f2059,f129]) ).
fof(f2077,plain,
! [X0] : quotient(X0,x0) = product(product(sF4,product(x0,X0)),sF4),
inference(forward_demodulation,[],[f2065,f1]) ).
fof(f2092,plain,
! [X0] : product(x0,product(X0,sF4)) = product(difference(sF4,X0),sF4),
inference(superposition,[],[f1936,f3]) ).
fof(f2132,plain,
! [X0] : product(sF4,product(x0,product(X0,x0))) = quotient(X0,sF4),
inference(superposition,[],[f3,f1954]) ).
fof(f2134,plain,
! [X0] : product(x0,product(X0,x0)) = quotient(product(x0,X0),sF4),
inference(backward_demodulation,[],[f1035,f2132]) ).
fof(f2136,plain,
product(x0,x0) = quotient(x0,sF4),
inference(backward_demodulation,[],[f1088,f2132]) ).
fof(f2332,plain,
! [X0] : product(X0,sF0) = product(product(quotient(X0,x0),sF4),x0),
inference(superposition,[],[f1857,f6]) ).
fof(f2362,plain,
! [X0] : difference(sF5,product(x0,X0)) = product(sF4,difference(x0,product(x0,difference(sF0,X0)))),
inference(superposition,[],[f1923,f1040]) ).
fof(f2366,plain,
difference(sF5,sF1) = product(sF4,difference(x0,sF5)),
inference(superposition,[],[f1923,f271]) ).
fof(f2367,plain,
! [X0] : difference(sF5,X0) = product(sF4,difference(x0,difference(sF4,X0))),
inference(superposition,[],[f1923,f3]) ).
fof(f2380,plain,
! [X0] : difference(sF5,X0) = product(sF4,product(product(X0,sF4),x0)),
inference(forward_demodulation,[],[f2367,f1964]) ).
fof(f2381,plain,
difference(sF5,sF1) = product(sF4,sF1),
inference(forward_demodulation,[],[f2366,f754]) ).
fof(f2385,plain,
! [X0] : difference(sF5,product(x0,X0)) = product(sF4,difference(sF0,X0)),
inference(forward_demodulation,[],[f2362,f4]) ).
fof(f2400,plain,
! [X0] : difference(sF5,product(sF1,X0)) = quotient(product(product(sF4,sF1),product(X0,sF5)),sF5),
inference(superposition,[],[f101,f2381]) ).
fof(f2409,plain,
! [X0] : product(sF4,product(X0,x0)) = difference(sF5,quotient(X0,sF4)),
inference(superposition,[],[f2380,f6]) ).
fof(f2410,plain,
difference(sF5,x0) = product(sF4,product(sF1,x0)),
inference(superposition,[],[f2380,f38]) ).
fof(f2417,plain,
! [X0] : product(product(X0,sF4),x0) = difference(sF4,difference(sF5,X0)),
inference(superposition,[],[f4,f2380]) ).
fof(f2510,plain,
product(x0,product(sF1,x0)) = quotient(sF5,sF4),
inference(superposition,[],[f2134,f745]) ).
fof(f2530,plain,
difference(sF4,x0) = quotient(sF5,sF4),
inference(backward_demodulation,[],[f1126,f2510]) ).
fof(f2539,plain,
difference(sF1,x0) = quotient(quotient(sF5,sF4),x0),
inference(backward_demodulation,[],[f1476,f2530]) ).
fof(f2621,plain,
! [X0] : product(x0,product(sF2,quotient(X0,sF3))) = product(sF3,quotient(quotient(X0,sF2),x0)),
inference(superposition,[],[f1255,f25]) ).
fof(f2646,plain,
! [X2,X0,X1] : product(X1,product(X2,quotient(product(X0,X2),product(X1,X2)))) = product(product(X1,X2),quotient(X0,X1)),
inference(superposition,[],[f1255,f5]) ).
fof(f2673,plain,
! [X2,X0,X1] : quotient(product(X1,product(quotient(quotient(X2,X1),X0),X0)),X0) = difference(X0,product(X0,product(X1,quotient(X2,product(X0,X1))))),
inference(superposition,[],[f7,f1255]) ).
fof(f2683,plain,
! [X2,X0,X1] : product(X1,quotient(X2,product(X0,X1))) = quotient(product(X1,product(quotient(quotient(X2,X1),X0),X0)),X0),
inference(forward_demodulation,[],[f2673,f4]) ).
fof(f2709,plain,
! [X2,X0,X1] : product(X1,quotient(X2,product(X0,X1))) = quotient(product(X1,quotient(X2,X1)),X0),
inference(forward_demodulation,[],[f2683,f6]) ).
fof(f2715,plain,
! [X0] : difference(X0,one) = product(X0,quotient(one,product(X0,X0))),
inference(backward_demodulation,[],[f60,f2709]) ).
fof(f2724,plain,
! [X0,X1] : product(X0,quotient(X0,product(X1,X0))) = quotient(product(X0,one),X1),
inference(superposition,[],[f2709,f84]) ).
fof(f2726,plain,
! [X0] : product(x0,quotient(one,product(X0,x0))) = quotient(product(x0,sF4),X0),
inference(superposition,[],[f2709,f27]) ).
fof(f2727,plain,
! [X0] : product(sF4,quotient(one,product(X0,sF4))) = quotient(product(sF4,sF5),X0),
inference(superposition,[],[f2709,f29]) ).
fof(f2728,plain,
! [X2,X0,X1] : quotient(product(X1,X0),X2) = product(X1,quotient(product(X0,X1),product(X2,X1))),
inference(superposition,[],[f2709,f5]) ).
fof(f2763,plain,
! [X2,X0,X1] : product(X0,quotient(X1,X0)) = product(product(X0,quotient(X1,product(X2,X0))),X2),
inference(superposition,[],[f6,f2709]) ).
fof(f2803,plain,
! [X2,X0,X1] : product(product(X1,X2),quotient(X0,X1)) = product(X1,quotient(product(X2,X0),X1)),
inference(backward_demodulation,[],[f2646,f2728]) ).
fof(f2804,plain,
! [X0] : product(sF4,quotient(one,product(X0,sF4))) = quotient(sF1,X0),
inference(forward_demodulation,[],[f2727,f271]) ).
fof(f2805,plain,
! [X0] : product(x0,quotient(one,product(X0,x0))) = quotient(sF1,X0),
inference(forward_demodulation,[],[f2726,f38]) ).
fof(f2807,plain,
! [X0,X1] : quotient(X0,X1) = product(X0,quotient(X0,product(X1,X0))),
inference(forward_demodulation,[],[f2724,f1]) ).
fof(f2902,plain,
quotient(sF1,sF0) = product(x0,quotient(one,sF1)),
inference(superposition,[],[f2805,f21]) ).
fof(f2908,plain,
! [X0] : product(x0,difference(sF0,quotient(one,product(X0,x0)))) = difference(sF4,quotient(sF1,X0)),
inference(superposition,[],[f1100,f2805]) ).
fof(f2922,plain,
product(sF1,x0) = product(x0,quotient(one,sF1)),
inference(forward_demodulation,[],[f2902,f544]) ).
fof(f2975,plain,
! [X0,X1] : quotient(X1,quotient(X0,X1)) = product(X1,quotient(X1,X0)),
inference(superposition,[],[f2807,f6]) ).
fof(f2999,plain,
quotient(sF5,sF4) = product(sF5,quotient(sF5,sF1)),
inference(superposition,[],[f2807,f271]) ).
fof(f3003,plain,
! [X0,X1] : difference(X0,quotient(X0,X1)) = quotient(X0,product(X1,X0)),
inference(superposition,[],[f4,f2807]) ).
fof(f3032,plain,
product(sF5,x0) = quotient(sF5,sF4),
inference(forward_demodulation,[],[f2999,f753]) ).
fof(f3058,plain,
quotient(product(sF5,x0),x0) = difference(sF1,x0),
inference(backward_demodulation,[],[f2539,f3032]) ).
fof(f3069,plain,
sF5 = difference(sF1,x0),
inference(forward_demodulation,[],[f3058,f5]) ).
fof(f3072,plain,
quotient(sF5,x0) = difference(sF5,x0),
inference(backward_demodulation,[],[f1478,f3069]) ).
fof(f3073,plain,
quotient(sF5,x0) = product(sF4,product(sF1,x0)),
inference(backward_demodulation,[],[f2410,f3072]) ).
fof(f3149,plain,
sF1 = quotient(x0,sF5),
inference(superposition,[],[f59,f3069]) ).
fof(f3164,plain,
! [X0] : difference(X0,one) = quotient(X0,product(X0,X0)),
inference(superposition,[],[f3003,f84]) ).
fof(f3373,plain,
! [X0] : quotient(one,product(X0,sF4)) = difference(sF4,quotient(sF1,X0)),
inference(superposition,[],[f4,f2804]) ).
fof(f3380,plain,
! [X0] : quotient(one,product(X0,sF4)) = product(x0,difference(sF0,quotient(one,product(X0,x0)))),
inference(backward_demodulation,[],[f2908,f3373]) ).
fof(f3403,plain,
! [X2,X0,X1] : product(X1,quotient(product(difference(X1,X0),X2),X1)) = product(X0,quotient(X2,X1)),
inference(superposition,[],[f2803,f3]) ).
fof(f3423,plain,
! [X0] : product(x0,quotient(product(sF2,X0),x0)) = product(sF3,quotient(X0,x0)),
inference(superposition,[],[f2803,f25]) ).
fof(f3424,plain,
! [X0] : product(x0,quotient(product(sF4,X0),x0)) = product(sF1,quotient(X0,x0)),
inference(superposition,[],[f2803,f38]) ).
fof(f3425,plain,
! [X0] : product(sF0,quotient(product(x0,X0),sF0)) = product(sF1,quotient(X0,sF0)),
inference(superposition,[],[f2803,f21]) ).
fof(f3430,plain,
! [X0] : product(sF4,quotient(X0,sF0)) = product(sF0,quotient(product(sF1,X0),sF0)),
inference(superposition,[],[f2803,f554]) ).
fof(f3450,plain,
! [X0] : product(sF4,quotient(product(X0,one),sF4)) = product(product(sF4,X0),sF5),
inference(superposition,[],[f2803,f29]) ).
fof(f3465,plain,
! [X0] : product(sF4,quotient(product(X0,sF0),sF4)) = product(product(sF4,X0),sF1),
inference(superposition,[],[f2803,f1989]) ).
fof(f3474,plain,
! [X0] : product(sF1,quotient(product(X0,sF5),sF1)) = product(product(sF1,X0),x0),
inference(superposition,[],[f2803,f753]) ).
fof(f3494,plain,
! [X0] : product(sF4,quotient(X0,sF4)) = product(product(sF4,X0),sF5),
inference(forward_demodulation,[],[f3450,f1]) ).
fof(f3558,plain,
product(x0,difference(sF0,quotient(one,product(x0,x0)))) = difference(sF4,difference(x0,one)),
inference(superposition,[],[f1100,f2715]) ).
fof(f3579,plain,
difference(sF4,sF0) = product(x0,difference(sF0,quotient(one,product(x0,x0)))),
inference(forward_demodulation,[],[f3558,f19]) ).
fof(f3602,plain,
difference(sF4,sF0) = quotient(one,product(x0,sF4)),
inference(forward_demodulation,[],[f3579,f3380]) ).
fof(f3616,plain,
difference(sF4,sF0) = quotient(one,sF1),
inference(forward_demodulation,[],[f3602,f38]) ).
fof(f3623,plain,
quotient(sF4,sF0) = quotient(one,sF1),
inference(forward_demodulation,[],[f3616,f1996]) ).
fof(f3630,plain,
product(sF1,x0) = product(x0,quotient(sF4,sF0)),
inference(backward_demodulation,[],[f2922,f3623]) ).
fof(f3634,plain,
quotient(sF4,sF0) = product(sF4,product(sF1,x0)),
inference(backward_demodulation,[],[f1998,f3630]) ).
fof(f3638,plain,
quotient(sF4,sF0) = quotient(sF5,x0),
inference(backward_demodulation,[],[f3073,f3634]) ).
fof(f3641,plain,
difference(sF1,one) = quotient(sF4,sF0),
inference(backward_demodulation,[],[f1749,f3638]) ).
fof(f3650,plain,
quotient(sF4,sF0) = difference(sF5,x0),
inference(backward_demodulation,[],[f3072,f3638]) ).
fof(f3686,plain,
! [X0] : product(x0,quotient(product(X0,sF5),x0)) = product(product(x0,X0),quotient(sF4,sF0)),
inference(superposition,[],[f2803,f3638]) ).
fof(f3766,plain,
! [X2,X0,X1] : quotient(product(X1,X2),quotient(X0,X1)) = product(X1,quotient(product(X2,X1),X0)),
inference(superposition,[],[f2728,f6]) ).
fof(f3795,plain,
! [X2,X0,X1] : quotient(product(X1,X0),product(X2,X0)) = difference(X0,quotient(product(X0,X1),X2)),
inference(superposition,[],[f4,f2728]) ).
fof(f3891,plain,
! [X2,X0,X1] : product(X1,quotient(product(difference(X1,X0),X1),X2)) = quotient(X0,quotient(X2,X1)),
inference(superposition,[],[f3766,f3]) ).
fof(f3910,plain,
! [X0,X1] : product(x0,quotient(product(product(product(sF4,X0),sF4),x0),X1)) = quotient(product(X0,sF4),quotient(X1,x0)),
inference(superposition,[],[f3766,f1936]) ).
fof(f3939,plain,
! [X0] : product(sF4,quotient(product(X0,sF4),one)) = quotient(product(sF4,X0),sF5),
inference(superposition,[],[f3766,f29]) ).
fof(f3940,plain,
! [X0] : product(sF1,quotient(product(X0,sF1),one)) = quotient(product(sF1,X0),quotient(sF4,sF0)),
inference(superposition,[],[f3766,f3623]) ).
fof(f3988,plain,
! [X0] : quotient(product(sF1,X0),quotient(sF4,sF0)) = product(sF1,product(X0,sF1)),
inference(forward_demodulation,[],[f3940,f70]) ).
fof(f3989,plain,
! [X0] : product(sF4,product(X0,sF4)) = quotient(product(sF4,X0),sF5),
inference(forward_demodulation,[],[f3939,f70]) ).
fof(f4006,plain,
! [X0,X1] : quotient(product(X0,sF4),quotient(X1,x0)) = product(x0,quotient(difference(x0,X0),X1)),
inference(forward_demodulation,[],[f3910,f1891]) ).
fof(f4476,plain,
! [X0] : quotient(product(X0,x0),product(x0,x0)) = product(sF0,product(product(x0,X0),sF0)),
inference(superposition,[],[f686,f3795]) ).
fof(f4485,plain,
! [X0] : quotient(product(X0,sF4),product(sF4,sF4)) = product(x0,product(product(sF4,X0),x0)),
inference(superposition,[],[f1954,f3795]) ).
fof(f4487,plain,
! [X0] : quotient(product(X0,sF5),product(sF4,sF5)) = product(sF4,product(product(sF5,X0),x0)),
inference(superposition,[],[f2409,f3795]) ).
fof(f4488,plain,
! [X0] : quotient(product(X0,sF5),sF1) = product(sF4,product(product(sF5,X0),x0)),
inference(forward_demodulation,[],[f4487,f271]) ).
fof(f4489,plain,
! [X0] : quotient(product(X0,sF4),product(sF0,sF0)) = product(x0,product(product(sF4,X0),x0)),
inference(forward_demodulation,[],[f4485,f999]) ).
fof(f4538,plain,
! [X0] : product(x0,product(product(sF4,quotient(X0,x0)),x0)) = quotient(product(x0,product(product(sF4,X0),x0)),x0),
inference(backward_demodulation,[],[f1184,f4489]) ).
fof(f4885,plain,
! [X0] : product(sF4,product(difference(sF4,X0),sF4)) = quotient(X0,sF5),
inference(superposition,[],[f3989,f3]) ).
fof(f4912,plain,
! [X0] : product(sF4,product(x0,product(X0,sF4))) = quotient(X0,sF5),
inference(forward_demodulation,[],[f4885,f2092]) ).
fof(f5622,plain,
product(sF5,sF5) = product(sF4,quotient(product(x0,x0),sF4)),
inference(superposition,[],[f3494,f1062]) ).
fof(f5633,plain,
! [X0] : product(X0,sF5) = product(sF4,quotient(difference(sF4,X0),sF4)),
inference(superposition,[],[f3494,f3]) ).
fof(f5670,plain,
product(sF4,product(x0,product(x0,x0))) = product(sF5,sF5),
inference(forward_demodulation,[],[f5622,f2134]) ).
fof(f5685,plain,
quotient(x0,sF4) = product(sF5,sF5),
inference(forward_demodulation,[],[f5670,f2132]) ).
fof(f5692,plain,
product(x0,x0) = product(sF5,sF5),
inference(backward_demodulation,[],[f2136,f5685]) ).
fof(f5700,plain,
difference(sF4,sF5) = product(sF5,sF5),
inference(backward_demodulation,[],[f1078,f5692]) ).
fof(f5722,plain,
! [X0] : product(sF0,product(product(x0,X0),sF0)) = quotient(product(X0,x0),product(sF5,sF5)),
inference(backward_demodulation,[],[f4476,f5692]) ).
fof(f5753,plain,
sF4 = difference(product(sF5,sF5),x0),
inference(superposition,[],[f135,f5685]) ).
fof(f5800,plain,
difference(x0,one) = quotient(x0,product(sF5,sF5)),
inference(superposition,[],[f3164,f5692]) ).
fof(f5803,plain,
! [X0] : quotient(product(x0,product(X0,x0)),x0) = difference(x0,product(product(sF5,sF5),X0)),
inference(superposition,[],[f7,f5692]) ).
fof(f5818,plain,
sF0 = quotient(x0,product(sF5,sF5)),
inference(forward_demodulation,[],[f5800,f19]) ).
fof(f6011,plain,
! [X0,X1] : quotient(quotient(X0,sF4),quotient(X1,sF4)) = product(sF4,quotient(product(product(x0,product(X0,x0)),sF4),X1)),
inference(superposition,[],[f3891,f1954]) ).
fof(f6030,plain,
! [X0,X1] : product(X0,product(difference(X0,X1),X0)) = quotient(X1,quotient(one,X0)),
inference(superposition,[],[f3891,f70]) ).
fof(f6039,plain,
! [X2,X0,X1] : quotient(product(difference(X2,X0),X2),X1) = difference(X2,quotient(X0,quotient(X1,X2))),
inference(superposition,[],[f4,f3891]) ).
fof(f6110,plain,
! [X0,X1] : quotient(quotient(X0,sF4),quotient(X1,sF4)) = product(sF4,quotient(product(x0,quotient(product(X0,x0),x0)),X1)),
inference(forward_demodulation,[],[f6011,f1837]) ).
fof(f6153,plain,
! [X0,X1] : product(sF4,product(x0,quotient(product(X0,x0),product(X1,x0)))) = quotient(quotient(X0,sF4),quotient(X1,sF4)),
inference(forward_demodulation,[],[f6110,f2709]) ).
fof(f6175,plain,
! [X0,X1] : product(sF4,quotient(product(x0,X0),X1)) = quotient(quotient(X0,sF4),quotient(X1,sF4)),
inference(forward_demodulation,[],[f6153,f2728]) ).
fof(f6289,plain,
! [X0] : difference(x0,quotient(X0,sF4)) = quotient(product(difference(x0,X0),x0),one),
inference(superposition,[],[f6039,f27]) ).
fof(f6291,plain,
! [X0] : quotient(product(difference(sF4,X0),sF4),one) = difference(sF4,quotient(X0,sF5)),
inference(superposition,[],[f6039,f29]) ).
fof(f6415,plain,
! [X0] : product(difference(sF4,X0),sF4) = difference(sF4,quotient(X0,sF5)),
inference(forward_demodulation,[],[f6291,f70]) ).
fof(f6417,plain,
! [X0] : product(difference(x0,X0),x0) = difference(x0,quotient(X0,sF4)),
inference(forward_demodulation,[],[f6289,f70]) ).
fof(f6450,plain,
! [X0] : product(x0,product(X0,sF4)) = difference(sF4,quotient(X0,sF5)),
inference(forward_demodulation,[],[f6415,f2092]) ).
fof(f6451,plain,
! [X0] : product(sF0,product(X0,x0)) = difference(x0,quotient(X0,sF4)),
inference(forward_demodulation,[],[f6417,f392]) ).
fof(f6542,plain,
! [X0] : difference(sF4,X0) = product(x0,product(product(X0,sF5),sF4)),
inference(superposition,[],[f6450,f5]) ).
fof(f6546,plain,
! [X0] : product(x0,product(quotient(X0,difference(sF5,one)),sF4)) = difference(sF4,product(sF5,product(difference(sF5,one),X0))),
inference(superposition,[],[f6450,f289]) ).
fof(f6581,plain,
! [X0] : product(x0,product(quotient(X0,sF4),sF4)) = difference(sF4,product(sF5,product(sF4,X0))),
inference(forward_demodulation,[],[f6546,f335]) ).
fof(f6601,plain,
! [X0] : product(x0,X0) = difference(sF4,product(sF5,product(sF4,X0))),
inference(forward_demodulation,[],[f6581,f6]) ).
fof(f6629,plain,
! [X0] : difference(sF4,product(sF5,X0)) = product(x0,difference(sF4,X0)),
inference(superposition,[],[f6601,f3]) ).
fof(f6635,plain,
! [X0] : product(sF4,product(x0,X0)) = product(sF5,product(sF4,X0)),
inference(superposition,[],[f3,f6601]) ).
fof(f6715,plain,
product(x0,difference(sF4,x1)) = difference(sF4,sF6),
inference(superposition,[],[f6629,f31]) ).
fof(f6725,plain,
! [X0] : product(sF5,X0) = product(sF4,product(x0,difference(sF4,X0))),
inference(superposition,[],[f3,f6629]) ).
fof(f6832,plain,
! [X0] : quotient(difference(sF4,X0),sF4) = product(x0,product(product(product(X0,sF5),sF4),x0)),
inference(superposition,[],[f2134,f6542]) ).
fof(f6833,plain,
! [X0] : difference(x0,difference(sF4,X0)) = product(product(X0,sF5),sF4),
inference(superposition,[],[f4,f6542]) ).
fof(f6846,plain,
! [X0] : product(product(X0,sF4),x0) = product(product(X0,sF5),sF4),
inference(forward_demodulation,[],[f6833,f1964]) ).
fof(f6847,plain,
! [X0] : quotient(difference(sF4,X0),sF4) = difference(sF4,product(X0,sF5)),
inference(forward_demodulation,[],[f6832,f1886]) ).
fof(f6919,plain,
product(sF4,product(x0,quotient(sF4,sF0))) = product(sF5,sF0),
inference(superposition,[],[f6725,f1996]) ).
fof(f6930,plain,
! [X0] : product(product(sF5,X0),x0) = quotient(difference(sF4,X0),sF0),
inference(superposition,[],[f971,f6725]) ).
fof(f6932,plain,
! [X0] : product(sF4,quotient(product(x0,difference(sF4,X0)),sF4)) = product(product(sF5,X0),sF5),
inference(superposition,[],[f3494,f6725]) ).
fof(f6936,plain,
! [X0] : difference(x0,product(sF5,X0)) = product(sF0,difference(x0,product(x0,difference(sF4,X0)))),
inference(superposition,[],[f821,f6725]) ).
fof(f6958,plain,
! [X0] : difference(x0,product(sF5,X0)) = product(sF0,difference(sF4,X0)),
inference(forward_demodulation,[],[f6936,f4]) ).
fof(f6962,plain,
! [X0] : product(sF4,product(x0,product(difference(sF4,X0),x0))) = product(product(sF5,X0),sF5),
inference(forward_demodulation,[],[f6932,f2134]) ).
fof(f6966,plain,
product(sF4,product(sF1,x0)) = product(sF5,sF0),
inference(forward_demodulation,[],[f6919,f3630]) ).
fof(f6981,plain,
! [X0] : quotient(difference(sF4,X0),sF4) = product(product(sF5,X0),sF5),
inference(forward_demodulation,[],[f6962,f2132]) ).
fof(f6984,plain,
quotient(sF4,sF0) = product(sF5,sF0),
inference(backward_demodulation,[],[f3634,f6966]) ).
fof(f6990,plain,
! [X0] : difference(sF4,product(X0,sF5)) = product(product(sF5,X0),sF5),
inference(backward_demodulation,[],[f6847,f6981]) ).
fof(f6991,plain,
! [X0] : product(X0,sF5) = product(sF4,product(product(sF5,X0),sF5)),
inference(backward_demodulation,[],[f5633,f6981]) ).
fof(f6999,plain,
quotient(one,sF1) = product(sF5,sF0),
inference(backward_demodulation,[],[f3623,f6984]) ).
fof(f7002,plain,
quotient(sF5,x0) = product(sF5,sF0),
inference(backward_demodulation,[],[f3638,f6984]) ).
fof(f7003,plain,
difference(sF1,one) = product(sF5,sF0),
inference(backward_demodulation,[],[f3641,f6984]) ).
fof(f7008,plain,
difference(sF5,x0) = product(sF5,sF0),
inference(backward_demodulation,[],[f3650,f6984]) ).
fof(f7020,plain,
! [X0] : product(x0,quotient(product(X0,sF5),x0)) = product(product(x0,X0),product(sF5,sF0)),
inference(backward_demodulation,[],[f3686,f6984]) ).
fof(f7027,plain,
! [X0] : product(sF1,product(X0,sF1)) = quotient(product(sF1,X0),product(sF5,sF0)),
inference(backward_demodulation,[],[f3988,f6984]) ).
fof(f7197,plain,
! [X0] : difference(x0,product(sF5,product(product(sF5,sF0),X0))) = quotient(quotient(product(X0,x0),product(sF5,sF0)),sF5),
inference(superposition,[],[f46,f7008]) ).
fof(f7207,plain,
! [X0] : product(sF0,difference(sF4,product(product(sF5,sF0),X0))) = quotient(quotient(product(X0,x0),product(sF5,sF0)),sF5),
inference(forward_demodulation,[],[f7197,f6958]) ).
fof(f7218,plain,
! [X0] : product(difference(sF5,X0),sF5) = product(sF4,product(X0,sF5)),
inference(superposition,[],[f6991,f3]) ).
fof(f9358,plain,
product(sF4,difference(sF0,sF2)) = difference(sF5,sF3),
inference(superposition,[],[f2385,f25]) ).
fof(f9534,plain,
! [X0] : difference(x0,product(sF0,X0)) = quotient(quotient(product(difference(product(sF5,sF5),X0),x0),product(sF5,sF5)),sF0),
inference(superposition,[],[f374,f5818]) ).
fof(f9601,plain,
! [X0] : difference(x0,product(sF0,X0)) = quotient(product(sF0,product(product(x0,difference(product(sF5,sF5),X0)),sF0)),sF0),
inference(forward_demodulation,[],[f9534,f5722]) ).
fof(f9671,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(product(sF4,quotient(product(x0,difference(product(sF5,sF5),X0)),x0)),x0),
inference(forward_demodulation,[],[f9601,f1168]) ).
fof(f10180,plain,
difference(sF4,x1) = difference(x0,difference(sF4,sF6)),
inference(superposition,[],[f4,f6715]) ).
fof(f10193,plain,
difference(sF4,x1) = product(product(sF6,sF4),x0),
inference(forward_demodulation,[],[f10180,f1964]) ).
fof(f11008,plain,
product(sF0,difference(sF4,x1)) = difference(x0,sF6),
inference(superposition,[],[f6958,f31]) ).
fof(f11192,plain,
! [X0] : product(sF4,difference(x0,product(difference(sF4,X0),sF4))) = difference(sF5,quotient(X0,quotient(one,sF4))),
inference(superposition,[],[f1923,f6030]) ).
fof(f11194,plain,
! [X0] : product(sF0,difference(x0,product(difference(sF4,X0),sF4))) = difference(x0,quotient(X0,quotient(one,sF4))),
inference(superposition,[],[f821,f6030]) ).
fof(f11201,plain,
! [X0] : product(sF0,difference(x0,product(difference(sF4,X0),sF4))) = difference(x0,quotient(X0,sF5)),
inference(forward_demodulation,[],[f11194,f29]) ).
fof(f11203,plain,
! [X0] : product(sF4,difference(x0,product(difference(sF4,X0),sF4))) = difference(sF5,quotient(X0,sF5)),
inference(forward_demodulation,[],[f11192,f29]) ).
fof(f11297,plain,
! [X0] : difference(x0,quotient(X0,sF5)) = product(sF0,product(product(sF4,difference(sF4,X0)),sF4)),
inference(forward_demodulation,[],[f11201,f1930]) ).
fof(f11299,plain,
! [X0] : difference(sF5,quotient(X0,sF5)) = product(sF4,product(product(sF4,difference(sF4,X0)),sF4)),
inference(forward_demodulation,[],[f11203,f1930]) ).
fof(f11374,plain,
! [X0] : product(sF0,product(X0,sF4)) = difference(x0,quotient(X0,sF5)),
inference(forward_demodulation,[],[f11297,f3]) ).
fof(f11376,plain,
! [X0] : product(sF4,product(X0,sF4)) = difference(sF5,quotient(X0,sF5)),
inference(forward_demodulation,[],[f11299,f3]) ).
fof(f11865,plain,
! [X0] : product(product(x0,sF4),product(X0,sF4)) = product(x0,quotient(difference(sF5,X0),x0)),
inference(superposition,[],[f113,f2380]) ).
fof(f11915,plain,
! [X0,X1] : product(x0,product(quotient(product(X0,product(X1,x0)),x0),x0)) = quotient(product(product(x0,X0),X1),sF4),
inference(superposition,[],[f2134,f113]) ).
fof(f11923,plain,
! [X0,X1] : quotient(product(product(sF4,X0),X1),sF5) = product(sF4,product(quotient(product(X0,product(X1,sF4)),sF4),sF4)),
inference(superposition,[],[f3989,f113]) ).
fof(f11936,plain,
! [X0,X1] : quotient(product(product(sF4,X0),X1),sF5) = product(sF4,product(X0,product(X1,sF4))),
inference(forward_demodulation,[],[f11923,f6]) ).
fof(f11941,plain,
! [X0,X1] : quotient(product(product(x0,X0),X1),sF4) = product(x0,product(X0,product(X1,x0))),
inference(forward_demodulation,[],[f11915,f6]) ).
fof(f11980,plain,
! [X0] : product(sF1,product(X0,sF4)) = product(x0,quotient(difference(sF5,X0),x0)),
inference(forward_demodulation,[],[f11865,f38]) ).
fof(f12017,plain,
! [X0] : difference(sF5,product(sF1,X0)) = product(sF4,product(sF1,product(product(X0,sF5),sF4))),
inference(backward_demodulation,[],[f2400,f11936]) ).
fof(f12039,plain,
! [X0] : difference(sF4,quotient(X0,sF0)) = product(x0,product(X0,product(sF1,x0))),
inference(backward_demodulation,[],[f1154,f11941]) ).
fof(f12086,plain,
! [X0] : difference(sF5,product(sF1,X0)) = product(sF4,product(sF1,product(product(X0,sF4),x0))),
inference(forward_demodulation,[],[f12017,f6846]) ).
fof(f12236,plain,
! [X0] : product(x0,quotient(X0,x0)) = product(sF1,product(product(sF5,X0),sF4)),
inference(superposition,[],[f11980,f4]) ).
fof(f12254,plain,
! [X0] : quotient(product(sF1,product(X0,sF4)),sF4) = product(x0,product(quotient(difference(sF5,X0),x0),x0)),
inference(superposition,[],[f2134,f11980]) ).
fof(f12278,plain,
! [X0] : quotient(product(sF1,product(X0,sF4)),sF4) = product(x0,difference(sF5,X0)),
inference(forward_demodulation,[],[f12254,f6]) ).
fof(f12325,plain,
product(x0,quotient(x1,x0)) = product(sF1,product(sF6,sF4)),
inference(superposition,[],[f12236,f31]) ).
fof(f12341,plain,
! [X0] : product(product(sF5,X0),sF4) = difference(sF1,product(x0,quotient(X0,x0))),
inference(superposition,[],[f4,f12236]) ).
fof(f12362,plain,
! [X0] : product(product(sF5,X0),sF4) = quotient(difference(difference(x0,sF1),X0),x0),
inference(forward_demodulation,[],[f12341,f1350]) ).
fof(f12374,plain,
! [X0] : product(product(sF5,X0),sF4) = quotient(difference(sF4,X0),x0),
inference(forward_demodulation,[],[f12362,f42]) ).
fof(f12423,plain,
! [X0] : quotient(product(x0,product(X0,x0)),x0) = product(product(sF5,quotient(X0,sF4)),sF4),
inference(superposition,[],[f12374,f1954]) ).
fof(f12476,plain,
! [X0] : difference(x0,product(product(sF5,sF5),X0)) = product(product(sF5,quotient(X0,sF4)),sF4),
inference(backward_demodulation,[],[f5803,f12423]) ).
fof(f12478,plain,
! [X0] : product(x0,product(product(sF4,quotient(X0,x0)),x0)) = product(product(sF5,quotient(product(sF4,X0),sF4)),sF4),
inference(backward_demodulation,[],[f4538,f12423]) ).
fof(f14031,plain,
! [X0] : difference(x0,product(x0,product(X0,sF4))) = product(product(quotient(X0,sF5),sF4),x0),
inference(superposition,[],[f1964,f6450]) ).
fof(f14081,plain,
! [X0] : product(X0,sF4) = product(product(quotient(X0,sF5),sF4),x0),
inference(forward_demodulation,[],[f14031,f4]) ).
fof(f14691,plain,
! [X0] : difference(sF4,X0) = product(product(sF5,quotient(X0,sF5)),sF5),
inference(superposition,[],[f6990,f6]) ).
fof(f15369,plain,
! [X0] : quotient(product(X0,sF5),product(sF5,sF5)) = product(sF4,product(product(sF5,X0),sF4)),
inference(superposition,[],[f3795,f11376]) ).
fof(f18454,plain,
difference(sF0,sF2) = difference(sF4,difference(sF5,sF3)),
inference(superposition,[],[f4,f9358]) ).
fof(f18474,plain,
difference(sF0,sF2) = product(product(sF3,sF4),x0),
inference(forward_demodulation,[],[f18454,f2417]) ).
fof(f19013,plain,
! [X0] : product(one,quotient(X0,sF1)) = product(sF1,quotient(product(product(sF5,sF0),X0),sF1)),
inference(superposition,[],[f3403,f7003]) ).
fof(f19050,plain,
! [X0,X1] : product(X1,quotient(one,X0)) = product(X0,quotient(difference(X0,X1),X0)),
inference(superposition,[],[f3403,f1]) ).
fof(f19053,plain,
! [X2,X0,X1] : product(X1,quotient(X0,X1)) = product(X2,quotient(difference(difference(X1,X2),X0),X1)),
inference(superposition,[],[f3403,f3]) ).
fof(f19094,plain,
! [X0,X1] : difference(sF0,product(difference(x0,X0),X1)) = product(product(X0,quotient(X1,x0)),x0),
inference(superposition,[],[f440,f3403]) ).
fof(f19172,plain,
! [X0] : quotient(X0,sF1) = product(sF1,quotient(product(product(sF5,sF0),X0),sF1)),
inference(forward_demodulation,[],[f19013,f2]) ).
fof(f19291,plain,
! [X0] : product(quotient(X0,sF5),quotient(one,x0)) = product(x0,quotient(product(sF0,product(X0,sF4)),x0)),
inference(superposition,[],[f19050,f11374]) ).
fof(f19327,plain,
! [X0] : product(quotient(X0,sF4),quotient(one,sF4)) = product(sF4,quotient(product(x0,product(X0,x0)),sF4)),
inference(superposition,[],[f19050,f1954]) ).
fof(f19462,plain,
! [X0] : product(quotient(X0,sF4),quotient(one,sF4)) = product(sF4,product(x0,product(product(X0,x0),x0))),
inference(forward_demodulation,[],[f19327,f2134]) ).
fof(f19498,plain,
! [X0] : product(quotient(X0,sF5),quotient(one,x0)) = product(x0,product(sF0,product(product(X0,sF4),sF0))),
inference(forward_demodulation,[],[f19291,f666]) ).
fof(f19564,plain,
! [X0] : quotient(product(X0,x0),sF4) = product(quotient(X0,sF4),quotient(one,sF4)),
inference(forward_demodulation,[],[f19462,f2132]) ).
fof(f19599,plain,
! [X0] : product(quotient(X0,sF5),quotient(one,x0)) = product(sF4,product(x0,product(product(X0,sF4),sF0))),
inference(forward_demodulation,[],[f19498,f949]) ).
fof(f19638,plain,
! [X0] : quotient(product(X0,x0),sF4) = product(quotient(X0,sF4),sF5),
inference(forward_demodulation,[],[f19564,f29]) ).
fof(f19660,plain,
! [X0] : quotient(product(X0,sF4),x0) = product(quotient(X0,sF5),quotient(one,x0)),
inference(forward_demodulation,[],[f19599,f974]) ).
fof(f19711,plain,
! [X0] : quotient(product(X0,sF4),x0) = product(quotient(X0,sF5),sF4),
inference(forward_demodulation,[],[f19660,f27]) ).
fof(f21345,plain,
! [X0] : product(product(x0,product(sF4,product(X0,sF0))),x0) = difference(sF0,difference(sF1,product(sF0,X0))),
inference(superposition,[],[f433,f1158]) ).
fof(f21352,plain,
! [X0] : product(sF4,product(X0,sF0)) = quotient(difference(sF1,product(sF0,X0)),x0),
inference(superposition,[],[f5,f1158]) ).
fof(f22477,plain,
! [X0] : quotient(product(sF0,X0),sF4) = product(sF4,product(x0,product(sF0,quotient(X0,sF0)))),
inference(superposition,[],[f2132,f675]) ).
fof(f22495,plain,
! [X0] : quotient(difference(x0,X0),sF4) = product(sF4,quotient(X0,quotient(one,x0))),
inference(superposition,[],[f2132,f6030]) ).
fof(f22551,plain,
! [X0] : product(sF4,quotient(X0,sF4)) = quotient(difference(x0,X0),sF4),
inference(forward_demodulation,[],[f22495,f27]) ).
fof(f22566,plain,
! [X0] : quotient(product(sF0,X0),sF4) = product(sF4,product(sF4,product(x0,quotient(X0,sF0)))),
inference(forward_demodulation,[],[f22477,f949]) ).
fof(f22733,plain,
! [X0] : quotient(product(sF0,product(X0,sF4)),sF4) = product(sF4,quotient(quotient(X0,sF5),sF4)),
inference(superposition,[],[f22551,f11374]) ).
fof(f22985,plain,
! [X0,X1] : difference(sF4,product(difference(sF5,X0),X1)) = product(product(X0,quotient(X1,sF5)),sF5),
inference(superposition,[],[f14691,f3403]) ).
fof(f23080,plain,
! [X2,X0,X1] : product(difference(X1,X0),X1) = product(difference(X1,X2),product(difference(X2,X0),X1)),
inference(superposition,[],[f369,f3]) ).
fof(f23126,plain,
! [X2,X0,X1] : product(difference(X1,X0),X1) = product(difference(X1,quotient(X0,X2)),product(X2,X1)),
inference(superposition,[],[f369,f6]) ).
fof(f23692,plain,
! [X0] : product(difference(x0,X0),x0) = product(sF4,product(difference(sF1,X0),x0)),
inference(superposition,[],[f23080,f42]) ).
fof(f23694,plain,
! [X0] : product(difference(x0,X0),x0) = product(sF1,product(difference(sF5,X0),x0)),
inference(superposition,[],[f23080,f754]) ).
fof(f23741,plain,
! [X0] : product(difference(sF5,X0),sF5) = product(product(sF5,sF0),product(difference(x0,X0),sF5)),
inference(superposition,[],[f23080,f7008]) ).
fof(f23966,plain,
! [X0] : product(sF4,product(X0,sF5)) = product(product(sF5,sF0),product(difference(x0,X0),sF5)),
inference(forward_demodulation,[],[f23741,f7218]) ).
fof(f23992,plain,
! [X0] : product(sF0,product(X0,x0)) = product(sF1,product(difference(sF5,X0),x0)),
inference(forward_demodulation,[],[f23694,f392]) ).
fof(f23994,plain,
! [X0] : product(sF0,product(X0,x0)) = product(sF4,product(difference(sF1,X0),x0)),
inference(forward_demodulation,[],[f23692,f392]) ).
fof(f24251,plain,
! [X0] : product(sF4,product(X0,x0)) = product(sF0,product(product(sF1,X0),x0)),
inference(superposition,[],[f23994,f4]) ).
fof(f24378,plain,
! [X0] : product(x0,product(sF4,product(X0,x0))) = product(sF4,product(x0,product(product(sF1,X0),x0))),
inference(superposition,[],[f949,f24251]) ).
fof(f24412,plain,
! [X0] : product(x0,product(sF4,product(X0,x0))) = quotient(product(sF1,X0),sF4),
inference(forward_demodulation,[],[f24378,f2132]) ).
fof(f24490,plain,
! [X0] : product(sF1,product(X0,x0)) = product(sF0,product(product(sF5,X0),x0)),
inference(superposition,[],[f23992,f4]) ).
fof(f24564,plain,
! [X0] : product(sF0,product(product(sF4,product(x0,X0)),x0)) = product(sF1,product(product(sF4,X0),x0)),
inference(superposition,[],[f24490,f6635]) ).
fof(f24568,plain,
product(sF0,product(sF6,x0)) = product(sF1,product(x1,x0)),
inference(superposition,[],[f24490,f31]) ).
fof(f24588,plain,
! [X0] : product(sF4,product(x0,product(product(sF5,X0),x0))) = product(x0,product(sF1,product(X0,x0))),
inference(superposition,[],[f949,f24490]) ).
fof(f24622,plain,
! [X0] : quotient(product(sF5,X0),sF4) = product(x0,product(sF1,product(X0,x0))),
inference(forward_demodulation,[],[f24588,f2132]) ).
fof(f24639,plain,
! [X0] : product(sF0,quotient(X0,sF0)) = product(sF1,product(product(sF4,X0),x0)),
inference(forward_demodulation,[],[f24564,f971]) ).
fof(f25509,plain,
! [X0] : product(difference(sF4,X0),sF4) = product(difference(sF4,quotient(X0,x0)),sF1),
inference(superposition,[],[f23126,f38]) ).
fof(f25522,plain,
! [X0] : product(difference(x0,X0),x0) = product(difference(x0,quotient(X0,sF0)),sF1),
inference(superposition,[],[f23126,f21]) ).
fof(f25640,plain,
! [X0] : product(sF0,product(X0,x0)) = product(difference(x0,quotient(X0,sF0)),sF1),
inference(forward_demodulation,[],[f25522,f392]) ).
fof(f25646,plain,
! [X0] : product(x0,product(X0,sF4)) = product(difference(sF4,quotient(X0,x0)),sF1),
inference(forward_demodulation,[],[f25509,f2092]) ).
fof(f26133,plain,
! [X0] : product(difference(sF4,X0),sF1) = product(x0,product(product(X0,x0),sF4)),
inference(superposition,[],[f25646,f5]) ).
fof(f28716,plain,
! [X0] : difference(sF0,product(sF4,X0)) = product(product(sF1,quotient(X0,x0)),x0),
inference(superposition,[],[f440,f3424]) ).
fof(f29047,plain,
! [X0] : difference(X0,product(sF1,product(sF6,sF4))) = quotient(difference(difference(x0,X0),x1),x0),
inference(superposition,[],[f1350,f12325]) ).
fof(f29108,plain,
! [X0] : product(sF4,difference(x0,quotient(X0,sF4))) = quotient(difference(difference(sF4,sF5),X0),sF4),
inference(superposition,[],[f1923,f1350]) ).
fof(f29114,plain,
! [X0] : product(sF4,difference(x0,quotient(X0,sF4))) = quotient(difference(product(sF5,sF5),X0),sF4),
inference(forward_demodulation,[],[f29108,f5700]) ).
fof(f29264,plain,
! [X0] : product(sF4,product(sF0,product(X0,x0))) = quotient(difference(product(sF5,sF5),X0),sF4),
inference(forward_demodulation,[],[f29114,f6451]) ).
fof(f31453,plain,
! [X0] : product(difference(sF4,product(sF4,product(X0,sF0))),sF1) = product(x0,product(difference(sF1,product(sF0,X0)),sF4)),
inference(superposition,[],[f26133,f1158]) ).
fof(f31535,plain,
! [X0] : product(product(X0,sF0),sF1) = product(x0,product(difference(sF1,product(sF0,X0)),sF4)),
inference(forward_demodulation,[],[f31453,f4]) ).
fof(f34278,plain,
! [X0] : product(sF4,difference(x0,product(x0,product(X0,sF0)))) = difference(sF5,quotient(X0,x0)),
inference(superposition,[],[f1923,f974]) ).
fof(f34282,plain,
! [X0] : product(quotient(X0,x0),sF5) = product(sF4,quotient(product(x0,product(X0,sF0)),sF4)),
inference(superposition,[],[f3494,f974]) ).
fof(f34287,plain,
! [X0] : product(x0,product(X0,sF0)) = difference(sF4,quotient(X0,x0)),
inference(superposition,[],[f4,f974]) ).
fof(f34349,plain,
! [X0] : product(quotient(X0,x0),sF5) = product(sF4,product(x0,product(product(X0,sF0),x0))),
inference(forward_demodulation,[],[f34282,f2134]) ).
fof(f34352,plain,
! [X0] : product(sF4,product(X0,sF0)) = difference(sF5,quotient(X0,x0)),
inference(forward_demodulation,[],[f34278,f4]) ).
fof(f34384,plain,
! [X0] : quotient(product(X0,sF0),sF4) = product(quotient(X0,x0),sF5),
inference(forward_demodulation,[],[f34349,f2132]) ).
fof(f34402,plain,
! [X0] : product(product(sF4,X0),sF1) = product(sF4,product(quotient(X0,x0),sF5)),
inference(backward_demodulation,[],[f3465,f34384]) ).
fof(f34566,plain,
! [X0] : quotient(product(X0,sF4),product(x0,sF4)) = product(x0,product(product(sF4,X0),sF0)),
inference(superposition,[],[f3795,f34287]) ).
fof(f34597,plain,
! [X0] : quotient(product(X0,sF4),sF1) = product(x0,product(product(sF4,X0),sF0)),
inference(forward_demodulation,[],[f34566,f38]) ).
fof(f34701,plain,
! [X0] : product(sF4,product(difference(sF4,X0),sF0)) = difference(sF5,product(product(sF5,X0),sF4)),
inference(superposition,[],[f34352,f12374]) ).
fof(f34767,plain,
! [X0] : quotient(product(X0,product(sF4,sF5)),sF5) = product(sF4,product(difference(sF4,X0),sF0)),
inference(forward_demodulation,[],[f34701,f7]) ).
fof(f34789,plain,
! [X0] : quotient(product(X0,sF1),sF5) = product(sF4,product(difference(sF4,X0),sF0)),
inference(forward_demodulation,[],[f34767,f271]) ).
fof(f37264,plain,
! [X0] : quotient(X0,product(sF1,x0)) = product(product(sF0,product(product(sF1,x0),X0)),sF0),
inference(superposition,[],[f311,f492]) ).
fof(f37274,plain,
! [X0,X1] : quotient(product(difference(difference(X1,one),X0),difference(X1,one)),difference(X1,one)) = product(product(X1,quotient(X0,quotient(one,difference(X1,one)))),X1),
inference(superposition,[],[f311,f6030]) ).
fof(f37407,plain,
! [X0,X1] : product(product(X1,quotient(X0,X1)),X1) = quotient(product(difference(difference(X1,one),X0),difference(X1,one)),difference(X1,one)),
inference(forward_demodulation,[],[f37274,f59]) ).
fof(f37457,plain,
! [X0,X1] : difference(difference(X1,one),X0) = product(product(X1,quotient(X0,X1)),X1),
inference(forward_demodulation,[],[f37407,f5]) ).
fof(f37496,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF0,difference(difference(sF0,one),X0)),
inference(backward_demodulation,[],[f684,f37457]) ).
fof(f37523,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF0,difference(product(sF1,x0),X0)),
inference(forward_demodulation,[],[f37496,f492]) ).
fof(f45276,plain,
! [X0] : quotient(product(X0,x0),sF5) = product(sF4,product(difference(sF4,X0),sF1)),
inference(superposition,[],[f4912,f26133]) ).
fof(f50115,plain,
! [X0] : difference(x0,product(product(sF5,sF5),product(sF4,X0))) = quotient(quotient(product(X0,x0),sF4),product(sF5,sF5)),
inference(superposition,[],[f46,f5753]) ).
fof(f50152,plain,
! [X0] : difference(x0,product(product(sF5,sF5),product(sF4,X0))) = quotient(product(quotient(X0,sF4),sF5),product(sF5,sF5)),
inference(forward_demodulation,[],[f50115,f19638]) ).
fof(f50167,plain,
! [X0] : product(sF4,product(product(sF5,quotient(X0,sF4)),sF4)) = difference(x0,product(product(sF5,sF5),product(sF4,X0))),
inference(forward_demodulation,[],[f50152,f15369]) ).
fof(f50177,plain,
! [X0] : product(sF4,product(product(sF5,quotient(X0,sF4)),sF4)) = product(product(sF5,quotient(product(sF4,X0),sF4)),sF4),
inference(forward_demodulation,[],[f50167,f12476]) ).
fof(f50183,plain,
! [X0] : product(x0,product(product(sF4,quotient(X0,x0)),x0)) = product(sF4,product(product(sF5,quotient(X0,sF4)),sF4)),
inference(backward_demodulation,[],[f12478,f50177]) ).
fof(f50550,plain,
! [X0] : product(sF0,X0) = difference(x0,product(sF0,product(product(sF1,x0),X0))),
inference(superposition,[],[f37523,f4]) ).
fof(f50669,plain,
! [X0] : product(x0,product(sF0,X0)) = product(sF0,product(product(sF1,x0),X0)),
inference(superposition,[],[f3,f50550]) ).
fof(f50697,plain,
! [X0] : product(sF4,product(x0,X0)) = product(sF0,product(product(sF1,x0),X0)),
inference(forward_demodulation,[],[f50669,f949]) ).
fof(f50731,plain,
! [X0] : quotient(X0,product(sF1,x0)) = product(product(sF4,product(x0,X0)),sF0),
inference(backward_demodulation,[],[f37264,f50697]) ).
fof(f50886,plain,
! [X0] : product(quotient(X0,sF4),sF0) = quotient(product(X0,x0),product(sF1,x0)),
inference(superposition,[],[f50731,f2132]) ).
fof(f53432,plain,
! [X2,X0,X1] : product(quotient(X1,X0),quotient(X2,quotient(X1,X0))) = product(X1,quotient(difference(X0,X2),quotient(X1,X0))),
inference(superposition,[],[f19053,f135]) ).
fof(f54273,plain,
! [X0] : difference(sF4,product(X0,x0)) = product(difference(sF1,product(x0,X0)),x0),
inference(superposition,[],[f1371,f42]) ).
fof(f58879,plain,
! [X0,X1] : difference(X1,product(sF0,product(X0,x0))) = product(difference(product(x0,X1),X0),x0),
inference(superposition,[],[f1645,f392]) ).
fof(f59569,plain,
! [X0] : difference(sF0,product(quotient(sF0,x0),X0)) = quotient(product(quotient(difference(x0,X0),x0),sF4),quotient(sF0,x0)),
inference(superposition,[],[f374,f1920]) ).
fof(f59616,plain,
! [X0] : difference(sF0,product(quotient(sF0,x0),X0)) = product(x0,quotient(difference(x0,quotient(difference(x0,X0),x0)),sF0)),
inference(forward_demodulation,[],[f59569,f4006]) ).
fof(f59641,plain,
! [X0] : difference(sF0,product(quotient(sF0,x0),X0)) = product(x0,product(product(sF4,quotient(difference(x0,X0),x0)),x0)),
inference(forward_demodulation,[],[f59616,f1139]) ).
fof(f59657,plain,
! [X0] : difference(sF0,product(quotient(sF0,x0),X0)) = product(sF4,product(product(sF5,quotient(difference(x0,X0),sF4)),sF4)),
inference(forward_demodulation,[],[f59641,f50183]) ).
fof(f59666,plain,
! [X0] : difference(sF0,product(quotient(sF0,x0),X0)) = product(sF4,product(product(sF5,product(sF4,quotient(X0,sF4))),sF4)),
inference(forward_demodulation,[],[f59657,f22551]) ).
fof(f59672,plain,
! [X0] : difference(sF0,product(quotient(sF0,x0),X0)) = product(sF4,product(product(sF4,product(x0,quotient(X0,sF4))),sF4)),
inference(forward_demodulation,[],[f59666,f6635]) ).
fof(f59680,plain,
! [X0] : difference(sF0,product(quotient(sF0,x0),X0)) = product(sF4,quotient(quotient(X0,sF4),x0)),
inference(forward_demodulation,[],[f59672,f2077]) ).
fof(f59684,plain,
! [X0] : difference(sF0,product(product(sF0,sF0),X0)) = product(sF4,quotient(quotient(X0,sF4),x0)),
inference(forward_demodulation,[],[f59680,f724]) ).
fof(f59686,plain,
! [X0] : quotient(product(sF0,product(X0,sF0)),sF0) = product(sF4,quotient(quotient(X0,sF4),x0)),
inference(forward_demodulation,[],[f59684,f7]) ).
fof(f59688,plain,
! [X0] : product(product(sF4,quotient(X0,x0)),x0) = product(sF4,quotient(quotient(X0,sF4),x0)),
inference(backward_demodulation,[],[f1168,f59686]) ).
fof(f59693,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,quotient(quotient(product(x0,difference(product(sF5,sF5),X0)),sF4),x0)),
inference(backward_demodulation,[],[f9671,f59688]) ).
fof(f59694,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,quotient(product(x0,product(difference(product(sF5,sF5),X0),x0)),x0)),
inference(forward_demodulation,[],[f59693,f2134]) ).
fof(f59696,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,product(product(sF5,quotient(difference(product(sF5,sF5),X0),sF4)),sF4)),
inference(forward_demodulation,[],[f59694,f12423]) ).
fof(f59698,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,product(product(sF5,product(sF4,product(sF0,product(X0,x0)))),sF4)),
inference(forward_demodulation,[],[f59696,f29264]) ).
fof(f59699,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,product(product(sF4,product(x0,product(sF0,product(X0,x0)))),sF4)),
inference(forward_demodulation,[],[f59698,f6635]) ).
fof(f59700,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,quotient(product(sF0,product(X0,x0)),x0)),
inference(forward_demodulation,[],[f59699,f2077]) ).
fof(f59701,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,product(sF0,product(product(X0,x0),sF0))),
inference(forward_demodulation,[],[f59700,f666]) ).
fof(f59702,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,product(sF0,product(product(X0,sF4),x0))),
inference(forward_demodulation,[],[f59701,f1857]) ).
fof(f59703,plain,
! [X0] : difference(x0,product(sF0,X0)) = product(sF4,difference(x0,X0)),
inference(forward_demodulation,[],[f59702,f1810]) ).
fof(f59788,plain,
! [X0] : difference(x0,X0) = product(sF4,difference(x0,difference(sF0,X0))),
inference(superposition,[],[f59703,f3]) ).
fof(f59816,plain,
! [X0] : product(sF0,X0) = product(x0,product(sF4,difference(x0,X0))),
inference(superposition,[],[f3,f59703]) ).
fof(f59834,plain,
! [X0] : product(x0,quotient(product(sF4,difference(x0,X0)),x0)) = product(product(sF0,X0),quotient(one,x0)),
inference(superposition,[],[f19050,f59703]) ).
fof(f59840,plain,
! [X0] : product(product(sF0,X0),sF4) = product(x0,quotient(product(sF4,difference(x0,X0)),x0)),
inference(forward_demodulation,[],[f59834,f27]) ).
fof(f59883,plain,
! [X0] : product(product(sF0,X0),sF4) = product(sF1,quotient(difference(x0,X0),x0)),
inference(forward_demodulation,[],[f59840,f3424]) ).
fof(f59920,plain,
! [X0] : product(product(sF0,X0),sF4) = product(sF1,product(product(sF4,X0),sF4)),
inference(forward_demodulation,[],[f59883,f1921]) ).
fof(f60010,plain,
! [X0] : product(sF4,product(x0,difference(x0,difference(sF0,X0)))) = product(sF5,difference(x0,X0)),
inference(superposition,[],[f6635,f59788]) ).
fof(f60080,plain,
! [X0] : product(sF4,difference(sF0,X0)) = product(sF5,difference(x0,X0)),
inference(forward_demodulation,[],[f60010,f3]) ).
fof(f60224,plain,
! [X0] : product(sF0,difference(sF4,X0)) = product(x0,product(sF4,product(product(X0,sF4),x0))),
inference(superposition,[],[f59816,f1964]) ).
fof(f60241,plain,
! [X0] : product(x0,product(sF4,X0)) = product(sF0,product(x0,X0)),
inference(superposition,[],[f59816,f4]) ).
fof(f60258,plain,
! [X0] : difference(sF4,product(sF0,X0)) = product(x0,difference(sF0,product(sF4,difference(x0,X0)))),
inference(superposition,[],[f1100,f59816]) ).
fof(f60326,plain,
! [X0] : quotient(quotient(product(X0,sF1),sF4),x0) = difference(sF1,product(sF0,product(x0,X0))),
inference(backward_demodulation,[],[f40,f60241]) ).
fof(f60366,plain,
! [X0] : quotient(product(sF1,X0),sF4) = product(sF0,product(x0,product(X0,x0))),
inference(backward_demodulation,[],[f24412,f60241]) ).
fof(f60367,plain,
! [X0] : difference(sF0,difference(sF1,product(sF0,X0))) = product(product(sF0,product(x0,product(X0,sF0))),x0),
inference(backward_demodulation,[],[f21345,f60241]) ).
fof(f60439,plain,
! [X0] : product(sF0,difference(sF4,X0)) = product(sF0,product(x0,product(product(X0,sF4),x0))),
inference(forward_demodulation,[],[f60224,f60241]) ).
fof(f60513,plain,
! [X0] : difference(sF0,difference(sF1,product(sF0,X0))) = product(sF0,quotient(product(x0,product(X0,sF0)),sF0)),
inference(forward_demodulation,[],[f60367,f675]) ).
fof(f60518,plain,
! [X0] : quotient(quotient(product(X0,sF1),sF4),x0) = quotient(quotient(product(X0,sF1),x0),sF0),
inference(backward_demodulation,[],[f49,f60326]) ).
fof(f60526,plain,
! [X0] : product(sF0,difference(sF4,X0)) = quotient(product(sF1,product(X0,sF4)),sF4),
inference(forward_demodulation,[],[f60439,f60366]) ).
fof(f60548,plain,
! [X0] : difference(sF0,difference(sF1,product(sF0,X0))) = product(sF1,quotient(product(X0,sF0),sF0)),
inference(forward_demodulation,[],[f60513,f3425]) ).
fof(f60553,plain,
! [X0] : product(sF0,difference(sF4,X0)) = product(x0,difference(sF5,X0)),
inference(backward_demodulation,[],[f12278,f60526]) ).
fof(f60567,plain,
! [X0] : product(sF1,X0) = difference(sF0,difference(sF1,product(sF0,X0))),
inference(forward_demodulation,[],[f60548,f5]) ).
fof(f60616,plain,
! [X0] : product(x0,X0) = product(sF0,product(x0,difference(sF4,X0))),
inference(superposition,[],[f60241,f3]) ).
fof(f60649,plain,
! [X0] : product(product(X0,x0),sF4) = product(X0,quotient(product(sF0,product(x0,X0)),X0)),
inference(superposition,[],[f113,f60241]) ).
fof(f60685,plain,
! [X0] : product(product(X0,x0),sF4) = product(product(X0,sF0),x0),
inference(forward_demodulation,[],[f60649,f113]) ).
fof(f60741,plain,
! [X0] : product(difference(sF4,X0),sF1) = product(x0,product(product(X0,sF0),x0)),
inference(backward_demodulation,[],[f26133,f60685]) ).
fof(f60927,plain,
! [X0] : difference(sF0,product(x0,X0)) = product(x0,difference(sF4,X0)),
inference(superposition,[],[f4,f60616]) ).
fof(f61133,plain,
product(x0,difference(sF4,sF2)) = difference(sF0,sF3),
inference(superposition,[],[f60927,f25]) ).
fof(f61581,plain,
! [X0] : quotient(product(X0,sF0),sF4) = product(sF4,product(difference(sF4,X0),sF1)),
inference(superposition,[],[f2132,f60741]) ).
fof(f61644,plain,
! [X0] : product(quotient(X0,x0),sF5) = product(sF4,product(difference(sF4,X0),sF1)),
inference(forward_demodulation,[],[f61581,f34384]) ).
fof(f61676,plain,
! [X0] : quotient(product(X0,x0),sF5) = product(quotient(X0,x0),sF5),
inference(backward_demodulation,[],[f45276,f61644]) ).
fof(f62205,plain,
! [X0] : difference(sF0,difference(sF1,X0)) = product(sF1,difference(sF0,X0)),
inference(superposition,[],[f60567,f3]) ).
fof(f62228,plain,
! [X0] : difference(sF1,product(sF0,X0)) = product(sF0,product(sF1,X0)),
inference(superposition,[],[f3,f60567]) ).
fof(f62265,plain,
! [X0] : product(sF4,product(X0,sF0)) = quotient(product(sF0,product(sF1,X0)),x0),
inference(backward_demodulation,[],[f21352,f62228]) ).
fof(f62282,plain,
! [X0] : product(product(X0,sF0),sF1) = product(x0,product(product(sF0,product(sF1,X0)),sF4)),
inference(backward_demodulation,[],[f31535,f62228]) ).
fof(f62319,plain,
! [X0] : quotient(quotient(product(X0,sF1),sF4),x0) = product(sF0,product(sF1,product(x0,X0))),
inference(backward_demodulation,[],[f60326,f62228]) ).
fof(f62425,plain,
! [X0] : quotient(quotient(product(X0,sF1),x0),sF0) = product(sF0,product(sF1,product(x0,X0))),
inference(backward_demodulation,[],[f60518,f62319]) ).
fof(f62457,plain,
! [X0] : product(sF4,product(X0,sF0)) = product(sF0,product(product(sF1,X0),sF0)),
inference(forward_demodulation,[],[f62265,f666]) ).
fof(f62535,plain,
! [X0] : product(sF0,product(X0,sF0)) = product(sF4,product(difference(sF1,X0),sF0)),
inference(superposition,[],[f62457,f3]) ).
fof(f62690,plain,
! [X0] : difference(sF0,X0) = product(sF1,difference(sF0,product(sF1,X0))),
inference(superposition,[],[f62205,f4]) ).
fof(f62725,plain,
! [X0] : product(difference(sF1,X0),quotient(one,sF0)) = product(sF0,quotient(product(sF1,difference(sF0,X0)),sF0)),
inference(superposition,[],[f19050,f62205]) ).
fof(f62729,plain,
! [X0] : product(difference(sF1,X0),quotient(one,sF0)) = product(sF4,quotient(difference(sF0,X0),sF0)),
inference(forward_demodulation,[],[f62725,f3430]) ).
fof(f62755,plain,
! [X0] : product(sF4,product(product(x0,X0),x0)) = product(difference(sF1,X0),quotient(one,sF0)),
inference(forward_demodulation,[],[f62729,f1142]) ).
fof(f62773,plain,
! [X0] : product(sF4,product(product(x0,X0),x0)) = product(difference(sF1,X0),x0),
inference(forward_demodulation,[],[f62755,f67]) ).
fof(f63055,plain,
! [X0] : product(x0,quotient(product(difference(sF1,X0),x0),x0)) = product(product(x0,sF4),product(x0,X0)),
inference(superposition,[],[f113,f62773]) ).
fof(f63094,plain,
! [X0] : product(sF1,product(x0,X0)) = product(x0,quotient(product(difference(sF1,X0),x0),x0)),
inference(forward_demodulation,[],[f63055,f38]) ).
fof(f63159,plain,
! [X0] : product(x0,difference(sF1,X0)) = product(sF1,product(x0,X0)),
inference(forward_demodulation,[],[f63094,f5]) ).
fof(f63288,plain,
product(x0,x1) = product(sF1,product(x0,sF2)),
inference(superposition,[],[f63159,f50]) ).
fof(f63292,plain,
! [X0] : product(x0,X0) = product(sF1,product(x0,product(sF1,X0))),
inference(superposition,[],[f63159,f4]) ).
fof(f63378,plain,
product(x0,x1) = product(sF1,sF3),
inference(forward_demodulation,[],[f63288,f25]) ).
fof(f63449,plain,
product(x0,quotient(x1,x0)) = product(product(sF1,sF3),sF4),
inference(superposition,[],[f1837,f63378]) ).
fof(f63457,plain,
product(x0,difference(sF4,x1)) = difference(sF0,product(sF1,sF3)),
inference(superposition,[],[f60927,f63378]) ).
fof(f63491,plain,
difference(sF4,sF6) = difference(sF0,product(sF1,sF3)),
inference(forward_demodulation,[],[f63457,f6715]) ).
fof(f63492,plain,
product(sF1,product(sF6,sF4)) = product(product(sF1,sF3),sF4),
inference(forward_demodulation,[],[f63449,f12325]) ).
fof(f63511,plain,
! [X0] : product(x0,difference(sF0,product(sF1,X0))) = product(sF1,product(x0,difference(sF0,X0))),
inference(superposition,[],[f63292,f62690]) ).
fof(f63543,plain,
! [X0] : difference(sF1,product(x0,X0)) = product(x0,product(sF1,X0)),
inference(superposition,[],[f4,f63292]) ).
fof(f63611,plain,
! [X0] : difference(sF4,product(X0,x0)) = product(product(x0,product(sF1,X0)),x0),
inference(backward_demodulation,[],[f54273,f63543]) ).
fof(f63989,plain,
product(difference(sF0,sF1),product(sF3,sF0)) = product(difference(sF4,sF6),sF0),
inference(superposition,[],[f369,f63491]) ).
fof(f64020,plain,
product(difference(sF4,sF6),sF0) = product(x0,product(sF3,sF0)),
inference(forward_demodulation,[],[f63989,f47]) ).
fof(f64041,plain,
! [X0] : difference(sF1,difference(sF4,X0)) = product(x0,product(sF1,product(product(X0,sF4),x0))),
inference(superposition,[],[f63543,f1886]) ).
fof(f64044,plain,
! [X0] : difference(sF1,product(X0,sF4)) = product(x0,product(sF1,product(product(sF4,X0),sF4))),
inference(superposition,[],[f63543,f1936]) ).
fof(f64082,plain,
! [X0] : difference(sF1,X0) = product(x0,product(sF1,difference(x0,X0))),
inference(superposition,[],[f63543,f3]) ).
fof(f64177,plain,
! [X0] : product(x0,product(product(sF0,X0),sF4)) = difference(sF1,product(X0,sF4)),
inference(forward_demodulation,[],[f64044,f59920]) ).
fof(f64180,plain,
! [X0] : quotient(product(sF5,product(X0,sF4)),sF4) = difference(sF1,difference(sF4,X0)),
inference(forward_demodulation,[],[f64041,f24622]) ).
fof(f64214,plain,
! [X0] : product(product(X0,sF0),sF1) = difference(sF1,product(product(sF1,X0),sF4)),
inference(backward_demodulation,[],[f62282,f64177]) ).
fof(f64215,plain,
! [X0] : difference(sF4,product(sF1,X0)) = difference(sF1,difference(sF4,X0)),
inference(backward_demodulation,[],[f275,f64180]) ).
fof(f64238,plain,
! [X0] : product(product(X0,sF0),sF1) = quotient(product(X0,product(sF4,sF1)),sF1),
inference(forward_demodulation,[],[f64214,f7]) ).
fof(f64559,plain,
! [X0] : difference(sF1,product(sF4,X0)) = product(x0,product(sF1,product(sF0,difference(x0,X0)))),
inference(superposition,[],[f64082,f821]) ).
fof(f64595,plain,
! [X0] : difference(sF4,difference(sF1,X0)) = product(x0,difference(sF0,product(sF1,difference(x0,X0)))),
inference(superposition,[],[f1100,f64082]) ).
fof(f64610,plain,
! [X0] : difference(x0,difference(sF1,X0)) = product(sF1,difference(x0,X0)),
inference(superposition,[],[f4,f64082]) ).
fof(f64653,plain,
! [X0] : difference(sF4,difference(sF1,X0)) = product(sF1,product(x0,difference(sF0,difference(x0,X0)))),
inference(forward_demodulation,[],[f64595,f63511]) ).
fof(f64694,plain,
! [X0] : difference(sF4,difference(sF1,X0)) = product(sF1,product(x0,product(product(X0,sF4),x0))),
inference(forward_demodulation,[],[f64653,f1841]) ).
fof(f64718,plain,
! [X0] : difference(sF4,difference(sF1,X0)) = product(sF1,difference(sF4,X0)),
inference(forward_demodulation,[],[f64694,f1886]) ).
fof(f65006,plain,
! [X0] : product(sF4,quotient(product(difference(sF1,X0),sF0),sF4)) = product(product(sF0,product(X0,sF0)),sF5),
inference(superposition,[],[f3494,f62535]) ).
fof(f65011,plain,
! [X0] : product(sF0,quotient(product(difference(sF1,X0),sF0),sF0)) = product(sF1,product(product(sF0,product(X0,sF0)),x0)),
inference(superposition,[],[f24639,f62535]) ).
fof(f65052,plain,
! [X0] : product(sF0,quotient(product(difference(sF1,X0),sF0),sF0)) = product(sF1,product(sF0,quotient(product(X0,sF0),sF0))),
inference(forward_demodulation,[],[f65011,f675]) ).
fof(f65055,plain,
! [X0] : product(product(sF0,product(X0,sF0)),sF5) = product(sF4,product(quotient(difference(sF1,X0),x0),sF5)),
inference(forward_demodulation,[],[f65006,f34384]) ).
fof(f65083,plain,
! [X0] : product(sF1,product(sF0,X0)) = product(sF0,quotient(product(difference(sF1,X0),sF0),sF0)),
inference(forward_demodulation,[],[f65052,f5]) ).
fof(f65087,plain,
! [X0] : product(product(sF0,product(X0,sF0)),sF5) = product(product(sF4,difference(sF1,X0)),sF1),
inference(forward_demodulation,[],[f65055,f34402]) ).
fof(f65109,plain,
! [X0] : product(sF1,product(sF0,X0)) = product(sF0,difference(sF1,X0)),
inference(forward_demodulation,[],[f65083,f5]) ).
fof(f65127,plain,
! [X0] : difference(sF1,product(sF4,X0)) = product(x0,product(sF0,difference(sF1,difference(x0,X0)))),
inference(backward_demodulation,[],[f64559,f65109]) ).
fof(f65138,plain,
! [X0] : difference(sF1,product(sF4,X0)) = product(sF4,product(x0,difference(sF1,difference(x0,X0)))),
inference(forward_demodulation,[],[f65127,f949]) ).
fof(f65151,plain,
! [X0] : difference(sF1,product(sF4,X0)) = product(sF4,product(sF1,product(x0,difference(x0,X0)))),
inference(forward_demodulation,[],[f65138,f63159]) ).
fof(f65159,plain,
! [X0] : difference(sF1,product(sF4,X0)) = product(sF4,product(sF1,X0)),
inference(forward_demodulation,[],[f65151,f3]) ).
fof(f65259,plain,
! [X0] : product(sF0,difference(sF1,product(difference(sF0,X0),sF0))) = product(sF1,quotient(X0,quotient(one,sF0))),
inference(superposition,[],[f65109,f6030]) ).
fof(f65324,plain,
! [X0] : product(sF1,quotient(X0,x0)) = product(sF0,difference(sF1,product(difference(sF0,X0),sF0))),
inference(forward_demodulation,[],[f65259,f67]) ).
fof(f65354,plain,
! [X0] : product(sF1,quotient(X0,x0)) = product(sF0,product(difference(product(sF0,sF1),X0),sF0)),
inference(forward_demodulation,[],[f65324,f1645]) ).
fof(f65370,plain,
! [X0] : product(sF1,quotient(X0,x0)) = product(sF0,product(difference(sF4,X0),sF0)),
inference(forward_demodulation,[],[f65354,f554]) ).
fof(f65404,plain,
! [X0] : product(sF4,product(sF1,product(product(X0,sF4),x0))) = difference(sF1,difference(sF5,X0)),
inference(superposition,[],[f65159,f2380]) ).
fof(f65439,plain,
! [X0] : difference(sF1,X0) = product(sF4,product(sF1,difference(sF4,X0))),
inference(superposition,[],[f65159,f3]) ).
fof(f65530,plain,
! [X0] : difference(sF5,product(sF1,X0)) = difference(sF1,difference(sF5,X0)),
inference(backward_demodulation,[],[f12086,f65404]) ).
fof(f65804,plain,
! [X0] : difference(x0,X0) = product(sF1,difference(x0,product(sF1,X0))),
inference(superposition,[],[f64610,f4]) ).
fof(f65972,plain,
! [X0] : difference(x0,product(difference(sF1,x0),X0)) = product(sF1,quotient(quotient(product(X0,x0),difference(sF1,x0)),sF1)),
inference(superposition,[],[f65804,f46]) ).
fof(f65982,plain,
! [X0] : difference(x0,product(sF1,X0)) = difference(sF1,difference(x0,X0)),
inference(superposition,[],[f4,f65804]) ).
fof(f66083,plain,
! [X0] : difference(x0,product(sF5,X0)) = product(sF1,quotient(quotient(product(X0,x0),sF5),sF1)),
inference(forward_demodulation,[],[f65972,f3069]) ).
fof(f66141,plain,
! [X0] : difference(x0,product(sF5,X0)) = product(sF1,quotient(product(quotient(X0,x0),sF5),sF1)),
inference(forward_demodulation,[],[f66083,f61676]) ).
fof(f66182,plain,
! [X0] : difference(x0,product(sF5,X0)) = product(product(sF1,quotient(X0,x0)),x0),
inference(forward_demodulation,[],[f66141,f3474]) ).
fof(f66212,plain,
! [X0] : difference(sF0,product(sF4,X0)) = difference(x0,product(sF5,X0)),
inference(forward_demodulation,[],[f66182,f28716]) ).
fof(f66230,plain,
! [X0] : difference(sF0,product(sF4,X0)) = product(sF0,difference(sF4,X0)),
inference(forward_demodulation,[],[f66212,f6958]) ).
fof(f66257,plain,
! [X0] : difference(sF4,product(sF0,X0)) = product(x0,product(sF0,difference(sF4,difference(x0,X0)))),
inference(backward_demodulation,[],[f60258,f66230]) ).
fof(f66276,plain,
! [X0] : difference(sF4,product(sF0,X0)) = product(sF4,product(x0,difference(sF4,difference(x0,X0)))),
inference(forward_demodulation,[],[f66257,f949]) ).
fof(f66289,plain,
! [X0] : difference(sF4,product(sF0,X0)) = product(sF5,difference(x0,X0)),
inference(forward_demodulation,[],[f66276,f6725]) ).
fof(f66299,plain,
! [X0] : difference(sF4,product(sF0,X0)) = product(sF4,difference(sF0,X0)),
inference(forward_demodulation,[],[f66289,f60080]) ).
fof(f66402,plain,
! [X0] : product(x0,product(sF4,X0)) = product(sF4,product(x0,product(sF0,difference(sF4,X0)))),
inference(superposition,[],[f1040,f66230]) ).
fof(f66408,plain,
! [X0] : product(difference(sF0,sF4),product(X0,sF0)) = product(product(sF0,difference(sF4,X0)),sF0),
inference(superposition,[],[f369,f66230]) ).
fof(f66410,plain,
! [X0] : product(sF4,X0) = product(sF0,product(sF0,difference(sF4,X0))),
inference(superposition,[],[f3,f66230]) ).
fof(f66426,plain,
! [X0] : quotient(product(sF4,X0),quotient(one,sF0)) = product(sF0,product(product(sF0,difference(sF4,X0)),sF0)),
inference(superposition,[],[f6030,f66230]) ).
fof(f66435,plain,
! [X0] : quotient(product(sF4,X0),x0) = product(sF0,product(product(sF0,difference(sF4,X0)),sF0)),
inference(forward_demodulation,[],[f66426,f67]) ).
fof(f66441,plain,
! [X0] : product(sF1,product(X0,sF0)) = product(product(sF0,difference(sF4,X0)),sF0),
inference(forward_demodulation,[],[f66408,f553]) ).
fof(f66447,plain,
! [X0] : product(x0,product(sF4,X0)) = product(sF4,product(sF4,product(x0,difference(sF4,X0)))),
inference(forward_demodulation,[],[f66402,f949]) ).
fof(f66500,plain,
! [X0] : quotient(product(sF4,X0),x0) = product(sF0,product(sF1,product(X0,sF0))),
inference(backward_demodulation,[],[f66435,f66441]) ).
fof(f66508,plain,
! [X0] : product(x0,product(sF4,X0)) = product(sF4,product(sF5,X0)),
inference(forward_demodulation,[],[f66447,f6725]) ).
fof(f66558,plain,
! [X0] : product(sF0,product(x0,X0)) = product(sF4,product(sF5,X0)),
inference(forward_demodulation,[],[f66508,f60241]) ).
fof(f67936,plain,
! [X0] : product(sF4,product(sF4,product(x0,X0))) = product(sF0,product(x0,product(sF4,X0))),
inference(superposition,[],[f66558,f6635]) ).
fof(f67943,plain,
product(sF4,sF6) = product(sF0,product(x0,x1)),
inference(superposition,[],[f66558,f31]) ).
fof(f68041,plain,
product(sF4,sF6) = product(sF0,product(sF1,sF3)),
inference(forward_demodulation,[],[f67943,f63378]) ).
fof(f68048,plain,
! [X0] : product(sF4,product(sF4,product(x0,X0))) = product(sF0,product(sF0,product(x0,X0))),
inference(forward_demodulation,[],[f67936,f60241]) ).
fof(f68112,plain,
! [X0] : quotient(product(sF0,X0),sF4) = product(sF0,product(sF0,product(x0,quotient(X0,sF0)))),
inference(backward_demodulation,[],[f22566,f68048]) ).
fof(f68165,plain,
product(sF0,difference(sF1,product(sF1,sF3))) = product(sF1,product(sF4,sF6)),
inference(superposition,[],[f65109,f68041]) ).
fof(f68166,plain,
product(product(sF3,sF0),sF1) = product(sF3,quotient(product(sF4,sF6),sF3)),
inference(superposition,[],[f113,f68041]) ).
fof(f68202,plain,
product(sF0,sF3) = product(sF1,product(sF4,sF6)),
inference(forward_demodulation,[],[f68165,f4]) ).
fof(f68652,plain,
! [X0] : quotient(quotient(X0,x0),sF0) = product(sF0,product(sF1,product(x0,quotient(X0,sF1)))),
inference(superposition,[],[f62425,f6]) ).
fof(f68658,plain,
! [X0] : product(sF0,product(quotient(product(X0,sF1),x0),x0)) = product(difference(x0,product(sF0,product(sF1,product(x0,X0)))),sF1),
inference(superposition,[],[f25640,f62425]) ).
fof(f68692,plain,
! [X0] : product(sF0,product(quotient(product(X0,sF1),x0),x0)) = product(product(sF4,difference(x0,product(sF1,product(x0,X0)))),sF1),
inference(forward_demodulation,[],[f68658,f59703]) ).
fof(f68729,plain,
! [X0] : product(sF0,product(quotient(product(X0,sF1),x0),x0)) = product(product(sF4,difference(sF1,difference(x0,product(x0,X0)))),sF1),
inference(forward_demodulation,[],[f68692,f65982]) ).
fof(f68759,plain,
! [X0] : product(sF0,product(quotient(product(X0,sF1),x0),x0)) = product(product(sF0,product(difference(x0,product(x0,X0)),sF0)),sF5),
inference(forward_demodulation,[],[f68729,f65087]) ).
fof(f68781,plain,
! [X0] : product(product(sF0,product(X0,sF0)),sF5) = product(sF0,product(quotient(product(X0,sF1),x0),x0)),
inference(forward_demodulation,[],[f68759,f4]) ).
fof(f68799,plain,
! [X0] : product(sF0,product(X0,sF1)) = product(product(sF0,product(X0,sF0)),sF5),
inference(forward_demodulation,[],[f68781,f6]) ).
fof(f68862,plain,
! [X0] : product(sF0,product(product(X0,x0),sF1)) = product(product(sF0,product(product(X0,sF4),x0)),sF5),
inference(superposition,[],[f68799,f1857]) ).
fof(f68887,plain,
! [X0] : sF5 = difference(product(sF0,product(X0,sF0)),product(sF0,product(X0,sF1))),
inference(superposition,[],[f4,f68799]) ).
fof(f68928,plain,
! [X0] : sF5 = quotient(difference(product(X0,sF0),product(product(X0,sF1),sF0)),sF0),
inference(forward_demodulation,[],[f68887,f123]) ).
fof(f68949,plain,
! [X0] : product(difference(x0,X0),sF5) = product(sF0,product(product(X0,x0),sF1)),
inference(forward_demodulation,[],[f68862,f1810]) ).
fof(f68957,plain,
! [X0] : sF5 = quotient(quotient(difference(sF0,product(sF1,product(sF0,X0))),X0),sF0),
inference(forward_demodulation,[],[f68928,f1688]) ).
fof(f68975,plain,
! [X0] : sF5 = quotient(quotient(difference(sF0,product(sF0,difference(sF1,X0))),X0),sF0),
inference(forward_demodulation,[],[f68957,f65109]) ).
fof(f68986,plain,
! [X0] : sF5 = quotient(quotient(difference(sF1,X0),X0),sF0),
inference(forward_demodulation,[],[f68975,f4]) ).
fof(f69027,plain,
! [X0] : product(sF5,sF0) = quotient(difference(sF1,X0),X0),
inference(superposition,[],[f6,f68986]) ).
fof(f69154,plain,
! [X0] : difference(sF1,X0) = product(product(sF5,sF0),X0),
inference(superposition,[],[f6,f69027]) ).
fof(f69160,plain,
! [X0] : quotient(X0,product(sF5,sF0)) = product(X0,quotient(X0,difference(sF1,X0))),
inference(superposition,[],[f2975,f69027]) ).
fof(f69245,plain,
! [X0] : product(X0,sF1) = quotient(X0,product(sF5,sF0)),
inference(forward_demodulation,[],[f69160,f59]) ).
fof(f69254,plain,
! [X0] : quotient(quotient(product(X0,x0),product(sF5,sF0)),sF5) = product(sF0,difference(sF4,difference(sF1,X0))),
inference(backward_demodulation,[],[f7207,f69154]) ).
fof(f69277,plain,
! [X0] : quotient(X0,sF1) = product(sF1,quotient(difference(sF1,X0),sF1)),
inference(backward_demodulation,[],[f19172,f69154]) ).
fof(f69362,plain,
! [X0] : product(sF4,product(X0,sF5)) = difference(sF1,product(difference(x0,X0),sF5)),
inference(backward_demodulation,[],[f23966,f69154]) ).
fof(f69592,plain,
! [X0] : product(sF1,product(X0,sF1)) = product(product(sF1,X0),sF1),
inference(backward_demodulation,[],[f7027,f69245]) ).
fof(f69750,plain,
! [X0] : quotient(X0,sF1) = product(X0,quotient(one,sF1)),
inference(forward_demodulation,[],[f69277,f19050]) ).
fof(f69769,plain,
! [X0] : quotient(quotient(product(X0,x0),product(sF5,sF0)),sF5) = product(sF0,product(sF1,difference(sF4,X0))),
inference(forward_demodulation,[],[f69254,f64718]) ).
fof(f69950,plain,
! [X0] : quotient(X0,sF1) = product(X0,product(sF5,sF0)),
inference(forward_demodulation,[],[f69750,f6999]) ).
fof(f69957,plain,
! [X0] : quotient(product(product(X0,x0),sF1),sF5) = product(sF0,product(sF1,difference(sF4,X0))),
inference(forward_demodulation,[],[f69769,f69245]) ).
fof(f70118,plain,
! [X0] : product(x0,quotient(product(X0,sF5),x0)) = quotient(product(x0,X0),sF1),
inference(backward_demodulation,[],[f7020,f69950]) ).
fof(f71024,plain,
! [X0] : product(product(sF0,product(X0,x0)),sF1) = product(sF1,product(product(difference(sF5,X0),x0),sF1)),
inference(superposition,[],[f69592,f23992]) ).
fof(f72525,plain,
! [X0] : quotient(product(sF0,product(X0,sF5)),sF5) = difference(sF5,difference(sF1,X0)),
inference(superposition,[],[f7,f69154]) ).
fof(f74174,plain,
difference(sF1,difference(sF4,product(sF4,sF6))) = difference(sF4,product(sF0,sF3)),
inference(superposition,[],[f64215,f68202]) ).
fof(f74214,plain,
difference(sF1,difference(sF4,product(sF4,sF6))) = product(sF4,difference(sF0,sF3)),
inference(forward_demodulation,[],[f74174,f66299]) ).
fof(f74225,plain,
difference(sF1,sF6) = product(sF4,difference(sF0,sF3)),
inference(forward_demodulation,[],[f74214,f4]) ).
fof(f76981,plain,
product(sF5,sF2) = product(sF4,difference(sF0,sF3)),
inference(superposition,[],[f6725,f61133]) ).
fof(f77051,plain,
difference(sF1,sF6) = product(sF5,sF2),
inference(backward_demodulation,[],[f74225,f76981]) ).
fof(f77121,plain,
sF6 = product(sF1,product(sF5,sF2)),
inference(superposition,[],[f3,f77051]) ).
fof(f77175,plain,
product(product(sF2,sF1),sF5) = product(sF2,quotient(sF6,sF2)),
inference(superposition,[],[f113,f77121]) ).
fof(f77841,plain,
! [X0] : product(sF1,difference(sF0,product(difference(x0,X0),sF5))) = difference(sF0,product(sF4,product(X0,sF5))),
inference(superposition,[],[f62205,f69362]) ).
fof(f77884,plain,
! [X0] : product(sF0,difference(sF4,product(X0,sF5))) = product(sF1,difference(sF0,product(difference(x0,X0),sF5))),
inference(forward_demodulation,[],[f77841,f66230]) ).
fof(f77916,plain,
! [X0] : product(sF0,difference(sF4,product(X0,sF5))) = product(sF1,product(product(X0,quotient(sF5,x0)),x0)),
inference(forward_demodulation,[],[f77884,f19094]) ).
fof(f77944,plain,
! [X0] : product(sF0,difference(sF4,product(X0,sF5))) = product(sF1,product(product(X0,product(sF5,sF0)),x0)),
inference(forward_demodulation,[],[f77916,f7002]) ).
fof(f77959,plain,
! [X0] : product(sF0,difference(sF4,product(X0,sF5))) = product(sF1,product(quotient(X0,sF1),x0)),
inference(forward_demodulation,[],[f77944,f69950]) ).
fof(f77968,plain,
! [X0] : product(sF0,product(product(sF5,X0),sF5)) = product(sF1,product(quotient(X0,sF1),x0)),
inference(forward_demodulation,[],[f77959,f6990]) ).
fof(f79354,plain,
! [X0] : quotient(product(x0,product(sF0,product(X0,sF0))),sF1) = product(x0,quotient(product(sF0,product(X0,sF1)),x0)),
inference(superposition,[],[f70118,f68799]) ).
fof(f79404,plain,
! [X0] : quotient(product(X0,sF5),x0) = difference(x0,quotient(product(x0,X0),sF1)),
inference(superposition,[],[f4,f70118]) ).
fof(f79445,plain,
! [X0] : quotient(product(X0,sF5),x0) = quotient(product(X0,x0),product(sF1,x0)),
inference(forward_demodulation,[],[f79404,f3795]) ).
fof(f79485,plain,
! [X0] : quotient(product(x0,product(sF0,product(X0,sF0))),sF1) = product(x0,product(sF0,product(product(X0,sF1),sF0))),
inference(forward_demodulation,[],[f79354,f666]) ).
fof(f79492,plain,
! [X0] : quotient(product(X0,sF5),x0) = product(quotient(X0,sF4),sF0),
inference(forward_demodulation,[],[f79445,f50886]) ).
fof(f79524,plain,
! [X0] : quotient(product(x0,product(sF0,product(X0,sF0))),sF1) = product(sF4,product(x0,product(product(X0,sF1),sF0))),
inference(forward_demodulation,[],[f79485,f949]) ).
fof(f79587,plain,
! [X0] : quotient(product(X0,sF1),x0) = quotient(product(x0,product(sF0,product(X0,sF0))),sF1),
inference(forward_demodulation,[],[f79524,f974]) ).
fof(f79621,plain,
! [X0] : quotient(product(X0,sF1),x0) = quotient(product(sF4,product(x0,product(X0,sF0))),sF1),
inference(forward_demodulation,[],[f79587,f949]) ).
fof(f79634,plain,
! [X0] : quotient(product(X0,sF1),x0) = quotient(quotient(X0,x0),sF1),
inference(forward_demodulation,[],[f79621,f974]) ).
fof(f79815,plain,
! [X0] : quotient(X0,sF1) = quotient(product(product(X0,x0),sF1),x0),
inference(superposition,[],[f79634,f5]) ).
fof(f79972,plain,
! [X0] : quotient(quotient(X0,sF1),sF0) = product(sF0,product(sF1,product(x0,product(X0,x0)))),
inference(superposition,[],[f62425,f79815]) ).
fof(f79985,plain,
! [X0] : product(quotient(X0,sF1),x0) = product(product(X0,x0),sF1),
inference(superposition,[],[f6,f79815]) ).
fof(f80021,plain,
! [X0] : product(sF0,product(product(sF5,X0),sF5)) = product(sF1,product(product(X0,x0),sF1)),
inference(backward_demodulation,[],[f77968,f79985]) ).
fof(f80085,plain,
! [X0] : product(sF0,product(product(sF5,difference(sF5,X0)),sF5)) = product(product(sF0,product(X0,x0)),sF1),
inference(backward_demodulation,[],[f71024,f80021]) ).
fof(f80120,plain,
! [X0] : product(sF0,product(X0,sF5)) = product(product(sF0,product(X0,x0)),sF1),
inference(forward_demodulation,[],[f80085,f3]) ).
fof(f81221,plain,
! [X0] : product(sF4,product(sF4,X0)) = product(sF0,product(sF0,X0)),
inference(superposition,[],[f66410,f4]) ).
fof(f83821,plain,
difference(sF1,product(sF1,product(sF6,sF4))) = quotient(product(sF3,product(sF4,sF1)),sF1),
inference(superposition,[],[f7,f63492]) ).
fof(f83883,plain,
difference(sF1,product(sF1,product(sF6,sF4))) = product(product(sF3,sF0),sF1),
inference(forward_demodulation,[],[f83821,f64238]) ).
fof(f83901,plain,
quotient(difference(difference(x0,sF1),x1),x0) = product(product(sF3,sF0),sF1),
inference(forward_demodulation,[],[f83883,f29047]) ).
fof(f83914,plain,
quotient(difference(sF4,x1),x0) = product(product(sF3,sF0),sF1),
inference(forward_demodulation,[],[f83901,f42]) ).
fof(f83920,plain,
product(product(sF5,x1),sF4) = product(product(sF3,sF0),sF1),
inference(forward_demodulation,[],[f83914,f12374]) ).
fof(f83923,plain,
product(sF6,sF4) = product(product(sF3,sF0),sF1),
inference(forward_demodulation,[],[f83920,f31]) ).
fof(f83926,plain,
product(sF6,sF4) = product(sF3,quotient(product(sF4,sF6),sF3)),
inference(backward_demodulation,[],[f68166,f83923]) ).
fof(f84715,plain,
! [X0] : quotient(quotient(X0,sF4),x0) = product(sF0,product(sF1,product(x0,quotient(X0,sF1)))),
inference(superposition,[],[f62319,f6]) ).
fof(f84732,plain,
! [X0] : quotient(product(X0,sF1),sF4) = product(product(sF0,product(sF1,product(x0,X0))),x0),
inference(superposition,[],[f6,f62319]) ).
fof(f84765,plain,
! [X0] : quotient(product(X0,sF1),sF4) = product(sF0,quotient(product(sF1,product(x0,X0)),sF0)),
inference(forward_demodulation,[],[f84732,f675]) ).
fof(f84780,plain,
! [X0] : quotient(quotient(X0,x0),sF0) = quotient(quotient(X0,sF4),x0),
inference(backward_demodulation,[],[f68652,f84715]) ).
fof(f84813,plain,
! [X0] : quotient(product(X0,sF1),sF4) = product(sF4,quotient(product(x0,X0),sF0)),
inference(forward_demodulation,[],[f84765,f3430]) ).
fof(f85015,plain,
! [X0] : quotient(product(quotient(X0,sF4),sF0),sF0) = quotient(quotient(product(X0,sF5),sF4),x0),
inference(superposition,[],[f84780,f79492]) ).
fof(f85016,plain,
! [X0] : quotient(X0,sF0) = quotient(quotient(product(X0,x0),sF4),x0),
inference(superposition,[],[f84780,f5]) ).
fof(f85093,plain,
! [X0] : quotient(X0,sF0) = quotient(product(quotient(X0,sF4),sF5),x0),
inference(forward_demodulation,[],[f85016,f19638]) ).
fof(f85094,plain,
! [X0] : quotient(X0,sF4) = quotient(quotient(product(X0,sF5),sF4),x0),
inference(forward_demodulation,[],[f85015,f5]) ).
fof(f85125,plain,
! [X0] : quotient(X0,sF0) = product(quotient(quotient(X0,sF4),sF4),sF0),
inference(forward_demodulation,[],[f85093,f79492]) ).
fof(f85242,plain,
! [X0] : quotient(quotient(X0,sF4),x0) = quotient(quotient(X0,sF5),sF4),
inference(superposition,[],[f85094,f6]) ).
fof(f85258,plain,
! [X0] : quotient(product(X0,sF5),sF4) = product(quotient(X0,sF4),x0),
inference(superposition,[],[f6,f85094]) ).
fof(f85325,plain,
! [X0] : quotient(product(sF0,product(X0,sF4)),sF4) = product(sF4,quotient(quotient(X0,sF4),x0)),
inference(backward_demodulation,[],[f22733,f85242]) ).
fof(f85914,plain,
! [X0] : quotient(quotient(X0,sF4),sF4) = quotient(quotient(X0,sF0),sF0),
inference(superposition,[],[f5,f85125]) ).
fof(f87920,plain,
! [X0] : product(product(sF0,product(sF1,difference(sF4,X0))),sF4) = product(sF1,product(difference(sF1,X0),sF4)),
inference(superposition,[],[f59920,f65439]) ).
fof(f88139,plain,
difference(sF0,product(quotient(sF0,sF4),sF6)) = quotient(quotient(product(x0,product(sF3,sF0)),sF4),quotient(sF0,sF4)),
inference(superposition,[],[f374,f64020]) ).
fof(f88192,plain,
difference(sF0,product(quotient(sF0,sF4),sF6)) = product(sF4,quotient(product(x0,product(x0,product(sF3,sF0))),sF0)),
inference(forward_demodulation,[],[f88139,f6175]) ).
fof(f88204,plain,
difference(sF0,product(quotient(sF0,sF4),sF6)) = quotient(product(product(x0,product(sF3,sF0)),sF1),sF4),
inference(forward_demodulation,[],[f88192,f84813]) ).
fof(f88213,plain,
difference(sF0,product(quotient(sF0,sF4),sF6)) = product(x0,product(product(sF3,sF0),product(sF1,x0))),
inference(forward_demodulation,[],[f88204,f11941]) ).
fof(f88218,plain,
difference(sF0,product(quotient(sF0,sF4),sF6)) = difference(sF4,quotient(product(sF3,sF0),sF0)),
inference(forward_demodulation,[],[f88213,f12039]) ).
fof(f88219,plain,
difference(sF4,sF3) = difference(sF0,product(quotient(sF0,sF4),sF6)),
inference(forward_demodulation,[],[f88218,f5]) ).
fof(f88220,plain,
difference(sF4,sF3) = difference(sF0,product(sF1,sF6)),
inference(forward_demodulation,[],[f88219,f1989]) ).
fof(f88221,plain,
product(sF1,difference(sF4,sF3)) = difference(sF0,sF6),
inference(superposition,[],[f62690,f88220]) ).
fof(f88231,plain,
product(sF1,sF6) = product(sF0,difference(sF4,sF3)),
inference(superposition,[],[f3,f88220]) ).
fof(f88247,plain,
quotient(product(sF1,sF6),quotient(one,sF0)) = product(sF0,product(difference(sF4,sF3),sF0)),
inference(superposition,[],[f6030,f88220]) ).
fof(f88256,plain,
quotient(product(sF1,sF6),quotient(one,sF0)) = product(sF1,quotient(sF3,x0)),
inference(forward_demodulation,[],[f88247,f65370]) ).
fof(f88270,plain,
quotient(product(sF1,sF6),x0) = product(sF1,quotient(sF3,x0)),
inference(forward_demodulation,[],[f88256,f67]) ).
fof(f88381,plain,
product(sF0,product(difference(sF0,sF6),sF0)) = product(sF4,product(difference(sF4,sF3),sF0)),
inference(superposition,[],[f62457,f88221]) ).
fof(f88435,plain,
product(sF0,product(difference(sF0,sF6),sF0)) = quotient(product(sF3,sF1),sF5),
inference(forward_demodulation,[],[f88381,f34789]) ).
fof(f88447,plain,
quotient(sF6,quotient(one,sF0)) = quotient(product(sF3,sF1),sF5),
inference(forward_demodulation,[],[f88435,f6030]) ).
fof(f88453,plain,
quotient(sF6,x0) = quotient(product(sF3,sF1),sF5),
inference(forward_demodulation,[],[f88447,f67]) ).
fof(f88465,plain,
product(product(sF3,sF1),sF4) = product(product(quotient(sF6,x0),sF4),x0),
inference(superposition,[],[f14081,f88453]) ).
fof(f88502,plain,
product(sF6,sF0) = product(product(sF3,sF1),sF4),
inference(forward_demodulation,[],[f88465,f2332]) ).
fof(f88523,plain,
product(sF0,product(product(sF1,sF6),sF0)) = difference(x0,product(sF1,quotient(sF3,x0))),
inference(superposition,[],[f686,f88270]) ).
fof(f88576,plain,
product(sF0,product(product(sF1,sF6),sF0)) = difference(sF1,difference(x0,quotient(sF3,x0))),
inference(forward_demodulation,[],[f88523,f65982]) ).
fof(f88593,plain,
product(sF0,product(product(sF1,sF6),sF0)) = difference(sF1,product(sF0,product(sF3,sF0))),
inference(forward_demodulation,[],[f88576,f686]) ).
fof(f88603,plain,
product(sF0,product(product(sF1,sF6),sF0)) = product(sF0,product(sF1,product(sF3,sF0))),
inference(forward_demodulation,[],[f88593,f62228]) ).
fof(f88610,plain,
product(sF0,product(product(sF1,sF6),sF0)) = quotient(product(sF4,sF3),x0),
inference(forward_demodulation,[],[f88603,f66500]) ).
fof(f88614,plain,
product(sF4,product(sF6,sF0)) = quotient(product(sF4,sF3),x0),
inference(forward_demodulation,[],[f88610,f62457]) ).
fof(f88879,plain,
product(sF4,sF3) = product(sF0,product(sF1,sF6)),
inference(superposition,[],[f66410,f88231]) ).
fof(f88884,plain,
product(x0,product(sF1,sF6)) = product(sF4,product(x0,difference(sF4,sF3))),
inference(superposition,[],[f949,f88231]) ).
fof(f88934,plain,
product(sF5,sF3) = product(x0,product(sF1,sF6)),
inference(forward_demodulation,[],[f88884,f6725]) ).
fof(f89032,plain,
product(difference(sF1,product(sF1,sF6)),x0) = product(sF4,product(product(sF5,sF3),x0)),
inference(superposition,[],[f62773,f88934]) ).
fof(f89078,plain,
product(difference(sF1,product(sF1,sF6)),x0) = quotient(product(sF3,sF5),sF1),
inference(forward_demodulation,[],[f89032,f4488]) ).
fof(f89098,plain,
product(sF6,x0) = quotient(product(sF3,sF5),sF1),
inference(forward_demodulation,[],[f89078,f4]) ).
fof(f89207,plain,
product(sF3,sF5) = product(product(sF6,x0),sF1),
inference(superposition,[],[f6,f89098]) ).
fof(f89255,plain,
product(sF0,product(sF1,product(x0,product(sF6,x0)))) = quotient(quotient(product(sF3,sF5),sF4),x0),
inference(superposition,[],[f62319,f89207]) ).
fof(f89293,plain,
product(sF0,product(sF1,product(x0,product(sF6,x0)))) = quotient(product(quotient(sF3,sF4),x0),x0),
inference(forward_demodulation,[],[f89255,f85258]) ).
fof(f89300,plain,
quotient(sF3,sF4) = product(sF0,product(sF1,product(x0,product(sF6,x0)))),
inference(forward_demodulation,[],[f89293,f5]) ).
fof(f89305,plain,
quotient(sF3,sF4) = quotient(quotient(sF6,sF1),sF0),
inference(forward_demodulation,[],[f89300,f79972]) ).
fof(f89309,plain,
product(sF0,product(quotient(sF6,sF1),x0)) = product(difference(x0,quotient(sF3,sF4)),sF1),
inference(superposition,[],[f25640,f89305]) ).
fof(f89345,plain,
product(sF0,product(quotient(sF6,sF1),x0)) = product(product(sF0,product(sF3,x0)),sF1),
inference(forward_demodulation,[],[f89309,f6451]) ).
fof(f89355,plain,
product(sF0,product(quotient(sF6,sF1),x0)) = product(sF0,product(sF3,sF5)),
inference(forward_demodulation,[],[f89345,f80120]) ).
fof(f89361,plain,
product(sF0,product(product(sF6,x0),sF1)) = product(sF0,product(sF3,sF5)),
inference(forward_demodulation,[],[f89355,f79985]) ).
fof(f89365,plain,
product(difference(x0,sF6),sF5) = product(sF0,product(sF3,sF5)),
inference(forward_demodulation,[],[f89361,f68949]) ).
fof(f89392,plain,
difference(x0,sF6) = quotient(product(sF0,product(sF3,sF5)),sF5),
inference(superposition,[],[f5,f89365]) ).
fof(f89428,plain,
difference(x0,sF6) = difference(sF5,difference(sF1,sF3)),
inference(forward_demodulation,[],[f89392,f72525]) ).
fof(f89483,plain,
product(sF1,product(difference(sF1,sF3),sF4)) = product(x0,quotient(difference(x0,sF6),x0)),
inference(superposition,[],[f11980,f89428]) ).
fof(f89526,plain,
product(sF1,product(difference(sF1,sF3),sF4)) = product(sF6,quotient(one,x0)),
inference(forward_demodulation,[],[f89483,f19050]) ).
fof(f89535,plain,
product(sF6,sF4) = product(sF1,product(difference(sF1,sF3),sF4)),
inference(forward_demodulation,[],[f89526,f27]) ).
fof(f90350,plain,
difference(sF4,product(sF4,product(sF6,sF0))) = product(x0,product(product(sF4,sF3),sF0)),
inference(superposition,[],[f34287,f88614]) ).
fof(f90394,plain,
quotient(product(sF3,sF4),sF1) = difference(sF4,product(sF4,product(sF6,sF0))),
inference(forward_demodulation,[],[f90350,f34597]) ).
fof(f90413,plain,
product(sF6,sF0) = quotient(product(sF3,sF4),sF1),
inference(forward_demodulation,[],[f90394,f4]) ).
fof(f90442,plain,
product(sF3,sF4) = product(product(sF6,sF0),sF1),
inference(superposition,[],[f6,f90413]) ).
fof(f90547,plain,
product(sF1,product(sF4,sF3)) = product(sF0,difference(sF1,product(sF1,sF6))),
inference(superposition,[],[f65109,f88879]) ).
fof(f90589,plain,
product(sF0,sF6) = product(sF1,product(sF4,sF3)),
inference(forward_demodulation,[],[f90547,f4]) ).
fof(f90644,plain,
product(product(sF3,sF1),sF4) = product(sF3,quotient(product(sF0,sF6),sF3)),
inference(superposition,[],[f113,f90589]) ).
fof(f90683,plain,
product(sF6,sF0) = product(sF3,quotient(product(sF0,sF6),sF3)),
inference(forward_demodulation,[],[f90644,f88502]) ).
fof(f96367,plain,
difference(sF5,sF2) = difference(sF1,difference(sF5,x1)),
inference(superposition,[],[f65530,f23]) ).
fof(f96632,plain,
difference(sF5,x1) = product(sF1,difference(sF5,sF2)),
inference(superposition,[],[f3,f96367]) ).
fof(f99627,plain,
quotient(product(sF4,sF6),sF3) = difference(sF3,product(sF6,sF4)),
inference(superposition,[],[f4,f83926]) ).
fof(f103191,plain,
! [X0] : product(X0,sF4) = product(product(quotient(X0,x0),sF0),x0),
inference(superposition,[],[f60685,f6]) ).
fof(f103897,plain,
difference(sF4,product(difference(sF5,sF2),x0)) = product(product(x0,difference(sF5,x1)),x0),
inference(superposition,[],[f63611,f96632]) ).
fof(f104027,plain,
product(product(sF0,difference(sF4,x1)),x0) = difference(sF4,product(difference(sF5,sF2),x0)),
inference(forward_demodulation,[],[f103897,f60553]) ).
fof(f104096,plain,
product(product(sF0,difference(sF4,x1)),x0) = product(product(sF2,quotient(x0,sF5)),sF5),
inference(forward_demodulation,[],[f104027,f22985]) ).
fof(f104143,plain,
product(product(sF0,difference(sF4,x1)),x0) = product(product(sF2,sF1),sF5),
inference(forward_demodulation,[],[f104096,f3149]) ).
fof(f104180,plain,
product(product(sF0,difference(sF4,x1)),x0) = product(sF2,quotient(sF6,sF2)),
inference(forward_demodulation,[],[f104143,f77175]) ).
fof(f104206,plain,
product(sF0,quotient(difference(sF4,x1),sF0)) = product(sF2,quotient(sF6,sF2)),
inference(forward_demodulation,[],[f104180,f675]) ).
fof(f104227,plain,
product(sF0,product(product(sF5,x1),x0)) = product(sF2,quotient(sF6,sF2)),
inference(forward_demodulation,[],[f104206,f6930]) ).
fof(f104242,plain,
product(sF1,product(x1,x0)) = product(sF2,quotient(sF6,sF2)),
inference(forward_demodulation,[],[f104227,f24490]) ).
fof(f104265,plain,
product(sF0,product(sF6,x0)) = product(sF2,quotient(sF6,sF2)),
inference(forward_demodulation,[],[f104242,f24568]) ).
fof(f104405,plain,
quotient(sF6,sF2) = difference(sF2,product(sF0,product(sF6,x0))),
inference(superposition,[],[f4,f104265]) ).
fof(f104444,plain,
quotient(sF6,sF2) = product(difference(product(x0,sF2),sF6),x0),
inference(forward_demodulation,[],[f104405,f58879]) ).
fof(f104459,plain,
quotient(sF6,sF2) = product(difference(sF3,sF6),x0),
inference(forward_demodulation,[],[f104444,f25]) ).
fof(f104485,plain,
difference(sF3,sF6) = quotient(quotient(sF6,sF2),x0),
inference(superposition,[],[f5,f104459]) ).
fof(f104519,plain,
product(sF3,difference(sF3,sF6)) = product(x0,product(sF2,quotient(sF6,sF3))),
inference(superposition,[],[f2621,f104485]) ).
fof(f104563,plain,
sF6 = product(x0,product(sF2,quotient(sF6,sF3))),
inference(forward_demodulation,[],[f104519,f3]) ).
fof(f104575,plain,
product(sF6,sF4) = product(x0,quotient(product(sF2,quotient(sF6,sF3)),x0)),
inference(superposition,[],[f1837,f104563]) ).
fof(f104591,plain,
product(product(quotient(sF6,sF3),x0),sF2) = product(quotient(sF6,sF3),quotient(sF6,quotient(sF6,sF3))),
inference(superposition,[],[f113,f104563]) ).
fof(f104592,plain,
difference(x0,sF6) = product(sF2,quotient(sF6,sF3)),
inference(superposition,[],[f4,f104563]) ).
fof(f104646,plain,
product(product(quotient(sF6,sF3),x0),sF2) = product(sF6,quotient(difference(sF3,sF6),quotient(sF6,sF3))),
inference(forward_demodulation,[],[f104591,f53432]) ).
fof(f104662,plain,
product(sF6,sF4) = product(sF3,quotient(quotient(sF6,sF3),x0)),
inference(forward_demodulation,[],[f104575,f3423]) ).
fof(f104729,plain,
! [X0] : product(quotient(sF6,sF3),quotient(X0,quotient(sF6,sF3))) = product(product(quotient(sF6,sF3),quotient(X0,difference(x0,sF6))),sF2),
inference(superposition,[],[f2763,f104592]) ).
fof(f104743,plain,
! [X0] : product(product(quotient(sF6,sF3),quotient(X0,difference(x0,sF6))),sF2) = product(sF6,quotient(difference(sF3,X0),quotient(sF6,sF3))),
inference(forward_demodulation,[],[f104729,f53432]) ).
fof(f104768,plain,
difference(sF3,product(sF6,sF4)) = quotient(quotient(sF6,sF3),x0),
inference(superposition,[],[f4,f104662]) ).
fof(f104805,plain,
quotient(product(sF4,sF6),sF3) = quotient(quotient(sF6,sF3),x0),
inference(forward_demodulation,[],[f104768,f99627]) ).
fof(f104855,plain,
product(quotient(product(sF4,sF6),sF3),x0) = quotient(sF6,sF3),
inference(superposition,[],[f6,f104805]) ).
fof(f106584,plain,
! [X0] : quotient(product(X0,sF4),x0) = product(quotient(X0,x0),sF0),
inference(superposition,[],[f5,f103191]) ).
fof(f106625,plain,
! [X0] : product(quotient(X0,x0),sF0) = product(quotient(X0,sF5),sF4),
inference(forward_demodulation,[],[f106584,f19711]) ).
fof(f106841,plain,
! [X0] : product(quotient(X0,sF1),sF0) = product(quotient(product(product(X0,x0),sF1),sF5),sF4),
inference(superposition,[],[f106625,f79815]) ).
fof(f106943,plain,
! [X0] : product(quotient(X0,sF1),sF0) = product(product(sF0,product(sF1,difference(sF4,X0))),sF4),
inference(forward_demodulation,[],[f106841,f69957]) ).
fof(f107013,plain,
! [X0] : product(quotient(X0,sF1),sF0) = product(sF1,product(difference(sF1,X0),sF4)),
inference(backward_demodulation,[],[f87920,f106943]) ).
fof(f107041,plain,
product(sF6,sF4) = product(quotient(sF3,sF1),sF0),
inference(backward_demodulation,[],[f89535,f107013]) ).
fof(f107066,plain,
product(sF0,product(quotient(sF3,sF1),sF1)) = product(product(sF0,product(sF6,sF4)),sF5),
inference(superposition,[],[f68799,f107041]) ).
fof(f107102,plain,
product(sF0,sF3) = product(product(sF0,product(sF6,sF4)),sF5),
inference(forward_demodulation,[],[f107066,f6]) ).
fof(f107125,plain,
quotient(product(sF0,sF3),sF4) = product(quotient(product(sF0,product(sF6,sF4)),sF4),x0),
inference(superposition,[],[f85258,f107102]) ).
fof(f107181,plain,
quotient(product(sF0,sF3),sF4) = product(product(sF4,quotient(quotient(sF6,sF4),x0)),x0),
inference(forward_demodulation,[],[f107125,f85325]) ).
fof(f107199,plain,
quotient(product(sF0,sF3),sF4) = product(sF4,quotient(quotient(quotient(sF6,sF4),sF4),x0)),
inference(forward_demodulation,[],[f107181,f59688]) ).
fof(f107207,plain,
quotient(product(sF0,sF3),sF4) = product(sF4,quotient(quotient(quotient(sF6,sF0),sF0),x0)),
inference(forward_demodulation,[],[f107199,f85914]) ).
fof(f107211,plain,
quotient(product(sF0,sF3),sF4) = product(sF4,product(sF4,product(x0,quotient(sF6,sF0)))),
inference(forward_demodulation,[],[f107207,f972]) ).
fof(f107214,plain,
quotient(product(sF0,sF3),sF4) = product(sF0,product(sF0,product(x0,quotient(sF6,sF0)))),
inference(forward_demodulation,[],[f107211,f81221]) ).
fof(f107215,plain,
quotient(product(sF0,sF6),sF4) = quotient(product(sF0,sF3),sF4),
inference(forward_demodulation,[],[f107214,f68112]) ).
fof(f107304,plain,
product(sF0,sF6) = product(quotient(product(sF0,sF3),sF4),sF4),
inference(superposition,[],[f6,f107215]) ).
fof(f107340,plain,
product(sF0,sF3) = product(sF0,sF6),
inference(forward_demodulation,[],[f107304,f6]) ).
fof(f107391,plain,
product(sF6,sF0) = product(sF3,quotient(product(sF0,sF3),sF3)),
inference(backward_demodulation,[],[f90683,f107340]) ).
fof(f107510,plain,
product(sF3,sF0) = product(sF6,sF0),
inference(forward_demodulation,[],[f107391,f5]) ).
fof(f107650,plain,
product(sF3,sF4) = product(product(sF3,sF0),sF1),
inference(backward_demodulation,[],[f90442,f107510]) ).
fof(f107801,plain,
product(sF3,sF4) = product(sF6,sF4),
inference(backward_demodulation,[],[f83923,f107650]) ).
fof(f107948,plain,
difference(sF4,x1) = product(product(sF3,sF4),x0),
inference(backward_demodulation,[],[f10193,f107801]) ).
fof(f108056,plain,
quotient(product(sF4,sF6),sF3) = difference(sF3,product(sF3,sF4)),
inference(backward_demodulation,[],[f99627,f107801]) ).
fof(f108249,plain,
sF4 = quotient(product(sF4,sF6),sF3),
inference(forward_demodulation,[],[f108056,f4]) ).
fof(f108268,plain,
difference(sF0,sF2) = difference(sF4,x1),
inference(forward_demodulation,[],[f107948,f18474]) ).
fof(f108394,plain,
product(sF4,x0) = quotient(sF6,sF3),
inference(backward_demodulation,[],[f104855,f108249]) ).
fof(f108455,plain,
difference(x0,sF6) = product(sF0,difference(sF0,sF2)),
inference(backward_demodulation,[],[f11008,f108268]) ).
fof(f108694,plain,
one = quotient(sF6,sF3),
inference(forward_demodulation,[],[f108394,f129]) ).
fof(f108759,plain,
sF2 = difference(x0,sF6),
inference(forward_demodulation,[],[f108455,f3]) ).
fof(f108923,plain,
product(product(one,x0),sF2) = product(sF6,quotient(difference(sF3,sF6),one)),
inference(backward_demodulation,[],[f104646,f108694]) ).
fof(f108949,plain,
! [X0] : product(product(one,quotient(X0,difference(x0,sF6))),sF2) = product(sF6,quotient(difference(sF3,X0),one)),
inference(backward_demodulation,[],[f104743,f108694]) ).
fof(f109293,plain,
! [X0] : product(sF6,difference(sF3,X0)) = product(product(one,quotient(X0,difference(x0,sF6))),sF2),
inference(forward_demodulation,[],[f108949,f70]) ).
fof(f109319,plain,
product(sF6,difference(sF3,sF6)) = product(product(one,x0),sF2),
inference(forward_demodulation,[],[f108923,f70]) ).
fof(f110063,plain,
! [X0] : product(sF6,difference(sF3,X0)) = product(quotient(X0,difference(x0,sF6)),sF2),
inference(forward_demodulation,[],[f109293,f2]) ).
fof(f110083,plain,
product(x0,sF2) = product(sF6,difference(sF3,sF6)),
inference(forward_demodulation,[],[f109319,f2]) ).
fof(f110565,plain,
! [X0] : product(quotient(X0,sF2),sF2) = product(sF6,difference(sF3,X0)),
inference(forward_demodulation,[],[f110063,f108759]) ).
fof(f110578,plain,
sF3 = product(sF6,difference(sF3,sF6)),
inference(forward_demodulation,[],[f110083,f25]) ).
fof(f111371,plain,
! [X0] : product(sF6,difference(sF3,X0)) = X0,
inference(forward_demodulation,[],[f110565,f6]) ).
fof(f112139,plain,
sF3 = sF6,
inference(backward_demodulation,[],[f110578,f111371]) ).
fof(f112706,plain,
$false,
inference(forward_subsumption_resolution,[],[f112139,f32]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP764-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/11.02 % Computer : n004.cluster.edu
% 0.10/11.02 % Model : x86_64 x86_64
% 0.10/11.02 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/11.02 % Memory : 8046.5625MB
% 0.10/11.02 % OS : Linux 6.8.0-71-generic
% 0.10/11.02 % CPULimit : 300
% 0.10/11.02 % WCLimit : 300
% 0.10/11.02 % DateTime : Sun Sep 27 10:43:05 UTC 2026
% 0.10/11.02 % CPUTime :
% 0.10/11.02 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/11.06 Running first-order theorem proving
% 0.15/11.06 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
% 86.97/23.72 % (3326133)Detected a unit-equality problem, will run specialized UEQ schedule.
% 86.97/23.72 % (3326142)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2928253987:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 86.97/23.72 % (3326138)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=857142992:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 86.97/23.72 % (3326140)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3141112914:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 86.97/23.72 % (3326143)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1766751824:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 86.97/23.72 % (3326141)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1418526955:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 86.97/23.72 % (3326139)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=1630978126:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 86.97/23.72 % (3326144)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=507930068:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 86.97/23.72 % (3326142)Instruction limit reached!
% 86.97/23.72 % (3326142)------------------------------
% 86.97/23.72 % (3326142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.97/23.72 % (3326142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.97/23.72 % (3326142)CaDiCaL version: 2.1.3
% 86.97/23.72 % (3326142)Termination reason: Instruction limit
% 86.97/23.72 % (3326142)Termination phase: Saturation
% 86.97/23.72 % (3326142)Time elapsed: 0.058 s
% 86.97/23.72 % (3326142)Peak memory usage: 89 MB
% 86.97/23.72 % (3326142)Instructions burned: 183 (million)
% 86.97/23.72 % (3326141)Instruction limit reached!
% 86.97/23.72 % (3326141)------------------------------
% 86.97/23.72 % (3326141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.97/23.72 % (3326141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.97/23.72 % (3326141)CaDiCaL version: 2.1.3
% 86.97/23.72 % (3326141)Termination reason: Instruction limit
% 86.97/23.72 % (3326141)Termination phase: Saturation
% 86.97/23.72 % (3326141)Time elapsed: 0.081 s
% 86.97/23.72 % (3326141)Peak memory usage: 89 MB
% 86.97/23.72 % (3326141)Instructions burned: 136 (million)
% 86.97/23.72 % (3326152)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1965335516:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 86.97/23.72 % (3326143)Instruction limit reached!
% 86.97/23.72 % (3326143)------------------------------
% 86.97/23.72 % (3326143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.97/23.72 % (3326143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.97/23.72 % (3326143)CaDiCaL version: 2.1.3
% 86.97/23.72 % (3326143)Termination reason: Instruction limit
% 86.97/23.72 % (3326143)Termination phase: Saturation
% 86.97/23.72 % (3326143)Time elapsed: 0.157 s
% 86.97/23.72 % (3326143)Peak memory usage: 90 MB
% 86.97/23.72 % (3326143)Instructions burned: 258 (million)
% 86.97/23.72 % (3326153)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1757569663:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 86.97/23.72 % (3326155)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1010870442:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 86.97/23.72 % (3326155)Instruction limit reached!
% 86.97/23.72 % (3326155)------------------------------
% 86.97/23.72 % (3326155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.97/23.72 % (3326155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.97/23.72 % (3326155)CaDiCaL version: 2.1.3
% 86.97/23.72 % (3326155)Termination reason: Instruction limit
% 86.97/23.72 % (3326155)Termination phase: Saturation
% 86.97/23.72 % (3326155)Time elapsed: 0.122 s
% 51.16/25.32 % (3326155)Peak memory usage: 90 MB
% 51.16/25.32 % (3326155)Instructions burned: 216 (million)
% 51.16/25.32 % (3326158)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=587319033:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 51.16/25.32 % (3326144)Instruction limit reached!
% 51.16/25.32 % (3326144)------------------------------
% 51.16/25.32 % (3326144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326144)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326144)Termination reason: Instruction limit
% 51.16/25.32 % (3326144)Termination phase: Saturation
% 51.16/25.32 % (3326144)Time elapsed: 0.664 s
% 51.16/25.32 % (3326144)Peak memory usage: 99 MB
% 51.16/25.32 % (3326144)Instructions burned: 1188 (million)
% 51.16/25.32 % (3326158)Instruction limit reached!
% 51.16/25.32 % (3326158)------------------------------
% 51.16/25.32 % (3326158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326158)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326158)Termination reason: Instruction limit
% 51.16/25.32 % (3326158)Termination phase: Saturation
% 51.16/25.32 % (3326158)Time elapsed: 0.213 s
% 51.16/25.32 % (3326158)Peak memory usage: 94 MB
% 51.16/25.32 % (3326158)Instructions burned: 318 (million)
% 51.16/25.32 % (3326160)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=1695616750:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 51.16/25.32 % (3326152)Instruction limit reached!
% 51.16/25.32 % (3326152)------------------------------
% 51.16/25.32 % (3326152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326152)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326152)Termination reason: Instruction limit
% 51.16/25.32 % (3326152)Termination phase: Saturation
% 51.16/25.32 % (3326152)Time elapsed: 0.745 s
% 51.16/25.32 % (3326152)Peak memory usage: 142 MB
% 51.16/25.32 % (3326152)Instructions burned: 2054 (million)
% 51.16/25.32 % (3326161)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=411671490:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 51.16/25.32 % (3326163)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3170125490:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 51.16/25.32 % (3326161)Instruction limit reached!
% 51.16/25.32 % (3326161)------------------------------
% 51.16/25.32 % (3326161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326161)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326161)Termination reason: Instruction limit
% 51.16/25.32 % (3326161)Termination phase: Saturation
% 51.16/25.32 % (3326161)Time elapsed: 1.921 s
% 51.16/25.32 % (3326161)Peak memory usage: 140 MB
% 51.16/25.32 % (3326161)Instructions burned: 2837 (million)
% 51.16/25.32 % (3326166)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=2127403064:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2969 on theBenchmark for (2969ds/11832Mi)
% 51.16/25.32 % (3326153)Instruction limit reached!
% 51.16/25.32 % (3326153)------------------------------
% 51.16/25.32 % (3326153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326153)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326153)Termination reason: Instruction limit
% 51.16/25.32 % (3326153)Termination phase: Saturation
% 51.16/25.32 % (3326153)Time elapsed: 2.913 s
% 51.16/25.32 % (3326153)Peak memory usage: 171 MB
% 51.16/25.32 % (3326153)Instructions burned: 4948 (million)
% 51.16/25.32 % (3326168)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=1326624400:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 51.16/25.32 % (3326168)Instruction limit reached!
% 51.16/25.32 % (3326168)------------------------------
% 51.16/25.32 % (3326168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326168)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326168)Termination reason: Instruction limit
% 51.16/25.32 % (3326168)Termination phase: Saturation
% 51.16/25.32 % (3326168)Time elapsed: 1.369 s
% 51.16/25.32 % (3326168)Peak memory usage: 139 MB
% 51.16/25.32 % (3326168)Instructions burned: 2280 (million)
% 51.16/25.32 % (3326170)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=3685979759:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 51.16/25.32 % (3326160)Instruction limit reached!
% 51.16/25.32 % (3326160)------------------------------
% 51.16/25.32 % (3326160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326160)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326160)Termination reason: Instruction limit
% 51.16/25.32 % (3326160)Termination phase: Saturation
% 51.16/25.32 % (3326160)Time elapsed: 4.183 s
% 51.16/25.32 % (3326160)Peak memory usage: 244 MB
% 51.16/25.32 % (3326160)Instructions burned: 12125 (million)
% 51.16/25.32 % (3326172)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1520458570:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2948 on theBenchmark for (2948ds/21755Mi)
% 51.16/25.32 % (3326170)Instruction limit reached!
% 51.16/25.32 % (3326170)------------------------------
% 51.16/25.32 % (3326170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326170)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326170)Termination reason: Instruction limit
% 51.16/25.32 % (3326170)Termination phase: Saturation
% 51.16/25.32 % (3326170)Time elapsed: 3.405 s
% 51.16/25.32 % (3326170)Peak memory usage: 152 MB
% 51.16/25.32 % (3326170)Instructions burned: 6225 (million)
% 51.16/25.32 % (3326174)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=2288407485:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2915 on theBenchmark for (2915ds/16427Mi)
% 51.16/25.32 % (3326163)Instruction limit reached!
% 51.16/25.32 % (3326163)------------------------------
% 51.16/25.32 % (3326163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326163)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326163)Termination reason: Instruction limit
% 51.16/25.32 % (3326163)Termination phase: Saturation
% 51.16/25.32 % (3326163)Time elapsed: 9.019 s
% 51.16/25.32 % (3326163)Peak memory usage: 254 MB
% 51.16/25.32 % (3326163)Instructions burned: 14535 (million)
% 51.16/25.32 % (3326176)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=1388515886:i=9356:fgj=on:bd=preordered:av=off_2897 on theBenchmark for (2897ds/9356Mi)
% 51.16/25.32 % (3326166)Instruction limit reached!
% 51.16/25.32 % (3326166)------------------------------
% 51.16/25.32 % (3326166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326166)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326166)Termination reason: Instruction limit
% 51.16/25.32 % (3326166)Termination phase: Saturation
% 51.16/25.32 % (3326166)Time elapsed: 7.500 s
% 51.16/25.32 % (3326166)Peak memory usage: 239 MB
% 51.16/25.32 % (3326166)Instructions burned: 11833 (million)
% 51.16/25.32 % (3326178)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=1838852025:i=2070:kws=inv_precedence:slsql=off:bd=all_2892 on theBenchmark for (2892ds/2070Mi)
% 51.16/25.32 % (3326178)Instruction limit reached!
% 51.16/25.32 % (3326178)------------------------------
% 51.16/25.32 % (3326178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.16/25.32 % (3326178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.16/25.32 % (3326178)CaDiCaL version: 2.1.3
% 51.16/25.32 % (3326178)Termination reason: Instruction limit
% 51.16/25.32 % (3326178)Termination phase: Saturation
% 51.16/25.32 % (3326178)Time elapsed: 1.283 s
% 51.16/25.32 % (3326178)Peak memory usage: 130 MB
% 51.16/25.32 % (3326178)Instructions burned: 2071 (million)
% 51.16/25.32 % (3326180)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=3969401050:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2877 on theBenchmark for (2877ds/6461Mi)
% 51.16/25.32 % (3326140)First to succeed.
% 51.16/25.32 % (3326140)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3326133"
% 51.16/25.32 % (3326140)Refutation found. Thanks to Tanya!
% 51.16/25.32 % SZS status Unsatisfiable for theBenchmark
% 51.16/25.32 % SZS output start Proof for theBenchmark
% See solution above
% 98.49/25.52 % (3326140)------------------------------
% 98.49/25.52 % (3326140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.49/25.52 % (3326140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.49/25.52 % (3326140)CaDiCaL version: 2.1.3
% 98.49/25.52 % (3326140)Termination reason: Refutation
% 98.49/25.52 % (3326140)Time elapsed: 13.307 s
% 98.49/25.52 % (3326140)Peak memory usage: 313 MB
% 98.49/25.52 % (3326140)Instructions burned: 20685 (million)
% 98.49/25.52 % (3326140)------------------------------
% 98.49/25.52 % (3326140)------------------------------
% 98.49/25.52 % (3326133)Success in time 13.811 s
% 98.49/25.52 % Vampire exiting
%------------------------------------------------------------------------------