%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYN463-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 03:24:34 PM UTC 2026
% Result : Satisfiable 80.25s 17.33s
% Output : Saturation 80.25s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_226ERROR: Could not build tree for root c_0_247ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_161,negated_conjecture,
ndr1_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_156,c_0_157]),c_0_158]),c_0_159]),
[final] ).
cnf(c_0_171,negated_conjecture,
( ~ hskp1
| c1_1(a1254) ),
c_0_162,
[final] ).
cnf(c_0_172,negated_conjecture,
( ~ hskp1
| ~ c3_1(a1254) ),
c_0_163,
[final] ).
cnf(c_0_173,negated_conjecture,
( ~ hskp1
| ~ c2_1(a1254) ),
c_0_164,
[final] ).
cnf(c_0_183,negated_conjecture,
( ~ hskp5
| ~ c2_1(a1258) ),
c_0_166,
[final] ).
cnf(c_0_184,negated_conjecture,
( ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X1)
| epred21_0 ),
inference(split_equiv,[status(thm)],[c_0_167]),
[final] ).
cnf(c_0_185,negated_conjecture,
( ~ hskp5
| c3_1(a1258) ),
c_0_168,
[final] ).
cnf(c_0_196,negated_conjecture,
( ~ c0_1(X1)
| hskp1
| c3_1(X1)
| c1_1(X1)
| epred8_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_175]),c_0_161])]),
[final] ).
cnf(c_0_197,negated_conjecture,
( ~ hskp16
| c0_1(a1274) ),
c_0_176,
[final] ).
cnf(c_0_198,negated_conjecture,
( ~ hskp16
| ~ c3_1(a1274) ),
c_0_177,
[final] ).
cnf(c_0_199,negated_conjecture,
( ~ hskp16
| ~ c1_1(a1274) ),
c_0_178,
[final] ).
cnf(c_0_207,negated_conjecture,
( ~ hskp5
| ~ c0_1(a1258)
| epred21_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_184]),c_0_185]),
[final] ).
cnf(c_0_220,negated_conjecture,
( ~ hskp16
| hskp1
| epred8_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_196,c_0_197]),c_0_198]),c_0_199]),
[final] ).
cnf(c_0_222,negated_conjecture,
( c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred9_0 ),
inference(split_equiv,[status(thm)],[c_0_201]),
[final] ).
cnf(c_0_247,negated_conjecture,
( ~ hskp21
| c3_1(a1288) ),
c_0_226,
[final] ).
cnf(c_0_248,negated_conjecture,
( ~ hskp21
| c1_1(a1288) ),
c_0_227,
[final] ).
cnf(c_0_249,negated_conjecture,
( ~ hskp21
| ~ c0_1(a1288) ),
c_0_228,
[final] ).
cnf(c_0_258,negated_conjecture,
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred39_0 ),
inference(split_equiv,[status(thm)],[c_0_240]),
[final] ).
cnf(c_0_259,negated_conjecture,
( ~ hskp5
| ~ c1_1(a1258) ),
c_0_241,
[final] ).
cnf(c_0_275,negated_conjecture,
( ~ hskp5
| ~ c0_1(a1258)
| epred39_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_258]),c_0_259]),
[final] ).
cnf(c_0_286,negated_conjecture,
( ~ epred8_0
| ~ epred9_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_270,c_0_175]),c_0_201]),
[final] ).
cnf(c_0_327,negated_conjecture,
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| hskp20
| hskp2 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_293,c_0_161])]),
[final] ).
cnf(c_0_344,negated_conjecture,
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred44_0 ),
inference(split_equiv,[status(thm)],[c_0_312]),
[final] ).
cnf(c_0_346,negated_conjecture,
( ~ hskp12
| c2_1(a1266) ),
c_0_314,
[final] ).
cnf(c_0_347,negated_conjecture,
( ~ hskp12
| ~ c0_1(a1266) ),
c_0_315,
[final] ).
cnf(c_0_348,negated_conjecture,
( ~ hskp12
| ~ c1_1(a1266) ),
c_0_316,
[final] ).
cnf(c_0_354,negated_conjecture,
( ~ c3_1(X1)
| hskp12
| hskp11
| c0_1(X1)
| c1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_319,c_0_161])]),
[final] ).
cnf(c_0_364,negated_conjecture,
( ~ hskp2
| c2_1(a1255) ),
c_0_323,
[final] ).
cnf(c_0_365,negated_conjecture,
( ~ hskp2
| ~ c1_1(a1255) ),
c_0_324,
[final] ).
cnf(c_0_367,negated_conjecture,
( ~ hskp2
| c0_1(a1255) ),
c_0_326,
[final] ).
cnf(c_0_381,negated_conjecture,
( ~ hskp16
| epred44_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_344]),c_0_197]),c_0_199]),
[final] ).
cnf(c_0_391,negated_conjecture,
( ~ hskp13
| ~ c2_1(a1268) ),
c_0_356,
[final] ).
cnf(c_0_392,negated_conjecture,
( ~ hskp13
| c1_1(a1268) ),
c_0_357,
[final] ).
cnf(c_0_393,negated_conjecture,
( ~ hskp13
| ~ c0_1(a1268) ),
c_0_358,
[final] ).
cnf(c_0_394,negated_conjecture,
( ~ c0_1(X1)
| hskp13
| hskp12
| c2_1(X1)
| c1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_359,c_0_161])]),
[final] ).
cnf(c_0_410,negated_conjecture,
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred42_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_376]),c_0_161])]),
[final] ).
cnf(c_0_432,negated_conjecture,
( ~ epred20_0
| ~ epred21_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_404,c_0_242]),c_0_167]),
[final] ).
cnf(c_0_436,negated_conjecture,
( ~ hskp5
| epred42_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_410]),c_0_185]),c_0_259]),
[final] ).
cnf(c_0_500,negated_conjecture,
( ~ hskp3
| c3_1(a1256) ),
c_0_469,
[final] ).
cnf(c_0_501,negated_conjecture,
( ~ hskp3
| ~ c0_1(a1256) ),
c_0_470,
[final] ).
cnf(c_0_502,negated_conjecture,
( ~ hskp3
| ~ c1_1(a1256) ),
c_0_471,
[final] ).
cnf(c_0_503,negated_conjecture,
( ~ hskp18
| ~ c2_1(a1279) ),
c_0_472,
[final] ).
cnf(c_0_504,negated_conjecture,
( hskp3
| hskp2
| c0_1(X1)
| c2_1(X1)
| c1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_473,c_0_161])]),
[final] ).
cnf(c_0_505,negated_conjecture,
( ~ hskp18
| ~ c0_1(a1279) ),
c_0_474,
[final] ).
cnf(c_0_506,negated_conjecture,
( ~ hskp18
| ~ c1_1(a1279) ),
c_0_475,
[final] ).
cnf(c_0_507,negated_conjecture,
( ~ hskp26
| c2_1(a1250) ),
c_0_476,
[final] ).
cnf(c_0_508,negated_conjecture,
( ~ hskp26
| c1_1(a1250) ),
c_0_477,
[final] ).
cnf(c_0_509,negated_conjecture,
( ~ hskp26
| c0_1(a1250) ),
c_0_478,
[final] ).
cnf(c_0_527,negated_conjecture,
( ~ c1_1(X1)
| hskp16
| c2_1(X1)
| c3_1(X1)
| epred10_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_498]),c_0_161])]),
[final] ).
cnf(c_0_530,negated_conjecture,
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred45_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_499]),c_0_161])]),
[final] ).
cnf(c_0_532,negated_conjecture,
( ~ hskp18
| hskp3
| hskp2 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_503,c_0_504]),c_0_505]),c_0_506]),
[final] ).
cnf(c_0_561,negated_conjecture,
( ~ hskp1
| hskp16
| epred10_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_527,c_0_171]),c_0_173]),c_0_172]),
[final] ).
cnf(c_0_563,negated_conjecture,
( ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| epred4_0 ),
inference(split_equiv,[status(thm)],[c_0_529]),
[final] ).
cnf(c_0_564,negated_conjecture,
( ~ hskp5
| ~ c0_1(a1258)
| epred45_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_530]),c_0_259]),
[final] ).
cnf(c_0_629,negated_conjecture,
( ~ hskp24
| ~ c3_1(a1301) ),
c_0_578,
[final] ).
cnf(c_0_630,negated_conjecture,
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred11_0 ),
inference(split_equiv,[status(thm)],[c_0_579]),
[final] ).
cnf(c_0_631,negated_conjecture,
( ~ hskp24
| ~ c0_1(a1301) ),
c_0_580,
[final] ).
cnf(c_0_632,negated_conjecture,
( ~ hskp24
| c2_1(a1301) ),
c_0_581,
[final] ).
cnf(c_0_633,negated_conjecture,
( ~ hskp23
| ~ c3_1(a1300) ),
c_0_582,
[final] ).
cnf(c_0_634,negated_conjecture,
( ~ hskp23
| c1_1(a1300) ),
c_0_583,
[final] ).
cnf(c_0_635,negated_conjecture,
( ~ hskp23
| ~ c0_1(a1300) ),
c_0_584,
[final] ).
cnf(c_0_636,negated_conjecture,
( ~ c0_1(X1)
| hskp24
| hskp23
| c3_1(X1)
| c1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_585,c_0_161])]),
[final] ).
cnf(c_0_651,negated_conjecture,
( ~ c0_1(X1)
| hskp8
| c3_1(X1)
| c1_1(X1)
| epred14_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_596]),c_0_161])]),
[final] ).
cnf(c_0_652,negated_conjecture,
( ~ c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| epred15_0 ),
inference(split_equiv,[status(thm)],[c_0_597]),
[final] ).
cnf(c_0_685,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1301)
| epred11_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_629,c_0_630]),c_0_631]),
[final] ).
cnf(c_0_687,negated_conjecture,
( ~ hskp23
| epred11_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_633,c_0_630]),c_0_634]),c_0_635]),
[final] ).
cnf(c_0_688,negated_conjecture,
( ~ hskp16
| hskp24
| hskp23 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_636,c_0_197]),c_0_198]),c_0_199]),
[final] ).
cnf(c_0_696,negated_conjecture,
( ~ hskp25
| ~ c3_1(a1303) ),
c_0_641,
[final] ).
cnf(c_0_698,negated_conjecture,
( ~ hskp25
| ~ c0_1(a1303) ),
c_0_643,
[final] ).
cnf(c_0_699,negated_conjecture,
( ~ hskp25
| ~ c1_1(a1303) ),
c_0_644,
[final] ).
cnf(c_0_706,negated_conjecture,
( ~ hskp5
| c0_1(a1258)
| epred15_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_652,c_0_185]),c_0_259]),
[final] ).
cnf(c_0_729,negated_conjecture,
( ~ hskp27
| c3_1(a1253) ),
c_0_673,
[final] ).
cnf(c_0_730,negated_conjecture,
( ~ hskp27
| c0_1(a1253) ),
c_0_674,
[final] ).
cnf(c_0_731,negated_conjecture,
( ~ hskp27
| c1_1(a1253) ),
c_0_675,
[final] ).
cnf(c_0_742,negated_conjecture,
( ~ hskp16
| hskp24
| epred11_0 ),
inference(spm,[status(thm)],[c_0_687,c_0_688]),
[final] ).
cnf(c_0_756,negated_conjecture,
( ~ hskp5
| epred15_0
| epred39_0 ),
inference(spm,[status(thm)],[c_0_275,c_0_706]),
[final] ).
cnf(c_0_760,negated_conjecture,
( ~ epred10_0
| ~ epred11_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_712,c_0_498]),c_0_579]),
[final] ).
cnf(c_0_770,negated_conjecture,
( ~ c2_1(X1)
| ~ c1_1(X1)
| hskp20
| c3_1(X1)
| epred29_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_723]),c_0_161])]),
[final] ).
cnf(c_0_779,negated_conjecture,
( ~ hskp5
| epred15_0
| epred45_0 ),
inference(spm,[status(thm)],[c_0_564,c_0_706]),
[final] ).
cnf(c_0_791,negated_conjecture,
( ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| epred41_0 ),
inference(split_equiv,[status(thm)],[c_0_739]),
[final] ).
cnf(c_0_795,negated_conjecture,
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| hskp21
| epred36_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_743]),c_0_161])]),
[final] ).
cnf(c_0_805,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| hskp9
| hskp6
| c3_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_750,c_0_161])]),
[final] ).
cnf(c_0_830,negated_conjecture,
( ~ hskp9
| c0_1(a1263) ),
c_0_772,
[final] ).
cnf(c_0_831,negated_conjecture,
( ~ hskp9
| ~ c1_1(a1263) ),
c_0_773,
[final] ).
cnf(c_0_832,negated_conjecture,
( ~ c2_1(X1)
| ~ c3_1(X1)
| hskp9
| c1_1(X1)
| epred22_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_774]),c_0_161])]),
[final] ).
cnf(c_0_867,negated_conjecture,
( ~ hskp5
| epred15_0
| epred21_0 ),
inference(spm,[status(thm)],[c_0_207,c_0_706]),
[final] ).
cnf(c_0_868,negated_conjecture,
( ~ hskp9
| c3_1(a1263) ),
c_0_804,
[final] ).
cnf(c_0_897,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| hskp6
| c3_1(X1)
| epred4_0 ),
inference(spm,[status(thm)],[c_0_805,c_0_563]),
[final] ).
cnf(c_0_929,negated_conjecture,
( ~ epred14_0
| ~ epred15_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_871,c_0_596]),c_0_597]),
[final] ).
cnf(c_0_946,negated_conjecture,
( ~ epred15_0
| ~ epred22_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_893,c_0_774]),c_0_597]),
[final] ).
cnf(c_0_1105,negated_conjecture,
( ~ epred21_0
| ~ epred41_0
| ~ epred45_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1070,c_0_499]),c_0_739]),c_0_167]),
[final] ).
cnf(c_0_1119,negated_conjecture,
( ~ hskp27
| hskp21
| epred36_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_729]),c_0_730]),c_0_731]),
[final] ).
cnf(c_0_1124,negated_conjecture,
( ~ epred11_0
| ~ epred25_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1099,c_0_980]),c_0_579]),
[final] ).
cnf(c_0_1146,negated_conjecture,
( c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| epred2_0 ),
inference(split_equiv,[status(thm)],[c_0_1125]),
[final] ).
cnf(c_0_1179,negated_conjecture,
( ~ c2_1(X1)
| hskp13
| c0_1(X1)
| c3_1(X1)
| epred5_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1166]),c_0_161])]),
[final] ).
cnf(c_0_1183,negated_conjecture,
( hskp18
| hskp24
| hskp27 ),
clause32,
[final] ).
cnf(c_0_1189,negated_conjecture,
~ epred36_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1052,c_0_1173]),c_0_1174]),
[final] ).
cnf(c_0_1195,negated_conjecture,
( ~ c1_1(X1)
| hskp26
| c2_1(X1)
| c3_1(X1)
| epred1_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1180]),c_0_161])]),
[final] ).
cnf(c_0_1210,negated_conjecture,
( ~ hskp3
| hskp12
| hskp11 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_354,c_0_500]),c_0_501]),c_0_502]),
[final] ).
cnf(c_0_1211,negated_conjecture,
( ~ hskp1
| hskp26
| epred1_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1195,c_0_171]),c_0_173]),c_0_172]),
[final] ).
cnf(c_0_1214,negated_conjecture,
( hskp27
| hskp1
| c0_1(X1)
| c2_1(X1)
| c1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1196,c_0_161])]),
[final] ).
cnf(c_0_1231,negated_conjecture,
( ~ hskp16
| hskp26
| epred1_0
| epred8_0 ),
inference(spm,[status(thm)],[c_0_1211,c_0_220]),
[final] ).
cnf(c_0_1235,negated_conjecture,
( ~ hskp18
| hskp27
| hskp1 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_503,c_0_1214]),c_0_505]),c_0_506]),
[final] ).
cnf(c_0_1248,negated_conjecture,
( ~ epred2_0
| ~ epred5_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1225,c_0_1166]),c_0_1125]),
[final] ).
cnf(c_0_1273,negated_conjecture,
( ~ hskp27
| hskp20
| hskp2 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_729]),c_0_730]),c_0_731]),
[final] ).
cnf(c_0_1276,negated_conjecture,
( ~ hskp18
| ~ c3_1(a1279)
| epred42_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_503,c_0_410]),c_0_506]),
[final] ).
cnf(c_0_1277,negated_conjecture,
( ~ hskp18
| c3_1(a1279)
| epred9_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_503,c_0_222]),c_0_506]),
[final] ).
cnf(c_0_1284,negated_conjecture,
( ~ hskp3
| epred15_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_652,c_0_500]),c_0_501]),c_0_502]),
[final] ).
cnf(c_0_1302,negated_conjecture,
( ~ hskp18
| epred9_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_1276,c_0_1277]),
[final] ).
cnf(c_0_1327,negated_conjecture,
( ~ epred1_0
| ~ epred2_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1303,c_0_1180]),c_0_1125]),
[final] ).
cnf(c_0_1364,negated_conjecture,
~ epred29_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1315,c_0_1340]),c_0_1341]),c_0_1342]),
[final] ).
cnf(c_0_1411,negated_conjecture,
epred33_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1105,c_0_1408]),c_0_1133]),c_0_1155]),
[final] ).
cnf(c_0_1415,negated_conjecture,
~ epred32_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1410,c_0_1411])]),
[final] ).
cnf(c_0_1425,negated_conjecture,
~ epred30_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_456,c_0_1418]),c_0_458]),
[final] ).
cnf(c_0_1514,negated_conjecture,
epred37_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1105,c_0_1505]),c_0_1506]),c_0_1507]),
[final] ).
cnf(c_0_1581,negated_conjecture,
( ~ hskp15
| ~ c2_1(a1272) ),
c_0_1570,
[final] ).
cnf(c_0_1582,negated_conjecture,
( hskp3
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| epred6_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1571]),c_0_161])]),
[final] ).
cnf(c_0_1583,negated_conjecture,
( ~ hskp15
| ~ c0_1(a1272) ),
c_0_1572,
[final] ).
cnf(c_0_1584,negated_conjecture,
( ~ hskp15
| ~ c3_1(a1272) ),
c_0_1573,
[final] ).
cnf(c_0_1586,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1301)
| hskp20
| epred29_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_632]),c_0_629]),
[final] ).
cnf(c_0_1588,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1)
| epred35_0 ),
inference(split_equiv,[status(thm)],[c_0_1575]),
[final] ).
cnf(c_0_1591,negated_conjecture,
epred38_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_432,c_0_1579]),c_0_1580]),
[final] ).
cnf(c_0_1592,negated_conjecture,
( ~ hskp15
| hskp3
| epred6_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1582]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_1600,negated_conjecture,
~ epred39_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1590,c_0_1591])]),
[final] ).
cnf(c_0_1606,negated_conjecture,
( ~ hskp26
| epred35_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1588,c_0_507]),c_0_509]),c_0_508]),
[final] ).
cnf(c_0_1730,negated_conjecture,
epred19_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_302,c_0_1716]),c_0_1483]),
[final] ).
cnf(c_0_1755,negated_conjecture,
epred24_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_432,c_0_1741]),c_0_1495]),
[final] ).
cnf(c_0_1773,negated_conjecture,
~ epred26_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_948,c_0_1755])]),
[final] ).
cnf(c_0_1788,negated_conjecture,
epred43_0,
inference(sr,[status(thm)],[c_0_1772,c_0_1773]),
[final] ).
cnf(c_0_1801,negated_conjecture,
~ epred44_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_845,c_0_1755])]),c_0_1788])]),
[final] ).
cnf(c_0_1802,negated_conjecture,
~ epred42_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1789,c_0_1755])]),
[final] ).
cnf(c_0_1813,negated_conjecture,
~ hskp20,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_489,c_0_344]),c_0_1801]),c_0_1802]),c_0_395]),c_0_397]),
[final] ).
cnf(c_0_1826,negated_conjecture,
( hskp26
| c0_1(X1)
| c2_1(X1)
| c1_1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1812,c_0_899]),c_0_1801]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1828,negated_conjecture,
( c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred35_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1815,c_0_899]),c_0_1606]),c_0_1816]),
[final] ).
cnf(c_0_1829,negated_conjecture,
epred17_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1817,c_0_217]),c_0_1558]),
[final] ).
cnf(c_0_1830,negated_conjecture,
( ~ c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| epred28_0 ),
inference(split_equiv,[status(thm)],[c_0_1818]),
[final] ).
cnf(c_0_1842,negated_conjecture,
( ~ hskp15
| hskp26
| c1_1(a1272) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1826]),c_0_1583]),
[final] ).
cnf(c_0_1844,negated_conjecture,
~ hskp6,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1813,c_0_982]),c_0_1364]),
[final] ).
cnf(c_0_1845,negated_conjecture,
( ~ hskp15
| c1_1(a1272)
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1828]),c_0_1583]),
[final] ).
cnf(c_0_1846,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp20
| c3_1(X1)
| epred4_0
| epred29_0 ),
inference(spm,[status(thm)],[c_0_770,c_0_563]),
[final] ).
cnf(c_0_1847,negated_conjecture,
~ epred4_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1523,c_0_1829])]),
[final] ).
cnf(c_0_1848,negated_conjecture,
( ~ hskp15
| ~ c1_1(a1272)
| epred28_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1830]),c_0_1584]),
[final] ).
cnf(c_0_1851,negated_conjecture,
~ epred23_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_880,c_0_1755])]),
[final] ).
cnf(c_0_1864,negated_conjecture,
( hskp27
| hskp16
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred10_0 ),
inference(spm,[status(thm)],[c_0_561,c_0_1214]),
[final] ).
cnf(c_0_1866,negated_conjecture,
( hskp15
| c2_1(X1)
| c3_1(X1)
| c1_1(X1) ),
inference(sr,[status(thm)],[c_0_1843,c_0_1844]),
[final] ).
cnf(c_0_1870,negated_conjecture,
( ~ hskp15
| hskp26
| epred1_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1195,c_0_1842]),c_0_1581]),c_0_1584]),
[final] ).
cnf(c_0_1871,negated_conjecture,
~ hskp0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1846,c_0_1800]),c_0_1801]),c_0_1364]),c_0_1847]),c_0_1813]),c_0_898]),c_0_885]),
[final] ).
cnf(c_0_1873,negated_conjecture,
epred7_0,
inference(sr,[status(thm)],[c_0_1850,c_0_1851]),
[final] ).
cnf(c_0_1874,negated_conjecture,
( ~ hskp15
| hskp27
| hskp1
| c1_1(a1272) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1214]),c_0_1583]),
[final] ).
cnf(c_0_1875,negated_conjecture,
( ~ hskp1
| epred28_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_1830]),c_0_171]),c_0_172]),
[final] ).
cnf(c_0_1876,negated_conjecture,
( ~ c0_1(X1)
| hskp11
| hskp0
| c2_1(X1)
| c3_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1852,c_0_161])]),
[final] ).
cnf(c_0_1877,negated_conjecture,
( ~ c1_1(X1)
| hskp20
| c0_1(X1)
| c3_1(X1)
| epred2_0
| epred29_0 ),
inference(spm,[status(thm)],[c_0_770,c_0_1146]),
[final] ).
cnf(c_0_1879,negated_conjecture,
hskp7,
inference(sr,[status(thm)],[c_0_1853,c_0_1851]),
[final] ).
cnf(c_0_1894,negated_conjecture,
( ~ hskp1
| ~ c0_1(a1254) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1846,c_0_171]),c_0_1364]),c_0_1847]),c_0_1813]),c_0_172]),
[final] ).
cnf(c_0_1896,negated_conjecture,
( ~ hskp15
| ~ c1_1(a1272)
| epred11_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1584,c_0_630]),c_0_1583]),
[final] ).
cnf(c_0_1897,negated_conjecture,
( hskp26
| c2_1(X1)
| c3_1(X1)
| epred1_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1870,c_0_1866]),c_0_1195]),
[final] ).
cnf(c_0_1898,negated_conjecture,
( ~ hskp15
| hskp26
| epred28_0 ),
inference(spm,[status(thm)],[c_0_1871,c_0_1872]),
[final] ).
cnf(c_0_1900,negated_conjecture,
~ epred6_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1696,c_0_1873])]),
[final] ).
cnf(c_0_1901,negated_conjecture,
( ~ hskp15
| hskp27
| epred28_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1848,c_0_1874]),c_0_1875]),
[final] ).
cnf(c_0_1902,negated_conjecture,
( ~ hskp15
| epred28_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_1848,c_0_1845]),
[final] ).
cnf(c_0_1903,negated_conjecture,
( ~ c1_1(X1)
| hskp20
| c3_1(X1)
| epred28_0
| epred29_0 ),
inference(spm,[status(thm)],[c_0_770,c_0_1830]),
[final] ).
cnf(c_0_1905,negated_conjecture,
( ~ hskp23
| epred2_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1877,c_0_634]),c_0_1364]),c_0_1813]),c_0_635]),c_0_633]),
[final] ).
cnf(c_0_1907,negated_conjecture,
epred13_0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1421,c_0_1879])]),c_0_1802]),
[final] ).
cnf(c_0_1915,negated_conjecture,
~ epred18_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_406,c_0_1730])]),
[final] ).
cnf(c_0_1921,negated_conjecture,
( ~ hskp15
| hskp27
| hskp16
| epred10_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_527,c_0_1890]),c_0_1581]),c_0_1584]),
[final] ).
cnf(c_0_1922,negated_conjecture,
( hskp26
| c2_1(X1)
| c3_1(X1)
| epred10_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_381,c_0_1891]),c_0_1801]),
[final] ).
cnf(c_0_1923,negated_conjecture,
( c2_1(X1)
| c3_1(X1)
| epred10_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_381,c_0_1892]),c_0_1801]),
[final] ).
cnf(c_0_1926,negated_conjecture,
( ~ hskp1
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1894,c_0_1895]),
[final] ).
cnf(c_0_1929,negated_conjecture,
( c2_1(X1)
| c3_1(X1)
| epred1_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_1606,c_0_1897]),
[final] ).
cnf(c_0_1932,negated_conjecture,
~ hskp11,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1846,c_0_386]),c_0_1364]),c_0_1847]),c_0_1813]),c_0_387]),c_0_388]),
[final] ).
cnf(c_0_1934,negated_conjecture,
( ~ c1_1(X1)
| hskp20
| hskp3
| c0_1(X1)
| c3_1(X1)
| epred6_0
| epred29_0 ),
inference(spm,[status(thm)],[c_0_770,c_0_1582]),
[final] ).
cnf(c_0_1935,negated_conjecture,
( hskp26
| c2_1(X1)
| c3_1(X1)
| epred28_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1898,c_0_1866]),c_0_1830]),
[final] ).
cnf(c_0_1936,negated_conjecture,
( c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| epred15_0 ),
inference(sr,[status(thm)],[c_0_1899,c_0_1900]),
[final] ).
cnf(c_0_1937,negated_conjecture,
( ~ hskp15
| epred2_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1146]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_1938,negated_conjecture,
( hskp27
| c2_1(X1)
| c3_1(X1)
| epred28_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1901,c_0_1866]),c_0_1830]),
[final] ).
cnf(c_0_1939,negated_conjecture,
( c2_1(X1)
| c3_1(X1)
| epred28_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1902,c_0_1866]),c_0_1830]),
[final] ).
cnf(c_0_1945,negated_conjecture,
~ epred12_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_302,c_0_1907])]),
[final] ).
cnf(c_0_1946,negated_conjecture,
hskp19,
inference(sr,[status(thm)],[c_0_1908,c_0_1802]),
[final] ).
cnf(c_0_1960,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| hskp6
| c3_1(X1)
| c1_1(X1)
| epred39_0 ),
inference(spm,[status(thm)],[c_0_805,c_0_258]),
[final] ).
cnf(c_0_1961,negated_conjecture,
( hskp27
| hskp16
| c2_1(X1)
| c3_1(X1)
| epred10_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1921,c_0_1866]),c_0_527]),
[final] ).
cnf(c_0_1962,negated_conjecture,
( ~ c1_1(X1)
| hskp26
| c3_1(X1)
| epred10_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1922]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1963,negated_conjecture,
( ~ c1_1(X1)
| c3_1(X1)
| epred10_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1923]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1964,negated_conjecture,
( ~ c0_1(X1)
| ~ c3_1(X1)
| hskp12
| c2_1(X1)
| epred34_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1924]),c_0_161])]),
[final] ).
cnf(c_0_1965,negated_conjecture,
( hskp27
| hskp3
| c0_1(X1)
| c2_1(X1)
| c1_1(X1) ),
inference(sr,[status(thm)],[c_0_1925,c_0_1900]),
[final] ).
cnf(c_0_1966,negated_conjecture,
( ~ hskp15
| hskp27
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1926,c_0_1927]),
[final] ).
cnf(c_0_1967,negated_conjecture,
( ~ hskp15
| hskp26
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1871,c_0_1928]),
[final] ).
cnf(c_0_1968,negated_conjecture,
( ~ c1_1(X1)
| c3_1(X1)
| epred1_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1929]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1969,negated_conjecture,
( ~ c1_1(X1)
| hskp26
| c3_1(X1)
| epred1_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1897]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1970,negated_conjecture,
( ~ hskp22
| c1_1(a1291) ),
c_0_1930,
[final] ).
cnf(c_0_1971,negated_conjecture,
( ~ hskp22
| c0_1(a1291) ),
c_0_1931,
[final] ).
cnf(c_0_1972,negated_conjecture,
( ~ hskp15
| epred11_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_1896,c_0_1845]),
[final] ).
cnf(c_0_1973,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| epred4_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_1588,c_0_563]),
[final] ).
cnf(c_0_1974,negated_conjecture,
( hskp27
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred28_0 ),
inference(spm,[status(thm)],[c_0_1875,c_0_1214]),
[final] ).
cnf(c_0_1975,negated_conjecture,
( hskp12
| c0_1(X1)
| c2_1(X1)
| c3_1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1210,c_0_1582]),c_0_1900]),c_0_1932]),
[final] ).
cnf(c_0_1976,negated_conjecture,
( ~ hskp15
| hskp12 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1932,c_0_1933]),c_0_1900]),
[final] ).
cnf(c_0_1977,negated_conjecture,
( ~ hskp23
| hskp3 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1934,c_0_634]),c_0_1364]),c_0_1900]),c_0_1813]),c_0_635]),c_0_633]),
[final] ).
cnf(c_0_1978,negated_conjecture,
( ~ c1_1(X1)
| hskp26
| c3_1(X1)
| epred28_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1935]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1979,negated_conjecture,
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred15_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1936]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1982,negated_conjecture,
( ~ hskp15
| c1_1(a1272)
| epred9_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_222]),c_0_1584]),
[final] ).
cnf(c_0_1984,negated_conjecture,
( ~ c1_1(X1)
| hskp27
| c3_1(X1)
| epred28_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1938]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1985,negated_conjecture,
( ~ c1_1(X1)
| c3_1(X1)
| epred28_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1939]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_1986,negated_conjecture,
( ~ hskp22
| ~ c2_1(a1291) ),
c_0_1940,
[final] ).
cnf(c_0_1991,negated_conjecture,
hskp14,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_556,c_0_1879])]),c_0_1945]),
[final] ).
cnf(c_0_1993,negated_conjecture,
hskp4,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_837,c_0_1946])]),c_0_1773]),
[final] ).
cnf(c_0_1994,negated_conjecture,
( ~ hskp18
| hskp3
| c3_1(a1279)
| epred6_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_503,c_0_1582]),c_0_505]),
[final] ).
cnf(c_0_1996,negated_conjecture,
( ~ hskp5
| hskp27
| hskp1
| c0_1(a1258) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_1214]),c_0_259]),
[final] ).
cnf(c_0_2006,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| epred4_0
| epred41_0 ),
inference(spm,[status(thm)],[c_0_791,c_0_563]),
[final] ).
cnf(c_0_2011,negated_conjecture,
( ~ c1_1(X1)
| c3_1(X1)
| epred28_0
| epred41_0 ),
inference(spm,[status(thm)],[c_0_791,c_0_1830]),
[final] ).
cnf(c_0_2014,negated_conjecture,
hskp10,
inference(sr,[status(thm)],[c_0_1954,c_0_1851]),
[final] ).
cnf(c_0_2019,negated_conjecture,
( ~ hskp16
| hskp9 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1960,c_0_197]),c_0_1600]),c_0_1844]),c_0_198]),c_0_199]),
[final] ).
cnf(c_0_2020,negated_conjecture,
( ~ c1_1(X1)
| hskp27
| hskp16
| c3_1(X1)
| epred10_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1961]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_2022,negated_conjecture,
( ~ hskp23
| hskp26
| epred10_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1962,c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2023,negated_conjecture,
( ~ hskp1
| hskp26
| epred10_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_1922]),c_0_172]),
[final] ).
cnf(c_0_2024,negated_conjecture,
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| epred21_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_1588,c_0_184]),
[final] ).
cnf(c_0_2025,negated_conjecture,
( ~ hskp23
| epred10_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_633,c_0_1963]),c_0_634]),
[final] ).
cnf(c_0_2026,negated_conjecture,
( ~ hskp1
| epred10_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_1923]),c_0_172]),
[final] ).
cnf(c_0_2028,negated_conjecture,
( ~ c0_1(X1)
| hskp12
| c2_1(X1)
| c1_1(X1)
| epred34_0
| epred44_0 ),
inference(spm,[status(thm)],[c_0_1964,c_0_344]),
[final] ).
cnf(c_0_2030,negated_conjecture,
( hskp27
| c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1966,c_0_1866]),
[final] ).
cnf(c_0_2031,negated_conjecture,
( hskp26
| c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1967,c_0_1866]),
[final] ).
cnf(c_0_2032,negated_conjecture,
( ~ hskp23
| epred1_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_633,c_0_1968]),c_0_634]),
[final] ).
cnf(c_0_2033,negated_conjecture,
( ~ hskp23
| hskp26
| epred1_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1969,c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2034,negated_conjecture,
( ~ hskp1
| epred1_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_1929]),c_0_172]),
[final] ).
cnf(c_0_2035,negated_conjecture,
( ~ hskp22
| c3_1(a1291) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1846,c_0_1970]),c_0_1364]),c_0_1847]),c_0_1813]),c_0_1971]),
[final] ).
cnf(c_0_2036,negated_conjecture,
( c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred11_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_1972,c_0_1866]),
[final] ).
cnf(c_0_2037,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp20
| hskp2
| epred4_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_327,c_0_1973]),
[final] ).
cnf(c_0_2038,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp12
| epred4_0
| epred34_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_1973]),c_0_1588]),
[final] ).
cnf(c_0_2040,negated_conjecture,
( ~ hskp1
| hskp12 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_1975]),c_0_1894]),c_0_172]),
[final] ).
cnf(c_0_2041,negated_conjecture,
( ~ c1_1(X1)
| hskp12
| c0_1(X1)
| c3_1(X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_1975]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_2042,negated_conjecture,
( hskp12
| c2_1(X1)
| c3_1(X1)
| c1_1(X1) ),
inference(spm,[status(thm)],[c_0_1976,c_0_1866]),
[final] ).
cnf(c_0_2043,negated_conjecture,
( ~ hskp16
| hskp24
| hskp3 ),
inference(spm,[status(thm)],[c_0_1977,c_0_688]),
[final] ).
cnf(c_0_2044,negated_conjecture,
( ~ hskp23
| hskp26
| epred28_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1978,c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2045,negated_conjecture,
( ~ hskp23
| epred15_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_633,c_0_1979]),c_0_634]),c_0_635]),
[final] ).
cnf(c_0_2046,negated_conjecture,
( c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred15_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1980,c_0_1866]),c_0_1900]),
[final] ).
cnf(c_0_2047,negated_conjecture,
( c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred2_0 ),
inference(sr,[status(thm)],[c_0_1981,c_0_1844]),
[final] ).
cnf(c_0_2048,negated_conjecture,
( ~ hskp15
| hskp16
| epred9_0
| epred10_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_527,c_0_1982]),c_0_1581]),c_0_1584]),
[final] ).
cnf(c_0_2049,negated_conjecture,
( ~ hskp18
| hskp15 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1276,c_0_1983]),c_0_1802]),
[final] ).
cnf(c_0_2050,negated_conjecture,
( ~ hskp15
| epred9_0
| epred28_0 ),
inference(spm,[status(thm)],[c_0_1848,c_0_1982]),
[final] ).
cnf(c_0_2051,negated_conjecture,
( ~ hskp15
| epred9_0
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1896,c_0_1982]),
[final] ).
cnf(c_0_2052,negated_conjecture,
( ~ hskp23
| hskp27
| epred28_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1984,c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2053,negated_conjecture,
( ~ hskp23
| epred28_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_633,c_0_1985]),c_0_634]),
[final] ).
cnf(c_0_2055,negated_conjecture,
( hskp12
| c2_1(X1)
| c3_1(X1)
| epred28_0 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1987,c_0_1866]),c_0_1900]),c_0_1813]),c_0_1830]),
[final] ).
cnf(c_0_2061,negated_conjecture,
~ hskp8,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1846,c_0_1995]),c_0_1600]),c_0_1364]),c_0_1847]),c_0_1813]),c_0_649]),c_0_650]),
[final] ).
cnf(c_0_2062,negated_conjecture,
( ~ hskp1
| epred2_0 ),
inference(spm,[status(thm)],[c_0_1894,c_0_1212]),
[final] ).
cnf(c_0_2063,negated_conjecture,
( ~ hskp5
| hskp27
| hskp1
| epred39_0 ),
inference(spm,[status(thm)],[c_0_275,c_0_1996]),
[final] ).
cnf(c_0_2064,negated_conjecture,
( ~ hskp1
| hskp3 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1894,c_0_1869]),c_0_1900]),
[final] ).
cnf(c_0_2066,negated_conjecture,
( ~ hskp1
| epred15_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1868,c_0_1998]),c_0_1847]),
[final] ).
cnf(c_0_2067,negated_conjecture,
( ~ hskp15
| epred15_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1936]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_2070,negated_conjecture,
hskp29,
inference(sr,[status(thm)],[c_0_2000,c_0_1844]),
[final] ).
cnf(c_0_2071,negated_conjecture,
hskp28,
inference(sr,[status(thm)],[c_0_2001,c_0_1844]),
[final] ).
cnf(c_0_2072,negated_conjecture,
hskp17,
inference(sr,[status(thm)],[c_0_2002,c_0_1801]),
[final] ).
cnf(c_0_2076,negated_conjecture,
( ~ hskp23
| hskp16
| c2_1(a1300)
| epred10_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_527,c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2079,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp21
| epred4_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_1973]),c_0_1189]),
[final] ).
cnf(c_0_2080,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp21
| epred41_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_2006]),c_0_1189]),c_0_1847]),
[final] ).
cnf(c_0_2082,negated_conjecture,
epred40_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1590,c_0_2010]),c_0_570]),
[final] ).
cnf(c_0_2083,negated_conjecture,
( ~ hskp23
| hskp20
| epred28_0
| epred29_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1903,c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2084,negated_conjecture,
( ~ hskp5
| hskp3
| hskp2
| c0_1(a1258) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_504]),c_0_259]),
[final] ).
cnf(c_0_2085,negated_conjecture,
( ~ hskp23
| epred28_0
| epred41_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_633,c_0_2011]),c_0_634]),
[final] ).
cnf(c_0_2089,negated_conjecture,
~ c3_1(a1283),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_279,c_0_1946])]),
[final] ).
cnf(c_0_2090,negated_conjecture,
~ c1_1(a1283),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_280,c_0_1946])]),
[final] ).
cnf(c_0_2095,negated_conjecture,
( ~ hskp15
| hskp3
| epred35_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1934,c_0_1845]),c_0_1364]),c_0_1900]),c_0_1813]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_2096,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp12
| epred10_0
| epred34_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_1963]),c_0_1588]),
[final] ).
cnf(c_0_2097,negated_conjecture,
( ~ c0_1(X1)
| hskp27
| hskp9
| c3_1(X1)
| epred10_0 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1961]),c_0_1844]),c_0_2019]),
[final] ).
cnf(c_0_2098,negated_conjecture,
( ~ hskp23
| hskp27
| hskp16
| epred10_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2020,c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2099,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp12
| epred1_0
| epred34_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_1968]),c_0_1588]),
[final] ).
cnf(c_0_2100,negated_conjecture,
( ~ hskp15
| hskp3
| hskp2 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1934,c_0_2021]),c_0_1364]),c_0_1900]),c_0_1813]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_2101,negated_conjecture,
( ~ c0_1(X1)
| hskp26
| hskp9
| c3_1(X1)
| epred10_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1922]),c_0_1844]),
[final] ).
cnf(c_0_2102,negated_conjecture,
( ~ hskp16
| hskp26
| hskp24
| epred10_0 ),
inference(spm,[status(thm)],[c_0_2022,c_0_688]),
[final] ).
cnf(c_0_2103,negated_conjecture,
( ~ hskp13
| hskp26
| c3_1(a1268)
| epred10_0 ),
inference(spm,[status(thm)],[c_0_391,c_0_1922]),
[final] ).
cnf(c_0_2104,negated_conjecture,
( ~ hskp16
| hskp26
| epred8_0
| epred10_0 ),
inference(spm,[status(thm)],[c_0_2023,c_0_220]),
[final] ).
cnf(c_0_2105,negated_conjecture,
( ~ hskp15
| hskp26
| epred10_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1922]),c_0_1584]),
[final] ).
cnf(c_0_2106,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| epred10_0
| epred21_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2024,c_0_1963]),
[final] ).
cnf(c_0_2107,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp2
| epred10_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_1963]),c_0_1813]),
[final] ).
cnf(c_0_2108,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp21
| epred10_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_1963]),c_0_1189]),
[final] ).
cnf(c_0_2109,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| c3_1(X1)
| epred10_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1923]),c_0_1844]),
[final] ).
cnf(c_0_2110,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1301)
| epred10_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_629,c_0_1963]),
[final] ).
cnf(c_0_2111,negated_conjecture,
( ~ hskp16
| hskp24
| epred10_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2025,c_0_688]),
[final] ).
cnf(c_0_2112,negated_conjecture,
( ~ hskp13
| c3_1(a1268)
| epred10_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_391,c_0_1923]),
[final] ).
cnf(c_0_2113,negated_conjecture,
( ~ hskp16
| epred8_0
| epred10_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2026,c_0_220]),
[final] ).
cnf(c_0_2114,negated_conjecture,
( ~ hskp15
| epred10_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1923]),c_0_1584]),
[final] ).
cnf(c_0_2115,negated_conjecture,
( ~ hskp5
| hskp27
| hskp16
| epred10_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_275,c_0_2027]),c_0_1600]),
[final] ).
cnf(c_0_2116,negated_conjecture,
( ~ hskp16
| hskp12
| c2_1(a1274)
| epred34_0 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2028,c_0_197]),c_0_1801]),c_0_199]),
[final] ).
cnf(c_0_2117,negated_conjecture,
( ~ hskp15
| hskp27
| hskp3 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1934,c_0_2029]),c_0_1364]),c_0_1900]),c_0_1813]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_2118,negated_conjecture,
( ~ c0_1(X1)
| hskp27
| hskp9
| c3_1(X1)
| c1_1(X1)
| epred11_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_2030]),c_0_1844]),
[final] ).
cnf(c_0_2119,negated_conjecture,
( ~ c0_1(X1)
| hskp26
| hskp9
| c3_1(X1)
| c1_1(X1)
| epred11_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_2031]),c_0_1844]),
[final] ).
cnf(c_0_2120,negated_conjecture,
( ~ hskp15
| hskp26
| hskp3 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1934,c_0_1842]),c_0_1364]),c_0_1900]),c_0_1813]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_2121,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| epred1_0
| epred21_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2024,c_0_1968]),
[final] ).
cnf(c_0_2122,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp2
| epred1_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_1968]),c_0_1813]),
[final] ).
cnf(c_0_2123,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp21
| epred1_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_1968]),c_0_1189]),
[final] ).
cnf(c_0_2124,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| c3_1(X1)
| epred1_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1929]),c_0_1844]),
[final] ).
cnf(c_0_2125,negated_conjecture,
( ~ c0_1(X1)
| hskp26
| hskp9
| c3_1(X1)
| epred1_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1897]),c_0_1844]),
[final] ).
cnf(c_0_2126,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1301)
| epred1_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_629,c_0_1968]),
[final] ).
cnf(c_0_2127,negated_conjecture,
( ~ hskp16
| hskp24
| epred1_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2032,c_0_688]),
[final] ).
cnf(c_0_2128,negated_conjecture,
( ~ hskp16
| hskp26
| hskp24
| epred1_0 ),
inference(spm,[status(thm)],[c_0_2033,c_0_688]),
[final] ).
cnf(c_0_2129,negated_conjecture,
( ~ hskp13
| c3_1(a1268)
| epred1_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_391,c_0_1929]),
[final] ).
cnf(c_0_2130,negated_conjecture,
( ~ hskp16
| epred1_0
| epred8_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2034,c_0_220]),
[final] ).
cnf(c_0_2131,negated_conjecture,
( ~ hskp15
| epred1_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1581,c_0_1929]),c_0_1584]),
[final] ).
cnf(c_0_2132,negated_conjecture,
( ~ hskp2
| hskp9
| c3_1(a1255) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1960,c_0_367]),c_0_1600]),c_0_1844]),c_0_365]),
[final] ).
cnf(c_0_2133,negated_conjecture,
( ~ hskp22
| hskp12
| epred34_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_2035]),c_0_1971]),c_0_1986]),
[final] ).
cnf(c_0_2134,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| c3_1(X1)
| c1_1(X1)
| epred11_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_2036]),c_0_1844]),
[final] ).
cnf(c_0_2135,negated_conjecture,
( ~ hskp27
| hskp2
| epred35_0 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2037,c_0_730]),c_0_1847]),c_0_1813]),c_0_731]),
[final] ).
cnf(c_0_2136,negated_conjecture,
( ~ hskp27
| hskp12
| epred34_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2038,c_0_730]),c_0_1847]),c_0_731]),
[final] ).
cnf(c_0_2137,negated_conjecture,
( ~ hskp5
| hskp27
| epred28_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_275,c_0_2039]),c_0_1600]),
[final] ).
cnf(c_0_2138,negated_conjecture,
( hskp12
| hskp2
| c0_1(X1)
| c2_1(X1)
| c1_1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1210,c_0_504]),c_0_1932]),
[final] ).
cnf(c_0_2139,negated_conjecture,
( hskp27
| hskp12
| c0_1(X1)
| c2_1(X1)
| c1_1(X1) ),
inference(spm,[status(thm)],[c_0_2040,c_0_1214]),
[final] ).
cnf(c_0_2140,negated_conjecture,
( ~ hskp23
| hskp12 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2041,c_0_634]),c_0_635]),c_0_633]),
[final] ).
cnf(c_0_2141,negated_conjecture,
( ~ hskp13
| hskp12
| c3_1(a1268) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_391,c_0_1975]),c_0_393]),
[final] ).
cnf(c_0_2142,negated_conjecture,
( ~ hskp22
| hskp2 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_2035]),c_0_1813]),c_0_1971]),c_0_1970]),
[final] ).
cnf(c_0_2143,negated_conjecture,
( ~ hskp22
| hskp21 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_2035]),c_0_1189]),c_0_1971]),c_0_1970]),
[final] ).
cnf(c_0_2144,negated_conjecture,
( ~ c0_1(X1)
| hskp12
| hskp9
| c3_1(X1)
| c1_1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_2042]),c_0_1844]),
[final] ).
cnf(c_0_2145,negated_conjecture,
( ~ hskp16
| hskp24
| hskp12 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1210,c_0_2043]),c_0_1932]),
[final] ).
cnf(c_0_2146,negated_conjecture,
( ~ c0_1(X1)
| hskp26
| hskp9
| c3_1(X1)
| epred28_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1935]),c_0_1844]),
[final] ).
cnf(c_0_2147,negated_conjecture,
( ~ hskp16
| hskp26
| hskp24
| epred28_0 ),
inference(spm,[status(thm)],[c_0_2044,c_0_688]),
[final] ).
cnf(c_0_2148,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1301)
| epred15_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_629,c_0_1979]),c_0_631]),
[final] ).
cnf(c_0_2149,negated_conjecture,
( ~ hskp16
| hskp24
| epred15_0 ),
inference(spm,[status(thm)],[c_0_2045,c_0_688]),
[final] ).
cnf(c_0_2150,negated_conjecture,
( ~ hskp13
| hskp3
| c3_1(a1268) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1934,c_0_392]),c_0_1364]),c_0_1900]),c_0_1813]),c_0_393]),
[final] ).
cnf(c_0_2151,negated_conjecture,
( hskp27
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred15_0 ),
inference(spm,[status(thm)],[c_0_1284,c_0_1965]),
[final] ).
cnf(c_0_2152,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| c3_1(X1)
| c1_1(X1)
| epred15_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_2046]),c_0_1844]),
[final] ).
cnf(c_0_2153,negated_conjecture,
( ~ hskp15
| hskp3
| epred9_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1934,c_0_1982]),c_0_1364]),c_0_1900]),c_0_1813]),c_0_1583]),c_0_1584]),
[final] ).
cnf(c_0_2154,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| c3_1(X1)
| c1_1(X1)
| epred2_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_2047]),c_0_1844]),
[final] ).
cnf(c_0_2155,negated_conjecture,
( ~ c0_1(X1)
| hskp15
| hskp9
| c3_1(X1)
| c1_1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1866]),c_0_1844]),
[final] ).
cnf(c_0_2156,negated_conjecture,
( ~ hskp18
| hskp16
| epred9_0
| epred10_0 ),
inference(spm,[status(thm)],[c_0_2048,c_0_2049]),
[final] ).
cnf(c_0_2157,negated_conjecture,
( ~ hskp18
| epred9_0
| epred28_0 ),
inference(spm,[status(thm)],[c_0_2050,c_0_2049]),
[final] ).
cnf(c_0_2158,negated_conjecture,
( ~ hskp18
| epred9_0
| epred11_0 ),
inference(spm,[status(thm)],[c_0_2051,c_0_2049]),
[final] ).
cnf(c_0_2159,negated_conjecture,
( ~ hskp18
| epred2_0 ),
inference(spm,[status(thm)],[c_0_1937,c_0_2049]),
[final] ).
cnf(c_0_2160,negated_conjecture,
( ~ c0_1(X1)
| hskp27
| hskp9
| c3_1(X1)
| epred28_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1938]),c_0_1844]),
[final] ).
cnf(c_0_2161,negated_conjecture,
( ~ hskp26
| c3_1(a1250) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1846,c_0_508]),c_0_1364]),c_0_1847]),c_0_1813]),c_0_509]),
[final] ).
cnf(c_0_2162,negated_conjecture,
( ~ hskp16
| hskp27
| hskp24
| epred28_0 ),
inference(spm,[status(thm)],[c_0_2052,c_0_688]),
[final] ).
cnf(c_0_2163,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| c3_1(X1)
| epred28_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_1939]),c_0_1844]),
[final] ).
cnf(c_0_2164,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1301)
| epred28_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_629,c_0_1985]),
[final] ).
cnf(c_0_2165,negated_conjecture,
( ~ hskp16
| hskp24
| epred28_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2053,c_0_688]),
[final] ).
cnf(c_0_2166,negated_conjecture,
( ~ hskp22
| epred21_0 ),
inference(spm,[status(thm)],[c_0_2054,c_0_2035]),
[final] ).
cnf(c_0_2167,negated_conjecture,
( ~ c0_1(X1)
| hskp12
| hskp9
| c3_1(X1)
| epred28_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_2055]),c_0_1844]),
[final] ).
cnf(c_0_2168,negated_conjecture,
( ~ hskp16
| hskp12
| epred8_0 ),
inference(spm,[status(thm)],[c_0_1932,c_0_2056]),
[final] ).
cnf(c_0_2169,negated_conjecture,
( hskp27
| hskp24
| epred2_0 ),
inference(sr,[status(thm)],[c_0_2057,c_0_1932]),
[final] ).
cnf(c_0_2170,negated_conjecture,
( hskp12
| c1_1(a1270) ),
inference(sr,[status(thm)],[c_0_2058,c_0_1932]),
[final] ).
cnf(c_0_2171,negated_conjecture,
( hskp12
| c0_1(a1257) ),
inference(sr,[status(thm)],[c_0_2059,c_0_1932]),
[final] ).
cnf(c_0_2172,negated_conjecture,
( ~ hskp5
| hskp12 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1932,c_0_466]),c_0_1600]),
[final] ).
cnf(c_0_2173,negated_conjecture,
( ~ hskp18
| hskp12 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1932,c_0_2060]),c_0_1900]),
[final] ).
cnf(c_0_2174,negated_conjecture,
( ~ hskp16
| epred14_0 ),
inference(spm,[status(thm)],[c_0_2061,c_0_705]),
[final] ).
cnf(c_0_2175,negated_conjecture,
( ~ hskp5
| hskp27
| epred2_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2062,c_0_2063]),c_0_1600]),
[final] ).
cnf(c_0_2176,negated_conjecture,
( ~ hskp16
| epred2_0
| epred8_0 ),
inference(spm,[status(thm)],[c_0_2062,c_0_220]),
[final] ).
cnf(c_0_2177,negated_conjecture,
( ~ hskp5
| hskp27
| epred11_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1926,c_0_2063]),c_0_1600]),
[final] ).
cnf(c_0_2178,negated_conjecture,
( ~ hskp18
| hskp27
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1926,c_0_1235]),
[final] ).
cnf(c_0_2179,negated_conjecture,
( ~ hskp16
| epred8_0
| epred11_0 ),
inference(spm,[status(thm)],[c_0_1926,c_0_220]),
[final] ).
cnf(c_0_2180,negated_conjecture,
( ~ hskp5
| hskp27
| hskp3 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2064,c_0_2063]),c_0_1600]),
[final] ).
cnf(c_0_2181,negated_conjecture,
( ~ hskp18
| hskp27
| hskp3 ),
inference(spm,[status(thm)],[c_0_2064,c_0_1235]),
[final] ).
cnf(c_0_2182,negated_conjecture,
( ~ hskp16
| hskp3
| epred8_0 ),
inference(spm,[status(thm)],[c_0_2064,c_0_220]),
[final] ).
cnf(c_0_2183,negated_conjecture,
( ~ hskp5
| hskp26 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1871,c_0_2065]),c_0_1600]),
[final] ).
cnf(c_0_2184,negated_conjecture,
( ~ hskp18
| hskp26 ),
inference(spm,[status(thm)],[c_0_1871,c_0_953]),
[final] ).
cnf(c_0_2185,negated_conjecture,
( ~ c1_1(X1)
| hskp12
| c3_1(X1)
| epred28_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_2055]),c_0_1364]),c_0_1813]),
[final] ).
cnf(c_0_2186,negated_conjecture,
( ~ hskp16
| hskp24
| epred2_0 ),
inference(spm,[status(thm)],[c_0_1905,c_0_688]),
[final] ).
cnf(c_0_2187,negated_conjecture,
( ~ hskp13
| c3_1(a1268)
| epred15_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_391,c_0_1936]),c_0_393]),
[final] ).
cnf(c_0_2188,negated_conjecture,
( ~ hskp5
| hskp27
| epred15_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2066,c_0_2063]),c_0_1600]),
[final] ).
cnf(c_0_2189,negated_conjecture,
( ~ hskp16
| epred8_0
| epred15_0 ),
inference(spm,[status(thm)],[c_0_2066,c_0_220]),
[final] ).
cnf(c_0_2190,negated_conjecture,
( ~ hskp18
| epred15_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2067,c_0_2068]),c_0_1802]),c_0_1844]),
[final] ).
cnf(c_0_2191,negated_conjecture,
( ~ hskp26
| hskp2 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_2069]),c_0_1364]),c_0_1813]),c_0_509]),c_0_508]),
[final] ).
cnf(c_0_2192,negated_conjecture,
( ~ hskp26
| hskp21 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_2069]),c_0_1189]),c_0_1364]),c_0_1813]),c_0_509]),c_0_508]),
[final] ).
cnf(c_0_2193,negated_conjecture,
( ~ c1_1(a1280)
| epred35_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1702,c_0_2070])]),
[final] ).
cnf(c_0_2194,negated_conjecture,
( ~ c1_1(a1280)
| hskp2 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1466,c_0_2070])]),c_0_1813]),
[final] ).
cnf(c_0_2195,negated_conjecture,
( ~ c1_1(a1280)
| hskp21 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1481,c_0_2070])]),c_0_1189]),
[final] ).
cnf(c_0_2196,negated_conjecture,
( ~ c0_1(a1259)
| epred35_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1596,c_0_2071])]),
[final] ).
cnf(c_0_2197,negated_conjecture,
( ~ c0_1(a1259)
| hskp2 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_368,c_0_2071])]),c_0_1813]),
[final] ).
cnf(c_0_2198,negated_conjecture,
( ~ c0_1(a1259)
| hskp21 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1127,c_0_2071])]),c_0_1189]),
[final] ).
cnf(c_0_2199,negated_conjecture,
( ~ c0_1(a1277)
| hskp20
| hskp2 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_400,c_0_2072])]),
[final] ).
cnf(c_0_2200,negated_conjecture,
( ~ c0_1(a1277)
| hskp12
| epred34_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2073,c_0_2072])]),
[final] ).
cnf(c_0_2201,negated_conjecture,
( c1_1(a1270)
| epred15_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1335,c_0_1991])]),
[final] ).
cnf(c_0_2202,negated_conjecture,
( ~ c0_1(a1277)
| epred21_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_253,c_0_2072])]),
[final] ).
cnf(c_0_2203,negated_conjecture,
( ~ c0_1(a1277)
| hskp21 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_853,c_0_2072])]),c_0_1189]),
[final] ).
cnf(c_0_2204,negated_conjecture,
( c0_1(a1257)
| epred15_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_777,c_0_1993])]),
[final] ).
cnf(c_0_2205,negated_conjecture,
( hskp13
| epred5_0 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_2074,c_0_1946])]),c_0_1801]),
[final] ).
cnf(c_0_2206,negated_conjecture,
( hskp9
| epred22_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_890,c_0_1993])]),
[final] ).
cnf(c_0_2207,negated_conjecture,
( ~ hskp5
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_275,c_0_2075]),c_0_1600]),
[final] ).
cnf(c_0_2208,negated_conjecture,
( ~ hskp18
| epred35_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_503,c_0_1828]),c_0_505]),c_0_506]),
[final] ).
cnf(c_0_2209,negated_conjecture,
( ~ hskp23
| hskp16
| epred10_0
| epred41_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_791,c_0_2076]),c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2210,negated_conjecture,
( ~ hskp23
| hskp20
| hskp16
| epred10_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_770,c_0_2076]),c_0_1364]),c_0_634]),c_0_633]),
[final] ).
cnf(c_0_2211,negated_conjecture,
( hskp27
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred11_0 ),
inference(sr,[status(thm)],[c_0_2077,c_0_1847]),
[final] ).
cnf(c_0_2212,negated_conjecture,
( hskp27
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred2_0 ),
inference(sr,[status(thm)],[c_0_2078,c_0_1847]),
[final] ).
cnf(c_0_2213,negated_conjecture,
( ~ hskp27
| hskp21
| epred35_0 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2079,c_0_730]),c_0_1847]),c_0_731]),
[final] ).
cnf(c_0_2214,negated_conjecture,
( ~ hskp27
| hskp21
| epred41_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2080,c_0_730]),c_0_731]),
[final] ).
cnf(c_0_2215,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| epred21_0
| epred35_0
| epred41_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2024,c_0_2006]),c_0_1847]),
[final] ).
cnf(c_0_2216,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp20
| hskp2
| epred41_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_2006]),c_0_1847]),
[final] ).
cnf(c_0_2217,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp12
| c2_1(X1)
| epred34_0
| epred41_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_2006]),c_0_1847]),
[final] ).
cnf(c_0_2218,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp2
| epred28_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_1950]),c_0_2081]),
[final] ).
cnf(c_0_2219,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp21
| epred28_0
| epred35_0 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_795,c_0_1950]),c_0_1189]),
[final] ).
cnf(c_0_2220,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp12
| epred28_0
| epred34_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_1950]),c_0_1588]),
[final] ).
cnf(c_0_2221,negated_conjecture,
( ~ hskp27
| epred21_0
| epred35_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_2024,c_0_729]),c_0_730]),c_0_731]),
[final] ).
cnf(c_0_2222,negated_conjecture,
( ~ epred11_0
| ~ epred41_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_907,c_0_2082])]),
[final] ).
cnf(c_0_2223,negated_conjecture,
( hskp2
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| epred15_0 ),
inference(spm,[status(thm)],[c_0_1284,c_0_504]),
[final] ).
cnf(c_0_2224,negated_conjecture,
( ~ hskp5
| hskp27
| hskp1
| epred45_0 ),
inference(spm,[status(thm)],[c_0_564,c_0_1996]),
[final] ).
cnf(c_0_2225,negated_conjecture,
( ~ hskp5
| hskp27
| hskp1
| epred21_0 ),
inference(spm,[status(thm)],[c_0_207,c_0_1996]),
[final] ).
cnf(c_0_2226,negated_conjecture,
( ~ hskp18
| hskp27
| hskp16
| epred10_0 ),
inference(spm,[status(thm)],[c_0_561,c_0_1235]),
[final] ).
cnf(c_0_2227,negated_conjecture,
( ~ hskp18
| hskp27
| epred28_0 ),
inference(spm,[status(thm)],[c_0_1875,c_0_1235]),
[final] ).
cnf(c_0_2228,negated_conjecture,
( ~ hskp16
| hskp24
| hskp20
| epred28_0
| epred29_0 ),
inference(spm,[status(thm)],[c_0_2083,c_0_688]),
[final] ).
cnf(c_0_2229,negated_conjecture,
( ~ hskp5
| hskp3
| hskp2
| epred45_0 ),
inference(spm,[status(thm)],[c_0_564,c_0_2084]),
[final] ).
cnf(c_0_2230,negated_conjecture,
( ~ hskp5
| hskp3
| hskp2
| epred39_0 ),
inference(spm,[status(thm)],[c_0_275,c_0_2084]),
[final] ).
cnf(c_0_2231,negated_conjecture,
( ~ hskp5
| hskp3
| hskp2
| epred21_0 ),
inference(spm,[status(thm)],[c_0_207,c_0_2084]),
[final] ).
cnf(c_0_2232,negated_conjecture,
( ~ hskp27
| hskp12
| c2_1(a1253)
| epred34_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_729]),c_0_730]),
[final] ).
cnf(c_0_2233,negated_conjecture,
( ~ hskp9
| hskp12
| c2_1(a1263)
| epred34_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1964,c_0_868]),c_0_830]),
[final] ).
cnf(c_0_2234,negated_conjecture,
( ~ hskp16
| hskp24
| epred28_0
| epred41_0 ),
inference(spm,[status(thm)],[c_0_2085,c_0_688]),
[final] ).
cnf(c_0_2235,negated_conjecture,
( ~ hskp2
| hskp24
| hskp23
| c3_1(a1255) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_636,c_0_367]),c_0_365]),
[final] ).
cnf(c_0_2236,negated_conjecture,
( ~ hskp16
| hskp13
| hskp12
| c2_1(a1274) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_394,c_0_197]),c_0_199]),
[final] ).
cnf(c_0_2237,negated_conjecture,
( ~ hskp9
| hskp13
| hskp12
| c2_1(a1263) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_394,c_0_830]),c_0_831]),
[final] ).
cnf(c_0_2238,negated_conjecture,
( ~ hskp16
| hskp11
| hskp0
| c2_1(a1274) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1876,c_0_197]),c_0_198]),
[final] ).
cnf(c_0_2239,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| hskp6
| c3_1(X1)
| c1_1(X1)
| epred45_0 ),
inference(spm,[status(thm)],[c_0_805,c_0_530]),
[final] ).
cnf(c_0_2240,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| hskp9
| hskp6
| c3_1(X1)
| epred28_0 ),
inference(spm,[status(thm)],[c_0_805,c_0_1830]),
[final] ).
cnf(c_0_2241,negated_conjecture,
( ~ c0_1(X1)
| hskp9
| hskp6
| c3_1(X1)
| c1_1(X1)
| epred9_0 ),
inference(spm,[status(thm)],[c_0_805,c_0_222]),
[final] ).
cnf(c_0_2242,negated_conjecture,
( ~ hskp18
| hskp3
| epred6_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_1276,c_0_1994]),
[final] ).
cnf(c_0_2243,negated_conjecture,
( ~ hskp2
| hskp8
| c3_1(a1255)
| epred14_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_651,c_0_367]),c_0_365]),
[final] ).
cnf(c_0_2244,negated_conjecture,
( ~ hskp13
| hskp16
| c3_1(a1268)
| epred10_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_527,c_0_392]),c_0_391]),
[final] ).
cnf(c_0_2245,negated_conjecture,
( ~ hskp16
| epred8_0
| epred28_0 ),
inference(spm,[status(thm)],[c_0_1875,c_0_220]),
[final] ).
cnf(c_0_2246,negated_conjecture,
( ~ hskp2
| hskp1
| c3_1(a1255)
| epred8_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_196,c_0_367]),c_0_365]),
[final] ).
cnf(c_0_2247,negated_conjecture,
( ~ c1_1(X1)
| hskp3
| c0_1(X1)
| c3_1(X1)
| epred6_0
| epred41_0 ),
inference(spm,[status(thm)],[c_0_791,c_0_1582]),
[final] ).
cnf(c_0_2248,negated_conjecture,
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred2_0
| epred41_0 ),
inference(spm,[status(thm)],[c_0_791,c_0_1146]),
[final] ).
cnf(c_0_2249,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1301)
| epred41_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_791,c_0_632]),c_0_629]),
[final] ).
cnf(c_0_2250,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| epred21_0
| epred28_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2024,c_0_1950]),
[final] ).
cnf(c_0_2251,negated_conjecture,
( ~ c0_1(X1)
| ~ c1_1(X1)
| epred4_0
| epred21_0
| epred35_0 ),
inference(spm,[status(thm)],[c_0_2024,c_0_1973]),
[final] ).
cnf(c_0_2252,negated_conjecture,
( ~ hskp13
| c3_1(a1268)
| epred28_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_391,c_0_1830]),c_0_392]),
[final] ).
cnf(c_0_2253,negated_conjecture,
( ~ hskp13
| hskp26
| c3_1(a1268)
| epred1_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1195,c_0_392]),c_0_391]),
[final] ).
cnf(c_0_2254,negated_conjecture,
( ~ hskp13
| c3_1(a1268)
| epred2_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_391,c_0_1146]),c_0_393]),
[final] ).
cnf(c_0_2255,negated_conjecture,
( ~ epred34_0
| ~ epred35_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_2086,c_0_1924]),c_0_1575]),
[final] ).
cnf(c_0_2256,negated_conjecture,
( ~ epred27_0
| ~ epred28_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_2088,c_0_2087]),c_0_1818]),
[final] ).
cnf(c_0_2257,negated_conjecture,
~ c0_1(a1270),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_206,c_0_1991])]),
[final] ).
cnf(c_0_2258,negated_conjecture,
~ c0_1(a1283),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2089,c_0_344]),c_0_1801]),c_0_2090]),
[final] ).
cnf(c_0_2259,negated_conjecture,
~ c2_1(a1277),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_231,c_0_2072])]),
[final] ).
cnf(c_0_2260,negated_conjecture,
~ c1_1(a1257),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_342,c_0_1993])]),
[final] ).
cnf(c_0_2261,negated_conjecture,
~ c0_1(a1264),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_218,c_0_2014])]),
[final] ).
cnf(c_0_2262,negated_conjecture,
~ c0_1(a1261),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_353,c_0_1879])]),
[final] ).
cnf(c_0_2263,negated_conjecture,
~ c2_1(a1261),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_352,c_0_1879])]),
[final] ).
cnf(c_0_2264,negated_conjecture,
~ epred16_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_333,c_0_1829])]),
[final] ).
cnf(c_0_2265,negated_conjecture,
c0_1(a1280),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_671,c_0_2070])]),
[final] ).
cnf(c_0_2266,negated_conjecture,
c2_1(a1280),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_668,c_0_2070])]),
[final] ).
cnf(c_0_2267,negated_conjecture,
c3_1(a1280),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_669,c_0_2070])]),
[final] ).
cnf(c_0_2268,negated_conjecture,
c2_1(a1259),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_330,c_0_2071])]),
[final] ).
cnf(c_0_2269,negated_conjecture,
c3_1(a1259),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_328,c_0_2071])]),
[final] ).
cnf(c_0_2270,negated_conjecture,
c1_1(a1259),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_329,c_0_2071])]),
[final] ).
cnf(c_0_2271,negated_conjecture,
c3_1(a1264),
inference(sr,[status(thm)],[c_0_2091,c_0_1813]),
[final] ).
cnf(c_0_2272,negated_conjecture,
c2_1(a1270),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_204,c_0_1991])]),
[final] ).
cnf(c_0_2273,negated_conjecture,
c3_1(a1270),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_205,c_0_1991])]),
[final] ).
cnf(c_0_2274,negated_conjecture,
c3_1(a1277),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_232,c_0_2072])]),
[final] ).
cnf(c_0_2275,negated_conjecture,
c1_1(a1277),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_233,c_0_2072])]),
[final] ).
cnf(c_0_2276,negated_conjecture,
c2_1(a1257),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_341,c_0_1993])]),
[final] ).
cnf(c_0_2277,negated_conjecture,
c3_1(a1257),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_343,c_0_1993])]),
[final] ).
cnf(c_0_2278,negated_conjecture,
c2_1(a1264),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_216,c_0_2014])]),
[final] ).
cnf(c_0_2279,negated_conjecture,
c1_1(a1264),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_217,c_0_2014])]),
[final] ).
cnf(c_0_2280,negated_conjecture,
c3_1(a1261),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_355,c_0_1879])]),
[final] ).
cnf(c_0_2281,negated_conjecture,
c1_1(a1261),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_546,c_0_1879])]),c_0_1802]),
[final] ).
cnf(c_0_2282,negated_conjecture,
c2_1(a1283),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_278,c_0_1946])]),
[final] ).
cnf(c_0_2283,negated_conjecture,
epred31_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1105,c_0_2092]),c_0_2093]),c_0_2094]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN463-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/5.41 % Computer : n026.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Mon Sep 21 11:02:27 UTC 2026
% 0.14/5.41 % CPUTime :
% 0.14/5.41 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/5.47 Running first-order theorem proving
% 0.14/5.47 Running: /export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p
% 80.25/17.33 % Version: 3.5.1
% 80.25/17.33 % Preprocessing class: FSLSSLSMSSSNFFN.
% 80.25/17.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 80.25/17.33 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 80.25/17.33 % Starting new_bool_3 with 300s (1) cores
% 80.25/17.33 % Starting new_bool_1 with 300s (1) cores
% 80.25/17.33 % Starting sh5l with 300s (1) cores
% 80.25/17.33 % G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with pid 2101637 completed with status 1
% 80.25/17.33 % Result found by G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1
% 80.25/17.33 % Preprocessing class: FSLSSLSMSSSNFFN.
% 80.25/17.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 80.25/17.33 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 80.25/17.33 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 80.25/17.33 % No SInE strategy applied
% 80.25/17.33 % Search class: FGHNF-FSMS00-SFFFFFNN
% 80.25/17.33 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 80.25/17.33 % Starting SubtermCWHack with 151s (1) cores
% 80.25/17.33 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 901s (1) cores
% 80.25/17.33 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with 151s (1) cores
% 80.25/17.33 % Starting new_bool_3 with 151s (1) cores
% 80.25/17.33 % Starting new_bool_1 with 146s (1) cores
% 80.25/17.33 % G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with pid 2101645 completed with status 1
% 80.25/17.33 % Result found by G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y
% 80.25/17.33 % Preprocessing class: FSLSSLSMSSSNFFN.
% 80.25/17.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 80.25/17.33 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 80.25/17.33 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 80.25/17.33 % No SInE strategy applied
% 80.25/17.33 % Search class: FGHNF-FSMS00-SFFFFFNN
% 80.25/17.33 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 80.25/17.33 % Starting SubtermCWHack with 151s (1) cores
% 80.25/17.33 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 901s (1) cores
% 80.25/17.33 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with 151s (1) cores
% 80.25/17.33 % Preprocessing time : 0.003 s
% 80.25/17.33
% 80.25/17.33 % No proof found!
% 80.25/17.33 % SZS status Satisfiable
% 80.25/17.33 % SZS output start Saturation
% See solution above
% 80.25/17.34 % Parsed axioms : 180
% 80.25/17.34 % Removed by relevancy pruning/SinE : 0
% 80.25/17.34 % Initial clauses : 180
% 80.25/17.34 % Removed in clause preprocessing : 0
% 80.25/17.34 % Initial clauses in saturation : 180
% 80.25/17.34 % Processed clauses : 36961
% 80.25/17.34 % ...of these trivial : 285
% 80.25/17.34 % ...subsumed : 20472
% 80.25/17.34 % ...remaining for further processing : 16204
% 80.25/17.34 % Other redundant clauses eliminated : 0
% 80.25/17.34 % Clauses deleted for lack of memory : 0
% 80.25/17.34 % Backward-subsumed : 12327
% 80.25/17.34 % Backward-rewritten : 2745
% 80.25/17.34 % Generated clauses : 462767
% 80.25/17.34 % ...of the previous two non-redundant : 438882
% 80.25/17.34 % ...aggressively subsumed : 0
% 80.25/17.34 % Contextual simplify-reflections : 3073
% 80.25/17.34 % Paramodulations : 462038
% 80.25/17.34 % Factorizations : 0
% 80.25/17.34 % NegExts : 0
% 80.25/17.34 % Equation resolutions : 0
% 80.25/17.34 % Disequality decompositions : 0
% 80.25/17.34 % Total rewrite steps : 3538
% 80.25/17.34 % ...of those cached : 3501
% 80.25/17.34 % Propositional unsat checks : 3
% 80.25/17.34 % Propositional check models : 3
% 80.25/17.34 % Propositional check unsatisfiable : 0
% 80.25/17.34 % Propositional clauses : 0
% 80.25/17.34 % Propositional clauses after purity: 0
% 80.25/17.34 % Propositional unsat core size : 0
% 80.25/17.34 % Propositional preprocessing time : 0.000
% 80.25/17.34 % Propositional encoding time : 0.268
% 80.25/17.34 % Propositional solver time : 0.777
% 80.25/17.34 % Success case prop preproc time : 0.000
% 80.25/17.34 % Success case prop encoding time : 0.000
% 80.25/17.34 % Success case prop solver time : 0.000
% 80.25/17.34 % Current number of processed clauses : 448
% 80.25/17.34 % Positive orientable unit clauses : 38
% 80.25/17.34 % Positive unorientable unit clauses: 0
% 80.25/17.34 % Negative unit clauses : 28
% 80.25/17.34 % Non-unit-clauses : 382
% 80.25/17.34 % Current number of unprocessed clauses: 0
% 80.25/17.34 % ...number of literals in the above : 0
% 80.25/17.34 % Current number of archived formulas : 0
% 80.25/17.34 % Current number of archived clauses : 15728
% 80.25/17.34 % Clause-clause subsumption calls (NU) : 22833459
% 80.25/17.34 % Rec. Clause-clause subsumption calls : 813224
% 80.25/17.34 % Non-unit clause-clause subsumptions : 35354
% 80.25/17.34 % Unit Clause-clause subsumption calls : 45945
% 80.25/17.34 % Rewrite failures with RHS unbound : 0
% 80.25/17.34 % BW rewrite match attempts : 23
% 80.25/17.34 % BW rewrite match successes : 23
% 80.25/17.34 % Condensation attempts : 36961
% 80.25/17.34 % Condensation successes : 0
% 80.25/17.34 % Termbank termtop insertions : 4497879
% 80.25/17.34 % Search garbage collected termcells : 426
% 80.25/17.34
% 80.25/17.34 % -------------------------------------------------
% 80.25/17.34 % User time : 11.312 s
% 80.25/17.34 % System time : 0.304 s
% 80.25/17.34 % Total time : 11.616 s
% 80.25/17.34 % Maximum resident set size: 4284 pages
% 80.25/17.34
% 80.25/17.34 % -------------------------------------------------
% 80.25/17.34 % User time : 55.347 s
% 80.25/17.34 % System time : 1.233 s
% 80.25/17.34 % Total time : 56.579 s
% 80.25/17.34 % Maximum resident set size: 4864 pages
% 80.25/17.34 % E exiting
%------------------------------------------------------------------------------