%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN421-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 : n012.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:07:49 PM UTC 2026
% Result : Satisfiable 0.08s 0.16s
% Output : Saturation 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1026,negated_conjecture,
~ c6_0 ).
cnf(u1032,negated_conjecture,
ndr1_0 ).
cnf(u1045,negated_conjecture,
~ ndr1_1(a566) ).
cnf(u1054,negated_conjecture,
~ ssSkC23 ).
cnf(u1067,negated_conjecture,
~ c4_0 ).
cnf(u1078,negated_conjecture,
( ~ c10_2(X0,X2)
| c1_1(X0)
| c3_1(X0)
| c1_2(X0,X2)
| ~ ndr1_1(X0)
| c6_2(X0,X2) ) ).
cnf(u1083,negated_conjecture,
~ c3_1(a566) ).
cnf(u1088,negated_conjecture,
~ c10_0 ).
cnf(u1092,negated_conjecture,
~ c8_0 ).
cnf(u1111,negated_conjecture,
~ ssSkC2 ).
cnf(u1123,negated_conjecture,
c7_0 ).
cnf(u1146,negated_conjecture,
c9_0 ).
cnf(u1162,negated_conjecture,
~ c1_0 ).
cnf(u1166,negated_conjecture,
( ~ c7_1(X0)
| c2_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c10_2(X0,X2)
| ~ c4_2(X0,X1)
| c3_2(X0,X1)
| c4_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1173,negated_conjecture,
( ~ c7_1(X0)
| ~ c3_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u1176,negated_conjecture,
~ ssSkC22 ).
cnf(u1224,negated_conjecture,
~ c1_2(a502,a503) ).
cnf(u1240,negated_conjecture,
ssSkC24 ).
cnf(u1244,negated_conjecture,
( ~ c5_2(X0,X1)
| c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ssSkP10(X0) ) ).
cnf(u1263,negated_conjecture,
~ c3_0 ).
cnf(u1267,negated_conjecture,
( ~ ssSkP2(X0)
| c6_2(X0,X1)
| c10_2(X0,a487)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| ~ c8_2(X0,X1) ) ).
cnf(u1282,negated_conjecture,
~ c9_1(a502) ).
cnf(u1287,negated_conjecture,
c5_1(a502) ).
cnf(u1292,negated_conjecture,
c8_2(a502,a503) ).
cnf(u1315,negated_conjecture,
( ~ c8_2(X0,a593)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1318,negated_conjecture,
~ ssSkC29 ).
cnf(u1322,negated_conjecture,
ssSkC28 ).
cnf(u1327,negated_conjecture,
( ~ c6_2(X0,a593)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1331,negated_conjecture,
( ~ c5_2(X0,a593)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_1(X0)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1335,negated_conjecture,
( ~ c6_2(X0,a604)
| c6_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c6_1(X0)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1338,negated_conjecture,
ssSkC32 ).
cnf(u1342,negated_conjecture,
~ ssSkC31 ).
cnf(u1347,negated_conjecture,
( ~ c9_2(X0,a568)
| ssSkP10(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u1355,negated_conjecture,
( ~ c9_2(X0,a487)
| ~ ssSkP2(X0)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1)
| ~ c8_2(X0,X1) ) ).
cnf(u1364,negated_conjecture,
ssSkC9 ).
cnf(u1377,negated_conjecture,
ndr1_1(a502) ).
cnf(u1393,negated_conjecture,
( ~ c10_2(X0,a604)
| c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1397,negated_conjecture,
( ~ c6_1(X0)
| c3_2(X0,a604)
| c6_2(X0,X1)
| ~ c4_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1406,negated_conjecture,
~ ssSkC10 ).
cnf(u1413,negated_conjecture,
~ ssSkC11 ).
cnf(u1417,negated_conjecture,
( ~ c3_2(X0,X1)
| c3_2(X0,a508)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ssSkP4(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u1421,negated_conjecture,
( ~ c2_2(X0,a508)
| ssSkP4(X0)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u1425,negated_conjecture,
( ~ c3_2(X0,X1)
| c7_2(X0,a508)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ssSkP4(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u1429,negated_conjecture,
ssSkC21 ).
cnf(u1433,negated_conjecture,
( ~ c10_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c5_1(X0)
| c2_2(X0,a548) ) ).
cnf(u1437,negated_conjecture,
( ~ c6_2(X0,a548)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1)
| c3_2(X0,X1)
| c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1442,negated_conjecture,
~ c5_0 ).
cnf(u1449,negated_conjecture,
c2_0 ).
cnf(u1453,negated_conjecture,
( ~ c7_1(X0)
| c1_1(X0)
| c9_2(X0,X1)
| c6_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1457,negated_conjecture,
( ~ c10_1(X0)
| ~ ndr1_1(X0)
| c7_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1)
| c9_2(X0,a459) ) ).
cnf(u1483,negated_conjecture,
( ~ c9_2(X0,a548)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1)
| c3_2(X0,X1)
| c5_1(X0) ) ).
cnf(u1488,negated_conjecture,
ssSkC27 ).
cnf(u1503,negated_conjecture,
( ~ c10_1(X0)
| ~ ndr1_1(X0)
| c8_2(X0,a459)
| c7_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u1507,negated_conjecture,
( ~ c2_2(X0,a459)
| ~ c10_1(X0)
| ~ ndr1_1(X0)
| c7_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u1511,negated_conjecture,
( ~ c10_1(X0)
| ~ c6_2(X0,X1)
| ~ c5_1(X0)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1522,negated_conjecture,
~ ssSkC6 ).
cnf(u1527,negated_conjecture,
( ~ c1_2(X0,a530)
| c1_2(X0,X1)
| ssSkP6(X0)
| ~ ndr1_1(X0)
| c10_2(X0,X1) ) ).
cnf(u1539,negated_conjecture,
ssSkC12 ).
cnf(u1543,negated_conjecture,
( ~ c2_2(X0,a512)
| ~ ssSkP5(X0)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u1547,negated_conjecture,
( ~ ssSkP5(X0)
| c1_2(X0,a512)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u1551,negated_conjecture,
( ~ ssSkP5(X0)
| c7_2(X0,a512)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u1564,negated_conjecture,
~ ndr1_1(a470) ).
cnf(u1570,negated_conjecture,
ssSkC3 ).
cnf(u1576,negated_conjecture,
~ ndr1_1(a473) ).
cnf(u1582,negated_conjecture,
ssSkC4 ).
cnf(u1587,negated_conjecture,
( c10_2(X0,X1)
| c6_2(X0,a530)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ssSkP6(X0) ) ).
cnf(u1591,negated_conjecture,
( ~ c9_2(X0,a530)
| ssSkP6(X0)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| c10_2(X0,X1) ) ).
cnf(u1624,negated_conjecture,
ssSkC30 ).
cnf(u1692,negated_conjecture,
( ~ c3_2(X0,a528)
| ~ c2_1(X0)
| c5_1(X0) ) ).
cnf(u1695,negated_conjecture,
ssSkC15 ).
cnf(u1700,negated_conjecture,
( c2_2(X0,a528)
| ~ c2_1(X0)
| c5_1(X0) ) ).
cnf(u1704,negated_conjecture,
( c4_2(X0,a528)
| ~ c2_1(X0)
| c5_1(X0) ) ).
cnf(u1715,negated_conjecture,
ssSkC18 ).
cnf(u1720,negated_conjecture,
~ ssSkC17 ).
cnf(u1725,negated_conjecture,
~ ndr1_1(a556) ).
cnf(u1733,negated_conjecture,
~ ndr1_1(a584) ).
cnf(u1748,negated_conjecture,
( ~ c6_2(X0,a450)
| ~ c1_1(X0)
| c5_1(X0) ) ).
cnf(u1751,negated_conjecture,
ssSkC0 ).
cnf(u1756,negated_conjecture,
( ~ c8_2(X0,a450)
| ~ c1_1(X0)
| c5_1(X0) ) ).
cnf(u1767,negated_conjecture,
ssSkC1 ).
cnf(u1852,negated_conjecture,
( ~ c9_2(X0,a450)
| c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1870,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0)
| c5_1(X0) ) ).
cnf(u1910,negated_conjecture,
ssSkC16 ).
cnf(u1914,negated_conjecture,
( ~ c1_2(X0,a532)
| ~ c1_1(X0)
| ssSkP7(X0) ) ).
cnf(u1918,negated_conjecture,
( c4_2(X0,a532)
| ~ c1_1(X0)
| ssSkP7(X0) ) ).
cnf(u1923,negated_conjecture,
~ ssSkC20 ).
cnf(u1973,negated_conjecture,
ssSkC8 ).
cnf(u1985,negated_conjecture,
ssSkC13 ).
cnf(u1996,negated_conjecture,
( c5_1(X0)
| ndr1_1(X0)
| ~ c1_1(X0) ) ).
cnf(u2008,negated_conjecture,
( c10_2(X0,a545)
| c2_1(X0)
| ~ c7_1(X0) ) ).
cnf(u2011,negated_conjecture,
~ ssSkC19 ).
cnf(u2016,negated_conjecture,
( c4_2(X0,a545)
| c2_1(X0)
| ~ c7_1(X0) ) ).
cnf(u2026,negated_conjecture,
~ ssSkC5 ).
cnf(u2030,negated_conjecture,
( ~ c6_2(X0,a474)
| c9_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2038,negated_conjecture,
( ~ c9_2(X0,a532)
| ssSkP7(X0)
| ~ c1_1(X0) ) ).
cnf(u2042,negated_conjecture,
( ~ c3_2(X0,a536)
| c6_1(X0)
| c2_1(X0) ) ).
cnf(u2046,negated_conjecture,
( c4_2(X0,a536)
| c6_1(X0)
| c2_1(X0) ) ).
cnf(u2082,negated_conjecture,
( ~ c6_1(X0)
| ~ c7_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2094,negated_conjecture,
( c7_2(X0,a474)
| c9_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2098,negated_conjecture,
( c8_2(X0,a474)
| c9_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2102,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0)
| ~ c1_1(X0) ) ).
cnf(u2106,negated_conjecture,
( ~ c9_2(X0,a536)
| c6_1(X0)
| c2_1(X0) ) ).
cnf(u2140,negated_conjecture,
( ~ c7_1(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u2148,negated_conjecture,
( ~ c10_1(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u2152,negated_conjecture,
( c2_1(X0)
| c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u2248,negated_conjecture,
~ c6_2(a494,a495) ).
cnf(u2253,negated_conjecture,
c9_2(a494,a495) ).
cnf(u2414,negated_conjecture,
~ c5_2(a489,a490) ).
cnf(u2417,negated_conjecture,
~ ssSkC7 ).
cnf(u2423,negated_conjecture,
~ c1_2(a489,a490) ).
cnf(u2428,negated_conjecture,
c2_2(a489,a490) ).
cnf(u2433,negated_conjecture,
~ c1_1(a494) ).
cnf(u2438,negated_conjecture,
c4_1(a494) ).
cnf(u2443,negated_conjecture,
~ c10_2(a494,a495) ).
cnf(u2533,negated_conjecture,
~ c3_1(a554) ).
cnf(u2538,negated_conjecture,
~ c2_1(a554) ).
cnf(u2563,negated_conjecture,
~ c8_2(a578,a579) ).
cnf(u2577,negated_conjecture,
ssSkC26 ).
cnf(u2647,negated_conjecture,
~ ssSkC14 ).
cnf(u2656,negated_conjecture,
ssSkC25 ).
cnf(u2722,negated_conjecture,
~ c2_1(a470) ).
cnf(u2727,negated_conjecture,
c9_1(a473) ).
cnf(u2732,negated_conjecture,
~ c7_1(a473) ).
cnf(u2767,negated_conjecture,
c10_1(a489) ).
cnf(u2772,negated_conjecture,
~ c6_1(a489) ).
cnf(u2777,negated_conjecture,
ndr1_1(a494) ).
cnf(u2889,negated_conjecture,
~ c8_1(a554) ).
cnf(u2894,negated_conjecture,
c8_1(a556) ).
cnf(u2899,negated_conjecture,
c5_1(a556) ).
cnf(u2926,negated_conjecture,
~ c6_1(a577) ).
cnf(u2931,negated_conjecture,
c8_1(a577) ).
cnf(u2936,negated_conjecture,
~ c1_1(a577) ).
cnf(u2941,negated_conjecture,
c8_1(a578) ).
cnf(u2946,negated_conjecture,
~ c2_2(a578,a579) ).
cnf(u2951,negated_conjecture,
c7_2(a578,a579) ).
cnf(u2961,negated_conjecture,
~ c6_1(a584) ).
cnf(u3086,negated_conjecture,
c5_1(a585) ).
cnf(u3117,negated_conjecture,
~ c8_1(a470) ).
cnf(u3130,negated_conjecture,
ndr1_1(a489) ).
cnf(u3202,negated_conjecture,
c1_1(a578) ).
cnf(u3207,negated_conjecture,
ndr1_1(a578) ).
cnf(u3213,negated_conjecture,
~ c8_1(a584) ).
cnf(u3334,negated_conjecture,
c9_1(a585) ).
cnf(u3411,negated_conjecture,
~ ndr1_1(a554) ).
cnf(u3416,negated_conjecture,
c6_1(a554) ).
cnf(u3422,negated_conjecture,
~ c5_1(a470) ).
cnf(u3432,negated_conjecture,
~ c5_1(a554) ).
cnf(u3447,negated_conjecture,
c5_1(a577) ).
cnf(u3459,negated_conjecture,
~ c5_1(a489) ).
cnf(u3472,negated_conjecture,
ssSkP6(a494) ).
cnf(u3526,negated_conjecture,
c9_2(a489,a459) ).
cnf(u3536,negated_conjecture,
c8_2(a489,a459) ).
cnf(u3560,negated_conjecture,
c3_1(a502) ).
cnf(u3565,negated_conjecture,
ssSkP6(a489) ).
cnf(u3597,negated_conjecture,
c6_2(a578,a530) ).
cnf(u3497,negated_conjecture,
( ~ c6_1(X0)
| c6_2(X0,X1)
| ~ c4_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| c6_2(X0,a530)
| c1_2(X0,a604)
| ssSkP6(X0) ) ).
cnf(clause75,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause138,negated_conjecture,
( c6_2(X0,a511)
| ssSkP5(X0) ) ).
cnf(u638,negated_conjecture,
( c5_2(X0,a542)
| ~ ssSkP8(X0) ) ).
cnf(u641,negated_conjecture,
( c3_2(X0,a529)
| ~ ssSkP6(X0) ) ).
cnf(u3519,negated_conjecture,
( ~ c2_2(X0,a545)
| c3_2(X0,a545)
| c5_1(X0)
| c2_2(X0,a548)
| c2_1(X0)
| ~ c7_1(X0) ) ).
cnf(u3514,negated_conjecture,
( ~ c4_2(X0,a529)
| c7_2(X0,a508)
| ssSkP4(X0)
| ~ c6_2(X0,a529)
| ~ ssSkP6(X0) ) ).
cnf(u730,negated_conjecture,
( c2_2(X0,a564)
| ~ ssSkP9(X0) ) ).
cnf(u642,negated_conjecture,
( ~ c2_2(X0,a529)
| ~ ssSkP6(X0) ) ).
cnf(u3492,negated_conjecture,
( ~ c7_2(X0,a531)
| c10_2(X0,a568)
| ~ c1_2(X0,a531)
| ssSkP10(X0)
| ~ ssSkP7(X0) ) ).
cnf(u743,negated_conjecture,
( c2_2(X0,a452)
| ssSkP1(X0) ) ).
cnf(u3518,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c3_2(X0,X1)
| c5_1(X0)
| c2_2(X0,a548)
| c6_2(X0,a530)
| c1_2(X0,X1)
| ssSkP6(X0) ) ).
cnf(u732,negated_conjecture,
( c10_2(X0,a531)
| ~ ssSkP7(X0) ) ).
cnf(u3488,negated_conjecture,
( c1_2(X0,a531)
| c3_1(X0)
| c1_1(X0)
| ~ ssSkP7(X0) ) ).
cnf(u3408,negated_conjecture,
c6_1(a470) ).
cnf(u3520,negated_conjecture,
( ~ c2_2(X0,a531)
| c3_2(X0,a531)
| c5_1(X0)
| c2_2(X0,a548)
| ~ ssSkP7(X0) ) ).
cnf(clause62,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u650,negated_conjecture,
( ~ c2_2(X0,a497)
| ssSkP3(X0) ) ).
cnf(u731,negated_conjecture,
( ~ c6_2(X0,a542)
| ~ ssSkP8(X0) ) ).
cnf(u728,negated_conjecture,
( ~ c3_2(X0,a567)
| ~ ssSkP10(X0) ) ).
cnf(u737,negated_conjecture,
( c2_2(X0,a486)
| ssSkP2(X0) ) ).
cnf(u3407,negated_conjecture,
( c6_1(X0)
| ndr1_1(X0)
| c5_1(X0) ) ).
cnf(clause244,negated_conjecture,
( ~ c1_2(X0,a486)
| ssSkP2(X0) ) ).
cnf(u729,negated_conjecture,
( c9_2(X0,a564)
| ~ ssSkP9(X0) ) ).
cnf(u640,negated_conjecture,
( c5_2(X0,a531)
| ~ ssSkP7(X0) ) ).
cnf(clause151,negated_conjecture,
( c1_2(X0,a452)
| ssSkP1(X0) ) ).
cnf(u735,negated_conjecture,
( c4_2(X0,a507)
| ~ ssSkP4(X0) ) ).
cnf(clause154,negated_conjecture,
( c7_2(X0,a451)
| ssSkP0(X0) ) ).
cnf(u651,negated_conjecture,
( ~ c9_2(X0,a497)
| ssSkP3(X0) ) ).
cnf(u585,negated_conjecture,
( ~ ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u657,negated_conjecture,
( ~ c9_2(X0,a452)
| ssSkP1(X0) ) ).
cnf(u3453,negated_conjecture,
c5_1(a584) ).
cnf(clause60,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(clause65,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u583,negated_conjecture,
( ~ ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(clause74,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u589,negated_conjecture,
( ~ ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u3401,negated_conjecture,
( ~ c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u3511,negated_conjecture,
( ~ c4_2(X0,a529)
| c3_2(X0,a508)
| ssSkP4(X0)
| ~ c6_2(X0,a529)
| ~ ssSkP6(X0) ) ).
cnf(u736,negated_conjecture,
( c4_2(X0,a497)
| ssSkP3(X0) ) ).
cnf(u643,negated_conjecture,
( c7_2(X0,a529)
| ~ ssSkP6(X0) ) ).
cnf(u636,negated_conjecture,
( c6_2(X0,a567)
| ~ ssSkP10(X0) ) ).
cnf(u738,negated_conjecture,
( c9_2(X0,a486)
| ssSkP2(X0) ) ).
cnf(u637,negated_conjecture,
( c1_2(X0,a542)
| ~ ssSkP8(X0) ) ).
cnf(u581,negated_conjecture,
( ~ ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(clause241,negated_conjecture,
( ~ c5_2(X0,a511)
| ssSkP5(X0) ) ).
cnf(u586,negated_conjecture,
( ~ ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u658,negated_conjecture,
( ~ c4_2(X0,a451)
| ssSkP0(X0) ) ).
cnf(u727,negated_conjecture,
( c2_2(X0,a567)
| ~ ssSkP10(X0) ) ).
cnf(u733,negated_conjecture,
( ~ c6_2(X0,a531)
| ~ ssSkP7(X0) ) ).
cnf(u3494,negated_conjecture,
( ~ c7_2(X0,a542)
| c10_2(X0,a568)
| ssSkP10(X0)
| ~ ssSkP8(X0) ) ).
cnf(u648,negated_conjecture,
( c6_2(X0,a507)
| ~ ssSkP4(X0) ) ).
cnf(u582,negated_conjecture,
( ~ ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u649,negated_conjecture,
( c3_2(X0,a507)
| ~ ssSkP4(X0) ) ).
cnf(u3486,negated_conjecture,
( c1_2(X0,a545)
| c3_1(X0)
| c1_1(X0)
| c6_2(X0,a545)
| c2_1(X0)
| ~ c7_1(X0) ) ).
cnf(u3485,negated_conjecture,
( ~ ndr1_1(X0)
| c3_1(X0)
| c1_2(X0,X1)
| c1_1(X0)
| c6_2(X0,X1)
| c6_2(X0,a530)
| ssSkP6(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN421-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 15:55:04 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.11 Running first-order model finding
% 0.08/0.11 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.08/0.16 % (3481977)Will run a generic schedule for satisfiability detection.
% 0.08/0.16 % (3481983)% WARNING: option uhcvi not known.
% 0.08/0.16 % (3481982)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4002713487_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.16 % (3481983)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2413769352:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.16 % (3481985)dis+10_1_sil=32000:sp=arity:random_seed=3510920103:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.16 % (3481984)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3250269049:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.16 % (3481988)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4288371761:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.16 % (3481986)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=637545751:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.16 % (3481987)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2595469053:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.16 % (3481983) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3481977-3481983"...
% 0.08/0.16 % (3481983)...printing done.
% 0.08/0.16 % Detected minimum model sizes of [1]
% 0.08/0.16 % Detected maximum model sizes of [159]
% 0.08/0.16 % TRYING [1]
% 0.08/0.16 % SZS status Satisfiable for theBenchmark
% 0.08/0.16 % SZS output start Saturation.
% See solution above
% 0.08/0.16 % SZS output start Definitions and Model Updates.
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC22"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC23"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC19"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c10_2"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC16"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c4_2"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c2_2"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC12"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC20"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC24"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c9_2"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c8_1"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c10_1"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkP4"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c4_1"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkP6"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkP7"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkP8"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkP9"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkP10"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c7_1"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC2"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC10"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC21"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c5_1"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c7_0"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c3_0"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC6"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC7"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC14"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC26"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC29"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "ssSkC31"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c9_0"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c4_0"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c5_0"
% 0.08/0.16 globally flip the polarity of every occurrence of predicate "c1_0"
% 0.08/0.16 % SZS output end Definitions and Model Updates.
% 0.08/0.16 % (3481983)------------------------------
% 0.08/0.16 % (3481983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.16 % (3481983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.16 % (3481983)CaDiCaL version: 2.1.3
% 0.08/0.16 % (3481983)Termination reason: Satisfiable
% 0.08/0.16 % (3481983)Time elapsed: 0.010 s
% 0.08/0.16 % (3481983)Peak memory usage: 13 MB
% 0.08/0.16 % (3481983)Instructions burned: 26 (million)
% 0.08/0.16 % (3481977)Success in time 0.042 s
% 0.08/0.16 % Vampire exiting
%------------------------------------------------------------------------------