%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : PUZ065+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 : n003.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:29 PM UTC 2026
% Result : Satisfiable 11.88s 3.00s
% Output : Saturation 11.88s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named ax355ERROR: Could not build tree for root c_0_141ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_141,plain,
ssA(n2,n4) = n3,
inference(split_conjunct,[status(thm)],[ax355]),
[final] ).
cnf(c_0_145,plain,
ssA(n5,n3) = n3,
inference(split_conjunct,[status(thm)],[ax362]),
[final] ).
cnf(c_0_149,plain,
ssA(n9,n4) = n7,
inference(split_conjunct,[status(thm)],[ax368]),
[final] ).
cnf(c_0_151,plain,
ssA(n5,n1) = n7,
inference(split_conjunct,[status(thm)],[ax361]),
[final] ).
cnf(c_0_156,plain,
ssA(n7,n4) = n6,
inference(split_conjunct,[status(thm)],[ax365]),
[final] ).
cnf(c_0_160,plain,
ssA(n4,n5) = n1,
inference(split_conjunct,[status(thm)],[ax358]),
[final] ).
cnf(c_0_162,plain,
ssA(n1,n2) = n1,
inference(split_conjunct,[status(thm)],[ax353]),
[final] ).
cnf(c_0_168,plain,
ssA(n4,n6) = n2,
inference(split_conjunct,[status(thm)],[ax359]),
[final] ).
cnf(c_0_170,plain,
n1 != n3,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_171,plain,
n2 != n3,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_178,plain,
n1 != n7,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_179,plain,
n2 != n7,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_186,plain,
n1 != n6,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_187,plain,
n2 != n6,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_192,plain,
ssA(n6,n1) = n5,
inference(split_conjunct,[status(thm)],[ax363]),
[final] ).
cnf(c_0_197,plain,
n1 != n5,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_200,plain,
ssA(n3,n7) = n6,
inference(split_conjunct,[status(thm)],[ax357]),
[final] ).
cnf(c_0_203,plain,
n3 != n7,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_205,plain,
n3 != n6,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_206,plain,
n6 != n7,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_210,plain,
ssA(n6,n3) = 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_191,c_0_151]),c_0_145]),c_0_192]),c_0_193]),c_0_194]),c_0_195]),c_0_178]),c_0_196]),c_0_170]),c_0_197]),c_0_198]),
[final] ).
cnf(c_0_211,plain,
n5 != n6,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_229,plain,
ssA(n4,n7) = n4,
inference(split_conjunct,[status(thm)],[ax360]),
[final] ).
cnf(c_0_245,plain,
n2 != n5,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_246,plain,
n1 != n2,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_251,plain,
n4 != n7,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_252,plain,
n3 != n4,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_253,plain,
n4 != n5,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_254,plain,
n1 != n4,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_262,plain,
ssA(n8,n8) = n2,
inference(split_conjunct,[status(thm)],[ax367]),
[final] ).
cnf(c_0_263,plain,
ssA(n9,n8) = n5,
inference(split_conjunct,[status(thm)],[ax369]),
[final] ).
cnf(c_0_272,plain,
n2 != n4,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_274,plain,
n4 != n6,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_288,plain,
ssA(n1,n9) = n9,
inference(split_conjunct,[status(thm)],[ax354]),
[final] ).
cnf(c_0_299,plain,
ssA(n2,n7) = n8,
inference(split_conjunct,[status(thm)],[ax356]),
[final] ).
cnf(c_0_327,plain,
ssA(n6,n8) = n6,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_213,c_0_320]),c_0_206]),c_0_205]),
[final] ).
cnf(c_0_345,plain,
n2 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_346,plain,
n5 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_358,plain,
ssA(n7,n1) = n8,
inference(split_conjunct,[status(thm)],[ax364]),
[final] ).
cnf(c_0_381,plain,
n2 != n8,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_382,plain,
n5 != n8,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_405,plain,
n6 != n8,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_415,plain,
n3 != n5,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_417,plain,
n5 != n7,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_460,plain,
ssA(n4,n4) = n5,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_436,c_0_437]),c_0_203]),
[final] ).
cnf(c_0_489,plain,
n8 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_490,plain,
n6 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_491,plain,
n4 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_520,plain,
ssA(n5,n2) = n2,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_493,c_0_465]),c_0_494]),
[final] ).
cnf(c_0_522,plain,
ssA(n7,n8) = n9,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_493,c_0_466]),c_0_495]),
[final] ).
cnf(c_0_544,plain,
n1 != n8,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_570,plain,
n1 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_574,plain,
ssA(n8,n5) = n4,
inference(split_conjunct,[status(thm)],[ax366]),
[final] ).
cnf(c_0_624,plain,
n4 != n8,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_663,plain,
ssA(n1,n7) = n2,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_493,c_0_621]),c_0_640]),
[final] ).
cnf(c_0_699,plain,
ssA(n7,n9) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_667,c_0_522]),c_0_491]),
[final] ).
cnf(c_0_732,plain,
ssA(n3,n4) = n2,
inference(sr,[status(thm)],[c_0_559,c_0_694]),
[final] ).
cnf(c_0_759,plain,
ssA(n9,n1) = n1,
inference(sr,[status(thm)],[c_0_722,c_0_694]),
[final] ).
cnf(c_0_778,plain,
ssA(n1,n4) = n4,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_740,c_0_741]),c_0_694]),
[final] ).
cnf(c_0_793,plain,
n3 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_841,plain,
ssA(n9,n3) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_774,c_0_759]),c_0_254]),
[final] ).
cnf(c_0_845,plain,
ssA(n9,n7) = n3,
inference(sr,[status(thm)],[c_0_795,c_0_796]),
[final] ).
cnf(c_0_865,plain,
ssA(n5,n9) = n1,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_811,c_0_663]),c_0_245]),
[final] ).
cnf(c_0_867,plain,
ssA(n2,n1) = n2,
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_814,c_0_759]),c_0_246]),c_0_815]),c_0_816]),
[final] ).
cnf(c_0_871,plain,
ssA(n5,n6) = n4,
inference(sr,[status(thm)],[c_0_820,c_0_821]),
[final] ).
cnf(c_0_873,plain,
n3 != n8,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_891,plain,
n7 != n8,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_895,plain,
ssA(n9,n5) = n2,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_840,c_0_759]),c_0_246]),c_0_841]),c_0_272]),
[final] ).
cnf(c_0_913,plain,
ssA(n2,n8) = n4,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_866,c_0_867]),c_0_868]),c_0_869]),c_0_870]),c_0_272]),c_0_871])]),
[final] ).
cnf(c_0_917,plain,
ssA(n5,n8) = n8,
inference(sr,[status(thm)],[c_0_876,c_0_877]),
[final] ).
cnf(c_0_935,plain,
n7 != n9,
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
cnf(c_0_936,plain,
ssA(n7,n3) = n2,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_894,c_0_895])]),
[final] ).
cnf(c_0_937,plain,
ssA(n7,n7) = n1,
inference(sr,[status(thm)],[c_0_896,c_0_694]),
[final] ).
cnf(c_0_946,plain,
ssA(n2,n6) = n1,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_911,c_0_912]),c_0_913]),c_0_254]),
[final] ).
cnf(c_0_948,plain,
ssA(n3,n8) = n1,
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_916,c_0_522]),c_0_570]),c_0_917]),c_0_913]),c_0_544]),c_0_254]),
[final] ).
cnf(c_0_970,plain,
ssA(n7,n2) = n7,
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_934,c_0_522]),c_0_935]),c_0_936]),c_0_937]),c_0_699]),c_0_179]),c_0_178]),c_0_251]),
[final] ).
cnf(c_0_976,plain,
ssA(n1,n6) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_945,c_0_871]),c_0_274]),c_0_946]),c_0_186]),
[final] ).
cnf(c_0_997,plain,
ssA(n8,n4) = n1,
inference(sr,[status(thm)],[c_0_586,c_0_694]),
[final] ).
cnf(c_0_1031,plain,
ssA(n1,n1) = n3,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1007,c_0_815]),c_0_1008]),c_0_1009]),
[final] ).
cnf(c_0_1060,plain,
ssA(n4,n9) = n7,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1030,c_0_1031])]),
[final] ).
cnf(c_0_1092,plain,
ssA(n1,n5) = n5,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1059,c_0_1060]),c_0_203]),
[final] ).
cnf(c_0_1094,plain,
ssA(n5,n5) = n6,
inference(sr,[status(thm)],[c_0_1062,c_0_821]),
[final] ).
cnf(c_0_1164,plain,
ssA(n8,n2) = n3,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1001,c_0_1031])]),
[final] ).
cnf(c_0_1165,plain,
ssA(n7,n6) = n5,
inference(sr,[status(thm)],[c_0_1127,c_0_1128]),
[final] ).
cnf(c_0_1199,plain,
ssA(n8,n3) = n5,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1163,c_0_1164]),c_0_415]),c_0_1165])]),
[final] ).
cnf(c_0_1203,plain,
ssA(n2,n5) = n9,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1167,c_0_1092]),c_0_382]),
[final] ).
cnf(c_0_1205,plain,
ssA(n1,n8) = n7,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1170,c_0_1031])]),
[final] ).
cnf(c_0_1222,plain,
ssA(n6,n2) = n4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_271,c_0_520]),c_0_272]),
[final] ).
cnf(c_0_1262,plain,
ssA(n2,n9) = n5,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1169,c_0_1205]),c_0_203]),
[final] ).
cnf(c_0_1273,plain,
ssA(n2,n2) = n6,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_1236,c_0_1237]),c_0_1238]),c_0_1239]),
[final] ).
cnf(c_0_1286,plain,
ssA(n5,n7) = n5,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_620,c_0_663]),c_0_245]),
[final] ).
cnf(c_0_1287,plain,
ssA(n6,n4) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_672,c_0_663]),c_0_245]),
[final] ).
cnf(c_0_1288,plain,
ssA(n6,n7) = n9,
inference(sr,[status(thm)],[c_0_362,c_0_1256]),
[final] ).
cnf(c_0_1289,plain,
ssA(n6,n9) = n2,
inference(sr,[status(thm)],[c_0_1257,c_0_1256]),
[final] ).
cnf(c_0_1290,plain,
ssA(n8,n7) = n7,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1258,c_0_937]),c_0_178]),
[final] ).
cnf(c_0_1298,plain,
ssA(n1,n3) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1269,c_0_1092]),c_0_382]),
[final] ).
cnf(c_0_1300,plain,
ssA(n4,n3) = n6,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1272,c_0_1273])]),
[final] ).
cnf(c_0_1306,plain,
ssA(n6,n5) = n7,
inference(sr,[status(thm)],[c_0_1279,c_0_1128]),
[final] ).
cnf(c_0_1307,plain,
ssA(n4,n1) = n9,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1280,c_0_1273])]),
[final] ).
cnf(c_0_1311,plain,
ssA(n8,n9) = n8,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1284,c_0_1273])]),
[final] ).
cnf(c_0_1313,plain,
ssA(n2,n3) = n7,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1291,c_0_1273])]),c_0_1292]),c_0_1293]),c_0_869]),c_0_1294]),
[final] ).
cnf(c_0_1314,plain,
ssA(n3,n1) = n4,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1295,c_0_1140]),c_0_1296]),
[final] ).
cnf(c_0_1315,plain,
ssA(n3,n2) = n5,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1297,c_0_1298]),c_0_382]),c_0_1239]),c_0_1199])]),c_0_1293]),
[final] ).
cnf(c_0_1316,plain,
ssA(n3,n3) = n9,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_1299,c_0_1292]),c_0_1300]),c_0_1199]),c_0_490]),c_0_346]),
[final] ).
cnf(c_0_1317,plain,
ssA(n3,n5) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1130,c_0_1092]),c_0_382]),
[final] ).
cnf(c_0_1318,plain,
ssA(n3,n6) = n7,
inference(sr,[status(thm)],[c_0_1301,c_0_1128]),
[final] ).
cnf(c_0_1319,plain,
ssA(n3,n9) = n3,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1302,c_0_1205]),c_0_203]),
[final] ).
cnf(c_0_1320,plain,
ssA(n4,n2) = n8,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1303,c_0_1031])]),
[final] ).
cnf(c_0_1321,plain,
ssA(n4,n8) = n3,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1304,c_0_1031])]),
[final] ).
cnf(c_0_1322,plain,
ssA(n5,n4) = n9,
inference(sr,[status(thm)],[c_0_1305,c_0_821]),
[final] ).
cnf(c_0_1323,plain,
ssA(n6,n6) = n3,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_201,c_0_1306]),c_0_203]),
[final] ).
cnf(c_0_1324,plain,
ssA(n7,n5) = n3,
inference(sr,[status(thm)],[c_0_1090,c_0_1128]),
[final] ).
cnf(c_0_1325,plain,
ssA(n8,n1) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1253,c_0_1307]),c_0_490]),
[final] ).
cnf(c_0_1326,plain,
ssA(n8,n6) = n9,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1308,c_0_1273])]),
[final] ).
cnf(c_0_1327,plain,
ssA(n9,n2) = n9,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1309,c_0_1273])]),
[final] ).
cnf(c_0_1328,plain,
ssA(n9,n6) = n8,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_1310,c_0_1307]),c_0_490]),
[final] ).
cnf(c_0_1329,plain,
ssA(n9,n9) = n6,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_279,c_0_1311]),c_0_405]),
[final] ).
cnf(c_0_1330,plain,
ssP(n3,n1,n8,n4,n5,n6,n2,n7,n9,n2,n6,n7,n3,n9,n1,n8,n4,n5,n4,n5,n9,n2,n8,n7,n6,n1,n3,n9,n8,n6,n5,n1,n2,n4,n3,n7,n7,n2,n3,n9,n6,n4,n5,n8,n1,n5,n4,n1,n8,n7,n3,n9,n6,n2,n8,n7,n2,n6,n3,n5,n1,n9,n4,n6,n3,n5,n1,n4,n9,n7,n2,n8,n1,n9,n4,n7,n2,n8,n3,n5,n6),
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)],[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_1312,c_0_867]),c_0_1031]),c_0_1298]),c_0_778]),c_0_1092]),c_0_976]),c_0_1205]),c_0_1273]),c_0_1313]),c_0_1203]),c_0_946]),c_0_913]),c_0_1262]),c_0_1314]),c_0_1315]),c_0_1316]),c_0_1317]),c_0_1318]),c_0_948]),c_0_1319]),c_0_1307]),c_0_1320]),c_0_1300]),c_0_1321]),c_0_1060]),c_0_1322]),c_0_1094]),c_0_871]),c_0_1306]),c_0_1323]),c_0_970]),c_0_936]),c_0_1324]),c_0_1165]),c_0_1325]),c_0_1164]),c_0_1199]),c_0_1326]),c_0_1311]),c_0_1327]),c_0_895]),c_0_1328]),c_0_1329]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PUZ065+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.45 % Computer : n003.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 03:51:15 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.51 Running first-order theorem proving
% 0.20/0.51 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
% 11.88/3.00 % Version: 3.5.1
% 11.88/3.00 % Preprocessing class: FSLSSMSMSSSNFFN.
% 11.88/3.00 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 11.88/3.00 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 11.88/3.00 % Starting new_bool_3 with 300s (1) cores
% 11.88/3.00 % Starting new_bool_1 with 300s (1) cores
% 11.88/3.00 % Starting sh5l with 300s (1) cores
% 11.88/3.00 % new_bool_1 with pid 3342134 completed with status 9
% 11.88/3.00 % sh5l with pid 3342135 completed with status 9
% 11.88/3.00 % new_bool_3 with pid 3342133 completed with status 9
% 11.88/3.00 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 3342132 completed with status 1
% 11.88/3.00 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 11.88/3.00 % Preprocessing class: FSLSSMSMSSSNFFN.
% 11.88/3.00 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 11.88/3.00 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 11.88/3.00 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 11.88/3.00 % No SInE strategy applied
% 11.88/3.00 % Search class: FGUSF-SSLM22-SFFFFFNN
% 11.88/3.00 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 11.88/3.00 % Starting SubtermCWHack with 136s (1) cores
% 11.88/3.00 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 11.88/3.00 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 11.88/3.00 % Starting new_bool_3 with 136s (1) cores
% 11.88/3.00 % Starting new_bool_1 with 136s (1) cores
% 11.88/3.00 % new_bool_3 with pid 3342156 completed with status 1
% 11.88/3.00 % Result found by new_bool_3
% 11.88/3.00 % Preprocessing class: FSLSSMSMSSSNFFN.
% 11.88/3.00 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 11.88/3.00 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 11.88/3.00 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 11.88/3.00 % No SInE strategy applied
% 11.88/3.00 % Search class: FGUSF-SSLM22-SFFFFFNN
% 11.88/3.00 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 11.88/3.00 % Starting SubtermCWHack with 136s (1) cores
% 11.88/3.00 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 11.88/3.00 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 11.88/3.00 % Starting new_bool_3 with 136s (1) cores
% 11.88/3.00 % Preprocessing time : 0.021 s
% 11.88/3.00 % Presaturation interreduction done
% 11.88/3.00
% 11.88/3.00 % No proof found!
% 11.88/3.00 % SZS status Satisfiable
% 11.88/3.00 % SZS output start Saturation
% See solution above
% 11.88/3.00 % Parsed axioms : 370
% 11.88/3.00 % Removed by relevancy pruning/SinE : 0
% 11.88/3.00 % Initial clauses : 1350
% 11.88/3.00 % Removed in clause preprocessing : 0
% 11.88/3.00 % Initial clauses in saturation : 1350
% 11.88/3.00 % Processed clauses : 15698
% 11.88/3.00 % ...of these trivial : 703
% 11.88/3.00 % ...subsumed : 9972
% 11.88/3.00 % ...remaining for further processing : 5023
% 11.88/3.00 % Other redundant clauses eliminated : 0
% 11.88/3.00 % Clauses deleted for lack of memory : 0
% 11.88/3.00 % Backward-subsumed : 1131
% 11.88/3.00 % Backward-rewritten : 2299
% 11.88/3.00 % Generated clauses : 43533
% 11.88/3.00 % ...of the previous two non-redundant : 43627
% 11.88/3.00 % ...aggressively subsumed : 0
% 11.88/3.00 % Contextual simplify-reflections : 71
% 11.88/3.00 % Paramodulations : 42647
% 11.88/3.00 % Factorizations : 460
% 11.88/3.00 % NegExts : 0
% 11.88/3.00 % Equation resolutions : 0
% 11.88/3.00 % Disequality decompositions : 0
% 11.88/3.00 % Total rewrite steps : 6260
% 11.88/3.00 % ...of those cached : 6179
% 11.88/3.00 % Propositional unsat checks : 1
% 11.88/3.00 % Propositional check models : 1
% 11.88/3.00 % Propositional check unsatisfiable : 0
% 11.88/3.00 % Propositional clauses : 0
% 11.88/3.00 % Propositional clauses after purity: 0
% 11.88/3.00 % Propositional unsat core size : 0
% 11.88/3.00 % Propositional preprocessing time : 0.000
% 11.88/3.00 % Propositional encoding time : 0.036
% 11.88/3.00 % Propositional solver time : 0.006
% 11.88/3.00 % Success case prop preproc time : 0.000
% 11.88/3.00 % Success case prop encoding time : 0.000
% 11.88/3.00 % Success case prop solver time : 0.000
% 11.88/3.00 % Current number of processed clauses : 118
% 11.88/3.00 % Positive orientable unit clauses : 82
% 11.88/3.00 % Positive unorientable unit clauses: 0
% 11.88/3.00 % Negative unit clauses : 36
% 11.88/3.00 % Non-unit-clauses : 0
% 11.88/3.00 % Current number of unprocessed clauses: 0
% 11.88/3.00 % ...number of literals in the above : 0
% 11.88/3.00 % Current number of archived formulas : 0
% 11.88/3.00 % Current number of archived clauses : 4905
% 11.88/3.00 % Clause-clause subsumption calls (NU) : 61444
% 11.88/3.00 % Rec. Clause-clause subsumption calls : 4758
% 11.88/3.00 % Non-unit clause-clause subsumptions : 1413
% 11.88/3.00 % Unit Clause-clause subsumption calls : 128841
% 11.88/3.00 % Rewrite failures with RHS unbound : 0
% 11.88/3.00 % BW rewrite match attempts : 64
% 11.88/3.00 % BW rewrite match successes : 64
% 11.88/3.00 % Condensation attempts : 0
% 11.88/3.00 % Condensation successes : 0
% 11.88/3.00 % Termbank termtop insertions : 1312331
% 11.88/3.00 % Search garbage collected termcells : 5231
% 11.88/3.00
% 11.88/3.00 % -------------------------------------------------
% 11.88/3.00 % User time : 2.261 s
% 11.88/3.00 % System time : 0.056 s
% 11.88/3.00 % Total time : 2.317 s
% 11.88/3.00 % Maximum resident set size: 5636 pages
% 11.88/3.00
% 11.88/3.00 % -------------------------------------------------
% 11.88/3.00 % User time : 11.277 s
% 11.88/3.00 % System time : 0.317 s
% 11.88/3.00 % Total time : 11.594 s
% 11.88/3.00 % Maximum resident set size: 5888 pages
% 11.88/3.00 % E exiting
%------------------------------------------------------------------------------