%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV543-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 01:25:14 PM UTC 2026
% Result : Unsatisfiable 0.84s 0.42s
% Output : Refutation 0.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 47
% Syntax : Number of formulae : 119 ( 119 unt; 0 def)
% Number of atoms : 119 ( 118 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 51 ( 51 usr; 49 con; 0-3 aty)
% Number of variables : 9 ( 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f3,axiom,
! [X2,X0,X1] : store(store(X0,X1,select(X0,X2)),X2,select(X0,X1)) = store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f6,axiom,
a_787 = store(a_785,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f7,axiom,
a_789 = store(a_787,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f8,axiom,
a_791 = store(a_789,i0,e_790),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f9,axiom,
a_793 = store(a_791,i5,e_792),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f10,axiom,
a_795 = store(a_793,i2,e_794),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f11,axiom,
a_797 = store(a_795,i5,e_796),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f12,axiom,
a_799 = store(a_797,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f13,axiom,
a_800 = store(a_799,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f14,axiom,
a_802 = store(a_800,i5,e_801),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f15,axiom,
a_804 = store(a_802,i2,e_803),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f16,axiom,
a_806 = store(a_804,i5,e_805),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f17,axiom,
a_808 = store(a_806,i2,e_807),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f18,axiom,
a_809 = store(a_785,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f19,axiom,
a_810 = store(a_809,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f20,axiom,
a_812 = store(a_810,i5,e_811),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f21,axiom,
a_814 = store(a_812,i0,e_813),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f22,axiom,
a_816 = store(a_814,i5,e_815),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f23,axiom,
a_818 = store(a_816,i2,e_817),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f24,axiom,
a_820 = store(a_818,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f25,axiom,
a_821 = store(a_820,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f26,axiom,
a_823 = store(a_821,i5,e_822),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f27,axiom,
a_825 = store(a_823,i2,e_824),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f28,axiom,
a_827 = store(a_825,i5,e_826),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f29,axiom,
a_829 = store(a_827,i2,e_828),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f32,axiom,
e_786 = select(a_785,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f33,axiom,
e_788 = select(a_785,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f34,axiom,
e_790 = select(a_789,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f35,axiom,
e_792 = select(a_789,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f36,axiom,
e_794 = select(a_793,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f37,axiom,
e_796 = select(a_793,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f38,axiom,
e_798 = select(a_797,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f39,axiom,
e_801 = select(a_800,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f40,axiom,
e_803 = select(a_800,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f41,axiom,
e_805 = select(a_804,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f42,axiom,
e_807 = select(a_804,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f43,axiom,
e_811 = select(a_810,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f44,axiom,
e_813 = select(a_810,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f45,axiom,
e_815 = select(a_814,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f46,axiom,
e_817 = select(a_814,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
fof(f47,axiom,
e_819 = select(a_818,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f48,axiom,
e_822 = select(a_821,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f49,axiom,
e_824 = select(a_821,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f50,axiom,
e_826 = select(a_825,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f51,axiom,
e_828 = select(a_825,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f52,negated_conjecture,
a_808 != a_829,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f59,plain,
e_792 = select(a_793,i5),
inference(superposition,[],[f1,f9]) ).
fof(f65,plain,
e_803 = select(a_804,i2),
inference(superposition,[],[f1,f15]) ).
fof(f76,plain,
e_824 = select(a_825,i2),
inference(superposition,[],[f1,f27]) ).
fof(f110,plain,
! [X0] : store(store(a_785,i1,select(a_785,X0)),X0,e_786) = store(store(a_785,X0,e_786),i1,select(a_785,X0)),
inference(superposition,[],[f3,f32]) ).
fof(f113,plain,
! [X0] : store(store(a_789,i5,select(a_789,X0)),X0,e_790) = store(store(a_789,X0,e_790),i5,select(a_789,X0)),
inference(superposition,[],[f3,f34]) ).
fof(f124,plain,
! [X0] : store(store(a_814,i2,select(a_814,X0)),X0,e_815) = store(store(a_814,X0,e_815),i2,select(a_814,X0)),
inference(superposition,[],[f3,f45]) ).
fof(f169,plain,
e_792 = e_794,
inference(superposition,[],[f59,f36]) ).
fof(f170,plain,
e_792 = e_794,
inference(superposition,[],[f36,f59]) ).
fof(f177,plain,
a_795 = store(a_793,i2,e_792),
inference(superposition,[],[f10,f169]) ).
fof(f187,plain,
e_803 = e_805,
inference(superposition,[],[f65,f41]) ).
fof(f195,plain,
a_806 = store(a_804,i5,e_803),
inference(superposition,[],[f16,f187]) ).
fof(f216,plain,
e_824 = e_826,
inference(superposition,[],[f50,f76]) ).
fof(f224,plain,
a_827 = store(a_825,i5,e_824),
inference(superposition,[],[f28,f216]) ).
fof(f881,plain,
store(store(a_785,i1,e_788),i2,e_786) = store(store(a_785,i2,e_786),i1,e_788),
inference(superposition,[],[f110,f33]) ).
fof(f885,plain,
store(a_787,i1,e_788) = store(store(a_785,i1,e_788),i2,e_786),
inference(forward_demodulation,[],[f881,f6]) ).
fof(f886,plain,
store(a_787,i1,e_788) = store(a_809,i2,e_786),
inference(forward_demodulation,[],[f885,f18]) ).
fof(f887,plain,
store(a_787,i1,e_788) = a_810,
inference(forward_demodulation,[],[f886,f19]) ).
fof(f888,plain,
a_789 = a_810,
inference(forward_demodulation,[],[f887,f7]) ).
fof(f891,plain,
e_813 = select(a_789,i5),
inference(superposition,[],[f44,f888]) ).
fof(f892,plain,
e_811 = select(a_789,i0),
inference(superposition,[],[f43,f888]) ).
fof(f893,plain,
e_792 = e_811,
inference(forward_demodulation,[],[f892,f35]) ).
fof(f894,plain,
e_790 = e_813,
inference(forward_demodulation,[],[f891,f34]) ).
fof(f903,plain,
a_812 = store(a_810,i5,e_792),
inference(superposition,[],[f20,f893]) ).
fof(f904,plain,
a_812 = store(a_789,i5,e_792),
inference(forward_demodulation,[],[f903,f888]) ).
fof(f905,plain,
store(store(a_789,i5,e_792),i0,e_790) = store(store(a_789,i0,e_790),i5,e_792),
inference(superposition,[],[f113,f35]) ).
fof(f909,plain,
store(a_791,i5,e_792) = store(store(a_789,i5,e_792),i0,e_790),
inference(forward_demodulation,[],[f905,f8]) ).
fof(f910,plain,
store(a_791,i5,e_792) = store(a_812,i0,e_790),
inference(forward_demodulation,[],[f909,f904]) ).
fof(f911,plain,
a_793 = store(a_812,i0,e_790),
inference(forward_demodulation,[],[f910,f9]) ).
fof(f912,plain,
a_814 = store(a_812,i0,e_790),
inference(superposition,[],[f21,f894]) ).
fof(f913,plain,
a_793 = a_814,
inference(forward_demodulation,[],[f912,f911]) ).
fof(f923,plain,
e_817 = select(a_793,i5),
inference(superposition,[],[f46,f913]) ).
fof(f924,plain,
e_815 = select(a_793,i2),
inference(superposition,[],[f45,f913]) ).
fof(f925,plain,
e_796 = e_815,
inference(forward_demodulation,[],[f924,f37]) ).
fof(f926,plain,
e_794 = e_817,
inference(forward_demodulation,[],[f923,f36]) ).
fof(f928,plain,
e_792 = e_817,
inference(forward_demodulation,[],[f926,f170]) ).
fof(f959,plain,
a_818 = store(a_816,i2,e_792),
inference(superposition,[],[f23,f928]) ).
fof(f1098,plain,
store(store(a_814,i2,e_817),i5,e_815) = store(store(a_814,i5,e_815),i2,e_817),
inference(superposition,[],[f124,f46]) ).
fof(f1107,plain,
store(store(a_814,i2,e_792),i5,e_815) = store(store(a_814,i5,e_815),i2,e_792),
inference(forward_demodulation,[],[f1098,f928]) ).
fof(f1112,plain,
store(a_816,i2,e_792) = store(store(a_814,i2,e_792),i5,e_815),
inference(forward_demodulation,[],[f1107,f22]) ).
fof(f1114,plain,
store(a_816,i2,e_792) = store(store(a_814,i2,e_792),i5,e_796),
inference(forward_demodulation,[],[f1112,f925]) ).
fof(f1115,plain,
store(store(a_793,i2,e_792),i5,e_796) = store(a_816,i2,e_792),
inference(forward_demodulation,[],[f1114,f913]) ).
fof(f1116,plain,
a_818 = store(store(a_793,i2,e_792),i5,e_796),
inference(forward_demodulation,[],[f1115,f959]) ).
fof(f1117,plain,
store(a_795,i5,e_796) = a_818,
inference(forward_demodulation,[],[f1116,f177]) ).
fof(f1118,plain,
a_797 = a_818,
inference(forward_demodulation,[],[f1117,f11]) ).
fof(f1121,plain,
e_819 = select(a_797,i1),
inference(superposition,[],[f47,f1118]) ).
fof(f1122,plain,
e_798 = e_819,
inference(forward_demodulation,[],[f1121,f38]) ).
fof(f1153,plain,
a_820 = store(a_818,i1,e_798),
inference(superposition,[],[f24,f1122]) ).
fof(f1154,plain,
store(a_797,i1,e_798) = a_820,
inference(forward_demodulation,[],[f1153,f1118]) ).
fof(f1155,plain,
a_799 = a_820,
inference(forward_demodulation,[],[f1154,f12]) ).
fof(f1173,plain,
a_821 = store(a_799,i1,e_819),
inference(superposition,[],[f25,f1155]) ).
fof(f1174,plain,
store(a_799,i1,e_798) = a_821,
inference(forward_demodulation,[],[f1173,f1122]) ).
fof(f1177,plain,
a_800 = a_821,
inference(forward_demodulation,[],[f1174,f13]) ).
fof(f1209,plain,
e_822 = select(a_800,i2),
inference(superposition,[],[f48,f1177]) ).
fof(f1210,plain,
e_824 = select(a_800,i5),
inference(superposition,[],[f49,f1177]) ).
fof(f1215,plain,
e_803 = e_824,
inference(forward_demodulation,[],[f1210,f40]) ).
fof(f1216,plain,
e_801 = e_822,
inference(forward_demodulation,[],[f1209,f39]) ).
fof(f1277,plain,
a_823 = store(a_821,i5,e_801),
inference(superposition,[],[f26,f1216]) ).
fof(f1278,plain,
store(a_800,i5,e_801) = a_823,
inference(forward_demodulation,[],[f1277,f1177]) ).
fof(f1280,plain,
a_802 = a_823,
inference(forward_demodulation,[],[f1278,f14]) ).
fof(f1289,plain,
a_825 = store(a_802,i2,e_824),
inference(superposition,[],[f27,f1280]) ).
fof(f1290,plain,
store(a_802,i2,e_803) = a_825,
inference(forward_demodulation,[],[f1289,f1215]) ).
fof(f1293,plain,
a_804 = a_825,
inference(forward_demodulation,[],[f1290,f15]) ).
fof(f1319,plain,
e_828 = select(a_804,i5),
inference(superposition,[],[f51,f1293]) ).
fof(f1324,plain,
a_827 = store(a_804,i5,e_824),
inference(superposition,[],[f224,f1293]) ).
fof(f1325,plain,
a_827 = store(a_804,i5,e_803),
inference(forward_demodulation,[],[f1324,f1215]) ).
fof(f1329,plain,
e_807 = e_828,
inference(forward_demodulation,[],[f1319,f42]) ).
fof(f1332,plain,
a_806 = a_827,
inference(forward_demodulation,[],[f1325,f195]) ).
fof(f1353,plain,
a_829 = store(a_827,i2,e_807),
inference(superposition,[],[f29,f1329]) ).
fof(f1354,plain,
store(a_806,i2,e_807) = a_829,
inference(forward_demodulation,[],[f1353,f1332]) ).
fof(f1360,plain,
a_808 = a_829,
inference(forward_demodulation,[],[f1354,f17]) ).
fof(f1478,plain,
a_808 != a_808,
inference(superposition,[],[f52,f1360]) ).
fof(f1479,plain,
$false,
inference(trivial_inequality_removal,[],[f1478]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV543-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 11:40:02 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.84/0.42 % (1873865)Will run a generic schedule for satisfiability detection.
% 0.84/0.42 % (1873870)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1219110112_2999 on theBenchmark for (2999ds/0Mi)
% 0.84/0.42 % TRYING [1]
% 0.84/0.42 % TRYING [2]
% 0.84/0.42 % TRYING [3]
% 0.84/0.42 % (1873871)% WARNING: option uhcvi not known.
% 0.84/0.42 % (1873875)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3234238197:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.84/0.42 % (1873871)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4266559944:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.84/0.42 % (1873872)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3291388311:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.84/0.42 % (1873873)dis+10_1_sil=32000:sp=arity:random_seed=3955861691:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.84/0.42 % (1873874)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=102108285:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.84/0.42 % TRYING [4]
% 0.84/0.42 % (1873876)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3472530684:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.84/0.42 % TRYING [5]
% 0.84/0.42 % (1873873)Instruction limit reached!
% 0.84/0.42 % (1873873)------------------------------
% 0.84/0.42 % (1873873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.42 % (1873873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.42 % (1873873)CaDiCaL version: 2.1.3
% 0.84/0.42 % (1873873)Termination reason: Instruction limit
% 0.84/0.42 % (1873873)Termination phase: Saturation
% 0.84/0.42 % (1873873)Time elapsed: 0.052 s
% 0.84/0.42 % (1873873)Peak memory usage: 12 MB
% 0.84/0.42 % (1873873)Instructions burned: 104 (million)
% 0.84/0.42 % (1873874)Instruction limit reached!
% 0.84/0.42 % (1873874)------------------------------
% 0.84/0.42 % (1873874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.42 % (1873874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.42 % (1873874)CaDiCaL version: 2.1.3
% 0.84/0.42 % (1873874)Termination reason: Instruction limit
% 0.84/0.42 % (1873874)Termination phase: Saturation
% 0.84/0.42 % (1873874)Time elapsed: 0.061 s
% 0.84/0.42 % (1873874)Peak memory usage: 13 MB
% 0.84/0.42 % (1873874)Instructions burned: 119 (million)
% 0.84/0.42 % TRYING [6]
% 0.84/0.42 % (1873875)Instruction limit reached!
% 0.84/0.42 % (1873875)------------------------------
% 0.84/0.42 % (1873875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.42 % (1873875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.42 % (1873875)CaDiCaL version: 2.1.3
% 0.84/0.42 % (1873875)Termination reason: Instruction limit
% 0.84/0.42 % (1873875)Termination phase: Saturation
% 0.84/0.42 % (1873875)Time elapsed: 0.067 s
% 0.84/0.42 % (1873875)Peak memory usage: 12 MB
% 0.84/0.42 % (1873875)Instructions burned: 133 (million)
% 0.84/0.42 % (1873884)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2226473372:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.84/0.42 % TRYING [1]
% 0.84/0.42 % TRYING [2]
% 0.84/0.42 % TRYING [3]
% 0.84/0.42 % (1873885)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=451022013:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.84/0.42 % (1873886)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=1935787594:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.84/0.42 % TRYING [4]
% 0.84/0.42 % (1873876)Instruction limit reached!
% 0.84/0.42 % (1873876)------------------------------
% 0.84/0.42 % (1873876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.42 % (1873876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.42 % (1873876)CaDiCaL version: 2.1.3
% 0.84/0.42 % (1873876)Termination reason: Instruction limit
% 0.84/0.42 % (1873876)Termination phase: Saturation
% 0.84/0.42 % (1873876)Time elapsed: 0.093 s
% 0.84/0.42 % (1873876)Peak memory usage: 13 MB
% 0.84/0.42 % (1873876)Instructions burned: 159 (million)
% 0.84/0.42 % (1873890)ott-21_1_sil=16000:fs=off:random_seed=28067554:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.84/0.42 % TRYING [5]
% 0.84/0.42 % (1873890) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1873865-1873890"...
% 0.84/0.42 % (1873890)...printing done.
% 0.84/0.42 % (1873890)Refutation found. Thanks to Tanya!
% 0.84/0.42 % SZS status Unsatisfiable for theBenchmark
% 0.84/0.42 % SZS output start Proof for theBenchmark
% See solution above
% 0.84/0.42 % (1873890)------------------------------
% 0.84/0.42 % (1873890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.84/0.42 % (1873890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.84/0.42 % (1873890)CaDiCaL version: 2.1.3
% 0.84/0.42 % (1873890)Termination reason: Refutation
% 0.84/0.42 % (1873890)Time elapsed: 0.031 s
% 0.84/0.42 % (1873890)Peak memory usage: 12 MB
% 0.84/0.42 % (1873890)Instructions burned: 58 (million)
% 0.84/0.42 % (1873865)Success in time 0.186 s
% 0.84/0.42 % Vampire exiting
%------------------------------------------------------------------------------