%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWV506-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 : Thu Sep 24 02:56:44 PM UTC 2026
% Result : Satisfiable 0.26s 0.60s
% Output : Saturation 0.26s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named hyp35ERROR: Could not build tree for root c_0_1616ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_501,axiom,
( select(store(X3,X1,X4),X2) = select(X3,X2)
| X1 = X2 ),
a2,
[final] ).
cnf(c_0_502,hypothesis,
a_1128 = store(a_1127,i10,e10),
hyp59,
[final] ).
cnf(c_0_503,hypothesis,
a_1127 = store(a_1126,i7,e7),
hyp58,
[final] ).
cnf(c_0_504,hypothesis,
a_1126 = store(a_1125,i24,e24),
hyp57,
[final] ).
cnf(c_0_505,hypothesis,
( i10 = X1
| select(a_1127,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_502]),
[final] ).
cnf(c_0_506,hypothesis,
( i7 = X1
| select(a_1127,X1) = select(a_1126,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_503]),
[final] ).
cnf(c_0_507,hypothesis,
a_1098 = store(a_1097,i1,e1),
hyp29,
[final] ).
cnf(c_0_508,hypothesis,
a_1097 = store(a_1096,i29,e29),
hyp28,
[final] ).
cnf(c_0_509,hypothesis,
a_1125 = store(a_1124,i23,e23),
hyp56,
[final] ).
cnf(c_0_510,hypothesis,
( i24 = X1
| select(a_1126,X1) = select(a_1125,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_504]),
[final] ).
cnf(c_0_511,hypothesis,
( i10 = X1
| i7 = X1
| select(a_1126,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_505,c_0_506]),
[final] ).
cnf(c_0_512,hypothesis,
a_1096 = store(a_1095,i28,e28),
hyp27,
[final] ).
cnf(c_0_513,hypothesis,
( i1 = X1
| select(a_1097,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_507]),
[final] ).
cnf(c_0_514,hypothesis,
( i29 = X1
| select(a_1097,X1) = select(a_1096,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_508]),
[final] ).
cnf(c_0_515,hypothesis,
a_1124 = store(a_1123,i17,e17),
hyp55,
[final] ).
cnf(c_0_516,hypothesis,
( i23 = X1
| select(a_1125,X1) = select(a_1124,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_509]),
[final] ).
cnf(c_0_517,hypothesis,
( i24 = X1
| i7 = X1
| i10 = X1
| select(a_1125,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_510,c_0_511]),
[final] ).
cnf(c_0_518,hypothesis,
a_1095 = store(a_1094,i27,e27),
hyp26,
[final] ).
cnf(c_0_519,hypothesis,
( i28 = X1
| select(a_1096,X1) = select(a_1095,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_512]),
[final] ).
cnf(c_0_520,hypothesis,
( i1 = X1
| i29 = X1
| select(a_1096,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_513,c_0_514]),
[final] ).
cnf(c_0_521,hypothesis,
a_1123 = store(a_1122,i28,e28),
hyp54,
[final] ).
cnf(c_0_522,hypothesis,
( i17 = X1
| select(a_1124,X1) = select(a_1123,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_515]),
[final] ).
cnf(c_0_523,hypothesis,
( i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| select(a_1124,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_516,c_0_517]),
[final] ).
cnf(c_0_524,hypothesis,
a_1094 = store(a_1093,i26,e26),
hyp25,
[final] ).
cnf(c_0_525,hypothesis,
( i27 = X1
| select(a_1095,X1) = select(a_1094,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_518]),
[final] ).
cnf(c_0_526,hypothesis,
( i28 = X1
| i29 = X1
| i1 = X1
| select(a_1095,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_519,c_0_520]),
[final] ).
cnf(c_0_527,hypothesis,
a_1122 = store(a_1121,i16,e16),
hyp53,
[final] ).
cnf(c_0_528,hypothesis,
( i28 = X1
| select(a_1123,X1) = select(a_1122,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_521]),
[final] ).
cnf(c_0_529,hypothesis,
( i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| select(a_1123,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_522,c_0_523]),
[final] ).
cnf(c_0_530,hypothesis,
a_1093 = store(a_1092,i25,e25),
hyp24,
[final] ).
cnf(c_0_531,hypothesis,
( i26 = X1
| select(a_1094,X1) = select(a_1093,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_524]),
[final] ).
cnf(c_0_532,hypothesis,
( i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| select(a_1094,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_525,c_0_526]),
[final] ).
cnf(c_0_533,hypothesis,
a_1121 = store(a_1120,i12,e12),
hyp52,
[final] ).
cnf(c_0_534,hypothesis,
( i16 = X1
| select(a_1122,X1) = select(a_1121,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_527]),
[final] ).
cnf(c_0_535,hypothesis,
( i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| select(a_1122,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_528,c_0_529]),
[final] ).
cnf(c_0_536,hypothesis,
a_1092 = store(a_1091,i24,e24),
hyp23,
[final] ).
cnf(c_0_537,hypothesis,
( i25 = X1
| select(a_1093,X1) = select(a_1092,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_530]),
[final] ).
cnf(c_0_538,hypothesis,
( i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| select(a_1093,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_531,c_0_532]),
[final] ).
cnf(c_0_539,hypothesis,
a_1120 = store(a_1119,i3,e3),
hyp51,
[final] ).
cnf(c_0_540,hypothesis,
( i12 = X1
| select(a_1121,X1) = select(a_1120,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_533]),
[final] ).
cnf(c_0_541,hypothesis,
( i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| select(a_1121,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_534,c_0_535]),
[final] ).
cnf(c_0_542,hypothesis,
a_1091 = store(a_1090,i23,e23),
hyp22,
[final] ).
cnf(c_0_543,hypothesis,
( i24 = X1
| select(a_1092,X1) = select(a_1091,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_536]),
[final] ).
cnf(c_0_544,hypothesis,
( i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| select(a_1092,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_537,c_0_538]),
[final] ).
cnf(c_0_545,hypothesis,
a_1119 = store(a_1118,i27,e27),
hyp50,
[final] ).
cnf(c_0_546,hypothesis,
( i3 = X1
| select(a_1120,X1) = select(a_1119,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_539]),
[final] ).
cnf(c_0_547,hypothesis,
( i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| select(a_1120,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_540,c_0_541]),
[final] ).
cnf(c_0_548,hypothesis,
a_1090 = store(a_1089,i22,e22),
hyp21,
[final] ).
cnf(c_0_549,hypothesis,
( i23 = X1
| select(a_1091,X1) = select(a_1090,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_542]),
[final] ).
cnf(c_0_550,hypothesis,
( i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| select(a_1091,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_543,c_0_544]),
[final] ).
cnf(c_0_551,hypothesis,
a_1118 = store(a_1117,i22,e22),
hyp49,
[final] ).
cnf(c_0_552,hypothesis,
( i27 = X1
| select(a_1119,X1) = select(a_1118,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_545]),
[final] ).
cnf(c_0_553,hypothesis,
( i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| select(a_1119,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_546,c_0_547]),
[final] ).
cnf(c_0_554,hypothesis,
a_1089 = store(a_1088,i21,e21),
hyp20,
[final] ).
cnf(c_0_555,hypothesis,
( i22 = X1
| select(a_1090,X1) = select(a_1089,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_548]),
[final] ).
cnf(c_0_556,hypothesis,
( i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| select(a_1090,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_549,c_0_550]),
[final] ).
cnf(c_0_557,hypothesis,
a_1117 = store(a_1116,i26,e26),
hyp48,
[final] ).
cnf(c_0_558,hypothesis,
( i22 = X1
| select(a_1118,X1) = select(a_1117,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_551]),
[final] ).
cnf(c_0_559,hypothesis,
( i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| select(a_1118,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_552,c_0_553]),
[final] ).
cnf(c_0_560,hypothesis,
a_1088 = store(a_1087,i20,e20),
hyp19,
[final] ).
cnf(c_0_561,hypothesis,
( i21 = X1
| select(a_1089,X1) = select(a_1088,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_554]),
[final] ).
cnf(c_0_562,hypothesis,
( i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| select(a_1089,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_555,c_0_556]),
[final] ).
cnf(c_0_563,hypothesis,
a_1116 = store(a_1115,i5,e5),
hyp47,
[final] ).
cnf(c_0_564,hypothesis,
( i26 = X1
| select(a_1117,X1) = select(a_1116,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_557]),
[final] ).
cnf(c_0_565,hypothesis,
( i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| select(a_1117,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_558,c_0_559]),
[final] ).
cnf(c_0_566,hypothesis,
a_1087 = store(a_1086,i19,e19),
hyp18,
[final] ).
cnf(c_0_567,hypothesis,
( i20 = X1
| select(a_1088,X1) = select(a_1087,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_560]),
[final] ).
cnf(c_0_568,hypothesis,
( i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| select(a_1088,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_561,c_0_562]),
[final] ).
cnf(c_0_569,hypothesis,
a_1115 = store(a_1114,i29,e29),
hyp46,
[final] ).
cnf(c_0_570,hypothesis,
( i5 = X1
| select(a_1116,X1) = select(a_1115,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_563]),
[final] ).
cnf(c_0_571,hypothesis,
( i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| select(a_1116,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_564,c_0_565]),
[final] ).
cnf(c_0_572,hypothesis,
a_1086 = store(a_1085,i18,e18),
hyp17,
[final] ).
cnf(c_0_573,hypothesis,
( i19 = X1
| select(a_1087,X1) = select(a_1086,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_566]),
[final] ).
cnf(c_0_574,hypothesis,
( i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| select(a_1087,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_567,c_0_568]),
[final] ).
cnf(c_0_575,hypothesis,
a_1114 = store(a_1113,i14,e14),
hyp45,
[final] ).
cnf(c_0_576,hypothesis,
( i29 = X1
| select(a_1115,X1) = select(a_1114,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_569]),
[final] ).
cnf(c_0_577,hypothesis,
( i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| select(a_1115,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_570,c_0_571]),
[final] ).
cnf(c_0_578,hypothesis,
a_1085 = store(a_1084,i17,e17),
hyp16,
[final] ).
cnf(c_0_579,hypothesis,
( i18 = X1
| select(a_1086,X1) = select(a_1085,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_572]),
[final] ).
cnf(c_0_580,hypothesis,
( i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| select(a_1086,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_573,c_0_574]),
[final] ).
cnf(c_0_581,hypothesis,
a_1113 = store(a_1112,i11,e11),
hyp44,
[final] ).
cnf(c_0_582,hypothesis,
( i14 = X1
| select(a_1114,X1) = select(a_1113,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_575]),
[final] ).
cnf(c_0_583,hypothesis,
( i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| select(a_1114,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_576,c_0_577]),
[final] ).
cnf(c_0_584,hypothesis,
a_1084 = store(a_1083,i16,e16),
hyp15,
[final] ).
cnf(c_0_585,hypothesis,
( i17 = X1
| select(a_1085,X1) = select(a_1084,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_578]),
[final] ).
cnf(c_0_586,hypothesis,
( i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| select(a_1085,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_579,c_0_580]),
[final] ).
cnf(c_0_587,hypothesis,
a_1112 = store(a_1111,i6,e6),
hyp43,
[final] ).
cnf(c_0_588,hypothesis,
( i11 = X1
| select(a_1113,X1) = select(a_1112,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_581]),
[final] ).
cnf(c_0_589,hypothesis,
( i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| select(a_1113,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_582,c_0_583]),
[final] ).
cnf(c_0_590,hypothesis,
a_1083 = store(a_1082,i15,e15),
hyp14,
[final] ).
cnf(c_0_591,hypothesis,
( i16 = X1
| select(a_1084,X1) = select(a_1083,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_584]),
[final] ).
cnf(c_0_592,hypothesis,
( i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| select(a_1084,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_585,c_0_586]),
[final] ).
cnf(c_0_593,hypothesis,
a_1111 = store(a_1110,i21,e21),
hyp42,
[final] ).
cnf(c_0_594,hypothesis,
( i6 = X1
| select(a_1112,X1) = select(a_1111,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_587]),
[final] ).
cnf(c_0_595,hypothesis,
( i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| select(a_1112,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_588,c_0_589]),
[final] ).
cnf(c_0_596,hypothesis,
a_1082 = store(a_1081,i14,e14),
hyp13,
[final] ).
cnf(c_0_597,hypothesis,
( i15 = X1
| select(a_1083,X1) = select(a_1082,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_590]),
[final] ).
cnf(c_0_598,hypothesis,
( i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| select(a_1083,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_591,c_0_592]),
[final] ).
cnf(c_0_599,hypothesis,
a_1110 = store(a_1109,i8,e8),
hyp41,
[final] ).
cnf(c_0_600,hypothesis,
( i21 = X1
| select(a_1111,X1) = select(a_1110,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_593]),
[final] ).
cnf(c_0_601,hypothesis,
( i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| select(a_1111,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_594,c_0_595]),
[final] ).
cnf(c_0_602,hypothesis,
a_1081 = store(a_1080,i13,e13),
hyp12,
[final] ).
cnf(c_0_603,hypothesis,
( i14 = X1
| select(a_1082,X1) = select(a_1081,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_596]),
[final] ).
cnf(c_0_604,hypothesis,
( i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| select(a_1082,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_597,c_0_598]),
[final] ).
cnf(c_0_605,hypothesis,
a_1109 = store(a_1108,i20,e20),
hyp40,
[final] ).
cnf(c_0_606,hypothesis,
( i8 = X1
| select(a_1110,X1) = select(a_1109,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_599]),
[final] ).
cnf(c_0_607,hypothesis,
( i21 = X1
| i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| i6 = X1
| select(a_1110,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_600,c_0_601]),
[final] ).
cnf(c_0_608,hypothesis,
a_1080 = store(a_1079,i12,e12),
hyp11,
[final] ).
cnf(c_0_609,hypothesis,
( i13 = X1
| select(a_1081,X1) = select(a_1080,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_602]),
[final] ).
cnf(c_0_610,hypothesis,
( i14 = X1
| i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| i15 = X1
| select(a_1081,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_603,c_0_604]),
[final] ).
cnf(c_0_611,hypothesis,
a_1108 = store(a_1107,i18,e18),
hyp39,
[final] ).
cnf(c_0_612,hypothesis,
( i20 = X1
| select(a_1109,X1) = select(a_1108,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_605]),
[final] ).
cnf(c_0_613,hypothesis,
( i8 = X1
| i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| i21 = X1
| select(a_1109,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_606,c_0_607]),
[final] ).
cnf(c_0_614,hypothesis,
a_1079 = store(a_1078,i11,e11),
hyp10,
[final] ).
cnf(c_0_615,hypothesis,
( i12 = X1
| select(a_1080,X1) = select(a_1079,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_608]),
[final] ).
cnf(c_0_616,hypothesis,
( i13 = X1
| i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| i14 = X1
| select(a_1080,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_609,c_0_610]),
[final] ).
cnf(c_0_617,hypothesis,
a_1107 = store(a_1106,i25,e25),
hyp38,
[final] ).
cnf(c_0_618,hypothesis,
( i18 = X1
| select(a_1108,X1) = select(a_1107,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_611]),
[final] ).
cnf(c_0_619,hypothesis,
( i20 = X1
| i21 = X1
| i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| i6 = X1
| i8 = X1
| select(a_1108,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_612,c_0_613]),
[final] ).
cnf(c_0_620,hypothesis,
a_1078 = store(a_1077,i10,e10),
hyp9,
[final] ).
cnf(c_0_621,hypothesis,
( i11 = X1
| select(a_1079,X1) = select(a_1078,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_614]),
[final] ).
cnf(c_0_622,hypothesis,
( i12 = X1
| i14 = X1
| i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| i15 = X1
| i13 = X1
| select(a_1079,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_615,c_0_616]),
[final] ).
cnf(c_0_623,hypothesis,
a_1106 = store(a_1105,i15,e15),
hyp37,
[final] ).
cnf(c_0_624,hypothesis,
( i25 = X1
| select(a_1107,X1) = select(a_1106,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_617]),
[final] ).
cnf(c_0_625,hypothesis,
( i18 = X1
| i8 = X1
| i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| i21 = X1
| i20 = X1
| select(a_1107,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_618,c_0_619]),
[final] ).
cnf(c_0_626,hypothesis,
a_1077 = store(a_1076,i9,e9),
hyp8,
[final] ).
cnf(c_0_627,hypothesis,
( i10 = X1
| select(a_1078,X1) = select(a_1077,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_620]),
[final] ).
cnf(c_0_628,hypothesis,
( i11 = X1
| i13 = X1
| i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| i14 = X1
| i12 = X1
| select(a_1078,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_621,c_0_622]),
[final] ).
cnf(c_0_629,hypothesis,
a_1105 = store(a_1104,i2,e2),
hyp36,
[final] ).
cnf(c_0_630,hypothesis,
( i15 = X1
| select(a_1106,X1) = select(a_1105,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_623]),
[final] ).
cnf(c_0_631,hypothesis,
( i25 = X1
| i20 = X1
| i21 = X1
| i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| i6 = X1
| i8 = X1
| i18 = X1
| select(a_1106,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_624,c_0_625]),
[final] ).
cnf(c_0_632,hypothesis,
a_1076 = store(a_1075,i8,e8),
hyp7,
[final] ).
cnf(c_0_633,hypothesis,
( i9 = X1
| select(a_1077,X1) = select(a_1076,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_626]),
[final] ).
cnf(c_0_634,hypothesis,
( i10 = X1
| i12 = X1
| i14 = X1
| i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| i15 = X1
| i13 = X1
| i11 = X1
| select(a_1077,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_627,c_0_628]),
[final] ).
cnf(c_0_635,hypothesis,
a_1104 = store(a_1103,i30,e30),
hyp35,
[final] ).
cnf(c_0_636,hypothesis,
( i2 = X1
| select(a_1105,X1) = select(a_1104,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_629]),
[final] ).
cnf(c_0_637,hypothesis,
( i15 = X1
| i18 = X1
| i8 = X1
| i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| i21 = X1
| i20 = X1
| i25 = X1
| select(a_1105,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_630,c_0_631]),
[final] ).
cnf(c_0_638,hypothesis,
a_1075 = store(a_1074,i7,e7),
hyp6,
[final] ).
cnf(c_0_639,hypothesis,
( i8 = X1
| select(a_1076,X1) = select(a_1075,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_632]),
[final] ).
cnf(c_0_640,hypothesis,
( i9 = X1
| i11 = X1
| i13 = X1
| i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| i14 = X1
| i12 = X1
| i10 = X1
| select(a_1076,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_633,c_0_634]),
[final] ).
cnf(c_0_641,hypothesis,
a_1103 = store(a_1102,i9,e9),
hyp34,
[final] ).
cnf(c_0_642,hypothesis,
( i30 = X1
| select(a_1104,X1) = select(a_1103,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_635]),
[final] ).
cnf(c_0_643,hypothesis,
( i2 = X1
| i25 = X1
| i20 = X1
| i21 = X1
| i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| i6 = X1
| i8 = X1
| i18 = X1
| i15 = X1
| select(a_1104,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_636,c_0_637]),
[final] ).
cnf(c_0_644,hypothesis,
a_1074 = store(a_1073,i6,e6),
hyp5,
[final] ).
cnf(c_0_645,hypothesis,
( i7 = X1
| select(a_1075,X1) = select(a_1074,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_638]),
[final] ).
cnf(c_0_646,hypothesis,
( i8 = X1
| i10 = X1
| i12 = X1
| i14 = X1
| i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| i15 = X1
| i13 = X1
| i11 = X1
| i9 = X1
| select(a_1075,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_639,c_0_640]),
[final] ).
cnf(c_0_647,hypothesis,
a_1102 = store(a_1101,i4,e4),
hyp33,
[final] ).
cnf(c_0_648,hypothesis,
( i9 = X1
| select(a_1103,X1) = select(a_1102,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_641]),
[final] ).
cnf(c_0_649,hypothesis,
( i30 = X1
| i15 = X1
| i18 = X1
| i8 = X1
| i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| i21 = X1
| i20 = X1
| i25 = X1
| i2 = X1
| select(a_1103,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_642,c_0_643]),
[final] ).
cnf(c_0_650,hypothesis,
a_1073 = store(a_1072,i5,e5),
hyp4,
[final] ).
cnf(c_0_651,hypothesis,
( i6 = X1
| select(a_1074,X1) = select(a_1073,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_644]),
[final] ).
cnf(c_0_652,hypothesis,
( i7 = X1
| i9 = X1
| i11 = X1
| i13 = X1
| i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| i14 = X1
| i12 = X1
| i10 = X1
| i8 = X1
| select(a_1074,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_645,c_0_646]),
[final] ).
cnf(c_0_653,hypothesis,
a_1101 = store(a_1100,i19,e19),
hyp32,
[final] ).
cnf(c_0_654,hypothesis,
( i4 = X1
| select(a_1102,X1) = select(a_1101,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_647]),
[final] ).
cnf(c_0_655,hypothesis,
( i9 = X1
| i2 = X1
| i25 = X1
| i20 = X1
| i21 = X1
| i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| i6 = X1
| i8 = X1
| i18 = X1
| i15 = X1
| i30 = X1
| select(a_1102,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_648,c_0_649]),
[final] ).
cnf(c_0_656,hypothesis,
a_1072 = store(a_1071,i4,e4),
hyp3,
[final] ).
cnf(c_0_657,hypothesis,
( i5 = X1
| select(a_1073,X1) = select(a_1072,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_650]),
[final] ).
cnf(c_0_658,hypothesis,
( i6 = X1
| i8 = X1
| i10 = X1
| i12 = X1
| i14 = X1
| i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| i15 = X1
| i13 = X1
| i11 = X1
| i9 = X1
| i7 = X1
| select(a_1073,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_651,c_0_652]),
[final] ).
cnf(c_0_659,hypothesis,
a_1100 = store(a_1099,i1,e1),
hyp31,
[final] ).
cnf(c_0_660,hypothesis,
( i19 = X1
| select(a_1101,X1) = select(a_1100,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_653]),
[final] ).
cnf(c_0_661,hypothesis,
( i4 = X1
| i30 = X1
| i15 = X1
| i18 = X1
| i8 = X1
| i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| i21 = X1
| i20 = X1
| i25 = X1
| i2 = X1
| i9 = X1
| select(a_1101,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_654,c_0_655]),
[final] ).
cnf(c_0_662,hypothesis,
a_1071 = store(a_1070,i3,e3),
hyp2,
[final] ).
cnf(c_0_663,hypothesis,
( i4 = X1
| select(a_1072,X1) = select(a_1071,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_656]),
[final] ).
cnf(c_0_664,hypothesis,
( i5 = X1
| i7 = X1
| i9 = X1
| i11 = X1
| i13 = X1
| i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| i14 = X1
| i12 = X1
| i10 = X1
| i8 = X1
| i6 = X1
| select(a_1072,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_657,c_0_658]),
[final] ).
cnf(c_0_665,hypothesis,
a_1099 = store(a1,i13,e13),
hyp30,
[final] ).
cnf(c_0_666,hypothesis,
( i1 = X1
| select(a_1100,X1) = select(a_1099,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_659]),
[final] ).
cnf(c_0_667,hypothesis,
( i19 = X1
| i9 = X1
| i2 = X1
| i25 = X1
| i20 = X1
| i21 = X1
| i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| i6 = X1
| i8 = X1
| i18 = X1
| i15 = X1
| i30 = X1
| i4 = X1
| select(a_1100,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_660,c_0_661]),
[final] ).
cnf(c_0_668,hypothesis,
a_1070 = store(a_1069,i2,e2),
hyp1,
[final] ).
cnf(c_0_669,hypothesis,
( i3 = X1
| select(a_1071,X1) = select(a_1070,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_662]),
[final] ).
cnf(c_0_670,hypothesis,
( i4 = X1
| i6 = X1
| i8 = X1
| i10 = X1
| i12 = X1
| i14 = X1
| i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| i15 = X1
| i13 = X1
| i11 = X1
| i9 = X1
| i7 = X1
| i5 = X1
| select(a_1071,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_663,c_0_664]),
[final] ).
cnf(c_0_671,hypothesis,
a_1069 = store(a1,i1,e1),
hyp0,
[final] ).
cnf(c_0_672,hypothesis,
( i13 = X1
| select(a_1099,X1) = select(a1,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_665]),
[final] ).
cnf(c_0_673,hypothesis,
( i1 = X1
| i4 = X1
| i30 = X1
| i15 = X1
| i18 = X1
| i8 = X1
| i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| i21 = X1
| i20 = X1
| i25 = X1
| i2 = X1
| i9 = X1
| i19 = X1
| select(a_1099,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_666,c_0_667]),
[final] ).
cnf(c_0_674,hypothesis,
( i2 = X1
| select(a_1070,X1) = select(a_1069,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_668]),
[final] ).
cnf(c_0_675,hypothesis,
( i3 = X1
| i5 = X1
| i7 = X1
| i9 = X1
| i11 = X1
| i13 = X1
| i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| i14 = X1
| i12 = X1
| i10 = X1
| i8 = X1
| i6 = X1
| i4 = X1
| select(a_1070,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_669,c_0_670]),
[final] ).
cnf(c_0_676,hypothesis,
( i1 = X1
| select(a1,X1) = select(a_1069,X1) ),
inference(spm,[status(thm)],[c_0_501,c_0_671]),
[final] ).
cnf(c_0_677,hypothesis,
( i13 = X1
| i19 = X1
| i9 = X1
| i2 = X1
| i25 = X1
| i20 = X1
| i21 = X1
| i11 = X1
| i29 = X1
| i26 = X1
| i27 = X1
| i12 = X1
| i28 = X1
| i23 = X1
| i10 = X1
| i7 = X1
| i24 = X1
| i17 = X1
| i16 = X1
| i3 = X1
| i22 = X1
| i5 = X1
| i14 = X1
| i6 = X1
| i8 = X1
| i18 = X1
| i15 = X1
| i30 = X1
| i4 = X1
| i1 = X1
| select(a1,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_672,c_0_673]),
[final] ).
cnf(c_0_678,hypothesis,
( i2 = X1
| i4 = X1
| i6 = X1
| i8 = X1
| i10 = X1
| i12 = X1
| i14 = X1
| i16 = X1
| i18 = X1
| i20 = X1
| i22 = X1
| i24 = X1
| i26 = X1
| i28 = X1
| i29 = X1
| i1 = X1
| i27 = X1
| i25 = X1
| i23 = X1
| i21 = X1
| i19 = X1
| i17 = X1
| i15 = X1
| i13 = X1
| i11 = X1
| i9 = X1
| i7 = X1
| i5 = X1
| i3 = X1
| select(a_1069,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_674,c_0_675]),
[final] ).
cnf(c_0_679,hypothesis,
( i1 = X1
| i4 = X1
| i30 = X1
| i15 = X1
| i18 = X1
| i8 = X1
| i6 = X1
| i14 = X1
| i5 = X1
| i22 = X1
| i3 = X1
| i16 = X1
| i17 = X1
| i24 = X1
| i7 = X1
| i10 = X1
| i23 = X1
| i28 = X1
| i12 = X1
| i27 = X1
| i26 = X1
| i29 = X1
| i11 = X1
| i21 = X1
| i20 = X1
| i25 = X1
| i2 = X1
| i9 = X1
| i19 = X1
| i13 = X1
| select(a_1069,X1) = select(a_1128,X1) ),
inference(spm,[status(thm)],[c_0_676,c_0_677]),
[final] ).
cnf(c_0_681,axiom,
select(store(X1,X2,X3),X2) = X3,
a1,
[final] ).
cnf(c_0_706,hypothesis,
e_1131 = select(a_1128,i_1129),
hyp61,
[final] ).
cnf(c_0_707,hypothesis,
( i3 = X1
| i5 = X1
| i7 = X1
| i9 = X1
| i11 = X1
| i13 = X1
| i15 = X1
| i17 = X1
| i19 = X1
| i21 = X1
| i23 = X1
| i25 = X1
| i27 = X1
| i1 = X1
| i29 = X1
| i28 = X1
| i26 = X1
| i24 = X1
| i22 = X1
| i20 = X1
| i18 = X1
| i16 = X1
| i14 = X1
| i12 = X1
| i10 = X1
| i8 = X1
| i6 = X1
| i4 = X1
| i2 = X1
| i30 = X1
| select(a_1128,X1) = select(a_1098,X1) ),
inference(spm,[status(thm)],[c_0_678,c_0_679]),
[final] ).
cnf(c_0_708,hypothesis,
e_1130 = select(a_1098,i_1129),
hyp60,
[final] ).
cnf(c_0_709,negated_conjecture,
e_1130 != e_1131,
c_0_680,
[final] ).
cnf(c_0_710,hypothesis,
select(a_1104,i30) = e30,
inference(spm,[status(thm)],[c_0_681,c_0_635]),
[final] ).
cnf(c_0_711,hypothesis,
i15 != i30,
c_0_682,
[final] ).
cnf(c_0_712,hypothesis,
i18 != i30,
c_0_683,
[final] ).
cnf(c_0_713,hypothesis,
i8 != i30,
c_0_684,
[final] ).
cnf(c_0_714,hypothesis,
i6 != i30,
c_0_685,
[final] ).
cnf(c_0_715,hypothesis,
i14 != i30,
c_0_686,
[final] ).
cnf(c_0_716,hypothesis,
i5 != i30,
c_0_687,
[final] ).
cnf(c_0_717,hypothesis,
i22 != i30,
c_0_688,
[final] ).
cnf(c_0_718,hypothesis,
i3 != i30,
c_0_689,
[final] ).
cnf(c_0_719,hypothesis,
i16 != i30,
c_0_690,
[final] ).
cnf(c_0_720,hypothesis,
i17 != i30,
c_0_691,
[final] ).
cnf(c_0_721,hypothesis,
i24 != i30,
c_0_692,
[final] ).
cnf(c_0_722,hypothesis,
i7 != i30,
c_0_693,
[final] ).
cnf(c_0_723,hypothesis,
i10 != i30,
c_0_694,
[final] ).
cnf(c_0_724,hypothesis,
i23 != i30,
c_0_695,
[final] ).
cnf(c_0_725,hypothesis,
i28 != i30,
c_0_696,
[final] ).
cnf(c_0_726,hypothesis,
i12 != i30,
c_0_697,
[final] ).
cnf(c_0_727,hypothesis,
i27 != i30,
c_0_698,
[final] ).
cnf(c_0_728,hypothesis,
i26 != i30,
c_0_699,
[final] ).
cnf(c_0_729,hypothesis,
i29 != i30,
c_0_700,
[final] ).
cnf(c_0_730,hypothesis,
i11 != i30,
c_0_701,
[final] ).
cnf(c_0_731,hypothesis,
i21 != i30,
c_0_702,
[final] ).
cnf(c_0_732,hypothesis,
i20 != i30,
c_0_703,
[final] ).
cnf(c_0_733,hypothesis,
i25 != i30,
c_0_704,
[final] ).
cnf(c_0_734,hypothesis,
i2 != i30,
c_0_705,
[final] ).
cnf(c_0_735,hypothesis,
( i_1129 = i30
| i_1129 = i2
| i_1129 = i4
| i_1129 = i6
| i_1129 = i8
| i_1129 = i10
| i_1129 = i12
| i_1129 = i14
| i_1129 = i16
| i_1129 = i18
| i_1129 = i20
| i_1129 = i22
| i_1129 = i24
| i_1129 = i26
| i_1129 = i28
| i_1129 = i29
| i_1129 = i1
| i_1129 = i27
| i_1129 = i25
| i_1129 = i23
| i_1129 = i21
| i_1129 = i19
| i_1129 = i17
| i_1129 = i15
| i_1129 = i13
| i_1129 = i11
| i_1129 = i9
| i_1129 = i7
| i_1129 = i5
| i_1129 = i3 ),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_706,c_0_707]),c_0_708]),c_0_709]),
[final] ).
cnf(c_0_736,hypothesis,
select(a_1128,i30) = e30,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_710,c_0_643]),c_0_711]),c_0_712]),c_0_713]),c_0_714]),c_0_715]),c_0_716]),c_0_717]),c_0_718]),c_0_719]),c_0_720]),c_0_721]),c_0_722]),c_0_723]),c_0_724]),c_0_725]),c_0_726]),c_0_727]),c_0_728]),c_0_729]),c_0_730]),c_0_731]),c_0_732]),c_0_733]),c_0_734]),
[final] ).
cnf(c_0_1148,hypothesis,
( e30 = e_1131
| i_1129 = i3
| i_1129 = i5
| i_1129 = i7
| i_1129 = i9
| i_1129 = i11
| i_1129 = i13
| i_1129 = i15
| i_1129 = i17
| i_1129 = i19
| i_1129 = i21
| i_1129 = i23
| i_1129 = i25
| i_1129 = i27
| i_1129 = i1
| i_1129 = i29
| i_1129 = i28
| i_1129 = i26
| i_1129 = i24
| i_1129 = i22
| i_1129 = i20
| i_1129 = i18
| i_1129 = i16
| i_1129 = i14
| i_1129 = i12
| i_1129 = i10
| i_1129 = i8
| i_1129 = i6
| i_1129 = i4
| i_1129 = i2 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_706,c_0_735]),c_0_736]),
[final] ).
cnf(c_0_1149,hypothesis,
select(a_1099,i13) = e13,
inference(spm,[status(thm)],[c_0_681,c_0_665]),
[final] ).
cnf(c_0_1150,hypothesis,
i13 != i19,
c_0_737,
[final] ).
cnf(c_0_1151,hypothesis,
i9 != i13,
c_0_738,
[final] ).
cnf(c_0_1152,hypothesis,
i2 != i13,
c_0_739,
[final] ).
cnf(c_0_1153,hypothesis,
i13 != i25,
c_0_740,
[final] ).
cnf(c_0_1154,hypothesis,
i13 != i20,
c_0_741,
[final] ).
cnf(c_0_1155,hypothesis,
i13 != i21,
c_0_742,
[final] ).
cnf(c_0_1156,hypothesis,
i11 != i13,
c_0_743,
[final] ).
cnf(c_0_1157,hypothesis,
i13 != i29,
c_0_744,
[final] ).
cnf(c_0_1158,hypothesis,
i13 != i26,
c_0_745,
[final] ).
cnf(c_0_1159,hypothesis,
i13 != i27,
c_0_746,
[final] ).
cnf(c_0_1160,hypothesis,
i12 != i13,
c_0_747,
[final] ).
cnf(c_0_1161,hypothesis,
i13 != i28,
c_0_748,
[final] ).
cnf(c_0_1162,hypothesis,
i13 != i23,
c_0_749,
[final] ).
cnf(c_0_1163,hypothesis,
i10 != i13,
c_0_750,
[final] ).
cnf(c_0_1164,hypothesis,
i7 != i13,
c_0_751,
[final] ).
cnf(c_0_1165,hypothesis,
i13 != i24,
c_0_752,
[final] ).
cnf(c_0_1166,hypothesis,
i13 != i17,
c_0_753,
[final] ).
cnf(c_0_1167,hypothesis,
i13 != i16,
c_0_754,
[final] ).
cnf(c_0_1168,hypothesis,
i3 != i13,
c_0_755,
[final] ).
cnf(c_0_1169,hypothesis,
i13 != i22,
c_0_756,
[final] ).
cnf(c_0_1170,hypothesis,
i5 != i13,
c_0_757,
[final] ).
cnf(c_0_1171,hypothesis,
i13 != i14,
c_0_758,
[final] ).
cnf(c_0_1172,hypothesis,
i6 != i13,
c_0_759,
[final] ).
cnf(c_0_1173,hypothesis,
i8 != i13,
c_0_760,
[final] ).
cnf(c_0_1174,hypothesis,
i13 != i18,
c_0_761,
[final] ).
cnf(c_0_1175,hypothesis,
i13 != i15,
c_0_762,
[final] ).
cnf(c_0_1176,hypothesis,
i13 != i30,
c_0_763,
[final] ).
cnf(c_0_1177,hypothesis,
i4 != i13,
c_0_764,
[final] ).
cnf(c_0_1178,hypothesis,
i1 != i13,
c_0_765,
[final] ).
cnf(c_0_1179,hypothesis,
select(a_1070,i2) = e2,
inference(spm,[status(thm)],[c_0_681,c_0_668]),
[final] ).
cnf(c_0_1180,hypothesis,
i2 != i4,
c_0_766,
[final] ).
cnf(c_0_1181,hypothesis,
i2 != i6,
c_0_767,
[final] ).
cnf(c_0_1182,hypothesis,
i2 != i8,
c_0_768,
[final] ).
cnf(c_0_1183,hypothesis,
i2 != i10,
c_0_769,
[final] ).
cnf(c_0_1184,hypothesis,
i2 != i12,
c_0_770,
[final] ).
cnf(c_0_1185,hypothesis,
i2 != i14,
c_0_771,
[final] ).
cnf(c_0_1186,hypothesis,
i2 != i16,
c_0_772,
[final] ).
cnf(c_0_1187,hypothesis,
i2 != i18,
c_0_773,
[final] ).
cnf(c_0_1188,hypothesis,
i2 != i20,
c_0_774,
[final] ).
cnf(c_0_1189,hypothesis,
i2 != i22,
c_0_775,
[final] ).
cnf(c_0_1190,hypothesis,
i2 != i24,
c_0_776,
[final] ).
cnf(c_0_1191,hypothesis,
i2 != i26,
c_0_777,
[final] ).
cnf(c_0_1192,hypothesis,
i2 != i28,
c_0_778,
[final] ).
cnf(c_0_1193,hypothesis,
i2 != i29,
c_0_779,
[final] ).
cnf(c_0_1194,hypothesis,
i1 != i2,
c_0_780,
[final] ).
cnf(c_0_1195,hypothesis,
i2 != i27,
c_0_781,
[final] ).
cnf(c_0_1196,hypothesis,
i2 != i25,
c_0_782,
[final] ).
cnf(c_0_1197,hypothesis,
i2 != i23,
c_0_783,
[final] ).
cnf(c_0_1198,hypothesis,
i2 != i21,
c_0_784,
[final] ).
cnf(c_0_1199,hypothesis,
i2 != i19,
c_0_785,
[final] ).
cnf(c_0_1200,hypothesis,
i2 != i17,
c_0_786,
[final] ).
cnf(c_0_1201,hypothesis,
i2 != i15,
c_0_787,
[final] ).
cnf(c_0_1202,hypothesis,
i2 != i11,
c_0_788,
[final] ).
cnf(c_0_1203,hypothesis,
i2 != i9,
c_0_789,
[final] ).
cnf(c_0_1204,hypothesis,
i2 != i7,
c_0_790,
[final] ).
cnf(c_0_1205,hypothesis,
i2 != i5,
c_0_791,
[final] ).
cnf(c_0_1206,hypothesis,
i2 != i3,
c_0_792,
[final] ).
cnf(c_0_1207,hypothesis,
select(a_1100,i1) = e1,
inference(spm,[status(thm)],[c_0_681,c_0_659]),
[final] ).
cnf(c_0_1208,hypothesis,
i1 != i4,
c_0_793,
[final] ).
cnf(c_0_1209,hypothesis,
i1 != i30,
c_0_794,
[final] ).
cnf(c_0_1210,hypothesis,
i1 != i15,
c_0_795,
[final] ).
cnf(c_0_1211,hypothesis,
i1 != i18,
c_0_796,
[final] ).
cnf(c_0_1212,hypothesis,
i1 != i8,
c_0_797,
[final] ).
cnf(c_0_1213,hypothesis,
i1 != i6,
c_0_798,
[final] ).
cnf(c_0_1214,hypothesis,
i1 != i14,
c_0_799,
[final] ).
cnf(c_0_1215,hypothesis,
i1 != i5,
c_0_800,
[final] ).
cnf(c_0_1216,hypothesis,
i1 != i22,
c_0_801,
[final] ).
cnf(c_0_1217,hypothesis,
i1 != i3,
c_0_802,
[final] ).
cnf(c_0_1218,hypothesis,
i1 != i16,
c_0_803,
[final] ).
cnf(c_0_1219,hypothesis,
i1 != i17,
c_0_804,
[final] ).
cnf(c_0_1220,hypothesis,
i1 != i24,
c_0_805,
[final] ).
cnf(c_0_1221,hypothesis,
i1 != i7,
c_0_806,
[final] ).
cnf(c_0_1222,hypothesis,
i1 != i10,
c_0_807,
[final] ).
cnf(c_0_1223,hypothesis,
i1 != i23,
c_0_808,
[final] ).
cnf(c_0_1224,hypothesis,
i1 != i28,
c_0_809,
[final] ).
cnf(c_0_1225,hypothesis,
i1 != i12,
c_0_810,
[final] ).
cnf(c_0_1226,hypothesis,
i1 != i27,
c_0_811,
[final] ).
cnf(c_0_1227,hypothesis,
i1 != i26,
c_0_812,
[final] ).
cnf(c_0_1228,hypothesis,
i1 != i29,
c_0_813,
[final] ).
cnf(c_0_1229,hypothesis,
i1 != i11,
c_0_814,
[final] ).
cnf(c_0_1230,hypothesis,
i1 != i21,
c_0_815,
[final] ).
cnf(c_0_1231,hypothesis,
i1 != i20,
c_0_816,
[final] ).
cnf(c_0_1232,hypothesis,
i1 != i25,
c_0_817,
[final] ).
cnf(c_0_1233,hypothesis,
i1 != i9,
c_0_818,
[final] ).
cnf(c_0_1234,hypothesis,
i1 != i19,
c_0_819,
[final] ).
cnf(c_0_1235,hypothesis,
select(a_1071,i3) = e3,
inference(spm,[status(thm)],[c_0_681,c_0_662]),
[final] ).
cnf(c_0_1236,hypothesis,
i3 != i5,
c_0_820,
[final] ).
cnf(c_0_1237,hypothesis,
i3 != i7,
c_0_821,
[final] ).
cnf(c_0_1238,hypothesis,
i3 != i9,
c_0_822,
[final] ).
cnf(c_0_1239,hypothesis,
i3 != i11,
c_0_823,
[final] ).
cnf(c_0_1240,hypothesis,
i3 != i15,
c_0_824,
[final] ).
cnf(c_0_1241,hypothesis,
i3 != i17,
c_0_825,
[final] ).
cnf(c_0_1242,hypothesis,
i3 != i19,
c_0_826,
[final] ).
cnf(c_0_1243,hypothesis,
i3 != i21,
c_0_827,
[final] ).
cnf(c_0_1244,hypothesis,
i3 != i23,
c_0_828,
[final] ).
cnf(c_0_1245,hypothesis,
i3 != i25,
c_0_829,
[final] ).
cnf(c_0_1246,hypothesis,
i3 != i27,
c_0_830,
[final] ).
cnf(c_0_1247,hypothesis,
i3 != i29,
c_0_831,
[final] ).
cnf(c_0_1248,hypothesis,
i3 != i28,
c_0_832,
[final] ).
cnf(c_0_1249,hypothesis,
i3 != i26,
c_0_833,
[final] ).
cnf(c_0_1250,hypothesis,
i3 != i24,
c_0_834,
[final] ).
cnf(c_0_1251,hypothesis,
i3 != i22,
c_0_835,
[final] ).
cnf(c_0_1252,hypothesis,
i3 != i20,
c_0_836,
[final] ).
cnf(c_0_1253,hypothesis,
i3 != i18,
c_0_837,
[final] ).
cnf(c_0_1254,hypothesis,
i3 != i16,
c_0_838,
[final] ).
cnf(c_0_1255,hypothesis,
i3 != i14,
c_0_839,
[final] ).
cnf(c_0_1256,hypothesis,
i3 != i12,
c_0_840,
[final] ).
cnf(c_0_1257,hypothesis,
i3 != i10,
c_0_841,
[final] ).
cnf(c_0_1258,hypothesis,
i3 != i8,
c_0_842,
[final] ).
cnf(c_0_1259,hypothesis,
i3 != i6,
c_0_843,
[final] ).
cnf(c_0_1260,hypothesis,
i3 != i4,
c_0_844,
[final] ).
cnf(c_0_1261,hypothesis,
select(a_1101,i19) = e19,
inference(spm,[status(thm)],[c_0_681,c_0_653]),
[final] ).
cnf(c_0_1262,hypothesis,
i9 != i19,
c_0_845,
[final] ).
cnf(c_0_1263,hypothesis,
i19 != i25,
c_0_846,
[final] ).
cnf(c_0_1264,hypothesis,
i19 != i20,
c_0_847,
[final] ).
cnf(c_0_1265,hypothesis,
i19 != i21,
c_0_848,
[final] ).
cnf(c_0_1266,hypothesis,
i11 != i19,
c_0_849,
[final] ).
cnf(c_0_1267,hypothesis,
i19 != i29,
c_0_850,
[final] ).
cnf(c_0_1268,hypothesis,
i19 != i26,
c_0_851,
[final] ).
cnf(c_0_1269,hypothesis,
i19 != i27,
c_0_852,
[final] ).
cnf(c_0_1270,hypothesis,
i12 != i19,
c_0_853,
[final] ).
cnf(c_0_1271,hypothesis,
i19 != i28,
c_0_854,
[final] ).
cnf(c_0_1272,hypothesis,
i19 != i23,
c_0_855,
[final] ).
cnf(c_0_1273,hypothesis,
i10 != i19,
c_0_856,
[final] ).
cnf(c_0_1274,hypothesis,
i7 != i19,
c_0_857,
[final] ).
cnf(c_0_1275,hypothesis,
i19 != i24,
c_0_858,
[final] ).
cnf(c_0_1276,hypothesis,
i17 != i19,
c_0_859,
[final] ).
cnf(c_0_1277,hypothesis,
i16 != i19,
c_0_860,
[final] ).
cnf(c_0_1278,hypothesis,
i19 != i22,
c_0_861,
[final] ).
cnf(c_0_1279,hypothesis,
i5 != i19,
c_0_862,
[final] ).
cnf(c_0_1280,hypothesis,
i14 != i19,
c_0_863,
[final] ).
cnf(c_0_1281,hypothesis,
i6 != i19,
c_0_864,
[final] ).
cnf(c_0_1282,hypothesis,
i8 != i19,
c_0_865,
[final] ).
cnf(c_0_1283,hypothesis,
i18 != i19,
c_0_866,
[final] ).
cnf(c_0_1284,hypothesis,
i15 != i19,
c_0_867,
[final] ).
cnf(c_0_1285,hypothesis,
i19 != i30,
c_0_868,
[final] ).
cnf(c_0_1286,hypothesis,
i4 != i19,
c_0_869,
[final] ).
cnf(c_0_1287,hypothesis,
select(a_1072,i4) = e4,
inference(spm,[status(thm)],[c_0_681,c_0_656]),
[final] ).
cnf(c_0_1288,hypothesis,
i4 != i6,
c_0_870,
[final] ).
cnf(c_0_1289,hypothesis,
i4 != i8,
c_0_871,
[final] ).
cnf(c_0_1290,hypothesis,
i4 != i10,
c_0_872,
[final] ).
cnf(c_0_1291,hypothesis,
i4 != i12,
c_0_873,
[final] ).
cnf(c_0_1292,hypothesis,
i4 != i14,
c_0_874,
[final] ).
cnf(c_0_1293,hypothesis,
i4 != i16,
c_0_875,
[final] ).
cnf(c_0_1294,hypothesis,
i4 != i18,
c_0_876,
[final] ).
cnf(c_0_1295,hypothesis,
i4 != i20,
c_0_877,
[final] ).
cnf(c_0_1296,hypothesis,
i4 != i22,
c_0_878,
[final] ).
cnf(c_0_1297,hypothesis,
i4 != i24,
c_0_879,
[final] ).
cnf(c_0_1298,hypothesis,
i4 != i26,
c_0_880,
[final] ).
cnf(c_0_1299,hypothesis,
i4 != i28,
c_0_881,
[final] ).
cnf(c_0_1300,hypothesis,
i4 != i29,
c_0_882,
[final] ).
cnf(c_0_1301,hypothesis,
i4 != i27,
c_0_883,
[final] ).
cnf(c_0_1302,hypothesis,
i4 != i25,
c_0_884,
[final] ).
cnf(c_0_1303,hypothesis,
i4 != i23,
c_0_885,
[final] ).
cnf(c_0_1304,hypothesis,
i4 != i21,
c_0_886,
[final] ).
cnf(c_0_1305,hypothesis,
i4 != i17,
c_0_887,
[final] ).
cnf(c_0_1306,hypothesis,
i4 != i15,
c_0_888,
[final] ).
cnf(c_0_1307,hypothesis,
i4 != i11,
c_0_889,
[final] ).
cnf(c_0_1308,hypothesis,
i4 != i9,
c_0_890,
[final] ).
cnf(c_0_1309,hypothesis,
i4 != i7,
c_0_891,
[final] ).
cnf(c_0_1310,hypothesis,
i4 != i5,
c_0_892,
[final] ).
cnf(c_0_1311,hypothesis,
select(a_1102,i4) = e4,
inference(spm,[status(thm)],[c_0_681,c_0_647]),
[final] ).
cnf(c_0_1312,hypothesis,
i4 != i30,
c_0_893,
[final] ).
cnf(c_0_1313,hypothesis,
select(a_1073,i5) = e5,
inference(spm,[status(thm)],[c_0_681,c_0_650]),
[final] ).
cnf(c_0_1314,hypothesis,
i5 != i7,
c_0_894,
[final] ).
cnf(c_0_1315,hypothesis,
i5 != i9,
c_0_895,
[final] ).
cnf(c_0_1316,hypothesis,
i5 != i11,
c_0_896,
[final] ).
cnf(c_0_1317,hypothesis,
i5 != i15,
c_0_897,
[final] ).
cnf(c_0_1318,hypothesis,
i5 != i17,
c_0_898,
[final] ).
cnf(c_0_1319,hypothesis,
i5 != i21,
c_0_899,
[final] ).
cnf(c_0_1320,hypothesis,
i5 != i23,
c_0_900,
[final] ).
cnf(c_0_1321,hypothesis,
i5 != i25,
c_0_901,
[final] ).
cnf(c_0_1322,hypothesis,
i5 != i27,
c_0_902,
[final] ).
cnf(c_0_1323,hypothesis,
i5 != i29,
c_0_903,
[final] ).
cnf(c_0_1324,hypothesis,
i5 != i28,
c_0_904,
[final] ).
cnf(c_0_1325,hypothesis,
i5 != i26,
c_0_905,
[final] ).
cnf(c_0_1326,hypothesis,
i5 != i24,
c_0_906,
[final] ).
cnf(c_0_1327,hypothesis,
i5 != i22,
c_0_907,
[final] ).
cnf(c_0_1328,hypothesis,
i5 != i20,
c_0_908,
[final] ).
cnf(c_0_1329,hypothesis,
i5 != i18,
c_0_909,
[final] ).
cnf(c_0_1330,hypothesis,
i5 != i16,
c_0_910,
[final] ).
cnf(c_0_1331,hypothesis,
i5 != i14,
c_0_911,
[final] ).
cnf(c_0_1332,hypothesis,
i5 != i12,
c_0_912,
[final] ).
cnf(c_0_1333,hypothesis,
i5 != i10,
c_0_913,
[final] ).
cnf(c_0_1334,hypothesis,
i5 != i8,
c_0_914,
[final] ).
cnf(c_0_1335,hypothesis,
i5 != i6,
c_0_915,
[final] ).
cnf(c_0_1336,hypothesis,
select(a_1103,i9) = e9,
inference(spm,[status(thm)],[c_0_681,c_0_641]),
[final] ).
cnf(c_0_1337,hypothesis,
i9 != i25,
c_0_916,
[final] ).
cnf(c_0_1338,hypothesis,
i9 != i20,
c_0_917,
[final] ).
cnf(c_0_1339,hypothesis,
i9 != i21,
c_0_918,
[final] ).
cnf(c_0_1340,hypothesis,
i9 != i11,
c_0_919,
[final] ).
cnf(c_0_1341,hypothesis,
i9 != i29,
c_0_920,
[final] ).
cnf(c_0_1342,hypothesis,
i9 != i26,
c_0_921,
[final] ).
cnf(c_0_1343,hypothesis,
i9 != i27,
c_0_922,
[final] ).
cnf(c_0_1344,hypothesis,
i9 != i12,
c_0_923,
[final] ).
cnf(c_0_1345,hypothesis,
i9 != i28,
c_0_924,
[final] ).
cnf(c_0_1346,hypothesis,
i9 != i23,
c_0_925,
[final] ).
cnf(c_0_1347,hypothesis,
i9 != i10,
c_0_926,
[final] ).
cnf(c_0_1348,hypothesis,
i7 != i9,
c_0_927,
[final] ).
cnf(c_0_1349,hypothesis,
i9 != i24,
c_0_928,
[final] ).
cnf(c_0_1350,hypothesis,
i9 != i17,
c_0_929,
[final] ).
cnf(c_0_1351,hypothesis,
i9 != i16,
c_0_930,
[final] ).
cnf(c_0_1352,hypothesis,
i9 != i22,
c_0_931,
[final] ).
cnf(c_0_1353,hypothesis,
i9 != i14,
c_0_932,
[final] ).
cnf(c_0_1354,hypothesis,
i6 != i9,
c_0_933,
[final] ).
cnf(c_0_1355,hypothesis,
i8 != i9,
c_0_934,
[final] ).
cnf(c_0_1356,hypothesis,
i9 != i18,
c_0_935,
[final] ).
cnf(c_0_1357,hypothesis,
i9 != i15,
c_0_936,
[final] ).
cnf(c_0_1358,hypothesis,
i9 != i30,
c_0_937,
[final] ).
cnf(c_0_1359,hypothesis,
select(a_1074,i6) = e6,
inference(spm,[status(thm)],[c_0_681,c_0_644]),
[final] ).
cnf(c_0_1360,hypothesis,
i6 != i8,
c_0_938,
[final] ).
cnf(c_0_1361,hypothesis,
i6 != i10,
c_0_939,
[final] ).
cnf(c_0_1362,hypothesis,
i6 != i12,
c_0_940,
[final] ).
cnf(c_0_1363,hypothesis,
i6 != i14,
c_0_941,
[final] ).
cnf(c_0_1364,hypothesis,
i6 != i16,
c_0_942,
[final] ).
cnf(c_0_1365,hypothesis,
i6 != i18,
c_0_943,
[final] ).
cnf(c_0_1366,hypothesis,
i6 != i20,
c_0_944,
[final] ).
cnf(c_0_1367,hypothesis,
i6 != i22,
c_0_945,
[final] ).
cnf(c_0_1368,hypothesis,
i6 != i24,
c_0_946,
[final] ).
cnf(c_0_1369,hypothesis,
i6 != i26,
c_0_947,
[final] ).
cnf(c_0_1370,hypothesis,
i6 != i28,
c_0_948,
[final] ).
cnf(c_0_1371,hypothesis,
i6 != i29,
c_0_949,
[final] ).
cnf(c_0_1372,hypothesis,
i6 != i27,
c_0_950,
[final] ).
cnf(c_0_1373,hypothesis,
i6 != i25,
c_0_951,
[final] ).
cnf(c_0_1374,hypothesis,
i6 != i23,
c_0_952,
[final] ).
cnf(c_0_1375,hypothesis,
i6 != i21,
c_0_953,
[final] ).
cnf(c_0_1376,hypothesis,
i6 != i17,
c_0_954,
[final] ).
cnf(c_0_1377,hypothesis,
i6 != i15,
c_0_955,
[final] ).
cnf(c_0_1378,hypothesis,
i6 != i11,
c_0_956,
[final] ).
cnf(c_0_1379,hypothesis,
i6 != i7,
c_0_957,
[final] ).
cnf(c_0_1380,hypothesis,
select(a_1075,i7) = e7,
inference(spm,[status(thm)],[c_0_681,c_0_638]),
[final] ).
cnf(c_0_1381,hypothesis,
i7 != i11,
c_0_958,
[final] ).
cnf(c_0_1382,hypothesis,
i7 != i15,
c_0_959,
[final] ).
cnf(c_0_1383,hypothesis,
i7 != i17,
c_0_960,
[final] ).
cnf(c_0_1384,hypothesis,
i7 != i21,
c_0_961,
[final] ).
cnf(c_0_1385,hypothesis,
i7 != i23,
c_0_962,
[final] ).
cnf(c_0_1386,hypothesis,
i7 != i25,
c_0_963,
[final] ).
cnf(c_0_1387,hypothesis,
i7 != i27,
c_0_964,
[final] ).
cnf(c_0_1388,hypothesis,
i7 != i29,
c_0_965,
[final] ).
cnf(c_0_1389,hypothesis,
i7 != i28,
c_0_966,
[final] ).
cnf(c_0_1390,hypothesis,
i7 != i26,
c_0_967,
[final] ).
cnf(c_0_1391,hypothesis,
i7 != i24,
c_0_968,
[final] ).
cnf(c_0_1392,hypothesis,
i7 != i22,
c_0_969,
[final] ).
cnf(c_0_1393,hypothesis,
i7 != i20,
c_0_970,
[final] ).
cnf(c_0_1394,hypothesis,
i7 != i18,
c_0_971,
[final] ).
cnf(c_0_1395,hypothesis,
i7 != i16,
c_0_972,
[final] ).
cnf(c_0_1396,hypothesis,
i7 != i14,
c_0_973,
[final] ).
cnf(c_0_1397,hypothesis,
i7 != i12,
c_0_974,
[final] ).
cnf(c_0_1398,hypothesis,
i7 != i10,
c_0_975,
[final] ).
cnf(c_0_1399,hypothesis,
i7 != i8,
c_0_976,
[final] ).
cnf(c_0_1400,hypothesis,
select(a_1105,i2) = e2,
inference(spm,[status(thm)],[c_0_681,c_0_629]),
[final] ).
cnf(c_0_1401,hypothesis,
select(a_1076,i8) = e8,
inference(spm,[status(thm)],[c_0_681,c_0_632]),
[final] ).
cnf(c_0_1402,hypothesis,
i8 != i10,
c_0_977,
[final] ).
cnf(c_0_1403,hypothesis,
i8 != i12,
c_0_978,
[final] ).
cnf(c_0_1404,hypothesis,
i8 != i14,
c_0_979,
[final] ).
cnf(c_0_1405,hypothesis,
i8 != i16,
c_0_980,
[final] ).
cnf(c_0_1406,hypothesis,
i8 != i18,
c_0_981,
[final] ).
cnf(c_0_1407,hypothesis,
i8 != i20,
c_0_982,
[final] ).
cnf(c_0_1408,hypothesis,
i8 != i22,
c_0_983,
[final] ).
cnf(c_0_1409,hypothesis,
i8 != i24,
c_0_984,
[final] ).
cnf(c_0_1410,hypothesis,
i8 != i26,
c_0_985,
[final] ).
cnf(c_0_1411,hypothesis,
i8 != i28,
c_0_986,
[final] ).
cnf(c_0_1412,hypothesis,
i8 != i29,
c_0_987,
[final] ).
cnf(c_0_1413,hypothesis,
i8 != i27,
c_0_988,
[final] ).
cnf(c_0_1414,hypothesis,
i8 != i25,
c_0_989,
[final] ).
cnf(c_0_1415,hypothesis,
i8 != i23,
c_0_990,
[final] ).
cnf(c_0_1416,hypothesis,
i8 != i21,
c_0_991,
[final] ).
cnf(c_0_1417,hypothesis,
i8 != i17,
c_0_992,
[final] ).
cnf(c_0_1418,hypothesis,
i8 != i15,
c_0_993,
[final] ).
cnf(c_0_1419,hypothesis,
i8 != i11,
c_0_994,
[final] ).
cnf(c_0_1420,hypothesis,
select(a_1106,i15) = e15,
inference(spm,[status(thm)],[c_0_681,c_0_623]),
[final] ).
cnf(c_0_1421,hypothesis,
i15 != i18,
c_0_995,
[final] ).
cnf(c_0_1422,hypothesis,
i14 != i15,
c_0_996,
[final] ).
cnf(c_0_1423,hypothesis,
i15 != i22,
c_0_997,
[final] ).
cnf(c_0_1424,hypothesis,
i15 != i16,
c_0_998,
[final] ).
cnf(c_0_1425,hypothesis,
i15 != i17,
c_0_999,
[final] ).
cnf(c_0_1426,hypothesis,
i15 != i24,
c_0_1000,
[final] ).
cnf(c_0_1427,hypothesis,
i10 != i15,
c_0_1001,
[final] ).
cnf(c_0_1428,hypothesis,
i15 != i23,
c_0_1002,
[final] ).
cnf(c_0_1429,hypothesis,
i15 != i28,
c_0_1003,
[final] ).
cnf(c_0_1430,hypothesis,
i12 != i15,
c_0_1004,
[final] ).
cnf(c_0_1431,hypothesis,
i15 != i27,
c_0_1005,
[final] ).
cnf(c_0_1432,hypothesis,
i15 != i26,
c_0_1006,
[final] ).
cnf(c_0_1433,hypothesis,
i15 != i29,
c_0_1007,
[final] ).
cnf(c_0_1434,hypothesis,
i11 != i15,
c_0_1008,
[final] ).
cnf(c_0_1435,hypothesis,
i15 != i21,
c_0_1009,
[final] ).
cnf(c_0_1436,hypothesis,
i15 != i20,
c_0_1010,
[final] ).
cnf(c_0_1437,hypothesis,
i15 != i25,
c_0_1011,
[final] ).
cnf(c_0_1438,hypothesis,
select(a_1077,i9) = e9,
inference(spm,[status(thm)],[c_0_681,c_0_626]),
[final] ).
cnf(c_0_1439,hypothesis,
select(a_1107,i25) = e25,
inference(spm,[status(thm)],[c_0_681,c_0_617]),
[final] ).
cnf(c_0_1440,hypothesis,
i20 != i25,
c_0_1012,
[final] ).
cnf(c_0_1441,hypothesis,
i21 != i25,
c_0_1013,
[final] ).
cnf(c_0_1442,hypothesis,
i11 != i25,
c_0_1014,
[final] ).
cnf(c_0_1443,hypothesis,
i25 != i29,
c_0_1015,
[final] ).
cnf(c_0_1444,hypothesis,
i25 != i26,
c_0_1016,
[final] ).
cnf(c_0_1445,hypothesis,
i25 != i27,
c_0_1017,
[final] ).
cnf(c_0_1446,hypothesis,
i12 != i25,
c_0_1018,
[final] ).
cnf(c_0_1447,hypothesis,
i25 != i28,
c_0_1019,
[final] ).
cnf(c_0_1448,hypothesis,
i23 != i25,
c_0_1020,
[final] ).
cnf(c_0_1449,hypothesis,
i10 != i25,
c_0_1021,
[final] ).
cnf(c_0_1450,hypothesis,
i24 != i25,
c_0_1022,
[final] ).
cnf(c_0_1451,hypothesis,
i17 != i25,
c_0_1023,
[final] ).
cnf(c_0_1452,hypothesis,
i16 != i25,
c_0_1024,
[final] ).
cnf(c_0_1453,hypothesis,
i22 != i25,
c_0_1025,
[final] ).
cnf(c_0_1454,hypothesis,
i14 != i25,
c_0_1026,
[final] ).
cnf(c_0_1455,hypothesis,
i18 != i25,
c_0_1027,
[final] ).
cnf(c_0_1456,hypothesis,
select(a_1078,i10) = e10,
inference(spm,[status(thm)],[c_0_681,c_0_620]),
[final] ).
cnf(c_0_1457,hypothesis,
i10 != i12,
c_0_1028,
[final] ).
cnf(c_0_1458,hypothesis,
i10 != i14,
c_0_1029,
[final] ).
cnf(c_0_1459,hypothesis,
i10 != i16,
c_0_1030,
[final] ).
cnf(c_0_1460,hypothesis,
i10 != i18,
c_0_1031,
[final] ).
cnf(c_0_1461,hypothesis,
i10 != i20,
c_0_1032,
[final] ).
cnf(c_0_1462,hypothesis,
i10 != i22,
c_0_1033,
[final] ).
cnf(c_0_1463,hypothesis,
i10 != i24,
c_0_1034,
[final] ).
cnf(c_0_1464,hypothesis,
i10 != i26,
c_0_1035,
[final] ).
cnf(c_0_1465,hypothesis,
i10 != i28,
c_0_1036,
[final] ).
cnf(c_0_1466,hypothesis,
i10 != i29,
c_0_1037,
[final] ).
cnf(c_0_1467,hypothesis,
i10 != i27,
c_0_1038,
[final] ).
cnf(c_0_1468,hypothesis,
i10 != i23,
c_0_1039,
[final] ).
cnf(c_0_1469,hypothesis,
i10 != i21,
c_0_1040,
[final] ).
cnf(c_0_1470,hypothesis,
i10 != i17,
c_0_1041,
[final] ).
cnf(c_0_1471,hypothesis,
i10 != i11,
c_0_1042,
[final] ).
cnf(c_0_1472,hypothesis,
select(a_1108,i18) = e18,
inference(spm,[status(thm)],[c_0_681,c_0_611]),
[final] ).
cnf(c_0_1473,hypothesis,
i14 != i18,
c_0_1043,
[final] ).
cnf(c_0_1474,hypothesis,
i18 != i22,
c_0_1044,
[final] ).
cnf(c_0_1475,hypothesis,
i16 != i18,
c_0_1045,
[final] ).
cnf(c_0_1476,hypothesis,
i17 != i18,
c_0_1046,
[final] ).
cnf(c_0_1477,hypothesis,
i18 != i24,
c_0_1047,
[final] ).
cnf(c_0_1478,hypothesis,
i18 != i23,
c_0_1048,
[final] ).
cnf(c_0_1479,hypothesis,
i18 != i28,
c_0_1049,
[final] ).
cnf(c_0_1480,hypothesis,
i12 != i18,
c_0_1050,
[final] ).
cnf(c_0_1481,hypothesis,
i18 != i27,
c_0_1051,
[final] ).
cnf(c_0_1482,hypothesis,
i18 != i26,
c_0_1052,
[final] ).
cnf(c_0_1483,hypothesis,
i18 != i29,
c_0_1053,
[final] ).
cnf(c_0_1484,hypothesis,
i11 != i18,
c_0_1054,
[final] ).
cnf(c_0_1485,hypothesis,
i18 != i21,
c_0_1055,
[final] ).
cnf(c_0_1486,hypothesis,
i18 != i20,
c_0_1056,
[final] ).
cnf(c_0_1487,hypothesis,
select(a_1079,i11) = e11,
inference(spm,[status(thm)],[c_0_681,c_0_614]),
[final] ).
cnf(c_0_1488,hypothesis,
i11 != i17,
c_0_1057,
[final] ).
cnf(c_0_1489,hypothesis,
i11 != i21,
c_0_1058,
[final] ).
cnf(c_0_1490,hypothesis,
i11 != i23,
c_0_1059,
[final] ).
cnf(c_0_1491,hypothesis,
i11 != i27,
c_0_1060,
[final] ).
cnf(c_0_1492,hypothesis,
i11 != i29,
c_0_1061,
[final] ).
cnf(c_0_1493,hypothesis,
i11 != i28,
c_0_1062,
[final] ).
cnf(c_0_1494,hypothesis,
i11 != i26,
c_0_1063,
[final] ).
cnf(c_0_1495,hypothesis,
i11 != i24,
c_0_1064,
[final] ).
cnf(c_0_1496,hypothesis,
i11 != i22,
c_0_1065,
[final] ).
cnf(c_0_1497,hypothesis,
i11 != i20,
c_0_1066,
[final] ).
cnf(c_0_1498,hypothesis,
i11 != i16,
c_0_1067,
[final] ).
cnf(c_0_1499,hypothesis,
i11 != i14,
c_0_1068,
[final] ).
cnf(c_0_1500,hypothesis,
i11 != i12,
c_0_1069,
[final] ).
cnf(c_0_1501,hypothesis,
select(a_1109,i20) = e20,
inference(spm,[status(thm)],[c_0_681,c_0_605]),
[final] ).
cnf(c_0_1502,hypothesis,
i20 != i21,
c_0_1070,
[final] ).
cnf(c_0_1503,hypothesis,
i20 != i29,
c_0_1071,
[final] ).
cnf(c_0_1504,hypothesis,
i20 != i26,
c_0_1072,
[final] ).
cnf(c_0_1505,hypothesis,
i20 != i27,
c_0_1073,
[final] ).
cnf(c_0_1506,hypothesis,
i12 != i20,
c_0_1074,
[final] ).
cnf(c_0_1507,hypothesis,
i20 != i28,
c_0_1075,
[final] ).
cnf(c_0_1508,hypothesis,
i20 != i23,
c_0_1076,
[final] ).
cnf(c_0_1509,hypothesis,
i20 != i24,
c_0_1077,
[final] ).
cnf(c_0_1510,hypothesis,
i17 != i20,
c_0_1078,
[final] ).
cnf(c_0_1511,hypothesis,
i16 != i20,
c_0_1079,
[final] ).
cnf(c_0_1512,hypothesis,
i20 != i22,
c_0_1080,
[final] ).
cnf(c_0_1513,hypothesis,
i14 != i20,
c_0_1081,
[final] ).
cnf(c_0_1514,hypothesis,
select(a_1080,i12) = e12,
inference(spm,[status(thm)],[c_0_681,c_0_608]),
[final] ).
cnf(c_0_1515,hypothesis,
i12 != i14,
c_0_1082,
[final] ).
cnf(c_0_1516,hypothesis,
i12 != i16,
c_0_1083,
[final] ).
cnf(c_0_1517,hypothesis,
i12 != i22,
c_0_1084,
[final] ).
cnf(c_0_1518,hypothesis,
i12 != i24,
c_0_1085,
[final] ).
cnf(c_0_1519,hypothesis,
i12 != i26,
c_0_1086,
[final] ).
cnf(c_0_1520,hypothesis,
i12 != i28,
c_0_1087,
[final] ).
cnf(c_0_1521,hypothesis,
i12 != i29,
c_0_1088,
[final] ).
cnf(c_0_1522,hypothesis,
i12 != i27,
c_0_1089,
[final] ).
cnf(c_0_1523,hypothesis,
i12 != i23,
c_0_1090,
[final] ).
cnf(c_0_1524,hypothesis,
i12 != i21,
c_0_1091,
[final] ).
cnf(c_0_1525,hypothesis,
i12 != i17,
c_0_1092,
[final] ).
cnf(c_0_1526,hypothesis,
select(a_1110,i8) = e8,
inference(spm,[status(thm)],[c_0_681,c_0_599]),
[final] ).
cnf(c_0_1527,hypothesis,
select(a_1081,i13) = e13,
inference(spm,[status(thm)],[c_0_681,c_0_602]),
[final] ).
cnf(c_0_1528,hypothesis,
select(a_1111,i21) = e21,
inference(spm,[status(thm)],[c_0_681,c_0_593]),
[final] ).
cnf(c_0_1529,hypothesis,
i21 != i29,
c_0_1093,
[final] ).
cnf(c_0_1530,hypothesis,
i21 != i26,
c_0_1094,
[final] ).
cnf(c_0_1531,hypothesis,
i21 != i27,
c_0_1095,
[final] ).
cnf(c_0_1532,hypothesis,
i21 != i28,
c_0_1096,
[final] ).
cnf(c_0_1533,hypothesis,
i21 != i23,
c_0_1097,
[final] ).
cnf(c_0_1534,hypothesis,
i21 != i24,
c_0_1098,
[final] ).
cnf(c_0_1535,hypothesis,
i17 != i21,
c_0_1099,
[final] ).
cnf(c_0_1536,hypothesis,
i16 != i21,
c_0_1100,
[final] ).
cnf(c_0_1537,hypothesis,
i21 != i22,
c_0_1101,
[final] ).
cnf(c_0_1538,hypothesis,
i14 != i21,
c_0_1102,
[final] ).
cnf(c_0_1539,hypothesis,
select(a_1082,i14) = e14,
inference(spm,[status(thm)],[c_0_681,c_0_596]),
[final] ).
cnf(c_0_1540,hypothesis,
i14 != i16,
c_0_1103,
[final] ).
cnf(c_0_1541,hypothesis,
i14 != i22,
c_0_1104,
[final] ).
cnf(c_0_1542,hypothesis,
i14 != i24,
c_0_1105,
[final] ).
cnf(c_0_1543,hypothesis,
i14 != i26,
c_0_1106,
[final] ).
cnf(c_0_1544,hypothesis,
i14 != i28,
c_0_1107,
[final] ).
cnf(c_0_1545,hypothesis,
i14 != i29,
c_0_1108,
[final] ).
cnf(c_0_1546,hypothesis,
i14 != i27,
c_0_1109,
[final] ).
cnf(c_0_1547,hypothesis,
i14 != i23,
c_0_1110,
[final] ).
cnf(c_0_1548,hypothesis,
i14 != i17,
c_0_1111,
[final] ).
cnf(c_0_1549,hypothesis,
select(a_1112,i6) = e6,
inference(spm,[status(thm)],[c_0_681,c_0_587]),
[final] ).
cnf(c_0_1550,hypothesis,
select(a_1083,i15) = e15,
inference(spm,[status(thm)],[c_0_681,c_0_590]),
[final] ).
cnf(c_0_1551,hypothesis,
select(a_1113,i11) = e11,
inference(spm,[status(thm)],[c_0_681,c_0_581]),
[final] ).
cnf(c_0_1552,hypothesis,
select(a_1084,i16) = e16,
inference(spm,[status(thm)],[c_0_681,c_0_584]),
[final] ).
cnf(c_0_1553,hypothesis,
i16 != i22,
c_0_1112,
[final] ).
cnf(c_0_1554,hypothesis,
i16 != i24,
c_0_1113,
[final] ).
cnf(c_0_1555,hypothesis,
i16 != i26,
c_0_1114,
[final] ).
cnf(c_0_1556,hypothesis,
i16 != i28,
c_0_1115,
[final] ).
cnf(c_0_1557,hypothesis,
i16 != i29,
c_0_1116,
[final] ).
cnf(c_0_1558,hypothesis,
i16 != i27,
c_0_1117,
[final] ).
cnf(c_0_1559,hypothesis,
i16 != i23,
c_0_1118,
[final] ).
cnf(c_0_1560,hypothesis,
i16 != i17,
c_0_1119,
[final] ).
cnf(c_0_1561,hypothesis,
select(a_1114,i14) = e14,
inference(spm,[status(thm)],[c_0_681,c_0_575]),
[final] ).
cnf(c_0_1562,hypothesis,
select(a_1085,i17) = e17,
inference(spm,[status(thm)],[c_0_681,c_0_578]),
[final] ).
cnf(c_0_1563,hypothesis,
i17 != i23,
c_0_1120,
[final] ).
cnf(c_0_1564,hypothesis,
i17 != i27,
c_0_1121,
[final] ).
cnf(c_0_1565,hypothesis,
i17 != i29,
c_0_1122,
[final] ).
cnf(c_0_1566,hypothesis,
i17 != i28,
c_0_1123,
[final] ).
cnf(c_0_1567,hypothesis,
i17 != i26,
c_0_1124,
[final] ).
cnf(c_0_1568,hypothesis,
i17 != i24,
c_0_1125,
[final] ).
cnf(c_0_1569,hypothesis,
i17 != i22,
c_0_1126,
[final] ).
cnf(c_0_1570,hypothesis,
select(a_1115,i29) = e29,
inference(spm,[status(thm)],[c_0_681,c_0_569]),
[final] ).
cnf(c_0_1571,hypothesis,
i26 != i29,
c_0_1127,
[final] ).
cnf(c_0_1572,hypothesis,
i27 != i29,
c_0_1128,
[final] ).
cnf(c_0_1573,hypothesis,
i28 != i29,
c_0_1129,
[final] ).
cnf(c_0_1574,hypothesis,
i23 != i29,
c_0_1130,
[final] ).
cnf(c_0_1575,hypothesis,
i24 != i29,
c_0_1131,
[final] ).
cnf(c_0_1576,hypothesis,
i22 != i29,
c_0_1132,
[final] ).
cnf(c_0_1577,hypothesis,
select(a_1086,i18) = e18,
inference(spm,[status(thm)],[c_0_681,c_0_572]),
[final] ).
cnf(c_0_1578,hypothesis,
select(a_1116,i5) = e5,
inference(spm,[status(thm)],[c_0_681,c_0_563]),
[final] ).
cnf(c_0_1579,hypothesis,
select(a_1087,i19) = e19,
inference(spm,[status(thm)],[c_0_681,c_0_566]),
[final] ).
cnf(c_0_1580,hypothesis,
select(a_1117,i26) = e26,
inference(spm,[status(thm)],[c_0_681,c_0_557]),
[final] ).
cnf(c_0_1581,hypothesis,
i26 != i27,
c_0_1133,
[final] ).
cnf(c_0_1582,hypothesis,
i26 != i28,
c_0_1134,
[final] ).
cnf(c_0_1583,hypothesis,
i23 != i26,
c_0_1135,
[final] ).
cnf(c_0_1584,hypothesis,
i24 != i26,
c_0_1136,
[final] ).
cnf(c_0_1585,hypothesis,
i22 != i26,
c_0_1137,
[final] ).
cnf(c_0_1586,hypothesis,
select(a_1088,i20) = e20,
inference(spm,[status(thm)],[c_0_681,c_0_560]),
[final] ).
cnf(c_0_1587,hypothesis,
select(a_1118,i22) = e22,
inference(spm,[status(thm)],[c_0_681,c_0_551]),
[final] ).
cnf(c_0_1588,hypothesis,
i22 != i24,
c_0_1138,
[final] ).
cnf(c_0_1589,hypothesis,
i22 != i23,
c_0_1139,
[final] ).
cnf(c_0_1590,hypothesis,
i22 != i28,
c_0_1140,
[final] ).
cnf(c_0_1591,hypothesis,
i22 != i27,
c_0_1141,
[final] ).
cnf(c_0_1592,hypothesis,
select(a_1089,i21) = e21,
inference(spm,[status(thm)],[c_0_681,c_0_554]),
[final] ).
cnf(c_0_1593,hypothesis,
select(a_1119,i27) = e27,
inference(spm,[status(thm)],[c_0_681,c_0_545]),
[final] ).
cnf(c_0_1594,hypothesis,
i27 != i28,
c_0_1142,
[final] ).
cnf(c_0_1595,hypothesis,
i23 != i27,
c_0_1143,
[final] ).
cnf(c_0_1596,hypothesis,
i24 != i27,
c_0_1144,
[final] ).
cnf(c_0_1597,hypothesis,
select(a_1090,i22) = e22,
inference(spm,[status(thm)],[c_0_681,c_0_548]),
[final] ).
cnf(c_0_1598,hypothesis,
select(a_1120,i3) = e3,
inference(spm,[status(thm)],[c_0_681,c_0_539]),
[final] ).
cnf(c_0_1599,hypothesis,
select(a_1091,i23) = e23,
inference(spm,[status(thm)],[c_0_681,c_0_542]),
[final] ).
cnf(c_0_1600,hypothesis,
i23 != i28,
c_0_1145,
[final] ).
cnf(c_0_1601,hypothesis,
i23 != i24,
c_0_1146,
[final] ).
cnf(c_0_1602,hypothesis,
select(a_1121,i12) = e12,
inference(spm,[status(thm)],[c_0_681,c_0_533]),
[final] ).
cnf(c_0_1603,hypothesis,
select(a_1092,i24) = e24,
inference(spm,[status(thm)],[c_0_681,c_0_536]),
[final] ).
cnf(c_0_1604,hypothesis,
i24 != i28,
c_0_1147,
[final] ).
cnf(c_0_1605,hypothesis,
select(a_1122,i16) = e16,
inference(spm,[status(thm)],[c_0_681,c_0_527]),
[final] ).
cnf(c_0_1606,hypothesis,
select(a_1093,i25) = e25,
inference(spm,[status(thm)],[c_0_681,c_0_530]),
[final] ).
cnf(c_0_1607,hypothesis,
select(a_1123,i28) = e28,
inference(spm,[status(thm)],[c_0_681,c_0_521]),
[final] ).
cnf(c_0_1608,hypothesis,
select(a_1094,i26) = e26,
inference(spm,[status(thm)],[c_0_681,c_0_524]),
[final] ).
cnf(c_0_1609,hypothesis,
select(a_1124,i17) = e17,
inference(spm,[status(thm)],[c_0_681,c_0_515]),
[final] ).
cnf(c_0_1610,hypothesis,
select(a_1095,i27) = e27,
inference(spm,[status(thm)],[c_0_681,c_0_518]),
[final] ).
cnf(c_0_1611,hypothesis,
select(a_1125,i23) = e23,
inference(spm,[status(thm)],[c_0_681,c_0_509]),
[final] ).
cnf(c_0_1612,hypothesis,
select(a_1096,i28) = e28,
inference(spm,[status(thm)],[c_0_681,c_0_512]),
[final] ).
cnf(c_0_1613,hypothesis,
select(a_1126,i24) = e24,
inference(spm,[status(thm)],[c_0_681,c_0_504]),
[final] ).
cnf(c_0_1614,hypothesis,
select(a_1097,i29) = e29,
inference(spm,[status(thm)],[c_0_681,c_0_508]),
[final] ).
cnf(c_0_1615,hypothesis,
select(a_1127,i7) = e7,
inference(spm,[status(thm)],[c_0_681,c_0_503]),
[final] ).
cnf(c_0_1616,hypothesis,
( i_1129 = i2
| i_1129 = i4
| i_1129 = i6
| i_1129 = i8
| i_1129 = i10
| i_1129 = i12
| i_1129 = i14
| i_1129 = i16
| i_1129 = i18
| i_1129 = i20
| i_1129 = i22
| i_1129 = i24
| i_1129 = i26
| i_1129 = i28
| i_1129 = i29
| i_1129 = i1
| i_1129 = i27
| i_1129 = i25
| i_1129 = i23
| i_1129 = i21
| i_1129 = i19
| i_1129 = i17
| i_1129 = i15
| i_1129 = i13
| i_1129 = i11
| i_1129 = i9
| i_1129 = i7
| i_1129 = i5
| i_1129 = i3
| store(a_1103,i30,e_1131) = a_1104 ),
inference(spm,[status(thm)],[c_0_635,c_0_1148]),
[final] ).
cnf(c_0_1617,hypothesis,
( i_1129 = i3
| i_1129 = i5
| i_1129 = i7
| i_1129 = i9
| i_1129 = i11
| i_1129 = i13
| i_1129 = i15
| i_1129 = i17
| i_1129 = i19
| i_1129 = i21
| i_1129 = i23
| i_1129 = i25
| i_1129 = i27
| i_1129 = i1
| i_1129 = i29
| i_1129 = i28
| i_1129 = i26
| i_1129 = i24
| i_1129 = i22
| i_1129 = i20
| i_1129 = i18
| i_1129 = i16
| i_1129 = i14
| i_1129 = i12
| i_1129 = i10
| i_1129 = i8
| i_1129 = i6
| i_1129 = i4
| i_1129 = i2
| select(a_1098,i30) = e_1130 ),
inference(spm,[status(thm)],[c_0_708,c_0_735]),
[final] ).
cnf(c_0_1618,hypothesis,
select(a_1128,i13) = e13,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1149,c_0_673]),c_0_1150]),c_0_1151]),c_0_1152]),c_0_1153]),c_0_1154]),c_0_1155]),c_0_1156]),c_0_1157]),c_0_1158]),c_0_1159]),c_0_1160]),c_0_1161]),c_0_1162]),c_0_1163]),c_0_1164]),c_0_1165]),c_0_1166]),c_0_1167]),c_0_1168]),c_0_1169]),c_0_1170]),c_0_1171]),c_0_1172]),c_0_1173]),c_0_1174]),c_0_1175]),c_0_1176]),c_0_1177]),c_0_1178]),
[final] ).
cnf(c_0_1619,hypothesis,
select(a_1098,i2) = e2,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1179,c_0_675]),c_0_1180]),c_0_1181]),c_0_1182]),c_0_1183]),c_0_1184]),c_0_1185]),c_0_1186]),c_0_1187]),c_0_1188]),c_0_1189]),c_0_1190]),c_0_1191]),c_0_1192]),c_0_1193]),c_0_1194]),c_0_1195]),c_0_1196]),c_0_1197]),c_0_1198]),c_0_1199]),c_0_1200]),c_0_1201]),c_0_1152]),c_0_1202]),c_0_1203]),c_0_1204]),c_0_1205]),c_0_1206]),
[final] ).
cnf(c_0_1620,hypothesis,
select(a_1128,i1) = e1,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1207,c_0_667]),c_0_1208]),c_0_1209]),c_0_1210]),c_0_1211]),c_0_1212]),c_0_1213]),c_0_1214]),c_0_1215]),c_0_1216]),c_0_1217]),c_0_1218]),c_0_1219]),c_0_1220]),c_0_1221]),c_0_1222]),c_0_1223]),c_0_1224]),c_0_1225]),c_0_1226]),c_0_1227]),c_0_1228]),c_0_1229]),c_0_1230]),c_0_1231]),c_0_1232]),c_0_1194]),c_0_1233]),c_0_1234]),
[final] ).
cnf(c_0_1621,hypothesis,
select(a_1098,i3) = e3,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1235,c_0_670]),c_0_1236]),c_0_1237]),c_0_1238]),c_0_1239]),c_0_1168]),c_0_1240]),c_0_1241]),c_0_1242]),c_0_1243]),c_0_1244]),c_0_1245]),c_0_1246]),c_0_1217]),c_0_1247]),c_0_1248]),c_0_1249]),c_0_1250]),c_0_1251]),c_0_1252]),c_0_1253]),c_0_1254]),c_0_1255]),c_0_1256]),c_0_1257]),c_0_1258]),c_0_1259]),c_0_1260]),
[final] ).
cnf(c_0_1622,hypothesis,
select(a_1128,i19) = e19,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1261,c_0_661]),c_0_1262]),c_0_1199]),c_0_1263]),c_0_1264]),c_0_1265]),c_0_1266]),c_0_1267]),c_0_1268]),c_0_1269]),c_0_1270]),c_0_1271]),c_0_1272]),c_0_1273]),c_0_1274]),c_0_1275]),c_0_1276]),c_0_1277]),c_0_1242]),c_0_1278]),c_0_1279]),c_0_1280]),c_0_1281]),c_0_1282]),c_0_1283]),c_0_1284]),c_0_1285]),c_0_1286]),
[final] ).
cnf(c_0_1623,hypothesis,
select(a_1098,i4) = e4,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1287,c_0_664]),c_0_1288]),c_0_1289]),c_0_1290]),c_0_1291]),c_0_1292]),c_0_1293]),c_0_1294]),c_0_1295]),c_0_1296]),c_0_1297]),c_0_1298]),c_0_1299]),c_0_1300]),c_0_1208]),c_0_1301]),c_0_1302]),c_0_1303]),c_0_1304]),c_0_1286]),c_0_1305]),c_0_1306]),c_0_1177]),c_0_1307]),c_0_1308]),c_0_1309]),c_0_1310]),
[final] ).
cnf(c_0_1624,hypothesis,
select(a_1128,i4) = e4,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1311,c_0_655]),c_0_1312]),c_0_1306]),c_0_1294]),c_0_1289]),c_0_1288]),c_0_1292]),c_0_1310]),c_0_1296]),c_0_1260]),c_0_1293]),c_0_1305]),c_0_1297]),c_0_1309]),c_0_1290]),c_0_1303]),c_0_1299]),c_0_1291]),c_0_1301]),c_0_1298]),c_0_1300]),c_0_1307]),c_0_1304]),c_0_1295]),c_0_1302]),c_0_1180]),c_0_1308]),
[final] ).
cnf(c_0_1625,hypothesis,
select(a_1098,i5) = e5,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1313,c_0_658]),c_0_1314]),c_0_1315]),c_0_1316]),c_0_1170]),c_0_1317]),c_0_1318]),c_0_1279]),c_0_1319]),c_0_1320]),c_0_1321]),c_0_1322]),c_0_1215]),c_0_1323]),c_0_1324]),c_0_1325]),c_0_1326]),c_0_1327]),c_0_1328]),c_0_1329]),c_0_1330]),c_0_1331]),c_0_1332]),c_0_1333]),c_0_1334]),c_0_1335]),
[final] ).
cnf(c_0_1626,hypothesis,
select(a_1128,i9) = e9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1336,c_0_649]),c_0_1203]),c_0_1337]),c_0_1338]),c_0_1339]),c_0_1340]),c_0_1341]),c_0_1342]),c_0_1343]),c_0_1344]),c_0_1345]),c_0_1346]),c_0_1347]),c_0_1348]),c_0_1349]),c_0_1350]),c_0_1351]),c_0_1238]),c_0_1352]),c_0_1315]),c_0_1353]),c_0_1354]),c_0_1355]),c_0_1356]),c_0_1357]),c_0_1358]),
[final] ).
cnf(c_0_1627,hypothesis,
select(a_1098,i6) = e6,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1359,c_0_652]),c_0_1360]),c_0_1361]),c_0_1362]),c_0_1363]),c_0_1364]),c_0_1365]),c_0_1366]),c_0_1367]),c_0_1368]),c_0_1369]),c_0_1370]),c_0_1371]),c_0_1213]),c_0_1372]),c_0_1373]),c_0_1374]),c_0_1375]),c_0_1281]),c_0_1376]),c_0_1377]),c_0_1172]),c_0_1378]),c_0_1354]),c_0_1379]),
[final] ).
cnf(c_0_1628,hypothesis,
select(a_1098,i7) = e7,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1380,c_0_646]),c_0_1348]),c_0_1381]),c_0_1164]),c_0_1382]),c_0_1383]),c_0_1274]),c_0_1384]),c_0_1385]),c_0_1386]),c_0_1387]),c_0_1221]),c_0_1388]),c_0_1389]),c_0_1390]),c_0_1391]),c_0_1392]),c_0_1393]),c_0_1394]),c_0_1395]),c_0_1396]),c_0_1397]),c_0_1398]),c_0_1399]),
[final] ).
cnf(c_0_1629,hypothesis,
select(a_1128,i2) = e2,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1400,c_0_637]),c_0_1196]),c_0_1188]),c_0_1198]),c_0_1202]),c_0_1193]),c_0_1191]),c_0_1195]),c_0_1184]),c_0_1192]),c_0_1197]),c_0_1183]),c_0_1204]),c_0_1190]),c_0_1200]),c_0_1186]),c_0_1206]),c_0_1189]),c_0_1205]),c_0_1185]),c_0_1181]),c_0_1182]),c_0_1187]),c_0_1201]),
[final] ).
cnf(c_0_1630,hypothesis,
select(a_1098,i8) = e8,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1401,c_0_640]),c_0_1402]),c_0_1403]),c_0_1404]),c_0_1405]),c_0_1406]),c_0_1407]),c_0_1408]),c_0_1409]),c_0_1410]),c_0_1411]),c_0_1412]),c_0_1212]),c_0_1413]),c_0_1414]),c_0_1415]),c_0_1416]),c_0_1282]),c_0_1417]),c_0_1418]),c_0_1173]),c_0_1419]),c_0_1355]),
[final] ).
cnf(c_0_1631,hypothesis,
select(a_1128,i15) = e15,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1420,c_0_631]),c_0_1421]),c_0_1418]),c_0_1377]),c_0_1422]),c_0_1317]),c_0_1423]),c_0_1240]),c_0_1424]),c_0_1425]),c_0_1426]),c_0_1382]),c_0_1427]),c_0_1428]),c_0_1429]),c_0_1430]),c_0_1431]),c_0_1432]),c_0_1433]),c_0_1434]),c_0_1435]),c_0_1436]),c_0_1437]),
[final] ).
cnf(c_0_1632,hypothesis,
select(a_1098,i9) = e9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1438,c_0_634]),c_0_1340]),c_0_1151]),c_0_1357]),c_0_1350]),c_0_1262]),c_0_1339]),c_0_1346]),c_0_1337]),c_0_1343]),c_0_1233]),c_0_1341]),c_0_1345]),c_0_1342]),c_0_1349]),c_0_1352]),c_0_1338]),c_0_1356]),c_0_1351]),c_0_1353]),c_0_1344]),c_0_1347]),
[final] ).
cnf(c_0_1633,hypothesis,
select(a_1128,i25) = e25,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1439,c_0_625]),c_0_1440]),c_0_1441]),c_0_1442]),c_0_1443]),c_0_1444]),c_0_1445]),c_0_1446]),c_0_1447]),c_0_1448]),c_0_1449]),c_0_1386]),c_0_1450]),c_0_1451]),c_0_1452]),c_0_1245]),c_0_1453]),c_0_1321]),c_0_1454]),c_0_1373]),c_0_1414]),c_0_1455]),
[final] ).
cnf(c_0_1634,hypothesis,
select(a_1098,i10) = e10,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1456,c_0_628]),c_0_1457]),c_0_1458]),c_0_1459]),c_0_1460]),c_0_1461]),c_0_1462]),c_0_1463]),c_0_1464]),c_0_1465]),c_0_1466]),c_0_1222]),c_0_1467]),c_0_1449]),c_0_1468]),c_0_1469]),c_0_1273]),c_0_1470]),c_0_1427]),c_0_1163]),c_0_1471]),
[final] ).
cnf(c_0_1635,hypothesis,
select(a_1128,i18) = e18,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1472,c_0_619]),c_0_1406]),c_0_1365]),c_0_1473]),c_0_1329]),c_0_1474]),c_0_1253]),c_0_1475]),c_0_1476]),c_0_1477]),c_0_1394]),c_0_1460]),c_0_1478]),c_0_1479]),c_0_1480]),c_0_1481]),c_0_1482]),c_0_1483]),c_0_1484]),c_0_1485]),c_0_1486]),
[final] ).
cnf(c_0_1636,hypothesis,
select(a_1098,i11) = e11,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1487,c_0_622]),c_0_1156]),c_0_1434]),c_0_1488]),c_0_1266]),c_0_1489]),c_0_1490]),c_0_1442]),c_0_1491]),c_0_1229]),c_0_1492]),c_0_1493]),c_0_1494]),c_0_1495]),c_0_1496]),c_0_1497]),c_0_1484]),c_0_1498]),c_0_1499]),c_0_1500]),
[final] ).
cnf(c_0_1637,hypothesis,
select(a_1128,i20) = e20,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1501,c_0_613]),c_0_1502]),c_0_1497]),c_0_1503]),c_0_1504]),c_0_1505]),c_0_1506]),c_0_1507]),c_0_1508]),c_0_1461]),c_0_1393]),c_0_1509]),c_0_1510]),c_0_1511]),c_0_1252]),c_0_1512]),c_0_1328]),c_0_1513]),c_0_1366]),c_0_1407]),
[final] ).
cnf(c_0_1638,hypothesis,
select(a_1098,i12) = e12,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1514,c_0_616]),c_0_1515]),c_0_1516]),c_0_1480]),c_0_1506]),c_0_1517]),c_0_1518]),c_0_1519]),c_0_1520]),c_0_1521]),c_0_1225]),c_0_1522]),c_0_1446]),c_0_1523]),c_0_1524]),c_0_1270]),c_0_1525]),c_0_1430]),c_0_1160]),
[final] ).
cnf(c_0_1639,hypothesis,
select(a_1128,i8) = e8,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1526,c_0_607]),c_0_1360]),c_0_1404]),c_0_1334]),c_0_1408]),c_0_1258]),c_0_1405]),c_0_1417]),c_0_1409]),c_0_1399]),c_0_1402]),c_0_1415]),c_0_1411]),c_0_1403]),c_0_1413]),c_0_1410]),c_0_1412]),c_0_1419]),c_0_1416]),
[final] ).
cnf(c_0_1640,hypothesis,
select(a_1098,i13) = e13,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1527,c_0_610]),c_0_1175]),c_0_1166]),c_0_1150]),c_0_1155]),c_0_1162]),c_0_1153]),c_0_1159]),c_0_1178]),c_0_1157]),c_0_1161]),c_0_1158]),c_0_1165]),c_0_1169]),c_0_1154]),c_0_1174]),c_0_1167]),c_0_1171]),
[final] ).
cnf(c_0_1641,hypothesis,
select(a_1128,i21) = e21,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1528,c_0_601]),c_0_1489]),c_0_1529]),c_0_1530]),c_0_1531]),c_0_1524]),c_0_1532]),c_0_1533]),c_0_1469]),c_0_1384]),c_0_1534]),c_0_1535]),c_0_1536]),c_0_1243]),c_0_1537]),c_0_1319]),c_0_1538]),c_0_1375]),
[final] ).
cnf(c_0_1642,hypothesis,
select(a_1098,i14) = e14,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1539,c_0_604]),c_0_1540]),c_0_1473]),c_0_1513]),c_0_1541]),c_0_1542]),c_0_1543]),c_0_1544]),c_0_1545]),c_0_1214]),c_0_1546]),c_0_1454]),c_0_1547]),c_0_1538]),c_0_1280]),c_0_1548]),c_0_1422]),
[final] ).
cnf(c_0_1643,hypothesis,
select(a_1128,i6) = e6,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1549,c_0_595]),c_0_1363]),c_0_1335]),c_0_1367]),c_0_1259]),c_0_1364]),c_0_1376]),c_0_1368]),c_0_1379]),c_0_1361]),c_0_1374]),c_0_1370]),c_0_1362]),c_0_1372]),c_0_1369]),c_0_1371]),c_0_1378]),
[final] ).
cnf(c_0_1644,hypothesis,
select(a_1098,i15) = e15,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1550,c_0_598]),c_0_1425]),c_0_1284]),c_0_1435]),c_0_1428]),c_0_1437]),c_0_1431]),c_0_1210]),c_0_1433]),c_0_1429]),c_0_1432]),c_0_1426]),c_0_1423]),c_0_1436]),c_0_1421]),c_0_1424]),
[final] ).
cnf(c_0_1645,hypothesis,
select(a_1128,i11) = e11,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1551,c_0_589]),c_0_1492]),c_0_1494]),c_0_1491]),c_0_1500]),c_0_1493]),c_0_1490]),c_0_1471]),c_0_1381]),c_0_1495]),c_0_1488]),c_0_1498]),c_0_1239]),c_0_1496]),c_0_1316]),c_0_1499]),
[final] ).
cnf(c_0_1646,hypothesis,
select(a_1098,i16) = e16,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1552,c_0_592]),c_0_1475]),c_0_1511]),c_0_1553]),c_0_1554]),c_0_1555]),c_0_1556]),c_0_1557]),c_0_1218]),c_0_1558]),c_0_1452]),c_0_1559]),c_0_1536]),c_0_1277]),c_0_1560]),
[final] ).
cnf(c_0_1647,hypothesis,
select(a_1128,i14) = e14,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1561,c_0_583]),c_0_1331]),c_0_1541]),c_0_1255]),c_0_1540]),c_0_1548]),c_0_1542]),c_0_1396]),c_0_1458]),c_0_1547]),c_0_1544]),c_0_1515]),c_0_1546]),c_0_1543]),c_0_1545]),
[final] ).
cnf(c_0_1648,hypothesis,
select(a_1098,i17) = e17,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1562,c_0_586]),c_0_1276]),c_0_1535]),c_0_1563]),c_0_1451]),c_0_1564]),c_0_1219]),c_0_1565]),c_0_1566]),c_0_1567]),c_0_1568]),c_0_1569]),c_0_1510]),c_0_1476]),
[final] ).
cnf(c_0_1649,hypothesis,
select(a_1128,i29) = e29,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1570,c_0_577]),c_0_1571]),c_0_1572]),c_0_1521]),c_0_1573]),c_0_1574]),c_0_1466]),c_0_1388]),c_0_1575]),c_0_1565]),c_0_1557]),c_0_1247]),c_0_1576]),c_0_1323]),
[final] ).
cnf(c_0_1650,hypothesis,
select(a_1098,i18) = e18,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1577,c_0_580]),c_0_1486]),c_0_1474]),c_0_1477]),c_0_1482]),c_0_1479]),c_0_1483]),c_0_1211]),c_0_1481]),c_0_1455]),c_0_1478]),c_0_1485]),c_0_1283]),
[final] ).
cnf(c_0_1651,hypothesis,
select(a_1128,i5) = e5,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1578,c_0_571]),c_0_1327]),c_0_1236]),c_0_1330]),c_0_1318]),c_0_1326]),c_0_1314]),c_0_1333]),c_0_1320]),c_0_1324]),c_0_1332]),c_0_1322]),c_0_1325]),
[final] ).
cnf(c_0_1652,hypothesis,
select(a_1098,i19) = e19,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1579,c_0_574]),c_0_1265]),c_0_1272]),c_0_1263]),c_0_1269]),c_0_1234]),c_0_1267]),c_0_1271]),c_0_1268]),c_0_1275]),c_0_1278]),c_0_1264]),
[final] ).
cnf(c_0_1653,hypothesis,
select(a_1128,i26) = e26,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1580,c_0_565]),c_0_1581]),c_0_1519]),c_0_1582]),c_0_1583]),c_0_1464]),c_0_1390]),c_0_1584]),c_0_1567]),c_0_1555]),c_0_1249]),c_0_1585]),
[final] ).
cnf(c_0_1654,hypothesis,
select(a_1098,i20) = e20,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1586,c_0_568]),c_0_1512]),c_0_1509]),c_0_1504]),c_0_1507]),c_0_1503]),c_0_1231]),c_0_1505]),c_0_1440]),c_0_1508]),c_0_1502]),
[final] ).
cnf(c_0_1655,hypothesis,
select(a_1128,i22) = e22,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1587,c_0_559]),c_0_1251]),c_0_1553]),c_0_1569]),c_0_1588]),c_0_1392]),c_0_1462]),c_0_1589]),c_0_1590]),c_0_1517]),c_0_1591]),
[final] ).
cnf(c_0_1656,hypothesis,
select(a_1098,i21) = e21,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1592,c_0_562]),c_0_1533]),c_0_1441]),c_0_1531]),c_0_1230]),c_0_1529]),c_0_1532]),c_0_1530]),c_0_1534]),c_0_1537]),
[final] ).
cnf(c_0_1657,hypothesis,
select(a_1128,i27) = e27,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1593,c_0_553]),c_0_1522]),c_0_1594]),c_0_1595]),c_0_1467]),c_0_1387]),c_0_1596]),c_0_1564]),c_0_1558]),c_0_1246]),
[final] ).
cnf(c_0_1658,hypothesis,
select(a_1098,i22) = e22,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1597,c_0_556]),c_0_1588]),c_0_1585]),c_0_1590]),c_0_1576]),c_0_1216]),c_0_1591]),c_0_1453]),c_0_1589]),
[final] ).
cnf(c_0_1659,hypothesis,
select(a_1128,i3) = e3,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1598,c_0_547]),c_0_1254]),c_0_1241]),c_0_1250]),c_0_1237]),c_0_1257]),c_0_1244]),c_0_1248]),c_0_1256]),
[final] ).
cnf(c_0_1660,hypothesis,
select(a_1098,i23) = e23,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1599,c_0_550]),c_0_1448]),c_0_1595]),c_0_1223]),c_0_1574]),c_0_1600]),c_0_1583]),c_0_1601]),
[final] ).
cnf(c_0_1661,hypothesis,
select(a_1128,i12) = e12,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1602,c_0_541]),c_0_1520]),c_0_1523]),c_0_1457]),c_0_1397]),c_0_1518]),c_0_1525]),c_0_1516]),
[final] ).
cnf(c_0_1662,hypothesis,
select(a_1098,i24) = e24,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1603,c_0_544]),c_0_1584]),c_0_1604]),c_0_1575]),c_0_1220]),c_0_1596]),c_0_1450]),
[final] ).
cnf(c_0_1663,hypothesis,
select(a_1128,i16) = e16,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1605,c_0_535]),c_0_1560]),c_0_1554]),c_0_1395]),c_0_1459]),c_0_1559]),c_0_1556]),
[final] ).
cnf(c_0_1664,hypothesis,
select(a_1098,i25) = e25,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1606,c_0_538]),c_0_1445]),c_0_1232]),c_0_1443]),c_0_1447]),c_0_1444]),
[final] ).
cnf(c_0_1665,hypothesis,
select(a_1128,i28) = e28,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1607,c_0_529]),c_0_1600]),c_0_1465]),c_0_1389]),c_0_1604]),c_0_1566]),
[final] ).
cnf(c_0_1666,hypothesis,
select(a_1098,i26) = e26,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1608,c_0_532]),c_0_1582]),c_0_1571]),c_0_1227]),c_0_1581]),
[final] ).
cnf(c_0_1667,hypothesis,
select(a_1128,i17) = e17,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1609,c_0_523]),c_0_1568]),c_0_1383]),c_0_1470]),c_0_1563]),
[final] ).
cnf(c_0_1668,hypothesis,
select(a_1098,i27) = e27,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1610,c_0_526]),c_0_1226]),c_0_1572]),c_0_1594]),
[final] ).
cnf(c_0_1669,hypothesis,
select(a_1128,i23) = e23,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1611,c_0_517]),c_0_1468]),c_0_1385]),c_0_1601]),
[final] ).
cnf(c_0_1670,hypothesis,
select(a_1098,i28) = e28,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1612,c_0_520]),c_0_1573]),c_0_1224]),
[final] ).
cnf(c_0_1671,hypothesis,
select(a_1128,i24) = e24,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1613,c_0_511]),c_0_1391]),c_0_1463]),
[final] ).
cnf(c_0_1672,hypothesis,
select(a_1098,i29) = e29,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1614,c_0_513]),c_0_1228]),
[final] ).
cnf(c_0_1673,hypothesis,
select(a_1128,i7) = e7,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1615,c_0_505]),c_0_1398]),
[final] ).
cnf(c_0_1674,hypothesis,
select(a_1069,i1) = e1,
inference(spm,[status(thm)],[c_0_681,c_0_671]),
[final] ).
cnf(c_0_1675,hypothesis,
select(a_1098,i1) = e1,
inference(spm,[status(thm)],[c_0_681,c_0_507]),
[final] ).
cnf(c_0_1676,hypothesis,
select(a_1128,i10) = e10,
inference(spm,[status(thm)],[c_0_681,c_0_502]),
[final] ).
cnf(c_0_1677,hypothesis,
i_1129 = sk(a_1098,a_1128),
hyp62,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV506-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n010.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 08:56:40 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.50 Running first-order theorem proving
% 0.26/0.50 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.26/0.60 % Version: 3.5.1
% 0.26/0.60 % Preprocessing class: FSLMSMSLSSSNFFN.
% 0.26/0.60 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.26/0.60 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 900s (3) cores
% 0.26/0.60 % Starting new_bool_3 with 600s (2) cores
% 0.26/0.60 % Starting new_bool_1 with 600s (2) cores
% 0.26/0.60 % Starting sh5l with 300s (1) cores
% 0.26/0.60 % G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with pid 533005 completed with status 1
% 0.26/0.60 % Result found by G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI
% 0.26/0.60 % Preprocessing class: FSLMSMSLSSSNFFN.
% 0.26/0.60 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.26/0.60 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 900s (3) cores
% 0.26/0.60 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.26/0.60 % No SInE strategy applied
% 0.26/0.60 % Search class: FGUPF-FSLM32-SFFFFFNN
% 0.26/0.60 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 0.26/0.60 % Starting SubtermCWHack with 82s (1) cores
% 0.26/0.60 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 91s (1) cores
% 0.26/0.60 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y with 82s (1) cores
% 0.26/0.60 % SubtermCWHack with pid 533009 completed with status 1
% 0.26/0.60 % Result found by SubtermCWHack
% 0.26/0.60 % Preprocessing class: FSLMSMSLSSSNFFN.
% 0.26/0.60 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.26/0.60 % Starting G-E--_008_C45_F1_PI_SE_Q4_CS_SP_S4SI with 900s (3) cores
% 0.26/0.60 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.26/0.60 % No SInE strategy applied
% 0.26/0.60 % Search class: FGUPF-FSLM32-SFFFFFNN
% 0.26/0.60 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 0.26/0.60 % Starting SubtermCWHack with 82s (1) cores
% 0.26/0.60 % Preprocessing time : 0.003 s
% 0.26/0.60
% 0.26/0.60 % No proof found!
% 0.26/0.60 % SZS status Satisfiable
% 0.26/0.60 % SZS output start Saturation
% See solution above
% 0.26/0.60 % Parsed axioms : 501
% 0.26/0.60 % Removed by relevancy pruning/SinE : 0
% 0.26/0.60 % Initial clauses : 501
% 0.26/0.60 % Removed in clause preprocessing : 0
% 0.26/0.60 % Initial clauses in saturation : 501
% 0.26/0.60 % Processed clauses : 772
% 0.26/0.60 % ...of these trivial : 0
% 0.26/0.60 % ...subsumed : 31
% 0.26/0.60 % ...remaining for further processing : 741
% 0.26/0.60 % Other redundant clauses eliminated : 0
% 0.26/0.60 % Clauses deleted for lack of memory : 0
% 0.26/0.60 % Backward-subsumed : 0
% 0.26/0.60 % Backward-rewritten : 0
% 0.26/0.60 % Generated clauses : 271
% 0.26/0.60 % ...of the previous two non-redundant : 271
% 0.26/0.60 % ...aggressively subsumed : 0
% 0.26/0.60 % Contextual simplify-reflections : 0
% 0.26/0.60 % Paramodulations : 242
% 0.26/0.60 % Factorizations : 29
% 0.26/0.60 % NegExts : 0
% 0.26/0.60 % Equation resolutions : 0
% 0.26/0.60 % Disequality decompositions : 0
% 0.26/0.60 % Total rewrite steps : 3
% 0.26/0.60 % ...of those cached : 0
% 0.26/0.60 % Propositional unsat checks : 0
% 0.26/0.60 % Propositional check models : 0
% 0.26/0.60 % Propositional check unsatisfiable : 0
% 0.26/0.60 % Propositional clauses : 0
% 0.26/0.60 % Propositional clauses after purity: 0
% 0.26/0.60 % Propositional unsat core size : 0
% 0.26/0.60 % Propositional preprocessing time : 0.000
% 0.26/0.60 % Propositional encoding time : 0.000
% 0.26/0.60 % Propositional solver time : 0.000
% 0.26/0.60 % Success case prop preproc time : 0.000
% 0.26/0.60 % Success case prop encoding time : 0.000
% 0.26/0.60 % Success case prop solver time : 0.000
% 0.26/0.60 % Current number of processed clauses : 741
% 0.26/0.60 % Positive orientable unit clauses : 181
% 0.26/0.60 % Positive unorientable unit clauses: 0
% 0.26/0.60 % Negative unit clauses : 436
% 0.26/0.60 % Non-unit-clauses : 124
% 0.26/0.60 % Current number of unprocessed clauses: 0
% 0.26/0.60 % ...number of literals in the above : 0
% 0.26/0.60 % Current number of archived formulas : 0
% 0.26/0.60 % Current number of archived clauses : 0
% 0.26/0.60 % Clause-clause subsumption calls (NU) : 94791
% 0.26/0.60 % Rec. Clause-clause subsumption calls : 2663
% 0.26/0.60 % Non-unit clause-clause subsumptions : 2
% 0.26/0.60 % Unit Clause-clause subsumption calls : 6888
% 0.26/0.60 % Rewrite failures with RHS unbound : 0
% 0.26/0.60 % BW rewrite match attempts : 0
% 0.26/0.60 % BW rewrite match successes : 0
% 0.26/0.60 % Condensation attempts : 0
% 0.26/0.60 % Condensation successes : 0
% 0.26/0.60 % Termbank termtop insertions : 10036
% 0.26/0.60 % Search garbage collected termcells : 872
% 0.26/0.60
% 0.26/0.60 % -------------------------------------------------
% 0.26/0.60 % User time : 0.056 s
% 0.26/0.60 % System time : 0.006 s
% 0.26/0.60 % Total time : 0.062 s
% 0.26/0.60 % Maximum resident set size: 4352 pages
% 0.26/0.60
% 0.26/0.60 % -------------------------------------------------
% 0.26/0.60 % User time : 0.152 s
% 0.26/0.60 % System time : 0.020 s
% 0.26/0.60 % Total time : 0.171 s
% 0.26/0.60 % Maximum resident set size: 5120 pages
% 0.26/0.60 % E exiting
%------------------------------------------------------------------------------