%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP655-11 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:25 AM UTC 2026
% Result : Unsatisfiable 15.85s 6.31s
% Output : Refutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 96
% Number of leaves : 8
% Syntax : Number of formulae : 580 ( 580 unt; 2 def)
% Number of atoms : 580 ( 579 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 795 ( 795 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f2,negated_conjecture,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f3,negated_conjecture,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f4,negated_conjecture,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f04) ).
fof(f5,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X2,X1))) = mult(mult(mult(X0,X1),X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).
fof(f6,negated_conjecture,
mult(x0,rd(x1,x1)) != x0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f7,plain,
x0 != mult(x0,rd(x1,x1)),
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF0 = rd(x1,x1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f9,plain,
rd(x1,x1) = sF0,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF1 = mult(x0,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f11,plain,
mult(x0,sF0) = sF1,
inference(reorient_equations,[],[f10]) ).
fof(f12,plain,
x0 != sF1,
inference(definition_folding,[],[f7,f11,f9]) ).
fof(f13,plain,
sF0 = ld(x0,sF1),
inference(superposition,[],[f2,f11]) ).
fof(f14,plain,
x1 = mult(sF0,x1),
inference(superposition,[],[f3,f9]) ).
fof(f15,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f16,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),mult(X2,ld(X1,X0)))) = mult(mult(X0,X2),ld(X1,X0)),
inference(superposition,[],[f5,f1]) ).
fof(f18,plain,
! [X2,X0,X1] : mult(rd(X0,X1),mult(X1,mult(X2,X1))) = mult(mult(X0,X2),X1),
inference(superposition,[],[f5,f3]) ).
fof(f20,plain,
! [X2,X0,X1] : mult(mult(X0,X1),mult(X2,mult(X1,X2))) = mult(mult(X0,mult(X1,mult(X2,X1))),X2),
inference(superposition,[],[f5,f5]) ).
fof(f23,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f24,plain,
! [X2,X0,X1] : mult(mult(X0,X1),X2) = rd(mult(X0,mult(X1,mult(X2,X1))),X1),
inference(superposition,[],[f4,f5]) ).
fof(f25,plain,
x0 = rd(sF1,sF0),
inference(superposition,[],[f4,f11]) ).
fof(f28,plain,
! [X2,X0,X1] : mult(mult(X1,X2),rd(X0,X2)) = rd(mult(X1,mult(X2,X0)),X2),
inference(superposition,[],[f24,f3]) ).
fof(f31,plain,
! [X2,X0,X1] : rd(X0,X1) = mult(mult(rd(X0,mult(X1,mult(X2,X1))),X1),X2),
inference(superposition,[],[f24,f3]) ).
fof(f42,plain,
x1 = ld(sF0,x1),
inference(superposition,[],[f15,f9]) ).
fof(f59,plain,
! [X2,X3,X0,X1] : mult(mult(X3,mult(mult(X0,X1),X2)),X1) = mult(rd(X3,X1),mult(X1,mult(X0,mult(X1,mult(X2,X1))))),
inference(superposition,[],[f18,f5]) ).
fof(f60,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X0,X2)),X2) = mult(rd(X1,X2),mult(X2,X0)),
inference(superposition,[],[f18,f3]) ).
fof(f62,plain,
! [X0] : mult(mult(X0,x0),sF0) = mult(rd(X0,sF0),mult(sF0,sF1)),
inference(superposition,[],[f18,f11]) ).
fof(f66,plain,
! [X2,X0,X1] : mult(X2,mult(X1,X2)) = ld(rd(X0,X2),mult(mult(X0,X1),X2)),
inference(superposition,[],[f2,f18]) ).
fof(f71,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X2,X0),X1)) = ld(rd(X2,X1),mult(X0,X1)),
inference(superposition,[],[f66,f1]) ).
fof(f90,plain,
! [X2,X0,X1] : mult(ld(X0,X1),mult(ld(X1,X2),ld(X0,X1))) = ld(X0,mult(X2,ld(X0,X1))),
inference(superposition,[],[f71,f23]) ).
fof(f91,plain,
! [X2,X0,X1] : mult(X1,mult(ld(mult(X0,X1),X2),X1)) = ld(X0,mult(X2,X1)),
inference(superposition,[],[f71,f4]) ).
fof(f96,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X2,rd(X0,X1)),X1)) = ld(rd(X2,X1),X0),
inference(superposition,[],[f71,f3]) ).
fof(f124,plain,
! [X2,X0,X1] : mult(ld(X0,rd(X2,X1)),X1) = ld(X1,ld(rd(X0,X1),X2)),
inference(superposition,[],[f2,f96]) ).
fof(f128,plain,
! [X2,X0,X1] : mult(ld(mult(X0,X1),rd(X2,X1)),X1) = ld(X1,ld(X0,X2)),
inference(superposition,[],[f124,f4]) ).
fof(f131,plain,
! [X0,X1] : mult(ld(X1,rd(X1,X0)),X0) = ld(X0,X0),
inference(superposition,[],[f124,f15]) ).
fof(f147,plain,
! [X2,X0,X1] : mult(ld(mult(X1,X2),X0),X2) = ld(X2,ld(X1,mult(X0,X2))),
inference(superposition,[],[f128,f4]) ).
fof(f153,plain,
! [X2,X0,X1] : ld(mult(X1,X0),rd(X2,X0)) = rd(ld(X0,ld(X1,X2)),X0),
inference(superposition,[],[f4,f128]) ).
fof(f169,plain,
! [X0] : ld(sF1,rd(X0,sF0)) = rd(ld(sF0,ld(x0,X0)),sF0),
inference(superposition,[],[f153,f11]) ).
fof(f177,plain,
! [X2,X0,X1] : rd(X2,X0) = mult(mult(X1,X0),rd(ld(X0,ld(X1,X2)),X0)),
inference(superposition,[],[f1,f153]) ).
fof(f183,plain,
! [X0,X1] : ld(ld(X0,X1),ld(X0,X1)) = mult(ld(X1,X0),ld(X0,X1)),
inference(superposition,[],[f131,f23]) ).
fof(f184,plain,
! [X0,X1] : mult(ld(mult(X0,X1),X0),X1) = ld(X1,X1),
inference(superposition,[],[f131,f4]) ).
fof(f192,plain,
! [X0,X1] : ld(X1,rd(X1,X0)) = rd(ld(X0,X0),X0),
inference(superposition,[],[f4,f131]) ).
fof(f193,plain,
! [X2,X0,X1] : mult(ld(X1,rd(X1,X0)),mult(X0,mult(X2,X0))) = mult(mult(ld(X0,X0),X2),X0),
inference(superposition,[],[f5,f131]) ).
fof(f201,plain,
! [X0,X1] : ld(mult(X0,X1),X0) = rd(ld(X1,X1),X1),
inference(superposition,[],[f192,f4]) ).
fof(f202,plain,
ld(x1,sF0) = rd(ld(x1,x1),x1),
inference(superposition,[],[f192,f9]) ).
fof(f203,plain,
ld(sF1,x0) = rd(ld(sF0,sF0),sF0),
inference(superposition,[],[f192,f25]) ).
fof(f209,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(ld(X0,X0),X0)),
inference(superposition,[],[f1,f192]) ).
fof(f227,plain,
! [X2,X0,X1] : rd(X2,X1) = mult(X2,ld(X0,rd(X0,X1))),
inference(superposition,[],[f209,f192]) ).
fof(f240,plain,
! [X2,X0,X1] : mult(X0,mult(rd(ld(X1,X1),X1),mult(X2,rd(ld(X1,X1),X1)))) = rd(mult(mult(X0,rd(ld(X1,X1),X1)),X2),X1),
inference(superposition,[],[f5,f209]) ).
fof(f243,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),X2),X1) = mult(X0,mult(rd(ld(X1,X1),X1),mult(X2,rd(ld(X1,X1),X1)))),
inference(forward_demodulation,[],[f240,f209]) ).
fof(f248,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),X2),X1) = mult(X0,mult(rd(ld(X1,X1),X1),rd(X2,X1))),
inference(forward_demodulation,[],[f243,f209]) ).
fof(f260,plain,
! [X2,X0,X1] : ld(mult(X0,X1),X0) = ld(mult(X2,X1),X2),
inference(superposition,[],[f201,f201]) ).
fof(f266,plain,
! [X2,X0,X1] : rd(X2,X1) = mult(X2,ld(mult(X0,X1),X0)),
inference(superposition,[],[f209,f201]) ).
fof(f267,plain,
! [X2,X0,X1] : ld(mult(X0,X1),X0) = ld(X2,rd(X2,X1)),
inference(superposition,[],[f192,f201]) ).
fof(f300,plain,
! [X2,X0,X1] : mult(X1,ld(X2,X0)) = rd(X1,ld(X0,X2)),
inference(superposition,[],[f227,f23]) ).
fof(f304,plain,
! [X0] : rd(X0,x1) = mult(X0,ld(x1,sF0)),
inference(superposition,[],[f227,f9]) ).
fof(f305,plain,
! [X0] : rd(X0,sF0) = mult(X0,ld(sF1,x0)),
inference(superposition,[],[f227,f25]) ).
fof(f387,plain,
! [X0,X1] : mult(ld(sF1,x0),mult(ld(X1,X0),ld(sF1,x0))) = ld(rd(X1,ld(sF1,x0)),rd(X0,sF0)),
inference(superposition,[],[f71,f305]) ).
fof(f402,plain,
! [X0,X1] : mult(ld(sF1,x0),mult(ld(X1,X0),ld(sF1,x0))) = ld(mult(X1,ld(x0,sF1)),rd(X0,sF0)),
inference(forward_demodulation,[],[f387,f300]) ).
fof(f416,plain,
! [X0,X1] : mult(ld(sF1,x0),mult(ld(X1,X0),ld(sF1,x0))) = ld(mult(X1,sF0),rd(X0,sF0)),
inference(forward_demodulation,[],[f402,f13]) ).
fof(f427,plain,
! [X0,X1] : mult(ld(sF1,x0),mult(ld(X1,X0),ld(sF1,x0))) = rd(ld(sF0,ld(X1,X0)),sF0),
inference(forward_demodulation,[],[f416,f153]) ).
fof(f434,plain,
! [X0,X1] : rd(ld(sF0,ld(X1,X0)),sF0) = mult(ld(sF1,x0),rd(ld(X1,X0),sF0)),
inference(forward_demodulation,[],[f427,f305]) ).
fof(f788,plain,
! [X2,X3,X0,X1] : rd(X3,mult(X2,mult(X1,X2))) = mult(X3,ld(mult(mult(X0,X1),X2),rd(X0,X2))),
inference(superposition,[],[f266,f18]) ).
fof(f812,plain,
! [X2,X3,X0,X1] : mult(rd(mult(X0,X1),X2),X1) = mult(X0,mult(X1,mult(ld(mult(X3,X2),X3),X1))),
inference(superposition,[],[f5,f266]) ).
fof(f834,plain,
! [X2,X3,X0,X1] : rd(X3,mult(X2,mult(X1,X2))) = mult(X3,rd(ld(X2,ld(mult(X0,X1),X0)),X2)),
inference(forward_demodulation,[],[f788,f153]) ).
fof(f900,plain,
! [X2,X0,X1] : rd(mult(rd(X2,X1),ld(X1,X1)),X1) = mult(X2,mult(ld(mult(X0,X1),X0),ld(mult(X0,X1),X0))),
inference(superposition,[],[f248,f201]) ).
fof(f901,plain,
! [X2,X0,X1] : rd(mult(rd(X2,X1),ld(X1,X1)),X1) = mult(X2,mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1)))),
inference(superposition,[],[f248,f192]) ).
fof(f903,plain,
! [X0] : rd(mult(rd(X0,x1),x1),x1) = mult(X0,mult(rd(ld(x1,x1),x1),sF0)),
inference(superposition,[],[f248,f9]) ).
fof(f911,plain,
! [X2,X0,X1] : ld(X0,rd(mult(rd(X0,X1),X2),X1)) = mult(rd(ld(X1,X1),X1),rd(X2,X1)),
inference(superposition,[],[f2,f248]) ).
fof(f938,plain,
! [X0] : rd(mult(rd(X0,x1),x1),x1) = mult(X0,mult(ld(x1,sF0),sF0)),
inference(forward_demodulation,[],[f903,f202]) ).
fof(f939,plain,
! [X2,X0,X1] : rd(mult(rd(X2,X1),ld(X1,X1)),X1) = mult(X2,rd(ld(X0,rd(X0,X1)),X1)),
inference(forward_demodulation,[],[f901,f227]) ).
fof(f940,plain,
! [X2,X0,X1] : rd(mult(rd(X2,X1),ld(X1,X1)),X1) = mult(X2,rd(ld(mult(X0,X1),X0),X1)),
inference(forward_demodulation,[],[f900,f266]) ).
fof(f946,plain,
! [X0] : rd(X0,x1) = mult(X0,mult(ld(x1,sF0),sF0)),
inference(forward_demodulation,[],[f938,f4]) ).
fof(f960,plain,
! [X0] : mult(mult(X0,ld(x1,sF0)),sF0) = mult(rd(X0,sF0),rd(sF0,x1)),
inference(superposition,[],[f18,f946]) ).
fof(f961,plain,
! [X0] : ld(X0,rd(X0,x1)) = mult(ld(x1,sF0),sF0),
inference(superposition,[],[f2,f946]) ).
fof(f988,plain,
rd(ld(x1,x1),x1) = mult(ld(x1,sF0),sF0),
inference(forward_demodulation,[],[f961,f192]) ).
fof(f989,plain,
! [X0] : mult(rd(X0,sF0),rd(sF0,x1)) = mult(rd(X0,x1),sF0),
inference(forward_demodulation,[],[f960,f304]) ).
fof(f1006,plain,
ld(x1,sF0) = mult(ld(x1,sF0),sF0),
inference(forward_demodulation,[],[f988,f202]) ).
fof(f1054,plain,
ld(sF0,sF0) = mult(ld(ld(x1,sF0),ld(x1,sF0)),sF0),
inference(superposition,[],[f184,f1006]) ).
fof(f1055,plain,
rd(ld(sF0,sF0),sF0) = ld(ld(x1,sF0),ld(x1,sF0)),
inference(superposition,[],[f201,f1006]) ).
fof(f1056,plain,
! [X0] : rd(X0,sF0) = mult(X0,ld(ld(x1,sF0),ld(x1,sF0))),
inference(superposition,[],[f266,f1006]) ).
fof(f1059,plain,
! [X0] : rd(X0,sF0) = mult(X0,mult(ld(sF0,x1),ld(x1,sF0))),
inference(forward_demodulation,[],[f1056,f183]) ).
fof(f1060,plain,
rd(ld(sF0,sF0),sF0) = mult(ld(sF0,x1),ld(x1,sF0)),
inference(forward_demodulation,[],[f1055,f183]) ).
fof(f1061,plain,
ld(sF0,sF0) = mult(mult(ld(sF0,x1),ld(x1,sF0)),sF0),
inference(forward_demodulation,[],[f1054,f183]) ).
fof(f1065,plain,
! [X0] : rd(X0,sF0) = mult(X0,rd(ld(sF0,x1),x1)),
inference(forward_demodulation,[],[f1059,f304]) ).
fof(f1066,plain,
rd(ld(sF0,sF0),sF0) = rd(ld(sF0,x1),x1),
inference(forward_demodulation,[],[f1060,f304]) ).
fof(f1067,plain,
ld(sF0,sF0) = mult(rd(ld(sF0,x1),x1),sF0),
inference(forward_demodulation,[],[f1061,f304]) ).
fof(f1071,plain,
! [X0] : rd(X0,sF0) = mult(X0,rd(x1,x1)),
inference(forward_demodulation,[],[f1065,f42]) ).
fof(f1072,plain,
rd(x1,x1) = rd(ld(sF0,sF0),sF0),
inference(forward_demodulation,[],[f1066,f42]) ).
fof(f1073,plain,
ld(sF0,sF0) = mult(rd(x1,x1),sF0),
inference(forward_demodulation,[],[f1067,f42]) ).
fof(f1076,plain,
! [X0] : mult(X0,sF0) = rd(X0,sF0),
inference(forward_demodulation,[],[f1071,f9]) ).
fof(f1077,plain,
sF0 = rd(ld(sF0,sF0),sF0),
inference(forward_demodulation,[],[f1072,f9]) ).
fof(f1078,plain,
ld(sF0,sF0) = mult(sF0,sF0),
inference(forward_demodulation,[],[f1073,f9]) ).
fof(f1080,plain,
! [X0] : mult(mult(X0,x0),sF0) = mult(mult(X0,sF0),mult(sF0,sF1)),
inference(backward_demodulation,[],[f62,f1076]) ).
fof(f1083,plain,
! [X0] : rd(ld(sF0,ld(x0,X0)),sF0) = ld(sF1,mult(X0,sF0)),
inference(backward_demodulation,[],[f169,f1076]) ).
fof(f1087,plain,
! [X0] : mult(rd(X0,x1),sF0) = mult(mult(X0,sF0),rd(sF0,x1)),
inference(backward_demodulation,[],[f989,f1076]) ).
fof(f1091,plain,
! [X0,X1] : mult(ld(sF1,x0),rd(ld(X1,X0),sF0)) = mult(ld(sF0,ld(X1,X0)),sF0),
inference(backward_demodulation,[],[f434,f1076]) ).
fof(f1092,plain,
ld(sF1,x0) = mult(ld(sF0,sF0),sF0),
inference(backward_demodulation,[],[f203,f1076]) ).
fof(f1096,plain,
x0 = mult(sF1,sF0),
inference(backward_demodulation,[],[f25,f1076]) ).
fof(f1097,plain,
sF0 = mult(ld(sF0,sF0),sF0),
inference(forward_demodulation,[],[f1077,f1076]) ).
fof(f1102,plain,
ld(sF1,x0) = mult(mult(sF0,sF0),sF0),
inference(forward_demodulation,[],[f1092,f1078]) ).
fof(f1103,plain,
! [X0,X1] : mult(ld(sF0,ld(X1,X0)),sF0) = mult(ld(sF1,x0),mult(ld(X1,X0),sF0)),
inference(forward_demodulation,[],[f1091,f1076]) ).
fof(f1107,plain,
! [X0] : ld(sF1,mult(X0,sF0)) = mult(ld(sF0,ld(x0,X0)),sF0),
inference(forward_demodulation,[],[f1083,f1076]) ).
fof(f1108,plain,
sF0 = mult(mult(sF0,sF0),sF0),
inference(forward_demodulation,[],[f1097,f1078]) ).
fof(f1113,plain,
sF0 = ld(sF1,x0),
inference(backward_demodulation,[],[f1102,f1108]) ).
fof(f1117,plain,
! [X0,X1] : mult(ld(sF0,ld(X1,X0)),sF0) = mult(sF0,mult(ld(X1,X0),sF0)),
inference(backward_demodulation,[],[f1103,f1113]) ).
fof(f1121,plain,
! [X0] : ld(sF1,mult(X0,sF0)) = mult(sF0,mult(ld(x0,X0),sF0)),
inference(backward_demodulation,[],[f1107,f1117]) ).
fof(f1126,plain,
! [X0,X1] : mult(sF0,mult(ld(X0,X1),sF0)) = ld(mult(X0,sF0),mult(X1,sF0)),
inference(superposition,[],[f71,f1076]) ).
fof(f1140,plain,
! [X0] : mult(mult(X0,sF0),sF0) = X0,
inference(superposition,[],[f4,f1076]) ).
fof(f1192,plain,
! [X0,X1] : mult(mult(X1,mult(X0,sF0)),sF0) = mult(rd(X1,sF0),mult(sF0,X0)),
inference(superposition,[],[f18,f1140]) ).
fof(f1205,plain,
! [X0,X1] : mult(mult(X1,mult(X0,sF0)),sF0) = mult(mult(X1,sF0),mult(sF0,X0)),
inference(forward_demodulation,[],[f1192,f1076]) ).
fof(f1229,plain,
sF0 = mult(sF0,mult(sF0,sF0)),
inference(superposition,[],[f1,f1078]) ).
fof(f1296,plain,
! [X0] : mult(sF0,mult(mult(sF0,sF0),mult(X0,mult(sF0,sF0)))) = mult(mult(sF0,X0),mult(sF0,sF0)),
inference(superposition,[],[f5,f1229]) ).
fof(f1299,plain,
! [X0] : rd(ld(mult(sF0,sF0),ld(sF0,X0)),mult(sF0,sF0)) = ld(sF0,rd(X0,mult(sF0,sF0))),
inference(superposition,[],[f153,f1229]) ).
fof(f1300,plain,
ld(mult(sF0,sF0),mult(sF0,sF0)) = mult(ld(sF0,sF0),mult(sF0,sF0)),
inference(superposition,[],[f184,f1229]) ).
fof(f1301,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = mult(X0,ld(sF0,sF0)),
inference(superposition,[],[f266,f1229]) ).
fof(f1304,plain,
! [X0] : mult(X0,mult(sF0,sF0)) = rd(X0,mult(sF0,sF0)),
inference(forward_demodulation,[],[f1301,f1078]) ).
fof(f1305,plain,
ld(mult(sF0,sF0),mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(sF0,sF0)),
inference(forward_demodulation,[],[f1300,f1078]) ).
fof(f1310,plain,
! [X0] : rd(ld(mult(sF0,sF0),ld(sF0,X0)),mult(sF0,sF0)) = ld(sF0,mult(X0,mult(sF0,sF0))),
inference(backward_demodulation,[],[f1299,f1304]) ).
fof(f1312,plain,
mult(mult(sF0,sF0),mult(sF0,sF0)) = mult(sF0,mult(ld(sF0,sF0),sF0)),
inference(forward_demodulation,[],[f1305,f1126]) ).
fof(f1314,plain,
! [X0] : ld(sF0,mult(X0,mult(sF0,sF0))) = mult(ld(mult(sF0,sF0),ld(sF0,X0)),mult(sF0,sF0)),
inference(forward_demodulation,[],[f1310,f1304]) ).
fof(f1315,plain,
mult(mult(sF0,sF0),mult(sF0,sF0)) = mult(sF0,mult(mult(sF0,sF0),sF0)),
inference(forward_demodulation,[],[f1312,f1078]) ).
fof(f1316,plain,
mult(sF0,sF0) = mult(mult(sF0,sF0),mult(sF0,sF0)),
inference(forward_demodulation,[],[f1315,f1140]) ).
fof(f1323,plain,
! [X0,X1] : mult(mult(sF0,sF0),mult(ld(X0,X1),mult(sF0,sF0))) = ld(mult(X0,mult(sF0,sF0)),mult(X1,mult(sF0,sF0))),
inference(superposition,[],[f71,f1304]) ).
fof(f1327,plain,
! [X0,X1] : rd(ld(mult(sF0,sF0),ld(X1,X0)),mult(sF0,sF0)) = ld(mult(X1,mult(sF0,sF0)),mult(X0,mult(sF0,sF0))),
inference(superposition,[],[f153,f1304]) ).
fof(f1351,plain,
! [X0,X1] : ld(mult(X1,mult(sF0,sF0)),mult(X0,mult(sF0,sF0))) = mult(ld(mult(sF0,sF0),ld(X1,X0)),mult(sF0,sF0)),
inference(forward_demodulation,[],[f1327,f1304]) ).
fof(f1366,plain,
! [X0,X1] : mult(ld(mult(sF0,sF0),ld(X1,X0)),mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(ld(X1,X0),mult(sF0,sF0))),
inference(forward_demodulation,[],[f1351,f1323]) ).
fof(f1377,plain,
! [X0] : ld(sF0,mult(X0,mult(sF0,sF0))) = mult(mult(sF0,sF0),mult(ld(sF0,X0),mult(sF0,sF0))),
inference(backward_demodulation,[],[f1314,f1366]) ).
fof(f1419,plain,
! [X0,X1] : rd(X1,rd(sF0,x1)) = mult(X1,ld(mult(rd(X0,x1),sF0),mult(X0,sF0))),
inference(superposition,[],[f266,f1087]) ).
fof(f1422,plain,
! [X0,X1] : rd(X1,rd(sF0,x1)) = mult(X1,mult(sF0,mult(ld(rd(X0,x1),X0),sF0))),
inference(forward_demodulation,[],[f1419,f1126]) ).
fof(f1431,plain,
! [X1] : rd(X1,rd(sF0,x1)) = mult(X1,mult(sF0,mult(x1,sF0))),
inference(forward_demodulation,[],[f1422,f15]) ).
fof(f1464,plain,
! [X2,X3,X0,X1] : mult(ld(X2,X1),mult(ld(X0,X3),ld(X2,X1))) = ld(mult(X0,ld(X1,X2)),mult(X3,ld(X2,X1))),
inference(superposition,[],[f71,f300]) ).
fof(f1468,plain,
! [X2,X3,X0,X1] : rd(ld(ld(X2,X1),ld(X3,X0)),ld(X2,X1)) = ld(mult(X3,ld(X2,X1)),mult(X0,ld(X1,X2))),
inference(superposition,[],[f153,f300]) ).
fof(f1492,plain,
! [X2,X3,X0,X1] : ld(mult(X3,ld(X2,X1)),mult(X0,ld(X1,X2))) = mult(ld(ld(X2,X1),ld(X3,X0)),ld(X1,X2)),
inference(forward_demodulation,[],[f1468,f300]) ).
fof(f1515,plain,
! [X2,X3,X0,X1] : mult(ld(ld(X2,X1),ld(X3,X0)),ld(X1,X2)) = mult(ld(X1,X2),mult(ld(X3,X0),ld(X1,X2))),
inference(forward_demodulation,[],[f1492,f1464]) ).
fof(f1682,plain,
! [X0,X1] : ld(mult(rd(X0,x1),sF0),mult(X0,sF0)) = ld(mult(X1,rd(sF0,x1)),X1),
inference(superposition,[],[f260,f1087]) ).
fof(f1727,plain,
! [X0,X1] : mult(sF0,mult(ld(rd(X0,x1),X0),sF0)) = ld(mult(X1,rd(sF0,x1)),X1),
inference(forward_demodulation,[],[f1682,f1126]) ).
fof(f1758,plain,
! [X1] : mult(sF0,mult(x1,sF0)) = ld(mult(X1,rd(sF0,x1)),X1),
inference(forward_demodulation,[],[f1727,f15]) ).
fof(f1819,plain,
! [X2,X0,X1] : rd(mult(X1,X0),X2) = mult(mult(X1,X2),rd(ld(X2,X0),X2)),
inference(superposition,[],[f177,f2]) ).
fof(f1821,plain,
! [X2,X3,X0,X1] : rd(rd(X2,X1),X3) = mult(mult(X2,X3),rd(ld(X3,ld(mult(X0,X1),X0)),X3)),
inference(superposition,[],[f177,f267]) ).
fof(f1887,plain,
! [X2,X3,X1] : rd(rd(X2,X1),X3) = rd(mult(X2,X3),mult(X3,mult(X1,X3))),
inference(forward_demodulation,[],[f1821,f834]) ).
fof(f2004,plain,
! [X0,X1] : rd(mult(mult(X0,sF0),X1),sF0) = mult(X0,rd(ld(sF0,X1),sF0)),
inference(superposition,[],[f1819,f1140]) ).
fof(f2007,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),X2),X1) = mult(X0,rd(ld(X1,X2),X1)),
inference(superposition,[],[f1819,f3]) ).
fof(f2019,plain,
! [X2,X0,X1] : rd(mult(X1,rd(X2,X0)),X2) = mult(mult(X1,X2),rd(rd(ld(X0,X0),X0),X2)),
inference(superposition,[],[f1819,f192]) ).
fof(f2028,plain,
! [X0] : rd(mult(X0,x1),sF0) = mult(mult(X0,sF0),rd(x1,sF0)),
inference(superposition,[],[f1819,f42]) ).
fof(f2052,plain,
! [X2,X3,X0,X1] : rd(X3,rd(ld(X2,X1),X2)) = mult(X3,ld(rd(mult(X0,X1),X2),mult(X0,X2))),
inference(superposition,[],[f266,f1819]) ).
fof(f2055,plain,
! [X2,X3,X0,X1] : rd(X3,rd(ld(X2,X1),X2)) = mult(X3,mult(X2,mult(ld(mult(X0,X1),X0),X2))),
inference(forward_demodulation,[],[f2052,f71]) ).
fof(f2070,plain,
! [X0] : rd(mult(X0,x1),sF0) = mult(mult(X0,sF0),mult(x1,sF0)),
inference(forward_demodulation,[],[f2028,f1076]) ).
fof(f2090,plain,
! [X2,X0,X1] : mult(rd(ld(X1,X1),X1),rd(X2,X1)) = ld(X0,mult(X0,rd(ld(X1,X2),X1))),
inference(backward_demodulation,[],[f911,f2007]) ).
fof(f2104,plain,
! [X2,X0,X1] : mult(X2,rd(ld(mult(X0,X1),X0),X1)) = mult(X2,rd(ld(X1,ld(X1,X1)),X1)),
inference(backward_demodulation,[],[f940,f2007]) ).
fof(f2105,plain,
! [X2,X0,X1] : mult(X2,rd(ld(X0,rd(X0,X1)),X1)) = mult(X2,rd(ld(X1,ld(X1,X1)),X1)),
inference(backward_demodulation,[],[f939,f2007]) ).
fof(f2111,plain,
! [X0,X1] : rd(mult(mult(X0,sF0),X1),sF0) = mult(X0,mult(ld(sF0,X1),sF0)),
inference(forward_demodulation,[],[f2004,f1076]) ).
fof(f2122,plain,
! [X2,X3,X1] : mult(rd(mult(X3,X2),X1),X2) = rd(X3,rd(ld(X2,X1),X2)),
inference(forward_demodulation,[],[f2055,f812]) ).
fof(f2127,plain,
! [X0] : mult(mult(X0,sF0),mult(x1,sF0)) = mult(mult(X0,x1),sF0),
inference(forward_demodulation,[],[f2070,f1076]) ).
fof(f2138,plain,
! [X2,X1] : mult(rd(ld(X1,X1),X1),rd(X2,X1)) = rd(ld(X1,X2),X1),
inference(forward_demodulation,[],[f2090,f2]) ).
fof(f2141,plain,
! [X0,X1] : mult(mult(mult(X0,sF0),X1),sF0) = mult(X0,mult(ld(sF0,X1),sF0)),
inference(forward_demodulation,[],[f2111,f1076]) ).
fof(f2173,plain,
! [X0,X1] : mult(X0,mult(sF0,mult(X1,sF0))) = mult(X0,mult(ld(sF0,X1),sF0)),
inference(forward_demodulation,[],[f2141,f5]) ).
fof(f2197,plain,
! [X0] : rd(ld(sF0,X0),sF0) = mult(rd(mult(sF0,sF0),sF0),rd(X0,sF0)),
inference(superposition,[],[f2138,f1078]) ).
fof(f2203,plain,
! [X2,X0,X1] : mult(rd(ld(ld(X2,X1),ld(X2,X1)),ld(X2,X1)),mult(X0,ld(X1,X2))) = rd(ld(ld(X2,X1),X0),ld(X2,X1)),
inference(superposition,[],[f2138,f300]) ).
fof(f2204,plain,
! [X0] : mult(rd(ld(mult(sF0,sF0),mult(sF0,sF0)),mult(sF0,sF0)),mult(X0,mult(sF0,sF0))) = rd(ld(mult(sF0,sF0),X0),mult(sF0,sF0)),
inference(superposition,[],[f2138,f1304]) ).
fof(f2207,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(ld(X1,ld(X1,X1)),X1),
inference(superposition,[],[f2138,f192]) ).
fof(f2208,plain,
! [X0,X1] : mult(rd(ld(X1,X1),X1),X0) = rd(ld(X1,mult(X0,X1)),X1),
inference(superposition,[],[f2138,f4]) ).
fof(f2211,plain,
! [X0] : rd(rd(ld(X0,X0),X0),X0) = rd(ld(X0,ld(X0,X0)),X0),
inference(superposition,[],[f209,f2138]) ).
fof(f2212,plain,
! [X0,X1] : rd(X1,X0) = ld(rd(ld(X0,X0),X0),rd(ld(X0,X1),X0)),
inference(superposition,[],[f2,f2138]) ).
fof(f2213,plain,
! [X0,X1] : rd(ld(X0,X0),X0) = rd(rd(ld(X0,X1),X0),rd(X1,X0)),
inference(superposition,[],[f4,f2138]) ).
fof(f2228,plain,
! [X2,X0,X1] : mult(X2,rd(ld(mult(X0,X1),X0),X1)) = mult(X2,rd(rd(ld(X1,X1),X1),X1)),
inference(backward_demodulation,[],[f2104,f2211]) ).
fof(f2229,plain,
! [X2,X0,X1] : mult(X2,rd(ld(X0,rd(X0,X1)),X1)) = mult(X2,rd(rd(ld(X1,X1),X1),X1)),
inference(backward_demodulation,[],[f2105,f2211]) ).
fof(f2231,plain,
! [X0,X1] : rd(ld(X0,rd(X0,X1)),X1) = rd(ld(X1,ld(X1,X1)),X1),
inference(forward_demodulation,[],[f2207,f227]) ).
fof(f2234,plain,
! [X0] : mult(rd(ld(mult(sF0,sF0),mult(sF0,sF0)),mult(sF0,sF0)),mult(X0,mult(sF0,sF0))) = mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0)),
inference(forward_demodulation,[],[f2204,f1304]) ).
fof(f2235,plain,
! [X2,X0,X1] : mult(rd(ld(ld(X2,X1),ld(X2,X1)),ld(X2,X1)),mult(X0,ld(X1,X2))) = mult(ld(ld(X2,X1),X0),ld(X1,X2)),
inference(forward_demodulation,[],[f2203,f300]) ).
fof(f2239,plain,
! [X0] : rd(ld(sF0,X0),sF0) = mult(rd(mult(sF0,sF0),sF0),mult(X0,sF0)),
inference(forward_demodulation,[],[f2197,f1076]) ).
fof(f2241,plain,
! [X0] : mult(mult(ld(mult(sF0,sF0),mult(sF0,sF0)),mult(sF0,sF0)),mult(X0,mult(sF0,sF0))) = mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0)),
inference(forward_demodulation,[],[f2234,f1304]) ).
fof(f2242,plain,
! [X2,X0,X1] : mult(mult(ld(ld(X2,X1),ld(X2,X1)),ld(X1,X2)),mult(X0,ld(X1,X2))) = mult(ld(ld(X2,X1),X0),ld(X1,X2)),
inference(forward_demodulation,[],[f2235,f300]) ).
fof(f2246,plain,
! [X0] : mult(sF0,mult(X0,sF0)) = rd(ld(sF0,X0),sF0),
inference(forward_demodulation,[],[f2239,f4]) ).
fof(f2248,plain,
! [X0] : mult(mult(mult(sF0,mult(ld(sF0,sF0),sF0)),mult(sF0,sF0)),mult(X0,mult(sF0,sF0))) = mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0)),
inference(forward_demodulation,[],[f2241,f1126]) ).
fof(f2249,plain,
! [X2,X0,X1] : mult(ld(ld(X2,X1),X0),ld(X1,X2)) = mult(mult(ld(X1,X2),mult(ld(X2,X1),ld(X1,X2))),mult(X0,ld(X1,X2))),
inference(forward_demodulation,[],[f2242,f1515]) ).
fof(f2253,plain,
! [X0] : mult(sF0,mult(X0,sF0)) = mult(ld(sF0,X0),sF0),
inference(forward_demodulation,[],[f2246,f1076]) ).
fof(f2255,plain,
! [X0] : mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0)) = mult(mult(mult(sF0,mult(sF0,mult(sF0,sF0))),mult(sF0,sF0)),mult(X0,mult(sF0,sF0))),
inference(forward_demodulation,[],[f2248,f2173]) ).
fof(f2256,plain,
! [X2,X0,X1] : mult(ld(ld(X2,X1),X0),ld(X1,X2)) = mult(ld(X1,mult(X1,ld(X1,X2))),mult(X0,ld(X1,X2))),
inference(forward_demodulation,[],[f2249,f90]) ).
fof(f2260,plain,
! [X0] : mult(mult(mult(sF0,sF0),mult(sF0,sF0)),mult(X0,mult(sF0,sF0))) = mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0)),
inference(forward_demodulation,[],[f2255,f1229]) ).
fof(f2261,plain,
! [X2,X0,X1] : mult(ld(X1,X2),mult(X0,ld(X1,X2))) = mult(ld(ld(X2,X1),X0),ld(X1,X2)),
inference(forward_demodulation,[],[f2256,f2]) ).
fof(f2264,plain,
! [X0] : mult(mult(sF0,sF0),mult(X0,mult(sF0,sF0))) = mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0)),
inference(forward_demodulation,[],[f2260,f1316]) ).
fof(f2277,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = ld(rd(ld(X1,X1),X1),rd(X0,X1)),
inference(superposition,[],[f2212,f2]) ).
fof(f2299,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = ld(rd(ld(mult(sF0,sF0),mult(sF0,sF0)),mult(sF0,sF0)),mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0))),
inference(superposition,[],[f2212,f1304]) ).
fof(f2303,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),X1),rd(ld(X0,X0),X0)) = mult(rd(rd(X0,X0),rd(ld(X0,X0),X0)),rd(X1,rd(ld(X0,X0),X0))),
inference(superposition,[],[f2138,f2212]) ).
fof(f2314,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),X1),rd(ld(X0,X0),X0)) = mult(rd(rd(X0,X0),rd(ld(X0,X0),X0)),mult(rd(mult(X1,X0),X0),X0)),
inference(forward_demodulation,[],[f2303,f2122]) ).
fof(f2317,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(ld(ld(mult(sF0,sF0),mult(sF0,sF0)),ld(mult(sF0,sF0),X0)),mult(sF0,sF0))),
inference(forward_demodulation,[],[f2299,f71]) ).
fof(f2347,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),X1),rd(ld(X0,X0),X0)) = mult(rd(rd(X0,X0),rd(ld(X0,X0),X0)),mult(X1,X0)),
inference(forward_demodulation,[],[f2314,f3]) ).
fof(f2349,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(ld(mult(sF0,mult(ld(sF0,sF0),sF0)),ld(mult(sF0,sF0),X0)),mult(sF0,sF0))),
inference(forward_demodulation,[],[f2317,f1126]) ).
fof(f2368,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),X1),rd(ld(X0,X0),X0)) = mult(mult(rd(mult(rd(X0,X0),X0),X0),X0),mult(X1,X0)),
inference(forward_demodulation,[],[f2347,f2122]) ).
fof(f2370,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(ld(mult(sF0,mult(sF0,mult(sF0,sF0))),ld(mult(sF0,sF0),X0)),mult(sF0,sF0))),
inference(forward_demodulation,[],[f2349,f2253]) ).
fof(f2384,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),X1),rd(ld(X0,X0),X0)) = mult(mult(rd(X0,X0),X0),mult(X1,X0)),
inference(forward_demodulation,[],[f2368,f3]) ).
fof(f2386,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(ld(mult(sF0,sF0),ld(mult(sF0,sF0),X0)),mult(sF0,sF0))),
inference(forward_demodulation,[],[f2370,f1229]) ).
fof(f2398,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = rd(ld(rd(ld(X0,X0),X0),X1),rd(ld(X0,X0),X0)),
inference(forward_demodulation,[],[f2384,f3]) ).
fof(f2400,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(mult(sF0,sF0),mult(ld(mult(sF0,sF0),X0),mult(sF0,sF0)))),
inference(forward_demodulation,[],[f2386,f2264]) ).
fof(f2410,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = mult(rd(mult(ld(rd(ld(X0,X0),X0),X1),X0),X0),X0),
inference(forward_demodulation,[],[f2398,f2122]) ).
fof(f2411,plain,
! [X0] : rd(X0,mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(mult(sF0,sF0),mult(mult(sF0,sF0),mult(X0,mult(sF0,sF0))))),
inference(forward_demodulation,[],[f2400,f2264]) ).
fof(f2419,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = mult(ld(rd(ld(X0,X0),X0),X1),X0),
inference(forward_demodulation,[],[f2410,f3]) ).
fof(f2420,plain,
! [X0] : mult(X0,mult(sF0,sF0)) = mult(mult(sF0,sF0),mult(mult(sF0,sF0),mult(mult(sF0,sF0),mult(X0,mult(sF0,sF0))))),
inference(forward_demodulation,[],[f2411,f1304]) ).
fof(f2432,plain,
! [X0,X1] : rd(ld(X1,X1),X1) = rd(rd(X0,X1),rd(mult(X1,X0),X1)),
inference(superposition,[],[f2213,f2]) ).
fof(f2560,plain,
rd(ld(ld(x1,sF0),ld(x1,sF0)),ld(x1,sF0)) = rd(rd(sF0,ld(x1,sF0)),rd(ld(x1,sF0),ld(x1,sF0))),
inference(superposition,[],[f2432,f1006]) ).
fof(f2567,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)) = rd(rd(rd(X1,X0),rd(ld(X0,X0),X0)),rd(rd(ld(X0,X1),X0),rd(ld(X0,X0),X0))),
inference(superposition,[],[f2432,f2138]) ).
fof(f2573,plain,
! [X0] : rd(ld(X0,X0),X0) = rd(rd(X0,X0),X0),
inference(superposition,[],[f2432,f4]) ).
fof(f2600,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(rd(X0,X0),X0)),
inference(backward_demodulation,[],[f209,f2573]) ).
fof(f2610,plain,
! [X2,X0,X1] : rd(mult(X1,rd(X2,X0)),X2) = mult(mult(X1,X2),rd(rd(rd(X0,X0),X0),X2)),
inference(backward_demodulation,[],[f2019,f2573]) ).
fof(f2612,plain,
! [X2,X1] : rd(ld(X1,X2),X1) = mult(rd(rd(X1,X1),X1),rd(X2,X1)),
inference(backward_demodulation,[],[f2138,f2573]) ).
fof(f2613,plain,
! [X0,X1] : rd(ld(X1,mult(X0,X1)),X1) = mult(rd(rd(X1,X1),X1),X0),
inference(backward_demodulation,[],[f2208,f2573]) ).
fof(f2615,plain,
! [X0,X1] : rd(rd(ld(X0,X1),X0),rd(X1,X0)) = rd(rd(X0,X0),X0),
inference(backward_demodulation,[],[f2213,f2573]) ).
fof(f2625,plain,
! [X2,X0,X1] : mult(X2,rd(ld(mult(X0,X1),X0),X1)) = mult(X2,rd(rd(rd(X1,X1),X1),X1)),
inference(backward_demodulation,[],[f2228,f2573]) ).
fof(f2626,plain,
! [X2,X0,X1] : mult(X2,rd(ld(X0,rd(X0,X1)),X1)) = mult(X2,rd(rd(rd(X1,X1),X1),X1)),
inference(backward_demodulation,[],[f2229,f2573]) ).
fof(f2627,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = ld(rd(rd(X1,X1),X1),rd(X0,X1)),
inference(backward_demodulation,[],[f2277,f2573]) ).
fof(f2630,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = mult(ld(rd(rd(X0,X0),X0),X1),X0),
inference(backward_demodulation,[],[f2419,f2573]) ).
fof(f2652,plain,
ld(x1,sF0) = rd(rd(x1,x1),x1),
inference(backward_demodulation,[],[f202,f2573]) ).
fof(f2659,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)) = rd(rd(rd(X1,X0),rd(ld(X0,X0),X0)),mult(rd(mult(rd(ld(X0,X1),X0),X0),X0),X0)),
inference(forward_demodulation,[],[f2567,f2122]) ).
fof(f2666,plain,
rd(ld(ld(x1,sF0),ld(x1,sF0)),ld(x1,sF0)) = rd(rd(sF0,ld(x1,sF0)),mult(ld(x1,sF0),ld(sF0,x1))),
inference(forward_demodulation,[],[f2560,f300]) ).
fof(f2690,plain,
ld(x1,sF0) = rd(sF0,x1),
inference(forward_demodulation,[],[f2652,f9]) ).
fof(f2697,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)) = rd(rd(rd(X1,X0),rd(ld(X0,X0),X0)),mult(rd(ld(X0,X1),X0),X0)),
inference(forward_demodulation,[],[f2659,f3]) ).
fof(f2700,plain,
rd(ld(ld(x1,sF0),ld(x1,sF0)),ld(x1,sF0)) = rd(rd(sF0,ld(x1,sF0)),mult(ld(x1,sF0),x1)),
inference(forward_demodulation,[],[f2666,f42]) ).
fof(f2718,plain,
! [X0] : rd(X0,x1) = mult(X0,rd(sF0,x1)),
inference(backward_demodulation,[],[f304,f2690]) ).
fof(f2733,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)) = rd(rd(rd(X1,X0),rd(ld(X0,X0),X0)),ld(X0,X1)),
inference(forward_demodulation,[],[f2697,f3]) ).
fof(f2734,plain,
rd(ld(rd(sF0,x1),rd(sF0,x1)),rd(sF0,x1)) = rd(rd(sF0,rd(sF0,x1)),mult(rd(sF0,x1),x1)),
inference(forward_demodulation,[],[f2700,f2690]) ).
fof(f2748,plain,
! [X1] : mult(sF0,mult(x1,sF0)) = ld(rd(X1,x1),X1),
inference(backward_demodulation,[],[f1758,f2718]) ).
fof(f2765,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)) = mult(rd(rd(X1,X0),rd(ld(X0,X0),X0)),ld(X1,X0)),
inference(forward_demodulation,[],[f2733,f300]) ).
fof(f2766,plain,
rd(ld(rd(sF0,x1),rd(sF0,x1)),rd(sF0,x1)) = rd(rd(sF0,rd(sF0,x1)),sF0),
inference(forward_demodulation,[],[f2734,f3]) ).
fof(f2782,plain,
x1 = mult(sF0,mult(x1,sF0)),
inference(forward_demodulation,[],[f2748,f15]) ).
fof(f2785,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)) = mult(mult(rd(mult(rd(X1,X0),X0),X0),X0),ld(X1,X0)),
inference(forward_demodulation,[],[f2765,f2122]) ).
fof(f2786,plain,
rd(ld(rd(sF0,x1),rd(sF0,x1)),rd(sF0,x1)) = mult(rd(sF0,rd(sF0,x1)),sF0),
inference(forward_demodulation,[],[f2766,f1076]) ).
fof(f2796,plain,
! [X1] : mult(X1,x1) = rd(X1,rd(sF0,x1)),
inference(backward_demodulation,[],[f1431,f2782]) ).
fof(f2800,plain,
! [X0,X1] : rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)) = mult(mult(rd(X1,X0),X0),ld(X1,X0)),
inference(forward_demodulation,[],[f2785,f3]) ).
fof(f2801,plain,
mult(rd(sF0,rd(sF0,x1)),sF0) = rd(rd(rd(sF0,x1),rd(sF0,x1)),rd(sF0,x1)),
inference(forward_demodulation,[],[f2786,f2573]) ).
fof(f2814,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = rd(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),rd(ld(X0,X0),X0)),
inference(forward_demodulation,[],[f2800,f3]) ).
fof(f2815,plain,
mult(rd(sF0,rd(sF0,x1)),sF0) = mult(rd(rd(sF0,x1),rd(sF0,x1)),x1),
inference(forward_demodulation,[],[f2801,f2796]) ).
fof(f2822,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = mult(rd(mult(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),X0),X0),X0),
inference(forward_demodulation,[],[f2814,f2122]) ).
fof(f2823,plain,
mult(rd(sF0,rd(sF0,x1)),sF0) = mult(mult(rd(sF0,x1),x1),x1),
inference(forward_demodulation,[],[f2815,f2796]) ).
fof(f2828,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = mult(ld(rd(ld(X0,X0),X0),rd(ld(X0,X0),X0)),X0),
inference(forward_demodulation,[],[f2822,f3]) ).
fof(f2829,plain,
mult(sF0,x1) = mult(rd(sF0,rd(sF0,x1)),sF0),
inference(forward_demodulation,[],[f2823,f3]) ).
fof(f2832,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = mult(ld(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0)),X0),
inference(forward_demodulation,[],[f2828,f2573]) ).
fof(f2833,plain,
mult(sF0,x1) = mult(mult(sF0,x1),sF0),
inference(forward_demodulation,[],[f2829,f2796]) ).
fof(f2834,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = mult(X0,mult(rd(rd(X0,X0),X0),X0)),
inference(forward_demodulation,[],[f2832,f2630]) ).
fof(f2835,plain,
x1 = mult(x1,sF0),
inference(forward_demodulation,[],[f2833,f14]) ).
fof(f2836,plain,
! [X0,X1] : mult(X1,ld(X1,X0)) = mult(X0,rd(X0,X0)),
inference(forward_demodulation,[],[f2834,f3]) ).
fof(f2837,plain,
! [X0] : mult(mult(X0,sF0),x1) = mult(mult(X0,x1),sF0),
inference(backward_demodulation,[],[f2127,f2835]) ).
fof(f2841,plain,
! [X0] : mult(X0,rd(X0,X0)) = X0,
inference(forward_demodulation,[],[f2836,f1]) ).
fof(f2848,plain,
! [X0] : ld(X0,X0) = rd(X0,X0),
inference(superposition,[],[f2,f2841]) ).
fof(f2851,plain,
! [X0,X1] : mult(mult(X1,X0),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),X0)),
inference(superposition,[],[f18,f2841]) ).
fof(f2858,plain,
! [X0,X1] : rd(X1,rd(X0,X0)) = mult(X1,ld(X0,X0)),
inference(superposition,[],[f266,f2841]) ).
fof(f2871,plain,
! [X0,X1] : mult(mult(X1,X0),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f2851,f3]) ).
fof(f2873,plain,
! [X0,X1] : mult(ld(X1,rd(X1,X0)),X0) = rd(X0,X0),
inference(backward_demodulation,[],[f131,f2848]) ).
fof(f2874,plain,
! [X0,X1] : mult(ld(mult(X0,X1),X0),X1) = rd(X1,X1),
inference(backward_demodulation,[],[f184,f2848]) ).
fof(f2877,plain,
! [X0,X1] : ld(X1,rd(X1,X0)) = rd(rd(X0,X0),X0),
inference(backward_demodulation,[],[f192,f2848]) ).
fof(f2878,plain,
! [X2,X0,X1] : mult(ld(X1,rd(X1,X0)),mult(X0,mult(X2,X0))) = mult(mult(rd(X0,X0),X2),X0),
inference(backward_demodulation,[],[f193,f2848]) ).
fof(f2881,plain,
! [X0,X1] : ld(mult(X0,X1),X0) = rd(rd(X1,X1),X1),
inference(backward_demodulation,[],[f201,f2848]) ).
fof(f2899,plain,
! [X0,X1] : rd(ld(X0,rd(X0,X1)),X1) = rd(ld(X1,rd(X1,X1)),X1),
inference(backward_demodulation,[],[f2231,f2848]) ).
fof(f2910,plain,
! [X0,X1] : mult(X1,rd(X0,X0)) = rd(X1,rd(X0,X0)),
inference(backward_demodulation,[],[f2858,f2848]) ).
fof(f2936,plain,
! [X0,X1] : mult(mult(X1,X0),rd(X0,X0)) = mult(mult(X1,rd(X0,X0)),X0),
inference(backward_demodulation,[],[f2871,f2910]) ).
fof(f2939,plain,
! [X0,X1] : rd(ld(X0,rd(X0,X1)),X1) = rd(rd(rd(X1,X1),X1),X1),
inference(backward_demodulation,[],[f2899,f2877]) ).
fof(f2948,plain,
! [X0,X1] : mult(mult(X1,X0),rd(X0,X0)) = mult(rd(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f2936,f60]) ).
fof(f2961,plain,
ld(sF1,mult(x0,sF0)) = mult(sF0,mult(rd(x0,x0),sF0)),
inference(superposition,[],[f1121,f2848]) ).
fof(f2962,plain,
ld(sF1,sF1) = mult(sF0,mult(rd(x0,x0),sF0)),
inference(forward_demodulation,[],[f2961,f11]) ).
fof(f2964,plain,
rd(sF1,sF1) = mult(sF0,mult(rd(x0,x0),sF0)),
inference(forward_demodulation,[],[f2962,f2848]) ).
fof(f2974,plain,
! [X2,X0,X1] : mult(mult(X0,X2),rd(X1,X1)) = mult(mult(X0,rd(X1,X1)),mult(rd(X1,X1),mult(X2,rd(X1,X1)))),
inference(superposition,[],[f18,f2910]) ).
fof(f2984,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X1)),rd(X1,X1)) = X0,
inference(superposition,[],[f4,f2910]) ).
fof(f3289,plain,
! [X0,X1] : ld(X0,mult(X1,X0)) = mult(mult(rd(rd(X0,X0),X0),X1),X0),
inference(superposition,[],[f3,f2613]) ).
fof(f3434,plain,
! [X2,X0,X1] : mult(X1,ld(rd(X2,X0),X2)) = rd(X1,rd(rd(X0,X0),X0)),
inference(superposition,[],[f300,f2877]) ).
fof(f3462,plain,
! [X0,X1] : mult(X1,X0) = rd(X1,rd(rd(X0,X0),X0)),
inference(forward_demodulation,[],[f3434,f15]) ).
fof(f4364,plain,
! [X0,X1] : mult(mult(mult(X0,X1),X1),rd(X1,X1)) = mult(X0,mult(X1,X1)),
inference(superposition,[],[f2948,f4]) ).
fof(f4373,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0))) = mult(rd(X1,rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),X0)),
inference(superposition,[],[f2948,f2600]) ).
fof(f4375,plain,
! [X0,X1] : mult(X1,X1) = ld(rd(X0,X1),mult(mult(X0,X1),rd(X1,X1))),
inference(superposition,[],[f2,f2948]) ).
fof(f4389,plain,
! [X0,X1] : rd(mult(X1,X1),mult(X1,X1)) = mult(ld(mult(mult(X0,X1),rd(X1,X1)),rd(X0,X1)),mult(X1,X1)),
inference(superposition,[],[f2874,f2948]) ).
fof(f4390,plain,
! [X0,X1] : ld(mult(mult(X0,X1),rd(X1,X1)),rd(X0,X1)) = rd(rd(mult(X1,X1),mult(X1,X1)),mult(X1,X1)),
inference(superposition,[],[f2881,f2948]) ).
fof(f4393,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0))) = mult(mult(X1,X0),rd(rd(rd(X0,X0),X0),X0)),
inference(forward_demodulation,[],[f4373,f3462]) ).
fof(f4404,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0))) = rd(mult(X1,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f4393,f2610]) ).
fof(f4414,plain,
! [X0,X1] : rd(mult(X1,rd(X0,X0)),X0) = rd(mult(X1,rd(rd(rd(X0,X0),X0),X0)),rd(rd(X0,X0),X0)),
inference(forward_demodulation,[],[f4404,f2610]) ).
fof(f4420,plain,
! [X0,X1] : rd(mult(X1,rd(X0,X0)),X0) = mult(mult(X1,rd(rd(rd(X0,X0),X0),X0)),X0),
inference(forward_demodulation,[],[f4414,f3462]) ).
fof(f4426,plain,
! [X0,X1] : rd(mult(X1,rd(X0,X0)),X0) = mult(rd(X1,X0),mult(X0,rd(rd(X0,X0),X0))),
inference(forward_demodulation,[],[f4420,f60]) ).
fof(f4431,plain,
! [X0,X1] : rd(mult(X1,rd(X0,X0)),X0) = mult(rd(X1,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f4426,f2600]) ).
fof(f4446,plain,
! [X0,X1] : mult(X1,X1) = ld(ld(mult(X0,X1),X0),mult(mult(rd(X1,X1),X1),rd(X1,X1))),
inference(superposition,[],[f4375,f2881]) ).
fof(f4447,plain,
! [X0,X1] : mult(X1,X1) = ld(ld(X0,rd(X0,X1)),mult(mult(rd(X1,X1),X1),rd(X1,X1))),
inference(superposition,[],[f4375,f2877]) ).
fof(f4471,plain,
mult(x1,x1) = ld(rd(sF0,x1),mult(x1,rd(x1,x1))),
inference(superposition,[],[f4375,f14]) ).
fof(f4501,plain,
mult(x1,x1) = ld(rd(sF0,x1),x1),
inference(forward_demodulation,[],[f4471,f2841]) ).
fof(f4518,plain,
! [X0,X1] : mult(X1,X1) = ld(ld(X0,rd(X0,X1)),mult(X1,rd(X1,X1))),
inference(forward_demodulation,[],[f4447,f3]) ).
fof(f4519,plain,
! [X0,X1] : mult(X1,X1) = ld(ld(mult(X0,X1),X0),mult(X1,rd(X1,X1))),
inference(forward_demodulation,[],[f4446,f3]) ).
fof(f4548,plain,
! [X0,X1] : mult(X1,X1) = ld(ld(X0,rd(X0,X1)),X1),
inference(forward_demodulation,[],[f4518,f2841]) ).
fof(f4549,plain,
! [X0,X1] : mult(X1,X1) = ld(ld(mult(X0,X1),X0),X1),
inference(forward_demodulation,[],[f4519,f2841]) ).
fof(f4587,plain,
! [X2,X0,X1] : mult(ld(X2,rd(X2,X1)),ld(X2,rd(X2,X1))) = ld(ld(rd(X0,X1),X0),ld(X2,rd(X2,X1))),
inference(superposition,[],[f4549,f227]) ).
fof(f4588,plain,
! [X2,X0,X1] : mult(ld(mult(X2,X1),X2),ld(mult(X2,X1),X2)) = ld(ld(rd(X0,X1),X0),ld(mult(X2,X1),X2)),
inference(superposition,[],[f4549,f266]) ).
fof(f4593,plain,
! [X0,X1] : mult(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1)) = ld(ld(rd(X0,X1),X0),rd(rd(X1,X1),X1)),
inference(superposition,[],[f4549,f2600]) ).
fof(f4617,plain,
! [X2,X0,X1] : rd(X1,mult(X0,X0)) = mult(X1,ld(X0,ld(mult(X2,X0),X2))),
inference(superposition,[],[f300,f4549]) ).
fof(f4636,plain,
! [X1] : mult(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1)) = ld(X1,rd(rd(X1,X1),X1)),
inference(forward_demodulation,[],[f4593,f15]) ).
fof(f4639,plain,
! [X2,X1] : mult(ld(mult(X2,X1),X2),ld(mult(X2,X1),X2)) = ld(X1,ld(mult(X2,X1),X2)),
inference(forward_demodulation,[],[f4588,f15]) ).
fof(f4640,plain,
! [X2,X1] : mult(ld(X2,rd(X2,X1)),ld(X2,rd(X2,X1))) = ld(X1,ld(X2,rd(X2,X1))),
inference(forward_demodulation,[],[f4587,f15]) ).
fof(f4650,plain,
! [X1] : rd(ld(X1,rd(X1,X1)),X1) = ld(X1,rd(rd(X1,X1),X1)),
inference(forward_demodulation,[],[f4636,f2612]) ).
fof(f4653,plain,
! [X2,X1] : rd(ld(mult(X2,X1),X2),X1) = ld(X1,ld(mult(X2,X1),X2)),
inference(forward_demodulation,[],[f4639,f266]) ).
fof(f4654,plain,
! [X2,X1] : rd(ld(X2,rd(X2,X1)),X1) = ld(X1,ld(X2,rd(X2,X1))),
inference(forward_demodulation,[],[f4640,f227]) ).
fof(f4659,plain,
! [X1] : rd(rd(rd(X1,X1),X1),X1) = ld(X1,rd(rd(X1,X1),X1)),
inference(forward_demodulation,[],[f4650,f2939]) ).
fof(f4661,plain,
! [X2,X0,X1] : rd(X1,mult(X0,X0)) = mult(X1,rd(ld(mult(X2,X0),X2),X0)),
inference(backward_demodulation,[],[f4617,f4653]) ).
fof(f4665,plain,
! [X2,X1] : mult(X2,rd(rd(rd(X1,X1),X1),X1)) = rd(X2,mult(X1,X1)),
inference(backward_demodulation,[],[f2625,f4661]) ).
fof(f4668,plain,
! [X2,X0,X1] : mult(X2,rd(ld(X0,rd(X0,X1)),X1)) = rd(X2,mult(X1,X1)),
inference(backward_demodulation,[],[f2626,f4665]) ).
fof(f4840,plain,
! [X0,X1] : mult(mult(X0,X1),mult(X1,mult(rd(X1,X1),X1))) = mult(mult(X0,mult(X1,X1)),X1),
inference(superposition,[],[f5,f4364]) ).
fof(f4841,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(mult(X0,mult(X1,X1)),rd(X1,X1)),
inference(superposition,[],[f2984,f4364]) ).
fof(f4873,plain,
! [X0,X1] : mult(mult(X0,X1),mult(X1,X1)) = mult(mult(X0,mult(X1,X1)),X1),
inference(forward_demodulation,[],[f4840,f3]) ).
fof(f4972,plain,
! [X0,X1] : mult(rd(mult(X0,X0),mult(X0,X0)),X0) = mult(mult(ld(X1,rd(X1,mult(X0,X0))),X0),mult(X0,X0)),
inference(superposition,[],[f4873,f2873]) ).
fof(f4976,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(rd(X0,mult(X1,X1)),X1),mult(X1,X1)),
inference(superposition,[],[f4873,f3]) ).
fof(f5008,plain,
! [X0,X1] : rd(mult(X0,mult(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),X1) = mult(mult(X0,rd(rd(X1,X1),X1)),mult(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(superposition,[],[f2600,f4873]) ).
fof(f5013,plain,
! [X0,X1] : rd(mult(X0,rd(ld(X1,rd(X1,X1)),X1)),X1) = mult(mult(X0,rd(rd(X1,X1),X1)),rd(ld(X1,rd(X1,X1)),X1)),
inference(forward_demodulation,[],[f5008,f2612]) ).
fof(f5034,plain,
! [X0,X1] : rd(mult(X0,rd(ld(X1,rd(X1,X1)),X1)),X1) = rd(mult(X0,rd(rd(X1,X1),X1)),mult(X1,X1)),
inference(forward_demodulation,[],[f5013,f4668]) ).
fof(f5049,plain,
! [X0,X1] : rd(rd(X0,X1),mult(X1,X1)) = rd(mult(X0,rd(ld(X1,rd(X1,X1)),X1)),X1),
inference(forward_demodulation,[],[f5034,f2600]) ).
fof(f5061,plain,
! [X0,X1] : rd(rd(X0,X1),mult(X1,X1)) = rd(rd(X0,mult(X1,X1)),X1),
inference(forward_demodulation,[],[f5049,f4668]) ).
fof(f5075,plain,
x1 = mult(rd(sF0,x1),mult(x1,x1)),
inference(superposition,[],[f1,f4501]) ).
fof(f5076,plain,
x1 = mult(mult(sF0,x1),rd(x1,x1)),
inference(forward_demodulation,[],[f5075,f2948]) ).
fof(f5081,plain,
x1 = mult(mult(sF0,x1),sF0),
inference(forward_demodulation,[],[f5076,f9]) ).
fof(f5090,plain,
x1 = mult(mult(sF0,sF0),x1),
inference(forward_demodulation,[],[f5081,f2837]) ).
fof(f5106,plain,
rd(x1,x1) = mult(sF0,sF0),
inference(superposition,[],[f4,f5090]) ).
fof(f5136,plain,
sF0 = mult(sF0,sF0),
inference(forward_demodulation,[],[f5106,f9]) ).
fof(f5150,plain,
! [X0] : mult(mult(sF0,X0),sF0) = mult(sF0,mult(sF0,mult(X0,sF0))),
inference(backward_demodulation,[],[f1296,f5136]) ).
fof(f5160,plain,
! [X0] : ld(sF0,mult(X0,sF0)) = mult(sF0,mult(ld(sF0,X0),sF0)),
inference(backward_demodulation,[],[f1377,f5136]) ).
fof(f5162,plain,
! [X0] : mult(X0,sF0) = mult(sF0,mult(sF0,mult(sF0,mult(X0,sF0)))),
inference(backward_demodulation,[],[f2420,f5136]) ).
fof(f5176,plain,
! [X0] : ld(sF0,mult(X0,sF0)) = mult(sF0,mult(sF0,mult(X0,sF0))),
inference(forward_demodulation,[],[f5160,f2253]) ).
fof(f5178,plain,
! [X0] : mult(X0,sF0) = mult(sF0,mult(mult(sF0,X0),sF0)),
inference(backward_demodulation,[],[f5162,f5150]) ).
fof(f5182,plain,
! [X0] : mult(mult(sF0,X0),sF0) = ld(sF0,mult(X0,sF0)),
inference(forward_demodulation,[],[f5176,f5150]) ).
fof(f5270,plain,
! [X2,X0,X1] : ld(X1,mult(X2,X1)) = mult(mult(ld(X0,rd(X0,X1)),X2),X1),
inference(superposition,[],[f3289,f2877]) ).
fof(f5296,plain,
! [X0] : ld(X0,mult(mult(X0,X0),X0)) = mult(mult(rd(rd(X0,X0),X0),X0),mult(X0,X0)),
inference(superposition,[],[f4873,f3289]) ).
fof(f5345,plain,
! [X0] : mult(rd(X0,X0),mult(X0,X0)) = ld(X0,mult(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f5296,f3]) ).
fof(f5366,plain,
! [X0] : mult(rd(mult(X0,X0),mult(X0,X0)),X0) = ld(mult(X0,X0),mult(X0,mult(X0,X0))),
inference(backward_demodulation,[],[f4972,f5270]) ).
fof(f5384,plain,
! [X0] : mult(mult(X0,X0),rd(X0,X0)) = ld(X0,mult(mult(X0,X0),X0)),
inference(forward_demodulation,[],[f5345,f2948]) ).
fof(f5575,plain,
! [X0] : ld(sF0,X0) = mult(mult(sF0,mult(X0,sF0)),sF0),
inference(superposition,[],[f5182,f1140]) ).
fof(f5580,plain,
ld(sF0,sF1) = mult(mult(sF0,x0),sF0),
inference(superposition,[],[f5182,f11]) ).
fof(f5583,plain,
ld(sF0,x0) = mult(mult(sF0,sF1),sF0),
inference(superposition,[],[f5182,f1096]) ).
fof(f5600,plain,
! [X0] : ld(sF0,X0) = mult(mult(sF0,sF0),mult(sF0,X0)),
inference(forward_demodulation,[],[f5575,f1205]) ).
fof(f5610,plain,
! [X0] : ld(sF0,X0) = mult(sF0,mult(sF0,X0)),
inference(forward_demodulation,[],[f5600,f5136]) ).
fof(f5641,plain,
! [X0,X1] : mult(mult(sF0,X0),mult(ld(X1,sF0),mult(sF0,X0))) = ld(rd(X1,mult(sF0,X0)),ld(sF0,X0)),
inference(superposition,[],[f71,f5610]) ).
fof(f5851,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(rd(mult(mult(X0,X0),rd(X0,X0)),X0),rd(mult(mult(X0,X0),X0),X0)),
inference(superposition,[],[f2615,f5384]) ).
fof(f5863,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(rd(mult(mult(X0,X0),rd(X0,X0)),X0),mult(X0,X0)),
inference(forward_demodulation,[],[f5851,f4]) ).
fof(f5880,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(mult(rd(mult(X0,X0),X0),rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f5863,f4431]) ).
fof(f5895,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(mult(X0,rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f5880,f4]) ).
fof(f5909,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(X0,mult(X0,X0)),
inference(forward_demodulation,[],[f5895,f2841]) ).
fof(f5921,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(X0,mult(X0,X0))),
inference(backward_demodulation,[],[f2600,f5909]) ).
fof(f5929,plain,
! [X2,X0,X1] : rd(mult(X1,rd(X2,X0)),X2) = mult(mult(X1,X2),rd(rd(X0,mult(X0,X0)),X2)),
inference(backward_demodulation,[],[f2610,f5909]) ).
fof(f5931,plain,
! [X2,X1] : rd(ld(X1,X2),X1) = mult(rd(X1,mult(X1,X1)),rd(X2,X1)),
inference(backward_demodulation,[],[f2612,f5909]) ).
fof(f5933,plain,
! [X0,X1] : rd(rd(ld(X0,X1),X0),rd(X1,X0)) = rd(X0,mult(X0,X0)),
inference(backward_demodulation,[],[f2615,f5909]) ).
fof(f5941,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = ld(rd(X1,mult(X1,X1)),rd(X0,X1)),
inference(backward_demodulation,[],[f2627,f5909]) ).
fof(f5984,plain,
! [X0,X1] : mult(X1,X0) = rd(X1,rd(X0,mult(X0,X0))),
inference(backward_demodulation,[],[f3462,f5909]) ).
fof(f5994,plain,
! [X1] : rd(rd(X1,mult(X1,X1)),X1) = ld(X1,rd(X1,mult(X1,X1))),
inference(backward_demodulation,[],[f4659,f5909]) ).
fof(f5995,plain,
! [X2,X1] : rd(X2,mult(X1,X1)) = mult(X2,rd(rd(X1,mult(X1,X1)),X1)),
inference(backward_demodulation,[],[f4665,f5909]) ).
fof(f6010,plain,
! [X0,X1] : ld(mult(mult(X0,X1),rd(X1,X1)),rd(X0,X1)) = rd(mult(X1,X1),mult(mult(X1,X1),mult(X1,X1))),
inference(backward_demodulation,[],[f4390,f5909]) ).
fof(f6048,plain,
! [X2,X1] : rd(X2,mult(X1,X1)) = mult(X2,rd(rd(X1,X1),mult(X1,X1))),
inference(forward_demodulation,[],[f5995,f5061]) ).
fof(f6049,plain,
! [X1] : rd(rd(X1,X1),mult(X1,X1)) = ld(X1,rd(X1,mult(X1,X1))),
inference(forward_demodulation,[],[f5994,f5061]) ).
fof(f6098,plain,
! [X0,X1] : ld(X1,rd(X1,X0)) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f2877,f5909]) ).
fof(f6099,plain,
! [X0] : rd(X0,X0) = mult(rd(X0,mult(X0,X0)),X0),
inference(superposition,[],[f3,f5909]) ).
fof(f6287,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))) = mult(rd(X1,rd(X0,mult(X0,X0))),rd(rd(X0,mult(X0,X0)),X0)),
inference(superposition,[],[f2948,f5921]) ).
fof(f6344,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))) = mult(rd(X1,rd(X0,mult(X0,X0))),rd(rd(X0,X0),mult(X0,X0))),
inference(forward_demodulation,[],[f6287,f5061]) ).
fof(f6382,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))) = rd(rd(X1,rd(X0,mult(X0,X0))),mult(X0,X0)),
inference(forward_demodulation,[],[f6344,f6048]) ).
fof(f6416,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))) = rd(mult(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f6382,f5984]) ).
fof(f6435,plain,
! [X0,X1] : rd(mult(X1,X0),mult(X0,X0)) = rd(mult(X1,rd(rd(X0,mult(X0,X0)),X0)),rd(X0,mult(X0,X0))),
inference(forward_demodulation,[],[f6416,f5929]) ).
fof(f6446,plain,
! [X0,X1] : rd(mult(X1,X0),mult(X0,X0)) = mult(mult(X1,rd(rd(X0,mult(X0,X0)),X0)),X0),
inference(forward_demodulation,[],[f6435,f5984]) ).
fof(f6453,plain,
! [X0,X1] : rd(mult(X1,X0),mult(X0,X0)) = mult(rd(X1,X0),mult(X0,rd(X0,mult(X0,X0)))),
inference(forward_demodulation,[],[f6446,f60]) ).
fof(f6457,plain,
! [X0,X1] : mult(rd(X1,X0),rd(X0,X0)) = rd(mult(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f6453,f5921]) ).
fof(f6459,plain,
! [X0,X1] : mult(rd(X1,X1),rd(X1,X1)) = mult(ld(mult(mult(X0,X1),rd(X1,X1)),rd(X0,X1)),mult(X1,X1)),
inference(backward_demodulation,[],[f4389,f6457]) ).
fof(f6462,plain,
! [X0] : mult(mult(rd(X0,X0),rd(X0,X0)),X0) = ld(mult(X0,X0),mult(X0,mult(X0,X0))),
inference(backward_demodulation,[],[f5366,f6457]) ).
fof(f6466,plain,
! [X0] : mult(rd(rd(X0,X0),X0),mult(X0,X0)) = ld(mult(X0,X0),mult(X0,mult(X0,X0))),
inference(forward_demodulation,[],[f6462,f60]) ).
fof(f6467,plain,
! [X0] : mult(mult(rd(X0,X0),X0),rd(X0,X0)) = ld(mult(X0,X0),mult(X0,mult(X0,X0))),
inference(forward_demodulation,[],[f6466,f2948]) ).
fof(f6468,plain,
! [X0] : mult(X0,rd(X0,X0)) = ld(mult(X0,X0),mult(X0,mult(X0,X0))),
inference(forward_demodulation,[],[f6467,f3]) ).
fof(f6469,plain,
! [X0] : ld(mult(X0,X0),mult(X0,mult(X0,X0))) = X0,
inference(forward_demodulation,[],[f6468,f2841]) ).
fof(f6725,plain,
! [X0,X1] : mult(mult(X1,mult(X1,X1)),rd(mult(X1,X1),mult(X1,X1))) = mult(ld(X0,rd(X0,X1)),mult(mult(X1,X1),mult(X1,X1))),
inference(superposition,[],[f2948,f6098]) ).
fof(f6727,plain,
! [X0,X1] : mult(mult(X1,X1),mult(X1,X1)) = ld(ld(X1,ld(X0,rd(X0,X1))),mult(X1,X1)),
inference(superposition,[],[f4548,f6098]) ).
fof(f6730,plain,
! [X0,X1] : mult(mult(X1,X1),mult(X1,X1)) = ld(rd(ld(X0,rd(X0,X1)),X1),mult(X1,X1)),
inference(forward_demodulation,[],[f6727,f4654]) ).
fof(f6732,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),mult(mult(X1,X1),mult(X1,X1))) = mult(mult(X1,mult(X1,X1)),mult(rd(X1,X1),rd(X1,X1))),
inference(forward_demodulation,[],[f6725,f6457]) ).
fof(f6750,plain,
! [X0,X1] : mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(ld(ld(X0,rd(X0,X1)),X1),X1)),
inference(forward_demodulation,[],[f6730,f71]) ).
fof(f6764,plain,
! [X1] : mult(mult(X1,X1),mult(X1,X1)) = mult(X1,mult(mult(X1,X1),X1)),
inference(forward_demodulation,[],[f6750,f4548]) ).
fof(f6777,plain,
! [X0,X1] : ld(mult(mult(X0,X1),rd(X1,X1)),rd(X0,X1)) = rd(mult(X1,X1),mult(X1,mult(mult(X1,X1),X1))),
inference(backward_demodulation,[],[f6010,f6764]) ).
fof(f6782,plain,
! [X0,X1] : mult(mult(X1,mult(X1,X1)),mult(rd(X1,X1),rd(X1,X1))) = mult(ld(X0,rd(X0,X1)),mult(X1,mult(mult(X1,X1),X1))),
inference(backward_demodulation,[],[f6732,f6764]) ).
fof(f6789,plain,
! [X1] : mult(mult(X1,mult(X1,X1)),mult(rd(X1,X1),rd(X1,X1))) = mult(mult(rd(X1,X1),mult(X1,X1)),X1),
inference(forward_demodulation,[],[f6782,f2878]) ).
fof(f6792,plain,
! [X0,X1] : ld(mult(mult(X0,X1),rd(X1,X1)),rd(X0,X1)) = rd(rd(X1,mult(X1,X1)),X1),
inference(forward_demodulation,[],[f6777,f1887]) ).
fof(f6798,plain,
! [X1] : mult(mult(X1,mult(X1,X1)),mult(rd(X1,X1),rd(X1,X1))) = mult(mult(rd(X1,X1),X1),mult(X1,X1)),
inference(forward_demodulation,[],[f6789,f4873]) ).
fof(f6801,plain,
! [X0,X1] : ld(mult(mult(X0,X1),rd(X1,X1)),rd(X0,X1)) = rd(rd(X1,X1),mult(X1,X1)),
inference(forward_demodulation,[],[f6792,f5061]) ).
fof(f6807,plain,
! [X1] : mult(X1,mult(X1,X1)) = mult(mult(X1,mult(X1,X1)),mult(rd(X1,X1),rd(X1,X1))),
inference(forward_demodulation,[],[f6798,f3]) ).
fof(f6810,plain,
! [X1] : mult(rd(X1,X1),rd(X1,X1)) = mult(rd(rd(X1,X1),mult(X1,X1)),mult(X1,X1)),
inference(backward_demodulation,[],[f6459,f6801]) ).
fof(f6815,plain,
! [X1] : rd(X1,X1) = mult(rd(X1,X1),rd(X1,X1)),
inference(forward_demodulation,[],[f6810,f3]) ).
fof(f6825,plain,
! [X1] : mult(X1,mult(X1,X1)) = mult(mult(X1,mult(X1,X1)),rd(X1,X1)),
inference(backward_demodulation,[],[f6807,f6815]) ).
fof(f6827,plain,
! [X1] : mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
inference(forward_demodulation,[],[f6825,f4841]) ).
fof(f6833,plain,
! [X0] : mult(mult(X0,X0),rd(X0,X0)) = ld(X0,mult(X0,mult(X0,X0))),
inference(backward_demodulation,[],[f5384,f6827]) ).
fof(f6869,plain,
! [X0] : mult(X0,X0) = mult(mult(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f6833,f2]) ).
fof(f7068,plain,
! [X0,X1] : mult(mult(X1,mult(X0,X0)),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),mult(X0,X0))),
inference(superposition,[],[f18,f6869]) ).
fof(f7094,plain,
! [X0,X1] : mult(mult(X1,mult(X0,X0)),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),mult(mult(X0,X0),rd(X0,X0))),
inference(forward_demodulation,[],[f7068,f2948]) ).
fof(f7118,plain,
! [X0,X1] : mult(mult(X1,mult(X0,X0)),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f7094,f6869]) ).
fof(f7139,plain,
! [X0,X1] : mult(mult(X1,mult(X0,X0)),rd(X0,X0)) = mult(mult(X1,rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f7118,f2910]) ).
fof(f7152,plain,
! [X0,X1] : mult(mult(X1,X0),X0) = mult(mult(X1,rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f7139,f4841]) ).
fof(f8493,plain,
! [X0] : rd(X0,mult(X0,X0)) = ld(rd(rd(X0,mult(X0,X0)),X0),mult(rd(X0,mult(X0,X0)),rd(rd(X0,mult(X0,X0)),X0))),
inference(superposition,[],[f6469,f5921]) ).
fof(f8509,plain,
! [X0] : rd(X0,mult(X0,X0)) = ld(rd(rd(X0,mult(X0,X0)),X0),rd(ld(X0,rd(X0,mult(X0,X0))),X0)),
inference(forward_demodulation,[],[f8493,f5931]) ).
fof(f8518,plain,
! [X0] : rd(X0,mult(X0,X0)) = ld(rd(rd(X0,mult(X0,X0)),X0),rd(rd(rd(X0,X0),mult(X0,X0)),X0)),
inference(forward_demodulation,[],[f8509,f6049]) ).
fof(f8525,plain,
! [X0] : rd(X0,mult(X0,X0)) = ld(rd(rd(X0,mult(X0,X0)),X0),rd(rd(rd(X0,X0),X0),mult(X0,X0))),
inference(forward_demodulation,[],[f8518,f5061]) ).
fof(f8528,plain,
! [X0] : rd(X0,mult(X0,X0)) = ld(rd(rd(X0,mult(X0,X0)),X0),rd(rd(X0,mult(X0,X0)),mult(X0,X0))),
inference(forward_demodulation,[],[f8525,f5909]) ).
fof(f8531,plain,
! [X0] : rd(X0,mult(X0,X0)) = ld(rd(rd(X0,X0),mult(X0,X0)),rd(rd(X0,mult(X0,X0)),mult(X0,X0))),
inference(forward_demodulation,[],[f8528,f5061]) ).
fof(f8557,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(X0,mult(X0,X0))) = mult(mult(X1,rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))),rd(rd(X0,mult(X0,X0)),X0)),
inference(superposition,[],[f7152,f5921]) ).
fof(f8602,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(X0,mult(X0,X0))) = mult(mult(X1,rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))),rd(rd(X0,X0),mult(X0,X0))),
inference(forward_demodulation,[],[f8557,f5061]) ).
fof(f8636,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(X0,mult(X0,X0))) = rd(mult(X1,rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))),mult(X0,X0)),
inference(forward_demodulation,[],[f8602,f6048]) ).
fof(f8667,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(X0,mult(X0,X0))) = rd(mult(X1,mult(rd(X0,mult(X0,X0)),X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f8636,f5984]) ).
fof(f8686,plain,
! [X0,X1] : mult(mult(X1,rd(X0,mult(X0,X0))),rd(X0,mult(X0,X0))) = rd(mult(X1,rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f8667,f6099]) ).
fof(f8703,plain,
! [X0,X1] : rd(mult(X1,rd(X0,mult(X0,X0))),X0) = rd(mult(X1,rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f8686,f5921]) ).
fof(f8713,plain,
! [X0,X1] : rd(rd(X1,X0),X0) = rd(mult(X1,rd(X0,X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f8703,f5921]) ).
fof(f8793,plain,
mult(sF0,mult(sF1,mult(sF0,sF1))) = mult(ld(sF0,x0),sF1),
inference(superposition,[],[f5,f5583]) ).
fof(f8797,plain,
sF0 = ld(mult(sF0,sF1),ld(sF0,x0)),
inference(superposition,[],[f2,f5583]) ).
fof(f8810,plain,
rd(rd(sF0,sF0),sF0) = ld(ld(sF0,x0),mult(sF0,sF1)),
inference(superposition,[],[f2881,f5583]) ).
fof(f8822,plain,
mult(rd(sF0,sF0),sF0) = ld(ld(sF0,x0),mult(sF0,sF1)),
inference(forward_demodulation,[],[f8810,f1076]) ).
fof(f8839,plain,
sF0 = ld(ld(sF0,x0),mult(sF0,sF1)),
inference(forward_demodulation,[],[f8822,f3]) ).
fof(f9049,plain,
! [X0,X1] : mult(mult(X1,mult(sF0,X0)),sF0) = mult(rd(X1,sF0),mult(X0,sF0)),
inference(superposition,[],[f18,f5178]) ).
fof(f9080,plain,
! [X0,X1] : mult(mult(X1,mult(sF0,X0)),sF0) = mult(mult(X1,sF0),mult(X0,sF0)),
inference(forward_demodulation,[],[f9049,f1076]) ).
fof(f9246,plain,
! [X0,X1] : ld(rd(rd(X0,mult(X0,X0)),X0),X1) = mult(X0,mult(rd(mult(X0,X1),X0),X0)),
inference(superposition,[],[f96,f5941]) ).
fof(f9269,plain,
! [X0,X1] : ld(rd(rd(X0,mult(X0,X0)),X0),X1) = mult(X0,mult(X0,X1)),
inference(forward_demodulation,[],[f9246,f3]) ).
fof(f9312,plain,
! [X0,X1] : mult(X0,mult(X0,X1)) = ld(rd(rd(X0,X0),mult(X0,X0)),X1),
inference(forward_demodulation,[],[f9269,f5061]) ).
fof(f9337,plain,
! [X0] : rd(X0,mult(X0,X0)) = mult(X0,mult(X0,rd(rd(X0,mult(X0,X0)),mult(X0,X0)))),
inference(backward_demodulation,[],[f8531,f9312]) ).
fof(f10117,plain,
sF0 = ld(mult(sF0,x0),ld(sF0,sF1)),
inference(superposition,[],[f2,f5580]) ).
fof(f10130,plain,
rd(rd(sF0,sF0),sF0) = ld(ld(sF0,sF1),mult(sF0,x0)),
inference(superposition,[],[f2881,f5580]) ).
fof(f10142,plain,
mult(rd(sF0,sF0),sF0) = ld(ld(sF0,sF1),mult(sF0,x0)),
inference(forward_demodulation,[],[f10130,f1076]) ).
fof(f10160,plain,
sF0 = ld(ld(sF0,sF1),mult(sF0,x0)),
inference(forward_demodulation,[],[f10142,f3]) ).
fof(f10561,plain,
! [X0,X1] : ld(X1,rd(X1,mult(X0,X0))) = rd(mult(rd(X0,X0),rd(X0,X0)),mult(X0,X0)),
inference(superposition,[],[f2877,f6457]) ).
fof(f10562,plain,
! [X0,X1] : ld(mult(X1,mult(X0,X0)),X1) = rd(mult(rd(X0,X0),rd(X0,X0)),mult(X0,X0)),
inference(superposition,[],[f2881,f6457]) ).
fof(f10616,plain,
! [X0,X1] : rd(rd(rd(X0,X0),X0),X0) = ld(mult(X1,mult(X0,X0)),X1),
inference(forward_demodulation,[],[f10562,f8713]) ).
fof(f10617,plain,
! [X0,X1] : rd(rd(rd(X0,X0),X0),X0) = ld(X1,rd(X1,mult(X0,X0))),
inference(forward_demodulation,[],[f10561,f8713]) ).
fof(f10680,plain,
! [X0,X1] : ld(mult(X1,mult(X0,X0)),X1) = rd(rd(X0,mult(X0,X0)),X0),
inference(forward_demodulation,[],[f10616,f5909]) ).
fof(f10681,plain,
! [X0,X1] : ld(X1,rd(X1,mult(X0,X0))) = rd(rd(X0,mult(X0,X0)),X0),
inference(forward_demodulation,[],[f10617,f5909]) ).
fof(f10734,plain,
! [X0,X1] : ld(mult(X1,mult(X0,X0)),X1) = rd(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f10680,f5061]) ).
fof(f10735,plain,
! [X0,X1] : ld(X1,rd(X1,mult(X0,X0))) = rd(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f10681,f5061]) ).
fof(f11862,plain,
! [X0,X1] : mult(rd(X0,mult(X1,X1)),X1) = rd(mult(X0,X1),mult(X1,X1)),
inference(superposition,[],[f4,f4976]) ).
fof(f11895,plain,
! [X0,X1] : mult(rd(X0,X1),rd(X1,X1)) = mult(rd(X0,mult(X1,X1)),X1),
inference(forward_demodulation,[],[f11862,f6457]) ).
fof(f12385,plain,
mult(mult(rd(x0,x0),sF0),sF0) = mult(sF0,mult(rd(sF1,sF1),sF0)),
inference(superposition,[],[f5178,f2964]) ).
fof(f12388,plain,
! [X0] : mult(mult(X0,rd(x0,x0)),sF0) = mult(rd(X0,sF0),rd(sF1,sF1)),
inference(superposition,[],[f18,f2964]) ).
fof(f12425,plain,
! [X0] : mult(mult(X0,rd(x0,x0)),sF0) = mult(mult(X0,sF0),rd(sF1,sF1)),
inference(forward_demodulation,[],[f12388,f1076]) ).
fof(f12428,plain,
rd(x0,x0) = mult(sF0,mult(rd(sF1,sF1),sF0)),
inference(forward_demodulation,[],[f12385,f1140]) ).
fof(f12860,plain,
mult(mult(sF0,rd(x0,x0)),rd(sF0,rd(x0,x0))) = rd(rd(sF1,sF1),rd(x0,x0)),
inference(superposition,[],[f28,f2964]) ).
fof(f12918,plain,
mult(mult(sF0,rd(x0,x0)),rd(sF0,rd(x0,x0))) = mult(rd(sF1,sF1),rd(x0,x0)),
inference(forward_demodulation,[],[f12860,f2910]) ).
fof(f12961,plain,
mult(rd(sF1,sF1),rd(x0,x0)) = mult(mult(sF0,rd(x0,x0)),mult(sF0,rd(x0,x0))),
inference(forward_demodulation,[],[f12918,f2910]) ).
fof(f13034,plain,
mult(mult(x0,x0),sF0) = mult(sF1,mult(sF0,sF1)),
inference(superposition,[],[f1080,f11]) ).
fof(f13045,plain,
! [X0] : mult(X0,sF0) = rd(mult(mult(X0,x0),sF0),mult(sF0,sF1)),
inference(superposition,[],[f4,f1080]) ).
fof(f14003,plain,
! [X0,X1] : rd(mult(rd(X0,X1),rd(X1,X1)),mult(X1,X1)) = mult(X0,rd(ld(mult(X1,X1),X1),mult(X1,X1))),
inference(superposition,[],[f2007,f11895]) ).
fof(f14010,plain,
! [X2,X3,X0,X1] : rd(rd(rd(X0,X1),X2),X1) = mult(X0,rd(ld(X1,ld(mult(X3,X2),X3)),X1)),
inference(superposition,[],[f2007,f266]) ).
fof(f14089,plain,
! [X2,X0,X1] : rd(X0,mult(X1,mult(X2,X1))) = rd(rd(rd(X0,X1),X2),X1),
inference(forward_demodulation,[],[f14010,f834]) ).
fof(f14095,plain,
! [X0,X1] : rd(mult(rd(X0,X1),rd(X1,X1)),mult(X1,X1)) = mult(X0,rd(rd(rd(X1,X1),X1),mult(X1,X1))),
inference(forward_demodulation,[],[f14003,f2881]) ).
fof(f14139,plain,
! [X0,X1] : rd(mult(rd(X0,X1),rd(X1,X1)),mult(X1,X1)) = mult(X0,rd(rd(X1,mult(X1,X1)),mult(X1,X1))),
inference(forward_demodulation,[],[f14095,f5909]) ).
fof(f14165,plain,
! [X0,X1] : rd(rd(rd(X0,X1),X1),X1) = mult(X0,rd(rd(X1,mult(X1,X1)),mult(X1,X1))),
inference(forward_demodulation,[],[f14139,f8713]) ).
fof(f14178,plain,
! [X0,X1] : mult(X0,rd(rd(X1,mult(X1,X1)),mult(X1,X1))) = rd(X0,mult(X1,mult(X1,X1))),
inference(forward_demodulation,[],[f14165,f14089]) ).
fof(f14183,plain,
! [X0] : rd(X0,mult(X0,X0)) = mult(X0,rd(X0,mult(X0,mult(X0,X0)))),
inference(backward_demodulation,[],[f9337,f14178]) ).
fof(f14194,plain,
! [X0] : ld(X0,rd(X0,mult(X0,X0))) = rd(X0,mult(X0,mult(X0,X0))),
inference(superposition,[],[f2,f14183]) ).
fof(f14244,plain,
! [X0] : rd(rd(X0,X0),mult(X0,X0)) = rd(X0,mult(X0,mult(X0,X0))),
inference(forward_demodulation,[],[f14194,f10735]) ).
fof(f18791,plain,
! [X0] : mult(rd(mult(X0,ld(sF0,x0)),mult(sF0,sF1)),ld(sF0,x0)) = rd(X0,rd(sF0,ld(sF0,x0))),
inference(superposition,[],[f2122,f8839]) ).
fof(f18792,plain,
! [X0] : mult(rd(mult(X0,ld(sF0,sF1)),mult(sF0,x0)),ld(sF0,sF1)) = rd(X0,rd(sF0,ld(sF0,sF1))),
inference(superposition,[],[f2122,f10160]) ).
fof(f18827,plain,
! [X2,X3,X0,X1] : mult(rd(mult(X3,ld(X0,X1)),X2),ld(X0,X1)) = rd(X3,mult(ld(ld(X0,X1),X2),ld(X1,X0))),
inference(superposition,[],[f2122,f300]) ).
fof(f18965,plain,
! [X2,X3,X0,X1] : mult(rd(mult(X3,ld(X0,X1)),X2),ld(X0,X1)) = rd(X3,mult(ld(X1,X0),mult(X2,ld(X1,X0)))),
inference(forward_demodulation,[],[f18827,f2261]) ).
fof(f18991,plain,
! [X0] : mult(rd(mult(X0,ld(sF0,sF1)),mult(sF0,x0)),ld(sF0,sF1)) = rd(X0,mult(sF0,ld(sF1,sF0))),
inference(forward_demodulation,[],[f18792,f300]) ).
fof(f18992,plain,
! [X0] : mult(rd(mult(X0,ld(sF0,x0)),mult(sF0,sF1)),ld(sF0,x0)) = rd(X0,mult(sF0,ld(x0,sF0))),
inference(forward_demodulation,[],[f18791,f300]) ).
fof(f19800,plain,
ld(sF1,sF0) = mult(ld(mult(ld(sF0,x0),sF1),sF0),sF1),
inference(superposition,[],[f147,f8839]) ).
fof(f22186,plain,
! [X0,X1] : mult(mult(X0,X1),ld(X1,X0)) = mult(X1,mult(ld(X1,X0),X0)),
inference(superposition,[],[f16,f1]) ).
fof(f22218,plain,
! [X2,X3,X0,X1] : rd(X3,mult(ld(X2,X0),mult(X1,ld(X2,X0)))) = mult(X3,ld(mult(mult(X0,X1),ld(X2,X0)),X2)),
inference(superposition,[],[f266,f16]) ).
fof(f22266,plain,
! [X2,X3,X0,X1] : mult(rd(mult(X3,ld(X0,X1)),X2),ld(X0,X1)) = mult(X3,ld(mult(mult(X0,X2),ld(X1,X0)),X1)),
inference(backward_demodulation,[],[f18965,f22218]) ).
fof(f22320,plain,
! [X0] : rd(X0,mult(sF0,ld(sF1,sF0))) = mult(X0,ld(mult(mult(sF0,mult(sF0,x0)),ld(sF1,sF0)),sF1)),
inference(backward_demodulation,[],[f18991,f22266]) ).
fof(f22321,plain,
! [X0] : rd(X0,mult(sF0,ld(x0,sF0))) = mult(X0,ld(mult(mult(sF0,mult(sF0,sF1)),ld(x0,sF0)),x0)),
inference(backward_demodulation,[],[f18992,f22266]) ).
fof(f22364,plain,
! [X0] : rd(X0,mult(sF0,ld(x0,sF0))) = mult(X0,ld(mult(ld(sF0,sF1),ld(x0,sF0)),x0)),
inference(forward_demodulation,[],[f22321,f5610]) ).
fof(f22365,plain,
! [X0] : rd(X0,mult(sF0,ld(sF1,sF0))) = mult(X0,ld(mult(ld(sF0,x0),ld(sF1,sF0)),sF1)),
inference(forward_demodulation,[],[f22320,f5610]) ).
fof(f30095,plain,
! [X0] : mult(rd(mult(X0,mult(sF0,sF1)),ld(sF0,x0)),mult(sF0,sF1)) = rd(X0,rd(sF0,mult(sF0,sF1))),
inference(superposition,[],[f2122,f8797]) ).
fof(f30106,plain,
! [X0] : rd(X0,rd(sF0,mult(sF0,sF1))) = mult(mult(mult(X0,mult(sF0,sF1)),ld(x0,sF0)),mult(sF0,sF1)),
inference(forward_demodulation,[],[f30095,f300]) ).
fof(f30115,plain,
! [X0] : rd(X0,rd(sF0,mult(sF0,sF1))) = mult(X0,mult(mult(sF0,sF1),mult(ld(x0,sF0),mult(sF0,sF1)))),
inference(forward_demodulation,[],[f30106,f5]) ).
fof(f30120,plain,
! [X0] : rd(X0,rd(sF0,mult(sF0,sF1))) = mult(X0,ld(rd(x0,mult(sF0,sF1)),ld(sF0,sF1))),
inference(forward_demodulation,[],[f30115,f5641]) ).
fof(f35381,plain,
mult(rd(sF1,sF1),sF0) = ld(sF0,rd(x0,x0)),
inference(superposition,[],[f2,f12428]) ).
fof(f35537,plain,
mult(mult(x0,x0),sF0) = rd(mult(mult(x0,mult(x0,x0)),sF0),mult(sF0,sF1)),
inference(superposition,[],[f13045,f6827]) ).
fof(f35543,plain,
! [X0] : rd(mult(X0,sF0),mult(sF0,sF1)) = mult(rd(X0,x0),sF0),
inference(superposition,[],[f13045,f3]) ).
fof(f35625,plain,
mult(mult(x0,x0),sF0) = mult(rd(mult(x0,mult(x0,x0)),x0),sF0),
inference(forward_demodulation,[],[f35537,f35543]) ).
fof(f35662,plain,
mult(mult(mult(x0,x0),rd(x0,x0)),sF0) = mult(mult(x0,x0),sF0),
inference(forward_demodulation,[],[f35625,f28]) ).
fof(f35690,plain,
mult(mult(mult(x0,x0),rd(x0,x0)),sF0) = mult(sF1,mult(sF0,sF1)),
inference(forward_demodulation,[],[f35662,f13034]) ).
fof(f35711,plain,
mult(sF1,mult(sF0,sF1)) = mult(mult(mult(x0,x0),sF0),rd(sF1,sF1)),
inference(forward_demodulation,[],[f35690,f12425]) ).
fof(f35730,plain,
mult(sF1,mult(sF0,sF1)) = mult(mult(sF1,mult(sF0,sF1)),rd(sF1,sF1)),
inference(forward_demodulation,[],[f35711,f13034]) ).
fof(f35898,plain,
! [X2,X0,X1] : mult(rd(X0,mult(X1,mult(X2,X1))),X1) = rd(rd(X0,X1),X2),
inference(superposition,[],[f4,f31]) ).
fof(f36522,plain,
! [X2,X0,X1] : mult(rd(X1,mult(X2,X0)),X2) = rd(rd(X1,X2),rd(X0,X2)),
inference(superposition,[],[f35898,f3]) ).
fof(f36818,plain,
! [X0,X1] : rd(X0,mult(X0,X0)) = mult(rd(ld(X0,X1),mult(X0,X1)),X0),
inference(backward_demodulation,[],[f5933,f36522]) ).
fof(f37490,plain,
! [X0,X1] : rd(rd(X0,mult(X0,X0)),X0) = rd(ld(X0,X1),mult(X0,X1)),
inference(superposition,[],[f4,f36818]) ).
fof(f37635,plain,
! [X0,X1] : rd(rd(X0,X0),mult(X0,X0)) = rd(ld(X0,X1),mult(X0,X1)),
inference(forward_demodulation,[],[f37490,f5061]) ).
fof(f38312,plain,
rd(rd(x0,x0),mult(x0,x0)) = rd(sF0,mult(x0,sF1)),
inference(superposition,[],[f37635,f13]) ).
fof(f38324,plain,
rd(sF0,mult(sF1,x0)) = rd(rd(sF1,sF1),mult(sF1,sF1)),
inference(superposition,[],[f37635,f1113]) ).
fof(f38326,plain,
! [X0,X1] : rd(rd(X1,X1),mult(X1,X1)) = rd(ld(X1,ld(X1,X0)),X0),
inference(superposition,[],[f37635,f1]) ).
fof(f38361,plain,
rd(rd(x0,x0),mult(x0,x0)) = rd(ld(x0,sF0),sF1),
inference(superposition,[],[f37635,f11]) ).
fof(f38374,plain,
rd(ld(sF1,sF0),x0) = rd(rd(sF1,sF1),mult(sF1,sF1)),
inference(superposition,[],[f37635,f1096]) ).
fof(f38530,plain,
rd(ld(sF1,sF0),x0) = rd(sF1,mult(sF1,mult(sF1,sF1))),
inference(forward_demodulation,[],[f38374,f14244]) ).
fof(f38543,plain,
rd(x0,mult(x0,mult(x0,x0))) = rd(ld(x0,sF0),sF1),
inference(forward_demodulation,[],[f38361,f14244]) ).
fof(f38568,plain,
rd(sF0,mult(sF1,x0)) = rd(sF1,mult(sF1,mult(sF1,sF1))),
inference(forward_demodulation,[],[f38324,f14244]) ).
fof(f38580,plain,
rd(x0,mult(x0,mult(x0,x0))) = rd(sF0,mult(x0,sF1)),
inference(forward_demodulation,[],[f38312,f14244]) ).
fof(f38729,plain,
rd(sF0,mult(sF1,x0)) = rd(ld(sF1,sF0),x0),
inference(backward_demodulation,[],[f38530,f38568]) ).
fof(f38741,plain,
rd(sF0,mult(x0,sF1)) = rd(ld(x0,sF0),sF1),
inference(backward_demodulation,[],[f38543,f38580]) ).
fof(f39224,plain,
sF1 = ld(rd(sF0,mult(x0,sF1)),ld(x0,sF0)),
inference(superposition,[],[f15,f38741]) ).
fof(f39420,plain,
! [X0,X1] : mult(rd(rd(X0,X0),mult(X0,X0)),X1) = ld(X0,ld(X0,X1)),
inference(superposition,[],[f3,f38326]) ).
fof(f39472,plain,
! [X0] : rd(rd(X0,X0),mult(X0,X0)) = mult(ld(X0,ld(X0,sF0)),sF0),
inference(superposition,[],[f1076,f38326]) ).
fof(f39475,plain,
! [X0,X1] : ld(mult(X1,mult(X0,X0)),X1) = mult(ld(X0,ld(X0,sF0)),sF0),
inference(backward_demodulation,[],[f10734,f39472]) ).
fof(f39548,plain,
! [X0,X1] : ld(X0,ld(X0,X1)) = mult(mult(ld(X0,ld(X0,sF0)),sF0),X1),
inference(forward_demodulation,[],[f39420,f39472]) ).
fof(f43598,plain,
ld(sF1,sF0) = mult(rd(sF0,mult(sF1,x0)),x0),
inference(superposition,[],[f3,f38729]) ).
fof(f43599,plain,
x0 = ld(rd(sF0,mult(sF1,x0)),ld(sF1,sF0)),
inference(superposition,[],[f15,f38729]) ).
fof(f47878,plain,
! [X2,X0,X1] : ld(mult(X0,rd(X2,X1)),mult(rd(X0,X1),mult(X1,X2))) = X1,
inference(superposition,[],[f2,f60]) ).
fof(f48219,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X2,X2)),mult(mult(X0,rd(X2,X2)),mult(rd(X2,X2),mult(X0,rd(X2,X2))))) = mult(mult(X1,mult(rd(X2,X2),X0)),mult(X0,rd(X2,X2))),
inference(superposition,[],[f20,f2984]) ).
fof(f48258,plain,
! [X0] : mult(mult(X0,mult(rd(x0,x0),sF0)),mult(sF0,mult(mult(rd(x0,x0),sF0),sF0))) = mult(mult(X0,mult(mult(rd(x0,x0),sF0),rd(sF1,sF1))),sF0),
inference(superposition,[],[f20,f2964]) ).
fof(f48517,plain,
! [X0] : mult(mult(X0,mult(rd(x0,x0),sF0)),mult(sF0,rd(x0,x0))) = mult(mult(X0,mult(mult(rd(x0,x0),sF0),rd(sF1,sF1))),sF0),
inference(forward_demodulation,[],[f48258,f1140]) ).
fof(f48552,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X2,X2)),mult(mult(X0,X0),rd(X2,X2))) = mult(mult(X1,mult(rd(X2,X2),X0)),mult(X0,rd(X2,X2))),
inference(forward_demodulation,[],[f48219,f2974]) ).
fof(f48660,plain,
! [X0] : mult(mult(X0,mult(mult(rd(x0,x0),sF0),rd(sF1,sF1))),sF0) = mult(mult(X0,rd(x0,x0)),mult(mult(sF0,sF0),rd(x0,x0))),
inference(backward_demodulation,[],[f48517,f48552]) ).
fof(f48727,plain,
! [X0] : mult(mult(X0,mult(mult(rd(x0,x0),sF0),rd(sF1,sF1))),sF0) = mult(mult(X0,rd(x0,x0)),mult(sF0,rd(x0,x0))),
inference(forward_demodulation,[],[f48660,f5136]) ).
fof(f53337,plain,
mult(x0,mult(sF0,x0)) = ld(sF0,mult(ld(sF0,sF1),x0)),
inference(superposition,[],[f91,f10117]) ).
fof(f56190,plain,
! [X0] : sF0 = ld(mult(X0,rd(mult(rd(x0,x0),sF0),sF0)),mult(rd(X0,sF0),rd(sF1,sF1))),
inference(superposition,[],[f47878,f2964]) ).
fof(f56236,plain,
! [X0] : sF0 = ld(mult(X0,rd(mult(rd(x0,x0),sF0),sF0)),mult(mult(X0,sF0),rd(sF1,sF1))),
inference(forward_demodulation,[],[f56190,f1076]) ).
fof(f56345,plain,
! [X0] : sF0 = ld(mult(X0,rd(x0,x0)),mult(mult(X0,sF0),rd(sF1,sF1))),
inference(forward_demodulation,[],[f56236,f4]) ).
fof(f56851,plain,
! [X0,X1] : mult(mult(X0,mult(mult(X1,sF0),rd(sF1,sF1))),sF0) = mult(rd(X0,sF0),mult(sF0,mult(X1,rd(x0,x0)))),
inference(superposition,[],[f59,f12428]) ).
fof(f57003,plain,
! [X0,X1] : mult(mult(X0,mult(mult(X1,sF0),rd(sF1,sF1))),sF0) = mult(mult(X0,sF0),mult(sF0,mult(X1,rd(x0,x0)))),
inference(forward_demodulation,[],[f56851,f1076]) ).
fof(f57133,plain,
! [X0] : mult(mult(X0,rd(x0,x0)),mult(sF0,rd(x0,x0))) = mult(mult(X0,sF0),mult(sF0,mult(rd(x0,x0),rd(x0,x0)))),
inference(backward_demodulation,[],[f48727,f57003]) ).
fof(f57205,plain,
! [X0] : mult(mult(X0,sF0),mult(sF0,rd(x0,x0))) = mult(mult(X0,rd(x0,x0)),mult(sF0,rd(x0,x0))),
inference(forward_demodulation,[],[f57133,f6815]) ).
fof(f57248,plain,
mult(rd(sF1,sF1),rd(x0,x0)) = mult(mult(sF0,sF0),mult(sF0,rd(x0,x0))),
inference(backward_demodulation,[],[f12961,f57205]) ).
fof(f57277,plain,
mult(rd(sF1,sF1),rd(x0,x0)) = mult(sF0,mult(sF0,rd(x0,x0))),
inference(forward_demodulation,[],[f57248,f5136]) ).
fof(f57299,plain,
mult(rd(sF1,sF1),rd(x0,x0)) = ld(sF0,rd(x0,x0)),
inference(forward_demodulation,[],[f57277,f5610]) ).
fof(f57314,plain,
mult(rd(sF1,sF1),sF0) = mult(rd(sF1,sF1),rd(x0,x0)),
inference(forward_demodulation,[],[f57299,f35381]) ).
fof(f57330,plain,
mult(rd(rd(sF1,sF1),x0),rd(x0,x0)) = rd(mult(rd(sF1,sF1),sF0),x0),
inference(superposition,[],[f4431,f57314]) ).
fof(f57332,plain,
mult(mult(rd(sF1,sF1),x0),x0) = mult(mult(rd(sF1,sF1),sF0),mult(x0,x0)),
inference(superposition,[],[f7152,f57314]) ).
fof(f57335,plain,
x0 = ld(mult(rd(sF1,sF1),sF0),mult(rd(rd(sF1,sF1),x0),mult(x0,x0))),
inference(superposition,[],[f47878,f57314]) ).
fof(f57336,plain,
mult(mult(rd(sF1,sF1),sF0),x0) = mult(rd(rd(sF1,sF1),x0),mult(x0,x0)),
inference(superposition,[],[f60,f57314]) ).
fof(f57337,plain,
rd(x0,x0) = ld(rd(sF1,sF1),mult(rd(sF1,sF1),sF0)),
inference(superposition,[],[f2,f57314]) ).
fof(f57427,plain,
sF0 = rd(x0,x0),
inference(forward_demodulation,[],[f57337,f2]) ).
fof(f57428,plain,
mult(mult(rd(sF1,sF1),sF0),x0) = mult(mult(rd(sF1,sF1),x0),rd(x0,x0)),
inference(forward_demodulation,[],[f57336,f2948]) ).
fof(f57429,plain,
x0 = ld(mult(rd(sF1,sF1),sF0),mult(mult(rd(sF1,sF1),x0),rd(x0,x0))),
inference(forward_demodulation,[],[f57335,f2948]) ).
fof(f57564,plain,
! [X0] : sF0 = ld(mult(X0,sF0),mult(mult(X0,sF0),rd(sF1,sF1))),
inference(backward_demodulation,[],[f56345,f57427]) ).
fof(f57572,plain,
rd(mult(rd(sF1,sF1),sF0),x0) = mult(rd(rd(sF1,sF1),x0),sF0),
inference(backward_demodulation,[],[f57330,f57427]) ).
fof(f57586,plain,
mult(mult(rd(sF1,sF1),sF0),x0) = mult(mult(rd(sF1,sF1),x0),sF0),
inference(forward_demodulation,[],[f57428,f57427]) ).
fof(f57587,plain,
x0 = ld(mult(rd(sF1,sF1),sF0),mult(mult(rd(sF1,sF1),x0),sF0)),
inference(forward_demodulation,[],[f57429,f57427]) ).
fof(f57634,plain,
sF0 = rd(sF1,sF1),
inference(forward_demodulation,[],[f57564,f2]) ).
fof(f57712,plain,
x0 = mult(sF0,mult(ld(rd(sF1,sF1),mult(rd(sF1,sF1),x0)),sF0)),
inference(forward_demodulation,[],[f57587,f1126]) ).
fof(f57761,plain,
mult(sF1,mult(sF0,sF1)) = mult(mult(sF1,mult(sF0,sF1)),sF0),
inference(backward_demodulation,[],[f35730,f57634]) ).
fof(f57770,plain,
mult(mult(sF0,x0),x0) = mult(mult(sF0,sF0),mult(x0,x0)),
inference(backward_demodulation,[],[f57332,f57634]) ).
fof(f57780,plain,
mult(rd(sF0,x0),sF0) = rd(mult(sF0,sF0),x0),
inference(backward_demodulation,[],[f57572,f57634]) ).
fof(f57781,plain,
mult(mult(sF0,x0),sF0) = mult(mult(sF0,sF0),x0),
inference(backward_demodulation,[],[f57586,f57634]) ).
fof(f57869,plain,
x0 = mult(sF0,mult(x0,sF0)),
inference(forward_demodulation,[],[f57712,f2]) ).
fof(f57913,plain,
mult(sF0,x0) = mult(mult(sF0,x0),sF0),
inference(forward_demodulation,[],[f57781,f5136]) ).
fof(f57914,plain,
rd(sF0,x0) = mult(rd(sF0,x0),sF0),
inference(forward_demodulation,[],[f57780,f5136]) ).
fof(f57924,plain,
mult(mult(sF0,x0),x0) = mult(sF0,mult(x0,x0)),
inference(forward_demodulation,[],[f57770,f5136]) ).
fof(f57926,plain,
mult(sF1,mult(sF0,sF1)) = mult(mult(sF1,sF0),mult(sF1,sF0)),
inference(forward_demodulation,[],[f57761,f9080]) ).
fof(f57995,plain,
x0 = mult(sF0,sF1),
inference(forward_demodulation,[],[f57869,f11]) ).
fof(f58033,plain,
mult(sF0,x0) = ld(sF0,sF1),
inference(backward_demodulation,[],[f5580,f57913]) ).
fof(f58045,plain,
mult(x0,x0) = mult(sF1,mult(sF0,sF1)),
inference(forward_demodulation,[],[f57926,f1096]) ).
fof(f58106,plain,
mult(x0,sF0) = ld(sF0,x0),
inference(backward_demodulation,[],[f5583,f57995]) ).
fof(f58107,plain,
mult(ld(sF0,x0),sF1) = mult(sF0,mult(sF1,x0)),
inference(backward_demodulation,[],[f8793,f57995]) ).
fof(f58167,plain,
! [X0] : rd(X0,rd(sF0,x0)) = mult(X0,ld(rd(x0,x0),ld(sF0,sF1))),
inference(backward_demodulation,[],[f30120,f57995]) ).
fof(f58351,plain,
! [X0] : rd(X0,mult(sF0,ld(x0,sF0))) = mult(X0,ld(mult(mult(sF0,x0),ld(x0,sF0)),x0)),
inference(backward_demodulation,[],[f22364,f58033]) ).
fof(f58364,plain,
mult(x0,mult(sF0,x0)) = ld(sF0,mult(mult(sF0,x0),x0)),
inference(backward_demodulation,[],[f53337,f58033]) ).
fof(f58374,plain,
mult(x0,x0) = mult(sF1,x0),
inference(forward_demodulation,[],[f58045,f57995]) ).
fof(f58491,plain,
! [X0] : rd(X0,rd(sF0,x0)) = mult(X0,ld(rd(x0,x0),mult(sF0,x0))),
inference(forward_demodulation,[],[f58167,f58033]) ).
fof(f58519,plain,
ld(sF1,sF0) = mult(ld(mult(sF0,mult(sF1,x0)),sF0),sF1),
inference(backward_demodulation,[],[f19800,f58107]) ).
fof(f58520,plain,
sF1 = ld(sF0,x0),
inference(forward_demodulation,[],[f58106,f11]) ).
fof(f58588,plain,
mult(x0,mult(sF0,x0)) = ld(sF0,mult(sF0,mult(x0,x0))),
inference(forward_demodulation,[],[f58364,f57924]) ).
fof(f58593,plain,
! [X0] : rd(X0,mult(sF0,ld(x0,sF0))) = mult(X0,ld(mult(x0,mult(ld(x0,sF0),sF0)),x0)),
inference(forward_demodulation,[],[f58351,f22186]) ).
fof(f58608,plain,
ld(sF1,sF0) = mult(rd(sF0,mult(x0,x0)),x0),
inference(backward_demodulation,[],[f43598,f58374]) ).
fof(f58609,plain,
x0 = ld(rd(sF0,mult(x0,x0)),ld(sF1,sF0)),
inference(backward_demodulation,[],[f43599,f58374]) ).
fof(f58718,plain,
! [X0] : rd(X0,rd(sF0,x0)) = mult(X0,mult(x0,mult(ld(x0,sF0),x0))),
inference(forward_demodulation,[],[f58491,f71]) ).
fof(f58731,plain,
ld(sF1,sF0) = mult(ld(mult(sF0,mult(x0,x0)),sF0),sF1),
inference(forward_demodulation,[],[f58519,f58374]) ).
fof(f58733,plain,
! [X0] : rd(X0,mult(sF0,ld(sF1,sF0))) = mult(X0,ld(mult(sF1,ld(sF1,sF0)),sF1)),
inference(backward_demodulation,[],[f22365,f58520]) ).
fof(f58784,plain,
mult(x0,x0) = mult(x0,mult(sF0,x0)),
inference(forward_demodulation,[],[f58588,f2]) ).
fof(f58788,plain,
! [X0] : rd(X0,mult(sF0,ld(x0,sF0))) = rd(X0,mult(ld(x0,sF0),sF0)),
inference(forward_demodulation,[],[f58593,f266]) ).
fof(f58802,plain,
ld(sF1,sF0) = mult(rd(sF0,x0),rd(x0,x0)),
inference(forward_demodulation,[],[f58608,f11895]) ).
fof(f58850,plain,
ld(sF1,sF0) = mult(mult(ld(x0,ld(x0,sF0)),sF0),sF1),
inference(forward_demodulation,[],[f58731,f39475]) ).
fof(f58874,plain,
! [X0] : rd(X0,mult(sF0,ld(sF1,sF0))) = rd(X0,ld(sF1,sF0)),
inference(forward_demodulation,[],[f58733,f266]) ).
fof(f58907,plain,
ld(sF1,sF0) = mult(rd(sF0,x0),sF0),
inference(forward_demodulation,[],[f58802,f57427]) ).
fof(f58939,plain,
ld(sF1,sF0) = ld(x0,ld(x0,sF1)),
inference(forward_demodulation,[],[f58850,f39548]) ).
fof(f58945,plain,
! [X0] : mult(X0,ld(sF0,sF1)) = rd(X0,mult(sF0,ld(sF1,sF0))),
inference(forward_demodulation,[],[f58874,f300]) ).
fof(f58974,plain,
rd(sF0,x0) = ld(sF1,sF0),
inference(forward_demodulation,[],[f58907,f57914]) ).
fof(f58997,plain,
ld(sF1,sF0) = ld(x0,sF0),
inference(forward_demodulation,[],[f58939,f13]) ).
fof(f59000,plain,
! [X0] : mult(X0,mult(sF0,x0)) = rd(X0,mult(sF0,ld(sF1,sF0))),
inference(forward_demodulation,[],[f58945,f58033]) ).
fof(f59018,plain,
x0 = ld(rd(sF0,mult(x0,x0)),rd(sF0,x0)),
inference(backward_demodulation,[],[f58609,f58974]) ).
fof(f59070,plain,
rd(sF0,x0) = ld(x0,sF0),
inference(forward_demodulation,[],[f58997,f58974]) ).
fof(f59073,plain,
! [X0] : mult(X0,mult(sF0,x0)) = rd(X0,mult(sF0,rd(sF0,x0))),
inference(forward_demodulation,[],[f59000,f58974]) ).
fof(f59098,plain,
sF1 = ld(rd(sF0,mult(x0,sF1)),rd(sF0,x0)),
inference(backward_demodulation,[],[f39224,f59070]) ).
fof(f59127,plain,
! [X0] : rd(X0,rd(sF0,x0)) = mult(X0,mult(x0,mult(rd(sF0,x0),x0))),
inference(backward_demodulation,[],[f58718,f59070]) ).
fof(f59132,plain,
! [X0] : rd(X0,mult(sF0,rd(sF0,x0))) = rd(X0,mult(rd(sF0,x0),sF0)),
inference(backward_demodulation,[],[f58788,f59070]) ).
fof(f59162,plain,
! [X0] : rd(X0,rd(sF0,x0)) = rd(X0,mult(sF0,rd(sF0,x0))),
inference(forward_demodulation,[],[f59132,f57914]) ).
fof(f59165,plain,
! [X0] : mult(X0,mult(x0,sF0)) = rd(X0,rd(sF0,x0)),
inference(forward_demodulation,[],[f59127,f3]) ).
fof(f59180,plain,
! [X0] : mult(X0,mult(sF0,x0)) = rd(X0,rd(sF0,x0)),
inference(forward_demodulation,[],[f59162,f59073]) ).
fof(f59183,plain,
! [X0] : mult(X0,sF1) = rd(X0,rd(sF0,x0)),
inference(forward_demodulation,[],[f59165,f11]) ).
fof(f59214,plain,
! [X0] : mult(X0,mult(sF0,x0)) = mult(X0,sF1),
inference(backward_demodulation,[],[f59180,f59183]) ).
fof(f59268,plain,
mult(x0,x0) = mult(x0,sF1),
inference(backward_demodulation,[],[f58784,f59214]) ).
fof(f59364,plain,
sF1 = ld(rd(sF0,mult(x0,x0)),rd(sF0,x0)),
inference(backward_demodulation,[],[f59098,f59268]) ).
fof(f59472,plain,
x0 = sF1,
inference(forward_demodulation,[],[f59364,f59018]) ).
fof(f59523,plain,
$false,
inference(forward_subsumption_resolution,[],[f59472,f12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP655-11 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.35 % Computer : n013.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 27 10:31:07 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 Running first-order theorem proving
% 0.13/0.38 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
% 15.85/6.31 % (19164)Detected a unit-equality problem, will run specialized UEQ schedule.
% 15.85/6.31 % (19172)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2755542255:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 15.85/6.31 % (19170)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=3170668428:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 15.85/6.31 % (19172)Instruction limit reached!
% 15.85/6.31 % (19172)------------------------------
% 15.85/6.31 % (19172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19172)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19172)Termination reason: Instruction limit
% 15.85/6.31 % (19172)Termination phase: Saturation
% 15.85/6.31 % (19172)Time elapsed: 0.044 s
% 15.85/6.31 % (19171)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1225270127:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 15.85/6.31 % (19169)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=773114790:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 15.85/6.31 % (19172)Peak memory usage: 88 MB
% 15.85/6.31 % (19172)Instructions burned: 139 (million)
% 15.85/6.31 % (19174)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=565462045:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 15.85/6.31 % (19173)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=4179256119:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 15.85/6.31 % (19175)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3647347958:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 15.85/6.31 % (19180)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=862426992:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 15.85/6.31 % (19173)Instruction limit reached!
% 15.85/6.31 % (19173)------------------------------
% 15.85/6.31 % (19173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19173)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19173)Termination reason: Instruction limit
% 15.85/6.31 % (19173)Termination phase: Saturation
% 15.85/6.31 % (19173)Time elapsed: 0.107 s
% 15.85/6.31 % (19173)Peak memory usage: 89 MB
% 15.85/6.31 % (19173)Instructions burned: 181 (million)
% 15.85/6.31 % (19174)Instruction limit reached!
% 15.85/6.31 % (19174)------------------------------
% 15.85/6.31 % (19174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19174)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19174)Termination reason: Instruction limit
% 15.85/6.31 % (19174)Termination phase: Saturation
% 15.85/6.31 % (19174)Time elapsed: 0.157 s
% 15.85/6.31 % (19174)Peak memory usage: 90 MB
% 15.85/6.31 % (19174)Instructions burned: 257 (million)
% 15.85/6.31 % (19185)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=983671941:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 15.85/6.31 % (19186)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1363396467:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 15.85/6.31 % (19186)Instruction limit reached!
% 15.85/6.31 % (19186)------------------------------
% 15.85/6.31 % (19186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19186)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19186)Termination reason: Instruction limit
% 15.85/6.31 % (19186)Termination phase: Saturation
% 15.85/6.31 % (19186)Time elapsed: 0.114 s
% 15.85/6.31 % (19186)Peak memory usage: 90 MB
% 15.85/6.31 % (19186)Instructions burned: 216 (million)
% 15.85/6.31 % (19190)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=2762330290:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 15.85/6.31 % (19175)Instruction limit reached!
% 15.85/6.31 % (19175)------------------------------
% 15.85/6.31 % (19175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19175)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19175)Termination reason: Instruction limit
% 15.85/6.31 % (19175)Termination phase: Saturation
% 15.85/6.31 % (19175)Time elapsed: 0.656 s
% 15.85/6.31 % (19175)Peak memory usage: 99 MB
% 15.85/6.31 % (19175)Instructions burned: 1188 (million)
% 15.85/6.31 % (19190)Instruction limit reached!
% 15.85/6.31 % (19190)------------------------------
% 15.85/6.31 % (19190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19190)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19190)Termination reason: Instruction limit
% 15.85/6.31 % (19190)Termination phase: Saturation
% 15.85/6.31 % (19190)Time elapsed: 0.195 s
% 15.85/6.31 % (19190)Peak memory usage: 93 MB
% 15.85/6.31 % (19190)Instructions burned: 318 (million)
% 15.85/6.31 % (19192)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=664741150:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 15.85/6.31 % (19180)Instruction limit reached!
% 15.85/6.31 % (19180)------------------------------
% 15.85/6.31 % (19180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19180)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19180)Termination reason: Instruction limit
% 15.85/6.31 % (19180)Termination phase: Saturation
% 15.85/6.31 % (19180)Time elapsed: 0.744 s
% 15.85/6.31 % (19180)Peak memory usage: 142 MB
% 15.85/6.31 % (19180)Instructions burned: 2052 (million)
% 15.85/6.31 % (19193)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=973028302:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 15.85/6.31 % (19195)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1341274155:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2990 on theBenchmark for (2990ds/14534Mi)
% 15.85/6.31 % (19193)Instruction limit reached!
% 15.85/6.31 % (19193)------------------------------
% 15.85/6.31 % (19193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19193)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19193)Termination reason: Instruction limit
% 15.85/6.31 % (19193)Termination phase: Saturation
% 15.85/6.31 % (19193)Time elapsed: 1.943 s
% 15.85/6.31 % (19193)Peak memory usage: 124 MB
% 15.85/6.31 % (19193)Instructions burned: 2836 (million)
% 15.85/6.31 % (19198)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=361890239:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/11832Mi)
% 15.85/6.31 % (19185)Instruction limit reached!
% 15.85/6.31 % (19185)------------------------------
% 15.85/6.31 % (19185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19185)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19185)Termination reason: Instruction limit
% 15.85/6.31 % (19185)Termination phase: Saturation
% 15.85/6.31 % (19185)Time elapsed: 2.988 s
% 15.85/6.31 % (19185)Peak memory usage: 166 MB
% 15.85/6.31 % (19185)Instructions burned: 4949 (million)
% 15.85/6.31 % (19200)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=683668237:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 15.85/6.31 % (19200)Instruction limit reached!
% 15.85/6.31 % (19200)------------------------------
% 15.85/6.31 % (19200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.85/6.31 % (19200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.85/6.31 % (19200)CaDiCaL version: 2.1.3
% 15.85/6.31 % (19200)Termination reason: Instruction limit
% 15.85/6.31 % (19200)Termination phase: Saturation
% 15.85/6.31 % (19200)Time elapsed: 1.371 s
% 15.85/6.31 % (19200)Peak memory usage: 141 MB
% 15.85/6.31 % (19200)Instructions burned: 2280 (million)
% 15.85/6.31 % (19202)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=2463086373:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 15.85/6.31 % (19171)First to succeed.
% 15.85/6.31 % (19171)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-19164"
% 15.85/6.31 % (19171)Refutation found. Thanks to Tanya!
% 15.85/6.31 % SZS status Unsatisfiable for theBenchmark
% 15.85/6.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.13/6.50 % (19171)------------------------------
% 0.13/6.50 % (19171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.13/6.50 % (19171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.13/6.50 % (19171)CaDiCaL version: 2.1.3
% 0.13/6.50 % (19171)Termination reason: Refutation
% 0.13/6.50 % (19171)Time elapsed: 5.065 s
% 0.13/6.50 % (19171)Peak memory usage: 188 MB
% 0.13/6.50 % (19171)Instructions burned: 8040 (million)
% 0.13/6.50 % (19171)------------------------------
% 0.13/6.50 % (19171)------------------------------
% 0.13/6.50 % (19164)Success in time 5.492 s
% 0.13/6.50 % Vampire exiting
%------------------------------------------------------------------------------