%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP655-12 : 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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:15:26 AM UTC 2026
% Result : Unsatisfiable 67.81s 21.61s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 6
% Syntax : Number of formulae : 357 ( 357 unt; 0 def)
% Number of atoms : 357 ( 356 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 879 ( 879 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f4,axiom,
! [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(rd(x1,x1),x0) != x0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f7,plain,
x0 != mult(rd(x1,x1),x0),
inference(reorient_equations,[],[f6]) ).
fof(f8,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f9,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f15,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),X2) = rd(mult(X0,mult(X1,mult(X2,X1))),X1),
inference(superposition,[],[f4,f5]) ).
fof(f22,plain,
! [X2,X0,X1] : mult(mult(X1,X2),rd(X0,X2)) = rd(mult(X1,mult(X2,X0)),X2),
inference(superposition,[],[f20,f3]) ).
fof(f31,plain,
! [X2,X0,X1] : mult(mult(X1,X2),rd(ld(X2,X0),X2)) = rd(mult(X1,X0),X2),
inference(superposition,[],[f22,f1]) ).
fof(f34,plain,
! [X2,X0,X1] : rd(X0,X1) = mult(mult(rd(X0,mult(X1,X2)),X1),rd(X2,X1)),
inference(superposition,[],[f22,f3]) ).
fof(f46,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X0,X2)),X2) = mult(rd(X1,X2),mult(X2,X0)),
inference(superposition,[],[f15,f3]) ).
fof(f54,plain,
! [X2,X0,X1] : mult(X2,mult(X1,X2)) = ld(rd(X0,X2),mult(mult(X0,X1),X2)),
inference(superposition,[],[f2,f15]) ).
fof(f55,plain,
! [X2,X0,X1] : rd(X0,X2) = rd(mult(mult(X0,X1),X2),mult(X2,mult(X1,X2))),
inference(superposition,[],[f4,f15]) ).
fof(f64,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X2,X0),X1)) = ld(rd(X2,X1),mult(X0,X1)),
inference(superposition,[],[f54,f1]) ).
fof(f65,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = ld(rd(rd(X0,X2),X1),mult(X0,X1)),
inference(superposition,[],[f54,f3]) ).
fof(f75,plain,
! [X2,X0,X1] : mult(X1,mult(ld(mult(X0,X1),X2),X1)) = ld(X0,mult(X2,X1)),
inference(superposition,[],[f64,f4]) ).
fof(f77,plain,
! [X2,X3,X0,X1] : mult(X1,mult(ld(mult(X0,mult(X1,X2)),X3),X1)) = ld(mult(mult(X0,X1),rd(X2,X1)),mult(X3,X1)),
inference(superposition,[],[f64,f22]) ).
fof(f80,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X2,rd(X0,X1)),X1)) = ld(rd(X2,X1),X0),
inference(superposition,[],[f64,f3]) ).
fof(f98,plain,
! [X2,X0,X1] : mult(X1,mult(X2,X1)) = ld(rd(rd(rd(X0,X1),X2),X1),X0),
inference(superposition,[],[f65,f3]) ).
fof(f103,plain,
! [X2,X0,X1] : rd(rd(X2,X1),X0) = rd(mult(X2,X0),mult(X0,mult(X1,X0))),
inference(superposition,[],[f8,f65]) ).
fof(f116,plain,
! [X2,X0,X1] : mult(ld(X0,rd(X2,X1)),X1) = ld(X1,ld(rd(X0,X1),X2)),
inference(superposition,[],[f2,f80]) ).
fof(f137,plain,
! [X2,X0,X1] : rd(X2,mult(X0,mult(X1,X0))) = rd(rd(rd(X2,X0),X1),X0),
inference(superposition,[],[f8,f98]) ).
fof(f145,plain,
! [X2,X0,X1] : mult(ld(mult(X0,X1),rd(X2,X1)),X1) = ld(X1,ld(X0,X2)),
inference(superposition,[],[f116,f4]) ).
fof(f149,plain,
! [X0,X1] : mult(ld(X1,rd(X1,X0)),X0) = ld(X0,X0),
inference(superposition,[],[f116,f9]) ).
fof(f170,plain,
! [X2,X0,X1] : mult(ld(mult(X1,X2),X0),X2) = ld(X2,ld(X1,mult(X0,X2))),
inference(superposition,[],[f145,f4]) ).
fof(f176,plain,
! [X2,X0,X1] : ld(mult(X1,X0),rd(X2,X0)) = rd(ld(X0,ld(X1,X2)),X0),
inference(superposition,[],[f4,f145]) ).
fof(f196,plain,
! [X0,X1] : ld(X1,X1) = mult(ld(mult(X0,X1),X0),X1),
inference(superposition,[],[f149,f4]) ).
fof(f204,plain,
! [X0,X1] : ld(X1,rd(X1,X0)) = rd(ld(X0,X0),X0),
inference(superposition,[],[f4,f149]) ).
fof(f207,plain,
! [X2,X0,X1] : mult(mult(X1,X0),ld(X2,rd(X2,X0))) = rd(mult(X1,mult(X0,ld(X0,X0))),X0),
inference(superposition,[],[f20,f149]) ).
fof(f216,plain,
! [X2,X0,X1] : mult(mult(X1,X0),ld(X2,rd(X2,X0))) = mult(mult(X1,X0),rd(ld(X0,X0),X0)),
inference(forward_demodulation,[],[f207,f22]) ).
fof(f221,plain,
! [X2,X0,X1] : rd(mult(X1,X0),X0) = mult(mult(X1,X0),ld(X2,rd(X2,X0))),
inference(forward_demodulation,[],[f216,f31]) ).
fof(f223,plain,
! [X2,X0,X1] : mult(mult(X1,X0),ld(X2,rd(X2,X0))) = X1,
inference(forward_demodulation,[],[f221,f4]) ).
fof(f230,plain,
! [X2,X0,X1] : rd(X0,X1) = mult(X0,ld(X2,rd(X2,X1))),
inference(superposition,[],[f223,f3]) ).
fof(f232,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(mult(X0,X2),X0)) = X1,
inference(superposition,[],[f223,f4]) ).
fof(f235,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X0,X2)),ld(X2,X0)) = X1,
inference(superposition,[],[f223,f8]) ).
fof(f243,plain,
! [X2,X0,X1] : mult(X0,X1) = rd(X0,ld(X2,rd(X2,X1))),
inference(superposition,[],[f4,f223]) ).
fof(f264,plain,
! [X2,X0,X1] : rd(X1,X2) = mult(X1,ld(mult(X0,X2),X0)),
inference(superposition,[],[f230,f4]) ).
fof(f267,plain,
! [X2,X0,X1] : mult(X1,ld(X2,X0)) = rd(X1,ld(X0,X2)),
inference(superposition,[],[f230,f8]) ).
fof(f280,plain,
! [X2,X3,X0,X1] : mult(ld(X2,rd(X2,X1)),mult(ld(X3,X0),ld(X2,rd(X2,X1)))) = ld(rd(X3,ld(X2,rd(X2,X1))),rd(X0,X1)),
inference(superposition,[],[f64,f230]) ).
fof(f288,plain,
! [X2,X3,X0,X1] : mult(ld(X3,rd(X3,X2)),mult(X1,ld(X3,rd(X3,X2)))) = ld(rd(X0,ld(X3,rd(X3,X2))),rd(mult(X0,X1),X2)),
inference(superposition,[],[f54,f230]) ).
fof(f289,plain,
! [X2,X3,X0,X1] : mult(X0,mult(X1,mult(ld(X3,rd(X3,X2)),X1))) = mult(rd(mult(X0,X1),X2),X1),
inference(superposition,[],[f5,f230]) ).
fof(f294,plain,
! [X2,X3,X0,X1] : mult(ld(X3,rd(X3,X2)),mult(X1,ld(X3,rd(X3,X2)))) = ld(mult(X0,X2),rd(mult(X0,X1),X2)),
inference(forward_demodulation,[],[f288,f243]) ).
fof(f301,plain,
! [X2,X3,X0,X1] : mult(ld(X2,rd(X2,X1)),mult(ld(X3,X0),ld(X2,rd(X2,X1)))) = ld(mult(X3,X1),rd(X0,X1)),
inference(forward_demodulation,[],[f280,f243]) ).
fof(f312,plain,
! [X2,X3,X0,X1] : mult(ld(X3,rd(X3,X2)),mult(X1,ld(X3,rd(X3,X2)))) = rd(ld(X2,ld(X0,mult(X0,X1))),X2),
inference(forward_demodulation,[],[f294,f176]) ).
fof(f319,plain,
! [X2,X3,X0,X1] : mult(ld(X2,rd(X2,X1)),mult(ld(X3,X0),ld(X2,rd(X2,X1)))) = rd(ld(X1,ld(X3,X0)),X1),
inference(forward_demodulation,[],[f301,f176]) ).
fof(f326,plain,
! [X2,X3,X1] : mult(ld(X3,rd(X3,X2)),mult(X1,ld(X3,rd(X3,X2)))) = rd(ld(X2,X1),X2),
inference(forward_demodulation,[],[f312,f2]) ).
fof(f330,plain,
! [X2,X3,X0,X1] : rd(ld(X1,ld(X3,X0)),X1) = mult(ld(X2,rd(X2,X1)),rd(ld(X3,X0),X1)),
inference(forward_demodulation,[],[f319,f230]) ).
fof(f333,plain,
! [X2,X3,X1] : rd(ld(X2,X1),X2) = mult(ld(X3,rd(X3,X2)),rd(X1,X2)),
inference(forward_demodulation,[],[f326,f230]) ).
fof(f367,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X3,X2),X3),mult(X1,ld(mult(X3,X2),X3))) = ld(rd(X0,ld(mult(X3,X2),X3)),rd(mult(X0,X1),X2)),
inference(superposition,[],[f54,f264]) ).
fof(f368,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,f264]) ).
fof(f373,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X3,X2),X3),mult(X1,ld(mult(X3,X2),X3))) = ld(mult(X0,ld(X3,mult(X3,X2))),rd(mult(X0,X1),X2)),
inference(forward_demodulation,[],[f367,f267]) ).
fof(f397,plain,
! [X2,X3,X0,X1] : ld(mult(X0,X2),rd(mult(X0,X1),X2)) = mult(ld(mult(X3,X2),X3),mult(X1,ld(mult(X3,X2),X3))),
inference(forward_demodulation,[],[f373,f2]) ).
fof(f414,plain,
! [X2,X3,X0,X1] : ld(mult(X0,X2),rd(mult(X0,X1),X2)) = mult(ld(mult(X3,X2),X3),rd(X1,X2)),
inference(forward_demodulation,[],[f397,f264]) ).
fof(f426,plain,
! [X2,X3,X0,X1] : rd(ld(X2,ld(X0,mult(X0,X1))),X2) = mult(ld(mult(X3,X2),X3),rd(X1,X2)),
inference(forward_demodulation,[],[f414,f176]) ).
fof(f434,plain,
! [X2,X3,X1] : rd(ld(X2,X1),X2) = mult(ld(mult(X3,X2),X3),rd(X1,X2)),
inference(forward_demodulation,[],[f426,f2]) ).
fof(f451,plain,
! [X2,X0,X1] : ld(X2,X1) = ld(mult(X0,ld(X1,X2)),X0),
inference(superposition,[],[f9,f267]) ).
fof(f465,plain,
! [X2,X3,X0,X1] : mult(mult(X0,ld(X1,X2)),rd(X3,ld(X1,X2))) = mult(mult(X0,mult(ld(X1,X2),X3)),ld(X2,X1)),
inference(superposition,[],[f22,f267]) ).
fof(f470,plain,
! [X2,X3,X0,X1] : mult(mult(X0,mult(ld(X1,X2),X3)),ld(X2,X1)) = mult(mult(X0,ld(X1,X2)),mult(X3,ld(X2,X1))),
inference(forward_demodulation,[],[f465,f267]) ).
fof(f512,plain,
! [X2,X0,X1] : ld(mult(X0,X1),X0) = ld(mult(X2,X1),X2),
inference(superposition,[],[f2,f232]) ).
fof(f520,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X1,X2),X1),mult(X3,ld(mult(X1,X2),X1))) = ld(rd(rd(mult(X0,X2),X3),ld(mult(X1,X2),X1)),X0),
inference(superposition,[],[f65,f232]) ).
fof(f527,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X1,X2),X1),mult(X3,ld(mult(X1,X2),X1))) = ld(mult(rd(mult(X0,X2),X3),ld(X1,mult(X1,X2))),X0),
inference(forward_demodulation,[],[f520,f267]) ).
fof(f559,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X1,X2),X1),mult(X3,ld(mult(X1,X2),X1))) = ld(mult(rd(mult(X0,X2),X3),X2),X0),
inference(forward_demodulation,[],[f527,f2]) ).
fof(f574,plain,
! [X2,X3,X0,X1] : mult(ld(mult(X1,X2),X1),rd(X3,X2)) = ld(mult(rd(mult(X0,X2),X3),X2),X0),
inference(forward_demodulation,[],[f559,f264]) ).
fof(f581,plain,
! [X2,X3,X0] : ld(mult(rd(mult(X0,X2),X3),X2),X0) = rd(ld(X2,X3),X2),
inference(forward_demodulation,[],[f574,f434]) ).
fof(f889,plain,
! [X2,X0,X1] : mult(mult(X1,ld(mult(X2,X0),X2)),rd(X0,ld(mult(X2,X0),X2))) = rd(mult(X1,ld(X0,X0)),ld(mult(X2,X0),X2)),
inference(superposition,[],[f22,f196]) ).
fof(f907,plain,
! [X2,X0,X1] : mult(mult(X1,ld(mult(X2,X0),X2)),rd(X0,ld(mult(X2,X0),X2))) = mult(mult(X1,ld(X0,X0)),ld(X2,mult(X2,X0))),
inference(forward_demodulation,[],[f889,f267]) ).
fof(f923,plain,
! [X2,X0,X1] : mult(mult(X1,ld(mult(X2,X0),X2)),rd(X0,ld(mult(X2,X0),X2))) = mult(mult(X1,ld(X0,X0)),X0),
inference(forward_demodulation,[],[f907,f2]) ).
fof(f932,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X0,X0)),X0) = mult(mult(X1,ld(mult(X2,X0),X2)),mult(X0,ld(X2,mult(X2,X0)))),
inference(forward_demodulation,[],[f923,f267]) ).
fof(f940,plain,
! [X2,X0,X1] : mult(mult(X1,ld(X0,X0)),X0) = mult(mult(X1,ld(mult(X2,X0),X2)),mult(X0,X0)),
inference(forward_demodulation,[],[f932,f2]) ).
fof(f947,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X0)),X0) = mult(rd(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f940,f264]) ).
fof(f948,plain,
! [X0] : mult(X0,X0) = mult(rd(X0,X0),mult(X0,X0)),
inference(superposition,[],[f947,f1]) ).
fof(f958,plain,
! [X0,X1] : mult(X1,mult(ld(X1,X1),X1)) = ld(rd(X0,X1),mult(rd(X0,X1),mult(X1,X1))),
inference(superposition,[],[f54,f947]) ).
fof(f964,plain,
! [X0,X1] : mult(X0,ld(X1,X1)) = rd(mult(rd(X0,X1),mult(X1,X1)),X1),
inference(superposition,[],[f4,f947]) ).
fof(f989,plain,
! [X0,X1] : mult(X0,ld(X1,X1)) = mult(mult(rd(X0,X1),X1),rd(X1,X1)),
inference(forward_demodulation,[],[f964,f22]) ).
fof(f994,plain,
! [X1] : mult(X1,X1) = mult(X1,mult(ld(X1,X1),X1)),
inference(forward_demodulation,[],[f958,f2]) ).
fof(f1006,plain,
! [X0,X1] : mult(X0,ld(X1,X1)) = mult(X0,rd(X1,X1)),
inference(forward_demodulation,[],[f989,f3]) ).
fof(f1050,plain,
! [X0] : mult(X0,rd(X0,X0)) = X0,
inference(superposition,[],[f1,f1006]) ).
fof(f1052,plain,
! [X0,X1] : ld(X1,X1) = ld(X0,mult(X0,rd(X1,X1))),
inference(superposition,[],[f2,f1006]) ).
fof(f1057,plain,
! [X2,X0,X1] : mult(mult(X2,X0),rd(ld(X1,X1),X0)) = rd(mult(X2,mult(X0,rd(X1,X1))),X0),
inference(superposition,[],[f22,f1006]) ).
fof(f1058,plain,
! [X2,X0,X1] : mult(X2,mult(ld(X1,X1),X2)) = ld(rd(X0,X2),mult(mult(X0,rd(X1,X1)),X2)),
inference(superposition,[],[f54,f1006]) ).
fof(f1067,plain,
! [X2,X0,X1] : rd(X2,ld(X1,X1)) = mult(X2,ld(mult(X0,rd(X1,X1)),X0)),
inference(superposition,[],[f264,f1006]) ).
fof(f1069,plain,
! [X2,X0,X1] : ld(mult(X0,rd(X1,X1)),X0) = ld(mult(X2,ld(X1,X1)),X2),
inference(superposition,[],[f512,f1006]) ).
fof(f1078,plain,
! [X0,X1] : mult(rd(X0,ld(X1,X1)),rd(X1,X1)) = X0,
inference(superposition,[],[f3,f1006]) ).
fof(f1079,plain,
! [X0,X1] : mult(mult(X0,ld(X1,X1)),rd(X1,X1)) = X0,
inference(forward_demodulation,[],[f1078,f267]) ).
fof(f1088,plain,
! [X0,X1] : ld(X1,X1) = ld(mult(X0,rd(X1,X1)),X0),
inference(forward_demodulation,[],[f1069,f451]) ).
fof(f1090,plain,
! [X2,X1] : rd(X2,ld(X1,X1)) = rd(X2,rd(X1,X1)),
inference(forward_demodulation,[],[f1067,f264]) ).
fof(f1099,plain,
! [X2,X1] : mult(X2,mult(ld(X1,X1),X2)) = mult(X2,mult(rd(X1,X1),X2)),
inference(forward_demodulation,[],[f1058,f54]) ).
fof(f1100,plain,
! [X2,X0,X1] : mult(mult(X2,X0),rd(ld(X1,X1),X0)) = mult(mult(X2,X0),rd(rd(X1,X1),X0)),
inference(forward_demodulation,[],[f1057,f22]) ).
fof(f1105,plain,
! [X1] : ld(X1,X1) = rd(X1,X1),
inference(forward_demodulation,[],[f1052,f2]) ).
fof(f1112,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X1)),rd(X1,X1)) = X0,
inference(forward_demodulation,[],[f1079,f1006]) ).
fof(f1120,plain,
! [X2,X1] : mult(X2,ld(X1,X1)) = rd(X2,rd(X1,X1)),
inference(forward_demodulation,[],[f1090,f267]) ).
fof(f1145,plain,
! [X2,X1] : rd(X2,rd(X1,X1)) = mult(X2,rd(X1,X1)),
inference(forward_demodulation,[],[f1120,f1006]) ).
fof(f1209,plain,
! [X2,X0,X1] : mult(rd(X1,X1),mult(X2,rd(X1,X1))) = ld(mult(rd(rd(X0,rd(X1,X1)),X2),rd(X1,X1)),X0),
inference(superposition,[],[f98,f1145]) ).
fof(f1210,plain,
! [X2,X0,X1] : mult(rd(X1,X1),mult(X2,rd(X1,X1))) = ld(mult(rd(mult(X0,rd(X1,X1)),X2),rd(X1,X1)),X0),
inference(forward_demodulation,[],[f1209,f1145]) ).
fof(f1224,plain,
! [X2,X1] : mult(rd(X1,X1),mult(X2,rd(X1,X1))) = rd(ld(rd(X1,X1),X2),rd(X1,X1)),
inference(forward_demodulation,[],[f1210,f581]) ).
fof(f1232,plain,
! [X2,X1] : mult(rd(X1,X1),mult(X2,rd(X1,X1))) = mult(ld(rd(X1,X1),X2),rd(X1,X1)),
inference(forward_demodulation,[],[f1224,f1145]) ).
fof(f1234,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,X1),mult(ld(X0,X1),ld(X1,X0))),
inference(superposition,[],[f1050,f267]) ).
fof(f1236,plain,
! [X0] : rd(X0,X0) = mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))),
inference(superposition,[],[f1050,f1145]) ).
fof(f1240,plain,
! [X0,X1] : mult(mult(X1,X0),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),X0)),
inference(superposition,[],[f15,f1050]) ).
fof(f1242,plain,
! [X0,X1] : rd(mult(X1,X0),X0) = mult(mult(X1,X0),rd(rd(X0,X0),X0)),
inference(superposition,[],[f22,f1050]) ).
fof(f1268,plain,
! [X0,X1] : mult(mult(X1,X0),rd(rd(X0,X0),X0)) = X1,
inference(forward_demodulation,[],[f1242,f4]) ).
fof(f1270,plain,
! [X0,X1] : mult(mult(X1,X0),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f1240,f3]) ).
fof(f1278,plain,
! [X0,X1] : mult(mult(X1,rd(X0,X0)),X0) = mult(mult(X1,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f1270,f1145]) ).
fof(f1281,plain,
! [X0,X1] : mult(rd(X1,X0),mult(X0,X0)) = mult(mult(X1,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f1278,f46]) ).
fof(f1285,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = mult(ld(X0,rd(X0,X1)),rd(ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))),X1)),
inference(superposition,[],[f994,f230]) ).
fof(f1335,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(ld(X1,ld(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1)))),X1),
inference(forward_demodulation,[],[f1285,f330]) ).
fof(f1359,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(ld(X1,rd(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1)))),X1),
inference(forward_demodulation,[],[f1335,f1105]) ).
fof(f1367,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(ld(X1,mult(ld(X0,rd(X0,X1)),X1)),X1),
inference(forward_demodulation,[],[f1359,f243]) ).
fof(f1371,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(ld(X1,ld(X1,X1)),X1),
inference(forward_demodulation,[],[f1367,f149]) ).
fof(f1373,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(ld(X1,rd(X1,X1)),X1),
inference(forward_demodulation,[],[f1371,f1105]) ).
fof(f1375,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(rd(ld(X1,X1),X1),X1),
inference(forward_demodulation,[],[f1373,f204]) ).
fof(f1377,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(rd(rd(X1,X1),X1),X1),
inference(forward_demodulation,[],[f1375,f1105]) ).
fof(f1379,plain,
! [X0,X1] : mult(ld(X0,rd(X0,X1)),ld(X0,rd(X0,X1))) = rd(X1,mult(X1,mult(X1,X1))),
inference(forward_demodulation,[],[f1377,f137]) ).
fof(f1381,plain,
! [X0,X1] : rd(X1,mult(X1,mult(X1,X1))) = rd(ld(X0,rd(X0,X1)),X1),
inference(forward_demodulation,[],[f1379,f230]) ).
fof(f1391,plain,
! [X0] : rd(X0,X0) = rd(mult(X0,X0),mult(X0,X0)),
inference(superposition,[],[f4,f948]) ).
fof(f1400,plain,
! [X0] : ld(mult(X0,X0),mult(X0,X0)) = mult(ld(mult(X0,X0),rd(X0,X0)),mult(X0,X0)),
inference(superposition,[],[f196,f948]) ).
fof(f1405,plain,
! [X0,X1] : rd(X1,mult(X0,X0)) = mult(X1,ld(mult(X0,X0),rd(X0,X0))),
inference(superposition,[],[f264,f948]) ).
fof(f1410,plain,
! [X0,X1] : rd(X1,mult(X0,X0)) = mult(X1,rd(ld(X0,ld(X0,X0)),X0)),
inference(forward_demodulation,[],[f1405,f176]) ).
fof(f1415,plain,
! [X0] : ld(mult(X0,X0),mult(X0,X0)) = mult(rd(ld(X0,ld(X0,X0)),X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1400,f176]) ).
fof(f1428,plain,
! [X0,X1] : rd(X1,mult(X0,X0)) = mult(X1,rd(ld(X0,rd(X0,X0)),X0)),
inference(forward_demodulation,[],[f1410,f1105]) ).
fof(f1431,plain,
! [X0] : ld(mult(X0,X0),mult(X0,X0)) = mult(mult(ld(X0,ld(X0,X0)),X0),rd(X0,X0)),
inference(forward_demodulation,[],[f1415,f1281]) ).
fof(f1441,plain,
! [X0,X1] : rd(X1,mult(X0,X0)) = mult(X1,rd(X0,mult(X0,mult(X0,X0)))),
inference(forward_demodulation,[],[f1428,f1381]) ).
fof(f1444,plain,
! [X0] : ld(mult(X0,X0),mult(X0,X0)) = mult(mult(ld(X0,rd(X0,X0)),X0),rd(X0,X0)),
inference(forward_demodulation,[],[f1431,f1105]) ).
fof(f1449,plain,
! [X0] : mult(ld(X0,X0),rd(X0,X0)) = ld(mult(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1444,f149]) ).
fof(f1453,plain,
! [X0] : mult(ld(X0,X0),rd(X0,X0)) = rd(mult(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1449,f1105]) ).
fof(f1457,plain,
! [X0] : rd(X0,X0) = mult(ld(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f1453,f1391]) ).
fof(f1459,plain,
! [X0] : rd(X0,X0) = mult(rd(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f1457,f1105]) ).
fof(f1471,plain,
! [X0,X1] : mult(rd(X0,X0),mult(ld(X1,rd(X0,X0)),rd(X0,X0))) = ld(rd(X1,rd(X0,X0)),rd(X0,X0)),
inference(superposition,[],[f64,f1459]) ).
fof(f1473,plain,
! [X0,X1] : ld(rd(X0,X0),ld(rd(X0,X0),X1)) = mult(ld(rd(X0,X0),rd(X1,rd(X0,X0))),rd(X0,X0)),
inference(superposition,[],[f145,f1459]) ).
fof(f1490,plain,
! [X0,X1] : ld(rd(X0,X0),ld(rd(X0,X0),X1)) = mult(rd(X0,X0),mult(rd(X1,rd(X0,X0)),rd(X0,X0))),
inference(forward_demodulation,[],[f1473,f1232]) ).
fof(f1492,plain,
! [X0,X1] : mult(rd(X0,X0),mult(ld(X1,rd(X0,X0)),rd(X0,X0))) = ld(mult(X1,rd(X0,X0)),rd(X0,X0)),
inference(forward_demodulation,[],[f1471,f1145]) ).
fof(f1508,plain,
! [X0,X1] : mult(rd(X0,X0),X1) = ld(rd(X0,X0),ld(rd(X0,X0),X1)),
inference(forward_demodulation,[],[f1490,f3]) ).
fof(f1607,plain,
! [X0] : mult(X0,X0) = mult(mult(X0,X0),rd(X0,X0)),
inference(superposition,[],[f1050,f1391]) ).
fof(f1678,plain,
! [X0,X1] : rd(X0,X1) = mult(X0,rd(rd(X1,X1),X1)),
inference(superposition,[],[f1268,f3]) ).
fof(f1691,plain,
! [X0,X1] : mult(rd(rd(X1,X1),X1),mult(X1,rd(rd(X1,X1),X1))) = ld(rd(X0,rd(rd(X1,X1),X1)),X0),
inference(superposition,[],[f54,f1268]) ).
fof(f1694,plain,
! [X0,X1] : mult(X0,X1) = rd(X0,rd(rd(X1,X1),X1)),
inference(superposition,[],[f4,f1268]) ).
fof(f1722,plain,
! [X1] : rd(rd(X1,X1),X1) = mult(rd(rd(X1,X1),X1),mult(X1,rd(rd(X1,X1),X1))),
inference(forward_demodulation,[],[f1691,f9]) ).
fof(f1752,plain,
! [X1] : rd(rd(X1,X1),X1) = mult(rd(rd(X1,X1),X1),rd(X1,X1)),
inference(forward_demodulation,[],[f1722,f1678]) ).
fof(f1793,plain,
! [X0] : rd(rd(rd(X0,X0),X0),X0) = mult(rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),X0)),
inference(superposition,[],[f948,f1678]) ).
fof(f1794,plain,
! [X0,X1] : ld(X0,rd(X0,X1)) = rd(rd(X1,X1),X1),
inference(superposition,[],[f2,f1678]) ).
fof(f1799,plain,
! [X2,X0,X1] : rd(mult(X2,rd(X0,X1)),X0) = mult(mult(X2,X0),rd(rd(rd(X1,X1),X1),X0)),
inference(superposition,[],[f22,f1678]) ).
fof(f1821,plain,
! [X2,X0,X1] : mult(rd(rd(X2,X2),X2),mult(X1,rd(rd(X2,X2),X2))) = ld(rd(X0,rd(rd(X2,X2),X2)),rd(mult(X0,X1),X2)),
inference(superposition,[],[f54,f1678]) ).
fof(f1825,plain,
! [X2,X0,X1] : ld(mult(X0,X2),rd(mult(X0,X1),X2)) = mult(rd(rd(X2,X2),X2),mult(X1,rd(rd(X2,X2),X2))),
inference(forward_demodulation,[],[f1821,f1694]) ).
fof(f1850,plain,
! [X0] : rd(X0,mult(X0,mult(X0,X0))) = mult(rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0)),rd(X0,mult(X0,mult(X0,X0)))),
inference(forward_demodulation,[],[f1793,f137]) ).
fof(f1864,plain,
! [X2,X0,X1] : ld(mult(X0,X2),rd(mult(X0,X1),X2)) = mult(rd(rd(X2,X2),X2),rd(X1,X2)),
inference(forward_demodulation,[],[f1825,f1678]) ).
fof(f1886,plain,
! [X0] : rd(X0,mult(X0,mult(X0,X0))) = rd(rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f1850,f1441]) ).
fof(f1897,plain,
! [X2,X0,X1] : rd(ld(X2,ld(X0,mult(X0,X1))),X2) = mult(rd(rd(X2,X2),X2),rd(X1,X2)),
inference(forward_demodulation,[],[f1864,f176]) ).
fof(f1908,plain,
! [X0] : rd(X0,mult(X0,mult(X0,X0))) = rd(mult(rd(rd(X0,X0),X0),X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1886,f1694]) ).
fof(f1915,plain,
! [X2,X1] : rd(ld(X2,X1),X2) = mult(rd(rd(X2,X2),X2),rd(X1,X2)),
inference(forward_demodulation,[],[f1897,f2]) ).
fof(f1921,plain,
! [X0] : rd(X0,mult(X0,mult(X0,X0))) = rd(rd(X0,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f1908,f3]) ).
fof(f1964,plain,
! [X0,X1] : ld(X0,ld(X1,mult(X1,X0))) = mult(rd(rd(X0,X0),X0),X0),
inference(superposition,[],[f145,f1794]) ).
fof(f1996,plain,
! [X0,X1] : ld(X0,ld(X1,mult(X1,X0))) = rd(X0,X0),
inference(forward_demodulation,[],[f1964,f3]) ).
fof(f2015,plain,
! [X0,X1] : mult(ld(mult(X1,X0),X1),X0) = rd(X0,X0),
inference(forward_demodulation,[],[f1996,f170]) ).
fof(f2044,plain,
! [X0,X1] : mult(ld(X0,X1),ld(X1,X0)) = rd(ld(X1,X0),ld(X1,X0)),
inference(superposition,[],[f2015,f1]) ).
fof(f2146,plain,
! [X0,X1] : mult(ld(X1,X0),ld(X0,X1)) = mult(ld(X0,X1),ld(X1,X0)),
inference(forward_demodulation,[],[f2044,f267]) ).
fof(f3200,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),mult(rd(X0,X0),rd(rd(X0,X0),X0))),
inference(superposition,[],[f15,f1752]) ).
fof(f3237,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(X0,X0)) = mult(rd(X1,rd(X0,X0)),rd(rd(X0,X0),X0)),
inference(forward_demodulation,[],[f3200,f1678]) ).
fof(f3267,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(X0,X0)) = rd(rd(X1,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f3237,f1678]) ).
fof(f3290,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(X0,X0)) = rd(mult(X1,rd(X0,X0)),X0),
inference(forward_demodulation,[],[f3267,f1145]) ).
fof(f3306,plain,
! [X0,X1] : rd(mult(X1,rd(X0,X0)),X0) = mult(rd(X1,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f3290,f1678]) ).
fof(f3343,plain,
! [X0,X1] : ld(rd(X0,X0),X1) = mult(rd(X0,X0),mult(rd(X0,X0),X1)),
inference(superposition,[],[f1,f1508]) ).
fof(f3362,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = mult(mult(mult(X0,X1),X1),rd(X1,X1)),
inference(superposition,[],[f1281,f4]) ).
fof(f3371,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,[],[f1281,f1678]) ).
fof(f3410,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(X0,mult(X0,mult(X0,X0)))),
inference(forward_demodulation,[],[f3371,f137]) ).
fof(f3428,plain,
! [X0,X1] : mult(mult(X1,rd(rd(X0,X0),X0)),rd(rd(rd(X0,X0),X0),rd(rd(X0,X0),X0))) = rd(rd(X1,rd(rd(X0,X0),X0)),mult(X0,X0)),
inference(forward_demodulation,[],[f3410,f1441]) ).
fof(f3438,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,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f3428,f1694]) ).
fof(f3444,plain,
! [X0,X1] : rd(mult(X1,X0),mult(X0,X0)) = rd(mult(X1,rd(rd(rd(X0,X0),X0),X0)),rd(rd(X0,X0),X0)),
inference(forward_demodulation,[],[f3438,f1799]) ).
fof(f3449,plain,
! [X0,X1] : rd(mult(X1,X0),mult(X0,X0)) = mult(mult(X1,rd(rd(rd(X0,X0),X0),X0)),X0),
inference(forward_demodulation,[],[f3444,f1694]) ).
fof(f3454,plain,
! [X0,X1] : rd(mult(X1,X0),mult(X0,X0)) = mult(rd(X1,X0),mult(X0,rd(rd(X0,X0),X0))),
inference(forward_demodulation,[],[f3449,f46]) ).
fof(f3459,plain,
! [X0,X1] : mult(rd(X1,X0),rd(X0,X0)) = rd(mult(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f3454,f1678]) ).
fof(f3483,plain,
! [X0,X1] : rd(X0,mult(X1,X1)) = mult(rd(rd(X0,X1),X1),rd(X1,X1)),
inference(superposition,[],[f3459,f3]) ).
fof(f3693,plain,
! [X0,X1] : rd(mult(X0,X1),mult(mult(X1,X1),mult(X1,X1))) = mult(rd(mult(rd(X0,X1),rd(X1,X1)),mult(X1,X1)),rd(mult(X1,X1),mult(X1,X1))),
inference(superposition,[],[f3483,f3459]) ).
fof(f3709,plain,
! [X0] : rd(rd(X0,X0),X0) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f1752,f3483]) ).
fof(f3711,plain,
! [X0,X1] : rd(rd(X0,X1),X1) = mult(rd(X0,mult(X1,X1)),rd(X1,X1)),
inference(superposition,[],[f1112,f3483]) ).
fof(f3769,plain,
! [X0,X1] : rd(mult(X0,X1),mult(mult(X1,X1),mult(X1,X1))) = mult(rd(mult(rd(X0,X1),rd(X1,X1)),mult(X1,X1)),mult(rd(X1,X1),rd(X1,X1))),
inference(forward_demodulation,[],[f3693,f3459]) ).
fof(f3800,plain,
! [X0,X1] : rd(mult(X0,X1),mult(mult(X1,X1),mult(X1,X1))) = mult(rd(mult(rd(X0,X1),rd(X1,X1)),mult(X1,X1)),rd(X1,X1)),
inference(forward_demodulation,[],[f3769,f1459]) ).
fof(f3816,plain,
! [X0,X1] : rd(mult(X0,X1),mult(mult(X1,X1),mult(X1,X1))) = rd(rd(mult(rd(X0,X1),rd(X1,X1)),X1),X1),
inference(forward_demodulation,[],[f3800,f3711]) ).
fof(f3825,plain,
! [X0,X1] : rd(mult(X0,X1),mult(mult(X1,X1),mult(X1,X1))) = rd(mult(rd(rd(X0,X1),X1),rd(X1,X1)),X1),
inference(forward_demodulation,[],[f3816,f3306]) ).
fof(f3833,plain,
! [X0,X1] : rd(mult(X0,X1),mult(mult(X1,X1),mult(X1,X1))) = mult(rd(rd(rd(X0,X1),X1),X1),rd(X1,X1)),
inference(forward_demodulation,[],[f3825,f3306]) ).
fof(f3840,plain,
! [X0,X1] : rd(rd(X0,X1),mult(X1,X1)) = rd(mult(X0,X1),mult(mult(X1,X1),mult(X1,X1))),
inference(forward_demodulation,[],[f3833,f3483]) ).
fof(f3860,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,rd(X0,mult(X0,X0))),
inference(superposition,[],[f1678,f3709]) ).
fof(f3862,plain,
! [X0,X1] : mult(X1,X0) = rd(X1,rd(X0,mult(X0,X0))),
inference(superposition,[],[f1694,f3709]) ).
fof(f3865,plain,
! [X0] : rd(X0,X0) = mult(rd(X0,mult(X0,X0)),X0),
inference(superposition,[],[f3,f3709]) ).
fof(f3885,plain,
! [X0] : rd(rd(X0,X0),mult(X0,X0)) = mult(rd(rd(X0,mult(X0,X0)),X0),rd(X0,X0)),
inference(superposition,[],[f3483,f3709]) ).
fof(f3894,plain,
! [X0] : rd(X0,mult(X0,mult(X0,X0))) = mult(rd(rd(X0,mult(X0,X0)),X0),rd(X0,X0)),
inference(forward_demodulation,[],[f3885,f1921]) ).
fof(f4117,plain,
! [X0] : rd(rd(X0,mult(X0,X0)),X0) = mult(rd(rd(X0,mult(X0,X0)),X0),rd(rd(X0,mult(X0,X0)),rd(X0,mult(X0,X0)))),
inference(superposition,[],[f1607,f3860]) ).
fof(f4195,plain,
! [X0] : rd(rd(X0,mult(X0,X0)),X0) = mult(rd(rd(X0,mult(X0,X0)),X0),mult(rd(X0,mult(X0,X0)),X0)),
inference(forward_demodulation,[],[f4117,f3862]) ).
fof(f4248,plain,
! [X0] : rd(rd(X0,mult(X0,X0)),X0) = mult(rd(rd(X0,mult(X0,X0)),X0),rd(X0,X0)),
inference(forward_demodulation,[],[f4195,f3865]) ).
fof(f4283,plain,
! [X0] : rd(X0,mult(X0,mult(X0,X0))) = rd(rd(X0,mult(X0,X0)),X0),
inference(forward_demodulation,[],[f4248,f3894]) ).
fof(f4729,plain,
! [X0,X1] : rd(ld(X1,mult(X0,X1)),X1) = mult(rd(rd(X1,X1),X1),X0),
inference(superposition,[],[f1915,f4]) ).
fof(f4757,plain,
! [X0,X1] : rd(rd(X0,X0),X0) = rd(rd(ld(X0,X1),X0),rd(X1,X0)),
inference(superposition,[],[f4,f1915]) ).
fof(f4800,plain,
! [X0,X1] : rd(X0,mult(X0,X0)) = rd(rd(ld(X0,X1),X0),rd(X1,X0)),
inference(forward_demodulation,[],[f4757,f3709]) ).
fof(f4828,plain,
! [X0,X1] : rd(ld(X1,mult(X0,X1)),X1) = mult(rd(X1,mult(X1,X1)),X0),
inference(forward_demodulation,[],[f4729,f3709]) ).
fof(f5266,plain,
! [X2,X3,X0,X1] : mult(mult(X3,ld(mult(X0,X2),X1)),X2) = mult(rd(X3,X2),ld(X0,mult(X1,X2))),
inference(superposition,[],[f15,f75]) ).
fof(f5737,plain,
! [X2,X0,X1] : rd(ld(X1,mult(X0,X1)),X1) = mult(ld(X2,rd(X2,X1)),X0),
inference(superposition,[],[f333,f4]) ).
fof(f5960,plain,
! [X2,X0,X1] : mult(ld(X0,rd(X0,X1)),X2) = mult(rd(X1,mult(X1,X1)),X2),
inference(superposition,[],[f4828,f5737]) ).
fof(f5961,plain,
! [X2,X0,X1] : ld(X1,mult(X2,X1)) = mult(mult(ld(X0,rd(X0,X1)),X2),X1),
inference(superposition,[],[f3,f5737]) ).
fof(f6522,plain,
! [X0,X1] : mult(rd(rd(rd(X0,X1),X1),X1),mult(X1,X1)) = mult(rd(X0,mult(X1,X1)),X1),
inference(superposition,[],[f46,f3483]) ).
fof(f6597,plain,
! [X0,X1] : mult(rd(X0,mult(X1,X1)),X1) = mult(mult(rd(rd(X0,X1),X1),X1),rd(X1,X1)),
inference(forward_demodulation,[],[f6522,f1281]) ).
fof(f6640,plain,
! [X0,X1] : mult(rd(X0,X1),rd(X1,X1)) = mult(rd(X0,mult(X1,X1)),X1),
inference(forward_demodulation,[],[f6597,f3]) ).
fof(f6946,plain,
! [X0,X1] : rd(rd(X0,mult(X1,X1)),X1) = mult(rd(rd(rd(X0,X1),X1),X1),rd(X1,X1)),
inference(superposition,[],[f3306,f3483]) ).
fof(f7017,plain,
! [X0,X1] : rd(rd(X0,X1),mult(X1,X1)) = rd(rd(X0,mult(X1,X1)),X1),
inference(forward_demodulation,[],[f6946,f3483]) ).
fof(f7933,plain,
! [X2,X0,X1] : rd(mult(rd(X0,X1),X2),X1) = mult(X0,rd(ld(X1,X2),X1)),
inference(superposition,[],[f31,f3]) ).
fof(f7979,plain,
! [X2,X0,X1] : mult(X0,X2) = rd(rd(mult(X0,X1),X2),rd(ld(X2,X1),X2)),
inference(superposition,[],[f4,f31]) ).
fof(f7994,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,[],[f264,f31]) ).
fof(f8013,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,[],[f7994,f64]) ).
fof(f8067,plain,
! [X2,X3,X1] : mult(rd(mult(X3,X2),X1),X2) = rd(X3,rd(ld(X2,X1),X2)),
inference(forward_demodulation,[],[f8013,f368]) ).
fof(f8668,plain,
! [X2,X3,X0,X1] : rd(mult(rd(ld(X0,X1),X0),X3),mult(X3,mult(rd(X1,X0),X3))) = rd(ld(mult(X2,X0),X2),X3),
inference(superposition,[],[f55,f434]) ).
fof(f8886,plain,
! [X2,X3,X0,X1] : rd(ld(mult(X2,X0),X2),X3) = rd(rd(rd(ld(X0,X1),X0),rd(X1,X0)),X3),
inference(forward_demodulation,[],[f8668,f103]) ).
fof(f8967,plain,
! [X2,X3,X0] : rd(ld(mult(X2,X0),X2),X3) = rd(rd(X0,mult(X0,X0)),X3),
inference(forward_demodulation,[],[f8886,f4800]) ).
fof(f9112,plain,
! [X2,X0,X1] : rd(X0,mult(ld(X1,X2),ld(X1,X2))) = mult(mult(rd(X0,ld(X1,X2)),rd(ld(X1,X2),ld(X1,X2))),ld(X2,X1)),
inference(superposition,[],[f235,f6640]) ).
fof(f9235,plain,
! [X2,X0,X1] : rd(X0,mult(ld(X1,X2),ld(X1,X2))) = mult(mult(rd(X0,ld(X1,X2)),mult(ld(X1,X2),ld(X2,X1))),ld(X2,X1)),
inference(forward_demodulation,[],[f9112,f267]) ).
fof(f9296,plain,
! [X2,X0,X1] : rd(X0,mult(ld(X1,X2),ld(X1,X2))) = mult(mult(rd(X0,ld(X1,X2)),ld(X1,X2)),mult(ld(X2,X1),ld(X2,X1))),
inference(forward_demodulation,[],[f9235,f470]) ).
fof(f9331,plain,
! [X2,X0,X1] : rd(X0,mult(ld(X1,X2),ld(X1,X2))) = mult(X0,mult(ld(X2,X1),ld(X2,X1))),
inference(forward_demodulation,[],[f9296,f3]) ).
fof(f9511,plain,
! [X0,X1] : mult(ld(X1,X0),mult(ld(X0,X1),ld(X0,X1))) = mult(mult(mult(ld(X0,X1),ld(X1,X0)),ld(X0,X1)),rd(ld(X0,X1),ld(X0,X1))),
inference(superposition,[],[f3362,f2146]) ).
fof(f9654,plain,
! [X0,X1] : mult(ld(X1,X0),mult(ld(X0,X1),ld(X0,X1))) = mult(mult(mult(ld(X0,X1),ld(X1,X0)),ld(X0,X1)),mult(ld(X0,X1),ld(X1,X0))),
inference(forward_demodulation,[],[f9511,f267]) ).
fof(f9717,plain,
! [X0,X1] : mult(ld(X0,X1),mult(ld(X0,X1),ld(X1,X0))) = mult(ld(X1,X0),mult(ld(X0,X1),ld(X0,X1))),
inference(forward_demodulation,[],[f9654,f235]) ).
fof(f9761,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X1,X0),mult(ld(X0,X1),ld(X0,X1))),
inference(forward_demodulation,[],[f9717,f1234]) ).
fof(f12332,plain,
! [X0,X1] : rd(X1,mult(X1,X1)) = rd(rd(X0,X1),rd(mult(X1,X0),X1)),
inference(superposition,[],[f4800,f2]) ).
fof(f12602,plain,
! [X0,X1] : rd(ld(X0,X1),mult(ld(X0,X1),ld(X0,X1))) = rd(X0,rd(mult(ld(X0,X1),X1),ld(X0,X1))),
inference(superposition,[],[f12332,f8]) ).
fof(f12688,plain,
! [X0,X1] : mult(X0,mult(rd(mult(X0,X1),X0),X0)) = ld(rd(rd(X0,mult(X0,X0)),X0),X1),
inference(superposition,[],[f98,f12332]) ).
fof(f12738,plain,
! [X0,X1] : ld(rd(X0,mult(X0,mult(X0,X0))),X1) = mult(X0,mult(rd(mult(X0,X1),X0),X0)),
inference(forward_demodulation,[],[f12688,f4283]) ).
fof(f12796,plain,
! [X0,X1] : rd(ld(X0,X1),mult(ld(X0,X1),ld(X0,X1))) = rd(X0,mult(mult(ld(X0,X1),X1),ld(X1,X0))),
inference(forward_demodulation,[],[f12602,f267]) ).
fof(f12804,plain,
! [X0,X1] : ld(rd(X0,mult(X0,mult(X0,X0))),X1) = mult(X0,mult(X0,X1)),
inference(forward_demodulation,[],[f12738,f3]) ).
fof(f12851,plain,
! [X0,X1] : mult(ld(X0,X1),mult(ld(X1,X0),ld(X1,X0))) = rd(X0,mult(mult(ld(X0,X1),X1),ld(X1,X0))),
inference(forward_demodulation,[],[f12796,f9331]) ).
fof(f12894,plain,
! [X0,X1] : ld(X1,X0) = rd(X0,mult(mult(ld(X0,X1),X1),ld(X1,X0))),
inference(forward_demodulation,[],[f12851,f9761]) ).
fof(f13374,plain,
! [X0,X1] : rd(X0,mult(X0,mult(X0,X0))) = rd(X1,mult(X0,mult(X0,X1))),
inference(superposition,[],[f8,f12804]) ).
fof(f18471,plain,
! [X0,X1] : rd(rd(X0,mult(X0,X0)),X0) = rd(ld(X0,X1),mult(X0,mult(rd(X1,X0),X0))),
inference(superposition,[],[f137,f4800]) ).
fof(f18472,plain,
! [X0,X1] : rd(rd(X0,mult(X0,X0)),X0) = rd(X1,mult(X0,mult(rd(mult(X0,X1),X0),X0))),
inference(superposition,[],[f137,f12332]) ).
fof(f18586,plain,
! [X0,X1] : rd(rd(X0,mult(X0,X0)),X0) = rd(X1,mult(X0,mult(X0,X1))),
inference(forward_demodulation,[],[f18472,f3]) ).
fof(f18587,plain,
! [X0,X1] : rd(rd(X0,mult(X0,X0)),X0) = rd(ld(X0,X1),mult(X0,X1)),
inference(forward_demodulation,[],[f18471,f3]) ).
fof(f18626,plain,
! [X0,X1] : rd(rd(X0,X0),mult(X0,X0)) = rd(X1,mult(X0,mult(X0,X1))),
inference(forward_demodulation,[],[f18586,f7017]) ).
fof(f18627,plain,
! [X0,X1] : rd(rd(X0,X0),mult(X0,X0)) = rd(ld(X0,X1),mult(X0,X1)),
inference(forward_demodulation,[],[f18587,f7017]) ).
fof(f18724,plain,
! [X0,X1] : rd(X1,X1) = mult(rd(X0,mult(X1,mult(X1,X0))),mult(X1,X1)),
inference(superposition,[],[f3,f18626]) ).
fof(f19179,plain,
! [X0,X1] : rd(rd(X1,X1),mult(X1,X1)) = rd(ld(X1,ld(X1,X0)),X0),
inference(superposition,[],[f18627,f1]) ).
fof(f19759,plain,
! [X0,X1] : ld(X0,ld(X0,X1)) = mult(rd(rd(X0,X0),mult(X0,X0)),X1),
inference(superposition,[],[f3,f19179]) ).
fof(f19845,plain,
! [X0,X1] : ld(X0,ld(X0,X1)) = mult(rd(X0,mult(X0,mult(X0,X0))),X1),
inference(forward_demodulation,[],[f19759,f1921]) ).
fof(f21331,plain,
! [X2,X0,X1] : rd(X2,mult(X1,X1)) = mult(mult(rd(X2,mult(mult(X1,X1),rd(X1,X1))),mult(X1,X1)),rd(X0,mult(X1,mult(X1,X0)))),
inference(superposition,[],[f34,f18626]) ).
fof(f21361,plain,
! [X2,X0,X1] : mult(rd(X0,mult(X1,X2)),X1) = rd(rd(X0,X1),rd(X2,X1)),
inference(superposition,[],[f4,f34]) ).
fof(f21383,plain,
! [X2,X3,X0,X1] : rd(X2,rd(X3,X1)) = mult(X2,ld(rd(X0,X1),mult(rd(X0,mult(X1,X3)),X1))),
inference(superposition,[],[f264,f34]) ).
fof(f21415,plain,
! [X2,X3,X0,X1] : rd(X2,rd(X3,X1)) = mult(X2,mult(X1,mult(ld(X0,rd(X0,mult(X1,X3))),X1))),
inference(forward_demodulation,[],[f21383,f64]) ).
fof(f21447,plain,
! [X2,X0,X1] : rd(X2,mult(X1,X1)) = mult(mult(rd(X2,mult(X1,X1)),mult(X1,X1)),rd(X0,mult(X1,mult(X1,X0)))),
inference(forward_demodulation,[],[f21331,f1607]) ).
fof(f21555,plain,
! [X2,X3,X1] : rd(X2,rd(X3,X1)) = mult(rd(mult(X2,X1),mult(X1,X3)),X1),
inference(forward_demodulation,[],[f21415,f289]) ).
fof(f21572,plain,
! [X2,X0,X1] : rd(X2,mult(X1,X1)) = mult(X2,rd(X0,mult(X1,mult(X1,X0)))),
inference(forward_demodulation,[],[f21447,f3]) ).
fof(f21796,plain,
! [X2,X0,X1] : rd(X1,mult(rd(X0,X2),rd(X0,X2))) = mult(X1,rd(X2,mult(rd(X0,X2),X0))),
inference(superposition,[],[f21572,f3]) ).
fof(f21865,plain,
! [X2,X0,X1] : ld(X0,rd(X0,mult(X1,X1))) = rd(X2,mult(X1,mult(X1,X2))),
inference(superposition,[],[f2,f21572]) ).
fof(f22429,plain,
! [X0,X1] : rd(X0,X1) = mult(rd(X0,X1),mult(rd(X0,mult(X1,X0)),X1)),
inference(superposition,[],[f1050,f21361]) ).
fof(f22771,plain,
! [X2,X0,X1] : rd(X2,rd(mult(rd(X0,X0),X1),rd(X0,X0))) = mult(rd(mult(X2,rd(X0,X0)),ld(rd(X0,X0),X1)),rd(X0,X0)),
inference(superposition,[],[f21555,f3343]) ).
fof(f22922,plain,
! [X2,X0,X1] : rd(X2,rd(mult(rd(X0,X0),X1),rd(X0,X0))) = mult(mult(mult(X2,rd(X0,X0)),ld(X1,rd(X0,X0))),rd(X0,X0)),
inference(forward_demodulation,[],[f22771,f267]) ).
fof(f23024,plain,
! [X2,X0,X1] : rd(X2,rd(mult(rd(X0,X0),X1),rd(X0,X0))) = mult(X2,mult(rd(X0,X0),mult(ld(X1,rd(X0,X0)),rd(X0,X0)))),
inference(forward_demodulation,[],[f22922,f5]) ).
fof(f23088,plain,
! [X2,X0,X1] : rd(X2,rd(mult(rd(X0,X0),X1),rd(X0,X0))) = mult(X2,ld(mult(X1,rd(X0,X0)),rd(X0,X0))),
inference(forward_demodulation,[],[f23024,f1492]) ).
fof(f23133,plain,
! [X2,X0,X1] : mult(X2,ld(mult(X1,rd(X0,X0)),rd(X0,X0))) = rd(X2,mult(mult(rd(X0,X0),X1),rd(X0,X0))),
inference(forward_demodulation,[],[f23088,f1145]) ).
fof(f28468,plain,
! [X2,X3,X0,X1] : rd(mult(ld(X0,rd(X0,ld(mult(X1,X2),X1))),X3),X2) = ld(ld(mult(X1,X2),X1),mult(X3,ld(mult(X1,X2),X1))),
inference(superposition,[],[f5961,f264]) ).
fof(f28636,plain,
! [X2,X3,X0,X1] : rd(mult(ld(X0,rd(X0,ld(mult(X1,X2),X1))),X3),X2) = ld(ld(mult(X1,X2),X1),rd(X3,X2)),
inference(forward_demodulation,[],[f28468,f264]) ).
fof(f28749,plain,
! [X2,X3,X0,X1] : ld(ld(mult(X1,X2),X1),rd(X3,X2)) = rd(mult(ld(X0,mult(X0,ld(X1,mult(X1,X2)))),X3),X2),
inference(forward_demodulation,[],[f28636,f267]) ).
fof(f28813,plain,
! [X2,X3,X1] : ld(ld(mult(X1,X2),X1),rd(X3,X2)) = rd(mult(ld(X1,mult(X1,X2)),X3),X2),
inference(forward_demodulation,[],[f28749,f2]) ).
fof(f28846,plain,
! [X2,X3,X1] : ld(ld(mult(X1,X2),X1),rd(X3,X2)) = rd(mult(X2,X3),X2),
inference(forward_demodulation,[],[f28813,f2]) ).
fof(f29031,plain,
! [X2,X0,X1] : ld(mult(X2,X0),X2) = rd(rd(X1,X0),rd(mult(X0,X1),X0)),
inference(superposition,[],[f8,f28846]) ).
fof(f29058,plain,
! [X2,X0,X1] : ld(mult(X2,X0),X2) = mult(rd(X1,mult(X0,mult(X0,X1))),X0),
inference(forward_demodulation,[],[f29031,f21361]) ).
fof(f30355,plain,
! [X2,X0,X1] : ld(mult(X1,rd(X0,X2)),X1) = mult(rd(X2,mult(rd(X0,X2),X0)),rd(X0,X2)),
inference(superposition,[],[f29058,f3]) ).
fof(f32852,plain,
! [X2,X3,X0,X1] : ld(X0,mult(X0,rd(X1,mult(rd(X2,X1),X2)))) = rd(X3,mult(rd(X2,X1),mult(rd(X2,X1),X3))),
inference(superposition,[],[f21865,f21796]) ).
fof(f33218,plain,
! [X2,X3,X1] : rd(X1,mult(rd(X2,X1),X2)) = rd(X3,mult(rd(X2,X1),mult(rd(X2,X1),X3))),
inference(forward_demodulation,[],[f32852,f2]) ).
fof(f35245,plain,
! [X2,X0,X1] : rd(ld(X2,rd(X2,X1)),X1) = rd(X0,mult(X1,mult(X1,X0))),
inference(superposition,[],[f1381,f13374]) ).
fof(f39376,plain,
! [X3,X0,X1] : mult(rd(X0,mult(X1,mult(X1,X0))),X3) = mult(rd(mult(X1,X1),mult(mult(X1,X1),mult(X1,X1))),X3),
inference(superposition,[],[f5960,f21865]) ).
fof(f40128,plain,
! [X3,X0,X1] : mult(rd(X0,mult(X1,mult(X1,X0))),X3) = mult(rd(rd(X1,X1),mult(X1,X1)),X3),
inference(forward_demodulation,[],[f39376,f3840]) ).
fof(f40386,plain,
! [X3,X0,X1] : mult(rd(X0,mult(X1,mult(X1,X0))),X3) = mult(rd(X1,mult(X1,mult(X1,X1))),X3),
inference(forward_demodulation,[],[f40128,f1921]) ).
fof(f40601,plain,
! [X3,X0,X1] : ld(X1,ld(X1,X3)) = mult(rd(X0,mult(X1,mult(X1,X0))),X3),
inference(forward_demodulation,[],[f40386,f19845]) ).
fof(f42193,plain,
! [X2,X3,X0,X1] : mult(rd(X2,mult(X1,mult(X1,X2))),X3) = rd(rd(ld(mult(X0,X1),X0),X3),rd(ld(X3,X1),X3)),
inference(superposition,[],[f7979,f29058]) ).
fof(f42501,plain,
! [X2,X3,X0,X1] : mult(rd(X2,mult(X1,mult(X1,X2))),X3) = mult(rd(mult(rd(ld(mult(X0,X1),X0),X3),X3),X1),X3),
inference(forward_demodulation,[],[f42193,f8067]) ).
fof(f42685,plain,
! [X2,X3,X0,X1] : mult(rd(X2,mult(X1,mult(X1,X2))),X3) = mult(rd(ld(mult(X0,X1),X0),X1),X3),
inference(forward_demodulation,[],[f42501,f3]) ).
fof(f42817,plain,
! [X3,X0,X1] : ld(X1,ld(X1,X3)) = mult(rd(ld(mult(X0,X1),X0),X1),X3),
inference(forward_demodulation,[],[f42685,f40601]) ).
fof(f44576,plain,
! [X2,X0,X1] : rd(ld(mult(X0,rd(X1,X2)),X0),rd(X1,X2)) = rd(X2,mult(rd(X1,X2),X1)),
inference(superposition,[],[f4,f30355]) ).
fof(f44623,plain,
! [X2,X3,X0,X1] : mult(rd(X2,mult(rd(X1,X2),X1)),X3) = rd(rd(ld(mult(X0,rd(X1,X2)),X0),X3),rd(ld(X3,rd(X1,X2)),X3)),
inference(superposition,[],[f7979,f30355]) ).
fof(f44657,plain,
! [X2,X3,X0,X1] : mult(rd(X2,mult(rd(X1,X2),X1)),X3) = mult(rd(mult(rd(ld(mult(X0,rd(X1,X2)),X0),X3),X3),rd(X1,X2)),X3),
inference(forward_demodulation,[],[f44623,f8067]) ).
fof(f44860,plain,
! [X2,X3,X0,X1] : mult(rd(X2,mult(rd(X1,X2),X1)),X3) = mult(rd(ld(mult(X0,rd(X1,X2)),X0),rd(X1,X2)),X3),
inference(forward_demodulation,[],[f44657,f3]) ).
fof(f45007,plain,
! [X2,X3,X1] : mult(rd(X2,mult(rd(X1,X2),X1)),X3) = ld(rd(X1,X2),ld(rd(X1,X2),X3)),
inference(forward_demodulation,[],[f44860,f42817]) ).
fof(f67306,plain,
! [X2,X0,X1] : rd(rd(X1,X1),mult(mult(X0,rd(X1,X1)),X0)) = rd(X2,mult(mult(X0,rd(X1,X1)),mult(mult(X0,rd(X1,X1)),X2))),
inference(superposition,[],[f33218,f1145]) ).
fof(f78490,plain,
! [X0,X1] : rd(X1,rd(X0,X1)) = mult(rd(X1,rd(X0,X1)),mult(rd(X1,X0),rd(X0,X1))),
inference(superposition,[],[f22429,f3]) ).
fof(f78549,plain,
! [X0,X1] : rd(rd(X0,X1),X1) = mult(X0,rd(ld(X1,mult(rd(X0,mult(X1,X0)),X1)),X1)),
inference(superposition,[],[f7933,f22429]) ).
fof(f78700,plain,
! [X0,X1] : rd(rd(X0,X1),X1) = mult(X0,mult(rd(X1,mult(X1,X1)),rd(X0,mult(X1,X0)))),
inference(forward_demodulation,[],[f78549,f4828]) ).
fof(f125863,plain,
! [X2,X0,X1] : rd(X2,mult(rd(X0,X1),rd(X1,X0))) = mult(X2,ld(rd(X0,rd(X1,X0)),rd(X0,rd(X1,X0)))),
inference(superposition,[],[f264,f78490]) ).
fof(f125969,plain,
! [X2,X0,X1] : rd(X2,mult(rd(X0,X1),rd(X1,X0))) = mult(X2,rd(rd(X0,rd(X1,X0)),rd(X0,rd(X1,X0)))),
inference(forward_demodulation,[],[f125863,f1006]) ).
fof(f126178,plain,
! [X2,X0,X1] : rd(X2,mult(rd(X0,X1),rd(X1,X0))) = mult(X2,mult(rd(X0,mult(rd(X1,X0),X0)),rd(X1,X0))),
inference(forward_demodulation,[],[f125969,f21361]) ).
fof(f126336,plain,
! [X2,X0,X1] : mult(X2,mult(rd(X0,X1),rd(X1,X0))) = rd(X2,mult(rd(X0,X1),rd(X1,X0))),
inference(forward_demodulation,[],[f126178,f3]) ).
fof(f212881,plain,
! [X0,X1] : rd(rd(X1,rd(X0,X0)),rd(X0,X0)) = mult(X1,mult(mult(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))),rd(X1,mult(rd(X0,X0),X1)))),
inference(superposition,[],[f78700,f126336]) ).
fof(f213510,plain,
! [X0,X1] : rd(rd(X1,rd(X0,X0)),rd(X0,X0)) = mult(X1,mult(rd(X0,X0),rd(X1,mult(rd(X0,X0),X1)))),
inference(forward_demodulation,[],[f212881,f1236]) ).
fof(f213776,plain,
! [X0,X1] : mult(rd(X1,rd(X0,X0)),rd(X0,X0)) = mult(X1,mult(rd(X0,X0),rd(X1,mult(rd(X0,X0),X1)))),
inference(forward_demodulation,[],[f213510,f1145]) ).
fof(f214002,plain,
! [X0,X1] : mult(X1,mult(rd(X0,X0),rd(X1,mult(rd(X0,X0),X1)))) = X1,
inference(forward_demodulation,[],[f213776,f3]) ).
fof(f320417,plain,
! [X0,X1] : rd(X0,X0) = mult(rd(mult(rd(X1,X1),rd(X0,mult(rd(X1,X1),X0))),mult(X0,X0)),mult(X0,X0)),
inference(superposition,[],[f18724,f214002]) ).
fof(f320608,plain,
! [X0,X1] : rd(X0,X0) = mult(rd(X1,X1),rd(X0,mult(rd(X1,X1),X0))),
inference(forward_demodulation,[],[f320417,f3]) ).
fof(f321480,plain,
! [X0,X1] : rd(mult(rd(X1,X1),X0),mult(rd(X0,mult(rd(X1,X1),X0)),X0)) = rd(ld(rd(X0,X0),rd(X1,X1)),rd(X0,mult(rd(X1,X1),X0))),
inference(superposition,[],[f44576,f320608]) ).
fof(f321483,plain,
! [X0,X1] : rd(X0,mult(rd(X1,X1),X0)) = ld(rd(X1,X1),rd(X0,X0)),
inference(superposition,[],[f2,f320608]) ).
fof(f321516,plain,
! [X2,X0,X1] : rd(X1,rd(X0,mult(rd(X2,X2),X0))) = mult(X1,ld(rd(X0,X0),rd(X2,X2))),
inference(superposition,[],[f264,f320608]) ).
fof(f321725,plain,
! [X0,X1] : rd(mult(rd(X1,X1),X0),mult(rd(X0,mult(rd(X1,X1),X0)),X0)) = mult(ld(rd(X0,X0),rd(X1,X1)),ld(rd(X0,X0),rd(X1,X1))),
inference(forward_demodulation,[],[f321480,f321516]) ).
fof(f321905,plain,
! [X0,X1] : rd(mult(rd(X1,X1),X0),mult(rd(X0,mult(rd(X1,X1),X0)),X0)) = mult(rd(X1,mult(rd(X0,X0),X1)),rd(X1,mult(rd(X0,X0),X1))),
inference(forward_demodulation,[],[f321725,f321483]) ).
fof(f322312,plain,
! [X0,X1] : rd(rd(X0,X0),mult(rd(X1,X1),rd(X0,X0))) = ld(rd(X1,X1),mult(rd(X0,X0),rd(X0,X0))),
inference(superposition,[],[f321483,f1145]) ).
fof(f322325,plain,
! [X2,X0,X1] : rd(ld(mult(X1,X0),X1),mult(rd(X2,X2),ld(mult(X1,X0),X1))) = ld(rd(X2,X2),rd(rd(X0,mult(X0,X0)),ld(mult(X1,X0),X1))),
inference(superposition,[],[f321483,f8967]) ).
fof(f322331,plain,
! [X2,X0,X1] : rd(rd(X0,X1),mult(rd(X2,X2),rd(X0,X1))) = ld(rd(X2,X2),mult(rd(X0,mult(X1,X0)),X1)),
inference(superposition,[],[f321483,f21361]) ).
fof(f322435,plain,
! [X2,X0,X1] : mult(mult(X2,ld(rd(X0,X0),rd(X1,X1))),rd(X0,mult(rd(X1,X1),X0))) = X2,
inference(superposition,[],[f235,f321483]) ).
fof(f322541,plain,
! [X2,X0,X1] : mult(mult(X2,rd(X1,mult(rd(X0,X0),X1))),rd(X0,mult(rd(X1,X1),X0))) = X2,
inference(forward_demodulation,[],[f322435,f321483]) ).
fof(f322604,plain,
! [X2,X0,X1] : rd(ld(mult(X1,X0),X1),mult(rd(X2,X2),ld(mult(X1,X0),X1))) = ld(rd(X2,X2),mult(rd(X0,mult(X0,X0)),ld(X1,mult(X1,X0)))),
inference(forward_demodulation,[],[f322325,f267]) ).
fof(f322617,plain,
! [X0,X1] : ld(rd(X1,X1),rd(X0,X0)) = rd(rd(X0,X0),mult(rd(X1,X1),rd(X0,X0))),
inference(forward_demodulation,[],[f322312,f1459]) ).
fof(f322727,plain,
! [X2,X0,X1] : rd(ld(mult(X1,X0),X1),mult(rd(X2,X2),ld(mult(X1,X0),X1))) = ld(rd(X2,X2),mult(rd(X0,mult(X0,X0)),X0)),
inference(forward_demodulation,[],[f322604,f2]) ).
fof(f322739,plain,
! [X0,X1] : rd(X0,mult(rd(X1,X1),X0)) = rd(rd(X0,X0),mult(rd(X1,X1),rd(X0,X0))),
inference(forward_demodulation,[],[f322617,f321483]) ).
fof(f322807,plain,
! [X2,X0,X1] : rd(rd(X0,X0),mult(rd(X2,X2),rd(X0,X0))) = rd(ld(mult(X1,X0),X1),mult(rd(X2,X2),ld(mult(X1,X0),X1))),
inference(forward_demodulation,[],[f322727,f322331]) ).
fof(f322867,plain,
! [X2,X0,X1] : rd(rd(X0,X0),mult(rd(X2,X2),rd(X0,X0))) = rd(ld(mult(X1,X0),X1),rd(rd(X2,X2),X0)),
inference(forward_demodulation,[],[f322807,f264]) ).
fof(f322902,plain,
! [X2,X0,X1] : rd(X0,mult(rd(X2,X2),X0)) = rd(ld(mult(X1,X0),X1),rd(rd(X2,X2),X0)),
inference(forward_demodulation,[],[f322867,f322739]) ).
fof(f323236,plain,
! [X2,X0,X1] : ld(mult(X2,X0),X2) = mult(rd(X0,mult(rd(X1,X1),X0)),rd(rd(X1,X1),X0)),
inference(superposition,[],[f3,f322902]) ).
fof(f323353,plain,
! [X2,X3,X0,X1] : mult(rd(rd(rd(X1,X1),X0),mult(rd(X0,mult(rd(X1,X1),X0)),ld(mult(X2,X0),X2))),X3) = ld(rd(X0,mult(rd(X1,X1),X0)),ld(rd(X0,mult(rd(X1,X1),X0)),X3)),
inference(superposition,[],[f45007,f322902]) ).
fof(f323400,plain,
! [X2,X3,X0,X1] : mult(rd(rd(rd(X1,X1),X0),mult(rd(X0,mult(rd(X1,X1),X0)),ld(mult(X2,X0),X2))),X3) = mult(rd(mult(rd(X1,X1),X0),mult(rd(X0,mult(rd(X1,X1),X0)),X0)),X3),
inference(forward_demodulation,[],[f323353,f45007]) ).
fof(f323745,plain,
! [X2,X3,X0,X1] : mult(rd(rd(rd(X1,X1),X0),mult(rd(X0,mult(rd(X1,X1),X0)),ld(mult(X2,X0),X2))),X3) = mult(mult(rd(X1,mult(rd(X0,X0),X1)),rd(X1,mult(rd(X0,X0),X1))),X3),
inference(forward_demodulation,[],[f323400,f321905]) ).
fof(f324003,plain,
! [X3,X0,X1] : mult(mult(rd(X1,mult(rd(X0,X0),X1)),rd(X1,mult(rd(X0,X0),X1))),X3) = mult(rd(rd(rd(X1,X1),X0),rd(rd(X0,mult(rd(X1,X1),X0)),X0)),X3),
inference(forward_demodulation,[],[f323745,f264]) ).
fof(f324138,plain,
! [X3,X0,X1] : mult(mult(rd(X1,mult(rd(X0,X0),X1)),rd(X1,mult(rd(X0,X0),X1))),X3) = mult(mult(rd(rd(X1,X1),mult(X0,rd(X0,mult(rd(X1,X1),X0)))),X0),X3),
inference(forward_demodulation,[],[f324003,f21361]) ).
fof(f326127,plain,
! [X2,X3,X0,X1] : ld(mult(X2,rd(X1,mult(rd(X3,X3),X1))),X2) = mult(rd(rd(rd(X3,X3),X1),mult(rd(X1,mult(rd(X3,X3),X1)),ld(mult(X0,X1),X0))),rd(X1,mult(rd(X3,X3),X1))),
inference(superposition,[],[f29058,f323236]) ).
fof(f326196,plain,
! [X2,X3,X1] : ld(mult(X2,rd(X1,mult(rd(X3,X3),X1))),X2) = mult(rd(rd(rd(X3,X3),X1),rd(rd(X1,mult(rd(X3,X3),X1)),X1)),rd(X1,mult(rd(X3,X3),X1))),
inference(forward_demodulation,[],[f326127,f264]) ).
fof(f326722,plain,
! [X2,X3,X1] : ld(mult(X2,rd(X1,mult(rd(X3,X3),X1))),X2) = mult(mult(rd(rd(X3,X3),mult(X1,rd(X1,mult(rd(X3,X3),X1)))),X1),rd(X1,mult(rd(X3,X3),X1))),
inference(forward_demodulation,[],[f326196,f21361]) ).
fof(f327088,plain,
! [X2,X3,X1] : ld(mult(X2,rd(X1,mult(rd(X3,X3),X1))),X2) = mult(mult(rd(X3,mult(rd(X1,X1),X3)),rd(X3,mult(rd(X1,X1),X3))),rd(X1,mult(rd(X3,X3),X1))),
inference(forward_demodulation,[],[f326722,f324138]) ).
fof(f327337,plain,
! [X2,X3,X1] : ld(mult(X2,rd(X1,mult(rd(X3,X3),X1))),X2) = rd(X3,mult(rd(X1,X1),X3)),
inference(forward_demodulation,[],[f327088,f322541]) ).
fof(f327871,plain,
! [X2,X0,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = ld(mult(mult(X0,mult(rd(X1,X1),ld(X2,X2))),rd(rd(X2,X2),mult(rd(X1,X1),ld(X2,X2)))),mult(X0,mult(rd(X1,X1),ld(X2,X2)))),
inference(superposition,[],[f327337,f1100]) ).
fof(f328227,plain,
! [X2,X0,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = mult(mult(rd(X1,X1),ld(X2,X2)),mult(ld(mult(X0,mult(mult(rd(X1,X1),ld(X2,X2)),rd(X2,X2))),X0),mult(rd(X1,X1),ld(X2,X2)))),
inference(forward_demodulation,[],[f327871,f77]) ).
fof(f328458,plain,
! [X2,X0,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),mult(ld(mult(X0,mult(mult(rd(X1,X1),rd(X2,X2)),rd(X2,X2))),X0),mult(rd(X1,X1),rd(X2,X2)))),
inference(forward_demodulation,[],[f328227,f1006]) ).
fof(f328639,plain,
! [X2,X0,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),mult(ld(mult(X0,rd(X1,X1)),X0),mult(rd(X1,X1),rd(X2,X2)))),
inference(forward_demodulation,[],[f328458,f1112]) ).
fof(f328764,plain,
! [X2,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),mult(ld(X1,X1),mult(rd(X1,X1),rd(X2,X2)))),
inference(forward_demodulation,[],[f328639,f1088]) ).
fof(f328866,plain,
! [X2,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),mult(rd(X1,X1),mult(rd(X1,X1),rd(X2,X2)))),
inference(forward_demodulation,[],[f328764,f1099]) ).
fof(f328941,plain,
! [X2,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),ld(rd(X1,X1),rd(X2,X2))),
inference(forward_demodulation,[],[f328866,f3343]) ).
fof(f329001,plain,
! [X2,X1] : rd(X1,mult(rd(ld(X2,X2),ld(X2,X2)),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),rd(X2,mult(rd(X1,X1),X2))),
inference(forward_demodulation,[],[f328941,f321483]) ).
fof(f329041,plain,
! [X2,X1] : mult(mult(rd(X1,X1),rd(X2,X2)),rd(X2,mult(rd(X1,X1),X2))) = rd(X1,mult(mult(ld(X2,X2),ld(X2,X2)),X1)),
inference(forward_demodulation,[],[f329001,f267]) ).
fof(f329064,plain,
! [X2,X1] : mult(mult(rd(X1,X1),rd(X2,X2)),rd(X2,mult(rd(X1,X1),X2))) = rd(X1,mult(mult(ld(X2,X2),rd(X2,X2)),X1)),
inference(forward_demodulation,[],[f329041,f1006]) ).
fof(f329081,plain,
! [X2,X1] : rd(X1,mult(mult(rd(X2,X2),rd(X2,X2)),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),rd(X2,mult(rd(X1,X1),X2))),
inference(forward_demodulation,[],[f329064,f1105]) ).
fof(f329092,plain,
! [X2,X1] : rd(X1,mult(rd(X2,X2),X1)) = mult(mult(rd(X1,X1),rd(X2,X2)),rd(X2,mult(rd(X1,X1),X2))),
inference(forward_demodulation,[],[f329081,f1459]) ).
fof(f329250,plain,
! [X0,X1] : mult(rd(X1,X1),rd(X0,X0)) = ld(rd(X0,mult(rd(X1,X1),X0)),rd(X0,X0)),
inference(superposition,[],[f9,f322739]) ).
fof(f329254,plain,
! [X2,X0,X1] : mult(rd(X2,mult(rd(X1,X1),rd(X0,X0))),mult(mult(rd(X1,X1),rd(X0,X0)),rd(X0,X0))) = mult(mult(X2,rd(X0,mult(rd(X1,X1),X0))),mult(rd(X1,X1),rd(X0,X0))),
inference(superposition,[],[f46,f322739]) ).
fof(f329352,plain,
! [X2,X0,X1] : rd(ld(rd(X0,X0),rd(X0,mult(rd(X1,X1),X0))),mult(rd(X1,X1),rd(X0,X0))) = rd(X2,mult(mult(rd(X1,X1),rd(X0,X0)),mult(mult(rd(X1,X1),rd(X0,X0)),X2))),
inference(superposition,[],[f35245,f322739]) ).
fof(f329403,plain,
! [X0,X1] : rd(ld(rd(X0,X0),rd(X0,mult(rd(X1,X1),X0))),mult(rd(X1,X1),rd(X0,X0))) = rd(rd(X0,X0),mult(mult(rd(X1,X1),rd(X0,X0)),rd(X1,X1))),
inference(forward_demodulation,[],[f329352,f67306]) ).
fof(f329467,plain,
! [X2,X0,X1] : mult(mult(X2,rd(X0,mult(rd(X1,X1),X0))),mult(rd(X1,X1),rd(X0,X0))) = mult(rd(X2,mult(rd(X1,X1),rd(X0,X0))),rd(X1,X1)),
inference(forward_demodulation,[],[f329254,f1112]) ).
fof(f329606,plain,
! [X0,X1] : rd(ld(rd(X0,X0),rd(X0,mult(rd(X1,X1),X0))),mult(rd(X1,X1),rd(X0,X0))) = mult(rd(X0,X0),ld(mult(rd(X0,X0),rd(X1,X1)),rd(X1,X1))),
inference(forward_demodulation,[],[f329403,f23133]) ).
fof(f330299,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),mult(mult(ld(rd(X1,X1),rd(X1,mult(rd(X0,X0),X1))),rd(X1,mult(rd(X0,X0),X1))),mult(rd(X0,X0),rd(X1,X1)))),
inference(superposition,[],[f12894,f329250]) ).
fof(f330358,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),mult(rd(ld(rd(X1,X1),rd(X1,mult(rd(X0,X0),X1))),mult(rd(X0,X0),rd(X1,X1))),rd(X0,X0))),
inference(forward_demodulation,[],[f330299,f329467]) ).
fof(f330528,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),mult(mult(rd(X1,X1),ld(mult(rd(X1,X1),rd(X0,X0)),rd(X0,X0))),rd(X0,X0))),
inference(forward_demodulation,[],[f330358,f329606]) ).
fof(f330665,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),mult(rd(rd(X1,X1),rd(X0,X0)),ld(rd(X1,X1),mult(rd(X0,X0),rd(X0,X0))))),
inference(forward_demodulation,[],[f330528,f5266]) ).
fof(f330784,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),mult(rd(rd(X1,X1),rd(X0,X0)),ld(rd(X1,X1),rd(X0,X0)))),
inference(forward_demodulation,[],[f330665,f1459]) ).
fof(f330878,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),mult(rd(rd(X1,X1),rd(X0,X0)),rd(X0,mult(rd(X1,X1),X0)))),
inference(forward_demodulation,[],[f330784,f321483]) ).
fof(f330954,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),mult(mult(rd(X1,X1),rd(X0,X0)),rd(X0,mult(rd(X1,X1),X0)))),
inference(forward_demodulation,[],[f330878,f1145]) ).
fof(f331009,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = rd(rd(X1,X1),rd(X1,mult(rd(X0,X0),X1))),
inference(forward_demodulation,[],[f330954,f329092]) ).
fof(f331048,plain,
! [X0,X1] : mult(rd(X0,X0),rd(X1,X1)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X0,X0))),
inference(forward_demodulation,[],[f331009,f321516]) ).
fof(f331075,plain,
! [X0,X1] : rd(X0,X0) = mult(rd(X0,X0),rd(X1,X1)),
inference(forward_demodulation,[],[f331048,f1]) ).
fof(f331467,plain,
! [X0,X1] : rd(rd(X0,X0),rd(X0,X0)) = mult(rd(rd(X1,X1),mult(rd(X0,X0),rd(X0,X0))),mult(rd(X0,X0),rd(X0,X0))),
inference(superposition,[],[f18724,f331075]) ).
fof(f331607,plain,
! [X0,X1] : rd(X1,X1) = rd(rd(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f331467,f3]) ).
fof(f331944,plain,
! [X0,X1] : rd(X1,X1) = mult(rd(X0,X0),rd(X0,X0)),
inference(forward_demodulation,[],[f331607,f1145]) ).
fof(f332226,plain,
! [X0,X1] : rd(X1,X1) = rd(X0,X0),
inference(forward_demodulation,[],[f331944,f331075]) ).
fof(f333105,plain,
! [X0,X1] : mult(rd(X0,X0),X1) = X1,
inference(superposition,[],[f3,f332226]) ).
fof(f346319,plain,
x0 != x0,
inference(superposition,[],[f7,f333105]) ).
fof(f346747,plain,
$false,
inference(trivial_inequality_removal,[],[f346319]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP655-12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/5.81 % Computer : n004.cluster.edu
% 0.14/5.81 % Model : x86_64 x86_64
% 0.14/5.81 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.81 % Memory : 8046.5625MB
% 0.14/5.81 % OS : Linux 6.8.0-71-generic
% 0.14/5.81 % CPULimit : 300
% 0.14/5.81 % WCLimit : 300
% 0.14/5.81 % DateTime : Sun Sep 27 10:32:15 UTC 2026
% 0.14/5.81 % CPUTime :
% 0.14/5.82 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/5.84 Running first-order theorem proving
% 0.14/5.84 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
% 87.87/18.63 % (3313775)Detected a unit-equality problem, will run specialized UEQ schedule.
% 87.87/18.63 % (3313783)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=907465478:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 87.87/18.63 % (3313783)Instruction limit reached!
% 87.87/18.63 % (3313783)------------------------------
% 87.87/18.63 % (3313783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.87/18.63 % (3313783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.87/18.63 % (3313783)CaDiCaL version: 2.1.3
% 87.87/18.63 % (3313783)Termination reason: Instruction limit
% 87.87/18.63 % (3313783)Termination phase: Saturation
% 87.87/18.63 % (3313783)Time elapsed: 0.043 s
% 87.87/18.63 % (3313783)Peak memory usage: 88 MB
% 87.87/18.63 % (3313783)Instructions burned: 139 (million)
% 87.87/18.63 % (3313785)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1847745929:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 87.87/18.63 % (3313786)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3370190710:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 87.87/18.63 % (3313782)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=832420072:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 87.87/18.63 % (3313781)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=2051545619:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 87.87/18.63 % (3313784)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2480606184:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 87.87/18.63 % (3313780)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=571529231:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 87.87/18.63 % (3313794)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=926606975:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 87.87/18.63 % (3313784)Instruction limit reached!
% 87.87/18.63 % (3313784)------------------------------
% 87.87/18.63 % (3313784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.87/18.63 % (3313784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.87/18.63 % (3313784)CaDiCaL version: 2.1.3
% 87.87/18.63 % (3313784)Termination reason: Instruction limit
% 87.87/18.63 % (3313784)Termination phase: Saturation
% 87.87/18.63 % (3313784)Time elapsed: 0.107 s
% 87.87/18.63 % (3313784)Peak memory usage: 89 MB
% 87.87/18.63 % (3313784)Instructions burned: 181 (million)
% 87.87/18.63 % (3313785)Instruction limit reached!
% 87.87/18.63 % (3313785)------------------------------
% 87.87/18.63 % (3313785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.87/18.63 % (3313785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.87/18.63 % (3313785)CaDiCaL version: 2.1.3
% 87.87/18.63 % (3313785)Termination reason: Instruction limit
% 87.87/18.63 % (3313785)Termination phase: Saturation
% 87.87/18.63 % (3313785)Time elapsed: 0.152 s
% 87.87/18.63 % (3313785)Peak memory usage: 90 MB
% 87.87/18.63 % (3313785)Instructions burned: 257 (million)
% 87.87/18.63 % (3313796)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2703354043:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 87.87/18.63 % (3313797)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=446919156:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 87.87/18.63 % (3313797)Instruction limit reached!
% 87.87/18.63 % (3313797)------------------------------
% 87.87/18.63 % (3313797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.87/18.63 % (3313797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.87/18.63 % (3313797)CaDiCaL version: 2.1.3
% 87.87/18.63 % (3313797)Termination reason: Instruction limit
% 87.87/18.63 % (3313797)Termination phase: Saturation
% 87.87/18.63 % (3313797)Time elapsed: 0.113 s
% 67.81/21.61 % (3313797)Peak memory usage: 90 MB
% 67.81/21.61 % (3313797)Instructions burned: 216 (million)
% 67.81/21.61 % (3313800)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=2789727501: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)
% 67.81/21.61 % (3313786)Instruction limit reached!
% 67.81/21.61 % (3313786)------------------------------
% 67.81/21.61 % (3313786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313786)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313786)Termination reason: Instruction limit
% 67.81/21.61 % (3313786)Termination phase: Saturation
% 67.81/21.61 % (3313786)Time elapsed: 0.652 s
% 67.81/21.61 % (3313786)Peak memory usage: 99 MB
% 67.81/21.61 % (3313786)Instructions burned: 1188 (million)
% 67.81/21.61 % (3313800)Instruction limit reached!
% 67.81/21.61 % (3313800)------------------------------
% 67.81/21.61 % (3313800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313800)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313800)Termination reason: Instruction limit
% 67.81/21.61 % (3313800)Termination phase: Saturation
% 67.81/21.61 % (3313800)Time elapsed: 0.198 s
% 67.81/21.61 % (3313800)Peak memory usage: 93 MB
% 67.81/21.61 % (3313800)Instructions burned: 317 (million)
% 67.81/21.61 % (3313802)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=3010822864:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 67.81/21.61 % (3313794)Instruction limit reached!
% 67.81/21.61 % (3313794)------------------------------
% 67.81/21.61 % (3313794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313794)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313794)Termination reason: Instruction limit
% 67.81/21.61 % (3313794)Termination phase: Saturation
% 67.81/21.61 % (3313794)Time elapsed: 0.713 s
% 67.81/21.61 % (3313794)Peak memory usage: 142 MB
% 67.81/21.61 % (3313794)Instructions burned: 2051 (million)
% 67.81/21.61 % (3313803)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2697613523:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 67.81/21.61 % (3313805)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3008919212:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2990 on theBenchmark for (2990ds/14534Mi)
% 67.81/21.61 % (3313803)Instruction limit reached!
% 67.81/21.61 % (3313803)------------------------------
% 67.81/21.61 % (3313803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313803)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313803)Termination reason: Instruction limit
% 67.81/21.61 % (3313803)Termination phase: Saturation
% 67.81/21.61 % (3313803)Time elapsed: 1.852 s
% 67.81/21.61 % (3313803)Peak memory usage: 120 MB
% 67.81/21.61 % (3313803)Instructions burned: 2837 (million)
% 67.81/21.61 % (3313808)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=904933365:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/11832Mi)
% 67.81/21.61 % (3313796)Instruction limit reached!
% 67.81/21.61 % (3313796)------------------------------
% 67.81/21.61 % (3313796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313796)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313796)Termination reason: Instruction limit
% 67.81/21.61 % (3313796)Termination phase: Saturation
% 67.81/21.61 % (3313796)Time elapsed: 2.970 s
% 67.81/21.61 % (3313796)Peak memory usage: 166 MB
% 67.81/21.61 % (3313796)Instructions burned: 4948 (million)
% 67.81/21.61 % (3313810)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=1974233159:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 67.81/21.61 % (3313810)Instruction limit reached!
% 67.81/21.61 % (3313810)------------------------------
% 67.81/21.61 % (3313810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313810)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313810)Termination reason: Instruction limit
% 67.81/21.61 % (3313810)Termination phase: Saturation
% 67.81/21.61 % (3313810)Time elapsed: 1.383 s
% 67.81/21.61 % (3313810)Peak memory usage: 141 MB
% 67.81/21.61 % (3313810)Instructions burned: 2279 (million)
% 67.81/21.61 % (3313928)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=4163712978:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 67.81/21.61 % (3313805)Instruction limit reached!
% 67.81/21.61 % (3313805)------------------------------
% 67.81/21.61 % (3313805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313805)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313805)Termination reason: Instruction limit
% 67.81/21.61 % (3313805)Termination phase: Saturation
% 67.81/21.61 % (3313805)Time elapsed: 5.036 s
% 67.81/21.61 % (3313805)Peak memory usage: 244 MB
% 67.81/21.61 % (3313805)Instructions burned: 14534 (million)
% 67.81/21.61 % (3314044)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1021721303:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2939 on theBenchmark for (2939ds/21755Mi)
% 67.81/21.61 % (3313928)Instruction limit reached!
% 67.81/21.61 % (3313928)------------------------------
% 67.81/21.61 % (3313928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313928)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313928)Termination reason: Instruction limit
% 67.81/21.61 % (3313928)Termination phase: Saturation
% 67.81/21.61 % (3313928)Time elapsed: 3.682 s
% 67.81/21.61 % (3313928)Peak memory usage: 205 MB
% 67.81/21.61 % (3313928)Instructions burned: 6225 (million)
% 67.81/21.61 % (3313802)Instruction limit reached!
% 67.81/21.61 % (3313802)------------------------------
% 67.81/21.61 % (3313802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313802)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313802)Termination reason: Instruction limit
% 67.81/21.61 % (3313802)Termination phase: Saturation
% 67.81/21.61 % (3313802)Time elapsed: 7.817 s
% 67.81/21.61 % (3313802)Peak memory usage: 231 MB
% 67.81/21.61 % (3313802)Instructions burned: 12125 (million)
% 67.81/21.61 % (3314218)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=1412086281:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2913 on theBenchmark for (2913ds/16427Mi)
% 67.81/21.61 % (3314219)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=2455157134:i=9356:fgj=on:bd=preordered:av=off_2912 on theBenchmark for (2912ds/9356Mi)
% 67.81/21.61 % (3313808)Instruction limit reached!
% 67.81/21.61 % (3313808)------------------------------
% 67.81/21.61 % (3313808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3313808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3313808)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3313808)Termination reason: Instruction limit
% 67.81/21.61 % (3313808)Termination phase: Saturation
% 67.81/21.61 % (3313808)Time elapsed: 7.948 s
% 67.81/21.61 % (3313808)Peak memory usage: 224 MB
% 67.81/21.61 % (3313808)Instructions burned: 11832 (million)
% 67.81/21.61 % (3314222)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=628424012:i=2070:kws=inv_precedence:slsql=off:bd=all_2890 on theBenchmark for (2890ds/2070Mi)
% 67.81/21.61 % (3314222)Instruction limit reached!
% 67.81/21.61 % (3314222)------------------------------
% 67.81/21.61 % (3314222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3314222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3314222)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3314222)Termination reason: Instruction limit
% 67.81/21.61 % (3314222)Termination phase: Saturation
% 67.81/21.61 % (3314222)Time elapsed: 1.253 s
% 67.81/21.61 % (3314222)Peak memory usage: 121 MB
% 67.81/21.61 % (3314222)Instructions burned: 2071 (million)
% 67.81/21.61 % (3314224)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=2450585012:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2876 on theBenchmark for (2876ds/6461Mi)
% 67.81/21.61 % (3314044)Instruction limit reached!
% 67.81/21.61 % (3314044)------------------------------
% 67.81/21.61 % (3314044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3314044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3314044)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3314044)Termination reason: Instruction limit
% 67.81/21.61 % (3314044)Termination phase: Saturation
% 67.81/21.61 % (3314044)Time elapsed: 8.695 s
% 67.81/21.61 % (3314044)Peak memory usage: 198 MB
% 67.81/21.61 % (3314044)Instructions burned: 21755 (million)
% 67.81/21.61 % (3314226)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=3852753196:i=2310:bd=all:ss=included_2851 on theBenchmark for (2851ds/2310Mi)
% 67.81/21.61 % (3313781)First to succeed.
% 67.81/21.61 % (3313781)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3313775"
% 67.81/21.61 % (3314219)Instruction limit reached!
% 67.81/21.61 % (3314219)------------------------------
% 67.81/21.61 % (3314219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.81/21.61 % (3314219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.81/21.61 % (3314219)CaDiCaL version: 2.1.3
% 67.81/21.61 % (3314219)Termination reason: Instruction limit
% 67.81/21.61 % (3314219)Termination phase: Saturation
% 67.81/21.61 % (3314219)Time elapsed: 6.154 s
% 67.81/21.61 % (3314219)Peak memory usage: 484 MB
% 67.81/21.61 % (3314219)Instructions burned: 9358 (million)
% 67.81/21.61 % (3314228)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=3887015448:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2849 on theBenchmark for (2849ds/2616Mi)
% 67.81/21.61 % (3313781)Refutation found. Thanks to Tanya!
% 67.81/21.61 % SZS status Unsatisfiable for theBenchmark
% 67.81/21.61 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/21.80 % (3313781)------------------------------
% 0.17/21.80 % (3313781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/21.80 % (3313781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/21.80 % (3313781)CaDiCaL version: 2.1.3
% 0.17/21.80 % (3313781)Termination reason: Refutation
% 0.17/21.80 % (3313781)Time elapsed: 14.869 s
% 0.17/21.80 % (3313781)Peak memory usage: 310 MB
% 0.17/21.80 % (3313781)Instructions burned: 22915 (million)
% 0.17/21.80 % (3313781)------------------------------
% 0.17/21.80 % (3313781)------------------------------
% 0.17/21.80 % (3313775)Success in time 15.327 s
% 0.17/21.80 % Vampire exiting
%------------------------------------------------------------------------------