%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN418-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 01:50:33 PM UTC 2026
% Result : Satisfiable 3.17s 1.52s
% Output : Saturation 6.29s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u511,negated_conjecture,
( ~ c8_2(X2,X3)
| c5_1(X2)
| c2_2(X2,X4)
| c1_2(X2,X3)
| ~ c3_2(X2,X4)
| ~ c7_2(X2,X4)
| ~ ndr1_1(X2)
| ~ c5_2(X2,X3) ) ).
cnf(u514,negated_conjecture,
ndr1_0 ).
cnf(u547,negated_conjecture,
( c5_1(X4)
| c1_1(X4) ) ).
cnf(u557,negated_conjecture,
~ c5_0 ).
cnf(u561,negated_conjecture,
( ~ c2_2(X3,X4)
| c5_1(X3)
| c6_2(X3,X4)
| c8_2(X3,X4)
| ~ c1_1(X3)
| ~ ndr1_1(X3) ) ).
cnf(u579,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_1(X0)
| c3_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u582,negated_conjecture,
ssSkC2 ).
cnf(u595,negated_conjecture,
ndr1_1(a73) ).
cnf(u599,negated_conjecture,
( ~ c10_2(a73,X3)
| c5_2(a73,X3)
| ~ c7_2(a73,X3) ) ).
cnf(u602,negated_conjecture,
( ~ c5_2(X0,X1)
| c8_1(X0)
| c2_2(X0,X2)
| c9_2(X0,X2)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u606,negated_conjecture,
c6_0 ).
cnf(u613,negated_conjecture,
( ~ c5_2(X0,X1)
| c9_1(X0)
| c10_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u622,negated_conjecture,
c8_0 ).
cnf(u645,negated_conjecture,
c10_0 ).
cnf(u652,negated_conjecture,
( ~ c8_2(X0,X2)
| c7_2(X0,X1)
| ~ c4_2(X0,a40)
| ~ c3_2(X0,X2)
| ~ c6_2(X0,X2)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u655,negated_conjecture,
ssSkC9 ).
cnf(u659,negated_conjecture,
ssSkC8 ).
cnf(u664,negated_conjecture,
( ~ c8_2(X0,X2)
| c7_2(X0,X1)
| ~ c3_2(X0,a40)
| ~ c3_2(X0,X2)
| ~ c6_2(X0,X2)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u669,negated_conjecture,
c3_0 ).
cnf(u676,negated_conjecture,
( ~ c8_2(X0,X2)
| c9_2(X0,a40)
| c7_2(X0,X1)
| ~ c3_2(X0,X2)
| ~ c6_2(X0,X2)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u688,negated_conjecture,
~ c2_0 ).
cnf(u692,negated_conjecture,
( ~ c6_2(X2,X3)
| c7_1(X2)
| c8_2(X2,X3)
| c7_2(X2,X3)
| ~ ndr1_1(X2) ) ).
cnf(u707,negated_conjecture,
~ ssSkC27 ).
cnf(u711,negated_conjecture,
( ~ c1_2(X0,a131)
| c9_2(X0,X2)
| c2_2(X0,X1)
| c9_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u715,negated_conjecture,
( ~ c10_2(X0,a131)
| c9_2(X0,X2)
| c2_2(X0,X1)
| c9_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u723,negated_conjecture,
( ~ c7_2(X0,X2)
| c2_2(X0,a131)
| c9_2(X0,X2)
| c2_2(X0,X1)
| c9_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c6_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u727,negated_conjecture,
c4_0 ).
cnf(u731,negated_conjecture,
( ~ c8_2(X0,X2)
| c6_2(X0,X2)
| c9_2(X0,X2)
| c7_2(X0,X1)
| c8_2(X0,X1)
| ~ c7_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u735,negated_conjecture,
~ c9_0 ).
cnf(u739,negated_conjecture,
( ~ c9_2(X0,X1)
| c3_2(X0,X2)
| c2_2(X0,X2)
| ~ c10_2(X0,a42)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u742,negated_conjecture,
ssSkC10 ).
cnf(u747,negated_conjecture,
c7_1(a73) ).
cnf(u753,negated_conjecture,
~ c4_1(a73) ).
cnf(u757,negated_conjecture,
( ~ c9_2(X0,X1)
| c4_2(X0,a42)
| c3_2(X0,X2)
| c2_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u761,negated_conjecture,
( ~ c9_2(X0,X1)
| c5_2(X0,a42)
| c3_2(X0,X2)
| c2_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u765,negated_conjecture,
( ~ c8_2(X0,X1)
| c10_2(X0,a92)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u768,negated_conjecture,
ssSkC19 ).
cnf(u773,negated_conjecture,
( ~ c8_2(X0,X1)
| c9_2(X0,a92)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u777,negated_conjecture,
( ~ c8_2(X0,X1)
| c8_2(X0,a92)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u781,negated_conjecture,
c7_0 ).
cnf(u785,negated_conjecture,
( ~ c8_2(X0,X1)
| c6_1(X0)
| c1_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u792,negated_conjecture,
ssSkC3 ).
cnf(u797,negated_conjecture,
( ~ c5_2(X0,X1)
| c8_2(X0,a76)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u800,negated_conjecture,
ssSkC17 ).
cnf(u805,negated_conjecture,
( ~ c5_2(X0,X1)
| c6_2(X0,a76)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u809,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_2(X0,a76)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u817,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_1(X0)
| c10_1(X0)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u826,negated_conjecture,
( ~ c5_2(X0,X1)
| c6_2(X0,a83)
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u830,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_1(X0)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u834,negated_conjecture,
~ c1_0 ).
cnf(u838,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_1(X0)
| ~ c3_1(X0)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u850,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ c3_2(X0,a70)
| ~ ndr1_1(X0) ) ).
cnf(u853,negated_conjecture,
ssSkC16 ).
cnf(u858,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ c4_2(X0,a70)
| ~ ndr1_1(X0) ) ).
cnf(u862,negated_conjecture,
( ~ c5_2(X0,a70)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u910,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_1(X0)
| c10_2(X0,X1)
| c8_2(X0,X1)
| ~ c7_2(X0,a130)
| ~ ndr1_1(X0) ) ).
cnf(u914,negated_conjecture,
~ ssSkC14 ).
cnf(u918,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_2(X0,X1)
| c7_2(X0,X1)
| ~ c5_2(X0,a61)
| ~ ndr1_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u922,negated_conjecture,
( ~ c7_2(X0,X1)
| c10_1(X0)
| c10_2(X0,X1)
| ~ c9_2(X0,a52)
| ~ ndr1_1(X0) ) ).
cnf(u934,negated_conjecture,
~ ssSkC12 ).
cnf(u943,negated_conjecture,
ndr1_1(X2) ).
cnf(u947,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_1(X0)
| c1_2(X0,a130)
| c10_2(X0,X1)
| c8_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u959,negated_conjecture,
( ~ c1_2(X0,X1)
| c9_2(X0,a61)
| c5_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u964,negated_conjecture,
ssSkC23 ).
cnf(u975,negated_conjecture,
ndr1_1(a28) ).
cnf(u979,negated_conjecture,
( ~ c1_2(a28,X0)
| c5_2(a28,X0)
| ~ c8_2(a28,X0) ) ).
cnf(u995,negated_conjecture,
( ~ c7_2(X0,X1)
| c10_1(X0)
| c8_2(X0,a52)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1015,negated_conjecture,
( ~ c6_2(a28,X0)
| c3_2(a28,X0)
| c7_2(a28,X0) ) ).
cnf(u1047,negated_conjecture,
ndr1_1(a128) ).
cnf(u1056,negated_conjecture,
ssSkC4 ).
cnf(u1074,negated_conjecture,
ssSkC13 ).
cnf(u1090,negated_conjecture,
ndr1_1(a114) ).
cnf(u1094,negated_conjecture,
( ~ c8_2(a114,X0)
| c1_2(a114,X0)
| c10_2(a114,X0) ) ).
cnf(u1109,negated_conjecture,
( c7_1(X1)
| c6_1(X1) ) ).
cnf(u1112,negated_conjecture,
( ~ c1_2(X0,a146)
| ~ c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1115,negated_conjecture,
ssSkC30 ).
cnf(u1120,negated_conjecture,
( ~ c9_2(X0,a146)
| ~ c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1124,negated_conjecture,
ndr1_1(a75) ).
cnf(u1133,negated_conjecture,
ssSkC18 ).
cnf(u1145,negated_conjecture,
ssSkC21 ).
cnf(u1160,negated_conjecture,
( ~ c4_1(X1)
| c10_1(X1) ) ).
cnf(u1179,negated_conjecture,
( ~ c6_2(X0,a65)
| ~ c4_1(X0)
| ~ ssSkP4(X0) ) ).
cnf(u1191,negated_conjecture,
~ ssSkC6 ).
cnf(u1195,negated_conjecture,
ndr1_1(a31) ).
cnf(u1199,negated_conjecture,
( ~ c2_2(a31,X0)
| c6_2(a31,X0)
| c1_2(a31,X0) ) ).
cnf(u1203,negated_conjecture,
( ~ c8_1(X1)
| c1_1(X1) ) ).
cnf(u1206,negated_conjecture,
ssSkC11 ).
cnf(u1226,negated_conjecture,
( ~ ssSkP4(X0)
| c5_2(X0,a65)
| ~ c4_1(X0) ) ).
cnf(u1230,negated_conjecture,
( ~ ssSkP4(X0)
| c4_2(X0,a65)
| ~ c4_1(X0) ) ).
cnf(u1237,negated_conjecture,
ssSkC15 ).
cnf(u1254,negated_conjecture,
~ ssSkC25 ).
cnf(u1261,negated_conjecture,
ssSkC28 ).
cnf(u1274,negated_conjecture,
( ~ c7_1(X0)
| ndr1_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1281,negated_conjecture,
ndr1_1(a41) ).
cnf(u1287,negated_conjecture,
ssSkC24 ).
cnf(u1298,negated_conjecture,
ndr1_1(a108) ).
cnf(u1302,negated_conjecture,
( ~ c7_2(a108,X0)
| ~ c2_2(a108,X0) ) ).
cnf(u1305,negated_conjecture,
ssSkC22 ).
cnf(u1318,negated_conjecture,
( ~ ssSkP4(X0)
| ndr1_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1339,negated_conjecture,
ssSkC29 ).
cnf(u1350,negated_conjecture,
( ~ c5_2(X0,a145)
| c9_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1355,negated_conjecture,
~ c3_2(a3,a4) ).
cnf(u1361,negated_conjecture,
ssSkC0 ).
cnf(u1367,negated_conjecture,
~ c3_2(a3,a5) ).
cnf(u1372,negated_conjecture,
~ c1_2(a3,a5) ).
cnf(u1385,negated_conjecture,
ssSkC20 ).
cnf(u1404,negated_conjecture,
( ~ c4_2(X0,a80)
| c7_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1408,negated_conjecture,
( ~ c8_2(X0,a86)
| ~ ssSkP6(X0)
| ~ ssSkP7(X0) ) ).
cnf(u1412,negated_conjecture,
( ~ c2_2(X0,a86)
| ~ ssSkP6(X0)
| ~ ssSkP7(X0) ) ).
cnf(u1416,negated_conjecture,
( ~ c10_2(X0,a86)
| ~ ssSkP6(X0)
| ~ ssSkP7(X0) ) ).
cnf(u1453,negated_conjecture,
~ c1_1(a3) ).
cnf(u1458,negated_conjecture,
c5_2(a3,a4) ).
cnf(u1463,negated_conjecture,
c1_2(a3,a4) ).
cnf(u1468,negated_conjecture,
c7_2(a3,a5) ).
cnf(u1497,negated_conjecture,
~ c2_2(a22,a24) ).
cnf(u1503,negated_conjecture,
ssSkC5 ).
cnf(u1509,negated_conjecture,
~ c1_2(a22,a24) ).
cnf(u1514,negated_conjecture,
~ c6_2(a22,a24) ).
cnf(u1518,negated_conjecture,
( ~ ssSkP5(X0)
| c7_1(X0)
| c3_2(X0,a80) ) ).
cnf(u1522,negated_conjecture,
( ~ ssSkP5(X0)
| c7_1(X0)
| c10_2(X0,a80) ) ).
cnf(u1542,negated_conjecture,
( ~ c1_1(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u1551,negated_conjecture,
ndr1_1(a3) ).
cnf(u1555,negated_conjecture,
( ~ c3_1(X0)
| c3_2(X0,a25) ) ).
cnf(u1559,negated_conjecture,
( ~ c3_1(X0)
| c5_2(X0,a25) ) ).
cnf(u1563,negated_conjecture,
( ~ c3_1(X0)
| c8_2(X0,a25) ) ).
cnf(u1572,negated_conjecture,
c10_2(a22,a23) ).
cnf(u1577,negated_conjecture,
c7_2(a22,a23) ).
cnf(u1582,negated_conjecture,
c2_2(a22,a23) ).
cnf(u1586,negated_conjecture,
( ~ ssSkP5(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u1590,negated_conjecture,
( ~ ssSkP6(X0)
| ndr1_1(X0)
| ~ ssSkP7(X0) ) ).
cnf(u1598,negated_conjecture,
( ~ c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1618,negated_conjecture,
~ c4_2(a95,a96) ).
cnf(u1623,negated_conjecture,
~ c2_2(a95,a96) ).
cnf(u1649,negated_conjecture,
c8_1(a22) ).
cnf(u1654,negated_conjecture,
ndr1_1(a22) ).
cnf(u1664,negated_conjecture,
~ c10_1(a28) ).
cnf(u1684,negated_conjecture,
c8_2(a95,a96) ).
cnf(u1699,negated_conjecture,
~ c4_2(a114,a115) ).
cnf(u1704,negated_conjecture,
~ c5_2(a114,a115) ).
cnf(u1753,negated_conjecture,
ssSkC7 ).
cnf(u1795,negated_conjecture,
c4_1(a95) ).
cnf(u1800,negated_conjecture,
ndr1_1(a95) ).
cnf(u1825,negated_conjecture,
~ c2_2(a108,a109) ).
cnf(u1830,negated_conjecture,
~ c7_2(a108,a109) ).
cnf(u1835,negated_conjecture,
~ c2_2(a108,a110) ).
cnf(u1845,negated_conjecture,
~ c1_1(a114) ).
cnf(u1850,negated_conjecture,
c2_2(a114,a115) ).
cnf(u1875,negated_conjecture,
~ c4_1(a128) ).
cnf(u1880,negated_conjecture,
~ c1_1(a128) ).
cnf(u1971,negated_conjecture,
~ c7_2(a31,a32) ).
cnf(u2081,negated_conjecture,
ssSkC26 ).
cnf(u2113,negated_conjecture,
~ ssSkC1 ).
cnf(u2208,negated_conjecture,
c1_2(a108,a109) ).
cnf(u2213,negated_conjecture,
c3_2(a108,a110) ).
cnf(u2276,negated_conjecture,
~ c4_1(a6) ).
cnf(u2281,negated_conjecture,
~ c6_1(a6) ).
cnf(u2336,negated_conjecture,
~ c5_1(a31) ).
cnf(u2341,negated_conjecture,
c8_2(a31,a32) ).
cnf(u2346,negated_conjecture,
c3_2(a31,a32) ).
cnf(u2371,negated_conjecture,
~ c10_1(a41) ).
cnf(u2391,negated_conjecture,
~ c10_1(a55) ).
cnf(u2396,negated_conjecture,
~ c6_1(a55) ).
cnf(u2406,negated_conjecture,
~ c2_1(a75) ).
cnf(u2411,negated_conjecture,
~ c9_1(a75) ).
cnf(u2451,negated_conjecture,
~ c10_1(a121) ).
cnf(u2456,negated_conjecture,
~ c6_1(a121) ).
cnf(u2461,negated_conjecture,
~ c9_1(a121) ).
cnf(u2608,negated_conjecture,
c10_1(a6) ).
cnf(u2807,negated_conjecture,
~ c7_2(a73,a80) ).
cnf(u2840,negated_conjecture,
~ c10_1(a73) ).
cnf(u2883,negated_conjecture,
~ c9_2(a3,a52) ).
cnf(u2918,negated_conjecture,
c8_2(a3,a52) ).
cnf(u2930,negated_conjecture,
~ c6_2(a22,a23) ).
cnf(u2935,negated_conjecture,
c5_1(a22) ).
cnf(u2940,negated_conjecture,
c8_2(a114,a115) ).
cnf(u2943,negated_conjecture,
~ c6_2(a114,a115) ).
cnf(u2954,negated_conjecture,
c10_2(a114,a115) ).
cnf(u2967,negated_conjecture,
~ c8_1(a3) ).
cnf(u2971,negated_conjecture,
~ c4_1(a3) ).
cnf(u2975,negated_conjecture,
c2_2(a3,a52) ).
cnf(u2987,negated_conjecture,
~ c8_1(a31) ).
cnf(u2991,negated_conjecture,
~ c4_1(a31) ).
cnf(u3000,negated_conjecture,
~ c8_1(a95) ).
cnf(u3013,negated_conjecture,
c5_1(a3) ).
cnf(u3018,negated_conjecture,
c7_2(a3,a4) ).
cnf(u3031,negated_conjecture,
~ c5_1(a108) ).
cnf(u3055,negated_conjecture,
~ c10_2(a108,a109) ).
cnf(u3058,negated_conjecture,
c7_1(a108) ).
cnf(u3072,negated_conjecture,
~ c10_2(a3,a4) ).
cnf(u3075,negated_conjecture,
c7_1(a3) ).
cnf(u3112,negated_conjecture,
~ c6_2(a3,a52) ).
cnf(u3128,negated_conjecture,
c6_2(a95,a96) ).
cnf(u3133,negated_conjecture,
~ c3_1(a95) ).
cnf(u3150,negated_conjecture,
c6_1(a114) ).
cnf(u3155,negated_conjecture,
~ c6_2(a31,a32) ).
cnf(u3159,negated_conjecture,
~ c3_1(a31) ).
cnf(u3204,negated_conjecture,
~ ssSkP2(a108) ).
cnf(u3221,negated_conjecture,
~ c3_2(a108,a60) ).
cnf(u3233,negated_conjecture,
~ c2_2(a108,a60) ).
cnf(u3248,negated_conjecture,
~ c3_2(a108,a70) ).
cnf(u3253,negated_conjecture,
~ c4_2(a108,a70) ).
cnf(u3265,negated_conjecture,
~ c9_2(a108,a52) ).
cnf(u3274,negated_conjecture,
c8_2(a108,a52) ).
cnf(u3284,negated_conjecture,
~ c8_1(a108) ).
cnf(u3292,negated_conjecture,
c2_2(a108,a52) ).
cnf(u3304,negated_conjecture,
c6_2(a108,a52) ).
cnf(u3313,negated_conjecture,
c6_1(a108) ).
cnf(u3344,negated_conjecture,
~ c9_2(a95,a96) ).
cnf(u3356,negated_conjecture,
~ c9_2(a114,a115) ).
cnf(u3360,negated_conjecture,
~ c10_2(a114,a42) ).
cnf(u3367,negated_conjecture,
c9_2(a31,a32) ).
cnf(u3372,negated_conjecture,
~ c10_2(a31,a42) ).
cnf(u3375,negated_conjecture,
( ~ c7_2(a31,X0)
| c3_2(a31,X0)
| c2_2(a31,X0) ) ).
cnf(u3390,negated_conjecture,
c4_2(a31,a42) ).
cnf(u3447,negated_conjecture,
~ c5_2(a95,a96) ).
cnf(u3463,negated_conjecture,
~ c5_2(a108,a52) ).
cnf(u3471,negated_conjecture,
~ c5_2(a31,a32) ).
cnf(u3496,negated_conjecture,
c7_1(a95) ).
cnf(u3505,negated_conjecture,
~ c7_1(a114) ).
cnf(u3535,negated_conjecture,
~ c2_2(a108,a79) ).
cnf(u3572,negated_conjecture,
~ c3_2(a95,a96) ).
cnf(u3592,negated_conjecture,
c3_2(a114,a80) ).
cnf(u3597,negated_conjecture,
c10_2(a114,a80) ).
cnf(u3611,negated_conjecture,
~ c6_2(a108,a79) ).
cnf(u3652,negated_conjecture,
~ c3_2(a108,a52) ).
cnf(u3681,negated_conjecture,
~ c6_2(a108,a60) ).
cnf(u3709,negated_conjecture,
~ c6_2(a3,a4) ).
cnf(u3725,negated_conjecture,
~ c6_2(a3,a5) ).
cnf(clause228,negated_conjecture,
( ~ c9_2(X0,a60)
| ssSkP2(X0) ) ).
cnf(u2761,negated_conjecture,
( c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u2789,negated_conjecture,
c1_1(a31) ).
cnf(clause135,negated_conjecture,
( ssSkP1(X0)
| c7_2(X0,a57) ) ).
cnf(u3414,negated_conjecture,
( ~ c5_2(a95,X0)
| c7_2(a95,X0)
| c6_2(a95,X0) ) ).
cnf(u2759,negated_conjecture,
( ~ c2_2(X3,X4)
| c5_1(X3)
| c6_2(X3,X4)
| c8_2(X3,X4)
| ~ ndr1_1(X3) ) ).
cnf(clause51,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause220,negated_conjecture,
( ~ c8_2(X0,a84)
| ssSkP6(X0) ) ).
cnf(clause227,negated_conjecture,
( ~ c9_2(X0,a62)
| ssSkP3(X0) ) ).
cnf(u3210,negated_conjecture,
c5_2(a108,a60) ).
cnf(clause133,negated_conjecture,
( ssSkP2(X0)
| c7_2(X0,a60) ) ).
cnf(u2835,negated_conjecture,
( ~ c8_2(X0,X2)
| c8_1(X0)
| c2_2(X0,X2)
| c9_2(X0,X2)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(clause58,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause231,negated_conjecture,
( ~ c3_2(X0,a49)
| ssSkP0(X0) ) ).
cnf(u3493,negated_conjecture,
( ~ c3_2(a3,X0)
| c8_2(a3,X0)
| c7_2(a3,X0) ) ).
cnf(u2788,negated_conjecture,
( ~ c8_2(X0,X1)
| c5_2(X0,a42)
| c3_2(X0,X2)
| c2_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ c9_2(X0,X1) ) ).
cnf(u3100,negated_conjecture,
c9_1(a3) ).
cnf(u2781,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,a76)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(clause62,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u2776,negated_conjecture,
( ~ c7_2(X0,a130)
| c5_1(X0)
| c10_2(X0,X1)
| c8_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(clause225,negated_conjecture,
( ~ c6_2(X0,a64)
| ssSkP4(X0) ) ).
cnf(u2777,negated_conjecture,
( ~ c6_2(X0,X1)
| c5_1(X0)
| c1_2(X0,a130)
| c10_2(X0,X1)
| c8_2(X0,X1) ) ).
cnf(u2786,negated_conjecture,
( ~ c8_2(X0,X1)
| c3_2(X0,X2)
| c2_2(X0,X2)
| ~ c10_2(X0,a42)
| ~ c7_2(X0,X2)
| ~ c9_2(X0,X1) ) ).
cnf(clause53,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(clause125,negated_conjecture,
( ssSkP6(X0)
| c9_2(X0,a84) ) ).
cnf(clause229,negated_conjecture,
( ~ c5_2(X0,a57)
| ssSkP1(X0) ) ).
cnf(u2775,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_1(X0)
| ~ c8_1(X0) ) ).
cnf(u2827,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_1(X0)
| c10_1(X0)
| c8_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(clause60,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u2906,negated_conjecture,
c1_1(a22) ).
cnf(clause127,negated_conjecture,
( ssSkP5(X0)
| c2_2(X0,a79) ) ).
cnf(clause134,negated_conjecture,
( ssSkP2(X0)
| c5_2(X0,a60) ) ).
cnf(clause221,negated_conjecture,
( ~ c8_2(X0,a79)
| ssSkP5(X0) ) ).
cnf(clause219,negated_conjecture,
( ~ c9_2(X0,a85)
| ssSkP7(X0) ) ).
cnf(clause52,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause131,negated_conjecture,
( ssSkP3(X0)
| c3_2(X0,a62) ) ).
cnf(clause59,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause226,negated_conjecture,
( ~ c9_2(X0,a64)
| ssSkP4(X0) ) ).
cnf(u2787,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a42)
| c3_2(X0,X2)
| c2_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ c9_2(X0,X1) ) ).
cnf(clause132,negated_conjecture,
( ssSkP3(X0)
| c5_2(X0,a62) ) ).
cnf(u2793,negated_conjecture,
( c7_1(X0)
| c3_2(X0,a80)
| c2_2(X0,a79) ) ).
cnf(clause126,negated_conjecture,
( ssSkP6(X0)
| c5_2(X0,a84) ) ).
cnf(clause230,negated_conjecture,
( ~ c4_2(X0,a57)
| ssSkP1(X0) ) ).
cnf(u2782,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,a76)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u2783,negated_conjecture,
( ~ c1_2(X0,X1)
| c7_2(X0,a76)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u3211,negated_conjecture,
c7_2(a108,a60) ).
cnf(clause123,negated_conjecture,
( ssSkP7(X0)
| c6_2(X0,a85) ) ).
cnf(u3040,negated_conjecture,
c1_1(a108) ).
cnf(clause139,negated_conjecture,
( ssSkP0(X0)
| c7_2(X0,a49) ) ).
cnf(clause138,negated_conjecture,
( ssSkP0(X0)
| c5_2(X0,a49) ) ).
cnf(clause61,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u2796,negated_conjecture,
( c7_1(X0)
| c10_2(X0,a80)
| c2_2(X0,a79) ) ).
cnf(u2907,negated_conjecture,
c10_1(a95) ).
cnf(clause124,negated_conjecture,
( ssSkP7(X0)
| c3_2(X0,a85) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN418-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 % Computer : n004.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 15:55:07 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.26 Running first-order theorem proving
% 0.09/0.26 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.17/1.51 % (489638)Input is clausal, will run a generic CNF schedule.
% 3.17/1.51 % (489648)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2102102554:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.17/1.51 % (489649)dis-21_1_sil=8000:lcm=predicate:random_seed=3011394186:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.17/1.51 % (489648)Refutation not found, incomplete strategy
% 3.17/1.51 % (489648)------------------------------
% 3.17/1.51 % (489648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.17/1.51 % (489648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.17/1.51 % (489648)CaDiCaL version: 2.1.3
% 3.17/1.51 % (489648)Termination reason: Refutation not found, incomplete strategy
% 3.17/1.51 % (489648)Time elapsed: 0.018 s
% 3.17/1.51 % (489648)Peak memory usage: 90 MB
% 3.17/1.51 % (489648)Instructions burned: 32 (million)
% 3.17/1.51 % (489649)Instruction limit reached!
% 3.17/1.51 % (489649)------------------------------
% 3.17/1.51 % (489649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.17/1.51 % (489649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.17/1.51 % (489649)CaDiCaL version: 2.1.3
% 3.17/1.51 % (489649)Termination reason: Instruction limit
% 3.17/1.51 % (489649)Termination phase: Saturation
% 3.17/1.51 % (489649)Time elapsed: 0.073 s
% 3.17/1.51 % (489649)Peak memory usage: 90 MB
% 3.17/1.51 % (489649)Instructions burned: 117 (million)
% 3.17/1.51 % (489643)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3036611407:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.17/1.51 % (489646)lrs+10_1_sil=8000:sp=occurrence:random_seed=4091828301:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.17/1.51 % (489647)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3241194312:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.17/1.51 % (489644)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4051729155:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.17/1.51 % (489645)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4211062644:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.17/1.51 % (489646)Instruction limit reached!
% 3.17/1.51 % (489646)------------------------------
% 3.17/1.51 % (489646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.17/1.51 % (489646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.17/1.51 % (489646)CaDiCaL version: 2.1.3
% 3.17/1.51 % (489646)Termination reason: Instruction limit
% 3.17/1.51 % (489646)Termination phase: Saturation
% 3.17/1.51 % (489646)Time elapsed: 0.095 s
% 3.17/1.51 % (489646)Peak memory usage: 90 MB
% 3.17/1.51 % (489646)Instructions burned: 107 (million)
% 3.17/1.51 % (489647)Instruction limit reached!
% 3.17/1.51 % (489647)------------------------------
% 3.17/1.51 % (489647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.17/1.51 % (489647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.17/1.52 % (489647)CaDiCaL version: 2.1.3
% 3.17/1.52 % (489647)Termination reason: Instruction limit
% 3.17/1.52 % (489647)Termination phase: Saturation
% 3.17/1.52 % (489647)Time elapsed: 0.107 s
% 3.17/1.52 % (489647)Peak memory usage: 90 MB
% 3.17/1.52 % (489647)Instructions burned: 118 (million)
% 3.17/1.52 % (489648)------------------------------
% 3.17/1.52 % (489648)------------------------------
% 3.17/1.52 % (489657)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2169190019:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 3.17/1.52 % (489663)lrs+10_64_to=lpo:sil=8000:random_seed=665623573:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 3.17/1.52 % (489663)First to succeed.
% 3.17/1.52 % (489663)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-489638"
% 3.17/1.52 % (489660)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3790363716:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 3.17/1.52 % (489661)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=127396713:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 3.17/1.52 % (489660)Refutation not found, incomplete strategy
% 3.17/1.52 % (489660)------------------------------
% 3.17/1.52 % (489660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.17/1.52 % (489660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.17/1.52 % (489660)CaDiCaL version: 2.1.3
% 3.17/1.52 % (489660)Termination reason: Refutation not found, incomplete strategy
% 3.17/1.52 % (489660)Time elapsed: 0.051 s
% 3.17/1.52 % (489660)Peak memory usage: 90 MB
% 3.17/1.52 % (489660)Instructions burned: 56 (million)
% 3.17/1.52 % (489657)Instruction limit reached!
% 3.17/1.52 % (489657)------------------------------
% 3.17/1.52 % (489657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.17/1.52 % (489657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.17/1.52 % (489657)CaDiCaL version: 2.1.3
% 3.17/1.52 % (489657)Termination reason: Instruction limit
% 3.17/1.52 % (489657)Termination phase: Saturation
% 3.17/1.52 % (489657)Time elapsed: 0.124 s
% 3.17/1.52 % (489657)Peak memory usage: 90 MB
% 3.17/1.52 % (489657)Instructions burned: 143 (million)
% 3.17/1.52 % (489661)Instruction limit reached!
% 3.17/1.52 % (489661)------------------------------
% 3.17/1.52 % (489661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.17/1.52 % (489661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.17/1.52 % (489661)CaDiCaL version: 2.1.3
% 3.17/1.52 % (489661)Termination reason: Instruction limit
% 3.17/1.52 % (489661)Termination phase: Saturation
% 3.17/1.52 % (489661)Time elapsed: 0.127 s
% 3.17/1.52 % (489661)Peak memory usage: 92 MB
% 3.17/1.52 % (489661)Instructions burned: 219 (million)
% 3.17/1.52 % SZS status Satisfiable for theBenchmark
% 3.17/1.52 % SZS output start Saturation.
% See solution above
% 6.29/1.74 % SZS output start Definitions and Model Updates.
% 6.29/1.74 % SZS output end Definitions and Model Updates.
% 6.29/1.74 % (489663)------------------------------
% 6.29/1.74 % (489663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.74 % (489663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.74 % (489663)CaDiCaL version: 2.1.3
% 6.29/1.74 % (489663)Termination reason: Satisfiable
% 6.29/1.74 % (489663)Time elapsed: 0.014 s
% 6.29/1.74 % (489663)Peak memory usage: 90 MB
% 6.29/1.74 % (489663)Instructions burned: 40 (million)
% 6.29/1.74 % (489663)------------------------------
% 6.29/1.74 % (489663)------------------------------
% 6.29/1.74 % (489638)Success in time 0.805 s
% 6.29/1.74 % Vampire exiting
%------------------------------------------------------------------------------