%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN514-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:00:47 PM UTC 2026
% Result : Satisfiable 9.54s 1.95s
% Output : Saturation 11.31s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u291,negated_conjecture,
( ~ c2_2(X2,X3)
| c3_1(X2)
| c2_1(X2)
| c3_2(X2,X3)
| ~ ndr1_1(X2)
| ~ c4_2(X2,X3) ) ).
cnf(u294,negated_conjecture,
ndr1_0 ).
cnf(u308,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_1(X0)
| c4_2(X0,X1)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u318,negated_conjecture,
~ ndr1_1(a249) ).
cnf(u338,negated_conjecture,
( ~ c4_2(X1,X2)
| c1_1(X1)
| c3_2(X1,X2)
| c1_2(X1,X2)
| ~ c2_1(X1)
| ~ ndr1_1(X1) ) ).
cnf(u355,negated_conjecture,
c3_0 ).
cnf(u362,negated_conjecture,
( ~ c3_2(X0,X2)
| c5_1(X0)
| c4_2(X0,X2)
| ~ c1_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u368,negated_conjecture,
~ c1_0 ).
cnf(u386,negated_conjecture,
( ~ c3_2(X2,X3)
| c4_1(X2)
| c5_2(X2,a205)
| c2_2(X2,X3)
| ~ ndr1_1(X2)
| ~ c1_2(X2,X3) ) ).
cnf(u393,negated_conjecture,
( ~ c3_2(X2,X3)
| c4_1(X2)
| c4_2(X2,a205)
| c2_2(X2,X3)
| ~ ndr1_1(X2)
| ~ c1_2(X2,X3) ) ).
cnf(u397,negated_conjecture,
( ~ c3_2(X2,X3)
| c4_1(X2)
| c3_2(X2,a205)
| c2_2(X2,X3)
| ~ ndr1_1(X2)
| ~ c1_2(X2,X3) ) ).
cnf(u434,negated_conjecture,
( ~ c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c2_1(X0)
| ~ c4_2(X0,X2)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u438,negated_conjecture,
( ~ c3_2(X0,X1)
| ~ c5_2(X0,a196)
| ~ c2_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u441,negated_conjecture,
ssSkC1 ).
cnf(u446,negated_conjecture,
( ~ c3_2(X0,a196)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u451,negated_conjecture,
~ c3_1(a240) ).
cnf(u458,negated_conjecture,
( ~ c3_2(X0,X1)
| c4_2(X0,a196)
| ~ c2_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u465,negated_conjecture,
( ~ c2_2(X0,X1)
| c4_1(X0)
| c2_1(X0)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u477,negated_conjecture,
~ c5_0 ).
cnf(u481,negated_conjecture,
( ~ c3_2(X0,X2)
| c2_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_2(X0,a224)
| ~ c5_2(X0,X2)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u486,negated_conjecture,
c2_1(a240) ).
cnf(u490,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_2(X0,a221)
| c5_2(X0,X2)
| c1_2(X0,X2)
| c2_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u494,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_2(X0,a221)
| c5_2(X0,X2)
| c1_2(X0,X2)
| c2_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u498,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_2(X0,a221)
| c5_2(X0,X2)
| c1_2(X0,X2)
| c2_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u502,negated_conjecture,
( ~ c3_2(X0,X2)
| c4_2(X0,a224)
| c2_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u506,negated_conjecture,
( ~ c3_2(X0,X2)
| c1_2(X0,a224)
| c2_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_2(X0,X2)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u517,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u532,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_1(X0)
| c5_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u540,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0)
| ~ c5_2(X0,a190)
| ~ ndr1_1(X0) ) ).
cnf(u544,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_2(X0,a190)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u548,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a190)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u575,negated_conjecture,
~ ssSkC6 ).
cnf(u579,negated_conjecture,
( ~ c5_2(X0,a218)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u583,negated_conjecture,
~ c2_0 ).
cnf(u587,negated_conjecture,
( ~ c4_2(X0,X1)
| c5_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u591,negated_conjecture,
( ~ c4_2(X0,a184)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u600,negated_conjecture,
( ~ c1_1(X0)
| c2_2(X0,a218)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u604,negated_conjecture,
( ~ c1_1(X0)
| c1_2(X0,a218)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u609,negated_conjecture,
ssSkC8 ).
cnf(u616,negated_conjecture,
( ~ c3_2(X0,a181)
| c5_1(X0)
| c1_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u620,negated_conjecture,
( ~ c5_1(X0)
| c3_2(X0,a184)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u624,negated_conjecture,
( ~ c5_1(X0)
| c1_2(X0,a184)
| c5_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u640,negated_conjecture,
( ~ c4_2(X0,X1)
| c5_1(X0)
| c5_2(X0,a181)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u644,negated_conjecture,
( ~ c4_2(X0,X1)
| c5_1(X0)
| c1_2(X0,a181)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u648,negated_conjecture,
ndr1_1(a186) ).
cnf(u652,negated_conjecture,
( ~ c3_2(a186,X0)
| ~ c1_2(a186,X0)
| ~ c2_2(a186,X0) ) ).
cnf(u656,negated_conjecture,
~ ssSkC0 ).
cnf(u668,negated_conjecture,
( ~ c5_2(X0,a223)
| c1_2(X0,X1)
| ~ ssSkP3(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u673,negated_conjecture,
~ ndr1_1(a226) ).
cnf(u679,negated_conjecture,
ssSkC7 ).
cnf(u687,negated_conjecture,
( ~ c5_1(X0)
| c4_1(X0) ) ).
cnf(u699,negated_conjecture,
~ ssSkC4 ).
cnf(u703,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_1(X0)
| c5_2(X0,a206)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u707,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_1(X0)
| c3_2(X0,a206)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u711,negated_conjecture,
ndr1_1(a177) ).
cnf(u715,negated_conjecture,
( ~ c1_2(a177,X0)
| c5_2(a177,X0)
| c4_2(a177,X0) ) ).
cnf(u719,negated_conjecture,
ndr1_1(a182) ).
cnf(u723,negated_conjecture,
( ~ c4_2(a182,X0)
| c5_2(a182,X0)
| c1_2(a182,X0) ) ).
cnf(u731,negated_conjecture,
( ~ c5_2(a193,X0)
| c3_2(a193,X0)
| ~ c4_2(a193,X0) ) ).
cnf(u735,negated_conjecture,
ndr1_1(a199) ).
cnf(u743,negated_conjecture,
~ ssSkC2 ).
cnf(u747,negated_conjecture,
ndr1_1(a211) ).
cnf(u751,negated_conjecture,
( ~ c1_2(a211,X0)
| c5_2(a211,X0)
| c2_2(a211,X0) ) ).
cnf(u755,negated_conjecture,
ndr1_1(a214) ).
cnf(u759,negated_conjecture,
( ~ c2_2(a214,X0)
| c3_2(a214,X0)
| ~ c4_2(a214,X0) ) ).
cnf(u762,negated_conjecture,
ssSkC5 ).
cnf(u767,negated_conjecture,
( ~ c5_2(X0,X1)
| c3_2(X0,a223)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u771,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,a223)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u792,negated_conjecture,
ssSkC16 ).
cnf(u803,negated_conjecture,
( ~ c3_2(X0,X1)
| c1_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u807,negated_conjecture,
ndr1_1(a189) ).
cnf(u811,negated_conjecture,
( ~ c5_2(a189,X0)
| c1_2(a189,X0)
| ~ c4_2(a189,X0) ) ).
cnf(u815,negated_conjecture,
ndr1_1(a192) ).
cnf(u819,negated_conjecture,
( ~ c5_2(a192,X0)
| c3_2(a192,X0)
| c2_2(a192,X0) ) ).
cnf(u827,negated_conjecture,
ndr1_1(a202) ).
cnf(u831,negated_conjecture,
( ~ c1_2(a202,X0)
| c5_2(a202,X0)
| c2_2(a202,X0) ) ).
cnf(u835,negated_conjecture,
( ~ c1_2(X0,a198)
| ~ c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u839,negated_conjecture,
( ~ c5_2(a177,X0)
| c2_2(a177,X0) ) ).
cnf(u843,negated_conjecture,
ndr1_1(a259) ).
cnf(u847,negated_conjecture,
( ~ c1_2(a259,X0)
| ~ c5_2(a259,X0) ) ).
cnf(u850,negated_conjecture,
ssSkC14 ).
cnf(u854,negated_conjecture,
ssSkC13 ).
cnf(u859,negated_conjecture,
( ~ c4_1(X0)
| c5_2(X0,a198)
| ~ c5_1(X0) ) ).
cnf(u864,negated_conjecture,
ssSkC10 ).
cnf(u867,negated_conjecture,
( ~ c4_2(X0,a247)
| c4_1(X0)
| ~ c3_1(X0) ) ).
cnf(u880,negated_conjecture,
~ ndr1_1(a185) ).
cnf(u899,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u904,negated_conjecture,
ssSkC9 ).
cnf(u924,negated_conjecture,
ssSkC11 ).
cnf(u939,negated_conjecture,
ndr1_1(a188) ).
cnf(u943,negated_conjecture,
( ~ c4_2(a188,X0)
| c2_2(a188,X0) ) ).
cnf(u947,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u955,negated_conjecture,
( ~ c2_2(X0,a217)
| c3_1(X0)
| ~ ssSkP2(X0) ) ).
cnf(u1003,negated_conjecture,
( ~ ssSkP2(X0)
| c3_1(X0)
| c3_2(X0,a217) ) ).
cnf(u1023,negated_conjecture,
( ~ c5_1(X0)
| c5_2(X0,a178) ) ).
cnf(u1027,negated_conjecture,
( ~ c5_1(X0)
| c4_2(X0,a178) ) ).
cnf(u1031,negated_conjecture,
( ~ c5_1(X0)
| c3_2(X0,a178) ) ).
cnf(u1053,negated_conjecture,
( ~ ssSkP2(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1057,negated_conjecture,
( ~ c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u1067,negated_conjecture,
~ c1_2(a211,a212) ).
cnf(u1116,negated_conjecture,
~ c2_1(a182) ).
cnf(u1121,negated_conjecture,
~ c3_2(a186,a187) ).
cnf(u1126,negated_conjecture,
~ c2_2(a186,a187) ).
cnf(u1146,negated_conjecture,
c5_2(a211,a212) ).
cnf(u1151,negated_conjecture,
c2_2(a211,a212) ).
cnf(u1156,negated_conjecture,
~ c5_2(a214,a215) ).
cnf(u1161,negated_conjecture,
~ c3_2(a214,a215) ).
cnf(u1166,negated_conjecture,
~ c1_2(a214,a215) ).
cnf(u1192,negated_conjecture,
~ c4_2(a263,a264) ).
cnf(u1196,negated_conjecture,
~ ssSkC15 ).
cnf(u1207,negated_conjecture,
c3_1(a177) ).
cnf(u1212,negated_conjecture,
~ c3_2(a179,a180) ).
cnf(u1217,negated_conjecture,
~ c1_2(a179,a180) ).
cnf(u1222,negated_conjecture,
~ c1_1(a186) ).
cnf(u1226,negated_conjecture,
~ c1_2(a186,a187) ).
cnf(u1232,negated_conjecture,
~ c1_1(a191) ).
cnf(u1237,negated_conjecture,
~ c4_1(a192) ).
cnf(u1247,negated_conjecture,
~ c4_1(a199) ).
cnf(u1252,negated_conjecture,
~ c1_1(a199) ).
cnf(u1257,negated_conjecture,
~ c1_1(a201) ).
cnf(u1260,negated_conjecture,
ssSkC3 ).
cnf(u1281,negated_conjecture,
c3_1(a211) ).
cnf(u1287,negated_conjecture,
~ c3_1(a214) ).
cnf(u1310,negated_conjecture,
~ c5_1(a248) ).
cnf(u1315,negated_conjecture,
~ c3_1(a255) ).
cnf(u1318,negated_conjecture,
ssSkC12 ).
cnf(u1324,negated_conjecture,
~ c1_1(a259) ).
cnf(u1329,negated_conjecture,
~ c1_1(a263) ).
cnf(u1334,negated_conjecture,
c3_2(a263,a264) ).
cnf(u1339,negated_conjecture,
c1_2(a263,a264) ).
cnf(u1374,negated_conjecture,
~ c4_1(a260) ).
cnf(u1379,negated_conjecture,
c4_2(a260,a261) ).
cnf(u1384,negated_conjecture,
c2_2(a260,a261) ).
cnf(u1389,negated_conjecture,
c1_2(a260,a261) ).
cnf(u1396,negated_conjecture,
~ c3_1(a179) ).
cnf(u1401,negated_conjecture,
c5_2(a179,a180) ).
cnf(u1407,negated_conjecture,
~ c3_1(a189) ).
cnf(u1412,negated_conjecture,
c2_1(a191) ).
cnf(u1417,negated_conjecture,
c2_1(a192) ).
cnf(u1421,negated_conjecture,
~ c5_1(a193) ).
cnf(u1427,negated_conjecture,
c2_1(a201) ).
cnf(u1459,negated_conjecture,
c4_1(a248) ).
cnf(u1463,negated_conjecture,
~ ndr1_1(a263) ).
cnf(u1469,negated_conjecture,
c2_1(a185) ).
cnf(u1509,negated_conjecture,
c1_1(a260) ).
cnf(u1514,negated_conjecture,
ndr1_1(a260) ).
cnf(u1526,negated_conjecture,
ndr1_1(a179) ).
cnf(u1531,negated_conjecture,
c5_1(a188) ).
cnf(u1536,negated_conjecture,
c3_1(a202) ).
cnf(u1652,negated_conjecture,
~ c4_1(a177) ).
cnf(u1661,negated_conjecture,
~ c4_1(a211) ).
cnf(u1670,negated_conjecture,
~ c4_1(a202) ).
cnf(u1721,negated_conjecture,
~ c3_1(a186) ).
cnf(u1731,negated_conjecture,
c3_1(a263) ).
cnf(u1739,negated_conjecture,
~ c3_1(a188) ).
cnf(u1906,negated_conjecture,
c4_1(a226) ).
cnf(u1911,negated_conjecture,
c2_1(a226) ).
cnf(u1925,negated_conjecture,
c4_1(a249) ).
cnf(u1930,negated_conjecture,
c2_1(a249) ).
cnf(u1948,negated_conjecture,
~ c2_1(a260) ).
cnf(u1951,negated_conjecture,
~ c5_2(a260,a261) ).
cnf(u1966,negated_conjecture,
c5_2(a186,a187) ).
cnf(u1969,negated_conjecture,
~ c5_1(a186) ).
cnf(u1987,negated_conjecture,
c4_1(a263) ).
cnf(u1992,negated_conjecture,
c2_1(a263) ).
cnf(u2008,negated_conjecture,
~ c5_2(a186,a206) ).
cnf(u2013,negated_conjecture,
c4_1(a186) ).
cnf(u2034,negated_conjecture,
~ ssSkP3(a179) ).
cnf(u2043,negated_conjecture,
~ ssSkP3(a211) ).
cnf(u2061,negated_conjecture,
~ c5_2(a186,a190) ).
cnf(u2065,negated_conjecture,
c4_2(a186,a187) ).
cnf(u2075,negated_conjecture,
c2_2(a186,a190) ).
cnf(u2085,negated_conjecture,
~ c1_2(a186,a190) ).
cnf(u2096,negated_conjecture,
c3_2(a260,a261) ).
cnf(u2110,negated_conjecture,
~ c4_2(a211,a212) ).
cnf(u2136,negated_conjecture,
( c5_2(a260,X0)
| c1_2(a260,X0)
| c4_2(a260,X0) ) ).
cnf(u2157,negated_conjecture,
~ c3_2(a186,a184) ).
cnf(u2166,negated_conjecture,
c3_2(a188,a184) ).
cnf(u2180,negated_conjecture,
c1_2(a186,a184) ).
cnf(u2185,negated_conjecture,
c1_2(a188,a184) ).
cnf(u2207,negated_conjecture,
c5_2(a186,a221) ).
cnf(u2225,negated_conjecture,
~ ssSkP3(a188) ).
cnf(u2228,negated_conjecture,
~ c1_2(a188,a178) ).
cnf(u2265,negated_conjecture,
c1_1(a188) ).
cnf(u2273,negated_conjecture,
( ~ c2_2(a188,X0)
| ~ c1_2(a188,X0) ) ).
cnf(u2297,negated_conjecture,
~ c1_2(a177,a247) ).
cnf(u2325,negated_conjecture,
~ c1_2(a211,a247) ).
cnf(u2334,negated_conjecture,
~ c5_2(a211,a247) ).
cnf(u2379,negated_conjecture,
~ c1_2(a202,a247) ).
cnf(u2388,negated_conjecture,
~ c5_2(a202,a247) ).
cnf(u2426,negated_conjecture,
ssSkP3(a186) ).
cnf(u2435,negated_conjecture,
c3_2(a186,a223) ).
cnf(u2440,negated_conjecture,
c2_2(a186,a223) ).
cnf(u2460,negated_conjecture,
~ c4_2(a186,a190) ).
cnf(u2467,negated_conjecture,
~ c2_1(a186) ).
cnf(u2518,negated_conjecture,
~ c5_2(a188,a184) ).
cnf(u2524,negated_conjecture,
~ c2_2(a188,a184) ).
cnf(u2547,negated_conjecture,
~ c4_2(a188,a184) ).
cnf(u2551,negated_conjecture,
~ c2_1(a188) ).
cnf(u2570,negated_conjecture,
( c5_2(a188,X0)
| c1_2(a188,X0)
| c4_2(a188,X0) ) ).
cnf(u2616,negated_conjecture,
ndr1_1(a248) ).
cnf(u2620,negated_conjecture,
c2_1(a248) ).
cnf(u2644,negated_conjecture,
c2_2(a255,a216) ).
cnf(u2653,negated_conjecture,
c2_2(a189,a216) ).
cnf(u2666,negated_conjecture,
c3_2(a214,a217) ).
cnf(u2671,negated_conjecture,
c2_2(a179,a216) ).
cnf(u2680,negated_conjecture,
c2_2(a188,a216) ).
cnf(u2700,negated_conjecture,
~ ssSkP3(a260) ).
cnf(u2756,negated_conjecture,
~ c1_2(a186,a178) ).
cnf(u2776,negated_conjecture,
c4_2(a186,a224) ).
cnf(u2781,negated_conjecture,
~ c5_2(a186,a224) ).
cnf(u2816,negated_conjecture,
~ c5_1(a179) ).
cnf(u2819,negated_conjecture,
~ c3_2(a179,a222) ).
cnf(u2859,negated_conjecture,
c4_1(a179) ).
cnf(u2869,negated_conjecture,
c5_2(a179,a222) ).
cnf(u2873,negated_conjecture,
( ~ c4_2(a179,X0)
| c5_2(a179,X0)
| c1_2(a179,X0) ) ).
cnf(u2910,negated_conjecture,
~ c4_2(a186,a184) ).
cnf(u2933,negated_conjecture,
~ c4_2(a186,a221) ).
cnf(u2939,negated_conjecture,
c2_2(a186,a221) ).
cnf(u2960,negated_conjecture,
~ c1_2(a186,a221) ).
cnf(u2965,negated_conjecture,
c5_2(a186,a181) ).
cnf(u2970,negated_conjecture,
c1_2(a186,a181) ).
cnf(u3028,negated_conjecture,
c3_2(a186,a217) ).
cnf(u3092,negated_conjecture,
( ~ c4_2(a211,X0)
| c5_2(a211,X0)
| c1_2(a211,X0) ) ).
cnf(u3125,negated_conjecture,
c2_2(a186,a184) ).
cnf(u3144,negated_conjecture,
~ c1_1(a255) ).
cnf(u3158,negated_conjecture,
~ c1_2(a255,a216) ).
cnf(u3164,negated_conjecture,
~ c4_2(a255,a216) ).
cnf(u3192,negated_conjecture,
~ c1_1(a189) ).
cnf(u3206,negated_conjecture,
~ c1_2(a189,a216) ).
cnf(u3212,negated_conjecture,
~ c4_2(a189,a216) ).
cnf(u3254,negated_conjecture,
~ c1_2(a214,a217) ).
cnf(u3263,negated_conjecture,
~ c5_2(a214,a217) ).
cnf(u3289,negated_conjecture,
~ c4_2(a214,a217) ).
cnf(u3348,negated_conjecture,
~ c1_1(a179) ).
cnf(u3363,negated_conjecture,
~ c4_2(a179,a216) ).
cnf(u3372,negated_conjecture,
~ c1_2(a179,a216) ).
cnf(u3387,negated_conjecture,
~ c4_2(a188,a216) ).
cnf(u3415,negated_conjecture,
c2_2(a186,a181) ).
cnf(u3483,negated_conjecture,
c3_2(a188,a222) ).
cnf(u3505,negated_conjecture,
~ c5_2(a188,a222) ).
cnf(u3612,negated_conjecture,
( c5_2(a260,X0)
| c1_2(a260,X0) ) ).
cnf(u3681,negated_conjecture,
~ c1_2(a211,a206) ).
cnf(u3695,negated_conjecture,
c2_2(a211,a206) ).
cnf(u3702,negated_conjecture,
~ c4_2(a211,a206) ).
cnf(u3759,negated_conjecture,
c3_2(a240,a217) ).
cnf(u3786,negated_conjecture,
~ c1_2(a240,a217) ).
cnf(u3795,negated_conjecture,
~ c5_2(a240,a217) ).
cnf(u3821,negated_conjecture,
~ c4_2(a240,a217) ).
cnf(u3916,negated_conjecture,
~ c5_2(a186,a217) ).
cnf(u3991,negated_conjecture,
c2_2(a260,a206) ).
cnf(u4010,negated_conjecture,
~ c4_2(a260,a206) ).
cnf(u4016,negated_conjecture,
~ c1_2(a260,a206) ).
cnf(u3583,negated_conjecture,
c5_2(a260,a222) ).
cnf(u3436,negated_conjecture,
~ c1_2(a188,a216) ).
cnf(u1600,negated_conjecture,
ssSkP1(a249) ).
cnf(u1607,negated_conjecture,
ssSkP0(a249) ).
cnf(u1765,negated_conjecture,
( ~ c1_2(X0,X1)
| c1_2(X0,a190)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(clause80,negated_conjecture,
( ssSkP0(X0)
| c5_2(X0,a175) ) ).
cnf(clause73,negated_conjecture,
( ssSkP4(X0)
| c1_2(X0,a245) ) ).
cnf(u1803,negated_conjecture,
~ c5_1(a192) ).
cnf(u1854,negated_conjecture,
~ c5_1(a263) ).
cnf(u1973,negated_conjecture,
~ c4_2(a211,a247) ).
cnf(u1850,negated_conjecture,
ssSkP3(a263) ).
cnf(u3015,negated_conjecture,
ssSkP0(a185) ).
cnf(clause74,negated_conjecture,
( ssSkP4(X0)
| c4_2(X0,a245) ) ).
cnf(u1642,negated_conjecture,
c4_2(a188,a178) ).
cnf(clause76,negated_conjecture,
( ssSkP3(X0)
| c1_2(X0,a222) ) ).
cnf(u3017,negated_conjecture,
c3_1(a185) ).
cnf(clause39,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u1979,negated_conjecture,
~ c5_1(a202) ).
cnf(u3013,negated_conjecture,
ssSkP2(a185) ).
cnf(u2168,negated_conjecture,
~ c2_2(a211,a222) ).
cnf(u1955,negated_conjecture,
~ c4_2(a177,a247) ).
cnf(u1853,negated_conjecture,
ssSkP0(a263) ).
cnf(u1632,negated_conjecture,
c3_1(a249) ).
cnf(clause112,negated_conjecture,
( ~ c5_2(X0,a251)
| ssSkP5(X0) ) ).
cnf(u1579,negated_conjecture,
ssSkP4(a249) ).
cnf(u3016,negated_conjecture,
~ c5_1(a185) ).
cnf(u1593,negated_conjecture,
ssSkP2(a249) ).
cnf(u1849,negated_conjecture,
ssSkP4(a263) ).
cnf(u2241,negated_conjecture,
c2_2(a188,a178) ).
cnf(u1764,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_2(X0,a190)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0) ) ).
cnf(clause77,negated_conjecture,
( ssSkP2(X0)
| c2_2(X0,a216) ) ).
cnf(u1615,negated_conjecture,
~ c5_1(a226) ).
cnf(clause34,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u3012,negated_conjecture,
ssSkP3(a185) ).
cnf(u1847,negated_conjecture,
~ c5_1(a260) ).
cnf(u3751,negated_conjecture,
ndr1_1(a240) ).
cnf(u1811,negated_conjecture,
( ~ c5_1(X0)
| c5_2(X0,a198) ) ).
cnf(u1852,negated_conjecture,
ssSkP1(a263) ).
cnf(u2171,negated_conjecture,
c1_2(a211,a222) ).
cnf(clause116,negated_conjecture,
( ~ c4_2(X0,a175)
| ssSkP0(X0) ) ).
cnf(u1977,negated_conjecture,
~ c4_2(a202,a247) ).
cnf(clause33,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u3870,negated_conjecture,
~ c4_2(a186,a181) ).
cnf(u1957,negated_conjecture,
~ c5_1(a177) ).
cnf(u3585,negated_conjecture,
c3_2(a260,a206) ).
cnf(clause75,negated_conjecture,
( ssSkP4(X0)
| c5_2(X0,a245) ) ).
cnf(u2246,negated_conjecture,
~ c2_2(a188,a222) ).
cnf(clause78,negated_conjecture,
( ssSkP1(X0)
| c4_2(X0,a203) ) ).
cnf(u1645,negated_conjecture,
( ~ c4_1(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u2726,negated_conjecture,
~ c2_2(a260,a222) ).
cnf(u3066,negated_conjecture,
c3_2(a211,a206) ).
cnf(u1848,negated_conjecture,
ssSkP5(a263) ).
cnf(u1644,negated_conjecture,
c3_2(a188,a178) ).
cnf(u1578,negated_conjecture,
ssSkP4(a226) ).
cnf(u1975,negated_conjecture,
~ c5_1(a211) ).
cnf(u1640,negated_conjecture,
c5_2(a188,a178) ).
cnf(u2146,negated_conjecture,
c1_2(a179,a222) ).
cnf(clause114,negated_conjecture,
( ~ c3_2(X0,a216)
| ssSkP2(X0) ) ).
cnf(u1824,negated_conjecture,
~ c1_2(a188,a198) ).
cnf(clause113,negated_conjecture,
( ~ c2_2(X0,a222)
| ssSkP3(X0) ) ).
cnf(u1592,negated_conjecture,
ssSkP2(a226) ).
cnf(u1599,negated_conjecture,
ssSkP1(a226) ).
cnf(u1763,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_1(X0)
| ~ c5_2(X0,a190) ) ).
cnf(u1616,negated_conjecture,
~ c5_1(a249) ).
cnf(u3924,negated_conjecture,
c5_2(a188,a216) ).
cnf(u1572,negated_conjecture,
ssSkP5(a249) ).
cnf(u2729,negated_conjecture,
c1_2(a260,a222) ).
cnf(u3563,negated_conjecture,
~ c1_2(a186,a223) ).
cnf(u1810,negated_conjecture,
( ~ c1_2(X0,a198)
| ~ c5_1(X0) ) ).
cnf(u1606,negated_conjecture,
ssSkP0(a226) ).
cnf(u3010,negated_conjecture,
ssSkP5(a185) ).
cnf(u2635,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,a216)
| c2_1(X0)
| c3_2(X0,a217) ) ).
cnf(u3031,negated_conjecture,
~ c3_2(a186,a181) ).
cnf(u3417,negated_conjecture,
~ c1_2(a186,a217) ).
cnf(u3014,negated_conjecture,
ssSkP1(a185) ).
cnf(clause42,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause72,negated_conjecture,
( ssSkP5(X0)
| c1_2(X0,a251) ) ).
cnf(clause79,negated_conjecture,
( ssSkP0(X0)
| c3_2(X0,a175) ) ).
cnf(u2143,negated_conjecture,
~ c2_2(a179,a222) ).
cnf(u1700,negated_conjecture,
( c3_1(X0)
| c3_2(X0,a217)
| c2_2(X0,a216) ) ).
cnf(u1828,negated_conjecture,
c5_2(a188,a198) ).
cnf(clause38,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(clause37,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u3584,negated_conjecture,
c5_2(a260,a206) ).
cnf(u1807,negated_conjecture,
~ c5_1(a199) ).
cnf(u3441,negated_conjecture,
~ c4_2(a188,a222) ).
cnf(u3561,negated_conjecture,
~ c5_2(a186,a223) ).
cnf(u3011,negated_conjecture,
ssSkP4(a185) ).
cnf(u1637,negated_conjecture,
ndr1_1(a255) ).
cnf(u1851,negated_conjecture,
ssSkP2(a263) ).
cnf(u2249,negated_conjecture,
c1_2(a188,a222) ).
cnf(u1586,negated_conjecture,
ssSkP3(a249) ).
cnf(u1585,negated_conjecture,
ssSkP3(a226) ).
cnf(u1609,negated_conjecture,
c4_1(a188) ).
cnf(u1565,negated_conjecture,
( c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u3063,negated_conjecture,
c5_2(a211,a222) ).
cnf(clause115,negated_conjecture,
( ~ c1_2(X0,a203)
| ssSkP1(X0) ) ).
cnf(u3065,negated_conjecture,
c5_2(a211,a206) ).
cnf(u1631,negated_conjecture,
c3_1(a226) ).
cnf(u1571,negated_conjecture,
ssSkP5(a226) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN514-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n018.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 16:23:10 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.97/1.88 % (3518625)Input is clausal, will run a generic CNF schedule.
% 8.97/1.88 % (3518635)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3992890816:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.97/1.88 % (3518635)Refutation not found, incomplete strategy
% 8.97/1.88 % (3518635)------------------------------
% 8.97/1.88 % (3518635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.97/1.88 % (3518635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.88 % (3518635)CaDiCaL version: 2.1.3
% 8.97/1.88 % (3518635)Termination reason: Refutation not found, incomplete strategy
% 8.97/1.88 % (3518635)Time elapsed: 0.015 s
% 8.97/1.88 % (3518635)Peak memory usage: 89 MB
% 8.97/1.88 % (3518635)Instructions burned: 42 (million)
% 8.97/1.88 % (3518632)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=400259848:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.97/1.88 % (3518630)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=1097613984:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.97/1.88 % (3518636)dis-21_1_sil=8000:lcm=predicate:random_seed=848251680: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)
% 8.97/1.88 % (3518633)lrs+10_1_sil=8000:sp=occurrence:random_seed=553949746:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.97/1.88 % (3518634)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1895641984:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.97/1.88 % (3518631)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3933828837:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.97/1.88 % (3518633)Instruction limit reached!
% 8.97/1.88 % (3518633)------------------------------
% 8.97/1.88 % (3518633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.97/1.88 % (3518633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.88 % (3518633)CaDiCaL version: 2.1.3
% 8.97/1.88 % (3518633)Termination reason: Instruction limit
% 8.97/1.88 % (3518633)Termination phase: Saturation
% 8.97/1.88 % (3518633)Time elapsed: 0.061 s
% 8.97/1.88 % (3518633)Peak memory usage: 89 MB
% 8.97/1.88 % (3518633)Instructions burned: 108 (million)
% 8.97/1.88 % (3518634)Instruction limit reached!
% 8.97/1.88 % (3518634)------------------------------
% 8.97/1.88 % (3518634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.97/1.88 % (3518634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.88 % (3518634)CaDiCaL version: 2.1.3
% 8.97/1.88 % (3518634)Termination reason: Instruction limit
% 8.97/1.88 % (3518634)Termination phase: Saturation
% 8.97/1.88 % (3518634)Time elapsed: 0.066 s
% 8.97/1.88 % (3518634)Peak memory usage: 89 MB
% 8.97/1.88 % (3518634)Instructions burned: 114 (million)
% 8.97/1.88 % (3518636)Instruction limit reached!
% 8.97/1.88 % (3518636)------------------------------
% 8.97/1.88 % (3518636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.97/1.88 % (3518636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.97/1.88 % (3518636)CaDiCaL version: 2.1.3
% 8.97/1.88 % (3518636)Termination reason: Instruction limit
% 8.97/1.88 % (3518636)Termination phase: Saturation
% 8.97/1.88 % (3518636)Time elapsed: 0.068 s
% 8.97/1.88 % (3518636)Peak memory usage: 90 MB
% 8.97/1.88 % (3518636)Instructions burned: 117 (million)
% 8.97/1.88 % (3518635)------------------------------
% 8.97/1.88 % (3518635)------------------------------
% 8.97/1.88 % (3518645)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=668347947:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 8.97/1.88 % (3518644)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=2577077153:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.97/1.88 % (3518646)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1119862408:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.97/1.88 % (3518645)Refutation not found, incomplete strategy
% 8.97/1.88 % (3518645)------------------------------
% 9.54/1.95 % (3518645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518645)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518645)Termination reason: Refutation not found, incomplete strategy
% 9.54/1.95 % (3518645)Time elapsed: 0.024 s
% 9.54/1.95 % (3518645)Peak memory usage: 89 MB
% 9.54/1.95 % (3518645)Instructions burned: 40 (million)
% 9.54/1.95 % (3518647)lrs+10_64_to=lpo:sil=8000:random_seed=1155185114:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 9.54/1.95 % (3518644)Instruction limit reached!
% 9.54/1.95 % (3518644)------------------------------
% 9.54/1.95 % (3518644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518644)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518644)Termination reason: Instruction limit
% 9.54/1.95 % (3518644)Termination phase: Saturation
% 9.54/1.95 % (3518644)Time elapsed: 0.080 s
% 9.54/1.95 % (3518644)Peak memory usage: 89 MB
% 9.54/1.95 % (3518644)Instructions burned: 143 (million)
% 9.54/1.95 % (3518647)Instruction limit reached!
% 9.54/1.95 % (3518647)------------------------------
% 9.54/1.95 % (3518647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518647)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518647)Termination reason: Instruction limit
% 9.54/1.95 % (3518647)Termination phase: Saturation
% 9.54/1.95 % (3518647)Time elapsed: 0.040 s
% 9.54/1.95 % (3518647)Peak memory usage: 90 MB
% 9.54/1.95 % (3518647)Instructions burned: 126 (million)
% 9.54/1.95 % (3518646)Instruction limit reached!
% 9.54/1.95 % (3518646)------------------------------
% 9.54/1.95 % (3518646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518646)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518646)Termination reason: Instruction limit
% 9.54/1.95 % (3518646)Termination phase: Saturation
% 9.54/1.95 % (3518646)Time elapsed: 0.123 s
% 9.54/1.95 % (3518646)Peak memory usage: 91 MB
% 9.54/1.95 % (3518646)Instructions burned: 219 (million)
% 9.54/1.95 % (3518653)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2678827433:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 9.54/1.95 % (3518652)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=912993064:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 9.54/1.95 % (3518653)Instruction limit reached!
% 9.54/1.95 % (3518653)------------------------------
% 9.54/1.95 % (3518653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518653)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518653)Termination reason: Instruction limit
% 9.54/1.95 % (3518653)Termination phase: Saturation
% 9.54/1.95 % (3518653)Time elapsed: 0.050 s
% 9.54/1.95 % (3518653)Peak memory usage: 91 MB
% 9.54/1.95 % (3518653)Instructions burned: 158 (million)
% 9.54/1.95 % (3518645)------------------------------
% 9.54/1.95 % (3518645)------------------------------
% 9.54/1.95 % (3518654)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3610814298:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 9.54/1.95 % (3518652)Refutation not found, incomplete strategy
% 9.54/1.95 % (3518652)------------------------------
% 9.54/1.95 % (3518652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518652)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518652)Termination reason: Refutation not found, incomplete strategy
% 9.54/1.95 % (3518652)Time elapsed: 0.076 s
% 9.54/1.95 % (3518652)Peak memory usage: 90 MB
% 9.54/1.95 % (3518652)Instructions burned: 129 (million)
% 9.54/1.95 % (3518657)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2962177515:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 9.54/1.95 % (3518657)Refutation not found, incomplete strategy
% 9.54/1.95 % (3518657)------------------------------
% 9.54/1.95 % (3518657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518657)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518657)Termination reason: Refutation not found, incomplete strategy
% 9.54/1.95 % (3518657)Time elapsed: 0.009 s
% 9.54/1.95 % (3518657)Peak memory usage: 89 MB
% 9.54/1.95 % (3518657)Instructions burned: 27 (million)
% 9.54/1.95 % (3518631)Refutation not found, incomplete strategy
% 9.54/1.95 % (3518631)------------------------------
% 9.54/1.95 % (3518631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518631)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518631)Termination reason: Refutation not found, incomplete strategy
% 9.54/1.95 % (3518631)Time elapsed: 0.635 s
% 9.54/1.95 % (3518631)Peak memory usage: 130 MB
% 9.54/1.95 % (3518631)Instructions burned: 951 (million)
% 9.54/1.95 % (3518658)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1838419769:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 9.54/1.95 % (3518658)Instruction limit reached!
% 9.54/1.95 % (3518658)------------------------------
% 9.54/1.95 % (3518658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518658)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518658)Termination reason: Instruction limit
% 9.54/1.95 % (3518658)Termination phase: Saturation
% 9.54/1.95 % (3518658)Time elapsed: 0.066 s
% 9.54/1.95 % (3518658)Peak memory usage: 90 MB
% 9.54/1.95 % (3518658)Instructions burned: 108 (million)
% 9.54/1.95 % (3518657)------------------------------
% 9.54/1.95 % (3518657)------------------------------
% 9.54/1.95 % (3518652)------------------------------
% 9.54/1.95 % (3518652)------------------------------
% 9.54/1.95 % (3518662)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=438614311:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 9.54/1.95 % (3518663)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1861952605:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 9.54/1.95 % (3518631)------------------------------
% 9.54/1.95 % (3518631)------------------------------
% 9.54/1.95 % (3518662)Refutation not found, incomplete strategy
% 9.54/1.95 % (3518662)------------------------------
% 9.54/1.95 % (3518662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518662)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518662)Termination reason: Refutation not found, incomplete strategy
% 9.54/1.95 % (3518662)Time elapsed: 0.047 s
% 9.54/1.95 % (3518662)Peak memory usage: 88 MB
% 9.54/1.95 % (3518662)Instructions burned: 90 (million)
% 9.54/1.95 % (3518664)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2573083601:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 9.54/1.95 % (3518664)Instruction limit reached!
% 9.54/1.95 % (3518664)------------------------------
% 9.54/1.95 % (3518664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518664)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518664)Termination reason: Instruction limit
% 9.54/1.95 % (3518664)Termination phase: Saturation
% 9.54/1.95 % (3518664)Time elapsed: 0.077 s
% 9.54/1.95 % (3518664)Peak memory usage: 90 MB
% 9.54/1.95 % (3518664)Instructions burned: 135 (million)
% 9.54/1.95 % (3518667)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3853581862:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 9.54/1.95 % (3518667)First to succeed.
% 9.54/1.95 % (3518667)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3518625"
% 9.54/1.95 % (3518662)------------------------------
% 9.54/1.95 % (3518662)------------------------------
% 9.54/1.95 % (3518669)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=580482427:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 9.54/1.95 % (3518671)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1388182884:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 9.54/1.95 % (3518669)Instruction limit reached!
% 9.54/1.95 % (3518669)------------------------------
% 9.54/1.95 % (3518669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.54/1.95 % (3518669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.54/1.95 % (3518669)CaDiCaL version: 2.1.3
% 9.54/1.95 % (3518669)Termination reason: Instruction limit
% 9.54/1.95 % (3518669)Termination phase: Saturation
% 9.54/1.95 % (3518669)Time elapsed: 0.113 s
% 9.54/1.95 % (3518669)Peak memory usage: 91 MB
% 9.54/1.95 % (3518669)Instructions burned: 192 (million)
% 9.54/1.95 % SZS status Satisfiable for theBenchmark
% 9.54/1.95 % SZS output start Saturation.
% See solution above
% 11.31/2.16 % SZS output start Definitions and Model Updates.
% 11.31/2.16 for all inputs,
% 11.31/2.16 define c4_0 := $false
% 11.31/2.16 % SZS output end Definitions and Model Updates.
% 11.31/2.16 % (3518667)------------------------------
% 11.31/2.16 % (3518667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.16 % (3518667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.16 % (3518667)CaDiCaL version: 2.1.3
% 11.31/2.16 % (3518667)Termination reason: Satisfiable
% 11.31/2.16 % (3518667)Time elapsed: 0.059 s
% 11.31/2.16 % (3518667)Peak memory usage: 90 MB
% 11.31/2.16 % (3518667)Instructions burned: 92 (million)
% 11.31/2.16 % (3518667)------------------------------
% 11.31/2.16 % (3518667)------------------------------
% 11.31/2.16 % (3518625)Success in time 1.54 s
% 11.31/2.16 % Vampire exiting
%------------------------------------------------------------------------------