%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN539+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 : Tue Sep 29 02:17:31 PM UTC 2026
% Result : CounterSatisfiable 0.10s 0.26s
% Output : Saturation 0.10s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u421,negated_conjecture,
~ c4_0 ).
cnf(u424,negated_conjecture,
~ ndr1_0 ).
cnf(u445,negated_conjecture,
c4_2(a637,a638) ).
cnf(u449,negated_conjecture,
~ c3_0 ).
cnf(u454,negated_conjecture,
c1_2(a637,a638) ).
cnf(u458,negated_conjecture,
ndr1_1(a637) ).
cnf(u464,negated_conjecture,
c2_1(a637) ).
cnf(u469,negated_conjecture,
c3_1(a637) ).
cnf(u478,negated_conjecture,
c2_0 ).
cnf(u481,negated_conjecture,
~ c5_0 ).
cnf(u490,negated_conjecture,
~ c1_0 ).
cnf(u494,negated_conjecture,
( ndr1_1(X39)
| ~ c2_2(X39,a635)
| ~ c1_2(X39,X40)
| c2_2(X39,X40)
| ~ c5_1(X39) ) ).
cnf(u497,negated_conjecture,
~ c2_1(a634) ).
cnf(u502,negated_conjecture,
~ sP0 ).
cnf(u506,negated_conjecture,
( ndr1_1(X37)
| ~ c3_2(X37,a632)
| ~ c2_1(X37)
| c3_2(X37,X38)
| ~ c5_2(X37,X38)
| ~ c1_2(X37,X38) ) ).
cnf(u510,negated_conjecture,
( ndr1_1(X37)
| ~ c2_2(X37,a632)
| ~ c2_1(X37)
| c3_2(X37,X38)
| ~ c5_2(X37,X38)
| ~ c1_2(X37,X38) ) ).
cnf(u515,negated_conjecture,
c3_1(a631) ).
cnf(u520,negated_conjecture,
c1_1(a631) ).
cnf(u525,negated_conjecture,
sP1 ).
cnf(u529,negated_conjecture,
( c5_2(X35,a628)
| ~ c4_1(X35)
| c2_2(X35,X36)
| ndr1_1(X35)
| c3_2(X35,X36)
| ~ c1_2(X35,X36) ) ).
cnf(u533,negated_conjecture,
( ndr1_1(X35)
| ~ c4_1(X35)
| ~ c1_2(X35,a628)
| c2_2(X35,X36)
| c3_2(X35,X36)
| ~ c1_2(X35,X36) ) ).
cnf(u537,negated_conjecture,
( ~ c4_2(X35,a628)
| ~ c4_1(X35)
| c2_2(X35,X36)
| ndr1_1(X35)
| c3_2(X35,X36)
| ~ c1_2(X35,X36) ) ).
cnf(u541,negated_conjecture,
( c1_2(X33,a627)
| ndr1_1(X33)
| ~ c3_2(X33,X34)
| ~ c1_2(X33,X34)
| c5_2(X33,X34)
| c3_1(X33) ) ).
cnf(u544,negated_conjecture,
sP2 ).
cnf(u549,negated_conjecture,
( ndr1_1(X33)
| c3_1(X33)
| ~ c3_2(X33,X34)
| ~ c1_2(X33,X34)
| c5_2(X33,X34)
| ~ c2_2(X33,a627) ) ).
cnf(u553,negated_conjecture,
( ndr1_1(X31)
| ~ c3_2(X31,a623)
| ~ c2_2(X31,X32)
| c1_2(X31,X32)
| c4_2(X31,X32)
| c3_1(X31) ) ).
cnf(u557,negated_conjecture,
( c4_1(X29)
| c2_1(X29)
| ndr1_1(X29)
| c4_2(X29,X30)
| ~ c1_2(X29,X30)
| c2_2(X29,X30) ) ).
cnf(u561,negated_conjecture,
( ~ c5_2(X28,a622)
| c2_1(X28)
| ~ sP3(X28) ) ).
cnf(u568,negated_conjecture,
( ~ c1_2(X28,a622)
| c2_1(X28)
| ~ sP3(X28) ) ).
cnf(u572,negated_conjecture,
( ~ sP3(X28)
| ~ ndr1_1(X28)
| c2_1(X28) ) ).
cnf(u577,negated_conjecture,
~ c4_1(a620) ).
cnf(u584,negated_conjecture,
c5_1(a619) ).
cnf(u589,negated_conjecture,
c1_1(a619) ).
cnf(u594,negated_conjecture,
c4_1(a619) ).
cnf(u623,negated_conjecture,
~ c2_1(a616) ).
cnf(u628,negated_conjecture,
~ c1_1(a616) ).
cnf(u633,negated_conjecture,
~ c3_1(a616) ).
cnf(u639,negated_conjecture,
~ ndr1_1(a615) ).
cnf(u652,negated_conjecture,
~ c1_1(a615) ).
cnf(u657,negated_conjecture,
~ ndr1_1(a613) ).
cnf(u664,negated_conjecture,
( c5_1(X20)
| c3_1(X20) ) ).
cnf(u669,negated_conjecture,
~ c3_2(a613,a614) ).
cnf(u674,negated_conjecture,
c4_2(a613,a614) ).
cnf(u679,negated_conjecture,
c1_2(a613,a614) ).
cnf(u685,negated_conjecture,
c3_1(a613) ).
cnf(u690,negated_conjecture,
~ c1_1(a611) ).
cnf(u694,negated_conjecture,
~ ndr1_1(a611) ).
cnf(u703,negated_conjecture,
~ c1_2(a611,a612) ).
cnf(u708,negated_conjecture,
~ c5_2(a611,a612) ).
cnf(u717,negated_conjecture,
sP4 ).
cnf(u721,negated_conjecture,
( ndr1_1(X16)
| c3_1(X16)
| ~ c1_1(X16)
| ~ c4_2(X16,X17)
| ~ c5_2(X16,X17) ) ).
cnf(u741,negated_conjecture,
ndr1_1(a605) ).
cnf(u752,negated_conjecture,
( ndr1_1(X7)
| ~ c1_1(X7)
| ~ c4_2(X7,X8)
| c5_2(X7,X8)
| c1_2(X7,X8) ) ).
cnf(u768,negated_conjecture,
sP8 ).
cnf(u771,negated_conjecture,
( c5_2(X5,a599)
| ~ c2_1(X5)
| ~ sP7(X5) ) ).
cnf(u775,negated_conjecture,
( ~ c3_2(X5,a599)
| ~ c2_1(X5)
| ~ sP7(X5) ) ).
cnf(u787,negated_conjecture,
sP9 ).
cnf(u791,negated_conjecture,
( c1_1(X3)
| ~ c2_1(X3)
| ndr1_1(X3)
| c3_2(X3,X4)
| ~ c2_2(X3,X4) ) ).
cnf(u795,negated_conjecture,
( ndr1_1(X1)
| ~ c1_2(X1,a595)
| c5_2(X1,X2)
| c2_2(X1,X2)
| ~ c1_1(X1) ) ).
cnf(u799,negated_conjecture,
( c4_2(X1,a595)
| ndr1_1(X1)
| c5_2(X1,X2)
| c2_2(X1,X2)
| ~ c1_1(X1) ) ).
cnf(u804,negated_conjecture,
c4_1(a594) ).
cnf(u807,negated_conjecture,
~ sP10 ).
cnf(u811,negated_conjecture,
~ sP11 ).
cnf(u817,negated_conjecture,
c1_1(a594) ).
cnf(u826,negated_conjecture,
sP12 ).
cnf(u832,negated_conjecture,
c5_1(a587) ).
cnf(u836,negated_conjecture,
c3_1(a587) ).
cnf(u841,negated_conjecture,
c2_1(a587) ).
cnf(u848,axiom,
~ c1_1(a633) ).
cnf(u852,axiom,
~ ndr1_1(a633) ).
cnf(u861,axiom,
c3_1(a633) ).
cnf(u866,axiom,
c3_1(a629) ).
cnf(u871,axiom,
~ c2_1(a629) ).
cnf(u876,axiom,
~ c5_2(a629,a630) ).
cnf(u882,axiom,
~ c2_2(a629,a630) ).
cnf(u887,axiom,
~ ndr1_1(a629) ).
cnf(u893,axiom,
~ c4_2(a624,a626) ).
cnf(u898,axiom,
~ c3_2(a624,a626) ).
cnf(u903,axiom,
~ c5_2(a624,a626) ).
cnf(u908,axiom,
~ ndr1_1(a624) ).
cnf(u913,axiom,
~ c2_2(a624,a625) ).
cnf(u918,axiom,
~ c1_2(a624,a625) ).
cnf(u922,axiom,
~ c3_2(a624,a625) ).
cnf(u933,axiom,
~ c4_2(a608,a609) ).
cnf(u939,axiom,
~ c5_2(a608,a609) ).
cnf(u944,axiom,
~ ndr1_1(a608) ).
cnf(u957,axiom,
( ~ c5_2(X0,a601)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u961,axiom,
( c2_2(X0,a601)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u965,axiom,
( ~ c4_2(X0,a601)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u969,axiom,
( ~ ndr1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u973,axiom,
~ c2_2(a596,a598) ).
cnf(u978,axiom,
~ c4_2(a596,a598) ).
cnf(u983,axiom,
~ c1_2(a596,a598) ).
cnf(u989,axiom,
~ ndr1_1(a596) ).
cnf(u994,axiom,
~ c1_2(a596,a597) ).
cnf(u999,axiom,
~ c2_2(a596,a597) ).
cnf(u1004,axiom,
~ c5_2(a596,a597) ).
cnf(u1015,axiom,
~ c5_1(a593) ).
cnf(u1020,axiom,
~ c2_1(a593) ).
cnf(u1024,axiom,
~ ndr1_1(a593) ).
cnf(u1034,axiom,
~ c4_1(a592) ).
cnf(u1038,axiom,
~ ndr1_1(a592) ).
cnf(u1046,axiom,
~ c3_1(a592) ).
cnf(u1053,axiom,
~ c2_2(a588,a591) ).
cnf(u1058,axiom,
~ c5_2(a588,a591) ).
cnf(u1063,axiom,
~ ndr1_1(a588) ).
cnf(u1067,axiom,
~ c1_2(a588,a590) ).
cnf(u1072,axiom,
~ c2_2(a588,a590) ).
cnf(u1077,axiom,
~ c4_2(a588,a590) ).
cnf(u1083,axiom,
~ c3_2(a588,a589) ).
cnf(u1088,axiom,
~ c2_2(a588,a589) ).
cnf(u1094,axiom,
~ c1_2(a588,a589) ).
cnf(u1117,negated_conjecture,
~ c3_1(a615) ).
cnf(u1125,negated_conjecture,
~ c3_1(a611) ).
cnf(u1132,negated_conjecture,
c3_1(a605) ).
cnf(u1145,negated_conjecture,
~ c1_1(a613) ).
cnf(u1157,negated_conjecture,
~ ndr1_1(a619) ).
cnf(u1162,negated_conjecture,
~ c2_1(a619) ).
cnf(u1166,negated_conjecture,
( c3_2(a615,X0)
| ~ c2_2(a615,X0) ) ).
cnf(u1169,negated_conjecture,
c2_1(a615) ).
cnf(u1178,negated_conjecture,
~ c2_1(a613) ).
cnf(u1186,negated_conjecture,
~ c2_1(a611) ).
cnf(u1197,negated_conjecture,
~ c1_1(a637) ).
cnf(u1204,negated_conjecture,
~ c1_2(a637,a595) ).
cnf(u1213,negated_conjecture,
( ~ c5_2(a619,X0)
| ~ c4_2(a619,X0) ) ).
cnf(u1216,negated_conjecture,
~ c3_1(a619) ).
cnf(u1221,negated_conjecture,
( c5_2(a619,X0)
| c2_2(a619,X0) ) ).
cnf(u1225,negated_conjecture,
~ c1_2(a619,a595) ).
cnf(u1240,negated_conjecture,
~ c2_2(a619,a635) ).
cnf(u1244,negated_conjecture,
c5_1(a615) ).
cnf(u1252,negated_conjecture,
~ c2_2(a615,a635) ).
cnf(u1257,negated_conjecture,
~ c5_1(a613) ).
cnf(u1264,negated_conjecture,
~ c2_2(a613,a635) ).
cnf(u1268,negated_conjecture,
c5_1(a611) ).
cnf(u1276,negated_conjecture,
~ c2_2(a611,a635) ).
cnf(u1289,negated_conjecture,
( c5_2(a619,X0)
| c1_2(a619,X0)
| ~ c4_2(a619,X0) ) ).
cnf(u1297,negated_conjecture,
~ sP3(a619) ).
cnf(u1301,negated_conjecture,
~ c4_2(a619,a622) ).
cnf(u1304,negated_conjecture,
~ c1_2(a619,a622) ).
cnf(u1316,negated_conjecture,
ndr1_1(a620) ).
cnf(u1320,negated_conjecture,
c2_1(a620) ).
cnf(u1344,negated_conjecture,
~ c1_2(a619,a628) ).
cnf(u1352,negated_conjecture,
~ c1_2(a615,a628) ).
cnf(u1356,negated_conjecture,
~ c4_1(a615) ).
cnf(u1364,negated_conjecture,
~ c1_2(a613,a628) ).
cnf(u1368,negated_conjecture,
~ c4_1(a613) ).
cnf(u1376,negated_conjecture,
~ c1_2(a611,a628) ).
cnf(u1379,negated_conjecture,
c4_1(a611) ).
cnf(u1390,negated_conjecture,
( c4_2(a613,X0)
| c2_2(a613,X0)
| ~ c1_2(a613,X0) ) ).
cnf(u1403,negated_conjecture,
~ c2_2(a619,a627) ).
cnf(u1416,negated_conjecture,
~ c3_2(a619,a623) ).
cnf(u1425,negated_conjecture,
~ c2_1(a633) ).
cnf(u1442,negated_conjecture,
~ c3_2(a633,a623) ).
cnf(u1447,negated_conjecture,
~ c2_2(a633,a627) ).
cnf(u1458,negated_conjecture,
~ c1_2(a633,a628) ).
cnf(u1461,negated_conjecture,
c4_1(a633) ).
cnf(u1467,negated_conjecture,
~ c5_1(a633) ).
cnf(u1474,negated_conjecture,
~ c2_2(a633,a635) ).
cnf(u1495,negated_conjecture,
~ c1_1(a629) ).
cnf(u1502,negated_conjecture,
~ c1_2(a629,a595) ).
cnf(u1518,negated_conjecture,
~ c3_2(a629,a623) ).
cnf(u1523,negated_conjecture,
~ c2_2(a629,a627) ).
cnf(u1534,negated_conjecture,
~ c1_2(a629,a628) ).
cnf(u1538,negated_conjecture,
~ c4_1(a629) ).
cnf(u1543,negated_conjecture,
~ c5_1(a629) ).
cnf(u1550,negated_conjecture,
~ c2_2(a629,a635) ).
cnf(u1556,negated_conjecture,
( c4_2(a629,X0)
| c2_2(a629,X0)
| ~ c1_2(a629,X0) ) ).
cnf(u1564,negated_conjecture,
~ c2_2(a629,a632) ).
cnf(u1569,negated_conjecture,
~ c3_2(a629,a632) ).
cnf(u1590,negated_conjecture,
~ c1_1(a624) ).
cnf(u1597,negated_conjecture,
~ c1_2(a624,a595) ).
cnf(u1609,negated_conjecture,
c3_1(a624) ).
cnf(u1617,negated_conjecture,
~ c3_2(a624,a623) ).
cnf(u1622,negated_conjecture,
~ c2_2(a624,a627) ).
cnf(u1633,negated_conjecture,
~ c1_2(a624,a628) ).
cnf(u1637,negated_conjecture,
~ c4_1(a624) ).
cnf(u1645,negated_conjecture,
~ c2_1(a624) ).
cnf(u1649,negated_conjecture,
~ c2_2(a624,a632) ).
cnf(u1654,negated_conjecture,
~ c3_2(a624,a632) ).
cnf(u1659,negated_conjecture,
~ c5_1(a624) ).
cnf(u1666,negated_conjecture,
~ c2_2(a624,a635) ).
cnf(u1672,negated_conjecture,
( c4_2(a624,X0)
| c2_2(a624,X0)
| ~ c1_2(a624,X0) ) ).
cnf(u1693,negated_conjecture,
~ c1_1(a608) ).
cnf(u1700,negated_conjecture,
~ c1_2(a608,a595) ).
cnf(u1712,negated_conjecture,
c3_1(a608) ).
cnf(u1720,negated_conjecture,
~ c3_2(a608,a623) ).
cnf(u1725,negated_conjecture,
~ c2_2(a608,a627) ).
cnf(u1736,negated_conjecture,
~ c1_2(a608,a628) ).
cnf(u1739,negated_conjecture,
c4_1(a608) ).
cnf(u1748,negated_conjecture,
~ c2_1(a608) ).
cnf(u1752,negated_conjecture,
~ c2_2(a608,a632) ).
cnf(u1757,negated_conjecture,
~ c3_2(a608,a632) ).
cnf(u1762,negated_conjecture,
~ c5_1(a608) ).
cnf(u1769,negated_conjecture,
~ c2_2(a608,a635) ).
cnf(u1783,negated_conjecture,
~ c1_1(a596) ).
cnf(u1790,negated_conjecture,
~ c1_2(a596,a595) ).
cnf(u1801,negated_conjecture,
~ c3_1(a596) ).
cnf(u1810,negated_conjecture,
~ c3_2(a596,a623) ).
cnf(u1815,negated_conjecture,
~ c2_2(a596,a627) ).
cnf(u1826,negated_conjecture,
~ c1_2(a596,a628) ).
cnf(u1829,negated_conjecture,
c4_1(a596) ).
cnf(u1838,negated_conjecture,
~ c2_1(a596) ).
cnf(u1842,negated_conjecture,
~ c2_2(a596,a632) ).
cnf(u1847,negated_conjecture,
~ c3_2(a596,a632) ).
cnf(u1851,negated_conjecture,
c5_1(a596) ).
cnf(u1859,negated_conjecture,
~ c2_2(a596,a635) ).
cnf(u1890,negated_conjecture,
~ c1_1(a593) ).
cnf(u1897,negated_conjecture,
~ c1_2(a593,a595) ).
cnf(u1909,negated_conjecture,
~ c1_2(a593,a628) ).
cnf(u1912,negated_conjecture,
c4_1(a593) ).
cnf(u1923,negated_conjecture,
c2_1(a592) ).
cnf(u1942,negated_conjecture,
~ c1_1(a592) ).
cnf(u1949,negated_conjecture,
~ c1_2(a592,a595) ).
cnf(u1965,negated_conjecture,
~ c3_2(a592,a623) ).
cnf(u1970,negated_conjecture,
~ c2_2(a592,a627) ).
cnf(u1981,negated_conjecture,
~ c2_2(a592,a632) ).
cnf(u1986,negated_conjecture,
~ c3_2(a592,a632) ).
cnf(u1990,negated_conjecture,
c5_1(a592) ).
cnf(u1998,negated_conjecture,
~ c2_2(a592,a635) ).
cnf(u2003,negated_conjecture,
( c3_2(a592,X0)
| ~ c2_2(a592,X0) ) ).
cnf(u2012,negated_conjecture,
sP7(a592) ).
cnf(u2017,negated_conjecture,
~ c2_2(a592,a599) ).
cnf(u2032,negated_conjecture,
~ c1_1(a588) ).
cnf(u2039,negated_conjecture,
~ c1_2(a588,a595) ).
cnf(u2051,negated_conjecture,
c3_1(a588) ).
cnf(u2059,negated_conjecture,
~ c3_2(a588,a623) ).
cnf(u2064,negated_conjecture,
~ c2_2(a588,a627) ).
cnf(u2075,negated_conjecture,
~ c1_2(a588,a628) ).
cnf(u2079,negated_conjecture,
~ c4_1(a588) ).
cnf(u2087,negated_conjecture,
~ c2_1(a588) ).
cnf(u2091,negated_conjecture,
~ c2_2(a588,a632) ).
cnf(u2096,negated_conjecture,
~ c3_2(a588,a632) ).
cnf(u2101,negated_conjecture,
~ c5_1(a588) ).
cnf(u2108,negated_conjecture,
~ c2_2(a588,a635) ).
cnf(u2114,negated_conjecture,
( c4_2(a588,X0)
| c2_2(a588,X0)
| ~ c1_2(a588,X0) ) ).
cnf(u2174,negated_conjecture,
~ c3_2(a611,a623) ).
cnf(u2179,negated_conjecture,
~ c2_2(a611,a627) ).
cnf(u2198,negated_conjecture,
~ c1_1(a587) ).
cnf(u2217,negated_conjecture,
~ c5_1(a634) ).
cnf(u2224,negated_conjecture,
~ c2_2(a634,a635) ).
cnf(u2228,negated_conjecture,
c5_1(a616) ).
cnf(u2236,negated_conjecture,
~ c2_2(a616,a635) ).
cnf(u2244,negated_conjecture,
~ c2_2(a587,a635) ).
cnf(u2268,negated_conjecture,
~ c1_1(a634) ).
cnf(u2303,negated_conjecture,
~ c1_2(a634,a628) ).
cnf(u2306,negated_conjecture,
c4_1(a634) ).
cnf(u2315,negated_conjecture,
~ c1_2(a616,a628) ).
cnf(u2318,negated_conjecture,
c4_1(a616) ).
cnf(u2327,negated_conjecture,
~ c1_2(a587,a628) ).
cnf(u2331,negated_conjecture,
~ c4_1(a587) ).
cnf(u2339,negated_conjecture,
~ ndr1_1(a634) ).
cnf(u2348,negated_conjecture,
~ ndr1_1(a616) ).
cnf(u2358,negated_conjecture,
ndr1_1(a587) ).
cnf(u2388,negated_conjecture,
~ c3_2(a616,a623) ).
cnf(u2393,negated_conjecture,
~ c2_2(a616,a627) ).
cnf(u2419,negated_conjecture,
~ c1_2(a624,a626) ).
cnf(u2422,negated_conjecture,
~ c2_2(a624,a626) ).
cnf(u2437,negated_conjecture,
~ c2_2(a619,a603) ).
cnf(u2442,negated_conjecture,
~ sP6(a619) ).
cnf(u2474,negated_conjecture,
c3_1(a620) ).
cnf(u2479,negated_conjecture,
c2_1(a605) ).
cnf(u2490,negated_conjecture,
~ c1_2(a615,a595) ).
cnf(u2502,negated_conjecture,
~ c3_2(a615,a632) ).
cnf(u2507,negated_conjecture,
~ c2_2(a615,a632) ).
cnf(u2525,negated_conjecture,
~ c3_2(a615,a623) ).
cnf(u2530,negated_conjecture,
~ c2_2(a615,a627) ).
cnf(u2545,negated_conjecture,
~ c5_1(a605) ).
cnf(u2552,negated_conjecture,
~ c2_2(a605,a635) ).
cnf(u2560,negated_conjecture,
~ c1_1(a605) ).
cnf(u2568,negated_conjecture,
~ c1_2(a605,a595) ).
cnf(u2576,negated_conjecture,
~ c1_2(a605,a628) ).
cnf(u2580,negated_conjecture,
~ c4_1(a605) ).
cnf(u2592,negated_conjecture,
sP7(a615) ).
cnf(u2597,negated_conjecture,
~ c2_2(a615,a599) ).
cnf(u2469,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c2_2(X0,a632)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u2150,negated_conjecture,
( c2_1(X0)
| ~ c1_2(X0,a595)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c1_1(X0) ) ).
cnf(u2149,negated_conjecture,
( c2_1(X0)
| ~ c1_1(X0)
| ~ c4_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(u264,axiom,
( ~ sP6(X0)
| ~ ndr1_1(X0) ) ).
cnf(u2451,negated_conjecture,
~ c2_2(a619,a621) ).
cnf(u278,axiom,
( sP3(X0)
| c1_2(X0,a621) ) ).
cnf(u1293,negated_conjecture,
( ~ c4_2(a619,X0)
| c1_2(a619,X0) ) ).
cnf(u277,axiom,
( sP3(X0)
| ~ ndr1_1(X0) ) ).
cnf(u270,axiom,
( sP5(X0)
| ~ c1_2(X0,a604) ) ).
cnf(u2460,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c1_2(X0,a595)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c1_1(X0) ) ).
cnf(u265,axiom,
( ~ c5_2(X0,a603)
| ~ sP6(X0) ) ).
cnf(u2146,negated_conjecture,
( c3_1(X0)
| c2_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,a627) ) ).
cnf(u84,axiom,
( c3_2(X0,a603)
| ~ sP6(X0) ) ).
cnf(u2148,negated_conjecture,
( c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u261,axiom,
( sP7(X0)
| c1_2(X0,a600) ) ).
cnf(u1322,negated_conjecture,
( ~ c4_2(a619,X0)
| c2_2(a619,X0) ) ).
cnf(u2459,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c4_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(u262,axiom,
( sP7(X0)
| ~ c3_2(X0,a600) ) ).
cnf(u2246,negated_conjecture,
c3_1(a634) ).
cnf(u280,axiom,
( sP3(X0)
| ~ c2_2(X0,a621) ) ).
cnf(u2007,negated_conjecture,
~ c2_2(a592,a623) ).
cnf(u1877,negated_conjecture,
c3_1(a593) ).
cnf(u2467,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c3_2(X0,a623)
| ~ c2_2(X0,X1)
| c1_2(X0,X1)
| c4_2(X0,X1) ) ).
cnf(u2142,negated_conjecture,
( c2_1(X0)
| ~ c2_2(X0,a635)
| ~ c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(u279,axiom,
( sP3(X0)
| ~ c4_2(X0,a621) ) ).
cnf(u2470,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c3_2(X0,a632)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u2588,negated_conjecture,
~ c2_2(a615,a623) ).
cnf(u2145,negated_conjecture,
( c2_1(X0)
| ~ c4_1(X0)
| ~ c1_2(X0,a628)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u2151,negated_conjecture,
c2_1(a605) ).
cnf(u2141,negated_conjecture,
( ~ ndr1_1(X0)
| c2_1(X0) ) ).
cnf(u263,axiom,
( sP7(X0)
| c2_2(X0,a600) ) ).
cnf(u260,axiom,
( sP7(X0)
| ~ ndr1_1(X0) ) ).
cnf(u2466,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u267,axiom,
( sP5(X0)
| ~ ndr1_1(X0) ) ).
cnf(u268,axiom,
( sP5(X0)
| ~ c4_2(X0,a604) ) ).
cnf(u2452,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c2_2(X0,a635)
| ~ c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(u2449,negated_conjecture,
~ c4_2(a619,a621) ).
cnf(u2147,negated_conjecture,
( c3_1(X0)
| ~ c3_2(X0,a623)
| ~ c2_2(X0,X1)
| c1_2(X0,X1)
| c4_2(X0,X1)
| c2_1(X0) ) ).
cnf(u2455,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c4_1(X0)
| ~ c1_2(X0,a628)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u394,negated_conjecture,
~ c5_0 ).
cnf(u2447,negated_conjecture,
c1_2(a619,a621) ).
cnf(u266,axiom,
( c4_2(X0,a603)
| ~ sP6(X0) ) ).
cnf(u2468,negated_conjecture,
( c3_1(X0)
| ~ c2_1(X0)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,a627) ) ).
cnf(u269,axiom,
( sP5(X0)
| c3_2(X0,a604) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN539+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n004.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 16:26:52 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 Running first-order model finding
% 0.10/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.26 % (502061)Will run a generic schedule for satisfiability detection.
% 0.10/0.26 % (502072)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1342551799:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.10/0.26 % (502067)% WARNING: option uhcvi not known.
% 0.10/0.26 % (502066)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1070909961_2999 on theBenchmark for (2999ds/0Mi)
% 0.10/0.26 % (502070)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=506177074:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.10/0.26 % (502069)dis+10_1_sil=32000:sp=arity:random_seed=3163052268:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.10/0.26 % (502068)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3692539909:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.10/0.26 % (502071)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=269413570:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.10/0.26 % (502067)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3143957943:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.10/0.26 % (502072) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-502061-502072"...
% 0.10/0.26 % (502072)...printing done.
% 0.10/0.26 % SZS status CounterSatisfiable for theBenchmark
% 0.10/0.26 % SZS output start Saturation.
% See solution above
% 0.10/0.26 % SZS output start Definitions and Model Updates.
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP12"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP9"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP7"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP5"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP4"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP3"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP2"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "sP1"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c5_0"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c3_0"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c2_0"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c5_2"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c4_2"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "ndr1_1"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c3_1"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c2_1"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "ndr1_0"
% 0.10/0.26 globally flip the polarity of every occurrence of predicate "c4_0"
% 0.10/0.26 % SZS output end Definitions and Model Updates.
% 0.10/0.26 % (502072)------------------------------
% 0.10/0.26 % (502072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.26 % (502072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.26 % (502072)CaDiCaL version: 2.1.3
% 0.10/0.26 % (502072)Termination reason: Satisfiable
% 0.10/0.26 % (502072)Time elapsed: 0.014 s
% 0.10/0.26 % (502072)Peak memory usage: 13 MB
% 0.10/0.26 % (502072)Instructions burned: 36 (million)
% 0.10/0.26 % (502061)Success in time 0.045 s
% 0.10/0.26 % Vampire exiting
%------------------------------------------------------------------------------