%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP662-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:29 AM UTC 2026
% Result : Unsatisfiable 119.83s 17.80s
% Output : Refutation 120.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 10
% Syntax : Number of formulae : 482 ( 482 unt; 0 def)
% Number of atoms : 482 ( 481 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 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 : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 735 ( 735 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(rd(mult(X0,X1),X0),mult(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c07) ).
fof(f8,axiom,
! [X2,X0,X1] : mult(mult(X0,X1),X2) = mult(mult(X0,X2),ld(X2,mult(X1,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c08) ).
fof(f9,axiom,
mult(op_c,op_d) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c09) ).
fof(f10,plain,
unit = mult(op_c,op_d),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
mult(mult(a,mult(op_d,op_c)),b) != mult(a,mult(mult(op_d,op_c),b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f14,plain,
! [X0] : mult(op_c,mult(X0,op_d)) = mult(rd(mult(op_c,X0),op_c),unit),
inference(superposition,[],[f7,f10]) ).
fof(f16,plain,
! [X0] : mult(op_c,mult(X0,op_d)) = rd(mult(op_c,X0),op_c),
inference(forward_demodulation,[],[f14,f5]) ).
fof(f17,plain,
! [X0] : mult(mult(op_c,X0),op_d) = mult(unit,ld(op_d,mult(X0,op_d))),
inference(superposition,[],[f8,f10]) ).
fof(f18,plain,
! [X2,X3,X0,X1] : mult(mult(rd(mult(X0,X1),X0),X3),mult(X0,X2)) = mult(mult(X0,mult(X1,X2)),ld(mult(X0,X2),mult(X3,mult(X0,X2)))),
inference(superposition,[],[f8,f7]) ).
fof(f20,plain,
! [X0] : mult(mult(X0,op_c),op_d) = mult(mult(X0,op_d),ld(op_d,unit)),
inference(superposition,[],[f8,f10]) ).
fof(f25,plain,
! [X0] : mult(mult(op_c,X0),op_d) = ld(op_d,mult(X0,op_d)),
inference(forward_demodulation,[],[f17,f6]) ).
fof(f36,plain,
! [X2,X0,X1] : ld(X2,mult(X1,X2)) = ld(mult(X0,X2),mult(mult(X0,X1),X2)),
inference(superposition,[],[f2,f8]) ).
fof(f37,plain,
! [X2,X0,X1] : mult(X0,X2) = ld(rd(mult(X0,X1),X0),mult(X0,mult(X1,X2))),
inference(superposition,[],[f2,f7]) ).
fof(f38,plain,
! [X0] : ld(unit,X0) = X0,
inference(superposition,[],[f2,f6]) ).
fof(f39,plain,
op_d = ld(op_c,unit),
inference(superposition,[],[f2,f10]) ).
fof(f40,plain,
! [X0] : unit = ld(X0,X0),
inference(superposition,[],[f2,f5]) ).
fof(f55,plain,
! [X2,X0,X1] : mult(X1,mult(X2,ld(X1,X0))) = mult(rd(mult(X1,X2),X1),X0),
inference(superposition,[],[f7,f1]) ).
fof(f56,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),X2)) = mult(rd(X0,X1),mult(X1,X2)),
inference(superposition,[],[f7,f1]) ).
fof(f65,plain,
! [X2,X3,X0,X1] : mult(mult(X0,mult(X1,X2)),ld(mult(X0,X2),mult(X3,mult(X0,X2)))) = mult(mult(X0,mult(X1,ld(X0,X3))),mult(X0,X2)),
inference(backward_demodulation,[],[f18,f55]) ).
fof(f72,plain,
! [X2,X0,X1] : ld(ld(X1,X0),mult(X2,ld(X1,X0))) = ld(X0,mult(mult(X1,X2),ld(X1,X0))),
inference(superposition,[],[f36,f1]) ).
fof(f77,plain,
! [X2,X0,X1] : ld(X1,mult(ld(X2,X0),X1)) = ld(mult(X2,X1),mult(X0,X1)),
inference(superposition,[],[f36,f1]) ).
fof(f106,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f107,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X2,X0)) = mult(mult(X1,rd(X0,X2)),X2),
inference(superposition,[],[f8,f3]) ).
fof(f108,plain,
! [X2,X0,X1] : mult(X0,ld(X1,mult(X2,X1))) = mult(mult(rd(X0,X1),X2),X1),
inference(superposition,[],[f8,f3]) ).
fof(f109,plain,
! [X0] : rd(X0,unit) = X0,
inference(superposition,[],[f5,f3]) ).
fof(f112,plain,
mult(mult(op_c,op_c),op_d) = mult(unit,ld(op_d,unit)),
inference(superposition,[],[f20,f10]) ).
fof(f118,plain,
ld(op_d,unit) = mult(mult(op_c,op_c),op_d),
inference(forward_demodulation,[],[f112,f6]) ).
fof(f127,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f128,plain,
! [X2,X0,X1] : mult(X0,X2) = rd(mult(mult(X0,X1),X2),ld(X2,mult(X1,X2))),
inference(superposition,[],[f4,f8]) ).
fof(f130,plain,
! [X0] : unit = rd(X0,X0),
inference(superposition,[],[f4,f6]) ).
fof(f131,plain,
op_c = rd(unit,op_d),
inference(superposition,[],[f4,f10]) ).
fof(f132,plain,
! [X2,X0,X1] : mult(X0,mult(X1,X2)) = mult(X1,mult(ld(X1,mult(X0,X1)),X2)),
inference(superposition,[],[f56,f4]) ).
fof(f134,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X2),ld(X1,X0))) = mult(rd(X2,X1),X0),
inference(superposition,[],[f56,f1]) ).
fof(f137,plain,
! [X2,X0,X1] : mult(rd(X0,X1),mult(ld(rd(X0,X1),X2),X1)) = mult(rd(X2,rd(X0,X1)),X0),
inference(superposition,[],[f56,f3]) ).
fof(f140,plain,
! [X0] : mult(op_c,mult(ld(op_c,X0),op_d)) = mult(rd(X0,op_c),unit),
inference(superposition,[],[f56,f10]) ).
fof(f147,plain,
! [X0] : mult(op_c,mult(ld(op_c,X0),op_d)) = rd(X0,op_c),
inference(forward_demodulation,[],[f140,f5]) ).
fof(f152,plain,
rd(unit,op_c) = mult(op_c,mult(op_d,op_d)),
inference(superposition,[],[f16,f10]) ).
fof(f167,plain,
! [X2,X0,X1] : mult(X0,X2) = mult(mult(rd(X0,rd(X1,X2)),X2),ld(X2,X1)),
inference(superposition,[],[f107,f3]) ).
fof(f171,plain,
! [X2,X0,X1] : mult(X0,rd(X2,X1)) = rd(mult(mult(X0,X1),ld(X1,X2)),X1),
inference(superposition,[],[f4,f107]) ).
fof(f244,plain,
! [X2,X0,X1] : mult(rd(X0,X1),X2) = rd(mult(X0,X2),ld(X2,mult(X1,X2))),
inference(superposition,[],[f128,f3]) ).
fof(f328,plain,
! [X2,X0,X1] : mult(X1,ld(X2,X0)) = ld(rd(mult(X1,X2),X1),mult(X1,X0)),
inference(superposition,[],[f37,f1]) ).
fof(f373,plain,
! [X2,X0,X1] : rd(X0,ld(X1,mult(X2,X1))) = mult(rd(rd(X0,X1),X2),X1),
inference(superposition,[],[f244,f3]) ).
fof(f383,plain,
! [X2,X0,X1] : mult(rd(X1,rd(X0,X2)),X2) = rd(mult(X1,X2),ld(X2,X0)),
inference(superposition,[],[f244,f3]) ).
fof(f464,plain,
! [X2,X0,X1] : mult(ld(X1,mult(X0,X1)),X2) = ld(X1,mult(X0,mult(X1,X2))),
inference(superposition,[],[f2,f132]) ).
fof(f511,plain,
! [X2,X0,X1] : ld(X1,mult(ld(X2,rd(X0,X1)),X1)) = ld(mult(X2,X1),X0),
inference(superposition,[],[f77,f3]) ).
fof(f513,plain,
! [X0,X1] : ld(X0,mult(ld(X1,unit),X0)) = ld(mult(X1,X0),X0),
inference(superposition,[],[f77,f6]) ).
fof(f588,plain,
! [X2,X0,X1] : rd(mult(X0,X1),X0) = rd(mult(X0,mult(X1,ld(X0,X2))),X2),
inference(superposition,[],[f4,f55]) ).
fof(f598,plain,
! [X0,X1] : rd(mult(X0,X1),X0) = mult(X0,mult(X1,ld(X0,unit))),
inference(superposition,[],[f5,f55]) ).
fof(f673,plain,
! [X2,X0,X1] : mult(X1,ld(ld(X1,X0),X2)) = ld(rd(X0,X1),mult(X1,X2)),
inference(superposition,[],[f328,f1]) ).
fof(f689,plain,
! [X2,X0,X1] : ld(rd(mult(X1,X2),X1),X0) = mult(X1,ld(X2,ld(X1,X0))),
inference(superposition,[],[f328,f1]) ).
fof(f705,plain,
! [X2,X0,X1] : rd(mult(X0,X1),X0) = rd(mult(X0,X2),mult(X0,ld(X1,X2))),
inference(superposition,[],[f127,f328]) ).
fof(f777,plain,
! [X2,X0,X1] : ld(X1,mult(X2,X0)) = mult(ld(X1,mult(X2,X1)),ld(X1,X0)),
inference(superposition,[],[f464,f1]) ).
fof(f787,plain,
! [X0] : mult(ld(op_c,mult(X0,op_c)),op_d) = ld(op_c,mult(X0,unit)),
inference(superposition,[],[f464,f10]) ).
fof(f793,plain,
! [X2,X0,X1] : ld(X1,X0) = mult(ld(X1,mult(rd(X0,mult(X1,X2)),X1)),X2),
inference(superposition,[],[f464,f3]) ).
fof(f796,plain,
mult(ld(op_d,mult(op_c,op_d)),op_d) = ld(op_d,rd(unit,op_c)),
inference(superposition,[],[f464,f152]) ).
fof(f801,plain,
ld(op_d,rd(unit,op_c)) = mult(mult(mult(op_c,op_c),op_d),op_d),
inference(forward_demodulation,[],[f796,f25]) ).
fof(f806,plain,
! [X0] : ld(op_c,X0) = mult(ld(op_c,mult(X0,op_c)),op_d),
inference(forward_demodulation,[],[f787,f5]) ).
fof(f809,plain,
ld(op_d,rd(unit,op_c)) = mult(ld(op_d,unit),op_d),
inference(forward_demodulation,[],[f801,f118]) ).
fof(f830,plain,
! [X2,X0,X1] : mult(ld(X1,X0),ld(X1,X2)) = ld(X1,mult(rd(X0,X1),X2)),
inference(superposition,[],[f777,f3]) ).
fof(f845,plain,
! [X2,X0,X1] : ld(X0,mult(X1,X0)) = rd(ld(X0,mult(X1,X2)),ld(X0,X2)),
inference(superposition,[],[f4,f777]) ).
fof(f873,plain,
! [X2,X0,X1] : rd(mult(X1,X2),X1) = rd(mult(X1,mult(X2,X0)),mult(X1,X0)),
inference(superposition,[],[f588,f2]) ).
fof(f881,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,X2)),X2) = rd(mult(X2,mult(mult(X0,X1),X2)),mult(X1,X2)),
inference(superposition,[],[f588,f8]) ).
fof(f945,plain,
! [X2,X0,X1] : rd(mult(X1,rd(X0,X2)),X1) = rd(mult(X1,X0),mult(X1,X2)),
inference(superposition,[],[f873,f3]) ).
fof(f949,plain,
! [X0] : rd(mult(X0,op_c),X0) = rd(mult(X0,unit),mult(X0,op_d)),
inference(superposition,[],[f873,f10]) ).
fof(f994,plain,
! [X0] : rd(mult(X0,op_c),X0) = rd(X0,mult(X0,op_d)),
inference(forward_demodulation,[],[f949,f5]) ).
fof(f1107,plain,
! [X0,X1] : mult(mult(X1,X0),op_d) = mult(mult(X1,op_d),mult(mult(op_c,X0),op_d)),
inference(superposition,[],[f8,f25]) ).
fof(f1112,plain,
! [X0] : mult(X0,op_d) = mult(op_d,mult(mult(op_c,X0),op_d)),
inference(superposition,[],[f1,f25]) ).
fof(f1126,plain,
! [X0] : mult(ld(op_c,X0),op_d) = mult(op_d,mult(X0,op_d)),
inference(superposition,[],[f1112,f1]) ).
fof(f1151,plain,
! [X0] : rd(X0,op_c) = mult(op_c,mult(op_d,mult(X0,op_d))),
inference(backward_demodulation,[],[f147,f1126]) ).
fof(f1152,plain,
! [X0] : ld(op_c,X0) = mult(op_d,mult(mult(X0,op_c),op_d)),
inference(backward_demodulation,[],[f806,f1126]) ).
fof(f1173,plain,
! [X0] : ld(op_c,rd(X0,op_d)) = mult(op_d,mult(X0,ld(op_d,mult(op_c,op_d)))),
inference(superposition,[],[f1152,f108]) ).
fof(f1178,plain,
! [X0] : mult(mult(X0,op_c),op_d) = ld(op_d,ld(op_c,X0)),
inference(superposition,[],[f2,f1152]) ).
fof(f1194,plain,
! [X0] : ld(op_c,rd(X0,op_d)) = mult(op_d,mult(X0,mult(mult(op_c,op_c),op_d))),
inference(forward_demodulation,[],[f1173,f25]) ).
fof(f1198,plain,
! [X0] : ld(op_c,rd(X0,op_d)) = mult(op_d,mult(X0,ld(op_d,unit))),
inference(forward_demodulation,[],[f1194,f118]) ).
fof(f1200,plain,
! [X0] : rd(mult(op_d,X0),op_d) = ld(op_c,rd(X0,op_d)),
inference(forward_demodulation,[],[f1198,f598]) ).
fof(f1217,plain,
! [X0] : mult(op_c,mult(op_d,X0)) = rd(rd(X0,op_d),op_c),
inference(superposition,[],[f1151,f3]) ).
fof(f1284,plain,
rd(op_d,mult(op_d,op_d)) = ld(op_c,rd(op_c,op_d)),
inference(superposition,[],[f994,f1200]) ).
fof(f1321,plain,
! [X0,X1] : rd(mult(X1,rd(X0,op_d)),mult(X1,op_c)) = rd(mult(X1,mult(op_c,mult(op_d,X0))),X1),
inference(superposition,[],[f945,f1217]) ).
fof(f1341,plain,
! [X0,X1] : mult(mult(X1,ld(op_c,X0)),op_d) = mult(mult(X1,op_d),mult(X0,op_d)),
inference(superposition,[],[f1107,f1]) ).
fof(f1412,plain,
! [X0,X1] : mult(ld(op_c,X0),mult(op_d,X1)) = mult(op_d,mult(ld(op_d,mult(op_d,mult(X0,op_d))),X1)),
inference(superposition,[],[f132,f1126]) ).
fof(f1419,plain,
! [X0,X1] : mult(ld(op_c,X0),mult(op_d,X1)) = mult(op_d,mult(mult(X0,op_d),X1)),
inference(forward_demodulation,[],[f1412,f2]) ).
fof(f1490,plain,
! [X2,X0,X1] : mult(rd(X0,X1),rd(X2,X1)) = rd(mult(X0,ld(X1,X2)),X1),
inference(superposition,[],[f171,f3]) ).
fof(f1494,plain,
! [X0] : mult(op_c,rd(X0,op_d)) = rd(mult(unit,ld(op_d,X0)),op_d),
inference(superposition,[],[f171,f10]) ).
fof(f1503,plain,
! [X2,X0,X1] : mult(X1,rd(mult(X2,X0),X2)) = rd(mult(mult(X1,X2),X0),X2),
inference(superposition,[],[f171,f2]) ).
fof(f1539,plain,
! [X0] : mult(op_c,rd(X0,op_d)) = rd(ld(op_d,X0),op_d),
inference(forward_demodulation,[],[f1494,f6]) ).
fof(f1602,plain,
! [X2,X0,X1] : mult(rd(X0,X1),rd(mult(X1,X2),X1)) = rd(mult(X0,X2),X1),
inference(superposition,[],[f1503,f3]) ).
fof(f1616,plain,
mult(op_c,rd(mult(op_c,op_d),op_c)) = rd(ld(op_d,unit),op_c),
inference(superposition,[],[f1503,f118]) ).
fof(f1627,plain,
! [X2,X3,X0,X1] : mult(mult(X3,X1),ld(X1,mult(mult(X0,X1),X2))) = mult(mult(X3,mult(X0,rd(mult(X1,X2),X1))),X1),
inference(superposition,[],[f107,f1503]) ).
fof(f1642,plain,
rd(ld(op_d,unit),op_c) = mult(op_c,mult(op_c,mult(op_d,op_d))),
inference(forward_demodulation,[],[f1616,f16]) ).
fof(f1658,plain,
rd(ld(op_d,unit),op_c) = mult(op_c,rd(unit,op_c)),
inference(forward_demodulation,[],[f1642,f152]) ).
fof(f1707,plain,
! [X0,X1] : rd(mult(X1,mult(mult(op_c,X0),op_d)),op_d) = mult(rd(X1,op_d),rd(mult(X0,op_d),op_d)),
inference(superposition,[],[f1602,f1112]) ).
fof(f1721,plain,
! [X2,X0,X1] : rd(mult(X2,X1),X2) = ld(rd(X0,X2),rd(mult(X0,X1),X2)),
inference(superposition,[],[f2,f1602]) ).
fof(f1752,plain,
! [X0,X1] : mult(rd(X1,op_d),X0) = rd(mult(X1,mult(mult(op_c,X0),op_d)),op_d),
inference(forward_demodulation,[],[f1707,f4]) ).
fof(f2016,plain,
! [X0,X1] : mult(mult(ld(op_c,mult(X0,op_c)),op_d),mult(X1,op_d)) = mult(ld(op_c,mult(X0,X1)),op_d),
inference(superposition,[],[f1341,f777]) ).
fof(f2065,plain,
! [X0,X1] : mult(mult(ld(op_c,mult(X0,op_c)),op_d),mult(X1,op_d)) = mult(op_d,mult(mult(X0,X1),op_d)),
inference(forward_demodulation,[],[f2016,f1126]) ).
fof(f2076,plain,
! [X0,X1] : mult(op_d,mult(mult(X0,X1),op_d)) = mult(mult(op_d,mult(mult(X0,op_c),op_d)),mult(X1,op_d)),
inference(forward_demodulation,[],[f2065,f1126]) ).
fof(f2080,plain,
! [X0,X1] : mult(ld(op_c,X0),mult(X1,op_d)) = mult(op_d,mult(mult(X0,X1),op_d)),
inference(forward_demodulation,[],[f2076,f1152]) ).
fof(f2088,plain,
! [X0,X1] : mult(X0,mult(X1,op_d)) = mult(op_d,mult(mult(mult(op_c,X0),X1),op_d)),
inference(superposition,[],[f2080,f2]) ).
fof(f2166,plain,
! [X0,X1] : ld(op_c,rd(mult(mult(mult(op_c,X0),X1),op_d),op_d)) = rd(mult(X0,mult(X1,op_d)),op_d),
inference(superposition,[],[f1200,f2088]) ).
fof(f2188,plain,
! [X0,X1] : rd(mult(X0,mult(X1,op_d)),op_d) = ld(op_c,mult(mult(op_c,X0),X1)),
inference(forward_demodulation,[],[f2166,f4]) ).
fof(f2201,plain,
! [X0,X1] : mult(rd(X1,op_d),X0) = ld(op_c,mult(mult(op_c,X1),mult(op_c,X0))),
inference(backward_demodulation,[],[f1752,f2188]) ).
fof(f2205,plain,
! [X0,X1] : mult(rd(X1,op_d),X0) = mult(ld(op_c,mult(mult(op_c,X1),op_c)),X0),
inference(forward_demodulation,[],[f2201,f464]) ).
fof(f2314,plain,
! [X0,X1] : mult(op_c,mult(rd(X0,op_d),X1)) = mult(mult(op_c,X0),mult(op_c,X1)),
inference(superposition,[],[f132,f2205]) ).
fof(f2315,plain,
! [X0,X1] : mult(rd(X0,op_d),ld(op_c,X1)) = ld(op_c,mult(mult(op_c,X0),X1)),
inference(superposition,[],[f777,f2205]) ).
fof(f2343,plain,
! [X0] : rd(ld(op_c,mult(mult(op_c,X0),op_c)),mult(ld(op_c,mult(mult(op_c,X0),op_c)),op_d)) = rd(mult(rd(X0,op_d),op_c),ld(op_c,mult(mult(op_c,X0),op_c))),
inference(superposition,[],[f994,f2205]) ).
fof(f2354,plain,
! [X0] : rd(ld(op_c,mult(mult(op_c,X0),op_c)),mult(ld(op_c,mult(mult(op_c,X0),op_c)),op_d)) = mult(rd(rd(X0,op_d),rd(mult(mult(op_c,X0),op_c),op_c)),op_c),
inference(forward_demodulation,[],[f2343,f383]) ).
fof(f2381,plain,
! [X0,X1] : mult(rd(X0,op_d),ld(op_c,X1)) = rd(mult(X0,mult(X1,op_d)),op_d),
inference(backward_demodulation,[],[f2188,f2315]) ).
fof(f2403,plain,
! [X0] : rd(ld(op_c,mult(mult(op_c,X0),op_c)),mult(ld(op_c,mult(mult(op_c,X0),op_c)),op_d)) = mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c),
inference(forward_demodulation,[],[f2354,f4]) ).
fof(f2445,plain,
! [X0] : mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c) = rd(ld(op_c,mult(mult(op_c,X0),op_c)),mult(op_d,mult(mult(mult(op_c,X0),op_c),op_d))),
inference(forward_demodulation,[],[f2403,f1126]) ).
fof(f2484,plain,
! [X0] : mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c) = rd(ld(op_c,mult(mult(op_c,X0),op_c)),mult(X0,mult(op_c,op_d))),
inference(forward_demodulation,[],[f2445,f2088]) ).
fof(f2501,plain,
! [X0] : mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c) = rd(ld(op_c,mult(mult(op_c,X0),op_c)),mult(X0,unit)),
inference(forward_demodulation,[],[f2484,f10]) ).
fof(f2513,plain,
! [X0] : mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c) = rd(ld(op_c,mult(mult(op_c,X0),op_c)),X0),
inference(forward_demodulation,[],[f2501,f5]) ).
fof(f2521,plain,
! [X0] : mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c) = rd(mult(rd(X0,op_d),ld(op_c,op_c)),X0),
inference(forward_demodulation,[],[f2513,f2315]) ).
fof(f2524,plain,
! [X0] : mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c) = rd(mult(rd(X0,op_d),unit),X0),
inference(forward_demodulation,[],[f2521,f40]) ).
fof(f2526,plain,
! [X0] : mult(rd(rd(X0,op_d),mult(op_c,X0)),op_c) = rd(rd(X0,op_d),X0),
inference(forward_demodulation,[],[f2524,f5]) ).
fof(f2555,plain,
! [X2,X0,X1] : rd(mult(ld(X0,X1),X2),ld(X0,X1)) = ld(X0,rd(mult(X1,X2),ld(X0,X1))),
inference(superposition,[],[f1721,f127]) ).
fof(f2569,plain,
! [X2,X0,X1] : rd(mult(X1,ld(X2,X0)),X1) = ld(rd(X2,X1),rd(X0,X1)),
inference(superposition,[],[f1721,f1]) ).
fof(f2583,plain,
! [X2,X0,X1] : rd(mult(X1,X2),X1) = ld(rd(rd(X0,X2),X1),rd(X0,X1)),
inference(superposition,[],[f1721,f3]) ).
fof(f2587,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = ld(rd(unit,X1),rd(X0,X1)),
inference(superposition,[],[f1721,f6]) ).
fof(f2686,plain,
! [X0,X1] : rd(mult(X1,mult(X0,X1)),X1) = ld(rd(unit,X1),X0),
inference(superposition,[],[f2587,f4]) ).
fof(f2712,plain,
! [X2,X0,X1] : rd(mult(X2,mult(mult(X0,X1),X2)),mult(X1,X2)) = ld(rd(unit,X2),X0),
inference(backward_demodulation,[],[f881,f2686]) ).
fof(f2754,plain,
! [X2,X0,X1] : ld(X1,X0) = mult(ld(X1,X2),ld(X1,ld(rd(X2,X1),X0))),
inference(superposition,[],[f830,f1]) ).
fof(f2845,plain,
! [X2,X0,X1] : rd(X0,ld(X1,X2)) = mult(rd(rd(X0,X1),rd(X2,X1)),X1),
inference(superposition,[],[f383,f3]) ).
fof(f2849,plain,
! [X0,X1] : mult(rd(unit,rd(X1,X0)),X0) = rd(X0,ld(X0,X1)),
inference(superposition,[],[f383,f6]) ).
fof(f2861,plain,
! [X2,X0,X1] : rd(mult(X1,X2),X0) = mult(rd(X1,rd(mult(X2,X0),X2)),X2),
inference(superposition,[],[f383,f2]) ).
fof(f2975,plain,
! [X2,X0,X1] : rd(X0,rd(mult(X1,X2),X1)) = rd(rd(mult(X0,X1),X2),X1),
inference(superposition,[],[f4,f2861]) ).
fof(f3118,plain,
! [X0,X1] : mult(mult(X0,mult(op_c,ld(X0,X1))),mult(X0,op_d)) = mult(mult(X0,unit),ld(mult(X0,op_d),mult(X1,mult(X0,op_d)))),
inference(superposition,[],[f65,f10]) ).
fof(f3243,plain,
! [X0,X1] : mult(mult(X0,mult(op_c,ld(X0,X1))),mult(X0,op_d)) = mult(X0,ld(mult(X0,op_d),mult(X1,mult(X0,op_d)))),
inference(forward_demodulation,[],[f3118,f5]) ).
fof(f3348,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X1,X0)),X0) = mult(rd(X2,X0),ld(rd(unit,X0),X1)),
inference(superposition,[],[f1602,f2686]) ).
fof(f3356,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,mult(X1,X0))),mult(X2,X0)) = rd(mult(X2,ld(rd(unit,X0),X1)),X2),
inference(superposition,[],[f945,f2686]) ).
fof(f3361,plain,
! [X2,X0,X1] : rd(mult(mult(rd(mult(X0,X1),X0),mult(X2,rd(mult(X0,X1),X0))),X0),X1) = mult(ld(rd(unit,rd(mult(X0,X1),X0)),X2),X0),
inference(superposition,[],[f2861,f2686]) ).
fof(f3363,plain,
! [X0] : ld(rd(unit,op_c),X0) = mult(op_c,mult(mult(X0,op_c),op_d)),
inference(superposition,[],[f16,f2686]) ).
fof(f3371,plain,
! [X2,X0,X1] : mult(ld(rd(unit,rd(mult(X0,X1),X0)),X2),X0) = rd(mult(mult(rd(mult(X0,X1),X0),X0),ld(X0,mult(mult(X2,X0),X1))),X1),
inference(forward_demodulation,[],[f3361,f1627]) ).
fof(f3373,plain,
! [X2,X0,X1] : rd(mult(X2,mult(X0,mult(X1,X0))),mult(X2,X0)) = ld(rd(rd(unit,X0),X2),rd(X1,X2)),
inference(forward_demodulation,[],[f3356,f2569]) ).
fof(f3411,plain,
! [X2,X0,X1] : mult(ld(rd(unit,rd(mult(X0,X1),X0)),X2),X0) = rd(mult(mult(X0,X1),ld(X0,mult(mult(X2,X0),X1))),X1),
inference(forward_demodulation,[],[f3371,f3]) ).
fof(f3431,plain,
! [X2,X0,X1] : mult(ld(rd(unit,rd(mult(X0,X1),X0)),X2),X0) = mult(X0,rd(mult(X1,ld(X0,mult(mult(X2,X0),X1))),X1)),
inference(forward_demodulation,[],[f3411,f1503]) ).
fof(f3443,plain,
! [X2,X0,X1] : mult(ld(rd(unit,rd(mult(X0,X1),X0)),X2),X0) = mult(X0,ld(rd(X0,X1),rd(mult(mult(X2,X0),X1),X1))),
inference(forward_demodulation,[],[f3431,f2569]) ).
fof(f3449,plain,
! [X2,X0,X1] : mult(ld(rd(unit,rd(mult(X0,X1),X0)),X2),X0) = mult(X0,ld(rd(X0,X1),mult(X2,X0))),
inference(forward_demodulation,[],[f3443,f4]) ).
fof(f3484,plain,
! [X0,X1] : rd(mult(X0,X1),X0) = ld(rd(rd(X0,X1),X0),unit),
inference(superposition,[],[f2583,f130]) ).
fof(f3664,plain,
! [X0,X1] : mult(X1,ld(X0,unit)) = ld(X0,rd(mult(X0,X1),X0)),
inference(superposition,[],[f2,f598]) ).
fof(f3696,plain,
! [X0] : mult(mult(X0,ld(op_c,unit)),op_d) = mult(op_d,mult(rd(mult(op_c,X0),op_c),op_d)),
inference(superposition,[],[f1112,f598]) ).
fof(f3703,plain,
! [X0] : mult(mult(X0,ld(op_c,unit)),op_d) = mult(op_d,mult(op_c,mult(X0,ld(op_c,op_d)))),
inference(forward_demodulation,[],[f3696,f55]) ).
fof(f3744,plain,
! [X0] : mult(mult(X0,op_d),mult(unit,op_d)) = mult(op_d,mult(op_c,mult(X0,ld(op_c,op_d)))),
inference(forward_demodulation,[],[f3703,f1341]) ).
fof(f3777,plain,
! [X0] : mult(mult(X0,op_d),op_d) = mult(op_d,mult(op_c,mult(X0,ld(op_c,op_d)))),
inference(forward_demodulation,[],[f3744,f6]) ).
fof(f3963,plain,
! [X0,X1] : mult(mult(op_c,X1),X0) = mult(op_c,mult(rd(X1,op_d),ld(op_c,X0))),
inference(superposition,[],[f2314,f1]) ).
fof(f3967,plain,
! [X0] : mult(mult(op_c,X0),op_c) = mult(op_c,mult(rd(X0,op_d),unit)),
inference(superposition,[],[f2314,f5]) ).
fof(f4022,plain,
! [X0] : mult(op_c,rd(X0,op_d)) = mult(mult(op_c,X0),op_c),
inference(forward_demodulation,[],[f3967,f5]) ).
fof(f4082,plain,
! [X0,X1] : mult(mult(X1,mult(op_c,X0)),op_c) = mult(mult(X1,op_c),ld(op_c,mult(op_c,rd(X0,op_d)))),
inference(superposition,[],[f8,f4022]) ).
fof(f4110,plain,
! [X0,X1] : mult(mult(X1,mult(op_c,X0)),op_c) = mult(mult(X1,op_c),rd(X0,op_d)),
inference(forward_demodulation,[],[f4082,f2]) ).
fof(f4672,plain,
! [X0,X1] : mult(rd(unit,X0),rd(X1,X0)) = rd(ld(X0,X1),X0),
inference(superposition,[],[f1490,f6]) ).
fof(f4784,plain,
! [X0] : mult(op_d,mult(op_c,X0)) = mult(mult(rd(X0,ld(op_c,op_d)),op_d),op_d),
inference(superposition,[],[f3777,f3]) ).
fof(f4863,plain,
! [X2,X0,X1] : mult(X1,ld(ld(X1,mult(X0,X1)),X2)) = ld(X0,mult(X1,X2)),
inference(superposition,[],[f673,f4]) ).
fof(f4881,plain,
! [X0,X1] : mult(X0,ld(ld(X0,X1),unit)) = ld(rd(X1,X0),X0),
inference(superposition,[],[f673,f5]) ).
fof(f5220,plain,
! [X2,X0,X1] : ld(ld(X1,mult(X0,X1)),X2) = ld(X1,ld(X0,mult(X1,X2))),
inference(superposition,[],[f2,f4863]) ).
fof(f5562,plain,
! [X0] : ld(ld(op_d,unit),X0) = ld(op_d,ld(op_c,mult(op_d,X0))),
inference(superposition,[],[f5220,f10]) ).
fof(f5645,plain,
! [X0] : ld(ld(op_d,unit),X0) = mult(mult(mult(op_d,X0),op_c),op_d),
inference(forward_demodulation,[],[f5562,f1178]) ).
fof(f6279,plain,
! [X2,X0,X1] : rd(rd(X0,X1),rd(X2,X1)) = rd(rd(X0,ld(X1,X2)),X1),
inference(superposition,[],[f4,f2845]) ).
fof(f6418,plain,
! [X2,X0,X1] : mult(X1,ld(mult(X0,X1),X2)) = mult(ld(X0,rd(X2,X1)),X1),
inference(superposition,[],[f1,f511]) ).
fof(f6421,plain,
! [X2,X3,X0,X1] : mult(rd(X3,rd(mult(ld(X0,rd(X2,X1)),X1),X1)),X1) = rd(mult(X3,X1),ld(mult(X0,X1),X2)),
inference(superposition,[],[f383,f511]) ).
fof(f6438,plain,
! [X0,X1] : rd(ld(mult(X0,op_d),X1),op_d) = mult(op_c,rd(mult(ld(X0,rd(X1,op_d)),op_d),op_d)),
inference(superposition,[],[f1539,f511]) ).
fof(f6439,plain,
! [X0,X1] : rd(ld(mult(X0,op_d),X1),op_d) = mult(op_c,ld(X0,rd(X1,op_d))),
inference(forward_demodulation,[],[f6438,f4]) ).
fof(f6445,plain,
! [X2,X3,X0,X1] : rd(mult(X3,X1),ld(mult(X0,X1),X2)) = mult(rd(X3,ld(X0,rd(X2,X1))),X1),
inference(forward_demodulation,[],[f6421,f4]) ).
fof(f6569,plain,
! [X0] : mult(ld(X0,op_c),op_d) = mult(op_d,ld(mult(X0,op_d),unit)),
inference(superposition,[],[f6418,f131]) ).
fof(f7666,plain,
! [X0,X1] : rd(unit,rd(mult(X0,X1),X0)) = rd(rd(X0,X1),X0),
inference(superposition,[],[f127,f3484]) ).
fof(f7681,plain,
! [X2,X0,X1] : mult(X0,ld(rd(X0,X1),mult(X2,X0))) = mult(ld(rd(rd(X0,X1),X0),X2),X0),
inference(backward_demodulation,[],[f3449,f7666]) ).
fof(f7965,plain,
! [X2,X0,X1] : ld(X0,mult(rd(X1,mult(X0,X2)),X0)) = rd(ld(X0,X1),X2),
inference(superposition,[],[f4,f793]) ).
fof(f8486,plain,
! [X0,X1] : ld(op_c,rd(ld(X0,X1),op_d)) = ld(rd(X0,op_d),rd(X1,op_d)),
inference(superposition,[],[f1200,f2569]) ).
fof(f8792,plain,
! [X2,X0,X1] : ld(ld(rd(unit,X0),X1),X2) = mult(X0,ld(mult(X1,X0),ld(X0,X2))),
inference(superposition,[],[f689,f2686]) ).
fof(f8793,plain,
! [X2,X3,X0,X1] : mult(X0,ld(rd(X1,X2),ld(X0,X3))) = ld(rd(mult(X0,X1),mult(X0,X2)),X3),
inference(superposition,[],[f689,f945]) ).
fof(f9251,plain,
! [X0] : rd(rd(unit,X0),op_d) = rd(op_c,rd(mult(op_d,X0),op_d)),
inference(superposition,[],[f2975,f10]) ).
fof(f9272,plain,
! [X0] : rd(op_d,rd(mult(X0,op_d),X0)) = rd(ld(op_c,rd(X0,op_d)),X0),
inference(superposition,[],[f2975,f1200]) ).
fof(f9304,plain,
! [X0] : rd(X0,rd(mult(op_c,op_d),op_c)) = mult(op_c,mult(op_d,mult(X0,op_c))),
inference(superposition,[],[f1217,f2975]) ).
fof(f9311,plain,
! [X0] : rd(X0,mult(op_c,mult(op_d,op_d))) = mult(op_c,mult(op_d,mult(X0,op_c))),
inference(forward_demodulation,[],[f9304,f16]) ).
fof(f9334,plain,
! [X0] : rd(rd(unit,X0),op_d) = rd(op_c,ld(op_c,rd(X0,op_d))),
inference(forward_demodulation,[],[f9251,f1200]) ).
fof(f9355,plain,
! [X0] : rd(X0,rd(unit,op_c)) = mult(op_c,mult(op_d,mult(X0,op_c))),
inference(forward_demodulation,[],[f9311,f152]) ).
fof(f9978,plain,
! [X2,X0,X1] : mult(ld(rd(X0,X1),X2),X1) = mult(X1,ld(X0,mult(X2,X1))),
inference(superposition,[],[f7681,f127]) ).
fof(f10125,plain,
! [X2,X0,X1] : mult(rd(X2,rd(X0,X1)),X0) = mult(rd(X0,X1),mult(X1,ld(X0,mult(X2,X1)))),
inference(backward_demodulation,[],[f137,f9978]) ).
fof(f10167,plain,
! [X2,X0,X1] : mult(rd(X2,rd(X0,X1)),X0) = mult(X1,mult(ld(X1,X0),ld(X0,mult(X2,X1)))),
inference(forward_demodulation,[],[f10125,f56]) ).
fof(f10259,plain,
! [X2,X3,X0,X1] : mult(ld(rd(X1,X0),X2),mult(X0,X3)) = mult(X0,mult(ld(X0,mult(X0,ld(X1,mult(X2,X0)))),X3)),
inference(superposition,[],[f132,f9978]) ).
fof(f10327,plain,
! [X2,X3,X0,X1] : mult(ld(rd(X1,X0),X2),mult(X0,X3)) = mult(X0,mult(ld(X1,mult(X2,X0)),X3)),
inference(forward_demodulation,[],[f10259,f2]) ).
fof(f10722,plain,
! [X0,X1] : mult(rd(unit,X1),X0) = rd(ld(X1,mult(X0,X1)),X1),
inference(superposition,[],[f4672,f4]) ).
fof(f10744,plain,
! [X0,X1] : rd(mult(rd(unit,X0),X1),mult(rd(unit,X0),X0)) = rd(rd(ld(X0,X1),X0),rd(unit,X0)),
inference(superposition,[],[f945,f4672]) ).
fof(f10753,plain,
! [X2,X0,X1] : mult(rd(unit,X0),mult(rd(X1,X0),ld(rd(unit,X0),X2))) = mult(rd(rd(ld(X0,X1),X0),rd(unit,X0)),X2),
inference(superposition,[],[f55,f4672]) ).
fof(f10787,plain,
! [X2,X0,X1] : mult(rd(rd(ld(X0,X1),X0),rd(unit,X0)),X2) = mult(rd(unit,X0),rd(mult(X1,mult(X2,X0)),X0)),
inference(forward_demodulation,[],[f10753,f3348]) ).
fof(f10792,plain,
! [X0,X1] : rd(rd(ld(X0,X1),X0),rd(unit,X0)) = rd(mult(rd(unit,X0),X1),unit),
inference(forward_demodulation,[],[f10744,f3]) ).
fof(f10826,plain,
! [X2,X0,X1] : mult(rd(rd(ld(X0,X1),X0),rd(unit,X0)),X2) = rd(ld(X0,mult(X1,mult(X2,X0))),X0),
inference(forward_demodulation,[],[f10787,f4672]) ).
fof(f10829,plain,
! [X0,X1] : mult(rd(unit,X0),X1) = rd(rd(ld(X0,X1),X0),rd(unit,X0)),
inference(forward_demodulation,[],[f10792,f109]) ).
fof(f10856,plain,
! [X2,X0,X1] : mult(mult(rd(unit,X0),X1),X2) = rd(ld(X0,mult(X1,mult(X2,X0))),X0),
inference(backward_demodulation,[],[f10826,f10829]) ).
fof(f11147,plain,
! [X2,X0,X1] : ld(X1,mult(rd(X0,X2),X1)) = rd(ld(X1,X0),ld(X1,X2)),
inference(superposition,[],[f845,f3]) ).
fof(f11589,plain,
! [X2,X0,X1] : mult(X0,mult(mult(X1,X2),X0)) = mult(ld(rd(unit,X0),X1),mult(X2,X0)),
inference(superposition,[],[f3,f2712]) ).
fof(f12158,plain,
! [X2,X0,X1] : rd(X0,ld(X1,X2)) = ld(X1,mult(rd(mult(X1,X0),X2),X1)),
inference(superposition,[],[f11147,f2]) ).
fof(f12428,plain,
! [X0,X1] : ld(X0,mult(mult(X0,X1),X0)) = rd(X1,ld(X0,unit)),
inference(superposition,[],[f12158,f109]) ).
fof(f12787,plain,
! [X2,X0,X1] : mult(rd(rd(X2,X1),mult(X1,X0)),X1) = rd(X2,rd(X0,ld(X1,unit))),
inference(superposition,[],[f373,f12428]) ).
fof(f12788,plain,
! [X2,X0,X1] : ld(X1,mult(mult(X1,X0),X2)) = mult(rd(X0,ld(X1,unit)),ld(X1,X2)),
inference(superposition,[],[f777,f12428]) ).
fof(f12790,plain,
! [X0,X1] : mult(rd(unit,X1),mult(X1,X0)) = rd(rd(X0,ld(X1,unit)),X1),
inference(superposition,[],[f10722,f12428]) ).
fof(f12844,plain,
! [X0,X1] : rd(rd(X0,X1),rd(unit,X1)) = mult(rd(unit,X1),mult(X1,X0)),
inference(forward_demodulation,[],[f12790,f6279]) ).
fof(f12913,plain,
! [X0,X1] : rd(rd(X0,X1),rd(unit,X1)) = mult(X1,mult(ld(X1,unit),X0)),
inference(forward_demodulation,[],[f12844,f56]) ).
fof(f13833,plain,
! [X0] : ld(rd(mult(X0,op_d),op_d),op_d) = mult(op_d,ld(mult(mult(op_c,X0),op_d),unit)),
inference(superposition,[],[f4881,f25]) ).
fof(f13947,plain,
! [X0] : ld(rd(mult(X0,op_d),op_d),op_d) = mult(ld(mult(op_c,X0),op_c),op_d),
inference(forward_demodulation,[],[f13833,f6569]) ).
fof(f13999,plain,
! [X0] : ld(X0,op_d) = mult(ld(mult(op_c,X0),op_c),op_d),
inference(forward_demodulation,[],[f13947,f4]) ).
fof(f14668,plain,
! [X0,X1] : mult(rd(X1,rd(X1,X0)),X1) = mult(X0,mult(ld(X0,X1),X0)),
inference(superposition,[],[f10167,f2]) ).
fof(f14680,plain,
! [X0,X1] : mult(rd(X0,rd(unit,X1)),unit) = mult(X1,mult(ld(X1,unit),mult(X0,X1))),
inference(superposition,[],[f10167,f38]) ).
fof(f14784,plain,
! [X0,X1] : rd(X0,rd(unit,X1)) = mult(X1,mult(ld(X1,unit),mult(X0,X1))),
inference(forward_demodulation,[],[f14680,f5]) ).
fof(f15448,plain,
! [X2,X3,X0,X1] : mult(rd(X1,mult(X0,X2)),mult(X0,X3)) = mult(X0,mult(rd(ld(X0,X1),X2),X3)),
inference(superposition,[],[f132,f7965]) ).
fof(f15455,plain,
! [X2,X0,X1] : mult(rd(X1,mult(X0,X2)),X0) = mult(X0,rd(ld(X0,X1),X2)),
inference(superposition,[],[f1,f7965]) ).
fof(f15536,plain,
! [X2,X0,X1] : rd(X2,rd(X0,ld(X1,unit))) = mult(X1,rd(ld(X1,rd(X2,X1)),X0)),
inference(backward_demodulation,[],[f12787,f15455]) ).
fof(f15552,plain,
! [X0] : rd(rd(X0,op_d),X0) = mult(op_c,rd(ld(op_c,rd(X0,op_d)),X0)),
inference(backward_demodulation,[],[f2526,f15455]) ).
fof(f15687,plain,
! [X0] : rd(rd(X0,op_d),X0) = mult(op_c,rd(op_d,rd(mult(X0,op_d),X0))),
inference(forward_demodulation,[],[f15552,f9272]) ).
fof(f16742,plain,
! [X0] : rd(op_c,ld(op_c,rd(X0,op_d))) = mult(rd(unit,mult(op_c,mult(op_d,X0))),op_c),
inference(superposition,[],[f2849,f1217]) ).
fof(f16744,plain,
mult(rd(unit,op_c),op_d) = rd(op_d,ld(op_d,unit)),
inference(superposition,[],[f2849,f131]) ).
fof(f16842,plain,
! [X0] : rd(op_c,ld(op_c,rd(X0,op_d))) = mult(op_c,rd(ld(op_c,unit),mult(op_d,X0))),
inference(forward_demodulation,[],[f16742,f15455]) ).
fof(f16873,plain,
! [X0] : rd(op_c,ld(op_c,rd(X0,op_d))) = mult(op_c,rd(op_d,mult(op_d,X0))),
inference(forward_demodulation,[],[f16842,f39]) ).
fof(f16893,plain,
! [X0] : rd(rd(unit,X0),op_d) = mult(op_c,rd(op_d,mult(op_d,X0))),
inference(forward_demodulation,[],[f16873,f9334]) ).
fof(f17139,plain,
! [X2,X0,X1] : rd(mult(X2,rd(rd(X0,X1),X0)),X2) = rd(mult(X2,unit),mult(X2,rd(mult(X0,X1),X0))),
inference(superposition,[],[f705,f3484]) ).
fof(f17238,plain,
! [X2,X0,X1] : rd(mult(X2,rd(rd(X0,X1),X0)),X2) = rd(X2,mult(X2,rd(mult(X0,X1),X0))),
inference(forward_demodulation,[],[f17139,f5]) ).
fof(f17335,plain,
! [X2,X0,X1] : rd(X2,mult(X2,rd(mult(X0,X1),X0))) = rd(mult(X2,rd(X0,X1)),mult(X2,X0)),
inference(forward_demodulation,[],[f17238,f945]) ).
fof(f17705,plain,
! [X0] : rd(X0,ld(op_c,ld(op_d,unit))) = mult(rd(rd(X0,op_c),mult(op_c,rd(unit,op_c))),op_c),
inference(superposition,[],[f2845,f1658]) ).
fof(f17716,plain,
! [X0] : rd(X0,ld(op_c,ld(op_d,unit))) = mult(op_c,rd(ld(op_c,rd(X0,op_c)),rd(unit,op_c))),
inference(forward_demodulation,[],[f17705,f15455]) ).
fof(f17732,plain,
! [X0] : rd(X0,ld(op_c,ld(op_d,unit))) = rd(X0,rd(rd(unit,op_c),ld(op_c,unit))),
inference(forward_demodulation,[],[f17716,f15536]) ).
fof(f17740,plain,
! [X0] : rd(X0,ld(op_c,ld(op_d,unit))) = rd(X0,rd(rd(unit,op_c),op_d)),
inference(forward_demodulation,[],[f17732,f39]) ).
fof(f19196,plain,
rd(rd(op_c,op_d),op_c) = mult(op_c,rd(op_d,rd(unit,op_c))),
inference(superposition,[],[f15687,f10]) ).
fof(f19310,plain,
mult(op_c,mult(op_d,op_c)) = mult(op_c,rd(op_d,rd(unit,op_c))),
inference(forward_demodulation,[],[f19196,f1217]) ).
fof(f19393,plain,
ld(rd(op_d,rd(unit,op_c)),op_d) = mult(ld(mult(op_c,mult(op_d,op_c)),op_c),op_d),
inference(superposition,[],[f13999,f19310]) ).
fof(f19396,plain,
rd(op_d,rd(unit,op_c)) = ld(op_c,mult(op_c,mult(op_d,op_c))),
inference(superposition,[],[f2,f19310]) ).
fof(f19420,plain,
ld(rd(unit,rd(op_d,rd(unit,op_c))),op_c) = rd(mult(rd(op_d,rd(unit,op_c)),mult(op_c,mult(op_d,op_c))),rd(op_d,rd(unit,op_c))),
inference(superposition,[],[f2686,f19310]) ).
fof(f19437,plain,
ld(rd(unit,rd(op_d,rd(unit,op_c))),op_c) = rd(mult(rd(op_d,rd(unit,op_c)),rd(op_c,op_d)),mult(rd(op_d,rd(unit,op_c)),op_c)),
inference(forward_demodulation,[],[f19420,f1321]) ).
fof(f19450,plain,
mult(op_d,op_c) = rd(op_d,rd(unit,op_c)),
inference(forward_demodulation,[],[f19396,f2]) ).
fof(f19453,plain,
ld(rd(op_d,rd(unit,op_c)),op_d) = ld(mult(op_d,op_c),op_d),
inference(forward_demodulation,[],[f19393,f13999]) ).
fof(f19468,plain,
ld(rd(unit,rd(op_d,rd(unit,op_c))),op_c) = rd(rd(op_d,rd(unit,op_c)),mult(rd(op_d,rd(unit,op_c)),rd(mult(op_c,op_d),op_c))),
inference(forward_demodulation,[],[f19437,f17335]) ).
fof(f19500,plain,
rd(unit,op_c) = ld(mult(op_d,op_c),op_d),
inference(forward_demodulation,[],[f19453,f106]) ).
fof(f19511,plain,
ld(rd(unit,rd(op_d,rd(unit,op_c))),op_c) = rd(rd(op_d,rd(unit,op_c)),mult(rd(op_d,rd(unit,op_c)),mult(op_c,mult(op_d,op_d)))),
inference(forward_demodulation,[],[f19468,f16]) ).
fof(f19534,plain,
ld(rd(unit,rd(op_d,rd(unit,op_c))),op_c) = rd(rd(op_d,rd(unit,op_c)),mult(rd(op_d,rd(unit,op_c)),rd(unit,op_c))),
inference(forward_demodulation,[],[f19511,f152]) ).
fof(f19544,plain,
rd(rd(op_d,rd(unit,op_c)),op_d) = ld(rd(unit,rd(op_d,rd(unit,op_c))),op_c),
inference(forward_demodulation,[],[f19534,f3]) ).
fof(f19552,plain,
rd(mult(op_d,op_c),op_d) = ld(rd(unit,mult(op_d,op_c)),op_c),
inference(forward_demodulation,[],[f19544,f19450]) ).
fof(f19555,plain,
rd(op_d,mult(op_d,op_d)) = ld(rd(unit,mult(op_d,op_c)),op_c),
inference(forward_demodulation,[],[f19552,f994]) ).
fof(f19557,plain,
ld(op_c,rd(op_c,op_d)) = ld(rd(unit,mult(op_d,op_c)),op_c),
inference(forward_demodulation,[],[f19555,f1284]) ).
fof(f19559,plain,
mult(op_d,op_c) = mult(mult(mult(op_d,op_c),op_c),ld(op_c,unit)),
inference(superposition,[],[f167,f19450]) ).
fof(f19596,plain,
mult(op_d,op_c) = mult(mult(mult(op_d,op_c),op_c),op_d),
inference(forward_demodulation,[],[f19559,f39]) ).
fof(f19605,plain,
mult(op_d,op_c) = ld(ld(op_d,unit),op_c),
inference(forward_demodulation,[],[f19596,f5645]) ).
fof(f19617,plain,
ld(op_d,unit) = rd(op_c,mult(op_d,op_c)),
inference(superposition,[],[f127,f19605]) ).
fof(f19624,plain,
! [X0] : ld(ld(op_d,unit),mult(X0,op_c)) = mult(ld(ld(op_d,unit),mult(X0,ld(op_d,unit))),mult(op_d,op_c)),
inference(superposition,[],[f777,f19605]) ).
fof(f19649,plain,
! [X0] : ld(ld(op_d,unit),mult(X0,op_c)) = mult(ld(unit,mult(mult(op_d,X0),ld(op_d,unit))),mult(op_d,op_c)),
inference(forward_demodulation,[],[f19624,f72]) ).
fof(f19659,plain,
! [X0] : ld(ld(op_d,unit),mult(X0,op_c)) = mult(mult(mult(op_d,X0),ld(op_d,unit)),mult(op_d,op_c)),
inference(forward_demodulation,[],[f19649,f38]) ).
fof(f19785,plain,
rd(mult(op_d,op_c),ld(mult(op_d,op_c),op_c)) = mult(rd(unit,ld(op_d,unit)),mult(op_d,op_c)),
inference(superposition,[],[f2849,f19617]) ).
fof(f19791,plain,
mult(op_d,mult(op_d,op_c)) = rd(mult(op_d,op_c),ld(mult(op_d,op_c),op_c)),
inference(forward_demodulation,[],[f19785,f127]) ).
fof(f19799,plain,
mult(op_d,mult(op_d,op_c)) = mult(rd(op_d,ld(op_d,rd(op_c,op_c))),op_c),
inference(forward_demodulation,[],[f19791,f6445]) ).
fof(f19801,plain,
mult(op_d,mult(op_d,op_c)) = mult(rd(op_d,ld(op_d,unit)),op_c),
inference(forward_demodulation,[],[f19799,f130]) ).
fof(f19802,plain,
mult(op_d,mult(op_d,op_c)) = mult(mult(rd(unit,op_c),op_d),op_c),
inference(forward_demodulation,[],[f19801,f16744]) ).
fof(f19803,plain,
mult(op_d,mult(op_d,op_c)) = mult(unit,ld(op_c,mult(op_d,op_c))),
inference(forward_demodulation,[],[f19802,f108]) ).
fof(f19804,plain,
mult(op_d,mult(op_d,op_c)) = ld(op_c,mult(op_d,op_c)),
inference(forward_demodulation,[],[f19803,f6]) ).
fof(f20631,plain,
! [X0,X1] : mult(X1,ld(mult(X1,op_d),mult(mult(X1,X0),mult(X1,op_d)))) = mult(mult(X1,mult(op_c,X0)),mult(X1,op_d)),
inference(superposition,[],[f3243,f2]) ).
fof(f21078,plain,
! [X0] : ld(op_c,rd(ld(mult(op_d,op_d),mult(mult(op_d,X0),mult(op_d,op_d))),op_d)) = rd(mult(mult(op_d,mult(op_c,X0)),mult(op_d,op_d)),op_d),
inference(superposition,[],[f1200,f20631]) ).
fof(f21079,plain,
! [X0] : ld(op_c,rd(ld(mult(op_d,op_d),mult(mult(op_d,X0),mult(op_d,op_d))),op_d)) = mult(rd(mult(op_d,mult(op_c,X0)),op_d),ld(op_c,op_d)),
inference(forward_demodulation,[],[f21078,f2381]) ).
fof(f21183,plain,
! [X0] : ld(op_c,rd(ld(mult(op_d,op_d),mult(mult(op_d,X0),mult(op_d,op_d))),op_d)) = mult(op_d,mult(mult(op_c,X0),ld(op_d,ld(op_c,op_d)))),
inference(forward_demodulation,[],[f21079,f55]) ).
fof(f21272,plain,
! [X0] : ld(op_c,rd(ld(mult(op_d,op_d),mult(mult(op_d,X0),mult(op_d,op_d))),op_d)) = mult(op_d,mult(mult(op_c,X0),mult(mult(op_d,op_c),op_d))),
inference(forward_demodulation,[],[f21183,f1178]) ).
fof(f21365,plain,
! [X0] : mult(op_d,mult(mult(op_c,X0),mult(mult(op_d,op_c),op_d))) = ld(op_c,mult(op_c,ld(op_d,rd(mult(mult(op_d,X0),mult(op_d,op_d)),op_d)))),
inference(forward_demodulation,[],[f21272,f6439]) ).
fof(f21413,plain,
! [X0] : mult(op_d,mult(mult(op_c,X0),mult(mult(op_d,op_c),op_d))) = ld(op_d,rd(mult(mult(op_d,X0),mult(op_d,op_d)),op_d)),
inference(forward_demodulation,[],[f21365,f2]) ).
fof(f21448,plain,
! [X0] : mult(op_d,mult(mult(op_c,X0),mult(mult(op_d,op_c),op_d))) = ld(op_d,mult(rd(mult(op_d,X0),op_d),ld(op_c,op_d))),
inference(forward_demodulation,[],[f21413,f2381]) ).
fof(f21468,plain,
! [X0] : mult(op_d,mult(mult(op_c,X0),mult(mult(op_d,op_c),op_d))) = mult(ld(op_d,mult(op_d,X0)),ld(op_d,ld(op_c,op_d))),
inference(forward_demodulation,[],[f21448,f830]) ).
fof(f21483,plain,
! [X0] : mult(op_d,mult(mult(op_c,X0),mult(mult(op_d,op_c),op_d))) = mult(ld(op_d,mult(op_d,X0)),mult(mult(op_d,op_c),op_d)),
inference(forward_demodulation,[],[f21468,f1178]) ).
fof(f21491,plain,
! [X0] : mult(X0,mult(mult(op_d,op_c),op_d)) = mult(op_d,mult(mult(op_c,X0),mult(mult(op_d,op_c),op_d))),
inference(forward_demodulation,[],[f21483,f2]) ).
fof(f21507,plain,
! [X0] : mult(op_d,mult(X0,mult(mult(op_d,op_c),op_d))) = mult(ld(op_c,X0),mult(mult(op_d,op_c),op_d)),
inference(superposition,[],[f21491,f1]) ).
fof(f21594,plain,
! [X0] : mult(op_d,mult(X0,mult(mult(op_d,op_c),op_d))) = mult(op_d,mult(mult(X0,mult(op_d,op_c)),op_d)),
inference(forward_demodulation,[],[f21507,f2080]) ).
fof(f21679,plain,
! [X0] : mult(mult(X0,mult(op_d,op_c)),op_d) = ld(op_d,mult(op_d,mult(X0,mult(mult(op_d,op_c),op_d)))),
inference(superposition,[],[f2,f21594]) ).
fof(f21730,plain,
! [X0] : mult(X0,mult(mult(op_d,op_c),op_d)) = mult(mult(X0,mult(op_d,op_c)),op_d),
inference(forward_demodulation,[],[f21679,f2]) ).
fof(f21884,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = rd(mult(X0,mult(mult(op_d,op_c),op_d)),op_d),
inference(superposition,[],[f4,f21730]) ).
fof(f21913,plain,
! [X0] : mult(rd(unit,op_d),mult(X0,mult(op_d,op_c))) = rd(ld(op_d,mult(X0,mult(mult(op_d,op_c),op_d))),op_d),
inference(superposition,[],[f10722,f21730]) ).
fof(f21921,plain,
! [X0] : mult(rd(unit,op_d),mult(X0,mult(op_d,op_c))) = mult(op_c,rd(mult(X0,mult(mult(op_d,op_c),op_d)),op_d)),
inference(forward_demodulation,[],[f21913,f1539]) ).
fof(f21937,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(rd(X0,op_d),ld(op_c,mult(op_d,op_c))),
inference(forward_demodulation,[],[f21884,f2381]) ).
fof(f21969,plain,
! [X0] : mult(op_c,mult(rd(X0,op_d),ld(op_c,mult(op_d,op_c)))) = mult(rd(unit,op_d),mult(X0,mult(op_d,op_c))),
inference(forward_demodulation,[],[f21921,f2381]) ).
fof(f21987,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(rd(X0,op_d),mult(op_d,mult(op_d,op_c))),
inference(forward_demodulation,[],[f21937,f19804]) ).
fof(f22009,plain,
! [X0] : mult(op_c,mult(X0,mult(op_d,op_c))) = mult(op_c,mult(rd(X0,op_d),ld(op_c,mult(op_d,op_c)))),
inference(forward_demodulation,[],[f21969,f131]) ).
fof(f22034,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(op_d,mult(ld(op_d,X0),mult(op_d,op_c))),
inference(forward_demodulation,[],[f21987,f56]) ).
fof(f22041,plain,
! [X0] : mult(op_c,mult(X0,mult(op_d,op_c))) = mult(mult(op_c,X0),mult(op_d,op_c)),
inference(forward_demodulation,[],[f22009,f3963]) ).
fof(f22121,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(op_c,mult(ld(op_c,X0),mult(op_d,op_c))),
inference(superposition,[],[f22041,f1]) ).
fof(f22141,plain,
! [X0] : mult(op_c,X0) = rd(mult(op_c,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)),
inference(superposition,[],[f4,f22041]) ).
fof(f22196,plain,
! [X0] : mult(op_c,mult(op_d,mult(mult(X0,op_d),op_c))) = mult(X0,mult(op_d,op_c)),
inference(forward_demodulation,[],[f22121,f1419]) ).
fof(f22214,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = rd(mult(X0,op_d),rd(unit,op_c)),
inference(forward_demodulation,[],[f22196,f9355]) ).
fof(f22241,plain,
! [X0] : rd(X0,rd(unit,op_c)) = mult(rd(X0,op_d),mult(op_d,op_c)),
inference(superposition,[],[f22214,f3]) ).
fof(f22319,plain,
! [X0] : rd(X0,rd(unit,op_c)) = mult(op_d,mult(ld(op_d,X0),op_c)),
inference(forward_demodulation,[],[f22241,f56]) ).
fof(f22370,plain,
! [X0] : mult(op_d,mult(X0,mult(op_d,op_c))) = mult(mult(op_d,X0),mult(op_d,op_c)),
inference(superposition,[],[f22034,f2]) ).
fof(f22532,plain,
! [X0] : mult(ld(op_d,mult(mult(op_d,X0),op_d)),op_c) = ld(op_d,mult(op_d,mult(X0,mult(op_d,op_c)))),
inference(superposition,[],[f464,f22370]) ).
fof(f22566,plain,
! [X0] : mult(rd(unit,mult(op_d,op_c)),mult(op_d,X0)) = rd(ld(mult(op_d,op_c),mult(op_d,mult(X0,mult(op_d,op_c)))),mult(op_d,op_c)),
inference(superposition,[],[f10722,f22370]) ).
fof(f22573,plain,
! [X0] : mult(rd(unit,mult(op_d,op_c)),mult(op_d,X0)) = mult(mult(rd(unit,mult(op_d,op_c)),op_d),X0),
inference(forward_demodulation,[],[f22566,f10856]) ).
fof(f22585,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(ld(op_d,mult(mult(op_d,X0),op_d)),op_c),
inference(forward_demodulation,[],[f22532,f2]) ).
fof(f22604,plain,
! [X0] : mult(rd(unit,mult(op_d,op_c)),mult(op_d,X0)) = mult(mult(op_d,rd(ld(op_d,unit),op_c)),X0),
inference(forward_demodulation,[],[f22573,f15455]) ).
fof(f22611,plain,
! [X0] : mult(rd(X0,ld(op_d,unit)),op_c) = mult(X0,mult(op_d,op_c)),
inference(forward_demodulation,[],[f22585,f12428]) ).
fof(f22619,plain,
! [X0] : mult(rd(unit,mult(op_d,op_c)),mult(op_d,X0)) = mult(mult(op_d,mult(op_c,rd(unit,op_c))),X0),
inference(forward_demodulation,[],[f22604,f1658]) ).
fof(f22626,plain,
! [X0] : mult(mult(op_d,mult(op_c,rd(unit,op_c))),X0) = mult(op_d,mult(rd(ld(op_d,unit),op_c),X0)),
inference(forward_demodulation,[],[f22619,f15448]) ).
fof(f22630,plain,
! [X0] : mult(mult(op_d,mult(op_c,rd(unit,op_c))),X0) = mult(op_d,mult(mult(op_c,rd(unit,op_c)),X0)),
inference(forward_demodulation,[],[f22626,f1658]) ).
fof(f22769,plain,
! [X0] : mult(X0,op_c) = mult(mult(X0,ld(op_d,unit)),mult(op_d,op_c)),
inference(superposition,[],[f22611,f4]) ).
fof(f22859,plain,
! [X0] : mult(mult(op_d,X0),op_c) = ld(ld(op_d,unit),mult(X0,op_c)),
inference(backward_demodulation,[],[f19659,f22769]) ).
fof(f23060,plain,
! [X0] : rd(mult(op_c,X0),mult(op_d,op_c)) = mult(op_c,rd(X0,mult(op_d,op_c))),
inference(superposition,[],[f22141,f3]) ).
fof(f23101,plain,
! [X0] : rd(mult(mult(op_d,op_c),mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = ld(rd(op_c,mult(op_d,op_c)),mult(op_c,X0)),
inference(superposition,[],[f1721,f22141]) ).
fof(f23102,plain,
! [X0] : rd(mult(mult(op_d,op_c),mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = ld(ld(op_d,unit),mult(op_c,X0)),
inference(forward_demodulation,[],[f23101,f19617]) ).
fof(f23148,plain,
! [X0] : ld(rd(unit,mult(op_d,op_c)),X0) = ld(ld(op_d,unit),mult(op_c,X0)),
inference(forward_demodulation,[],[f23102,f2686]) ).
fof(f23184,plain,
ld(op_c,rd(op_c,op_d)) = ld(ld(op_d,unit),mult(op_c,op_c)),
inference(backward_demodulation,[],[f19557,f23148]) ).
fof(f23202,plain,
ld(op_c,rd(op_c,op_d)) = mult(mult(op_d,op_c),op_c),
inference(forward_demodulation,[],[f23184,f22859]) ).
fof(f23248,plain,
rd(unit,mult(op_d,op_c)) = mult(op_c,rd(op_d,mult(op_d,op_c))),
inference(superposition,[],[f23060,f10]) ).
fof(f23264,plain,
rd(op_c,mult(op_d,op_c)) = mult(op_c,rd(unit,mult(op_d,op_c))),
inference(superposition,[],[f23060,f5]) ).
fof(f23321,plain,
ld(op_d,unit) = mult(op_c,rd(unit,mult(op_d,op_c))),
inference(forward_demodulation,[],[f23264,f19617]) ).
fof(f23331,plain,
rd(rd(unit,op_c),op_d) = rd(unit,mult(op_d,op_c)),
inference(forward_demodulation,[],[f23248,f16893]) ).
fof(f23353,plain,
! [X0] : rd(X0,ld(op_c,ld(op_d,unit))) = rd(X0,rd(unit,mult(op_d,op_c))),
inference(backward_demodulation,[],[f17740,f23331]) ).
fof(f23735,plain,
! [X0] : mult(mult(X0,op_d),mult(rd(op_c,op_d),op_d)) = mult(mult(X0,mult(mult(op_d,op_c),op_c)),op_d),
inference(superposition,[],[f1341,f23202]) ).
fof(f23751,plain,
! [X0] : mult(rd(X0,op_c),rd(rd(op_c,op_d),op_c)) = rd(mult(X0,mult(mult(op_d,op_c),op_c)),op_c),
inference(superposition,[],[f1490,f23202]) ).
fof(f23776,plain,
! [X0] : mult(rd(X0,op_c),mult(op_c,mult(op_d,op_c))) = rd(mult(X0,mult(mult(op_d,op_c),op_c)),op_c),
inference(forward_demodulation,[],[f23751,f1217]) ).
fof(f23786,plain,
! [X0] : mult(mult(X0,op_d),op_c) = mult(mult(X0,mult(mult(op_d,op_c),op_c)),op_d),
inference(forward_demodulation,[],[f23735,f3]) ).
fof(f23796,plain,
! [X0] : mult(op_c,mult(ld(op_c,X0),mult(op_d,op_c))) = rd(mult(X0,mult(mult(op_d,op_c),op_c)),op_c),
inference(forward_demodulation,[],[f23776,f56]) ).
fof(f23810,plain,
! [X0] : mult(op_c,mult(op_d,mult(mult(X0,op_d),op_c))) = rd(mult(X0,mult(mult(op_d,op_c),op_c)),op_c),
inference(forward_demodulation,[],[f23796,f1419]) ).
fof(f23820,plain,
! [X0] : rd(mult(X0,op_d),rd(unit,op_c)) = rd(mult(X0,mult(mult(op_d,op_c),op_c)),op_c),
inference(forward_demodulation,[],[f23810,f9355]) ).
fof(f23825,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = rd(mult(X0,mult(mult(op_d,op_c),op_c)),op_c),
inference(forward_demodulation,[],[f23820,f22214]) ).
fof(f24025,plain,
! [X0] : mult(rd(X0,mult(op_d,op_c)),mult(op_d,op_c)) = rd(mult(mult(op_d,op_c),mult(ld(mult(op_d,op_c),X0),op_c)),op_c),
inference(superposition,[],[f23825,f56]) ).
fof(f24041,plain,
mult(op_c,mult(op_d,op_c)) = ld(rd(unit,op_c),mult(op_d,op_c)),
inference(superposition,[],[f2686,f23825]) ).
fof(f24046,plain,
! [X0] : mult(mult(X0,op_c),mult(op_d,op_c)) = mult(X0,rd(mult(op_c,mult(mult(op_d,op_c),op_c)),op_c)),
inference(superposition,[],[f1503,f23825]) ).
fof(f24091,plain,
! [X0] : mult(mult(X0,op_c),mult(op_d,op_c)) = mult(X0,ld(rd(unit,op_c),mult(op_d,op_c))),
inference(forward_demodulation,[],[f24046,f2686]) ).
fof(f24111,plain,
! [X0] : mult(rd(X0,mult(op_d,op_c)),mult(op_d,op_c)) = mult(op_d,rd(mult(op_c,mult(ld(mult(op_d,op_c),X0),op_c)),op_c)),
inference(forward_demodulation,[],[f24025,f1503]) ).
fof(f24123,plain,
! [X0] : mult(X0,mult(op_c,mult(op_d,op_c))) = mult(mult(X0,op_c),mult(op_d,op_c)),
inference(forward_demodulation,[],[f24091,f24041]) ).
fof(f24133,plain,
! [X0] : mult(rd(X0,mult(op_d,op_c)),mult(op_d,op_c)) = mult(op_d,ld(rd(unit,op_c),ld(mult(op_d,op_c),X0))),
inference(forward_demodulation,[],[f24111,f2686]) ).
fof(f24155,plain,
! [X0] : mult(op_d,ld(rd(unit,op_c),ld(mult(op_d,op_c),X0))) = X0,
inference(forward_demodulation,[],[f24133,f3]) ).
fof(f24242,plain,
! [X0,X1] : mult(mult(X0,op_c),ld(mult(op_d,op_c),ld(mult(X0,op_c),X1))) = ld(rd(mult(X0,mult(op_c,mult(op_d,op_c))),mult(X0,op_c)),X1),
inference(superposition,[],[f689,f24123]) ).
fof(f24269,plain,
! [X0,X1] : mult(mult(X0,op_c),ld(mult(op_d,op_c),ld(mult(X0,op_c),X1))) = mult(X0,ld(rd(mult(op_c,mult(op_d,op_c)),op_c),ld(X0,X1))),
inference(forward_demodulation,[],[f24242,f8793]) ).
fof(f24292,plain,
! [X0,X1] : mult(mult(X0,op_c),ld(mult(op_d,op_c),ld(mult(X0,op_c),X1))) = mult(X0,mult(op_c,ld(mult(op_d,op_c),ld(op_c,ld(X0,X1))))),
inference(forward_demodulation,[],[f24269,f689]) ).
fof(f24304,plain,
! [X0,X1] : mult(X0,ld(ld(rd(unit,op_c),op_d),ld(X0,X1))) = mult(mult(X0,op_c),ld(mult(op_d,op_c),ld(mult(X0,op_c),X1))),
inference(forward_demodulation,[],[f24292,f8792]) ).
fof(f26114,plain,
! [X0] : mult(mult(op_d,op_c),X0) = mult(op_d,ld(rd(unit,op_c),X0)),
inference(superposition,[],[f24155,f2]) ).
fof(f26120,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(op_d,mult(ld(rd(unit,op_c),ld(mult(op_d,op_c),X0)),mult(op_d,op_c))),
inference(superposition,[],[f22370,f24155]) ).
fof(f26210,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(op_d,mult(op_c,mult(mult(ld(mult(op_d,op_c),X0),op_d),op_c))),
inference(forward_demodulation,[],[f26120,f11589]) ).
fof(f26267,plain,
! [X0] : mult(op_d,X0) = mult(mult(op_d,op_c),mult(rd(unit,op_c),X0)),
inference(superposition,[],[f26114,f2]) ).
fof(f26272,plain,
! [X0] : mult(op_d,rd(mult(op_c,X0),op_c)) = mult(mult(op_d,op_c),rd(X0,op_c)),
inference(superposition,[],[f26114,f2587]) ).
fof(f26278,plain,
! [X0] : ld(op_c,rd(ld(rd(unit,op_c),X0),op_d)) = rd(mult(mult(op_d,op_c),X0),op_d),
inference(superposition,[],[f1200,f26114]) ).
fof(f26302,plain,
! [X0,X1] : mult(op_d,ld(ld(rd(unit,op_c),X0),ld(op_d,X1))) = ld(rd(mult(mult(op_d,op_c),X0),op_d),X1),
inference(superposition,[],[f689,f26114]) ).
fof(f26344,plain,
! [X0] : mult(op_d,mult(op_c,mult(X0,op_d))) = mult(mult(op_d,op_c),rd(X0,op_c)),
inference(forward_demodulation,[],[f26272,f16]) ).
fof(f26935,plain,
! [X0] : mult(rd(unit,op_c),X0) = ld(mult(op_d,op_c),mult(op_d,X0)),
inference(superposition,[],[f2,f26267]) ).
fof(f27110,plain,
! [X0] : mult(mult(op_d,op_c),mult(X0,mult(op_d,op_c))) = mult(op_d,mult(op_c,mult(mult(X0,mult(mult(op_d,op_c),op_c)),op_d))),
inference(superposition,[],[f26344,f23825]) ).
fof(f27180,plain,
! [X0] : mult(mult(op_d,op_c),mult(X0,mult(op_d,op_c))) = mult(op_d,mult(op_c,mult(mult(X0,op_d),op_c))),
inference(forward_demodulation,[],[f27110,f23786]) ).
fof(f27262,plain,
! [X0] : ld(rd(unit,mult(op_d,op_c)),X0) = rd(mult(op_d,mult(op_c,mult(mult(X0,op_d),op_c))),mult(op_d,op_c)),
inference(superposition,[],[f2686,f27180]) ).
fof(f27263,plain,
! [X0] : mult(rd(X0,rd(X0,mult(op_d,op_c))),X0) = mult(op_d,mult(op_c,mult(mult(ld(mult(op_d,op_c),X0),op_d),op_c))),
inference(superposition,[],[f14668,f27180]) ).
fof(f27292,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(rd(X1,mult(op_d,op_c)),rd(mult(op_d,mult(op_c,mult(mult(X0,op_d),op_c))),mult(op_d,op_c))),
inference(superposition,[],[f1602,f27180]) ).
fof(f27310,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(rd(X1,mult(op_d,op_c)),ld(rd(rd(unit,op_c),op_d),rd(mult(X0,op_d),op_d))),
inference(forward_demodulation,[],[f27292,f3373]) ).
fof(f27319,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = mult(rd(X0,rd(X0,mult(op_d,op_c))),X0),
inference(forward_demodulation,[],[f27263,f26210]) ).
fof(f27320,plain,
! [X0] : ld(rd(unit,mult(op_d,op_c)),X0) = ld(rd(rd(unit,op_c),op_d),rd(mult(X0,op_d),op_d)),
inference(forward_demodulation,[],[f27262,f3373]) ).
fof(f27354,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(rd(X1,mult(op_d,op_c)),ld(op_c,rd(ld(rd(unit,op_c),mult(X0,op_d)),op_d))),
inference(forward_demodulation,[],[f27310,f8486]) ).
fof(f27363,plain,
! [X0] : ld(rd(unit,mult(op_d,op_c)),X0) = ld(op_c,rd(ld(rd(unit,op_c),mult(X0,op_d)),op_d)),
inference(forward_demodulation,[],[f27320,f8486]) ).
fof(f27389,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(rd(X1,mult(op_d,op_c)),rd(mult(mult(op_d,op_c),mult(X0,op_d)),op_d)),
inference(forward_demodulation,[],[f27354,f26278]) ).
fof(f27396,plain,
! [X0] : ld(rd(unit,mult(op_d,op_c)),X0) = rd(mult(mult(op_d,op_c),mult(X0,op_d)),op_d),
inference(forward_demodulation,[],[f27363,f26278]) ).
fof(f27417,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(rd(X1,mult(op_d,op_c)),mult(rd(mult(op_d,op_c),op_d),ld(op_c,X0))),
inference(forward_demodulation,[],[f27389,f2381]) ).
fof(f27421,plain,
! [X0] : mult(rd(mult(op_d,op_c),op_d),ld(op_c,X0)) = ld(rd(unit,mult(op_d,op_c)),X0),
inference(forward_demodulation,[],[f27396,f2381]) ).
fof(f27438,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(rd(X1,mult(op_d,op_c)),mult(op_d,mult(op_c,ld(op_d,ld(op_c,X0))))),
inference(forward_demodulation,[],[f27417,f55]) ).
fof(f27442,plain,
! [X0] : mult(rd(mult(op_d,op_c),op_d),ld(op_c,X0)) = ld(ld(op_d,unit),mult(op_c,X0)),
inference(forward_demodulation,[],[f27421,f23148]) ).
fof(f27449,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(op_d,mult(rd(ld(op_d,X1),op_c),mult(op_c,ld(op_d,ld(op_c,X0))))),
inference(forward_demodulation,[],[f27438,f15448]) ).
fof(f27453,plain,
! [X0] : mult(op_d,mult(op_c,ld(op_d,ld(op_c,X0)))) = ld(ld(op_d,unit),mult(op_c,X0)),
inference(forward_demodulation,[],[f27442,f55]) ).
fof(f27460,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(op_d,mult(op_c,mult(ld(op_c,ld(op_d,X1)),ld(op_d,ld(op_c,X0))))),
inference(forward_demodulation,[],[f27449,f56]) ).
fof(f27463,plain,
! [X0] : mult(op_d,mult(op_c,mult(mult(X0,op_c),op_d))) = ld(ld(op_d,unit),mult(op_c,X0)),
inference(forward_demodulation,[],[f27453,f1178]) ).
fof(f27470,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(op_d,mult(op_c,mult(ld(op_c,ld(op_d,X1)),mult(mult(X0,op_c),op_d)))),
inference(forward_demodulation,[],[f27460,f1178]) ).
fof(f27473,plain,
! [X0] : mult(op_d,ld(rd(unit,op_c),X0)) = ld(ld(op_d,unit),mult(op_c,X0)),
inference(forward_demodulation,[],[f27463,f3363]) ).
fof(f27480,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(op_d,mult(op_c,mult(op_d,mult(mult(ld(op_d,X1),mult(X0,op_c)),op_d)))),
inference(forward_demodulation,[],[f27470,f2080]) ).
fof(f27483,plain,
! [X0] : mult(mult(op_d,op_c),X0) = ld(ld(op_d,unit),mult(op_c,X0)),
inference(forward_demodulation,[],[f27473,f26114]) ).
fof(f27492,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(op_d,rd(mult(ld(op_d,X1),mult(X0,op_c)),op_c)),
inference(forward_demodulation,[],[f27480,f1151]) ).
fof(f27501,plain,
! [X0] : mult(mult(op_d,op_c),X0) = ld(rd(unit,mult(op_d,op_c)),X0),
inference(backward_demodulation,[],[f23148,f27483]) ).
fof(f28213,plain,
! [X0,X1] : mult(mult(mult(op_d,op_c),X0),mult(X1,mult(op_d,op_c))) = mult(mult(op_d,op_c),mult(mult(X0,X1),mult(op_d,op_c))),
inference(superposition,[],[f11589,f27501]) ).
fof(f28215,plain,
! [X0] : ld(mult(op_d,op_c),X0) = mult(ld(mult(op_d,op_c),unit),ld(mult(op_d,op_c),mult(mult(op_d,op_c),X0))),
inference(superposition,[],[f2754,f27501]) ).
fof(f28223,plain,
! [X0,X1] : mult(rd(X1,rd(unit,mult(op_d,op_c))),X0) = mult(rd(unit,mult(op_d,op_c)),mult(ld(rd(unit,mult(op_d,op_c)),X1),mult(mult(op_d,op_c),X0))),
inference(superposition,[],[f134,f27501]) ).
fof(f28302,plain,
! [X0,X1] : mult(rd(X1,rd(unit,mult(op_d,op_c))),X0) = mult(rd(unit,mult(op_d,op_c)),mult(mult(op_d,op_c),mult(ld(unit,mult(X1,mult(op_d,op_c))),X0))),
inference(forward_demodulation,[],[f28223,f10327]) ).
fof(f28307,plain,
! [X0] : ld(mult(op_d,op_c),X0) = mult(ld(mult(op_d,op_c),unit),X0),
inference(forward_demodulation,[],[f28215,f2]) ).
fof(f28308,plain,
! [X0,X1] : mult(mult(mult(op_d,op_c),X0),mult(X1,mult(op_d,op_c))) = mult(op_d,mult(op_c,mult(mult(mult(X0,X1),op_d),op_c))),
inference(forward_demodulation,[],[f28213,f27180]) ).
fof(f28339,plain,
! [X0,X1] : mult(rd(X1,rd(unit,mult(op_d,op_c))),X0) = mult(mult(op_d,op_c),mult(ld(mult(op_d,op_c),unit),mult(ld(unit,mult(X1,mult(op_d,op_c))),X0))),
inference(forward_demodulation,[],[f28302,f56]) ).
fof(f28375,plain,
! [X0,X1] : mult(rd(X1,rd(unit,mult(op_d,op_c))),X0) = mult(mult(op_d,op_c),ld(mult(op_d,op_c),mult(ld(unit,mult(X1,mult(op_d,op_c))),X0))),
inference(forward_demodulation,[],[f28339,f28307]) ).
fof(f28391,plain,
! [X0,X1] : mult(rd(X1,rd(unit,mult(op_d,op_c))),X0) = mult(ld(unit,mult(X1,mult(op_d,op_c))),X0),
inference(forward_demodulation,[],[f28375,f1]) ).
fof(f28403,plain,
! [X0,X1] : mult(rd(X1,rd(unit,mult(op_d,op_c))),X0) = mult(mult(X1,mult(op_d,op_c)),X0),
inference(forward_demodulation,[],[f28391,f38]) ).
fof(f28408,plain,
! [X0,X1] : mult(rd(X1,ld(op_c,ld(op_d,unit))),X0) = mult(mult(X1,mult(op_d,op_c)),X0),
inference(forward_demodulation,[],[f28403,f23353]) ).
fof(f28565,plain,
! [X0] : rd(rd(X0,op_c),rd(unit,op_c)) = mult(op_d,mult(op_c,ld(mult(op_d,op_c),X0))),
inference(superposition,[],[f22319,f6418]) ).
fof(f28630,plain,
! [X0] : mult(op_c,mult(ld(op_c,unit),X0)) = mult(op_d,mult(op_c,ld(mult(op_d,op_c),X0))),
inference(forward_demodulation,[],[f28565,f12913]) ).
fof(f28645,plain,
! [X0] : mult(op_c,mult(op_d,X0)) = mult(op_d,mult(op_c,ld(mult(op_d,op_c),X0))),
inference(forward_demodulation,[],[f28630,f39]) ).
fof(f28657,plain,
! [X0] : mult(op_d,mult(op_c,X0)) = mult(op_c,mult(op_d,mult(mult(op_d,op_c),X0))),
inference(superposition,[],[f28645,f2]) ).
fof(f28661,plain,
mult(op_c,mult(op_d,op_d)) = mult(op_d,mult(op_c,rd(unit,op_c))),
inference(superposition,[],[f28645,f19500]) ).
fof(f28674,plain,
! [X0] : ld(op_d,mult(op_c,mult(op_d,X0))) = mult(op_c,ld(mult(op_d,op_c),X0)),
inference(superposition,[],[f2,f28645]) ).
fof(f28726,plain,
! [X0] : mult(ld(op_d,mult(op_c,op_d)),X0) = mult(op_c,ld(mult(op_d,op_c),X0)),
inference(forward_demodulation,[],[f28674,f464]) ).
fof(f28736,plain,
rd(unit,op_c) = mult(op_d,mult(op_c,rd(unit,op_c))),
inference(forward_demodulation,[],[f28661,f152]) ).
fof(f28752,plain,
! [X0] : mult(mult(mult(op_c,op_c),op_d),X0) = mult(op_c,ld(mult(op_d,op_c),X0)),
inference(forward_demodulation,[],[f28726,f25]) ).
fof(f28761,plain,
! [X0] : mult(rd(unit,op_c),X0) = mult(op_d,mult(mult(op_c,rd(unit,op_c)),X0)),
inference(backward_demodulation,[],[f22630,f28736]) ).
fof(f28775,plain,
! [X0] : mult(ld(op_d,unit),X0) = mult(op_c,ld(mult(op_d,op_c),X0)),
inference(forward_demodulation,[],[f28752,f118]) ).
fof(f28869,plain,
! [X0] : mult(mult(op_d,mult(op_c,X0)),op_c) = mult(op_c,rd(mult(op_d,mult(mult(op_d,op_c),X0)),op_d)),
inference(superposition,[],[f4022,f28657]) ).
fof(f28941,plain,
! [X0] : mult(mult(op_d,mult(op_c,X0)),op_c) = mult(op_c,ld(op_c,rd(mult(mult(op_d,op_c),X0),op_d))),
inference(forward_demodulation,[],[f28869,f1200]) ).
fof(f28980,plain,
! [X0] : mult(mult(op_d,mult(op_c,X0)),op_c) = rd(mult(mult(op_d,op_c),X0),op_d),
inference(forward_demodulation,[],[f28941,f1]) ).
fof(f29070,plain,
! [X0] : mult(mult(op_d,op_c),rd(X0,op_d)) = rd(mult(mult(op_d,op_c),X0),op_d),
inference(forward_demodulation,[],[f28980,f4110]) ).
fof(f29097,plain,
! [X0,X1] : mult(op_d,ld(ld(rd(unit,op_c),X0),ld(op_d,X1))) = ld(mult(mult(op_d,op_c),rd(X0,op_d)),X1),
inference(backward_demodulation,[],[f26302,f29070]) ).
fof(f29932,plain,
mult(ld(op_d,unit),op_d) = mult(op_c,rd(unit,op_c)),
inference(superposition,[],[f28775,f19500]) ).
fof(f30042,plain,
ld(op_d,rd(unit,op_c)) = mult(op_c,rd(unit,op_c)),
inference(backward_demodulation,[],[f809,f29932]) ).
fof(f31581,plain,
ld(op_c,ld(op_d,unit)) = rd(unit,mult(op_d,op_c)),
inference(superposition,[],[f2,f23321]) ).
fof(f31651,plain,
ld(op_c,ld(op_d,unit)) = rd(rd(unit,op_c),op_d),
inference(backward_demodulation,[],[f23331,f31581]) ).
fof(f31656,plain,
! [X0] : mult(mult(op_d,op_c),X0) = ld(ld(op_c,ld(op_d,unit)),X0),
inference(backward_demodulation,[],[f27501,f31581]) ).
fof(f31942,plain,
! [X0,X1] : mult(mult(op_d,op_c),mult(rd(X0,ld(op_c,ld(op_d,unit))),X1)) = mult(ld(ld(op_c,ld(op_d,unit)),X0),ld(ld(op_c,ld(op_d,unit)),X1)),
inference(superposition,[],[f830,f31656]) ).
fof(f31945,plain,
! [X0] : ld(X0,mult(mult(mult(op_d,op_c),unit),X0)) = ld(mult(ld(op_c,ld(op_d,unit)),X0),X0),
inference(superposition,[],[f513,f31656]) ).
fof(f31950,plain,
! [X0] : ld(X0,mult(mult(op_d,op_c),X0)) = ld(mult(ld(op_c,ld(op_d,unit)),X0),X0),
inference(forward_demodulation,[],[f31945,f5]) ).
fof(f31953,plain,
! [X0,X1] : mult(mult(op_d,op_c),mult(rd(X0,ld(op_c,ld(op_d,unit))),X1)) = mult(ld(ld(op_c,ld(op_d,unit)),X0),mult(mult(op_d,op_c),X1)),
inference(forward_demodulation,[],[f31942,f31656]) ).
fof(f31991,plain,
! [X0,X1] : mult(mult(op_d,op_c),mult(rd(X0,ld(op_c,ld(op_d,unit))),X1)) = mult(mult(mult(op_d,op_c),X0),mult(mult(op_d,op_c),X1)),
inference(forward_demodulation,[],[f31953,f31656]) ).
fof(f32021,plain,
! [X0,X1] : mult(mult(op_d,op_c),mult(mult(X0,mult(op_d,op_c)),X1)) = mult(mult(mult(op_d,op_c),X0),mult(mult(op_d,op_c),X1)),
inference(forward_demodulation,[],[f31991,f28408]) ).
fof(f32816,plain,
! [X0] : mult(rd(rd(unit,op_c),op_d),X0) = mult(op_d,mult(mult(op_c,rd(unit,op_c)),ld(op_d,X0))),
inference(superposition,[],[f134,f30042]) ).
fof(f32854,plain,
! [X0] : mult(rd(rd(unit,op_c),op_d),X0) = mult(rd(unit,op_c),ld(op_d,X0)),
inference(forward_demodulation,[],[f32816,f28761]) ).
fof(f32877,plain,
! [X0] : mult(ld(op_c,ld(op_d,unit)),X0) = mult(rd(unit,op_c),ld(op_d,X0)),
inference(forward_demodulation,[],[f32854,f31651]) ).
fof(f32905,plain,
! [X0] : ld(X0,mult(mult(op_d,op_c),X0)) = ld(mult(rd(unit,op_c),ld(op_d,X0)),X0),
inference(backward_demodulation,[],[f31950,f32877]) ).
fof(f33348,plain,
! [X0] : mult(rd(unit,mult(op_d,op_c)),X0) = mult(mult(op_d,op_c),ld(mult(op_d,op_c),ld(mult(op_d,op_c),X0))),
inference(superposition,[],[f134,f28307]) ).
fof(f33351,plain,
! [X0] : mult(rd(X0,rd(unit,mult(op_d,op_c))),unit) = mult(mult(op_d,op_c),ld(mult(op_d,op_c),ld(unit,mult(X0,mult(op_d,op_c))))),
inference(superposition,[],[f10167,f28307]) ).
fof(f33361,plain,
! [X0,X1] : mult(ld(mult(op_d,op_c),unit),mult(ld(ld(mult(op_d,op_c),unit),X1),X0)) = mult(rd(X1,ld(mult(op_d,op_c),unit)),ld(mult(op_d,op_c),X0)),
inference(superposition,[],[f56,f28307]) ).
fof(f33378,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = mult(rd(X1,ld(mult(op_d,op_c),unit)),rd(ld(mult(op_d,op_c),X0),ld(mult(op_d,op_c),unit))),
inference(superposition,[],[f1602,f28307]) ).
fof(f33388,plain,
! [X0] : rd(X0,ld(ld(mult(op_d,op_c),unit),unit)) = ld(ld(mult(op_d,op_c),unit),mult(ld(mult(op_d,op_c),X0),ld(mult(op_d,op_c),unit))),
inference(superposition,[],[f12428,f28307]) ).
fof(f33406,plain,
! [X0] : mult(rd(X0,rd(X0,ld(mult(op_d,op_c),unit))),X0) = ld(mult(op_d,op_c),mult(ld(ld(mult(op_d,op_c),unit),X0),ld(mult(op_d,op_c),unit))),
inference(superposition,[],[f14668,f28307]) ).
fof(f33508,plain,
! [X0] : rd(X0,ld(ld(mult(op_d,op_c),unit),unit)) = ld(unit,mult(mult(mult(op_d,op_c),ld(mult(op_d,op_c),X0)),ld(mult(op_d,op_c),unit))),
inference(forward_demodulation,[],[f33388,f72]) ).
fof(f33513,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = mult(rd(X1,ld(mult(op_d,op_c),unit)),ld(mult(op_d,op_c),mult(rd(X0,unit),mult(op_d,op_c)))),
inference(forward_demodulation,[],[f33378,f11147]) ).
fof(f33526,plain,
! [X0,X1] : mult(ld(mult(op_d,op_c),unit),mult(ld(ld(mult(op_d,op_c),unit),X1),X0)) = ld(mult(op_d,op_c),mult(mult(mult(op_d,op_c),X1),X0)),
inference(forward_demodulation,[],[f33361,f12788]) ).
fof(f33532,plain,
! [X0] : ld(unit,mult(X0,mult(op_d,op_c))) = mult(rd(X0,rd(unit,mult(op_d,op_c))),unit),
inference(forward_demodulation,[],[f33351,f1]) ).
fof(f33535,plain,
! [X0] : mult(op_d,ld(ld(rd(unit,op_c),op_d),ld(op_d,X0))) = mult(rd(unit,mult(op_d,op_c)),X0),
inference(forward_demodulation,[],[f33348,f24304]) ).
fof(f33588,plain,
! [X0] : rd(X0,ld(ld(mult(op_d,op_c),unit),unit)) = mult(mult(mult(op_d,op_c),ld(mult(op_d,op_c),X0)),ld(mult(op_d,op_c),unit)),
inference(forward_demodulation,[],[f33508,f38]) ).
fof(f33592,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = ld(mult(op_d,op_c),mult(mult(mult(op_d,op_c),X1),mult(rd(X0,unit),mult(op_d,op_c)))),
inference(forward_demodulation,[],[f33513,f12788]) ).
fof(f33600,plain,
! [X0,X1] : ld(mult(op_d,op_c),mult(mult(mult(op_d,op_c),X1),X0)) = ld(mult(op_d,op_c),mult(ld(ld(mult(op_d,op_c),unit),X1),X0)),
inference(forward_demodulation,[],[f33526,f28307]) ).
fof(f33605,plain,
! [X0] : rd(X0,rd(unit,mult(op_d,op_c))) = ld(unit,mult(X0,mult(op_d,op_c))),
inference(forward_demodulation,[],[f33532,f5]) ).
fof(f33610,plain,
! [X0] : mult(ld(op_c,ld(op_d,unit)),X0) = mult(op_d,ld(ld(rd(unit,op_c),op_d),ld(op_d,X0))),
inference(forward_demodulation,[],[f33535,f31581]) ).
fof(f33663,plain,
! [X0] : mult(X0,ld(mult(op_d,op_c),unit)) = rd(X0,ld(ld(mult(op_d,op_c),unit),unit)),
inference(forward_demodulation,[],[f33588,f1]) ).
fof(f33666,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = ld(mult(op_d,op_c),mult(op_d,mult(op_c,mult(mult(mult(X1,rd(X0,unit)),op_d),op_c)))),
inference(forward_demodulation,[],[f33592,f28308]) ).
fof(f33673,plain,
! [X0] : mult(rd(X0,rd(X0,ld(mult(op_d,op_c),unit))),X0) = ld(mult(op_d,op_c),mult(mult(mult(op_d,op_c),X0),ld(mult(op_d,op_c),unit))),
inference(backward_demodulation,[],[f33406,f33600]) ).
fof(f33677,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = rd(X0,rd(unit,mult(op_d,op_c))),
inference(forward_demodulation,[],[f33605,f38]) ).
fof(f33679,plain,
! [X0] : mult(ld(op_c,ld(op_d,unit)),X0) = ld(mult(mult(op_d,op_c),rd(op_d,op_d)),X0),
inference(forward_demodulation,[],[f33610,f29097]) ).
fof(f33721,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = mult(rd(unit,op_c),mult(op_c,mult(mult(mult(X1,rd(X0,unit)),op_d),op_c))),
inference(forward_demodulation,[],[f33666,f26935]) ).
fof(f33729,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = rd(X0,ld(op_c,ld(op_d,unit))),
inference(forward_demodulation,[],[f33677,f31581]) ).
fof(f33731,plain,
! [X0] : mult(ld(op_c,ld(op_d,unit)),X0) = ld(mult(mult(op_d,op_c),unit),X0),
inference(forward_demodulation,[],[f33679,f130]) ).
fof(f33752,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = mult(op_c,mult(ld(op_c,unit),mult(mult(mult(X1,rd(X0,unit)),op_d),op_c))),
inference(forward_demodulation,[],[f33721,f56]) ).
fof(f33770,plain,
! [X0] : mult(ld(op_c,ld(op_d,unit)),X0) = ld(mult(op_d,op_c),X0),
inference(forward_demodulation,[],[f33731,f5]) ).
fof(f33783,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = rd(mult(mult(X1,rd(X0,unit)),op_d),rd(unit,op_c)),
inference(forward_demodulation,[],[f33752,f14784]) ).
fof(f33791,plain,
! [X0] : ld(mult(op_d,op_c),X0) = mult(rd(unit,op_c),ld(op_d,X0)),
inference(forward_demodulation,[],[f33770,f32877]) ).
fof(f33801,plain,
! [X0,X1] : rd(mult(X1,X0),ld(mult(op_d,op_c),unit)) = mult(mult(X1,rd(X0,unit)),mult(op_d,op_c)),
inference(forward_demodulation,[],[f33783,f22214]) ).
fof(f33813,plain,
! [X0] : ld(ld(mult(op_d,op_c),X0),X0) = ld(X0,mult(mult(op_d,op_c),X0)),
inference(backward_demodulation,[],[f32905,f33791]) ).
fof(f33834,plain,
! [X0,X1] : mult(mult(X1,X0),mult(op_d,op_c)) = rd(mult(X1,X0),ld(mult(op_d,op_c),unit)),
inference(forward_demodulation,[],[f33801,f109]) ).
fof(f33847,plain,
! [X0] : mult(X0,ld(mult(op_d,op_c),unit)) = rd(X0,ld(unit,mult(mult(op_d,op_c),unit))),
inference(backward_demodulation,[],[f33663,f33813]) ).
fof(f33865,plain,
! [X0] : mult(X0,ld(mult(op_d,op_c),unit)) = mult(rd(rd(X0,unit),mult(op_d,op_c)),unit),
inference(forward_demodulation,[],[f33847,f373]) ).
fof(f33887,plain,
! [X0] : mult(X0,ld(mult(op_d,op_c),unit)) = rd(rd(X0,unit),mult(op_d,op_c)),
inference(forward_demodulation,[],[f33865,f5]) ).
fof(f33901,plain,
! [X0] : rd(X0,mult(op_d,op_c)) = mult(X0,ld(mult(op_d,op_c),unit)),
inference(forward_demodulation,[],[f33887,f109]) ).
fof(f33920,plain,
! [X0] : mult(rd(X0,rd(X0,ld(mult(op_d,op_c),unit))),X0) = ld(mult(op_d,op_c),rd(mult(mult(op_d,op_c),X0),mult(op_d,op_c))),
inference(backward_demodulation,[],[f33673,f33901]) ).
fof(f33937,plain,
! [X0] : mult(X0,ld(mult(op_d,op_c),unit)) = mult(rd(X0,rd(X0,ld(mult(op_d,op_c),unit))),X0),
inference(forward_demodulation,[],[f33920,f3664]) ).
fof(f33947,plain,
! [X0] : rd(X0,mult(op_d,op_c)) = mult(rd(X0,rd(X0,ld(mult(op_d,op_c),unit))),X0),
inference(forward_demodulation,[],[f33937,f33901]) ).
fof(f34035,plain,
! [X0] : mult(X0,mult(op_d,op_c)) = rd(X0,ld(mult(op_d,op_c),unit)),
inference(superposition,[],[f33834,f6]) ).
fof(f34162,plain,
! [X0] : rd(X0,mult(op_d,op_c)) = mult(rd(X0,mult(X0,mult(op_d,op_c))),X0),
inference(backward_demodulation,[],[f33947,f34035]) ).
fof(f34206,plain,
! [X0] : rd(X0,mult(op_d,op_c)) = mult(X0,rd(ld(X0,X0),mult(op_d,op_c))),
inference(forward_demodulation,[],[f34162,f15455]) ).
fof(f34245,plain,
! [X0] : rd(X0,mult(op_d,op_c)) = mult(X0,rd(unit,mult(op_d,op_c))),
inference(forward_demodulation,[],[f34206,f40]) ).
fof(f34295,plain,
! [X0] : rd(X0,mult(op_d,op_c)) = mult(X0,ld(op_c,ld(op_d,unit))),
inference(forward_demodulation,[],[f34245,f31581]) ).
fof(f40626,plain,
! [X0,X1] : mult(mult(X1,ld(op_c,ld(op_d,unit))),ld(ld(op_c,ld(op_d,unit)),X0)) = mult(mult(X1,mult(X0,mult(op_d,op_c))),ld(op_c,ld(op_d,unit))),
inference(superposition,[],[f107,f33729]) ).
fof(f40687,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(mult(X1,ld(op_c,ld(op_d,unit))),ld(ld(op_c,ld(op_d,unit)),X0)),
inference(forward_demodulation,[],[f40626,f34295]) ).
fof(f40763,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(mult(X1,ld(op_c,ld(op_d,unit))),mult(mult(op_d,op_c),X0)),
inference(forward_demodulation,[],[f40687,f31656]) ).
fof(f40828,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(rd(X1,mult(op_d,op_c)),mult(mult(op_d,op_c),X0)),
inference(forward_demodulation,[],[f40763,f34295]) ).
fof(f40884,plain,
! [X0,X1] : rd(mult(X1,mult(X0,mult(op_d,op_c))),mult(op_d,op_c)) = mult(mult(op_d,op_c),mult(ld(mult(op_d,op_c),X1),X0)),
inference(forward_demodulation,[],[f40828,f56]) ).
fof(f40922,plain,
! [X0,X1] : mult(op_d,rd(mult(ld(op_d,X1),mult(X0,op_c)),op_c)) = mult(mult(op_d,op_c),mult(ld(mult(op_d,op_c),X1),X0)),
inference(forward_demodulation,[],[f40884,f27492]) ).
fof(f46635,plain,
! [X0,X1] : mult(op_d,mult(op_c,mult(mult(X0,ld(op_c,op_d)),X1))) = mult(mult(mult(X0,rd(mult(ld(op_c,op_d),X1),ld(op_c,op_d))),op_d),op_d),
inference(superposition,[],[f4784,f1503]) ).
fof(f46662,plain,
! [X0,X1] : mult(mult(X1,mult(rd(X0,ld(op_c,op_d)),op_d)),op_d) = mult(mult(X1,op_d),ld(op_d,mult(op_d,mult(op_c,X0)))),
inference(superposition,[],[f8,f4784]) ).
fof(f46715,plain,
! [X0,X1] : mult(mult(X1,op_d),mult(op_c,X0)) = mult(mult(X1,mult(rd(X0,ld(op_c,op_d)),op_d)),op_d),
inference(forward_demodulation,[],[f46662,f2]) ).
fof(f46736,plain,
! [X0,X1] : mult(op_d,mult(op_c,mult(mult(X0,ld(op_c,op_d)),X1))) = mult(mult(mult(X0,ld(op_c,rd(mult(op_d,X1),ld(op_c,op_d)))),op_d),op_d),
inference(forward_demodulation,[],[f46635,f2555]) ).
fof(f46762,plain,
! [X0,X1] : mult(op_d,mult(op_c,mult(mult(X0,ld(op_c,op_d)),X1))) = mult(mult(mult(X0,op_d),mult(rd(mult(op_d,X1),ld(op_c,op_d)),op_d)),op_d),
inference(forward_demodulation,[],[f46736,f1341]) ).
fof(f46776,plain,
! [X0,X1] : mult(op_d,mult(op_c,mult(mult(X0,ld(op_c,op_d)),X1))) = mult(mult(mult(X0,op_d),op_d),mult(op_c,mult(op_d,X1))),
inference(forward_demodulation,[],[f46762,f46715]) ).
fof(f46830,plain,
! [X0,X1] : mult(op_d,mult(op_c,mult(mult(rd(X0,ld(op_c,op_d)),ld(op_c,op_d)),X1))) = mult(mult(op_d,mult(op_c,X0)),mult(op_c,mult(op_d,X1))),
inference(superposition,[],[f46776,f4784]) ).
fof(f46928,plain,
! [X0,X1] : mult(mult(op_d,mult(op_c,X0)),mult(op_c,mult(op_d,X1))) = mult(op_d,mult(op_c,mult(X0,X1))),
inference(forward_demodulation,[],[f46830,f3]) ).
fof(f47027,plain,
! [X0,X1] : mult(op_d,mult(op_c,mult(ld(op_c,X0),X1))) = mult(mult(op_d,X0),mult(op_c,mult(op_d,X1))),
inference(superposition,[],[f46928,f1]) ).
fof(f47388,plain,
! [X0,X1] : mult(op_d,mult(op_c,mult(ld(op_c,X1),mult(mult(X0,op_c),op_d)))) = mult(mult(op_d,X1),mult(op_c,ld(op_c,X0))),
inference(superposition,[],[f47027,f1152]) ).
fof(f47551,plain,
! [X0,X1] : mult(mult(op_d,X1),X0) = mult(op_d,mult(op_c,mult(ld(op_c,X1),mult(mult(X0,op_c),op_d)))),
inference(forward_demodulation,[],[f47388,f1]) ).
fof(f47619,plain,
! [X0,X1] : mult(mult(op_d,X1),X0) = mult(op_d,mult(op_c,mult(op_d,mult(mult(X1,mult(X0,op_c)),op_d)))),
inference(forward_demodulation,[],[f47551,f2080]) ).
fof(f47744,plain,
! [X0,X1] : mult(mult(op_d,X1),X0) = mult(op_d,rd(mult(X1,mult(X0,op_c)),op_c)),
inference(forward_demodulation,[],[f47619,f1151]) ).
fof(f47801,plain,
! [X0,X1] : mult(mult(op_d,op_c),mult(ld(mult(op_d,op_c),X1),X0)) = mult(mult(op_d,ld(op_d,X1)),X0),
inference(backward_demodulation,[],[f40922,f47744]) ).
fof(f47888,plain,
! [X0,X1] : mult(X1,X0) = mult(mult(op_d,op_c),mult(ld(mult(op_d,op_c),X1),X0)),
inference(forward_demodulation,[],[f47801,f1]) ).
fof(f48916,plain,
! [X0,X1] : mult(mult(op_d,ld(rd(unit,op_c),X0)),X1) = mult(op_d,rd(mult(op_c,mult(mult(X0,X1),op_c)),op_c)),
inference(superposition,[],[f47744,f11589]) ).
fof(f48973,plain,
! [X0,X1] : ld(op_d,mult(mult(op_d,X0),X1)) = rd(mult(X0,mult(X1,op_c)),op_c),
inference(superposition,[],[f2,f47744]) ).
fof(f49101,plain,
! [X0,X1] : mult(mult(op_d,ld(rd(unit,op_c),X0)),X1) = mult(op_d,ld(op_d,mult(mult(op_d,op_c),mult(X0,X1)))),
inference(forward_demodulation,[],[f48916,f48973]) ).
fof(f49172,plain,
! [X0,X1] : mult(mult(op_d,ld(rd(unit,op_c),X0)),X1) = mult(mult(op_d,op_c),mult(X0,X1)),
inference(forward_demodulation,[],[f49101,f1]) ).
fof(f49232,plain,
! [X0,X1] : mult(mult(mult(op_d,op_c),X0),X1) = mult(mult(op_d,op_c),mult(X0,X1)),
inference(forward_demodulation,[],[f49172,f26114]) ).
fof(f49373,plain,
! [X0,X1] : mult(mult(op_d,op_c),mult(mult(X0,mult(op_d,op_c)),X1)) = mult(mult(op_d,op_c),mult(X0,mult(mult(op_d,op_c),X1))),
inference(backward_demodulation,[],[f32021,f49232]) ).
fof(f49824,plain,
! [X0,X1] : mult(mult(op_d,op_c),mult(mult(ld(mult(op_d,op_c),X0),mult(op_d,op_c)),X1)) = mult(mult(rd(X0,rd(X0,mult(op_d,op_c))),X0),X1),
inference(superposition,[],[f49232,f14668]) ).
fof(f50129,plain,
! [X0,X1] : mult(mult(X0,mult(op_d,op_c)),X1) = mult(mult(op_d,op_c),mult(mult(ld(mult(op_d,op_c),X0),mult(op_d,op_c)),X1)),
inference(forward_demodulation,[],[f49824,f27319]) ).
fof(f50257,plain,
! [X0,X1] : mult(mult(X0,mult(op_d,op_c)),X1) = mult(mult(op_d,op_c),mult(ld(mult(op_d,op_c),X0),mult(mult(op_d,op_c),X1))),
inference(forward_demodulation,[],[f50129,f49373]) ).
fof(f50371,plain,
! [X0,X1] : mult(mult(X0,mult(op_d,op_c)),X1) = mult(X0,mult(mult(op_d,op_c),X1)),
inference(forward_demodulation,[],[f50257,f47888]) ).
fof(f50649,plain,
mult(a,mult(mult(op_d,op_c),b)) != mult(a,mult(mult(op_d,op_c),b)),
inference(backward_demodulation,[],[f11,f50371]) ).
fof(f50650,plain,
$false,
inference(trivial_inequality_removal,[],[f50649]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP662-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n008.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 10:33:56 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 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.45/13.19 % (1028416)Detected a unit-equality problem, will run specialized UEQ schedule.
% 87.45/13.19 % (1028421)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=2551700753:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 87.45/13.19 % (1028425)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3713681826:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 87.45/13.19 % (1028423)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=4269459988:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 87.45/13.19 % (1028422)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=178866131:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 87.45/13.19 % (1028424)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=4050832644:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 87.45/13.19 % (1028426)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3436245719:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 87.45/13.19 % (1028427)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3590046929:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 87.45/13.19 % (1028424)Instruction limit reached!
% 87.45/13.19 % (1028424)------------------------------
% 87.45/13.19 % (1028424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.45/13.19 % (1028424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.45/13.19 % (1028424)CaDiCaL version: 2.1.3
% 87.45/13.19 % (1028424)Termination reason: Instruction limit
% 87.45/13.19 % (1028424)Termination phase: Saturation
% 87.45/13.19 % (1028424)Time elapsed: 0.078 s
% 87.45/13.19 % (1028424)Peak memory usage: 89 MB
% 87.45/13.19 % (1028424)Instructions burned: 137 (million)
% 87.45/13.19 % (1028425)Instruction limit reached!
% 87.45/13.19 % (1028425)------------------------------
% 87.45/13.19 % (1028425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.45/13.19 % (1028425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.45/13.19 % (1028425)CaDiCaL version: 2.1.3
% 87.45/13.19 % (1028425)Termination reason: Instruction limit
% 87.45/13.19 % (1028425)Termination phase: Saturation
% 87.45/13.19 % (1028425)Time elapsed: 0.105 s
% 87.45/13.19 % (1028425)Peak memory usage: 89 MB
% 87.45/13.19 % (1028425)Instructions burned: 183 (million)
% 87.45/13.19 % (1028426)Instruction limit reached!
% 87.45/13.19 % (1028426)------------------------------
% 87.45/13.19 % (1028426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.45/13.19 % (1028426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.45/13.19 % (1028426)CaDiCaL version: 2.1.3
% 87.45/13.19 % (1028426)Termination reason: Instruction limit
% 87.45/13.19 % (1028426)Termination phase: Saturation
% 87.45/13.19 % (1028426)Time elapsed: 0.154 s
% 87.45/13.19 % (1028426)Peak memory usage: 90 MB
% 87.45/13.19 % (1028426)Instructions burned: 259 (million)
% 87.45/13.19 % (1028435)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1881564168:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 87.45/13.19 % (1028436)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=54424357:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 87.45/13.19 % (1028437)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2245692008:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 87.45/13.19 % (1028437)Instruction limit reached!
% 87.45/13.19 % (1028437)------------------------------
% 87.45/13.19 % (1028437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.45/13.19 % (1028437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.45/13.19 % (1028437)CaDiCaL version: 2.1.3
% 87.45/13.19 % (1028437)Termination reason: Instruction limit
% 87.45/13.19 % (1028437)Termination phase: Saturation
% 87.45/13.19 % (1028437)Time elapsed: 0.118 s
% 119.83/17.79 % (1028437)Peak memory usage: 90 MB
% 119.83/17.79 % (1028437)Instructions burned: 217 (million)
% 119.83/17.79 % (1028441)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=4100587492: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)
% 119.83/17.79 % (1028427)Instruction limit reached!
% 119.83/17.79 % (1028427)------------------------------
% 119.83/17.79 % (1028427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.79 % (1028427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.79 % (1028427)CaDiCaL version: 2.1.3
% 119.83/17.79 % (1028427)Termination reason: Instruction limit
% 119.83/17.79 % (1028427)Termination phase: Saturation
% 119.83/17.79 % (1028427)Time elapsed: 0.661 s
% 119.83/17.79 % (1028427)Peak memory usage: 102 MB
% 119.83/17.79 % (1028427)Instructions burned: 1188 (million)
% 119.83/17.79 % (1028441)Instruction limit reached!
% 119.83/17.79 % (1028441)------------------------------
% 119.83/17.79 % (1028441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.79 % (1028441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.79 % (1028441)CaDiCaL version: 2.1.3
% 119.83/17.79 % (1028441)Termination reason: Instruction limit
% 119.83/17.79 % (1028441)Termination phase: Saturation
% 119.83/17.79 % (1028441)Time elapsed: 0.203 s
% 119.83/17.79 % (1028441)Peak memory usage: 94 MB
% 119.83/17.79 % (1028441)Instructions burned: 318 (million)
% 119.83/17.79 % (1028443)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=2212583217:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 119.83/17.79 % (1028444)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=4209105664:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 119.83/17.79 % (1028435)Instruction limit reached!
% 119.83/17.79 % (1028435)------------------------------
% 119.83/17.79 % (1028435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.79 % (1028435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.79 % (1028435)CaDiCaL version: 2.1.3
% 119.83/17.79 % (1028435)Termination reason: Instruction limit
% 119.83/17.79 % (1028435)Termination phase: Saturation
% 119.83/17.79 % (1028435)Time elapsed: 1.295 s
% 119.83/17.79 % (1028435)Peak memory usage: 141 MB
% 119.83/17.79 % (1028435)Instructions burned: 2051 (million)
% 119.83/17.79 % (1028447)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2994620184:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2983 on theBenchmark for (2983ds/14534Mi)
% 119.83/17.79 % (1028444)Instruction limit reached!
% 119.83/17.79 % (1028444)------------------------------
% 119.83/17.79 % (1028444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.79 % (1028444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.79 % (1028444)CaDiCaL version: 2.1.3
% 119.83/17.79 % (1028444)Termination reason: Instruction limit
% 119.83/17.79 % (1028444)Termination phase: Saturation
% 119.83/17.79 % (1028444)Time elapsed: 1.923 s
% 119.83/17.79 % (1028444)Peak memory usage: 139 MB
% 119.83/17.79 % (1028444)Instructions burned: 2836 (million)
% 119.83/17.79 % (1028449)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=3552680408:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/11832Mi)
% 119.83/17.79 % (1028436)Instruction limit reached!
% 119.83/17.79 % (1028436)------------------------------
% 119.83/17.79 % (1028436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.79 % (1028436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.79 % (1028436)CaDiCaL version: 2.1.3
% 119.83/17.79 % (1028436)Termination reason: Instruction limit
% 119.83/17.79 % (1028436)Termination phase: Saturation
% 119.83/17.79 % (1028436)Time elapsed: 2.939 s
% 119.83/17.79 % (1028436)Peak memory usage: 170 MB
% 119.83/17.79 % (1028436)Instructions burned: 4950 (million)
% 119.83/17.79 % (1028451)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=54328268:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 119.83/17.79 % (1028451)Instruction limit reached!
% 119.83/17.79 % (1028451)------------------------------
% 119.83/17.79 % (1028451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.79 % (1028451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.79 % (1028451)CaDiCaL version: 2.1.3
% 119.83/17.79 % (1028451)Termination reason: Instruction limit
% 119.83/17.79 % (1028451)Termination phase: Saturation
% 119.83/17.79 % (1028451)Time elapsed: 1.333 s
% 119.83/17.79 % (1028451)Peak memory usage: 138 MB
% 119.83/17.79 % (1028451)Instructions burned: 2279 (million)
% 119.83/17.79 % (1028453)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=3617145468:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2952 on theBenchmark for (2952ds/6225Mi)
% 119.83/17.79 % (1028443)Instruction limit reached!
% 119.83/17.79 % (1028443)------------------------------
% 119.83/17.79 % (1028443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.79 % (1028443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.79 % (1028443)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028443)Termination reason: Instruction limit
% 119.83/17.80 % (1028443)Termination phase: Saturation
% 119.83/17.80 % (1028443)Time elapsed: 7.188 s
% 119.83/17.80 % (1028443)Peak memory usage: 245 MB
% 119.83/17.80 % (1028443)Instructions burned: 12126 (million)
% 119.83/17.80 % (1028456)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1641997130:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2918 on theBenchmark for (2918ds/21755Mi)
% 119.83/17.80 % (1028453)Instruction limit reached!
% 119.83/17.80 % (1028453)------------------------------
% 119.83/17.80 % (1028453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028453)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028453)Termination reason: Instruction limit
% 119.83/17.80 % (1028453)Termination phase: Saturation
% 119.83/17.80 % (1028453)Time elapsed: 3.423 s
% 119.83/17.80 % (1028453)Peak memory usage: 163 MB
% 119.83/17.80 % (1028453)Instructions burned: 6226 (million)
% 119.83/17.80 % (1028458)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=2411749586:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2916 on theBenchmark for (2916ds/16427Mi)
% 119.83/17.80 % (1028449)Instruction limit reached!
% 119.83/17.80 % (1028449)------------------------------
% 119.83/17.80 % (1028449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028449)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028449)Termination reason: Instruction limit
% 119.83/17.80 % (1028449)Termination phase: Saturation
% 119.83/17.80 % (1028449)Time elapsed: 7.548 s
% 119.83/17.80 % (1028449)Peak memory usage: 232 MB
% 119.83/17.80 % (1028449)Instructions burned: 11832 (million)
% 119.83/17.80 % (1028460)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=3847164314:i=9356:fgj=on:bd=preordered:av=off_2893 on theBenchmark for (2893ds/9356Mi)
% 119.83/17.80 % (1028447)Instruction limit reached!
% 119.83/17.80 % (1028447)------------------------------
% 119.83/17.80 % (1028447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028447)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028447)Termination reason: Instruction limit
% 119.83/17.80 % (1028447)Termination phase: Saturation
% 119.83/17.80 % (1028447)Time elapsed: 9.121 s
% 119.83/17.80 % (1028447)Peak memory usage: 258 MB
% 119.83/17.80 % (1028447)Instructions burned: 14535 (million)
% 119.83/17.80 % (1028462)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=2024396753:i=2070:kws=inv_precedence:slsql=off:bd=all_2890 on theBenchmark for (2890ds/2070Mi)
% 119.83/17.80 % (1028462)Instruction limit reached!
% 119.83/17.80 % (1028462)------------------------------
% 119.83/17.80 % (1028462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028462)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028462)Termination reason: Instruction limit
% 119.83/17.80 % (1028462)Termination phase: Saturation
% 119.83/17.80 % (1028462)Time elapsed: 1.251 s
% 119.83/17.80 % (1028462)Peak memory usage: 128 MB
% 119.83/17.80 % (1028462)Instructions burned: 2070 (million)
% 119.83/17.80 % (1028464)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=892037372:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2876 on theBenchmark for (2876ds/6461Mi)
% 119.83/17.80 % (1028464)Refutation not found, incomplete strategy
% 119.83/17.80 % (1028464)------------------------------
% 119.83/17.80 % (1028464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028464)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028464)Termination reason: Refutation not found, incomplete strategy
% 119.83/17.80 % (1028464)Time elapsed: 0.570 s
% 119.83/17.80 % (1028464)Peak memory usage: 127 MB
% 119.83/17.80 % (1028464)Instructions burned: 859 (million)
% 119.83/17.80 % (1028464)------------------------------
% 119.83/17.80 % (1028464)------------------------------
% 119.83/17.80 % (1028466)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=2567684093:i=2310:bd=all:ss=included_2867 on theBenchmark for (2867ds/2310Mi)
% 119.83/17.80 % (1028466)Instruction limit reached!
% 119.83/17.80 % (1028466)------------------------------
% 119.83/17.80 % (1028466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028466)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028466)Termination reason: Instruction limit
% 119.83/17.80 % (1028466)Termination phase: Saturation
% 119.83/17.80 % (1028466)Time elapsed: 1.258 s
% 119.83/17.80 % (1028466)Peak memory usage: 104 MB
% 119.83/17.80 % (1028466)Instructions burned: 2312 (million)
% 119.83/17.80 % (1028468)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=1636560233:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2853 on theBenchmark for (2853ds/2616Mi)
% 119.83/17.80 % (1028468)Refutation not found, incomplete strategy
% 119.83/17.80 % (1028468)------------------------------
% 119.83/17.80 % (1028468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028468)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028468)Termination reason: Refutation not found, incomplete strategy
% 119.83/17.80 % (1028468)Time elapsed: 0.001 s
% 119.83/17.80 % (1028468)Peak memory usage: 87 MB
% 119.83/17.80 % (1028468)------------------------------
% 119.83/17.80 % (1028468)------------------------------
% 119.83/17.80 % (1028470)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=1613003918:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2849 on theBenchmark for (2849ds/30521Mi)
% 119.83/17.80 % (1028460)Instruction limit reached!
% 119.83/17.80 % (1028460)------------------------------
% 119.83/17.80 % (1028460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.83/17.80 % (1028460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.83/17.80 % (1028460)CaDiCaL version: 2.1.3
% 119.83/17.80 % (1028460)Termination reason: Instruction limit
% 119.83/17.80 % (1028460)Termination phase: Saturation
% 119.83/17.80 % (1028460)Time elapsed: 5.276 s
% 119.83/17.80 % (1028460)Peak memory usage: 205 MB
% 119.83/17.80 % (1028460)Instructions burned: 9358 (million)
% 119.83/17.80 % (1028472)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=2707458353:i=3258:fgj=on:bd=all:ins=1_2839 on theBenchmark for (2839ds/3258Mi)
% 119.83/17.80 % (1028458)First to succeed.
% 119.83/17.80 % (1028458)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1028416"
% 119.83/17.80 % (1028458)Refutation found. Thanks to Tanya!
% 119.83/17.80 % SZS status Unsatisfiable for theBenchmark
% 119.83/17.80 % SZS output start Proof for theBenchmark
% See solution above
% 120.51/17.99 % (1028458)------------------------------
% 120.51/17.99 % (1028458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.51/17.99 % (1028458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.51/17.99 % (1028458)CaDiCaL version: 2.1.3
% 120.51/17.99 % (1028458)Termination reason: Refutation
% 120.51/17.99 % (1028458)Time elapsed: 8.118 s
% 120.51/17.99 % (1028458)Peak memory usage: 238 MB
% 120.51/17.99 % (1028458)Instructions burned: 12784 (million)
% 120.51/17.99 % (1028458)------------------------------
% 120.51/17.99 % (1028458)------------------------------
% 120.51/17.99 % (1028416)Success in time 16.921 s
% 120.51/17.99 % Vampire exiting
%------------------------------------------------------------------------------