%------------------------------------------------------------------------------
% File : Vampire-SAT---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/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:24:42 PM UTC 2026
% Result : Satisfiable 1.42s 0.53s
% Output : Saturation 1.42s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1126,axiom,
i1 != sF60 ).
cnf(u1131,axiom,
sF61 = select(sF28,sF60) ).
cnf(u1138,axiom,
i29 != sF60 ).
cnf(u1143,axiom,
sF61 = select(sF27,sF60) ).
cnf(u1164,axiom,
i10 != sF60 ).
cnf(u1169,axiom,
sF62 = select(sF58,sF60) ).
cnf(u1202,axiom,
i7 != sF60 ).
cnf(u1207,axiom,
sF62 = select(sF57,sF60) ).
cnf(u1435,axiom,
i24 != sF60 ).
cnf(u1440,axiom,
sF62 = select(sF56,sF60) ).
cnf(u1449,axiom,
i28 != sF60 ).
cnf(u1454,axiom,
sF61 = select(sF26,sF60) ).
cnf(u1461,axiom,
i23 != sF60 ).
cnf(u1466,axiom,
sF62 = select(sF55,sF60) ).
cnf(u1517,axiom,
i27 != sF60 ).
cnf(u1522,axiom,
sF61 = select(sF25,sF60) ).
cnf(u1529,axiom,
i17 != sF60 ).
cnf(u1534,axiom,
sF62 = select(sF54,sF60) ).
cnf(u1541,axiom,
i26 != sF60 ).
cnf(u1546,axiom,
sF61 = select(sF24,sF60) ).
cnf(u1644,axiom,
i16 != sF60 ).
cnf(u1649,axiom,
sF62 = select(sF52,sF60) ).
cnf(u1680,axiom,
i12 != sF60 ).
cnf(u1685,axiom,
sF62 = select(sF51,sF60) ).
cnf(u1694,axiom,
i3 != sF60 ).
cnf(u1699,axiom,
sF62 = select(sF50,sF60) ).
cnf(u1748,axiom,
i22 != sF60 ).
cnf(u1752,axiom,
e26 != sF62 ).
cnf(u1857,axiom,
i25 != sF60 ).
cnf(u1862,axiom,
sF61 = select(sF23,sF60) ).
cnf(u1917,axiom,
i21 != sF60 ).
cnf(u2064,axiom,
i5 != sF60 ).
cnf(u2069,axiom,
e10 != select(sF46,sF60) ).
cnf(u2096,hypothesis,
i6 != sF60 ).
cnf(u2101,hypothesis,
e10 != select(sF42,sF60) ).
cnf(u2116,hypothesis,
i8 != sF60 ).
cnf(u2121,hypothesis,
e10 != select(sF40,sF60) ).
cnf(u2245,axiom,
e7 != select(sF46,sF60) ).
cnf(u2276,hypothesis,
e7 != select(sF42,sF60) ).
cnf(u2353,axiom,
i14 != sF60 ).
cnf(u2358,axiom,
e10 != select(sF44,sF60) ).
cnf(u2363,axiom,
e7 != select(sF44,sF60) ).
cnf(u2367,hypothesis,
i20 != sF60 ).
cnf(u2372,hypothesis,
e10 != select(sF39,sF60) ).
cnf(u2377,hypothesis,
e7 != select(sF39,sF60) ).
cnf(u2572,hypothesis,
i2 != sF60 ).
cnf(u2577,hypothesis,
e10 != select(sF35,sF60) ).
cnf(u2583,hypothesis,
e7 != select(sF35,sF60) ).
cnf(u2593,hypothesis,
e3 != select(sF35,sF60) ).
cnf(u2647,hypothesis,
i19 != sF60 ).
cnf(u2652,hypothesis,
sF61 = select(sF17,sF60) ).
cnf(u2657,axiom,
i11 != sF60 ).
cnf(u2662,axiom,
e10 != select(sF43,sF60) ).
cnf(u2667,axiom,
e7 != select(sF43,sF60) ).
cnf(u2671,hypothesis,
i18 != sF60 ).
cnf(u2676,hypothesis,
e10 != select(sF38,sF60) ).
cnf(u2681,hypothesis,
e7 != select(sF38,sF60) ).
cnf(u2686,hypothesis,
i30 = sF60 ).
cnf(u2690,hypothesis,
e10 != select(sF34,sF60) ).
cnf(u2695,hypothesis,
e7 != select(sF34,sF60) ).
cnf(u2700,hypothesis,
e3 != select(sF34,sF60) ).
cnf(u2705,axiom,
e10 != select(sF45,sF60) ).
cnf(u2710,axiom,
e7 != select(sF45,sF60) ).
cnf(u2784,axiom,
sF62 = select(sF43,sF60) ).
cnf(u2869,hypothesis,
i15 != sF60 ).
cnf(u2874,hypothesis,
sF61 = select(sF13,sF60) ).
cnf(u2891,hypothesis,
i13 != sF60 ).
cnf(u2896,hypothesis,
sF61 = select(sF11,sF60) ).
cnf(u2990,hypothesis,
sF62 = select(sF35,sF60) ).
cnf(u3003,hypothesis,
i9 != sF60 ).
cnf(u3008,hypothesis,
e10 != select(sF33,sF60) ).
cnf(u3014,hypothesis,
e7 != select(sF33,sF60) ).
cnf(u3020,hypothesis,
e3 != select(sF33,sF60) ).
cnf(u3228,hypothesis,
i4 != sF60 ).
cnf(u3233,hypothesis,
e10 != select(sF32,sF60) ).
cnf(u3238,hypothesis,
e7 != select(sF32,sF60) ).
cnf(u3243,hypothesis,
e3 != select(sF32,sF60) ).
cnf(u3248,hypothesis,
sF61 = select(sF2,sF60) ).
cnf(u661,hypothesis,
i26 != i4 ).
cnf(u1021,axiom,
e21 = select(sF20,i21) ).
cnf(u948,axiom,
store(sF36,i15,e15) = sF37 ).
cnf(u3356,hypothesis,
e10 != sF61 ).
cnf(u659,hypothesis,
i27 != i4 ).
cnf(u1019,axiom,
e19 = select(sF18,i19) ).
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(u3360,hypothesis,
e7 != sF61 ).
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(u2825,hypothesis,
sF61 = select(sF14,sF60) ).
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(u423,hypothesis,
i30 != i9 ).
cnf(u561,hypothesis,
i27 != i6 ).
cnf(u1077,axiom,
( select(sF15,X0) = select(sF16,X0)
| i17 = X0 ) ).
cnf(u575,hypothesis,
i20 != i6 ).
cnf(u946,axiom,
store(sF35,i2,e2) = sF36 ).
cnf(u1058,axiom,
e7 = select(sF58,i7) ).
cnf(u51,hypothesis,
i27 != i23 ).
cnf(u189,hypothesis,
i28 != i16 ).
cnf(u952,axiom,
store(sF38,i18,e18) = sF39 ).
cnf(u421,hypothesis,
i11 != i10 ).
cnf(u689,hypothesis,
i12 != i4 ).
cnf(u914,axiom,
store(sF19,i21,e21) = sF20 ).
cnf(u179,hypothesis,
i20 != i17 ).
cnf(u335,hypothesis,
i17 != i12 ).
cnf(u1087,axiom,
( select(sF25,X0) = select(sF26,X0)
| i27 = X0 ) ).
cnf(u950,axiom,
store(sF37,i25,e25) = sF38 ).
cnf(u177,hypothesis,
i21 != i17 ).
cnf(u956,axiom,
store(sF40,i8,e8) = sF41 ).
cnf(u1094,axiom,
( select(sF33,X0) = select(sF34,X0)
| i9 = X0 ) ).
cnf(u333,hypothesis,
i18 != i12 ).
cnf(u833,hypothesis,
i21 != i1 ).
cnf(u1117,axiom,
( select(sF56,X0) = select(sF57,X0)
| i24 = X0 ) ).
cnf(u847,hypothesis,
i14 != i1 ).
cnf(u1098,axiom,
( select(sF37,X0) = select(sF38,X0)
| i25 = X0 ) ).
cnf(u91,hypothesis,
i22 != i21 ).
cnf(u1092,axiom,
( select(sF31,X0) = select(sF32,X0)
| i19 = X0 ) ).
cnf(u323,hypothesis,
i23 != i12 ).
cnf(u461,hypothesis,
i11 != i9 ).
cnf(u1107,axiom,
( select(sF46,X0) = select(sF47,X0)
| i5 = X0 ) ).
cnf(u1096,axiom,
( select(sF35,X0) = select(sF36,X0)
| i2 = X0 ) ).
cnf(u89,hypothesis,
i23 != i21 ).
cnf(u451,hypothesis,
i16 != i9 ).
cnf(u605,hypothesis,
i29 != i5 ).
cnf(u2761,axiom,
sF62 = select(sF45,sF60) ).
cnf(u603,hypothesis,
i30 != i5 ).
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,
e13 = select(sF30,i13) ).
cnf(u731,hypothesis,
i17 != i3 ).
cnf(u1015,axiom,
e15 = select(sF14,i15) ).
cnf(u223,hypothesis,
i25 != i15 ).
cnf(u361,hypothesis,
i22 != i11 ).
cnf(u491,hypothesis,
i17 != i8 ).
cnf(u517,hypothesis,
i26 != i7 ).
cnf(u2925,hypothesis,
sF62 = select(sF41,sF60) ).
cnf(u515,hypothesis,
i27 != i7 ).
cnf(u7,hypothesis,
i29 != i28 ).
cnf(u984,axiom,
store(sF54,i17,e17) = sF55 ).
cnf(u1044,axiom,
e11 = select(sF44,i11) ).
cnf(u489,hypothesis,
i18 != i8 ).
cnf(u645,hypothesis,
i9 != i5 ).
cnf(u1005,axiom,
e5 = select(sF4,i5) ).
cnf(u2943,hypothesis,
sF62 = select(sF39,sF60) ).
cnf(u890,axiom,
store(sF7,i9,e9) = sF8 ).
cnf(u3321,hypothesis,
e7 != e30 ).
cnf(u643,hypothesis,
i10 != i5 ).
cnf(u1003,axiom,
e3 = select(sF2,i3) ).
cnf(u5,hypothesis,
i30 != i28 ).
cnf(u2979,hypothesis,
sF62 = select(sF36,sF60) ).
cnf(u135,hypothesis,
i30 != i18 ).
cnf(u273,hypothesis,
i15 != i14 ).
cnf(u495,hypothesis,
i15 != i8 ).
cnf(u633,hypothesis,
i15 != i5 ).
cnf(u932,axiom,
store(sF28,i1,e1) = sF29 ).
cnf(u835,hypothesis,
i20 != i1 ).
cnf(u789,hypothesis,
i15 != i2 ).
cnf(u519,hypothesis,
i25 != i7 ).
cnf(u3351,hypothesis,
sF61 = select(sF0,sF60) ).
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,
e25 = select(sF24,i25) ).
cnf(u647,hypothesis,
i8 != i5 ).
cnf(u45,hypothesis,
i30 != i23 ).
cnf(u3315,hypothesis,
sF35 = store(sF34,sF60,e30) ).
cnf(u3139,hypothesis,
sF61 = select(sF9,sF60) ).
cnf(u277,hypothesis,
i29 != i13 ).
cnf(u407,hypothesis,
i18 != i10 ).
cnf(u545,hypothesis,
i12 != i7 ).
cnf(u829,hypothesis,
i23 != i1 ).
cnf(u1061,axiom,
( select(a1,X0) = select(sF30,X0)
| i13 = X0 ) ).
cnf(u559,hypothesis,
i28 != i6 ).
cnf(u930,axiom,
store(sF27,i29,e29) = sF28 ).
cnf(u1042,axiom,
e21 = select(sF42,i21) ).
cnf(u35,hypothesis,
i29 != i24 ).
cnf(u173,hypothesis,
i23 != i17 ).
cnf(u319,hypothesis,
i25 != i12 ).
cnf(u405,hypothesis,
i19 != i10 ).
cnf(u673,hypothesis,
i20 != i4 ).
cnf(u687,hypothesis,
i13 != i4 ).
cnf(u713,hypothesis,
i26 != i3 ).
cnf(u163,hypothesis,
i28 != i17 ).
cnf(u1078,axiom,
( select(sF16,X0) = select(sF17,X0)
| i18 = X0 ) ).
cnf(u317,hypothesis,
i26 != i12 ).
cnf(u447,hypothesis,
i18 != i9 ).
cnf(u1071,axiom,
( select(sF9,X0) = select(sF10,X0)
| i11 = X0 ) ).
cnf(u817,hypothesis,
i29 != i1 ).
cnf(u934,axiom,
store(a1,i13,e13) = sF30 ).
cnf(u831,hypothesis,
i22 != i1 ).
cnf(u1082,axiom,
( select(sF20,X0) = select(sF21,X0)
| i22 = X0 ) ).
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(sF40,X0) = select(sF41,X0)
| i8 = X0 ) ).
cnf(u1080,axiom,
( select(sF18,X0) = select(sF19,X0)
| i20 = X0 ) ).
cnf(u75,hypothesis,
i30 != i21 ).
cnf(u435,hypothesis,
i24 != i9 ).
cnf(u1091,axiom,
( select(sF30,X0) = select(sF31,X0)
| i1 = X0 ) ).
cnf(u2758,axiom,
e7 != sF62 ).
cnf(u73,hypothesis,
i23 != i22 ).
cnf(u1118,axiom,
( select(sF57,X0) = select(sF58,X0)
| i7 = X0 ) ).
cnf(u589,hypothesis,
i13 != i6 ).
cnf(u1111,axiom,
( select(sF50,X0) = select(sF51,X0)
| i3 = X0 ) ).
cnf(u857,hypothesis,
i9 != i1 ).
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,
( select(sF55,X0) = select(sF56,X0)
| i23 = X0 ) ).
cnf(u347,hypothesis,
i29 != i11 ).
cnf(u717,hypothesis,
i24 != i3 ).
cnf(u715,hypothesis,
i25 != i3 ).
cnf(u999,negated_conjecture,
sF61 != sF62 ).
cnf(u207,hypothesis,
i19 != i16 ).
cnf(u345,hypothesis,
i30 != i11 ).
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,
e28 = select(sF27,i28) ).
cnf(u473,hypothesis,
i26 != i8 ).
cnf(u757,hypothesis,
i4 != i3 ).
cnf(u1632,axiom,
sF62 = select(sF53,sF60) ).
cnf(u874,axiom,
store(a1,i1,e1) = sF0 ).
cnf(u755,hypothesis,
i5 != i3 ).
cnf(u1113,axiom,
( select(sF52,X0) = select(sF53,X0)
| i16 = 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(u2965,hypothesis,
sF62 = select(sF37,sF60) ).
cnf(u617,hypothesis,
i23 != i5 ).
cnf(u773,hypothesis,
i23 != i2 ).
cnf(u631,hypothesis,
i16 != i5 ).
cnf(u1002,axiom,
e2 = select(sF1,i2) ).
cnf(u771,hypothesis,
i24 != i2 ).
cnf(u916,axiom,
store(sF20,i22,e22) = sF21 ).
cnf(u245,hypothesis,
i29 != i14 ).
cnf(u1008,axiom,
e8 = select(sF7,i8) ).
cnf(u263,hypothesis,
i20 != i14 ).
cnf(u385,hypothesis,
i29 != i10 ).
cnf(u745,hypothesis,
i10 != i3 ).
cnf(u759,hypothesis,
i30 != i2 ).
cnf(u2958,hypothesis,
e7 != select(sF37,sF60) ).
cnf(u29,hypothesis,
i27 != i25 ).
cnf(u261,hypothesis,
i21 != i14 ).
cnf(u3320,hypothesis,
e3 != e30 ).
cnf(u391,hypothesis,
i26 != i10 ).
cnf(u529,hypothesis,
i20 != i7 ).
cnf(u1045,axiom,
e14 = select(sF45,i14) ).
cnf(u543,hypothesis,
i13 != i7 ).
cnf(u3348,hypothesis,
e3 != select(sF30,sF60) ).
cnf(u1026,axiom,
e26 = select(sF25,i26) ).
cnf(u19,hypothesis,
i28 != i26 ).
cnf(u157,hypothesis,
i19 != i18 ).
cnf(u303,hypothesis,
i16 != i13 ).
cnf(u389,hypothesis,
i27 != i10 ).
cnf(u3186,hypothesis,
sF61 = select(sF3,sF60) ).
cnf(u1049,axiom,
e22 = select(sF49,i22) ).
cnf(u938,axiom,
store(sF31,i19,e19) = sF32 ).
cnf(u1121,axiom,
( select(sF0,X0) = select(sF30,X0)
| i1 = X0
| i13 = X0 ) ).
cnf(u671,hypothesis,
i21 != i4 ).
cnf(u17,hypothesis,
i29 != i26 ).
cnf(u147,hypothesis,
i24 != i18 ).
cnf(u1062,axiom,
( select(sF0,X0) = select(sF1,X0)
| i2 = X0 ) ).
cnf(u301,hypothesis,
i17 != i13 ).
cnf(u431,hypothesis,
i26 != i9 ).
cnf(u569,hypothesis,
i23 != i6 ).
cnf(u1055,axiom,
e17 = select(sF55,i17) ).
cnf(u801,hypothesis,
i9 != i2 ).
cnf(u1085,axiom,
( select(sF23,X0) = select(sF24,X0)
| i25 = X0 ) ).
cnf(u918,axiom,
store(sF21,i23,e23) = sF22 ).
cnf(u815,hypothesis,
i30 != i1 ).
cnf(u1066,axiom,
( select(sF4,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u59,hypothesis,
i30 != i22 ).
cnf(u145,hypothesis,
i25 != i18 ).
cnf(u924,axiom,
store(sF24,i26,e26) = sF25 ).
cnf(u291,hypothesis,
i22 != i13 ).
cnf(u429,hypothesis,
i27 != i9 ).
cnf(u2974,hypothesis,
e7 != select(sF36,sF60) ).
cnf(u2970,hypothesis,
e10 != select(sF36,sF60) ).
cnf(u1075,axiom,
( select(sF13,X0) = select(sF14,X0)
| i15 = X0 ) ).
cnf(u1064,axiom,
( select(sF2,X0) = select(sF3,X0)
| i4 = X0 ) ).
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(u185,hypothesis,
i30 != i16 ).
cnf(u1102,axiom,
( select(sF41,X0) = select(sF42,X0)
| i21 = X0 ) ).
cnf(u701,hypothesis,
i6 != i4 ).
cnf(u1095,axiom,
( select(sF34,X0) = select(sF35,X0)
| i30 = X0 ) ).
cnf(u841,hypothesis,
i17 != i1 ).
cnf(u699,hypothesis,
i7 != i4 ).
cnf(u855,hypothesis,
i10 != i1 ).
cnf(u3329,hypothesis,
e26 != e30 ).
cnf(u191,hypothesis,
i27 != i16 ).
cnf(u964,axiom,
store(sF44,i14,e14) = sF45 ).
cnf(u331,hypothesis,
i19 != i12 ).
cnf(u1115,axiom,
( select(sF54,X0) = select(sF55,X0)
| i17 = X0 ) ).
cnf(u1104,axiom,
( select(sF43,X0) = select(sF44,X0)
| i11 = X0 ) ).
cnf(u329,hypothesis,
i20 != i12 ).
cnf(u459,hypothesis,
i12 != i9 ).
cnf(u613,hypothesis,
i25 != i5 ).
cnf(u845,hypothesis,
i15 != i1 ).
cnf(u3161,hypothesis,
sF61 = select(sF5,sF60) ).
cnf(u611,hypothesis,
i26 != i5 ).
cnf(u843,hypothesis,
i16 != i1 ).
cnf(u103,hypothesis,
i25 != i20 ).
cnf(u3151,hypothesis,
sF61 = select(sF6,sF60) ).
cnf(u457,hypothesis,
i13 != i9 ).
cnf(u741,hypothesis,
i12 != i3 ).
cnf(u739,hypothesis,
i13 != i3 ).
cnf(u1740,axiom,
sF62 = select(sF49,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(u865,hypothesis,
i5 != i1 ).
cnf(u615,hypothesis,
i24 != i5 ).
cnf(u986,axiom,
store(sF55,i23,e23) = sF56 ).
cnf(u2283,hypothesis,
e7 != select(sF41,sF60) ).
cnf(u229,hypothesis,
i22 != i15 ).
cnf(u992,axiom,
store(sF58,i10,e10) = sF59 ).
cnf(u375,hypothesis,
i15 != i11 ).
cnf(u497,hypothesis,
i14 != i8 ).
cnf(u729,hypothesis,
i18 != i3 ).
cnf(u1013,axiom,
e13 = select(sF12,i13) ).
cnf(u900,axiom,
store(sF12,i14,e14) = sF13 ).
cnf(u743,hypothesis,
i11 != i3 ).
cnf(u1011,axiom,
e11 = select(sF10,i11) ).
cnf(u13,hypothesis,
i28 != i27 ).
cnf(u219,hypothesis,
i27 != i15 ).
cnf(u373,hypothesis,
i16 != i11 ).
cnf(u503,hypothesis,
i11 != i8 ).
cnf(u691,hypothesis,
i11 != i4 ).
cnf(u513,hypothesis,
i28 != i7 ).
cnf(u1029,axiom,
e29 = select(sF28,i29) ).
cnf(u527,hypothesis,
i21 != i7 ).
cnf(u898,axiom,
store(sF11,i13,e13) = sF12 ).
cnf(u2033,axiom,
sF61 = select(sF20,sF60) ).
cnf(u3324,hypothesis,
( select(sF34,X0) = select(sF35,X0)
| sF60 = X0 ) ).
cnf(hyp0,hypothesis,
i29 != i30 ).
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,
e29 = select(sF46,i29) ).
cnf(u285,hypothesis,
i25 != i13 ).
cnf(u415,hypothesis,
i14 != i10 ).
cnf(u553,hypothesis,
i8 != i7 ).
cnf(u1039,axiom,
e18 = select(sF39,i18) ).
cnf(u203,hypothesis,
i21 != i16 ).
cnf(u785,hypothesis,
i17 != i2 ).
cnf(u1069,axiom,
( select(sF7,X0) = select(sF8,X0)
| i9 = X0 ) ).
cnf(u902,axiom,
store(sF13,i15,e15) = sF14 ).
cnf(u3330,negated_conjecture,
e30 != sF61 ).
cnf(u799,hypothesis,
i10 != i2 ).
cnf(u1050,axiom,
e27 = select(sF50,i27) ).
cnf(u43,hypothesis,
i25 != i24 ).
cnf(u129,hypothesis,
i22 != i19 ).
cnf(u908,axiom,
store(sF16,i18,e18) = sF17 ).
cnf(u275,hypothesis,
i30 != i13 ).
cnf(u413,hypothesis,
i15 != i10 ).
cnf(u2821,hypothesis,
sF61 = select(sF15,sF60) ).
cnf(u1073,axiom,
( select(sF11,X0) = select(sF12,X0)
| i13 = X0 ) ).
cnf(u2954,hypothesis,
e10 != select(sF37,sF60) ).
cnf(u1059,axiom,
e10 = select(sF59,i10) ).
cnf(u962,axiom,
store(sF43,i11,e11) = sF44 ).
cnf(u1048,axiom,
e26 = select(sF48,i26) ).
cnf(u41,hypothesis,
i26 != i24 ).
cnf(u171,hypothesis,
i24 != i17 ).
cnf(u1086,axiom,
( select(sF24,X0) = select(sF25,X0)
| i26 = X0 ) ).
cnf(u403,hypothesis,
i20 != i10 ).
cnf(u557,hypothesis,
i29 != i6 ).
cnf(u1079,axiom,
( select(sF17,X0) = select(sF18,X0)
| i19 = X0 ) ).
cnf(u2759,axiom,
e10 != sF62 ).
cnf(u825,hypothesis,
i25 != i1 ).
cnf(u555,hypothesis,
i30 != i6 ).
cnf(u942,axiom,
store(sF33,i9,e9) = sF34 ).
cnf(u47,hypothesis,
i29 != i23 ).
cnf(u169,hypothesis,
i25 != i17 ).
cnf(u1084,axiom,
( select(sF22,X0) = select(sF23,X0)
| i24 = X0 ) ).
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(u2745,axiom,
sF62 = select(sF47,sF60) ).
cnf(u175,hypothesis,
i22 != i17 ).
cnf(u313,hypothesis,
i28 != i12 ).
cnf(u443,hypothesis,
i20 != i9 ).
cnf(u1099,axiom,
( select(sF38,X0) = select(sF39,X0)
| i18 = X0 ) ).
cnf(u827,hypothesis,
i24 != i1 ).
cnf(u1088,axiom,
( select(sF26,X0) = select(sF27,X0)
| i28 = X0 ) ).
cnf(u936,axiom,
store(sF30,i1,e1) = sF31 ).
cnf(u441,hypothesis,
i21 != i9 ).
cnf(u597,hypothesis,
i9 != i6 ).
cnf(u595,hypothesis,
i10 != i6 ).
cnf(u87,hypothesis,
i24 != i21 ).
cnf(u725,hypothesis,
i20 != i3 ).
cnf(u2885,hypothesis,
sF62 = select(sF42,sF60) ).
cnf(u3322,hypothesis,
e10 != e30 ).
cnf(u85,hypothesis,
i25 != i21 ).
cnf(u215,hypothesis,
i29 != i15 ).
cnf(u353,hypothesis,
i26 != i11 ).
cnf(u1081,axiom,
( select(sF19,X0) = select(sF20,X0)
| i21 = X0 ) ).
cnf(u585,hypothesis,
i15 != i6 ).
cnf(u869,hypothesis,
i3 != i1 ).
cnf(u599,hypothesis,
i8 != i6 ).
cnf(u970,axiom,
store(sF47,i26,e26) = sF48 ).
cnf(u867,hypothesis,
i4 != i1 ).
cnf(u2931,hypothesis,
sF62 = select(sF40,sF60) ).
cnf(u213,hypothesis,
i30 != i15 ).
cnf(u976,axiom,
store(sF50,i3,e3) = sF51 ).
cnf(u359,hypothesis,
i23 != i11 ).
cnf(u481,hypothesis,
i22 != i8 ).
cnf(u1105,axiom,
( select(sF44,X0) = select(sF45,X0)
| i14 = X0 ) ).
cnf(u635,hypothesis,
i14 != i5 ).
cnf(u882,axiom,
store(sF3,i5,e5) = sF4 ).
cnf(u727,hypothesis,
i19 != i3 ).
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(u639,hypothesis,
i12 != i5 ).
cnf(u1010,axiom,
e10 = select(sF9,i10) ).
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(u113,hypothesis,
i30 != i19 ).
cnf(u892,axiom,
store(sF8,i10,e10) = sF9 ).
cnf(u243,hypothesis,
i30 != i14 ).
cnf(u1030,axiom,
e1 = select(sF29,i1) ).
cnf(u269,hypothesis,
i17 != i14 ).
cnf(u399,hypothesis,
i22 != i10 ).
cnf(u769,hypothesis,
i25 != i2 ).
cnf(u3339,hypothesis,
sF61 = select(sF1,sF60) ).
cnf(u1053,axiom,
e16 = select(sF53,i16) ).
cnf(u1014,axiom,
e14 = select(sF13,i14) ).
cnf(u783,hypothesis,
i18 != i2 ).
cnf(u1034,axiom,
e9 = select(sF34,i9) ).
cnf(u27,hypothesis,
i28 != i25 ).
cnf(u241,hypothesis,
i16 != i15 ).
cnf(u1020,axiom,
e20 = select(sF19,i20) ).
cnf(u259,hypothesis,
i22 != i14 ).
cnf(u3342,hypothesis,
e10 != select(sF30,sF60) ).
cnf(u397,hypothesis,
i23 != i10 ).
cnf(u1057,axiom,
e24 = select(sF57,i24) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u1043,axiom,
e6 = select(sF43,i6) ).
cnf(u1032,axiom,
e19 = select(sF32,i19) ).
cnf(u3346,hypothesis,
e7 != select(sF30,sF60) ).
cnf(u25,hypothesis,
i29 != i25 ).
cnf(u155,hypothesis,
i20 != i18 ).
cnf(u1070,axiom,
( select(sF8,X0) = select(sF9,X0)
| i10 = X0 ) ).
cnf(u309,hypothesis,
i30 != i12 ).
cnf(u387,hypothesis,
i28 != i10 ).
cnf(u541,hypothesis,
i14 != i7 ).
cnf(u705,hypothesis,
i30 != i3 ).
cnf(u1063,axiom,
( select(sF1,X0) = select(sF2,X0)
| i3 = X0 ) ).
cnf(u809,hypothesis,
i5 != i2 ).
cnf(u539,hypothesis,
i15 != i7 ).
cnf(u926,axiom,
store(sF25,i27,e27) = sF26 ).
cnf(u3167,hypothesis,
sF61 = select(sF4,sF60) ).
cnf(u823,hypothesis,
i26 != i1 ).
cnf(u31,hypothesis,
i26 != i25 ).
cnf(u153,hypothesis,
i21 != i18 ).
cnf(u1068,axiom,
( select(sF6,X0) = select(sF7,X0)
| i8 = X0 ) ).
cnf(u299,hypothesis,
i18 != i13 ).
cnf(u669,hypothesis,
i22 != i4 ).
cnf(u1083,axiom,
( select(sF21,X0) = select(sF22,X0)
| i23 = X0 ) ).
cnf(u667,hypothesis,
i23 != i4 ).
cnf(u1072,axiom,
( select(sF10,X0) = select(sF11,X0)
| i12 = X0 ) ).
cnf(u2994,hypothesis,
e3 != sF62 ).
cnf(u159,hypothesis,
i30 != i17 ).
cnf(u297,hypothesis,
i19 != i13 ).
cnf(u427,hypothesis,
i28 != i9 ).
cnf(u813,hypothesis,
i3 != i2 ).
cnf(u811,hypothesis,
i4 != i2 ).
cnf(u2817,hypothesis,
sF61 = select(sF16,sF60) ).
cnf(u920,axiom,
store(sF22,i24,e24) = sF23 ).
cnf(u425,hypothesis,
i29 != i9 ).
cnf(u2108,hypothesis,
e10 != select(sF41,sF60) ).
cnf(u581,hypothesis,
i17 != i6 ).
cnf(u2879,hypothesis,
sF61 = select(sF12,sF60) ).
cnf(u2741,axiom,
sF62 = select(sF48,sF60) ).
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(u1018,axiom,
e18 = select(sF17,i18) ).
cnf(u697,hypothesis,
i8 != i4 ).
cnf(u853,hypothesis,
i11 != i1 ).
cnf(u583,hypothesis,
i16 != i6 ).
cnf(u851,hypothesis,
i12 != i1 ).
cnf(u1065,axiom,
( select(sF3,X0) = select(sF4,X0)
| i5 = X0 ) ).
cnf(u197,hypothesis,
i24 != i16 ).
cnf(u960,axiom,
store(sF42,i6,e6) = sF43 ).
cnf(u343,hypothesis,
i13 != i12 ).
cnf(u465,hypothesis,
i30 != i8 ).
cnf(u1089,axiom,
( select(sF27,X0) = select(sF28,X0)
| i29 = 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(u1106,axiom,
( select(sF45,X0) = select(sF46,X0)
| i29 = X0 ) ).
cnf(u99,hypothesis,
i27 != i20 ).
cnf(u237,hypothesis,
i18 != i15 ).
cnf(u383,hypothesis,
i30 != i10 ).
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,
e15 = select(sF37,i15) ).
cnf(u998,axiom,
select(sF59,sF60) = sF62 ).
cnf(u11,hypothesis,
i29 != i27 ).
cnf(u225,hypothesis,
i24 != i15 ).
cnf(u1004,axiom,
e4 = select(sF3,i4) ).
cnf(u371,hypothesis,
i17 != i11 ).
cnf(u509,hypothesis,
i30 != i7 ).
cnf(u1041,axiom,
e8 = select(sF41,i8) ).
cnf(u1009,axiom,
e9 = select(sF8,i9) ).
cnf(u1027,axiom,
e27 = select(sF26,i27) ).
cnf(u703,hypothesis,
i5 != i4 ).
cnf(u1023,axiom,
e23 = select(sF22,i23) ).
cnf(u9,hypothesis,
i30 != i27 ).
cnf(u139,hypothesis,
i28 != i18 ).
cnf(u1054,axiom,
e28 = select(sF54,i28) ).
cnf(u499,hypothesis,
i13 != i8 ).
cnf(u525,hypothesis,
i22 != i7 ).
cnf(u2773,axiom,
sF62 = select(sF44,sF60) ).
cnf(u1047,axiom,
e5 = select(sF47,i5) ).
cnf(u793,hypothesis,
i13 != i2 ).
cnf(u523,hypothesis,
i23 != i7 ).
cnf(u910,axiom,
store(sF17,i19,e19) = sF18 ).
cnf(u807,hypothesis,
i6 != i2 ).
cnf(u15,hypothesis,
i30 != i26 ).
cnf(u137,hypothesis,
i29 != i18 ).
cnf(u1052,axiom,
e12 = select(sF52,i12) ).
cnf(u283,hypothesis,
i26 != i13 ).
cnf(u653,hypothesis,
i30 != i4 ).
cnf(u1067,axiom,
( select(sF5,X0) = select(sF6,X0)
| i7 = X0 ) ).
cnf(u651,hypothesis,
i6 != i5 ).
cnf(u1056,axiom,
e23 = select(sF56,i23) ).
cnf(u49,hypothesis,
i28 != i23 ).
cnf(u143,hypothesis,
i26 != i18 ).
cnf(u281,hypothesis,
i27 != i13 ).
cnf(u2460,hypothesis,
sF61 = select(sF18,sF60) ).
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(u53,hypothesis,
i26 != i23 ).
cnf(u183,hypothesis,
i18 != i17 ).
cnf(u2289,hypothesis,
e7 != select(sF40,sF60) ).
cnf(u567,hypothesis,
i24 != i6 ).
cnf(u181,hypothesis,
i19 != i17 ).
cnf(u944,axiom,
store(sF34,i30,e30) = sF35 ).
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(u2749,axiom,
sF62 = select(sF46,sF60) ).
cnf(u327,hypothesis,
i21 != i12 ).
cnf(u449,hypothesis,
i17 != i9 ).
cnf(u3364,hypothesis,
e3 != sF61 ).
cnf(u93,hypothesis,
i30 != i20 ).
cnf(u325,hypothesis,
i22 != i12 ).
cnf(u455,hypothesis,
i14 != i9 ).
cnf(u593,hypothesis,
i11 != i6 ).
cnf(u1109,axiom,
( select(sF48,X0) = select(sF49,X0)
| i22 = X0 ) ).
cnf(u607,hypothesis,
i28 != i5 ).
cnf(u978,axiom,
store(sF51,i12,e12) = sF52 ).
cnf(u1090,axiom,
( select(sF28,X0) = select(sF29,X0)
| i1 = X0 ) ).
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(u81,hypothesis,
i27 != i21 ).
cnf(u211,hypothesis,
i17 != i16 ).
cnf(u365,hypothesis,
i20 != i11 ).
cnf(u1100,axiom,
( select(sF39,X0) = select(sF40,X0)
| i20 = X0 ) ).
cnf(u1119,axiom,
( select(sF58,X0) = select(sF59,X0)
| i10 = X0 ) ).
cnf(u2019,axiom,
sF61 = select(sF22,sF60) ).
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,
e7 = select(sF6,i7) ).
cnf(u121,hypothesis,
i26 != i19 ).
cnf(u251,hypothesis,
i26 != i14 ).
cnf(u1038,axiom,
e25 = select(sF38,i25) ).
cnf(u483,hypothesis,
i21 != i8 ).
cnf(u637,hypothesis,
i13 != i5 ).
cnf(u1031,axiom,
e1 = select(sF31,i1) ).
cnf(u777,hypothesis,
i21 != i2 ).
cnf(u1022,axiom,
e22 = select(sF21,i22) ).
cnf(u2949,hypothesis,
sF62 = select(sF38,sF60) ).
cnf(u791,hypothesis,
i14 != i2 ).
cnf(u127,hypothesis,
i23 != i19 ).
cnf(u249,hypothesis,
i27 != i14 ).
cnf(u1036,axiom,
e2 = select(sF36,i2) ).
cnf(u267,hypothesis,
i18 != i14 ).
cnf(u765,hypothesis,
i27 != i2 ).
cnf(u1051,axiom,
e3 = select(sF51,i3) ).
cnf(u763,hypothesis,
i28 != i2 ).
cnf(u1040,axiom,
e20 = select(sF40,i20) ).
cnf(u33,hypothesis,
i30 != i24 ).
cnf(u255,hypothesis,
i24 != i14 ).
cnf(u2042,axiom,
sF61 = select(sF19,sF60) ).
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,
e16 = select(sF15,i16) ).
cnf(u1076,axiom,
( select(sF14,X0) = select(sF15,X0)
| i16 = X0 ) ).
cnf(u393,hypothesis,
i25 != i10 ).
cnf(u677,hypothesis,
i18 != i4 ).
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(u3143,hypothesis,
sF61 = select(sF8,sF60) ).
cnf(u1074,axiom,
( select(sF12,X0) = select(sF13,X0)
| i14 = X0 ) ).
cnf(u77,hypothesis,
i29 != i21 ).
cnf(u3319,hypothesis,
e30 = sF62 ).
cnf(u437,hypothesis,
i23 != i9 ).
cnf(u1033,axiom,
e4 = select(sF33,i4) ).
cnf(u577,hypothesis,
i19 != i6 ).
cnf(u3147,hypothesis,
sF61 = select(sF7,sF60) ).
cnf(u1093,axiom,
( select(sF32,X0) = select(sF33,X0)
| i4 = X0 ) ).
cnf(u591,hypothesis,
i12 != i6 ).
cnf(u67,hypothesis,
i26 != i22 ).
cnf(u205,hypothesis,
i20 != i16 ).
cnf(u351,hypothesis,
i27 != i11 ).
cnf(u1097,axiom,
( select(sF36,X0) = select(sF37,X0)
| i15 = X0 ) ).
cnf(u587,hypothesis,
i14 != i6 ).
cnf(u719,hypothesis,
i23 != i3 ).
cnf(u3334,hypothesis,
e7 != select(sF31,sF60) ).
cnf(u65,hypothesis,
i27 != i22 ).
cnf(u195,hypothesis,
i25 != i16 ).
cnf(u1110,axiom,
( select(sF49,X0) = select(sF50,X0)
| i27 = X0 ) ).
cnf(u349,hypothesis,
i28 != i11 ).
cnf(u1103,axiom,
( select(sF42,X0) = select(sF43,X0)
| i6 = X0 ) ).
cnf(u849,hypothesis,
i13 != i1 ).
cnf(u966,axiom,
store(sF45,i29,e29) = sF46 ).
cnf(u863,hypothesis,
i6 != i1 ).
cnf(u1114,axiom,
( select(sF53,X0) = select(sF54,X0)
| i28 = X0 ) ).
cnf(u107,hypothesis,
i23 != i20 ).
cnf(u193,hypothesis,
i26 != i16 ).
cnf(u1108,axiom,
( select(sF47,X0) = select(sF48,X0)
| i26 = X0 ) ).
cnf(u339,hypothesis,
i15 != i12 ).
cnf(u477,hypothesis,
i24 != i8 ).
cnf(u3135,hypothesis,
sF61 = select(sF10,sF60) ).
cnf(u878,axiom,
store(sF1,i3,e3) = sF2 ).
cnf(u707,hypothesis,
i29 != i3 ).
cnf(u1112,axiom,
( select(sF51,X0) = select(sF52,X0)
| i12 = X0 ) ).
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(u619,hypothesis,
i22 != i5 ).
cnf(u1006,axiom,
e6 = select(sF5,i6) ).
cnf(u775,hypothesis,
i22 != i2 ).
cnf(u111,hypothesis,
i21 != i20 ).
cnf(u233,hypothesis,
i20 != i15 ).
cnf(u1012,axiom,
e12 = select(sF11,i12) ).
cnf(u379,hypothesis,
i13 != i11 ).
cnf(u657,hypothesis,
i28 != i4 ).
cnf(u749,hypothesis,
i8 != i3 ).
cnf(u1017,axiom,
e17 = select(sF16,i17) ).
cnf(u1035,axiom,
e30 = select(sF35,i30) ).
cnf(u747,hypothesis,
i9 != i3 ).
cnf(u1024,axiom,
e24 = select(sF23,i24) ).
cnf(u239,hypothesis,
i17 != i15 ).
cnf(u2026,axiom,
sF61 = select(sF21,sF60) ).
cnf(u377,hypothesis,
i14 != i11 ).
cnf(u3332,hypothesis,
e10 != select(sF31,sF60) ).
cnf(u507,hypothesis,
i9 != i8 ).
cnf(u533,hypothesis,
i18 != i7 ).
cnf(u531,hypothesis,
i19 != i7 ).
cnf(u3336,hypothesis,
e3 != select(sF31,sF60) ).
cnf(u23,hypothesis,
i30 != i25 ).
cnf(u1000,axiom,
e1 = select(sF0,i1) ).
cnf(u1060,axiom,
( select(a1,X0) = select(sF0,X0)
| i1 = X0 ) ).
cnf(u3314,hypothesis,
e30 = select(sF35,sF60) ).
cnf(u505,hypothesis,
i10 != i8 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV502-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.20 % Computer : n013.cluster.edu
% 0.06/0.20 % Model : x86_64 x86_64
% 0.06/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.20 % Memory : 8046.5625MB
% 0.06/0.20 % OS : Linux 6.8.0-71-generic
% 0.06/0.20 % CPULimit : 300
% 0.06/0.21 % WCLimit : 300
% 0.06/0.21 % DateTime : Mon Sep 28 11:21:07 UTC 2026
% 0.06/0.21 % CPUTime :
% 0.06/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.24 Running first-order model finding
% 0.06/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.42/0.53 % (1110151)Will run a generic schedule for satisfiability detection.
% 1.42/0.53 % (1110162)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3018128560:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.42/0.53 % (1110157)% WARNING: option uhcvi not known.
% 1.42/0.53 % (1110156)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3400711080_2999 on theBenchmark for (2999ds/0Mi)
% 1.42/0.53 % (1110158)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3027883080:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.42/0.53 % (1110157)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3857492723:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.42/0.53 % (1110159)dis+10_1_sil=32000:sp=arity:random_seed=1191225940:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.42/0.53 % (1110160)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=979554514:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.42/0.53 % (1110161)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=118538296:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.42/0.53 % Detected minimum model sizes of [30]
% 1.42/0.53 % Detected maximum model sizes of [max]
% 1.42/0.53 % TRYING [30]
% 1.42/0.53 % (1110162)Instruction limit reached!
% 1.42/0.53 % (1110162)------------------------------
% 1.42/0.53 % (1110162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110162)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110162)Termination reason: Instruction limit
% 1.42/0.53 % (1110162)Termination phase: Saturation
% 1.42/0.53 % (1110162)Time elapsed: 0.039 s
% 1.42/0.53 % (1110162)Peak memory usage: 13 MB
% 1.42/0.53 % (1110162)Instructions burned: 159 (million)
% 1.42/0.53 % (1110170)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1671907843:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.42/0.53 % Detected minimum model sizes of [30]
% 1.42/0.53 % Detected maximum model sizes of [max]
% 1.42/0.53 % TRYING [30]
% 1.42/0.53 % (1110159)Instruction limit reached!
% 1.42/0.53 % (1110159)------------------------------
% 1.42/0.53 % (1110159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110159)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110159)Termination reason: Instruction limit
% 1.42/0.53 % (1110159)Termination phase: Saturation
% 1.42/0.53 % (1110159)Time elapsed: 0.047 s
% 1.42/0.53 % (1110159)Peak memory usage: 12 MB
% 1.42/0.53 % (1110159)Instructions burned: 104 (million)
% 1.42/0.53 % (1110160)Instruction limit reached!
% 1.42/0.53 % (1110160)------------------------------
% 1.42/0.53 % (1110160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110160)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110160)Termination reason: Instruction limit
% 1.42/0.53 % (1110160)Termination phase: Saturation
% 1.42/0.53 % (1110160)Time elapsed: 0.052 s
% 1.42/0.53 % (1110160)Peak memory usage: 12 MB
% 1.42/0.53 % (1110160)Instructions burned: 116 (million)
% 1.42/0.53 % (1110161)Instruction limit reached!
% 1.42/0.53 % (1110161)------------------------------
% 1.42/0.53 % (1110161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110161)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110161)Termination reason: Instruction limit
% 1.42/0.53 % (1110161)Termination phase: Saturation
% 1.42/0.53 % (1110161)Time elapsed: 0.054 s
% 1.42/0.53 % (1110161)Peak memory usage: 12 MB
% 1.42/0.53 % (1110161)Instructions burned: 132 (million)
% 1.42/0.53 % (1110172)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3082658099:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.42/0.53 % (1110173)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=86859752:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.42/0.53 % (1110174)ott-21_1_sil=16000:fs=off:random_seed=1662598092:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.42/0.53 % (1110172)Instruction limit reached!
% 1.42/0.53 % (1110172)------------------------------
% 1.42/0.53 % (1110172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110172)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110172)Termination reason: Instruction limit
% 1.42/0.53 % (1110172)Termination phase: Saturation
% 1.42/0.53 % (1110172)Time elapsed: 0.059 s
% 1.42/0.53 % (1110172)Peak memory usage: 13 MB
% 1.42/0.53 % (1110172)Instructions burned: 133 (million)
% 1.42/0.53 % (1110174)Instruction limit reached!
% 1.42/0.53 % (1110174)------------------------------
% 1.42/0.53 % (1110174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110174)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110174)Termination reason: Instruction limit
% 1.42/0.53 % (1110174)Termination phase: Saturation
% 1.42/0.53 % (1110174)Time elapsed: 0.070 s
% 1.42/0.53 % (1110174)Peak memory usage: 11 MB
% 1.42/0.53 % (1110174)Instructions burned: 182 (million)
% 1.42/0.53 % (1110178)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3619567680:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.42/0.53 % (1110179)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3356957427:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.42/0.53 % Detected minimum model sizes of [30]
% 1.42/0.53 % Detected maximum model sizes of [max]
% 1.42/0.53 % (1110170)Instruction limit reached!
% 1.42/0.53 % (1110170)------------------------------
% 1.42/0.53 % (1110170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110170)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110170)Termination reason: Instruction limit
% 1.42/0.53 % (1110170)Termination phase: Finite model building constraint generation
% 1.42/0.53 % (1110170)Time elapsed: 0.134 s
% 1.42/0.53 % (1110170)Peak memory usage: 59 MB
% 1.42/0.53 % (1110170)Instructions burned: 715 (million)
% 1.42/0.53 % (1110182)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3444938975:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.42/0.53 % (1110182) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1110151-1110182"...
% 1.42/0.53 % (1110182)...printing done.
% 1.42/0.53 % SZS status Satisfiable for theBenchmark
% 1.42/0.53 % SZS output start Saturation.
% See solution above
% 1.42/0.53 % SZS output start Definitions and Model Updates.
% 1.42/0.53 % SZS output end Definitions and Model Updates.
% 1.42/0.53 % (1110182)------------------------------
% 1.42/0.53 % (1110182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.42/0.53 % (1110182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.42/0.53 % (1110182)CaDiCaL version: 2.1.3
% 1.42/0.53 % (1110182)Termination reason: Satisfiable
% 1.42/0.53 % (1110182)Time elapsed: 0.038 s
% 1.42/0.53 % (1110182)Peak memory usage: 13 MB
% 1.42/0.53 % (1110182)Instructions burned: 128 (million)
% 1.42/0.53 % (1110151)Success in time 0.284 s
% 1.42/0.53 % Vampire exiting
%------------------------------------------------------------------------------