%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV556-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 THM
% Computer : n017.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 2.99s 1.12s
% Output : Saturation 3.87s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u69,hypothesis,
i1 != i_59 ).
cnf(u74,hypothesis,
e_60 = select(a_32,i_59) ).
cnf(u82,hypothesis,
e_61 = select(a_34,i_59) ).
cnf(u95,hypothesis,
i2 != i3 ).
cnf(u100,hypothesis,
e_41 = select(a_32,i3) ).
cnf(u122,hypothesis,
e_45 = select(a_36,i4) ).
cnf(u125,hypothesis,
i2 != i4 ).
cnf(u134,hypothesis,
i3 = i4 ).
cnf(u142,hypothesis,
e_43 = select(a_38,i4) ).
cnf(u152,hypothesis,
e_49 = select(a_40,i5) ).
cnf(u155,hypothesis,
i3 != i5 ).
cnf(u161,hypothesis,
i4 != i5 ).
cnf(u170,hypothesis,
e_47 = select(a_42,i5) ).
cnf(u188,hypothesis,
e_53 = select(a_44,i6) ).
cnf(u191,hypothesis,
i4 != i6 ).
cnf(u198,hypothesis,
i5 = i6 ).
cnf(u206,hypothesis,
e_51 = select(a_46,i6) ).
cnf(u224,hypothesis,
e_57 = select(a_48,i7) ).
cnf(u233,hypothesis,
i6 != i7 ).
cnf(u242,hypothesis,
e_55 = select(a_50,i7) ).
cnf(u267,hypothesis,
i1 != i6 ).
cnf(u273,hypothesis,
i1 != i7 ).
cnf(u278,hypothesis,
e_55 = select(a_54,i1) ).
cnf(u307,hypothesis,
e_45 = select(a_32,i4) ).
cnf(u332,hypothesis,
e_49 = select(a_36,i5) ).
cnf(u357,hypothesis,
e_53 = select(a_40,i6) ).
cnf(u361,hypothesis,
i2 = i6 ).
cnf(u374,hypothesis,
i3 != i6 ).
cnf(u554,hypothesis,
i2 = i5 ).
cnf(u624,hypothesis,
e_55 = select(a_40,i1) ).
cnf(u628,hypothesis,
i1 = i3 ).
cnf(u640,hypothesis,
e_55 = select(a_42,i1) ).
cnf(u648,hypothesis,
e_55 = select(a_36,i1) ).
cnf(u660,hypothesis,
e_55 = select(a_38,i1) ).
cnf(u1725,hypothesis,
i2 != i7 ).
cnf(u1730,hypothesis,
e_57 = select(a_44,i7) ).
cnf(u1755,hypothesis,
e_31 = select(a_46,i7) ).
cnf(u1899,hypothesis,
e_31 = select(a_34,i7) ).
cnf(u2643,negated_conjecture,
i7 = i_59 ).
cnf(u2646,negated_conjecture,
i2 != i_59 ).
cnf(u404,hypothesis,
e_39 = e_45 ).
cnf(hyp0,hypothesis,
a_32 = store(a1,i1,e_31) ).
cnf(u448,hypothesis,
a_46 = store(a_42,i3,e_39) ).
cnf(u498,hypothesis,
e_47 = e_51 ).
cnf(u1070,hypothesis,
e_31 = e_41 ).
cnf(u2431,hypothesis,
a_48 = store(a_44,i2,e_35) ).
cnf(u37,hypothesis,
e_31 = select(a_32,i1) ).
cnf(u49,hypothesis,
e_53 = select(a_54,i6) ).
cnf(u1793,hypothesis,
( select(a_48,X0) = select(a_50,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(u2666,negated_conjecture,
e_60 = select(a1,i7) ).
cnf(u40,hypothesis,
e_35 = select(a_36,i2) ).
cnf(u1272,hypothesis,
( select(a_42,X0) = select(a_46,X0)
| i1 = X0 ) ).
cnf(u63,hypothesis,
( select(a_50,X0) = select(a_54,X0)
| i6 = X0 ) ).
cnf(u216,hypothesis,
e_49 = e_51 ).
cnf(u696,hypothesis,
a_52 = store(a_48,i2,e_35) ).
cnf(hyp4,hypothesis,
a_40 = store(a_36,i3,e_39) ).
cnf(u415,hypothesis,
e_47 = select(a_54,i5) ).
cnf(u1071,hypothesis,
e_31 = e_39 ).
cnf(hyp7,hypothesis,
a_46 = store(a_42,i4,e_45) ).
cnf(u754,hypothesis,
e_31 = e_55 ).
cnf(u2320,hypothesis,
e_35 = select(a_40,i2) ).
cnf(hyp22,hypothesis,
e_47 = select(a_46,i5) ).
cnf(u1050,hypothesis,
e_39 = select(a_38,i1) ).
cnf(u44,hypothesis,
e_43 = select(a_44,i4) ).
cnf(u1051,hypothesis,
e_41 = select(a_36,i1) ).
cnf(u51,hypothesis,
( select(a1,X0) = select(a_32,X0)
| i1 = X0 ) ).
cnf(u2473,hypothesis,
a_38 = store(a_34,i2,e_35) ).
cnf(u1328,hypothesis,
e_31 = select(a_40,i1) ).
cnf(u695,hypothesis,
( select(a_52,X0) = select(a_48,X0)
| i2 = X0 ) ).
cnf(hyp11,hypothesis,
a_54 = store(a_50,i6,e_53) ).
cnf(u730,hypothesis,
e_41 = select(a_44,i3) ).
cnf(u2432,hypothesis,
a_54 = store(a_50,i2,e_35) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(hyp26,hypothesis,
e_55 = select(a_54,i7) ).
cnf(u2586,hypothesis,
( select(a_38,X0) = select(a_40,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(u1048,hypothesis,
a_40 = store(a_36,i1,e_39) ).
cnf(u1890,hypothesis,
e_57 = select(a_36,i7) ).
cnf(hyp29,hypothesis,
e_61 = select(a2,i_59) ).
cnf(u1226,hypothesis,
e_31 = select(a_44,i1) ).
cnf(u1873,hypothesis,
( select(a_44,X0) = select(a_46,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(u55,hypothesis,
( select(a_34,X0) = select(a_38,X0)
| i2 = X0 ) ).
cnf(u567,hypothesis,
e_47 = select(a_48,i2) ).
cnf(u1174,hypothesis,
e_31 = e_43 ).
cnf(u778,hypothesis,
e_31 = e_33 ).
cnf(u58,hypothesis,
( select(a_40,X0) = select(a_44,X0)
| i4 = X0 ) ).
cnf(u2668,negated_conjecture,
e_31 = e_61 ).
cnf(u808,hypothesis,
( select(a_52,X0) = select(a_50,X0)
| i1 = X0
| i7 = X0
| i2 = X0 ) ).
cnf(u398,hypothesis,
e_43 = select(a_44,i3) ).
cnf(hyp2,hypothesis,
a_36 = store(a_32,i2,e_35) ).
cnf(u2670,negated_conjecture,
e_31 != e_57 ).
cnf(u1428,hypothesis,
e_31 = select(a_58,i1) ).
cnf(u1961,hypothesis,
e_35 = e_53 ).
cnf(hyp5,hypothesis,
a_42 = store(a_38,i3,e_41) ).
cnf(u36,hypothesis,
store(a_52,i1,e_55) = a_58 ).
cnf(u1826,hypothesis,
e_57 = select(a_40,i7) ).
cnf(u416,hypothesis,
e_49 = select(a_52,i5) ).
cnf(u598,hypothesis,
e_37 = select(a_54,i2) ).
cnf(hyp28,hypothesis,
e_60 = select(a1,i_59) ).
cnf(u43,hypothesis,
e_41 = select(a_42,i3) ).
cnf(u664,hypothesis,
( select(a_40,X0) = select(a_44,X0)
| i3 = X0 ) ).
cnf(u724,hypothesis,
e_39 = select(a_46,i3) ).
cnf(u980,hypothesis,
e_35 = select(a_48,i2) ).
cnf(u1061,hypothesis,
a_46 = store(a_42,i1,e_39) ).
cnf(u62,hypothesis,
( select(a_52,X0) = select(a_48,X0)
| i6 = X0 ) ).
cnf(u678,hypothesis,
( select(a_50,X0) = select(a_54,X0)
| i2 = X0 ) ).
cnf(u1053,hypothesis,
e_41 = select(a_42,i1) ).
cnf(u2318,hypothesis,
e_35 = e_47 ).
cnf(u458,hypothesis,
a_44 = store(a_40,i3,e_41) ).
cnf(u1287,hypothesis,
( select(a_40,X0) = select(a_44,X0)
| i1 = X0 ) ).
cnf(u253,hypothesis,
( select(a_52,X0) = select(a_54,X0)
| i1 = X0
| i7 = X0 ) ).
cnf(hyp9,hypothesis,
a_50 = store(a_46,i5,e_49) ).
cnf(u420,hypothesis,
a_52 = store(a_48,i5,e_49) ).
cnf(hyp16,hypothesis,
e_35 = select(a_34,i2) ).
cnf(u60,hypothesis,
( select(a_44,X0) = select(a_48,X0)
| i5 = X0 ) ).
cnf(u38,hypothesis,
e_33 = select(a_34,i1) ).
cnf(u1143,hypothesis,
e_33 = e_55 ).
cnf(u565,hypothesis,
e_47 = select(a_46,i2) ).
cnf(u53,hypothesis,
( select(a_52,X0) = select(a_58,X0)
| i1 = X0 ) ).
cnf(u669,hypothesis,
( select(a_42,X0) = select(a_46,X0)
| i3 = X0 ) ).
cnf(u1062,hypothesis,
a_44 = store(a_40,i1,e_41) ).
cnf(u2628,hypothesis,
( select(a_32,X0) = select(a_34,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(u56,hypothesis,
( select(a_36,X0) = select(a_40,X0)
| i3 = X0 ) ).
cnf(u1244,hypothesis,
a_40 = store(a_36,i1,e_31) ).
cnf(hyp20,hypothesis,
e_43 = select(a_42,i4) ).
cnf(u1063,hypothesis,
e_39 = select(a_46,i1) ).
cnf(u1863,hypothesis,
e_31 = select(a_54,i1) ).
cnf(u874,hypothesis,
( select(a_44,X0) = select(a_48,X0)
| i2 = X0 ) ).
cnf(hyp23,hypothesis,
e_49 = select(a_44,i5) ).
cnf(u2667,negated_conjecture,
e_57 = e_60 ).
cnf(u41,hypothesis,
e_37 = select(a_38,i2) ).
cnf(u2620,hypothesis,
( select(a_34,X0) = select(a_36,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(hyp8,hypothesis,
a_48 = store(a_44,i5,e_47) ).
cnf(hyp1,hypothesis,
a_34 = store(a2,i1,e_33) ).
cnf(u2573,hypothesis,
( select(a_40,X0) = select(a_42,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(u688,hypothesis,
e_37 = e_47 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(hyp27,hypothesis,
e_57 = select(a_52,i7) ).
cnf(hyp14,hypothesis,
e_31 = select(a2,i1) ).
cnf(u45,hypothesis,
e_45 = select(a_46,i4) ).
cnf(u48,hypothesis,
e_51 = select(a_52,i6) ).
cnf(u47,hypothesis,
e_49 = select(a_50,i5) ).
cnf(u1748,hypothesis,
e_31 = select(a_50,i1) ).
cnf(u1086,hypothesis,
a_46 = store(a_42,i1,e_33) ).
cnf(u574,hypothesis,
i1 != i2 ).
cnf(u395,hypothesis,
a_46 = store(a_42,i3,e_45) ).
cnf(u1262,hypothesis,
( select(a_38,X0) = select(a_42,X0)
| i1 = X0 ) ).
cnf(hyp3,hypothesis,
a_38 = store(a_34,i2,e_37) ).
cnf(u996,hypothesis,
e_35 = select(a_54,i2) ).
cnf(u926,hypothesis,
e_35 = select(a_50,i2) ).
cnf(u1049,hypothesis,
a_42 = store(a_38,i1,e_41) ).
cnf(u1485,hypothesis,
e_35 = select(a_38,i2) ).
cnf(u414,hypothesis,
i1 != i5 ).
cnf(u2391,hypothesis,
e_57 = select(a_32,i7) ).
cnf(hyp18,hypothesis,
e_39 = select(a_38,i3) ).
cnf(hyp30,hypothesis,
i_59 = sk(a1,a2) ).
cnf(u1962,hypothesis,
e_35 = e_51 ).
cnf(hyp21,hypothesis,
e_45 = select(a_40,i4) ).
cnf(u52,hypothesis,
( select(a2,X0) = select(a_34,X0)
| i1 = X0 ) ).
cnf(u1064,hypothesis,
e_41 = select(a_44,i1) ).
cnf(u59,hypothesis,
( select(a_42,X0) = select(a_46,X0)
| i4 = X0 ) ).
cnf(u1837,hypothesis,
e_31 = select(a_38,i7) ).
cnf(u399,hypothesis,
e_45 = select(a_46,i3) ).
cnf(u50,hypothesis,
e_57 = select(a_58,i7) ).
cnf(u1448,hypothesis,
e_31 = select(a_34,i1) ).
cnf(hyp6,hypothesis,
a_44 = store(a_40,i4,e_43) ).
cnf(u405,hypothesis,
e_41 = e_43 ).
cnf(u1808,hypothesis,
( select(a_46,X0) = select(a_48,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(hyp25,hypothesis,
e_53 = select(a_48,i6) ).
cnf(u925,hypothesis,
( select(a_46,X0) = select(a_50,X0)
| i2 = X0 ) ).
cnf(u1584,hypothesis,
e_47 = select(a_42,i2) ).
cnf(u1069,hypothesis,
e_33 = e_39 ).
cnf(goal,negated_conjecture,
e_60 != e_61 ).
cnf(u2608,hypothesis,
( select(a_36,X0) = select(a_38,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(u54,hypothesis,
( select(a_32,X0) = select(a_36,X0)
| i2 = X0 ) ).
cnf(u576,hypothesis,
e_35 = e_49 ).
cnf(u1656,hypothesis,
e_35 = select(a_42,i2) ).
cnf(u2322,hypothesis,
e_35 = select(a_44,i2) ).
cnf(hyp10,hypothesis,
a_52 = store(a_48,i6,e_51) ).
cnf(u1338,hypothesis,
e_31 = select(a_46,i1) ).
cnf(u1260,hypothesis,
a_34 = store(a2,i1,e_31) ).
cnf(hyp13,hypothesis,
a_58 = store(a_54,i7,e_57) ).
cnf(u2074,hypothesis,
( select(a_42,X0) = select(a_44,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(u2665,negated_conjecture,
e_61 = select(a2,i7) ).
cnf(u39,hypothesis,
e_55 = select(a_58,i1) ).
cnf(u419,hypothesis,
a_54 = store(a_50,i5,e_47) ).
cnf(u563,hypothesis,
a_48 = store(a_44,i2,e_47) ).
cnf(u42,hypothesis,
e_39 = select(a_40,i3) ).
cnf(u215,hypothesis,
e_47 = e_53 ).
cnf(u950,hypothesis,
e_35 = select(a_52,i2) ).
cnf(u129,hypothesis,
e_39 = select(a_34,i3) ).
cnf(u57,hypothesis,
( select(a_38,X0) = select(a_42,X0)
| i3 = X0 ) ).
cnf(u1245,hypothesis,
a_46 = store(a_42,i1,e_31) ).
cnf(u394,hypothesis,
a_44 = store(a_40,i3,e_43) ).
cnf(u1308,hypothesis,
e_31 = select(a_42,i1) ).
cnf(u1052,hypothesis,
e_39 = select(a_40,i1) ).
cnf(hyp15,hypothesis,
e_33 = select(a1,i1) ).
cnf(hyp17,hypothesis,
e_37 = select(a_32,i2) ).
cnf(u1769,hypothesis,
e_31 = select(a_42,i7) ).
cnf(u64,hypothesis,
( select(a_58,X0) = select(a_54,X0)
| i7 = X0 ) ).
cnf(u673,hypothesis,
a_54 = store(a_50,i2,e_47) ).
cnf(u604,hypothesis,
a_50 = store(a_46,i2,e_35) ).
cnf(hyp24,hypothesis,
e_51 = select(a_50,i6) ).
cnf(u591,hypothesis,
e_47 = select(a_54,i2) ).
cnf(u611,hypothesis,
e_35 = e_37 ).
cnf(u46,hypothesis,
e_47 = select(a_48,i5) ).
cnf(u881,hypothesis,
e_37 = select(a_48,i2) ).
cnf(u1078,hypothesis,
a_44 = store(a_40,i1,e_31) ).
cnf(u61,hypothesis,
( select(a_46,X0) = select(a_50,X0)
| i5 = X0 ) ).
cnf(u1255,hypothesis,
a_58 = store(a_52,i1,e_31) ).
cnf(hyp19,hypothesis,
e_41 = select(a_36,i3) ).
cnf(u1258,hypothesis,
( select(a_36,X0) = select(a_40,X0)
| i1 = X0 ) ).
cnf(u1085,hypothesis,
a_40 = store(a_36,i1,e_33) ).
cnf(u1075,hypothesis,
a_42 = store(a_38,i1,e_31) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV556-1.007 : 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.19 % Computer : n017.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:41:06 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 2.99/1.12 % (3493857)Input is clausal, will run a generic CNF schedule.
% 2.99/1.12 % (3493864)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2467772499:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.99/1.12 % (3493866)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=304138358:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.99/1.12 % (3493862)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=2403004404:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.99/1.12 % (3493865)lrs+10_1_sil=8000:sp=occurrence:random_seed=1150726349:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.99/1.12 % (3493863)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=482051090:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.99/1.12 % (3493867)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2084605687:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.99/1.12 % (3493868)dis-21_1_sil=8000:lcm=predicate:random_seed=3720858575: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)
% 2.99/1.12 % (3493868)Refutation not found, incomplete strategy
% 2.99/1.12 % (3493868)------------------------------
% 2.99/1.12 % (3493868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.12 % (3493868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.12 % (3493868)CaDiCaL version: 2.1.3
% 2.99/1.12 % (3493868)Termination reason: Refutation not found, incomplete strategy
% 2.99/1.12 % (3493868)Time elapsed: 0.001 s
% 2.99/1.12 % (3493868)Peak memory usage: 88 MB
% 2.99/1.12 % (3493868)Instructions burned: 1 (million)
% 2.99/1.12 % (3493865)First to succeed.
% 2.99/1.12 % (3493865)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3493857"
% 2.99/1.12 % (3493866)Instruction limit reached!
% 2.99/1.12 % (3493866)------------------------------
% 2.99/1.12 % (3493866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.12 % (3493866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.12 % (3493866)CaDiCaL version: 2.1.3
% 2.99/1.12 % (3493866)Termination reason: Instruction limit
% 2.99/1.12 % (3493866)Termination phase: Saturation
% 2.99/1.12 % (3493866)Time elapsed: 0.067 s
% 2.99/1.12 % (3493866)Peak memory usage: 89 MB
% 2.99/1.12 % (3493866)Instructions burned: 115 (million)
% 2.99/1.12 % (3493867)Refutation not found, incomplete strategy
% 2.99/1.12 % (3493867)------------------------------
% 2.99/1.12 % (3493867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.12 % (3493867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.12 % (3493867)CaDiCaL version: 2.1.3
% 2.99/1.12 % (3493867)Termination reason: Refutation not found, incomplete strategy
% 2.99/1.12 % (3493867)Time elapsed: 0.061 s
% 2.99/1.12 % (3493867)Peak memory usage: 89 MB
% 2.99/1.12 % (3493867)Instructions burned: 102 (million)
% 2.99/1.12 % (3493876)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=3377220379:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 2.99/1.12 % (3493868)------------------------------
% 2.99/1.12 % (3493868)------------------------------
% 2.99/1.12 % (3493876)Instruction limit reached!
% 2.99/1.12 % (3493876)------------------------------
% 2.99/1.12 % (3493876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.12 % (3493876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.12 % (3493876)CaDiCaL version: 2.1.3
% 2.99/1.12 % (3493876)Termination reason: Instruction limit
% 2.99/1.12 % (3493876)Termination phase: Saturation
% 2.99/1.12 % (3493876)Time elapsed: 0.091 s
% 2.99/1.12 % (3493876)Peak memory usage: 88 MB
% 2.99/1.12 % (3493876)Instructions burned: 144 (million)
% 2.99/1.12 % SZS status Satisfiable for theBenchmark
% 2.99/1.12 % SZS output start Saturation.
% See solution above
% 3.87/1.32 % SZS output start Definitions and Model Updates.
% 3.87/1.32 for all inputs,
% 3.87/1.32 define a_56 := a_58
% 3.87/1.32 % SZS output end Definitions and Model Updates.
% 3.87/1.32 % (3493865)------------------------------
% 3.87/1.32 % (3493865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.87/1.32 % (3493865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.87/1.32 % (3493865)CaDiCaL version: 2.1.3
% 3.87/1.32 % (3493865)Termination reason: Satisfiable
% 3.87/1.32 % (3493865)Time elapsed: 0.048 s
% 3.87/1.32 % (3493865)Peak memory usage: 89 MB
% 3.87/1.32 % (3493865)Instructions burned: 82 (million)
% 3.87/1.32 % (3493865)------------------------------
% 3.87/1.32 % (3493865)------------------------------
% 3.87/1.32 % (3493857)Success in time 0.459 s
% 3.87/1.32 % Vampire exiting
%------------------------------------------------------------------------------