%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV502-1.050 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 4.00s 0.95s
% Output : Saturation 4.00s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2866,axiom,
i1 != sF100 ).
cnf(u2871,axiom,
sF101 = select(sF48,sF100) ).
cnf(u2878,axiom,
i49 != sF100 ).
cnf(u2883,axiom,
sF101 = select(sF47,sF100) ).
cnf(u2905,axiom,
sF102 = select(sF98,sF100) ).
cnf(u2912,axiom,
i31 != sF100 ).
cnf(u2917,axiom,
sF102 = select(sF97,sF100) ).
cnf(u3096,axiom,
i48 != sF100 ).
cnf(u3101,axiom,
sF101 = select(sF46,sF100) ).
cnf(u3108,axiom,
i21 != sF100 ).
cnf(u3113,axiom,
sF102 = select(sF96,sF100) ).
cnf(u3292,axiom,
i24 != sF100 ).
cnf(u3297,axiom,
sF102 = select(sF95,sF100) ).
cnf(u3342,axiom,
i4 != sF100 ).
cnf(u3347,axiom,
sF102 = select(sF94,sF100) ).
cnf(u3410,axiom,
i32 != sF100 ).
cnf(u3415,axiom,
sF102 = select(sF93,sF100) ).
cnf(u3422,axiom,
i5 != sF100 ).
cnf(u3427,axiom,
sF102 = select(sF92,sF100) ).
cnf(u3436,axiom,
i12 != sF100 ).
cnf(u3441,axiom,
sF102 = select(sF91,sF100) ).
cnf(u3495,axiom,
i37 != sF100 ).
cnf(u3500,axiom,
sF102 = select(sF90,sF100) ).
cnf(u3590,axiom,
i3 != sF100 ).
cnf(u3595,axiom,
sF102 = select(sF89,sF100) ).
cnf(u3679,axiom,
i29 != sF100 ).
cnf(u3683,axiom,
e48 != sF102 ).
cnf(u3894,axiom,
i10 != sF100 ).
cnf(u3899,axiom,
e24 != select(sF86,sF100) ).
cnf(u3908,axiom,
i2 != sF100 ).
cnf(u3913,axiom,
e24 != select(sF85,sF100) ).
cnf(u3946,hypothesis,
i23 != sF100 ).
cnf(u3951,hypothesis,
e24 != select(sF80,sF100) ).
cnf(u3978,hypothesis,
i11 != sF100 ).
cnf(u3983,hypothesis,
e24 != select(sF76,sF100) ).
cnf(u4021,axiom,
sF102 = select(sF88,sF100) ).
cnf(u4147,axiom,
e4 != select(sF85,sF100) ).
cnf(u4529,axiom,
e5 != select(sF85,sF100) ).
cnf(u4970,axiom,
e3 != select(sF85,sF100) ).
cnf(u5364,axiom,
i47 != sF100 ).
cnf(u5369,axiom,
sF101 = select(sF45,sF100) ).
cnf(u5375,axiom,
i50 = sF100 ).
cnf(u5379,axiom,
e24 != select(sF84,sF100) ).
cnf(u5383,hypothesis,
i38 != sF100 ).
cnf(u5388,hypothesis,
e24 != select(sF79,sF100) ).
cnf(u5392,hypothesis,
i34 != sF100 ).
cnf(u5397,hypothesis,
e24 != select(sF75,sF100) ).
cnf(u5402,axiom,
e4 != select(sF84,sF100) ).
cnf(u5407,axiom,
e5 != select(sF84,sF100) ).
cnf(u5411,axiom,
sF102 = select(sF85,sF100) ).
cnf(u5417,axiom,
e3 != select(sF84,sF100) ).
cnf(u5423,axiom,
i46 != sF100 ).
cnf(u5428,axiom,
sF101 = select(sF44,sF100) ).
cnf(u5435,axiom,
i45 != sF100 ).
cnf(u5440,axiom,
sF101 = select(sF43,sF100) ).
cnf(u5458,axiom,
i44 != sF100 ).
cnf(u5462,axiom,
sF101 = select(sF42,sF100) ).
cnf(u5475,axiom,
i43 != sF100 ).
cnf(u5480,axiom,
e46 != select(sF41,sF100) ).
cnf(u5487,axiom,
i42 != sF100 ).
cnf(u5492,axiom,
e46 != select(sF40,sF100) ).
cnf(u5499,axiom,
i41 != sF100 ).
cnf(u5504,axiom,
e46 != select(sF39,sF100) ).
cnf(u5521,axiom,
i40 != sF100 ).
cnf(u5526,axiom,
e46 != select(sF38,sF100) ).
cnf(u5535,axiom,
i39 != sF100 ).
cnf(u5540,axiom,
e46 != select(sF37,sF100) ).
cnf(u5550,axiom,
e46 != select(sF36,sF100) ).
cnf(u5571,axiom,
i36 != sF100 ).
cnf(u5576,axiom,
e46 != select(sF34,sF100) ).
cnf(u5582,axiom,
i35 != sF100 ).
cnf(u5587,axiom,
e24 != e46 ).
cnf(u5594,axiom,
e4 != e46 ).
cnf(u5601,axiom,
e5 != e46 ).
cnf(u5608,axiom,
e3 != e46 ).
cnf(u5620,axiom,
e46 != sF102 ).
cnf(u5627,axiom,
e24 != select(sF83,sF100) ).
cnf(u5632,axiom,
e4 != select(sF83,sF100) ).
cnf(u5637,axiom,
e5 != select(sF83,sF100) ).
cnf(u5642,axiom,
e3 != select(sF83,sF100) ).
cnf(u5646,axiom,
sF102 != select(sF83,sF100) ).
cnf(u5652,axiom,
sF101 = select(sF41,sF100) ).
cnf(u5674,axiom,
e47 != select(sF40,sF100) ).
cnf(u5682,axiom,
e47 != select(sF39,sF100) ).
cnf(u5690,axiom,
e47 != select(sF38,sF100) ).
cnf(u5698,axiom,
e47 != select(sF37,sF100) ).
cnf(u5706,axiom,
e47 != select(sF36,sF100) ).
cnf(u5714,axiom,
e47 != select(sF34,sF100) ).
cnf(u5720,axiom,
e46 != select(sF33,sF100) ).
cnf(u5726,axiom,
e47 != select(sF33,sF100) ).
cnf(u5748,axiom,
e46 != select(sF32,sF100) ).
cnf(u5754,axiom,
e47 != select(sF32,sF100) ).
cnf(u5759,axiom,
i25 != sF100 ).
cnf(u5764,axiom,
e24 != select(sF81,sF100) ).
cnf(u5770,axiom,
e4 != select(sF81,sF100) ).
cnf(u5776,axiom,
e5 != select(sF81,sF100) ).
cnf(u5782,axiom,
e3 != select(sF81,sF100) ).
cnf(u5792,axiom,
sF102 != select(sF81,sF100) ).
cnf(u5799,axiom,
i33 != sF100 ).
cnf(u5804,axiom,
e46 != select(sF31,sF100) ).
cnf(u5853,axiom,
e47 != select(sF31,sF100) ).
cnf(u5878,hypothesis,
e4 != select(sF79,sF100) ).
cnf(u5884,hypothesis,
e5 != select(sF79,sF100) ).
cnf(u5890,hypothesis,
e3 != select(sF79,sF100) ).
cnf(u5900,hypothesis,
sF102 != select(sF79,sF100) ).
cnf(u5937,hypothesis,
e24 != select(sF78,sF100) ).
cnf(u5943,hypothesis,
e4 != select(sF78,sF100) ).
cnf(u5949,hypothesis,
e5 != select(sF78,sF100) ).
cnf(u5955,hypothesis,
e3 != select(sF78,sF100) ).
cnf(u5965,hypothesis,
sF102 != select(sF78,sF100) ).
cnf(u5985,axiom,
i30 != sF100 ).
cnf(u5990,axiom,
e46 != select(sF28,sF100) ).
cnf(u5996,axiom,
e47 != select(sF28,sF100) ).
cnf(u6002,hypothesis,
e24 != select(sF77,sF100) ).
cnf(u6008,hypothesis,
e4 != select(sF77,sF100) ).
cnf(u6014,hypothesis,
e5 != select(sF77,sF100) ).
cnf(u6020,hypothesis,
e3 != select(sF77,sF100) ).
cnf(u6030,hypothesis,
sF102 != select(sF77,sF100) ).
cnf(u6214,hypothesis,
sF101 = select(sF33,sF100) ).
cnf(u6224,hypothesis,
sF101 = select(sF32,sF100) ).
cnf(u6281,axiom,
i28 != sF100 ).
cnf(u6286,axiom,
e46 != select(sF26,sF100) ).
cnf(u6298,axiom,
e47 != select(sF26,sF100) ).
cnf(u6303,axiom,
i27 != sF100 ).
cnf(u6308,axiom,
e46 != select(sF25,sF100) ).
cnf(u6314,axiom,
e47 != select(sF25,sF100) ).
cnf(u6319,hypothesis,
i26 != sF100 ).
cnf(u6324,hypothesis,
e24 != select(sF74,sF100) ).
cnf(u6330,axiom,
e46 != select(sF24,sF100) ).
cnf(u6336,axiom,
e47 != select(sF24,sF100) ).
cnf(u6355,hypothesis,
sF101 = select(sF31,sF100) ).
cnf(u6415,hypothesis,
e4 != select(sF74,sF100) ).
cnf(u6421,hypothesis,
e5 != select(sF74,sF100) ).
cnf(u6427,hypothesis,
e3 != select(sF74,sF100) ).
cnf(u6437,hypothesis,
sF102 != select(sF74,sF100) ).
cnf(u6444,hypothesis,
i18 != sF100 ).
cnf(u6449,hypothesis,
e24 != select(sF73,sF100) ).
cnf(u6455,hypothesis,
e4 != select(sF73,sF100) ).
cnf(u6461,hypothesis,
e5 != select(sF73,sF100) ).
cnf(u6467,hypothesis,
e3 != select(sF73,sF100) ).
cnf(u6477,hypothesis,
sF102 != select(sF73,sF100) ).
cnf(u6567,hypothesis,
i17 != sF100 ).
cnf(u6572,hypothesis,
e24 != select(sF70,sF100) ).
cnf(u6578,hypothesis,
e4 != select(sF70,sF100) ).
cnf(u6584,hypothesis,
e5 != select(sF70,sF100) ).
cnf(u6590,hypothesis,
e3 != select(sF70,sF100) ).
cnf(u6600,hypothesis,
sF102 != select(sF70,sF100) ).
cnf(u6794,hypothesis,
i9 != sF100 ).
cnf(u6799,hypothesis,
e24 != select(sF69,sF100) ).
cnf(u6805,hypothesis,
e4 != select(sF69,sF100) ).
cnf(u6811,hypothesis,
e5 != select(sF69,sF100) ).
cnf(u6817,hypothesis,
e3 != select(sF69,sF100) ).
cnf(u6868,hypothesis,
i7 != sF100 ).
cnf(u6873,hypothesis,
e24 != select(sF67,sF100) ).
cnf(u6881,hypothesis,
e4 != select(sF67,sF100) ).
cnf(u6887,hypothesis,
e5 != select(sF67,sF100) ).
cnf(u6893,hypothesis,
e3 != select(sF67,sF100) ).
cnf(u6908,hypothesis,
i15 != sF100 ).
cnf(u6913,hypothesis,
e24 != select(sF66,sF100) ).
cnf(u6921,hypothesis,
e4 != select(sF66,sF100) ).
cnf(u6929,hypothesis,
e5 != select(sF66,sF100) ).
cnf(u6935,hypothesis,
e3 != select(sF66,sF100) ).
cnf(u6957,hypothesis,
i22 != sF100 ).
cnf(u6962,hypothesis,
e46 != select(sF20,sF100) ).
cnf(u6967,hypothesis,
e47 != select(sF20,sF100) ).
cnf(u6972,hypothesis,
sF101 = select(sF20,sF100) ).
cnf(u7015,hypothesis,
sF102 != select(sF69,sF100) ).
cnf(u7047,hypothesis,
sF102 != select(sF67,sF100) ).
cnf(u7074,hypothesis,
sF102 != select(sF66,sF100) ).
cnf(u7101,hypothesis,
i6 != sF100 ).
cnf(u7106,hypothesis,
e24 != select(sF64,sF100) ).
cnf(u7112,hypothesis,
e4 != select(sF64,sF100) ).
cnf(u7118,hypothesis,
e5 != select(sF64,sF100) ).
cnf(u7124,hypothesis,
e3 != select(sF64,sF100) ).
cnf(u7134,hypothesis,
sF102 != select(sF64,sF100) ).
cnf(u7493,hypothesis,
i20 != sF100 ).
cnf(u7498,hypothesis,
e46 != select(sF18,sF100) ).
cnf(u7503,hypothesis,
e47 != select(sF18,sF100) ).
cnf(u7509,hypothesis,
i13 != sF100 ).
cnf(u7514,hypothesis,
e24 != select(sF63,sF100) ).
cnf(u7519,hypothesis,
e4 != select(sF63,sF100) ).
cnf(u7524,hypothesis,
e5 != select(sF63,sF100) ).
cnf(u7529,hypothesis,
e3 != select(sF63,sF100) ).
cnf(u7551,hypothesis,
e33 != select(sF18,sF100) ).
cnf(u7557,hypothesis,
e33 != select(sF39,sF100) ).
cnf(u7727,hypothesis,
sF101 = select(sF18,sF100) ).
cnf(u8805,hypothesis,
e43 != select(sF18,sF100) ).
cnf(u8816,hypothesis,
i19 != sF100 ).
cnf(u8821,hypothesis,
e46 != select(sF17,sF100) ).
cnf(u8827,hypothesis,
e47 != select(sF17,sF100) ).
cnf(u8833,hypothesis,
e33 != select(sF17,sF100) ).
cnf(u8845,hypothesis,
e43 != select(sF17,sF100) ).
cnf(u8884,hypothesis,
i16 != sF100 ).
cnf(u8889,hypothesis,
e46 != select(sF14,sF100) ).
cnf(u8895,hypothesis,
e47 != select(sF14,sF100) ).
cnf(u8901,hypothesis,
e33 != select(sF14,sF100) ).
cnf(u8907,hypothesis,
e43 != select(sF14,sF100) ).
cnf(u8917,hypothesis,
e46 != select(sF63,sF100) ).
cnf(u8932,hypothesis,
i14 != sF100 ).
cnf(u8937,hypothesis,
e24 != select(sF62,sF100) ).
cnf(u8943,hypothesis,
e4 != select(sF62,sF100) ).
cnf(u8949,hypothesis,
e5 != select(sF62,sF100) ).
cnf(u8955,hypothesis,
e3 != select(sF62,sF100) ).
cnf(u8965,hypothesis,
e46 != select(sF62,sF100) ).
cnf(u9026,hypothesis,
e46 != select(sF12,sF100) ).
cnf(u9032,hypothesis,
e47 != select(sF12,sF100) ).
cnf(u9038,hypothesis,
e33 != select(sF12,sF100) ).
cnf(u9044,hypothesis,
e43 != select(sF12,sF100) ).
cnf(u9078,hypothesis,
e24 != select(sF60,sF100) ).
cnf(u9084,hypothesis,
e4 != select(sF60,sF100) ).
cnf(u9090,hypothesis,
e5 != select(sF60,sF100) ).
cnf(u9096,hypothesis,
e3 != select(sF60,sF100) ).
cnf(u9106,hypothesis,
e46 != select(sF60,sF100) ).
cnf(u9231,hypothesis,
e24 != select(sF59,sF100) ).
cnf(u9237,hypothesis,
e4 != select(sF59,sF100) ).
cnf(u9243,hypothesis,
e5 != select(sF59,sF100) ).
cnf(u9249,hypothesis,
e3 != select(sF59,sF100) ).
cnf(u9259,hypothesis,
e46 != select(sF59,sF100) ).
cnf(u9341,hypothesis,
e24 != select(sF57,sF100) ).
cnf(u9347,hypothesis,
e4 != select(sF57,sF100) ).
cnf(u9353,hypothesis,
e5 != select(sF57,sF100) ).
cnf(u9359,hypothesis,
e3 != select(sF57,sF100) ).
cnf(u9369,hypothesis,
e46 != select(sF57,sF100) ).
cnf(u9469,hypothesis,
e24 != select(sF54,sF100) ).
cnf(u9475,hypothesis,
e4 != select(sF54,sF100) ).
cnf(u9481,hypothesis,
e5 != select(sF54,sF100) ).
cnf(u9487,hypothesis,
e3 != select(sF54,sF100) ).
cnf(u9497,hypothesis,
e46 != select(sF54,sF100) ).
cnf(u14319,axiom,
e46 != select(sF23,sF100) ).
cnf(u14324,axiom,
e47 != select(sF23,sF100) ).
cnf(u14879,hypothesis,
e46 != select(sF6,sF100) ).
cnf(u14884,hypothesis,
e47 != select(sF6,sF100) ).
cnf(u14889,hypothesis,
e33 != select(sF6,sF100) ).
cnf(u14894,hypothesis,
e43 != select(sF6,sF100) ).
cnf(u14899,hypothesis,
sF101 = select(sF6,sF100) ).
cnf(u14971,hypothesis,
e50 != select(sF60,sF100) ).
cnf(u1693,hypothesis,
i25 != i9 ).
cnf(u1339,hypothesis,
i48 != i13 ).
cnf(u1883,hypothesis,
i13 != i7 ).
cnf(u2735,axiom,
e26 = select(sF75,i26) ).
cnf(u8868,hypothesis,
e46 != select(sF15,sF100) ).
cnf(u995,hypothesis,
i50 != i18 ).
cnf(u2405,hypothesis,
i25 != i1 ).
cnf(u1193,hypothesis,
i50 != i15 ).
cnf(u15049,hypothesis,
sF101 = select(sF2,sF100) ).
cnf(u1517,hypothesis,
i34 != i11 ).
cnf(u1035,hypothesis,
i30 != i18 ).
cnf(u1707,hypothesis,
i18 != i9 ).
cnf(u203,hypothesis,
i41 != i36 ).
cnf(u1905,hypothesis,
i45 != i6 ).
cnf(u8924,hypothesis,
e47 != select(sF13,sF100) ).
cnf(u1087,hypothesis,
i36 != i17 ).
cnf(u14946,hypothesis,
e50 != select(sF69,sF100) ).
cnf(u2229,hypothesis,
i18 != i3 ).
cnf(u1395,hypothesis,
i20 != i13 ).
cnf(u507,hypothesis,
i29 != i28 ).
cnf(u33,hypothesis,
i50 != i44 ).
cnf(u1601,hypothesis,
i31 != i10 ).
cnf(u1249,hypothesis,
i22 != i15 ).
cnf(u1807,hypothesis,
i9 != i8 ).
cnf(u1925,hypothesis,
i35 != i6 ).
cnf(u1091,hypothesis,
i34 != i17 ).
cnf(u1763,hypothesis,
i31 != i8 ).
cnf(u265,hypothesis,
i39 != i34 ).
cnf(u2710,axiom,
e1 = select(sF49,i1) ).
cnf(u1425,hypothesis,
i42 != i12 ).
cnf(u1631,hypothesis,
i16 != i10 ).
cnf(u2303,hypothesis,
i28 != i2 ).
cnf(u1749,hypothesis,
i38 != i8 ).
cnf(u1939,hypothesis,
i28 != i6 ).
cnf(u569,hypothesis,
i43 != i26 ).
cnf(u89,hypothesis,
i43 != i41 ).
cnf(u1785,hypothesis,
i20 != i8 ).
cnf(u1319,hypothesis,
i22 != i14 ).
cnf(u2732,axiom,
e42 = select(sF72,i42) ).
cnf(u1275,hypothesis,
i44 != i14 ).
cnf(u801,hypothesis,
i29 != i22 ).
cnf(u2327,hypothesis,
i16 != i2 ).
cnf(u1961,hypothesis,
i17 != i6 ).
cnf(u1481,hypothesis,
i14 != i12 ).
cnf(u2339,hypothesis,
i10 != i2 ).
cnf(u1143,hypothesis,
i41 != i16 ).
cnf(u1687,hypothesis,
i28 != i9 ).
cnf(u2365,hypothesis,
i45 != i1 ).
cnf(u1451,hypothesis,
i29 != i12 ).
cnf(u1995,hypothesis,
i44 != i5 ).
cnf(u625,hypothesis,
i39 != i25 ).
cnf(u145,hypothesis,
i45 != i38 ).
cnf(u831,hypothesis,
i42 != i21 ).
cnf(u2842,axiom,
( select(sF81,X0) = select(sF82,X0)
| i25 = X0 ) ).
cnf(u2163,hypothesis,
i5 != i4 ).
cnf(u1863,hypothesis,
i23 != i7 ).
cnf(u2061,hypothesis,
i11 != i5 ).
cnf(u8860,hypothesis,
e43 != select(sF16,sF100) ).
cnf(u321,hypothesis,
i44 != i32 ).
cnf(u2017,hypothesis,
i33 != i5 ).
cnf(u527,hypothesis,
i41 != i27 ).
cnf(u1199,hypothesis,
i47 != i15 ).
cnf(u2693,axiom,
e33 = select(sF32,i33) ).
cnf(u1507,hypothesis,
i39 != i11 ).
cnf(u2674,axiom,
e14 = select(sF13,i14) ).
cnf(u681,hypothesis,
i36 != i24 ).
cnf(u1375,hypothesis,
i30 != i13 ).
cnf(u2047,hypothesis,
i18 != i5 ).
cnf(u2707,axiom,
e47 = select(sF46,i47) ).
cnf(u857,hypothesis,
i29 != i21 ).
cnf(u505,hypothesis,
i30 != i28 ).
cnf(u39,hypothesis,
i47 != i44 ).
cnf(u2648,axiom,
store(sF96,i21,e21) = sF97 ).
cnf(u2508,axiom,
store(sF26,i28,e28) = sF27 ).
cnf(u1743,hypothesis,
i41 != i8 ).
cnf(u2786,axiom,
( select(sF24,X0) = select(sF25,X0)
| i26 = X0 ) ).
cnf(u201,hypothesis,
i42 != i36 ).
cnf(u887,hypothesis,
i43 != i20 ).
cnf(u1431,hypothesis,
i39 != i12 ).
cnf(u2808,axiom,
( select(sF46,X0) = select(sF47,X0)
| i48 = X0 ) ).
cnf(u2843,axiom,
( select(sF82,X0) = select(sF83,X0)
| i46 = X0 ) ).
cnf(u913,hypothesis,
i30 != i20 ).
cnf(u2586,axiom,
store(sF65,i27,e27) = sF66 ).
cnf(u95,hypothesis,
i49 != i40 ).
cnf(u2451,hypothesis,
i2 != i1 ).
cnf(u1255,hypothesis,
i19 != i15 ).
cnf(u2105,hypothesis,
i34 != i4 ).
cnf(u2829,axiom,
( select(sF68,X0) = select(sF69,X0)
| i33 = X0 ) ).
cnf(u2667,axiom,
e7 = select(sF6,i7) ).
cnf(u737,hypothesis,
i34 != i23 ).
cnf(u6102,axiom,
sF101 = select(sF37,sF100) ).
cnf(u271,hypothesis,
i36 != i34 ).
cnf(u943,hypothesis,
i45 != i19 ).
cnf(u1487,hypothesis,
i49 != i11 ).
cnf(u2608,axiom,
store(sF76,i11,e11) = sF77 ).
cnf(u2275,hypothesis,
i42 != i2 ).
cnf(u2301,hypothesis,
i29 != i2 ).
cnf(u5563,axiom,
e4 != sF102 ).
cnf(u767,hypothesis,
i46 != i22 ).
cnf(u2816,axiom,
( select(sF55,X0) = select(sF56,X0)
| i22 = X0 ) ).
cnf(u327,hypothesis,
i41 != i32 ).
cnf(u2552,axiom,
store(sF48,i1,e1) = sF49 ).
cnf(u969,hypothesis,
i32 != i19 ).
cnf(u617,hypothesis,
i43 != i25 ).
cnf(u151,hypothesis,
i42 != i38 ).
cnf(u2760,axiom,
( select(a1,X0) = select(sF0,X0)
| i1 = X0 ) ).
cnf(u37,hypothesis,
i48 != i44 ).
cnf(u8856,hypothesis,
e47 != select(sF16,sF100) ).
cnf(u999,hypothesis,
i48 != i18 ).
cnf(u2393,hypothesis,
i31 != i1 ).
cnf(u6620,hypothesis,
sF101 = select(sF28,sF100) ).
cnf(u2765,axiom,
( select(sF3,X0) = select(sF4,X0)
| i5 = X0 ) ).
cnf(u2411,hypothesis,
i22 != i1 ).
cnf(u2698,axiom,
e38 = select(sF37,i38) ).
cnf(u207,hypothesis,
i39 != i36 ).
cnf(u729,hypothesis,
i38 != i23 ).
cnf(u2217,hypothesis,
i24 != i3 ).
cnf(u2235,hypothesis,
i15 != i3 ).
cnf(u2779,axiom,
( select(sF17,X0) = select(sF18,X0)
| i19 = X0 ) ).
cnf(u573,hypothesis,
i41 != i26 ).
cnf(u511,hypothesis,
i49 != i27 ).
cnf(u2720,axiom,
e16 = select(sF60,i16) ).
cnf(u6563,hypothesis,
e47 != select(sF21,sF100) ).
cnf(u269,hypothesis,
i37 != i34 ).
cnf(u15086,hypothesis,
e33 != select(sF0,sF100) ).
cnf(u9547,hypothesis,
e24 != select(sF53,sF100) ).
cnf(u2574,axiom,
store(sF59,i16,e16) = sF60 ).
cnf(u14980,hypothesis,
e50 != select(sF56,sF100) ).
cnf(u93,hypothesis,
i50 != i40 ).
cnf(u15042,hypothesis,
e43 != select(sF2,sF100) ).
cnf(u9448,hypothesis,
e3 != select(sF55,sF100) ).
cnf(u6260,hypothesis,
e4 != select(sF76,sF100) ).
cnf(u805,hypothesis,
i27 != i22 ).
cnf(u325,hypothesis,
i42 != i32 ).
cnf(u2558,axiom,
store(sF51,i45,e45) = sF52 ).
cnf(u2596,axiom,
store(sF70,i17,e17) = sF71 ).
cnf(u2343,hypothesis,
i8 != i2 ).
cnf(u2353,hypothesis,
i3 != i2 ).
cnf(u629,hypothesis,
i37 != i25 ).
cnf(u149,hypothesis,
i43 != i38 ).
cnf(u819,hypothesis,
i48 != i21 ).
cnf(u1303,hypothesis,
i30 != i14 ).
cnf(u2167,hypothesis,
i49 != i3 ).
cnf(u2711,axiom,
e30 = select(sF51,i30) ).
cnf(u8601,hypothesis,
e33 != select(sF29,sF100) ).
cnf(u1341,hypothesis,
i47 != i13 ).
cnf(u2049,hypothesis,
i17 != i5 ).
cnf(u861,hypothesis,
i27 != i21 ).
cnf(u5930,axiom,
e46 != select(sF29,sF100) ).
cnf(u2496,axiom,
store(sF20,i22,e22) = sF21 ).
cnf(u515,hypothesis,
i47 != i27 ).
cnf(u15002,hypothesis,
e47 != select(sF4,sF100) ).
cnf(u1037,hypothesis,
i29 != i18 ).
cnf(u685,hypothesis,
i34 != i24 ).
cnf(u875,hypothesis,
i49 != i20 ).
cnf(u1397,hypothesis,
i19 != i13 ).
cnf(u509,hypothesis,
i50 != i27 ).
cnf(u27,hypothesis,
i48 != i45 ).
cnf(u699,hypothesis,
i27 != i24 ).
cnf(u2817,axiom,
( select(sF56,X0) = select(sF57,X0)
| i39 = X0 ) ).
cnf(u15024,hypothesis,
e43 != select(sF3,sF100) ).
cnf(u1573,hypothesis,
i45 != i10 ).
cnf(u1093,hypothesis,
i33 != i17 ).
cnf(u2814,axiom,
( select(sF53,X0) = select(sF54,X0)
| i28 = X0 ) ).
cnf(u259,hypothesis,
i42 != i34 ).
cnf(u205,hypothesis,
i40 != i36 ).
cnf(u1073,hypothesis,
i43 != i17 ).
cnf(u1805,hypothesis,
i10 != i8 ).
cnf(u2289,hypothesis,
i35 != i2 ).
cnf(u2847,axiom,
( select(sF86,X0) = select(sF87,X0)
| i10 = X0 ) ).
cnf(u917,hypothesis,
i28 != i20 ).
cnf(u1587,hypothesis,
i38 != i10 ).
cnf(u83,hypothesis,
i46 != i41 ).
cnf(u2708,axiom,
e48 = select(sF47,i48) ).
cnf(u1305,hypothesis,
i29 != i14 ).
cnf(u6205,hypothesis,
sF101 = select(sF34,sF100) ).
cnf(u1629,hypothesis,
i17 != i10 ).
cnf(u1819,hypothesis,
i45 != i7 ).
cnf(u2671,axiom,
e11 = select(sF10,i11) ).
cnf(u9318,hypothesis,
e5 != select(sF58,sF100) ).
cnf(u741,hypothesis,
i32 != i23 ).
cnf(u931,hypothesis,
i21 != i20 ).
cnf(u2341,hypothesis,
i9 != i2 ).
cnf(u1129,hypothesis,
i48 != i16 ).
cnf(u2279,hypothesis,
i40 != i2 ).
cnf(u1453,hypothesis,
i28 != i12 ).
cnf(u973,hypothesis,
i30 != i19 ).
cnf(u1643,hypothesis,
i50 != i9 ).
cnf(u5857,hypothesis,
e4 != select(sF80,sF100) ).
cnf(u1841,hypothesis,
i34 != i7 ).
cnf(u755,hypothesis,
i25 != i23 ).
cnf(u2165,hypothesis,
i50 != i3 ).
cnf(u1331,hypothesis,
i16 != i14 ).
cnf(u1277,hypothesis,
i43 != i14 ).
cnf(u6626,hypothesis,
sF101 = select(sF27,sF100) ).
cnf(u443,hypothesis,
i40 != i29 ).
cnf(u987,hypothesis,
i23 != i19 ).
cnf(u1537,hypothesis,
i24 != i11 ).
cnf(u1185,hypothesis,
i20 != i16 ).
cnf(u9226,hypothesis,
e43 != select(sF10,sF100) ).
cnf(u1509,hypothesis,
i38 != i11 ).
cnf(u1027,hypothesis,
i34 != i18 ).
cnf(u2646,axiom,
store(sF95,i24,e24) = sF96 ).
cnf(u139,hypothesis,
i48 != i38 ).
cnf(u1361,hypothesis,
i37 != i13 ).
cnf(u1567,hypothesis,
i48 != i10 ).
cnf(u2239,hypothesis,
i13 != i3 ).
cnf(u1685,hypothesis,
i29 != i9 ).
cnf(u6084,axiom,
sF101 = select(sF40,sF100) ).
cnf(u1875,hypothesis,
i17 != i7 ).
cnf(u499,hypothesis,
i33 != i28 ).
cnf(u25,hypothesis,
i49 != i45 ).
cnf(u1721,hypothesis,
i11 != i9 ).
cnf(u2502,axiom,
store(sF23,i25,e25) = sF24 ).
cnf(u2668,axiom,
e8 = select(sF7,i8) ).
cnf(u2045,hypothesis,
i19 != i5 ).
cnf(u2753,axiom,
e5 = select(sF93,i5) ).
cnf(u2415,hypothesis,
i20 != i1 ).
cnf(u1699,hypothesis,
i22 != i9 ).
cnf(u195,hypothesis,
i45 != i36 ).
cnf(u1897,hypothesis,
i49 != i6 ).
cnf(u1417,hypothesis,
i46 != i12 ).
cnf(u1079,hypothesis,
i40 != i17 ).
cnf(u1623,hypothesis,
i20 != i10 ).
cnf(u1741,hypothesis,
i42 != i8 ).
cnf(u1387,hypothesis,
i24 != i13 ).
cnf(u1931,hypothesis,
i32 != i6 ).
cnf(u2783,axiom,
( select(sF21,X0) = select(sF22,X0)
| i23 = X0 ) ).
cnf(u561,hypothesis,
i47 != i26 ).
cnf(u81,hypothesis,
i47 != i41 ).
cnf(u1241,hypothesis,
i26 != i15 ).
cnf(u2099,hypothesis,
i37 != i4 ).
cnf(u1799,hypothesis,
i13 != i8 ).
cnf(u1211,hypothesis,
i41 != i15 ).
cnf(u1755,hypothesis,
i35 != i8 ).
cnf(u257,hypothesis,
i43 != i34 ).
cnf(u1953,hypothesis,
i21 != i6 ).
cnf(u1135,hypothesis,
i45 != i16 ).
cnf(u631,hypothesis,
i36 != i25 ).
cnf(u2277,hypothesis,
i41 != i2 ).
cnf(u2819,axiom,
( select(sF58,X0) = select(sF59,X0)
| i40 = X0 ) ).
cnf(u1443,hypothesis,
i33 != i12 ).
cnf(u2562,axiom,
store(sF53,i28,e28) = sF54 ).
cnf(u2780,axiom,
( select(sF18,X0) = select(sF19,X0)
| i20 = X0 ) ).
cnf(u1311,hypothesis,
i26 != i14 ).
cnf(u1983,hypothesis,
i50 != i5 ).
cnf(u1267,hypothesis,
i48 != i14 ).
cnf(u6266,hypothesis,
e3 != select(sF76,sF100) ).
cnf(u793,hypothesis,
i33 != i22 ).
cnf(u441,hypothesis,
i41 != i29 ).
cnf(u2546,axiom,
store(sF45,i47,e47) = sF46 ).
cnf(u2758,axiom,
e31 = select(sF98,i31) ).
cnf(u519,hypothesis,
i45 != i27 ).
cnf(u1473,hypothesis,
i18 != i12 ).
cnf(u5562,axiom,
e5 != sF102 ).
cnf(u8549,hypothesis,
e33 != select(sF33,sF100) ).
cnf(u1679,hypothesis,
i32 != i9 ).
cnf(u9316,hypothesis,
e4 != select(sF58,sF100) ).
cnf(u1987,hypothesis,
i48 != i5 ).
cnf(u2610,axiom,
store(sF77,i36,e36) = sF78 ).
cnf(u137,hypothesis,
i49 != i38 ).
cnf(u9224,hypothesis,
e33 != select(sF10,sF100) ).
cnf(u823,hypothesis,
i46 != i21 ).
cnf(u1367,hypothesis,
i34 != i13 ).
cnf(u849,hypothesis,
i33 != i21 ).
cnf(u1761,hypothesis,
i32 != i8 ).
cnf(u31,hypothesis,
i46 != i45 ).
cnf(u2009,hypothesis,
i37 != i5 ).
cnf(u2387,hypothesis,
i34 != i1 ).
cnf(u1191,hypothesis,
i17 != i16 ).
cnf(u1735,hypothesis,
i45 != i8 ).
cnf(u2413,hypothesis,
i21 != i1 ).
cnf(u1499,hypothesis,
i43 != i11 ).
cnf(u673,hypothesis,
i40 != i24 ).
cnf(u193,hypothesis,
i46 != i36 ).
cnf(u2858,axiom,
( select(sF97,X0) = select(sF98,X0)
| i31 = X0 ) ).
cnf(u879,hypothesis,
i47 != i20 ).
cnf(u2039,hypothesis,
i22 != i5 ).
cnf(u2755,axiom,
e4 = select(sF95,i4) ).
cnf(u2237,hypothesis,
i14 != i3 ).
cnf(u497,hypothesis,
i34 != i28 ).
cnf(u703,hypothesis,
i25 != i24 ).
cnf(u1247,hypothesis,
i23 != i15 ).
cnf(u6660,hypothesis,
sF101 = select(sF26,sF100) ).
cnf(u2802,axiom,
( select(sF40,X0) = select(sF41,X0)
| i42 = X0 ) ).
cnf(u263,hypothesis,
i40 != i34 ).
cnf(u1423,hypothesis,
i43 != i12 ).
cnf(u15084,hypothesis,
e47 != select(sF0,sF100) ).
cnf(u905,hypothesis,
i34 != i20 ).
cnf(u6674,hypothesis,
sF102 != select(sF72,sF100) ).
cnf(u87,hypothesis,
i44 != i41 ).
cnf(u759,hypothesis,
i50 != i22 ).
cnf(u1479,hypothesis,
i15 != i12 ).
cnf(u8539,hypothesis,
e33 != select(sF35,sF100) ).
cnf(u2701,axiom,
e41 = select(sF40,i41) ).
cnf(u2347,hypothesis,
i6 != i2 ).
cnf(u961,hypothesis,
i36 != i19 ).
cnf(u2634,axiom,
store(sF89,i3,e3) = sF90 ).
cnf(u143,hypothesis,
i46 != i38 ).
cnf(u15040,hypothesis,
e33 != select(sF2,sF100) ).
cnf(u2153,hypothesis,
i10 != i4 ).
cnf(u2171,hypothesis,
i47 != i3 ).
cnf(u2715,axiom,
e19 = select(sF55,i19) ).
cnf(u447,hypothesis,
i38 != i29 ).
cnf(u991,hypothesis,
i21 != i19 ).
cnf(u2656,axiom,
select(sF49,sF100) = sF101 ).
cnf(u14717,hypothesis,
sF101 = select(sF8,sF100) ).
cnf(u15022,hypothesis,
e33 != select(sF3,sF100) ).
cnf(u14916,axiom,
e4 != e50 ).
cnf(u503,hypothesis,
i31 != i28 ).
cnf(u29,hypothesis,
i47 != i45 ).
cnf(u14978,hypothesis,
e50 != select(sF57,sF100) ).
cnf(u261,hypothesis,
i41 != i34 ).
cnf(u2494,axiom,
store(sF19,i21,e21) = sF20 ).
cnf(u199,hypothesis,
i43 != i36 ).
cnf(u2745,axiom,
e50 = select(sF85,i50) ).
cnf(u565,hypothesis,
i45 != i26 ).
cnf(u85,hypothesis,
i45 != i41 ).
cnf(u15000,hypothesis,
e46 != select(sF4,sF100) ).
cnf(u2441,hypothesis,
i7 != i1 ).
cnf(u2103,hypothesis,
i35 != i4 ).
cnf(u797,hypothesis,
i31 != i22 ).
cnf(u2265,hypothesis,
i47 != i2 ).
cnf(u2823,axiom,
( select(sF62,X0) = select(sF63,X0)
| i14 = X0 ) ).
cnf(u2283,hypothesis,
i38 != i2 ).
cnf(u621,hypothesis,
i41 != i25 ).
cnf(u811,hypothesis,
i24 != i22 ).
cnf(u2768,axiom,
( select(sF6,X0) = select(sF7,X0)
| i8 = X0 ) ).
cnf(u2838,axiom,
( select(sF77,X0) = select(sF78,X0)
| i36 = X0 ) ).
cnf(u1333,hypothesis,
i15 != i14 ).
cnf(u445,hypothesis,
i39 != i29 ).
cnf(u635,hypothesis,
i34 != i25 ).
cnf(u14960,hypothesis,
e50 != select(sF63,sF100) ).
cnf(u1029,hypothesis,
i33 != i18 ).
cnf(u2750,axiom,
e3 = select(sF90,i3) ).
cnf(u14939,hypothesis,
e50 != select(sF72,sF100) ).
cnf(u141,hypothesis,
i47 != i38 ).
cnf(u2225,hypothesis,
i20 != i3 ).
cnf(u1295,hypothesis,
i34 != i14 ).
cnf(u853,hypothesis,
i31 != i21 ).
cnf(u501,hypothesis,
i32 != i28 ).
cnf(u19,hypothesis,
i48 != i46 ).
cnf(u2644,axiom,
store(sF94,i4,e4) = sF95 ).
cnf(u2391,hypothesis,
i32 != i1 ).
cnf(u1565,hypothesis,
i49 != i10 ).
cnf(u2401,hypothesis,
i27 != i1 ).
cnf(u677,hypothesis,
i38 != i24 ).
cnf(u197,hypothesis,
i44 != i36 ).
cnf(u867,hypothesis,
i24 != i21 ).
cnf(u1065,hypothesis,
i47 != i17 ).
cnf(u14921,negated_conjecture,
e50 != sF101 ).
cnf(u2215,hypothesis,
i25 != i3 ).
cnf(u2759,axiom,
e1 = select(sF99,i1) ).
cnf(u2804,axiom,
( select(sF42,X0) = select(sF43,X0)
| i44 = X0 ) ).
cnf(u1389,hypothesis,
i23 != i13 ).
cnf(u909,hypothesis,
i32 != i20 ).
cnf(u1579,hypothesis,
i42 != i10 ).
cnf(u691,hypothesis,
i31 != i24 ).
cnf(u2101,hypothesis,
i36 != i4 ).
cnf(u14736,hypothesis,
sF101 = select(sF7,sF100) ).
cnf(u1213,hypothesis,
i40 != i15 ).
cnf(u733,hypothesis,
i36 != i23 ).
cnf(u379,hypothesis,
i33 != i31 ).
cnf(u923,hypothesis,
i25 != i20 ).
cnf(u1121,hypothesis,
i19 != i17 ).
cnf(u1797,hypothesis,
i14 != i8 ).
cnf(u1445,hypothesis,
i32 != i12 ).
cnf(u2582,axiom,
store(sF63,i13,e13) = sF64 ).
cnf(u75,hypothesis,
i50 != i41 ).
cnf(u747,hypothesis,
i29 != i23 ).
cnf(u1297,hypothesis,
i33 != i14 ).
cnf(u2175,hypothesis,
i45 != i3 ).
cnf(u1621,hypothesis,
i21 != i10 ).
cnf(u1269,hypothesis,
i47 != i14 ).
cnf(u1811,hypothesis,
i49 != i7 ).
cnf(u435,hypothesis,
i44 != i29 ).
cnf(u2548,axiom,
store(sF46,i48,e48) = sF47 ).
cnf(u1657,hypothesis,
i43 != i9 ).
cnf(u2604,axiom,
store(sF74,i26,e26) = sF75 ).
cnf(u1981,hypothesis,
i7 != i6 ).
cnf(u2689,axiom,
e29 = select(sF28,i29) ).
cnf(u2351,hypothesis,
i4 != i2 ).
cnf(u965,hypothesis,
i34 != i19 ).
cnf(u1635,hypothesis,
i14 != i10 ).
cnf(u131,hypothesis,
i41 != i39 ).
cnf(u2756,axiom,
e24 = select(sF96,i24) ).
cnf(u1833,hypothesis,
i38 != i7 ).
cnf(u1353,hypothesis,
i41 != i13 ).
cnf(u1559,hypothesis,
i13 != i11 ).
cnf(u1677,hypothesis,
i33 != i9 ).
cnf(u1323,hypothesis,
i20 != i14 ).
cnf(u1867,hypothesis,
i21 != i7 ).
cnf(u2719,axiom,
e40 = select(sF59,i40) ).
cnf(u17,hypothesis,
i49 != i46 ).
cnf(u979,hypothesis,
i27 != i19 ).
cnf(u2389,hypothesis,
i33 != i1 ).
cnf(u1177,hypothesis,
i24 != i16 ).
cnf(u1501,hypothesis,
i42 != i11 ).
cnf(u1147,hypothesis,
i39 != i16 ).
cnf(u1691,hypothesis,
i26 != i9 ).
cnf(u6090,axiom,
sF101 = select(sF39,sF100) ).
cnf(u1889,hypothesis,
i10 != i7 ).
cnf(u1071,hypothesis,
i44 != i17 ).
cnf(u2213,hypothesis,
i26 != i3 ).
cnf(u1379,hypothesis,
i28 != i13 ).
cnf(u9422,hypothesis,
e5 != select(sF56,sF100) ).
cnf(u6840,hypothesis,
e24 != select(sF68,sF100) ).
cnf(u491,hypothesis,
i37 != i28 ).
cnf(u1713,hypothesis,
i15 != i9 ).
cnf(u1233,hypothesis,
i30 != i15 ).
cnf(u1919,hypothesis,
i38 != i6 ).
cnf(u2037,hypothesis,
i23 != i5 ).
cnf(u1203,hypothesis,
i45 != i15 ).
cnf(u1747,hypothesis,
i39 != i8 ).
cnf(u377,hypothesis,
i34 != i31 ).
cnf(u2482,axiom,
store(sF13,i15,e15) = sF14 ).
cnf(u2694,axiom,
e34 = select(sF33,i34) ).
cnf(u1409,hypothesis,
i50 != i12 ).
cnf(u1615,hypothesis,
i24 != i10 ).
cnf(u2287,hypothesis,
i36 != i2 ).
cnf(u1733,hypothesis,
i46 != i8 ).
cnf(u1923,hypothesis,
i36 != i6 ).
cnf(u553,hypothesis,
i28 != i27 ).
cnf(u73,hypothesis,
i43 != i42 ).
cnf(u1769,hypothesis,
i28 != i8 ).
cnf(u14604,hypothesis,
sF102 != select(sF68,sF100) ).
cnf(u2856,axiom,
( select(sF95,X0) = select(sF96,X0)
| i24 = X0 ) ).
cnf(u2716,axiom,
e22 = select(sF56,i22) ).
cnf(u1259,hypothesis,
i17 != i15 ).
cnf(u785,hypothesis,
i37 != i22 ).
cnf(u9308,hypothesis,
e47 != select(sF9,sF100) ).
cnf(u1945,hypothesis,
i25 != i6 ).
cnf(u2323,hypothesis,
i18 != i2 ).
cnf(u1127,hypothesis,
i49 != i16 ).
cnf(u1671,hypothesis,
i36 != i9 ).
cnf(u2349,hypothesis,
i5 != i2 ).
cnf(u1435,hypothesis,
i37 != i12 ).
cnf(u609,hypothesis,
i47 != i25 ).
cnf(u129,hypothesis,
i42 != i39 ).
cnf(u815,hypothesis,
i50 != i21 ).
cnf(u2147,hypothesis,
i13 != i4 ).
cnf(u1975,hypothesis,
i10 != i6 ).
cnf(u2691,axiom,
e31 = select(sF30,i31) ).
cnf(u2173,hypothesis,
i46 != i3 ).
cnf(u2826,axiom,
( select(sF65,X0) = select(sF66,X0)
| i27 = X0 ) ).
cnf(u433,hypothesis,
i45 != i29 ).
cnf(u2001,hypothesis,
i41 != i5 ).
cnf(u639,hypothesis,
i32 != i25 ).
cnf(u1183,hypothesis,
i21 != i16 ).
cnf(u2805,axiom,
( select(sF43,X0) = select(sF44,X0)
| i45 = X0 ) ).
cnf(u1491,hypothesis,
i47 != i11 ).
cnf(u665,hypothesis,
i44 != i24 ).
cnf(u6761,hypothesis,
sF101 = select(sF22,sF100) ).
cnf(u2658,axiom,
select(sF99,sF100) = sF102 ).
cnf(u1359,hypothesis,
i38 != i13 ).
cnf(u2031,hypothesis,
i26 != i5 ).
cnf(u15020,hypothesis,
e47 != select(sF3,sF100) ).
cnf(u2680,axiom,
e20 = select(sF19,i20) ).
cnf(u841,hypothesis,
i37 != i21 ).
cnf(u489,hypothesis,
i38 != i28 ).
cnf(u23,hypothesis,
i50 != i45 ).
cnf(u695,hypothesis,
i29 != i24 ).
cnf(u871,hypothesis,
i22 != i21 ).
cnf(u14998,hypothesis,
e50 != select(sF55,sF100) ).
cnf(u1415,hypothesis,
i47 != i12 ).
cnf(u8653,hypothesis,
e33 != select(sF25,sF100) ).
cnf(u2827,axiom,
( select(sF66,X0) = select(sF67,X0)
| i15 = X0 ) ).
cnf(u897,hypothesis,
i38 != i20 ).
cnf(u2570,axiom,
store(sF57,i20,e20) = sF58 ).
cnf(u79,hypothesis,
i48 != i41 ).
cnf(u2792,axiom,
( select(sF30,X0) = select(sF31,X0)
| i32 = X0 ) ).
cnf(u2435,hypothesis,
i10 != i1 ).
cnf(u1239,hypothesis,
i27 != i15 ).
cnf(u2089,hypothesis,
i42 != i4 ).
cnf(u9420,hypothesis,
e4 != select(sF56,sF100) ).
cnf(u2107,hypothesis,
i33 != i4 ).
cnf(u721,hypothesis,
i42 != i23 ).
cnf(u383,hypothesis,
i50 != i30 ).
cnf(u927,hypothesis,
i23 != i20 ).
cnf(u5859,hypothesis,
e5 != select(sF80,sF100) ).
cnf(u2592,axiom,
store(sF68,i33,e33) = sF69 ).
cnf(u2259,hypothesis,
i50 != i2 ).
cnf(u2309,hypothesis,
i25 != i2 ).
cnf(u15082,hypothesis,
e46 != select(sF0,sF100) ).
cnf(u2285,hypothesis,
i37 != i2 ).
cnf(u751,hypothesis,
i27 != i23 ).
cnf(u14958,hypothesis,
e50 != select(sF64,sF100) ).
cnf(u315,hypothesis,
i47 != i32 ).
cnf(u439,hypothesis,
i42 != i29 ).
cnf(u983,hypothesis,
i25 != i19 ).
cnf(u2554,axiom,
store(a1,i41,e41) = sF50 ).
cnf(u14914,axiom,
e5 != e50 ).
cnf(u855,hypothesis,
i30 != i21 ).
cnf(u135,hypothesis,
i50 != i38 ).
cnf(u2681,axiom,
e21 = select(sF20,i21) ).
cnf(u6396,hypothesis,
e4 != select(sF75,sF100) ).
cnf(u14995,hypothesis,
sF101 = select(sF5,sF100) ).
cnf(u495,hypothesis,
i35 != i28 ).
cnf(u21,hypothesis,
i47 != i46 ).
cnf(u15095,hypothesis,
sF101 = select(sF0,sF100) ).
cnf(u2857,axiom,
( select(sF96,X0) = select(sF97,X0)
| i21 = X0 ) ).
cnf(u2377,hypothesis,
i39 != i1 ).
cnf(u2395,hypothesis,
i30 != i1 ).
cnf(u2810,axiom,
( select(sF48,X0) = select(sF49,X0)
| i1 = X0 ) ).
cnf(u2201,hypothesis,
i32 != i3 ).
cnf(u14915,axiom,
e3 != e50 ).
cnf(u2219,hypothesis,
i23 != i3 ).
cnf(u2763,axiom,
( select(sF1,X0) = select(sF2,X0)
| i3 = X0 ) ).
cnf(u557,hypothesis,
i49 != i26 ).
cnf(u2704,axiom,
e44 = select(sF43,i44) ).
cnf(u14955,hypothesis,
e50 != select(sF65,sF100) ).
cnf(u381,hypothesis,
i32 != i31 ).
cnf(u2632,axiom,
store(sF88,i29,e29) = sF89 ).
cnf(u571,hypothesis,
i42 != i26 ).
cnf(u2686,axiom,
e26 = select(sF25,i26) ).
cnf(u77,hypothesis,
i49 != i41 ).
cnf(u6529,hypothesis,
e5 != select(sF72,sF100) ).
cnf(u9220,hypothesis,
e46 != select(sF10,sF100) ).
cnf(u789,hypothesis,
i35 != i22 ).
cnf(u437,hypothesis,
i43 != i29 ).
cnf(u2542,axiom,
store(sF43,i45,e45) = sF44 ).
cnf(u2580,axiom,
store(sF62,i14,e14) = sF63 ).
cnf(u2793,axiom,
( select(sF31,X0) = select(sF32,X0)
| i33 = X0 ) ).
cnf(u14927,axiom,
e46 != e50 ).
cnf(u8529,hypothesis,
e33 != select(sF37,sF100) ).
cnf(u2337,hypothesis,
i11 != i2 ).
cnf(u613,hypothesis,
i45 != i25 ).
cnf(u133,hypothesis,
i40 != i39 ).
cnf(u803,hypothesis,
i28 != i22 ).
cnf(u2151,hypothesis,
i11 != i4 ).
cnf(u2695,axiom,
e35 = select(sF34,i35) ).
cnf(u1325,hypothesis,
i19 != i14 ).
cnf(u2161,hypothesis,
i6 != i4 ).
cnf(u845,hypothesis,
i35 != i21 ).
cnf(u5729,axiom,
e24 != select(sF82,sF100) ).
cnf(u627,hypothesis,
i38 != i25 ).
cnf(u373,hypothesis,
i36 != i31 ).
cnf(u1149,hypothesis,
i38 != i16 ).
cnf(u669,hypothesis,
i42 != i24 ).
cnf(u2854,axiom,
( select(sF93,X0) = select(sF94,X0)
| i32 = X0 ) ).
cnf(u859,hypothesis,
i28 != i21 ).
cnf(u1381,hypothesis,
i27 != i13 ).
cnf(u493,hypothesis,
i36 != i28 ).
cnf(u11,hypothesis,
i49 != i47 ).
cnf(u683,hypothesis,
i35 != i24 ).
cnf(u2111,hypothesis,
i31 != i4 ).
cnf(u1557,hypothesis,
i14 != i11 ).
cnf(u1205,hypothesis,
i44 != i15 ).
cnf(u2798,axiom,
( select(sF36,X0) = select(sF37,X0)
| i38 = X0 ) ).
cnf(u371,hypothesis,
i37 != i31 ).
cnf(u2484,axiom,
store(sF14,i16,e16) = sF15 ).
cnf(u649,hypothesis,
i27 != i25 ).
cnf(u1057,hypothesis,
i19 != i18 ).
cnf(u1917,hypothesis,
i39 != i6 ).
cnf(u2273,hypothesis,
i43 != i2 ).
cnf(u2831,axiom,
( select(sF70,X0) = select(sF71,X0)
| i17 = X0 ) ).
cnf(u901,hypothesis,
i36 != i20 ).
cnf(u1571,hypothesis,
i46 != i10 ).
cnf(u67,hypothesis,
i46 != i42 ).
cnf(u2692,axiom,
e32 = select(sF31,i32) ).
cnf(u14837,hypothesis,
e24 != select(sF51,sF100) ).
cnf(u1289,hypothesis,
i37 != i14 ).
cnf(u2439,hypothesis,
i8 != i1 ).
cnf(u907,hypothesis,
i33 != i20 ).
cnf(u1613,hypothesis,
i25 != i10 ).
cnf(u2449,hypothesis,
i3 != i1 ).
cnf(u1803,hypothesis,
i11 != i8 ).
cnf(u14631,hypothesis,
sF102 != select(sF65,sF100) ).
cnf(u725,hypothesis,
i40 != i23 ).
cnf(u915,hypothesis,
i29 != i20 ).
cnf(u1593,hypothesis,
i35 != i10 ).
cnf(u2325,hypothesis,
i17 != i2 ).
cnf(u1113,hypothesis,
i23 != i17 ).
cnf(u2263,hypothesis,
i48 != i2 ).
cnf(u1437,hypothesis,
i36 != i12 ).
cnf(u1083,hypothesis,
i38 != i17 ).
cnf(u1627,hypothesis,
i18 != i10 ).
cnf(u1825,hypothesis,
i42 != i7 ).
cnf(u739,hypothesis,
i33 != i23 ).
cnf(u2149,hypothesis,
i12 != i4 ).
cnf(u1315,hypothesis,
i24 != i14 ).
cnf(u6263,hypothesis,
e5 != select(sF76,sF100) ).
cnf(u1261,hypothesis,
i16 != i15 ).
cnf(u427,hypothesis,
i48 != i29 ).
cnf(u971,hypothesis,
i31 != i19 ).
cnf(u1649,hypothesis,
i47 != i9 ).
cnf(u1169,hypothesis,
i28 != i16 ).
cnf(u1855,hypothesis,
i27 != i7 ).
cnf(u1973,hypothesis,
i11 != i6 ).
cnf(u1493,hypothesis,
i46 != i11 ).
cnf(u1139,hypothesis,
i43 != i16 ).
cnf(u313,hypothesis,
i48 != i32 ).
cnf(u2630,axiom,
store(sF87,i48,e48) = sF88 ).
cnf(u251,hypothesis,
i46 != i34 ).
cnf(u1345,hypothesis,
i45 != i13 ).
cnf(u1551,hypothesis,
i17 != i11 ).
cnf(u2223,hypothesis,
i21 != i3 ).
cnf(u1669,hypothesis,
i37 != i9 ).
cnf(u1859,hypothesis,
i25 != i7 ).
cnf(u483,hypothesis,
i41 != i28 ).
cnf(u9,hypothesis,
i50 != i47 ).
cnf(u1705,hypothesis,
i19 != i9 ).
cnf(u2652,axiom,
store(sF98,i1,e1) = sF99 ).
cnf(u2029,hypothesis,
i27 != i5 ).
cnf(u2399,hypothesis,
i28 != i1 ).
cnf(u15114,hypothesis,
e3 != sF101 ).
cnf(u1683,hypothesis,
i30 != i9 ).
cnf(u1881,hypothesis,
i14 != i7 ).
cnf(u1529,hypothesis,
i28 != i11 ).
cnf(u1063,hypothesis,
i48 != i17 ).
cnf(u1607,hypothesis,
i28 != i10 ).
cnf(u1371,hypothesis,
i32 != i13 ).
cnf(u2043,hypothesis,
i20 != i5 ).
cnf(u2767,axiom,
( select(sF5,X0) = select(sF6,X0)
| i7 = X0 ) ).
cnf(u545,hypothesis,
i32 != i27 ).
cnf(u65,hypothesis,
i47 != i42 ).
cnf(u2437,hypothesis,
i9 != i1 ).
cnf(u1225,hypothesis,
i34 != i15 ).
cnf(u2083,hypothesis,
i45 != i4 ).
cnf(u1911,hypothesis,
i42 != i6 ).
cnf(u6551,hypothesis,
e3 != select(sF71,sF100) ).
cnf(u9414,hypothesis,
e33 != select(sF7,sF100) ).
cnf(u2109,hypothesis,
i32 != i4 ).
cnf(u1195,hypothesis,
i49 != i15 ).
cnf(u1739,hypothesis,
i43 != i8 ).
cnf(u369,hypothesis,
i38 != i31 ).
cnf(u1937,hypothesis,
i29 != i6 ).
cnf(u575,hypothesis,
i40 != i26 ).
cnf(u5932,axiom,
e47 != select(sF29,sF100) ).
cnf(u1119,hypothesis,
i20 != i17 ).
cnf(u2741,axiom,
e23 = select(sF81,i23) ).
cnf(u2261,hypothesis,
i49 != i2 ).
cnf(u1427,hypothesis,
i41 != i12 ).
cnf(u601,hypothesis,
i27 != i26 ).
cnf(u15080,hypothesis,
e46 != select(sF50,sF100) ).
cnf(u2764,axiom,
( select(sF2,X0) = select(sF3,X0)
| i4 = X0 ) ).
cnf(u1967,hypothesis,
i14 != i6 ).
cnf(u1251,hypothesis,
i21 != i15 ).
cnf(u777,hypothesis,
i41 != i22 ).
cnf(u425,hypothesis,
i49 != i29 ).
cnf(u2530,axiom,
store(sF37,i39,e39) = sF38 ).
cnf(u2568,axiom,
store(sF56,i39,e39) = sF57 ).
cnf(u2556,axiom,
store(sF50,i30,e30) = sF51 ).
cnf(u9336,hypothesis,
e43 != select(sF8,sF100) ).
cnf(u1791,hypothesis,
i17 != i8 ).
cnf(u249,hypothesis,
i47 != i34 ).
cnf(u807,hypothesis,
i26 != i22 ).
cnf(u1351,hypothesis,
i42 != i13 ).
cnf(u15,hypothesis,
i50 != i46 ).
cnf(u833,hypothesis,
i41 != i21 ).
cnf(u2616,axiom,
store(sF80,i23,e23) = sF81 ).
cnf(u1993,hypothesis,
i45 != i5 ).
cnf(u2371,hypothesis,
i42 != i1 ).
cnf(u1175,hypothesis,
i25 != i16 ).
cnf(u2397,hypothesis,
i29 != i1 ).
cnf(u14917,axiom,
e24 != e50 ).
cnf(u1483,hypothesis,
i13 != i12 ).
cnf(u657,hypothesis,
i48 != i24 ).
cnf(u319,hypothesis,
i45 != i32 ).
cnf(u863,hypothesis,
i26 != i21 ).
cnf(u9053,hypothesis,
e3 != select(sF61,sF100) ).
cnf(u2195,hypothesis,
i35 != i3 ).
cnf(u2023,hypothesis,
i30 != i5 ).
cnf(u15018,hypothesis,
e46 != select(sF3,sF100) ).
cnf(u2706,axiom,
e46 = select(sF45,i46) ).
cnf(u2221,hypothesis,
i22 != i3 ).
cnf(u9412,hypothesis,
e47 != select(sF7,sF100) ).
cnf(u769,hypothesis,
i45 != i22 ).
cnf(u481,hypothesis,
i42 != i28 ).
cnf(u687,hypothesis,
i33 != i24 ).
cnf(u1231,hypothesis,
i31 != i15 ).
cnf(u6549,hypothesis,
e5 != select(sF71,sF100) ).
cnf(u713,hypothesis,
i46 != i23 ).
cnf(u13692,hypothesis,
e43 != sF101 ).
cnf(u375,hypothesis,
i35 != i31 ).
cnf(u2472,axiom,
store(sF8,i10,e10) = sF9 ).
cnf(u2490,axiom,
store(sF17,i19,e19) = sF18 ).
cnf(u1535,hypothesis,
i25 != i11 ).
cnf(u1017,hypothesis,
i39 != i18 ).
cnf(u71,hypothesis,
i44 != i42 ).
cnf(u743,hypothesis,
i31 != i23 ).
cnf(u14951,hypothesis,
e50 != select(sF67,sF100) ).
cnf(u5873,axiom,
e47 != select(sF30,sF100) ).
cnf(u14843,hypothesis,
e3 != select(sF51,sF100) ).
cnf(u967,hypothesis,
i33 != i19 ).
cnf(u15031,hypothesis,
sF101 = select(sF3,sF100) ).
cnf(u919,hypothesis,
i27 != i20 ).
cnf(u2313,hypothesis,
i23 != i2 ).
cnf(u2813,axiom,
( select(sF52,X0) = select(sF53,X0)
| i43 = X0 ) ).
cnf(u2331,hypothesis,
i14 != i2 ).
cnf(u2746,axiom,
e2 = select(sF86,i2) ).
cnf(u255,hypothesis,
i44 != i34 ).
cnf(u2137,hypothesis,
i18 != i4 ).
cnf(u2155,hypothesis,
i9 != i4 ).
cnf(u2699,axiom,
e39 = select(sF38,i39) ).
cnf(u419,hypothesis,
i32 != i30 ).
cnf(u431,hypothesis,
i46 != i29 ).
cnf(u975,hypothesis,
i29 != i19 ).
cnf(u2640,axiom,
store(sF92,i5,e5) = sF93 ).
cnf(u6105,axiom,
e47 != sF101 ).
cnf(u6114,hypothesis,
sF101 = select(sF35,sF100) ).
cnf(u317,hypothesis,
i46 != i32 ).
cnf(u2622,axiom,
store(sF83,i35,e35) = sF84 ).
cnf(u2419,hypothesis,
i18 != i1 ).
cnf(u487,hypothesis,
i39 != i28 ).
cnf(u13,hypothesis,
i48 != i47 ).
cnf(u11160,axiom,
sF102 != select(sF82,sF100) ).
cnf(u2830,axiom,
( select(sF69,X0) = select(sF70,X0)
| i9 = X0 ) ).
cnf(u2478,axiom,
store(sF11,i13,e13) = sF12 ).
cnf(u2729,axiom,
e33 = select(sF69,i33) ).
cnf(u549,hypothesis,
i30 != i27 ).
cnf(u69,hypothesis,
i45 != i42 ).
cnf(u15060,hypothesis,
e43 != select(sF1,sF100) ).
cnf(u2852,axiom,
( select(sF91,X0) = select(sF92,X0)
| i12 = X0 ) ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(u2087,hypothesis,
i43 != i4 ).
cnf(u2443,hypothesis,
i6 != i1 ).
cnf(u2097,hypothesis,
i38 != i4 ).
cnf(u781,hypothesis,
i39 != i22 ).
cnf(u2544,axiom,
store(sF44,i46,e46) = sF45 ).
cnf(u563,hypothesis,
i46 != i26 ).
cnf(u2249,hypothesis,
i8 != i3 ).
cnf(u2267,hypothesis,
i46 != i2 ).
cnf(u1085,hypothesis,
i37 != i17 ).
cnf(u605,hypothesis,
i49 != i25 ).
cnf(u14813,hypothesis,
e5 != select(sF52,sF100) ).
cnf(u795,hypothesis,
i32 != i22 ).
cnf(u2752,axiom,
e12 = select(sF92,i12) ).
cnf(u1317,hypothesis,
i23 != i14 ).
cnf(u361,hypothesis,
i42 != i31 ).
cnf(u2822,axiom,
( select(sF61,X0) = select(sF62,X0)
| i49 = X0 ) ).
cnf(u429,hypothesis,
i47 != i29 ).
cnf(u619,hypothesis,
i42 != i25 ).
cnf(u2844,axiom,
( select(sF83,X0) = select(sF84,X0)
| i35 = X0 ) ).
cnf(u1141,hypothesis,
i42 != i16 ).
cnf(u2734,axiom,
e18 = select(sF74,i18) ).
cnf(u307,hypothesis,
i34 != i33 ).
cnf(u14984,hypothesis,
e47 != select(sF5,sF100) ).
cnf(u253,hypothesis,
i45 != i34 ).
cnf(u1853,hypothesis,
i28 != i7 ).
cnf(u2209,hypothesis,
i28 != i3 ).
cnf(u837,hypothesis,
i39 != i21 ).
cnf(u485,hypothesis,
i40 != i28 ).
cnf(hyp0,hypothesis,
i49 != i50 ).
cnf(u2628,axiom,
store(sF86,i10,e10) = sF87 ).
cnf(u2375,hypothesis,
i40 != i1 ).
cnf(u1549,hypothesis,
i18 != i11 ).
cnf(u2385,hypothesis,
i35 != i1 ).
cnf(u661,hypothesis,
i46 != i24 ).
cnf(u851,hypothesis,
i32 != i21 ).
cnf(u1049,hypothesis,
i23 != i18 ).
cnf(u2199,hypothesis,
i33 != i3 ).
cnf(u1373,hypothesis,
i31 != i13 ).
cnf(u1021,hypothesis,
i37 != i18 ).
cnf(u1563,hypothesis,
i50 != i10 ).
cnf(u675,hypothesis,
i39 != i24 ).
cnf(u2085,hypothesis,
i44 != i4 ).
cnf(u1197,hypothesis,
i48 != i15 ).
cnf(u717,hypothesis,
i44 != i23 ).
cnf(u363,hypothesis,
i41 != i31 ).
cnf(u1585,hypothesis,
i39 != i10 ).
cnf(u1105,hypothesis,
i27 != i17 ).
cnf(u1909,hypothesis,
i43 != i6 ).
cnf(u1429,hypothesis,
i40 != i12 ).
cnf(u15056,hypothesis,
e47 != select(sF1,sF100) ).
cnf(u1075,hypothesis,
i42 != i17 ).
cnf(u2566,axiom,
store(sF55,i22,e22) = sF56 ).
cnf(u187,hypothesis,
i49 != i36 ).
cnf(u731,hypothesis,
i37 != i23 ).
cnf(u1281,hypothesis,
i41 != i14 ).
cnf(u14817,hypothesis,
e46 != select(sF52,sF100) ).
cnf(u2159,hypothesis,
i7 != i4 ).
cnf(u1605,hypothesis,
i29 != i10 ).
cnf(u1253,hypothesis,
i20 != i15 ).
cnf(u1795,hypothesis,
i15 != i8 ).
cnf(u2532,axiom,
store(sF38,i40,e40) = sF39 ).
cnf(u1641,hypothesis,
i11 != i10 ).
cnf(u2550,axiom,
store(sF47,i49,e49) = sF48 ).
cnf(u2588,axiom,
store(sF66,i15,e15) = sF67 ).
cnf(u9330,hypothesis,
e46 != select(sF8,sF100) ).
cnf(u1965,hypothesis,
i15 != i6 ).
cnf(u2801,axiom,
( select(sF39,X0) = select(sF40,X0)
| i41 = X0 ) ).
cnf(u2335,hypothesis,
i12 != i2 ).
cnf(u1619,hypothesis,
i22 != i10 ).
cnf(u243,hypothesis,
i50 != i34 ).
cnf(u14655,hypothesis,
sF102 != select(sF63,sF100) ).
cnf(u1817,hypothesis,
i46 != i7 ).
cnf(u1465,hypothesis,
i22 != i12 ).
cnf(u1543,hypothesis,
i21 != i11 ).
cnf(u1789,hypothesis,
i18 != i8 ).
cnf(u1307,hypothesis,
i28 != i14 ).
cnf(u1979,hypothesis,
i8 != i6 ).
cnf(u2703,axiom,
e43 = select(sF42,i43) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u963,hypothesis,
i35 != i19 ).
cnf(u2853,axiom,
( select(sF92,X0) = select(sF93,X0)
| i5 = X0 ) ).
cnf(u2373,hypothesis,
i41 != i1 ).
cnf(u1161,hypothesis,
i32 != i16 ).
cnf(u1847,hypothesis,
i31 != i7 ).
cnf(u1485,hypothesis,
i50 != i11 ).
cnf(u1131,hypothesis,
i47 != i16 ).
cnf(u1675,hypothesis,
i34 != i9 ).
cnf(u305,hypothesis,
i35 != i33 ).
cnf(u1873,hypothesis,
i18 != i7 ).
cnf(u1055,hypothesis,
i20 != i18 ).
cnf(u2677,axiom,
e17 = select(sF16,i17) ).
cnf(u2197,hypothesis,
i34 != i3 ).
cnf(u1363,hypothesis,
i36 != i13 ).
cnf(u537,hypothesis,
i36 != i27 ).
cnf(u475,hypothesis,
i45 != i28 ).
cnf(u1697,hypothesis,
i23 != i9 ).
cnf(u1217,hypothesis,
i38 != i15 ).
cnf(u1903,hypothesis,
i46 != i6 ).
cnf(u2021,hypothesis,
i31 != i5 ).
cnf(u1187,hypothesis,
i19 != i16 ).
cnf(u1731,hypothesis,
i47 != i8 ).
cnf(u2818,axiom,
( select(sF57,X0) = select(sF58,X0)
| i20 = X0 ) ).
cnf(u2466,axiom,
store(sF5,i7,e7) = sF6 ).
cnf(u2806,axiom,
( select(sF44,X0) = select(sF45,X0)
| i46 = X0 ) ).
cnf(u567,hypothesis,
i44 != i26 ).
cnf(u2492,axiom,
store(sF18,i20,e20) = sF19 ).
cnf(u1521,hypothesis,
i32 != i11 ).
cnf(u14941,hypothesis,
e50 != select(sF71,sF100) ).
cnf(u1727,hypothesis,
i49 != i8 ).
cnf(u2271,hypothesis,
i44 != i2 ).
cnf(u2035,hypothesis,
i24 != i5 ).
cnf(u185,hypothesis,
i50 != i36 ).
cnf(u1753,hypothesis,
i36 != i8 ).
cnf(u1287,hypothesis,
i38 != i14 ).
cnf(u2700,axiom,
e40 = select(sF39,i40) ).
cnf(u7089,hypothesis,
e3 != select(sF65,sF100) ).
cnf(u2447,hypothesis,
i4 != i1 ).
cnf(u1243,hypothesis,
i25 != i15 ).
cnf(u9442,hypothesis,
e24 != select(sF55,sF100) ).
cnf(u1929,hypothesis,
i33 != i6 ).
cnf(u14702,hypothesis,
sF101 = select(sF9,sF100) ).
cnf(u2307,hypothesis,
i26 != i2 ).
cnf(u1111,hypothesis,
i24 != i17 ).
cnf(u1783,hypothesis,
i21 != i8 ).
cnf(u2333,hypothesis,
i13 != i2 ).
cnf(u1419,hypothesis,
i45 != i12 ).
cnf(u593,hypothesis,
i31 != i26 ).
cnf(u241,hypothesis,
i36 != i35 ).
cnf(u799,hypothesis,
i30 != i22 ).
cnf(u5731,axiom,
e4 != select(sF82,sF100) ).
cnf(u6852,hypothesis,
e3 != select(sF68,sF100) ).
cnf(u2131,hypothesis,
i21 != i4 ).
cnf(u1959,hypothesis,
i18 != i6 ).
cnf(u2803,axiom,
( select(sF41,X0) = select(sF42,X0)
| i43 = X0 ) ).
cnf(u2157,hypothesis,
i8 != i4 ).
cnf(u417,hypothesis,
i33 != i30 ).
cnf(u1985,hypothesis,
i49 != i5 ).
cnf(u623,hypothesis,
i40 != i25 ).
cnf(u1167,hypothesis,
i29 != i16 ).
cnf(u2789,axiom,
( select(sF27,X0) = select(sF28,X0)
| i29 = X0 ) ).
cnf(u1681,hypothesis,
i31 != i9 ).
cnf(u1475,hypothesis,
i17 != i12 ).
cnf(u2722,axiom,
e49 = select(sF62,i49) ).
cnf(u9773,hypothesis,
e46 != select(sF53,sF100) ).
cnf(u311,hypothesis,
i49 != i32 ).
cnf(u14937,hypothesis,
e50 != select(sF73,sF100) ).
cnf(u1471,hypothesis,
i19 != i12 ).
cnf(u2015,hypothesis,
i34 != i5 ).
cnf(u953,hypothesis,
i40 != i19 ).
cnf(u473,hypothesis,
i46 != i28 ).
cnf(u7,hypothesis,
i49 != i48 ).
cnf(u679,hypothesis,
i37 != i24 ).
cnf(u2664,axiom,
e4 = select(sF3,i4) ).
cnf(u1527,hypothesis,
i29 != i11 ).
cnf(u2749,axiom,
e29 = select(sF89,i29) ).
cnf(u9720,hypothesis,
e46 != select(sF58,sF100) ).
cnf(u8874,hypothesis,
e43 != select(sF15,sF100) ).
cnf(u1009,hypothesis,
i43 != i18 ).
cnf(u14839,hypothesis,
e4 != select(sF51,sF100) ).
cnf(u2682,axiom,
e22 = select(sF21,i22) ).
cnf(u191,hypothesis,
i47 != i36 ).
cnf(u1223,hypothesis,
i35 != i15 ).
cnf(u2073,hypothesis,
i50 != i4 ).
cnf(u2445,hypothesis,
i5 != i1 ).
cnf(u2091,hypothesis,
i41 != i4 ).
cnf(u705,hypothesis,
i50 != i23 ).
cnf(u367,hypothesis,
i39 != i31 ).
cnf(u911,hypothesis,
i31 != i20 ).
cnf(u2576,axiom,
store(sF60,i8,e8) = sF61 ).
cnf(u2243,hypothesis,
i11 != i3 ).
cnf(u2269,hypothesis,
i45 != i2 ).
cnf(u735,hypothesis,
i35 != i23 ).
cnf(u423,hypothesis,
i50 != i29 ).
cnf(u2520,axiom,
store(sF32,i34,e34) = sF33 ).
cnf(u15102,hypothesis,
e24 != sF101 ).
cnf(u2538,axiom,
store(sF41,i43,e43) = sF42 ).
cnf(u247,hypothesis,
i48 != i34 ).
cnf(u2665,axiom,
e5 = select(sF4,i5) ).
cnf(u479,hypothesis,
i43 != i28 ).
cnf(u5,hypothesis,
i50 != i48 ).
cnf(u2841,axiom,
( select(sF80,X0) = select(sF81,X0)
| i23 = X0 ) ).
cnf(u2379,hypothesis,
i38 != i1 ).
cnf(u2794,axiom,
( select(sF32,X0) = select(sF33,X0)
| i34 = X0 ) ).
cnf(u309,hypothesis,
i50 != i32 ).
cnf(u2185,hypothesis,
i40 != i3 ).
cnf(u2203,hypothesis,
i31 != i3 ).
cnf(u541,hypothesis,
i34 != i27 ).
cnf(u15058,hypothesis,
e33 != select(sF1,sF100) ).
cnf(u2688,axiom,
e28 = select(sF27,i28) ).
cnf(u6531,hypothesis,
e3 != select(sF72,sF100) ).
cnf(u15054,hypothesis,
e46 != select(sF1,sF100) ).
cnf(u365,hypothesis,
i40 != i31 ).
cnf(u1399,hypothesis,
i18 != i13 ).
cnf(u555,hypothesis,
i50 != i26 ).
cnf(u2480,axiom,
store(sF12,i14,e14) = sF13 ).
cnf(u15110,hypothesis,
e5 != sF101 ).
cnf(u1077,hypothesis,
i41 != i17 ).
cnf(u2670,axiom,
e10 = select(sF9,i10) ).
cnf(u189,hypothesis,
i48 != i36 ).
cnf(u6666,hypothesis,
sF101 = select(sF25,sF100) ).
cnf(u2145,hypothesis,
i14 != i4 ).
cnf(u15076,hypothesis,
e5 != select(sF50,sF100) ).
cnf(u773,hypothesis,
i43 != i22 ).
cnf(u421,hypothesis,
i31 != i30 ).
cnf(u2526,axiom,
store(sF35,i37,e37) = sF36 ).
cnf(u2564,axiom,
store(sF54,i19,e19) = sF55 ).
cnf(u2777,axiom,
( select(sF15,X0) = select(sF16,X0)
| i17 = X0 ) ).
cnf(u1455,hypothesis,
i27 != i12 ).
cnf(u2311,hypothesis,
i24 != i2 ).
cnf(u2321,hypothesis,
i19 != i2 ).
cnf(u597,hypothesis,
i29 != i26 ).
cnf(u245,hypothesis,
i49 != i34 ).
cnf(u787,hypothesis,
i36 != i22 ).
cnf(u2135,hypothesis,
i19 != i4 ).
cnf(u9049,hypothesis,
e4 != select(sF61,sF100) ).
cnf(u2807,axiom,
( select(sF45,X0) = select(sF46,X0)
| i47 = X0 ) ).
cnf(u1309,hypothesis,
i27 != i14 ).
cnf(u8231,hypothesis,
e33 != select(sF38,sF100) ).
cnf(u957,hypothesis,
i38 != i19 ).
cnf(u611,hypothesis,
i46 != i25 ).
cnf(u1133,hypothesis,
i46 != i16 ).
cnf(u653,hypothesis,
i50 != i24 ).
cnf(u299,hypothesis,
i38 != i33 ).
cnf(u7192,hypothesis,
e46 != select(sF19,sF100) ).
cnf(u843,hypothesis,
i36 != i21 ).
cnf(u15098,hypothesis,
e50 != select(sF50,sF100) ).
cnf(u5861,hypothesis,
e3 != select(sF80,sF100) ).
cnf(u1845,hypothesis,
i32 != i7 ).
cnf(u1365,hypothesis,
i35 != i13 ).
cnf(u477,hypothesis,
i44 != i28 ).
cnf(u123,hypothesis,
i45 != i39 ).
cnf(u667,hypothesis,
i43 != i24 ).
cnf(u9314,hypothesis,
e24 != select(sF58,sF100) ).
cnf(u2095,hypothesis,
i39 != i4 ).
cnf(u1541,hypothesis,
i22 != i11 ).
cnf(u1189,hypothesis,
i18 != i16 ).
cnf(u2782,axiom,
( select(sF20,X0) = select(sF21,X0)
| i22 = X0 ) ).
cnf(u779,hypothesis,
i40 != i22 ).
cnf(u15036,hypothesis,
e46 != select(sF2,sF100) ).
cnf(u355,hypothesis,
i45 != i31 ).
cnf(u2468,axiom,
store(sF6,i8,e8) = sF7 ).
cnf(u2486,axiom,
store(sF15,i17,e17) = sF16 ).
cnf(u1041,hypothesis,
i27 != i18 ).
cnf(u1901,hypothesis,
i47 != i6 ).
cnf(u2737,axiom,
e11 = select(sF77,i11) ).
cnf(u2257,hypothesis,
i4 != i3 ).
cnf(u1013,hypothesis,
i41 != i18 ).
cnf(u8564,hypothesis,
e33 != select(sF32,sF100) ).
cnf(u1555,hypothesis,
i15 != i11 ).
cnf(u179,hypothesis,
i40 != i37 ).
cnf(u723,hypothesis,
i41 != i23 ).
cnf(u1401,hypothesis,
i17 != i13 ).
cnf(u1725,hypothesis,
i50 != i8 ).
cnf(u2433,hypothesis,
i11 != i1 ).
cnf(u1915,hypothesis,
i40 != i6 ).
cnf(u709,hypothesis,
i48 != i23 ).
cnf(u899,hypothesis,
i37 != i20 ).
cnf(u1577,hypothesis,
i43 != i10 ).
cnf(u1097,hypothesis,
i31 != i17 ).
cnf(u2247,hypothesis,
i9 != i3 ).
cnf(u1421,hypothesis,
i44 != i12 ).
cnf(u1067,hypothesis,
i46 != i17 ).
cnf(u1611,hypothesis,
i26 != i10 ).
cnf(u1809,hypothesis,
i50 != i7 ).
cnf(u2133,hypothesis,
i20 != i4 ).
cnf(u1299,hypothesis,
i32 != i14 ).
cnf(u1245,hypothesis,
i24 != i15 ).
cnf(u6257,axiom,
e47 != select(sF27,sF100) ).
cnf(u411,hypothesis,
i36 != i30 ).
cnf(u1633,hypothesis,
i15 != i10 ).
cnf(u1153,hypothesis,
i36 != i16 ).
cnf(u1839,hypothesis,
i35 != i7 ).
cnf(u1957,hypothesis,
i19 != i6 ).
cnf(u1477,hypothesis,
i16 != i12 ).
cnf(u1123,hypothesis,
i18 != i17 ).
cnf(u297,hypothesis,
i39 != i33 ).
cnf(u2742,axiom,
e25 = select(sF82,i25) ).
cnf(u235,hypothesis,
i39 != i35 ).
cnf(u1457,hypothesis,
i26 != i12 ).
cnf(u1663,hypothesis,
i40 != i9 ).
cnf(u2207,hypothesis,
i29 != i3 ).
cnf(u1781,hypothesis,
i22 != i8 ).
cnf(u1971,hypothesis,
i12 != i6 ).
cnf(u467,hypothesis,
i49 != i28 ).
cnf(u2796,axiom,
( select(sF34,X0) = select(sF35,X0)
| i36 = X0 ) ).
cnf(u121,hypothesis,
i46 != i39 ).
cnf(u5544,axiom,
sF102 = select(sF86,sF100) ).
cnf(u1689,hypothesis,
i27 != i9 ).
cnf(u2636,axiom,
store(sF90,i37,e37) = sF91 ).
cnf(u2013,hypothesis,
i35 != i5 ).
cnf(u2383,hypothesis,
i36 != i1 ).
cnf(u1667,hypothesis,
i38 != i9 ).
cnf(u8870,hypothesis,
e47 != select(sF15,sF100) ).
cnf(u1865,hypothesis,
i22 != i7 ).
cnf(u1513,hypothesis,
i36 != i11 ).
cnf(u1047,hypothesis,
i24 != i18 ).
cnf(u1719,hypothesis,
i12 != i9 ).
cnf(u1355,hypothesis,
i40 != i13 ).
cnf(u2027,hypothesis,
i28 != i5 ).
cnf(u529,hypothesis,
i40 != i27 ).
cnf(u177,hypothesis,
i41 != i37 ).
cnf(u9752,hypothesis,
e46 != select(sF55,sF100) ).
cnf(u2067,hypothesis,
i8 != i5 ).
cnf(u1895,hypothesis,
i50 != i6 ).
cnf(u6850,hypothesis,
e5 != select(sF68,sF100) ).
cnf(u2093,hypothesis,
i40 != i4 ).
cnf(u5709,axiom,
e47 != select(sF35,sF100) ).
cnf(u6545,hypothesis,
e24 != select(sF71,sF100) ).
cnf(u1179,hypothesis,
i23 != i16 ).
cnf(u353,hypothesis,
i46 != i31 ).
cnf(u1921,hypothesis,
i37 != i6 ).
cnf(u559,hypothesis,
i48 != i26 ).
cnf(u1103,hypothesis,
i28 != i17 ).
cnf(u2725,axiom,
e6 = select(sF65,i6) ).
cnf(u2245,hypothesis,
i10 != i3 ).
cnf(u1411,hypothesis,
i49 != i12 ).
cnf(u585,hypothesis,
i35 != i26 ).
cnf(u1745,hypothesis,
i40 != i8 ).
cnf(u1407,hypothesis,
i14 != i13 ).
cnf(u1951,hypothesis,
i22 != i6 ).
cnf(u14815,hypothesis,
e3 != select(sF52,sF100) ).
cnf(u2739,axiom,
e44 = select(sF79,i44) ).
cnf(u1235,hypothesis,
i29 != i15 ).
cnf(u889,hypothesis,
i42 != i20 ).
cnf(u409,hypothesis,
i37 != i30 ).
cnf(u2514,axiom,
store(sF29,i31,e31) = sF30 ).
cnf(u615,hypothesis,
i44 != i25 ).
cnf(u2540,axiom,
store(sF42,i44,e44) = sF43 ).
cnf(u2738,axiom,
e36 = select(sF78,i36) ).
cnf(u9320,hypothesis,
e3 != select(sF58,sF100) ).
cnf(u1775,hypothesis,
i25 != i8 ).
cnf(u233,hypothesis,
i40 != i35 ).
cnf(u791,hypothesis,
i34 != i22 ).
cnf(u1463,hypothesis,
i23 != i12 ).
cnf(u2685,axiom,
e25 = select(sF24,i25) ).
cnf(u945,hypothesis,
i44 != i19 ).
cnf(u2618,axiom,
store(sF81,i25,e25) = sF82 ).
cnf(u2578,axiom,
store(sF61,i49,e49) = sF62 ).
cnf(u127,hypothesis,
i43 != i39 ).
cnf(u1159,hypothesis,
i33 != i16 ).
cnf(u2861,axiom,
( select(sF0,X0) = select(sF50,X0)
| i1 = X0
| i41 = X0 ) ).
cnf(u2381,hypothesis,
i37 != i1 ).
cnf(u14687,hypothesis,
sF101 = select(sF10,sF100) ).
cnf(u641,hypothesis,
i31 != i25 ).
cnf(u303,hypothesis,
i36 != i33 ).
cnf(u847,hypothesis,
i34 != i21 ).
cnf(u2179,hypothesis,
i43 != i3 ).
cnf(u2007,hypothesis,
i38 != i5 ).
cnf(u2205,hypothesis,
i30 != i3 ).
cnf(u465,hypothesis,
i50 != i28 ).
cnf(u671,hypothesis,
i41 != i24 ).
cnf(u2848,axiom,
( select(sF87,X0) = select(sF88,X0)
| i48 = X0 ) ).
cnf(u2712,axiom,
e45 = select(sF52,i45) ).
cnf(u2770,axiom,
( select(sF8,X0) = select(sF9,X0)
| i10 = X0 ) ).
cnf(u359,hypothesis,
i43 != i31 ).
cnf(u2456,axiom,
store(sF0,i2,e2) = sF1 ).
cnf(u2474,axiom,
store(sF9,i11,e11) = sF10 ).
cnf(u1519,hypothesis,
i33 != i11 ).
cnf(u1001,hypothesis,
i47 != i18 ).
cnf(u183,hypothesis,
i38 != i37 ).
cnf(u727,hypothesis,
i39 != i23 ).
cnf(u14809,hypothesis,
e24 != select(sF52,sF100) ).
cnf(u2211,hypothesis,
i27 != i3 ).
cnf(u6608,hypothesis,
sF101 = select(sF30,sF100) ).
cnf(u8922,hypothesis,
e46 != select(sF13,sF100) ).
cnf(u903,hypothesis,
i35 != i20 ).
cnf(u15038,hypothesis,
e47 != select(sF2,sF100) ).
cnf(u2425,hypothesis,
i15 != i1 ).
cnf(u2797,axiom,
( select(sF35,X0) = select(sF36,X0)
| i37 = X0 ) ).
cnf(u2315,hypothesis,
i22 != i2 ).
cnf(u2730,axiom,
e9 = select(sF70,i9) ).
cnf(u239,hypothesis,
i37 != i35 ).
cnf(u2121,hypothesis,
i26 != i4 ).
cnf(u15052,hypothesis,
e50 != select(sF52,sF100) ).
cnf(u9553,hypothesis,
e5 != select(sF53,sF100) ).
cnf(u2139,hypothesis,
i17 != i4 ).
cnf(u2811,axiom,
( select(sF50,X0) = select(sF51,X0)
| i30 = X0 ) ).
cnf(u415,hypothesis,
i34 != i30 ).
cnf(u2624,axiom,
store(sF84,i50,e50) = sF85 ).
cnf(u521,hypothesis,
i44 != i27 ).
cnf(u301,hypothesis,
i37 != i33 ).
cnf(u2606,axiom,
store(sF75,i34,e34) = sF76 ).
cnf(u471,hypothesis,
i47 != i28 ).
cnf(u15016,hypothesis,
e50 != select(sF54,sF100) ).
cnf(u125,hypothesis,
i44 != i39 ).
cnf(u663,hypothesis,
i45 != i24 ).
cnf(u357,hypothesis,
i44 != i31 ).
cnf(u2462,axiom,
store(sF3,i5,e5) = sF4 ).
cnf(u15074,hypothesis,
e4 != select(sF50,sF100) ).
cnf(u2713,axiom,
e43 = select(sF53,i43) ).
cnf(u533,hypothesis,
i38 != i27 ).
cnf(u181,hypothesis,
i39 != i37 ).
cnf(u2836,axiom,
( select(sF75,X0) = select(sF76,X0)
| i34 = X0 ) ).
cnf(u2071,hypothesis,
i6 != i5 ).
cnf(u2743,axiom,
e46 = select(sF83,i46) ).
cnf(u2081,hypothesis,
i46 != i4 ).
cnf(u893,hypothesis,
i40 != i20 ).
cnf(u2528,axiom,
store(sF36,i38,e38) = sF37 ).
cnf(u547,hypothesis,
i31 != i27 ).
cnf(u2251,hypothesis,
i7 != i3 ).
cnf(u1069,hypothesis,
i45 != i17 ).
cnf(u589,hypothesis,
i33 != i26 ).
cnf(u1301,hypothesis,
i31 != i14 ).
cnf(u7085,hypothesis,
e4 != select(sF65,sF100) ).
cnf(u413,hypothesis,
i35 != i30 ).
cnf(u6614,hypothesis,
sF101 = select(sF29,sF100) ).
cnf(u59,hypothesis,
i50 != i42 ).
cnf(u603,hypothesis,
i50 != i25 ).
cnf(u2849,axiom,
( select(sF88,X0) = select(sF89,X0)
| i29 = X0 ) ).
cnf(u6527,hypothesis,
e4 != select(sF72,sF100) ).
cnf(u1125,hypothesis,
i50 != i16 ).
cnf(u2718,axiom,
e20 = select(sF58,i20) ).
cnf(u291,hypothesis,
i42 != i33 ).
cnf(u237,hypothesis,
i38 != i35 ).
cnf(u5735,axiom,
e3 != select(sF82,sF100) ).
cnf(u1837,hypothesis,
i36 != i7 ).
cnf(u2673,axiom,
e13 = select(sF12,i13) ).
cnf(u2193,hypothesis,
i36 != i3 ).
cnf(u949,hypothesis,
i42 != i19 ).
cnf(u469,hypothesis,
i48 != i28 ).
cnf(u115,hypothesis,
i49 != i39 ).
cnf(u13730,hypothesis,
sF101 = select(sF15,sF100) ).
cnf(u2740,axiom,
e38 = select(sF80,i38) ).
cnf(u1337,hypothesis,
i49 != i13 ).
cnf(u1661,hypothesis,
i41 != i9 ).
cnf(u2369,hypothesis,
i43 != i1 ).
cnf(u1851,hypothesis,
i29 != i7 ).
cnf(u645,hypothesis,
i29 != i25 ).
cnf(u835,hypothesis,
i40 != i21 ).
cnf(u1033,hypothesis,
i31 != i18 ).
cnf(u2183,hypothesis,
i41 != i3 ).
cnf(u9222,hypothesis,
e47 != select(sF10,sF100) ).
cnf(u1357,hypothesis,
i39 != i13 ).
cnf(u1005,hypothesis,
i45 != i18 ).
cnf(u1547,hypothesis,
i19 != i11 ).
cnf(u711,hypothesis,
i47 != i23 ).
cnf(u659,hypothesis,
i47 != i24 ).
cnf(u2069,hypothesis,
i7 != i5 ).
cnf(u8639,hypothesis,
e33 != select(sF26,sF100) ).
cnf(u14919,axiom,
( select(sF84,X0) = select(sF85,X0)
| sF100 = X0 ) ).
cnf(u1181,hypothesis,
i22 != i16 ).
cnf(u347,hypothesis,
i49 != i31 ).
cnf(u1019,hypothesis,
i38 != i18 ).
cnf(u1569,hypothesis,
i47 != i10 ).
cnf(u1089,hypothesis,
i35 != i17 ).
cnf(u1893,hypothesis,
i8 != i7 ).
cnf(u1413,hypothesis,
i48 != i12 ).
cnf(u1059,hypothesis,
i50 != i17 ).
cnf(u2850,axiom,
( select(sF89,X0) = select(sF90,X0)
| i3 = X0 ) ).
cnf(u2678,axiom,
e18 = select(sF17,i18) ).
cnf(u171,hypothesis,
i44 != i37 ).
cnf(u715,hypothesis,
i45 != i23 ).
cnf(u1393,hypothesis,
i21 != i13 ).
cnf(u6848,hypothesis,
e4 != select(sF68,sF100) ).
cnf(u1599,hypothesis,
i32 != i10 ).
cnf(u2143,hypothesis,
i15 != i4 ).
cnf(u1717,hypothesis,
i13 != i9 ).
cnf(u1237,hypothesis,
i28 != i15 ).
cnf(u1907,hypothesis,
i44 != i6 ).
cnf(u403,hypothesis,
i40 != i30 ).
cnf(u2516,axiom,
store(sF30,i32,e32) = sF31 ).
cnf(u8926,hypothesis,
e33 != select(sF13,sF100) ).
cnf(u57,hypothesis,
i44 != i43 ).
cnf(u1625,hypothesis,
i19 != i10 ).
cnf(u2534,axiom,
store(sF39,i41,e41) = sF40 ).
cnf(u2572,axiom,
store(sF58,i40,e40) = sF59 ).
cnf(u6525,hypothesis,
e24 != select(sF72,sF100) ).
cnf(u1949,hypothesis,
i23 != i6 ).
cnf(u2785,axiom,
( select(sF23,X0) = select(sF24,X0)
| i25 = X0 ) ).
cnf(u2319,hypothesis,
i20 != i2 ).
cnf(u1313,hypothesis,
i25 != i14 ).
cnf(u8612,hypothesis,
e33 != select(sF28,sF100) ).
cnf(u1603,hypothesis,
i30 != i10 ).
cnf(u227,hypothesis,
i43 != i35 ).
cnf(u1801,hypothesis,
i12 != i8 ).
cnf(u1449,hypothesis,
i30 != i12 ).
cnf(u1655,hypothesis,
i44 != i9 ).
cnf(u1773,hypothesis,
i26 != i8 ).
cnf(u1291,hypothesis,
i36 != i14 ).
cnf(u1963,hypothesis,
i16 != i6 ).
cnf(u2815,axiom,
( select(sF54,X0) = select(sF55,X0)
| i19 = X0 ) ).
cnf(u113,hypothesis,
i50 != i39 ).
cnf(u2837,axiom,
( select(sF76,X0) = select(sF77,X0)
| i11 = X0 ) ).
cnf(u1273,hypothesis,
i45 != i14 ).
cnf(u1831,hypothesis,
i39 != i7 ).
cnf(u1115,hypothesis,
i22 != i17 ).
cnf(u1787,hypothesis,
i19 != i8 ).
cnf(u289,hypothesis,
i43 != i33 ).
cnf(u1857,hypothesis,
i26 != i7 ).
cnf(u1039,hypothesis,
i28 != i18 ).
cnf(u2661,axiom,
e41 = select(sF50,i41) ).
cnf(u2181,hypothesis,
i42 != i3 ).
cnf(u2851,axiom,
( select(sF90,X0) = select(sF91,X0)
| i37 = X0 ) ).
cnf(u1347,hypothesis,
i44 != i13 ).
cnf(u2594,axiom,
store(sF69,i9,e9) = sF70 ).
cnf(u9556,hypothesis,
e3 != select(sF53,sF100) ).
cnf(u459,hypothesis,
i32 != i29 ).
cnf(u2812,axiom,
( select(sF51,X0) = select(sF52,X0)
| i45 = X0 ) ).
cnf(u1343,hypothesis,
i46 != i13 ).
cnf(u1887,hypothesis,
i11 != i7 ).
cnf(u2005,hypothesis,
i39 != i5 ).
cnf(u2675,axiom,
e15 = select(sF14,i15) ).
cnf(u1171,hypothesis,
i27 != i16 ).
cnf(u825,hypothesis,
i45 != i21 ).
cnf(u345,hypothesis,
i50 != i31 ).
cnf(u2790,axiom,
( select(sF28,X0) = select(sF29,X0)
| i30 = X0 ) ).
cnf(u551,hypothesis,
i29 != i27 ).
cnf(u2476,axiom,
store(sF10,i12,e12) = sF11 ).
cnf(u707,hypothesis,
i49 != i23 ).
cnf(u1505,hypothesis,
i40 != i11 ).
cnf(u1711,hypothesis,
i16 != i9 ).
cnf(u2255,hypothesis,
i5 != i3 ).
cnf(u2019,hypothesis,
i32 != i5 ).
cnf(u169,hypothesis,
i45 != i37 ).
cnf(u1737,hypothesis,
i44 != i8 ).
cnf(u2824,axiom,
( select(sF63,X0) = select(sF64,X0)
| i13 = X0 ) ).
cnf(u1227,hypothesis,
i33 != i15 ).
cnf(u6255,axiom,
e46 != select(sF27,sF100) ).
cnf(u881,hypothesis,
i46 != i20 ).
cnf(u63,hypothesis,
i48 != i42 ).
cnf(u2041,hypothesis,
i21 != i5 ).
cnf(u1095,hypothesis,
i32 != i17 ).
cnf(u1767,hypothesis,
i29 != i8 ).
cnf(u2317,hypothesis,
i21 != i2 ).
cnf(u1531,hypothesis,
i27 != i11 ).
cnf(u577,hypothesis,
i39 != i26 ).
cnf(u225,hypothesis,
i44 != i35 ).
cnf(u783,hypothesis,
i38 != i22 ).
cnf(u5561,axiom,
e3 != sF102 ).
cnf(u2115,hypothesis,
i29 != i4 ).
cnf(u1943,hypothesis,
i26 != i6 ).
cnf(u2787,axiom,
( select(sF25,X0) = select(sF26,X0)
| i27 = X0 ) ).
cnf(u2141,hypothesis,
i16 != i4 ).
cnf(u401,hypothesis,
i41 != i30 ).
cnf(u607,hypothesis,
i48 != i25 ).
cnf(u15106,hypothesis,
e4 != sF101 ).
cnf(u1279,hypothesis,
i42 != i14 ).
cnf(u2773,axiom,
( select(sF11,X0) = select(sF12,X0)
| i13 = X0 ) ).
cnf(u761,hypothesis,
i49 != i22 ).
cnf(u295,hypothesis,
i40 != i33 ).
cnf(u9312,hypothesis,
e43 != select(sF9,sF100) ).
cnf(u1999,hypothesis,
i42 != i5 ).
cnf(u6773,hypothesis,
sF101 = select(sF21,sF100) ).
cnf(u937,hypothesis,
i48 != i19 ).
cnf(u457,hypothesis,
i33 != i29 ).
cnf(u119,hypothesis,
i47 != i39 ).
cnf(u2728,axiom,
e7 = select(sF68,i7) ).
cnf(u2626,axiom,
store(sF85,i2,e2) = sF86 ).
cnf(u8858,hypothesis,
e33 != select(sF16,sF100) ).
cnf(u839,hypothesis,
i38 != i21 ).
cnf(u1511,hypothesis,
i37 != i11 ).
cnf(u2361,hypothesis,
i47 != i1 ).
cnf(u2733,axiom,
e47 = select(sF73,i47) ).
cnf(u993,hypothesis,
i20 != i19 ).
cnf(u2666,axiom,
e6 = select(sF5,i6) ).
cnf(u175,hypothesis,
i42 != i37 ).
cnf(u2057,hypothesis,
i13 != i5 ).
cnf(u2075,hypothesis,
i49 != i4 ).
cnf(u2747,axiom,
e10 = select(sF87,i10) ).
cnf(u6543,axiom,
e47 != select(sF22,sF100) ).
cnf(u351,hypothesis,
i47 != i31 ).
cnf(u1023,hypothesis,
i36 != i18 ).
cnf(u2560,axiom,
store(sF52,i43,e43) = sF53 ).
cnf(u697,hypothesis,
i28 != i24 ).
cnf(u14974,hypothesis,
e50 != select(sF59,sF100) ).
cnf(u2253,hypothesis,
i6 != i3 ).
cnf(u8544,hypothesis,
e33 != select(sF34,sF100) ).
cnf(u719,hypothesis,
i43 != i23 ).
cnf(u9424,hypothesis,
e3 != select(sF56,sF100) ).
cnf(u14841,hypothesis,
e5 != select(sF51,sF100) ).
cnf(u407,hypothesis,
i38 != i30 ).
cnf(u2504,axiom,
store(sF24,i26,e26) = sF25 ).
cnf(u61,hypothesis,
i49 != i42 ).
cnf(u2522,axiom,
store(sF33,i35,e35) = sF34 ).
cnf(u14948,hypothesis,
e50 != select(sF68,sF100) ).
cnf(u293,hypothesis,
i41 != i33 ).
cnf(u231,hypothesis,
i41 != i35 ).
cnf(u463,hypothesis,
i30 != i29 ).
cnf(u117,hypothesis,
i48 != i39 ).
cnf(u2825,axiom,
( select(sF64,X0) = select(sF65,X0)
| i6 = X0 ) ).
cnf(u2679,axiom,
e19 = select(sF18,i19) ).
cnf(u2809,axiom,
( select(sF47,X0) = select(sF48,X0)
| i49 = X0 ) ).
cnf(u2778,axiom,
( select(sF16,X0) = select(sF17,X0)
| i18 = X0 ) ).
cnf(u9741,hypothesis,
e46 != select(sF56,sF100) ).
cnf(u8569,hypothesis,
e33 != select(sF31,sF100) ).
cnf(u9334,hypothesis,
e33 != select(sF8,sF100) ).
cnf(u2297,hypothesis,
i31 != i2 ).
cnf(u2855,axiom,
( select(sF94,X0) = select(sF95,X0)
| i4 = X0 ) ).
cnf(u2187,hypothesis,
i39 != i3 ).
cnf(u525,hypothesis,
i42 != i27 ).
cnf(u2800,axiom,
( select(sF38,X0) = select(sF39,X0)
| i40 = X0 ) ).
cnf(u5733,axiom,
e5 != select(sF82,sF100) ).
cnf(u6541,axiom,
e46 != select(sF22,sF100) ).
cnf(u829,hypothesis,
i43 != i21 ).
cnf(u349,hypothesis,
i48 != i31 ).
cnf(u539,hypothesis,
i35 != i27 ).
cnf(u2464,axiom,
store(sF4,i6,e6) = sF5 ).
cnf(u1061,hypothesis,
i49 != i17 ).
cnf(u2654,axiom,
sk(sF49,sF99) = sF100 ).
cnf(u14908,axiom,
e50 = select(sF85,sF100) ).
cnf(u173,hypothesis,
i43 != i37 ).
cnf(u14913,axiom,
e50 = sF102 ).
cnf(u2129,hypothesis,
i22 != i4 ).
cnf(u8625,hypothesis,
e33 != select(sF27,sF100) ).
cnf(u885,hypothesis,
i44 != i20 ).
cnf(u405,hypothesis,
i39 != i30 ).
cnf(u2510,axiom,
store(sF27,i29,e29) = sF28 ).
cnf(u51,hypothesis,
i47 != i43 ).
cnf(u2676,axiom,
e16 = select(sF15,i16) ).
cnf(u2761,axiom,
( select(a1,X0) = select(sF50,X0)
| i41 = X0 ) ).
cnf(u2423,hypothesis,
i16 != i1 ).
cnf(u281,hypothesis,
i47 != i33 ).
cnf(u107,hypothesis,
i43 != i40 ).
cnf(u1597,hypothesis,
i33 != i10 ).
cnf(u2305,hypothesis,
i27 != i2 ).
cnf(u14953,hypothesis,
e50 != select(sF66,sF100) ).
cnf(u15078,hypothesis,
e3 != select(sF50,sF100) ).
cnf(u581,hypothesis,
i37 != i26 ).
cnf(u229,hypothesis,
i42 != i35 ).
cnf(u771,hypothesis,
i44 != i22 ).
cnf(u2119,hypothesis,
i27 != i4 ).
cnf(u2791,axiom,
( select(sF29,X0) = select(sF30,X0)
| i31 = X0 ) ).
cnf(u1293,hypothesis,
i35 != i14 ).
cnf(u941,hypothesis,
i46 != i19 ).
cnf(u595,hypothesis,
i30 != i26 ).
cnf(u1117,hypothesis,
i21 != i17 ).
cnf(u765,hypothesis,
i47 != i22 ).
cnf(u283,hypothesis,
i46 != i33 ).
cnf(u955,hypothesis,
i39 != i19 ).
cnf(u1025,hypothesis,
i35 != i18 ).
cnf(u1829,hypothesis,
i40 != i7 ).
cnf(u1349,hypothesis,
i43 != i13 ).
cnf(u9550,hypothesis,
e4 != select(sF53,sF100) ).
cnf(u461,hypothesis,
i31 != i29 ).
cnf(u2614,axiom,
store(sF79,i38,e38) = sF80 ).
cnf(u651,hypothesis,
i26 != i25 ).
cnf(u1329,hypothesis,
i17 != i14 ).
cnf(u2079,hypothesis,
i47 != i4 ).
cnf(u1653,hypothesis,
i45 != i9 ).
cnf(u1173,hypothesis,
i26 != i16 ).
cnf(u2766,axiom,
( select(sF4,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u1843,hypothesis,
i33 != i7 ).
cnf(u339,hypothesis,
i35 != i32 ).
cnf(u2470,axiom,
store(sF7,i9,e9) = sF8 ).
cnf(u1885,hypothesis,
i12 != i7 ).
cnf(u2721,axiom,
e8 = select(sF61,i8) ).
cnf(u2241,hypothesis,
i12 != i3 ).
cnf(u997,hypothesis,
i49 != i18 ).
cnf(u2840,axiom,
( select(sF79,X0) = select(sF80,X0)
| i38 = X0 ) ).
cnf(u1539,hypothesis,
i23 != i11 ).
cnf(u163,hypothesis,
i48 != i37 ).
cnf(u2788,axiom,
( select(sF26,X0) = select(sF27,X0)
| i28 = X0 ) ).
cnf(u1385,hypothesis,
i25 != i13 ).
cnf(u1591,hypothesis,
i36 != i10 ).
cnf(u1709,hypothesis,
i17 != i9 ).
cnf(u6108,hypothesis,
sF101 = select(sF36,sF100) ).
cnf(u1899,hypothesis,
i48 != i6 ).
cnf(u2751,axiom,
e37 = select(sF91,i37) ).
cnf(u1011,hypothesis,
i42 != i18 ).
cnf(u1561,hypothesis,
i12 != i11 ).
cnf(u2421,hypothesis,
i17 != i1 ).
cnf(u1209,hypothesis,
i42 != i15 ).
cnf(u161,hypothesis,
i49 != i37 ).
cnf(u1533,hypothesis,
i26 != i11 ).
cnf(u1051,hypothesis,
i22 != i18 ).
cnf(u1723,hypothesis,
i10 != i9 ).
cnf(u219,hypothesis,
i47 != i35 ).
cnf(u1793,hypothesis,
i16 != i8 ).
cnf(u2117,hypothesis,
i28 != i4 ).
cnf(u1283,hypothesis,
i40 != i14 ).
cnf(u1229,hypothesis,
i32 != i15 ).
cnf(u395,hypothesis,
i44 != i30 ).
cnf(u49,hypothesis,
i48 != i43 ).
cnf(u1617,hypothesis,
i23 != i10 ).
cnf(u1265,hypothesis,
i49 != i14 ).
cnf(u1823,hypothesis,
i43 != i7 ).
cnf(u9306,hypothesis,
e46 != select(sF9,sF100) ).
cnf(u1941,hypothesis,
i27 != i6 ).
cnf(u1107,hypothesis,
i26 != i17 ).
cnf(u2726,axiom,
e27 = select(sF66,i27) ).
cnf(u6749,hypothesis,
sF101 = select(sF23,sF100) ).
cnf(u1441,hypothesis,
i34 != i12 ).
cnf(u1647,hypothesis,
i48 != i9 ).
cnf(u2191,hypothesis,
i37 != i3 ).
cnf(u1765,hypothesis,
i30 != i8 ).
cnf(u1955,hypothesis,
i20 != i6 ).
cnf(u451,hypothesis,
i36 != i29 ).
cnf(u105,hypothesis,
i44 != i40 ).
cnf(u1673,hypothesis,
i35 != i9 ).
cnf(u6547,hypothesis,
e4 != select(sF71,sF100) ).
cnf(u1335,hypothesis,
i50 != i13 ).
cnf(u2748,axiom,
e48 = select(sF88,i48) ).
cnf(u1997,hypothesis,
i43 != i5 ).
cnf(u817,hypothesis,
i49 != i21 ).
cnf(u1779,hypothesis,
i23 != i8 ).
cnf(u1977,hypothesis,
i9 != i6 ).
cnf(u1497,hypothesis,
i44 != i11 ).
cnf(u2355,hypothesis,
i50 != i1 ).
cnf(u1031,hypothesis,
i32 != i18 ).
cnf(u1703,hypothesis,
i20 != i9 ).
cnf(u1467,hypothesis,
i21 != i12 ).
cnf(u14504,hypothesis,
sF102 != select(sF80,sF100) ).
cnf(u2011,hypothesis,
i36 != i5 ).
cnf(u513,hypothesis,
i48 != i27 ).
cnf(u2051,hypothesis,
i16 != i5 ).
cnf(u1879,hypothesis,
i15 != i7 ).
cnf(u2077,hypothesis,
i48 != i4 ).
cnf(u1163,hypothesis,
i31 != i16 ).
cnf(u337,hypothesis,
i36 != i32 ).
cnf(u2033,hypothesis,
i25 != i5 ).
cnf(u543,hypothesis,
i33 != i27 ).
cnf(u1215,hypothesis,
i39 != i15 ).
cnf(u2709,axiom,
e49 = select(sF48,i49) ).
cnf(u15034,hypothesis,
e50 != select(sF53,sF100) ).
cnf(u1523,hypothesis,
i31 != i11 ).
cnf(u2642,axiom,
store(sF93,i32,e32) = sF94 ).
cnf(u13697,hypothesis,
sF101 = select(sF17,sF100) ).
cnf(u1729,hypothesis,
i48 != i8 ).
cnf(u1391,hypothesis,
i22 != i13 ).
cnf(u1935,hypothesis,
i30 != i6 ).
cnf(u9418,hypothesis,
e24 != select(sF56,sF100) ).
cnf(u2723,axiom,
e14 = select(sF63,i14) ).
cnf(u1219,hypothesis,
i37 != i15 ).
cnf(u873,hypothesis,
i50 != i20 ).
cnf(u393,hypothesis,
i45 != i30 ).
cnf(u2498,axiom,
store(sF21,i23,e23) = sF22 ).
cnf(u55,hypothesis,
i45 != i43 ).
cnf(u599,hypothesis,
i28 != i26 ).
cnf(u2524,axiom,
store(sF34,i36,e36) = sF35 ).
cnf(u1759,hypothesis,
i33 != i8 ).
cnf(u14986,hypothesis,
e33 != select(sF5,sF100) ).
cnf(u217,hypothesis,
i48 != i35 ).
cnf(u775,hypothesis,
i42 != i22 ).
cnf(u2744,axiom,
e35 = select(sF84,i35) ).
cnf(u1447,hypothesis,
i31 != i12 ).
cnf(u1991,hypothesis,
i46 != i5 ).
cnf(u9051,hypothesis,
e5 != select(sF61,sF100) ).
cnf(u2669,axiom,
e9 = select(sF8,i9) ).
cnf(u5553,axiom,
e24 != sF102 ).
cnf(u2859,axiom,
( select(sF98,X0) = select(sF99,X0)
| i1 = X0 ) ).
cnf(u929,hypothesis,
i22 != i20 ).
cnf(u2602,axiom,
store(sF73,i18,e18) = sF74 ).
cnf(u111,hypothesis,
i41 != i40 ).
cnf(u15067,hypothesis,
sF101 = select(sF1,sF100) ).
cnf(u1271,hypothesis,
i46 != i14 ).
cnf(u2845,axiom,
( select(sF84,X0) = select(sF85,X0)
| i50 = X0 ) ).
cnf(u2683,axiom,
e23 = select(sF22,i23) ).
cnf(u753,hypothesis,
i26 != i23 ).
cnf(u287,hypothesis,
i44 != i33 ).
cnf(u2584,axiom,
store(sF64,i6,e6) = sF65 ).
cnf(u959,hypothesis,
i37 != i19 ).
cnf(u14153,hypothesis,
sF101 = select(sF13,sF100) ).
cnf(u2291,hypothesis,
i34 != i2 ).
cnf(u2189,hypothesis,
i38 != i3 ).
cnf(u14168,hypothesis,
sF101 = select(sF12,sF100) ).
cnf(u449,hypothesis,
i37 != i29 ).
cnf(u655,hypothesis,
i49 != i24 ).
cnf(u2832,axiom,
( select(sF71,X0) = select(sF72,X0)
| i42 = X0 ) ).
cnf(u2754,axiom,
e32 = select(sF94,i32) ).
cnf(u14533,hypothesis,
sF102 != select(sF76,sF100) ).
cnf(u343,hypothesis,
i33 != i32 ).
cnf(u2458,axiom,
store(sF1,i3,e3) = sF2 ).
cnf(u2696,axiom,
e36 = select(sF35,i36) ).
cnf(u1503,hypothesis,
i41 != i11 ).
cnf(u15013,hypothesis,
sF101 = select(sF4,sF100) ).
cnf(u7199,hypothesis,
sF101 = select(sF19,sF100) ).
cnf(u985,hypothesis,
i24 != i19 ).
cnf(u2846,axiom,
( select(sF85,X0) = select(sF86,X0)
| i2 = X0 ) ).
cnf(u167,hypothesis,
i46 != i37 ).
cnf(u7081,hypothesis,
e24 != select(sF65,sF100) ).
cnf(u2776,axiom,
( select(sF14,X0) = select(sF15,X0)
| i16 = X0 ) ).
cnf(u8872,hypothesis,
e33 != select(sF15,sF100) ).
cnf(u14933,hypothesis,
e50 != select(sF75,sF100) ).
cnf(u53,hypothesis,
i46 != i43 ).
cnf(u14811,hypothesis,
e4 != select(sF52,sF100) ).
cnf(u9416,hypothesis,
e43 != select(sF7,sF100) ).
cnf(u1015,hypothesis,
i40 != i18 ).
cnf(u2409,hypothesis,
i23 != i1 ).
cnf(u2781,axiom,
( select(sF19,X0) = select(sF20,X0)
| i21 = X0 ) ).
cnf(u6082,axiom,
e46 != sF101 ).
cnf(u2427,hypothesis,
i14 != i1 ).
cnf(u5871,axiom,
e46 != select(sF30,sF100) ).
cnf(u745,hypothesis,
i30 != i23 ).
cnf(u2714,axiom,
e28 = select(sF54,i28) ).
cnf(u9685,hypothesis,
e46 != select(sF61,sF100) ).
cnf(u223,hypothesis,
i45 != i35 ).
cnf(u5559,axiom,
e46 != select(sF35,sF100) ).
cnf(u2233,hypothesis,
i16 != i3 ).
cnf(u2123,hypothesis,
i25 != i4 ).
cnf(u2795,axiom,
( select(sF33,X0) = select(sF34,X0)
| i35 = X0 ) ).
cnf(u8928,hypothesis,
e43 != select(sF13,sF100) ).
cnf(u399,hypothesis,
i42 != i30 ).
cnf(u2736,axiom,
e34 = select(sF76,i34) ).
cnf(u285,hypothesis,
i45 != i33 ).
cnf(u535,hypothesis,
i37 != i27 ).
cnf(u2590,axiom,
store(sF67,i7,e7) = sF68 ).
cnf(u455,hypothesis,
i34 != i29 ).
cnf(u109,hypothesis,
i42 != i40 ).
cnf(u2488,axiom,
store(sF16,i18,e18) = sF17 ).
cnf(u6561,hypothesis,
e46 != select(sF21,sF100) ).
cnf(u821,hypothesis,
i47 != i21 ).
cnf(u341,hypothesis,
i34 != i32 ).
cnf(u2612,axiom,
store(sF78,i44,e44) = sF79 ).
cnf(u2697,axiom,
e37 = select(sF36,i37) ).
cnf(u2359,hypothesis,
i48 != i1 ).
cnf(u517,hypothesis,
i46 != i27 ).
cnf(u165,hypothesis,
i47 != i37 ).
cnf(u2820,axiom,
( select(sF59,X0) = select(sF60,X0)
| i16 = X0 ) ).
cnf(u2055,hypothesis,
i14 != i5 ).
cnf(u2727,axiom,
e15 = select(sF67,i15) ).
cnf(u7739,hypothesis,
e33 != sF101 ).
cnf(u2065,hypothesis,
i9 != i5 ).
cnf(u877,hypothesis,
i48 != i20 ).
cnf(u2512,axiom,
store(sF28,i30,e30) = sF29 ).
cnf(u531,hypothesis,
i39 != i27 ).
cnf(u1053,hypothesis,
i21 != i18 ).
cnf(u6402,hypothesis,
e3 != select(sF75,sF100) ).
cnf(u701,hypothesis,
i26 != i24 ).
cnf(u891,hypothesis,
i41 != i20 ).
cnf(u1285,hypothesis,
i39 != i14 ).
cnf(u6400,hypothesis,
e5 != select(sF75,sF100) ).
cnf(u397,hypothesis,
i43 != i30 ).
cnf(u43,hypothesis,
i45 != i44 ).
cnf(u587,hypothesis,
i34 != i26 ).
cnf(u2833,axiom,
( select(sF72,X0) = select(sF73,X0)
| i47 = X0 ) ).
cnf(u1589,hypothesis,
i37 != i10 ).
cnf(u1109,hypothesis,
i25 != i17 ).
cnf(u2702,axiom,
e42 = select(sF41,i42) ).
cnf(u275,hypothesis,
i50 != i33 ).
cnf(u221,hypothesis,
i46 != i35 ).
cnf(u1821,hypothesis,
i44 != i7 ).
cnf(u2177,hypothesis,
i44 != i3 ).
cnf(u933,hypothesis,
i50 != i19 ).
cnf(u453,hypothesis,
i35 != i29 ).
cnf(u99,hypothesis,
i47 != i40 ).
cnf(u2724,axiom,
e13 = select(sF64,i13) ).
cnf(u1321,hypothesis,
i21 != i14 ).
cnf(u1645,hypothesis,
i49 != i9 ).
cnf(u1835,hypothesis,
i37 != i7 ).
cnf(u2687,axiom,
e27 = select(sF26,i27) ).
cnf(u2329,hypothesis,
i15 != i2 ).
cnf(u15072,hypothesis,
e24 != select(sF50,sF100) ).
cnf(u757,hypothesis,
i24 != i23 ).
cnf(u947,hypothesis,
i43 != i19 ).
cnf(u2357,hypothesis,
i49 != i1 ).
cnf(u1145,hypothesis,
i40 != i16 ).
cnf(u2295,hypothesis,
i32 != i2 ).
cnf(u1469,hypothesis,
i20 != i12 ).
cnf(u989,hypothesis,
i22 != i19 ).
cnf(u1659,hypothesis,
i42 != i9 ).
cnf(u643,hypothesis,
i30 != i25 ).
cnf(u2053,hypothesis,
i15 != i5 ).
cnf(u13748,hypothesis,
sF101 = select(sF14,sF100) ).
cnf(u1165,hypothesis,
i30 != i16 ).
cnf(u1861,hypothesis,
i24 != i7 ).
cnf(u7194,hypothesis,
e47 != select(sF19,sF100) ).
cnf(u331,hypothesis,
i39 != i32 ).
cnf(u1003,hypothesis,
i46 != i18 ).
cnf(u1553,hypothesis,
i16 != i11 ).
cnf(u1201,hypothesis,
i46 != i15 ).
cnf(u14988,hypothesis,
e43 != select(sF5,sF100) ).
cnf(u1877,hypothesis,
i16 != i7 ).
cnf(u1525,hypothesis,
i30 != i11 ).
cnf(u1043,hypothesis,
i26 != i18 ).
cnf(u8854,hypothesis,
e46 != select(sF16,sF100) ).
cnf(u2662,axiom,
e2 = select(sF1,i2) ).
cnf(u155,hypothesis,
i40 != i38 ).
cnf(u1377,hypothesis,
i29 != i13 ).
cnf(u2834,axiom,
( select(sF73,X0) = select(sF74,X0)
| i18 = X0 ) ).
cnf(u1583,hypothesis,
i40 != i10 ).
cnf(u2127,hypothesis,
i23 != i4 ).
cnf(u1701,hypothesis,
i21 != i9 ).
cnf(u1221,hypothesis,
i36 != i15 ).
cnf(u1891,hypothesis,
i9 != i7 ).
cnf(u387,hypothesis,
i48 != i30 ).
cnf(u2500,axiom,
store(sF22,i24,e24) = sF23 ).
cnf(u41,hypothesis,
i46 != i44 ).
cnf(u1609,hypothesis,
i27 != i10 ).
cnf(u2518,axiom,
store(sF31,i33,e33) = sF32 ).
cnf(u15006,hypothesis,
e43 != select(sF4,sF100) ).
cnf(u2684,axiom,
e24 = select(sF23,i24) ).
cnf(u1933,hypothesis,
i31 != i6 ).
cnf(u2769,axiom,
( select(sF7,X0) = select(sF8,X0)
| i9 = X0 ) ).
cnf(u6699,hypothesis,
sF101 = select(sF24,sF100) ).
cnf(u2431,hypothesis,
i12 != i1 ).
cnf(u1715,hypothesis,
i14 != i9 ).
cnf(u211,hypothesis,
i37 != i36 ).
cnf(u1913,hypothesis,
i41 != i6 ).
cnf(u1433,hypothesis,
i38 != i12 ).
cnf(u13712,hypothesis,
sF101 = select(sF16,sF100) ).
cnf(u1639,hypothesis,
i12 != i10 ).
cnf(u1757,hypothesis,
i34 != i8 ).
cnf(u1403,hypothesis,
i16 != i13 ).
cnf(u1947,hypothesis,
i24 != i6 ).
cnf(u2799,axiom,
( select(sF37,X0) = select(sF38,X0)
| i39 = X0 ) ).
cnf(u9446,hypothesis,
e5 != select(sF55,sF100) ).
cnf(u97,hypothesis,
i48 != i40 ).
cnf(u2821,axiom,
( select(sF60,X0) = select(sF61,X0)
| i8 = X0 ) ).
cnf(u1257,hypothesis,
i18 != i15 ).
cnf(u1815,hypothesis,
i47 != i7 ).
cnf(u1099,hypothesis,
i30 != i17 ).
cnf(u1771,hypothesis,
i27 != i8 ).
cnf(u273,hypothesis,
i35 != i34 ).
cnf(u1969,hypothesis,
i13 != i6 ).
cnf(u1151,hypothesis,
i37 != i16 ).
cnf(u14966,hypothesis,
e50 != select(sF61,sF100) ).
cnf(u2293,hypothesis,
i33 != i2 ).
cnf(u2835,axiom,
( select(sF74,X0) = select(sF75,X0)
| i26 = X0 ) ).
cnf(u1459,hypothesis,
i25 != i12 ).
cnf(u633,hypothesis,
i35 != i25 ).
cnf(u1665,hypothesis,
i39 != i9 ).
cnf(u1327,hypothesis,
i18 != i14 ).
cnf(u1871,hypothesis,
i19 != i7 ).
cnf(u1989,hypothesis,
i47 != i5 ).
cnf(u2659,negated_conjecture,
sF101 != sF102 ).
cnf(u1155,hypothesis,
i35 != i16 ).
cnf(u809,hypothesis,
i25 != i22 ).
cnf(u14179,hypothesis,
sF101 = select(sF11,sF100) ).
cnf(u329,hypothesis,
i40 != i32 ).
cnf(u2774,axiom,
( select(sF12,X0) = select(sF13,X0)
| i14 = X0 ) ).
cnf(u2600,axiom,
store(sF72,i47,e47) = sF73 ).
cnf(u2460,axiom,
store(sF2,i4,e4) = sF3 ).
cnf(u1489,hypothesis,
i48 != i11 ).
cnf(u1695,hypothesis,
i24 != i9 ).
cnf(u9332,hypothesis,
e47 != select(sF8,sF100) ).
cnf(u14922,axiom,
e48 != e50 ).
cnf(u2003,hypothesis,
i40 != i5 ).
cnf(u153,hypothesis,
i41 != i38 ).
cnf(u5530,axiom,
sF102 = select(sF87,sF100) ).
cnf(u1383,hypothesis,
i26 != i13 ).
cnf(u1777,hypothesis,
i24 != i8 ).
cnf(u9410,hypothesis,
e46 != select(sF7,sF100) ).
cnf(u865,hypothesis,
i25 != i21 ).
cnf(u47,hypothesis,
i49 != i43 ).
cnf(u2025,hypothesis,
i29 != i5 ).
cnf(u2403,hypothesis,
i26 != i1 ).
cnf(u1207,hypothesis,
i43 != i15 ).
cnf(u1751,hypothesis,
i37 != i8 ).
cnf(u2429,hypothesis,
i13 != i1 ).
cnf(u1515,hypothesis,
i35 != i11 ).
cnf(u7087,hypothesis,
e5 != select(sF65,sF100) ).
cnf(u689,hypothesis,
i32 != i24 ).
cnf(u209,hypothesis,
i38 != i36 ).
cnf(u895,hypothesis,
i39 != i20 ).
cnf(u2227,hypothesis,
i19 != i3 ).
cnf(u1927,hypothesis,
i34 != i6 ).
cnf(u2771,axiom,
( select(sF9,X0) = select(sF10,X0)
| i11 = X0 ) ).
cnf(u2125,hypothesis,
i24 != i4 ).
cnf(u14963,hypothesis,
e50 != select(sF62,sF100) ).
cnf(u385,hypothesis,
i49 != i30 ).
cnf(u591,hypothesis,
i32 != i26 ).
cnf(u1263,hypothesis,
i50 != i14 ).
cnf(u2757,axiom,
e21 = select(sF97,i21) ).
cnf(u2690,axiom,
e30 = select(sF29,i30) ).
cnf(u14944,hypothesis,
e50 != select(sF70,sF100) ).
cnf(u279,hypothesis,
i48 != i33 ).
cnf(u1439,hypothesis,
i35 != i12 ).
cnf(u921,hypothesis,
i26 != i20 ).
cnf(u103,hypothesis,
i45 != i40 ).
cnf(u647,hypothesis,
i28 != i25 ).
cnf(u935,hypothesis,
i49 != i19 ).
cnf(u14935,hypothesis,
e50 != select(sF74,sF100) ).
cnf(u8677,hypothesis,
e33 != select(sF24,sF100) ).
cnf(u9444,hypothesis,
e4 != select(sF55,sF100) ).
cnf(u951,hypothesis,
i41 != i19 ).
cnf(u1495,hypothesis,
i45 != i11 ).
cnf(u2345,hypothesis,
i7 != i2 ).
cnf(u9310,hypothesis,
e33 != select(sF9,sF100) ).
cnf(u2717,axiom,
e39 = select(sF57,i39) ).
cnf(u2363,hypothesis,
i46 != i1 ).
cnf(u977,hypothesis,
i28 != i19 ).
cnf(u2650,axiom,
store(sF97,i31,e31) = sF98 ).
cnf(u159,hypothesis,
i50 != i37 ).
cnf(u2169,hypothesis,
i48 != i3 ).
cnf(u14909,axiom,
sF85 = store(sF84,sF100,e50) ).
cnf(u2059,hypothesis,
i12 != i5 ).
cnf(u2731,axiom,
e17 = select(sF71,i17) ).
cnf(u335,hypothesis,
i37 != i32 ).
cnf(u1007,hypothesis,
i44 != i18 ).
cnf(u2672,axiom,
e12 = select(sF11,i12) ).
cnf(u391,hypothesis,
i46 != i30 ).
cnf(u45,hypothesis,
i50 != i43 ).
cnf(u2506,axiom,
store(sF25,i27,e27) = sF26 ).
cnf(u15070,hypothesis,
e50 != select(sF51,sF100) ).
cnf(u14976,hypothesis,
e50 != select(sF58,sF100) ).
cnf(u277,hypothesis,
i49 != i33 ).
cnf(u8584,hypothesis,
e33 != select(sF30,sF100) ).
cnf(u215,hypothesis,
i49 != i35 ).
cnf(u6096,axiom,
sF101 = select(sF38,sF100) ).
cnf(u101,hypothesis,
i46 != i40 ).
cnf(u2663,axiom,
e3 = select(sF2,i3) ).
cnf(u813,hypothesis,
i23 != i22 ).
cnf(u2762,axiom,
( select(sF0,X0) = select(sF1,X0)
| i2 = X0 ) ).
cnf(u2281,hypothesis,
i39 != i2 ).
cnf(u583,hypothesis,
i36 != i26 ).
cnf(u2839,axiom,
( select(sF78,X0) = select(sF79,X0)
| i44 = X0 ) ).
cnf(u2299,hypothesis,
i30 != i2 ).
cnf(u637,hypothesis,
i33 != i25 ).
cnf(u827,hypothesis,
i44 != i21 ).
cnf(u2784,axiom,
( select(sF22,X0) = select(sF23,X0)
| i24 = X0 ) ).
cnf(u2536,axiom,
store(sF40,i42,e42) = sF41 ).
cnf(u14845,hypothesis,
e46 != select(sF51,sF100) ).
cnf(u333,hypothesis,
i38 != i32 ).
cnf(u523,hypothesis,
i43 != i27 ).
cnf(u1045,hypothesis,
i25 != i18 ).
cnf(u2638,axiom,
store(sF91,i12,e12) = sF92 ).
cnf(u8534,hypothesis,
e33 != select(sF36,sF100) ).
cnf(u157,hypothesis,
i39 != i38 ).
cnf(u2113,hypothesis,
i30 != i4 ).
cnf(u869,hypothesis,
i23 != i21 ).
cnf(u389,hypothesis,
i47 != i30 ).
cnf(u35,hypothesis,
i49 != i44 ).
cnf(u2660,axiom,
e1 = select(sF0,i1) ).
cnf(u2407,hypothesis,
i24 != i1 ).
cnf(u1581,hypothesis,
i41 != i10 ).
cnf(u2417,hypothesis,
i19 != i1 ).
cnf(u9047,hypothesis,
e24 != select(sF61,sF100) ).
cnf(u693,hypothesis,
i30 != i24 ).
cnf(u213,hypothesis,
i50 != i35 ).
cnf(u883,hypothesis,
i45 != i20 ).
cnf(u1081,hypothesis,
i39 != i17 ).
cnf(u2231,hypothesis,
i17 != i3 ).
cnf(u2775,axiom,
( select(sF13,X0) = select(sF14,X0)
| i15 = X0 ) ).
cnf(u1405,hypothesis,
i15 != i13 ).
cnf(u925,hypothesis,
i24 != i20 ).
cnf(u1595,hypothesis,
i34 != i10 ).
cnf(u15004,hypothesis,
e33 != select(sF4,sF100) ).
cnf(u579,hypothesis,
i38 != i26 ).
cnf(u1101,hypothesis,
i29 != i17 ).
cnf(u749,hypothesis,
i28 != i23 ).
cnf(u267,hypothesis,
i38 != i34 ).
cnf(u939,hypothesis,
i47 != i19 ).
cnf(u1137,hypothesis,
i44 != i16 ).
cnf(u14575,hypothesis,
sF102 != select(sF71,sF100) ).
cnf(u1813,hypothesis,
i48 != i7 ).
cnf(u14982,hypothesis,
e46 != select(sF5,sF100) ).
cnf(u1461,hypothesis,
i24 != i12 ).
cnf(u2598,axiom,
store(sF71,i42,e42) = sF72 ).
cnf(u91,hypothesis,
i42 != i41 ).
cnf(u763,hypothesis,
i48 != i22 ).
cnf(u2828,axiom,
( select(sF67,X0) = select(sF68,X0)
| i7 = X0 ) ).
cnf(u15088,hypothesis,
e43 != select(sF0,sF100) ).
cnf(u2063,hypothesis,
i10 != i5 ).
cnf(u1637,hypothesis,
i13 != i10 ).
cnf(u1157,hypothesis,
i34 != i16 ).
cnf(u1827,hypothesis,
i41 != i7 ).
cnf(u323,hypothesis,
i43 != i32 ).
cnf(u1545,hypothesis,
i20 != i11 ).
cnf(u2454,axiom,
store(a1,i1,e1) = sF0 ).
cnf(u2620,axiom,
store(sF82,i46,e46) = sF83 ).
cnf(u1869,hypothesis,
i20 != i7 ).
cnf(u2705,axiom,
e45 = select(sF44,i45) ).
cnf(u2367,hypothesis,
i44 != i1 ).
cnf(u981,hypothesis,
i26 != i19 ).
cnf(u1651,hypothesis,
i46 != i9 ).
cnf(u147,hypothesis,
i44 != i38 ).
cnf(u2772,axiom,
( select(sF10,X0) = select(sF11,X0)
| i12 = X0 ) ).
cnf(u1849,hypothesis,
i30 != i7 ).
cnf(u1369,hypothesis,
i33 != i13 ).
cnf(u1575,hypothesis,
i44 != i10 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV502-1.050 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n014.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:21:15 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.00/0.95 % (1717496)Will run a generic schedule for satisfiability detection.
% 4.00/0.95 % (1717502)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1867999120_2999 on theBenchmark for (2999ds/0Mi)
% 4.00/0.95 % (1717504)% WARNING: option uhcvi not known.
% 4.00/0.95 % (1717505)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3102668578:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.00/0.95 % (1717506)dis+10_1_sil=32000:sp=arity:random_seed=312694767:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.00/0.95 % (1717507)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1157720550:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.00/0.95 % (1717504)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=336255997:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.00/0.95 % (1717508)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=189123652:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.00/0.95 % (1717509)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1205544729:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.00/0.95 % Detected minimum model sizes of [50]
% 4.00/0.95 % Detected maximum model sizes of [max]
% 4.00/0.95 % TRYING [50]
% 4.00/0.95 % (1717506)Instruction limit reached!
% 4.00/0.95 % (1717506)------------------------------
% 4.00/0.95 % (1717506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717506)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717506)Termination reason: Instruction limit
% 4.00/0.95 % (1717506)Termination phase: Saturation
% 4.00/0.95 % (1717506)Time elapsed: 0.049 s
% 4.00/0.95 % (1717506)Peak memory usage: 13 MB
% 4.00/0.95 % (1717506)Instructions burned: 104 (million)
% 4.00/0.95 % (1717507)Instruction limit reached!
% 4.00/0.95 % (1717507)------------------------------
% 4.00/0.95 % (1717507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717507)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717507)Termination reason: Instruction limit
% 4.00/0.95 % (1717507)Termination phase: Saturation
% 4.00/0.95 % (1717507)Time elapsed: 0.054 s
% 4.00/0.95 % (1717507)Peak memory usage: 13 MB
% 4.00/0.95 % (1717507)Instructions burned: 120 (million)
% 4.00/0.95 % (1717508)Instruction limit reached!
% 4.00/0.95 % (1717508)------------------------------
% 4.00/0.95 % (1717508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717508)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717508)Termination reason: Instruction limit
% 4.00/0.95 % (1717508)Termination phase: Saturation
% 4.00/0.95 % (1717508)Time elapsed: 0.054 s
% 4.00/0.95 % (1717508)Peak memory usage: 13 MB
% 4.00/0.95 % (1717508)Instructions burned: 132 (million)
% 4.00/0.95 % (1717532)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1008632131:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.00/0.95 % (1717535)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2048837875:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.00/0.95 % (1717509)Instruction limit reached!
% 4.00/0.95 % (1717509)------------------------------
% 4.00/0.95 % (1717509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717509)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717509)Termination reason: Instruction limit
% 4.00/0.95 % (1717509)Termination phase: Saturation
% 4.00/0.95 % (1717509)Time elapsed: 0.073 s
% 4.00/0.95 % (1717509)Peak memory usage: 14 MB
% 4.00/0.95 % (1717509)Instructions burned: 161 (million)
% 4.00/0.95 % (1717536)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=3770581825:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.00/0.95 % Detected minimum model sizes of [50]
% 4.00/0.95 % Detected maximum model sizes of [max]
% 4.00/0.95 % TRYING [50]
% 4.00/0.95 % (1717547)ott-21_1_sil=16000:fs=off:random_seed=3792947143:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.00/0.95 % (1717535)Instruction limit reached!
% 4.00/0.95 % (1717535)------------------------------
% 4.00/0.95 % (1717535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717535)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717535)Termination reason: Instruction limit
% 4.00/0.95 % (1717535)Termination phase: Saturation
% 4.00/0.95 % (1717535)Time elapsed: 0.058 s
% 4.00/0.95 % (1717535)Peak memory usage: 14 MB
% 4.00/0.95 % (1717535)Instructions burned: 132 (million)
% 4.00/0.95 % (1717576)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3654296000:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.00/0.95 % (1717547)Instruction limit reached!
% 4.00/0.95 % (1717547)------------------------------
% 4.00/0.95 % (1717547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717547)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717547)Termination reason: Instruction limit
% 4.00/0.95 % (1717547)Termination phase: Saturation
% 4.00/0.95 % (1717547)Time elapsed: 0.088 s
% 4.00/0.95 % (1717547)Peak memory usage: 12 MB
% 4.00/0.95 % (1717547)Instructions burned: 186 (million)
% 4.00/0.95 % (1717591)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=612699899:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.00/0.95 % Detected minimum model sizes of [50]
% 4.00/0.95 % Detected maximum model sizes of [max]
% 4.00/0.95 % (1717532)Instruction limit reached!
% 4.00/0.95 % (1717532)------------------------------
% 4.00/0.95 % (1717532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717532)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717532)Termination reason: Instruction limit
% 4.00/0.95 % (1717532)Termination phase: Finite model building constraint generation
% 4.00/0.95 % (1717532)Time elapsed: 0.270 s
% 4.00/0.95 % (1717532)Peak memory usage: 60 MB
% 4.00/0.95 % (1717532)Instructions burned: 717 (million)
% 4.00/0.95 % (1717630)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3938218402:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 4.00/0.95 % (1717576)Instruction limit reached!
% 4.00/0.95 % (1717576)------------------------------
% 4.00/0.95 % (1717576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717576)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717576)Termination reason: Instruction limit
% 4.00/0.95 % (1717576)Termination phase: Saturation
% 4.00/0.95 % (1717576)Time elapsed: 0.221 s
% 4.00/0.95 % (1717576)Peak memory usage: 16 MB
% 4.00/0.95 % (1717576)Instructions burned: 477 (million)
% 4.00/0.95 % (1717536)Instruction limit reached!
% 4.00/0.95 % (1717536)------------------------------
% 4.00/0.95 % (1717536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717536)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717536)Termination reason: Instruction limit
% 4.00/0.95 % (1717536)Termination phase: Saturation
% 4.00/0.95 % (1717536)Time elapsed: 0.313 s
% 4.00/0.95 % (1717536)Peak memory usage: 17 MB
% 4.00/0.95 % (1717536)Instructions burned: 685 (million)
% 4.00/0.95 % (1717638)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2345339896:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 4.00/0.95 % (1717641)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1488665507:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 4.00/0.95 % TRYING [14]
% 4.00/0.95 % (1717591)Instruction limit reached!
% 4.00/0.95 % (1717591)------------------------------
% 4.00/0.95 % (1717591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.95 % (1717591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.95 % (1717591)CaDiCaL version: 2.1.3
% 4.00/0.95 % (1717591)Termination reason: Instruction limit
% 4.00/0.95 % (1717591)Termination phase: Finite model building constraint generation
% 4.00/0.95 % (1717591)Time elapsed: 0.407 s
% 4.00/0.95 % (1717591)Peak memory usage: 103 MB
% 4.00/0.95 % (1717591)Instructions burned: 867 (million)
% 4.00/0.95 % (1717663)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3953544182:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 4.00/0.95 % (1717630) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1717496-1717630"...
% 4.00/0.95 % (1717630)...printing done.
% 4.00/0.95 % SZS status Satisfiable for theBenchmark
% 4.00/0.95 % SZS output start Saturation.
% See solution above
% 4.00/0.98 % SZS output start Definitions and Model Updates.
% 4.00/0.98 % SZS output end Definitions and Model Updates.
% 4.00/0.98 % (1717630)------------------------------
% 4.00/0.98 % (1717630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.00/0.98 % (1717630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.00/0.98 % (1717630)CaDiCaL version: 2.1.3
% 4.00/0.98 % (1717630)Termination reason: Satisfiable
% 4.00/0.98 % (1717630)Time elapsed: 0.315 s
% 4.00/0.98 % (1717630)Peak memory usage: 17 MB
% 4.00/0.98 % (1717630)Instructions burned: 573 (million)
% 4.00/0.98 % (1717496)Success in time 0.744 s
% 4.00/0.98 % Vampire exiting
%------------------------------------------------------------------------------