%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP688-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:36 AM UTC 2026
% Result : Unsatisfiable 31.47s 5.38s
% Output : Refutation 32.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 19
% Syntax : Number of formulae : 457 ( 457 unt; 7 def)
% Number of atoms : 457 ( 456 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 388 ( 388 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).
fof(f2,negated_conjecture,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).
fof(f3,negated_conjecture,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).
fof(f4,negated_conjecture,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).
fof(f5,negated_conjecture,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).
fof(f6,negated_conjecture,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X0,X2))) = mult(mult(X0,mult(X1,X0)),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).
fof(f8,negated_conjecture,
! [X0,X1] : mult(i(X0),mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).
fof(f9,negated_conjecture,
! [X0,X1] : i(mult(X0,X1)) = mult(i(X0),i(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c09) ).
fof(f10,axiom,
mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
fof(f11,plain,
unit = mult(op_c,mult(op_c,mult(op_c,op_c))),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
mult(op_d,mult(op_d,op_d)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).
fof(f13,plain,
unit = mult(op_d,mult(op_d,op_d)),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
mult(op_c,op_d) != mult(op_d,op_c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f15,definition,
sF0 = mult(op_c,op_c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f16,plain,
mult(op_c,op_c) = sF0,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF1 = mult(op_c,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f18,plain,
mult(op_c,sF0) = sF1,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF2 = mult(op_c,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f20,plain,
mult(op_c,sF1) = sF2,
inference(reorient_equations,[],[f19]) ).
fof(f21,plain,
unit = sF2,
inference(definition_folding,[],[f11,f20,f18,f16]) ).
fof(f22,definition,
sF3 = mult(op_d,op_d),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f23,plain,
mult(op_d,op_d) = sF3,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF4 = mult(op_d,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f25,plain,
mult(op_d,sF3) = sF4,
inference(reorient_equations,[],[f24]) ).
fof(f26,plain,
unit = sF4,
inference(definition_folding,[],[f13,f25,f23]) ).
fof(f27,definition,
sF5 = mult(op_c,op_d),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f28,plain,
mult(op_c,op_d) = sF5,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF6 = mult(op_d,op_c),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f30,plain,
mult(op_d,op_c) = sF6,
inference(reorient_equations,[],[f29]) ).
fof(f31,plain,
sF5 != sF6,
inference(definition_folding,[],[f14,f30,f28]) ).
fof(f32,plain,
unit = mult(op_c,sF1),
inference(forward_demodulation,[],[f20,f21]) ).
fof(f33,plain,
unit = mult(op_d,sF3),
inference(forward_demodulation,[],[f25,f26]) ).
fof(f35,plain,
! [X0] : mult(op_c,mult(op_c,mult(op_c,X0))) = mult(mult(op_c,sF0),X0),
inference(superposition,[],[f7,f16]) ).
fof(f41,plain,
! [X0] : mult(op_c,mult(op_c,mult(op_c,X0))) = mult(sF1,X0),
inference(forward_demodulation,[],[f35,f18]) ).
fof(f43,plain,
! [X0] : mult(sF0,mult(op_c,mult(sF0,X0))) = mult(mult(sF0,sF1),X0),
inference(superposition,[],[f7,f18]) ).
fof(f47,plain,
! [X0] : mult(op_d,mult(op_d,mult(op_d,X0))) = mult(mult(op_d,sF3),X0),
inference(superposition,[],[f7,f23]) ).
fof(f48,plain,
! [X0] : mult(unit,X0) = mult(op_d,mult(op_d,mult(op_d,X0))),
inference(forward_demodulation,[],[f47,f33]) ).
fof(f49,plain,
! [X0] : mult(op_d,mult(op_d,mult(op_d,X0))) = X0,
inference(forward_demodulation,[],[f48,f6]) ).
fof(f51,plain,
op_d = ld(op_c,sF5),
inference(superposition,[],[f2,f28]) ).
fof(f52,plain,
op_c = ld(op_c,sF0),
inference(superposition,[],[f2,f16]) ).
fof(f53,plain,
sF0 = ld(op_c,sF1),
inference(superposition,[],[f2,f18]) ).
fof(f54,plain,
op_c = ld(op_d,sF6),
inference(superposition,[],[f2,f30]) ).
fof(f57,plain,
! [X0] : unit = ld(X0,X0),
inference(superposition,[],[f2,f5]) ).
fof(f64,plain,
! [X0,X1] : mult(X0,mult(unit,mult(X0,X1))) = mult(mult(X0,X0),X1),
inference(superposition,[],[f7,f6]) ).
fof(f68,plain,
! [X0,X1] : mult(mult(X0,X0),X1) = mult(X0,mult(X0,X1)),
inference(forward_demodulation,[],[f64,f6]) ).
fof(f70,plain,
sF1 = ld(op_c,unit),
inference(superposition,[],[f2,f32]) ).
fof(f71,plain,
! [X0] : mult(sF1,mult(op_c,mult(sF1,X0))) = mult(mult(sF1,unit),X0),
inference(superposition,[],[f7,f32]) ).
fof(f72,plain,
! [X0] : mult(sF1,X0) = mult(sF1,mult(op_c,mult(sF1,X0))),
inference(forward_demodulation,[],[f71,f5]) ).
fof(f81,plain,
! [X0] : mult(op_c,mult(op_c,X0)) = mult(sF1,ld(op_c,X0)),
inference(superposition,[],[f41,f1]) ).
fof(f83,plain,
! [X0] : mult(op_c,mult(sF1,X0)) = mult(sF1,mult(op_c,X0)),
inference(superposition,[],[f41,f41]) ).
fof(f84,plain,
! [X0] : mult(op_c,mult(op_c,X0)) = ld(op_c,mult(sF1,X0)),
inference(superposition,[],[f2,f41]) ).
fof(f86,plain,
! [X0] : mult(sF1,X0) = mult(sF1,mult(sF1,mult(op_c,X0))),
inference(backward_demodulation,[],[f72,f83]) ).
fof(f89,plain,
! [X0] : mult(sF1,ld(op_c,X0)) = ld(op_c,mult(sF1,X0)),
inference(backward_demodulation,[],[f84,f81]) ).
fof(f99,plain,
! [X0,X1] : ld(X1,X0) = mult(i(X1),X0),
inference(superposition,[],[f8,f1]) ).
fof(f107,plain,
sF1 = mult(i(op_c),unit),
inference(superposition,[],[f8,f32]) ).
fof(f110,plain,
sF3 = mult(i(op_d),unit),
inference(superposition,[],[f8,f33]) ).
fof(f113,plain,
! [X2,X0,X1] : mult(mult(X1,X0),mult(i(X1),mult(mult(X1,X0),X2))) = mult(mult(mult(X1,X0),X0),X2),
inference(superposition,[],[f7,f8]) ).
fof(f114,plain,
sF3 = i(op_d),
inference(forward_demodulation,[],[f110,f5]) ).
fof(f115,plain,
sF1 = i(op_c),
inference(forward_demodulation,[],[f107,f5]) ).
fof(f116,plain,
! [X0,X1] : i(mult(X0,X1)) = ld(X0,i(X1)),
inference(backward_demodulation,[],[f9,f99]) ).
fof(f118,plain,
! [X2,X0,X1] : mult(mult(mult(X1,X0),X0),X2) = mult(mult(X1,X0),ld(X1,mult(mult(X1,X0),X2))),
inference(backward_demodulation,[],[f113,f99]) ).
fof(f128,plain,
! [X0,X1] : i(X1) = mult(X0,i(mult(X0,X1))),
inference(superposition,[],[f1,f116]) ).
fof(f129,plain,
! [X0,X1] : i(ld(X1,X0)) = mult(X1,i(X0)),
inference(superposition,[],[f128,f1]) ).
fof(f130,plain,
! [X0] : i(unit) = mult(X0,i(X0)),
inference(superposition,[],[f128,f5]) ).
fof(f135,plain,
i(op_d) = mult(op_c,i(sF5)),
inference(superposition,[],[f128,f28]) ).
fof(f138,plain,
i(op_c) = mult(op_d,i(sF6)),
inference(superposition,[],[f128,f30]) ).
fof(f140,plain,
i(sF3) = mult(op_d,i(unit)),
inference(superposition,[],[f128,f33]) ).
fof(f151,plain,
sF1 = mult(op_d,i(sF6)),
inference(forward_demodulation,[],[f138,f115]) ).
fof(f152,plain,
sF3 = mult(op_c,i(sF5)),
inference(forward_demodulation,[],[f135,f114]) ).
fof(f165,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f168,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,mult(X1,mult(X0,X2))),X2),
inference(superposition,[],[f4,f7]) ).
fof(f178,plain,
! [X0,X1] : i(X1) = mult(rd(X0,X1),i(X0)),
inference(superposition,[],[f128,f3]) ).
fof(f180,plain,
! [X2,X0,X1] : mult(mult(X1,X0),X2) = mult(X1,mult(rd(X0,X1),mult(X1,X2))),
inference(superposition,[],[f7,f3]) ).
fof(f182,plain,
! [X0] : ld(op_c,X0) = mult(sF1,ld(op_c,ld(sF1,X0))),
inference(superposition,[],[f89,f1]) ).
fof(f183,plain,
ld(op_c,sF1) = mult(sF1,ld(op_c,unit)),
inference(superposition,[],[f89,f5]) ).
fof(f188,plain,
ld(op_c,sF1) = mult(sF1,sF1),
inference(forward_demodulation,[],[f183,f70]) ).
fof(f190,plain,
sF0 = mult(sF1,sF1),
inference(forward_demodulation,[],[f188,f53]) ).
fof(f192,plain,
ld(op_c,sF0) = mult(sF1,ld(op_c,sF1)),
inference(superposition,[],[f89,f190]) ).
fof(f194,plain,
i(sF1) = mult(sF1,i(sF0)),
inference(superposition,[],[f128,f190]) ).
fof(f196,plain,
! [X0] : mult(sF1,mult(sF1,mult(sF1,X0))) = mult(mult(sF1,sF0),X0),
inference(superposition,[],[f7,f190]) ).
fof(f197,plain,
ld(op_c,sF0) = mult(sF1,sF0),
inference(forward_demodulation,[],[f192,f53]) ).
fof(f198,plain,
op_c = mult(sF1,sF0),
inference(forward_demodulation,[],[f197,f52]) ).
fof(f199,plain,
! [X0] : mult(op_c,X0) = mult(sF1,mult(sF1,mult(sF1,X0))),
inference(backward_demodulation,[],[f196,f198]) ).
fof(f200,plain,
mult(sF1,ld(op_c,sF0)) = ld(op_c,op_c),
inference(superposition,[],[f89,f198]) ).
fof(f202,plain,
i(sF0) = mult(sF1,i(op_c)),
inference(superposition,[],[f128,f198]) ).
fof(f204,plain,
! [X0] : mult(sF0,mult(sF1,mult(sF0,X0))) = mult(mult(sF0,op_c),X0),
inference(superposition,[],[f7,f198]) ).
fof(f205,plain,
mult(sF1,sF1) = i(sF0),
inference(forward_demodulation,[],[f202,f115]) ).
fof(f206,plain,
unit = mult(sF1,ld(op_c,sF0)),
inference(forward_demodulation,[],[f200,f57]) ).
fof(f207,plain,
sF0 = i(sF0),
inference(forward_demodulation,[],[f205,f190]) ).
fof(f208,plain,
unit = mult(sF1,op_c),
inference(forward_demodulation,[],[f206,f52]) ).
fof(f209,plain,
mult(sF1,sF0) = i(sF1),
inference(backward_demodulation,[],[f194,f207]) ).
fof(f212,plain,
op_c = i(sF1),
inference(forward_demodulation,[],[f209,f198]) ).
fof(f216,plain,
! [X0] : i(mult(X0,sF0)) = ld(X0,sF0),
inference(superposition,[],[f116,f207]) ).
fof(f217,plain,
! [X0] : i(mult(X0,op_c)) = ld(X0,sF1),
inference(superposition,[],[f116,f115]) ).
fof(f218,plain,
! [X0] : i(mult(X0,op_d)) = ld(X0,sF3),
inference(superposition,[],[f116,f114]) ).
fof(f223,plain,
! [X0] : mult(sF1,ld(op_c,X0)) = mult(sF1,mult(sF1,X0)),
inference(superposition,[],[f86,f1]) ).
fof(f229,plain,
! [X0] : mult(sF1,mult(op_c,X0)) = ld(sF1,mult(sF1,X0)),
inference(superposition,[],[f2,f86]) ).
fof(f231,plain,
! [X0] : mult(sF1,mult(op_c,X0)) = X0,
inference(forward_demodulation,[],[f229,f2]) ).
fof(f236,plain,
! [X0] : mult(op_c,mult(op_c,X0)) = mult(sF1,mult(sF1,X0)),
inference(backward_demodulation,[],[f81,f223]) ).
fof(f237,plain,
! [X0] : ld(op_c,X0) = mult(sF1,mult(sF1,ld(sF1,X0))),
inference(backward_demodulation,[],[f182,f223]) ).
fof(f240,plain,
! [X0] : mult(op_c,mult(sF1,X0)) = X0,
inference(backward_demodulation,[],[f83,f231]) ).
fof(f242,plain,
! [X0] : mult(sF1,X0) = ld(op_c,X0),
inference(forward_demodulation,[],[f237,f1]) ).
fof(f247,plain,
op_d = mult(sF1,sF5),
inference(backward_demodulation,[],[f51,f242]) ).
fof(f253,plain,
! [X0] : i(mult(op_c,X0)) = mult(sF1,i(X0)),
inference(superposition,[],[f116,f242]) ).
fof(f256,plain,
! [X0] : mult(op_c,X0) = ld(sF1,X0),
inference(superposition,[],[f240,f1]) ).
fof(f279,plain,
! [X0] : mult(op_d,mult(op_d,X0)) = ld(op_d,X0),
inference(superposition,[],[f2,f49]) ).
fof(f318,plain,
! [X0] : i(i(X0)) = X0,
inference(superposition,[],[f3,f178]) ).
fof(f319,plain,
! [X0,X1] : rd(X1,X0) = rd(i(X0),i(X1)),
inference(superposition,[],[f4,f178]) ).
fof(f322,plain,
! [X2,X0,X1] : mult(i(X1),mult(rd(X1,X0),mult(i(X1),X2))) = mult(mult(i(X1),i(X0)),X2),
inference(superposition,[],[f7,f178]) ).
fof(f323,plain,
! [X2,X0,X1] : mult(i(X1),mult(rd(X1,X0),mult(i(X1),X2))) = mult(ld(X1,i(X0)),X2),
inference(forward_demodulation,[],[f322,f99]) ).
fof(f332,plain,
! [X2,X0,X1] : mult(i(mult(X1,X0)),X2) = mult(i(X1),mult(rd(X1,X0),mult(i(X1),X2))),
inference(forward_demodulation,[],[f323,f116]) ).
fof(f336,plain,
! [X2,X0,X1] : mult(i(mult(X1,X0)),X2) = ld(X1,mult(rd(X1,X0),mult(i(X1),X2))),
inference(forward_demodulation,[],[f332,f99]) ).
fof(f337,plain,
! [X2,X0,X1] : mult(i(mult(X1,X0)),X2) = ld(X1,mult(rd(X1,X0),ld(X1,X2))),
inference(forward_demodulation,[],[f336,f99]) ).
fof(f338,plain,
! [X2,X0,X1] : ld(mult(X1,X0),X2) = ld(X1,mult(rd(X1,X0),ld(X1,X2))),
inference(forward_demodulation,[],[f337,f99]) ).
fof(f340,plain,
op_d = i(sF3),
inference(superposition,[],[f318,f114]) ).
fof(f344,plain,
! [X0,X1] : ld(X1,X0) = i(mult(X1,i(X0))),
inference(superposition,[],[f116,f318]) ).
fof(f346,plain,
op_d = mult(op_d,i(unit)),
inference(backward_demodulation,[],[f140,f340]) ).
fof(f349,plain,
i(unit) = ld(op_d,op_d),
inference(superposition,[],[f2,f346]) ).
fof(f352,plain,
unit = i(unit),
inference(forward_demodulation,[],[f349,f57]) ).
fof(f359,plain,
! [X0] : unit = mult(X0,i(X0)),
inference(backward_demodulation,[],[f130,f352]) ).
fof(f406,plain,
! [X2,X0,X1] : i(mult(X2,ld(X0,X1))) = ld(X2,mult(X0,i(X1))),
inference(superposition,[],[f116,f129]) ).
fof(f412,plain,
i(sF6) = ld(op_d,sF1),
inference(superposition,[],[f2,f151]) ).
fof(f430,plain,
! [X0] : mult(op_c,mult(X0,op_c)) = rd(mult(op_c,mult(X0,unit)),sF1),
inference(superposition,[],[f168,f32]) ).
fof(f434,plain,
! [X0] : mult(op_d,mult(X0,op_d)) = rd(mult(op_d,mult(X0,unit)),sF3),
inference(superposition,[],[f168,f33]) ).
fof(f439,plain,
! [X2,X0,X1] : mult(X1,mult(rd(X0,mult(X1,X2)),X1)) = rd(mult(X1,X0),X2),
inference(superposition,[],[f168,f3]) ).
fof(f455,plain,
! [X0] : mult(op_d,mult(X0,op_d)) = rd(mult(op_d,X0),sF3),
inference(forward_demodulation,[],[f434,f5]) ).
fof(f456,plain,
! [X0] : mult(op_c,mult(X0,op_c)) = rd(mult(op_c,X0),sF1),
inference(forward_demodulation,[],[f430,f5]) ).
fof(f469,plain,
mult(op_c,mult(op_d,op_c)) = rd(sF5,sF1),
inference(superposition,[],[f456,f28]) ).
fof(f473,plain,
mult(op_c,mult(unit,op_c)) = rd(op_c,sF1),
inference(superposition,[],[f456,f5]) ).
fof(f486,plain,
mult(op_c,op_c) = rd(op_c,sF1),
inference(forward_demodulation,[],[f473,f6]) ).
fof(f490,plain,
mult(op_c,sF6) = rd(sF5,sF1),
inference(forward_demodulation,[],[f469,f30]) ).
fof(f494,plain,
sF0 = rd(op_c,sF1),
inference(forward_demodulation,[],[f486,f16]) ).
fof(f499,plain,
op_c = mult(sF0,sF1),
inference(superposition,[],[f3,f494]) ).
fof(f500,plain,
! [X0] : mult(op_c,X0) = mult(sF0,mult(op_c,mult(sF0,X0))),
inference(backward_demodulation,[],[f43,f499]) ).
fof(f512,plain,
! [X0] : mult(op_c,mult(sF0,X0)) = ld(sF0,mult(op_c,X0)),
inference(superposition,[],[f2,f500]) ).
fof(f529,plain,
mult(op_d,mult(unit,op_d)) = rd(op_d,sF3),
inference(superposition,[],[f455,f5]) ).
fof(f542,plain,
mult(op_d,op_d) = rd(op_d,sF3),
inference(forward_demodulation,[],[f529,f6]) ).
fof(f549,plain,
sF3 = rd(op_d,sF3),
inference(forward_demodulation,[],[f542,f23]) ).
fof(f554,plain,
op_d = mult(sF3,sF3),
inference(superposition,[],[f3,f549]) ).
fof(f557,plain,
mult(op_c,sF1) = mult(sF0,mult(op_c,op_c)),
inference(superposition,[],[f500,f499]) ).
fof(f562,plain,
! [X0] : mult(sF1,mult(sF0,mult(sF1,X0))) = mult(mult(sF1,op_c),X0),
inference(superposition,[],[f7,f499]) ).
fof(f563,plain,
! [X0] : mult(unit,X0) = mult(sF1,mult(sF0,mult(sF1,X0))),
inference(forward_demodulation,[],[f562,f208]) ).
fof(f565,plain,
mult(op_c,sF1) = mult(sF0,sF0),
inference(forward_demodulation,[],[f557,f16]) ).
fof(f566,plain,
! [X0] : mult(sF1,mult(sF0,mult(sF1,X0))) = X0,
inference(forward_demodulation,[],[f563,f6]) ).
fof(f568,plain,
unit = mult(sF0,sF0),
inference(forward_demodulation,[],[f565,f32]) ).
fof(f569,plain,
mult(op_c,sF0) = mult(sF0,mult(op_c,unit)),
inference(superposition,[],[f500,f568]) ).
fof(f574,plain,
! [X0] : mult(sF0,mult(sF0,mult(sF0,X0))) = mult(mult(sF0,unit),X0),
inference(superposition,[],[f7,f568]) ).
fof(f575,plain,
! [X0] : mult(sF0,X0) = mult(sF0,mult(sF0,mult(sF0,X0))),
inference(forward_demodulation,[],[f574,f5]) ).
fof(f580,plain,
mult(op_c,sF0) = mult(sF0,op_c),
inference(forward_demodulation,[],[f569,f5]) ).
fof(f582,plain,
sF1 = mult(sF0,op_c),
inference(forward_demodulation,[],[f580,f18]) ).
fof(f584,plain,
! [X0] : mult(sF1,X0) = mult(sF0,mult(sF1,mult(sF0,X0))),
inference(backward_demodulation,[],[f204,f582]) ).
fof(f625,plain,
! [X0] : mult(sF1,mult(sF0,X0)) = ld(sF0,mult(sF1,X0)),
inference(superposition,[],[f2,f584]) ).
fof(f651,plain,
! [X0] : i(mult(X0,sF3)) = ld(X0,op_d),
inference(superposition,[],[f116,f340]) ).
fof(f672,plain,
unit = mult(sF3,op_d),
inference(superposition,[],[f359,f340]) ).
fof(f675,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,mult(X1,unit)),i(X0)),
inference(superposition,[],[f168,f359]) ).
fof(f696,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,X1),i(X0)),
inference(forward_demodulation,[],[f675,f5]) ).
fof(f754,plain,
! [X0] : mult(sF3,mult(sF3,mult(sF3,X0))) = mult(mult(sF3,op_d),X0),
inference(superposition,[],[f7,f554]) ).
fof(f755,plain,
! [X0] : mult(unit,X0) = mult(sF3,mult(sF3,mult(sF3,X0))),
inference(forward_demodulation,[],[f754,f672]) ).
fof(f757,plain,
! [X0] : mult(sF3,mult(sF3,mult(sF3,X0))) = X0,
inference(forward_demodulation,[],[f755,f6]) ).
fof(f776,plain,
mult(op_d,sF6) = ld(op_d,op_c),
inference(superposition,[],[f279,f30]) ).
fof(f790,plain,
! [X0] : mult(op_d,X0) = ld(op_d,ld(op_d,X0)),
inference(superposition,[],[f2,f279]) ).
fof(f815,plain,
! [X0] : i(X0) = ld(rd(X0,sF0),sF0),
inference(superposition,[],[f216,f3]) ).
fof(f824,plain,
! [X0,X1] : i(mult(X1,mult(X0,sF0))) = ld(X1,ld(X0,sF0)),
inference(superposition,[],[f116,f216]) ).
fof(f839,plain,
! [X0] : rd(X0,sF0) = rd(sF0,i(X0)),
inference(superposition,[],[f165,f815]) ).
fof(f853,plain,
! [X0] : rd(sF0,X0) = rd(i(X0),sF0),
inference(superposition,[],[f839,f318]) ).
fof(f855,plain,
rd(op_d,sF0) = rd(sF0,sF3),
inference(superposition,[],[f839,f114]) ).
fof(f857,plain,
rd(sF3,sF0) = rd(sF0,op_d),
inference(superposition,[],[f839,f340]) ).
fof(f950,plain,
! [X0,X1] : rd(X1,i(X0)) = rd(X0,i(X1)),
inference(superposition,[],[f319,f318]) ).
fof(f951,plain,
! [X0] : rd(X0,op_c) = rd(sF1,i(X0)),
inference(superposition,[],[f319,f115]) ).
fof(f952,plain,
! [X0] : rd(X0,op_d) = rd(sF3,i(X0)),
inference(superposition,[],[f319,f114]) ).
fof(f955,plain,
! [X0] : rd(X0,sF3) = rd(op_d,i(X0)),
inference(superposition,[],[f319,f340]) ).
fof(f977,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = rd(X0,i(mult(X0,X1))),
inference(backward_demodulation,[],[f696,f950]) ).
fof(f1001,plain,
! [X0] : rd(mult(X0,sF0),sF3) = rd(op_d,ld(X0,sF0)),
inference(superposition,[],[f955,f216]) ).
fof(f1016,plain,
! [X0,X1] : rd(X1,i(X0)) = mult(X1,mult(ld(X1,X0),X1)),
inference(superposition,[],[f977,f1]) ).
fof(f1017,plain,
! [X0] : mult(X0,mult(unit,X0)) = rd(X0,i(X0)),
inference(superposition,[],[f977,f5]) ).
fof(f1021,plain,
! [X0,X1] : mult(rd(X0,X1),mult(X1,rd(X0,X1))) = rd(rd(X0,X1),i(X0)),
inference(superposition,[],[f977,f3]) ).
fof(f1089,plain,
! [X0,X1] : mult(rd(X0,X1),mult(X1,rd(X0,X1))) = rd(X0,i(rd(X0,X1))),
inference(forward_demodulation,[],[f1021,f950]) ).
fof(f1093,plain,
! [X0] : mult(X0,X0) = rd(X0,i(X0)),
inference(forward_demodulation,[],[f1017,f6]) ).
fof(f1266,plain,
! [X0,X1] : mult(ld(X0,X1),X0) = ld(X0,rd(X0,i(X1))),
inference(superposition,[],[f2,f1016]) ).
fof(f1277,plain,
! [X0] : mult(ld(sF1,X0),sF1) = mult(op_c,rd(sF1,i(X0))),
inference(superposition,[],[f240,f1016]) ).
fof(f1278,plain,
! [X0] : mult(ld(sF1,X0),sF1) = mult(op_c,rd(X0,op_c)),
inference(forward_demodulation,[],[f1277,f951]) ).
fof(f1302,plain,
! [X0] : mult(mult(op_c,X0),sF1) = mult(op_c,rd(X0,op_c)),
inference(forward_demodulation,[],[f1278,f256]) ).
fof(f1336,plain,
! [X0,X1] : ld(X1,rd(X1,X0)) = mult(ld(X1,i(X0)),X1),
inference(superposition,[],[f1266,f318]) ).
fof(f1378,plain,
! [X0,X1] : mult(i(mult(X1,X0)),X1) = ld(X1,rd(X1,X0)),
inference(forward_demodulation,[],[f1336,f116]) ).
fof(f1392,plain,
! [X0,X1] : ld(mult(X1,X0),X1) = ld(X1,rd(X1,X0)),
inference(forward_demodulation,[],[f1378,f99]) ).
fof(f1495,plain,
! [X0] : mult(sF0,mult(sF0,X0)) = X0,
inference(superposition,[],[f575,f1]) ).
fof(f1524,plain,
! [X2,X0,X1] : ld(ld(X0,X1),X2) = mult(mult(X0,i(X1)),X2),
inference(superposition,[],[f99,f129]) ).
fof(f1525,plain,
! [X0,X1] : ld(mult(X0,sF0),X1) = mult(ld(X0,sF0),X1),
inference(superposition,[],[f99,f216]) ).
fof(f1530,plain,
! [X0] : mult(sF3,X0) = ld(op_d,X0),
inference(superposition,[],[f99,f114]) ).
fof(f1531,plain,
! [X0] : mult(sF0,X0) = ld(sF0,X0),
inference(superposition,[],[f99,f207]) ).
fof(f1533,plain,
! [X0] : mult(op_d,X0) = ld(sF3,X0),
inference(superposition,[],[f99,f340]) ).
fof(f1541,plain,
! [X0,X1] : i(X0) = rd(ld(X0,X1),X1),
inference(superposition,[],[f4,f99]) ).
fof(f1544,plain,
! [X2,X0,X1] : mult(X1,mult(i(X0),mult(X1,X2))) = mult(mult(X1,ld(X0,X1)),X2),
inference(superposition,[],[f7,f99]) ).
fof(f1546,plain,
! [X2,X0,X1] : mult(i(X0),mult(X1,mult(i(X0),X2))) = mult(ld(X0,mult(X1,i(X0))),X2),
inference(superposition,[],[f7,f99]) ).
fof(f1560,plain,
! [X2,X0,X1] : mult(i(X0),mult(X1,mult(i(X0),X2))) = mult(i(mult(X0,ld(X1,X0))),X2),
inference(forward_demodulation,[],[f1546,f406]) ).
fof(f1562,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X0,X1)),X2) = mult(X1,ld(X0,mult(X1,X2))),
inference(forward_demodulation,[],[f1544,f99]) ).
fof(f1578,plain,
! [X0] : mult(op_c,mult(sF0,X0)) = mult(sF0,mult(op_c,X0)),
inference(backward_demodulation,[],[f512,f1531]) ).
fof(f1579,plain,
! [X0] : mult(sF1,mult(sF0,X0)) = mult(sF0,mult(sF1,X0)),
inference(backward_demodulation,[],[f625,f1531]) ).
fof(f1584,plain,
! [X0] : mult(op_d,mult(op_d,X0)) = mult(sF3,X0),
inference(backward_demodulation,[],[f279,f1530]) ).
fof(f1588,plain,
! [X0] : mult(op_d,X0) = ld(op_d,mult(sF3,X0)),
inference(backward_demodulation,[],[f790,f1530]) ).
fof(f1592,plain,
mult(op_d,sF6) = mult(sF3,op_c),
inference(backward_demodulation,[],[f776,f1530]) ).
fof(f1593,plain,
i(sF6) = mult(sF3,sF1),
inference(backward_demodulation,[],[f412,f1530]) ).
fof(f1595,plain,
op_c = mult(sF3,sF6),
inference(backward_demodulation,[],[f54,f1530]) ).
fof(f1603,plain,
! [X2,X0,X1] : mult(i(X0),mult(X1,mult(i(X0),X2))) = ld(mult(X0,ld(X1,X0)),X2),
inference(forward_demodulation,[],[f1560,f99]) ).
fof(f1616,plain,
! [X0] : mult(sF0,mult(sF1,mult(sF1,X0))) = X0,
inference(backward_demodulation,[],[f566,f1579]) ).
fof(f1630,plain,
! [X0] : mult(op_d,X0) = mult(sF3,mult(sF3,X0)),
inference(forward_demodulation,[],[f1588,f1530]) ).
fof(f1633,plain,
! [X2,X0,X1] : ld(X0,mult(X1,mult(i(X0),X2))) = ld(mult(X0,ld(X1,X0)),X2),
inference(forward_demodulation,[],[f1603,f99]) ).
fof(f1644,plain,
! [X0] : mult(op_d,mult(sF3,X0)) = X0,
inference(backward_demodulation,[],[f757,f1630]) ).
fof(f1647,plain,
! [X2,X0,X1] : ld(X0,mult(X1,ld(X0,X2))) = ld(mult(X0,ld(X1,X0)),X2),
inference(forward_demodulation,[],[f1633,f99]) ).
fof(f1661,plain,
! [X0] : i(mult(sF0,X0)) = mult(sF0,i(X0)),
inference(superposition,[],[f116,f1531]) ).
fof(f1677,plain,
! [X0] : i(mult(op_d,X0)) = mult(sF3,i(X0)),
inference(superposition,[],[f129,f1533]) ).
fof(f1679,plain,
! [X0] : mult(sF3,mult(op_d,X0)) = X0,
inference(superposition,[],[f1,f1533]) ).
fof(f1681,plain,
! [X0] : mult(ld(sF3,X0),sF3) = mult(op_d,rd(sF3,i(X0))),
inference(superposition,[],[f1266,f1533]) ).
fof(f1685,plain,
! [X0] : mult(ld(sF3,X0),sF3) = mult(op_d,rd(X0,op_d)),
inference(forward_demodulation,[],[f1681,f952]) ).
fof(f1690,plain,
! [X0] : mult(mult(op_d,X0),sF3) = mult(op_d,rd(X0,op_d)),
inference(forward_demodulation,[],[f1685,f1533]) ).
fof(f1716,plain,
! [X0,X1] : i(X1) = rd(X0,mult(X1,X0)),
inference(superposition,[],[f1541,f2]) ).
fof(f1762,plain,
! [X0,X1] : rd(X1,X0) = i(rd(X0,X1)),
inference(superposition,[],[f1716,f3]) ).
fof(f1813,plain,
! [X0,X1] : mult(rd(X0,X1),mult(X1,rd(X0,X1))) = rd(X0,rd(X1,X0)),
inference(backward_demodulation,[],[f1089,f1762]) ).
fof(f1881,plain,
mult(op_d,sF1) = mult(sF3,i(sF6)),
inference(superposition,[],[f1584,f151]) ).
fof(f1935,plain,
! [X0] : rd(sF3,mult(op_d,X0)) = i(mult(op_d,mult(X0,op_d))),
inference(superposition,[],[f1762,f455]) ).
fof(f1954,plain,
rd(sF1,sF5) = i(mult(op_c,sF6)),
inference(superposition,[],[f1762,f490]) ).
fof(f1958,plain,
! [X2,X0,X1] : ld(rd(X1,X0),X2) = mult(rd(X0,X1),X2),
inference(superposition,[],[f99,f1762]) ).
fof(f1962,plain,
! [X2,X0,X1] : rd(X2,rd(X1,X0)) = rd(rd(X0,X1),i(X2)),
inference(superposition,[],[f319,f1762]) ).
fof(f1978,plain,
rd(sF1,sF5) = mult(sF1,i(sF6)),
inference(forward_demodulation,[],[f1954,f253]) ).
fof(f1997,plain,
! [X0] : rd(sF3,mult(op_d,X0)) = mult(sF3,i(mult(X0,op_d))),
inference(forward_demodulation,[],[f1935,f1677]) ).
fof(f2002,plain,
! [X0] : rd(sF3,mult(op_d,X0)) = mult(sF3,ld(X0,sF3)),
inference(forward_demodulation,[],[f1997,f218]) ).
fof(f2033,plain,
! [X0] : mult(rd(sF1,sF5),X0) = ld(mult(op_c,sF6),X0),
inference(superposition,[],[f1958,f490]) ).
fof(f2049,plain,
! [X2,X0,X1] : mult(rd(X0,X1),i(X2)) = i(mult(rd(X1,X0),X2)),
inference(superposition,[],[f116,f1958]) ).
fof(f2605,plain,
! [X0] : mult(op_c,mult(sF0,X0)) = mult(sF1,mult(sF1,mult(sF0,mult(sF1,X0)))),
inference(superposition,[],[f199,f1579]) ).
fof(f2625,plain,
! [X0] : mult(op_c,mult(sF0,X0)) = mult(sF1,mult(sF0,mult(sF1,mult(sF1,X0)))),
inference(forward_demodulation,[],[f2605,f1579]) ).
fof(f2640,plain,
! [X0] : mult(op_c,mult(sF0,X0)) = mult(sF0,mult(sF1,mult(sF1,mult(sF1,X0)))),
inference(forward_demodulation,[],[f2625,f1579]) ).
fof(f2654,plain,
! [X0] : mult(sF1,X0) = mult(op_c,mult(sF0,X0)),
inference(forward_demodulation,[],[f2640,f1616]) ).
fof(f2660,plain,
! [X0] : mult(sF1,X0) = mult(sF0,mult(op_c,X0)),
inference(backward_demodulation,[],[f1578,f2654]) ).
fof(f2670,plain,
! [X0] : mult(sF0,X0) = mult(sF1,mult(sF1,X0)),
inference(superposition,[],[f2660,f240]) ).
fof(f2671,plain,
mult(sF0,sF3) = mult(sF1,i(sF5)),
inference(superposition,[],[f2660,f152]) ).
fof(f2673,plain,
mult(sF1,op_d) = mult(sF0,sF5),
inference(superposition,[],[f2660,f28]) ).
fof(f2685,plain,
! [X0] : mult(op_c,X0) = ld(sF0,mult(sF1,X0)),
inference(superposition,[],[f2,f2660]) ).
fof(f2695,plain,
! [X0] : mult(op_c,X0) = mult(sF0,mult(sF1,X0)),
inference(forward_demodulation,[],[f2685,f1531]) ).
fof(f2710,plain,
! [X0] : mult(op_c,mult(op_c,X0)) = mult(sF0,X0),
inference(backward_demodulation,[],[f236,f2670]) ).
fof(f4694,plain,
! [X0,X1] : mult(X0,mult(i(X1),X0)) = rd(X0,ld(X0,X1)),
inference(superposition,[],[f977,f344]) ).
fof(f4702,plain,
! [X2,X0,X1] : ld(X2,ld(X0,X1)) = i(mult(X2,mult(X0,i(X1)))),
inference(superposition,[],[f116,f344]) ).
fof(f4742,plain,
! [X0,X1] : mult(X0,ld(X1,X0)) = rd(X0,ld(X0,X1)),
inference(forward_demodulation,[],[f4694,f99]) ).
fof(f4798,plain,
! [X0] : mult(op_c,ld(X0,op_c)) = rd(op_c,mult(sF1,X0)),
inference(superposition,[],[f4742,f242]) ).
fof(f4810,plain,
! [X2,X0,X1] : ld(mult(X0,ld(X1,X0)),X2) = mult(rd(ld(X0,X1),X0),X2),
inference(superposition,[],[f1958,f4742]) ).
fof(f4818,plain,
! [X2,X0,X1] : ld(X0,mult(X1,ld(X0,X2))) = mult(rd(ld(X0,X1),X0),X2),
inference(backward_demodulation,[],[f1647,f4810]) ).
fof(f4837,plain,
! [X2,X0,X1] : ld(mult(X1,X0),X2) = mult(rd(ld(X1,rd(X1,X0)),X1),X2),
inference(backward_demodulation,[],[f338,f4818]) ).
fof(f4959,plain,
! [X0] : rd(mult(X0,sF0),op_d) = rd(sF3,ld(X0,sF0)),
inference(superposition,[],[f952,f216]) ).
fof(f5010,plain,
mult(sF0,i(sF6)) = mult(sF1,rd(sF1,sF5)),
inference(superposition,[],[f2670,f1978]) ).
fof(f5230,plain,
! [X0,X1] : mult(mult(i(X0),op_d),X1) = mult(i(X0),mult(rd(X0,sF3),mult(i(X0),X1))),
inference(superposition,[],[f180,f955]) ).
fof(f5243,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X1,X0)) = mult(X1,mult(rd(X2,X1),X0)),
inference(superposition,[],[f180,f1]) ).
fof(f5246,plain,
! [X2,X3,X0,X1] : mult(mult(X0,X3),mult(rd(X1,X0),mult(X0,X2))) = mult(X0,mult(rd(X3,X0),mult(mult(X0,X1),X2))),
inference(superposition,[],[f180,f180]) ).
fof(f5314,plain,
! [X2,X0,X1] : ld(X0,mult(mult(X0,X1),X2)) = mult(rd(X1,X0),mult(X0,X2)),
inference(superposition,[],[f2,f180]) ).
fof(f5337,plain,
! [X0,X1] : mult(sF3,mult(mult(op_d,X0),X1)) = mult(rd(X0,op_d),mult(op_d,X1)),
inference(superposition,[],[f1679,f180]) ).
fof(f5347,plain,
! [X0,X1] : mult(op_c,mult(mult(sF1,X0),X1)) = mult(rd(X0,sF1),mult(sF1,X1)),
inference(superposition,[],[f240,f180]) ).
fof(f5367,plain,
! [X2,X0,X1] : mult(mult(mult(X1,X0),X0),X2) = mult(mult(X1,X0),mult(rd(X0,X1),mult(X1,X2))),
inference(backward_demodulation,[],[f118,f5314]) ).
fof(f5420,plain,
! [X0,X1] : mult(mult(i(X0),op_d),X1) = ld(X0,mult(rd(X0,sF3),mult(i(X0),X1))),
inference(forward_demodulation,[],[f5230,f99]) ).
fof(f5454,plain,
! [X2,X0,X1] : mult(mult(mult(X1,X0),X0),X2) = mult(X1,mult(rd(X0,X1),mult(mult(X1,X0),X2))),
inference(forward_demodulation,[],[f5367,f5246]) ).
fof(f5484,plain,
! [X0,X1] : mult(mult(i(X0),op_d),X1) = ld(X0,mult(rd(X0,sF3),ld(X0,X1))),
inference(forward_demodulation,[],[f5420,f99]) ).
fof(f5520,plain,
! [X0,X1] : mult(mult(i(X0),op_d),X1) = mult(rd(ld(X0,rd(X0,sF3)),X0),X1),
inference(forward_demodulation,[],[f5484,f4818]) ).
fof(f5544,plain,
! [X0,X1] : mult(mult(i(X0),op_d),X1) = ld(mult(X0,sF3),X1),
inference(forward_demodulation,[],[f5520,f4837]) ).
fof(f5557,plain,
! [X0,X1] : ld(mult(X0,sF3),X1) = mult(ld(X0,op_d),X1),
inference(forward_demodulation,[],[f5544,f99]) ).
fof(f5708,plain,
mult(op_d,mult(sF6,op_d)) = rd(mult(sF3,op_c),sF3),
inference(superposition,[],[f455,f1592]) ).
fof(f5717,plain,
i(op_d) = rd(sF6,mult(sF3,op_c)),
inference(superposition,[],[f1716,f1592]) ).
fof(f5718,plain,
sF3 = rd(sF6,mult(sF3,op_c)),
inference(forward_demodulation,[],[f5717,f114]) ).
fof(f6977,plain,
! [X0,X1] : rd(mult(X0,sF3),i(X1)) = rd(X1,ld(X0,op_d)),
inference(superposition,[],[f950,f651]) ).
fof(f7236,plain,
! [X0,X1] : mult(rd(X0,sF3),mult(sF3,X1)) = mult(op_d,mult(mult(sF3,X0),X1)),
inference(superposition,[],[f1644,f180]) ).
fof(f7550,plain,
! [X0] : rd(mult(X0,op_c),sF3) = rd(op_d,ld(X0,sF1)),
inference(superposition,[],[f955,f217]) ).
fof(f7554,plain,
! [X0] : mult(mult(X0,op_c),mult(X0,op_c)) = rd(mult(X0,op_c),ld(X0,sF1)),
inference(superposition,[],[f1093,f217]) ).
fof(f7565,plain,
mult(op_d,mult(sF6,op_d)) = rd(op_d,ld(sF3,sF1)),
inference(backward_demodulation,[],[f5708,f7550]) ).
fof(f7597,plain,
mult(op_d,mult(sF6,op_d)) = rd(op_d,mult(op_d,sF1)),
inference(forward_demodulation,[],[f7565,f1533]) ).
fof(f8632,plain,
! [X0] : mult(mult(X0,op_d),mult(X0,op_d)) = rd(mult(X0,op_d),ld(X0,sF3)),
inference(superposition,[],[f1093,f218]) ).
fof(f8695,plain,
sF1 = rd(mult(sF0,sF3),i(sF5)),
inference(superposition,[],[f4,f2671]) ).
fof(f8702,plain,
ld(sF1,rd(sF1,i(sF5))) = ld(mult(sF0,sF3),sF1),
inference(superposition,[],[f1392,f2671]) ).
fof(f8711,plain,
ld(sF1,rd(sF1,i(sF5))) = mult(ld(sF0,op_d),sF1),
inference(forward_demodulation,[],[f8702,f5557]) ).
fof(f8718,plain,
sF1 = rd(sF5,ld(sF0,op_d)),
inference(forward_demodulation,[],[f8695,f6977]) ).
fof(f8730,plain,
ld(sF1,rd(sF1,i(sF5))) = mult(mult(sF0,op_d),sF1),
inference(forward_demodulation,[],[f8711,f1531]) ).
fof(f8736,plain,
sF1 = rd(sF5,mult(sF0,op_d)),
inference(forward_demodulation,[],[f8718,f1531]) ).
fof(f8745,plain,
mult(mult(sF0,op_d),sF1) = mult(ld(sF1,sF5),sF1),
inference(forward_demodulation,[],[f8730,f1266]) ).
fof(f8757,plain,
mult(mult(sF0,op_d),sF1) = mult(mult(op_c,sF5),sF1),
inference(forward_demodulation,[],[f8745,f256]) ).
fof(f8764,plain,
mult(mult(sF0,op_d),sF1) = mult(op_c,rd(sF5,op_c)),
inference(forward_demodulation,[],[f8757,f1302]) ).
fof(f9358,plain,
! [X2,X3,X0,X1] : rd(X3,mult(X0,mult(X1,i(X2)))) = rd(ld(X0,ld(X1,X2)),i(X3)),
inference(superposition,[],[f319,f4702]) ).
fof(f9869,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = i(mult(X0,mult(X0,i(X1)))),
inference(superposition,[],[f344,f68]) ).
fof(f9883,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = ld(X0,ld(X0,X1)),
inference(forward_demodulation,[],[f9869,f4702]) ).
fof(f10329,plain,
! [X2,X0,X1] : rd(mult(X0,mult(X1,sF0)),X2) = rd(i(X2),ld(X0,ld(X1,sF0))),
inference(superposition,[],[f319,f824]) ).
fof(f20830,plain,
! [X2,X0,X1] : rd(mult(X1,X2),ld(X1,X0)) = mult(X1,mult(rd(X2,X0),X1)),
inference(superposition,[],[f439,f1]) ).
fof(f20932,plain,
mult(sF0,mult(sF1,sF0)) = rd(mult(sF0,sF5),op_d),
inference(superposition,[],[f439,f8736]) ).
fof(f20968,plain,
! [X2,X0,X1] : mult(rd(X1,mult(X0,X2)),X0) = ld(X0,rd(mult(X0,X1),X2)),
inference(superposition,[],[f2,f439]) ).
fof(f21097,plain,
mult(op_c,sF0) = rd(mult(sF0,sF5),op_d),
inference(forward_demodulation,[],[f20932,f2695]) ).
fof(f21214,plain,
! [X0] : mult(mult(X0,op_c),mult(X0,op_c)) = mult(X0,mult(rd(op_c,sF1),X0)),
inference(backward_demodulation,[],[f7554,f20830]) ).
fof(f21215,plain,
! [X0] : mult(mult(X0,op_d),mult(X0,op_d)) = mult(X0,mult(rd(op_d,sF3),X0)),
inference(backward_demodulation,[],[f8632,f20830]) ).
fof(f21263,plain,
sF1 = rd(mult(sF0,sF5),op_d),
inference(forward_demodulation,[],[f21097,f18]) ).
fof(f21302,plain,
! [X0] : mult(X0,mult(sF3,X0)) = mult(mult(X0,op_d),mult(X0,op_d)),
inference(forward_demodulation,[],[f21215,f549]) ).
fof(f21303,plain,
! [X0] : mult(X0,mult(sF0,X0)) = mult(mult(X0,op_c),mult(X0,op_c)),
inference(forward_demodulation,[],[f21214,f494]) ).
fof(f21502,plain,
i(sF1) = rd(op_d,mult(sF0,sF5)),
inference(superposition,[],[f1762,f21263]) ).
fof(f21517,plain,
op_c = rd(op_d,mult(sF0,sF5)),
inference(forward_demodulation,[],[f21502,f212]) ).
fof(f21580,plain,
mult(op_d,mult(sF0,op_d)) = mult(sF6,sF6),
inference(superposition,[],[f21303,f30]) ).
fof(f21589,plain,
! [X0,X1] : mult(mult(X0,mult(sF0,X0)),X1) = mult(mult(X0,op_c),mult(mult(X0,op_c),X1)),
inference(superposition,[],[f68,f21303]) ).
fof(f21612,plain,
! [X0,X1] : mult(X0,mult(sF0,mult(X0,X1))) = mult(mult(X0,op_c),mult(mult(X0,op_c),X1)),
inference(forward_demodulation,[],[f21589,f7]) ).
fof(f21734,plain,
! [X0] : mult(op_c,mult(rd(op_d,X0),op_c)) = rd(sF5,ld(op_c,X0)),
inference(superposition,[],[f20830,f28]) ).
fof(f21743,plain,
! [X0] : mult(op_d,mult(rd(op_d,X0),op_d)) = rd(sF3,ld(op_d,X0)),
inference(superposition,[],[f20830,f23]) ).
fof(f21893,plain,
! [X0] : rd(sF3,mult(sF3,X0)) = mult(op_d,mult(rd(op_d,X0),op_d)),
inference(forward_demodulation,[],[f21743,f1530]) ).
fof(f21902,plain,
! [X0] : mult(op_c,mult(rd(op_d,X0),op_c)) = rd(sF5,mult(sF1,X0)),
inference(forward_demodulation,[],[f21734,f242]) ).
fof(f22539,plain,
! [X0,X1] : mult(rd(X1,mult(X0,i(mult(X0,X1)))),X0) = ld(X0,mult(mult(X0,X1),mult(X0,X1))),
inference(superposition,[],[f20968,f1093]) ).
fof(f22609,plain,
! [X0,X1] : mult(rd(X1,mult(X0,i(mult(X0,X1)))),X0) = mult(rd(X1,X0),mult(X0,mult(X0,X1))),
inference(forward_demodulation,[],[f22539,f5314]) ).
fof(f22724,plain,
! [X0,X1] : mult(rd(X1,X0),mult(X0,mult(X0,X1))) = mult(rd(X1,i(X1)),X0),
inference(forward_demodulation,[],[f22609,f128]) ).
fof(f22817,plain,
! [X0,X1] : mult(mult(X1,X1),X0) = mult(rd(X1,X0),mult(X0,mult(X0,X1))),
inference(forward_demodulation,[],[f22724,f1093]) ).
fof(f22835,plain,
! [X0,X1] : mult(X1,mult(X1,X0)) = mult(rd(X1,X0),mult(X0,mult(X0,X1))),
inference(forward_demodulation,[],[f22817,f68]) ).
fof(f22854,plain,
mult(op_c,mult(sF3,op_c)) = mult(sF5,sF5),
inference(superposition,[],[f21302,f28]) ).
fof(f22862,plain,
! [X0,X1] : mult(mult(X0,mult(sF3,X0)),X1) = mult(mult(X0,op_d),mult(mult(X0,op_d),X1)),
inference(superposition,[],[f68,f21302]) ).
fof(f22889,plain,
! [X0,X1] : mult(X0,mult(sF3,mult(X0,X1))) = mult(mult(X0,op_d),mult(mult(X0,op_d),X1)),
inference(forward_demodulation,[],[f22862,f7]) ).
fof(f26048,plain,
! [X2,X0,X1] : mult(X0,ld(mult(X0,X1),mult(X0,X2))) = mult(mult(X0,ld(X0,rd(X0,X1))),X2),
inference(superposition,[],[f1562,f1392]) ).
fof(f26295,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = mult(X0,ld(mult(X0,X1),mult(X0,X2))),
inference(forward_demodulation,[],[f26048,f1]) ).
fof(f26502,plain,
rd(mult(sF0,sF5),rd(op_d,mult(sF0,sF5))) = mult(sF1,mult(op_d,sF1)),
inference(superposition,[],[f1813,f21263]) ).
fof(f26688,plain,
mult(sF1,mult(op_d,sF1)) = rd(mult(sF0,sF5),op_c),
inference(forward_demodulation,[],[f26502,f21517]) ).
fof(f30888,plain,
! [X0] : mult(mult(mult(sF0,op_d),op_d),X0) = mult(sF0,mult(rd(sF0,sF3),mult(mult(sF0,op_d),X0))),
inference(superposition,[],[f5454,f855]) ).
fof(f33518,plain,
! [X0,X1] : mult(rd(sF0,X1),mult(sF0,X0)) = mult(sF0,ld(mult(sF0,X1),X0)),
inference(superposition,[],[f26295,f1495]) ).
fof(f33574,plain,
! [X2,X0,X1] : ld(X0,mult(rd(X0,X1),X2)) = ld(mult(X0,X1),mult(X0,X2)),
inference(superposition,[],[f2,f26295]) ).
fof(f34605,plain,
! [X0] : ld(mult(sF1,X0),mult(sF0,i(sF6))) = ld(sF1,mult(rd(sF1,X0),rd(sF1,sF5))),
inference(superposition,[],[f33574,f5010]) ).
fof(f34718,plain,
! [X0] : ld(mult(sF1,X0),mult(sF0,i(sF6))) = mult(op_c,mult(rd(sF1,X0),rd(sF1,sF5))),
inference(forward_demodulation,[],[f34605,f256]) ).
fof(f34943,plain,
! [X0] : i(mult(mult(sF1,X0),ld(sF0,sF6))) = mult(op_c,mult(rd(sF1,X0),rd(sF1,sF5))),
inference(forward_demodulation,[],[f34718,f406]) ).
fof(f35101,plain,
! [X0] : i(mult(mult(sF1,X0),mult(sF0,sF6))) = mult(op_c,mult(rd(sF1,X0),rd(sF1,sF5))),
inference(forward_demodulation,[],[f34943,f1531]) ).
fof(f36467,plain,
rd(sF5,mult(sF1,mult(op_d,sF1))) = mult(op_c,mult(mult(op_d,mult(sF6,op_d)),op_c)),
inference(superposition,[],[f21902,f7597]) ).
fof(f36563,plain,
rd(sF5,mult(sF1,mult(op_d,sF1))) = mult(op_c,mult(op_d,mult(sF6,mult(op_d,op_c)))),
inference(forward_demodulation,[],[f36467,f7]) ).
fof(f36590,plain,
rd(sF5,mult(sF1,mult(op_d,sF1))) = mult(op_c,mult(op_d,mult(sF6,sF6))),
inference(forward_demodulation,[],[f36563,f30]) ).
fof(f38715,plain,
mult(op_c,ld(op_d,op_c)) = rd(op_c,mult(sF0,sF5)),
inference(superposition,[],[f4798,f2673]) ).
fof(f38768,plain,
mult(op_c,mult(sF3,op_c)) = rd(op_c,mult(sF0,sF5)),
inference(forward_demodulation,[],[f38715,f1530]) ).
fof(f38788,plain,
rd(op_c,mult(sF0,sF5)) = mult(sF5,sF5),
inference(forward_demodulation,[],[f38768,f22854]) ).
fof(f42250,plain,
! [X0] : rd(mult(sF5,sF5),i(X0)) = rd(X0,rd(mult(sF0,sF5),op_c)),
inference(superposition,[],[f1962,f38788]) ).
fof(f42267,plain,
! [X0] : rd(mult(sF5,sF5),i(X0)) = rd(X0,mult(sF1,mult(op_d,sF1))),
inference(forward_demodulation,[],[f42250,f26688]) ).
fof(f42287,plain,
mult(op_c,mult(op_d,mult(sF6,sF6))) = rd(mult(sF5,sF5),i(sF5)),
inference(backward_demodulation,[],[f36590,f42267]) ).
fof(f42307,plain,
mult(op_c,mult(op_d,mult(sF6,sF6))) = rd(sF5,i(mult(sF5,sF5))),
inference(forward_demodulation,[],[f42287,f950]) ).
fof(f42321,plain,
mult(op_c,mult(op_d,mult(sF6,sF6))) = mult(sF5,mult(sF5,sF5)),
inference(forward_demodulation,[],[f42307,f977]) ).
fof(f47486,plain,
! [X0] : mult(i(X0),mult(i(X0),sF0)) = mult(rd(sF0,X0),mult(sF0,mult(sF0,i(X0)))),
inference(superposition,[],[f22835,f853]) ).
fof(f47525,plain,
mult(sF6,mult(sF6,mult(sF3,op_c))) = mult(sF3,mult(mult(sF3,op_c),mult(mult(sF3,op_c),sF6))),
inference(superposition,[],[f22835,f5718]) ).
fof(f47624,plain,
mult(op_c,mult(op_c,op_d)) = mult(rd(op_c,op_d),mult(op_d,sF6)),
inference(superposition,[],[f22835,f30]) ).
fof(f47644,plain,
mult(i(sF6),mult(i(sF6),sF1)) = mult(rd(i(sF6),sF1),mult(sF1,rd(sF1,sF5))),
inference(superposition,[],[f22835,f1978]) ).
fof(f47662,plain,
mult(sF1,mult(sF1,sF3)) = mult(rd(sF1,sF3),mult(sF3,i(sF6))),
inference(superposition,[],[f22835,f1593]) ).
fof(f47835,plain,
mult(sF1,mult(sF1,sF3)) = mult(op_d,mult(mult(sF3,sF1),i(sF6))),
inference(forward_demodulation,[],[f47662,f7236]) ).
fof(f47853,plain,
mult(i(sF6),mult(i(sF6),sF1)) = mult(op_c,mult(mult(sF1,i(sF6)),rd(sF1,sF5))),
inference(forward_demodulation,[],[f47644,f5347]) ).
fof(f47872,plain,
mult(op_c,mult(op_c,op_d)) = mult(sF3,mult(mult(op_d,op_c),sF6)),
inference(forward_demodulation,[],[f47624,f5337]) ).
fof(f47960,plain,
mult(sF6,mult(sF6,mult(sF3,op_c))) = mult(sF3,mult(sF3,mult(sF0,mult(sF3,sF6)))),
inference(forward_demodulation,[],[f47525,f21612]) ).
fof(f47999,plain,
! [X0] : mult(i(X0),mult(i(X0),sF0)) = mult(sF0,ld(mult(sF0,X0),mult(sF0,i(X0)))),
inference(forward_demodulation,[],[f47486,f33518]) ).
fof(f48079,plain,
mult(sF1,mult(sF1,sF3)) = mult(op_d,mult(i(sF6),i(sF6))),
inference(forward_demodulation,[],[f47835,f1593]) ).
fof(f48097,plain,
mult(i(sF6),mult(i(sF6),sF1)) = mult(op_c,ld(ld(sF1,sF6),rd(sF1,sF5))),
inference(forward_demodulation,[],[f47853,f1524]) ).
fof(f48116,plain,
mult(op_c,mult(op_c,op_d)) = mult(sF3,mult(sF6,sF6)),
inference(forward_demodulation,[],[f47872,f30]) ).
fof(f48187,plain,
mult(sF6,mult(sF6,mult(sF3,op_c))) = mult(op_d,mult(sF0,mult(sF3,sF6))),
inference(forward_demodulation,[],[f47960,f1630]) ).
fof(f48224,plain,
! [X0] : mult(i(X0),mult(i(X0),sF0)) = mult(sF0,i(mult(mult(sF0,X0),ld(sF0,X0)))),
inference(forward_demodulation,[],[f47999,f406]) ).
fof(f48288,plain,
mult(sF1,mult(sF1,sF3)) = mult(op_d,ld(sF6,i(sF6))),
inference(forward_demodulation,[],[f48079,f99]) ).
fof(f48306,plain,
mult(i(sF6),mult(i(sF6),sF1)) = mult(op_c,ld(mult(op_c,sF6),rd(sF1,sF5))),
inference(forward_demodulation,[],[f48097,f256]) ).
fof(f48323,plain,
mult(sF0,op_d) = mult(sF3,mult(sF6,sF6)),
inference(forward_demodulation,[],[f48116,f2710]) ).
fof(f48387,plain,
mult(sF6,mult(sF6,mult(sF3,op_c))) = mult(op_d,mult(sF0,op_c)),
inference(forward_demodulation,[],[f48187,f1595]) ).
fof(f48417,plain,
! [X0] : mult(i(X0),mult(i(X0),sF0)) = mult(sF0,i(mult(sF0,mult(rd(X0,sF0),X0)))),
inference(forward_demodulation,[],[f48224,f5243]) ).
fof(f48469,plain,
mult(sF1,mult(sF1,sF3)) = mult(op_d,i(mult(sF6,sF6))),
inference(forward_demodulation,[],[f48288,f116]) ).
fof(f48484,plain,
mult(i(sF6),mult(i(sF6),sF1)) = mult(op_c,mult(rd(sF1,sF5),rd(sF1,sF5))),
inference(forward_demodulation,[],[f48306,f2033]) ).
fof(f48537,plain,
mult(op_d,sF1) = mult(sF6,mult(sF6,mult(sF3,op_c))),
inference(forward_demodulation,[],[f48387,f582]) ).
fof(f48557,plain,
! [X0] : i(mult(rd(X0,sF0),X0)) = mult(i(X0),mult(i(X0),sF0)),
inference(forward_demodulation,[],[f48417,f128]) ).
fof(f48596,plain,
mult(sF0,sF3) = mult(op_d,i(mult(sF6,sF6))),
inference(forward_demodulation,[],[f48469,f2670]) ).
fof(f48604,plain,
mult(i(sF6),mult(i(sF6),sF1)) = i(mult(mult(sF1,sF5),mult(sF0,sF6))),
inference(forward_demodulation,[],[f48484,f35101]) ).
fof(f48646,plain,
! [X0] : i(mult(rd(X0,sF0),X0)) = ld(X0,mult(i(X0),sF0)),
inference(forward_demodulation,[],[f48557,f99]) ).
fof(f48677,plain,
mult(i(sF6),mult(i(sF6),sF1)) = i(mult(op_d,mult(sF0,sF6))),
inference(forward_demodulation,[],[f48604,f247]) ).
fof(f48710,plain,
! [X0] : i(mult(rd(X0,sF0),X0)) = ld(X0,ld(X0,sF0)),
inference(forward_demodulation,[],[f48646,f99]) ).
fof(f48733,plain,
mult(i(sF6),mult(i(sF6),sF1)) = mult(sF3,i(mult(sF0,sF6))),
inference(forward_demodulation,[],[f48677,f1677]) ).
fof(f48758,plain,
! [X0] : mult(rd(sF0,X0),i(X0)) = ld(X0,ld(X0,sF0)),
inference(forward_demodulation,[],[f48710,f2049]) ).
fof(f48771,plain,
mult(sF3,mult(sF0,i(sF6))) = mult(i(sF6),mult(i(sF6),sF1)),
inference(forward_demodulation,[],[f48733,f1661]) ).
fof(f48800,plain,
mult(sF3,mult(sF0,i(sF6))) = ld(sF6,mult(i(sF6),sF1)),
inference(forward_demodulation,[],[f48771,f99]) ).
fof(f48814,plain,
mult(sF3,mult(sF0,i(sF6))) = ld(sF6,ld(sF6,sF1)),
inference(forward_demodulation,[],[f48800,f99]) ).
fof(f48875,plain,
ld(sF3,ld(sF3,sF0)) = mult(rd(sF0,sF3),op_d),
inference(superposition,[],[f48758,f340]) ).
fof(f48893,plain,
! [X0] : rd(sF0,X0) = rd(ld(X0,ld(X0,sF0)),i(X0)),
inference(superposition,[],[f4,f48758]) ).
fof(f48904,plain,
! [X0] : i(rd(sF0,X0)) = rd(i(X0),ld(X0,ld(X0,sF0))),
inference(superposition,[],[f1716,f48758]) ).
fof(f48929,plain,
! [X0] : i(rd(sF0,X0)) = rd(mult(X0,mult(X0,sF0)),X0),
inference(forward_demodulation,[],[f48904,f10329]) ).
fof(f48939,plain,
! [X0] : rd(sF0,X0) = rd(X0,mult(X0,mult(X0,i(sF0)))),
inference(forward_demodulation,[],[f48893,f9358]) ).
fof(f48957,plain,
mult(op_d,ld(sF3,sF0)) = mult(rd(sF0,sF3),op_d),
inference(forward_demodulation,[],[f48875,f1533]) ).
fof(f49010,plain,
! [X0] : rd(X0,sF0) = rd(mult(X0,mult(X0,sF0)),X0),
inference(forward_demodulation,[],[f48929,f1762]) ).
fof(f49020,plain,
! [X0] : rd(sF0,X0) = rd(X0,mult(X0,mult(X0,sF0))),
inference(forward_demodulation,[],[f48939,f207]) ).
fof(f49038,plain,
mult(op_d,mult(op_d,sF0)) = mult(rd(sF0,sF3),op_d),
inference(forward_demodulation,[],[f48957,f1533]) ).
fof(f49105,plain,
mult(sF3,sF0) = mult(rd(sF0,sF3),op_d),
inference(forward_demodulation,[],[f49038,f1584]) ).
fof(f49260,plain,
rd(op_d,sF0) = rd(mult(sF3,sF0),op_d),
inference(superposition,[],[f49010,f1584]) ).
fof(f49262,plain,
rd(sF3,sF0) = rd(mult(op_d,sF0),sF3),
inference(superposition,[],[f49010,f1630]) ).
fof(f49365,plain,
rd(sF3,sF0) = rd(op_d,ld(op_d,sF0)),
inference(forward_demodulation,[],[f49262,f1001]) ).
fof(f49367,plain,
rd(op_d,sF0) = rd(sF3,ld(sF3,sF0)),
inference(forward_demodulation,[],[f49260,f4959]) ).
fof(f49442,plain,
rd(sF3,sF0) = mult(op_d,ld(sF0,op_d)),
inference(forward_demodulation,[],[f49365,f4742]) ).
fof(f49444,plain,
rd(op_d,sF0) = mult(sF3,ld(sF0,sF3)),
inference(forward_demodulation,[],[f49367,f4742]) ).
fof(f49506,plain,
rd(sF3,sF0) = mult(op_d,mult(sF0,op_d)),
inference(forward_demodulation,[],[f49442,f1531]) ).
fof(f49508,plain,
rd(op_d,sF0) = mult(sF3,mult(sF0,sF3)),
inference(forward_demodulation,[],[f49444,f1531]) ).
fof(f49565,plain,
rd(sF3,sF0) = mult(sF6,sF6),
inference(forward_demodulation,[],[f49506,f21580]) ).
fof(f49566,plain,
rd(sF0,sF3) = mult(sF3,mult(sF0,sF3)),
inference(forward_demodulation,[],[f49508,f855]) ).
fof(f49593,plain,
rd(sF0,op_d) = mult(sF6,sF6),
inference(backward_demodulation,[],[f857,f49565]) ).
fof(f49645,plain,
! [X0] : mult(mult(sF0,sF3),X0) = mult(sF0,mult(mult(sF6,sF6),mult(sF0,X0))),
inference(superposition,[],[f180,f49565]) ).
fof(f49646,plain,
rd(sF0,sF3) = i(mult(sF6,sF6)),
inference(superposition,[],[f1762,f49565]) ).
fof(f49648,plain,
! [X0] : mult(rd(sF0,sF3),X0) = ld(mult(sF6,sF6),X0),
inference(superposition,[],[f1958,f49565]) ).
fof(f49672,plain,
! [X0] : mult(rd(sF0,sF3),X0) = ld(sF6,ld(sF6,X0)),
inference(forward_demodulation,[],[f49648,f9883]) ).
fof(f49674,plain,
mult(sF0,sF3) = mult(op_d,rd(sF0,sF3)),
inference(backward_demodulation,[],[f48596,f49646]) ).
fof(f49678,plain,
! [X0] : mult(mult(sF0,sF3),X0) = mult(sF0,mult(sF6,mult(sF6,mult(sF0,X0)))),
inference(forward_demodulation,[],[f49645,f68]) ).
fof(f49691,plain,
mult(sF3,mult(sF0,i(sF6))) = mult(rd(sF0,sF3),sF1),
inference(backward_demodulation,[],[f48814,f49672]) ).
fof(f49765,plain,
rd(sF3,mult(sF3,mult(op_d,mult(op_d,sF0)))) = mult(op_d,mult(rd(sF0,op_d),op_d)),
inference(superposition,[],[f21893,f49020]) ).
fof(f49825,plain,
mult(op_d,sF0) = rd(sF3,mult(sF3,mult(op_d,mult(op_d,sF0)))),
inference(forward_demodulation,[],[f49765,f3]) ).
fof(f49880,plain,
mult(op_d,sF0) = rd(sF3,mult(op_d,sF0)),
inference(forward_demodulation,[],[f49825,f1679]) ).
fof(f49921,plain,
mult(op_d,sF0) = mult(sF3,ld(sF0,sF3)),
inference(forward_demodulation,[],[f49880,f2002]) ).
fof(f49952,plain,
mult(op_d,sF0) = mult(sF3,mult(sF0,sF3)),
inference(forward_demodulation,[],[f49921,f1531]) ).
fof(f49969,plain,
rd(sF0,sF3) = mult(op_d,sF0),
inference(backward_demodulation,[],[f49566,f49952]) ).
fof(f49985,plain,
! [X0] : mult(mult(mult(sF0,op_d),op_d),X0) = mult(sF0,mult(mult(op_d,sF0),mult(mult(sF0,op_d),X0))),
inference(backward_demodulation,[],[f30888,f49969]) ).
fof(f49987,plain,
mult(sF3,sF0) = mult(mult(op_d,sF0),op_d),
inference(backward_demodulation,[],[f49105,f49969]) ).
fof(f50005,plain,
mult(sF0,sF3) = mult(op_d,mult(op_d,sF0)),
inference(backward_demodulation,[],[f49674,f49969]) ).
fof(f50010,plain,
mult(sF3,mult(sF0,i(sF6))) = mult(mult(op_d,sF0),sF1),
inference(backward_demodulation,[],[f49691,f49969]) ).
fof(f50024,plain,
mult(sF0,sF3) = mult(sF3,sF0),
inference(forward_demodulation,[],[f50005,f1584]) ).
fof(f50047,plain,
mult(sF0,sF3) = mult(mult(op_d,sF0),op_d),
inference(backward_demodulation,[],[f49987,f50024]) ).
fof(f50090,plain,
sF0 = mult(mult(op_d,sF0),sF3),
inference(superposition,[],[f3,f49969]) ).
fof(f50093,plain,
rd(sF3,sF0) = i(mult(op_d,sF0)),
inference(superposition,[],[f1762,f49969]) ).
fof(f50095,plain,
! [X0] : mult(rd(sF3,sF0),X0) = ld(mult(op_d,sF0),X0),
inference(superposition,[],[f1958,f49969]) ).
fof(f50122,plain,
! [X0] : mult(rd(sF3,sF0),X0) = mult(ld(op_d,sF0),X0),
inference(forward_demodulation,[],[f50095,f1525]) ).
fof(f50124,plain,
rd(sF3,sF0) = ld(op_d,sF0),
inference(forward_demodulation,[],[f50093,f216]) ).
fof(f50127,plain,
sF0 = mult(op_d,rd(sF0,op_d)),
inference(forward_demodulation,[],[f50090,f1690]) ).
fof(f50144,plain,
! [X0] : mult(rd(sF3,sF0),X0) = mult(mult(sF3,sF0),X0),
inference(forward_demodulation,[],[f50122,f1530]) ).
fof(f50146,plain,
rd(sF3,sF0) = mult(sF3,sF0),
inference(forward_demodulation,[],[f50124,f1530]) ).
fof(f50149,plain,
sF0 = mult(op_d,mult(sF6,sF6)),
inference(forward_demodulation,[],[f50127,f49593]) ).
fof(f50164,plain,
! [X0] : mult(mult(sF0,sF3),X0) = mult(rd(sF3,sF0),X0),
inference(forward_demodulation,[],[f50144,f50024]) ).
fof(f50166,plain,
rd(sF3,sF0) = mult(sF0,sF3),
inference(forward_demodulation,[],[f50146,f50024]) ).
fof(f50168,plain,
mult(op_c,sF0) = mult(sF5,mult(sF5,sF5)),
inference(backward_demodulation,[],[f42321,f50149]) ).
fof(f50206,plain,
! [X0] : mult(mult(sF0,sF3),X0) = mult(mult(sF6,sF6),X0),
inference(forward_demodulation,[],[f50164,f49565]) ).
fof(f50208,plain,
mult(sF0,sF3) = mult(sF6,sF6),
inference(backward_demodulation,[],[f49565,f50166]) ).
fof(f50227,plain,
sF1 = mult(sF5,mult(sF5,sF5)),
inference(forward_demodulation,[],[f50168,f18]) ).
fof(f50248,plain,
! [X0] : mult(mult(sF0,sF3),X0) = mult(sF6,mult(sF6,X0)),
inference(forward_demodulation,[],[f50206,f68]) ).
fof(f50252,plain,
mult(sF0,op_d) = mult(sF3,mult(sF0,sF3)),
inference(backward_demodulation,[],[f48323,f50208]) ).
fof(f50314,plain,
! [X0] : mult(sF6,mult(sF6,X0)) = mult(sF0,mult(sF6,mult(sF6,mult(sF0,X0)))),
inference(backward_demodulation,[],[f49678,f50248]) ).
fof(f50326,plain,
mult(sF0,op_d) = mult(op_d,sF0),
inference(backward_demodulation,[],[f49952,f50252]) ).
fof(f50382,plain,
! [X0] : mult(mult(mult(sF0,op_d),op_d),X0) = mult(sF0,mult(mult(sF0,op_d),mult(mult(sF0,op_d),X0))),
inference(backward_demodulation,[],[f49985,f50326]) ).
fof(f50389,plain,
mult(mult(sF0,op_d),sF1) = mult(sF3,mult(sF0,i(sF6))),
inference(backward_demodulation,[],[f50010,f50326]) ).
fof(f50390,plain,
mult(sF0,sF3) = mult(mult(sF0,op_d),op_d),
inference(backward_demodulation,[],[f50047,f50326]) ).
fof(f50430,plain,
mult(op_c,rd(sF5,op_c)) = mult(sF3,mult(sF0,i(sF6))),
inference(forward_demodulation,[],[f50389,f8764]) ).
fof(f50432,plain,
! [X0] : mult(mult(mult(sF0,op_d),op_d),X0) = mult(sF0,mult(sF0,mult(sF3,mult(sF0,X0)))),
inference(forward_demodulation,[],[f50382,f22889]) ).
fof(f50469,plain,
! [X0] : mult(sF3,mult(sF0,X0)) = mult(mult(mult(sF0,op_d),op_d),X0),
inference(forward_demodulation,[],[f50432,f1495]) ).
fof(f50498,plain,
! [X0] : mult(mult(sF0,sF3),X0) = mult(sF3,mult(sF0,X0)),
inference(forward_demodulation,[],[f50469,f50390]) ).
fof(f50518,plain,
! [X0] : mult(sF3,mult(sF0,X0)) = mult(sF6,mult(sF6,X0)),
inference(backward_demodulation,[],[f50248,f50498]) ).
fof(f50533,plain,
! [X0] : mult(sF3,mult(sF0,X0)) = mult(sF0,mult(sF6,mult(sF6,mult(sF0,X0)))),
inference(backward_demodulation,[],[f50314,f50518]) ).
fof(f50538,plain,
mult(op_d,sF1) = mult(sF3,mult(sF0,mult(sF3,op_c))),
inference(backward_demodulation,[],[f48537,f50518]) ).
fof(f50560,plain,
! [X0] : mult(sF3,mult(sF0,X0)) = mult(sF0,mult(sF3,mult(sF0,mult(sF0,X0)))),
inference(forward_demodulation,[],[f50533,f50518]) ).
fof(f50569,plain,
! [X0] : mult(sF0,mult(sF3,X0)) = mult(sF3,mult(sF0,X0)),
inference(forward_demodulation,[],[f50560,f1495]) ).
fof(f50584,plain,
mult(op_d,sF1) = mult(sF0,mult(sF3,mult(sF3,op_c))),
inference(backward_demodulation,[],[f50538,f50569]) ).
fof(f50586,plain,
mult(op_c,rd(sF5,op_c)) = mult(sF0,mult(sF3,i(sF6))),
inference(backward_demodulation,[],[f50430,f50569]) ).
fof(f50599,plain,
mult(op_c,rd(sF5,op_c)) = mult(sF0,mult(op_d,sF1)),
inference(forward_demodulation,[],[f50586,f1881]) ).
fof(f50600,plain,
mult(op_d,sF1) = mult(sF0,mult(op_d,op_c)),
inference(forward_demodulation,[],[f50584,f1630]) ).
fof(f50610,plain,
mult(op_d,sF1) = mult(sF0,sF6),
inference(forward_demodulation,[],[f50600,f30]) ).
fof(f50642,plain,
mult(op_c,rd(sF5,op_c)) = mult(sF0,mult(sF0,sF6)),
inference(backward_demodulation,[],[f50599,f50610]) ).
fof(f50651,plain,
sF6 = mult(op_c,rd(sF5,op_c)),
inference(forward_demodulation,[],[f50642,f1495]) ).
fof(f50703,plain,
mult(sF5,mult(mult(sF5,sF5),sF5)) = rd(sF5,i(sF1)),
inference(superposition,[],[f977,f50227]) ).
fof(f50709,plain,
! [X0] : mult(sF1,ld(sF5,X0)) = mult(sF5,mult(rd(mult(sF5,sF5),sF5),X0)),
inference(superposition,[],[f5243,f50227]) ).
fof(f50729,plain,
! [X0] : mult(sF1,ld(sF5,X0)) = mult(sF5,mult(sF5,X0)),
inference(forward_demodulation,[],[f50709,f4]) ).
fof(f50735,plain,
rd(sF1,i(sF5)) = mult(sF5,mult(mult(sF5,sF5),sF5)),
inference(forward_demodulation,[],[f50703,f950]) ).
fof(f50954,plain,
rd(sF1,i(sF5)) = mult(sF5,mult(sF5,mult(sF5,sF5))),
inference(forward_demodulation,[],[f50735,f68]) ).
fof(f51209,plain,
rd(sF1,i(sF5)) = mult(sF1,ld(sF5,mult(sF5,sF5))),
inference(forward_demodulation,[],[f50954,f50729]) ).
fof(f51503,plain,
mult(sF1,sF5) = rd(sF1,i(sF5)),
inference(forward_demodulation,[],[f51209,f2]) ).
fof(f51881,plain,
mult(sF1,sF5) = rd(sF5,op_c),
inference(forward_demodulation,[],[f51503,f951]) ).
fof(f52394,plain,
op_d = rd(sF5,op_c),
inference(forward_demodulation,[],[f51881,f247]) ).
fof(f52787,plain,
mult(op_c,op_d) = sF6,
inference(backward_demodulation,[],[f50651,f52394]) ).
fof(f53071,plain,
sF5 = sF6,
inference(forward_demodulation,[],[f52787,f28]) ).
fof(f53551,plain,
$false,
inference(forward_subsumption_resolution,[],[f53071,f31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP688-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n003.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 10:37:55 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.45 Running first-order theorem proving
% 0.12/0.45 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.47/5.38 % (323621)Detected a unit-equality problem, will run specialized UEQ schedule.
% 31.47/5.38 % (323640)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3840780900:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 31.47/5.38 % (323642)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3298843621:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 31.47/5.38 % (323638)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=4012920357:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 31.47/5.38 % (323639)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=597808551:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 31.47/5.38 % (323641)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=942974877:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 31.47/5.38 % (323643)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=182496777:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 31.47/5.38 % (323637)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=3112545034:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 31.47/5.38 % (323640)Instruction limit reached!
% 31.47/5.38 % (323640)------------------------------
% 31.47/5.38 % (323640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323640)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323640)Termination reason: Instruction limit
% 31.47/5.38 % (323640)Termination phase: Saturation
% 31.47/5.38 % (323640)Time elapsed: 0.046 s
% 31.47/5.38 % (323640)Peak memory usage: 89 MB
% 31.47/5.38 % (323640)Instructions burned: 138 (million)
% 31.47/5.38 % (323641)Instruction limit reached!
% 31.47/5.38 % (323641)------------------------------
% 31.47/5.38 % (323641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323641)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323641)Termination reason: Instruction limit
% 31.47/5.38 % (323641)Termination phase: Saturation
% 31.47/5.38 % (323641)Time elapsed: 0.104 s
% 31.47/5.38 % (323641)Peak memory usage: 89 MB
% 31.47/5.38 % (323641)Instructions burned: 184 (million)
% 31.47/5.38 % (323694)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=292858709:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 31.47/5.38 % (323642)Instruction limit reached!
% 31.47/5.38 % (323642)------------------------------
% 31.47/5.38 % (323642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323642)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323642)Termination reason: Instruction limit
% 31.47/5.38 % (323642)Termination phase: Saturation
% 31.47/5.38 % (323642)Time elapsed: 0.158 s
% 31.47/5.38 % (323642)Peak memory usage: 89 MB
% 31.47/5.38 % (323642)Instructions burned: 257 (million)
% 31.47/5.38 % (323735)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=317159793:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 31.47/5.38 % (323752)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1048693455:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 31.47/5.38 % (323752)Instruction limit reached!
% 31.47/5.38 % (323752)------------------------------
% 31.47/5.38 % (323752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323752)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323752)Termination reason: Instruction limit
% 31.47/5.38 % (323752)Termination phase: Saturation
% 31.47/5.38 % (323752)Time elapsed: 0.119 s
% 31.47/5.38 % (323752)Peak memory usage: 90 MB
% 31.47/5.38 % (323752)Instructions burned: 216 (million)
% 31.47/5.38 % (323809)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=596580182: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)
% 31.47/5.38 % (323643)Instruction limit reached!
% 31.47/5.38 % (323643)------------------------------
% 31.47/5.38 % (323643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323643)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323643)Termination reason: Instruction limit
% 31.47/5.38 % (323643)Termination phase: Saturation
% 31.47/5.38 % (323643)Time elapsed: 0.662 s
% 31.47/5.38 % (323643)Peak memory usage: 99 MB
% 31.47/5.38 % (323643)Instructions burned: 1188 (million)
% 31.47/5.38 % (323809)Instruction limit reached!
% 31.47/5.38 % (323809)------------------------------
% 31.47/5.38 % (323809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323809)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323809)Termination reason: Instruction limit
% 31.47/5.38 % (323809)Termination phase: Saturation
% 31.47/5.38 % (323809)Time elapsed: 0.197 s
% 31.47/5.38 % (323809)Peak memory usage: 93 MB
% 31.47/5.38 % (323809)Instructions burned: 317 (million)
% 31.47/5.38 % (323811)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=2904630834:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 31.47/5.38 % (323694)Instruction limit reached!
% 31.47/5.38 % (323694)------------------------------
% 31.47/5.38 % (323694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323694)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323694)Termination reason: Instruction limit
% 31.47/5.38 % (323694)Termination phase: Saturation
% 31.47/5.38 % (323694)Time elapsed: 0.715 s
% 31.47/5.38 % (323694)Peak memory usage: 142 MB
% 31.47/5.38 % (323694)Instructions burned: 2052 (million)
% 31.47/5.38 % (323814)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=759122734:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 31.47/5.38 % (323812)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1807656095:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 31.47/5.38 % (323812)Instruction limit reached!
% 31.47/5.38 % (323812)------------------------------
% 31.47/5.38 % (323812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323812)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323812)Termination reason: Instruction limit
% 31.47/5.38 % (323812)Termination phase: Saturation
% 31.47/5.38 % (323812)Time elapsed: 1.931 s
% 31.47/5.38 % (323812)Peak memory usage: 133 MB
% 31.47/5.38 % (323812)Instructions burned: 2836 (million)
% 31.47/5.38 % (323818)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=712940439:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2969 on theBenchmark for (2969ds/11832Mi)
% 31.47/5.38 % (323735)Instruction limit reached!
% 31.47/5.38 % (323735)------------------------------
% 31.47/5.38 % (323735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.47/5.38 % (323735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.47/5.38 % (323735)CaDiCaL version: 2.1.3
% 31.47/5.38 % (323735)Termination reason: Instruction limit
% 31.47/5.38 % (323735)Termination phase: Saturation
% 31.47/5.38 % (323735)Time elapsed: 3.033 s
% 31.47/5.38 % (323735)Peak memory usage: 168 MB
% 31.47/5.38 % (323735)Instructions burned: 4949 (million)
% 31.47/5.38 % (323820)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=592758334:i=2279:fgj=on:bd=all_2965 on theBenchmark for (2965ds/2279Mi)
% 31.47/5.38 % (323639)First to succeed.
% 31.47/5.38 % (323639)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-323621"
% 31.47/5.38 % (323639)Refutation found. Thanks to Tanya!
% 31.47/5.38 % SZS status Unsatisfiable for theBenchmark
% 31.47/5.38 % SZS output start Proof for theBenchmark
% See solution above
% 32.04/5.48 % (323639)------------------------------
% 32.04/5.48 % (323639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.04/5.48 % (323639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.48 % (323639)CaDiCaL version: 2.1.3
% 32.04/5.48 % (323639)Termination reason: Refutation
% 32.04/5.48 % (323639)Time elapsed: 4.002 s
% 32.04/5.48 % (323639)Peak memory usage: 177 MB
% 32.04/5.48 % (323639)Instructions burned: 6459 (million)
% 32.04/5.48 % (323639)------------------------------
% 32.04/5.48 % (323639)------------------------------
% 32.04/5.48 % (323621)Success in time 4.451 s
% 32.04/5.48 % Vampire exiting
%------------------------------------------------------------------------------