%------------------------------------------------------------------------------
% 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 : n013.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 : CounterSatisfiable 70.04s 15.58s
% Output : Saturation 70.04s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_7ERROR: Could not build tree for root c_0_11ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_8,negated_conjecture,
ndr1_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_4,c_0_5]),c_0_6]),
[final] ).
cnf(c_0_11,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp6 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_7,c_0_8])]),
[final] ).
cnf(c_0_14,negated_conjecture,
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred47_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_9]),c_0_8])]),
[final] ).
cnf(c_0_28,negated_conjecture,
( ~ hskp6
| c1_1(a381) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_29,negated_conjecture,
( ~ hskp6
| c2_1(a381) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_30,negated_conjecture,
( ~ hskp6
| ~ c0_1(a381) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_36,negated_conjecture,
( ~ hskp13
| c1_1(a396) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_37,negated_conjecture,
( ~ hskp13
| ~ c0_1(a396) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_38,negated_conjecture,
( ~ hskp13
| ~ c3_1(a396) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_42,negated_conjecture,
( ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1)
| epred38_0 ),
inference(split_equiv,[status(thm)],[c_0_24]),
[final] ).
cnf(c_0_43,negated_conjecture,
( ~ hskp29
| c1_1(a390) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_44,negated_conjecture,
( ~ hskp29
| c0_1(a390) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_58,negated_conjecture,
( ~ hskp9
| c3_1(a387) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_59,negated_conjecture,
( ~ hskp9
| c2_1(a387) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_65,negated_conjecture,
( ~ hskp28
| c3_1(a386) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_66,negated_conjecture,
( ~ hskp28
| c2_1(a386) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_69,negated_conjecture,
( ~ hskp2
| c1_1(a377) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_70,negated_conjecture,
( ~ hskp2
| ~ c2_1(a377) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_71,negated_conjecture,
( ~ hskp2
| ~ c3_1(a377) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_75,negated_conjecture,
( ~ hskp13
| epred47_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_36]),c_0_37]),c_0_38]),
[final] ).
cnf(c_0_79,negated_conjecture,
( ~ c2_1(a390)
| ~ hskp29
| epred38_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_44]),
[final] ).
cnf(c_0_95,negated_conjecture,
( ~ hskp25
| c3_1(a425) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_96,negated_conjecture,
( ~ hskp25
| ~ c1_1(a425) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_97,negated_conjecture,
( ~ hskp25
| ~ c0_1(a425) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_112,negated_conjecture,
( ~ c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp16
| epred33_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_67]),c_0_8])]),
[final] ).
cnf(c_0_117,negated_conjecture,
( ~ hskp3
| c1_1(a378) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_118,negated_conjecture,
( ~ hskp3
| c3_1(a378) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_119,negated_conjecture,
( ~ hskp3
| ~ c0_1(a378) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_121,negated_conjecture,
( ~ hskp2
| c0_1(a377)
| epred47_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_69]),c_0_71]),
[final] ).
cnf(c_0_146,negated_conjecture,
( ~ hskp29
| c3_1(a390) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_184,negated_conjecture,
( ~ hskp7
| ~ c0_1(a384) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_186,negated_conjecture,
( ~ hskp7
| ~ c2_1(a384) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_196,negated_conjecture,
( ~ hskp28
| c1_1(a386) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_209,negated_conjecture,
( ~ c2_1(X1)
| c1_1(X1)
| c3_1(X1)
| epred43_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_166]),c_0_8])]),
[final] ).
cnf(c_0_284,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred41_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_259]),c_0_8])]),
[final] ).
cnf(c_0_324,negated_conjecture,
( ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X1)
| epred36_0 ),
inference(split_equiv,[status(thm)],[c_0_306]),
[final] ).
cnf(c_0_346,negated_conjecture,
( ~ hskp29
| epred36_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_324,c_0_43]),c_0_44]),c_0_146]),
[final] ).
cnf(c_0_351,negated_conjecture,
( ~ hskp9
| ~ c1_1(a387) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_375,negated_conjecture,
( ~ c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred49_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_349]),c_0_8])]),
[final] ).
cnf(c_0_384,negated_conjecture,
( ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| epred42_0 ),
inference(split_equiv,[status(thm)],[c_0_354]),
[final] ).
cnf(c_0_400,negated_conjecture,
( ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp29
| epred26_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_368]),c_0_8])]),
[final] ).
cnf(c_0_406,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| epred43_0
| epred49_0 ),
inference(spm,[status(thm)],[c_0_375,c_0_209]),
[final] ).
cnf(c_0_411,negated_conjecture,
( ~ c0_1(a386)
| ~ hskp28
| epred38_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_196]),c_0_66]),
[final] ).
cnf(c_0_437,negated_conjecture,
( ~ hskp2
| c0_1(a377)
| hskp29
| epred26_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_400,c_0_69]),c_0_71]),
[final] ).
cnf(c_0_474,negated_conjecture,
( ~ c0_1(a386)
| ~ hskp28
| epred36_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_324,c_0_196]),c_0_65]),
[final] ).
cnf(c_0_642,negated_conjecture,
( ~ hskp26
| ~ c3_1(a427) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_643,negated_conjecture,
( ~ hskp26
| ~ c0_1(a427) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_645,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp22
| hskp26 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_624,c_0_8])]),
[final] ).
cnf(c_0_687,negated_conjecture,
( ~ hskp7
| c3_1(a384) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_688,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp3
| epred3_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_664]),c_0_8])]),
[final] ).
cnf(c_0_695,negated_conjecture,
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| epred9_0 ),
inference(split_equiv,[status(thm)],[c_0_675]),
[final] ).
cnf(c_0_733,negated_conjecture,
epred46_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_569,c_0_712]),c_0_713]),
[final] ).
cnf(c_0_751,negated_conjecture,
( ~ hskp25
| epred9_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_695]),c_0_95]),c_0_97]),
[final] ).
cnf(c_0_786,negated_conjecture,
( ~ hskp9
| c0_1(a387)
| epred9_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_351,c_0_695]),c_0_58]),
[final] ).
cnf(c_0_801,negated_conjecture,
( ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| epred7_0 ),
inference(split_equiv,[status(thm)],[c_0_778]),
[final] ).
cnf(c_0_822,negated_conjecture,
( ~ hskp9
| c0_1(a387)
| epred7_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_351,c_0_801]),c_0_59]),
[final] ).
cnf(c_0_823,negated_conjecture,
( ~ c2_1(a425)
| ~ hskp25
| epred7_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_801]),c_0_97]),
[final] ).
cnf(c_0_882,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp24
| hskp25 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_859,c_0_8])]),
[final] ).
cnf(c_0_903,negated_conjecture,
( ~ hskp18
| c1_1(a404) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_904,negated_conjecture,
( ~ hskp18
| c3_1(a404) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_905,negated_conjecture,
( ~ hskp18
| ~ c2_1(a404) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_959,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| hskp6
| epred8_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_928]),c_0_8])]),
[final] ).
cnf(c_0_1031,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred38_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_42,c_0_384]),
[final] ).
cnf(c_0_1065,negated_conjecture,
( ~ hskp13
| hskp29
| epred26_0 ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_400,c_0_36]),c_0_37]),c_0_38]),
[final] ).
cnf(c_0_1087,negated_conjecture,
epred34_0,
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_490,c_0_1040]),c_0_1041]),c_0_1042]),
[final] ).
cnf(c_0_1127,negated_conjecture,
~ epred33_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_272,c_0_1087])]),
[final] ).
cnf(c_0_1321,negated_conjecture,
epred50_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1303,c_0_1304]),c_0_1305]),
[final] ).
cnf(c_0_1332,negated_conjecture,
epred30_0,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_758,c_0_1318]),c_0_1319]),
[final] ).
cnf(c_0_1333,negated_conjecture,
~ epred49_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1320,c_0_1321])]),
[final] ).
cnf(c_0_1345,negated_conjecture,
epred44_0,
inference(sr,[status(thm)],[c_0_1297,c_0_1333]),
[final] ).
cnf(c_0_1352,negated_conjecture,
( ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp20
| epred25_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1341]),c_0_8])]),
[final] ).
cnf(c_0_1355,negated_conjecture,
~ epred43_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1344,c_0_1345])]),
[final] ).
cnf(c_0_1358,negated_conjecture,
epred48_0,
inference(sr,[status(thm)],[c_0_1346,c_0_1333]),
[final] ).
cnf(c_0_1367,negated_conjecture,
epred45_0,
inference(sr,[status(thm)],[c_0_1170,c_0_1333]),
[final] ).
cnf(c_0_1368,negated_conjecture,
epred20_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_523,c_0_1333]),c_0_1355]),
[final] ).
cnf(c_0_1371,negated_conjecture,
~ epred38_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1357,c_0_1358])]),
[final] ).
cnf(c_0_1376,negated_conjecture,
~ epred7_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_921,c_0_1367])]),c_0_1368])]),
[final] ).
cnf(c_0_1378,negated_conjecture,
epred13_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1370,c_0_1355]),c_0_1371]),
[final] ).
cnf(c_0_1380,negated_conjecture,
epred32_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1273,c_0_1333]),c_0_1355]),
[final] ).
cnf(c_0_1386,negated_conjecture,
hskp0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_892,c_0_1371]),c_0_1376]),
[final] ).
cnf(c_0_1387,negated_conjecture,
~ epred25_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1377,c_0_1378])]),
[final] ).
cnf(c_0_1389,negated_conjecture,
~ epred47_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_357,c_0_1345])]),c_0_1380])]),
[final] ).
cnf(c_0_1392,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred38_0
| epred43_0 ),
inference(spm,[status(thm)],[c_0_42,c_0_209]),
[final] ).
cnf(c_0_1399,negated_conjecture,
hskp11,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1385,c_0_1386])]),c_0_1333]),c_0_1355]),c_0_1387]),
[final] ).
cnf(c_0_1400,negated_conjecture,
~ epred29_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_542,c_0_1332])]),
[final] ).
cnf(c_0_1401,negated_conjecture,
~ epred9_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_758,c_0_1380])]),
[final] ).
cnf(c_0_1403,negated_conjecture,
c3_1(a375),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_971,c_0_1386])]),c_0_1389]),
[final] ).
cnf(c_0_1404,negated_conjecture,
~ c2_1(a375),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_91,c_0_1386])]),
[final] ).
cnf(c_0_1405,negated_conjecture,
~ c0_1(a375),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_90,c_0_1386])]),
[final] ).
cnf(c_0_1409,negated_conjecture,
hskp8,
inference(sr,[status(thm)],[c_0_519,c_0_1333]),
[final] ).
cnf(c_0_1410,negated_conjecture,
epred18_0,
inference(sr,[status(thm)],[c_0_1393,c_0_1371]),
[final] ).
cnf(c_0_1411,negated_conjecture,
hskp5,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_607,c_0_1333]),c_0_1355]),c_0_1371]),
[final] ).
cnf(c_0_1417,negated_conjecture,
hskp12,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1398,c_0_1399])]),c_0_1400]),c_0_1401]),
[final] ).
cnf(c_0_1418,negated_conjecture,
~ epred12_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1402,c_0_1378])]),
[final] ).
cnf(c_0_1419,negated_conjecture,
epred5_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_686,c_0_1403]),c_0_1404]),c_0_1405]),
[final] ).
cnf(c_0_1421,negated_conjecture,
~ hskp20,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1407,c_0_1408]),c_0_1376]),
[final] ).
cnf(c_0_1423,negated_conjecture,
c0_1(a385),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20,c_0_1409])]),
[final] ).
cnf(c_0_1424,negated_conjecture,
c2_1(a385),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21,c_0_1409])]),
[final] ).
cnf(c_0_1426,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| hskp16
| epred33_0
| epred43_0 ),
inference(spm,[status(thm)],[c_0_112,c_0_209]),
[final] ).
cnf(c_0_1427,negated_conjecture,
~ epred17_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_253,c_0_1410])]),
[final] ).
cnf(c_0_1428,negated_conjecture,
epred35_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_522,c_0_1411])]),c_0_1333]),c_0_1355]),
[final] ).
cnf(c_0_1431,negated_conjecture,
epred24_0,
inference(sr,[status(thm)],[c_0_648,c_0_1333]),
[final] ).
cnf(c_0_1438,negated_conjecture,
~ epred40_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_313,c_0_1380])]),
[final] ).
cnf(c_0_1441,negated_conjecture,
~ epred4_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_815,c_0_1419])]),
[final] ).
cnf(c_0_1442,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp16
| epred7_0
| epred33_0 ),
inference(spm,[status(thm)],[c_0_112,c_0_801]),
[final] ).
cnf(c_0_1443,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_158,c_0_1392]),c_0_1355]),c_0_1371]),c_0_157]),c_0_156]),
[final] ).
cnf(c_0_1445,negated_conjecture,
~ hskp14,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1421,c_0_1365]),c_0_1387]),
[final] ).
cnf(c_0_1450,negated_conjecture,
~ epred36_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_503,c_0_1428])]),
[final] ).
cnf(c_0_1453,negated_conjecture,
~ epred23_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1430,c_0_1431])]),
[final] ).
cnf(c_0_1461,negated_conjecture,
~ epred39_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_336,c_0_1380])]),
[final] ).
cnf(c_0_1462,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred7_0
| epred47_0 ),
inference(spm,[status(thm)],[c_0_14,c_0_801]),
[final] ).
cnf(c_0_1463,negated_conjecture,
hskp23,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1436,c_0_1437]),c_0_1389]),c_0_1438]),
[final] ).
cnf(c_0_1467,negated_conjecture,
hskp4,
inference(sr,[status(thm)],[c_0_1440,c_0_1441]),
[final] ).
cnf(c_0_1470,negated_conjecture,
hskp15,
inference(sr,[status(thm)],[c_0_1444,c_0_1445]),
[final] ).
cnf(c_0_1471,negated_conjecture,
hskp21,
inference(sr,[status(thm)],[c_0_1446,c_0_1445]),
[final] ).
cnf(c_0_1474,negated_conjecture,
hskp10,
inference(sr,[status(thm)],[c_0_1449,c_0_1450]),
[final] ).
cnf(c_0_1475,negated_conjecture,
hskp1,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1451,c_0_1399])]),c_0_1418]),
[final] ).
cnf(c_0_1476,negated_conjecture,
hskp19,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1452,c_0_1399])]),c_0_1453]),
[final] ).
cnf(c_0_1477,negated_conjecture,
epred2_0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_852,c_0_1399])]),c_0_1401]),
[final] ).
cnf(c_0_1479,negated_conjecture,
epred15_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1456,c_0_1333]),c_0_1355]),
[final] ).
cnf(c_0_1481,negated_conjecture,
epred11_0,
inference(sr,[status(thm)],[c_0_1459,c_0_1333]),
[final] ).
cnf(c_0_1484,negated_conjecture,
hskp30,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1460,c_0_1386])]),c_0_1389]),c_0_1461]),
[final] ).
cnf(c_0_1485,negated_conjecture,
( ~ c2_1(a396)
| ~ hskp13 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_38,c_0_1462]),c_0_1389]),c_0_1376]),c_0_37]),
[final] ).
cnf(c_0_1486,negated_conjecture,
( ~ c2_1(a427)
| ~ hskp26 ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_642,c_0_1462]),c_0_1389]),c_0_1376]),c_0_643]),
[final] ).
cnf(c_0_1487,negated_conjecture,
( ~ hskp6
| c3_1(a381) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1442,c_0_29]),c_0_1127]),c_0_1376]),c_0_1443]),c_0_30]),
[final] ).
cnf(c_0_1488,negated_conjecture,
( ~ c0_1(a420)
| epred42_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_622,c_0_1463])]),
[final] ).
cnf(c_0_1489,negated_conjecture,
( hskp9
| hskp28 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_154,c_0_1386])]),
[final] ).
cnf(c_0_1490,negated_conjecture,
( ~ epred41_0
| ~ epred42_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_490,c_0_1431])]),
[final] ).
cnf(c_0_1491,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred7_0
| epred49_0 ),
inference(spm,[status(thm)],[c_0_375,c_0_801]),
[final] ).
cnf(c_0_1492,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred42_0
| epred49_0 ),
inference(spm,[status(thm)],[c_0_375,c_0_384]),
[final] ).
cnf(c_0_1493,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| epred43_0
| epred47_0 ),
inference(spm,[status(thm)],[c_0_14,c_0_209]),
[final] ).
cnf(c_0_1494,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp29
| epred26_0
| epred43_0 ),
inference(spm,[status(thm)],[c_0_400,c_0_209]),
[final] ).
cnf(c_0_1495,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp16
| epred33_0
| epred42_0 ),
inference(spm,[status(thm)],[c_0_112,c_0_384]),
[final] ).
cnf(c_0_1496,negated_conjecture,
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp29
| epred7_0
| epred26_0 ),
inference(spm,[status(thm)],[c_0_400,c_0_801]),
[final] ).
cnf(c_0_1497,negated_conjecture,
( ~ c0_1(a404)
| ~ hskp18
| epred36_0 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_324,c_0_903]),c_0_904]),
[final] ).
cnf(c_0_1498,negated_conjecture,
( ~ c2_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp14
| epred21_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1464]),c_0_8])]),
[final] ).
cnf(c_0_1499,negated_conjecture,
( ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| epred22_0 ),
inference(split_equiv,[status(thm)],[c_0_1465]),
[final] ).
cnf(c_0_1500,negated_conjecture,
( ~ epred21_0
| ~ epred22_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_1466,c_0_1464]),c_0_1465]),
[final] ).
cnf(c_0_1501,negated_conjecture,
( ~ hskp26
| ~ c1_1(a427) ),
inference(split_conjunct,[status(thm)],[c_0_3]),
[final] ).
cnf(c_0_1502,negated_conjecture,
~ c1_1(a379),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_229,c_0_1467])]),
[final] ).
cnf(c_0_1503,negated_conjecture,
~ c0_1(a379),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_179,c_0_1467])]),
[final] ).
cnf(c_0_1504,negated_conjecture,
~ c2_1(a379),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_181,c_0_1467])]),
[final] ).
cnf(c_0_1505,negated_conjecture,
~ c3_1(a379),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_740,c_0_1467])]),c_0_1401]),
[final] ).
cnf(c_0_1506,negated_conjecture,
~ hskp24,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1468,c_0_1469]),c_0_1401]),
[final] ).
cnf(c_0_1507,negated_conjecture,
~ c0_1(a399),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_212,c_0_1470])]),
[final] ).
cnf(c_0_1508,negated_conjecture,
~ c2_1(a399),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_213,c_0_1470])]),
[final] ).
cnf(c_0_1509,negated_conjecture,
~ c3_1(a399),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_210,c_0_1470])]),
[final] ).
cnf(c_0_1510,negated_conjecture,
~ c0_1(a411),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63,c_0_1471])]),
[final] ).
cnf(c_0_1511,negated_conjecture,
~ hskp27,
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_369,c_0_1392]),c_0_1355]),c_0_1371]),c_0_1450]),c_0_51]),c_0_52]),
[final] ).
cnf(c_0_1512,negated_conjecture,
~ hskp22,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1364,c_0_1472]),c_0_1355]),
[final] ).
cnf(c_0_1513,negated_conjecture,
~ hskp17,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1364,c_0_1473]),c_0_1355]),
[final] ).
cnf(c_0_1514,negated_conjecture,
~ c2_1(a392),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83,c_0_1474])]),
[final] ).
cnf(c_0_1515,negated_conjecture,
~ c3_1(a392),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_365,c_0_1474])]),c_0_1450]),
[final] ).
cnf(c_0_1516,negated_conjecture,
~ c3_1(a380),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_114,c_0_1411])]),
[final] ).
cnf(c_0_1517,negated_conjecture,
~ c2_1(a380),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_513,c_0_1411])]),c_0_1333]),
[final] ).
cnf(c_0_1518,negated_conjecture,
~ c2_1(a376),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_194,c_0_1475])]),
[final] ).
cnf(c_0_1519,negated_conjecture,
~ c3_1(a376),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_192,c_0_1475])]),
[final] ).
cnf(c_0_1520,negated_conjecture,
~ c2_1(a407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1331,c_0_1476])]),
[final] ).
cnf(c_0_1521,negated_conjecture,
~ c1_1(a395),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_430,c_0_1417])]),
[final] ).
cnf(c_0_1522,negated_conjecture,
~ c2_1(a395),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_433,c_0_1417])]),
[final] ).
cnf(c_0_1523,negated_conjecture,
~ c1_1(a394),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_780,c_0_1399])]),
[final] ).
cnf(c_0_1524,negated_conjecture,
~ c2_1(a394),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_803,c_0_1399])]),
[final] ).
cnf(c_0_1525,negated_conjecture,
~ c1_1(a420),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_191,c_0_1463])]),
[final] ).
cnf(c_0_1526,negated_conjecture,
~ c2_1(a420),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_190,c_0_1463])]),
[final] ).
cnf(c_0_1527,negated_conjecture,
~ c3_1(a420),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_189,c_0_1463])]),
[final] ).
cnf(c_0_1528,negated_conjecture,
~ epred1_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_471,c_0_1477])]),
[final] ).
cnf(c_0_1529,negated_conjecture,
~ epred3_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_797,c_0_1477])]),
[final] ).
cnf(c_0_1530,negated_conjecture,
~ epred26_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_439,c_0_1378])]),
[final] ).
cnf(c_0_1531,negated_conjecture,
~ c1_1(a385),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18,c_0_1409])]),
[final] ).
cnf(c_0_1532,negated_conjecture,
~ epred31_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_761,c_0_1380])]),
[final] ).
cnf(c_0_1533,negated_conjecture,
~ epred19_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1478,c_0_1368])]),
[final] ).
cnf(c_0_1534,negated_conjecture,
~ epred27_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_164,c_0_1368])]),
[final] ).
cnf(c_0_1535,negated_conjecture,
~ epred14_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_280,c_0_1479])]),
[final] ).
cnf(c_0_1536,negated_conjecture,
~ epred16_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_176,c_0_1479])]),
[final] ).
cnf(c_0_1537,negated_conjecture,
~ epred28_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1480,c_0_1479])]),
[final] ).
cnf(c_0_1538,negated_conjecture,
~ epred10_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_725,c_0_1481])]),
[final] ).
cnf(c_0_1539,negated_conjecture,
c1_1(a376),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1482,c_0_1475])]),c_0_1387]),c_0_1421]),
[final] ).
cnf(c_0_1540,negated_conjecture,
c3_1(a395),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1483,c_0_1417])]),c_0_1387]),c_0_1421]),
[final] ).
cnf(c_0_1541,negated_conjecture,
c2_1(a411),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_62,c_0_1471])]),
[final] ).
cnf(c_0_1542,negated_conjecture,
c3_1(a411),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61,c_0_1471])]),
[final] ).
cnf(c_0_1543,negated_conjecture,
c3_1(a385),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_321,c_0_1409])]),c_0_1355]),
[final] ).
cnf(c_0_1544,negated_conjecture,
c1_1(a392),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_81,c_0_1474])]),
[final] ).
cnf(c_0_1545,negated_conjecture,
c0_1(a392),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82,c_0_1474])]),
[final] ).
cnf(c_0_1546,negated_conjecture,
c1_1(a380),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_113,c_0_1411])]),
[final] ).
cnf(c_0_1547,negated_conjecture,
c0_1(a380),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_116,c_0_1411])]),
[final] ).
cnf(c_0_1548,negated_conjecture,
c0_1(a376),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_193,c_0_1475])]),
[final] ).
cnf(c_0_1549,negated_conjecture,
c0_1(a407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_517,c_0_1476])]),
[final] ).
cnf(c_0_1550,negated_conjecture,
c3_1(a407),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_516,c_0_1476])]),
[final] ).
cnf(c_0_1551,negated_conjecture,
c0_1(a395),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_432,c_0_1417])]),
[final] ).
cnf(c_0_1552,negated_conjecture,
c0_1(a397),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_149,c_0_1484])]),
[final] ).
cnf(c_0_1553,negated_conjecture,
c2_1(a397),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_150,c_0_1484])]),
[final] ).
cnf(c_0_1554,negated_conjecture,
c3_1(a397),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_148,c_0_1484])]),
[final] ).
cnf(c_0_1555,negated_conjecture,
c3_1(a394),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_781,c_0_1399])]),
[final] ).
cnf(c_0_1556,negated_conjecture,
c0_1(a394),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_806,c_0_1399])]),c_0_1401]),
[final] ).
cnf(c_0_1557,negated_conjecture,
c1_1(a375),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_89,c_0_1386])]),
[final] ).
cnf(c_0_1558,negated_conjecture,
epred37_0,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1295,c_0_1333]),c_0_1355]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN446+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/5.39 % Computer : n013.cluster.edu
% 0.12/5.39 % Model : x86_64 x86_64
% 0.12/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.39 % Memory : 8046.5625MB
% 0.12/5.39 % OS : Linux 6.8.0-71-generic
% 0.12/5.39 % CPULimit : 300
% 0.12/5.39 % WCLimit : 300
% 0.12/5.39 % DateTime : Mon Sep 21 10:57:05 UTC 2026
% 0.12/5.40 % CPUTime :
% 0.12/5.40 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/5.43 Running first-order theorem proving
% 0.15/5.43 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
% 70.04/15.58 % Version: 3.5.1
% 70.04/15.58 % Preprocessing class: FSLSSLSMSSSNFFN.
% 70.04/15.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 70.04/15.58 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 70.04/15.58 % Starting new_bool_3 with 300s (1) cores
% 70.04/15.58 % Starting new_bool_1 with 300s (1) cores
% 70.04/15.58 % Starting sh5l with 300s (1) cores
% 70.04/15.58 % G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with pid 607937 completed with status 1
% 70.04/15.58 % Result found by G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1
% 70.04/15.58 % Preprocessing class: FSLSSLSMSSSNFFN.
% 70.04/15.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 70.04/15.58 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 70.04/15.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 70.04/15.58 % No SInE strategy applied
% 70.04/15.58 % Search class: FGHNF-FSMM00-SFFFFFNN
% 70.04/15.58 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 70.04/15.58 % Starting SubtermCWHack with 151s (1) cores
% 70.04/15.58 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 901s (1) cores
% 70.04/15.58 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with 151s (1) cores
% 70.04/15.58 % Starting H----_042_B03_F1_AE_Q4_SP_S2S with 151s (1) cores
% 70.04/15.58 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S2g with 146s (1) cores
% 70.04/15.58 % G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with pid 607943 completed with status 1
% 70.04/15.58 % Result found by G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y
% 70.04/15.58 % Preprocessing class: FSLSSLSMSSSNFFN.
% 70.04/15.58 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 70.04/15.58 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 1500s (5) cores
% 70.04/15.58 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 70.04/15.58 % No SInE strategy applied
% 70.04/15.58 % Search class: FGHNF-FSMM00-SFFFFFNN
% 70.04/15.58 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 70.04/15.58 % Starting SubtermCWHack with 151s (1) cores
% 70.04/15.58 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y1 with 901s (1) cores
% 70.04/15.58 % Starting G-N--_023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y with 151s (1) cores
% 70.04/15.58 % Preprocessing time : 0.001 s
% 70.04/15.58
% 70.04/15.58 % No proof found!
% 70.04/15.58 % SZS status CounterSatisfiable
% 70.04/15.58 % SZS output start Saturation
% See solution above
% 70.04/15.58 % Parsed axioms : 1
% 70.04/15.58 % Removed by relevancy pruning/SinE : 0
% 70.04/15.58 % Initial clauses : 184
% 70.04/15.58 % Removed in clause preprocessing : 0
% 70.04/15.58 % Initial clauses in saturation : 184
% 70.04/15.58 % Processed clauses : 41986
% 70.04/15.58 % ...of these trivial : 734
% 70.04/15.58 % ...subsumed : 25213
% 70.04/15.58 % ...remaining for further processing : 16039
% 70.04/15.58 % Other redundant clauses eliminated : 0
% 70.04/15.58 % Clauses deleted for lack of memory : 0
% 70.04/15.58 % Backward-subsumed : 10888
% 70.04/15.58 % Backward-rewritten : 4220
% 70.04/15.58 % Generated clauses : 520842
% 70.04/15.58 % ...of the previous two non-redundant : 504630
% 70.04/15.58 % ...aggressively subsumed : 0
% 70.04/15.58 % Contextual simplify-reflections : 2639
% 70.04/15.58 % Paramodulations : 520057
% 70.04/15.58 % Factorizations : 0
% 70.04/15.58 % NegExts : 0
% 70.04/15.58 % Equation resolutions : 0
% 70.04/15.58 % Disequality decompositions : 0
% 70.04/15.58 % Total rewrite steps : 5628
% 70.04/15.58 % ...of those cached : 5576
% 70.04/15.58 % Propositional unsat checks : 3
% 70.04/15.58 % Propositional check models : 3
% 70.04/15.58 % Propositional check unsatisfiable : 0
% 70.04/15.58 % Propositional clauses : 0
% 70.04/15.58 % Propositional clauses after purity: 0
% 70.04/15.58 % Propositional unsat core size : 0
% 70.04/15.58 % Propositional preprocessing time : 0.000
% 70.04/15.58 % Propositional encoding time : 0.170
% 70.04/15.58 % Propositional solver time : 0.516
% 70.04/15.58 % Success case prop preproc time : 0.000
% 70.04/15.58 % Success case prop encoding time : 0.000
% 70.04/15.58 % Success case prop solver time : 0.000
% 70.04/15.58 % Current number of processed clauses : 196
% 70.04/15.58 % Positive orientable unit clauses : 54
% 70.04/15.58 % Positive unorientable unit clauses: 0
% 70.04/15.58 % Negative unit clauses : 58
% 70.04/15.58 % Non-unit-clauses : 84
% 70.04/15.58 % Current number of unprocessed clauses: 0
% 70.04/15.58 % ...number of literals in the above : 0
% 70.04/15.58 % Current number of archived formulas : 0
% 70.04/15.58 % Current number of archived clauses : 15811
% 70.04/15.58 % Clause-clause subsumption calls (NU) : 44288385
% 70.04/15.58 % Rec. Clause-clause subsumption calls : 1927113
% 70.04/15.58 % Non-unit clause-clause subsumptions : 37950
% 70.04/15.58 % Unit Clause-clause subsumption calls : 75716
% 70.04/15.58 % Rewrite failures with RHS unbound : 0
% 70.04/15.58 % BW rewrite match attempts : 34
% 70.04/15.58 % BW rewrite match successes : 34
% 70.04/15.58 % Condensation attempts : 41986
% 70.04/15.58 % Condensation successes : 0
% 70.04/15.58 % Termbank termtop insertions : 4708428
% 70.04/15.58 % Search garbage collected termcells : 1741
% 70.04/15.58
% 70.04/15.58 % -------------------------------------------------
% 70.04/15.58 % User time : 9.617 s
% 70.04/15.58 % System time : 0.242 s
% 70.04/15.58 % Total time : 9.859 s
% 70.04/15.58 % Maximum resident set size: 4656 pages
% 70.04/15.58
% 70.04/15.58 % -------------------------------------------------
% 70.04/15.58 % User time : 48.401 s
% 70.04/15.58 % System time : 1.146 s
% 70.04/15.58 % Total time : 49.547 s
% 70.04/15.58 % Maximum resident set size: 5376 pages
% 70.04/15.58 % E exiting
%------------------------------------------------------------------------------