%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n009.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:16:55 PM UTC 2026
% Result : Satisfiable 0.19s 1.04s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u77,hypothesis,
i1 = i3 ).
cnf(u81,hypothesis,
e_419 = select(a_417,i3) ).
cnf(u86,hypothesis,
i1 = i0 ).
cnf(u125,hypothesis,
e_433 = select(a_431,i2) ).
cnf(u139,hypothesis,
e_416 = e_435 ).
cnf(u183,hypothesis,
e_423 = select(a_420,i2) ).
cnf(u197,hypothesis,
e_433 = select(a_418,i2) ).
cnf(u209,hypothesis,
e_423 = e_433 ).
cnf(u223,hypothesis,
e_423 = e_427 ).
cnf(u242,hypothesis,
e_423 = e_439 ).
cnf(u279,hypothesis,
e_423 = select(a_417,i2) ).
cnf(hyp6,hypothesis,
a_428 = store(a_426,i2,e_427) ).
cnf(u58,hypothesis,
e_421 = e_425 ).
cnf(hyp16,hypothesis,
e_421 = select(a_418,i0) ).
cnf(u37,hypothesis,
e_423 = select(a_424,i3) ).
cnf(u47,hypothesis,
( select(a_431,X0) = select(a_432,X0)
| i0 = X0 ) ).
cnf(u408,hypothesis,
a_424 = a_434 ).
cnf(u171,hypothesis,
a_436 = store(a_434,i2,e_416) ).
cnf(u100,hypothesis,
e_439 = select(a_436,i1) ).
cnf(u189,hypothesis,
a_432 = store(a_431,i1,e_416) ).
cnf(u110,hypothesis,
a_430 = store(a_428,i1,e_416) ).
cnf(hyp24,hypothesis,
e_439 = select(a_436,i0) ).
cnf(u112,hypothesis,
a_431 = store(a_418,i3,e_416) ).
cnf(u156,hypothesis,
e_416 = select(a_431,i1) ).
cnf(u245,hypothesis,
a_440 = store(a_438,i2,e_423) ).
cnf(u55,hypothesis,
( select(a_436,X0) = select(a_434,X0)
| i2 = X0 ) ).
cnf(hyp9,hypothesis,
a_432 = store(a_431,i0,e_419) ).
cnf(u101,hypothesis,
e_419 = select(a_420,i1) ).
cnf(hyp19,hypothesis,
e_427 = select(a_426,i0) ).
cnf(u111,hypothesis,
a_426 = store(a_424,i2,e_416) ).
cnf(hyp21,hypothesis,
e_433 = select(a_432,i2) ).
cnf(u113,hypothesis,
a_422 = store(a_420,i3,e_416) ).
cnf(u34,hypothesis,
e_437 = select(a_438,i0) ).
cnf(u370,hypothesis,
a_420 = a_431 ).
cnf(u326,hypothesis,
( select(a_420,X0) = select(a_422,X0)
| i1 = X0 ) ).
cnf(u331,hypothesis,
e_423 = select(a_428,i2) ).
cnf(u322,hypothesis,
( select(a_432,X0) = select(a_434,X0)
| i1 = X0 ) ).
cnf(hyp17,hypothesis,
e_423 = select(a_422,i2) ).
cnf(u30,hypothesis,
e_416 = select(a_418,i1) ).
cnf(u32,hypothesis,
e_429 = select(a_430,i0) ).
cnf(hyp0,hypothesis,
a_417 = store(a1,i1,e_416) ).
cnf(u42,hypothesis,
e_439 = select(a_440,i2) ).
cnf(u145,hypothesis,
a_434 = store(a_432,i1,e_433) ).
cnf(u353,hypothesis,
e_416 = e_429 ).
cnf(hyp18,hypothesis,
e_425 = select(a_422,i3) ).
cnf(u31,hypothesis,
e_419 = select(a_420,i0) ).
cnf(u306,hypothesis,
( select(a_431,X0) = select(a_432,X0)
| i1 = X0 ) ).
cnf(u324,hypothesis,
( select(a_418,X0) = select(a_431,X0)
| i1 = X0 ) ).
cnf(u155,hypothesis,
e_416 = select(a_422,i1) ).
cnf(u94,hypothesis,
a_420 = store(a_418,i1,e_419) ).
cnf(hyp8,hypothesis,
a_431 = store(a_418,i3,e_421) ).
cnf(u44,hypothesis,
( select(a_417,X0) = select(a_418,X0)
| i1 = X0 ) ).
cnf(u29,hypothesis,
e_416 = select(a_417,i1) ).
cnf(u432,hypothesis,
e_416 = select(a_438,i1) ).
cnf(u106,hypothesis,
e_421 = select(a_430,i1) ).
cnf(u39,hypothesis,
e_425 = select(a_426,i2) ).
cnf(u67,hypothesis,
a_438 = store(a_436,i0,e_435) ).
cnf(u41,hypothesis,
e_435 = select(a_436,i2) ).
cnf(hyp3,hypothesis,
a_422 = store(a_420,i3,e_421) ).
cnf(u51,hypothesis,
( select(a_422,X0) = select(a_424,X0)
| i3 = X0 ) ).
cnf(hyp5,hypothesis,
a_426 = store(a_424,i2,e_425) ).
cnf(hyp15,hypothesis,
e_419 = select(a_418,i3) ).
cnf(u329,hypothesis,
e_416 = select(a_436,i2) ).
cnf(u428,hypothesis,
a_426 = a_436 ).
cnf(u313,hypothesis,
( select(a_428,X0) = select(a_430,X0)
| i1 = X0 ) ).
cnf(u372,hypothesis,
e_416 = select(a_420,i1) ).
cnf(hyp1,hypothesis,
a_418 = store(a_417,i1,e_416) ).
cnf(u49,hypothesis,
( select(a_418,X0) = select(a_431,X0)
| i3 = X0 ) ).
cnf(hyp11,hypothesis,
a_436 = store(a_434,i2,e_435) ).
cnf(u59,hypothesis,
a_426 = store(a_424,i2,e_421) ).
cnf(u103,hypothesis,
e_419 = select(a_432,i1) ).
cnf(hyp13,hypothesis,
a_440 = store(a_438,i2,e_439) ).
cnf(u108,hypothesis,
a_438 = store(a_436,i1,e_435) ).
cnf(u105,hypothesis,
e_435 = select(a_438,i1) ).
cnf(hyp23,hypothesis,
e_437 = select(a_436,i2) ).
cnf(u335,hypothesis,
e_416 = e_437 ).
cnf(u226,hypothesis,
a_428 = store(a_426,i2,e_423) ).
cnf(u159,hypothesis,
e_416 = e_419 ).
cnf(u337,hypothesis,
e_423 = select(a_440,i2) ).
cnf(hyp2,hypothesis,
a_420 = store(a_418,i0,e_419) ).
cnf(u54,hypothesis,
( select(a_428,X0) = select(a_426,X0)
| i2 = X0 ) ).
cnf(u347,hypothesis,
e_416 = select(a_426,i2) ).
cnf(hyp12,hypothesis,
a_438 = store(a_436,i0,e_437) ).
cnf(u56,hypothesis,
( select(a_438,X0) = select(a_440,X0)
| i2 = X0 ) ).
cnf(hyp14,hypothesis,
e_416 = select(a1,i1) ).
cnf(u160,hypothesis,
a_431 = store(a_418,i1,e_416) ).
cnf(u96,hypothesis,
a_432 = store(a_431,i1,e_419) ).
cnf(u315,hypothesis,
( select(a_422,X0) = select(a_424,X0)
| i1 = X0 ) ).
cnf(u314,hypothesis,
e_416 = select(a_430,i1) ).
cnf(u303,hypothesis,
( select(a_418,X0) = select(a_420,X0)
| i1 = X0 ) ).
cnf(u157,hypothesis,
e_419 = e_435 ).
cnf(u36,hypothesis,
e_421 = select(a_422,i3) ).
cnf(u52,hypothesis,
( select(a_432,X0) = select(a_434,X0)
| i3 = X0 ) ).
cnf(hyp10,hypothesis,
a_434 = store(a_432,i3,e_433) ).
cnf(u62,hypothesis,
e_421 = e_429 ).
cnf(hyp20,hypothesis,
e_429 = select(a_426,i2) ).
cnf(hyp22,hypothesis,
e_435 = select(a_432,i3) ).
cnf(u69,hypothesis,
e_421 = select(a_426,i2) ).
cnf(u143,hypothesis,
a_424 = store(a_422,i1,e_423) ).
cnf(u35,hypothesis,
e_421 = select(a_431,i3) ).
cnf(u384,hypothesis,
a_422 = a_432 ).
cnf(u53,hypothesis,
( select(a_424,X0) = select(a_426,X0)
| i2 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u441,hypothesis,
a_438 = store(a_426,i1,e_416) ).
cnf(u310,hypothesis,
( select(a_436,X0) = select(a_438,X0)
| i1 = X0 ) ).
cnf(u299,hypothesis,
a_438 = store(a_436,i1,e_416) ).
cnf(u188,hypothesis,
a_420 = store(a_418,i1,e_416) ).
cnf(u33,hypothesis,
e_419 = select(a_432,i0) ).
cnf(u152,hypothesis,
e_433 = select(a_434,i1) ).
cnf(u43,hypothesis,
( select(a1,X0) = select(a_417,X0)
| i1 = X0 ) ).
cnf(u352,hypothesis,
e_416 = e_425 ).
cnf(hyp7,hypothesis,
a_430 = store(a_428,i0,e_429) ).
cnf(u99,hypothesis,
e_427 = select(a_426,i1) ).
cnf(goal,negated_conjecture,
a_430 != a_440 ).
cnf(u228,hypothesis,
a_434 = store(a_432,i1,e_423) ).
cnf(u38,hypothesis,
e_433 = select(a_434,i3) ).
cnf(u66,hypothesis,
e_435 = e_437 ).
cnf(u40,hypothesis,
e_427 = select(a_428,i2) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u50,hypothesis,
( select(a_420,X0) = select(a_422,X0)
| i3 = X0 ) ).
cnf(u486,hypothesis,
( select(a_438,X0) = select(a_426,X0)
| i1 = X0 ) ).
cnf(u45,hypothesis,
( select(a_418,X0) = select(a_420,X0)
| i0 = X0 ) ).
cnf(u161,hypothesis,
a_422 = store(a_420,i1,e_416) ).
cnf(u107,hypothesis,
e_416 = e_421 ).
cnf(u151,hypothesis,
e_423 = select(a_424,i1) ).
cnf(u64,hypothesis,
a_430 = store(a_428,i0,e_421) ).
cnf(u46,hypothesis,
( select(a_428,X0) = select(a_430,X0)
| i0 = X0 ) ).
cnf(hyp4,hypothesis,
a_424 = store(a_422,i3,e_423) ).
cnf(u48,hypothesis,
( select(a_436,X0) = select(a_438,X0)
| i0 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % 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 THM
% 0.10/0.17 % Computer : n009.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 11:35:00 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running first-order theorem proving
% 0.10/0.21 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
% 0.19/1.04 % (2979022)Input is clausal, will run a generic CNF schedule.
% 0.19/1.04 % (2979115)dis-21_1_sil=8000:lcm=predicate:random_seed=4160942122:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 0.19/1.04 % (2979115)Refutation not found, incomplete strategy
% 0.19/1.04 % (2979115)------------------------------
% 0.19/1.04 % (2979115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/1.04 % (2979115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/1.04 % (2979115)CaDiCaL version: 2.1.3
% 0.19/1.04 % (2979115)Termination reason: Refutation not found, incomplete strategy
% 0.19/1.04 % (2979115)Time elapsed: 0.001 s
% 0.19/1.04 % (2979115)Peak memory usage: 88 MB
% 0.19/1.04 % (2979115)Instructions burned: 1 (million)
% 0.19/1.04 % (2979109)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1408417304:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.19/1.04 % (2979111)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3526391484:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.19/1.04 % (2979114)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=804913146:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.19/1.04 % (2979112)lrs+10_1_sil=8000:sp=occurrence:random_seed=2276797749:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.19/1.04 % (2979113)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=303852624:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.19/1.04 % (2979110)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3763742166:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.19/1.04 % (2979112)First to succeed.
% 0.19/1.04 % (2979112)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2979022"
% 0.19/1.04 % (2979114)Refutation not found, incomplete strategy
% 0.19/1.04 % (2979114)------------------------------
% 0.19/1.04 % (2979114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/1.04 % (2979114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/1.04 % (2979114)CaDiCaL version: 2.1.3
% 0.19/1.04 % (2979114)Termination reason: Refutation not found, incomplete strategy
% 0.19/1.04 % (2979114)Time elapsed: 0.015 s
% 0.19/1.04 % (2979114)Peak memory usage: 88 MB
% 0.19/1.04 % (2979114)Instructions burned: 23 (million)
% 0.19/1.04 % (2979113)Instruction limit reached!
% 0.19/1.04 % (2979113)------------------------------
% 0.19/1.04 % (2979113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/1.04 % (2979113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/1.04 % (2979113)CaDiCaL version: 2.1.3
% 0.19/1.04 % (2979113)Termination reason: Instruction limit
% 0.19/1.04 % (2979113)Termination phase: Saturation
% 0.19/1.04 % (2979113)Time elapsed: 0.065 s
% 0.19/1.04 % (2979113)Peak memory usage: 88 MB
% 0.19/1.04 % (2979113)Instructions burned: 115 (million)
% 0.19/1.04 % (2979115)------------------------------
% 0.19/1.04 % (2979115)------------------------------
% 0.19/1.04 % (2979178)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1982580426:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 0.19/1.04 % (2979179)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4193850714:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 0.19/1.04 % (2979178)Refutation not found, incomplete strategy
% 0.19/1.04 % (2979178)------------------------------
% 0.19/1.04 % (2979178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/1.04 % (2979178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/1.04 % (2979178)CaDiCaL version: 2.1.3
% 0.19/1.04 % (2979178)Termination reason: Refutation not found, incomplete strategy
% 0.19/1.04 % (2979178)Time elapsed: 0.016 s
% 0.19/1.04 % (2979178)Peak memory usage: 88 MB
% 0.19/1.04 % (2979178)Instructions burned: 23 (million)
% 0.19/1.04 % (2979114)------------------------------
% 0.19/1.04 % (2979114)------------------------------
% 0.19/1.04 % SZS status Satisfiable for theBenchmark
% 0.19/1.04 % SZS output start Saturation.
% See solution above
% 0.19/1.04 % SZS output start Definitions and Model Updates.
% 0.19/1.04 % SZS output end Definitions and Model Updates.
% 0.19/1.04 % (2979112)------------------------------
% 0.19/1.04 % (2979112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/1.04 % (2979112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/1.04 % (2979112)CaDiCaL version: 2.1.3
% 0.19/1.04 % (2979112)Termination reason: Satisfiable
% 0.19/1.04 % (2979112)Time elapsed: 0.012 s
% 0.19/1.04 % (2979112)Peak memory usage: 88 MB
% 0.19/1.04 % (2979112)Instructions burned: 19 (million)
% 0.19/1.04 % (2979112)------------------------------
% 0.19/1.04 % (2979112)------------------------------
% 0.19/1.04 % (2979022)Success in time 0.427 s
% 0.19/1.04 % Vampire exiting
%------------------------------------------------------------------------------