%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP668-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:33 AM UTC 2026
% Result : Unsatisfiable 5.81s 1.99s
% Output : Refutation 8.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 17
% Syntax : Number of formulae : 124 ( 124 unt; 8 def)
% Number of atoms : 124 ( 123 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 130 ( 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).
fof(f2,negated_conjecture,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).
fof(f3,negated_conjecture,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).
fof(f4,negated_conjecture,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).
fof(f5,negated_conjecture,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).
fof(f6,negated_conjecture,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X1,X2))) = mult(mult(mult(X0,X1),X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).
fof(f8,axiom,
! [X0,X1] : mult(mult(X0,X1),X0) = mult(X0,mult(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).
fof(f9,negated_conjecture,
mult(mult(a,b),mult(mult(c,b),c)) != mult(mult(a,mult(mult(b,c),b)),c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f10,definition,
sF0 = mult(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f11,plain,
mult(a,b) = sF0,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF1 = mult(c,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f13,plain,
mult(c,b) = sF1,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF2 = mult(sF1,c),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f15,plain,
mult(sF1,c) = sF2,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF3 = mult(sF0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f17,plain,
mult(sF0,sF2) = sF3,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF4 = mult(b,c),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f19,plain,
mult(b,c) = sF4,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF5 = mult(sF4,b),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f21,plain,
mult(sF4,b) = sF5,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF6 = mult(a,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f23,plain,
mult(a,sF5) = sF6,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF7 = mult(sF6,c),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f25,plain,
mult(sF6,c) = sF7,
inference(reorient_equations,[],[f24]) ).
fof(f26,plain,
sF3 != sF7,
inference(definition_folding,[],[f9,f25,f23,f21,f19,f17,f15,f13,f11]) ).
fof(f32,plain,
b = ld(sF4,sF5),
inference(superposition,[],[f2,f21]) ).
fof(f35,plain,
! [X0,X1] : mult(X0,X1) = mult(X1,mult(ld(X1,X0),X1)),
inference(superposition,[],[f8,f1]) ).
fof(f40,plain,
mult(sF1,c) = mult(c,mult(b,c)),
inference(superposition,[],[f8,f13]) ).
fof(f46,plain,
mult(sF1,c) = mult(c,sF4),
inference(forward_demodulation,[],[f40,f19]) ).
fof(f48,plain,
sF2 = mult(c,sF4),
inference(forward_demodulation,[],[f46,f15]) ).
fof(f53,plain,
sF4 = ld(c,sF2),
inference(superposition,[],[f2,f48]) ).
fof(f58,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f63,plain,
b = rd(sF4,c),
inference(superposition,[],[f4,f19]) ).
fof(f66,plain,
c = rd(sF2,sF4),
inference(superposition,[],[f4,f48]) ).
fof(f68,plain,
sF1 = rd(sF2,c),
inference(superposition,[],[f4,f15]) ).
fof(f72,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f77,plain,
! [X0] : unit = ld(X0,X0),
inference(superposition,[],[f2,f5]) ).
fof(f84,plain,
! [X2,X0,X1] : mult(X1,mult(ld(X1,X0),mult(ld(X1,X0),X2))) = mult(mult(X0,ld(X1,X0)),X2),
inference(superposition,[],[f7,f1]) ).
fof(f107,plain,
! [X2,X0,X1] : mult(mult(X0,X1),X1) = rd(mult(X0,mult(X1,mult(X1,X2))),X2),
inference(superposition,[],[f4,f7]) ).
fof(f111,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(X0,mult(X1,mult(X1,unit))),
inference(superposition,[],[f5,f7]) ).
fof(f112,plain,
! [X0,X1] : mult(mult(X0,X1),X1) = mult(X0,mult(X1,X1)),
inference(forward_demodulation,[],[f111,f5]) ).
fof(f120,plain,
! [X2,X0,X1] : rd(mult(X0,mult(X1,mult(X1,X2))),X2) = mult(X0,mult(X1,X1)),
inference(backward_demodulation,[],[f107,f112]) ).
fof(f123,plain,
! [X2,X0,X1] : mult(X0,mult(X1,mult(X1,X2))) = mult(mult(X0,mult(X1,X1)),X2),
inference(backward_demodulation,[],[f7,f112]) ).
fof(f133,plain,
! [X2,X0,X1] : mult(X0,X2) = mult(rd(X0,mult(X1,X1)),mult(X1,mult(X1,X2))),
inference(superposition,[],[f123,f3]) ).
fof(f336,plain,
! [X0,X1] : mult(X0,X1) = rd(mult(X0,mult(X1,X1)),X1),
inference(superposition,[],[f4,f112]) ).
fof(f366,plain,
! [X0,X1] : mult(ld(X1,X0),X1) = ld(X1,mult(X0,X1)),
inference(superposition,[],[f2,f35]) ).
fof(f400,plain,
! [X0,X1] : ld(X1,X0) = mult(ld(X1,rd(X0,X1)),X1),
inference(superposition,[],[f366,f3]) ).
fof(f401,plain,
! [X0] : ld(X0,X0) = mult(ld(X0,unit),X0),
inference(superposition,[],[f366,f6]) ).
fof(f422,plain,
! [X0] : unit = mult(ld(X0,unit),X0),
inference(forward_demodulation,[],[f401,f77]) ).
fof(f434,plain,
! [X0] : ld(X0,unit) = rd(unit,X0),
inference(superposition,[],[f4,f422]) ).
fof(f438,plain,
! [X0] : mult(unit,X0) = mult(ld(X0,unit),mult(X0,X0)),
inference(superposition,[],[f112,f422]) ).
fof(f439,plain,
! [X0,X1] : mult(X0,mult(ld(X1,unit),ld(X1,unit))) = rd(mult(X0,mult(ld(X1,unit),unit)),X1),
inference(superposition,[],[f120,f422]) ).
fof(f445,plain,
! [X0,X1] : mult(X0,mult(ld(X1,unit),ld(X1,unit))) = rd(mult(X0,ld(X1,unit)),X1),
inference(forward_demodulation,[],[f439,f5]) ).
fof(f446,plain,
! [X0] : mult(ld(X0,unit),mult(X0,X0)) = X0,
inference(forward_demodulation,[],[f438,f6]) ).
fof(f474,plain,
! [X0] : ld(X0,unit) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f4,f446]) ).
fof(f479,plain,
! [X0,X1] : mult(X1,mult(ld(X0,unit),ld(X0,unit))) = rd(mult(X1,mult(ld(X0,unit),X0)),mult(X0,X0)),
inference(superposition,[],[f120,f446]) ).
fof(f481,plain,
! [X0,X1] : mult(X1,mult(ld(X0,unit),ld(X0,unit))) = rd(mult(X1,unit),mult(X0,X0)),
inference(forward_demodulation,[],[f479,f422]) ).
fof(f487,plain,
! [X0,X1] : mult(X1,mult(ld(X0,unit),ld(X0,unit))) = rd(X1,mult(X0,X0)),
inference(forward_demodulation,[],[f481,f5]) ).
fof(f490,plain,
! [X0,X1] : rd(X0,mult(X1,X1)) = rd(mult(X0,ld(X1,unit)),X1),
inference(backward_demodulation,[],[f445,f487]) ).
fof(f715,plain,
! [X0,X1] : rd(X0,X1) = mult(rd(X0,mult(X1,X1)),X1),
inference(superposition,[],[f336,f3]) ).
fof(f747,plain,
! [X2,X0,X1] : mult(X1,ld(X2,X0)) = mult(rd(X1,mult(X2,X2)),mult(X2,X0)),
inference(superposition,[],[f133,f1]) ).
fof(f750,plain,
! [X0,X1] : mult(X0,X1) = mult(rd(X0,mult(ld(X1,unit),ld(X1,unit))),mult(ld(X1,unit),unit)),
inference(superposition,[],[f133,f422]) ).
fof(f775,plain,
! [X2,X0,X1] : mult(X2,mult(X2,X1)) = ld(rd(X0,mult(X2,X2)),mult(X0,X1)),
inference(superposition,[],[f2,f133]) ).
fof(f776,plain,
! [X2,X0,X1] : rd(X0,mult(X2,X2)) = rd(mult(X0,X1),mult(X2,mult(X2,X1))),
inference(superposition,[],[f4,f133]) ).
fof(f795,plain,
! [X0,X1] : mult(X0,X1) = mult(rd(X0,mult(ld(X1,unit),ld(X1,unit))),ld(X1,unit)),
inference(forward_demodulation,[],[f750,f5]) ).
fof(f829,plain,
! [X0,X1] : mult(X0,X1) = rd(X0,ld(X1,unit)),
inference(forward_demodulation,[],[f795,f715]) ).
fof(f843,plain,
! [X2,X0,X1] : mult(X1,mult(X1,ld(X2,X0))) = ld(rd(X2,mult(X1,X1)),X0),
inference(superposition,[],[f775,f1]) ).
fof(f925,plain,
! [X0] : rd(a,mult(X0,X0)) = rd(sF0,mult(X0,mult(X0,b))),
inference(superposition,[],[f776,f11]) ).
fof(f926,plain,
! [X0] : rd(a,mult(X0,X0)) = rd(sF6,mult(X0,mult(X0,sF5))),
inference(superposition,[],[f776,f23]) ).
fof(f994,plain,
! [X2,X0,X1] : mult(X1,ld(X2,ld(X2,X0))) = mult(rd(X1,mult(X2,X2)),X0),
inference(superposition,[],[f747,f1]) ).
fof(f995,plain,
! [X0,X1] : mult(X1,ld(X0,unit)) = mult(rd(X1,mult(X0,X0)),X0),
inference(superposition,[],[f747,f5]) ).
fof(f1059,plain,
! [X0,X1] : rd(X1,X0) = mult(X1,ld(X0,unit)),
inference(forward_demodulation,[],[f995,f715]) ).
fof(f1105,plain,
! [X0,X1] : rd(X0,mult(X1,X1)) = rd(rd(X0,X1),X1),
inference(backward_demodulation,[],[f490,f1059]) ).
fof(f1521,plain,
! [X0,X1] : ld(X0,rd(X1,X0)) = rd(ld(X0,X1),X0),
inference(superposition,[],[f4,f400]) ).
fof(f2507,plain,
! [X0,X1] : ld(X1,unit) = ld(X0,rd(X0,X1)),
inference(superposition,[],[f2,f1059]) ).
fof(f2705,plain,
! [X0,X1] : ld(X1,unit) = ld(mult(X0,X1),X0),
inference(superposition,[],[f2507,f4]) ).
fof(f2715,plain,
ld(sF4,unit) = ld(sF2,c),
inference(superposition,[],[f2507,f66]) ).
fof(f2716,plain,
ld(c,unit) = ld(sF2,sF1),
inference(superposition,[],[f2507,f68]) ).
fof(f2717,plain,
ld(sF4,b) = ld(c,unit),
inference(superposition,[],[f2507,f63]) ).
fof(f2736,plain,
ld(sF4,b) = ld(sF2,sF1),
inference(backward_demodulation,[],[f2717,f2716]) ).
fof(f2775,plain,
ld(c,unit) = ld(sF7,sF6),
inference(superposition,[],[f2705,f25]) ).
fof(f2793,plain,
ld(sF2,sF1) = ld(sF7,sF6),
inference(forward_demodulation,[],[f2775,f2716]) ).
fof(f2810,plain,
sF7 = rd(sF6,ld(sF2,sF1)),
inference(superposition,[],[f58,f2793]) ).
fof(f2840,plain,
! [X0] : rd(X0,sF4) = mult(X0,ld(sF2,c)),
inference(superposition,[],[f1059,f2715]) ).
fof(f2845,plain,
ld(sF4,rd(unit,sF4)) = rd(ld(sF2,c),sF4),
inference(superposition,[],[f1521,f2715]) ).
fof(f2853,plain,
ld(sF4,ld(sF4,unit)) = rd(ld(sF2,c),sF4),
inference(forward_demodulation,[],[f2845,f434]) ).
fof(f2858,plain,
ld(sF4,ld(sF2,c)) = rd(ld(sF2,c),sF4),
inference(forward_demodulation,[],[f2853,f2715]) ).
fof(f2870,plain,
! [X0,X1] : mult(X0,mult(ld(sF2,c),mult(ld(sF2,c),X1))) = mult(mult(X0,rd(ld(sF2,c),sF4)),X1),
inference(superposition,[],[f123,f2840]) ).
fof(f2901,plain,
! [X0] : mult(X0,mult(ld(sF2,c),ld(sF2,c))) = rd(mult(X0,ld(sF2,c)),sF4),
inference(superposition,[],[f112,f2840]) ).
fof(f2911,plain,
! [X0] : mult(X0,mult(ld(sF2,c),ld(sF2,c))) = rd(rd(X0,sF4),sF4),
inference(forward_demodulation,[],[f2901,f2840]) ).
fof(f2936,plain,
! [X0,X1] : mult(X0,mult(ld(sF2,c),mult(ld(sF2,c),X1))) = mult(mult(X0,ld(sF4,ld(sF2,c))),X1),
inference(forward_demodulation,[],[f2870,f2858]) ).
fof(f2944,plain,
! [X0] : rd(X0,mult(sF4,sF4)) = mult(X0,mult(ld(sF2,c),ld(sF2,c))),
inference(forward_demodulation,[],[f2911,f1105]) ).
fof(f2962,plain,
! [X0] : rd(X0,mult(sF4,sF4)) = mult(X0,rd(ld(sF2,c),sF4)),
inference(forward_demodulation,[],[f2944,f2840]) ).
fof(f2968,plain,
! [X0] : rd(X0,mult(sF4,sF4)) = mult(X0,ld(sF4,ld(sF2,c))),
inference(forward_demodulation,[],[f2962,f2858]) ).
fof(f2974,plain,
! [X0,X1] : mult(X0,mult(ld(sF2,c),mult(ld(sF2,c),X1))) = mult(rd(X0,mult(sF4,sF4)),X1),
inference(backward_demodulation,[],[f2936,f2968]) ).
fof(f2980,plain,
! [X0,X1] : mult(X0,mult(ld(sF2,c),mult(ld(sF2,c),X1))) = mult(X0,ld(sF4,ld(sF4,X1))),
inference(forward_demodulation,[],[f2974,f994]) ).
fof(f3165,plain,
! [X0] : mult(sF4,mult(ld(sF2,c),mult(ld(sF2,c),X0))) = mult(mult(unit,ld(sF2,c)),X0),
inference(superposition,[],[f84,f2715]) ).
fof(f3221,plain,
! [X0] : mult(ld(sF2,c),X0) = mult(sF4,mult(ld(sF2,c),mult(ld(sF2,c),X0))),
inference(forward_demodulation,[],[f3165,f6]) ).
fof(f3235,plain,
! [X0] : mult(ld(sF2,c),X0) = mult(sF4,ld(sF4,ld(sF4,X0))),
inference(forward_demodulation,[],[f3221,f2980]) ).
fof(f3246,plain,
! [X0] : mult(ld(sF2,c),X0) = ld(sF4,X0),
inference(forward_demodulation,[],[f3235,f1]) ).
fof(f3409,plain,
rd(a,mult(ld(sF2,c),ld(sF2,c))) = rd(sF0,mult(ld(sF2,c),ld(sF4,b))),
inference(superposition,[],[f925,f3246]) ).
fof(f3412,plain,
rd(a,mult(ld(sF2,c),ld(sF2,c))) = rd(sF6,mult(ld(sF2,c),ld(sF4,sF5))),
inference(superposition,[],[f926,f3246]) ).
fof(f3413,plain,
rd(a,mult(ld(sF2,c),ld(sF2,c))) = rd(sF6,ld(sF4,ld(sF4,sF5))),
inference(forward_demodulation,[],[f3412,f3246]) ).
fof(f3416,plain,
rd(a,mult(ld(sF2,c),ld(sF2,c))) = rd(sF0,ld(sF4,ld(sF4,b))),
inference(forward_demodulation,[],[f3409,f3246]) ).
fof(f3466,plain,
rd(a,mult(ld(sF2,c),ld(sF2,c))) = rd(sF6,ld(sF4,b)),
inference(forward_demodulation,[],[f3413,f32]) ).
fof(f3469,plain,
rd(a,mult(ld(sF2,c),ld(sF2,c))) = rd(sF0,ld(sF4,ld(sF2,sF1))),
inference(forward_demodulation,[],[f3416,f2736]) ).
fof(f3512,plain,
rd(sF6,ld(sF2,sF1)) = rd(a,mult(ld(sF2,c),ld(sF2,c))),
inference(forward_demodulation,[],[f3466,f2736]) ).
fof(f3513,plain,
rd(sF0,ld(sF4,ld(sF2,sF1))) = rd(a,ld(sF4,ld(sF2,c))),
inference(forward_demodulation,[],[f3469,f3246]) ).
fof(f3544,plain,
rd(sF6,ld(sF2,sF1)) = rd(a,ld(sF4,ld(sF2,c))),
inference(forward_demodulation,[],[f3512,f3246]) ).
fof(f3557,plain,
sF7 = rd(a,ld(sF4,ld(sF2,c))),
inference(forward_demodulation,[],[f3544,f2810]) ).
fof(f3566,plain,
sF7 = rd(sF0,ld(sF4,ld(sF2,sF1))),
inference(backward_demodulation,[],[f3513,f3557]) ).
fof(f3934,plain,
! [X0,X1] : mult(X0,mult(X0,ld(X0,X1))) = ld(ld(X0,unit),X1),
inference(superposition,[],[f843,f474]) ).
fof(f3998,plain,
! [X0,X1] : mult(X0,X1) = ld(ld(X0,unit),X1),
inference(forward_demodulation,[],[f3934,f1]) ).
fof(f4257,plain,
! [X0,X1] : ld(X0,X1) = mult(rd(unit,X0),X1),
inference(superposition,[],[f3998,f72]) ).
fof(f4311,plain,
! [X0,X1] : ld(X0,X1) = mult(ld(X0,unit),X1),
inference(forward_demodulation,[],[f4257,f434]) ).
fof(f4805,plain,
! [X0,X1] : ld(X0,unit) = rd(ld(X0,X1),X1),
inference(superposition,[],[f4,f4311]) ).
fof(f5496,plain,
ld(c,unit) = rd(sF4,sF2),
inference(superposition,[],[f4805,f53]) ).
fof(f5530,plain,
ld(sF2,sF1) = rd(sF4,sF2),
inference(forward_demodulation,[],[f5496,f2716]) ).
fof(f5640,plain,
ld(sF2,unit) = ld(sF4,ld(sF2,sF1)),
inference(superposition,[],[f2507,f5530]) ).
fof(f5646,plain,
sF7 = rd(sF0,ld(sF2,unit)),
inference(backward_demodulation,[],[f3566,f5640]) ).
fof(f5649,plain,
mult(sF0,sF2) = sF7,
inference(forward_demodulation,[],[f5646,f829]) ).
fof(f5652,plain,
sF3 = sF7,
inference(forward_demodulation,[],[f5649,f17]) ).
fof(f5653,plain,
$false,
inference(forward_subsumption_resolution,[],[f5652,f26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP668-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n016.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 10:39:32 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.81/1.99 % (2429576)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.81/1.99 % (2429583)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=742443054:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.81/1.99 % (2429586)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=4255737781:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.81/1.99 % (2429587)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3500240196:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.81/1.99 % (2429585)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=378651664:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.81/1.99 % (2429581)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=2562407694:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.81/1.99 % (2429584)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1651118778:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.81/1.99 % (2429582)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=471404427:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.81/1.99 % (2429584)Instruction limit reached!
% 5.81/1.99 % (2429584)------------------------------
% 5.81/1.99 % (2429584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.99 % (2429584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.99 % (2429584)CaDiCaL version: 2.1.3
% 5.81/1.99 % (2429584)Termination reason: Instruction limit
% 5.81/1.99 % (2429584)Termination phase: Saturation
% 5.81/1.99 % (2429584)Time elapsed: 0.076 s
% 5.81/1.99 % (2429584)Peak memory usage: 89 MB
% 5.81/1.99 % (2429584)Instructions burned: 136 (million)
% 5.81/1.99 % (2429585)Instruction limit reached!
% 5.81/1.99 % (2429585)------------------------------
% 5.81/1.99 % (2429585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.99 % (2429585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.99 % (2429585)CaDiCaL version: 2.1.3
% 5.81/1.99 % (2429585)Termination reason: Instruction limit
% 5.81/1.99 % (2429585)Termination phase: Saturation
% 5.81/1.99 % (2429585)Time elapsed: 0.101 s
% 5.81/1.99 % (2429585)Peak memory usage: 89 MB
% 5.81/1.99 % (2429585)Instructions burned: 182 (million)
% 5.81/1.99 % (2429586)Instruction limit reached!
% 5.81/1.99 % (2429586)------------------------------
% 5.81/1.99 % (2429586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.99 % (2429586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.99 % (2429586)CaDiCaL version: 2.1.3
% 5.81/1.99 % (2429586)Termination reason: Instruction limit
% 5.81/1.99 % (2429586)Termination phase: Saturation
% 5.81/1.99 % (2429586)Time elapsed: 0.154 s
% 5.81/1.99 % (2429586)Peak memory usage: 90 MB
% 5.81/1.99 % (2429586)Instructions burned: 258 (million)
% 5.81/1.99 % (2429595)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3796860992:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 5.81/1.99 % (2429596)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2245400817:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 5.81/1.99 % (2429597)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3295228899:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 5.81/1.99 % (2429597)Instruction limit reached!
% 5.81/1.99 % (2429597)------------------------------
% 5.81/1.99 % (2429597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.99 % (2429597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.99 % (2429597)CaDiCaL version: 2.1.3
% 5.81/1.99 % (2429597)Termination reason: Instruction limit
% 5.81/1.99 % (2429597)Termination phase: Saturation
% 5.81/1.99 % (2429597)Time elapsed: 0.116 s
% 5.81/1.99 % (2429597)Peak memory usage: 89 MB
% 5.81/1.99 % (2429597)Instructions burned: 217 (million)
% 5.81/1.99 % (2429601)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=3737132833: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)
% 5.81/1.99 % (2429587)Instruction limit reached!
% 5.81/1.99 % (2429587)------------------------------
% 5.81/1.99 % (2429587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.99 % (2429587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.99 % (2429587)CaDiCaL version: 2.1.3
% 5.81/1.99 % (2429587)Termination reason: Instruction limit
% 5.81/1.99 % (2429587)Termination phase: Saturation
% 5.81/1.99 % (2429587)Time elapsed: 0.649 s
% 5.81/1.99 % (2429587)Peak memory usage: 99 MB
% 5.81/1.99 % (2429587)Instructions burned: 1187 (million)
% 5.81/1.99 % (2429583)First to succeed.
% 5.81/1.99 % (2429583)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2429576"
% 5.81/1.99 % (2429601)Instruction limit reached!
% 5.81/1.99 % (2429601)------------------------------
% 5.81/1.99 % (2429601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.81/1.99 % (2429601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.81/1.99 % (2429601)CaDiCaL version: 2.1.3
% 5.81/1.99 % (2429601)Termination reason: Instruction limit
% 5.81/1.99 % (2429601)Termination phase: Saturation
% 5.81/1.99 % (2429601)Time elapsed: 0.204 s
% 5.81/1.99 % (2429601)Peak memory usage: 94 MB
% 5.81/1.99 % (2429601)Instructions burned: 318 (million)
% 5.81/1.99 % (2429603)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=726361923:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 5.81/1.99 % (2429604)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3768260780:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 5.81/1.99 % (2429583)Refutation found. Thanks to Tanya!
% 5.81/1.99 % SZS status Unsatisfiable for theBenchmark
% 5.81/1.99 % SZS output start Proof for theBenchmark
% See solution above
% 8.64/2.18 % (2429583)------------------------------
% 8.64/2.18 % (2429583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.18 % (2429583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.18 % (2429583)CaDiCaL version: 2.1.3
% 8.64/2.18 % (2429583)Termination reason: Refutation
% 8.64/2.18 % (2429583)Time elapsed: 0.764 s
% 8.64/2.18 % (2429583)Peak memory usage: 138 MB
% 8.64/2.18 % (2429583)Instructions burned: 1968 (million)
% 8.64/2.18 % (2429583)------------------------------
% 8.64/2.18 % (2429583)------------------------------
% 8.64/2.18 % (2429576)Success in time 1.133 s
% 8.64/2.18 % Vampire exiting
%------------------------------------------------------------------------------