%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV502-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:08 PM UTC 2026
% Result : Satisfiable 15.45s 3.61s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1124,axiom,
i1 != sF60 ).
cnf(u1129,axiom,
sF61 = select(sF28,sF60) ).
cnf(u1301,axiom,
i10 != sF60 ).
cnf(u1306,axiom,
sF62 = select(sF58,sF60) ).
cnf(u1439,axiom,
i7 != sF60 ).
cnf(u1444,axiom,
sF62 = select(sF57,sF60) ).
cnf(u1587,axiom,
i29 != sF60 ).
cnf(u1592,axiom,
sF61 = select(sF27,sF60) ).
cnf(u1691,axiom,
i24 != sF60 ).
cnf(u1696,axiom,
sF62 = select(sF56,sF60) ).
cnf(u1770,axiom,
i23 != sF60 ).
cnf(u1775,axiom,
sF62 = select(sF55,sF60) ).
cnf(u1856,axiom,
i28 != sF60 ).
cnf(u1861,axiom,
sF61 = select(sF26,sF60) ).
cnf(u1935,axiom,
i27 != sF60 ).
cnf(u1940,axiom,
sF61 = select(sF25,sF60) ).
cnf(u2021,axiom,
i17 != sF60 ).
cnf(u2026,axiom,
sF62 = select(sF54,sF60) ).
cnf(u2130,axiom,
i16 != sF60 ).
cnf(u2135,axiom,
sF62 = select(sF52,sF60) ).
cnf(u2245,axiom,
i26 != sF60 ).
cnf(u2250,axiom,
sF61 = select(sF24,sF60) ).
cnf(u2330,axiom,
i25 != sF60 ).
cnf(u2335,axiom,
sF61 = select(sF23,sF60) ).
cnf(u2466,axiom,
i22 != sF60 ).
cnf(u2471,axiom,
sF61 = select(sF20,sF60) ).
cnf(u2559,axiom,
i21 != sF60 ).
cnf(u2564,axiom,
sF61 = select(sF19,sF60) ).
cnf(u2683,axiom,
i20 != sF60 ).
cnf(u2688,axiom,
sF61 = select(sF18,sF60) ).
cnf(u2818,axiom,
i19 != sF60 ).
cnf(u2823,axiom,
sF61 = select(sF17,sF60) ).
cnf(u2988,axiom,
i18 != sF60 ).
cnf(u2993,axiom,
sF61 = select(sF16,sF60) ).
cnf(u3141,axiom,
i15 != sF60 ).
cnf(u3146,axiom,
sF61 = select(sF13,sF60) ).
cnf(u3303,axiom,
i14 != sF60 ).
cnf(u3308,axiom,
sF61 = select(sF12,sF60) ).
cnf(u3436,axiom,
i13 != sF60 ).
cnf(u3441,axiom,
sF61 = select(sF11,sF60) ).
cnf(u3632,axiom,
i12 != sF60 ).
cnf(u3637,axiom,
sF61 = select(sF10,sF60) ).
cnf(u3769,axiom,
i11 != sF60 ).
cnf(u3774,axiom,
sF61 = select(sF9,sF60) ).
cnf(u3907,axiom,
i9 != sF60 ).
cnf(u3912,axiom,
sF61 = select(sF7,sF60) ).
cnf(u4097,axiom,
i8 != sF60 ).
cnf(u4102,axiom,
sF61 = select(sF6,sF60) ).
cnf(u4258,axiom,
i6 != sF60 ).
cnf(u4263,axiom,
sF61 = select(sF4,sF60) ).
cnf(u4419,axiom,
i5 != sF60 ).
cnf(u4424,axiom,
sF61 = select(sF3,sF60) ).
cnf(u4567,axiom,
i4 != sF60 ).
cnf(u4572,axiom,
sF61 = select(sF2,sF60) ).
cnf(u4776,axiom,
i3 != sF60 ).
cnf(u4781,axiom,
sF61 = select(sF1,sF60) ).
cnf(u4969,axiom,
i2 != sF60 ).
cnf(u4974,axiom,
sF61 = select(sF0,sF60) ).
cnf(u5150,axiom,
i30 = sF60 ).
cnf(u661,hypothesis,
i26 != i4 ).
cnf(u1021,axiom,
( select(sF33,X0) = select(sF34,X0)
| i9 = X0 ) ).
cnf(u948,axiom,
store(sF36,i15,e15) = sF37 ).
cnf(u659,hypothesis,
i27 != i4 ).
cnf(u1019,axiom,
( select(sF28,X0) = select(sF27,X0)
| i29 = X0 ) ).
cnf(u21,hypothesis,
i27 != i26 ).
cnf(u151,hypothesis,
i22 != i18 ).
cnf(u289,hypothesis,
i23 != i13 ).
cnf(u521,hypothesis,
i24 != i7 ).
cnf(u805,hypothesis,
i7 != i2 ).
cnf(u535,hypothesis,
i17 != i7 ).
cnf(u906,axiom,
store(sF15,i17,e17) = sF16 ).
cnf(u803,hypothesis,
i8 != i2 ).
cnf(u149,hypothesis,
i23 != i18 ).
cnf(u912,axiom,
store(sF18,i20,e20) = sF19 ).
cnf(u295,hypothesis,
i20 != i13 ).
cnf(u417,hypothesis,
i13 != i10 ).
cnf(u649,hypothesis,
i7 != i5 ).
cnf(u663,hypothesis,
i25 != i4 ).
cnf(u61,hypothesis,
i29 != i22 ).
cnf(u293,hypothesis,
i21 != i13 ).
cnf(u375,hypothesis,
i15 != i11 ).
cnf(u561,hypothesis,
i27 != i6 ).
cnf(u1077,axiom,
( select(sF7,X0) = select(sF6,X0)
| i8 = X0 ) ).
cnf(u575,hypothesis,
i20 != i6 ).
cnf(u946,axiom,
store(sF35,i2,e2) = sF36 ).
cnf(u1058,axiom,
e24 = select(sF23,i24) ).
cnf(u51,hypothesis,
i27 != i23 ).
cnf(u189,hypothesis,
i28 != i16 ).
cnf(u952,axiom,
store(sF38,i18,e18) = sF39 ).
cnf(u421,hypothesis,
i11 != i10 ).
cnf(u970,axiom,
store(sF47,i26,e26) = sF48 ).
cnf(u914,axiom,
store(sF19,i21,e21) = sF20 ).
cnf(u179,hypothesis,
i20 != i17 ).
cnf(u335,hypothesis,
i17 != i12 ).
cnf(u1087,axiom,
( select(sF13,X0) = select(sF12,X0)
| i14 = X0 ) ).
cnf(u950,axiom,
store(sF37,i25,e25) = sF38 ).
cnf(u5193,axiom,
e30 = select(sF56,sF60) ).
cnf(u177,hypothesis,
i21 != i17 ).
cnf(u956,axiom,
store(sF40,i8,e8) = sF41 ).
cnf(u1094,axiom,
e19 = select(sF32,i19) ).
cnf(u333,hypothesis,
i18 != i12 ).
cnf(u833,hypothesis,
i21 != i1 ).
cnf(u1068,axiom,
e26 = select(sF25,i26) ).
cnf(u5206,axiom,
e30 = select(sF43,sF60) ).
cnf(u1117,axiom,
( select(sF30,X0) = select(sF31,X0)
| i1 = X0 ) ).
cnf(u847,hypothesis,
i14 != i1 ).
cnf(u1098,axiom,
e5 = select(sF4,i5) ).
cnf(u5201,axiom,
e30 = select(sF48,sF60) ).
cnf(u91,hypothesis,
i22 != i21 ).
cnf(u1092,axiom,
e22 = select(sF49,i22) ).
cnf(u323,hypothesis,
i23 != i12 ).
cnf(u461,hypothesis,
i11 != i9 ).
cnf(u5210,axiom,
e30 = select(sF39,sF60) ).
cnf(u5204,axiom,
e30 = select(sF45,sF60) ).
cnf(u1107,axiom,
( select(sF57,X0) = select(sF56,X0)
| i24 = X0 ) ).
cnf(u1096,axiom,
e7 = select(sF6,i7) ).
cnf(u5207,axiom,
e30 = select(sF42,sF60) ).
cnf(u89,hypothesis,
i23 != i21 ).
cnf(u451,hypothesis,
i16 != i9 ).
cnf(u605,hypothesis,
i29 != i5 ).
cnf(u5208,axiom,
e30 = select(sF41,sF60) ).
cnf(u5212,axiom,
e30 = select(sF37,sF60) ).
cnf(u990,axiom,
store(sF57,i7,e7) = sF58 ).
cnf(u95,hypothesis,
i29 != i20 ).
cnf(u217,hypothesis,
i28 != i15 ).
cnf(u996,axiom,
select(sF29,sF60) = sF61 ).
cnf(u363,hypothesis,
i21 != i11 ).
cnf(u733,hypothesis,
i16 != i3 ).
cnf(u1001,axiom,
( select(a1,X0) = select(sF30,X0)
| i13 = X0 ) ).
cnf(u731,hypothesis,
i17 != i3 ).
cnf(u1015,axiom,
( select(sF49,X0) = select(sF50,X0)
| i27 = X0 ) ).
cnf(u223,hypothesis,
i25 != i15 ).
cnf(u361,hypothesis,
i22 != i11 ).
cnf(u491,hypothesis,
i17 != i8 ).
cnf(u517,hypothesis,
i26 != i7 ).
cnf(u515,hypothesis,
i27 != i7 ).
cnf(u7,hypothesis,
i29 != i28 ).
cnf(u984,axiom,
store(sF54,i17,e17) = sF55 ).
cnf(u1044,axiom,
e22 = select(sF21,i22) ).
cnf(u489,hypothesis,
i18 != i8 ).
cnf(u645,hypothesis,
i9 != i5 ).
cnf(u1005,axiom,
( select(sF58,X0) = select(sF59,X0)
| i10 = X0 ) ).
cnf(u890,axiom,
store(sF7,i9,e9) = sF8 ).
cnf(u643,hypothesis,
i10 != i5 ).
cnf(u1003,axiom,
( select(a1,X0) = select(sF0,X0)
| i1 = X0 ) ).
cnf(u273,hypothesis,
i15 != i14 ).
cnf(u495,hypothesis,
i15 != i8 ).
cnf(u633,hypothesis,
i15 != i5 ).
cnf(u789,hypothesis,
i15 != i2 ).
cnf(u519,hypothesis,
i25 != i7 ).
cnf(u1018,axiom,
e29 = select(sF28,i29) ).
cnf(u787,hypothesis,
i16 != i2 ).
cnf(u133,hypothesis,
i20 != i19 ).
cnf(u896,axiom,
store(sF10,i12,e12) = sF11 ).
cnf(u279,hypothesis,
i28 != i13 ).
cnf(u401,hypothesis,
i21 != i10 ).
cnf(u1025,axiom,
( select(sF21,X0) = select(sF22,X0)
| i23 = X0 ) ).
cnf(u647,hypothesis,
i8 != i5 ).
cnf(u277,hypothesis,
i29 != i13 ).
cnf(u407,hypothesis,
i18 != i10 ).
cnf(u545,hypothesis,
i12 != i7 ).
cnf(u829,hypothesis,
i23 != i1 ).
cnf(u1061,axiom,
( select(sF52,X0) = select(sF51,X0)
| i12 = X0 ) ).
cnf(u559,hypothesis,
i28 != i6 ).
cnf(u930,axiom,
store(sF27,i29,e29) = sF28 ).
cnf(u1042,axiom,
e21 = select(sF20,i21) ).
cnf(u35,hypothesis,
i29 != i24 ).
cnf(u173,hypothesis,
i23 != i17 ).
cnf(u319,hypothesis,
i25 != i12 ).
cnf(u405,hypothesis,
i19 != i10 ).
cnf(u1065,axiom,
( select(sF23,X0) = select(sF24,X0)
| i25 = X0 ) ).
cnf(u687,hypothesis,
i13 != i4 ).
cnf(u713,hypothesis,
i26 != i3 ).
cnf(u163,hypothesis,
i28 != i17 ).
cnf(u1078,axiom,
e18 = select(sF17,i18) ).
cnf(u317,hypothesis,
i26 != i12 ).
cnf(u447,hypothesis,
i18 != i9 ).
cnf(u1071,axiom,
( select(sF41,X0) = select(sF42,X0)
| i21 = X0 ) ).
cnf(u817,hypothesis,
i29 != i1 ).
cnf(u934,axiom,
store(a1,i13,e13) = sF30 ).
cnf(u831,hypothesis,
i22 != i1 ).
cnf(u1082,axiom,
e14 = select(sF45,i14) ).
cnf(u161,hypothesis,
i29 != i17 ).
cnf(u940,axiom,
store(sF32,i4,e4) = sF33 ).
cnf(u307,hypothesis,
i14 != i13 ).
cnf(u445,hypothesis,
i19 != i9 ).
cnf(u1101,axiom,
( select(sF53,X0) = select(sF54,X0)
| i28 = X0 ) ).
cnf(u1080,axiom,
e8 = select(sF41,i8) ).
cnf(u5213,axiom,
e30 = select(sF36,sF60) ).
cnf(u435,hypothesis,
i24 != i9 ).
cnf(u1052,axiom,
e16 = select(sF53,i16) ).
cnf(u1091,axiom,
( select(sF43,X0) = select(sF42,X0)
| i6 = X0 ) ).
cnf(u5198,axiom,
e30 = select(sF51,sF60) ).
cnf(u73,hypothesis,
i23 != i22 ).
cnf(u5203,axiom,
e30 = select(sF46,sF60) ).
cnf(u589,hypothesis,
i13 != i6 ).
cnf(u1111,axiom,
( select(sF50,X0) = select(sF51,X0)
| i3 = X0 ) ).
cnf(u857,hypothesis,
i9 != i1 ).
cnf(u587,hypothesis,
i14 != i6 ).
cnf(u974,axiom,
store(sF49,i27,e27) = sF50 ).
cnf(u871,hypothesis,
i2 != i1 ).
cnf(u79,hypothesis,
i28 != i21 ).
cnf(u201,hypothesis,
i22 != i16 ).
cnf(u1116,axiom,
e1 = select(sF31,i1) ).
cnf(u347,hypothesis,
i29 != i11 ).
cnf(u717,hypothesis,
i24 != i3 ).
cnf(u715,hypothesis,
i25 != i3 ).
cnf(u207,hypothesis,
i19 != i16 ).
cnf(u475,hypothesis,
i25 != i8 ).
cnf(u629,hypothesis,
i17 != i5 ).
cnf(u861,hypothesis,
i7 != i1 ).
cnf(u627,hypothesis,
i18 != i5 ).
cnf(u859,hypothesis,
i8 != i1 ).
cnf(u119,hypothesis,
i27 != i19 ).
cnf(u968,axiom,
store(sF46,i5,e5) = sF47 ).
cnf(u1028,axiom,
e18 = select(sF39,i18) ).
cnf(u473,hypothesis,
i26 != i8 ).
cnf(u757,hypothesis,
i4 != i3 ).
cnf(u874,axiom,
store(a1,i1,e1) = sF0 ).
cnf(u755,hypothesis,
i5 != i3 ).
cnf(u1113,axiom,
( select(sF33,X0) = select(sF32,X0)
| i4 = X0 ) ).
cnf(u117,hypothesis,
i28 != i19 ).
cnf(u880,axiom,
store(sF2,i4,e4) = sF3 ).
cnf(u247,hypothesis,
i28 != i14 ).
cnf(u257,hypothesis,
i23 != i14 ).
cnf(u479,hypothesis,
i23 != i8 ).
cnf(u617,hypothesis,
i23 != i5 ).
cnf(u773,hypothesis,
i23 != i2 ).
cnf(u631,hypothesis,
i16 != i5 ).
cnf(u1002,axiom,
e1 = select(sF0,i1) ).
cnf(u771,hypothesis,
i24 != i2 ).
cnf(u245,hypothesis,
i29 != i14 ).
cnf(u1008,axiom,
e1 = select(sF29,i1) ).
cnf(u263,hypothesis,
i20 != i14 ).
cnf(u385,hypothesis,
i29 != i10 ).
cnf(u745,hypothesis,
i10 != i3 ).
cnf(u29,hypothesis,
i27 != i25 ).
cnf(u261,hypothesis,
i21 != i14 ).
cnf(u391,hypothesis,
i26 != i10 ).
cnf(u529,hypothesis,
i20 != i7 ).
cnf(u1045,axiom,
( select(sF21,X0) = select(sF20,X0)
| i22 = X0 ) ).
cnf(u543,hypothesis,
i13 != i7 ).
cnf(u1026,axiom,
e11 = select(sF10,i11) ).
cnf(u19,hypothesis,
i28 != i26 ).
cnf(u157,hypothesis,
i19 != i18 ).
cnf(u303,hypothesis,
i16 != i13 ).
cnf(u389,hypothesis,
i27 != i10 ).
cnf(u1049,axiom,
( select(sF10,X0) = select(sF11,X0)
| i12 = X0 ) ).
cnf(u671,hypothesis,
i21 != i4 ).
cnf(u17,hypothesis,
i29 != i26 ).
cnf(u147,hypothesis,
i24 != i18 ).
cnf(u1062,axiom,
e11 = select(sF44,i11) ).
cnf(u301,hypothesis,
i17 != i13 ).
cnf(u431,hypothesis,
i26 != i9 ).
cnf(u569,hypothesis,
i23 != i6 ).
cnf(u1055,axiom,
( select(sF55,X0) = select(sF54,X0)
| i17 = X0 ) ).
cnf(u801,hypothesis,
i9 != i2 ).
cnf(u1085,axiom,
( select(sF27,X0) = select(sF26,X0)
| i28 = X0 ) ).
cnf(u918,axiom,
store(sF21,i23,e23) = sF22 ).
cnf(u1066,axiom,
e16 = select(sF15,i16) ).
cnf(u145,hypothesis,
i25 != i18 ).
cnf(u924,axiom,
store(sF24,i26,e26) = sF25 ).
cnf(u291,hypothesis,
i22 != i13 ).
cnf(u429,hypothesis,
i27 != i9 ).
cnf(u1075,axiom,
( select(sF47,X0) = select(sF48,X0)
| i26 = X0 ) ).
cnf(u1064,axiom,
e25 = select(sF24,i25) ).
cnf(u57,hypothesis,
i24 != i23 ).
cnf(u187,hypothesis,
i29 != i16 ).
cnf(u419,hypothesis,
i12 != i10 ).
cnf(u573,hypothesis,
i21 != i6 ).
cnf(u571,hypothesis,
i22 != i6 ).
cnf(u958,axiom,
store(sF41,i21,e21) = sF42 ).
cnf(u63,hypothesis,
i28 != i22 ).
cnf(u1102,axiom,
e10 = select(sF9,i10) ).
cnf(u701,hypothesis,
i6 != i4 ).
cnf(u1095,axiom,
( select(sF31,X0) = select(sF32,X0)
| i19 = X0 ) ).
cnf(u841,hypothesis,
i17 != i1 ).
cnf(u5205,axiom,
e30 = select(sF44,sF60) ).
cnf(u699,hypothesis,
i7 != i4 ).
cnf(u855,hypothesis,
i10 != i1 ).
cnf(u3121,axiom,
sF61 = select(sF15,sF60) ).
cnf(u191,hypothesis,
i27 != i16 ).
cnf(u964,axiom,
store(sF44,i14,e14) = sF45 ).
cnf(u331,hypothesis,
i19 != i12 ).
cnf(u1115,axiom,
( select(sF11,X0) = select(sF12,X0)
| i13 = X0 ) ).
cnf(u1104,axiom,
e6 = select(sF5,i6) ).
cnf(u329,hypothesis,
i20 != i12 ).
cnf(u459,hypothesis,
i12 != i9 ).
cnf(u613,hypothesis,
i25 != i5 ).
cnf(u845,hypothesis,
i15 != i1 ).
cnf(u611,hypothesis,
i26 != i5 ).
cnf(u843,hypothesis,
i16 != i1 ).
cnf(u103,hypothesis,
i25 != i20 ).
cnf(u457,hypothesis,
i13 != i9 ).
cnf(u741,hypothesis,
i12 != i3 ).
cnf(u739,hypothesis,
i13 != i3 ).
cnf(u5191,axiom,
e30 = select(sF58,sF60) ).
cnf(u101,hypothesis,
i26 != i20 ).
cnf(u231,hypothesis,
i21 != i15 ).
cnf(u369,hypothesis,
i18 != i11 ).
cnf(u463,hypothesis,
i10 != i9 ).
cnf(u601,hypothesis,
i7 != i6 ).
cnf(u5195,axiom,
e30 = select(sF54,sF60) ).
cnf(u615,hypothesis,
i24 != i5 ).
cnf(u986,axiom,
store(sF55,i23,e23) = sF56 ).
cnf(u229,hypothesis,
i22 != i15 ).
cnf(u992,axiom,
store(sF58,i10,e10) = sF59 ).
cnf(u497,hypothesis,
i14 != i8 ).
cnf(u729,hypothesis,
i18 != i3 ).
cnf(u1013,axiom,
( select(sF58,X0) = select(sF57,X0)
| i7 = X0 ) ).
cnf(u900,axiom,
store(sF12,i14,e14) = sF13 ).
cnf(u743,hypothesis,
i11 != i3 ).
cnf(u1011,axiom,
( select(sF1,X0) = select(sF2,X0)
| i3 = X0 ) ).
cnf(u13,hypothesis,
i28 != i27 ).
cnf(u219,hypothesis,
i27 != i15 ).
cnf(u373,hypothesis,
i16 != i11 ).
cnf(u503,hypothesis,
i11 != i8 ).
cnf(u513,hypothesis,
i28 != i7 ).
cnf(u1029,axiom,
( select(sF38,X0) = select(sF39,X0)
| i18 = X0 ) ).
cnf(u527,hypothesis,
i21 != i7 ).
cnf(u898,axiom,
store(sF11,i13,e13) = sF12 ).
cnf(u5189,axiom,
e30 = select(sF59,sF60) ).
cnf(u141,hypothesis,
i27 != i18 ).
cnf(u287,hypothesis,
i24 != i13 ).
cnf(u501,hypothesis,
i12 != i8 ).
cnf(u641,hypothesis,
i11 != i5 ).
cnf(u655,hypothesis,
i29 != i4 ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u131,hypothesis,
i21 != i19 ).
cnf(u1046,axiom,
e9 = select(sF8,i9) ).
cnf(u285,hypothesis,
i25 != i13 ).
cnf(u415,hypothesis,
i14 != i10 ).
cnf(u553,hypothesis,
i8 != i7 ).
cnf(u1039,axiom,
( select(sF13,X0) = select(sF14,X0)
| i15 = X0 ) ).
cnf(u203,hypothesis,
i21 != i16 ).
cnf(u785,hypothesis,
i17 != i2 ).
cnf(u1069,axiom,
( select(sF25,X0) = select(sF24,X0)
| i26 = X0 ) ).
cnf(u902,axiom,
store(sF13,i15,e15) = sF14 ).
cnf(u799,hypothesis,
i10 != i2 ).
cnf(u1050,axiom,
e23 = select(sF56,i23) ).
cnf(u43,hypothesis,
i25 != i24 ).
cnf(u129,hypothesis,
i22 != i19 ).
cnf(u908,axiom,
store(sF16,i18,e18) = sF17 ).
cnf(u2454,axiom,
sF61 = select(sF21,sF60) ).
cnf(u413,hypothesis,
i15 != i10 ).
cnf(u1073,axiom,
( select(sF38,X0) = select(sF37,X0)
| i25 = X0 ) ).
cnf(u1059,axiom,
( select(sF22,X0) = select(sF23,X0)
| i24 = X0 ) ).
cnf(u1048,axiom,
e12 = select(sF11,i12) ).
cnf(u41,hypothesis,
i26 != i24 ).
cnf(u171,hypothesis,
i24 != i17 ).
cnf(u1086,axiom,
e14 = select(sF13,i14) ).
cnf(u403,hypothesis,
i20 != i10 ).
cnf(u557,hypothesis,
i29 != i6 ).
cnf(u1079,axiom,
( select(sF17,X0) = select(sF16,X0)
| i18 = X0 ) ).
cnf(u825,hypothesis,
i25 != i1 ).
cnf(u942,axiom,
store(sF33,i9,e9) = sF34 ).
cnf(u5089,axiom,
sF61 = select(a1,sF60) ).
cnf(u47,hypothesis,
i29 != i23 ).
cnf(u169,hypothesis,
i25 != i17 ).
cnf(u1084,axiom,
e28 = select(sF27,i28) ).
cnf(u315,hypothesis,
i27 != i12 ).
cnf(u685,hypothesis,
i14 != i4 ).
cnf(u972,axiom,
store(sF48,i22,e22) = sF49 ).
cnf(u683,hypothesis,
i15 != i4 ).
cnf(u839,hypothesis,
i18 != i1 ).
cnf(u175,hypothesis,
i22 != i17 ).
cnf(u313,hypothesis,
i28 != i12 ).
cnf(u443,hypothesis,
i20 != i9 ).
cnf(u4212,axiom,
sF61 = select(sF5,sF60) ).
cnf(u5196,axiom,
e30 = select(sF53,sF60) ).
cnf(u1099,axiom,
( select(sF3,X0) = select(sF4,X0)
| i5 = X0 ) ).
cnf(u827,hypothesis,
i24 != i1 ).
cnf(u1088,axiom,
e2 = select(sF36,i2) ).
cnf(u936,axiom,
store(sF30,i1,e1) = sF31 ).
cnf(u441,hypothesis,
i21 != i9 ).
cnf(u597,hypothesis,
i9 != i6 ).
cnf(u5200,axiom,
e30 = select(sF49,sF60) ).
cnf(u595,hypothesis,
i10 != i6 ).
cnf(u87,hypothesis,
i24 != i21 ).
cnf(u725,hypothesis,
i20 != i3 ).
cnf(u85,hypothesis,
i25 != i21 ).
cnf(u215,hypothesis,
i29 != i15 ).
cnf(u353,hypothesis,
i26 != i11 ).
cnf(u1081,axiom,
( select(sF40,X0) = select(sF41,X0)
| i8 = X0 ) ).
cnf(u585,hypothesis,
i15 != i6 ).
cnf(u5197,axiom,
e30 = select(sF52,sF60) ).
cnf(u869,hypothesis,
i3 != i1 ).
cnf(u599,hypothesis,
i8 != i6 ).
cnf(u867,hypothesis,
i4 != i1 ).
cnf(u976,axiom,
store(sF50,i3,e3) = sF51 ).
cnf(u359,hypothesis,
i23 != i11 ).
cnf(u481,hypothesis,
i22 != i8 ).
cnf(u1105,axiom,
( select(sF5,X0) = select(sF4,X0)
| i6 = X0 ) ).
cnf(u882,axiom,
store(sF3,i5,e5) = sF4 ).
cnf(u727,hypothesis,
i19 != i3 ).
cnf(u5187,axiom,
( select(sF34,X0) = select(sF35,X0)
| sF60 = X0 ) ).
cnf(u125,hypothesis,
i24 != i19 ).
cnf(u888,axiom,
store(sF6,i8,e8) = sF7 ).
cnf(u357,hypothesis,
i24 != i11 ).
cnf(u487,hypothesis,
i19 != i8 ).
cnf(u625,hypothesis,
i19 != i5 ).
cnf(u5202,axiom,
e30 = select(sF47,sF60) ).
cnf(u639,hypothesis,
i12 != i5 ).
cnf(u1010,axiom,
e3 = select(sF2,i3) ).
cnf(u115,hypothesis,
i29 != i19 ).
cnf(u253,hypothesis,
i25 != i14 ).
cnf(u271,hypothesis,
i16 != i14 ).
cnf(u485,hypothesis,
i20 != i8 ).
cnf(u753,hypothesis,
i6 != i3 ).
cnf(u886,axiom,
store(sF5,i7,e7) = sF6 ).
cnf(u767,hypothesis,
i26 != i2 ).
cnf(u892,axiom,
store(sF8,i10,e10) = sF9 ).
cnf(u1030,axiom,
e19 = select(sF18,i19) ).
cnf(u269,hypothesis,
i17 != i14 ).
cnf(u399,hypothesis,
i22 != i10 ).
cnf(u769,hypothesis,
i25 != i2 ).
cnf(u1053,axiom,
( select(sF52,X0) = select(sF53,X0)
| i16 = X0 ) ).
cnf(u1014,axiom,
e27 = select(sF50,i27) ).
cnf(u783,hypothesis,
i18 != i2 ).
cnf(u1034,axiom,
e20 = select(sF19,i20) ).
cnf(u27,hypothesis,
i28 != i25 ).
cnf(u241,hypothesis,
i16 != i15 ).
cnf(u1020,axiom,
e9 = select(sF34,i9) ).
cnf(u259,hypothesis,
i22 != i14 ).
cnf(u397,hypothesis,
i23 != i10 ).
cnf(u1057,axiom,
( select(sF15,X0) = select(sF16,X0)
| i17 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u1043,axiom,
( select(sF19,X0) = select(sF20,X0)
| i21 = X0 ) ).
cnf(u1032,axiom,
e15 = select(sF37,i15) ).
cnf(u25,hypothesis,
i29 != i25 ).
cnf(u155,hypothesis,
i20 != i18 ).
cnf(u1070,axiom,
e21 = select(sF42,i21) ).
cnf(u387,hypothesis,
i28 != i10 ).
cnf(u541,hypothesis,
i14 != i7 ).
cnf(u1063,axiom,
( select(sF43,X0) = select(sF44,X0)
| i11 = X0 ) ).
cnf(u809,hypothesis,
i5 != i2 ).
cnf(u539,hypothesis,
i15 != i7 ).
cnf(u926,axiom,
store(sF25,i27,e27) = sF26 ).
cnf(u823,hypothesis,
i26 != i1 ).
cnf(u31,hypothesis,
i26 != i25 ).
cnf(u153,hypothesis,
i21 != i18 ).
cnf(u932,axiom,
store(sF28,i1,e1) = sF29 ).
cnf(u299,hypothesis,
i18 != i13 ).
cnf(u669,hypothesis,
i22 != i4 ).
cnf(u1083,axiom,
( select(sF45,X0) = select(sF44,X0)
| i14 = X0 ) ).
cnf(u667,hypothesis,
i23 != i4 ).
cnf(u3125,axiom,
sF61 = select(sF14,sF60) ).
cnf(u1072,axiom,
e25 = select(sF38,i25) ).
cnf(u297,hypothesis,
i19 != i13 ).
cnf(u427,hypothesis,
i28 != i9 ).
cnf(u813,hypothesis,
i3 != i2 ).
cnf(u811,hypothesis,
i4 != i2 ).
cnf(u920,axiom,
store(sF22,i24,e24) = sF23 ).
cnf(u425,hypothesis,
i29 != i9 ).
cnf(u581,hypothesis,
i17 != i6 ).
cnf(u5188,axiom,
e30 = sF62 ).
cnf(u579,hypothesis,
i18 != i6 ).
cnf(u71,hypothesis,
i24 != i22 ).
cnf(u709,hypothesis,
i28 != i3 ).
cnf(u954,axiom,
store(sF39,i20,e20) = sF40 ).
cnf(u69,hypothesis,
i25 != i22 ).
cnf(u199,hypothesis,
i23 != i16 ).
cnf(u337,hypothesis,
i16 != i12 ).
cnf(u697,hypothesis,
i8 != i4 ).
cnf(u853,hypothesis,
i11 != i1 ).
cnf(u583,hypothesis,
i16 != i6 ).
cnf(u851,hypothesis,
i12 != i1 ).
cnf(u197,hypothesis,
i24 != i16 ).
cnf(u960,axiom,
store(sF42,i6,e6) = sF43 ).
cnf(u343,hypothesis,
i13 != i12 ).
cnf(u1089,axiom,
( select(sF36,X0) = select(sF35,X0)
| i2 = X0 ) ).
cnf(u711,hypothesis,
i27 != i3 ).
cnf(u109,hypothesis,
i22 != i20 ).
cnf(u341,hypothesis,
i14 != i12 ).
cnf(u471,hypothesis,
i27 != i8 ).
cnf(u609,hypothesis,
i27 != i5 ).
cnf(u623,hypothesis,
i20 != i5 ).
cnf(u994,axiom,
sk(sF29,sF59) = sF60 ).
cnf(u5211,axiom,
e30 = select(sF38,sF60) ).
cnf(u1106,axiom,
e24 = select(sF57,i24) ).
cnf(u5209,axiom,
e30 = select(sF40,sF60) ).
cnf(u99,hypothesis,
i27 != i20 ).
cnf(u237,hypothesis,
i18 != i15 ).
cnf(u469,hypothesis,
i28 != i8 ).
cnf(u737,hypothesis,
i14 != i3 ).
cnf(u751,hypothesis,
i7 != i3 ).
cnf(u97,hypothesis,
i28 != i20 ).
cnf(u876,axiom,
store(sF0,i2,e2) = sF1 ).
cnf(u227,hypothesis,
i23 != i15 ).
cnf(u381,hypothesis,
i12 != i11 ).
cnf(u511,hypothesis,
i29 != i7 ).
cnf(u1037,axiom,
( select(sF2,X0) = select(sF3,X0)
| i4 = X0 ) ).
cnf(u11,hypothesis,
i29 != i27 ).
cnf(u225,hypothesis,
i24 != i15 ).
cnf(u1004,axiom,
e10 = select(sF59,i10) ).
cnf(u371,hypothesis,
i17 != i11 ).
cnf(u1041,axiom,
( select(sF39,X0) = select(sF40,X0)
| i20 = X0 ) ).
cnf(u1009,axiom,
( select(sF28,X0) = select(sF29,X0)
| i1 = X0 ) ).
cnf(u1027,axiom,
( select(sF9,X0) = select(sF10,X0)
| i11 = X0 ) ).
cnf(u703,hypothesis,
i5 != i4 ).
cnf(u1023,axiom,
( select(sF25,X0) = select(sF26,X0)
| i27 = X0 ) ).
cnf(u689,hypothesis,
i12 != i4 ).
cnf(u139,hypothesis,
i28 != i18 ).
cnf(u1054,axiom,
e17 = select(sF55,i17) ).
cnf(u499,hypothesis,
i13 != i8 ).
cnf(u525,hypothesis,
i22 != i7 ).
cnf(u1047,axiom,
( select(sF7,X0) = select(sF8,X0)
| i9 = X0 ) ).
cnf(u793,hypothesis,
i13 != i2 ).
cnf(u523,hypothesis,
i23 != i7 ).
cnf(u910,axiom,
store(sF17,i19,e19) = sF18 ).
cnf(u807,hypothesis,
i6 != i2 ).
cnf(u137,hypothesis,
i29 != i18 ).
cnf(u916,axiom,
store(sF20,i22,e22) = sF21 ).
cnf(u283,hypothesis,
i26 != i13 ).
cnf(u1067,axiom,
( select(sF14,X0) = select(sF15,X0)
| i16 = X0 ) ).
cnf(u651,hypothesis,
i6 != i5 ).
cnf(u1056,axiom,
e17 = select(sF16,i17) ).
cnf(u49,hypothesis,
i28 != i23 ).
cnf(u143,hypothesis,
i26 != i18 ).
cnf(u281,hypothesis,
i27 != i13 ).
cnf(u411,hypothesis,
i16 != i10 ).
cnf(u565,hypothesis,
i25 != i6 ).
cnf(u797,hypothesis,
i11 != i2 ).
cnf(u563,hypothesis,
i26 != i6 ).
cnf(u795,hypothesis,
i12 != i2 ).
cnf(u55,hypothesis,
i25 != i23 ).
cnf(u904,axiom,
store(sF14,i16,e16) = sF15 ).
cnf(u409,hypothesis,
i17 != i10 ).
cnf(u980,axiom,
store(sF52,i16,e16) = sF53 ).
cnf(u693,hypothesis,
i10 != i4 ).
cnf(u691,hypothesis,
i11 != i4 ).
cnf(u53,hypothesis,
i26 != i23 ).
cnf(u183,hypothesis,
i18 != i17 ).
cnf(u567,hypothesis,
i24 != i6 ).
cnf(u938,axiom,
store(sF31,i19,e19) = sF32 ).
cnf(u181,hypothesis,
i19 != i17 ).
cnf(u321,hypothesis,
i24 != i12 ).
cnf(u681,hypothesis,
i16 != i4 ).
cnf(u837,hypothesis,
i19 != i1 ).
cnf(u695,hypothesis,
i9 != i4 ).
cnf(u761,hypothesis,
i29 != i2 ).
cnf(u327,hypothesis,
i21 != i12 ).
cnf(u449,hypothesis,
i17 != i9 ).
cnf(u5185,axiom,
sF35 = store(sF34,sF60,e30) ).
cnf(u325,hypothesis,
i22 != i12 ).
cnf(u455,hypothesis,
i14 != i9 ).
cnf(u593,hypothesis,
i11 != i6 ).
cnf(u1109,axiom,
( select(sF46,X0) = select(sF47,X0)
| i5 = X0 ) ).
cnf(u607,hypothesis,
i28 != i5 ).
cnf(u978,axiom,
store(sF51,i12,e12) = sF52 ).
cnf(u1090,axiom,
e6 = select(sF43,i6) ).
cnf(u83,hypothesis,
i26 != i21 ).
cnf(u221,hypothesis,
i26 != i15 ).
cnf(u367,hypothesis,
i19 != i11 ).
cnf(u453,hypothesis,
i15 != i9 ).
cnf(u721,hypothesis,
i22 != i3 ).
cnf(u735,hypothesis,
i15 != i3 ).
cnf(u5199,axiom,
e30 = select(sF50,sF60) ).
cnf(u81,hypothesis,
i27 != i21 ).
cnf(u211,hypothesis,
i17 != i16 ).
cnf(u365,hypothesis,
i20 != i11 ).
cnf(u1100,axiom,
e28 = select(sF54,i28) ).
cnf(u865,hypothesis,
i5 != i1 ).
cnf(u982,axiom,
store(sF53,i28,e28) = sF54 ).
cnf(u123,hypothesis,
i25 != i19 ).
cnf(u209,hypothesis,
i18 != i16 ).
cnf(u988,axiom,
store(sF56,i24,e24) = sF57 ).
cnf(u355,hypothesis,
i25 != i11 ).
cnf(u493,hypothesis,
i16 != i8 ).
cnf(u894,axiom,
store(sF9,i11,e11) = sF10 ).
cnf(u723,hypothesis,
i21 != i3 ).
cnf(u1007,axiom,
( select(sF0,X0) = select(sF1,X0)
| i2 = X0 ) ).
cnf(u121,hypothesis,
i26 != i19 ).
cnf(u251,hypothesis,
i26 != i14 ).
cnf(u1038,axiom,
e15 = select(sF14,i15) ).
cnf(u483,hypothesis,
i21 != i8 ).
cnf(u637,hypothesis,
i13 != i5 ).
cnf(u1031,axiom,
( select(sF17,X0) = select(sF18,X0)
| i19 = X0 ) ).
cnf(u777,hypothesis,
i21 != i2 ).
cnf(u673,hypothesis,
i20 != i4 ).
cnf(u635,hypothesis,
i14 != i5 ).
cnf(u1022,axiom,
e27 = select(sF26,i27) ).
cnf(u791,hypothesis,
i14 != i2 ).
cnf(u127,hypothesis,
i23 != i19 ).
cnf(u249,hypothesis,
i27 != i14 ).
cnf(u1036,axiom,
e4 = select(sF3,i4) ).
cnf(u267,hypothesis,
i18 != i14 ).
cnf(u765,hypothesis,
i27 != i2 ).
cnf(u1051,axiom,
( select(sF55,X0) = select(sF56,X0)
| i23 = X0 ) ).
cnf(u763,hypothesis,
i28 != i2 ).
cnf(u1040,axiom,
e20 = select(sF40,i20) ).
cnf(u255,hypothesis,
i24 != i14 ).
cnf(u265,hypothesis,
i19 != i14 ).
cnf(u395,hypothesis,
i24 != i10 ).
cnf(u549,hypothesis,
i10 != i7 ).
cnf(u781,hypothesis,
i19 != i2 ).
cnf(u547,hypothesis,
i11 != i7 ).
cnf(u779,hypothesis,
i20 != i2 ).
cnf(u39,hypothesis,
i27 != i24 ).
cnf(u1016,axiom,
e29 = select(sF46,i29) ).
cnf(u1076,axiom,
e8 = select(sF7,i8) ).
cnf(u393,hypothesis,
i25 != i10 ).
cnf(u677,hypothesis,
i18 != i4 ).
cnf(u2450,axiom,
sF61 = select(sF22,sF60) ).
cnf(u675,hypothesis,
i19 != i4 ).
cnf(u37,hypothesis,
i28 != i24 ).
cnf(u167,hypothesis,
i26 != i17 ).
cnf(u305,hypothesis,
i15 != i13 ).
cnf(u537,hypothesis,
i16 != i7 ).
cnf(u821,hypothesis,
i27 != i1 ).
cnf(u551,hypothesis,
i9 != i7 ).
cnf(u922,axiom,
store(sF23,i25,e25) = sF24 ).
cnf(u819,hypothesis,
i28 != i1 ).
cnf(u165,hypothesis,
i27 != i17 ).
cnf(u928,axiom,
store(sF26,i28,e28) = sF27 ).
cnf(u311,hypothesis,
i29 != i12 ).
cnf(u433,hypothesis,
i25 != i9 ).
cnf(u665,hypothesis,
i24 != i4 ).
cnf(u679,hypothesis,
i17 != i4 ).
cnf(u439,hypothesis,
i22 != i9 ).
cnf(u1074,axiom,
e26 = select(sF48,i26) ).
cnf(u77,hypothesis,
i29 != i21 ).
cnf(u437,hypothesis,
i23 != i9 ).
cnf(u1033,axiom,
( select(sF36,X0) = select(sF37,X0)
| i15 = X0 ) ).
cnf(u577,hypothesis,
i19 != i6 ).
cnf(u1093,axiom,
( select(sF49,X0) = select(sF48,X0)
| i22 = X0 ) ).
cnf(u591,hypothesis,
i12 != i6 ).
cnf(u962,axiom,
store(sF43,i11,e11) = sF44 ).
cnf(u67,hypothesis,
i26 != i22 ).
cnf(u205,hypothesis,
i20 != i16 ).
cnf(u351,hypothesis,
i27 != i11 ).
cnf(u5186,axiom,
e30 = select(sF35,sF60) ).
cnf(u1097,axiom,
( select(sF6,X0) = select(sF5,X0)
| i7 = X0 ) ).
cnf(u5190,negated_conjecture,
e30 != sF61 ).
cnf(u719,hypothesis,
i23 != i3 ).
cnf(u65,hypothesis,
i27 != i22 ).
cnf(u195,hypothesis,
i25 != i16 ).
cnf(u1110,axiom,
e3 = select(sF51,i3) ).
cnf(u349,hypothesis,
i28 != i11 ).
cnf(u1103,axiom,
( select(sF9,X0) = select(sF8,X0)
| i10 = X0 ) ).
cnf(u5194,axiom,
e30 = select(sF55,sF60) ).
cnf(u849,hypothesis,
i13 != i1 ).
cnf(u966,axiom,
store(sF45,i29,e29) = sF46 ).
cnf(u863,hypothesis,
i6 != i1 ).
cnf(u1114,axiom,
e13 = select(sF12,i13) ).
cnf(u107,hypothesis,
i23 != i20 ).
cnf(u193,hypothesis,
i26 != i16 ).
cnf(u1108,axiom,
e5 = select(sF47,i5) ).
cnf(u339,hypothesis,
i15 != i12 ).
cnf(u477,hypothesis,
i24 != i8 ).
cnf(u5192,axiom,
e30 = select(sF57,sF60) ).
cnf(u835,hypothesis,
i20 != i1 ).
cnf(u878,axiom,
store(sF1,i3,e3) = sF2 ).
cnf(u707,hypothesis,
i29 != i3 ).
cnf(u1112,axiom,
e4 = select(sF33,i4) ).
cnf(u105,hypothesis,
i24 != i20 ).
cnf(u884,axiom,
store(sF4,i6,e6) = sF5 ).
cnf(u235,hypothesis,
i19 != i15 ).
cnf(u467,hypothesis,
i29 != i8 ).
cnf(u621,hypothesis,
i21 != i5 ).
cnf(u3875,axiom,
sF61 = select(sF8,sF60) ).
cnf(u619,hypothesis,
i22 != i5 ).
cnf(u1006,axiom,
e2 = select(sF1,i2) ).
cnf(u775,hypothesis,
i22 != i2 ).
cnf(u111,hypothesis,
i21 != i20 ).
cnf(u233,hypothesis,
i20 != i15 ).
cnf(u1012,axiom,
e7 = select(sF58,i7) ).
cnf(u379,hypothesis,
i13 != i11 ).
cnf(u657,hypothesis,
i28 != i4 ).
cnf(u749,hypothesis,
i8 != i3 ).
cnf(u1017,axiom,
( select(sF45,X0) = select(sF46,X0)
| i29 = X0 ) ).
cnf(u1035,axiom,
( select(sF18,X0) = select(sF19,X0)
| i20 = X0 ) ).
cnf(u747,hypothesis,
i9 != i3 ).
cnf(u1024,axiom,
e23 = select(sF22,i23) ).
cnf(u239,hypothesis,
i17 != i15 ).
cnf(u377,hypothesis,
i14 != i11 ).
cnf(u507,hypothesis,
i9 != i8 ).
cnf(u533,hypothesis,
i18 != i7 ).
cnf(u531,hypothesis,
i19 != i7 ).
cnf(u1000,axiom,
e13 = select(sF30,i13) ).
cnf(u1060,axiom,
e12 = select(sF52,i12) ).
cnf(u505,hypothesis,
i10 != i8 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV502-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 % Computer : n002.cluster.edu
% 0.08/0.22 % Model : x86_64 x86_64
% 0.08/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.22 % Memory : 8046.5625MB
% 0.08/0.22 % OS : Linux 6.8.0-71-generic
% 0.08/0.22 % CPULimit : 300
% 0.08/0.22 % WCLimit : 300
% 0.08/0.22 % DateTime : Mon Sep 28 11:24:22 UTC 2026
% 0.08/0.22 % CPUTime :
% 0.08/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.26 Running first-order theorem proving
% 0.18/0.26 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.88/1.56 % (294256)Input is clausal, will run a generic CNF schedule.
% 6.88/1.56 % (294266)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3370113609:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.88/1.56 % (294265)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2628883833:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.88/1.56 % (294267)dis-21_1_sil=8000:lcm=predicate:random_seed=3243274553: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)
% 6.88/1.56 % (294262)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3487170841:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.88/1.56 % (294261)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=731911574:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.88/1.56 % (294264)lrs+10_1_sil=8000:sp=occurrence:random_seed=2660604001:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.88/1.56 % (294263)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3778742802:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.88/1.56 % (294267)Refutation not found, incomplete strategy
% 6.88/1.56 % (294267)------------------------------
% 6.88/1.56 % (294267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.56 % (294267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.56 % (294267)CaDiCaL version: 2.1.3
% 6.88/1.56 % (294267)Termination reason: Refutation not found, incomplete strategy
% 6.88/1.56 % (294267)Time elapsed: 0.013 s
% 6.88/1.56 % (294267)Peak memory usage: 88 MB
% 6.88/1.56 % (294267)Instructions burned: 24 (million)
% 6.88/1.56 % (294266)Instruction limit reached!
% 6.88/1.56 % (294266)------------------------------
% 6.88/1.56 % (294266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.56 % (294266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.56 % (294266)CaDiCaL version: 2.1.3
% 6.88/1.56 % (294266)Termination reason: Instruction limit
% 6.88/1.56 % (294266)Termination phase: Saturation
% 6.88/1.56 % (294266)Time elapsed: 0.040 s
% 6.88/1.56 % (294266)Peak memory usage: 89 MB
% 6.88/1.56 % (294266)Instructions burned: 182 (million)
% 6.88/1.56 % (294264)Instruction limit reached!
% 6.88/1.56 % (294264)------------------------------
% 6.88/1.56 % (294264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.56 % (294264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.56 % (294264)CaDiCaL version: 2.1.3
% 6.88/1.56 % (294264)Termination reason: Instruction limit
% 6.88/1.56 % (294264)Termination phase: Saturation
% 6.88/1.56 % (294264)Time elapsed: 0.046 s
% 6.88/1.56 % (294264)Peak memory usage: 89 MB
% 6.88/1.56 % (294264)Instructions burned: 109 (million)
% 6.88/1.56 % (294265)Instruction limit reached!
% 6.88/1.56 % (294265)------------------------------
% 6.88/1.56 % (294265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.56 % (294265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.56 % (294265)CaDiCaL version: 2.1.3
% 6.88/1.56 % (294265)Termination reason: Instruction limit
% 6.88/1.56 % (294265)Termination phase: Saturation
% 6.88/1.56 % (294265)Time elapsed: 0.051 s
% 6.88/1.56 % (294265)Peak memory usage: 89 MB
% 6.88/1.56 % (294265)Instructions burned: 116 (million)
% 6.88/1.56 % (294275)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=1515867639:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.88/1.56 % (294275)Instruction limit reached!
% 6.88/1.56 % (294275)------------------------------
% 6.88/1.56 % (294275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.56 % (294275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.56 % (294275)CaDiCaL version: 2.1.3
% 6.88/1.56 % (294275)Termination reason: Instruction limit
% 6.88/1.56 % (294275)Termination phase: Saturation
% 6.88/1.56 % (294275)Time elapsed: 0.033 s
% 6.88/1.56 % (294275)Peak memory usage: 89 MB
% 6.88/1.56 % (294275)Instructions burned: 143 (million)
% 6.88/1.56 % (294276)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=514053744:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 12.31/2.25 % (294277)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=525490566:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 12.31/2.25 % (294279)lrs+10_64_to=lpo:sil=8000:random_seed=2137884472:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 12.31/2.25 % (294279)Instruction limit reached!
% 12.31/2.25 % (294279)------------------------------
% 12.31/2.25 % (294279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.31/2.25 % (294279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.31/2.25 % (294279)CaDiCaL version: 2.1.3
% 12.31/2.25 % (294279)Termination reason: Instruction limit
% 12.31/2.25 % (294279)Termination phase: Saturation
% 12.31/2.25 % (294279)Time elapsed: 0.027 s
% 12.31/2.25 % (294279)Peak memory usage: 88 MB
% 12.31/2.25 % (294279)Instructions burned: 132 (million)
% 12.31/2.25 % (294267)------------------------------
% 12.31/2.25 % (294267)------------------------------
% 12.31/2.25 % (294276)Instruction limit reached!
% 12.31/2.25 % (294276)------------------------------
% 12.31/2.25 % (294276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.31/2.25 % (294276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.31/2.25 % (294276)CaDiCaL version: 2.1.3
% 12.31/2.25 % (294276)Termination reason: Instruction limit
% 12.31/2.25 % (294276)Termination phase: Saturation
% 12.31/2.25 % (294276)Time elapsed: 0.091 s
% 12.31/2.25 % (294276)Peak memory usage: 90 MB
% 12.31/2.25 % (294276)Instructions burned: 191 (million)
% 12.31/2.25 % (294277)Instruction limit reached!
% 12.31/2.25 % (294277)------------------------------
% 12.31/2.25 % (294277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.31/2.25 % (294277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.31/2.25 % (294277)CaDiCaL version: 2.1.3
% 12.31/2.25 % (294277)Termination reason: Instruction limit
% 12.31/2.25 % (294277)Termination phase: Saturation
% 12.31/2.25 % (294277)Time elapsed: 0.091 s
% 12.31/2.25 % (294277)Peak memory usage: 89 MB
% 12.31/2.25 % (294277)Instructions burned: 220 (million)
% 12.31/2.25 % (294283)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2346814940:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 12.31/2.25 % (294283)Instruction limit reached!
% 12.31/2.25 % (294283)------------------------------
% 12.31/2.25 % (294283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.31/2.25 % (294283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.31/2.25 % (294283)CaDiCaL version: 2.1.3
% 12.31/2.25 % (294283)Termination reason: Instruction limit
% 12.31/2.25 % (294283)Termination phase: Saturation
% 12.31/2.25 % (294283)Time elapsed: 0.041 s
% 12.31/2.25 % (294283)Peak memory usage: 89 MB
% 12.31/2.25 % (294283)Instructions burned: 197 (million)
% 12.31/2.25 % (294284)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2450842186:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.31/2.25 % (294285)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3687627469:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 12.31/2.25 % (294286)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=65288890:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 12.31/2.25 % (294286)Instruction limit reached!
% 12.31/2.25 % (294286)------------------------------
% 12.31/2.25 % (294286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.31/2.25 % (294286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.31/2.25 % (294286)CaDiCaL version: 2.1.3
% 12.31/2.25 % (294286)Termination reason: Instruction limit
% 12.31/2.25 % (294286)Termination phase: Saturation
% 12.31/2.25 % (294286)Time elapsed: 0.057 s
% 12.31/2.25 % (294286)Peak memory usage: 90 MB
% 12.31/2.25 % (294286)Instructions burned: 107 (million)
% 12.31/2.25 % (294284)Instruction limit reached!
% 12.31/2.25 % (294284)------------------------------
% 12.31/2.25 % (294284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.31/2.25 % (294284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.31/2.25 % (294284)CaDiCaL version: 2.1.3
% 12.31/2.25 % (294284)Termination reason: Instruction limit
% 15.03/2.86 % (294284)Termination phase: Saturation
% 15.03/2.86 % (294284)Time elapsed: 0.077 s
% 15.03/2.86 % (294284)Peak memory usage: 91 MB
% 15.03/2.86 % (294284)Instructions burned: 158 (million)
% 15.03/2.86 % (294288)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=280414333:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 15.03/2.86 % (294288)Instruction limit reached!
% 15.03/2.86 % (294288)------------------------------
% 15.03/2.86 % (294288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.03/2.86 % (294288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.03/2.86 % (294288)CaDiCaL version: 2.1.3
% 15.03/2.86 % (294288)Termination reason: Instruction limit
% 15.03/2.86 % (294288)Termination phase: Saturation
% 15.03/2.86 % (294288)Time elapsed: 0.025 s
% 15.03/2.86 % (294288)Peak memory usage: 88 MB
% 15.03/2.86 % (294288)Instructions burned: 111 (million)
% 15.03/2.86 % (294295)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1030438780:i=134:sd=2:doe=on:ss=axioms:sgt=14_2993 on theBenchmark for (2993ds/134Mi)
% 15.03/2.86 % (294294)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1614650671:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 15.03/2.86 % (294292)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1347517905:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 15.03/2.86 % (294295)Instruction limit reached!
% 15.03/2.86 % (294295)------------------------------
% 15.03/2.86 % (294295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.03/2.86 % (294295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.03/2.86 % (294295)CaDiCaL version: 2.1.3
% 15.03/2.86 % (294295)Termination reason: Instruction limit
% 15.03/2.86 % (294295)Termination phase: Saturation
% 15.03/2.86 % (294295)Time elapsed: 0.031 s
% 15.03/2.86 % (294295)Peak memory usage: 89 MB
% 15.03/2.86 % (294295)Instructions burned: 138 (million)
% 15.03/2.86 % (294292)Instruction limit reached!
% 15.03/2.86 % (294292)------------------------------
% 15.03/2.86 % (294292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.03/2.86 % (294292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.03/2.86 % (294292)CaDiCaL version: 2.1.3
% 15.03/2.86 % (294292)Termination reason: Instruction limit
% 15.03/2.86 % (294292)Termination phase: Saturation
% 15.03/2.86 % (294292)Time elapsed: 0.101 s
% 15.03/2.86 % (294292)Peak memory usage: 88 MB
% 15.03/2.86 % (294292)Instructions burned: 244 (million)
% 15.03/2.86 % (294299)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=280501517:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 15.03/2.86 % (294299)Instruction limit reached!
% 15.03/2.86 % (294299)------------------------------
% 15.03/2.86 % (294299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.03/2.86 % (294299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.03/2.86 % (294299)CaDiCaL version: 2.1.3
% 15.03/2.86 % (294299)Termination reason: Instruction limit
% 15.03/2.86 % (294299)Termination phase: Saturation
% 15.03/2.86 % (294299)Time elapsed: 0.120 s
% 15.03/2.86 % (294299)Peak memory usage: 92 MB
% 15.03/2.86 % (294299)Instructions burned: 502 (million)
% 15.03/2.86 % (294300)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=172186127:i=191:fgj=on:bd=all_2991 on theBenchmark for (2991ds/191Mi)
% 15.03/2.86 % (294302)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4250256613:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 15.03/2.86 % (294300)Instruction limit reached!
% 15.03/2.86 % (294300)------------------------------
% 15.03/2.86 % (294300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.03/2.86 % (294300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.03/2.86 % (294300)CaDiCaL version: 2.1.3
% 15.03/2.86 % (294300)Termination reason: Instruction limit
% 15.03/2.86 % (294300)Termination phase: Saturation
% 15.03/2.86 % (294300)Time elapsed: 0.083 s
% 15.03/2.86 % (294300)Peak memory usage: 88 MB
% 15.03/2.86 % (294300)Instructions burned: 193 (million)
% 15.03/2.86 % (294302)Instruction limit reached!
% 15.03/2.86 % (294302)------------------------------
% 15.03/2.86 % (294302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294302)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294302)Termination reason: Instruction limit
% 15.45/3.61 % (294302)Termination phase: Saturation
% 15.45/3.61 % (294302)Time elapsed: 0.059 s
% 15.45/3.61 % (294302)Peak memory usage: 90 MB
% 15.45/3.61 % (294302)Instructions burned: 266 (million)
% 15.45/3.61 % (294305)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1442363537:cond=on:i=156:bs=on:gtg=exists_all:er=known_2989 on theBenchmark for (2989ds/156Mi)
% 15.45/3.61 % (294263)Refutation not found, incomplete strategy
% 15.45/3.61 % (294263)------------------------------
% 15.45/3.61 % (294263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294263)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294263)Termination reason: Refutation not found, incomplete strategy
% 15.45/3.61 % (294263)Time elapsed: 1.051 s
% 15.45/3.61 % (294263)Peak memory usage: 134 MB
% 15.45/3.61 % (294263)Instructions burned: 1630 (million)
% 15.45/3.61 % (294306)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1719124594:i=3256:kws=precedence:bd=preordered:av=off_2988 on theBenchmark for (2988ds/3256Mi)
% 15.45/3.61 % (294305)Instruction limit reached!
% 15.45/3.61 % (294305)------------------------------
% 15.45/3.61 % (294305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294305)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294305)Termination reason: Instruction limit
% 15.45/3.61 % (294305)Termination phase: Saturation
% 15.45/3.61 % (294305)Time elapsed: 0.070 s
% 15.45/3.61 % (294305)Peak memory usage: 89 MB
% 15.45/3.61 % (294305)Instructions burned: 158 (million)
% 15.45/3.61 % (294309)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4765481:i=537:av=off:ss=included_2987 on theBenchmark for (2987ds/537Mi)
% 15.45/3.61 % (294263)------------------------------
% 15.45/3.61 % (294263)------------------------------
% 15.45/3.61 % (294309)Instruction limit reached!
% 15.45/3.61 % (294309)------------------------------
% 15.45/3.61 % (294309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294309)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294309)Termination reason: Instruction limit
% 15.45/3.61 % (294309)Termination phase: Saturation
% 15.45/3.61 % (294309)Time elapsed: 0.200 s
% 15.45/3.61 % (294309)Peak memory usage: 88 MB
% 15.45/3.61 % (294309)Instructions burned: 537 (million)
% 15.45/3.61 % (294311)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1828488777:i=180:bd=preordered:av=off_2985 on theBenchmark for (2985ds/180Mi)
% 15.45/3.61 % (294261)Refutation not found, incomplete strategy
% 15.45/3.61 % (294261)------------------------------
% 15.45/3.61 % (294261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294261)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294261)Termination reason: Refutation not found, incomplete strategy
% 15.45/3.61 % (294261)Time elapsed: 1.517 s
% 15.45/3.61 % (294261)Peak memory usage: 135 MB
% 15.45/3.61 % (294261)Instructions burned: 2390 (million)
% 15.45/3.61 % (294311)Instruction limit reached!
% 15.45/3.61 % (294311)------------------------------
% 15.45/3.61 % (294311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294311)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294311)Termination reason: Instruction limit
% 15.45/3.61 % (294311)Termination phase: Saturation
% 15.45/3.61 % (294311)Time elapsed: 0.084 s
% 15.45/3.61 % (294311)Peak memory usage: 89 MB
% 15.45/3.61 % (294311)Instructions burned: 180 (million)
% 15.45/3.61 % (294312)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=124575754:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2984 on theBenchmark for (2984ds/10307Mi)
% 15.45/3.61 % (294314)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2495101756:i=412:gtgl=4:gtg=exists_all_2983 on theBenchmark for (2983ds/412Mi)
% 15.45/3.61 % (294314)Refutation not found, incomplete strategy
% 15.45/3.61 % (294314)------------------------------
% 15.45/3.61 % (294314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294314)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294314)Termination reason: Refutation not found, incomplete strategy
% 15.45/3.61 % (294314)Time elapsed: 0.061 s
% 15.45/3.61 % (294314)Peak memory usage: 91 MB
% 15.45/3.61 % (294314)Instructions burned: 111 (million)
% 15.45/3.61 % (294261)------------------------------
% 15.45/3.61 % (294261)------------------------------
% 15.45/3.61 % (294294)Refutation not found, incomplete strategy
% 15.45/3.61 % (294294)------------------------------
% 15.45/3.61 % (294294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294294)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294294)Termination reason: Refutation not found, incomplete strategy
% 15.45/3.61 % (294294)Time elapsed: 1.202 s
% 15.45/3.61 % (294294)Peak memory usage: 133 MB
% 15.45/3.61 % (294294)Instructions burned: 2072 (million)
% 15.45/3.61 % (294317)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1043529087:s2pl=no:i=8478:s2at=4:nm=6_2980 on theBenchmark for (2980ds/8478Mi)
% 15.45/3.61 % (294314)------------------------------
% 15.45/3.61 % (294314)------------------------------
% 15.45/3.61 % (294306)Instruction limit reached!
% 15.45/3.61 % (294306)------------------------------
% 15.45/3.61 % (294306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294306)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294306)Termination reason: Instruction limit
% 15.45/3.61 % (294306)Termination phase: Saturation
% 15.45/3.61 % (294306)Time elapsed: 0.958 s
% 15.45/3.61 % (294306)Peak memory usage: 144 MB
% 15.45/3.61 % (294306)Instructions burned: 3256 (million)
% 15.45/3.61 % (294294)------------------------------
% 15.45/3.61 % (294294)------------------------------
% 15.45/3.61 % (294319)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3599210909:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2979 on theBenchmark for (2979ds/303Mi)
% 15.45/3.61 % (294320)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1508467484:st=4:i=720:sd=3:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/720Mi)
% 15.45/3.61 % (294321)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=525901638:i=598:bs=on:bd=preordered:av=off:ss=axioms_2978 on theBenchmark for (2978ds/598Mi)
% 15.45/3.61 % (294319)Refutation not found, incomplete strategy
% 15.45/3.61 % (294319)------------------------------
% 15.45/3.61 % (294319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294319)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294319)Termination reason: Refutation not found, incomplete strategy
% 15.45/3.61 % (294319)Time elapsed: 0.076 s
% 15.45/3.61 % (294319)Peak memory usage: 90 MB
% 15.45/3.61 % (294319)Instructions burned: 180 (million)
% 15.45/3.61 % (294285)Instruction limit reached!
% 15.45/3.61 % (294285)------------------------------
% 15.45/3.61 % (294285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294285)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294285)Termination reason: Instruction limit
% 15.45/3.61 % (294285)Termination phase: Saturation
% 15.45/3.61 % (294285)Time elapsed: 1.822 s
% 15.45/3.61 % (294285)Peak memory usage: 137 MB
% 15.45/3.61 % (294285)Instructions burned: 3394 (million)
% 15.45/3.61 % (294320)Instruction limit reached!
% 15.45/3.61 % (294320)------------------------------
% 15.45/3.61 % (294320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294320)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294320)Termination reason: Instruction limit
% 15.45/3.61 % (294320)Termination phase: Saturation
% 15.45/3.61 % (294320)Time elapsed: 0.171 s
% 15.45/3.61 % (294320)Peak memory usage: 94 MB
% 15.45/3.61 % (294320)Instructions burned: 722 (million)
% 15.45/3.61 % (294325)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2480947718:i=2989:sd=3:ss=axioms:sgt=60_2976 on theBenchmark for (2976ds/2989Mi)
% 15.45/3.61 % (294326)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=83315277:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2975 on theBenchmark for (2975ds/1997Mi)
% 15.45/3.61 % (294319)------------------------------
% 15.45/3.61 % (294319)------------------------------
% 15.45/3.61 % (294321)Instruction limit reached!
% 15.45/3.61 % (294321)------------------------------
% 15.45/3.61 % (294321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/3.61 % (294321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/3.61 % (294321)CaDiCaL version: 2.1.3
% 15.45/3.61 % (294321)Termination reason: Instruction limit
% 15.45/3.61 % (294321)Termination phase: Saturation
% 15.45/3.61 % (294321)Time elapsed: 0.322 s
% 15.45/3.61 % (294321)Peak memory usage: 92 MB
% 15.45/3.61 % (294321)Instructions burned: 598 (million)
% 15.45/3.61 % (294329)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=161533778:i=2088:bd=preordered:av=off_2974 on theBenchmark for (2974ds/2088Mi)
% 15.45/3.61 % (294330)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2274940781:i=1098:nicw=on_2973 on theBenchmark for (2973ds/1098Mi)
% 15.45/3.61 % (294312)First to succeed.
% 15.45/3.61 % (294312)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-294256"
% 15.45/3.61 % SZS status Satisfiable for theBenchmark
% 15.45/3.61 % SZS output start Saturation.
% See solution above
% 0.19/3.80 % SZS output start Definitions and Model Updates.
% 0.19/3.80 % SZS output end Definitions and Model Updates.
% 0.19/3.80 % (294312)------------------------------
% 0.19/3.80 % (294312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.19/3.80 % (294312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/3.80 % (294312)CaDiCaL version: 2.1.3
% 0.19/3.80 % (294312)Termination reason: Satisfiable
% 0.19/3.80 % (294312)Time elapsed: 1.202 s
% 0.19/3.80 % (294312)Peak memory usage: 136 MB
% 0.19/3.80 % (294312)Instructions burned: 1784 (million)
% 0.19/3.80 % (294312)------------------------------
% 0.19/3.80 % (294312)------------------------------
% 0.19/3.80 % (294256)Success in time 3.155 s
% 0.19/3.80 % Vampire exiting
%------------------------------------------------------------------------------