%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV533-1.004 : 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 : n001.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:24:55 PM UTC 2026
% Result : Satisfiable 0.08s 0.26s
% Output : Saturation 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u85,hypothesis,
select(a1,X0) = select(a_417,X0) ).
cnf(u562,hypothesis,
select(a_417,X0) = select(a_418,X0) ).
cnf(u567,hypothesis,
select(a_418,X0) = select(a_420,X0) ).
cnf(u1204,hypothesis,
select(a_428,X0) = select(a_430,X0) ).
cnf(u1219,hypothesis,
select(a_431,X0) = select(a_432,X0) ).
cnf(u1233,hypothesis,
i0 = i3 ).
cnf(u1237,hypothesis,
e_419 = e_435 ).
cnf(u1378,hypothesis,
select(a_424,X0) = select(a_426,X0) ).
cnf(u1870,hypothesis,
e_423 = e_427 ).
cnf(u1873,hypothesis,
i0 != i2 ).
cnf(u1901,hypothesis,
select(a_428,X0) = select(a_426,X0) ).
cnf(u1911,hypothesis,
e_419 = e_423 ).
cnf(u2096,hypothesis,
select(a_438,X0) = select(a_440,X0) ).
cnf(u2111,hypothesis,
select(a_438,X0) = select(a_426,X0) ).
cnf(u2134,hypothesis,
select(a_418,X0) = select(a_426,X0) ).
cnf(hyp6,hypothesis,
a_428 = store(a_426,i2,e_427) ).
cnf(hyp16,hypothesis,
e_421 = select(a_418,i0) ).
cnf(u2066,hypothesis,
e_419 = select(a_426,i0) ).
cnf(u37,hypothesis,
e_423 = select(a_424,i3) ).
cnf(u47,hypothesis,
e_435 = e_437 ).
cnf(u1322,hypothesis,
a_426 = a_436 ).
cnf(u830,hypothesis,
e_419 = select(a_418,i0) ).
cnf(u858,hypothesis,
e_419 = select(a_422,i3) ).
cnf(u1357,hypothesis,
e_423 = select(a_418,i2) ).
cnf(u1242,hypothesis,
a_434 = store(a_432,i0,e_433) ).
cnf(u835,hypothesis,
a_426 = store(a_424,i2,e_419) ).
cnf(hyp9,hypothesis,
a_432 = store(a_431,i0,e_419) ).
cnf(hyp24,hypothesis,
e_439 = select(a_436,i0) ).
cnf(u71,hypothesis,
( select(a_431,X0) = select(a_432,X0)
| i0 = X0 ) ).
cnf(u836,hypothesis,
a_431 = store(a_418,i3,e_419) ).
cnf(u45,hypothesis,
a_426 = store(a_424,i2,e_421) ).
cnf(u30,hypothesis,
e_416 = select(a_418,i1) ).
cnf(u848,hypothesis,
e_419 = select(a_426,i2) ).
cnf(u57,hypothesis,
e_421 = select(a_430,i0) ).
cnf(hyp19,hypothesis,
e_427 = select(a_426,i0) ).
cnf(u861,hypothesis,
e_419 = e_425 ).
cnf(hyp21,hypothesis,
e_433 = select(a_432,i2) ).
cnf(u68,hypothesis,
( select(a_418,X0) = select(a_420,X0)
| i0 = X0 ) ).
cnf(u34,hypothesis,
e_437 = select(a_438,i0) ).
cnf(u2059,hypothesis,
a_428 = store(a_426,i2,e_419) ).
cnf(u1298,hypothesis,
a_422 = a_432 ).
cnf(hyp17,hypothesis,
e_423 = select(a_422,i2) ).
cnf(u837,hypothesis,
a_422 = store(a_420,i3,e_419) ).
cnf(u1262,hypothesis,
a_420 = a_431 ).
cnf(u2058,hypothesis,
a_440 = store(a_438,i2,e_419) ).
cnf(u32,hypothesis,
e_429 = select(a_430,i0) ).
cnf(u1313,hypothesis,
a_424 = a_434 ).
cnf(u1215,hypothesis,
e_419 = select(a_428,i0) ).
cnf(u42,hypothesis,
e_439 = select(a_440,i2) ).
cnf(hyp0,hypothesis,
a_417 = store(a1,i1,e_416) ).
cnf(hyp18,hypothesis,
e_425 = select(a_422,i3) ).
cnf(u1895,hypothesis,
e_423 = select(a_426,i0) ).
cnf(u31,hypothesis,
e_419 = select(a_420,i0) ).
cnf(u1352,hypothesis,
select(a_418,X0) = select(a_422,X0) ).
cnf(u1333,hypothesis,
e_427 = e_439 ).
cnf(u1990,hypothesis,
a_424 = store(a_422,i0,e_419) ).
cnf(u2130,hypothesis,
( select(a_418,X0) = select(a_426,X0)
| i0 = X0 ) ).
cnf(hyp8,hypothesis,
a_431 = store(a_418,i3,e_421) ).
cnf(u29,hypothesis,
e_416 = select(a_417,i1) ).
cnf(u67,hypothesis,
( select(a_417,X0) = select(a_418,X0)
| i1 = X0 ) ).
cnf(u832,hypothesis,
e_419 = e_421 ).
cnf(u41,hypothesis,
e_435 = select(a_436,i2) ).
cnf(hyp3,hypothesis,
a_422 = store(a_420,i3,e_421) ).
cnf(u69,hypothesis,
( select(a_428,X0) = select(a_430,X0)
| i0 = X0 ) ).
cnf(hyp5,hypothesis,
a_426 = store(a_424,i2,e_425) ).
cnf(hyp15,hypothesis,
e_419 = select(a_418,i3) ).
cnf(u1264,hypothesis,
a_438 = store(a_436,i0,e_419) ).
cnf(hyp1,hypothesis,
a_418 = store(a_417,i1,e_416) ).
cnf(u49,hypothesis,
a_438 = store(a_436,i0,e_435) ).
cnf(hyp11,hypothesis,
a_436 = store(a_434,i2,e_435) ).
cnf(u1265,hypothesis,
a_436 = store(a_434,i2,e_419) ).
cnf(hyp13,hypothesis,
a_440 = store(a_438,i2,e_439) ).
cnf(hyp23,hypothesis,
e_437 = select(a_436,i2) ).
cnf(u1284,hypothesis,
e_419 = select(a_436,i2) ).
cnf(hyp2,hypothesis,
a_420 = store(a_418,i0,e_419) ).
cnf(u54,hypothesis,
e_435 = select(a_438,i0) ).
cnf(u82,hypothesis,
( select(a_438,X0) = select(a_440,X0)
| i2 = X0 ) ).
cnf(hyp12,hypothesis,
a_438 = store(a_436,i0,e_437) ).
cnf(hyp14,hypothesis,
e_416 = select(a1,i1) ).
cnf(u2052,hypothesis,
e_419 = e_427 ).
cnf(u854,hypothesis,
e_419 = select(a_431,i3) ).
cnf(u1347,hypothesis,
e_427 = select(a_440,i2) ).
cnf(u841,hypothesis,
e_419 = e_429 ).
cnf(u78,hypothesis,
( select(a_424,X0) = select(a_426,X0)
| i2 = X0 ) ).
cnf(u52,hypothesis,
a_430 = store(a_428,i0,e_421) ).
cnf(u80,hypothesis,
( select(a_428,X0) = select(a_426,X0)
| i2 = X0 ) ).
cnf(hyp10,hypothesis,
a_434 = store(a_432,i3,e_433) ).
cnf(hyp20,hypothesis,
e_429 = select(a_426,i2) ).
cnf(hyp22,hypothesis,
e_435 = select(a_432,i3) ).
cnf(u834,hypothesis,
a_430 = store(a_428,i0,e_419) ).
cnf(u35,hypothesis,
e_421 = select(a_431,i3) ).
cnf(u1240,hypothesis,
a_424 = store(a_422,i0,e_423) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u2107,hypothesis,
e_419 = select(a_438,i2) ).
cnf(u839,hypothesis,
e_419 = select(a_430,i0) ).
cnf(u1248,hypothesis,
e_423 = select(a_424,i0) ).
cnf(u2074,hypothesis,
e_419 = select(a_440,i2) ).
cnf(u1339,hypothesis,
a_440 = store(a_438,i2,e_427) ).
cnf(u2076,hypothesis,
e_419 = e_439 ).
cnf(u33,hypothesis,
e_419 = select(a_432,i0) ).
cnf(u43,hypothesis,
e_421 = e_425 ).
cnf(u2148,hypothesis,
e_419 = select(a_418,i2) ).
cnf(u1367,hypothesis,
( select(a_438,X0) = select(a_426,X0)
| i0 = X0 ) ).
cnf(hyp7,hypothesis,
a_430 = store(a_428,i0,e_429) ).
cnf(u1249,hypothesis,
e_433 = select(a_434,i0) ).
cnf(goal,negated_conjecture,
a_430 != a_440 ).
cnf(u1260,hypothesis,
a_422 = store(a_420,i0,e_419) ).
cnf(u38,hypothesis,
e_433 = select(a_434,i3) ).
cnf(u66,hypothesis,
( select(a1,X0) = select(a_417,X0)
| i1 = X0 ) ).
cnf(u40,hypothesis,
e_427 = select(a_428,i2) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u50,hypothesis,
e_421 = e_429 ).
cnf(u2061,hypothesis,
e_419 = select(a_428,i2) ).
cnf(u1255,hypothesis,
e_419 = select(a_422,i0) ).
cnf(u1304,hypothesis,
e_423 = e_433 ).
cnf(u1293,hypothesis,
e_419 = select(a_438,i0) ).
cnf(u36,hypothesis,
e_421 = select(a_422,i3) ).
cnf(u46,hypothesis,
e_421 = select(a_426,i2) ).
cnf(u1286,hypothesis,
e_419 = e_437 ).
cnf(hyp4,hypothesis,
a_424 = store(a_422,i3,e_423) ).
cnf(u1329,hypothesis,
a_438 = store(a_426,i0,e_419) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV533-1.004 : 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.18 % Computer : n001.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:40:48 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 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.08/0.26 % (296900)Will run a generic schedule for satisfiability detection.
% 0.08/0.26 % (296907)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=924393951:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.26 % (296906)% WARNING: option uhcvi not known.
% 0.08/0.26 % (296908)dis+10_1_sil=32000:sp=arity:random_seed=2986921301:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.26 % (296905)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=374365661_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.26 % (296911)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1734957560:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.26 % (296909)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3589840594:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.26 % (296910)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3026098076:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.26 % (296906)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1850152207:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.26 % TRYING [1]
% 0.08/0.26 % TRYING [2]
% 0.08/0.26 % TRYING [3]
% 0.08/0.26 % TRYING [4]
% 0.08/0.26 % (296907) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-296900-296907"...
% 0.08/0.26 % (296907)...printing done.
% 0.08/0.26 % SZS status Satisfiable for theBenchmark
% 0.08/0.26 % SZS output start Saturation.
% See solution above
% 0.08/0.26 % SZS output start Definitions and Model Updates.
% 0.08/0.26 % SZS output end Definitions and Model Updates.
% 0.08/0.26 % (296907)------------------------------
% 0.08/0.26 % (296907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.26 % (296907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.26 % (296907)CaDiCaL version: 2.1.3
% 0.08/0.26 % (296907)Termination reason: Satisfiable
% 0.08/0.26 % (296907)Time elapsed: 0.016 s
% 0.08/0.26 % (296907)Peak memory usage: 12 MB
% 0.08/0.26 % (296907)Instructions burned: 54 (million)
% 0.08/0.26 % (296900)Success in time 0.044 s
% 0.08/0.26 % Vampire exiting
%------------------------------------------------------------------------------