%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : PUZ071+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:02:31 PM UTC 2026
% Result : Satisfiable 1.96s 0.80s
% Output : Saturation 1.96s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named ax353ERROR: Could not build tree for root c_0_130ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_130,plain,
ssA(n1,n1) = n4,
inference(split_conjunct,[status(thm)],[ax353]),
[final] ).
cnf(c_0_131,plain,
ssA(n1,n2) = n5,
inference(split_conjunct,[status(thm)],[ax354]),
[final] ).
cnf(c_0_132,plain,
ssA(n3,n2) = n2,
inference(split_conjunct,[status(thm)],[ax358]),
[final] ).
cnf(c_0_133,plain,
n1 != n4,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_134,plain,
n1 != n5,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_135,plain,
n1 != n2,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_137,plain,
ssA(n2,n9) = n1,
inference(split_conjunct,[status(thm)],[ax357]),
[final] ).
cnf(c_0_147,plain,
ssA(n4,n3) = n1,
inference(split_conjunct,[status(thm)],[ax359]),
[final] ).
cnf(c_0_164,plain,
ssA(n3,n1) = n1,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_153,c_0_154]),c_0_155]),
[final] ).
cnf(c_0_167,plain,
ssA(n8,n4) = n1,
inference(split_conjunct,[status(thm)],[ax367]),
[final] ).
cnf(c_0_174,plain,
ssA(n1,n5) = n8,
inference(split_conjunct,[status(thm)],[ax355]),
[final] ).
cnf(c_0_175,plain,
ssA(n5,n5) = n4,
inference(split_conjunct,[status(thm)],[ax363]),
[final] ).
cnf(c_0_176,plain,
n1 != n8,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_209,plain,
ssA(n6,n5) = n1,
inference(sr,[status(thm)],[c_0_192,c_0_193]),
[final] ).
cnf(c_0_212,plain,
ssA(n2,n8) = n7,
inference(split_conjunct,[status(thm)],[ax356]),
[final] ).
cnf(c_0_222,plain,
ssA(n5,n7) = n2,
inference(split_conjunct,[status(thm)],[ax364]),
[final] ).
cnf(c_0_223,plain,
ssA(n7,n7) = n8,
inference(split_conjunct,[status(thm)],[ax366]),
[final] ).
cnf(c_0_230,plain,
n4 != n7,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_231,plain,
n5 != n7,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_232,plain,
n7 != n8,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_237,plain,
ssA(n9,n4) = n7,
inference(split_conjunct,[status(thm)],[ax369]),
[final] ).
cnf(c_0_243,plain,
ssA(n9,n7) = n1,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_221,c_0_222]),c_0_223]),c_0_196]),c_0_224]),c_0_225]),c_0_226]),c_0_135]),c_0_227]),c_0_176]),c_0_228]),
[final] ).
cnf(c_0_246,plain,
ssA(n1,n6) = n1,
inference(sr,[status(thm)],[c_0_238,c_0_239]),
[final] ).
cnf(c_0_247,plain,
n1 != n7,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_251,plain,
ssA(n1,n3) = n7,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_244,c_0_245]),c_0_246]),c_0_247]),
[final] ).
cnf(c_0_258,plain,
ssA(n7,n1) = n2,
inference(split_conjunct,[status(thm)],[ax365]),
[final] ).
cnf(c_0_259,plain,
ssA(n7,n2) = n1,
inference(sr,[status(thm)],[c_0_248,c_0_249]),
[final] ).
cnf(c_0_260,plain,
n2 != n7,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_267,plain,
ssA(n4,n8) = n3,
inference(split_conjunct,[status(thm)],[ax361]),
[final] ).
cnf(c_0_269,plain,
ssA(n8,n6) = n3,
inference(split_conjunct,[status(thm)],[ax368]),
[final] ).
cnf(c_0_283,plain,
ssA(n7,n9) = n7,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_257,c_0_258]),c_0_259]),c_0_223]),c_0_260]),c_0_247]),c_0_261]),c_0_262]),c_0_263]),c_0_264]),c_0_232]),c_0_265]),
[final] ).
cnf(c_0_284,plain,
n3 != n8,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_286,plain,
n3 != n7,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_290,plain,
n1 != n3,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_297,plain,
n3 != n4,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_305,plain,
n3 != n5,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_306,plain,
n2 != n3,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_312,plain,
ssA(n9,n9) = n3,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_282,c_0_223]),c_0_283]),c_0_243]),c_0_284]),c_0_285]),c_0_286]),c_0_287]),c_0_288]),c_0_289]),c_0_290]),c_0_291]),
[final] ).
cnf(c_0_351,plain,
ssA(n7,n3) = n3,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_328,c_0_329]),c_0_330]),c_0_331]),
[final] ).
cnf(c_0_389,plain,
ssA(n5,n1) = n5,
inference(split_conjunct,[status(thm)],[ax362]),
[final] ).
cnf(c_0_390,plain,
ssA(n5,n8) = n1,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_363,c_0_212]),c_0_267]),c_0_198]),c_0_247]),c_0_364]),c_0_290]),c_0_365]),c_0_366]),c_0_367]),c_0_368]),
[final] ).
cnf(c_0_395,plain,
ssA(n4,n4) = n6,
inference(split_conjunct,[status(thm)],[ax360]),
[final] ).
cnf(c_0_398,plain,
n2 != n6,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_423,plain,
ssA(n4,n5) = n7,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_401,c_0_402]),c_0_403]),
[final] ).
cnf(c_0_435,plain,
n6 != n8,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_438,plain,
n3 != n6,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_456,plain,
ssA(n4,n6) = n2,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_422,c_0_423]),c_0_260]),
[final] ).
cnf(c_0_462,plain,
ssA(n6,n3) = n2,
inference(sr,[status(thm)],[c_0_427,c_0_428]),
[final] ).
cnf(c_0_495,plain,
ssA(n5,n2) = n7,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_469,c_0_423])]),
[final] ).
cnf(c_0_532,plain,
ssA(n5,n4) = n3,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_494,c_0_495]),c_0_286]),
[final] ).
cnf(c_0_550,plain,
n2 != n8,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_553,plain,
ssA(n9,n6) = n8,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_513,c_0_167]),c_0_269]),c_0_237]),c_0_436]),c_0_514]),c_0_515]),c_0_176]),c_0_516]),c_0_284]),c_0_232]),c_0_517]),
[final] ).
cnf(c_0_560,plain,
ssA(n2,n4) = n2,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_524,c_0_525]),c_0_526]),
[final] ).
cnf(c_0_575,plain,
n2 != n4,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_589,plain,
ssA(n1,n7) = n3,
inference(sr,[status(thm)],[c_0_565,c_0_566]),
[final] ).
cnf(c_0_596,plain,
n5 != n8,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_597,plain,
n4 != n8,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_607,plain,
n4 != n5,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_609,plain,
ssA(n8,n1) = n7,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_580,c_0_495])]),
[final] ).
cnf(c_0_613,plain,
ssA(n1,n4) = n9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_583,c_0_566]),c_0_584]),
[final] ).
cnf(c_0_621,plain,
ssA(n3,n8) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_592,c_0_532]),c_0_284]),
[final] ).
cnf(c_0_623,plain,
n5 != n6,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_625,plain,
n4 != n6,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_627,plain,
n1 != n6,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_642,plain,
ssA(n3,n5) = n3,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_615,c_0_616]),c_0_617]),
[final] ).
cnf(c_0_648,plain,
n6 != n7,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_651,plain,
ssA(n3,n6) = n7,
inference(sr,[status(thm)],[c_0_631,c_0_632]),
[final] ).
cnf(c_0_657,plain,
ssA(n8,n2) = n8,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_636,c_0_637]),c_0_597]),c_0_596]),
[final] ).
cnf(c_0_715,plain,
ssA(n6,n4) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_465,c_0_532]),c_0_284]),
[final] ).
cnf(c_0_717,plain,
ssA(n2,n2) = n3,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_707,c_0_708]),c_0_709]),
[final] ).
cnf(c_0_749,plain,
ssA(n6,n1) = n3,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_732,c_0_717])]),
[final] ).
cnf(c_0_755,plain,
n2 != n5,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_780,plain,
ssA(n6,n6) = n5,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_754,c_0_715]),c_0_456]),c_0_423]),c_0_596]),c_0_755]),c_0_231]),
[final] ).
cnf(c_0_835,plain,
ssA(n1,n8) = n6,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_811,c_0_812]),c_0_623]),
[final] ).
cnf(c_0_841,plain,
ssA(n5,n6) = n9,
inference(sr,[status(thm)],[c_0_816,c_0_817]),
[final] ).
cnf(c_0_850,plain,
n1 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_851,plain,
n6 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_852,plain,
n3 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_866,plain,
n7 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_867,plain,
n2 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_870,plain,
ssA(n3,n3) = n6,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_855,c_0_835])]),c_0_856]),
[final] ).
cnf(c_0_878,plain,
ssA(n4,n2) = n4,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_380,c_0_868]),c_0_853]),
[final] ).
cnf(c_0_879,plain,
n4 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_880,plain,
ssA(n4,n9) = n8,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_869,c_0_870]),c_0_851]),
[final] ).
cnf(c_0_886,plain,
n8 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_891,plain,
ssA(n4,n7) = n5,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_828,c_0_880]),c_0_596]),
[final] ).
cnf(c_0_892,plain,
n5 != n9,
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_907,plain,
ssA(n4,n1) = n9,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_890,c_0_891]),c_0_892]),c_0_880]),c_0_886]),
[final] ).
cnf(c_0_920,plain,
ssA(n7,n6) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_906,c_0_907]),c_0_886]),
[final] ).
cnf(c_0_934,plain,
ssA(n7,n5) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_918,c_0_919]),c_0_920]),c_0_625]),
[final] ).
cnf(c_0_948,plain,
ssA(n7,n8) = n9,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_933,c_0_934]),c_0_851]),
[final] ).
cnf(c_0_981,plain,
ssA(n6,n7) = n7,
inference(sr,[status(thm)],[c_0_956,c_0_957]),
[final] ).
cnf(c_0_998,plain,
ssA(n6,n8) = n4,
inference(sr,[status(thm)],[c_0_969,c_0_970]),
[final] ).
cnf(c_0_1017,plain,
ssA(n2,n7) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_991,c_0_907]),c_0_886]),
[final] ).
cnf(c_0_1027,plain,
ssA(n2,n5) = n5,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_847,c_0_891])]),
[final] ).
cnf(c_0_1060,plain,
ssA(n8,n3) = n5,
inference(sr,[status(thm)],[c_0_1024,c_0_1025]),
[final] ).
cnf(c_0_1065,plain,
ssA(n5,n3) = n8,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_686,c_0_870]),c_0_851]),
[final] ).
cnf(c_0_1072,plain,
ssA(n1,n9) = n2,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1037,c_0_835])]),
[final] ).
cnf(c_0_1075,plain,
ssA(n8,n7) = n6,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1040,c_0_835])]),c_0_1041]),
[final] ).
cnf(c_0_1086,plain,
ssA(n3,n7) = n9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1050,c_0_856]),c_0_1051]),c_0_1052]),
[final] ).
cnf(c_0_1090,plain,
ssA(n9,n8) = n5,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1059,c_0_1060])]),c_0_1061]),
[final] ).
cnf(c_0_1103,plain,
ssA(n6,n2) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1079,c_0_1065]),c_0_435]),
[final] ).
cnf(c_0_1112,plain,
ssA(n9,n5) = n2,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1089,c_0_1090]),c_0_755]),
[final] ).
cnf(c_0_1114,plain,
ssA(n2,n1) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1092,c_0_907]),c_0_886]),
[final] ).
cnf(c_0_1115,plain,
ssA(n2,n3) = n9,
inference(sr,[status(thm)],[c_0_690,c_0_1093]),
[final] ).
cnf(c_0_1116,plain,
ssA(n2,n6) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_889,c_0_907]),c_0_886]),
[final] ).
cnf(c_0_1117,plain,
ssA(n3,n4) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1094,c_0_907]),c_0_886]),
[final] ).
cnf(c_0_1118,plain,
ssA(n5,n9) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_664,c_0_1065]),c_0_435]),
[final] ).
cnf(c_0_1119,plain,
ssA(n7,n4) = n5,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_876,c_0_907]),c_0_886]),
[final] ).
cnf(c_0_1120,plain,
ssA(n8,n8) = n2,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1095,c_0_1090]),c_0_755]),
[final] ).
cnf(c_0_1121,plain,
ssA(n8,n9) = n4,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1096,c_0_1097]),c_0_1098]),c_0_1099]),c_0_1100]),
[final] ).
cnf(c_0_1122,plain,
ssA(n9,n1) = n6,
inference(sr,[status(thm)],[c_0_772,c_0_1101]),
[final] ).
cnf(c_0_1123,plain,
ssA(n9,n2) = n9,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1102,c_0_1103]),c_0_851]),
[final] ).
cnf(c_0_1124,plain,
ssA(n9,n3) = n4,
inference(sr,[status(thm)],[c_0_1104,c_0_1025]),
[final] ).
cnf(c_0_1126,plain,
ssA(n3,n9) = n5,
inference(sr,[status(thm)],[c_0_1107,c_0_1108]),
[final] ).
cnf(c_0_1130,plain,
ssA(n6,n9) = n9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1125,c_0_880]),c_0_886]),c_0_1126]),c_0_1121]),c_0_892]),c_0_879]),
[final] ).
cnf(c_0_1131,plain,
ssA(n8,n5) = n9,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_1127,c_0_1128]),c_0_934]),c_0_851]),
[final] ).
cnf(c_0_1132,plain,
ssP(n4,n5,n7,n9,n8,n1,n3,n6,n2,n8,n3,n9,n2,n5,n6,n4,n7,n1,n1,n2,n6,n4,n3,n7,n9,n8,n5,n9,n4,n1,n6,n7,n2,n5,n3,n8,n5,n7,n8,n3,n4,n9,n2,n1,n6,n3,n6,n2,n8,n1,n5,n7,n4,n9,n2,n1,n3,n5,n6,n4,n8,n9,n7,n7,n8,n5,n1,n9,n3,n6,n2,n4,n6,n9,n4,n7,n2,n8,n1,n5,n3),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1129,c_0_1126]),c_0_1130]),c_0_1131]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ071+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n004.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 03:48:49 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 1.96/0.80 % Version: 3.5.1
% 1.96/0.80 % Preprocessing class: FSLSSMSMSSSNFFN.
% 1.96/0.80 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.96/0.80 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 1.96/0.80 % Starting new_bool_3 with 300s (1) cores
% 1.96/0.80 % Starting new_bool_1 with 300s (1) cores
% 1.96/0.80 % Starting sh5l with 300s (1) cores
% 1.96/0.80 % new_bool_3 with pid 2179987 completed with status 9
% 1.96/0.80 % new_bool_1 with pid 2179988 completed with status 9
% 1.96/0.80 % sh5l with pid 2179989 completed with status 9
% 1.96/0.80 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 2179986 completed with status 1
% 1.96/0.80 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 1.96/0.80 % Preprocessing class: FSLSSMSMSSSNFFN.
% 1.96/0.80 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.96/0.80 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 1.96/0.80 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.96/0.80 % No SInE strategy applied
% 1.96/0.80 % Search class: FGUSF-SSLM22-SFFFFFNN
% 1.96/0.80 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 1.96/0.80 % Starting SubtermCWHack with 136s (1) cores
% 1.96/0.80 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 1.96/0.80 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 1.96/0.80 % Starting new_bool_3 with 136s (1) cores
% 1.96/0.80 % Starting new_bool_1 with 136s (1) cores
% 1.96/0.80 % new_bool_1 with pid 2180032 completed with status 1
% 1.96/0.80 % Result found by new_bool_1
% 1.96/0.80 % Preprocessing class: FSLSSMSMSSSNFFN.
% 1.96/0.80 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.96/0.80 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 1.96/0.80 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.96/0.80 % No SInE strategy applied
% 1.96/0.80 % Search class: FGUSF-SSLM22-SFFFFFNN
% 1.96/0.80 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 1.96/0.80 % Starting SubtermCWHack with 136s (1) cores
% 1.96/0.80 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 1.96/0.80 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 1.96/0.80 % Starting new_bool_3 with 136s (1) cores
% 1.96/0.80 % Starting new_bool_1 with 136s (1) cores
% 1.96/0.80 % Preprocessing time : 0.011 s
% 1.96/0.80 % Presaturation interreduction done
% 1.96/0.80
% 1.96/0.80 % No proof found!
% 1.96/0.80 % SZS status Satisfiable
% 1.96/0.80 % SZS output start Saturation
% See solution above
% 1.96/0.80 % Parsed axioms : 370
% 1.96/0.80 % Removed by relevancy pruning/SinE : 0
% 1.96/0.80 % Initial clauses : 1350
% 1.96/0.80 % Removed in clause preprocessing : 0
% 1.96/0.80 % Initial clauses in saturation : 1350
% 1.96/0.80 % Processed clauses : 6223
% 1.96/0.80 % ...of these trivial : 236
% 1.96/0.80 % ...subsumed : 3343
% 1.96/0.80 % ...remaining for further processing : 2644
% 1.96/0.80 % Other redundant clauses eliminated : 0
% 1.96/0.80 % Clauses deleted for lack of memory : 0
% 1.96/0.80 % Backward-subsumed : 139
% 1.96/0.80 % Backward-rewritten : 1402
% 1.96/0.80 % Generated clauses : 7296
% 1.96/0.80 % ...of the previous two non-redundant : 8053
% 1.96/0.80 % ...aggressively subsumed : 0
% 1.96/0.80 % Contextual simplify-reflections : 6
% 1.96/0.80 % Paramodulations : 7008
% 1.96/0.80 % Factorizations : 131
% 1.96/0.80 % NegExts : 0
% 1.96/0.80 % Equation resolutions : 0
% 1.96/0.80 % Disequality decompositions : 0
% 1.96/0.80 % Total rewrite steps : 3250
% 1.96/0.80 % ...of those cached : 3169
% 1.96/0.80 % Propositional unsat checks : 0
% 1.96/0.80 % Propositional check models : 0
% 1.96/0.80 % Propositional check unsatisfiable : 0
% 1.96/0.80 % Propositional clauses : 0
% 1.96/0.80 % Propositional clauses after purity: 0
% 1.96/0.80 % Propositional unsat core size : 0
% 1.96/0.80 % Propositional preprocessing time : 0.000
% 1.96/0.80 % Propositional encoding time : 0.000
% 1.96/0.80 % Propositional solver time : 0.000
% 1.96/0.80 % Success case prop preproc time : 0.000
% 1.96/0.80 % Success case prop encoding time : 0.000
% 1.96/0.80 % Success case prop solver time : 0.000
% 1.96/0.80 % Current number of processed clauses : 118
% 1.96/0.80 % Positive orientable unit clauses : 82
% 1.96/0.80 % Positive unorientable unit clauses: 0
% 1.96/0.80 % Negative unit clauses : 36
% 1.96/0.80 % Non-unit-clauses : 0
% 1.96/0.80 % Current number of unprocessed clauses: 0
% 1.96/0.80 % ...number of literals in the above : 0
% 1.96/0.80 % Current number of archived formulas : 0
% 1.96/0.80 % Current number of archived clauses : 2526
% 1.96/0.80 % Clause-clause subsumption calls (NU) : 2908
% 1.96/0.80 % Rec. Clause-clause subsumption calls : 1248
% 1.96/0.80 % Non-unit clause-clause subsumptions : 237
% 1.96/0.80 % Unit Clause-clause subsumption calls : 95911
% 1.96/0.80 % Rewrite failures with RHS unbound : 0
% 1.96/0.80 % BW rewrite match attempts : 64
% 1.96/0.80 % BW rewrite match successes : 64
% 1.96/0.80 % Condensation attempts : 0
% 1.96/0.80 % Condensation successes : 0
% 1.96/0.80 % Termbank termtop insertions : 261497
% 1.96/0.80 % Search garbage collected termcells : 5231
% 1.96/0.80
% 1.96/0.80 % -------------------------------------------------
% 1.96/0.80 % User time : 0.330 s
% 1.96/0.80 % System time : 0.019 s
% 1.96/0.80 % Total time : 0.349 s
% 1.96/0.80 % Maximum resident set size: 5840 pages
% 1.96/0.80
% 1.96/0.80 % -------------------------------------------------
% 1.96/0.80 % User time : 1.653 s
% 1.96/0.80 % System time : 0.125 s
% 1.96/0.80 % Total time : 1.777 s
% 1.96/0.80 % Maximum resident set size: 5888 pages
% 1.96/0.80 % E exiting
%------------------------------------------------------------------------------