%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN422-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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:50 PM UTC 2026
% Result : Satisfiable 0.21s 0.30s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1032,negated_conjecture,
~ c9_0 ).
cnf(u1038,negated_conjecture,
~ ndr1_0 ).
cnf(u1054,negated_conjecture,
~ c5_0 ).
cnf(u1061,negated_conjecture,
( ~ c8_1(X0)
| c7_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c5_2(X0,X2)
| c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u1070,negated_conjecture,
~ c3_0 ).
cnf(u1107,negated_conjecture,
~ c10_0 ).
cnf(u1112,negated_conjecture,
~ ndr1_1(a755) ).
cnf(u1122,negated_conjecture,
~ c2_0 ).
cnf(u1130,negated_conjecture,
( ~ c10_1(X0)
| ~ c10_2(X0,X1)
| c8_2(X0,X2)
| ~ c6_2(X0,X2)
| c3_2(X0,X2)
| ~ ndr1_1(X0)
| c9_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u1140,negated_conjecture,
~ c1_0 ).
cnf(u1157,negated_conjecture,
c7_0 ).
cnf(u1175,negated_conjecture,
( c3_2(X3,a704)
| c4_1(X3)
| ~ c7_1(X3) ) ).
cnf(u1181,negated_conjecture,
ssSkC19 ).
cnf(u1186,negated_conjecture,
( ~ c5_2(X3,a704)
| c4_1(X3)
| ~ c7_1(X3) ) ).
cnf(u1215,negated_conjecture,
( ~ c9_2(X3,a704)
| c4_1(X3)
| ~ c7_1(X3) ) ).
cnf(u1237,negated_conjecture,
( c8_2(X0,X1)
| ~ c3_2(X0,X1)
| c10_1(X0)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1240,negated_conjecture,
ssSkC26 ).
cnf(u1250,negated_conjecture,
c6_0 ).
cnf(u1264,negated_conjecture,
( c4_1(X3)
| ~ c7_1(X3)
| ndr1_1(X3) ) ).
cnf(u1268,negated_conjecture,
~ c8_0 ).
cnf(u1272,negated_conjecture,
( ~ c9_2(X0,a610)
| c1_2(X0,X1)
| c6_2(X0,X1)
| ~ c9_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ c2_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1275,negated_conjecture,
~ ssSkC0 ).
cnf(u1280,negated_conjecture,
( ~ c4_2(X0,X2)
| c4_2(X0,a610)
| c6_2(X0,X1)
| ~ c9_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1284,negated_conjecture,
( ~ c3_2(X0,a610)
| c1_2(X0,X1)
| c6_2(X0,X1)
| ~ c9_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ c2_2(X0,X2)
| ~ c5_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1292,negated_conjecture,
( ~ c8_1(X0)
| c3_2(X0,X1)
| ~ c8_2(X0,X2)
| c4_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,X2)
| ~ c10_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1295,negated_conjecture,
~ ssSkC9 ).
cnf(u1306,negated_conjecture,
c4_0 ).
cnf(u1356,negated_conjecture,
( c7_2(X0,X1)
| ~ c1_2(X0,X1)
| c9_1(X0)
| c10_1(X0)
| ~ ndr1_1(X0)
| c8_2(X0,X1) ) ).
cnf(u1359,negated_conjecture,
ssSkC12 ).
cnf(u1406,negated_conjecture,
( c8_2(X0,X1)
| ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1409,negated_conjecture,
ssSkC6 ).
cnf(u1442,negated_conjecture,
( c7_2(X0,X1)
| ~ c8_2(X0,X1)
| c6_2(X0,X1)
| c8_1(X0)
| ~ c5_2(X0,a714)
| ~ ndr1_1(X0) ) ).
cnf(u1445,negated_conjecture,
~ ssSkC22 ).
cnf(u1450,negated_conjecture,
ssSkC32 ).
cnf(u1463,negated_conjecture,
~ c6_1(a755) ).
cnf(u1468,negated_conjecture,
~ c7_1(a755) ).
cnf(u1472,negated_conjecture,
( c8_2(X0,X1)
| c5_2(X0,X1)
| c8_1(X0)
| c10_1(X0)
| ~ ndr1_1(X0)
| c3_2(X0,X1) ) ).
cnf(u1495,negated_conjecture,
ssSkC15 ).
cnf(u1505,negated_conjecture,
( c7_2(X0,X1)
| ~ c7_2(X0,a714)
| ~ c8_2(X0,X1)
| c6_2(X0,X1)
| c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1509,negated_conjecture,
( c7_2(X0,X1)
| ~ c3_2(X0,a714)
| ~ c8_2(X0,X1)
| c6_2(X0,X1)
| c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1571,negated_conjecture,
~ ssSkC25 ).
cnf(u1590,negated_conjecture,
ssSkC33 ).
cnf(u1594,negated_conjecture,
( ~ c6_2(X0,X1)
| c7_1(X0)
| c2_2(X0,a751)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| c8_2(X0,X1) ) ).
cnf(u1598,negated_conjecture,
( ~ c3_2(X0,a751)
| c7_1(X0)
| ~ c6_2(X0,X1)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| c8_2(X0,X1) ) ).
cnf(u1605,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1617,negated_conjecture,
( ~ c10_1(X0)
| c3_1(X0)
| c3_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u1633,negated_conjecture,
~ ssSkC31 ).
cnf(u1637,negated_conjecture,
( ~ c8_2(X0,a744)
| ~ ssSkP10(X0)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(u1641,negated_conjecture,
( ~ ssSkP10(X0)
| c6_2(X0,a744)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(u1645,negated_conjecture,
( ~ c9_2(X0,a744)
| ~ ssSkP10(X0)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(u1678,negated_conjecture,
~ ndr1_1(a618) ).
cnf(u1684,negated_conjecture,
~ ssSkC2 ).
cnf(u1696,negated_conjecture,
~ ssSkC7 ).
cnf(u1702,negated_conjecture,
~ ndr1_1(a658) ).
cnf(u1716,negated_conjecture,
~ ssSkC18 ).
cnf(u1730,negated_conjecture,
~ ndr1_1(a733) ).
cnf(u1736,negated_conjecture,
ssSkC28 ).
cnf(u1750,negated_conjecture,
~ ssSkC20 ).
cnf(u1787,negated_conjecture,
~ ssSkC17 ).
cnf(u1808,negated_conjecture,
ssSkC10 ).
cnf(u1813,negated_conjecture,
~ ndr1_1(a655) ).
cnf(u1821,negated_conjecture,
ssSkC13 ).
cnf(u1833,negated_conjecture,
~ ssSkC14 ).
cnf(u1879,negated_conjecture,
~ ndr1_1(a708) ).
cnf(u1885,negated_conjecture,
~ ssSkC21 ).
cnf(u1890,negated_conjecture,
~ ssSkC3 ).
cnf(u1895,negated_conjecture,
~ ndr1_1(a621) ).
cnf(u1918,negated_conjecture,
( ~ c6_1(X0)
| c3_1(X0)
| c2_1(X0) ) ).
cnf(u1922,negated_conjecture,
( ~ c3_1(X0)
| ~ c1_1(X0)
| c8_1(X0) ) ).
cnf(u1942,negated_conjecture,
( ~ c6_2(X0,a685)
| c8_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1951,negated_conjecture,
~ ndr1_1(a756) ).
cnf(u1959,negated_conjecture,
~ ssSkC5 ).
cnf(u1985,negated_conjecture,
ssSkC34 ).
cnf(u1990,negated_conjecture,
( ~ c2_2(X0,a613)
| ~ c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1993,negated_conjecture,
~ ssSkC1 ).
cnf(u1998,negated_conjecture,
( c5_2(X0,a650)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u2001,negated_conjecture,
ssSkC8 ).
cnf(u2006,negated_conjecture,
( ~ c1_2(X0,a650)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u2010,negated_conjecture,
( ~ c7_2(X0,a650)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u2026,negated_conjecture,
( ~ c3_2(X0,a685)
| ~ ssSkP5(X0)
| c8_1(X0) ) ).
cnf(u2030,negated_conjecture,
( c10_2(X0,a685)
| ~ ssSkP5(X0)
| c8_1(X0) ) ).
cnf(u2057,negated_conjecture,
ssSkC23 ).
cnf(u2061,negated_conjecture,
( ~ c4_2(X0,a719)
| c10_1(X0)
| ssSkP8(X0) ) ).
cnf(u2065,negated_conjecture,
( c7_2(X0,a719)
| c10_1(X0)
| ssSkP8(X0) ) ).
cnf(u2092,negated_conjecture,
~ ssSkC30 ).
cnf(u2113,negated_conjecture,
( ~ c9_2(X0,a613)
| ~ c10_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2117,negated_conjecture,
( c1_1(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u2121,negated_conjecture,
~ ssSkC11 ).
cnf(u2125,negated_conjecture,
( ~ c2_2(X0,a662)
| c8_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u2129,negated_conjecture,
( ~ c6_2(X0,a662)
| c8_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u2145,negated_conjecture,
( ~ ssSkP5(X0)
| ndr1_1(X0)
| c8_1(X0) ) ).
cnf(u2154,negated_conjecture,
ssSkC4 ).
cnf(u2165,negated_conjecture,
( c2_2(X0,a719)
| ssSkP8(X0)
| c10_1(X0) ) ).
cnf(u2170,negated_conjecture,
ssSkC24 ).
cnf(u2201,negated_conjecture,
( ~ c10_1(X0)
| ndr1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2205,negated_conjecture,
( c10_2(X0,a662)
| ~ ssSkP1(X0)
| c8_1(X0) ) ).
cnf(u2227,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0)
| c10_1(X0) ) ).
cnf(u2247,negated_conjecture,
( ~ ssSkP1(X0)
| ndr1_1(X0)
| c8_1(X0) ) ).
cnf(u2303,negated_conjecture,
c8_2(a686,a687) ).
cnf(u2308,negated_conjecture,
c1_2(a686,a687) ).
cnf(u2331,negated_conjecture,
ssSkC27 ).
cnf(u2340,negated_conjecture,
ssSkC29 ).
cnf(u2466,negated_conjecture,
c4_2(a686,a687) ).
cnf(u2471,negated_conjecture,
c2_2(a686,a688) ).
cnf(u2476,negated_conjecture,
c4_2(a686,a688) ).
cnf(u2521,negated_conjecture,
~ c4_1(a733) ).
cnf(u2616,negated_conjecture,
~ ssSkC16 ).
cnf(u2674,negated_conjecture,
c3_1(a618) ).
cnf(u2750,negated_conjecture,
~ c8_1(a686) ).
cnf(u2755,negated_conjecture,
ndr1_1(a686) ).
cnf(u2791,negated_conjecture,
c5_1(a708) ).
cnf(u2884,negated_conjecture,
~ c3_1(a621) ).
cnf(u2959,negated_conjecture,
~ c3_1(a670) ).
cnf(u3073,negated_conjecture,
~ ssSkC35 ).
cnf(u3078,negated_conjecture,
c1_1(a757) ).
cnf(u3117,negated_conjecture,
c7_1(a658) ).
cnf(u3184,negated_conjecture,
~ c1_1(a621) ).
cnf(u3205,negated_conjecture,
~ c2_1(a655) ).
cnf(u3225,negated_conjecture,
~ c8_1(a670) ).
cnf(u3230,negated_conjecture,
~ c9_1(a670) ).
cnf(u3270,negated_conjecture,
~ c10_1(a757) ).
cnf(u3275,negated_conjecture,
~ c5_1(a757) ).
cnf(u3295,negated_conjecture,
c6_1(a756) ).
cnf(u3330,negated_conjecture,
~ c2_1(a756) ).
cnf(u3335,negated_conjecture,
c3_1(a756) ).
cnf(u3345,negated_conjecture,
~ c1_1(a618) ).
cnf(u3351,negated_conjecture,
~ c5_1(a756) ).
cnf(u3377,negated_conjecture,
c8_1(a756) ).
cnf(u3381,negated_conjecture,
~ c1_1(a756) ).
cnf(u3431,negated_conjecture,
~ c5_2(a686,a687) ).
cnf(u3447,negated_conjecture,
~ c5_2(a686,a688) ).
cnf(u3458,negated_conjecture,
~ c10_1(a686) ).
cnf(u3463,negated_conjecture,
c8_2(a686,a688) ).
cnf(u3571,negated_conjecture,
c7_2(a686,a687) ).
cnf(u3584,negated_conjecture,
c7_2(a686,a688) ).
cnf(clause240,negated_conjecture,
( ~ c5_2(X0,a682)
| ssSkP4(X0) ) ).
cnf(u3396,negated_conjecture,
c7_1(a756) ).
cnf(clause118,negated_conjecture,
( c6_2(X0,a749)
| ssSkP11(X0) ) ).
cnf(u659,negated_conjecture,
( ~ c8_2(X0,a676)
| ~ ssSkP3(X0) ) ).
cnf(u593,negated_conjecture,
( ~ ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause49,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(u3357,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0) ) ).
cnf(clause63,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause239,negated_conjecture,
( ~ c10_2(X0,a682)
| ssSkP4(X0) ) ).
cnf(u582,negated_conjecture,
( ~ ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause70,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u641,negated_conjecture,
( ~ c3_2(X0,a731)
| ~ ssSkP9(X0) ) ).
cnf(u744,negated_conjecture,
( c1_2(X0,a675)
| ssSkP2(X0) ) ).
cnf(u3394,negated_conjecture,
( c8_2(X0,a682)
| c8_1(X0)
| c10_1(X0)
| ssSkP4(X0) ) ).
cnf(u3371,negated_conjecture,
( c7_2(X0,a661)
| c9_1(X0)
| c10_1(X0)
| c8_2(X0,a661)
| ssSkP1(X0) ) ).
cnf(u579,negated_conjecture,
( ~ ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u730,negated_conjecture,
( c9_2(X0,a743)
| ssSkP10(X0) ) ).
cnf(u3368,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,X1)
| c9_1(X0)
| c10_1(X0)
| c8_2(X0,X1) ) ).
cnf(u745,negated_conjecture,
( c1_2(X0,a661)
| ssSkP1(X0) ) ).
cnf(u3360,negated_conjecture,
( c10_1(X0)
| ndr1_1(X0) ) ).
cnf(u657,negated_conjecture,
( ~ c7_2(X0,a684)
| ssSkP5(X0) ) ).
cnf(clause58,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u674,negated_conjecture,
( ~ c8_2(X0,a635)
| ~ ssSkP0(X0) ) ).
cnf(u743,negated_conjecture,
( c9_2(X0,a676)
| ~ ssSkP3(X0) ) ).
cnf(u3562,negated_conjecture,
( c7_2(X0,a682)
| c8_1(X0)
| c6_2(X0,a682)
| c8_2(X0,a714)
| c10_1(X0)
| ssSkP4(X0) ) ).
cnf(clause234,negated_conjecture,
( ~ c4_2(X0,a712)
| ssSkP6(X0) ) ).
cnf(u3367,negated_conjecture,
( ~ c4_1(X0)
| ~ c3_2(X0,X1)
| c10_1(X0)
| c8_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u3356,negated_conjecture,
c7_1(a621) ).
cnf(clause62,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u742,negated_conjecture,
( ~ c5_2(X0,a676)
| ~ ssSkP3(X0) ) ).
cnf(u3390,negated_conjecture,
( c8_2(X0,a749)
| c8_1(X0)
| c10_1(X0)
| c3_2(X0,a749)
| ssSkP11(X0) ) ).
cnf(u737,negated_conjecture,
( c3_2(X0,a715)
| ~ ssSkP7(X0) ) ).
cnf(u675,negated_conjecture,
( ~ c3_2(X0,a635)
| ~ ssSkP0(X0) ) ).
cnf(u735,negated_conjecture,
( c8_2(X0,a718)
| ~ ssSkP8(X0) ) ).
cnf(u3405,negated_conjecture,
( ~ c9_2(X0,a684)
| c2_2(X0,a751)
| c7_1(X0)
| c8_2(X0,a684)
| ssSkP5(X0) ) ).
cnf(u644,negated_conjecture,
( ~ c8_2(X0,a712)
| ssSkP6(X0) ) ).
cnf(u642,negated_conjecture,
( ~ c9_2(X0,a731)
| ~ ssSkP9(X0) ) ).
cnf(u585,negated_conjecture,
( ~ ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause145,negated_conjecture,
( c6_2(X0,a684)
| ssSkP5(X0) ) ).
cnf(u3402,negated_conjecture,
( ~ c3_2(X0,a714)
| c7_2(X0,X1)
| ~ c8_2(X0,X1)
| c6_2(X0,X1)
| c8_1(X0) ) ).
cnf(u658,negated_conjecture,
( ~ c3_2(X0,a682)
| ssSkP4(X0) ) ).
cnf(u3534,negated_conjecture,
~ c7_1(a733) ).
cnf(clause224,negated_conjecture,
( ~ c5_2(X0,a749)
| ssSkP11(X0) ) ).
cnf(u736,negated_conjecture,
( c7_2(X0,a718)
| ~ ssSkP8(X0) ) ).
cnf(u3401,negated_conjecture,
( ~ c7_2(X0,a714)
| c7_2(X0,X1)
| ~ c8_2(X0,X1)
| c6_2(X0,X1)
| c8_1(X0) ) ).
cnf(u643,negated_conjecture,
( c10_2(X0,a715)
| ~ ssSkP7(X0) ) ).
cnf(u633,negated_conjecture,
( ~ c7_2(X0,a749)
| ssSkP11(X0) ) ).
cnf(clause65,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u3383,negated_conjecture,
( ~ c6_1(X0)
| ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c8_1(X0)
| c8_2(X0,X1) ) ).
cnf(u3398,negated_conjecture,
( ~ c5_2(X0,a714)
| ~ c8_2(X0,X1)
| c6_2(X0,X1)
| c8_1(X0)
| c7_2(X0,X1) ) ).
cnf(u3372,negated_conjecture,
( c7_2(X0,a675)
| c9_1(X0)
| c10_1(X0)
| ssSkP2(X0) ) ).
cnf(clause50,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(u3556,negated_conjecture,
( ~ c8_2(X0,X1)
| c6_2(X0,X1)
| c8_1(X0)
| c7_2(X0,X1)
| c8_2(X0,a714)
| c10_1(X0) ) ).
cnf(u738,negated_conjecture,
( c9_2(X0,a712)
| ssSkP6(X0) ) ).
cnf(clause226,negated_conjecture,
( ~ c10_2(X0,a743)
| ssSkP10(X0) ) ).
cnf(u581,negated_conjecture,
( ~ ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u656,negated_conjecture,
( ~ c1_2(X0,a684)
| ssSkP5(X0) ) ).
cnf(u3363,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u3355,negated_conjecture,
c7_1(a618) ).
cnf(u751,negated_conjecture,
( ~ c2_2(X0,a635)
| ~ ssSkP0(X0) ) ).
cnf(u3389,negated_conjecture,
( c5_2(X0,X1)
| c8_2(X0,X1)
| c8_1(X0)
| c10_1(X0)
| c3_2(X0,X1) ) ).
cnf(clause245,negated_conjecture,
( ~ c6_2(X0,a661)
| ssSkP1(X0) ) ).
cnf(u660,negated_conjecture,
( ~ c8_2(X0,a675)
| ssSkP2(X0) ) ).
cnf(clause155,negated_conjecture,
( c5_2(X0,a661)
| ssSkP1(X0) ) ).
cnf(u3359,negated_conjecture,
ndr1_1(a670) ).
cnf(u3361,negated_conjecture,
ndr1_1(a757) ).
cnf(clause150,negated_conjecture,
( c5_2(X0,a675)
| ssSkP2(X0) ) ).
cnf(u3406,negated_conjecture,
( ~ c9_2(X0,a749)
| c2_2(X0,a751)
| c7_1(X0)
| c8_2(X0,a749)
| ssSkP11(X0) ) ).
cnf(u3393,negated_conjecture,
( c3_2(X0,a676)
| c10_1(X0)
| c8_1(X0)
| ~ ssSkP3(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN422-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.18 % Computer : n026.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Mon Sep 28 15:58:12 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.30 % (3977875)Will run a generic schedule for satisfiability detection.
% 0.21/0.30 % (3977884)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1052021403:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.30 % (3977881)% WARNING: option uhcvi not known.
% 0.21/0.30 % (3977880)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=126932298_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.30 % (3977881)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2849711031:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.30 % (3977882)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=326621174:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.30 % (3977883)dis+10_1_sil=32000:sp=arity:random_seed=3856572324:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.30 % (3977886)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2144468602:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.30 % (3977885)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2044334288:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.30 % (3977881) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3977875-3977881"...
% 0.21/0.30 % (3977881)...printing done.
% 0.21/0.30 % SZS status Satisfiable for theBenchmark
% 0.21/0.30 % SZS output start Saturation.
% See solution above
% 0.21/0.30 % SZS output start Definitions and Model Updates.
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC22"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c8_2"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c9_2"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c3_2"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c1_2"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c7_2"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC5"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC25"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkP0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c2_1"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c9_1"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkP3"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c8_1"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkP7"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkP8"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c1_1"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkP9"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c10_1"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c5_1"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c4_0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC23"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c10_0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC33"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC1"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC2"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC7"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC9"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC10"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC11"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC14"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC15"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC16"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC17"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC18"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC20"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC21"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC30"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ssSkC31"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c8_0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c5_0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c3_0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c9_0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "c7_0"
% 0.21/0.30 globally flip the polarity of every occurrence of predicate "ndr1_0"
% 0.21/0.30 % SZS output end Definitions and Model Updates.
% 0.21/0.30 % (3977881)------------------------------
% 0.21/0.30 % (3977881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3977881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3977881)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3977881)Termination reason: Satisfiable
% 0.21/0.30 % (3977881)Time elapsed: 0.019 s
% 0.21/0.30 % (3977881)Peak memory usage: 13 MB
% 0.21/0.30 % (3977881)Instructions burned: 26 (million)
% 0.21/0.30 % (3977875)Success in time 0.075 s
% 0.21/0.30 % Vampire exiting
%------------------------------------------------------------------------------