%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV556-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 : n005.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:18:32 PM UTC 2026
% Result : Satisfiable 3.77s 1.26s
% Output : Saturation 3.77s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u46,hypothesis,
i1 = i_35 ).
cnf(u49,hypothesis,
e_36 != select(a_20,i_35) ).
cnf(u57,hypothesis,
e_37 != select(a_22,i_35) ).
cnf(u71,hypothesis,
i2 != i3 ).
cnf(u76,hypothesis,
e_29 = select(a_20,i3) ).
cnf(u98,hypothesis,
e_33 = select(a_24,i4) ).
cnf(u101,hypothesis,
i2 != i4 ).
cnf(u110,hypothesis,
i3 = i4 ).
cnf(u118,hypothesis,
e_31 = select(a_26,i4) ).
cnf(u132,hypothesis,
e_31 = select(a_30,i1) ).
cnf(u135,hypothesis,
i1 != i3 ).
cnf(u161,hypothesis,
e_33 = select(a_20,i4) ).
cnf(u245,hypothesis,
e_23 != select(a_26,i1) ).
cnf(u250,hypothesis,
i1 = i2 ).
cnf(u313,hypothesis,
e_21 = e_23 ).
cnf(u749,hypothesis,
e_27 = select(a_22,i3) ).
cnf(u760,hypothesis,
e_21 != e_27 ).
cnf(u564,hypothesis,
e_21 = select(a_24,i1) ).
cnf(hyp16,hypothesis,
e_36 = select(a1,i_35) ).
cnf(u169,hypothesis,
e_27 = e_33 ).
cnf(u362,hypothesis,
a_26 = store(a_22,i1,e_19) ).
cnf(u807,hypothesis,
( select(a_22,X0) = select(a_24,X0)
| i1 = X0
| i3 = X0 ) ).
cnf(u604,hypothesis,
( select(a_22,X0) = select(a_26,X0)
| i1 = X0 ) ).
cnf(u1019,hypothesis,
e_19 = select(a_34,i1) ).
cnf(u189,hypothesis,
e_27 = e_29 ).
cnf(u27,hypothesis,
e_31 = select(a_34,i1) ).
cnf(hyp9,hypothesis,
e_21 = select(a1,i1) ).
cnf(u168,hypothesis,
e_29 = e_31 ).
cnf(u479,hypothesis,
e_27 = select(a_34,i1) ).
cnf(u1038,hypothesis,
e_19 = e_33 ).
cnf(u24,hypothesis,
store(a_28,i1,e_31) = a_34 ).
cnf(u34,hypothesis,
( select(a2,X0) = select(a_22,X0)
| i1 = X0 ) ).
cnf(u966,hypothesis,
a_34 = store(a_30,i3,e_19) ).
cnf(u460,hypothesis,
e_27 = select(a_34,i3) ).
cnf(u190,hypothesis,
a_34 = store(a_28,i1,e_27) ).
cnf(hyp18,hypothesis,
i_35 = sk(a1,a2) ).
cnf(u605,hypothesis,
e_19 = select(a_26,i1) ).
cnf(hyp17,hypothesis,
e_37 = select(a2,i_35) ).
cnf(u30,hypothesis,
e_27 = select(a_28,i3) ).
cnf(u32,hypothesis,
e_33 = select(a_34,i4) ).
cnf(u165,hypothesis,
a_34 = store(a_30,i3,e_33) ).
cnf(hyp0,hypothesis,
a_20 = store(a1,i1,e_19) ).
cnf(u31,hypothesis,
e_29 = select(a_30,i3) ).
cnf(u320,hypothesis,
e_23 = select(a_24,i1) ).
cnf(u791,hypothesis,
( select(a_28,X0) = select(a_30,X0)
| i1 = X0
| i3 = X0 ) ).
cnf(hyp8,hypothesis,
e_19 = select(a2,i1) ).
cnf(u29,hypothesis,
e_25 = select(a_26,i2) ).
cnf(u185,hypothesis,
e_27 = e_31 ).
cnf(u39,hypothesis,
( select(a_26,X0) = select(a_30,X0)
| i3 = X0 ) ).
cnf(hyp3,hypothesis,
a_26 = store(a_22,i2,e_25) ).
cnf(u968,hypothesis,
a_30 = store(a_26,i3,e_19) ).
cnf(hyp5,hypothesis,
a_30 = store(a_26,i3,e_29) ).
cnf(u1016,hypothesis,
e_19 = e_31 ).
cnf(hyp15,hypothesis,
e_33 = select(a_28,i4) ).
cnf(u329,hypothesis,
e_19 = e_25 ).
cnf(u962,hypothesis,
e_19 = select(a_30,i3) ).
cnf(u338,hypothesis,
( select(a_34,X0) = select(a_30,X0)
| i3 = X0 ) ).
cnf(u965,hypothesis,
a_28 = store(a_24,i3,e_19) ).
cnf(hyp1,hypothesis,
a_22 = store(a2,i1,e_21) ).
cnf(u967,hypothesis,
a_34 = store(a_28,i1,e_19) ).
cnf(hyp11,hypothesis,
e_25 = select(a_20,i2) ).
cnf(u170,hypothesis,
a_34 = store(a_28,i1,e_29) ).
cnf(hyp13,hypothesis,
e_29 = select(a_24,i3) ).
cnf(u509,hypothesis,
( select(a_20,X0) = select(a_24,X0)
| i1 = X0 ) ).
cnf(u26,hypothesis,
e_21 = select(a_22,i1) ).
cnf(u38,hypothesis,
( select(a_28,X0) = select(a_24,X0)
| i3 = X0 ) ).
cnf(u344,hypothesis,
a_24 = store(a_20,i1,e_21) ).
cnf(hyp2,hypothesis,
a_24 = store(a_20,i2,e_23) ).
cnf(hyp12,hypothesis,
e_27 = select(a_26,i3) ).
cnf(hyp14,hypothesis,
e_31 = select(a_30,i4) ).
cnf(u954,hypothesis,
e_19 = e_27 ).
cnf(u775,hypothesis,
( select(a_24,X0) = select(a_26,X0)
| i3 = X0
| i1 = X0 ) ).
cnf(u875,hypothesis,
( select(a_20,X0) = select(a_22,X0)
| i1 = X0
| i3 = X0 ) ).
cnf(u1013,hypothesis,
e_19 = select(a_34,i3) ).
cnf(u123,hypothesis,
( select(a_28,X0) = select(a_30,X0)
| i1 = X0
| i4 = X0 ) ).
cnf(hyp10,hypothesis,
e_23 = select(a_22,i2) ).
cnf(goal,negated_conjecture,
e_36 != e_37 ).
cnf(u179,hypothesis,
a_34 = store(a_30,i3,e_27) ).
cnf(u25,hypothesis,
e_19 = select(a_20,i1) ).
cnf(u1023,hypothesis,
e_19 = e_29 ).
cnf(u35,hypothesis,
( select(a_28,X0) = select(a_34,X0)
| i1 = X0 ) ).
cnf(u164,hypothesis,
e_33 = select(a_34,i3) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u63,hypothesis,
e_21 = e_36 ).
cnf(u33,hypothesis,
( select(a1,X0) = select(a_20,X0)
| i1 = X0 ) ).
cnf(hyp7,hypothesis,
a_34 = store(a_30,i4,e_33) ).
cnf(u261,hypothesis,
( select(a_28,X0) = select(a_26,X0)
| i3 = X0
| i1 = X0 ) ).
cnf(u28,hypothesis,
e_23 = select(a_24,i2) ).
cnf(u960,hypothesis,
e_19 = select(a_30,i1) ).
cnf(u37,hypothesis,
( select(a_22,X0) = select(a_26,X0)
| i2 = X0 ) ).
cnf(u40,hypothesis,
( select(a_34,X0) = select(a_30,X0)
| i4 = X0 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u288,hypothesis,
a_30 = store(a_26,i3,e_27) ).
cnf(u316,hypothesis,
a_24 = store(a_20,i1,e_23) ).
cnf(u953,hypothesis,
e_19 != e_21 ).
cnf(hyp4,hypothesis,
a_28 = store(a_24,i3,e_27) ).
cnf(u36,hypothesis,
( select(a_20,X0) = select(a_24,X0)
| i2 = X0 ) ).
cnf(u64,hypothesis,
e_19 = e_37 ).
cnf(u1009,hypothesis,
e_19 = select(a_28,i3) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV556-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n005.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 11:45:31 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 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.77/1.26 % (735449)Input is clausal, will run a generic CNF schedule.
% 3.77/1.26 % (735557)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3871302811:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.77/1.26 % (735552)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4172841013:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.77/1.26 % (735554)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2475694886:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.77/1.26 % (735550)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=1427489143:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.77/1.26 % (735556)lrs+10_1_sil=8000:sp=occurrence:random_seed=2374719024:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.77/1.26 % (735557)Instruction limit reached!
% 3.77/1.26 % (735557)------------------------------
% 3.77/1.26 % (735557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.26 % (735557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.26 % (735557)CaDiCaL version: 2.1.3
% 3.77/1.26 % (735557)Termination reason: Instruction limit
% 3.77/1.26 % (735557)Termination phase: Saturation
% 3.77/1.26 % (735557)Time elapsed: 0.036 s
% 3.77/1.26 % (735557)Peak memory usage: 89 MB
% 3.77/1.26 % (735557)Instructions burned: 117 (million)
% 3.77/1.26 % (735559)dis-21_1_sil=8000:lcm=predicate:random_seed=2343779915: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.77/1.26 % (735559)Refutation not found, incomplete strategy
% 3.77/1.26 % (735559)------------------------------
% 3.77/1.26 % (735559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.26 % (735559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.26 % (735559)CaDiCaL version: 2.1.3
% 3.77/1.26 % (735559)Termination reason: Refutation not found, incomplete strategy
% 3.77/1.26 % (735559)Time elapsed: 0.002 s
% 3.77/1.26 % (735559)Peak memory usage: 88 MB
% 3.77/1.26 % (735559)Instructions burned: 1 (million)
% 3.77/1.26 % (735556)First to succeed.
% 3.77/1.26 % (735556)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-735449"
% 3.77/1.26 % (735558)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2093125256:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.77/1.26 % (735558)Refutation not found, incomplete strategy
% 3.77/1.26 % (735558)------------------------------
% 3.77/1.26 % (735558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.26 % (735558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.26 % (735558)CaDiCaL version: 2.1.3
% 3.77/1.26 % (735558)Termination reason: Refutation not found, incomplete strategy
% 3.77/1.26 % (735558)Time elapsed: 0.015 s
% 3.77/1.26 % (735558)Peak memory usage: 88 MB
% 3.77/1.26 % (735558)Instructions burned: 22 (million)
% 3.77/1.26 % (735595)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=1027841942:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.77/1.26 % (735595)Refutation not found, incomplete strategy
% 3.77/1.26 % (735595)------------------------------
% 3.77/1.26 % (735595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.26 % (735595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.26 % (735595)CaDiCaL version: 2.1.3
% 3.77/1.26 % (735595)Termination reason: Refutation not found, incomplete strategy
% 3.77/1.26 % (735595)Time elapsed: 0.029 s
% 3.77/1.26 % (735595)Peak memory usage: 89 MB
% 3.77/1.26 % (735595)Instructions burned: 90 (million)
% 3.77/1.26 % (735559)------------------------------
% 3.77/1.26 % (735559)------------------------------
% 3.77/1.26 % SZS status Satisfiable for theBenchmark
% 3.77/1.26 % SZS output start Saturation.
% See solution above
% 3.77/1.26 % SZS output start Definitions and Model Updates.
% 3.77/1.26 for all inputs,
% 3.77/1.26 define a_32 := a_34
% 3.77/1.26 % SZS output end Definitions and Model Updates.
% 3.77/1.26 % (735556)------------------------------
% 3.77/1.26 % (735556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.77/1.26 % (735556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.77/1.26 % (735556)CaDiCaL version: 2.1.3
% 3.77/1.26 % (735556)Termination reason: Satisfiable
% 3.77/1.26 % (735556)Time elapsed: 0.028 s
% 3.77/1.26 % (735556)Peak memory usage: 89 MB
% 3.77/1.26 % (735556)Instructions burned: 33 (million)
% 3.77/1.26 % (735556)------------------------------
% 3.77/1.26 % (735556)------------------------------
% 3.77/1.26 % (735449)Success in time 0.47 s
% 3.77/1.26 % Vampire exiting
%------------------------------------------------------------------------------