%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV534-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:56 PM UTC 2026
% Result : Satisfiable 3.85s 1.32s
% Output : Saturation 3.85s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u78,hypothesis,
i1 = i3 ).
cnf(u82,hypothesis,
e_420 = select(a_418,i3) ).
cnf(u87,hypothesis,
i1 = i0 ).
cnf(u124,hypothesis,
e_434 = select(a_432,i2) ).
cnf(u138,hypothesis,
e_417 = e_436 ).
cnf(u185,hypothesis,
e_424 = select(a_421,i2) ).
cnf(u199,hypothesis,
e_434 = select(a_419,i2) ).
cnf(u211,hypothesis,
e_424 = e_434 ).
cnf(u227,hypothesis,
e_424 = e_428 ).
cnf(u254,hypothesis,
e_424 = e_438 ).
cnf(u262,hypothesis,
e_424 = e_440 ).
cnf(u310,hypothesis,
e_424 = select(a_418,i2) ).
cnf(hyp6,hypothesis,
a_429 = store(a_427,i2,e_428) ).
cnf(u58,hypothesis,
e_422 = e_426 ).
cnf(u102,hypothesis,
e_420 = select(a_421,i1) ).
cnf(hyp16,hypothesis,
e_422 = select(a_419,i0) ).
cnf(u191,hypothesis,
a_433 = store(a_432,i1,e_417) ).
cnf(u104,hypothesis,
e_420 = select(a_433,i1) ).
cnf(u37,hypothesis,
e_424 = select(a_425,i3) ).
cnf(u506,hypothesis,
( select(a_439,X0) = select(a_427,X0)
| i1 = X0 ) ).
cnf(u47,hypothesis,
( select(a_432,X0) = select(a_433,X0)
| i0 = X0 ) ).
cnf(u416,hypothesis,
e_424 = select(a_435,i1) ).
cnf(u100,hypothesis,
e_428 = select(a_427,i1) ).
cnf(u110,hypothesis,
a_427 = store(a_425,i2,e_417) ).
cnf(u401,hypothesis,
a_423 = a_433 ).
cnf(u45,hypothesis,
( select(a_419,X0) = select(a_421,X0)
| i0 = X0 ) ).
cnf(u377,hypothesis,
e_417 = e_426 ).
cnf(u55,hypothesis,
( select(a_429,X0) = select(a_427,X0)
| i2 = X0 ) ).
cnf(u354,hypothesis,
e_424 = select(a_439,i1) ).
cnf(hyp9,hypothesis,
a_433 = store(a_432,i0,e_420) ).
cnf(u101,hypothesis,
e_440 = select(a_437,i1) ).
cnf(hyp19,hypothesis,
e_428 = select(a_427,i0) ).
cnf(u111,hypothesis,
a_432 = store(a_419,i3,e_417) ).
cnf(hyp21,hypothesis,
e_434 = select(a_433,i2) ).
cnf(u34,hypothesis,
e_438 = select(a_439,i0) ).
cnf(u343,hypothesis,
( select(a_419,X0) = select(a_432,X0)
| i1 = X0 ) ).
cnf(u425,hypothesis,
a_425 = a_435 ).
cnf(u345,hypothesis,
( select(a_421,X0) = select(a_423,X0)
| i1 = X0 ) ).
cnf(u389,hypothesis,
e_417 = select(a_421,i1) ).
cnf(u338,hypothesis,
( select(a_433,X0) = select(a_435,X0)
| i1 = X0 ) ).
cnf(u44,hypothesis,
( select(a_418,X0) = select(a_419,X0)
| i1 = X0 ) ).
cnf(u144,hypothesis,
a_435 = store(a_433,i1,e_434) ).
cnf(hyp17,hypothesis,
e_424 = select(a_423,i2) ).
cnf(u109,hypothesis,
a_431 = store(a_429,i1,e_417) ).
cnf(u30,hypothesis,
e_417 = select(a_419,i1) ).
cnf(u41,hypothesis,
e_428 = select(a_429,i2) ).
cnf(u32,hypothesis,
e_430 = select(a_431,i0) ).
cnf(u378,hypothesis,
e_417 = e_430 ).
cnf(u42,hypothesis,
e_436 = select(a_437,i2) ).
cnf(hyp0,hypothesis,
a_418 = store(a1,i1,e_417) ).
cnf(u145,hypothesis,
a_441 = store(a_439,i1,e_440) ).
cnf(hyp18,hypothesis,
e_426 = select(a_423,i3) ).
cnf(u98,hypothesis,
a_439 = store(a_437,i1,e_438) ).
cnf(u31,hypothesis,
e_420 = select(a_421,i0) ).
cnf(u163,hypothesis,
a_423 = store(a_421,i1,e_417) ).
cnf(u230,hypothesis,
a_429 = store(a_427,i2,e_424) ).
cnf(hyp23,hypothesis,
e_438 = select(a_437,i3) ).
cnf(u215,hypothesis,
a_435 = store(a_433,i1,e_424) ).
cnf(u173,hypothesis,
a_437 = store(a_435,i2,e_417) ).
cnf(hyp8,hypothesis,
a_432 = store(a_419,i3,e_422) ).
cnf(u29,hypothesis,
e_417 = select(a_418,i1) ).
cnf(u106,hypothesis,
e_422 = select(a_431,i1) ).
cnf(u39,hypothesis,
e_440 = select(a_441,i3) ).
cnf(u152,hypothesis,
e_424 = select(a_425,i1) ).
cnf(hyp3,hypothesis,
a_423 = store(a_421,i3,e_422) ).
cnf(u51,hypothesis,
( select(a_423,X0) = select(a_425,X0)
| i3 = X0 ) ).
cnf(u95,hypothesis,
a_421 = store(a_419,i1,e_420) ).
cnf(hyp5,hypothesis,
a_427 = store(a_425,i2,e_426) ).
cnf(u268,hypothesis,
a_441 = store(a_439,i1,e_424) ).
cnf(u97,hypothesis,
a_433 = store(a_432,i1,e_420) ).
cnf(hyp15,hypothesis,
e_420 = select(a_419,i3) ).
cnf(u327,hypothesis,
( select(a_437,X0) = select(a_439,X0)
| i1 = X0 ) ).
cnf(u329,hypothesis,
( select(a_429,X0) = select(a_431,X0)
| i1 = X0 ) ).
cnf(u454,hypothesis,
a_427 = a_437 ).
cnf(u266,hypothesis,
a_439 = store(a_437,i1,e_424) ).
cnf(u158,hypothesis,
e_417 = select(a_432,i1) ).
cnf(hyp1,hypothesis,
a_419 = store(a_418,i1,e_417) ).
cnf(u49,hypothesis,
( select(a_419,X0) = select(a_432,X0)
| i3 = X0 ) ).
cnf(hyp11,hypothesis,
a_437 = store(a_435,i2,e_436) ).
cnf(u59,hypothesis,
a_427 = store(a_425,i2,e_422) ).
cnf(u350,hypothesis,
e_424 = select(a_429,i2) ).
cnf(hyp13,hypothesis,
a_441 = store(a_439,i3,e_440) ).
cnf(u105,hypothesis,
e_438 = select(a_439,i1) ).
cnf(u149,hypothesis,
e_438 = select(a_437,i1) ).
cnf(u335,hypothesis,
( select(a_423,X0) = select(a_425,X0)
| i1 = X0 ) ).
cnf(u473,hypothesis,
a_439 = store(a_427,i1,e_424) ).
cnf(u159,hypothesis,
e_420 = e_436 ).
cnf(hyp2,hypothesis,
a_421 = store(a_419,i0,e_420) ).
cnf(u54,hypothesis,
( select(a_425,X0) = select(a_427,X0)
| i2 = X0 ) ).
cnf(hyp12,hypothesis,
a_439 = store(a_437,i0,e_438) ).
cnf(u56,hypothesis,
( select(a_437,X0) = select(a_435,X0)
| i2 = X0 ) ).
cnf(hyp14,hypothesis,
e_417 = select(a1,i1) ).
cnf(u330,hypothesis,
e_417 = select(a_431,i1) ).
cnf(u348,hypothesis,
e_417 = select(a_437,i2) ).
cnf(u358,hypothesis,
e_424 = select(a_441,i1) ).
cnf(u43,hypothesis,
( select(a1,X0) = select(a_418,X0)
| i1 = X0 ) ).
cnf(u157,hypothesis,
e_417 = select(a_423,i1) ).
cnf(u52,hypothesis,
( select(a_433,X0) = select(a_435,X0)
| i3 = X0 ) ).
cnf(hyp10,hypothesis,
a_435 = store(a_433,i3,e_434) ).
cnf(u62,hypothesis,
e_422 = e_430 ).
cnf(hyp20,hypothesis,
e_430 = select(a_427,i2) ).
cnf(hyp22,hypothesis,
e_436 = select(a_433,i3) ).
cnf(u35,hypothesis,
e_422 = select(a_432,i3) ).
cnf(u53,hypothesis,
( select(a_439,X0) = select(a_441,X0)
| i3 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u368,hypothesis,
e_417 = select(a_427,i2) ).
cnf(u112,hypothesis,
a_423 = store(a_421,i3,e_417) ).
cnf(u341,hypothesis,
( select(a_439,X0) = select(a_441,X0)
| i1 = X0 ) ).
cnf(hyp24,hypothesis,
e_440 = select(a_437,i0) ).
cnf(u46,hypothesis,
( select(a_429,X0) = select(a_431,X0)
| i0 = X0 ) ).
cnf(u162,hypothesis,
a_432 = store(a_419,i1,e_417) ).
cnf(u142,hypothesis,
a_425 = store(a_423,i1,e_424) ).
cnf(u33,hypothesis,
e_420 = select(a_433,i0) ).
cnf(u324,hypothesis,
( select(a_432,X0) = select(a_433,X0)
| i1 = X0 ) ).
cnf(u154,hypothesis,
e_440 = select(a_441,i1) ).
cnf(hyp7,hypothesis,
a_431 = store(a_429,i0,e_430) ).
cnf(goal,negated_conjecture,
a_431 != a_441 ).
cnf(u321,hypothesis,
( select(a_419,X0) = select(a_421,X0)
| i1 = X0 ) ).
cnf(u38,hypothesis,
e_434 = select(a_435,i3) ).
cnf(u66,hypothesis,
e_422 = select(a_427,i2) ).
cnf(u40,hypothesis,
e_426 = select(a_427,i2) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u50,hypothesis,
( select(a_421,X0) = select(a_423,X0)
| i3 = X0 ) ).
cnf(u387,hypothesis,
a_421 = a_432 ).
cnf(u161,hypothesis,
e_417 = e_420 ).
cnf(u190,hypothesis,
a_421 = store(a_419,i1,e_417) ).
cnf(u107,hypothesis,
e_417 = e_422 ).
cnf(u36,hypothesis,
e_422 = select(a_423,i3) ).
cnf(u64,hypothesis,
a_431 = store(a_429,i0,e_422) ).
cnf(u153,hypothesis,
e_434 = select(a_435,i1) ).
cnf(hyp4,hypothesis,
a_425 = store(a_423,i3,e_424) ).
cnf(u48,hypothesis,
( select(a_437,X0) = select(a_439,X0)
| i0 = X0 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV534-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.09/0.18 % Computer : n009.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 11:35:15 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 3.85/1.32 % (2979709)Input is clausal, will run a generic CNF schedule.
% 3.85/1.32 % (2979795)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3457201335:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.85/1.32 % (2979795)Refutation not found, incomplete strategy
% 3.85/1.32 % (2979795)------------------------------
% 3.85/1.32 % (2979795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.32 % (2979795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.32 % (2979795)CaDiCaL version: 2.1.3
% 3.85/1.32 % (2979795)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.32 % (2979795)Time elapsed: 0.008 s
% 3.85/1.32 % (2979795)Peak memory usage: 88 MB
% 3.85/1.32 % (2979795)Instructions burned: 22 (million)
% 3.85/1.32 % (2979787)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=1595897133:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.85/1.32 % (2979788)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4165418344:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.85/1.32 % (2979791)lrs+10_1_sil=8000:sp=occurrence:random_seed=1279088527:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.85/1.32 % (2979793)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3949796987:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.85/1.32 % (2979791)First to succeed.
% 3.85/1.32 % (2979790)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4175964054:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.85/1.32 % (2979796)dis-21_1_sil=8000:lcm=predicate:random_seed=1794521021: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)
% 3.85/1.32 % (2979791)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2979709"
% 3.85/1.32 % (2979796)Refutation not found, incomplete strategy
% 3.85/1.32 % (2979796)------------------------------
% 3.85/1.32 % (2979796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.32 % (2979796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.32 % (2979796)CaDiCaL version: 2.1.3
% 3.85/1.32 % (2979796)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.32 % (2979796)Time elapsed: 0.001 s
% 3.85/1.32 % (2979796)Peak memory usage: 88 MB
% 3.85/1.32 % (2979796)Instructions burned: 1 (million)
% 3.85/1.32 % (2979793)Instruction limit reached!
% 3.85/1.32 % (2979793)------------------------------
% 3.85/1.32 % (2979793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.32 % (2979793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.32 % (2979793)CaDiCaL version: 2.1.3
% 3.85/1.32 % (2979793)Termination reason: Instruction limit
% 3.85/1.32 % (2979793)Termination phase: Saturation
% 3.85/1.32 % (2979793)Time elapsed: 0.066 s
% 3.85/1.32 % (2979793)Peak memory usage: 88 MB
% 3.85/1.32 % (2979793)Instructions burned: 115 (million)
% 3.85/1.32 % (2979795)------------------------------
% 3.85/1.32 % (2979795)------------------------------
% 3.85/1.32 % (2979847)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=3005673731:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.85/1.32 % (2979866)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4150632221:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 3.85/1.32 % (2979847)Refutation not found, incomplete strategy
% 3.85/1.32 % (2979847)------------------------------
% 3.85/1.32 % (2979847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.32 % (2979847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.32 % (2979847)CaDiCaL version: 2.1.3
% 3.85/1.32 % (2979847)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.32 % (2979847)Time elapsed: 0.015 s
% 3.85/1.32 % (2979847)Peak memory usage: 88 MB
% 3.85/1.32 % (2979847)Instructions burned: 22 (million)
% 3.85/1.32 % (2979796)------------------------------
% 3.85/1.32 % (2979796)------------------------------
% 3.85/1.32 % SZS status Satisfiable for theBenchmark
% 3.85/1.32 % SZS output start Saturation.
% See solution above
% 3.85/1.33 % SZS output start Definitions and Model Updates.
% 3.85/1.33 % SZS output end Definitions and Model Updates.
% 3.85/1.33 % (2979791)------------------------------
% 3.85/1.33 % (2979791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.33 % (2979791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.33 % (2979791)CaDiCaL version: 2.1.3
% 3.85/1.33 % (2979791)Termination reason: Satisfiable
% 3.85/1.33 % (2979791)Time elapsed: 0.013 s
% 3.85/1.33 % (2979791)Peak memory usage: 88 MB
% 3.85/1.33 % (2979791)Instructions burned: 19 (million)
% 3.85/1.33 % (2979791)------------------------------
% 3.85/1.33 % (2979791)------------------------------
% 3.85/1.33 % (2979709)Success in time 0.461 s
% 3.85/1.33 % Vampire exiting
%------------------------------------------------------------------------------