%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : PUZ071+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:01:48 PM UTC 2026
% Result : Satisfiable 2.04s 0.96s
% Output : Saturation 2.04s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named ax357ERROR: Could not build tree for root c_0_140ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_136,plain,
ssA(n4,n3) = n1,
inference(split_conjunct,[status(thm)],[ax359]),
[final] ).
cnf(c_0_138,plain,
ssA(n8,n4) = n1,
inference(split_conjunct,[status(thm)],[ax367]),
[final] ).
cnf(c_0_140,plain,
ssA(n2,n9) = n1,
inference(split_conjunct,[status(thm)],[ax357]),
[final] ).
cnf(c_0_149,plain,
ssA(n1,n1) = n4,
inference(split_conjunct,[status(thm)],[ax353]),
[final] ).
cnf(c_0_150,plain,
ssA(n1,n2) = n5,
inference(split_conjunct,[status(thm)],[ax354]),
[final] ).
cnf(c_0_151,plain,
ssA(n1,n5) = n8,
inference(split_conjunct,[status(thm)],[ax355]),
[final] ).
cnf(c_0_152,plain,
n1 != n4,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_153,plain,
n1 != n5,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_156,plain,
n1 != n8,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_166,plain,
ssA(n1,n6) = 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)],[inference(rw,[status(thm)],[c_0_148,c_0_149]),c_0_150]),c_0_151]),c_0_152]),c_0_153]),c_0_154]),c_0_155]),c_0_156]),c_0_157]),c_0_158]),c_0_159]),
[final] ).
cnf(c_0_176,plain,
ssA(n5,n5) = n4,
inference(split_conjunct,[status(thm)],[ax363]),
[final] ).
cnf(c_0_184,plain,
ssA(n4,n8) = n3,
inference(split_conjunct,[status(thm)],[ax361]),
[final] ).
cnf(c_0_186,plain,
ssA(n8,n6) = n3,
inference(split_conjunct,[status(thm)],[ax368]),
[final] ).
cnf(c_0_196,plain,
ssA(n9,n4) = n7,
inference(split_conjunct,[status(thm)],[ax369]),
[final] ).
cnf(c_0_198,plain,
ssA(n2,n8) = n7,
inference(split_conjunct,[status(thm)],[ax356]),
[final] ).
cnf(c_0_202,plain,
ssA(n6,n5) = 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_175,c_0_151]),c_0_176]),c_0_156]),c_0_177]),c_0_178]),c_0_179]),c_0_152]),c_0_180]),c_0_181]),c_0_182]),
[final] ).
cnf(c_0_203,plain,
n3 != n8,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_205,plain,
n3 != n4,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_206,plain,
n1 != n3,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_212,plain,
ssA(n5,n7) = n2,
inference(split_conjunct,[status(thm)],[ax364]),
[final] ).
cnf(c_0_215,plain,
ssA(n3,n2) = n2,
inference(split_conjunct,[status(thm)],[ax358]),
[final] ).
cnf(c_0_225,plain,
n3 != n5,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_228,plain,
n4 != n7,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_229,plain,
n5 != n7,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_231,plain,
n7 != n8,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_232,plain,
n1 != n7,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_245,plain,
ssA(n4,n4) = n6,
inference(split_conjunct,[status(thm)],[ax360]),
[final] ).
cnf(c_0_250,plain,
n2 != n7,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_251,plain,
n1 != n2,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_256,plain,
ssA(n7,n7) = n8,
inference(split_conjunct,[status(thm)],[ax366]),
[final] ).
cnf(c_0_266,plain,
ssA(n1,n3) = 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)],[inference(rw,[status(thm)],[c_0_227,c_0_149]),c_0_150]),c_0_151]),c_0_166]),c_0_228]),c_0_229]),c_0_230]),c_0_231]),c_0_232]),c_0_233]),c_0_234]),c_0_235]),
[final] ).
cnf(c_0_267,plain,
n3 != n7,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_282,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_255,c_0_212]),c_0_256]),c_0_157]),c_0_257]),c_0_258]),c_0_259]),c_0_251]),c_0_260]),c_0_156]),c_0_261]),
[final] ).
cnf(c_0_284,plain,
n2 != n3,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_293,plain,
ssA(n7,n1) = n2,
inference(split_conjunct,[status(thm)],[ax365]),
[final] ).
cnf(c_0_319,plain,
n6 != n8,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_335,plain,
ssA(n6,n3) = n2,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(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_308,c_0_266]),c_0_136]),c_0_250]),c_0_309]),c_0_310]),c_0_251]),c_0_311]),c_0_312]),c_0_313]),c_0_314]),
[final] ).
cnf(c_0_344,plain,
ssA(n1,n4) = n9,
inference(sr,[status(thm)],[c_0_321,c_0_322]),
[final] ).
cnf(c_0_353,plain,
ssA(n1,n7) = n3,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_329,c_0_330]),c_0_306]),
[final] ).
cnf(c_0_362,plain,
n2 != n6,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_382,plain,
ssA(n3,n1) = 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)],[inference(rw,[status(thm)],[c_0_346,c_0_149]),c_0_150]),c_0_215]),c_0_152]),c_0_153]),c_0_154]),c_0_347]),c_0_348]),c_0_349]),c_0_251]),c_0_350]),
[final] ).
cnf(c_0_435,plain,
ssA(n2,n4) = n2,
inference(sr,[status(thm)],[c_0_397,c_0_322]),
[final] ).
cnf(c_0_452,plain,
ssA(n7,n2) = n1,
inference(sr,[status(thm)],[c_0_418,c_0_419]),
[final] ).
cnf(c_0_470,plain,
ssA(n5,n1) = n5,
inference(split_conjunct,[status(thm)],[ax362]),
[final] ).
cnf(c_0_471,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_439,c_0_198]),c_0_184]),c_0_158]),c_0_232]),c_0_440]),c_0_206]),c_0_441]),c_0_442]),c_0_443]),c_0_444]),
[final] ).
cnf(c_0_477,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_456,c_0_293]),c_0_452]),c_0_256]),c_0_250]),c_0_232]),c_0_457]),c_0_458]),c_0_413]),c_0_459]),c_0_231]),c_0_460]),
[final] ).
cnf(c_0_483,plain,
n2 != n8,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_488,plain,
ssA(n7,n3) = n3,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_476,c_0_477]),c_0_267]),
[final] ).
cnf(c_0_512,plain,
ssA(n4,n5) = n7,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_487,c_0_488])]),
[final] ).
cnf(c_0_540,plain,
n2 != n4,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_545,plain,
n2 != n5,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_552,plain,
ssA(n5,n2) = n7,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_511,c_0_512])]),c_0_513]),
[final] ).
cnf(c_0_561,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_520,c_0_138]),c_0_186]),c_0_196]),c_0_320]),c_0_521]),c_0_402]),c_0_156]),c_0_522]),c_0_203]),c_0_231]),c_0_523]),
[final] ).
cnf(c_0_575,plain,
n5 != n6,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_577,plain,
n4 != n6,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_578,plain,
n1 != n6,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_580,plain,
ssA(n4,n6) = n2,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_533,c_0_499]),c_0_534]),
[final] ).
cnf(c_0_582,plain,
n4 != n5,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_616,plain,
n3 != n6,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_621,plain,
ssA(n8,n1) = n7,
inference(sr,[status(thm)],[c_0_587,c_0_588]),
[final] ).
cnf(c_0_629,plain,
ssA(n5,n6) = n9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_594,c_0_595]),c_0_596]),
[final] ).
cnf(c_0_630,plain,
n8 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_631,plain,
n7 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_645,plain,
n6 != n7,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_650,plain,
n5 != n8,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_658,plain,
n4 != n8,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_692,plain,
ssA(n8,n2) = n8,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_656,c_0_657]),c_0_658]),c_0_650]),
[final] ).
cnf(c_0_702,plain,
ssA(n5,n4) = n3,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_663,c_0_660]),c_0_552]),c_0_267]),
[final] ).
cnf(c_0_731,plain,
ssA(n6,n4) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_338,c_0_702]),c_0_203]),
[final] ).
cnf(c_0_754,plain,
ssA(n5,n3) = n8,
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_709,c_0_693]),c_0_704]),c_0_710]),c_0_720]),
[final] ).
cnf(c_0_779,plain,
ssA(n1,n8) = n6,
inference(sr,[status(thm)],[c_0_746,c_0_747]),
[final] ).
cnf(c_0_800,plain,
ssA(n4,n7) = n5,
inference(sr,[status(thm)],[c_0_783,c_0_784]),
[final] ).
cnf(c_0_815,plain,
n2 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_816,plain,
n1 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_817,plain,
n3 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_823,plain,
ssA(n2,n5) = n5,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_799,c_0_800])]),
[final] ).
cnf(c_0_834,plain,
ssA(n4,n2) = n4,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_805,c_0_806]),c_0_807]),
[final] ).
cnf(c_0_842,plain,
ssA(n4,n1) = n9,
inference(sr,[status(thm)],[c_0_813,c_0_784]),
[final] ).
cnf(c_0_846,plain,
ssA(n7,n4) = n5,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_822,c_0_823])]),
[final] ).
cnf(c_0_875,plain,
ssA(n2,n2) = n3,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_841,c_0_842])]),
[final] ).
cnf(c_0_877,plain,
ssA(n7,n5) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_845,c_0_846]),c_0_582]),
[final] ).
cnf(c_0_878,plain,
n6 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_893,plain,
ssA(n2,n1) = n8,
inference(sr,[status(thm)],[c_0_859,c_0_860]),
[final] ).
cnf(c_0_910,plain,
ssA(n7,n8) = n9,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_876,c_0_877]),c_0_878]),
[final] ).
cnf(c_0_921,plain,
ssA(n9,n1) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_806,c_0_893]),c_0_203]),
[final] ).
cnf(c_0_923,plain,
ssA(n9,n9) = n3,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_642,c_0_477]),c_0_267]),
[final] ).
cnf(c_0_928,plain,
ssA(n6,n7) = n7,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_898,c_0_899]),c_0_900]),
[final] ).
cnf(c_0_929,plain,
ssA(n6,n6) = n5,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_901,c_0_731]),c_0_650]),
[final] ).
cnf(c_0_930,plain,
ssA(n6,n2) = n6,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_902,c_0_903]),c_0_904]),c_0_905]),c_0_906]),c_0_907]),
[final] ).
cnf(c_0_931,plain,
ssA(n6,n1) = n3,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_908,c_0_893]),c_0_203]),
[final] ).
cnf(c_0_933,plain,
n5 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_939,plain,
ssA(n3,n5) = n3,
inference(sr,[status(thm)],[c_0_237,c_0_666]),
[final] ).
cnf(c_0_940,plain,
ssA(n3,n6) = n7,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_913,c_0_512])]),
[final] ).
cnf(c_0_953,plain,
ssA(n9,n2) = n9,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_920,c_0_921])]),
[final] ).
cnf(c_0_956,plain,
ssA(n6,n9) = n9,
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)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_927,c_0_928]),c_0_631]),c_0_929]),c_0_930]),c_0_931]),c_0_932]),c_0_933]),c_0_878]),c_0_817]),
[final] ).
cnf(c_0_957,plain,
n4 != n9,
inference(split_conjunct,[status(thm)],[c_0_134]),
[final] ).
cnf(c_0_973,plain,
ssA(n3,n8) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_944,c_0_702]),c_0_203]),
[final] ).
cnf(c_0_989,plain,
ssA(n6,n8) = n4,
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_955,c_0_928]),c_0_228]),c_0_956]),c_0_930]),c_0_957]),c_0_577]),
[final] ).
cnf(c_0_999,plain,
ssA(n3,n4) = n4,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_605,c_0_823])]),
[final] ).
cnf(c_0_1008,plain,
ssA(n8,n5) = n9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_984,c_0_844]),c_0_877]),c_0_985]),c_0_878]),
[final] ).
cnf(c_0_1019,plain,
ssA(n3,n9) = n5,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_998,c_0_999]),c_0_582]),
[final] ).
cnf(c_0_1020,plain,
ssA(n3,n3) = n6,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1000,c_0_939]),c_0_616]),c_0_940]),c_0_645]),c_0_973]),c_0_1001]),c_0_319]),c_0_1002]),
[final] ).
cnf(c_0_1023,plain,
ssA(n8,n7) = n6,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1005,c_0_353]),c_0_616]),c_0_928]),c_0_645]),c_0_1002]),c_0_1006]),
[final] ).
cnf(c_0_1024,plain,
ssA(n8,n8) = n2,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1007,c_0_1008]),c_0_815]),
[final] ).
cnf(c_0_1025,plain,
ssA(n8,n3) = n5,
inference(sr,[status(thm)],[c_0_1009,c_0_1010]),
[final] ).
cnf(c_0_1028,plain,
ssA(n9,n3) = n4,
inference(sr,[status(thm)],[c_0_987,c_0_1010]),
[final] ).
cnf(c_0_1030,plain,
ssA(n1,n9) = n2,
inference(sr,[status(thm)],[c_0_1014,c_0_747]),
[final] ).
cnf(c_0_1031,plain,
ssA(n2,n3) = n9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1015,c_0_860]),c_0_1016]),
[final] ).
cnf(c_0_1032,plain,
ssA(n2,n6) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_967,c_0_823]),c_0_575]),
[final] ).
cnf(c_0_1033,plain,
ssA(n2,n7) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1017,c_0_823]),c_0_575]),
[final] ).
cnf(c_0_1034,plain,
ssA(n3,n7) = 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_1018,c_0_973]),c_0_630]),c_0_1019]),c_0_1020]),c_0_933]),c_0_878]),
[final] ).
cnf(c_0_1035,plain,
ssA(n4,n9) = n8,
inference(sr,[status(thm)],[c_0_752,c_0_784]),
[final] ).
cnf(c_0_1036,plain,
ssA(n5,n9) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1021,c_0_754]),c_0_319]),
[final] ).
cnf(c_0_1037,plain,
ssA(n7,n6) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_820,c_0_846]),c_0_582]),
[final] ).
cnf(c_0_1038,plain,
ssA(n8,n9) = n4,
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_1022,c_0_1023]),c_0_577]),c_0_1024]),c_0_1025]),c_0_540]),c_0_582]),
[final] ).
cnf(c_0_1039,plain,
ssA(n9,n5) = n2,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_950,c_0_1008]),c_0_815]),
[final] ).
cnf(c_0_1040,plain,
ssA(n9,n8) = n5,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_1026,c_0_1027]),c_0_1028]),c_0_582]),
[final] ).
cnf(c_0_1041,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)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1029,c_0_779]),c_0_1030]),c_0_893]),c_0_875]),c_0_1031]),c_0_823]),c_0_1032]),c_0_1033]),c_0_1020]),c_0_999]),c_0_1034]),c_0_1019]),c_0_842]),c_0_834]),c_0_800]),c_0_1035]),c_0_754]),c_0_1036]),c_0_931]),c_0_930]),c_0_989]),c_0_956]),c_0_846]),c_0_877]),c_0_1037]),c_0_910]),c_0_1025]),c_0_1008]),c_0_1023]),c_0_1024]),c_0_1038]),c_0_921]),c_0_953]),c_0_1028]),c_0_1039]),c_0_1040]),
[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/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n009.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 03:48:57 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.44 Running first-order theorem proving
% 0.15/0.44 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.04/0.96 % Version: 3.5.1
% 2.04/0.96 % Preprocessing class: FSLSSMSMSSSNFFN.
% 2.04/0.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.04/0.96 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 2.04/0.96 % Starting new_bool_3 with 300s (1) cores
% 2.04/0.96 % Starting new_bool_1 with 300s (1) cores
% 2.04/0.96 % Starting sh5l with 300s (1) cores
% 2.04/0.96 % sh5l with pid 777684 completed with status 9
% 2.04/0.96 % new_bool_3 with pid 777682 completed with status 9
% 2.04/0.96 % new_bool_1 with pid 777683 completed with status 9
% 2.04/0.96 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 777681 completed with status 1
% 2.04/0.96 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 2.04/0.96 % Preprocessing class: FSLSSMSMSSSNFFN.
% 2.04/0.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.04/0.96 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 2.04/0.96 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 2.04/0.96 % No SInE strategy applied
% 2.04/0.96 % Search class: FGUSF-SSLM22-SFFFFFNN
% 2.04/0.96 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 2.04/0.96 % Starting SubtermCWHack with 136s (1) cores
% 2.04/0.96 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 2.04/0.96 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 2.04/0.96 % Starting new_bool_3 with 136s (1) cores
% 2.04/0.96 % Starting new_bool_1 with 136s (1) cores
% 2.04/0.96 % SubtermCWHack with pid 777699 completed with status 1
% 2.04/0.96 % Result found by SubtermCWHack
% 2.04/0.96 % Preprocessing class: FSLSSMSMSSSNFFN.
% 2.04/0.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 2.04/0.96 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 2.04/0.96 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 2.04/0.96 % No SInE strategy applied
% 2.04/0.96 % Search class: FGUSF-SSLM22-SFFFFFNN
% 2.04/0.96 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 2.04/0.96 % Starting SubtermCWHack with 136s (1) cores
% 2.04/0.96 % Preprocessing time : 0.016 s
% 2.04/0.96
% 2.04/0.96 % No proof found!
% 2.04/0.96 % SZS status Satisfiable
% 2.04/0.96 % SZS output start Saturation
% See solution above
% 2.04/0.97 % Parsed axioms : 370
% 2.04/0.97 % Removed by relevancy pruning/SinE : 0
% 2.04/0.97 % Initial clauses : 1350
% 2.04/0.97 % Removed in clause preprocessing : 0
% 2.04/0.97 % Initial clauses in saturation : 1350
% 2.04/0.97 % Processed clauses : 5912
% 2.04/0.97 % ...of these trivial : 242
% 2.04/0.97 % ...subsumed : 3912
% 2.04/0.97 % ...remaining for further processing : 1758
% 2.04/0.97 % Other redundant clauses eliminated : 0
% 2.04/0.97 % Clauses deleted for lack of memory : 0
% 2.04/0.97 % Backward-subsumed : 215
% 2.04/0.97 % Backward-rewritten : 1315
% 2.04/0.97 % Generated clauses : 8251
% 2.04/0.97 % ...of the previous two non-redundant : 8686
% 2.04/0.97 % ...aggressively subsumed : 0
% 2.04/0.97 % Contextual simplify-reflections : 17
% 2.04/0.97 % Paramodulations : 7959
% 2.04/0.97 % Factorizations : 182
% 2.04/0.97 % NegExts : 0
% 2.04/0.97 % Equation resolutions : 0
% 2.04/0.97 % Disequality decompositions : 0
% 2.04/0.97 % Total rewrite steps : 3327
% 2.04/0.97 % ...of those cached : 3246
% 2.04/0.97 % Propositional unsat checks : 0
% 2.04/0.97 % Propositional check models : 0
% 2.04/0.97 % Propositional check unsatisfiable : 0
% 2.04/0.97 % Propositional clauses : 0
% 2.04/0.97 % Propositional clauses after purity: 0
% 2.04/0.97 % Propositional unsat core size : 0
% 2.04/0.97 % Propositional preprocessing time : 0.000
% 2.04/0.97 % Propositional encoding time : 0.000
% 2.04/0.97 % Propositional solver time : 0.000
% 2.04/0.97 % Success case prop preproc time : 0.000
% 2.04/0.97 % Success case prop encoding time : 0.000
% 2.04/0.97 % Success case prop solver time : 0.000
% 2.04/0.97 % Current number of processed clauses : 118
% 2.04/0.97 % Positive orientable unit clauses : 82
% 2.04/0.97 % Positive unorientable unit clauses: 0
% 2.04/0.97 % Negative unit clauses : 36
% 2.04/0.97 % Non-unit-clauses : 0
% 2.04/0.97 % Current number of unprocessed clauses: 0
% 2.04/0.97 % ...number of literals in the above : 0
% 2.04/0.97 % Current number of archived formulas : 0
% 2.04/0.97 % Current number of archived clauses : 1640
% 2.04/0.97 % Clause-clause subsumption calls (NU) : 2360
% 2.04/0.97 % Rec. Clause-clause subsumption calls : 1110
% 2.04/0.97 % Non-unit clause-clause subsumptions : 288
% 2.04/0.97 % Unit Clause-clause subsumption calls : 77835
% 2.04/0.97 % Rewrite failures with RHS unbound : 0
% 2.04/0.97 % BW rewrite match attempts : 64
% 2.04/0.97 % BW rewrite match successes : 64
% 2.04/0.97 % Condensation attempts : 0
% 2.04/0.97 % Condensation successes : 0
% 2.04/0.97 % Termbank termtop insertions : 168202
% 2.04/0.97 % Search garbage collected termcells : 5231
% 2.04/0.97
% 2.04/0.97 % -------------------------------------------------
% 2.04/0.97 % User time : 0.434 s
% 2.04/0.97 % System time : 0.015 s
% 2.04/0.97 % Total time : 0.449 s
% 2.04/0.97 % Maximum resident set size: 6148 pages
% 2.04/0.97
% 2.04/0.97 % -------------------------------------------------
% 2.04/0.97 % User time : 2.091 s
% 2.04/0.97 % System time : 0.141 s
% 2.04/0.97 % Total time : 2.232 s
% 2.04/0.97 % Maximum resident set size: 5632 pages
% 2.04/0.97 % E exiting
%------------------------------------------------------------------------------