%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN708-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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 02:17:56 PM UTC 2026
% Result : Unsatisfiable 41.19s 6.13s
% Output : Refutation 41.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 38
% Syntax : Number of formulae : 117 ( 117 unt; 22 def)
% Number of atoms : 117 ( 116 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 1 ( 1 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 44 ( 44 usr; 28 con; 0-4 aty)
% Number of variables : 44 ( 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq2(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_001) ).
fof(f3,negated_conjecture,
p38(c56) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c56_is_p38_1) ).
fof(f4,negated_conjecture,
! [X0] : p10(X0,X0) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_3) ).
fof(f5,plain,
! [X0] : true = p10(X0,X0),
inference(reorient_equations,[],[f4]) ).
fof(f20,negated_conjecture,
p37(f15(c56),c48) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p37_13) ).
fof(f21,plain,
true = p37(f15(c56),c48),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
! [X0] : ifeq2(p38(X0),true,p38(f15(X0)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p38_15) ).
fof(f23,plain,
! [X0] : true = ifeq2(p38(X0),true,p38(f15(X0)),true),
inference(reorient_equations,[],[f22]) ).
fof(f30,negated_conjecture,
! [X0,X1] : ifeq2(p10(X0,X1),true,ifeq2(p38(X0),true,p38(X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p38_19) ).
fof(f31,plain,
! [X0,X1] : true = ifeq2(p10(X0,X1),true,ifeq2(p38(X0),true,p38(X1),true),true),
inference(reorient_equations,[],[f30]) ).
fof(f56,negated_conjecture,
! [X0,X1] : ifeq2(p10(X0,X1),true,p16(f19(X0),f19(X1)),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p16_32) ).
fof(f57,plain,
! [X0,X1] : true = ifeq2(p10(X0,X1),true,p16(f19(X0),f19(X1)),true),
inference(reorient_equations,[],[f56]) ).
fof(f64,negated_conjecture,
! [X0] : ifeq2(p38(X0),true,p16(f19(f15(X0)),f28(f19(X0))),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p16_36) ).
fof(f65,plain,
! [X0] : true = ifeq2(p38(X0),true,p16(f19(f15(X0)),f28(f19(X0))),true),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
! [X2,X0,X1] : ifeq2(p10(X0,X1),true,ifeq2(p10(X0,X2),true,p10(X2,X1),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_37) ).
fof(f67,plain,
! [X2,X0,X1] : true = ifeq2(p10(X0,X1),true,ifeq2(p10(X0,X2),true,p10(X2,X1),true),true),
inference(reorient_equations,[],[f66]) ).
fof(f96,negated_conjecture,
! [X2,X3,X0,X1] : ifeq2(p39(X0,X1),true,ifeq2(p16(X0,X2),true,ifeq2(p16(X1,X3),true,p39(X2,X3),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p39_52) ).
fof(f97,plain,
! [X2,X3,X0,X1] : true = ifeq2(p39(X0,X1),true,ifeq2(p16(X0,X2),true,ifeq2(p16(X1,X3),true,p39(X2,X3),true),true),true),
inference(reorient_equations,[],[f96]) ).
fof(f100,negated_conjecture,
! [X0,X1] : ifeq2(p37(X0,X1),true,ifeq2(p38(X1),true,ifeq2(p38(X0),true,p39(f19(X0),f19(X1)),true),true),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p39_54) ).
fof(f101,plain,
! [X0,X1] : true = ifeq2(p37(X0,X1),true,ifeq2(p38(X1),true,ifeq2(p38(X0),true,p39(f19(X0),f19(X1)),true),true),true),
inference(reorient_equations,[],[f100]) ).
fof(f120,negated_conjecture,
p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f11_is_p38_64) ).
fof(f121,plain,
true = p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
inference(reorient_equations,[],[f120]) ).
fof(f124,negated_conjecture,
p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_66) ).
fof(f125,plain,
true = p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
inference(reorient_equations,[],[f124]) ).
fof(f166,negated_conjecture,
ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p39_69) ).
fof(f167,plain,
b = ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b),
inference(reorient_equations,[],[f166]) ).
fof(f168,negated_conjecture,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f169,definition,
sF0 = p38(c56),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f170,plain,
p38(c56) = sF0,
inference(reorient_equations,[],[f169]) ).
fof(f171,plain,
true = sF0,
inference(definition_folding,[],[f3,f170]) ).
fof(f175,definition,
sF2 = f15(c56),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f176,plain,
f15(c56) = sF2,
inference(reorient_equations,[],[f175]) ).
fof(f177,definition,
sF3 = p37(sF2,c48),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f178,plain,
p37(sF2,c48) = sF3,
inference(reorient_equations,[],[f177]) ).
fof(f179,plain,
true = sF3,
inference(definition_folding,[],[f21,f178,f176]) ).
fof(f180,definition,
sF4 = f19(c56),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f181,plain,
f19(c56) = sF4,
inference(reorient_equations,[],[f180]) ).
fof(f189,definition,
sF8 = f7(c44),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f190,plain,
f7(c44) = sF8,
inference(reorient_equations,[],[f189]) ).
fof(f208,definition,
sF17 = f5(c44),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f209,plain,
f5(c44) = sF17,
inference(reorient_equations,[],[f208]) ).
fof(f210,definition,
sF18 = f7(sF8),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f211,plain,
f7(sF8) = sF18,
inference(reorient_equations,[],[f210]) ).
fof(f240,definition,
sF32 = f6(sF18),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f241,plain,
f6(sF18) = sF32,
inference(reorient_equations,[],[f240]) ).
fof(f242,definition,
sF33 = f6(sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f243,plain,
f6(sF32) = sF33,
inference(reorient_equations,[],[f242]) ).
fof(f244,definition,
sF34 = f7(sF33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f245,plain,
f7(sF33) = sF34,
inference(reorient_equations,[],[f244]) ).
fof(f246,definition,
sF35 = f7(sF34),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f247,plain,
f7(sF34) = sF35,
inference(reorient_equations,[],[f246]) ).
fof(f248,definition,
sF36 = f6(sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f249,plain,
f6(sF35) = sF36,
inference(reorient_equations,[],[f248]) ).
fof(f250,definition,
sF37 = f5(sF36),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f251,plain,
f5(sF36) = sF37,
inference(reorient_equations,[],[f250]) ).
fof(f252,definition,
sF38 = f14(sF37,sF17),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
fof(f253,plain,
f14(sF37,sF17) = sF38,
inference(reorient_equations,[],[f252]) ).
fof(f254,definition,
sF39 = f13(sF17,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
fof(f255,plain,
f13(sF17,sF38) = sF39,
inference(reorient_equations,[],[f254]) ).
fof(f256,definition,
sF40 = f11(sF39),
introduced(definition,[new_symbols(definition,[sF40])],[function_definition]) ).
fof(f257,plain,
f11(sF39) = sF40,
inference(reorient_equations,[],[f256]) ).
fof(f258,definition,
sF41 = p38(sF40),
introduced(definition,[new_symbols(definition,[sF41])],[function_definition]) ).
fof(f259,plain,
p38(sF40) = sF41,
inference(reorient_equations,[],[f258]) ).
fof(f260,plain,
true = sF41,
inference(definition_folding,[],[f121,f259,f257,f255,f253,f209,f251,f249,f247,f245,f243,f241,f211,f190,f209]) ).
fof(f270,definition,
sF46 = p10(c48,sF40),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f271,plain,
p10(c48,sF40) = sF46,
inference(reorient_equations,[],[f270]) ).
fof(f272,plain,
true = sF46,
inference(definition_folding,[],[f125,f271,f257,f255,f253,f209,f251,f249,f247,f245,f243,f241,f211,f190,f209]) ).
fof(f653,definition,
sF227 = f28(sF4),
introduced(definition,[new_symbols(definition,[sF227])],[function_definition]) ).
fof(f654,plain,
f28(sF4) = sF227,
inference(reorient_equations,[],[f653]) ).
fof(f655,definition,
sF228 = f19(sF40),
introduced(definition,[new_symbols(definition,[sF228])],[function_definition]) ).
fof(f656,plain,
f19(sF40) = sF228,
inference(reorient_equations,[],[f655]) ).
fof(f657,definition,
sF229 = p39(sF227,sF228),
introduced(definition,[new_symbols(definition,[sF229])],[function_definition]) ).
fof(f658,plain,
p39(sF227,sF228) = sF229,
inference(reorient_equations,[],[f657]) ).
fof(f659,definition,
sF230 = ifeq(sF229,true,a,b),
introduced(definition,[new_symbols(definition,[sF230])],[function_definition]) ).
fof(f660,plain,
ifeq(sF229,true,a,b) = sF230,
inference(reorient_equations,[],[f659]) ).
fof(f661,plain,
b = sF230,
inference(definition_folding,[],[f167,f660,f658,f656,f257,f255,f253,f209,f251,f249,f247,f245,f243,f241,f211,f190,f209,f654,f181]) ).
fof(f662,plain,
p38(c56) = true,
inference(forward_demodulation,[],[f170,f171]) ).
fof(f664,plain,
true = p37(sF2,c48),
inference(forward_demodulation,[],[f178,f179]) ).
fof(f669,plain,
true = p38(sF40),
inference(forward_demodulation,[],[f259,f260]) ).
fof(f671,plain,
true = p10(c48,sF40),
inference(forward_demodulation,[],[f271,f272]) ).
fof(f692,plain,
b = ifeq(sF229,true,a,b),
inference(forward_demodulation,[],[f660,f661]) ).
fof(f693,plain,
true = ifeq2(true,true,p38(f15(c56)),true),
inference(superposition,[],[f23,f662]) ).
fof(f698,plain,
true = p38(f15(c56)),
inference(forward_demodulation,[],[f693,f1]) ).
fof(f699,plain,
true = p38(sF2),
inference(forward_demodulation,[],[f698,f176]) ).
fof(f847,plain,
true = ifeq2(true,true,p16(f19(c48),f19(sF40)),true),
inference(superposition,[],[f57,f671]) ).
fof(f864,plain,
true = p16(f19(c48),f19(sF40)),
inference(forward_demodulation,[],[f847,f1]) ).
fof(f867,plain,
true = p16(f19(c48),sF228),
inference(forward_demodulation,[],[f864,f656]) ).
fof(f928,plain,
true = ifeq2(true,true,p16(f19(f15(c56)),f28(f19(c56))),true),
inference(superposition,[],[f65,f662]) ).
fof(f947,plain,
true = p16(f19(f15(c56)),f28(f19(c56))),
inference(forward_demodulation,[],[f928,f1]) ).
fof(f950,plain,
true = p16(f19(f15(c56)),f28(sF4)),
inference(forward_demodulation,[],[f947,f181]) ).
fof(f952,plain,
true = p16(f19(f15(c56)),sF227),
inference(forward_demodulation,[],[f950,f654]) ).
fof(f953,plain,
true = p16(f19(sF2),sF227),
inference(forward_demodulation,[],[f952,f176]) ).
fof(f1030,plain,
! [X0] : true = ifeq2(p10(sF40,X0),true,ifeq2(true,true,p38(X0),true),true),
inference(superposition,[],[f31,f669]) ).
fof(f1044,plain,
! [X0] : true = ifeq2(p10(sF40,X0),true,p38(X0),true),
inference(forward_demodulation,[],[f1030,f1]) ).
fof(f1079,plain,
! [X0] : true = ifeq2(p10(c48,X0),true,ifeq2(true,true,p10(sF40,X0),true),true),
inference(superposition,[],[f67,f671]) ).
fof(f1104,plain,
! [X0] : true = ifeq2(p10(c48,X0),true,p10(sF40,X0),true),
inference(forward_demodulation,[],[f1079,f1]) ).
fof(f2478,plain,
true = ifeq2(true,true,ifeq2(p38(c48),true,ifeq2(p38(sF2),true,p39(f19(sF2),f19(c48)),true),true),true),
inference(superposition,[],[f101,f664]) ).
fof(f2519,plain,
true = ifeq2(p38(c48),true,ifeq2(p38(sF2),true,p39(f19(sF2),f19(c48)),true),true),
inference(forward_demodulation,[],[f2478,f1]) ).
fof(f2526,plain,
true = ifeq2(p38(c48),true,ifeq2(true,true,p39(f19(sF2),f19(c48)),true),true),
inference(forward_demodulation,[],[f2519,f699]) ).
fof(f2527,plain,
true = ifeq2(p38(c48),true,p39(f19(sF2),f19(c48)),true),
inference(forward_demodulation,[],[f2526,f1]) ).
fof(f7999,plain,
! [X0,X1] : true = ifeq2(p39(X0,X1),true,ifeq2(p16(X0,sF227),true,ifeq2(p16(X1,sF228),true,sF229,true),true),true),
inference(superposition,[],[f97,f658]) ).
fof(f8419,plain,
true = ifeq2(true,true,p10(sF40,c48),true),
inference(superposition,[],[f1104,f5]) ).
fof(f8424,plain,
true = p10(sF40,c48),
inference(forward_demodulation,[],[f8419,f1]) ).
fof(f8427,plain,
true = ifeq2(true,true,p38(c48),true),
inference(superposition,[],[f1044,f8424]) ).
fof(f8461,plain,
true = p38(c48),
inference(forward_demodulation,[],[f8427,f1]) ).
fof(f11031,plain,
true = ifeq2(true,true,p39(f19(sF2),f19(c48)),true),
inference(superposition,[],[f2527,f8461]) ).
fof(f11032,plain,
true = p39(f19(sF2),f19(c48)),
inference(forward_demodulation,[],[f11031,f1]) ).
fof(f94788,plain,
true = ifeq2(true,true,ifeq2(p16(f19(sF2),sF227),true,ifeq2(p16(f19(c48),sF228),true,sF229,true),true),true),
inference(superposition,[],[f7999,f11032]) ).
fof(f94811,plain,
true = ifeq2(p16(f19(sF2),sF227),true,ifeq2(p16(f19(c48),sF228),true,sF229,true),true),
inference(forward_demodulation,[],[f94788,f1]) ).
fof(f94813,plain,
true = ifeq2(p16(f19(sF2),sF227),true,ifeq2(true,true,sF229,true),true),
inference(forward_demodulation,[],[f94811,f867]) ).
fof(f94815,plain,
true = ifeq2(p16(f19(sF2),sF227),true,sF229,true),
inference(forward_demodulation,[],[f94813,f1]) ).
fof(f94817,plain,
true = ifeq2(true,true,sF229,true),
inference(forward_demodulation,[],[f94815,f953]) ).
fof(f94818,plain,
true = sF229,
inference(forward_demodulation,[],[f94817,f1]) ).
fof(f94820,plain,
b = ifeq(true,true,a,b),
inference(superposition,[],[f692,f94818]) ).
fof(f94821,plain,
a = b,
inference(forward_demodulation,[],[f94820,f2]) ).
fof(f94822,plain,
$false,
inference(forward_subsumption_resolution,[],[f94821,f168]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN708-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n017.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:43:52 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.73/2.38 % (3696161)Will run a generic schedule for satisfiability detection.
% 14.73/2.38 % (3696176)dis+10_1_sil=32000:sp=arity:random_seed=2718652701:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.73/2.38 % (3696174)% WARNING: option uhcvi not known.
% 14.73/2.38 % (3696175)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3697442226:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.73/2.38 % (3696173)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3388648173_2999 on theBenchmark for (2999ds/0Mi)
% 14.73/2.38 % (3696174)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2584865628:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.73/2.38 % (3696177)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1137693132:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.73/2.38 % (3696180)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2054350735:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.73/2.38 % (3696179)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1184689093:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.73/2.38 % (3696176)Instruction limit reached!
% 14.73/2.38 % (3696176)------------------------------
% 14.73/2.38 % (3696176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.38 % (3696176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.38 % (3696176)CaDiCaL version: 2.1.3
% 14.73/2.38 % (3696176)Termination reason: Instruction limit
% 14.73/2.38 % (3696176)Termination phase: Saturation
% 14.73/2.38 % (3696176)Time elapsed: 0.030 s
% 14.73/2.38 % (3696176)Peak memory usage: 12 MB
% 14.73/2.38 % (3696176)Instructions burned: 106 (million)
% 14.73/2.38 % TRYING [1]
% 14.73/2.38 % TRYING [2]
% 14.73/2.38 % (3696209)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1281891115:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.73/2.38 % TRYING [3]
% 14.73/2.38 % TRYING [1]
% 14.73/2.38 % TRYING [2]
% 14.73/2.38 % TRYING [3]
% 14.73/2.38 % (3696177)Instruction limit reached!
% 14.73/2.38 % (3696177)------------------------------
% 14.73/2.38 % (3696177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.38 % (3696177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.38 % (3696177)CaDiCaL version: 2.1.3
% 14.73/2.38 % (3696177)Termination reason: Instruction limit
% 14.73/2.38 % (3696177)Termination phase: Saturation
% 14.73/2.38 % (3696177)Time elapsed: 0.062 s
% 14.73/2.38 % (3696177)Peak memory usage: 13 MB
% 14.73/2.38 % (3696177)Instructions burned: 117 (million)
% 14.73/2.38 % (3696179)Instruction limit reached!
% 14.73/2.38 % (3696179)------------------------------
% 14.73/2.38 % (3696179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.38 % (3696179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.38 % (3696179)CaDiCaL version: 2.1.3
% 14.73/2.38 % (3696179)Termination reason: Instruction limit
% 14.73/2.38 % (3696179)Termination phase: Saturation
% 14.73/2.38 % (3696179)Time elapsed: 0.070 s
% 14.73/2.38 % (3696179)Peak memory usage: 13 MB
% 14.73/2.38 % (3696179)Instructions burned: 135 (million)
% 14.73/2.38 % (3696215)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4079354837:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.73/2.38 % (3696216)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=489229610:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 14.73/2.38 % (3696180)Instruction limit reached!
% 14.73/2.38 % (3696180)------------------------------
% 14.73/2.38 % (3696180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.38 % (3696180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.73/2.38 % (3696180)CaDiCaL version: 2.1.3
% 14.73/2.38 % (3696180)Termination reason: Instruction limit
% 14.73/2.38 % (3696180)Termination phase: Saturation
% 14.73/2.38 % (3696180)Time elapsed: 0.091 s
% 14.73/2.38 % (3696180)Peak memory usage: 13 MB
% 14.73/2.38 % (3696180)Instructions burned: 159 (million)
% 14.73/2.38 % (3696219)ott-21_1_sil=16000:fs=off:random_seed=2682809160:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.73/2.38 % (3696215)Instruction limit reached!
% 14.73/2.38 % (3696215)------------------------------
% 14.73/2.38 % (3696215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.73/2.38 % (3696215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.57/5.88 % (3696215)CaDiCaL version: 2.1.3
% 39.57/5.88 % (3696215)Termination reason: Instruction limit
% 39.57/5.88 % (3696215)Termination phase: Saturation
% 39.57/5.88 % (3696215)Time elapsed: 0.077 s
% 39.57/5.88 % (3696215)Peak memory usage: 13 MB
% 39.57/5.88 % (3696215)Instructions burned: 132 (million)
% 39.57/5.88 % (3696221)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1385691413:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 39.57/5.88 % TRYING [4]
% 39.57/5.88 % (3696219)Instruction limit reached!
% 39.57/5.88 % (3696219)------------------------------
% 39.57/5.88 % (3696219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.57/5.88 % (3696219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.57/5.88 % (3696219)CaDiCaL version: 2.1.3
% 39.57/5.88 % (3696219)Termination reason: Instruction limit
% 39.57/5.88 % (3696219)Termination phase: Saturation
% 39.57/5.88 % (3696219)Time elapsed: 0.089 s
% 39.57/5.88 % (3696219)Peak memory usage: 13 MB
% 39.57/5.88 % (3696219)Instructions burned: 182 (million)
% 39.57/5.88 % TRYING [4]
% 39.57/5.88 % (3696223)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=819774212:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 39.57/5.88 % (3696209)Instruction limit reached!
% 39.57/5.88 % (3696209)------------------------------
% 39.57/5.88 % (3696209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.57/5.88 % (3696209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.57/5.88 % (3696209)CaDiCaL version: 2.1.3
% 39.57/5.88 % (3696209)Termination reason: Instruction limit
% 39.57/5.88 % (3696209)Termination phase: Finite model building constraint generation
% 39.57/5.88 % (3696209)Time elapsed: 0.188 s
% 39.57/5.88 % (3696209)Peak memory usage: 30 MB
% 39.57/5.88 % (3696209)Instructions burned: 721 (million)
% 39.57/5.88 % (3696225)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3710962792:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 39.57/5.88 % TRYING [1]
% 39.57/5.88 % TRYING [2]
% 39.57/5.88 % TRYING [3]
% 39.57/5.88 % (3696216)Instruction limit reached!
% 39.57/5.88 % (3696216)------------------------------
% 39.57/5.88 % (3696216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.57/5.88 % (3696216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.57/5.88 % (3696216)CaDiCaL version: 2.1.3
% 39.57/5.88 % (3696216)Termination reason: Instruction limit
% 39.57/5.88 % (3696216)Termination phase: Saturation
% 39.57/5.88 % (3696216)Time elapsed: 0.340 s
% 39.57/5.88 % (3696216)Peak memory usage: 18 MB
% 39.57/5.88 % (3696216)Instructions burned: 686 (million)
% 39.57/5.88 % (3696221)Instruction limit reached!
% 39.57/5.88 % (3696221)------------------------------
% 39.57/5.88 % (3696221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.57/5.88 % (3696221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.57/5.88 % (3696221)CaDiCaL version: 2.1.3
% 39.57/5.88 % (3696221)Termination reason: Instruction limit
% 39.57/5.88 % (3696221)Termination phase: Saturation
% 39.57/5.88 % (3696221)Time elapsed: 0.251 s
% 39.57/5.88 % (3696221)Peak memory usage: 16 MB
% 39.57/5.88 % (3696221)Instructions burned: 478 (million)
% 39.57/5.88 % (3696227)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1785485825:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 39.57/5.88 % (3696228)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3249733412:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 39.57/5.88 % TRYING [4]
% 39.57/5.88 % (3696223)Instruction limit reached!
% 39.57/5.88 % (3696223)------------------------------
% 39.57/5.88 % (3696223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.57/5.88 % (3696223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.57/5.88 % (3696223)CaDiCaL version: 2.1.3
% 39.57/5.88 % (3696223)Termination reason: Instruction limit
% 39.57/5.88 % (3696223)Termination phase: Finite model building constraint generation
% 39.57/5.88 % (3696223)Time elapsed: 0.345 s
% 39.57/5.88 % (3696223)Peak memory usage: 31 MB
% 39.57/5.88 % (3696223)Instructions burned: 868 (million)
% 39.57/5.88 % (3696225)Instruction limit reached!
% 39.57/5.88 % (3696225)------------------------------
% 39.57/5.88 % (3696225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.57/5.88 % (3696225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696225)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696225)Termination reason: Instruction limit
% 41.19/6.13 % (3696225)Termination phase: Saturation
% 41.19/6.13 % (3696225)Time elapsed: 0.342 s
% 41.19/6.13 % (3696225)Peak memory usage: 35 MB
% 41.19/6.13 % (3696225)Instructions burned: 1180 (million)
% 41.19/6.13 % (3696231)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1051955549:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 41.19/6.13 % (3696232)fmb+10_1_sil=64000:random_seed=3296408887:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 41.19/6.13 % TRYING [1]
% 41.19/6.13 % TRYING [2]
% 41.19/6.13 % TRYING [3]
% 41.19/6.13 % TRYING [4]
% 41.19/6.13 % (3696228)Instruction limit reached!
% 41.19/6.13 % (3696228)------------------------------
% 41.19/6.13 % (3696228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696228)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696228)Termination reason: Instruction limit
% 41.19/6.13 % (3696228)Termination phase: Saturation
% 41.19/6.13 % (3696228)Time elapsed: 0.354 s
% 41.19/6.13 % (3696228)Peak memory usage: 22 MB
% 41.19/6.13 % (3696228)Instructions burned: 693 (million)
% 41.19/6.13 % (3696235)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3071872737:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 41.19/6.13 % TRYING [20]
% 41.19/6.13 % (3696227)Instruction limit reached!
% 41.19/6.13 % (3696227)------------------------------
% 41.19/6.13 % (3696227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696227)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696227)Termination reason: Instruction limit
% 41.19/6.13 % (3696227)Termination phase: Finite model building constraint generation
% 41.19/6.13 % (3696227)Time elapsed: 0.406 s
% 41.19/6.13 % (3696227)Peak memory usage: 107 MB
% 41.19/6.13 % (3696227)Instructions burned: 891 (million)
% 41.19/6.13 % (3696237)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1830139022:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 41.19/6.13 % TRYING [8]
% 41.19/6.13 % TRYING [5]
% 41.19/6.13 % (3696231)Instruction limit reached!
% 41.19/6.13 % (3696231)------------------------------
% 41.19/6.13 % (3696231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696231)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696231)Termination reason: Instruction limit
% 41.19/6.13 % (3696231)Termination phase: Saturation
% 41.19/6.13 % (3696231)Time elapsed: 0.407 s
% 41.19/6.13 % (3696231)Peak memory usage: 18 MB
% 41.19/6.13 % (3696231)Instructions burned: 879 (million)
% 41.19/6.13 % (3696239)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=709129949:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 41.19/6.13 % (3696237)Instruction limit reached!
% 41.19/6.13 % (3696237)------------------------------
% 41.19/6.13 % (3696237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696237)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696237)Termination reason: Instruction limit
% 41.19/6.13 % (3696237)Termination phase: Finite model building constraint generation
% 41.19/6.13 % (3696237)Time elapsed: 0.329 s
% 41.19/6.13 % (3696237)Peak memory usage: 75 MB
% 41.19/6.13 % (3696237)Instructions burned: 920 (million)
% 41.19/6.13 % (3696241)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1064830229:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 41.19/6.13 % TRYING [5]
% 41.19/6.13 % (3696241)Instruction limit reached!
% 41.19/6.13 % (3696241)------------------------------
% 41.19/6.13 % (3696241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696241)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696241)Termination reason: Instruction limit
% 41.19/6.13 % (3696241)Termination phase: Saturation
% 41.19/6.13 % (3696241)Time elapsed: 0.821 s
% 41.19/6.13 % (3696241)Peak memory usage: 36 MB
% 41.19/6.13 % (3696241)Instructions burned: 1473 (million)
% 41.19/6.13 % (3696243)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2699178486:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 41.19/6.13 % (3696243)Cannot represent all propositional literals internally
% 41.19/6.13 % (3696243)Refutation not found, incomplete strategy
% 41.19/6.13 % (3696243)------------------------------
% 41.19/6.13 % (3696243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696243)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696243)Termination reason: Refutation not found, incomplete strategy
% 41.19/6.13 % (3696243)Time elapsed: 0.024 s
% 41.19/6.13 % (3696243)Peak memory usage: 11 MB
% 41.19/6.13 % (3696243)Instructions burned: 51 (million)
% 41.19/6.13 % (3696243)------------------------------
% 41.19/6.13 % (3696243)------------------------------
% 41.19/6.13 % (3696245)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=980014535:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 41.19/6.13 % TRYING [16]
% 41.19/6.13 % TRYING [6]
% 41.19/6.13 % (3696245)Instruction limit reached!
% 41.19/6.13 % (3696245)------------------------------
% 41.19/6.13 % (3696245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696245)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696245)Termination reason: Instruction limit
% 41.19/6.13 % (3696245)Termination phase: Finite model building constraint generation
% 41.19/6.13 % (3696245)Time elapsed: 0.765 s
% 41.19/6.13 % (3696245)Peak memory usage: 141 MB
% 41.19/6.13 % (3696245)Instructions burned: 2175 (million)
% 41.19/6.13 % (3696247)ott-2_1_sil=16000:newcnf=on:random_seed=678722930:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 41.19/6.13 % (3696247)Instruction limit reached!
% 41.19/6.13 % (3696247)------------------------------
% 41.19/6.13 % (3696247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696247)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696247)Termination reason: Instruction limit
% 41.19/6.13 % (3696247)Termination phase: Saturation
% 41.19/6.13 % (3696247)Time elapsed: 0.464 s
% 41.19/6.13 % (3696247)Peak memory usage: 24 MB
% 41.19/6.13 % (3696247)Instructions burned: 869 (million)
% 41.19/6.13 % (3696249)ott+10_1_sil=32000:tgt=ground:random_seed=1741000605:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 41.19/6.13 % (3696239)Instruction limit reached!
% 41.19/6.13 % (3696239)------------------------------
% 41.19/6.13 % (3696239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696239)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696239)Termination reason: Instruction limit
% 41.19/6.13 % (3696239)Termination phase: Saturation
% 41.19/6.13 % (3696239)Time elapsed: 2.507 s
% 41.19/6.13 % (3696239)Peak memory usage: 55 MB
% 41.19/6.13 % (3696239)Instructions burned: 5132 (million)
% 41.19/6.13 % (3696251)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2561464321:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 41.19/6.13 % TRYING [1]
% 41.19/6.13 % TRYING [2]
% 41.19/6.13 % TRYING [3]
% 41.19/6.13 % TRYING [4]
% 41.19/6.13 % (3696235)Instruction limit reached!
% 41.19/6.13 % (3696235)------------------------------
% 41.19/6.13 % (3696235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696235)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696235)Termination reason: Instruction limit
% 41.19/6.13 % (3696235)Termination phase: Finite model building constraint generation
% 41.19/6.13 % (3696235)Time elapsed: 3.221 s
% 41.19/6.13 % (3696235)Peak memory usage: 524 MB
% 41.19/6.13 % (3696235)Instructions burned: 9518 (million)
% 41.19/6.13 % (3696253)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4127813027:i=3512:aac=none_2958 on theBenchmark for (2958ds/3512Mi)
% 41.19/6.13 % TRYING [5]
% 41.19/6.13 % (3696232)Instruction limit reached!
% 41.19/6.13 % (3696232)------------------------------
% 41.19/6.13 % (3696232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696232)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696232)Termination reason: Instruction limit
% 41.19/6.13 % (3696232)Termination phase: Finite model building SAT solving
% 41.19/6.13 % (3696232)Time elapsed: 4.988 s
% 41.19/6.13 % (3696232)Peak memory usage: 296 MB
% 41.19/6.13 % (3696232)Instructions burned: 22062 (million)
% 41.19/6.13 % (3696255)dis+21_1_sil=32000:sas=cadical:random_seed=221488021:i=3773:amm=off_2943 on theBenchmark for (2943ds/3773Mi)
% 41.19/6.13 % (3696253)Instruction limit reached!
% 41.19/6.13 % (3696253)------------------------------
% 41.19/6.13 % (3696253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696253)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696253)Termination reason: Instruction limit
% 41.19/6.13 % (3696253)Termination phase: Saturation
% 41.19/6.13 % (3696253)Time elapsed: 1.655 s
% 41.19/6.13 % (3696253)Peak memory usage: 46 MB
% 41.19/6.13 % (3696253)Instructions burned: 3514 (million)
% 41.19/6.13 % (3696257)ott+11_1_sil=16000:gs=on:random_seed=4269580140:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2941 on theBenchmark for (2941ds/2251Mi)
% 41.19/6.13 % (3696249) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3696161-3696249"...
% 41.19/6.13 % (3696249)...printing done.
% 41.19/6.13 % (3696249)Refutation found. Thanks to Tanya!
% 41.19/6.13 % SZS status Unsatisfiable for theBenchmark
% 41.19/6.13 % SZS output start Proof for theBenchmark
% See solution above
% 41.19/6.13 % (3696249)------------------------------
% 41.19/6.13 % (3696249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.19/6.13 % (3696249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.19/6.13 % (3696249)CaDiCaL version: 2.1.3
% 41.19/6.13 % (3696249)Termination reason: Refutation
% 41.19/6.13 % (3696249)Time elapsed: 2.397 s
% 41.19/6.13 % (3696249)Peak memory usage: 109 MB
% 41.19/6.13 % (3696249)Instructions burned: 4452 (million)
% 41.19/6.13 % (3696161)Success in time 5.89 s
% 41.19/6.13 % Vampire exiting
%------------------------------------------------------------------------------