%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV493-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 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:02 PM UTC 2026
% Result : Satisfiable 3.21s 1.05s
% Output : Saturation 3.57s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u549,hypothesis,
i10 != i7 ).
cnf(u421,hypothesis,
i11 != i10 ).
cnf(u379,hypothesis,
i13 != i11 ).
cnf(u723,hypothesis,
i21 != i3 ).
cnf(u377,hypothesis,
i14 != i11 ).
cnf(u177,hypothesis,
i21 != i17 ).
cnf(u701,hypothesis,
i6 != i4 ).
cnf(u779,hypothesis,
i20 != i2 ).
cnf(u63,hypothesis,
i28 != i22 ).
cnf(u371,hypothesis,
i17 != i11 ).
cnf(u853,hypothesis,
i11 != i1 ).
cnf(u91,hypothesis,
i22 != i21 ).
cnf(u373,hypothesis,
i16 != i11 ).
cnf(u627,hypothesis,
i18 != i5 ).
cnf(u681,hypothesis,
i16 != i4 ).
cnf(u507,hypothesis,
i9 != i8 ).
cnf(u525,hypothesis,
i22 != i7 ).
cnf(u695,hypothesis,
i9 != i4 ).
cnf(u833,hypothesis,
i21 != i1 ).
cnf(u509,hypothesis,
i30 != i7 ).
cnf(u805,hypothesis,
i7 != i2 ).
cnf(u751,hypothesis,
i7 != i3 ).
cnf(u565,hypothesis,
i25 != i6 ).
cnf(u843,hypothesis,
i16 != i1 ).
cnf(u579,hypothesis,
i18 != i6 ).
cnf(u777,hypothesis,
i21 != i2 ).
cnf(u633,hypothesis,
i15 != i5 ).
cnf(u503,hypothesis,
i11 != i8 ).
cnf(u785,hypothesis,
i17 != i2 ).
cnf(u731,hypothesis,
i17 != i3 ).
cnf(u73,hypothesis,
i23 != i22 ).
cnf(u703,hypothesis,
i5 != i4 ).
cnf(u531,hypothesis,
i19 != i7 ).
cnf(u693,hypothesis,
i10 != i4 ).
cnf(u855,hypothesis,
i10 != i1 ).
cnf(u781,hypothesis,
i19 != i2 ).
cnf(u139,hypothesis,
i28 != i18 ).
cnf(u271,hypothesis,
i16 != i14 ).
cnf(u213,hypothesis,
i30 != i15 ).
cnf(u683,hypothesis,
i15 != i4 ).
cnf(u141,hypothesis,
i27 != i18 ).
cnf(u43,hypothesis,
i25 != i24 ).
cnf(u449,hypothesis,
i17 != i9 ).
cnf(u527,hypothesis,
i21 != i7 ).
cnf(u835,hypothesis,
i20 != i1 ).
cnf(u707,hypothesis,
i29 != i3 ).
cnf(u807,hypothesis,
i6 != i2 ).
cnf(u439,hypothesis,
i22 != i9 ).
cnf(u679,hypothesis,
i17 != i4 ).
cnf(u259,hypothesis,
i22 != i14 ).
cnf(u415,hypothesis,
i14 != i10 ).
cnf(u859,hypothesis,
i8 != i1 ).
cnf(u195,hypothesis,
i25 != i16 ).
cnf(u635,hypothesis,
i14 != i5 ).
cnf(u313,hypothesis,
i28 != i12 ).
cnf(u93,hypothesis,
i30 != i20 ).
cnf(u401,hypothesis,
i21 != i10 ).
cnf(goal,negated_conjecture,
store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i30,e30) != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i13,e13),i1,e1),i19,e19),i4,e4),i9,e9),i30,e30),i2,e2),i15,e15),i25,e25),i18,e18),i20,e20),i8,e8),i21,e21),i6,e6),i11,e11),i14,e14),i29,e29),i5,e5),i26,e26),i22,e22),i27,e27),i3,e3),i12,e12),i16,e16),i28,e28),i17,e17),i23,e23),i24,e24),i7,e7),i10,e10) ).
cnf(u725,hypothesis,
i20 != i3 ).
cnf(u49,hypothesis,
i28 != i23 ).
cnf(u87,hypothesis,
i24 != i21 ).
cnf(u395,hypothesis,
i24 != i10 ).
cnf(u631,hypothesis,
i16 != i5 ).
cnf(u367,hypothesis,
i19 != i11 ).
cnf(u385,hypothesis,
i29 != i10 ).
cnf(u25,hypothesis,
i29 != i25 ).
cnf(u397,hypothesis,
i23 != i10 ).
cnf(u705,hypothesis,
i30 != i3 ).
cnf(u45,hypothesis,
i30 != i23 ).
cnf(u547,hypothesis,
i11 != i7 ).
cnf(u67,hypothesis,
i26 != i22 ).
cnf(u225,hypothesis,
i24 != i15 ).
cnf(u39,hypothesis,
i27 != i24 ).
cnf(u857,hypothesis,
i9 != i1 ).
cnf(u69,hypothesis,
i25 != i22 ).
cnf(u219,hypothesis,
i27 != i15 ).
cnf(u677,hypothesis,
i18 != i4 ).
cnf(u319,hypothesis,
i25 != i12 ).
cnf(u435,hypothesis,
i24 != i9 ).
cnf(u349,hypothesis,
i28 != i11 ).
cnf(u185,hypothesis,
i30 != i16 ).
cnf(u153,hypothesis,
i21 != i18 ).
cnf(u19,hypothesis,
i28 != i26 ).
cnf(u629,hypothesis,
i17 != i5 ).
cnf(u501,hypothesis,
i12 != i8 ).
cnf(u21,hypothesis,
i27 != i26 ).
cnf(u811,hypothesis,
i4 != i2 ).
cnf(u329,hypothesis,
i20 != i12 ).
cnf(u147,hypothesis,
i24 != i18 ).
cnf(u495,hypothesis,
i15 != i8 ).
cnf(u829,hypothesis,
i23 != i1 ).
cnf(u15,hypothesis,
i30 != i26 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u323,hypothesis,
i23 != i12 ).
cnf(u123,hypothesis,
i25 != i19 ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u295,hypothesis,
i20 != i13 ).
cnf(u325,hypothesis,
i22 != i12 ).
cnf(u761,hypothesis,
i29 != i2 ).
cnf(u537,hypothesis,
i16 != i7 ).
cnf(u143,hypothesis,
i26 != i18 ).
cnf(u281,hypothesis,
i27 != i13 ).
cnf(u605,hypothesis,
i29 != i5 ).
cnf(u175,hypothesis,
i22 != i17 ).
cnf(u753,hypothesis,
i6 != i3 ).
cnf(u561,hypothesis,
i27 != i6 ).
cnf(u331,hypothesis,
i19 != i12 ).
cnf(u809,hypothesis,
i5 != i2 ).
cnf(u251,hypothesis,
i26 != i14 ).
cnf(u519,hypothesis,
i25 != i7 ).
cnf(u277,hypothesis,
i29 != i13 ).
cnf(u659,hypothesis,
i27 != i4 ).
cnf(u129,hypothesis,
i22 != i19 ).
cnf(u585,hypothesis,
i15 != i6 ).
cnf(u557,hypothesis,
i29 != i6 ).
cnf(u749,hypothesis,
i8 != i3 ).
cnf(u309,hypothesis,
i30 != i12 ).
cnf(u327,hypothesis,
i21 != i12 ).
cnf(u655,hypothesis,
i29 != i4 ).
cnf(u611,hypothesis,
i26 != i5 ).
cnf(u303,hypothesis,
i16 != i13 ).
cnf(u517,hypothesis,
i26 != i7 ).
cnf(u647,hypothesis,
i8 != i5 ).
cnf(u861,hypothesis,
i7 != i1 ).
cnf(u817,hypothesis,
i29 != i1 ).
cnf(u763,hypothesis,
i28 != i2 ).
cnf(u221,hypothesis,
i26 != i15 ).
cnf(u233,hypothesis,
i20 != i15 ).
cnf(u607,hypothesis,
i28 != i5 ).
cnf(u755,hypothesis,
i5 != i3 ).
cnf(u95,hypothesis,
i29 != i20 ).
cnf(u215,hypothesis,
i29 != i15 ).
cnf(u563,hypothesis,
i26 != i6 ).
cnf(u813,hypothesis,
i3 != i2 ).
cnf(u171,hypothesis,
i24 != i17 ).
cnf(u431,hypothesis,
i26 != i9 ).
cnf(u201,hypothesis,
i22 != i16 ).
cnf(u587,hypothesis,
i14 != i6 ).
cnf(u283,hypothesis,
i26 != i13 ).
cnf(u173,hypothesis,
i23 != i17 ).
cnf(u299,hypothesis,
i18 != i13 ).
cnf(u559,hypothesis,
i28 != i6 ).
cnf(u81,hypothesis,
i27 != i21 ).
cnf(u285,hypothesis,
i25 != i13 ).
cnf(u167,hypothesis,
i26 != i17 ).
cnf(u197,hypothesis,
i24 != i16 ).
cnf(u417,hypothesis,
i13 != i10 ).
cnf(u583,hypothesis,
i16 != i6 ).
cnf(u447,hypothesis,
i18 != i9 ).
cnf(u477,hypothesis,
i24 != i8 ).
cnf(u539,hypothesis,
i15 != i7 ).
cnf(u125,hypothesis,
i24 != i19 ).
cnf(u433,hypothesis,
i25 != i9 ).
cnf(u471,hypothesis,
i27 != i8 ).
cnf(u819,hypothesis,
i28 != i1 ).
cnf(u765,hypothesis,
i27 != i2 ).
cnf(u119,hypothesis,
i27 != i19 ).
cnf(u209,hypothesis,
i18 != i16 ).
cnf(u149,hypothesis,
i23 != i18 ).
cnf(u457,hypothesis,
i13 != i9 ).
cnf(u535,hypothesis,
i17 != i7 ).
cnf(u105,hypothesis,
i24 != i20 ).
cnf(u429,hypothesis,
i27 != i9 ).
cnf(u451,hypothesis,
i16 != i9 ).
cnf(u815,hypothesis,
i30 != i1 ).
cnf(u407,hypothesis,
i18 != i10 ).
cnf(u99,hypothesis,
i27 != i20 ).
cnf(u581,hypothesis,
i17 != i6 ).
cnf(u453,hypothesis,
i15 != i9 ).
cnf(u179,hypothesis,
i20 != i17 ).
cnf(u101,hypothesis,
i26 != i20 ).
cnf(u727,hypothesis,
i19 != i3 ).
cnf(u409,hypothesis,
i17 != i10 ).
cnf(u733,hypothesis,
i16 != i3 ).
cnf(u57,hypothesis,
i24 != i23 ).
cnf(u381,hypothesis,
i12 != i11 ).
cnf(u403,hypothesis,
i20 != i10 ).
cnf(u51,hypothesis,
i27 != i23 ).
cnf(u375,hypothesis,
i15 != i11 ).
cnf(u405,hypothesis,
i19 != i10 ).
cnf(u369,hypothesis,
i18 != i11 ).
cnf(u713,hypothesis,
i26 != i3 ).
cnf(u53,hypothesis,
i26 != i23 ).
cnf(u387,hypothesis,
i28 != i10 ).
cnf(u361,hypothesis,
i22 != i11 ).
cnf(u865,hypothesis,
i5 != i1 ).
cnf(u685,hypothesis,
i14 != i4 ).
cnf(u513,hypothesis,
i28 != i7 ).
cnf(u47,hypothesis,
i29 != i23 ).
cnf(u355,hypothesis,
i25 != i11 ).
cnf(u837,hypothesis,
i19 != i1 ).
cnf(u365,hypothesis,
i20 != i11 ).
cnf(u357,hypothesis,
i24 != i11 ).
cnf(u739,hypothesis,
i13 != i3 ).
cnf(u665,hypothesis,
i24 != i4 ).
cnf(u577,hypothesis,
i19 != i6 ).
cnf(u497,hypothesis,
i14 != i8 ).
cnf(u637,hypothesis,
i13 != i5 ).
cnf(u75,hypothesis,
i30 != i21 ).
cnf(u359,hypothesis,
i23 != i11 ).
cnf(u553,hypothesis,
i8 != i7 ).
cnf(u307,hypothesis,
i14 != i13 ).
cnf(u789,hypothesis,
i15 != i2 ).
cnf(u77,hypothesis,
i29 != i21 ).
cnf(u691,hypothesis,
i11 != i4 ).
cnf(u617,hypothesis,
i23 != i5 ).
cnf(u493,hypothesis,
i16 != i8 ).
cnf(u353,hypothesis,
i26 != i11 ).
cnf(u715,hypothesis,
i25 != i3 ).
cnf(u867,hypothesis,
i4 != i1 ).
cnf(u487,hypothesis,
i19 != i8 ).
cnf(u687,hypothesis,
i13 != i4 ).
cnf(u339,hypothesis,
i15 != i12 ).
cnf(u515,hypothesis,
i27 != i7 ).
cnf(u839,hypothesis,
i18 != i1 ).
cnf(u711,hypothesis,
i27 != i3 ).
cnf(u315,hypothesis,
i27 != i12 ).
cnf(u667,hypothesis,
i23 != i4 ).
cnf(u253,hypothesis,
i25 != i14 ).
cnf(u113,hypothesis,
i30 != i19 ).
cnf(u317,hypothesis,
i26 != i12 ).
cnf(u639,hypothesis,
i12 != i5 ).
cnf(u529,hypothesis,
i20 != i7 ).
cnf(u247,hypothesis,
i28 != i14 ).
cnf(u791,hypothesis,
i14 != i2 ).
cnf(u663,hypothesis,
i25 != i4 ).
cnf(u311,hypothesis,
i29 != i12 ).
cnf(u343,hypothesis,
i13 != i12 ).
cnf(u399,hypothesis,
i22 != i10 ).
cnf(u619,hypothesis,
i22 != i5 ).
cnf(u443,hypothesis,
i20 != i9 ).
cnf(u227,hypothesis,
i23 != i15 ).
cnf(u709,hypothesis,
i28 != i3 ).
cnf(u33,hypothesis,
i30 != i24 ).
cnf(u445,hypothesis,
i19 != i9 ).
cnf(u71,hypothesis,
i24 != i22 ).
cnf(u229,hypothesis,
i22 != i15 ).
cnf(u657,hypothesis,
i28 != i4 ).
cnf(u27,hypothesis,
i28 != i25 ).
cnf(u351,hypothesis,
i27 != i11 ).
cnf(u223,hypothesis,
i25 != i15 ).
cnf(u571,hypothesis,
i22 != i6 ).
cnf(u29,hypothesis,
i27 != i25 ).
cnf(u337,hypothesis,
i16 != i12 ).
cnf(u661,hypothesis,
i26 != i4 ).
cnf(u23,hypothesis,
i30 != i25 ).
cnf(u653,hypothesis,
i30 != i4 ).
cnf(u181,hypothesis,
i19 != i17 ).
cnf(u203,hypothesis,
i21 != i16 ).
cnf(u567,hypothesis,
i24 != i6 ).
cnf(u9,hypothesis,
i30 != i27 ).
cnf(u333,hypothesis,
i18 != i12 ).
cnf(u641,hypothesis,
i11 != i5 ).
cnf(hyp0,hypothesis,
i29 != i30 ).
cnf(u841,hypothesis,
i17 != i1 ).
cnf(u289,hypothesis,
i23 != i13 ).
cnf(u729,hypothesis,
i18 != i3 ).
cnf(u161,hypothesis,
i29 != i17 ).
cnf(u5,hypothesis,
i30 != i28 ).
cnf(u485,hypothesis,
i20 != i8 ).
cnf(u569,hypothesis,
i23 != i6 ).
cnf(u441,hypothesis,
i21 != i9 ).
cnf(u787,hypothesis,
i16 != i2 ).
cnf(u479,hypothesis,
i23 != i8 ).
cnf(u827,hypothesis,
i24 != i1 ).
cnf(u127,hypothesis,
i23 != i19 ).
cnf(u593,hypothesis,
i11 != i6 ).
cnf(u757,hypothesis,
i4 != i3 ).
cnf(u795,hypothesis,
i12 != i2 ).
cnf(u489,hypothesis,
i18 != i8 ).
cnf(u279,hypothesis,
i28 != i13 ).
cnf(u609,hypothesis,
i27 != i5 ).
cnf(u437,hypothesis,
i23 != i9 ).
cnf(u745,hypothesis,
i10 != i3 ).
cnf(u133,hypothesis,
i20 != i19 ).
cnf(u265,hypothesis,
i19 != i14 ).
cnf(u589,hypothesis,
i13 != i6 ).
cnf(u109,hypothesis,
i22 != i20 ).
cnf(u545,hypothesis,
i12 != i7 ).
cnf(u483,hypothesis,
i21 != i8 ).
cnf(u869,hypothesis,
i3 != i1 ).
cnf(u321,hypothesis,
i24 != i12 ).
cnf(u249,hypothesis,
i27 != i14 ).
cnf(u261,hypothesis,
i21 != i14 ).
cnf(u643,hypothesis,
i10 != i5 ).
cnf(u697,hypothesis,
i8 != i4 ).
cnf(u737,hypothesis,
i14 != i3 ).
cnf(u541,hypothesis,
i14 != i7 ).
cnf(u863,hypothesis,
i6 != i1 ).
cnf(u793,hypothesis,
i13 != i2 ).
cnf(u821,hypothesis,
i27 != i1 ).
cnf(u767,hypothesis,
i26 != i2 ).
cnf(u595,hypothesis,
i10 != i6 ).
cnf(u521,hypothesis,
i24 != i7 ).
cnf(u845,hypothesis,
i15 != i1 ).
cnf(u231,hypothesis,
i21 != i15 ).
cnf(u505,hypothesis,
i10 != i8 ).
cnf(u801,hypothesis,
i9 != i2 ).
cnf(u747,hypothesis,
i9 != i3 ).
cnf(u205,hypothesis,
i20 != i16 ).
cnf(u287,hypothesis,
i24 != i13 ).
cnf(u591,hypothesis,
i12 != i6 ).
cnf(u85,hypothesis,
i25 != i21 ).
cnf(u199,hypothesis,
i23 != i16 ).
cnf(u499,hypothesis,
i13 != i8 ).
cnf(u871,hypothesis,
i2 != i1 ).
cnf(u797,hypothesis,
i11 != i2 ).
cnf(u155,hypothesis,
i20 != i18 ).
cnf(u699,hypothesis,
i7 != i4 ).
cnf(u157,hypothesis,
i19 != i18 ).
cnf(u465,hypothesis,
i30 != i8 ).
cnf(u543,hypothesis,
i13 != i7 ).
cnf(u769,hypothesis,
i25 != i2 ).
cnf(u423,hypothesis,
i30 != i9 ).
cnf(u689,hypothesis,
i12 != i4 ).
cnf(u151,hypothesis,
i22 != i18 ).
cnf(u459,hypothesis,
i12 != i9 ).
cnf(u823,hypothesis,
i26 != i1 ).
cnf(u267,hypothesis,
i18 != i14 ).
cnf(u107,hypothesis,
i23 != i20 ).
cnf(u137,hypothesis,
i29 != i18 ).
cnf(u735,hypothesis,
i15 != i3 ).
cnf(u461,hypothesis,
i11 != i9 ).
cnf(u523,hypothesis,
i23 != i7 ).
cnf(u615,hypothesis,
i24 != i5 ).
cnf(u413,hypothesis,
i15 != i10 ).
cnf(u131,hypothesis,
i21 != i19 ).
cnf(u455,hypothesis,
i14 != i9 ).
cnf(u803,hypothesis,
i8 != i2 ).
cnf(u103,hypothesis,
i25 != i20 ).
cnf(u263,hypothesis,
i20 != i14 ).
cnf(u411,hypothesis,
i16 != i10 ).
cnf(u59,hypothesis,
i30 != i22 ).
cnf(u89,hypothesis,
i23 != i21 ).
cnf(u255,hypothesis,
i24 != i14 ).
cnf(u721,hypothesis,
i22 != i3 ).
cnf(u61,hypothesis,
i29 != i22 ).
cnf(u193,hypothesis,
i26 != i16 ).
cnf(u83,hypothesis,
i26 != i21 ).
cnf(u241,hypothesis,
i16 != i15 ).
cnf(u55,hypothesis,
i25 != i23 ).
cnf(u169,hypothesis,
i25 != i17 ).
cnf(u363,hypothesis,
i21 != i11 ).
cnf(u771,hypothesis,
i24 != i2 ).
cnf(u393,hypothesis,
i25 != i10 ).
cnf(u391,hypothesis,
i26 != i10 ).
cnf(u717,hypothesis,
i24 != i3 ).
cnf(u41,hypothesis,
i26 != i24 ).
cnf(u79,hypothesis,
i28 != i21 ).
cnf(u673,hypothesis,
i20 != i4 ).
cnf(u743,hypothesis,
i11 != i3 ).
cnf(u35,hypothesis,
i29 != i24 ).
cnf(u65,hypothesis,
i27 != i22 ).
cnf(u389,hypothesis,
i27 != i10 ).
cnf(u37,hypothesis,
i28 != i24 ).
cnf(u345,hypothesis,
i30 != i11 ).
cnf(u669,hypothesis,
i22 != i4 ).
cnf(u31,hypothesis,
i26 != i25 ).
cnf(u625,hypothesis,
i19 != i5 ).
cnf(u97,hypothesis,
i28 != i20 ).
cnf(u759,hypothesis,
i30 != i2 ).
cnf(u17,hypothesis,
i29 != i26 ).
cnf(u341,hypothesis,
i14 != i12 ).
cnf(u649,hypothesis,
i7 != i5 ).
cnf(u347,hypothesis,
i29 != i11 ).
cnf(u297,hypothesis,
i19 != i13 ).
cnf(u825,hypothesis,
i25 != i1 ).
cnf(u621,hypothesis,
i21 != i5 ).
cnf(u145,hypothesis,
i25 != i18 ).
cnf(u741,hypothesis,
i12 != i3 ).
cnf(u291,hypothesis,
i22 != i13 ).
cnf(u773,hypothesis,
i23 != i2 ).
cnf(u719,hypothesis,
i23 != i3 ).
cnf(u481,hypothesis,
i22 != i8 ).
cnf(u121,hypothesis,
i26 != i19 ).
cnf(u135,hypothesis,
i30 != i18 ).
cnf(u293,hypothesis,
i21 != i13 ).
cnf(u675,hypothesis,
i19 != i4 ).
cnf(u601,hypothesis,
i7 != i6 ).
cnf(u783,hypothesis,
i18 != i2 ).
cnf(u573,hypothesis,
i21 != i6 ).
cnf(u475,hypothesis,
i25 != i8 ).
cnf(u115,hypothesis,
i29 != i19 ).
cnf(u257,hypothesis,
i23 != i14 ).
cnf(u671,hypothesis,
i21 != i4 ).
cnf(u533,hypothesis,
i18 != i7 ).
cnf(u383,hypothesis,
i30 != i10 ).
cnf(u851,hypothesis,
i12 != i1 ).
cnf(u235,hypothesis,
i19 != i15 ).
cnf(u111,hypothesis,
i21 != i20 ).
cnf(u305,hypothesis,
i15 != i13 ).
cnf(u651,hypothesis,
i6 != i5 ).
cnf(u237,hypothesis,
i18 != i15 ).
cnf(u243,hypothesis,
i30 != i14 ).
cnf(u623,hypothesis,
i20 != i5 ).
cnf(u245,hypothesis,
i29 != i14 ).
cnf(u847,hypothesis,
i14 != i1 ).
cnf(u775,hypothesis,
i22 != i2 ).
cnf(u187,hypothesis,
i29 != i16 ).
cnf(u301,hypothesis,
i17 != i13 ).
cnf(u511,hypothesis,
i29 != i7 ).
cnf(u217,hypothesis,
i28 != i15 ).
cnf(u603,hypothesis,
i30 != i5 ).
cnf(u239,hypothesis,
i17 != i15 ).
cnf(u189,hypothesis,
i28 != i16 ).
cnf(u211,hypothesis,
i17 != i16 ).
cnf(u575,hypothesis,
i20 != i6 ).
cnf(u11,hypothesis,
i29 != i27 ).
cnf(u183,hypothesis,
i18 != i17 ).
cnf(u491,hypothesis,
i17 != i8 ).
cnf(u427,hypothesis,
i28 != i9 ).
cnf(u599,hypothesis,
i8 != i6 ).
cnf(u335,hypothesis,
i17 != i12 ).
cnf(u207,hypothesis,
i19 != i16 ).
cnf(u555,hypothesis,
i30 != i6 ).
cnf(u13,hypothesis,
i28 != i27 ).
cnf(u163,hypothesis,
i28 != i17 ).
cnf(u645,hypothesis,
i9 != i5 ).
cnf(u7,hypothesis,
i29 != i28 ).
cnf(u165,hypothesis,
i27 != i17 ).
cnf(u473,hypothesis,
i26 != i8 ).
cnf(u551,hypothesis,
i9 != i7 ).
cnf(u275,hypothesis,
i30 != i13 ).
cnf(u159,hypothesis,
i30 != i17 ).
cnf(u467,hypothesis,
i29 != i8 ).
cnf(u831,hypothesis,
i22 != i1 ).
cnf(u273,hypothesis,
i15 != i14 ).
cnf(u597,hypothesis,
i9 != i6 ).
cnf(u799,hypothesis,
i10 != i2 ).
cnf(u469,hypothesis,
i28 != i8 ).
cnf(u613,hypothesis,
i25 != i5 ).
cnf(u117,hypothesis,
i28 != i19 ).
cnf(u425,hypothesis,
i29 != i9 ).
cnf(u849,hypothesis,
i13 != i1 ).
cnf(u463,hypothesis,
i10 != i9 ).
cnf(u191,hypothesis,
i27 != i16 ).
cnf(u269,hypothesis,
i17 != i14 ).
cnf(u419,hypothesis,
i12 != i10 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV493-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n002.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 11:18:07 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 Running first-order theorem proving
% 0.08/0.19 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.21/1.05 % (292807)Input is clausal, will run a generic CNF schedule.
% 3.21/1.05 % (292813)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2151392904:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.21/1.05 % (292812)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=2971825165:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.21/1.05 % (292817)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1190844907:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.21/1.05 % (292814)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3803610139:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.21/1.05 % (292816)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1257236207:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.21/1.05 % (292818)dis-21_1_sil=8000:lcm=predicate:random_seed=3543684894:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.21/1.05 % (292815)lrs+10_1_sil=8000:sp=occurrence:random_seed=1720582133:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.21/1.05 % (292815)First to succeed.
% 3.21/1.05 % (292816)Refutation not found, incomplete strategy
% 3.21/1.05 % (292816)------------------------------
% 3.21/1.05 % (292816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.05 % (292817)Refutation not found, incomplete strategy
% 3.21/1.05 % (292817)------------------------------
% 3.21/1.05 % (292817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.05 % (292816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.05 % (292817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.05 % (292817)CaDiCaL version: 2.1.3
% 3.21/1.05 % (292816)CaDiCaL version: 2.1.3
% 3.21/1.05 % (292816)Termination reason: Refutation not found, incomplete strategy
% 3.21/1.05 % (292816)Time elapsed: 0.008 s
% 3.21/1.05 % (292816)Peak memory usage: 88 MB
% 3.21/1.05 % (292817)Termination reason: Refutation not found, incomplete strategy
% 3.21/1.05 % (292817)Time elapsed: 0.008 s
% 3.21/1.05 % (292816)Instructions burned: 15 (million)
% 3.21/1.05 % (292817)Peak memory usage: 88 MB
% 3.21/1.05 % (292817)Instructions burned: 16 (million)
% 3.21/1.05 % (292815)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-292807"
% 3.21/1.05 % (292818)Refutation not found, incomplete strategy
% 3.21/1.05 % (292818)------------------------------
% 3.21/1.05 % (292818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.05 % (292818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.05 % (292818)CaDiCaL version: 2.1.3
% 3.21/1.05 % (292818)Termination reason: Refutation not found, incomplete strategy
% 3.21/1.05 % (292818)Time elapsed: 0.012 s
% 3.21/1.05 % (292818)Peak memory usage: 88 MB
% 3.21/1.05 % (292818)Instructions burned: 22 (million)
% 3.21/1.05 % (292817)------------------------------
% 3.21/1.05 % (292817)------------------------------
% 3.21/1.05 % (292816)------------------------------
% 3.21/1.05 % (292816)------------------------------
% 3.21/1.05 % (292818)------------------------------
% 3.21/1.05 % (292818)------------------------------
% 3.21/1.05 % SZS status Satisfiable for theBenchmark
% 3.21/1.05 % SZS output start Saturation.
% See solution above
% 3.57/1.25 % SZS output start Definitions and Model Updates.
% 3.57/1.25 % SZS output end Definitions and Model Updates.
% 3.57/1.25 % (292815)------------------------------
% 3.57/1.25 % (292815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.57/1.25 % (292815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/1.25 % (292815)CaDiCaL version: 2.1.3
% 3.57/1.25 % (292815)Termination reason: Satisfiable
% 3.57/1.25 % (292815)Time elapsed: 0.010 s
% 3.57/1.25 % (292815)Peak memory usage: 88 MB
% 3.57/1.25 % (292815)Instructions burned: 17 (million)
% 3.57/1.25 % (292815)------------------------------
% 3.57/1.25 % (292815)------------------------------
% 3.57/1.25 % (292807)Success in time 0.421 s
% 3.57/1.25 % Vampire exiting
%------------------------------------------------------------------------------