%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP678-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 : n011.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:34 AM UTC 2026
% Result : Unsatisfiable 116.97s 33.23s
% Output : Refutation 227.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 14
% Syntax : Number of formulae : 217 ( 217 unt; 1 def)
% Number of atoms : 217 ( 213 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-3 aty)
% Number of variables : 539 ( 539 !; 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,
! [X2,X0,X1] : asoc(X0,X1,X2) = ld(mult(X0,mult(X1,X2)),mult(mult(X0,X1),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c09) ).
fof(f10,axiom,
! [X0,X1] : mult(op_c,mult(X0,X1)) = mult(mult(op_c,X0),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c10) ).
fof(f11,axiom,
! [X0,X1] : mult(X0,mult(op_c,X1)) = mult(mult(X0,op_c),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c11) ).
fof(f12,axiom,
! [X0,X1] : mult(X0,mult(X1,op_c)) = mult(mult(X0,X1),op_c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c12) ).
fof(f13,negated_conjecture,
mult(asoc(a,b,c),op_c) != mult(op_c,asoc(a,b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f14,definition,
~ sP0(mult(asoc(a,b,c),op_c)),
introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction]) ).
fof(f15,plain,
sP0(mult(op_c,asoc(a,b,c))),
inference(inequality_splitting,[],[f13,f14]) ).
fof(f21,plain,
! [X0,X1] : mult(X0,X1) = mult(op_c,mult(ld(op_c,X0),X1)),
inference(superposition,[],[f10,f1]) ).
fof(f54,plain,
! [X2,X0,X1] : ld(X2,mult(X1,X2)) = ld(mult(X0,X2),mult(mult(X0,X1),X2)),
inference(superposition,[],[f2,f8]) ).
fof(f71,plain,
! [X0,X1] : mult(op_c,X0) = mult(X1,ld(ld(op_c,X1),X0)),
inference(superposition,[],[f21,f1]) ).
fof(f76,plain,
! [X0,X1] : mult(ld(op_c,X0),X1) = ld(op_c,mult(X0,X1)),
inference(superposition,[],[f2,f21]) ).
fof(f82,plain,
! [X0,X1] : ld(op_c,X0) = mult(ld(op_c,X1),ld(X1,X0)),
inference(superposition,[],[f76,f1]) ).
fof(f104,plain,
! [X2,X0,X1] : asoc(X1,X2,ld(X2,X0)) = ld(mult(X1,X0),mult(mult(X1,X2),ld(X2,X0))),
inference(superposition,[],[f9,f1]) ).
fof(f147,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f148,plain,
! [X2,X0,X1] : mult(mult(X1,X2),ld(X2,X0)) = mult(mult(X1,rd(X0,X2)),X2),
inference(superposition,[],[f8,f3]) ).
fof(f151,plain,
! [X2,X0,X1] : asoc(X1,rd(X0,X2),X2) = ld(mult(X1,X0),mult(mult(X1,rd(X0,X2)),X2)),
inference(superposition,[],[f9,f3]) ).
fof(f152,plain,
! [X0,X1] : mult(X0,op_c) = mult(rd(X0,X1),mult(X1,op_c)),
inference(superposition,[],[f12,f3]) ).
fof(f153,plain,
! [X0,X1] : ld(op_c,X0) = mult(ld(op_c,rd(X0,X1)),X1),
inference(superposition,[],[f76,f3]) ).
fof(f167,plain,
! [X2,X0,X1] : asoc(X1,X2,ld(X2,X0)) = ld(mult(X1,X0),mult(mult(X1,rd(X0,X2)),X2)),
inference(backward_demodulation,[],[f104,f148]) ).
fof(f170,plain,
! [X2,X0,X1] : asoc(X1,X2,ld(X2,X0)) = asoc(X1,rd(X0,X2),X2),
inference(forward_demodulation,[],[f167,f151]) ).
fof(f178,plain,
! [X0] : ld(op_c,X0) = mult(ld(op_c,unit),X0),
inference(superposition,[],[f76,f6]) ).
fof(f179,plain,
! [X0] : ld(unit,X0) = X0,
inference(superposition,[],[f1,f6]) ).
fof(f180,plain,
! [X0,X1] : asoc(unit,X0,X1) = ld(mult(X0,X1),mult(mult(unit,X0),X1)),
inference(superposition,[],[f9,f6]) ).
fof(f182,plain,
! [X0,X1] : ld(mult(X0,X1),mult(X0,X1)) = asoc(unit,X0,X1),
inference(forward_demodulation,[],[f180,f6]) ).
fof(f239,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f240,plain,
! [X0,X1] : mult(X0,op_c) = rd(mult(X0,mult(op_c,X1)),X1),
inference(superposition,[],[f4,f11]) ).
fof(f241,plain,
! [X0,X1] : mult(op_c,X0) = rd(mult(op_c,mult(X0,X1)),X1),
inference(superposition,[],[f4,f10]) ).
fof(f244,plain,
! [X0] : unit = rd(X0,X0),
inference(superposition,[],[f4,f6]) ).
fof(f284,plain,
! [X0,X1] : mult(X1,op_c) = ld(rd(X0,X1),mult(X0,op_c)),
inference(superposition,[],[f2,f152]) ).
fof(f285,plain,
! [X0,X1] : rd(X0,X1) = rd(mult(X0,op_c),mult(X1,op_c)),
inference(superposition,[],[f4,f152]) ).
fof(f287,plain,
! [X2,X0,X1] : asoc(X1,rd(X0,X2),mult(X2,op_c)) = ld(mult(X1,mult(X0,op_c)),mult(mult(X1,rd(X0,X2)),mult(X2,op_c))),
inference(superposition,[],[f9,f152]) ).
fof(f315,plain,
! [X0,X1] : mult(X1,op_c) = ld(rd(rd(X0,op_c),X1),X0),
inference(superposition,[],[f284,f3]) ).
fof(f323,plain,
! [X0,X1] : rd(X0,mult(X1,op_c)) = rd(rd(X0,op_c),X1),
inference(superposition,[],[f285,f3]) ).
fof(f328,plain,
! [X0,X1] : rd(X1,rd(X0,op_c)) = rd(mult(X1,op_c),X0),
inference(superposition,[],[f285,f3]) ).
fof(f329,plain,
! [X0] : rd(X0,unit) = rd(mult(X0,op_c),op_c),
inference(superposition,[],[f285,f6]) ).
fof(f335,plain,
! [X0] : rd(X0,unit) = X0,
inference(forward_demodulation,[],[f329,f4]) ).
fof(f355,plain,
! [X0,X1] : rd(X0,X1) = rd(rd(X0,op_c),rd(X1,op_c)),
inference(superposition,[],[f328,f3]) ).
fof(f365,plain,
! [X0] : mult(X0,op_c) = rd(X0,rd(unit,op_c)),
inference(superposition,[],[f335,f328]) ).
fof(f377,plain,
! [X0,X1] : mult(X0,ld(mult(op_c,X0),X1)) = ld(op_c,X1),
inference(superposition,[],[f82,f2]) ).
fof(f401,plain,
! [X0,X1] : ld(op_c,mult(mult(op_c,X0),X1)) = mult(mult(X0,X1),asoc(op_c,X0,X1)),
inference(superposition,[],[f377,f9]) ).
fof(f405,plain,
! [X0,X1] : ld(mult(op_c,X1),X0) = ld(X1,ld(op_c,X0)),
inference(superposition,[],[f2,f377]) ).
fof(f439,plain,
! [X0,X1] : mult(ld(op_c,mult(op_c,X0)),X1) = mult(mult(X0,X1),asoc(op_c,X0,X1)),
inference(forward_demodulation,[],[f401,f76]) ).
fof(f449,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,X1),asoc(op_c,X0,X1)),
inference(forward_demodulation,[],[f439,f2]) ).
fof(f477,plain,
! [X0,X1] : mult(X0,asoc(op_c,rd(X0,X1),X1)) = X0,
inference(superposition,[],[f449,f3]) ).
fof(f487,plain,
! [X0,X1] : asoc(op_c,X0,X1) = ld(mult(X0,X1),mult(X0,X1)),
inference(superposition,[],[f2,f449]) ).
fof(f498,plain,
! [X0,X1] : asoc(op_c,X0,X1) = asoc(unit,X0,X1),
inference(forward_demodulation,[],[f487,f182]) ).
fof(f521,plain,
! [X0,X1] : mult(X0,asoc(unit,rd(X0,X1),X1)) = X0,
inference(backward_demodulation,[],[f477,f498]) ).
fof(f602,plain,
! [X0,X1] : ld(op_c,rd(X0,X1)) = rd(ld(op_c,X0),X1),
inference(superposition,[],[f4,f153]) ).
fof(f637,plain,
! [X0,X1] : ld(X0,X0) = asoc(unit,rd(X0,X1),X1),
inference(superposition,[],[f2,f521]) ).
fof(f672,plain,
! [X0,X1] : asoc(unit,rd(mult(op_c,X0),X1),X1) = ld(X0,ld(op_c,mult(op_c,X0))),
inference(superposition,[],[f405,f637]) ).
fof(f678,plain,
! [X0,X1] : ld(X0,X0) = asoc(unit,rd(mult(op_c,X0),X1),X1),
inference(forward_demodulation,[],[f672,f2]) ).
fof(f736,plain,
! [X0,X1] : mult(ld(X0,X1),op_c) = ld(X0,mult(X1,op_c)),
inference(superposition,[],[f284,f239]) ).
fof(f750,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),X2)) = mult(rd(X0,X1),mult(X1,X2)),
inference(superposition,[],[f7,f1]) ).
fof(f769,plain,
! [X2,X0,X1] : mult(rd(mult(X0,X1),X0),X0) = mult(X0,mult(X1,asoc(unit,rd(X0,X2),X2))),
inference(superposition,[],[f7,f521]) ).
fof(f785,plain,
! [X2,X0,X1] : mult(X0,X2) = ld(rd(mult(X0,X1),X0),mult(X0,mult(X1,X2))),
inference(superposition,[],[f2,f7]) ).
fof(f786,plain,
! [X2,X0,X1] : rd(mult(X0,X1),X0) = rd(mult(X0,mult(X1,X2)),mult(X0,X2)),
inference(superposition,[],[f4,f7]) ).
fof(f802,plain,
! [X2,X0,X1] : mult(X0,X1) = mult(X0,mult(X1,asoc(unit,rd(X0,X2),X2))),
inference(forward_demodulation,[],[f769,f3]) ).
fof(f873,plain,
! [X2,X0,X1] : ld(X0,mult(X0,X1)) = mult(X1,asoc(unit,rd(X0,X2),X2)),
inference(superposition,[],[f2,f802]) ).
fof(f903,plain,
! [X2,X0,X1] : mult(X1,asoc(unit,rd(X0,X2),X2)) = X1,
inference(forward_demodulation,[],[f873,f2]) ).
fof(f978,plain,
! [X0,X1] : unit = asoc(unit,rd(X0,X1),X1),
inference(superposition,[],[f6,f903]) ).
fof(f996,plain,
! [X0] : unit = ld(X0,X0),
inference(backward_demodulation,[],[f678,f978]) ).
fof(f1196,plain,
! [X2,X0,X1] : mult(ld(X1,X0),X2) = ld(X1,mult(rd(X0,X1),mult(X1,X2))),
inference(superposition,[],[f2,f750]) ).
fof(f1323,plain,
! [X2,X0,X1] : mult(mult(X1,rd(X2,ld(X1,X0))),ld(X1,X0)) = mult(X0,ld(ld(X1,X0),X2)),
inference(superposition,[],[f148,f1]) ).
fof(f1332,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X2)) = mult(mult(rd(X0,X1),rd(X2,X1)),X1),
inference(superposition,[],[f148,f3]) ).
fof(f1336,plain,
! [X2,X0,X1] : mult(mult(X1,rd(mult(X2,X0),X2)),X2) = mult(mult(X1,X2),X0),
inference(superposition,[],[f148,f2]) ).
fof(f1438,plain,
! [X0,X1] : rd(mult(op_c,X0),X1) = mult(op_c,rd(X0,X1)),
inference(superposition,[],[f241,f3]) ).
fof(f1547,plain,
! [X2,X0,X1] : ld(X1,mult(ld(X2,X0),X1)) = ld(mult(X2,X1),mult(X0,X1)),
inference(superposition,[],[f54,f1]) ).
fof(f1638,plain,
! [X2,X0,X1] : ld(op_c,mult(ld(X2,mult(X0,X1)),op_c)) = ld(mult(X2,op_c),mult(X0,mult(X1,op_c))),
inference(superposition,[],[f1547,f12]) ).
fof(f1639,plain,
! [X2,X0,X1] : ld(X1,mult(ld(X2,rd(X0,X1)),X1)) = ld(mult(X2,X1),X0),
inference(superposition,[],[f1547,f3]) ).
fof(f1665,plain,
! [X2,X0,X1] : ld(mult(X2,op_c),mult(X0,mult(X1,op_c))) = mult(ld(op_c,ld(X2,mult(X0,X1))),op_c),
inference(forward_demodulation,[],[f1638,f736]) ).
fof(f1890,plain,
! [X0] : rd(op_c,X0) = mult(op_c,rd(unit,X0)),
inference(superposition,[],[f1438,f5]) ).
fof(f1919,plain,
! [X0,X1] : mult(X1,op_c) = rd(mult(X1,X0),ld(op_c,X0)),
inference(superposition,[],[f240,f1]) ).
fof(f1963,plain,
! [X0,X1] : mult(X1,op_c) = rd(X0,ld(op_c,ld(X1,X0))),
inference(superposition,[],[f1919,f1]) ).
fof(f1974,plain,
! [X0,X1] : rd(X0,ld(op_c,X1)) = mult(rd(X0,X1),op_c),
inference(superposition,[],[f1919,f3]) ).
fof(f2041,plain,
! [X0,X1] : ld(mult(X0,op_c),X1) = ld(op_c,ld(X0,X1)),
inference(superposition,[],[f147,f1963]) ).
fof(f2059,plain,
! [X2,X0,X1] : mult(ld(op_c,ld(X2,mult(X0,X1))),op_c) = ld(op_c,ld(X2,mult(X0,mult(X1,op_c)))),
inference(backward_demodulation,[],[f1665,f2041]) ).
fof(f2104,plain,
! [X2,X0,X1] : rd(mult(X1,rd(X0,X2)),X1) = rd(mult(X1,X0),mult(X1,X2)),
inference(superposition,[],[f786,f3]) ).
fof(f2219,plain,
! [X2,X0,X1] : asoc(X1,rd(mult(X2,X0),X2),X2) = asoc(X1,X2,X0),
inference(superposition,[],[f170,f2]) ).
fof(f2293,plain,
! [X2,X0,X1] : ld(op_c,mult(ld(X2,rd(X0,X1)),op_c)) = ld(mult(X2,op_c),rd(X0,ld(op_c,X1))),
inference(superposition,[],[f1547,f1974]) ).
fof(f2298,plain,
! [X2,X0,X1] : ld(op_c,mult(ld(X2,rd(X0,X1)),op_c)) = ld(op_c,ld(X2,rd(X0,ld(op_c,X1)))),
inference(forward_demodulation,[],[f2293,f2041]) ).
fof(f2326,plain,
! [X2,X0,X1] : ld(op_c,ld(X2,rd(X0,ld(op_c,X1)))) = mult(ld(op_c,ld(X2,rd(X0,X1))),op_c),
inference(forward_demodulation,[],[f2298,f736]) ).
fof(f2367,plain,
! [X0,X1] : rd(X0,op_c) = mult(rd(X0,X1),rd(X1,op_c)),
inference(superposition,[],[f3,f355]) ).
fof(f2392,plain,
! [X2,X0,X1] : mult(ld(X1,X2),ld(X1,X0)) = ld(X1,mult(rd(X2,X1),X0)),
inference(superposition,[],[f1196,f1]) ).
fof(f2499,plain,
! [X2,X0,X1] : mult(X0,ld(X1,X2)) = ld(X1,mult(rd(mult(X1,X0),X1),X2)),
inference(superposition,[],[f2392,f2]) ).
fof(f2693,plain,
! [X0,X1] : ld(ld(op_c,X1),X0) = ld(X1,mult(op_c,X0)),
inference(superposition,[],[f2,f71]) ).
fof(f2715,plain,
! [X0] : mult(op_c,X0) = ld(ld(op_c,unit),X0),
inference(superposition,[],[f6,f71]) ).
fof(f2957,plain,
! [X0] : rd(unit,op_c) = ld(mult(X0,op_c),X0),
inference(superposition,[],[f147,f365]) ).
fof(f2974,plain,
! [X0] : rd(unit,op_c) = ld(op_c,ld(X0,X0)),
inference(forward_demodulation,[],[f2957,f2041]) ).
fof(f2993,plain,
ld(op_c,unit) = rd(unit,op_c),
inference(forward_demodulation,[],[f2974,f996]) ).
fof(f3001,plain,
! [X0] : mult(op_c,X0) = ld(rd(unit,op_c),X0),
inference(backward_demodulation,[],[f2715,f2993]) ).
fof(f3003,plain,
! [X0] : ld(op_c,X0) = mult(rd(unit,op_c),X0),
inference(backward_demodulation,[],[f178,f2993]) ).
fof(f3053,plain,
! [X0] : rd(rd(unit,op_c),rd(X0,op_c)) = rd(ld(op_c,op_c),X0),
inference(superposition,[],[f328,f3003]) ).
fof(f3058,plain,
! [X0] : ld(op_c,rd(op_c,X0)) = rd(rd(unit,op_c),rd(X0,op_c)),
inference(forward_demodulation,[],[f3053,f602]) ).
fof(f3087,plain,
! [X0] : rd(unit,X0) = ld(op_c,rd(op_c,X0)),
inference(forward_demodulation,[],[f3058,f355]) ).
fof(f3662,plain,
! [X0,X1] : mult(X0,ld(op_c,X1)) = mult(rd(X0,op_c),mult(rd(X1,op_c),op_c)),
inference(superposition,[],[f12,f1332]) ).
fof(f3700,plain,
! [X0,X1] : mult(X0,ld(op_c,X1)) = mult(rd(X0,op_c),X1),
inference(forward_demodulation,[],[f3662,f3]) ).
fof(f3826,plain,
! [X0,X1] : ld(op_c,X1) = ld(X0,mult(rd(X0,op_c),X1)),
inference(superposition,[],[f2,f3700]) ).
fof(f4974,plain,
! [X2,X0,X1] : ld(mult(X2,mult(X1,op_c)),X0) = ld(mult(X1,op_c),mult(ld(X2,rd(rd(X0,op_c),X1)),mult(X1,op_c))),
inference(superposition,[],[f1639,f323]) ).
fof(f5016,plain,
! [X0,X1] : mult(op_c,mult(ld(X0,rd(X1,rd(unit,op_c))),rd(unit,op_c))) = ld(mult(X0,rd(unit,op_c)),X1),
inference(superposition,[],[f3001,f1639]) ).
fof(f5039,plain,
! [X0,X1] : ld(mult(X0,rd(unit,op_c)),X1) = mult(op_c,mult(ld(X0,mult(X1,op_c)),rd(unit,op_c))),
inference(forward_demodulation,[],[f5016,f365]) ).
fof(f5074,plain,
! [X2,X0,X1] : ld(mult(X2,mult(X1,op_c)),X0) = ld(op_c,ld(X1,mult(ld(X2,rd(rd(X0,op_c),X1)),mult(X1,op_c)))),
inference(forward_demodulation,[],[f4974,f2041]) ).
fof(f5087,plain,
! [X0,X1] : ld(mult(X0,rd(unit,op_c)),X1) = mult(op_c,mult(mult(ld(X0,X1),op_c),rd(unit,op_c))),
inference(forward_demodulation,[],[f5039,f736]) ).
fof(f5115,plain,
! [X2,X0,X1] : ld(mult(X2,mult(X1,op_c)),X0) = mult(ld(op_c,ld(X1,mult(ld(X2,rd(rd(X0,op_c),X1)),X1))),op_c),
inference(forward_demodulation,[],[f5074,f2059]) ).
fof(f5125,plain,
! [X0,X1] : ld(mult(X0,rd(unit,op_c)),X1) = mult(op_c,mult(ld(X0,X1),mult(op_c,rd(unit,op_c)))),
inference(forward_demodulation,[],[f5087,f11]) ).
fof(f5144,plain,
! [X2,X0,X1] : ld(mult(X2,mult(X1,op_c)),X0) = mult(ld(op_c,ld(mult(X2,X1),rd(X0,op_c))),op_c),
inference(forward_demodulation,[],[f5115,f1639]) ).
fof(f5147,plain,
! [X0,X1] : ld(mult(X0,rd(unit,op_c)),X1) = mult(op_c,mult(ld(X0,X1),rd(op_c,op_c))),
inference(forward_demodulation,[],[f5125,f1890]) ).
fof(f5156,plain,
! [X2,X0,X1] : ld(mult(X2,mult(X1,op_c)),X0) = ld(op_c,ld(mult(X2,X1),rd(X0,ld(op_c,op_c)))),
inference(forward_demodulation,[],[f5144,f2326]) ).
fof(f5158,plain,
! [X0,X1] : ld(mult(X0,rd(unit,op_c)),X1) = mult(op_c,mult(ld(X0,X1),unit)),
inference(forward_demodulation,[],[f5147,f244]) ).
fof(f5163,plain,
! [X2,X0,X1] : ld(mult(X2,mult(X1,op_c)),X0) = ld(op_c,ld(mult(X2,X1),rd(X0,unit))),
inference(forward_demodulation,[],[f5156,f996]) ).
fof(f5164,plain,
! [X0,X1] : mult(op_c,ld(X0,X1)) = ld(mult(X0,rd(unit,op_c)),X1),
inference(forward_demodulation,[],[f5158,f5]) ).
fof(f5167,plain,
! [X2,X0,X1] : ld(mult(X2,mult(X1,op_c)),X0) = ld(op_c,ld(mult(X2,X1),X0)),
inference(forward_demodulation,[],[f5163,f335]) ).
fof(f5168,plain,
! [X2,X0,X1] : asoc(X1,rd(X0,X2),mult(X2,op_c)) = ld(op_c,ld(mult(X1,X0),mult(mult(X1,rd(X0,X2)),mult(X2,op_c)))),
inference(backward_demodulation,[],[f287,f5167]) ).
fof(f5171,plain,
! [X2,X0,X1] : asoc(X1,rd(X0,X2),mult(X2,op_c)) = mult(ld(op_c,ld(mult(X1,X0),mult(mult(X1,rd(X0,X2)),X2))),op_c),
inference(forward_demodulation,[],[f5168,f2059]) ).
fof(f5172,plain,
! [X2,X0,X1] : asoc(X1,rd(X0,X2),mult(X2,op_c)) = mult(ld(op_c,asoc(X1,rd(X0,X2),X2)),op_c),
inference(forward_demodulation,[],[f5171,f151]) ).
fof(f5174,plain,
! [X2,X0,X1] : mult(ld(X2,mult(X0,X1)),op_c) = ld(X2,mult(X0,mult(X1,op_c))),
inference(superposition,[],[f736,f12]) ).
fof(f5206,plain,
! [X2,X0,X1] : asoc(X2,rd(mult(X1,op_c),X0),X0) = asoc(X2,X0,mult(ld(X0,X1),op_c)),
inference(superposition,[],[f170,f736]) ).
fof(f5246,plain,
! [X2,X0,X1] : asoc(X2,X0,mult(ld(X0,X1),op_c)) = asoc(X2,rd(X1,rd(X0,op_c)),X0),
inference(forward_demodulation,[],[f5206,f328]) ).
fof(f5376,plain,
! [X2,X0,X1] : rd(mult(X1,rd(X2,ld(X1,X0))),X1) = rd(mult(X1,X2),X0),
inference(superposition,[],[f2104,f1]) ).
fof(f5577,plain,
! [X2,X3,X0,X1] : mult(rd(X1,ld(X0,X2)),ld(X0,X3)) = ld(X0,mult(rd(mult(X0,X1),X2),X3)),
inference(superposition,[],[f2499,f5376]) ).
fof(f5578,plain,
! [X2,X3,X0,X1] : asoc(X3,X0,rd(X1,ld(X0,X2))) = asoc(X3,rd(mult(X0,X1),X2),X0),
inference(superposition,[],[f2219,f5376]) ).
fof(f5582,plain,
! [X2,X0,X1] : mult(X0,rd(X1,ld(X0,X2))) = mult(rd(mult(X0,X1),X2),X0),
inference(superposition,[],[f3,f5376]) ).
fof(f5599,plain,
! [X2,X0,X1] : mult(X2,op_c) = ld(rd(rd(mult(op_c,X0),X1),X2),mult(op_c,rd(X0,ld(op_c,X1)))),
inference(superposition,[],[f315,f5376]) ).
fof(f5600,plain,
! [X2,X0,X1] : mult(X2,op_c) = ld(ld(op_c,rd(rd(mult(op_c,X0),X1),X2)),rd(X0,ld(op_c,X1))),
inference(forward_demodulation,[],[f5599,f2693]) ).
fof(f5645,plain,
! [X2,X0,X1] : mult(X2,op_c) = ld(ld(op_c,rd(mult(op_c,rd(X0,X1)),X2)),rd(X0,ld(op_c,X1))),
inference(forward_demodulation,[],[f5600,f1438]) ).
fof(f5679,plain,
! [X2,X0,X1] : mult(X2,op_c) = ld(ld(op_c,mult(op_c,rd(rd(X0,X1),X2))),rd(X0,ld(op_c,X1))),
inference(forward_demodulation,[],[f5645,f1438]) ).
fof(f5698,plain,
! [X2,X0,X1] : mult(X2,op_c) = ld(rd(rd(X0,X1),X2),rd(X0,ld(op_c,X1))),
inference(forward_demodulation,[],[f5679,f2]) ).
fof(f5746,plain,
! [X0] : rd(X0,op_c) = mult(X0,rd(unit,op_c)),
inference(superposition,[],[f2367,f335]) ).
fof(f5813,plain,
! [X0,X1] : ld(rd(X0,op_c),X1) = mult(op_c,ld(X0,X1)),
inference(backward_demodulation,[],[f5164,f5746]) ).
fof(f6016,plain,
! [X2,X0,X1] : ld(ld(op_c,X2),ld(X0,X1)) = ld(X2,ld(rd(X0,op_c),X1)),
inference(superposition,[],[f2693,f5813]) ).
fof(f6382,plain,
! [X2,X0,X1] : rd(mult(mult(X0,X1),X2),X1) = mult(X0,rd(mult(X1,X2),X1)),
inference(superposition,[],[f4,f1336]) ).
fof(f6600,plain,
! [X0,X1] : ld(op_c,rd(rd(op_c,X0),X1)) = rd(rd(unit,X0),X1),
inference(superposition,[],[f602,f3087]) ).
fof(f6602,plain,
! [X0,X1] : mult(X1,rd(unit,X0)) = mult(rd(X1,op_c),rd(op_c,X0)),
inference(superposition,[],[f3700,f3087]) ).
fof(f6902,plain,
! [X2,X0,X1] : mult(rd(X0,X2),X1) = mult(X1,rd(ld(X1,X0),ld(X1,X2))),
inference(superposition,[],[f5582,f1]) ).
fof(f7185,plain,
! [X2,X0,X1] : ld(rd(ld(op_c,X0),ld(op_c,X1)),ld(op_c,X2)) = ld(mult(rd(X0,X1),op_c),X2),
inference(superposition,[],[f405,f6902]) ).
fof(f7190,plain,
! [X2,X0,X1] : ld(op_c,ld(rd(X0,X1),X2)) = ld(rd(ld(op_c,X0),ld(op_c,X1)),ld(op_c,X2)),
inference(forward_demodulation,[],[f7185,f2041]) ).
fof(f7244,plain,
! [X2,X0,X1] : ld(op_c,ld(rd(X0,X1),X2)) = ld(ld(op_c,rd(X0,ld(op_c,X1))),ld(op_c,X2)),
inference(forward_demodulation,[],[f7190,f602]) ).
fof(f7279,plain,
! [X2,X0,X1] : ld(op_c,ld(rd(X0,X1),X2)) = ld(rd(X0,ld(op_c,X1)),ld(rd(op_c,op_c),X2)),
inference(forward_demodulation,[],[f7244,f6016]) ).
fof(f7298,plain,
! [X2,X0,X1] : ld(op_c,ld(rd(X0,X1),X2)) = ld(rd(X0,ld(op_c,X1)),ld(unit,X2)),
inference(forward_demodulation,[],[f7279,f244]) ).
fof(f7315,plain,
! [X2,X0,X1] : ld(rd(X0,ld(op_c,X1)),X2) = ld(op_c,ld(rd(X0,X1),X2)),
inference(forward_demodulation,[],[f7298,f179]) ).
fof(f7916,plain,
! [X0] : ld(op_c,unit) = ld(X0,rd(X0,op_c)),
inference(superposition,[],[f3826,f5]) ).
fof(f7990,plain,
! [X0] : rd(unit,op_c) = ld(X0,rd(X0,op_c)),
inference(forward_demodulation,[],[f7916,f2993]) ).
fof(f8072,plain,
! [X0,X1] : ld(X0,mult(rd(X1,X0),rd(X0,op_c))) = mult(ld(X0,X1),rd(unit,op_c)),
inference(superposition,[],[f2392,f7990]) ).
fof(f8099,plain,
! [X0,X1] : rd(ld(X0,X1),op_c) = ld(X0,mult(rd(X1,X0),rd(X0,op_c))),
inference(forward_demodulation,[],[f8072,f5746]) ).
fof(f8119,plain,
! [X0,X1] : ld(X0,rd(X1,op_c)) = rd(ld(X0,X1),op_c),
inference(forward_demodulation,[],[f8099,f2367]) ).
fof(f8331,plain,
! [X2,X0,X1] : mult(X1,ld(X2,X0)) = ld(rd(mult(X1,X2),X1),mult(X1,X0)),
inference(superposition,[],[f785,f1]) ).
fof(f8599,plain,
! [X2,X0,X1] : mult(X1,ld(ld(X1,X0),X2)) = ld(rd(X0,X1),mult(X1,X2)),
inference(superposition,[],[f8331,f1]) ).
fof(f8945,plain,
! [X2,X0,X1] : ld(ld(X1,X0),X2) = ld(X1,ld(rd(X0,X1),mult(X1,X2))),
inference(superposition,[],[f2,f8599]) ).
fof(f9343,plain,
! [X2,X0,X1] : ld(ld(X1,X2),ld(X1,X0)) = ld(X1,ld(rd(X2,X1),X0)),
inference(superposition,[],[f8945,f1]) ).
fof(f9648,plain,
! [X2,X0,X1] : ld(rd(ld(X0,X1),op_c),ld(X0,X2)) = mult(op_c,ld(X0,ld(rd(X1,X0),X2))),
inference(superposition,[],[f5813,f9343]) ).
fof(f9658,plain,
! [X2,X0,X1] : ld(rd(ld(X0,X1),op_c),ld(X0,X2)) = ld(rd(X0,op_c),ld(rd(X1,X0),X2)),
inference(forward_demodulation,[],[f9648,f5813]) ).
fof(f9702,plain,
! [X2,X0,X1] : ld(rd(X0,op_c),ld(rd(X1,X0),X2)) = ld(ld(X0,rd(X1,op_c)),ld(X0,X2)),
inference(forward_demodulation,[],[f9658,f8119]) ).
fof(f9723,plain,
! [X2,X0,X1] : ld(rd(X0,op_c),ld(rd(X1,X0),X2)) = ld(X0,ld(rd(rd(X1,op_c),X0),X2)),
inference(forward_demodulation,[],[f9702,f9343]) ).
fof(f12519,plain,
! [X2,X0,X1] : asoc(X1,rd(ld(X1,X0),X2),X2) = ld(X0,mult(mult(X1,rd(ld(X1,X0),X2)),X2)),
inference(superposition,[],[f151,f1]) ).
fof(f12544,plain,
! [X2,X0,X1] : asoc(rd(X0,X1),rd(X1,X2),X2) = ld(X0,mult(mult(rd(X0,X1),rd(X1,X2)),X2)),
inference(superposition,[],[f151,f3]) ).
fof(f15382,plain,
! [X2,X0,X1] : mult(rd(X0,X1),rd(mult(X1,X2),X1)) = rd(mult(X0,X2),X1),
inference(superposition,[],[f6382,f3]) ).
fof(f15714,plain,
! [X2,X3,X0,X1] : mult(rd(X3,X0),rd(mult(X0,X1),X2)) = rd(mult(X3,rd(X1,ld(X0,X2))),X0),
inference(superposition,[],[f15382,f5376]) ).
fof(f35076,plain,
! [X2,X0,X1] : mult(mult(rd(X0,X1),X2),ld(X2,X1)) = mult(X1,ld(ld(X2,X1),ld(X2,X0))),
inference(superposition,[],[f1323,f6902]) ).
fof(f35268,plain,
! [X2,X0,X1] : mult(mult(rd(X0,X1),X2),ld(X2,X1)) = mult(X1,ld(X2,ld(rd(X1,X2),X0))),
inference(forward_demodulation,[],[f35076,f9343]) ).
fof(f35345,plain,
! [X2,X0,X1] : mult(mult(rd(X0,X1),rd(X1,X2)),X2) = mult(X1,ld(X2,ld(rd(X1,X2),X0))),
inference(forward_demodulation,[],[f35268,f148]) ).
fof(f35404,plain,
! [X2,X0,X1] : asoc(rd(X0,X1),rd(X1,X2),X2) = ld(X0,mult(X1,ld(X2,ld(rd(X1,X2),X0)))),
inference(backward_demodulation,[],[f12544,f35345]) ).
fof(f35667,plain,
! [X2,X0,X1] : asoc(rd(X2,mult(X0,op_c)),rd(mult(X0,op_c),X1),X1) = ld(X2,mult(X0,mult(op_c,ld(X1,ld(rd(mult(X0,op_c),X1),X2))))),
inference(superposition,[],[f35404,f11]) ).
fof(f35732,plain,
! [X2,X0,X1] : asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2) = ld(op_c,ld(X0,mult(X1,ld(X2,ld(rd(X1,X2),mult(X0,op_c)))))),
inference(superposition,[],[f2041,f35404]) ).
fof(f35775,plain,
! [X2,X0,X1] : asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2) = ld(op_c,ld(X0,mult(X1,ld(X2,mult(ld(rd(X1,X2),X0),op_c))))),
inference(forward_demodulation,[],[f35732,f736]) ).
fof(f35802,plain,
! [X2,X0,X1] : asoc(rd(X2,mult(X0,op_c)),rd(mult(X0,op_c),X1),X1) = ld(X2,mult(X0,ld(rd(X1,op_c),ld(rd(mult(X0,op_c),X1),X2)))),
inference(forward_demodulation,[],[f35667,f5813]) ).
fof(f35865,plain,
! [X2,X0,X1] : asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2) = ld(op_c,ld(X0,mult(X1,mult(ld(X2,ld(rd(X1,X2),X0)),op_c)))),
inference(forward_demodulation,[],[f35775,f736]) ).
fof(f35888,plain,
! [X2,X0,X1] : asoc(rd(X2,mult(X0,op_c)),rd(mult(X0,op_c),X1),X1) = ld(X2,mult(X0,ld(X1,ld(rd(rd(mult(X0,op_c),op_c),X1),X2)))),
inference(forward_demodulation,[],[f35802,f9723]) ).
fof(f35946,plain,
! [X2,X0,X1] : asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2) = ld(op_c,mult(ld(X0,mult(X1,ld(X2,ld(rd(X1,X2),X0)))),op_c)),
inference(forward_demodulation,[],[f35865,f5174]) ).
fof(f35968,plain,
! [X2,X0,X1] : asoc(rd(X2,mult(X0,op_c)),rd(mult(X0,op_c),X1),X1) = ld(X2,mult(X0,ld(X1,ld(rd(X0,X1),X2)))),
inference(forward_demodulation,[],[f35888,f4]) ).
fof(f36018,plain,
! [X2,X0,X1] : asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2) = mult(ld(op_c,ld(X0,mult(X1,ld(X2,ld(rd(X1,X2),X0))))),op_c),
inference(forward_demodulation,[],[f35946,f736]) ).
fof(f36034,plain,
! [X2,X0,X1] : asoc(rd(X2,X0),rd(X0,X1),X1) = asoc(rd(X2,mult(X0,op_c)),rd(mult(X0,op_c),X1),X1),
inference(forward_demodulation,[],[f35968,f35404]) ).
fof(f36077,plain,
! [X2,X0,X1] : asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2) = mult(ld(op_c,asoc(rd(X0,X1),rd(X1,X2),X2)),op_c),
inference(forward_demodulation,[],[f36018,f35404]) ).
fof(f36086,plain,
! [X2,X0,X1] : asoc(rd(X2,X0),rd(X0,X1),X1) = asoc(rd(X2,mult(X0,op_c)),rd(X0,rd(X1,op_c)),X1),
inference(forward_demodulation,[],[f36034,f328]) ).
fof(f36115,plain,
! [X2,X0,X1] : asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2) = asoc(rd(X0,X1),rd(X1,X2),mult(X2,op_c)),
inference(forward_demodulation,[],[f36077,f5172]) ).
fof(f36124,plain,
! [X2,X0,X1] : asoc(rd(X2,X0),rd(X0,X1),X1) = asoc(rd(rd(X2,op_c),X0),rd(X0,rd(X1,op_c)),X1),
inference(forward_demodulation,[],[f36086,f323]) ).
fof(f36146,plain,
! [X2,X0,X1] : asoc(rd(X0,rd(X1,op_c)),rd(X1,X2),X2) = asoc(rd(X0,X1),rd(X1,X2),mult(X2,op_c)),
inference(forward_demodulation,[],[f36115,f328]) ).
fof(f60666,plain,
! [X2,X0,X1] : asoc(rd(rd(X1,op_c),X0),rd(mult(X0,op_c),X2),X2) = ld(X1,mult(mult(rd(rd(X1,op_c),X0),rd(mult(X0,op_c),X2)),X2)),
inference(superposition,[],[f12519,f315]) ).
fof(f60711,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3),X3) = ld(rd(X1,ld(op_c,X2)),mult(mult(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3)),X3)),
inference(superposition,[],[f12519,f5698]) ).
fof(f60942,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3),X3) = ld(op_c,ld(rd(X1,X2),mult(mult(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3)),X3))),
inference(forward_demodulation,[],[f60711,f7315]) ).
fof(f60962,plain,
! [X2,X0,X1] : asoc(rd(rd(X1,op_c),X0),rd(mult(X0,op_c),X2),X2) = ld(X1,mult(rd(mult(rd(X1,op_c),rd(op_c,ld(X0,X2))),X0),X2)),
inference(forward_demodulation,[],[f60666,f15714]) ).
fof(f61036,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3),X3) = ld(op_c,ld(rd(X1,X2),mult(rd(mult(rd(X1,X2),rd(op_c,ld(X0,X3))),X0),X3))),
inference(forward_demodulation,[],[f60942,f15714]) ).
fof(f61051,plain,
! [X2,X0,X1] : asoc(rd(rd(X1,op_c),X0),rd(mult(X0,op_c),X2),X2) = ld(X1,mult(rd(mult(X1,rd(unit,ld(X0,X2))),X0),X2)),
inference(forward_demodulation,[],[f60962,f6602]) ).
fof(f61111,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3),X3) = ld(op_c,mult(rd(rd(op_c,ld(X0,X3)),ld(rd(X1,X2),X0)),ld(rd(X1,X2),X3))),
inference(forward_demodulation,[],[f61036,f5577]) ).
fof(f61125,plain,
! [X2,X0,X1] : asoc(rd(rd(X1,op_c),X0),rd(mult(X0,op_c),X2),X2) = mult(rd(rd(unit,ld(X0,X2)),ld(X1,X0)),ld(X1,X2)),
inference(forward_demodulation,[],[f61051,f5577]) ).
fof(f61168,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3),X3) = mult(ld(op_c,rd(rd(op_c,ld(X0,X3)),ld(rd(X1,X2),X0))),ld(rd(X1,X2),X3)),
inference(forward_demodulation,[],[f61111,f76]) ).
fof(f61180,plain,
! [X2,X0,X1] : asoc(rd(rd(X1,op_c),X0),rd(X0,rd(X2,op_c)),X2) = mult(rd(rd(unit,ld(X0,X2)),ld(X1,X0)),ld(X1,X2)),
inference(forward_demodulation,[],[f61125,f328]) ).
fof(f61212,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(mult(X0,op_c),X3),X3) = mult(rd(rd(unit,ld(X0,X3)),ld(rd(X1,X2),X0)),ld(rd(X1,X2),X3)),
inference(forward_demodulation,[],[f61168,f6600]) ).
fof(f61221,plain,
! [X2,X0,X1] : asoc(rd(X1,X0),rd(X0,X2),X2) = mult(rd(rd(unit,ld(X0,X2)),ld(X1,X0)),ld(X1,X2)),
inference(forward_demodulation,[],[f61180,f36124]) ).
fof(f61242,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(X0,rd(X3,op_c)),X3) = mult(rd(rd(unit,ld(X0,X3)),ld(rd(X1,X2),X0)),ld(rd(X1,X2),X3)),
inference(forward_demodulation,[],[f61212,f328]) ).
fof(f61258,plain,
! [X2,X3,X0,X1] : asoc(rd(rd(X1,X2),X0),rd(X0,rd(X3,op_c)),X3) = asoc(rd(rd(X1,X2),X0),rd(X0,X3),X3),
inference(forward_demodulation,[],[f61242,f61221]) ).
fof(f61270,plain,
! [X2,X0,X1] : asoc(rd(X2,X0),rd(X0,X1),X1) = asoc(rd(rd(X2,op_c),X0),rd(X0,X1),X1),
inference(backward_demodulation,[],[f36124,f61258]) ).
fof(f61338,plain,
! [X2,X0,X1] : asoc(rd(X0,X1),rd(X1,X2),X2) = asoc(rd(mult(X0,op_c),X1),rd(X1,X2),X2),
inference(superposition,[],[f61270,f4]) ).
fof(f61498,plain,
! [X2,X0,X1] : asoc(rd(X0,X1),rd(X1,X2),X2) = asoc(rd(X0,rd(X1,op_c)),rd(X1,X2),X2),
inference(forward_demodulation,[],[f61338,f328]) ).
fof(f61565,plain,
! [X2,X0,X1] : asoc(rd(X0,X1),rd(X1,X2),X2) = asoc(rd(X0,X1),rd(X1,X2),mult(X2,op_c)),
inference(backward_demodulation,[],[f36146,f61498]) ).
fof(f64340,plain,
! [X2,X0,X1] : asoc(X1,X0,mult(X2,op_c)) = mult(ld(op_c,asoc(X1,X0,X2)),op_c),
inference(superposition,[],[f5172,f4]) ).
fof(f64728,plain,
! [X2,X0,X1] : mult(ld(op_c,asoc(X0,rd(X1,X2),X2)),op_c) = asoc(X0,X2,mult(ld(X2,X1),op_c)),
inference(superposition,[],[f64340,f170]) ).
fof(f64755,plain,
! [X2,X0,X1] : mult(op_c,asoc(X0,X1,mult(X2,op_c))) = mult(rd(asoc(X0,X1,X2),op_c),mult(op_c,op_c)),
inference(superposition,[],[f750,f64340]) ).
fof(f64872,plain,
! [X2,X0,X1] : mult(asoc(X0,X1,X2),op_c) = mult(op_c,asoc(X0,X1,mult(X2,op_c))),
inference(forward_demodulation,[],[f64755,f152]) ).
fof(f64899,plain,
! [X2,X0,X1] : mult(ld(op_c,asoc(X0,rd(X1,X2),X2)),op_c) = asoc(X0,rd(X1,rd(X2,op_c)),X2),
inference(forward_demodulation,[],[f64728,f5246]) ).
fof(f64956,plain,
! [X2,X0,X1] : asoc(X0,rd(X1,X2),mult(X2,op_c)) = asoc(X0,rd(X1,rd(X2,op_c)),X2),
inference(forward_demodulation,[],[f64899,f64340]) ).
fof(f65008,plain,
! [X2,X0,X1] : asoc(rd(X0,X1),rd(X1,X2),X2) = asoc(rd(X0,X1),rd(X1,rd(X2,op_c)),X2),
inference(backward_demodulation,[],[f61565,f64956]) ).
fof(f67260,plain,
! [X2,X0,X1] : asoc(X0,rd(X1,X2),X2) = asoc(X0,rd(X1,rd(X2,op_c)),X2),
inference(superposition,[],[f65008,f4]) ).
fof(f67426,plain,
! [X2,X0,X1] : asoc(X2,rd(X1,X0),X0) = asoc(X2,X0,mult(ld(X0,X1),op_c)),
inference(backward_demodulation,[],[f5246,f67260]) ).
fof(f67684,plain,
! [X2,X0,X1] : asoc(X1,rd(mult(X2,X0),X2),X2) = asoc(X1,X2,mult(X0,op_c)),
inference(superposition,[],[f67426,f2]) ).
fof(f67870,plain,
! [X2,X0,X1] : asoc(X1,X2,rd(X0,ld(X2,X2))) = asoc(X1,X2,mult(X0,op_c)),
inference(forward_demodulation,[],[f67684,f5578]) ).
fof(f67940,plain,
! [X2,X0,X1] : asoc(X1,X2,rd(X0,unit)) = asoc(X1,X2,mult(X0,op_c)),
inference(forward_demodulation,[],[f67870,f996]) ).
fof(f67985,plain,
! [X2,X0,X1] : asoc(X1,X2,X0) = asoc(X1,X2,mult(X0,op_c)),
inference(forward_demodulation,[],[f67940,f335]) ).
fof(f68046,plain,
! [X2,X0,X1] : mult(asoc(X0,X1,X2),op_c) = mult(op_c,asoc(X0,X1,X2)),
inference(backward_demodulation,[],[f64872,f67985]) ).
fof(f68237,plain,
~ sP0(mult(op_c,asoc(a,b,c))),
inference(backward_demodulation,[],[f14,f68046]) ).
fof(f68337,plain,
$false,
inference(forward_subsumption_resolution,[],[f68237,f15]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP678-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.45 % Computer : n011.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sun Sep 27 10:35:30 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.51 Running first-order theorem proving
% 0.24/0.51 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
% 122.57/18.50 % (2199751)Detected a unit-equality problem, will run specialized UEQ schedule.
% 122.57/18.50 % (2199759)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1007811293:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 122.57/18.50 % (2199756)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=2553780479:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 122.57/18.50 % (2199758)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2458565978:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 122.57/18.50 % (2199757)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=1775499115:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 122.57/18.50 % (2199761)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3097518618:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 122.57/18.50 % (2199760)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1038108202:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 122.57/18.50 % (2199759)Instruction limit reached!
% 122.57/18.50 % (2199759)------------------------------
% 122.57/18.50 % (2199759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.57/18.50 % (2199759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.57/18.50 % (2199759)CaDiCaL version: 2.1.3
% 122.57/18.50 % (2199759)Termination reason: Instruction limit
% 122.57/18.50 % (2199759)Termination phase: Saturation
% 122.57/18.50 % (2199759)Time elapsed: 0.071 s
% 122.57/18.50 % (2199759)Peak memory usage: 89 MB
% 122.57/18.50 % (2199759)Instructions burned: 137 (million)
% 122.57/18.50 % (2199762)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=139686984:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 122.57/18.50 % (2199760)Instruction limit reached!
% 122.57/18.50 % (2199760)------------------------------
% 122.57/18.50 % (2199760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.57/18.50 % (2199760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.57/18.50 % (2199760)CaDiCaL version: 2.1.3
% 122.57/18.50 % (2199760)Termination reason: Instruction limit
% 122.57/18.50 % (2199760)Termination phase: Saturation
% 122.57/18.50 % (2199760)Time elapsed: 0.183 s
% 122.57/18.50 % (2199760)Peak memory usage: 90 MB
% 122.57/18.50 % (2199760)Instructions burned: 181 (million)
% 122.57/18.50 % (2199769)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=985653453:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 122.57/18.50 % (2199761)Instruction limit reached!
% 122.57/18.50 % (2199761)------------------------------
% 122.57/18.50 % (2199761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.57/18.50 % (2199761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.57/18.50 % (2199761)CaDiCaL version: 2.1.3
% 122.57/18.50 % (2199761)Termination reason: Instruction limit
% 122.57/18.50 % (2199761)Termination phase: Saturation
% 122.57/18.50 % (2199761)Time elapsed: 0.256 s
% 122.57/18.50 % (2199761)Peak memory usage: 90 MB
% 122.57/18.50 % (2199761)Instructions burned: 258 (million)
% 122.57/18.50 % (2199771)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3648237001:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 122.57/18.50 % (2199773)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=205523848:i=215:ep=RSTC_2994 on theBenchmark for (2994ds/215Mi)
% 122.57/18.50 % (2199773)Instruction limit reached!
% 122.57/18.50 % (2199773)------------------------------
% 122.57/18.50 % (2199773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.57/18.50 % (2199773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.57/18.50 % (2199773)CaDiCaL version: 2.1.3
% 122.57/18.50 % (2199773)Termination reason: Instruction limit
% 122.57/18.50 % (2199773)Termination phase: Saturation
% 122.57/18.50 % (2199773)Time elapsed: 0.183 s
% 158.06/23.49 % (2199773)Peak memory usage: 90 MB
% 158.06/23.49 % (2199773)Instructions burned: 216 (million)
% 158.06/23.49 % (2199776)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=3292590810:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/317Mi)
% 158.06/23.49 % (2199762)Instruction limit reached!
% 158.06/23.49 % (2199762)------------------------------
% 158.06/23.49 % (2199762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 158.06/23.49 % (2199762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.06/23.49 % (2199762)CaDiCaL version: 2.1.3
% 158.06/23.49 % (2199762)Termination reason: Instruction limit
% 158.06/23.49 % (2199762)Termination phase: Saturation
% 158.06/23.49 % (2199762)Time elapsed: 1.113 s
% 158.06/23.49 % (2199762)Peak memory usage: 101 MB
% 158.06/23.49 % (2199762)Instructions burned: 1188 (million)
% 158.06/23.49 % (2199776)Instruction limit reached!
% 158.06/23.49 % (2199776)------------------------------
% 158.06/23.49 % (2199776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 158.06/23.49 % (2199776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.06/23.49 % (2199776)CaDiCaL version: 2.1.3
% 158.06/23.49 % (2199776)Termination reason: Instruction limit
% 158.06/23.49 % (2199776)Termination phase: Saturation
% 158.06/23.49 % (2199776)Time elapsed: 0.313 s
% 158.06/23.49 % (2199776)Peak memory usage: 93 MB
% 158.06/23.49 % (2199776)Instructions burned: 318 (million)
% 158.06/23.49 % (2199778)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=4251085307:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/12125Mi)
% 158.06/23.49 % (2199769)Instruction limit reached!
% 158.06/23.49 % (2199769)------------------------------
% 158.06/23.49 % (2199769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 158.06/23.49 % (2199769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.06/23.49 % (2199769)CaDiCaL version: 2.1.3
% 158.06/23.49 % (2199769)Termination reason: Instruction limit
% 158.06/23.49 % (2199769)Termination phase: Saturation
% 158.06/23.49 % (2199769)Time elapsed: 1.224 s
% 158.06/23.49 % (2199769)Peak memory usage: 141 MB
% 158.06/23.49 % (2199769)Instructions burned: 2052 (million)
% 158.06/23.49 % (2199779)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3283260660:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2983 on theBenchmark for (2983ds/2836Mi)
% 158.06/23.49 % (2199781)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2296276127:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2982 on theBenchmark for (2982ds/14534Mi)
% 158.06/23.49 % (2199779)Instruction limit reached!
% 158.06/23.49 % (2199779)------------------------------
% 158.06/23.49 % (2199779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 158.06/23.49 % (2199779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.06/23.49 % (2199779)CaDiCaL version: 2.1.3
% 158.06/23.49 % (2199779)Termination reason: Instruction limit
% 158.06/23.49 % (2199779)Termination phase: Saturation
% 158.06/23.49 % (2199779)Time elapsed: 3.100 s
% 158.06/23.49 % (2199779)Peak memory usage: 136 MB
% 158.06/23.49 % (2199779)Instructions burned: 2836 (million)
% 158.06/23.49 % (2199787)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=1227238382:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2949 on theBenchmark for (2949ds/11832Mi)
% 158.06/23.49 % (2199771)Instruction limit reached!
% 158.06/23.49 % (2199771)------------------------------
% 158.06/23.49 % (2199771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 158.06/23.49 % (2199771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 158.06/23.49 % (2199771)CaDiCaL version: 2.1.3
% 158.06/23.49 % (2199771)Termination reason: Instruction limit
% 158.06/23.49 % (2199771)Termination phase: Saturation
% 158.06/23.49 % (2199771)Time elapsed: 5.264 s
% 158.06/23.49 % (2199771)Peak memory usage: 167 MB
% 158.06/23.49 % (2199771)Instructions burned: 4949 (million)
% 158.06/23.49 % (2199789)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=2942328056:i=2279:fgj=on:bd=all_2939 on theBenchmark for (2939ds/2279Mi)
% 158.06/23.49 % (2199789)Instruction limit reached!
% 158.06/23.49 % (2199789)------------------------------
% 116.97/33.23 % (2199789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199789)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199789)Termination reason: Instruction limit
% 116.97/33.23 % (2199789)Termination phase: Saturation
% 116.97/33.23 % (2199789)Time elapsed: 2.341 s
% 116.97/33.23 % (2199789)Peak memory usage: 139 MB
% 116.97/33.23 % (2199789)Instructions burned: 2279 (million)
% 116.97/33.23 % (2199791)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=159333916:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2912 on theBenchmark for (2912ds/6225Mi)
% 116.97/33.23 % (2199781)Instruction limit reached!
% 116.97/33.23 % (2199781)------------------------------
% 116.97/33.23 % (2199781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199781)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199781)Termination reason: Instruction limit
% 116.97/33.23 % (2199781)Termination phase: Saturation
% 116.97/33.23 % (2199781)Time elapsed: 8.506 s
% 116.97/33.23 % (2199781)Peak memory usage: 255 MB
% 116.97/33.23 % (2199781)Instructions burned: 14535 (million)
% 116.97/33.23 % (2199793)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1522712315:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2895 on theBenchmark for (2895ds/21755Mi)
% 116.97/33.23 % (2199778)Instruction limit reached!
% 116.97/33.23 % (2199778)------------------------------
% 116.97/33.23 % (2199778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199778)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199778)Termination reason: Instruction limit
% 116.97/33.23 % (2199778)Termination phase: Saturation
% 116.97/33.23 % (2199778)Time elapsed: 11.795 s
% 116.97/33.23 % (2199778)Peak memory usage: 243 MB
% 116.97/33.23 % (2199778)Instructions burned: 12126 (million)
% 116.97/33.23 % (2199948)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=4012195476:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2864 on theBenchmark for (2864ds/16427Mi)
% 116.97/33.23 % (2199791)Instruction limit reached!
% 116.97/33.23 % (2199791)------------------------------
% 116.97/33.23 % (2199791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199791)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199791)Termination reason: Instruction limit
% 116.97/33.23 % (2199791)Termination phase: Saturation
% 116.97/33.23 % (2199791)Time elapsed: 5.007 s
% 116.97/33.23 % (2199791)Peak memory usage: 167 MB
% 116.97/33.23 % (2199791)Instructions burned: 6225 (million)
% 116.97/33.23 % (2199950)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=595445935:i=9356:fgj=on:bd=preordered:av=off_2859 on theBenchmark for (2859ds/9356Mi)
% 116.97/33.23 % (2199787)Instruction limit reached!
% 116.97/33.23 % (2199787)------------------------------
% 116.97/33.23 % (2199787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199787)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199787)Termination reason: Instruction limit
% 116.97/33.23 % (2199787)Termination phase: Saturation
% 116.97/33.23 % (2199787)Time elapsed: 10.623 s
% 116.97/33.23 % (2199787)Peak memory usage: 226 MB
% 116.97/33.23 % (2199787)Instructions burned: 11832 (million)
% 116.97/33.23 % (2199952)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=1756063609:i=2070:kws=inv_precedence:slsql=off:bd=all_2841 on theBenchmark for (2841ds/2070Mi)
% 116.97/33.23 % (2199952)Instruction limit reached!
% 116.97/33.23 % (2199952)------------------------------
% 116.97/33.23 % (2199952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199952)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199952)Termination reason: Instruction limit
% 116.97/33.23 % (2199952)Termination phase: Saturation
% 116.97/33.23 % (2199952)Time elapsed: 1.267 s
% 116.97/33.23 % (2199952)Peak memory usage: 127 MB
% 116.97/33.23 % (2199952)Instructions burned: 2071 (million)
% 116.97/33.23 % (2199954)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=31412269:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2827 on theBenchmark for (2827ds/6461Mi)
% 116.97/33.23 % (2199950)Instruction limit reached!
% 116.97/33.23 % (2199950)------------------------------
% 116.97/33.23 % (2199950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199950)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199950)Termination reason: Instruction limit
% 116.97/33.23 % (2199950)Termination phase: Saturation
% 116.97/33.23 % (2199950)Time elapsed: 5.545 s
% 116.97/33.23 % (2199950)Peak memory usage: 196 MB
% 116.97/33.23 % (2199950)Instructions burned: 9358 (million)
% 116.97/33.23 % (2199956)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=2585494245:i=2310:bd=all:ss=included_2802 on theBenchmark for (2802ds/2310Mi)
% 116.97/33.23 % (2199793)Instruction limit reached!
% 116.97/33.23 % (2199793)------------------------------
% 116.97/33.23 % (2199793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199793)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199793)Termination reason: Instruction limit
% 116.97/33.23 % (2199793)Termination phase: Saturation
% 116.97/33.23 % (2199793)Time elapsed: 9.454 s
% 116.97/33.23 % (2199793)Peak memory usage: 286 MB
% 116.97/33.23 % (2199793)Instructions burned: 21756 (million)
% 116.97/33.23 % (2199958)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=1501377398:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2798 on theBenchmark for (2798ds/2616Mi)
% 116.97/33.23 % (2199956)Instruction limit reached!
% 116.97/33.23 % (2199956)------------------------------
% 116.97/33.23 % (2199956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199956)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199956)Termination reason: Instruction limit
% 116.97/33.23 % (2199956)Termination phase: Saturation
% 116.97/33.23 % (2199956)Time elapsed: 1.200 s
% 116.97/33.23 % (2199956)Peak memory usage: 104 MB
% 116.97/33.23 % (2199956)Instructions burned: 2312 (million)
% 116.97/33.23 % (2199958)Instruction limit reached!
% 116.97/33.23 % (2199958)------------------------------
% 116.97/33.23 % (2199958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199958)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199958)Termination reason: Instruction limit
% 116.97/33.23 % (2199958)Termination phase: Saturation
% 116.97/33.23 % (2199958)Time elapsed: 0.822 s
% 116.97/33.23 % (2199958)Peak memory usage: 122 MB
% 116.97/33.23 % (2199958)Instructions burned: 2617 (million)
% 116.97/33.23 % (2199960)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3079113758:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2788 on theBenchmark for (2788ds/30521Mi)
% 116.97/33.23 % (2199961)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=818575871:i=3258:fgj=on:bd=all:ins=1_2788 on theBenchmark for (2788ds/3258Mi)
% 116.97/33.23 % (2199954)Instruction limit reached!
% 116.97/33.23 % (2199954)------------------------------
% 116.97/33.23 % (2199954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199954)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199954)Termination reason: Instruction limit
% 116.97/33.23 % (2199954)Termination phase: Saturation
% 116.97/33.23 % (2199954)Time elapsed: 4.066 s
% 116.97/33.23 % (2199954)Peak memory usage: 176 MB
% 116.97/33.23 % (2199954)Instructions burned: 6461 (million)
% 116.97/33.23 % (2199964)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=2981895823:i=5037:kws=precedence_2784 on theBenchmark for (2784ds/5037Mi)
% 116.97/33.23 % (2199961)Instruction limit reached!
% 116.97/33.23 % (2199961)------------------------------
% 116.97/33.23 % (2199961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199961)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199961)Termination reason: Instruction limit
% 116.97/33.23 % (2199961)Termination phase: Saturation
% 116.97/33.23 % (2199961)Time elapsed: 0.994 s
% 116.97/33.23 % (2199961)Peak memory usage: 144 MB
% 116.97/33.23 % (2199961)Instructions burned: 3262 (million)
% 116.97/33.23 % (2199966)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=629792478:i=65240_2777 on theBenchmark for (2777ds/65240Mi)
% 116.97/33.23 % (2199948)Instruction limit reached!
% 116.97/33.23 % (2199948)------------------------------
% 116.97/33.23 % (2199948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199948)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199948)Termination reason: Instruction limit
% 116.97/33.23 % (2199948)Termination phase: Saturation
% 116.97/33.23 % (2199948)Time elapsed: 10.605 s
% 116.97/33.23 % (2199948)Peak memory usage: 266 MB
% 116.97/33.23 % (2199948)Instructions burned: 16427 (million)
% 116.97/33.23 % (2199968)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=784446314:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2756 on theBenchmark for (2756ds/16502Mi)
% 116.97/33.23 % (2199964)Instruction limit reached!
% 116.97/33.23 % (2199964)------------------------------
% 116.97/33.23 % (2199964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199964)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199964)Termination reason: Instruction limit
% 116.97/33.23 % (2199964)Termination phase: Saturation
% 116.97/33.23 % (2199964)Time elapsed: 3.075 s
% 116.97/33.23 % (2199964)Peak memory usage: 169 MB
% 116.97/33.23 % (2199964)Instructions burned: 5045 (million)
% 116.97/33.23 % (2199970)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=973913383:i=7623:bd=preordered:er=filter_2752 on theBenchmark for (2752ds/7623Mi)
% 116.97/33.23 % (2199970)Instruction limit reached!
% 116.97/33.23 % (2199970)------------------------------
% 116.97/33.23 % (2199970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.97/33.23 % (2199970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.97/33.23 % (2199970)CaDiCaL version: 2.1.3
% 116.97/33.23 % (2199970)Termination reason: Instruction limit
% 116.97/33.23 % (2199970)Termination phase: Saturation
% 116.97/33.23 % (2199970)Time elapsed: 4.450 s
% 116.97/33.23 % (2199970)Peak memory usage: 179 MB
% 116.97/33.23 % (2199970)Instructions burned: 7623 (million)
% 116.97/33.23 % (2200224)dis+1010_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:tgt=full:npcc=on:sp=const_min:spb=non_intro:lcm=predicate:acc=on:urr=ec_only:rp=on:gs=on:random_seed=900342658:i=8183:kws=frequency:add=off:gsp=on_2705 on theBenchmark for (2705ds/8183Mi)
% 116.97/33.23 % (2199968)First to succeed.
% 116.97/33.23 % (2199968)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2199751"
% 116.97/33.23 % (2199968)Refutation found. Thanks to Tanya!
% 116.97/33.23 % SZS status Unsatisfiable for theBenchmark
% 116.97/33.23 % SZS output start Proof for theBenchmark
% See solution above
% 227.83/33.42 % (2199968)------------------------------
% 227.83/33.42 % (2199968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 227.83/33.42 % (2199968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 227.83/33.42 % (2199968)CaDiCaL version: 2.1.3
% 227.83/33.42 % (2199968)Termination reason: Refutation
% 227.83/33.42 % (2199968)Time elapsed: 7.166 s
% 227.83/33.42 % (2199968)Peak memory usage: 222 MB
% 227.83/33.42 % (2199968)Instructions burned: 10928 (million)
% 227.83/33.42 % (2199968)------------------------------
% 227.83/33.42 % (2199968)------------------------------
% 227.83/33.42 % (2199751)Success in time 32.009 s
% 227.83/33.42 % Vampire exiting
%------------------------------------------------------------------------------