%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV498-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 : n011.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:05 PM UTC 2026
% Result : Satisfiable 3.79s 1.50s
% Output : Saturation 3.79s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(hyp95,hypothesis,
i22 != i23 ).
cnf(hyp94,hypothesis,
i22 != i24 ).
cnf(hyp157,hypothesis,
i16 != i24 ).
cnf(hyp418,hypothesis,
i3 != i23 ).
cnf(hyp376,hypothesis,
i5 != i14 ).
cnf(u927,hypothesis,
a_1067 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)) ).
cnf(hyp374,hypothesis,
i5 != i16 ).
cnf(u609,hypothesis,
e13 = select(a_1030,i13) ).
cnf(hyp378,hypothesis,
i5 != i12 ).
cnf(hyp97,hypothesis,
i21 != i29 ).
cnf(u996,hypothesis,
( select(a_1020,X0) = select(a_1021,X0)
| i4 = X0 ) ).
cnf(hyp60,hypothesis,
i29 != i30 ).
cnf(hyp368,hypothesis,
i5 != i22 ).
cnf(hyp67,hypothesis,
i26 != i29 ).
cnf(hyp88,hypothesis,
i22 != i30 ).
cnf(u682,hypothesis,
a_1020 = store(a_1019,i3,select(a_1020,i3)) ).
cnf(hyp370,hypothesis,
i5 != i20 ).
cnf(u681,hypothesis,
a_1021 = store(a_1020,i4,select(a_1021,i4)) ).
cnf(hyp331,hypothesis,
i7 != i12 ).
cnf(u1005,hypothesis,
( select(a_1029,X0) = select(a_1030,X0)
| i13 = X0 ) ).
cnf(u1009,hypothesis,
( select(a_1033,X0) = select(a_1034,X0)
| i17 = X0 ) ).
cnf(hyp450,hypothesis,
i2 != i18 ).
cnf(hyp463,hypothesis,
i2 != i5 ).
cnf(u873,hypothesis,
a_1063 = store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)) ).
cnf(hyp465,hypothesis,
i2 != i3 ).
cnf(u938,hypothesis,
a_1068 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)) ).
cnf(hyp29,hypothesis,
a_1047 = store(a_1046,i1,e1) ).
cnf(hyp459,hypothesis,
i2 != i9 ).
cnf(hyp435,hypothesis,
i3 != i6 ).
cnf(u1011,hypothesis,
( select(a_1035,X0) = select(a_1036,X0)
| i19 = X0 ) ).
cnf(hyp333,hypothesis,
i7 != i10 ).
cnf(hyp486,hypothesis,
i1 != i10 ).
cnf(hyp440,hypothesis,
i2 != i28 ).
cnf(u781,hypothesis,
a_1058 = store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)) ).
cnf(hyp136,hypothesis,
i18 != i20 ).
cnf(hyp268,hypothesis,
i10 != i12 ).
cnf(hyp327,hypothesis,
i7 != i16 ).
cnf(hyp442,hypothesis,
i2 != i26 ).
cnf(hyp139,hypothesis,
i17 != i29 ).
cnf(u683,hypothesis,
a_1019 = store(a_1018,i2,select(a_1019,i2)) ).
cnf(hyp66,hypothesis,
i26 != i30 ).
cnf(hyp138,hypothesis,
i17 != i30 ).
cnf(hyp421,hypothesis,
i3 != i20 ).
cnf(hyp329,hypothesis,
i7 != i14 ).
cnf(hyp446,hypothesis,
i2 != i22 ).
cnf(hyp125,hypothesis,
i19 != i20 ).
cnf(u906,hypothesis,
a_1066 = store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)) ).
cnf(hyp285,hypothesis,
i9 != i15 ).
cnf(hyp132,hypothesis,
i18 != i24 ).
cnf(hyp323,hypothesis,
i7 != i20 ).
cnf(u1007,hypothesis,
( select(a_1031,X0) = select(a_1032,X0)
| i15 = X0 ) ).
cnf(hyp247,hypothesis,
i11 != i14 ).
cnf(hyp213,hypothesis,
i12 != i30 ).
cnf(hyp415,hypothesis,
i3 != i26 ).
cnf(hyp279,hypothesis,
i9 != i21 ).
cnf(hyp412,hypothesis,
i3 != i29 ).
cnf(hyp91,hypothesis,
i22 != i27 ).
cnf(hyp396,hypothesis,
i4 != i19 ).
cnf(hyp249,hypothesis,
i11 != i12 ).
cnf(hyp90,hypothesis,
i22 != i28 ).
cnf(hyp281,hypothesis,
i9 != i19 ).
cnf(hyp398,hypothesis,
i4 != i17 ).
cnf(hyp77,hypothesis,
i24 != i28 ).
cnf(hyp243,hypothesis,
i11 != i18 ).
cnf(hyp84,hypothesis,
i23 != i27 ).
cnf(u672,hypothesis,
a_1049 = store(store(a1,i13,select(a_1030,i13)),i1,e1) ).
cnf(hyp275,hypothesis,
i9 != i25 ).
cnf(hyp392,hypothesis,
i4 != i23 ).
cnf(hyp411,hypothesis,
i3 != i30 ).
cnf(hyp71,hypothesis,
i25 != i29 ).
cnf(hyp229,hypothesis,
i12 != i14 ).
cnf(hyp70,hypothesis,
i25 != i30 ).
cnf(hyp261,hypothesis,
i10 != i19 ).
cnf(hyp394,hypothesis,
i4 != i21 ).
cnf(hyp73,hypothesis,
i25 != i27 ).
cnf(hyp223,hypothesis,
i12 != i20 ).
cnf(hyp64,hypothesis,
i27 != i29 ).
cnf(hyp255,hypothesis,
i10 != i25 ).
cnf(hyp222,hypothesis,
i12 != i21 ).
cnf(hyp413,hypothesis,
i3 != i28 ).
cnf(u708,hypothesis,
a_1050 = store(store(store(a1,i13,select(a_1030,i13)),i1,e1),i19,select(a_1036,i19)) ).
cnf(hyp397,hypothesis,
i4 != i18 ).
cnf(u857,hypothesis,
a_1062 = store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)) ).
cnf(hyp344,hypothesis,
i6 != i22 ).
cnf(hyp481,hypothesis,
i1 != i15 ).
cnf(hyp257,hypothesis,
i10 != i23 ).
cnf(hyp216,hypothesis,
i12 != i27 ).
cnf(u614,hypothesis,
e18 = select(a_1035,i18) ).
cnf(hyp181,hypothesis,
i14 != i29 ).
cnf(hyp316,hypothesis,
i7 != i27 ).
cnf(u608,hypothesis,
e12 = select(a_1029,i12) ).
cnf(hyp346,hypothesis,
i6 != i20 ).
cnf(hyp379,hypothesis,
i5 != i11 ).
cnf(hyp182,hypothesis,
i14 != i28 ).
cnf(hyp175,hypothesis,
i15 != i20 ).
cnf(u1018,hypothesis,
( select(a_1042,X0) = select(a_1043,X0)
| i26 = X0 ) ).
cnf(hyp302,hypothesis,
i8 != i19 ).
cnf(u1014,hypothesis,
( select(a_1038,X0) = select(a_1039,X0)
| i22 = X0 ) ).
cnf(hyp174,hypothesis,
i15 != i21 ).
cnf(u948,hypothesis,
a_1069 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)) ).
cnf(hyp177,hypothesis,
i15 != i18 ).
cnf(hyp296,hypothesis,
i8 != i25 ).
cnf(u654,hypothesis,
a_1041 = store(a_1040,i24,select(a_1041,i24)) ).
cnf(hyp326,hypothesis,
i7 != i17 ).
cnf(hyp492,hypothesis,
i1 != i4 ).
cnf(u610,hypothesis,
e14 = select(a_1031,i14) ).
cnf(hyp298,hypothesis,
i8 != i23 ).
cnf(hyp320,hypothesis,
i7 != i23 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(hyp292,hypothesis,
i8 != i29 ).
cnf(u762,hypothesis,
a_1052 = store(store(store(store(store(a1,i13,select(a_1030,i13)),i1,e1),i19,select(a_1036,i19)),i4,select(a_1021,i4)),i9,select(a_1026,i9)) ).
cnf(hyp322,hypothesis,
i7 != i21 ).
cnf(u606,hypothesis,
e10 = select(a_1027,i10) ).
cnf(hyp278,hypothesis,
i9 != i22 ).
cnf(u605,hypothesis,
e9 = select(a_1026,i9) ).
cnf(u952,hypothesis,
a_1070 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)) ).
cnf(hyp172,hypothesis,
i15 != i23 ).
cnf(hyp272,hypothesis,
i9 != i28 ).
cnf(hyp109,hypothesis,
i20 != i26 ).
cnf(u618,hypothesis,
e22 = select(a_1039,i22) ).
cnf(u658,hypothesis,
a_1037 = store(a_1036,i20,select(a_1037,i20)) ).
cnf(hyp274,hypothesis,
i9 != i26 ).
cnf(hyp491,hypothesis,
i1 != i5 ).
cnf(u1008,hypothesis,
( select(a_1032,X0) = select(a_1033,X0)
| i16 = X0 ) ).
cnf(hyp103,hypothesis,
i21 != i23 ).
cnf(u736,hypothesis,
a_1051 = store(store(store(store(a1,i13,select(a_1030,i13)),i1,e1),i19,select(a_1036,i19)),i4,select(a_1021,i4)) ).
cnf(hyp455,hypothesis,
i2 != i13 ).
cnf(hyp324,hypothesis,
i7 != i19 ).
cnf(u601,hypothesis,
e5 = select(a_1022,i5) ).
cnf(u655,hypothesis,
a_1040 = store(a_1039,i23,select(a_1040,i23)) ).
cnf(u620,hypothesis,
e24 = select(a_1041,i24) ).
cnf(u1004,hypothesis,
( select(a_1028,X0) = select(a_1029,X0)
| i12 = X0 ) ).
cnf(u985,hypothesis,
a_1075 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)),i28,select(a_1045,i28)),i17,select(a_1034,i17)),i23,select(a_1040,i23)),i24,select(a_1041,i24)) ).
cnf(u611,hypothesis,
e15 = select(a_1032,i15) ).
cnf(hyp451,hypothesis,
i2 != i17 ).
cnf(hyp407,hypothesis,
i4 != i8 ).
cnf(hyp219,hypothesis,
i12 != i24 ).
cnf(u600,hypothesis,
e4 = select(a_1021,i4) ).
cnf(hyp218,hypothesis,
i12 != i25 ).
cnf(u616,hypothesis,
e20 = select(a_1037,i20) ).
cnf(hyp409,hypothesis,
i4 != i6 ).
cnf(hyp433,hypothesis,
i3 != i8 ).
cnf(u607,hypothesis,
e11 = select(a_1028,i11) ).
cnf(hyp205,hypothesis,
i13 != i21 ).
cnf(hyp365,hypothesis,
i5 != i25 ).
cnf(hyp212,hypothesis,
i13 != i14 ).
cnf(hyp403,hypothesis,
i4 != i12 ).
cnf(u887,hypothesis,
a_1064 = store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)) ).
cnf(hyp199,hypothesis,
i13 != i27 ).
cnf(hyp168,hypothesis,
i15 != i27 ).
cnf(hyp224,hypothesis,
i12 != i19 ).
cnf(hyp359,hypothesis,
i6 != i7 ).
cnf(hyp198,hypothesis,
i13 != i28 ).
cnf(hyp171,hypothesis,
i15 != i24 ).
cnf(hyp201,hypothesis,
i13 != i25 ).
cnf(hyp170,hypothesis,
i15 != i25 ).
cnf(hyp361,hypothesis,
i5 != i29 ).
cnf(hyp192,hypothesis,
i14 != i18 ).
cnf(hyp383,hypothesis,
i5 != i7 ).
cnf(hyp78,hypothesis,
i24 != i27 ).
cnf(hyp282,hypothesis,
i9 != i18 ).
cnf(hyp195,hypothesis,
i14 != i15 ).
cnf(hyp443,hypothesis,
i2 != i25 ).
cnf(hyp164,hypothesis,
i16 != i17 ).
cnf(hyp355,hypothesis,
i6 != i11 ).
cnf(hyp194,hypothesis,
i14 != i16 ).
cnf(hyp151,hypothesis,
i16 != i30 ).
cnf(hyp414,hypothesis,
i3 != i27 ).
cnf(hyp120,hypothesis,
i19 != i25 ).
cnf(hyp311,hypothesis,
i8 != i10 ).
cnf(hyp150,hypothesis,
i17 != i18 ).
cnf(hyp123,hypothesis,
i19 != i22 ).
cnf(hyp276,hypothesis,
i9 != i24 ).
cnf(u1019,hypothesis,
( select(a_1043,X0) = select(a_1044,X0)
| i27 = X0 ) ).
cnf(hyp153,hypothesis,
i16 != i28 ).
cnf(hyp122,hypothesis,
i19 != i23 ).
cnf(hyp313,hypothesis,
i7 != i30 ).
cnf(hyp144,hypothesis,
i17 != i24 ).
cnf(hyp335,hypothesis,
i7 != i8 ).
cnf(hyp429,hypothesis,
i3 != i12 ).
cnf(hyp147,hypothesis,
i17 != i21 ).
cnf(u599,hypothesis,
e3 = select(a_1020,i3) ).
cnf(hyp116,hypothesis,
i19 != i29 ).
cnf(hyp307,hypothesis,
i8 != i14 ).
cnf(hyp146,hypothesis,
i17 != i22 ).
cnf(hyp337,hypothesis,
i6 != i29 ).
cnf(hyp454,hypothesis,
i2 != i14 ).
cnf(hyp133,hypothesis,
i18 != i23 ).
cnf(hyp102,hypothesis,
i21 != i24 ).
cnf(hyp293,hypothesis,
i8 != i28 ).
cnf(hyp140,hypothesis,
i17 != i28 ).
cnf(hyp105,hypothesis,
i20 != i30 ).
cnf(hyp448,hypothesis,
i2 != i20 ).
cnf(hyp127,hypothesis,
i18 != i29 ).
cnf(hyp96,hypothesis,
i21 != i30 ).
cnf(u966,hypothesis,
a_1072 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)),i28,select(a_1045,i28)) ).
cnf(hyp287,hypothesis,
i9 != i13 ).
cnf(hyp126,hypothesis,
i18 != i30 ).
cnf(hyp99,hypothesis,
i21 != i27 ).
cnf(hyp256,hypothesis,
i10 != i24 ).
cnf(hyp129,hypothesis,
i18 != i27 ).
cnf(hyp176,hypothesis,
i15 != i19 ).
cnf(hyp98,hypothesis,
i21 != i28 ).
cnf(hyp289,hypothesis,
i9 != i11 ).
cnf(hyp406,hypothesis,
i4 != i9 ).
cnf(u1017,hypothesis,
( select(a_1041,X0) = select(a_1042,X0)
| i25 = X0 ) ).
cnf(hyp85,hypothesis,
i23 != i26 ).
cnf(hyp178,hypothesis,
i15 != i17 ).
cnf(u598,hypothesis,
e1 = select(a_1018,i1) ).
cnf(hyp92,hypothesis,
i22 != i26 ).
cnf(hyp283,hypothesis,
i9 != i17 ).
cnf(hyp400,hypothesis,
i4 != i15 ).
cnf(u597,hypothesis,
e2 = select(a_1019,i2) ).
cnf(hyp79,hypothesis,
i24 != i26 ).
cnf(u1013,hypothesis,
( select(a_1037,X0) = select(a_1038,X0)
| i21 = X0 ) ).
cnf(hyp388,hypothesis,
i4 != i27 ).
cnf(hyp372,hypothesis,
i5 != i18 ).
cnf(u684,hypothesis,
a_1054 = store(a_1053,i2,select(a_1019,i2)) ).
cnf(hyp402,hypothesis,
i4 != i13 ).
cnf(hyp366,hypothesis,
i5 != i24 ).
cnf(hyp358,hypothesis,
i6 != i8 ).
cnf(u993,hypothesis,
( select(a_1018,X0) = select(a_1019,X0)
| i2 = X0 ) ).
cnf(u994,hypothesis,
( select(a_1018,X0) = select(a1,X0)
| i1 = X0 ) ).
cnf(hyp352,hypothesis,
i6 != i14 ).
cnf(hyp468,hypothesis,
i1 != i28 ).
cnf(hyp319,hypothesis,
i7 != i24 ).
cnf(hyp362,hypothesis,
i5 != i28 ).
cnf(hyp354,hypothesis,
i6 != i12 ).
cnf(u665,hypothesis,
a_1034 = store(a_1033,i17,select(a_1034,i17)) ).
cnf(hyp321,hypothesis,
i7 != i22 ).
cnf(u989,hypothesis,
a_1076 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)),i28,select(a_1045,i28)),i17,select(a_1034,i17)),i23,select(a_1040,i23)),i24,select(a_1041,i24)),i7,select(a_1024,i7)) ).
cnf(hyp310,hypothesis,
i8 != i11 ).
cnf(hyp453,hypothesis,
i2 != i15 ).
cnf(hyp356,hypothesis,
i6 != i10 ).
cnf(hyp304,hypothesis,
i8 != i17 ).
cnf(u735,hypothesis,
a_1056 = store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)) ).
cnf(u822,hypothesis,
a_1060 = store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)) ).
cnf(hyp488,hypothesis,
i1 != i8 ).
cnf(hyp135,hypothesis,
i18 != i21 ).
cnf(u679,hypothesis,
a_1023 = store(a_1022,i6,select(a_1023,i6)) ).
cnf(hyp447,hypothesis,
i2 != i21 ).
cnf(hyp490,hypothesis,
i1 != i6 ).
cnf(hyp494,hypothesis,
i1 != i2 ).
cnf(hyp487,hypothesis,
i1 != i9 ).
cnf(hyp449,hypothesis,
i2 != i19 ).
cnf(u673,hypothesis,
a_1029 = store(a_1028,i12,select(a_1029,i12)) ).
cnf(u666,hypothesis,
a_1033 = store(a_1032,i16,select(a_1033,i16)) ).
cnf(u680,hypothesis,
a_1022 = store(a_1021,i5,select(a_1022,i5)) ).
cnf(hyp489,hypothesis,
i1 != i7 ).
cnf(hyp484,hypothesis,
i1 != i12 ).
cnf(hyp425,hypothesis,
i3 != i16 ).
cnf(u1015,hypothesis,
( select(a_1039,X0) = select(a_1040,X0)
| i23 = X0 ) ).
cnf(u995,hypothesis,
( select(a_1019,X0) = select(a_1020,X0)
| i3 = X0 ) ).
cnf(hyp317,hypothesis,
i7 != i26 ).
cnf(hyp336,hypothesis,
i6 != i30 ).
cnf(hyp483,hypothesis,
i1 != i13 ).
cnf(hyp248,hypothesis,
i11 != i13 ).
cnf(hyp260,hypothesis,
i10 != i20 ).
cnf(hyp439,hypothesis,
i2 != i29 ).
cnf(hyp251,hypothesis,
i10 != i29 ).
cnf(hyp430,hypothesis,
i3 != i11 ).
cnf(hyp225,hypothesis,
i12 != i18 ).
cnf(hyp250,hypothesis,
i10 != i30 ).
cnf(hyp441,hypothesis,
i2 != i27 ).
cnf(hyp237,hypothesis,
i11 != i24 ).
cnf(u676,hypothesis,
a_1026 = store(a_1025,i9,select(a_1026,i9)) ).
cnf(u1016,hypothesis,
( select(a_1040,X0) = select(a_1041,X0)
| i24 = X0 ) ).
cnf(hyp269,hypothesis,
i10 != i11 ).
cnf(hyp244,hypothesis,
i11 != i17 ).
cnf(hyp81,hypothesis,
i23 != i30 ).
cnf(hyp231,hypothesis,
i11 != i30 ).
cnf(hyp72,hypothesis,
i25 != i28 ).
cnf(hyp263,hypothesis,
i10 != i17 ).
cnf(hyp230,hypothesis,
i12 != i13 ).
cnf(hyp75,hypothesis,
i24 != i30 ).
cnf(u619,hypothesis,
e23 = select(a_1040,i23) ).
cnf(hyp233,hypothesis,
i11 != i28 ).
cnf(hyp74,hypothesis,
i25 != i26 ).
cnf(hyp265,hypothesis,
i10 != i15 ).
cnf(hyp382,hypothesis,
i5 != i8 ).
cnf(hyp61,hypothesis,
i28 != i30 ).
cnf(u624,hypothesis,
e28 = select(a_1045,i28) ).
cnf(hyp238,hypothesis,
i11 != i23 ).
cnf(hyp227,hypothesis,
i12 != i16 ).
cnf(hyp68,hypothesis,
i26 != i28 ).
cnf(u1022,hypothesis,
( select(store(store(store(store(store(a1,i13,select(a_1030,i13)),i1,e1),i19,select(a_1036,i19)),i4,select(a_1021,i4)),i9,select(a_1026,i9)),X0) = select(a_1053,X0)
| i30 = X0 ) ).
cnf(hyp259,hypothesis,
i10 != i21 ).
cnf(hyp226,hypothesis,
i12 != i17 ).
cnf(hyp401,hypothesis,
i4 != i14 ).
cnf(hyp183,hypothesis,
i14 != i27 ).
cnf(hyp187,hypothesis,
i14 != i23 ).
cnf(hyp348,hypothesis,
i6 != i18 ).
cnf(hyp373,hypothesis,
i5 != i17 ).
cnf(hyp220,hypothesis,
i12 != i23 ).
cnf(hyp436,hypothesis,
i3 != i5 ).
cnf(hyp185,hypothesis,
i14 != i25 ).
cnf(hyp207,hypothesis,
i13 != i19 ).
cnf(hyp334,hypothesis,
i7 != i9 ).
cnf(hyp367,hypothesis,
i5 != i23 ).
cnf(hyp206,hypothesis,
i13 != i20 ).
cnf(hyp179,hypothesis,
i15 != i16 ).
cnf(hyp306,hypothesis,
i8 != i15 ).
cnf(hyp209,hypothesis,
i13 != i17 ).
cnf(hyp328,hypothesis,
i7 != i15 ).
cnf(u664,hypothesis,
a_1035 = store(a_1034,i18,select(a_1035,i18)) ).
cnf(hyp369,hypothesis,
i5 != i21 ).
cnf(hyp200,hypothesis,
i13 != i26 ).
cnf(hyp165,hypothesis,
i15 != i30 ).
cnf(hyp300,hypothesis,
i8 != i21 ).
cnf(u642,hypothesis,
a_1045 = store(a_1044,i28,select(a_1045,i28)) ).
cnf(hyp330,hypothesis,
i7 != i13 ).
cnf(hyp0,hypothesis,
a_1018 = store(a1,i1,e1) ).
cnf(hyp363,hypothesis,
i5 != i27 ).
cnf(hyp480,hypothesis,
i1 != i16 ).
cnf(hyp381,hypothesis,
i5 != i9 ).
cnf(hyp159,hypothesis,
i16 != i22 ).
cnf(hyp286,hypothesis,
i9 != i14 ).
cnf(u998,hypothesis,
( select(a_1022,X0) = select(a_1023,X0)
| i6 = X0 ) ).
cnf(u626,hypothesis,
a_1046 = store(a_1045,i29,select(a_1046,i29)) ).
cnf(hyp158,hypothesis,
i16 != i23 ).
cnf(hyp482,hypothesis,
i1 != i14 ).
cnf(hyp161,hypothesis,
i16 != i20 ).
cnf(u625,hypothesis,
e29 = select(a_1046,i29) ).
cnf(hyp280,hypothesis,
i9 != i20 ).
cnf(hyp438,hypothesis,
i2 != i30 ).
cnf(hyp117,hypothesis,
i19 != i28 ).
cnf(hyp476,hypothesis,
i1 != i20 ).
cnf(u1002,hypothesis,
( select(a_1026,X0) = select(a_1027,X0)
| i10 = X0 ) ).
cnf(hyp124,hypothesis,
i19 != i21 ).
cnf(hyp315,hypothesis,
i7 != i28 ).
cnf(hyp432,hypothesis,
i3 != i9 ).
cnf(hyp111,hypothesis,
i20 != i24 ).
cnf(hyp113,hypothesis,
i20 != i22 ).
cnf(hyp82,hypothesis,
i23 != i29 ).
cnf(hyp110,hypothesis,
i20 != i25 ).
cnf(hyp353,hypothesis,
i6 != i13 ).
cnf(hyp434,hypothesis,
i3 != i7 ).
cnf(u991,negated_conjecture,
store(a_1046,i1,e1) != store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)),i28,select(a_1045,i28)),i17,select(a_1034,i17)),i23,select(a_1040,i23)),i24,select(a_1041,i24)),i7,select(a_1024,i7)),i10,select(a_1027,i10)) ).
cnf(hyp130,hypothesis,
i18 != i26 ).
cnf(hyp262,hypothesis,
i10 != i18 ).
cnf(hyp485,hypothesis,
i1 != i11 ).
cnf(hyp107,hypothesis,
i20 != i28 ).
cnf(u1012,hypothesis,
( select(a_1036,X0) = select(a_1037,X0)
| i20 = X0 ) ).
cnf(hyp347,hypothesis,
i6 != i19 ).
cnf(hyp106,hypothesis,
i20 != i29 ).
cnf(hyp380,hypothesis,
i5 != i10 ).
cnf(u840,hypothesis,
a_1061 = store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)) ).
cnf(u965,hypothesis,
a_1071 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)) ).
cnf(hyp479,hypothesis,
i1 != i17 ).
cnf(hyp258,hypothesis,
i10 != i22 ).
cnf(u643,hypothesis,
a_1044 = store(a_1043,i27,select(a_1044,i27)) ).
cnf(hyp469,hypothesis,
i1 != i27 ).
cnf(u1021,hypothesis,
( select(a_1045,X0) = select(a_1046,X0)
| i29 = X0 ) ).
cnf(u1024,hypothesis,
a_1053 = store(store(store(store(store(store(a1,i13,select(a_1030,i13)),i1,e1),i19,select(a_1036,i19)),i4,select(a_1021,i4)),i9,select(a_1026,i9)),i30,select(a_1053,i30)) ).
cnf(u644,hypothesis,
a_1043 = store(a_1042,i26,select(a_1043,i26)) ).
cnf(hyp445,hypothesis,
i2 != i23 ).
cnf(u980,hypothesis,
a_1074 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)),i28,select(a_1045,i28)),i17,select(a_1034,i17)),i23,select(a_1040,i23)) ).
cnf(hyp475,hypothesis,
i1 != i21 ).
cnf(u604,hypothesis,
e8 = select(a_1025,i8) ).
cnf(u992,hypothesis,
a_1077 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)),i28,select(a_1045,i28)),i17,select(a_1034,i17)),i23,select(a_1040,i23)),i24,select(a_1041,i24)),i7,select(a_1024,i7)),i10,select(a_1027,i10)) ).
cnf(hyp391,hypothesis,
i4 != i24 ).
cnf(hyp228,hypothesis,
i12 != i15 ).
cnf(hyp203,hypothesis,
i13 != i23 ).
cnf(hyp202,hypothesis,
i13 != i24 ).
cnf(hyp461,hypothesis,
i2 != i7 ).
cnf(hyp393,hypothesis,
i4 != i22 ).
cnf(hyp189,hypothesis,
i14 != i21 ).
cnf(u645,hypothesis,
a_1042 = store(a_1041,i25,select(a_1042,i25)) ).
cnf(hyp349,hypothesis,
i6 != i17 ).
cnf(hyp196,hypothesis,
i13 != i30 ).
cnf(hyp387,hypothesis,
i4 != i28 ).
cnf(hyp152,hypothesis,
i16 != i29 ).
cnf(hyp343,hypothesis,
i6 != i23 ).
cnf(hyp155,hypothesis,
i16 != i26 ).
cnf(u1023,hypothesis,
e30 = select(a_1053,i30) ).
cnf(hyp270,hypothesis,
i9 != i30 ).
cnf(hyp154,hypothesis,
i16 != i27 ).
cnf(hyp431,hypothesis,
i3 != i10 ).
cnf(hyp345,hypothesis,
i6 != i21 ).
cnf(hyp462,hypothesis,
i2 != i6 ).
cnf(u612,hypothesis,
e16 = select(a_1033,i16) ).
cnf(hyp141,hypothesis,
i17 != i27 ).
cnf(hyp420,hypothesis,
i3 != i21 ).
cnf(hyp417,hypothesis,
i3 != i24 ).
cnf(hyp301,hypothesis,
i8 != i20 ).
cnf(hyp148,hypothesis,
i17 != i20 ).
cnf(hyp339,hypothesis,
i6 != i27 ).
cnf(hyp456,hypothesis,
i2 != i12 ).
cnf(hyp264,hypothesis,
i10 != i16 ).
cnf(hyp63,hypothesis,
i27 != i30 ).
cnf(hyp104,hypothesis,
i21 != i22 ).
cnf(u974,hypothesis,
a_1073 = store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)),i26,select(a_1043,i26)),i22,select(a_1039,i22)),i27,select(a_1044,i27)),i3,select(a_1020,i3)),i12,select(a_1029,i12)),i16,select(a_1033,i16)),i28,select(a_1045,i28)),i17,select(a_1034,i17)) ).
cnf(hyp295,hypothesis,
i8 != i26 ).
cnf(hyp134,hypothesis,
i18 != i22 ).
cnf(hyp325,hypothesis,
i7 != i18 ).
cnf(hyp458,hypothesis,
i2 != i10 ).
cnf(hyp137,hypothesis,
i18 != i19 ).
cnf(u615,hypothesis,
e19 = select(a_1036,i19) ).
cnf(hyp410,hypothesis,
i4 != i5 ).
cnf(hyp297,hypothesis,
i8 != i24 ).
cnf(hyp128,hypothesis,
i18 != i28 ).
cnf(hyp93,hypothesis,
i22 != i25 ).
cnf(hyp452,hypothesis,
i2 != i16 ).
cnf(u803,hypothesis,
a_1059 = store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)) ).
cnf(hyp131,hypothesis,
i18 != i25 ).
cnf(hyp100,hypothesis,
i21 != i26 ).
cnf(u1003,hypothesis,
( select(a_1027,X0) = select(a_1028,X0)
| i11 = X0 ) ).
cnf(hyp291,hypothesis,
i8 != i30 ).
cnf(hyp408,hypothesis,
i4 != i7 ).
cnf(hyp87,hypothesis,
i23 != i24 ).
cnf(hyp173,hypothesis,
i15 != i22 ).
cnf(hyp245,hypothesis,
i11 != i16 ).
cnf(hyp86,hypothesis,
i23 != i25 ).
cnf(hyp277,hypothesis,
i9 != i23 ).
cnf(hyp252,hypothesis,
i10 != i28 ).
cnf(hyp89,hypothesis,
i22 != i29 ).
cnf(hyp239,hypothesis,
i11 != i22 ).
cnf(hyp80,hypothesis,
i24 != i25 ).
cnf(hyp271,hypothesis,
i9 != i29 ).
cnf(hyp404,hypothesis,
i4 != i11 ).
cnf(hyp83,hypothesis,
i23 != i28 ).
cnf(hyp241,hypothesis,
i11 != i20 ).
cnf(hyp166,hypothesis,
i15 != i29 ).
cnf(hyp360,hypothesis,
i5 != i30 ).
cnf(hyp169,hypothesis,
i15 != i26 ).
cnf(hyp273,hypothesis,
i9 != i27 ).
cnf(hyp390,hypothesis,
i4 != i25 ).
cnf(hyp69,hypothesis,
i26 != i27 ).
cnf(u613,hypothesis,
e17 = select(a_1034,i17) ).
cnf(hyp76,hypothesis,
i24 != i29 ).
cnf(hyp267,hypothesis,
i10 != i13 ).
cnf(hyp384,hypothesis,
i5 != i6 ).
cnf(hyp160,hypothesis,
i16 != i21 ).
cnf(hyp364,hypothesis,
i5 != i26 ).
cnf(u902,hypothesis,
a_1065 = store(store(store(store(store(store(store(store(store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)),i20,select(a_1037,i20)),i8,select(a_1025,i8)),i21,select(a_1038,i21)),i6,select(a_1023,i6)),i11,select(a_1028,i11)),i14,select(a_1031,i14)),i29,select(a_1046,i29)),i5,select(a_1022,i5)) ).
cnf(hyp62,hypothesis,
i28 != i29 ).
cnf(hyp386,hypothesis,
i4 != i29 ).
cnf(hyp65,hypothesis,
i27 != i28 ).
cnf(hyp312,hypothesis,
i8 != i9 ).
cnf(u670,hypothesis,
a_1030 = store(a_1029,i13,select(a_1030,i13)) ).
cnf(hyp477,hypothesis,
i1 != i19 ).
cnf(hyp342,hypothesis,
i6 != i24 ).
cnf(u669,hypothesis,
a_1031 = store(a_1030,i14,select(a_1031,i14)) ).
cnf(hyp385,hypothesis,
i4 != i30 ).
cnf(u1001,hypothesis,
( select(a_1025,X0) = select(a_1026,X0)
| i9 = X0 ) ).
cnf(hyp314,hypothesis,
i7 != i29 ).
cnf(hyp457,hypothesis,
i2 != i11 ).
cnf(hyp350,hypothesis,
i6 != i16 ).
cnf(hyp308,hypothesis,
i8 != i13 ).
cnf(u674,hypothesis,
a_1028 = store(a_1027,i11,select(a_1028,i11)) ).
cnf(hyp338,hypothesis,
i6 != i28 ).
cnf(u622,hypothesis,
e26 = select(a_1043,i26) ).
cnf(u678,hypothesis,
a_1024 = store(a_1023,i7,select(a_1024,i7)) ).
cnf(hyp294,hypothesis,
i8 != i27 ).
cnf(hyp437,hypothesis,
i3 != i4 ).
cnf(u621,hypothesis,
e25 = select(a_1042,i25) ).
cnf(u677,hypothesis,
a_1025 = store(a_1024,i8,select(a_1025,i8)) ).
cnf(u997,hypothesis,
( select(a_1021,X0) = select(a_1022,X0)
| i5 = X0 ) ).
cnf(u712,hypothesis,
a_1055 = store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)) ).
cnf(hyp288,hypothesis,
i9 != i12 ).
cnf(hyp284,hypothesis,
i9 != i16 ).
cnf(u667,hypothesis,
a_1032 = store(a_1031,i15,select(a_1032,i15)) ).
cnf(hyp478,hypothesis,
i1 != i18 ).
cnf(u602,hypothesis,
e6 = select(a_1023,i6) ).
cnf(hyp290,hypothesis,
i9 != i10 ).
cnf(u675,hypothesis,
a_1027 = store(a_1026,i10,select(a_1027,i10)) ).
cnf(hyp340,hypothesis,
i6 != i26 ).
cnf(u617,hypothesis,
e21 = select(a_1038,i21) ).
cnf(hyp471,hypothesis,
i1 != i25 ).
cnf(hyp472,hypothesis,
i1 != i24 ).
cnf(hyp493,hypothesis,
i1 != i3 ).
cnf(u663,hypothesis,
a_1036 = store(a_1035,i19,select(a_1036,i19)) ).
cnf(hyp254,hypothesis,
i10 != i26 ).
cnf(u656,hypothesis,
a_1039 = store(a_1038,i22,select(a_1039,i22)) ).
cnf(hyp473,hypothesis,
i1 != i23 ).
cnf(hyp474,hypothesis,
i1 != i22 ).
cnf(u671,hypothesis,
a_1048 = store(a1,i13,select(a_1030,i13)) ).
cnf(u999,hypothesis,
( select(a_1023,X0) = select(a_1024,X0)
| i7 = X0 ) ).
cnf(u1020,hypothesis,
( select(a_1044,X0) = select(a_1045,X0)
| i28 = X0 ) ).
cnf(hyp467,hypothesis,
i1 != i29 ).
cnf(hyp246,hypothesis,
i11 != i15 ).
cnf(hyp232,hypothesis,
i11 != i29 ).
cnf(hyp428,hypothesis,
i3 != i13 ).
cnf(hyp423,hypothesis,
i3 != i18 ).
cnf(hyp108,hypothesis,
i20 != i27 ).
cnf(hyp235,hypothesis,
i11 != i26 ).
cnf(hyp427,hypothesis,
i3 != i14 ).
cnf(hyp234,hypothesis,
i11 != i27 ).
cnf(hyp240,hypothesis,
i11 != i21 ).
cnf(hyp444,hypothesis,
i2 != i24 ).
cnf(u623,hypothesis,
e27 = select(a_1044,i27) ).
cnf(hyp221,hypothesis,
i12 != i22 ).
cnf(hyp253,hypothesis,
i10 != i27 ).
cnf(hyp242,hypothesis,
i11 != i19 ).
cnf(hyp419,hypothesis,
i3 != i22 ).
cnf(hyp215,hypothesis,
i12 != i28 ).
cnf(hyp184,hypothesis,
i14 != i26 ).
cnf(u760,hypothesis,
a_1057 = store(store(store(store(a_1053,i2,select(a_1019,i2)),i15,select(a_1032,i15)),i25,select(a_1042,i25)),i18,select(a_1035,i18)) ).
cnf(hyp375,hypothesis,
i5 != i15 ).
cnf(hyp214,hypothesis,
i12 != i29 ).
cnf(hyp405,hypothesis,
i4 != i10 ).
cnf(u1000,hypothesis,
( select(a_1024,X0) = select(a_1025,X0)
| i8 = X0 ) ).
cnf(u603,hypothesis,
e7 = select(a_1024,i7) ).
cnf(hyp217,hypothesis,
i12 != i26 ).
cnf(hyp236,hypothesis,
i11 != i25 ).
cnf(hyp186,hypothesis,
i14 != i24 ).
cnf(hyp377,hypothesis,
i5 != i13 ).
cnf(hyp208,hypothesis,
i13 != i18 ).
cnf(hyp399,hypothesis,
i4 != i16 ).
cnf(hyp389,hypothesis,
i4 != i26 ).
cnf(hyp211,hypothesis,
i13 != i15 ).
cnf(u1010,hypothesis,
( select(a_1034,X0) = select(a_1035,X0)
| i18 = X0 ) ).
cnf(hyp180,hypothesis,
i14 != i30 ).
cnf(hyp371,hypothesis,
i5 != i19 ).
cnf(hyp210,hypothesis,
i13 != i16 ).
cnf(hyp167,hypothesis,
i15 != i28 ).
cnf(hyp424,hypothesis,
i3 != i17 ).
cnf(hyp197,hypothesis,
i13 != i29 ).
cnf(hyp332,hypothesis,
i7 != i11 ).
cnf(hyp357,hypothesis,
i6 != i9 ).
cnf(hyp204,hypothesis,
i13 != i22 ).
cnf(hyp426,hypothesis,
i3 != i15 ).
cnf(hyp395,hypothesis,
i4 != i20 ).
cnf(hyp191,hypothesis,
i14 != i19 ).
cnf(hyp318,hypothesis,
i7 != i25 ).
cnf(hyp351,hypothesis,
i6 != i15 ).
cnf(hyp190,hypothesis,
i14 != i20 ).
cnf(hyp163,hypothesis,
i16 != i18 ).
cnf(hyp193,hypothesis,
i14 != i17 ).
cnf(hyp162,hypothesis,
i16 != i19 ).
cnf(hyp119,hypothesis,
i19 != i26 ).
cnf(hyp470,hypothesis,
i1 != i26 ).
cnf(hyp149,hypothesis,
i17 != i19 ).
cnf(u657,hypothesis,
a_1038 = store(a_1037,i21,select(a_1038,i21)) ).
cnf(hyp118,hypothesis,
i19 != i27 ).
cnf(u1006,hypothesis,
( select(a_1030,X0) = select(a_1031,X0)
| i14 = X0 ) ).
cnf(hyp309,hypothesis,
i8 != i12 ).
cnf(hyp156,hypothesis,
i16 != i25 ).
cnf(hyp121,hypothesis,
i19 != i24 ).
cnf(hyp464,hypothesis,
i2 != i4 ).
cnf(hyp143,hypothesis,
i17 != i25 ).
cnf(hyp112,hypothesis,
i20 != i23 ).
cnf(hyp303,hypothesis,
i8 != i18 ).
cnf(hyp142,hypothesis,
i17 != i26 ).
cnf(hyp115,hypothesis,
i19 != i30 ).
cnf(hyp466,hypothesis,
i1 != i30 ).
cnf(hyp145,hypothesis,
i17 != i23 ).
cnf(hyp114,hypothesis,
i20 != i21 ).
cnf(hyp305,hypothesis,
i8 != i16 ).
cnf(hyp422,hypothesis,
i3 != i19 ).
cnf(hyp101,hypothesis,
i21 != i25 ).
cnf(hyp460,hypothesis,
i2 != i8 ).
cnf(hyp188,hypothesis,
i14 != i22 ).
cnf(hyp266,hypothesis,
i10 != i14 ).
cnf(hyp299,hypothesis,
i8 != i22 ).
cnf(hyp416,hypothesis,
i3 != i25 ).
cnf(hyp341,hypothesis,
i6 != i25 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV498-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.11/0.17 % Computer : n011.cluster.edu
% 0.11/0.17 % Model : x86_64 x86_64
% 0.11/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.17 % Memory : 8046.5625MB
% 0.11/0.17 % OS : Linux 6.8.0-71-generic
% 0.11/0.17 % CPULimit : 300
% 0.11/0.17 % WCLimit : 300
% 0.11/0.17 % DateTime : Mon Sep 28 11:17:16 UTC 2026
% 0.11/0.17 % CPUTime :
% 0.11/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.21 Running first-order theorem proving
% 0.11/0.21 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
% 3.79/1.50 % (3332178)Input is clausal, will run a generic CNF schedule.
% 3.79/1.50 % (3332184)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3675866793:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.79/1.50 % (3332187)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3412920804:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.79/1.50 % (3332188)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2543985302:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.79/1.50 % (3332186)lrs+10_1_sil=8000:sp=occurrence:random_seed=633627345:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.79/1.50 % (3332185)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=942715877:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.79/1.50 % (3332183)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=1813358360:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.79/1.50 % (3332189)dis-21_1_sil=8000:lcm=predicate:random_seed=2600210980: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.79/1.50 % (3332186)Refutation not found, incomplete strategy
% 3.79/1.50 % (3332186)------------------------------
% 3.79/1.50 % (3332186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.50 % (3332186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.50 % (3332186)CaDiCaL version: 2.1.3
% 3.79/1.50 % (3332186)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.50 % (3332186)Time elapsed: 0.008 s
% 3.79/1.50 % (3332186)Peak memory usage: 88 MB
% 3.79/1.50 % (3332186)Instructions burned: 17 (million)
% 3.79/1.50 % (3332187)Refutation not found, incomplete strategy
% 3.79/1.50 % (3332187)------------------------------
% 3.79/1.50 % (3332187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.50 % (3332187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.50 % (3332187)CaDiCaL version: 2.1.3
% 3.79/1.50 % (3332187)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.50 % (3332187)Time elapsed: 0.015 s
% 3.79/1.50 % (3332187)Peak memory usage: 88 MB
% 3.79/1.50 % (3332187)Instructions burned: 30 (million)
% 3.79/1.50 % (3332188)Refutation not found, incomplete strategy
% 3.79/1.50 % (3332188)------------------------------
% 3.79/1.50 % (3332188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.50 % (3332188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.50 % (3332188)CaDiCaL version: 2.1.3
% 3.79/1.50 % (3332188)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.50 % (3332188)Time elapsed: 0.020 s
% 3.79/1.50 % (3332188)Peak memory usage: 88 MB
% 3.79/1.50 % (3332188)Instructions burned: 39 (million)
% 3.79/1.50 % (3332189)Refutation not found, incomplete strategy
% 3.79/1.50 % (3332189)------------------------------
% 3.79/1.50 % (3332189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.50 % (3332189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.50 % (3332189)CaDiCaL version: 2.1.3
% 3.79/1.50 % (3332189)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.50 % (3332189)Time elapsed: 0.012 s
% 3.79/1.50 % (3332189)Peak memory usage: 88 MB
% 3.79/1.50 % (3332189)Instructions burned: 24 (million)
% 3.79/1.50 % (3332187)------------------------------
% 3.79/1.50 % (3332187)------------------------------
% 3.79/1.50 % (3332186)------------------------------
% 3.79/1.50 % (3332186)------------------------------
% 3.79/1.50 % (3332188)------------------------------
% 3.79/1.50 % (3332188)------------------------------
% 3.79/1.50 % (3332189)------------------------------
% 3.79/1.50 % (3332189)------------------------------
% 3.79/1.50 % (3332197)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=2813813412:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 3.79/1.50 % (3332198)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=610483566:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 3.79/1.50 % (3332197)Refutation not found, incomplete strategy
% 3.79/1.50 % (3332197)------------------------------
% 3.79/1.50 % (3332197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.50 % (3332197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.50 % (3332197)CaDiCaL version: 2.1.3
% 3.79/1.50 % (3332197)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.50 % (3332197)Time elapsed: 0.011 s
% 3.79/1.50 % (3332197)Peak memory usage: 88 MB
% 3.79/1.50 % (3332197)Instructions burned: 20 (million)
% 3.79/1.50 % (3332199)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1934494035:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 3.79/1.50 % (3332200)lrs+10_64_to=lpo:sil=8000:random_seed=2643099409:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 3.79/1.50 % (3332198)Refutation not found, incomplete strategy
% 3.79/1.50 % (3332198)------------------------------
% 3.79/1.50 % (3332198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.50 % (3332198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.50 % (3332198)CaDiCaL version: 2.1.3
% 3.79/1.50 % (3332198)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.50 % (3332198)Time elapsed: 0.021 s
% 3.79/1.50 % (3332198)Peak memory usage: 88 MB
% 3.79/1.50 % (3332198)Instructions burned: 43 (million)
% 3.79/1.50 % (3332199)Refutation not found, incomplete strategy
% 3.79/1.50 % (3332199)------------------------------
% 3.79/1.50 % (3332199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.50 % (3332199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.50 % (3332199)CaDiCaL version: 2.1.3
% 3.79/1.50 % (3332199)Termination reason: Refutation not found, incomplete strategy
% 3.79/1.50 % (3332199)Time elapsed: 0.010 s
% 3.79/1.50 % (3332199)Peak memory usage: 88 MB
% 3.79/1.50 % (3332199)Instructions burned: 20 (million)
% 3.79/1.50 % (3332200)First to succeed.
% 3.79/1.50 % (3332200)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3332178"
% 3.79/1.50 % (3332197)------------------------------
% 3.79/1.50 % (3332197)------------------------------
% 3.79/1.50 % (3332199)------------------------------
% 3.79/1.50 % (3332199)------------------------------
% 3.79/1.50 % (3332198)------------------------------
% 3.79/1.50 % (3332198)------------------------------
% 3.79/1.50 % SZS status Satisfiable for theBenchmark
% 3.79/1.50 % SZS output start Saturation.
% See solution above
% 3.79/1.60 % SZS output start Definitions and Model Updates.
% 3.79/1.60 % SZS output end Definitions and Model Updates.
% 3.79/1.60 % (3332200)------------------------------
% 3.79/1.60 % (3332200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.60 % (3332200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.60 % (3332200)CaDiCaL version: 2.1.3
% 3.79/1.60 % (3332200)Termination reason: Satisfiable
% 3.79/1.60 % (3332200)Time elapsed: 0.048 s
% 3.79/1.60 % (3332200)Peak memory usage: 88 MB
% 3.79/1.60 % (3332200)Instructions burned: 103 (million)
% 3.79/1.60 % (3332200)------------------------------
% 3.79/1.60 % (3332200)------------------------------
% 3.79/1.60 % (3332178)Success in time 0.855 s
% 3.79/1.60 % Vampire exiting
%------------------------------------------------------------------------------