%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN420-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 : n019.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.21s 0.31s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1105,negated_conjecture,
~ c3_0 ).
cnf(u1109,negated_conjecture,
( c5_2(X2,X3)
| c4_1(X2)
| c7_2(X2,X4)
| c2_2(X2,X4)
| ~ c8_2(X2,X4)
| ~ ndr1_1(X2)
| ~ c9_2(X2,X3)
| c6_2(X2,X3) ) ).
cnf(u1112,negated_conjecture,
ndr1_0 ).
cnf(u1120,negated_conjecture,
~ c2_0 ).
cnf(u1124,negated_conjecture,
( ~ ndr1_1(X2)
| c1_2(X2,X3)
| c8_2(X2,X3)
| ~ c3_2(X2,X4)
| ~ c4_2(X2,X4)
| ~ c10_2(X2,X4)
| c9_1(X2)
| c2_2(X2,X3) ) ).
cnf(u1135,negated_conjecture,
( c4_2(X2,X3)
| ~ c5_2(X2,X3)
| c10_1(X2)
| c9_1(X2)
| ~ ndr1_1(X2)
| ~ c8_2(X2,X3) ) ).
cnf(u1156,negated_conjecture,
( ~ ndr1_1(X2)
| ~ c5_2(X2,X3)
| ~ c3_2(X2,X3)
| c9_2(X2,X3)
| ~ c3_1(X2)
| c1_1(X2) ) ).
cnf(u1199,negated_conjecture,
c5_0 ).
cnf(u1223,negated_conjecture,
c1_0 ).
cnf(u1227,negated_conjecture,
( c3_2(X2,X3)
| ~ c4_1(X2)
| c10_1(X2)
| ~ ndr1_1(X2)
| c2_2(X2,X3)
| c10_2(X2,X3) ) ).
cnf(u1235,negated_conjecture,
~ c8_0 ).
cnf(u1250,negated_conjecture,
~ c9_0 ).
cnf(u1297,negated_conjecture,
( c6_2(X0,X1)
| ~ c6_1(X0)
| ~ c5_2(X0,X2)
| ~ c4_2(X0,X2)
| c1_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0)
| c3_2(X0,X1) ) ).
cnf(u1300,negated_conjecture,
ssSkC19 ).
cnf(u1311,negated_conjecture,
c6_0 ).
cnf(u1329,negated_conjecture,
( c6_2(X0,X1)
| ~ c9_1(X0)
| c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c5_2(X0,X3)
| ~ ndr1_1(X0)
| c4_2(X0,X1) ) ).
cnf(u1332,negated_conjecture,
ssSkC14 ).
cnf(u1341,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ c10_1(X0)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1344,negated_conjecture,
~ ssSkC16 ).
cnf(u1367,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c1_1(X0)
| ~ c4_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| c10_2(X0,X1) ) ).
cnf(u1371,negated_conjecture,
c4_0 ).
cnf(u1469,negated_conjecture,
( c4_2(X1,X2)
| ~ c6_2(X1,X2)
| c1_2(X1,X2)
| c6_1(X1)
| c9_1(X1)
| ~ ndr1_1(X1) ) ).
cnf(u1480,negated_conjecture,
( ~ c8_2(X0,X1)
| c9_2(X0,X1)
| ~ c4_1(X0)
| c1_1(X0)
| ~ ndr1_1(X0)
| c5_2(X0,X1) ) ).
cnf(u1483,negated_conjecture,
~ ssSkC4 ).
cnf(u1500,negated_conjecture,
( ~ c5_1(X0)
| c3_1(X0) ) ).
cnf(u1540,negated_conjecture,
( c5_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,X1)
| c9_1(X0)
| ~ c1_2(X0,a419)
| ~ ndr1_1(X0) ) ).
cnf(u1544,negated_conjecture,
( c5_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_2(X0,X1)
| c9_1(X0)
| c5_2(X0,a419)
| ~ ndr1_1(X0) ) ).
cnf(u1551,negated_conjecture,
( ~ ndr1_1(X0)
| c5_1(X0)
| c2_1(X0)
| ~ c10_2(X0,X2)
| c7_2(X0,X2)
| ~ c2_2(X0,X2) ) ).
cnf(u1554,negated_conjecture,
~ ssSkC18 ).
cnf(u1573,negated_conjecture,
~ c7_0 ).
cnf(u1577,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0)
| c5_2(X0,a316)
| ~ ndr1_1(X0) ) ).
cnf(u1581,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0)
| c3_2(X0,a316)
| ~ ndr1_1(X0) ) ).
cnf(u1600,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_2(X0,a400)
| ~ ndr1_1(X0) ) ).
cnf(u1603,negated_conjecture,
ssSkC25 ).
cnf(u1608,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c8_2(X0,a400)
| ~ ndr1_1(X0) ) ).
cnf(u1638,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,a316)
| ~ c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1642,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c2_2(X0,a400)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1654,negated_conjecture,
~ ssSkC30 ).
cnf(u1658,negated_conjecture,
( c10_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_1(X0)
| c2_2(X0,a411)
| ~ ndr1_1(X0) ) ).
cnf(u1662,negated_conjecture,
( c10_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_1(X0)
| ~ c7_2(X0,a411)
| ~ ndr1_1(X0) ) ).
cnf(u1666,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c9_1(X0)
| c3_1(X0)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| c2_2(X0,X1) ) ).
cnf(u1670,negated_conjecture,
( c10_2(X0,X1)
| ~ c3_2(X0,a411)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1674,negated_conjecture,
~ ssSkC34 ).
cnf(u1678,negated_conjecture,
( c2_2(X0,X1)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c8_2(X0,a428)
| ~ ndr1_1(X0) ) ).
cnf(u1682,negated_conjecture,
( c2_2(X0,X1)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a428)
| ~ ndr1_1(X0) ) ).
cnf(u1686,negated_conjecture,
( c2_2(X0,X1)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c10_2(X0,a428)
| ~ ndr1_1(X0) ) ).
cnf(u1690,negated_conjecture,
c10_0 ).
cnf(u1694,negated_conjecture,
( c10_2(X0,X1)
| ~ c9_1(X0)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,X1) ) ).
cnf(u1708,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c6_1(X0)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1)
| c4_2(X0,a276) ) ).
cnf(u1720,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| c10_1(X1) ) ).
cnf(u1727,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c6_1(X0)
| c8_2(X0,a276)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1731,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c6_1(X0)
| ~ c2_2(X0,a276)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1735,negated_conjecture,
ndr1_1(a381) ).
cnf(u1739,negated_conjecture,
( ~ c9_2(a381,X0)
| c8_2(a381,X0)
| c10_2(a381,X0) ) ).
cnf(u1743,negated_conjecture,
( c1_1(X1)
| c7_1(X1)
| ~ c4_1(X1) ) ).
cnf(u1746,negated_conjecture,
ssSkC1 ).
cnf(u1758,negated_conjecture,
ndr1_1(a278) ).
cnf(u1762,negated_conjecture,
( ~ c7_2(a278,X0)
| ~ c4_2(a278,X0)
| c2_2(a278,X0) ) ).
cnf(u1766,negated_conjecture,
ndr1_1(a325) ).
cnf(u1774,negated_conjecture,
~ ssSkC9 ).
cnf(u1785,negated_conjecture,
~ ssSkC31 ).
cnf(u1791,negated_conjecture,
~ ssSkC7 ).
cnf(u1802,negated_conjecture,
~ ssSkC27 ).
cnf(u1806,negated_conjecture,
ndr1_1(a403) ).
cnf(u1810,negated_conjecture,
( c10_2(a403,X0)
| c4_2(a403,X0)
| c6_2(a403,X0) ) ).
cnf(u1818,negated_conjecture,
ndr1_1(a277) ).
cnf(u1822,negated_conjecture,
( ~ c10_2(a277,X0)
| c3_2(a277,X0)
| c4_2(a277,X0) ) ).
cnf(u1861,negated_conjecture,
ssSkC36 ).
cnf(u1883,negated_conjecture,
ssSkC0 ).
cnf(u1931,negated_conjecture,
ssSkC32 ).
cnf(u1943,negated_conjecture,
ssSkC33 ).
cnf(u1946,negated_conjecture,
ndr1_1(a427) ).
cnf(u1958,negated_conjecture,
ssSkC37 ).
cnf(u1962,negated_conjecture,
ndr1_1(a441) ).
cnf(u1966,negated_conjecture,
( ~ c8_2(a441,X0)
| c7_2(a441,X0)
| c5_2(a441,X0) ) ).
cnf(u1971,negated_conjecture,
ssSkC38 ).
cnf(u1993,negated_conjecture,
( ~ c2_1(X0)
| c8_1(X0)
| c3_1(X0) ) ).
cnf(u1997,negated_conjecture,
( ~ c4_2(a277,X0)
| c7_2(a277,X0)
| c6_2(a277,X0) ) ).
cnf(u2040,negated_conjecture,
ssSkC29 ).
cnf(u2045,negated_conjecture,
ssSkC28 ).
cnf(u2049,negated_conjecture,
ndr1_1(a443) ).
cnf(u2069,negated_conjecture,
~ ssSkC10 ).
cnf(u2073,negated_conjecture,
ndr1_1(a330) ).
cnf(u2077,negated_conjecture,
( ~ c3_2(a330,X0)
| ~ c2_2(a330,X0)
| ~ c1_2(a330,X0) ) ).
cnf(u2081,negated_conjecture,
ndr1_1(a406) ).
cnf(u2085,negated_conjecture,
( c9_2(a406,X0)
| c2_2(a406,X0)
| c1_2(a406,X0) ) ).
cnf(u2097,negated_conjecture,
( c4_2(a441,X0)
| ~ c2_2(a441,X0)
| ~ c5_2(a441,X0) ) ).
cnf(u2119,negated_conjecture,
( ~ c1_2(X0,a328)
| ~ c6_1(X0)
| c3_1(X0) ) ).
cnf(u2126,negated_conjecture,
ssSkC11 ).
cnf(u2134,negated_conjecture,
~ ssSkC12 ).
cnf(u2150,negated_conjecture,
~ ssSkC13 ).
cnf(u2158,negated_conjecture,
~ ssSkC21 ).
cnf(u2167,negated_conjecture,
ssSkC22 ).
cnf(u2171,negated_conjecture,
( ~ c1_2(X0,a390)
| c6_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u2175,negated_conjecture,
( c5_2(X0,a390)
| c6_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u2188,negated_conjecture,
~ ssSkC26 ).
cnf(u2233,negated_conjecture,
( ~ c2_2(X0,a328)
| ~ c6_1(X0)
| c3_1(X0) ) ).
cnf(u2237,negated_conjecture,
( c8_2(X0,a328)
| ~ c6_1(X0)
| c3_1(X0) ) ).
cnf(u2257,negated_conjecture,
( c9_2(X0,a390)
| ~ ssSkP3(X0)
| c6_1(X0) ) ).
cnf(u2273,negated_conjecture,
( c5_2(X0,a440)
| ~ c10_1(X0)
| c9_1(X0) ) ).
cnf(u2302,negated_conjecture,
ssSkC35 ).
cnf(u2306,negated_conjecture,
( c10_2(X0,a430)
| c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u2322,negated_conjecture,
( ~ c2_1(X0)
| c8_1(X0) ) ).
cnf(u2348,negated_conjecture,
ssSkC8 ).
cnf(u2381,negated_conjecture,
~ ssSkC3 ).
cnf(u2386,negated_conjecture,
ssSkC2 ).
cnf(u2390,negated_conjecture,
( c4_2(X0,a312)
| c7_1(X0)
| c3_1(X0) ) ).
cnf(u2393,negated_conjecture,
ssSkC6 ).
cnf(u2397,negated_conjecture,
ssSkC5 ).
cnf(u2402,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0)
| c3_1(X0) ) ).
cnf(u2422,negated_conjecture,
( ~ ssSkP3(X0)
| ndr1_1(X0)
| c6_1(X0) ) ).
cnf(u2434,negated_conjecture,
( ~ c6_2(X0,a440)
| ~ c10_1(X0)
| c9_1(X0) ) ).
cnf(u2438,negated_conjecture,
( c1_2(X0,a440)
| ~ c10_1(X0)
| c9_1(X0) ) ).
cnf(u2451,negated_conjecture,
ssSkC15 ).
cnf(u2466,negated_conjecture,
ssSkC23 ).
cnf(u2470,negated_conjecture,
( c3_2(X0,a393)
| ~ ssSkP4(X0)
| ~ ssSkP5(X0) ) ).
cnf(u2474,negated_conjecture,
( ~ c8_2(X0,a393)
| ~ ssSkP4(X0)
| ~ ssSkP5(X0) ) ).
cnf(u2494,negated_conjecture,
( ~ c2_2(X0,a430)
| c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u2498,negated_conjecture,
( ~ c6_2(X0,a430)
| c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u2553,negated_conjecture,
( ~ c2_2(X0,a312)
| c7_1(X0)
| c3_1(X0) ) ).
cnf(u2557,negated_conjecture,
( ~ c5_2(X0,a312)
| c7_1(X0)
| c3_1(X0) ) ).
cnf(u2562,negated_conjecture,
( ~ c10_1(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u2574,negated_conjecture,
( ~ c6_2(X0,a393)
| ~ ssSkP4(X0)
| ~ ssSkP5(X0) ) ).
cnf(u2590,negated_conjecture,
( c5_1(X0)
| ~ c4_1(X0)
| ndr1_1(X0) ) ).
cnf(u2603,negated_conjecture,
( c7_1(X0)
| ndr1_1(X0)
| c3_1(X0) ) ).
cnf(u2619,negated_conjecture,
( ~ ssSkP4(X0)
| ndr1_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u2637,negated_conjecture,
c5_2(a381,a382) ).
cnf(u2642,negated_conjecture,
c2_2(a381,a382) ).
cnf(u2647,negated_conjecture,
c3_2(a420,a421) ).
cnf(u2673,negated_conjecture,
( c7_1(X0)
| c4_1(X0) ) ).
cnf(u2703,negated_conjecture,
c4_2(a325,a326) ).
cnf(u2708,negated_conjecture,
c8_2(a381,a382) ).
cnf(u2728,negated_conjecture,
~ c8_1(a420) ).
cnf(u2733,negated_conjecture,
~ c10_2(a420,a421) ).
cnf(u2738,negated_conjecture,
c7_2(a420,a421) ).
cnf(u2777,negated_conjecture,
~ c4_1(a278) ).
cnf(u2782,negated_conjecture,
c8_2(a278,a279) ).
cnf(u2787,negated_conjecture,
~ c3_2(a278,a279) ).
cnf(u2792,negated_conjecture,
~ c4_2(a278,a279) ).
cnf(u2818,negated_conjecture,
c1_1(a325) ).
cnf(u2823,negated_conjecture,
c7_2(a325,a326) ).
cnf(u2828,negated_conjecture,
~ c5_2(a325,a326) ).
cnf(u2853,negated_conjecture,
~ c1_1(a381) ).
cnf(u2894,negated_conjecture,
c7_1(a420) ).
cnf(u2899,negated_conjecture,
ndr1_1(a420) ).
cnf(u2974,negated_conjecture,
~ c9_2(a323,a324) ).
cnf(u2979,negated_conjecture,
c10_2(a330,a331) ).
cnf(u3034,negated_conjecture,
ssSkC20 ).
cnf(u3063,negated_conjecture,
~ c7_2(a403,a404) ).
cnf(u3105,negated_conjecture,
~ c5_1(a277) ).
cnf(u3148,negated_conjecture,
c3_2(a348,a349) ).
cnf(u3171,negated_conjecture,
ssSkC17 ).
cnf(u3187,negated_conjecture,
ssSkC24 ).
cnf(u3265,negated_conjecture,
~ c6_1(a445) ).
cnf(u3270,negated_conjecture,
~ c1_1(a445) ).
cnf(u3290,negated_conjecture,
~ c7_1(a296) ).
cnf(u3360,negated_conjecture,
~ c3_1(a323) ).
cnf(u3365,negated_conjecture,
c10_1(a323) ).
cnf(u3370,negated_conjecture,
~ c4_2(a323,a324) ).
cnf(u3375,negated_conjecture,
c7_2(a323,a324) ).
cnf(u3380,negated_conjecture,
c1_1(a330) ).
cnf(u3385,negated_conjecture,
~ c6_2(a330,a331) ).
cnf(u3390,negated_conjecture,
c1_2(a330,a331) ).
cnf(u3490,negated_conjecture,
~ c3_1(a403) ).
cnf(u3495,negated_conjecture,
~ c3_2(a403,a404) ).
cnf(u3500,negated_conjecture,
~ c5_2(a403,a404) ).
cnf(u3505,negated_conjecture,
~ c3_1(a406) ).
cnf(u3525,negated_conjecture,
~ c7_1(a427) ).
cnf(u3601,negated_conjecture,
c6_1(a348) ).
cnf(u3606,negated_conjecture,
c7_2(a348,a349) ).
cnf(u3611,negated_conjecture,
~ c6_2(a348,a349) ).
cnf(u3707,negated_conjecture,
~ c10_1(a296) ).
cnf(u3712,negated_conjecture,
~ c6_1(a296) ).
cnf(u3734,negated_conjecture,
ndr1_1(a323) ).
cnf(u3838,negated_conjecture,
ndr1_1(a348) ).
cnf(u3942,negated_conjecture,
~ ssSkP3(a381) ).
cnf(u3957,negated_conjecture,
~ ssSkP1(a278) ).
cnf(u3971,negated_conjecture,
~ ssSkP2(a278) ).
cnf(u4041,negated_conjecture,
c4_2(a403,a446) ).
cnf(u4048,negated_conjecture,
~ c4_1(a277) ).
cnf(u4066,negated_conjecture,
~ c6_1(a441) ).
cnf(u4086,negated_conjecture,
c7_1(a277) ).
cnf(u4099,negated_conjecture,
~ ssSkP6(a277) ).
cnf(u4114,negated_conjecture,
~ ssSkP5(a330) ).
cnf(u4139,negated_conjecture,
~ c2_2(a330,a274) ).
cnf(u4154,negated_conjecture,
( ~ c5_2(a348,X0)
| ~ c3_2(a348,X0) ) ).
cnf(u4171,negated_conjecture,
c10_2(a348,a428) ).
cnf(u4193,negated_conjecture,
~ c5_2(a278,a279) ).
cnf(u4198,negated_conjecture,
c4_2(a381,a382) ).
cnf(u4215,negated_conjecture,
c10_1(a427) ).
cnf(u4233,negated_conjecture,
~ c10_1(a348) ).
cnf(u4269,negated_conjecture,
c3_1(a296) ).
cnf(u4292,negated_conjecture,
~ c2_2(a330,a331) ).
cnf(u4311,negated_conjecture,
~ c5_1(a403) ).
cnf(u4316,negated_conjecture,
c2_1(a403) ).
cnf(u4321,negated_conjecture,
~ c2_2(a348,a428) ).
cnf(u4359,negated_conjecture,
ssSkP7(a296) ).
cnf(u4376,negated_conjecture,
~ c5_1(a427) ).
cnf(u4381,negated_conjecture,
c2_1(a427) ).
cnf(u4394,negated_conjecture,
~ c4_2(a427,a446) ).
cnf(u4407,negated_conjecture,
c5_1(a296) ).
cnf(u4428,negated_conjecture,
( ~ c6_2(a296,X0)
| ~ c1_2(a296,X0)
| c7_2(a296,X0) ) ).
cnf(u4448,negated_conjecture,
( ~ c8_2(a406,X0)
| c7_2(a406,X0)
| c2_2(a406,X0) ) ).
cnf(u4462,negated_conjecture,
~ c10_2(a348,a349) ).
cnf(u4476,negated_conjecture,
( ~ c5_2(a348,X1)
| ~ c7_2(a348,X1)
| ~ c4_2(a348,X1) ) ).
cnf(u4489,negated_conjecture,
~ c6_1(a406) ).
cnf(u4504,negated_conjecture,
ssSkP5(a296) ).
cnf(u4515,negated_conjecture,
~ c5_2(a441,a392) ).
cnf(u4518,negated_conjecture,
~ ssSkP5(a441) ).
cnf(u634,negated_conjecture,
( ~ ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause135,negated_conjecture,
( c1_2(X0,a446)
| ssSkP7(X0) ) ).
cnf(clause66,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u4458,negated_conjecture,
( ~ c4_2(X0,a393)
| c1_2(X0,X1)
| c8_2(X0,X1)
| ~ c10_2(X0,a393)
| c9_1(X0)
| c2_2(X0,X1)
| ~ ssSkP4(X0)
| ~ ssSkP5(X0) ) ).
cnf(u4401,negated_conjecture,
c8_1(a427) ).
cnf(u796,negated_conjecture,
( ~ c8_2(X0,a274)
| ~ ssSkP0(X0) ) ).
cnf(u4370,negated_conjecture,
( ~ c7_2(X0,a411)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_1(X0)
| c10_2(X0,X1) ) ).
cnf(u3903,negated_conjecture,
c4_1(a296) ).
cnf(u684,negated_conjecture,
( ~ c10_2(X0,a446)
| ssSkP7(X0) ) ).
cnf(u696,negated_conjecture,
( ~ c5_2(X0,a389)
| ssSkP3(X0) ) ).
cnf(u638,negated_conjecture,
( ~ ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u4246,negated_conjecture,
( ~ c4_1(X0)
| c9_2(X0,X1)
| ~ c8_2(X0,X1)
| c1_1(X0)
| c5_2(X0,X1) ) ).
cnf(clause242,negated_conjecture,
( ~ c8_2(X0,a446)
| ssSkP7(X0) ) ).
cnf(u4481,negated_conjecture,
( ~ c6_2(X0,X1)
| ~ c10_1(X0)
| c7_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c5_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ c1_2(X0,X2) ) ).
cnf(u4440,negated_conjecture,
( ~ c9_2(X2,X3)
| c4_1(X2)
| c7_2(X2,X4)
| c2_2(X2,X4)
| ~ c8_2(X2,X4)
| c5_2(X2,X3)
| c6_2(X2,X3) ) ).
cnf(u4352,negated_conjecture,
( ~ c2_2(X0,a400)
| ~ c7_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_1(X0) ) ).
cnf(u3906,negated_conjecture,
c1_1(a296) ).
cnf(u695,negated_conjecture,
( ~ c4_2(X0,a389)
| ssSkP3(X0) ) ).
cnf(u3907,negated_conjecture,
c1_1(a427) ).
cnf(u4353,negated_conjecture,
( ~ c6_2(X0,X1)
| ~ c4_2(X0,X1)
| c10_2(X0,X1)
| c1_1(X0)
| c2_2(X0,a411) ) ).
cnf(u4208,negated_conjecture,
( ~ c3_1(X2)
| ~ c3_2(X2,X3)
| c9_2(X2,X3)
| ~ c5_2(X2,X3)
| c1_1(X2) ) ).
cnf(u4348,negated_conjecture,
( ~ c7_2(X0,a400)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u4369,negated_conjecture,
( ~ c4_2(X0,a392)
| c10_2(X0,a392)
| c1_1(X0)
| c2_2(X0,a411)
| ssSkP5(X0) ) ).
cnf(u3910,negated_conjecture,
ndr1_1(a445) ).
cnf(u3929,negated_conjecture,
( ~ c8_2(X0,a428)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X1) ) ).
cnf(u724,negated_conjecture,
( c7_2(X0,a285)
| ~ ssSkP1(X0) ) ).
cnf(u650,negated_conjecture,
( ~ ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u4209,negated_conjecture,
( ~ c4_1(X2)
| c3_2(X2,X3)
| c10_1(X2)
| c2_2(X2,X3)
| c10_2(X2,X3) ) ).
cnf(clause253,negated_conjecture,
( ~ c9_2(X0,a391)
| ssSkP4(X0) ) ).
cnf(u4156,negated_conjecture,
( ~ c6_1(X0)
| c8_2(X0,a276)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u772,negated_conjecture,
( c2_2(X0,a392)
| ssSkP5(X0) ) ).
cnf(u773,negated_conjecture,
( c6_2(X0,a392)
| ssSkP5(X0) ) ).
cnf(u726,negated_conjecture,
( c1_2(X0,a285)
| ~ ssSkP1(X0) ) ).
cnf(clause252,negated_conjecture,
( ~ c1_2(X0,a391)
| ssSkP4(X0) ) ).
cnf(u4176,negated_conjecture,
( ~ c8_2(X2,X3)
| ~ c5_2(X2,X3)
| c10_1(X2)
| c9_1(X2)
| c4_2(X2,X3) ) ).
cnf(u4399,negated_conjecture,
( ~ c9_1(X0)
| c6_2(X0,X1)
| c8_2(X0,X3)
| c1_2(X0,X3)
| ~ c5_2(X0,X3)
| c4_2(X0,X1) ) ).
cnf(u4243,negated_conjecture,
( c10_2(a296,X0)
| ~ c1_2(a296,X0)
| ~ c4_2(a296,X0) ) ).
cnf(clause67,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u698,negated_conjecture,
( ~ c6_2(X0,a379)
| ~ ssSkP2(X0) ) ).
cnf(u4343,negated_conjecture,
( ~ c3_1(X0)
| ~ c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,X1)
| c5_2(X0,a316) ) ).
cnf(u4482,negated_conjecture,
( ~ c8_2(X0,a392)
| c7_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c5_2(X0,a392)
| ~ c10_1(X0)
| ~ c1_2(X0,X1)
| ssSkP5(X0) ) ).
cnf(u4457,negated_conjecture,
( ~ ssSkP0(X0)
| c1_2(X0,X1)
| ~ c4_2(X0,a274)
| ~ c10_2(X0,a274)
| c9_1(X0)
| c2_2(X0,X1)
| c8_2(X0,X1) ) ).
cnf(u3931,negated_conjecture,
( ~ c6_1(X0)
| c2_2(X0,X1)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c10_2(X0,a428) ) ).
cnf(u4454,negated_conjecture,
( ~ c3_2(X2,X4)
| c8_2(X2,X3)
| c1_2(X2,X3)
| ~ c4_2(X2,X4)
| ~ c10_2(X2,X4)
| c9_1(X2)
| c2_2(X2,X3) ) ).
cnf(u3920,negated_conjecture,
ndr1_1(X0) ).
cnf(u4144,negated_conjecture,
( ~ c9_1(X0)
| c10_2(X0,X1)
| ~ c4_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u4244,negated_conjecture,
( ~ c6_2(X1,X2)
| c4_2(X1,X2)
| c1_2(X1,X2)
| c6_1(X1)
| c9_1(X1) ) ).
cnf(u4351,negated_conjecture,
( ~ c3_1(X0)
| c8_2(X0,a316)
| ~ c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u725,negated_conjecture,
( ~ c6_2(X0,a285)
| ~ ssSkP1(X0) ) ).
cnf(u690,negated_conjecture,
( ~ c3_2(X0,a412)
| ~ ssSkP6(X0) ) ).
cnf(u797,negated_conjecture,
( c3_2(X0,a274)
| ~ ssSkP0(X0) ) ).
cnf(clause65,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u4341,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_2(X0,X1)
| c1_2(X0,X1)
| c9_1(X0)
| c5_2(X0,a419) ) ).
cnf(u4371,negated_conjecture,
( ~ c3_2(X0,a411)
| c10_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| c1_1(X0) ) ).
cnf(u3911,negated_conjecture,
ndr1_1(a296) ).
cnf(u4471,negated_conjecture,
( ~ c6_1(X0)
| c6_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ c4_2(X0,X2)
| c1_2(X0,X1)
| ~ c7_2(X0,X2)
| c3_2(X0,X1) ) ).
cnf(u4339,negated_conjecture,
( ~ c1_2(X0,a419)
| ~ c6_2(X0,X1)
| c1_2(X0,X1)
| c9_1(X0)
| c5_2(X0,X1) ) ).
cnf(u798,negated_conjecture,
( c5_2(X0,a274)
| ~ ssSkP0(X0) ) ).
cnf(u4239,negated_conjecture,
~ ssSkP0(a348) ).
cnf(u691,negated_conjecture,
( ~ c5_2(X0,a412)
| ~ ssSkP6(X0) ) ).
cnf(u4242,negated_conjecture,
( c10_2(a427,X0)
| ~ c1_2(a427,X0)
| ~ c4_2(a427,X0) ) ).
cnf(u3909,negated_conjecture,
( c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u774,negated_conjecture,
( c2_2(X0,a391)
| ssSkP4(X0) ) ).
cnf(clause54,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u4179,negated_conjecture,
( ~ c5_2(X0,a328)
| c10_1(X0)
| c9_1(X0)
| c4_2(X0,a328)
| ~ c6_1(X0)
| c3_1(X0) ) ).
cnf(u3930,negated_conjecture,
( ~ c1_2(X0,a428)
| ~ c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X1) ) ).
cnf(u4346,negated_conjecture,
c8_1(a403) ).
cnf(u4283,negated_conjecture,
( ~ c10_2(X0,X2)
| c2_1(X0)
| c5_1(X0)
| c7_2(X0,X2)
| ~ c2_2(X0,X2) ) ).
cnf(u4220,negated_conjecture,
( c10_2(a296,X0)
| c2_2(a296,X0)
| c3_2(a296,X0) ) ).
cnf(u4164,negated_conjecture,
( ~ c2_2(X0,a276)
| ~ c6_1(X0)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u776,negated_conjecture,
( c4_2(X0,a379)
| ~ ssSkP2(X0) ) ).
cnf(u771,negated_conjecture,
( c4_2(X0,a412)
| ~ ssSkP6(X0) ) ).
cnf(u4350,negated_conjecture,
( ~ c8_2(X0,a400)
| ~ c2_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u699,negated_conjecture,
( c7_2(X0,a379)
| ~ ssSkP2(X0) ) ).
cnf(u4145,negated_conjecture,
( ~ c6_1(X0)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1)
| c4_2(X0,a276) ) ).
cnf(u3904,negated_conjecture,
c4_1(a427) ).
cnf(u4338,negated_conjecture,
( ~ c9_1(X0)
| ~ c7_2(X0,X1)
| c3_1(X0)
| c9_2(X0,X1)
| c2_2(X0,X1) ) ).
cnf(u775,negated_conjecture,
( c2_2(X0,a389)
| ssSkP3(X0) ) ).
cnf(u3905,negated_conjecture,
( c7_1(X1)
| c1_1(X1) ) ).
cnf(u4222,negated_conjecture,
( ~ c4_1(X0)
| ~ c1_1(X0)
| ~ c4_2(X0,X1)
| ~ c1_2(X0,X1)
| c10_2(X0,X1) ) ).
cnf(u4347,negated_conjecture,
c10_1(a403) ).
cnf(clause150,negated_conjecture,
( c1_2(X0,a392)
| ssSkP5(X0) ) ).
cnf(u649,negated_conjecture,
( ~ ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u4344,negated_conjecture,
( ~ c3_1(X0)
| ~ c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,X1)
| c3_2(X0,a316) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN420-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n019.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 15:55:48 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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.31 % (4119284)Will run a generic schedule for satisfiability detection.
% 0.21/0.31 % (4119313)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2209849616:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.31 % (4119310)% WARNING: option uhcvi not known.
% 0.21/0.31 % (4119310)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1232842149:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.31 % (4119312)dis+10_1_sil=32000:sp=arity:random_seed=3331153791:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.31 % (4119309)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2747598229_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.31 % (4119311)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3983155252:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.31 % (4119315)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=973145672:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.31 % (4119314)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=682258539:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.31 % (4119310) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4119284-4119310"...
% 0.21/0.31 % (4119313)Instruction limit reached!
% 0.21/0.31 % (4119313)------------------------------
% 0.21/0.31 % (4119313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (4119313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (4119313)CaDiCaL version: 2.1.3
% 0.21/0.31 % (4119313)Termination reason: Instruction limit
% 0.21/0.31 % (4119313)Termination phase: Saturation
% 0.21/0.31 % (4119313)Time elapsed: 0.037 s
% 0.21/0.31 % (4119313)Peak memory usage: 15 MB
% 0.21/0.31 % (4119313)Instructions burned: 120 (million)
% 0.21/0.31 % (4119310)...printing done.
% 0.21/0.31 % Detected minimum model sizes of [1]
% 0.21/0.31 % Detected maximum model sizes of [178]
% 0.21/0.31 % TRYING [1]
% 0.21/0.31 % SZS status Satisfiable for theBenchmark
% 0.21/0.31 % SZS output start Saturation.
% See solution above
% 0.21/0.31 % SZS output start Definitions and Model Updates.
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC12"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC35"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c5_2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c3_2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c4_2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c10_2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c1_0"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c2_2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c6_2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkP0"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkP1"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c6_1"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkP2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c9_1"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkP6"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c1_1"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c10_1"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC23"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC26"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c8_0"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC2"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC3"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC4"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC7"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC13"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC16"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC18"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC21"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC28"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC31"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "ssSkC37"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c6_0"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c9_0"
% 0.21/0.31 globally flip the polarity of every occurrence of predicate "c7_0"
% 0.21/0.31 % SZS output end Definitions and Model Updates.
% 0.21/0.31 % (4119310)------------------------------
% 0.21/0.31 % (4119310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (4119310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (4119310)CaDiCaL version: 2.1.3
% 0.21/0.31 % (4119310)Termination reason: Satisfiable
% 0.21/0.31 % (4119310)Time elapsed: 0.030 s
% 0.21/0.31 % (4119310)Peak memory usage: 14 MB
% 0.21/0.31 % (4119310)Instructions burned: 42 (million)
% 0.21/0.31 % (4119284)Success in time 0.092 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------