%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYN446-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 : n005.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:28 PM UTC 2026
% Result : Satisfiable 237.20s 30.93s
% Output : Saturation 237.20s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_159ERROR: Could not build tree for root c_0_207ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_163,negated_conjecture,
ndr1_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_156,c_0_157]),c_0_158]),
[final] ).
cnf(c_0_171,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1)
| epred39_0 ),
inference(split_equiv,[status(thm)],[c_0_159]),
[final] ).
cnf(c_0_174,negated_conjecture,
( ~ c1_1(X1)
| hskp29
| c0_1(X1)
| c3_1(X1)
| epred13_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_162]),c_0_163])]),
[final] ).
cnf(c_0_185,negated_conjecture,
( ~ hskp29
| c1_1(a390) ),
c_0_166,
[final] ).
cnf(c_0_186,negated_conjecture,
( ~ hskp29
| c0_1(a390) ),
c_0_167,
[final] ).
cnf(c_0_188,negated_conjecture,
( ~ hskp29
| c3_1(a390) ),
c_0_169,
[final] ).
cnf(c_0_197,negated_conjecture,
( ~ c2_1(X1)
| ~ c1_1(X1)
| hskp27
| hskp10
| c3_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_179,c_0_163])]),
[final] ).
cnf(c_0_207,negated_conjecture,
( ~ hskp29
| ~ c2_1(a390)
| epred39_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_171,c_0_185]),c_0_186]),
[final] ).
cnf(c_0_221,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| hskp6
| c3_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_198,c_0_163])]),
[final] ).
cnf(c_0_223,negated_conjecture,
( ~ hskp6
| c1_1(a381) ),
c_0_200,
[final] ).
cnf(c_0_224,negated_conjecture,
( ~ hskp6
| c2_1(a381) ),
c_0_201,
[final] ).
cnf(c_0_225,negated_conjecture,
( ~ hskp6
| ~ c0_1(a381) ),
c_0_202,
[final] ).
cnf(c_0_242,negated_conjecture,
( ~ hskp28
| c1_1(a386) ),
c_0_217,
[final] ).
cnf(c_0_243,negated_conjecture,
( ~ hskp28
| c2_1(a386) ),
c_0_218,
[final] ).
cnf(c_0_244,negated_conjecture,
( ~ hskp28
| c3_1(a386) ),
c_0_219,
[final] ).
cnf(c_0_263,negated_conjecture,
( ~ hskp10
| c1_1(a392) ),
c_0_232,
[final] ).
cnf(c_0_264,negated_conjecture,
( ~ hskp10
| c0_1(a392) ),
c_0_233,
[final] ).
cnf(c_0_265,negated_conjecture,
( ~ hskp10
| ~ c2_1(a392) ),
c_0_234,
[final] ).
cnf(c_0_275,negated_conjecture,
( ~ c2_1(X1)
| ~ c1_1(X1)
| hskp16
| c3_1(X1)
| epred30_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_239]),c_0_163])]),
[final] ).
cnf(c_0_302,negated_conjecture,
( ~ hskp9
| ~ c1_1(a387) ),
c_0_268,
[final] ).
cnf(c_0_303,negated_conjecture,
( ~ hskp9
| c2_1(a387) ),
c_0_269,
[final] ).
cnf(c_0_305,negated_conjecture,
( ~ hskp9
| c3_1(a387) ),
c_0_271,
[final] ).
cnf(c_0_371,negated_conjecture,
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred48_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_323]),c_0_163])]),
[final] ).
cnf(c_0_373,negated_conjecture,
( ~ hskp26
| ~ c3_1(a427) ),
c_0_324,
[final] ).
cnf(c_0_374,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred10_0 ),
inference(split_equiv,[status(thm)],[c_0_325]),
[final] ).
cnf(c_0_375,negated_conjecture,
( ~ hskp26
| ~ c0_1(a427) ),
c_0_326,
[final] ).
cnf(c_0_377,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| hskp26
| hskp22
| c3_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_328,c_0_163])]),
[final] ).
cnf(c_0_390,negated_conjecture,
( ~ hskp28
| ~ c0_1(a386)
| epred39_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_171,c_0_242]),c_0_243]),
[final] ).
cnf(c_0_424,negated_conjecture,
( ~ hskp25
| ~ c1_1(a425) ),
c_0_362,
[final] ).
cnf(c_0_425,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c1_1(X1)
| epred6_0 ),
inference(split_equiv,[status(thm)],[c_0_363]),
[final] ).
cnf(c_0_426,negated_conjecture,
( ~ hskp25
| ~ c0_1(a425) ),
c_0_364,
[final] ).
cnf(c_0_429,negated_conjecture,
( ~ hskp3
| c1_1(a378) ),
c_0_368,
[final] ).
cnf(c_0_430,negated_conjecture,
( ~ hskp3
| c3_1(a378) ),
c_0_369,
[final] ).
cnf(c_0_431,negated_conjecture,
( ~ hskp3
| ~ c0_1(a378) ),
c_0_370,
[final] ).
cnf(c_0_436,negated_conjecture,
( ~ hskp6
| c3_1(a381)
| epred48_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_371,c_0_223]),c_0_225]),
[final] ).
cnf(c_0_437,negated_conjecture,
( ~ c2_1(X1)
| hskp14
| c3_1(X1)
| c1_1(X1)
| epred18_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_372]),c_0_163])]),
[final] ).
cnf(c_0_444,negated_conjecture,
( ~ c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| epred26_0 ),
inference(split_equiv,[status(thm)],[c_0_381]),
[final] ).
cnf(c_0_466,negated_conjecture,
( ~ hskp25
| c3_1(a425) ),
c_0_411,
[final] ).
cnf(c_0_468,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred42_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_413]),c_0_163])]),
[final] ).
cnf(c_0_470,negated_conjecture,
( ~ hskp2
| c1_1(a377) ),
c_0_415,
[final] ).
cnf(c_0_471,negated_conjecture,
( ~ hskp2
| ~ c2_1(a377) ),
c_0_416,
[final] ).
cnf(c_0_472,negated_conjecture,
( ~ hskp2
| ~ c3_1(a377) ),
c_0_417,
[final] ).
cnf(c_0_476,negated_conjecture,
( ~ hskp7
| ~ c0_1(a384) ),
c_0_421,
[final] ).
cnf(c_0_477,negated_conjecture,
( ~ hskp7
| ~ c2_1(a384) ),
c_0_422,
[final] ).
cnf(c_0_481,negated_conjecture,
( ~ hskp25
| ~ c2_1(a425)
| epred6_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_424,c_0_425]),c_0_426]),
[final] ).
cnf(c_0_486,negated_conjecture,
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1)
| epred46_0 ),
inference(split_equiv,[status(thm)],[c_0_433]),
[final] ).
cnf(c_0_490,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred19_0 ),
inference(split_equiv,[status(thm)],[c_0_438]),
[final] ).
cnf(c_0_510,negated_conjecture,
( ~ hskp25
| epred26_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_424,c_0_444]),c_0_466]),c_0_426]),
[final] ).
cnf(c_0_524,negated_conjecture,
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| epred29_0 ),
inference(split_equiv,[status(thm)],[c_0_478]),
[final] ).
cnf(c_0_621,negated_conjecture,
( ~ hskp13
| c1_1(a396) ),
c_0_563,
[final] ).
cnf(c_0_622,negated_conjecture,
( ~ hskp13
| ~ c0_1(a396) ),
c_0_564,
[final] ).
cnf(c_0_623,negated_conjecture,
( ~ hskp13
| ~ c3_1(a396) ),
c_0_565,
[final] ).
cnf(c_0_649,negated_conjecture,
( ~ epred18_0
| ~ epred19_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_591,c_0_372]),c_0_438]),
[final] ).
cnf(c_0_659,negated_conjecture,
( ~ c3_1(X1)
| hskp6
| c0_1(X1)
| c1_1(X1)
| epred3_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_603]),c_0_163])]),
[final] ).
cnf(c_0_664,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| epred4_0 ),
inference(split_equiv,[status(thm)],[c_0_607]),
[final] ).
cnf(c_0_677,negated_conjecture,
( ~ hskp13
| epred48_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_371,c_0_621]),c_0_622]),c_0_623]),
[final] ).
cnf(c_0_768,negated_conjecture,
( ~ hskp2
| hskp29
| c0_1(a377)
| epred13_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_174,c_0_470]),c_0_472]),
[final] ).
cnf(c_0_772,negated_conjecture,
( ~ hskp28
| ~ c0_1(a386)
| epred29_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_524,c_0_242]),c_0_244]),
[final] ).
cnf(c_0_782,negated_conjecture,
( ~ c2_1(X1)
| hskp10
| c0_1(X1)
| c3_1(X1)
| epred22_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_742]),c_0_163])]),
[final] ).
cnf(c_0_805,negated_conjecture,
( ~ hskp29
| epred29_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_524,c_0_185]),c_0_186]),c_0_188]),
[final] ).
cnf(c_0_817,negated_conjecture,
( ~ epred3_0
| ~ epred4_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(csr,[status(thm)],[c_0_783,c_0_198]),c_0_603]),c_0_607]),
[final] ).
cnf(c_0_824,negated_conjecture,
epred45_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_730,c_0_790]),c_0_791]),c_0_792]),
[final] ).
cnf(c_0_844,negated_conjecture,
( ~ c2_1(X1)
| hskp27
| hskp10
| c3_1(X1)
| epred42_0 ),
inference(spm,[status(thm)],[c_0_197,c_0_468]),
[final] ).
cnf(c_0_851,negated_conjecture,
epred44_0,
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_823,c_0_824])]),c_0_825]),
[final] ).
cnf(c_0_874,negated_conjecture,
( ~ epred19_0
| ~ epred24_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_846,c_0_845]),c_0_438]),
[final] ).
cnf(c_0_876,negated_conjecture,
( ~ epred24_0
| ~ epred26_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_849,c_0_845]),c_0_381]),
[final] ).
cnf(c_0_936,negated_conjecture,
( ~ hskp26
| ~ c1_1(a427) ),
c_0_917,
[final] ).
cnf(c_0_956,negated_conjecture,
( ~ hskp10
| ~ c3_1(a392)
| epred29_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_524,c_0_263]),c_0_264]),
[final] ).
cnf(c_0_962,negated_conjecture,
( ~ hskp2
| c0_1(a377)
| epred48_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_371,c_0_470]),c_0_472]),
[final] ).
cnf(c_0_1004,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred39_0
| epred46_0 ),
inference(spm,[status(thm)],[c_0_171,c_0_486]),
[final] ).
cnf(c_0_1019,negated_conjecture,
( ~ hskp18
| c1_1(a404) ),
c_0_987,
[final] ).
cnf(c_0_1020,negated_conjecture,
( ~ hskp18
| c3_1(a404) ),
c_0_988,
[final] ).
cnf(c_0_1021,negated_conjecture,
( ~ hskp18
| ~ c2_1(a404) ),
c_0_989,
[final] ).
cnf(c_0_1047,negated_conjecture,
( ~ epred10_0
| ~ epred46_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_724,c_0_824])]),
[final] ).
cnf(c_0_1088,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| hskp25
| hskp24
| c3_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1062,c_0_163])]),
[final] ).
cnf(c_0_1104,negated_conjecture,
( ~ hskp9
| c0_1(a387)
| epred6_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_302,c_0_425]),c_0_303]),
[final] ).
cnf(c_0_1199,negated_conjecture,
( ~ c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| epred49_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1175]),c_0_163])]),
[final] ).
cnf(c_0_1201,negated_conjecture,
epred50_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1177,c_0_1178]),c_0_1117]),
[final] ).
cnf(c_0_1248,negated_conjecture,
( ~ hskp7
| c3_1(a384) ),
c_0_1228,
[final] ).
cnf(c_0_1251,negated_conjecture,
( ~ c0_1(X1)
| hskp3
| c2_1(X1)
| c1_1(X1)
| epred9_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1229]),c_0_163])]),
[final] ).
cnf(c_0_1307,negated_conjecture,
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred25_0 ),
inference(split_equiv,[status(thm)],[c_0_1283]),
[final] ).
cnf(c_0_1318,negated_conjecture,
( ~ epred9_0
| ~ epred10_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1292,c_0_1229]),c_0_325]),
[final] ).
cnf(c_0_1340,negated_conjecture,
( ~ hskp9
| c0_1(a387)
| epred26_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_302,c_0_444]),c_0_305]),
[final] ).
cnf(c_0_1366,negated_conjecture,
( ~ hskp25
| hskp6
| epred3_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_659,c_0_466]),c_0_426]),c_0_424]),
[final] ).
cnf(c_0_1374,negated_conjecture,
( ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| epred51_0 ),
inference(split_equiv,[status(thm)],[c_0_1343]),
[final] ).
cnf(c_0_1375,negated_conjecture,
( ~ hskp13
| hskp29
| epred13_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_174,c_0_621]),c_0_622]),c_0_623]),
[final] ).
cnf(c_0_1377,negated_conjecture,
epred41_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1346,c_0_1347]),c_0_1348]),
[final] ).
cnf(c_0_1406,negated_conjecture,
epred31_0,
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1376,c_0_1377])]),c_0_1378]),
[final] ).
cnf(c_0_1410,negated_conjecture,
( ~ epred24_0
| ~ epred25_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1382,c_0_845]),c_0_1283]),
[final] ).
cnf(c_0_1425,negated_conjecture,
( ~ hskp25
| epred49_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_424,c_0_1199]),c_0_466]),c_0_426]),
[final] ).
cnf(c_0_1436,negated_conjecture,
~ epred30_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_394,c_0_1406])]),
[final] ).
cnf(c_0_1486,negated_conjecture,
( ~ hskp9
| c0_1(a387)
| epred49_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_302,c_0_1199]),c_0_305]),
[final] ).
cnf(c_0_1529,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| epred42_0
| epred51_0 ),
inference(spm,[status(thm)],[c_0_1374,c_0_468]),
[final] ).
cnf(c_0_1551,negated_conjecture,
epred52_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1537,c_0_1538]),c_0_1483]),
[final] ).
cnf(c_0_1563,negated_conjecture,
~ epred51_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1550,c_0_1551])]),
[final] ).
cnf(c_0_1564,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred6_0
| epred51_0 ),
inference(spm,[status(thm)],[c_0_1374,c_0_425]),
[final] ).
cnf(c_0_1574,negated_conjecture,
epred43_0,
inference(sr,[status(thm)],[c_0_1562,c_0_1563]),
[final] ).
cnf(c_0_1583,negated_conjecture,
hskp8,
inference(sr,[status(thm)],[c_0_1559,c_0_1563]),
[final] ).
cnf(c_0_1585,negated_conjecture,
~ epred42_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1573,c_0_1574])]),
[final] ).
cnf(c_0_1594,negated_conjecture,
( ~ c0_1(X1)
| hskp20
| c3_1(X1)
| c1_1(X1)
| epred15_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1582]),c_0_163])]),
[final] ).
cnf(c_0_1597,negated_conjecture,
c0_1(a385),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_210,c_0_1583])]),
[final] ).
cnf(c_0_1598,negated_conjecture,
c2_1(a385),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_211,c_0_1583])]),
[final] ).
cnf(c_0_1599,negated_conjecture,
epred33_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1584,c_0_1563]),c_0_1585]),
[final] ).
cnf(c_0_1607,negated_conjecture,
~ epred49_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1221,c_0_1599])]),
[final] ).
cnf(c_0_1608,negated_conjecture,
~ epred37_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_671,c_0_1599])]),
[final] ).
cnf(c_0_1610,negated_conjecture,
epred14_0,
inference(sr,[status(thm)],[c_0_1601,c_0_1563]),
[final] ).
cnf(c_0_1612,negated_conjecture,
epred38_0,
inference(sr,[status(thm)],[c_0_1603,c_0_1563]),
[final] ).
cnf(c_0_1616,negated_conjecture,
~ epred15_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1609,c_0_1610])]),
[final] ).
cnf(c_0_1618,negated_conjecture,
~ epred39_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_756,c_0_1612])]),
[final] ).
cnf(c_0_1621,negated_conjecture,
hskp30,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1614,c_0_1615]),c_0_1585]),c_0_1616]),
[final] ).
cnf(c_0_1622,negated_conjecture,
~ epred48_0,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1608,c_0_1617]),c_0_1618]),
[final] ).
cnf(c_0_1627,negated_conjecture,
~ epred36_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_896,c_0_1610])]),
[final] ).
cnf(c_0_1637,negated_conjecture,
hskp5,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1614,c_0_1632]),c_0_1585]),c_0_1616]),
[final] ).
cnf(c_0_1638,negated_conjecture,
( ~ hskp6
| c3_1(a381)
| epred51_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1374,c_0_223]),c_0_224]),
[final] ).
cnf(c_0_1645,negated_conjecture,
epred12_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1636,c_0_1637])]),c_0_1607]),c_0_1585]),
[final] ).
cnf(c_0_1654,negated_conjecture,
( ~ c2_1(X1)
| hskp16
| c0_1(X1)
| c3_1(X1)
| epred6_0
| epred30_0 ),
inference(spm,[status(thm)],[c_0_275,c_0_425]),
[final] ).
cnf(c_0_1655,negated_conjecture,
~ epred6_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_882,c_0_1645])]),
[final] ).
cnf(c_0_1679,negated_conjecture,
epred35_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_726,c_0_1667]),c_0_1254]),
[final] ).
cnf(c_0_1694,negated_conjecture,
~ epred34_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_388,c_0_1679])]),
[final] ).
cnf(c_0_1702,negated_conjecture,
~ hskp24,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1683,c_0_1684]),c_0_1563]),c_0_1585]),
[final] ).
cnf(c_0_1723,negated_conjecture,
epred17_0,
inference(sr,[status(thm)],[c_0_1704,c_0_1563]),
[final] ).
cnf(c_0_1726,negated_conjecture,
hskp0,
inference(sr,[status(thm)],[c_0_1705,c_0_1655]),
[final] ).
cnf(c_0_1740,negated_conjecture,
( ~ c2_1(X1)
| hskp16
| c3_1(X1)
| epred30_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_275,c_0_468]),
[final] ).
cnf(c_0_1743,negated_conjecture,
~ epred16_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1275,c_0_1723])]),
[final] ).
cnf(c_0_1746,negated_conjecture,
c3_1(a375),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1204,c_0_1726])]),c_0_1622]),
[final] ).
cnf(c_0_1747,negated_conjecture,
~ c2_1(a375),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_320,c_0_1726])]),
[final] ).
cnf(c_0_1748,negated_conjecture,
~ c0_1(a375),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_319,c_0_1726])]),
[final] ).
cnf(c_0_1759,negated_conjecture,
~ epred27_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1012,c_0_1610])]),
[final] ).
cnf(c_0_1761,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred39_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_171,c_0_468]),
[final] ).
cnf(c_0_1763,negated_conjecture,
epred28_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1553,c_0_1637])]),c_0_1563]),c_0_1585]),
[final] ).
cnf(c_0_1768,negated_conjecture,
hskp19,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1742,c_0_1563]),c_0_1743]),
[final] ).
cnf(c_0_1770,negated_conjecture,
epred8_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1745,c_0_1746]),c_0_1747]),c_0_1748]),
[final] ).
cnf(c_0_1772,negated_conjecture,
epred21_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1751,c_0_1752]),c_0_1729]),c_0_1753]),
[final] ).
cnf(c_0_1779,negated_conjecture,
~ hskp16,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1003,c_0_1761]),c_0_1585]),c_0_1618]),c_0_273]),c_0_274]),
[final] ).
cnf(c_0_1781,negated_conjecture,
~ epred29_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_726,c_0_1763])]),
[final] ).
cnf(c_0_1782,negated_conjecture,
~ hskp14,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1425,c_0_1764]),c_0_1607]),
[final] ).
cnf(c_0_1786,negated_conjecture,
~ epred40_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_646,c_0_1599])]),
[final] ).
cnf(c_0_1789,negated_conjecture,
~ epred7_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1769,c_0_1770])]),
[final] ).
cnf(c_0_1792,negated_conjecture,
c3_1(a385),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_514,c_0_1583])]),c_0_1585]),
[final] ).
cnf(c_0_1793,negated_conjecture,
~ epred20_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1771,c_0_1772])]),
[final] ).
cnf(c_0_1794,negated_conjecture,
~ c1_1(a385),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_235,c_0_1583])]),
[final] ).
cnf(c_0_1798,negated_conjecture,
hskp1,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1614,c_0_1776]),c_0_1585]),c_0_1616]),
[final] ).
cnf(c_0_1801,negated_conjecture,
hskp12,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1170,c_0_1768])]),c_0_1694]),
[final] ).
cnf(c_0_1804,negated_conjecture,
~ epred32_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_508,c_0_1599])]),
[final] ).
cnf(c_0_1805,negated_conjecture,
( ~ c2_1(X1)
| hskp27
| hskp10
| c0_1(X1)
| c3_1(X1)
| epred6_0 ),
inference(spm,[status(thm)],[c_0_197,c_0_425]),
[final] ).
cnf(c_0_1806,negated_conjecture,
~ hskp27,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1779,c_0_1780]),c_0_1436]),c_0_1781]),
[final] ).
cnf(c_0_1807,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred6_0
| epred48_0 ),
inference(spm,[status(thm)],[c_0_371,c_0_425]),
[final] ).
cnf(c_0_1808,negated_conjecture,
hskp21,
inference(sr,[status(thm)],[c_0_1606,c_0_1782]),
[final] ).
cnf(c_0_1809,negated_conjecture,
~ hskp22,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_773,c_0_1783]),c_0_1585]),
[final] ).
cnf(c_0_1810,negated_conjecture,
hskp23,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1784,c_0_1785]),c_0_1563]),c_0_1786]),
[final] ).
cnf(c_0_1811,negated_conjecture,
( ~ c2_1(X1)
| hskp29
| c0_1(X1)
| c3_1(X1)
| epred6_0
| epred13_0 ),
inference(spm,[status(thm)],[c_0_174,c_0_425]),
[final] ).
cnf(c_0_1812,negated_conjecture,
~ epred13_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_298,c_0_1610])]),
[final] ).
cnf(c_0_1814,negated_conjecture,
hskp4,
inference(sr,[status(thm)],[c_0_1788,c_0_1789]),
[final] ).
cnf(c_0_1816,negated_conjecture,
hskp15,
inference(sr,[status(thm)],[c_0_1790,c_0_1782]),
[final] ).
cnf(c_0_1818,negated_conjecture,
hskp11,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1791,c_0_1792]),c_0_1597])]),c_0_1793]),c_0_1794]),
[final] ).
cnf(c_0_1819,negated_conjecture,
epred2_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1795,c_0_1563]),c_0_1607]),
[final] ).
cnf(c_0_1820,negated_conjecture,
epred23_0,
inference(sr,[status(thm)],[c_0_1796,c_0_1563]),
[final] ).
cnf(c_0_1822,negated_conjecture,
~ hskp20,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1799,c_0_735]),c_0_1655]),
[final] ).
cnf(c_0_1826,negated_conjecture,
( ~ hskp6
| hskp10
| c3_1(a381) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1805,c_0_224]),c_0_1655]),c_0_1806]),c_0_225]),
[final] ).
cnf(c_0_1827,negated_conjecture,
( ~ c2_1(X1)
| hskp6
| c0_1(X1)
| c1_1(X1)
| epred3_0 ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_659,c_0_1807]),c_0_1622]),c_0_1655]),
[final] ).
cnf(c_0_1828,negated_conjecture,
( ~ hskp13
| ~ c2_1(a396) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_623,c_0_1807]),c_0_1622]),c_0_1655]),c_0_622]),
[final] ).
cnf(c_0_1829,negated_conjecture,
( ~ hskp26
| ~ c2_1(a427) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_373,c_0_1807]),c_0_1622]),c_0_1655]),c_0_375]),
[final] ).
cnf(c_0_1830,negated_conjecture,
( hskp6
| c1_1(a411)
| epred3_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_706,c_0_1808])]),
[final] ).
cnf(c_0_1831,negated_conjecture,
( ~ hskp6
| hskp16
| c3_1(a381) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1654,c_0_224]),c_0_1436]),c_0_1655]),c_0_225]),
[final] ).
cnf(c_0_1832,negated_conjecture,
( hskp29
| hskp10 ),
inference(sr,[status(thm)],[c_0_703,c_0_1809]),
[final] ).
cnf(c_0_1833,negated_conjecture,
( ~ c0_1(a420)
| epred46_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_539,c_0_1810])]),
[final] ).
cnf(c_0_1834,negated_conjecture,
( ~ hskp6
| hskp29
| c3_1(a381) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1811,c_0_224]),c_0_1812]),c_0_1655]),c_0_225]),
[final] ).
cnf(c_0_1835,negated_conjecture,
( hskp28
| hskp9 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_393,c_0_1726])]),
[final] ).
cnf(c_0_1836,negated_conjecture,
( hskp3
| epred9_0 ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1813,c_0_1768])]),c_0_1694]),
[final] ).
cnf(c_0_1837,negated_conjecture,
( ~ epred10_0
| ~ epred26_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_686,c_0_1377])]),
[final] ).
cnf(c_0_1838,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| hskp27
| hskp10
| c3_1(X1)
| epred46_0 ),
inference(spm,[status(thm)],[c_0_197,c_0_486]),
[final] ).
cnf(c_0_1839,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred42_0
| epred48_0 ),
inference(spm,[status(thm)],[c_0_371,c_0_468]),
[final] ).
cnf(c_0_1840,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred25_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_1307,c_0_468]),
[final] ).
cnf(c_0_1841,negated_conjecture,
( ~ c2_1(X1)
| hskp29
| c0_1(X1)
| c3_1(X1)
| epred13_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_174,c_0_468]),
[final] ).
cnf(c_0_1842,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| hskp16
| c3_1(X1)
| epred30_0
| epred46_0 ),
inference(spm,[status(thm)],[c_0_275,c_0_486]),
[final] ).
cnf(c_0_1843,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred46_0
| epred51_0 ),
inference(spm,[status(thm)],[c_0_1374,c_0_486]),
[final] ).
cnf(c_0_1844,negated_conjecture,
( ~ hskp18
| ~ c0_1(a404)
| epred29_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_524,c_0_1019]),c_0_1020]),
[final] ).
cnf(c_0_1845,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred6_0
| epred25_0 ),
inference(spm,[status(thm)],[c_0_1307,c_0_425]),
[final] ).
cnf(c_0_1846,negated_conjecture,
( ~ hskp13
| epred25_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1307,c_0_621]),c_0_622]),c_0_623]),
[final] ).
cnf(c_0_1847,negated_conjecture,
( ~ hskp6
| c3_1(a381)
| epred25_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1307,c_0_223]),c_0_225]),
[final] ).
cnf(c_0_1848,negated_conjecture,
( ~ hskp2
| c0_1(a377)
| epred25_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1307,c_0_470]),c_0_472]),
[final] ).
cnf(c_0_1849,negated_conjecture,
( ~ hskp9
| hskp6
| c0_1(a387)
| epred3_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_659,c_0_305]),c_0_302]),
[final] ).
cnf(c_0_1850,negated_conjecture,
( ~ hskp7
| hskp6
| c1_1(a384)
| epred3_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_659,c_0_1248]),c_0_476]),
[final] ).
cnf(c_0_1851,negated_conjecture,
~ c0_1(a379),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_397,c_0_1814])]),
[final] ).
cnf(c_0_1852,negated_conjecture,
~ c2_1(a379),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_398,c_0_1814])]),
[final] ).
cnf(c_0_1853,negated_conjecture,
~ c1_1(a379),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_396,c_0_1814])]),
[final] ).
cnf(c_0_1854,negated_conjecture,
~ c3_1(a379),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1815,c_0_1814])]),c_0_1607]),
[final] ).
cnf(c_0_1855,negated_conjecture,
~ c0_1(a399),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_281,c_0_1816])]),
[final] ).
cnf(c_0_1856,negated_conjecture,
~ c2_1(a399),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_282,c_0_1816])]),
[final] ).
cnf(c_0_1857,negated_conjecture,
~ c3_1(a399),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_279,c_0_1816])]),
[final] ).
cnf(c_0_1858,negated_conjecture,
~ c0_1(a411),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_661,c_0_1808])]),
[final] ).
cnf(c_0_1859,negated_conjecture,
~ hskp17,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_773,c_0_1817]),c_0_1585]),
[final] ).
cnf(c_0_1860,negated_conjecture,
~ c2_1(a394),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_906,c_0_1818])]),
[final] ).
cnf(c_0_1861,negated_conjecture,
~ c1_1(a394),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_907,c_0_1818])]),
[final] ).
cnf(c_0_1862,negated_conjecture,
~ c3_1(a380),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_475,c_0_1637])]),
[final] ).
cnf(c_0_1863,negated_conjecture,
~ c2_1(a380),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1402,c_0_1637])]),c_0_1563]),
[final] ).
cnf(c_0_1864,negated_conjecture,
~ epred11_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1079,c_0_1645])]),
[final] ).
cnf(c_0_1865,negated_conjecture,
~ c2_1(a376),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_602,c_0_1798])]),
[final] ).
cnf(c_0_1866,negated_conjecture,
~ c3_1(a376),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_600,c_0_1798])]),
[final] ).
cnf(c_0_1867,negated_conjecture,
~ c2_1(a420),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_357,c_0_1810])]),
[final] ).
cnf(c_0_1868,negated_conjecture,
~ c3_1(a420),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_358,c_0_1810])]),
[final] ).
cnf(c_0_1869,negated_conjecture,
~ c1_1(a420),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_356,c_0_1810])]),
[final] ).
cnf(c_0_1870,negated_conjecture,
~ c2_1(a395),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_206,c_0_1801])]),
[final] ).
cnf(c_0_1871,negated_conjecture,
~ c1_1(a395),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_203,c_0_1801])]),
[final] ).
cnf(c_0_1872,negated_conjecture,
~ c2_1(a407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_993,c_0_1768])]),
[final] ).
cnf(c_0_1873,negated_conjecture,
~ epred1_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_609,c_0_1819])]),
[final] ).
cnf(c_0_1874,negated_conjecture,
~ epred22_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_919,c_0_1820])]),
[final] ).
cnf(c_0_1875,negated_conjecture,
c1_1(a376),
inference(sr,[status(thm)],[c_0_1821,c_0_1822]),
[final] ).
cnf(c_0_1876,negated_conjecture,
c3_1(a395),
inference(sr,[status(thm)],[c_0_1823,c_0_1822]),
[final] ).
cnf(c_0_1877,negated_conjecture,
c2_1(a411),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_707,c_0_1808])]),
[final] ).
cnf(c_0_1878,negated_conjecture,
c3_1(a411),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_660,c_0_1808])]),
[final] ).
cnf(c_0_1879,negated_conjecture,
c3_1(a394),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_905,c_0_1818])]),
[final] ).
cnf(c_0_1880,negated_conjecture,
c0_1(a394),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1220,c_0_1818])]),c_0_1607]),
[final] ).
cnf(c_0_1881,negated_conjecture,
c1_1(a375),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_318,c_0_1726])]),
[final] ).
cnf(c_0_1882,negated_conjecture,
c0_1(a380),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_474,c_0_1637])]),
[final] ).
cnf(c_0_1883,negated_conjecture,
c1_1(a380),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_473,c_0_1637])]),
[final] ).
cnf(c_0_1884,negated_conjecture,
c0_1(a376),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_601,c_0_1798])]),
[final] ).
cnf(c_0_1885,negated_conjecture,
c0_1(a397),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_399,c_0_1621])]),
[final] ).
cnf(c_0_1886,negated_conjecture,
c2_1(a397),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_400,c_0_1621])]),
[final] ).
cnf(c_0_1887,negated_conjecture,
c3_1(a397),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_403,c_0_1621])]),
[final] ).
cnf(c_0_1888,negated_conjecture,
epred47_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1824,c_0_1825]),c_0_1622]),c_0_1618]),
[final] ).
cnf(c_0_1889,negated_conjecture,
c0_1(a395),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_205,c_0_1801])]),
[final] ).
cnf(c_0_1890,negated_conjecture,
c0_1(a407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_578,c_0_1768])]),
[final] ).
cnf(c_0_1891,negated_conjecture,
c3_1(a407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_577,c_0_1768])]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN446-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.47 % Computer : n005.cluster.edu
% 0.17/0.47 % Model : x86_64 x86_64
% 0.17/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.47 % Memory : 8046.5625MB
% 0.17/0.47 % OS : Linux 6.8.0-71-generic
% 0.17/0.47 % CPULimit : 300
% 0.17/0.47 % WCLimit : 300
% 0.17/0.47 % DateTime : Mon Sep 21 10:57:03 UTC 2026
% 0.17/0.48 % CPUTime :
% 0.17/0.48 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.22/0.55 Running first-order theorem proving
% 0.22/0.55 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
% 237.20/30.93 % Version: 3.5.1
% 237.20/30.93 % Preprocessing class: FSLSSLSMSSSNFFN.
% 237.20/30.93 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 237.20/30.93 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 237.20/30.93 % Starting new_bool_3 with 300s (1) cores
% 237.20/30.93 % Starting new_bool_1 with 300s (1) cores
% 237.20/30.93 % Starting sh5l with 300s (1) cores
% 237.20/30.93 % G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with pid 3294196 completed with status 1
% 237.20/30.93 % Result found by G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1
% 237.20/30.93 % Preprocessing class: FSLSSLSMSSSNFFN.
% 237.20/30.93 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 237.20/30.93 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 237.20/30.93 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 237.20/30.93 % No SInE strategy applied
% 237.20/30.93 % Search class: FGHNF-FSMM00-SFFFFFNN
% 237.20/30.93 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 237.20/30.93 % Starting SubtermCWHack with 151s (1) cores
% 237.20/30.93 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 901s (1) cores
% 237.20/30.93 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with 151s (1) cores
% 237.20/30.93 % Starting H----_042_B03_F1_AE_Q4_SP_S2S with 151s (1) cores
% 237.20/30.93 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S2g with 146s (1) cores
% 237.20/30.93 % G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with pid 3294203 completed with status 1
% 237.20/30.93 % Result found by G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y
% 237.20/30.93 % Preprocessing class: FSLSSLSMSSSNFFN.
% 237.20/30.93 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 237.20/30.93 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 237.20/30.93 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 237.20/30.93 % No SInE strategy applied
% 237.20/30.93 % Search class: FGHNF-FSMM00-SFFFFFNN
% 237.20/30.93 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 237.20/30.93 % Starting SubtermCWHack with 151s (1) cores
% 237.20/30.93 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 901s (1) cores
% 237.20/30.93 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with 151s (1) cores
% 237.20/30.93 % Preprocessing time : 0.003 s
% 237.20/30.93
% 237.20/30.93 % No proof found!
% 237.20/30.93 % SZS status Satisfiable
% 237.20/30.93 % SZS output start Saturation
% See solution above
% 237.20/30.93 % Parsed axioms : 184
% 237.20/30.93 % Removed by relevancy pruning/SinE : 0
% 237.20/30.93 % Initial clauses : 184
% 237.20/30.93 % Removed in clause preprocessing : 0
% 237.20/30.93 % Initial clauses in saturation : 184
% 237.20/30.93 % Processed clauses : 47904
% 237.20/30.93 % ...of these trivial : 585
% 237.20/30.93 % ...subsumed : 28165
% 237.20/30.93 % ...remaining for further processing : 19154
% 237.20/30.93 % Other redundant clauses eliminated : 0
% 237.20/30.93 % Clauses deleted for lack of memory : 0
% 237.20/30.93 % Backward-subsumed : 13621
% 237.20/30.93 % Backward-rewritten : 4747
% 237.20/30.93 % Generated clauses : 671686
% 237.20/30.93 % ...of the previous two non-redundant : 653539
% 237.20/30.93 % ...aggressively subsumed : 0
% 237.20/30.93 % Contextual simplify-reflections : 3262
% 237.20/30.93 % Paramodulations : 671072
% 237.20/30.93 % Factorizations : 0
% 237.20/30.93 % NegExts : 0
% 237.20/30.93 % Equation resolutions : 0
% 237.20/30.93 % Disequality decompositions : 0
% 237.20/30.93 % Total rewrite steps : 5756
% 237.20/30.93 % ...of those cached : 5705
% 237.20/30.93 % Propositional unsat checks : 3
% 237.20/30.93 % Propositional check models : 3
% 237.20/30.93 % Propositional check unsatisfiable : 0
% 237.20/30.93 % Propositional clauses : 0
% 237.20/30.93 % Propositional clauses after purity: 0
% 237.20/30.93 % Propositional unsat core size : 0
% 237.20/30.93 % Propositional preprocessing time : 0.000
% 237.20/30.93 % Propositional encoding time : 0.373
% 237.20/30.93 % Propositional solver time : 1.311
% 237.20/30.93 % Success case prop preproc time : 0.000
% 237.20/30.93 % Success case prop encoding time : 0.000
% 237.20/30.93 % Success case prop solver time : 0.000
% 237.20/30.93 % Current number of processed clauses : 224
% 237.20/30.93 % Positive orientable unit clauses : 52
% 237.20/30.93 % Positive unorientable unit clauses: 0
% 237.20/30.93 % Negative unit clauses : 52
% 237.20/30.93 % Non-unit-clauses : 120
% 237.20/30.93 % Current number of unprocessed clauses: 0
% 237.20/30.93 % ...number of literals in the above : 0
% 237.20/30.93 % Current number of archived formulas : 0
% 237.20/30.93 % Current number of archived clauses : 18898
% 237.20/30.93 % Clause-clause subsumption calls (NU) : 64240316
% 237.20/30.93 % Rec. Clause-clause subsumption calls : 1663993
% 237.20/30.93 % Non-unit clause-clause subsumptions : 44289
% 237.20/30.93 % Unit Clause-clause subsumption calls : 79314
% 237.20/30.93 % Rewrite failures with RHS unbound : 0
% 237.20/30.93 % BW rewrite match attempts : 33
% 237.20/30.93 % BW rewrite match successes : 33
% 237.20/30.93 % Condensation attempts : 47904
% 237.20/30.93 % Condensation successes : 0
% 237.20/30.93 % Termbank termtop insertions : 6067602
% 237.20/30.93 % Search garbage collected termcells : 459
% 237.20/30.93
% 237.20/30.93 % -------------------------------------------------
% 237.20/30.93 % User time : 29.190 s
% 237.20/30.93 % System time : 0.665 s
% 237.20/30.93 % Total time : 29.855 s
% 237.20/30.93 % Maximum resident set size: 4236 pages
% 237.20/30.93
% 237.20/30.93 % -------------------------------------------------
% 237.20/30.93 % User time : 145.391 s
% 237.20/30.93 % System time : 2.958 s
% 237.20/30.93 % Total time : 148.349 s
% 237.20/30.93 % Maximum resident set size: 4864 pages
% 237.20/30.93 % E exiting
%------------------------------------------------------------------------------