%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p 300 THM
% 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:00:46 PM UTC 2026
% Result : CounterSatisfiable 8.76s 1.96s
% Output : Saturation 8.76s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1493,negated_conjecture,
~ sP1 ).
cnf(u488,negated_conjecture,
( ~ c5_2(a262,X116)
| c4_2(a262,X116)
| ~ c3_2(a262,X116) ) ).
cnf(u1467,negated_conjecture,
~ sP0 ).
cnf(u495,negated_conjecture,
c5_1(a262) ).
cnf(u499,negated_conjecture,
ndr1_0 ).
cnf(u503,negated_conjecture,
~ ndr1_1(a259) ).
cnf(u1515,negated_conjecture,
~ sP2 ).
cnf(u517,negated_conjecture,
~ c1_1(a259) ).
cnf(u531,negated_conjecture,
~ c3_1(a255) ).
cnf(u534,negated_conjecture,
c5_2(a253,a254) ).
cnf(u1536,negated_conjecture,
~ sP3 ).
cnf(u541,negated_conjecture,
c3_2(a253,a254) ).
cnf(u545,negated_conjecture,
c2_2(a253,a254) ).
cnf(u2918,negated_conjecture,
~ ndr1_1(a253) ).
cnf(u553,negated_conjecture,
~ c4_1(a253) ).
cnf(u557,negated_conjecture,
c1_1(a253) ).
cnf(u561,negated_conjecture,
( ~ c1_1(X112)
| ~ ndr1_1(X112)
| ~ c2_2(X112,X113)
| c5_2(X112,X113)
| ~ c2_1(X112) ) ).
cnf(u576,negated_conjecture,
~ ndr1_1(a249) ).
cnf(u597,negated_conjecture,
~ c5_1(a248) ).
cnf(u1565,negated_conjecture,
~ sP4 ).
cnf(u607,negated_conjecture,
c4_1(a248) ).
cnf(u621,negated_conjecture,
( ~ c5_1(X102)
| ~ ndr1_1(X102)
| ~ c5_2(X102,X103)
| c4_2(X102,X103)
| c2_2(X102,X103)
| c4_1(X102) ) ).
cnf(u637,negated_conjecture,
( c2_1(X92)
| ~ ndr1_1(X92)
| ~ c4_2(X92,X93)
| ~ c2_2(X92,X93)
| c3_2(X92,X93)
| c3_1(X92) ) ).
cnf(u661,negated_conjecture,
( ~ ndr1_1(X89)
| c1_1(X89)
| c4_2(X89,X90)
| c1_2(X89,X90)
| ~ c2_1(X89) ) ).
cnf(u695,negated_conjecture,
~ c3_0 ).
cnf(u748,negated_conjecture,
~ c5_0 ).
cnf(u758,negated_conjecture,
~ c2_0 ).
cnf(u1603,negated_conjecture,
~ sP5 ).
cnf(u777,negated_conjecture,
~ c1_0 ).
cnf(u799,negated_conjecture,
( ~ c1_1(X64)
| ~ ndr1_1(X64)
| ~ c4_2(X64,X65)
| c1_2(X64,X65)
| c4_1(X64) ) ).
cnf(u840,negated_conjecture,
~ c5_2(a227,a228) ).
cnf(u844,negated_conjecture,
~ c2_2(a227,a228) ).
cnf(u848,negated_conjecture,
c4_2(a227,a228) ).
cnf(u854,negated_conjecture,
~ ndr1_1(a227) ).
cnf(u857,negated_conjecture,
( ~ c4_2(a227,X63)
| c2_2(a227,X63)
| ~ c3_2(a227,X63) ) ).
cnf(u861,negated_conjecture,
c3_1(a227) ).
cnf(u869,negated_conjecture,
~ ndr1_1(a226) ).
cnf(u898,negated_conjecture,
( ~ c5_2(X57,a224)
| c2_2(X57,X58)
| ~ c4_2(X57,X59)
| c5_2(X57,X59)
| c3_2(X57,X59)
| ~ ndr1_1(X57)
| ~ c5_2(X57,X58)
| ~ c3_2(X57,X58) ) ).
cnf(u902,negated_conjecture,
( ~ ndr1_1(X57)
| c4_2(X57,a224)
| ~ c4_2(X57,X59)
| c5_2(X57,X59)
| c3_2(X57,X59)
| c2_2(X57,X58)
| ~ c5_2(X57,X58)
| ~ c3_2(X57,X58) ) ).
cnf(u906,negated_conjecture,
( ~ ndr1_1(X57)
| c1_2(X57,a224)
| ~ c4_2(X57,X59)
| c5_2(X57,X59)
| c3_2(X57,X59)
| c2_2(X57,X58)
| ~ c5_2(X57,X58)
| ~ c3_2(X57,X58) ) ).
cnf(u910,negated_conjecture,
( ~ c5_2(X55,a223)
| c1_2(X55,X56)
| ~ c2_2(X55,a222)
| ~ ndr1_1(X55)
| ~ c5_2(X55,X56) ) ).
cnf(u914,negated_conjecture,
( ~ ndr1_1(X55)
| c3_2(X55,a223)
| ~ c2_2(X55,a222)
| c1_2(X55,X56)
| ~ c5_2(X55,X56) ) ).
cnf(u918,negated_conjecture,
( ~ ndr1_1(X55)
| c2_2(X55,a223)
| ~ c2_2(X55,a222)
| c1_2(X55,X56)
| ~ c5_2(X55,X56) ) ).
cnf(u922,negated_conjecture,
( ~ c5_2(X55,a223)
| c1_2(X55,X56)
| c1_2(X55,a222)
| ~ ndr1_1(X55)
| ~ c5_2(X55,X56) ) ).
cnf(u926,negated_conjecture,
( ~ ndr1_1(X55)
| c3_2(X55,a223)
| c1_2(X55,a222)
| c1_2(X55,X56)
| ~ c5_2(X55,X56) ) ).
cnf(u930,negated_conjecture,
( ~ ndr1_1(X55)
| c2_2(X55,a223)
| c1_2(X55,a222)
| c1_2(X55,X56)
| ~ c5_2(X55,X56) ) ).
cnf(u934,negated_conjecture,
( ~ ndr1_1(X52)
| c5_2(X52,a221)
| ~ c5_2(X52,X54)
| ~ c1_2(X52,X54)
| c2_2(X52,X54)
| c1_2(X52,X53)
| ~ c4_2(X52,X53)
| c5_2(X52,X53) ) ).
cnf(u938,negated_conjecture,
( ~ ndr1_1(X52)
| c4_2(X52,a221)
| ~ c5_2(X52,X54)
| ~ c1_2(X52,X54)
| c2_2(X52,X54)
| c1_2(X52,X53)
| ~ c4_2(X52,X53)
| c5_2(X52,X53) ) ).
cnf(u942,negated_conjecture,
( ~ ndr1_1(X52)
| c2_2(X52,a221)
| ~ c5_2(X52,X54)
| ~ c1_2(X52,X54)
| c2_2(X52,X54)
| c1_2(X52,X53)
| ~ c4_2(X52,X53)
| c5_2(X52,X53) ) ).
cnf(u1629,negated_conjecture,
~ sP6 ).
cnf(u949,negated_conjecture,
( ~ c1_1(X50)
| ~ c5_2(X50,a218)
| ~ ndr1_1(X50)
| c5_2(X50,X51)
| c4_2(X50,X51)
| c1_2(X50,X51) ) ).
cnf(u953,negated_conjecture,
( ~ c1_1(X50)
| c2_2(X50,a218)
| ~ ndr1_1(X50)
| c5_2(X50,X51)
| c4_2(X50,X51)
| c1_2(X50,X51) ) ).
cnf(u957,negated_conjecture,
( ~ c1_1(X50)
| c1_2(X50,a218)
| ~ ndr1_1(X50)
| c5_2(X50,X51)
| c4_2(X50,X51)
| c1_2(X50,X51) ) ).
cnf(u961,negated_conjecture,
( ~ c2_2(X49,a217)
| c3_1(X49)
| ~ c3_2(X49,a216) ) ).
cnf(u965,negated_conjecture,
( c3_2(X49,a217)
| c3_1(X49)
| ~ c3_2(X49,a216) ) ).
cnf(u969,negated_conjecture,
( ~ c2_2(X49,a217)
| c3_1(X49)
| c2_2(X49,a216) ) ).
cnf(u973,negated_conjecture,
( c2_2(X49,a216)
| c3_2(X49,a217)
| c3_1(X49) ) ).
cnf(u977,negated_conjecture,
( c3_1(X49)
| ndr1_1(X49) ) ).
cnf(u1646,negated_conjecture,
~ sP7 ).
cnf(u984,negated_conjecture,
( ~ c2_2(X48,a213)
| c2_1(X48) ) ).
cnf(u988,negated_conjecture,
( c4_2(X48,a213)
| c2_1(X48) ) ).
cnf(u992,negated_conjecture,
( c2_1(X48)
| ndr1_1(X48) ) ).
cnf(u996,negated_conjecture,
~ c1_2(a211,a212) ).
cnf(u1000,negated_conjecture,
c5_2(a211,a212) ).
cnf(u1004,negated_conjecture,
c2_2(a211,a212) ).
cnf(u1010,negated_conjecture,
~ ndr1_1(a211) ).
cnf(u1013,negated_conjecture,
( c2_2(a211,X47)
| ~ c1_2(a211,X47)
| c5_2(a211,X47) ) ).
cnf(u1017,negated_conjecture,
c3_1(a211) ).
cnf(u1023,negated_conjecture,
~ c3_2(a209,a210) ).
cnf(u1027,negated_conjecture,
c2_2(a209,a210) ).
cnf(u1035,negated_conjecture,
~ c4_1(a209) ).
cnf(u1039,negated_conjecture,
c3_1(a209) ).
cnf(u1672,negated_conjecture,
~ sP8 ).
cnf(u1047,negated_conjecture,
( ~ c1_2(X45,X46)
| c5_2(X45,a206)
| ~ ndr1_1(X45)
| c4_1(X45)
| c2_2(X45,X46) ) ).
cnf(u1051,negated_conjecture,
( ~ ndr1_1(X45)
| c3_2(X45,a206)
| c4_1(X45)
| ~ c1_2(X45,X46)
| c2_2(X45,X46) ) ).
cnf(u1058,negated_conjecture,
( c2_1(X41)
| ~ ndr1_1(X41)
| ~ c4_2(X41,X42)
| ~ c2_2(X41,X42)
| c3_2(X41,X42)
| c5_1(X41) ) ).
cnf(u1087,negated_conjecture,
~ ndr1_1(a202) ).
cnf(u1094,negated_conjecture,
c3_1(a202) ).
cnf(u1103,negated_conjecture,
c2_1(a200) ).
cnf(u1113,negated_conjecture,
~ ndr1_1(a199) ).
cnf(u1123,negated_conjecture,
~ c4_1(a199) ).
cnf(u1127,negated_conjecture,
~ c1_1(a199) ).
cnf(u1146,negated_conjecture,
( c2_1(X34)
| ~ ndr1_1(X34)
| ~ c2_2(X34,X35)
| ~ c1_2(X34,X35)
| c4_2(X34,X35)
| c4_1(X34) ) ).
cnf(u1165,negated_conjecture,
( c5_2(X30,a195)
| c1_1(X30)
| c2_1(X30) ) ).
cnf(u1177,negated_conjecture,
( c3_2(X30,a195)
| c1_1(X30)
| c2_1(X30) ) ).
cnf(u1183,negated_conjecture,
( c1_2(X30,a195)
| c1_1(X30)
| c2_1(X30) ) ).
cnf(u1189,negated_conjecture,
( c1_1(X30)
| ndr1_1(X30)
| c2_1(X30) ) ).
cnf(u1214,negated_conjecture,
( c3_2(a193,X28)
| ~ c5_2(a193,X28)
| ~ c4_2(a193,X28) ) ).
cnf(u1218,negated_conjecture,
( c3_2(a193,X27)
| c4_2(a193,X27)
| c1_2(a193,X27) ) ).
cnf(u1222,negated_conjecture,
c5_1(a193) ).
cnf(u1227,negated_conjecture,
~ ndr1_1(a192) ).
cnf(u1234,negated_conjecture,
~ c4_1(a192) ).
cnf(u1238,negated_conjecture,
c2_1(a192) ).
cnf(u1243,negated_conjecture,
~ c1_1(a191) ).
cnf(u1247,negated_conjecture,
c2_1(a191) ).
cnf(u1252,negated_conjecture,
( ~ c5_1(X24)
| ~ c5_2(X24,a190)
| ~ ndr1_1(X24)
| ~ c1_2(X24,X25)
| c4_2(X24,X25)
| c3_2(X24,X25) ) ).
cnf(u1256,negated_conjecture,
( ~ c5_1(X24)
| c2_2(X24,a190)
| ~ ndr1_1(X24)
| ~ c1_2(X24,X25)
| c4_2(X24,X25)
| c3_2(X24,X25) ) ).
cnf(u1260,negated_conjecture,
( ~ c5_1(X24)
| c1_2(X24,a190)
| ~ ndr1_1(X24)
| ~ c1_2(X24,X25)
| c4_2(X24,X25)
| c3_2(X24,X25) ) ).
cnf(u1267,negated_conjecture,
( ~ c4_2(a189,X23)
| ~ c5_2(a189,X23)
| c1_2(a189,X23) ) ).
cnf(u1271,negated_conjecture,
~ c3_1(a189) ).
cnf(u1279,negated_conjecture,
( ~ c4_2(a188,X22)
| c2_2(a188,X22) ) ).
cnf(u1284,negated_conjecture,
( c2_2(a188,X21)
| ~ c4_2(a188,X21)
| ~ c3_2(a188,X21) ) ).
cnf(u1288,negated_conjecture,
c5_1(a188) ).
cnf(u1697,negated_conjecture,
~ sP9 ).
cnf(u1296,negated_conjecture,
~ ndr1_1(a185) ).
cnf(u1303,negated_conjecture,
c2_1(a185) ).
cnf(u1308,negated_conjecture,
( ~ c4_2(X18,a184)
| ~ c5_1(X18)
| ~ ndr1_1(X18)
| c5_2(X18,X19)
| c4_2(X18,X19)
| c3_2(X18,X19) ) ).
cnf(u1312,negated_conjecture,
( ~ c5_1(X18)
| c3_2(X18,a184)
| ~ ndr1_1(X18)
| c5_2(X18,X19)
| c4_2(X18,X19)
| c3_2(X18,X19) ) ).
cnf(u1316,negated_conjecture,
( ~ c5_1(X18)
| c1_2(X18,a184)
| ~ ndr1_1(X18)
| c5_2(X18,X19)
| c4_2(X18,X19)
| c3_2(X18,X19) ) ).
cnf(u1320,negated_conjecture,
( ~ c4_1(X17)
| c2_1(X17)
| ~ c3_1(X17) ) ).
cnf(u1337,negated_conjecture,
~ ndr1_1(a182) ).
cnf(u3655,negated_conjecture,
c2_1(a182) ).
cnf(u1349,negated_conjecture,
( ~ ndr1_1(X12)
| ~ c3_2(X12,a181)
| c5_1(X12)
| ~ c4_2(X12,X13)
| c1_2(X12,X13) ) ).
cnf(u1353,negated_conjecture,
( ~ ndr1_1(X12)
| c5_2(X12,a181)
| c5_1(X12)
| ~ c4_2(X12,X13)
| c1_2(X12,X13) ) ).
cnf(u1357,negated_conjecture,
( ~ ndr1_1(X12)
| c1_2(X12,a181)
| c5_1(X12)
| ~ c4_2(X12,X13)
| c1_2(X12,X13) ) ).
cnf(u1361,negated_conjecture,
( ~ c1_1(X10)
| ~ ndr1_1(X10)
| ~ c4_2(X10,X11)
| c5_2(X10,X11)
| c3_2(X10,X11)
| c5_1(X10) ) ).
cnf(u1365,negated_conjecture,
~ c3_2(a179,a180) ).
cnf(u1370,negated_conjecture,
~ c1_2(a179,a180) ).
cnf(u1374,negated_conjecture,
c5_2(a179,a180) ).
cnf(u1378,negated_conjecture,
ndr1_1(a179) ).
cnf(u1382,negated_conjecture,
~ c3_1(a179) ).
cnf(u1387,negated_conjecture,
( c5_2(X9,a178)
| ~ c5_1(X9) ) ).
cnf(u1391,negated_conjecture,
( ~ c5_1(X9)
| c4_2(X9,a178) ) ).
cnf(u1395,negated_conjecture,
( ~ c5_1(X9)
| c3_2(X9,a178) ) ).
cnf(u1399,negated_conjecture,
( ~ c5_1(X9)
| ndr1_1(X9) ) ).
cnf(u1407,negated_conjecture,
~ ndr1_1(a177) ).
cnf(u1418,negated_conjecture,
c3_1(a177) ).
cnf(u1465,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c5_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ c1_2(X0,X2)
| ~ c2_1(X0)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u1732,negated_conjecture,
~ c1_2(a211,a213) ).
cnf(u1735,negated_conjecture,
c2_1(a211) ).
cnf(u1811,negated_conjecture,
c5_1(a179) ).
cnf(u1818,negated_conjecture,
( c2_2(a179,X1)
| ~ c3_2(a179,X1)
| ~ c5_2(a179,X1) ) ).
cnf(u1839,negated_conjecture,
( ~ c1_2(a179,X1)
| c4_2(a179,X1)
| ~ c3_2(a179,X1) ) ).
cnf(u1849,negated_conjecture,
( ~ c1_2(a179,X0)
| ~ c5_2(a179,X0) ) ).
cnf(u1905,negated_conjecture,
c2_1(a179) ).
cnf(u1856,negated_conjecture,
( c4_2(a179,X0)
| c1_2(a179,X0) ) ).
cnf(u1860,negated_conjecture,
( ~ c5_2(a179,X0)
| ~ c1_2(a179,X0)
| ~ c2_2(a179,X0) ) ).
cnf(u2900,negated_conjecture,
c4_1(a179) ).
cnf(u1878,negated_conjecture,
c4_1(a193) ).
cnf(u1885,negated_conjecture,
( c3_2(a193,X0)
| c5_2(a193,X0)
| c4_2(a193,X0) ) ).
cnf(u1898,negated_conjecture,
( c2_2(a179,X0)
| ~ c1_2(a179,X0) ) ).
cnf(u3217,negated_conjecture,
~ c4_1(a262) ).
cnf(u1930,negated_conjecture,
( ~ c5_2(a262,X0)
| c2_2(a262,X0)
| c4_2(a262,X0) ) ).
cnf(u1934,negated_conjecture,
( c3_2(a262,X0)
| c5_2(a262,X0)
| c4_2(a262,X0) ) ).
cnf(u1949,negated_conjecture,
c2_1(a262) ).
cnf(u1975,negated_conjecture,
( c3_2(a188,X0)
| c5_2(a188,X0)
| c4_2(a188,X0) ) ).
cnf(u1988,negated_conjecture,
c4_1(a188) ).
cnf(u2002,negated_conjecture,
~ c1_2(a179,a217) ).
cnf(u2020,negated_conjecture,
c3_2(a179,a223) ).
cnf(u2044,negated_conjecture,
( c3_2(a179,X0)
| c5_2(a179,X0)
| c4_2(a179,X0) ) ).
cnf(u2060,negated_conjecture,
~ c5_2(a179,a217) ).
cnf(u2106,negated_conjecture,
c1_2(a211,a222) ).
cnf(u2113,negated_conjecture,
( ~ c3_2(a211,X1)
| c2_2(a211,X1)
| ~ c5_2(a211,X1) ) ).
cnf(u2151,negated_conjecture,
~ c4_1(a211) ).
cnf(u2158,negated_conjecture,
( ~ c1_2(a211,X0)
| c2_2(a211,X0) ) ).
cnf(u2171,negated_conjecture,
c2_2(a211,a195) ).
cnf(u2302,negated_conjecture,
c2_2(a179,a223) ).
cnf(u2326,negated_conjecture,
~ c3_2(a227,a213) ).
cnf(u2350,negated_conjecture,
~ c2_1(a255) ).
cnf(u2357,negated_conjecture,
( ~ c4_2(a255,X0)
| c1_2(a255,X0) ) ).
cnf(u2696,negated_conjecture,
~ c5_1(a255) ).
cnf(u2375,negated_conjecture,
( c1_2(a255,X1)
| c5_2(a255,X1)
| ~ c4_2(a255,X1) ) ).
cnf(u2389,negated_conjecture,
( ~ c5_2(a255,X0)
| c1_2(a255,X0) ) ).
cnf(u2406,negated_conjecture,
( ~ c4_2(a255,X0)
| c3_2(a255,X0)
| c5_2(a255,X0) ) ).
cnf(u2420,negated_conjecture,
( ~ c4_2(a255,X0)
| ~ c1_2(a255,X0)
| ~ c3_2(a255,X0) ) ).
cnf(u2424,negated_conjecture,
( ~ c1_2(a255,X0)
| c2_2(a255,X0)
| c5_2(a255,X0) ) ).
cnf(u2428,negated_conjecture,
( ~ c2_2(a255,X1)
| c4_2(a255,X1)
| ~ c1_2(a255,X1) ) ).
cnf(u2445,negated_conjecture,
~ c4_1(a255) ).
cnf(u2465,negated_conjecture,
( c3_2(a211,X0)
| c5_2(a211,X0)
| c4_2(a211,X0) ) ).
cnf(u2658,negated_conjecture,
c3_2(a255,a206) ).
cnf(u2667,negated_conjecture,
~ c3_1(a193) ).
cnf(u3059,negated_conjecture,
~ c2_1(a193) ).
cnf(u2676,negated_conjecture,
~ c3_1(a248) ).
cnf(u3304,negated_conjecture,
~ c2_1(a248) ).
cnf(u2721,negated_conjecture,
( ~ c4_2(a188,X1)
| c5_2(a188,X1)
| c1_2(a188,X1) ) ).
cnf(u2742,negated_conjecture,
c1_2(a188,a222) ).
cnf(u2757,negated_conjecture,
( ~ c4_2(a188,X1)
| c5_2(a188,X1)
| ~ c3_2(a188,X1) ) ).
cnf(u2764,negated_conjecture,
( ~ c3_2(a188,X1)
| c2_2(a188,X1)
| ~ c5_2(a188,X1) ) ).
cnf(u2778,negated_conjecture,
( c4_2(a188,X0)
| c1_2(a188,X0) ) ).
cnf(u3819,negated_conjecture,
~ c3_2(a188,a222) ).
cnf(u2796,negated_conjecture,
c4_2(a188,a222) ).
cnf(u2811,negated_conjecture,
c3_1(a188) ).
cnf(u2833,negated_conjecture,
c1_2(a188,X0) ).
cnf(u2853,negated_conjecture,
c5_2(a255,a206) ).
cnf(u2869,negated_conjecture,
~ c1_2(a255,a216) ).
cnf(u2892,negated_conjecture,
c3_2(a211,a222) ).
cnf(u2957,negated_conjecture,
c2_2(a262,a190) ).
cnf(u2964,negated_conjecture,
( c3_2(a193,X0)
| c4_2(a193,X0) ) ).
cnf(u2974,negated_conjecture,
c2_2(a188,a190) ).
cnf(u2981,negated_conjecture,
c2_2(a179,a190) ).
cnf(u2990,negated_conjecture,
c5_2(a179,a181) ).
cnf(u2994,negated_conjecture,
~ c3_2(a179,a181) ).
cnf(u3072,negated_conjecture,
c2_2(a193,a221) ).
cnf(u3076,negated_conjecture,
c4_2(a193,a221) ).
cnf(u3080,negated_conjecture,
c5_2(a193,a221) ).
cnf(u3090,negated_conjecture,
c2_2(a193,a223) ).
cnf(u3094,negated_conjecture,
c3_2(a193,a223) ).
cnf(u3107,negated_conjecture,
c1_1(a193) ).
cnf(u3113,negated_conjecture,
( ~ c5_2(a193,X1)
| ~ c3_2(a193,X1)
| c2_2(a193,X1) ) ).
cnf(u3138,negated_conjecture,
~ c2_2(a193,a195) ).
cnf(u3170,negated_conjecture,
( ~ c1_2(a262,X0)
| c2_2(a262,X0) ) ).
cnf(u3180,negated_conjecture,
( ~ c5_2(a262,X0)
| c2_2(a262,X0)
| ~ c1_2(a262,X0) ) ).
cnf(u3195,negated_conjecture,
( ~ c5_2(a262,X0)
| c1_2(a262,X0) ) ).
cnf(u3221,negated_conjecture,
( ~ c4_2(a262,X1)
| c5_2(a262,X1)
| ~ c3_2(a262,X1) ) ).
cnf(u3228,negated_conjecture,
( ~ c5_2(a262,X1)
| ~ c3_2(a262,X1)
| c2_2(a262,X1) ) ).
cnf(u3242,negated_conjecture,
( c4_2(a262,X0)
| c1_2(a262,X0) ) ).
cnf(u3258,negated_conjecture,
~ c3_2(a262,a216) ).
cnf(u3270,negated_conjecture,
c4_2(a262,a216) ).
cnf(u3317,negated_conjecture,
( ~ c1_2(a248,X0)
| c2_2(a248,X0)
| ~ c5_2(a248,X0) ) ).
cnf(u3876,negated_conjecture,
~ c2_2(a248,a221) ).
cnf(u3324,negated_conjecture,
c4_2(a248,a221) ).
cnf(u3328,negated_conjecture,
c5_2(a248,a221) ).
cnf(u3335,negated_conjecture,
c1_2(a248,a222) ).
cnf(u3346,negated_conjecture,
~ c2_2(a248,a222) ).
cnf(u3353,negated_conjecture,
( ~ c4_2(a248,X0)
| c3_2(a248,X0)
| c5_2(a248,X0) ) ).
cnf(u3378,negated_conjecture,
c1_2(a248,a181) ).
cnf(u3382,negated_conjecture,
c5_2(a248,a181) ).
cnf(u3386,negated_conjecture,
~ c3_2(a248,a181) ).
cnf(u3393,negated_conjecture,
( ~ c4_2(a248,X0)
| ~ c1_2(a248,X0)
| ~ c3_2(a248,X0) ) ).
cnf(u3422,negated_conjecture,
~ c1_2(a248,a217) ).
cnf(u3582,negated_conjecture,
~ c4_1(a182) ).
cnf(u3525,negated_conjecture,
c2_2(a182,a221) ).
cnf(u3529,negated_conjecture,
c4_2(a182,a221) ).
cnf(u3533,negated_conjecture,
c5_2(a182,a221) ).
cnf(u3540,negated_conjecture,
c1_2(a182,a222) ).
cnf(u3551,negated_conjecture,
~ c2_2(a182,a222) ).
cnf(u3556,negated_conjecture,
( ~ c3_2(a182,X1)
| c2_2(a182,X1)
| ~ c5_2(a182,X1) ) ).
cnf(u3604,negated_conjecture,
c4_2(a182,a222) ).
cnf(u3624,negated_conjecture,
c2_2(a182,a190) ).
cnf(u3675,negated_conjecture,
c2_2(a188,a178) ).
cnf(u3692,negated_conjecture,
( c5_2(a193,X0)
| c1_2(a193,X0)
| c4_2(a193,X0) ) ).
cnf(u3715,negated_conjecture,
c4_2(a193,a223) ).
cnf(u3733,negated_conjecture,
c4_2(a193,a195) ).
cnf(u3740,negated_conjecture,
c1_2(a193,a217) ).
cnf(u3755,negated_conjecture,
~ c5_2(a193,a217) ).
cnf(u3783,negated_conjecture,
~ c1_2(a248,a216) ).
cnf(u3793,negated_conjecture,
~ c3_2(a182,a216) ).
cnf(u3865,negated_conjecture,
c2_2(a248,a195) ).
cnf(u3895,negated_conjecture,
~ c3_2(a248,a221) ).
cnf(u3880,negated_conjecture,
c5_2(a248,a213) ).
cnf(u3903,negated_conjecture,
~ c1_2(a248,a213) ).
cnf(u3916,negated_conjecture,
c2_1(a189) ).
cnf(u3946,negated_conjecture,
( ~ c5_2(a189,X0)
| ~ c1_2(a189,X0)
| ~ c3_2(a189,X0) ) ).
cnf(u4277,negated_conjecture,
~ c5_1(a189) ).
cnf(u3956,negated_conjecture,
c1_2(a189,a181) ).
cnf(u3960,negated_conjecture,
c5_2(a189,a181) ).
cnf(u3964,negated_conjecture,
~ c3_2(a189,a181) ).
cnf(u3971,negated_conjecture,
c4_1(a189) ).
cnf(u3974,negated_conjecture,
c3_2(a189,a206) ).
cnf(u3984,negated_conjecture,
c1_2(a189,a222) ).
cnf(u3987,negated_conjecture,
c2_2(a189,a223) ).
cnf(u3995,negated_conjecture,
~ c2_2(a189,a222) ).
cnf(u4003,negated_conjecture,
( c3_2(a189,X0)
| ~ c4_2(a189,X0)
| c5_2(a189,X0) ) ).
cnf(u4024,negated_conjecture,
c1_1(a189) ).
cnf(u4028,negated_conjecture,
( c2_2(a189,X0)
| ~ c5_2(a189,X0)
| ~ c1_2(a189,X0) ) ).
cnf(u4054,negated_conjecture,
( c3_2(a189,X0)
| ~ c1_2(a189,X0)
| c4_2(a189,X0) ) ).
cnf(u4067,negated_conjecture,
c1_2(a189,a184) ).
cnf(u4071,negated_conjecture,
c3_2(a189,a184) ).
cnf(u4123,negated_conjecture,
( c5_2(a189,X0)
| c1_2(a189,X0) ) ).
cnf(u4139,negated_conjecture,
c1_2(a189,a223) ).
cnf(u4146,negated_conjecture,
c3_2(a189,a217) ).
cnf(u4149,negated_conjecture,
c5_2(a189,a216) ).
cnf(u4169,negated_conjecture,
c3_2(a189,a222) ).
cnf(u4209,negated_conjecture,
~ c3_2(a189,a216) ).
cnf(u4305,negated_conjecture,
~ c1_2(a189,a217) ).
cnf(u4222,negated_conjecture,
c4_2(a189,a216) ).
cnf(u4274,negated_conjecture,
c4_2(a189,a223) ).
cnf(u4340,negated_conjecture,
~ c2_2(a255,a206) ).
cnf(u4313,negated_conjecture,
c4_2(a189,a181) ).
cnf(u3860,negated_conjecture,
~ c5_2(a248,a222) ).
cnf(u2662,negated_conjecture,
( c2_2(X0,a195)
| c4_1(X0)
| c5_2(X0,a206)
| c1_1(X0)
| c2_1(X0) ) ).
cnf(u1870,negated_conjecture,
ndr1_1(a193) ).
cnf(u1919,negated_conjecture,
ndr1_1(a262) ).
cnf(u4261,negated_conjecture,
~ c3_2(a189,a223) ).
cnf(u2619,negated_conjecture,
( ~ c4_2(a255,X0)
| ~ c3_2(a255,X0) ) ).
cnf(u1737,negated_conjecture,
ndr1_1(a255) ).
cnf(u2801,negated_conjecture,
c2_2(a188,a222) ).
cnf(u1920,negated_conjecture,
c3_2(a262,a178) ).
cnf(u4353,negated_conjecture,
( c5_2(X0,a206)
| c4_1(X0)
| c1_1(X0)
| c2_1(X0)
| c4_2(X0,a195) ) ).
cnf(u1967,negated_conjecture,
c3_2(a188,a178) ).
cnf(u3668,negated_conjecture,
c2_2(a262,a178) ).
cnf(u1871,negated_conjecture,
c3_2(a193,a178) ).
cnf(u3910,negated_conjecture,
ndr1_1(a189) ).
cnf(u1994,negated_conjecture,
c2_1(a188) ).
cnf(u2322,negated_conjecture,
~ c3_2(a227,a228) ).
cnf(u3280,negated_conjecture,
ndr1_1(a248) ).
cnf(u2783,negated_conjecture,
( c2_2(a188,X0)
| c1_2(a188,X0) ) ).
cnf(u4304,negated_conjecture,
~ c5_2(a189,a222) ).
cnf(u1965,negated_conjecture,
c4_2(a188,a178) ).
cnf(u1865,negated_conjecture,
( ~ c1_2(X34,X35)
| ~ c2_2(X34,X35)
| c2_1(X34)
| c4_2(X34,X35)
| c4_1(X34) ) ).
cnf(u4154,negated_conjecture,
c5_2(a189,a223) ).
cnf(u1866,negated_conjecture,
( ~ c5_2(X24,a190)
| ~ c5_1(X24)
| ~ c1_2(X24,X25)
| c4_2(X24,X25)
| c3_2(X24,X25) ) ).
cnf(u1966,negated_conjecture,
ndr1_1(a188) ).
cnf(u1867,negated_conjecture,
( ~ c5_1(X24)
| c2_2(X24,a190)
| ~ c1_2(X24,X25)
| c4_2(X24,X25)
| c3_2(X24,X25) ) ).
cnf(u1918,negated_conjecture,
c4_2(a262,a178) ).
cnf(u2823,negated_conjecture,
( c5_2(a188,X0)
| c1_2(a188,X0) ) ).
cnf(u4093,negated_conjecture,
( ~ c2_2(a189,X0)
| c5_2(a189,X0) ) ).
cnf(u3712,negated_conjecture,
( c2_2(a193,X0)
| c4_2(a193,X0)
| c1_2(a193,X0) ) ).
cnf(u2640,negated_conjecture,
~ c3_2(a255,a213) ).
cnf(u2173,negated_conjecture,
c2_2(a211,a222) ).
cnf(u2033,negated_conjecture,
c4_2(a179,a178) ).
cnf(u3249,negated_conjecture,
c1_2(a262,a178) ).
cnf(u3842,negated_conjecture,
c3_2(a193,a221) ).
cnf(u2035,negated_conjecture,
c3_2(a179,a178) ).
cnf(u3818,negated_conjecture,
( ~ c4_2(X92,X93)
| c2_1(X92)
| ~ c2_2(X92,X93)
| c3_2(X92,X93)
| c3_1(X92) ) ).
cnf(u1724,negated_conjecture,
( ~ c4_2(X41,X42)
| c2_1(X41)
| ~ c2_2(X41,X42)
| c3_2(X41,X42)
| c5_1(X41) ) ).
cnf(u3252,negated_conjecture,
( ~ c3_2(a262,X0)
| c1_2(a262,X0) ) ).
cnf(u2176,negated_conjecture,
( ~ c2_2(X0,a195)
| c2_1(X0)
| c4_2(X0,a195)
| c4_1(X0)
| c1_1(X0) ) ).
cnf(u4233,negated_conjecture,
c1_2(a189,a216) ).
cnf(u3891,negated_conjecture,
c2_2(a248,a181) ).
cnf(u3144,negated_conjecture,
c2_2(a193,a178) ).
cnf(u3772,negated_conjecture,
c5_2(a188,a178) ).
cnf(u2859,negated_conjecture,
c5_2(a255,a213) ).
cnf(u1892,negated_conjecture,
c4_2(a193,a178) ).
cnf(u3279,negated_conjecture,
c1_2(a255,a206) ).
cnf(u3852,negated_conjecture,
c5_2(a262,a178) ).
cnf(u2642,negated_conjecture,
c1_2(a255,a213) ).
cnf(u1868,negated_conjecture,
( ~ c1_2(X24,X25)
| c1_2(X24,a190)
| ~ c5_1(X24)
| c4_2(X24,X25)
| c3_2(X24,X25) ) ).
%------------------------------------------------------------------------------
%----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/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n019.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:21:18 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 8.76/1.95 % (4132307)Detected formulas, will run a generic FOF schedule.
% 8.76/1.95 % (4132326)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3485556472:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.76/1.95 % (4132323)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=1844397061:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.76/1.95 % (4132331)dis-21_1_sil=8000:lcm=predicate:random_seed=854906584:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.76/1.95 % (4132324)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3275105589:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.76/1.95 % (4132327)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3202239355:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.76/1.95 % (4132328)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3215983789:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.76/1.95 % (4132330)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2525081917:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.76/1.95 % (4132327)Instruction limit reached!
% 8.76/1.95 % (4132327)------------------------------
% 8.76/1.95 % (4132327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.95 % (4132327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.95 % (4132327)CaDiCaL version: 2.1.3
% 8.76/1.95 % (4132327)Termination reason: Instruction limit
% 8.76/1.95 % (4132327)Termination phase: Saturation
% 8.76/1.95 % (4132327)Time elapsed: 0.069 s
% 8.76/1.95 % (4132327)Peak memory usage: 90 MB
% 8.76/1.95 % (4132327)Instructions burned: 110 (million)
% 8.76/1.95 % (4132331)Instruction limit reached!
% 8.76/1.95 % (4132331)------------------------------
% 8.76/1.95 % (4132331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.95 % (4132331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.95 % (4132331)CaDiCaL version: 2.1.3
% 8.76/1.95 % (4132331)Termination reason: Instruction limit
% 8.76/1.95 % (4132331)Termination phase: Saturation
% 8.76/1.95 % (4132331)Time elapsed: 0.074 s
% 8.76/1.95 % (4132331)Peak memory usage: 90 MB
% 8.76/1.95 % (4132331)Instructions burned: 131 (million)
% 8.76/1.95 % (4132328)Instruction limit reached!
% 8.76/1.95 % (4132328)------------------------------
% 8.76/1.95 % (4132328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.95 % (4132328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.95 % (4132328)CaDiCaL version: 2.1.3
% 8.76/1.95 % (4132328)Termination reason: Instruction limit
% 8.76/1.95 % (4132328)Termination phase: Saturation
% 8.76/1.95 % (4132328)Time elapsed: 0.074 s
% 8.76/1.95 % (4132328)Peak memory usage: 88 MB
% 8.76/1.95 % (4132328)Instructions burned: 120 (million)
% 8.76/1.95 % (4132330)Refutation not found, incomplete strategy
% 8.76/1.95 % (4132330)------------------------------
% 8.76/1.95 % (4132330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.95 % (4132330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.95 % (4132330)CaDiCaL version: 2.1.3
% 8.76/1.95 % (4132330)Termination reason: Refutation not found, incomplete strategy
% 8.76/1.95 % (4132330)Time elapsed: 0.094 s
% 8.76/1.95 % (4132330)Peak memory usage: 91 MB
% 8.76/1.95 % (4132330)Instructions burned: 137 (million)
% 8.76/1.95 % (4132411)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1487165958:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.76/1.95 % (4132411)Refutation not found, incomplete strategy
% 8.76/1.95 % (4132411)------------------------------
% 8.76/1.95 % (4132411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.95 % (4132411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.95 % (4132411)CaDiCaL version: 2.1.3
% 8.76/1.95 % (4132411)Termination reason: Refutation not found, incomplete strategy
% 8.76/1.95 % (4132411)Time elapsed: 0.036 s
% 8.76/1.95 % (4132411)Peak memory usage: 91 MB
% 8.76/1.95 % (4132411)Instructions burned: 103 (million)
% 8.76/1.95 % (4132409)lrs+10_1_sil=8000:sp=occurrence:random_seed=2774792431:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.76/1.95 % (4132410)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1277947287:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.76/1.95 % (4132410)Refutation not found, incomplete strategy
% 8.76/1.95 % (4132410)------------------------------
% 8.76/1.95 % (4132410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.95 % (4132410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.95 % (4132410)CaDiCaL version: 2.1.3
% 8.76/1.95 % (4132410)Termination reason: Refutation not found, incomplete strategy
% 8.76/1.95 % (4132410)Time elapsed: 0.018 s
% 8.76/1.95 % (4132410)Peak memory usage: 90 MB
% 8.76/1.95 % (4132410)Instructions burned: 23 (million)
% 8.76/1.95 % (4132330)------------------------------
% 8.76/1.95 % (4132330)------------------------------
% 8.76/1.95 % (4132409)Instruction limit reached!
% 8.76/1.95 % (4132409)------------------------------
% 8.76/1.95 % (4132409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.96 % (4132409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.96 % (4132409)CaDiCaL version: 2.1.3
% 8.76/1.96 % (4132409)Termination reason: Instruction limit
% 8.76/1.96 % (4132409)Termination phase: Saturation
% 8.76/1.96 % (4132409)Time elapsed: 0.153 s
% 8.76/1.96 % (4132409)Peak memory usage: 92 MB
% 8.76/1.96 % (4132409)Instructions burned: 285 (million)
% 8.76/1.96 % (4132411)------------------------------
% 8.76/1.96 % (4132411)------------------------------
% 8.76/1.96 % (4132410)------------------------------
% 8.76/1.96 % (4132410)------------------------------
% 8.76/1.96 % (4132463)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=571076757:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 8.76/1.96 % (4132462)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4035410753:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 8.76/1.96 % (4132464)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3300569818:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 8.76/1.96 % (4132462)Refutation not found, incomplete strategy
% 8.76/1.96 % (4132462)------------------------------
% 8.76/1.96 % (4132462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.96 % (4132462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.96 % (4132462)CaDiCaL version: 2.1.3
% 8.76/1.96 % (4132462)Termination reason: Refutation not found, incomplete strategy
% 8.76/1.96 % (4132462)Time elapsed: 0.013 s
% 8.76/1.96 % (4132462)Peak memory usage: 89 MB
% 8.76/1.96 % (4132462)Instructions burned: 21 (million)
% 8.76/1.96 % (4132465)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=176019623:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.76/1.96 % (4132463)Instruction limit reached!
% 8.76/1.96 % (4132463)------------------------------
% 8.76/1.96 % (4132463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.96 % (4132463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.96 % (4132463)CaDiCaL version: 2.1.3
% 8.76/1.96 % (4132463)Termination reason: Instruction limit
% 8.76/1.96 % (4132463)Termination phase: Saturation
% 8.76/1.96 % (4132463)Time elapsed: 0.184 s
% 8.76/1.96 % (4132463)Peak memory usage: 92 MB
% 8.76/1.96 % (4132463)Instructions burned: 294 (million)
% 8.76/1.96 % (4132465)Instruction limit reached!
% 8.76/1.96 % (4132465)------------------------------
% 8.76/1.96 % (4132465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.96 % (4132465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.96 % (4132465)CaDiCaL version: 2.1.3
% 8.76/1.96 % (4132465)Termination reason: Instruction limit
% 8.76/1.96 % (4132465)Termination phase: Saturation
% 8.76/1.96 % (4132465)Time elapsed: 0.100 s
% 8.76/1.96 % (4132465)Peak memory usage: 91 MB
% 8.76/1.96 % (4132465)Instructions burned: 113 (million)
% 8.76/1.96 % (4132462)------------------------------
% 8.76/1.96 % (4132462)------------------------------
% 8.76/1.96 % (4132324)First to succeed.
% 8.76/1.96 % (4132324)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4132307"
% 8.76/1.96 % (4132478)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=62224728:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 8.76/1.96 % (4132479)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=626774907:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 8.76/1.96 % (4132482)lrs+10_1_sil=8000:sp=occurrence:random_seed=542421894:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 8.76/1.96 % (4132478)Instruction limit reached!
% 8.76/1.96 % (4132478)------------------------------
% 8.76/1.96 % (4132478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.96 % (4132478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.96 % (4132478)CaDiCaL version: 2.1.3
% 8.76/1.96 % (4132478)Termination reason: Instruction limit
% 8.76/1.96 % (4132478)Termination phase: Saturation
% 8.76/1.96 % (4132478)Time elapsed: 0.107 s
% 8.76/1.96 % (4132478)Peak memory usage: 89 MB
% 8.76/1.96 % (4132478)Instructions burned: 127 (million)
% 8.76/1.96 % (4132479)Instruction limit reached!
% 8.76/1.96 % (4132479)------------------------------
% 8.76/1.96 % (4132479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/1.96 % (4132479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/1.96 % (4132479)CaDiCaL version: 2.1.3
% 8.76/1.96 % (4132479)Termination reason: Instruction limit
% 8.76/1.96 % (4132479)Termination phase: Saturation
% 8.76/1.96 % (4132479)Time elapsed: 0.093 s
% 8.76/1.96 % (4132479)Peak memory usage: 90 MB
% 8.76/1.96 % (4132479)Instructions burned: 114 (million)
% 8.76/1.96 % SZS status CounterSatisfiable for theBenchmark
% 8.76/1.96 % SZS output start Saturation.
% See solution above
% 8.76/1.96 % SZS output start Definitions and Model Updates.
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever ~c5_0 | c2_1(X40) | ndr1_1(X40) | c4_2(X40,a204) | ~ndr1_0 is false, set c4_2(X40,a204) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c3_1(X0) | c4_2(X0,a245) | ndr1_1(X0) | ~ndr1_0 | ~sP4 is false, set c4_2(X0,a245) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever ~c5_0 | c2_1(X40) | c4_2(X40,a203) | ndr1_1(X40) | ~ndr1_0 is false, set c4_2(X40,a203) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c5_1(X0) | ndr1_1(X0) | c5_2(X0,a252) | ~ndr1_0 | ~sP3 is false, set c5_2(X0,a252) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c1_0 | ~c2_0 | c5_2(X3,a175) | ndr1_1(X3) | ~ndr1_0 is false, set c5_2(X3,a175) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c3_1(X0) | c5_2(X0,a245) | ndr1_1(X0) | ~ndr1_0 | ~sP4 is false, set c5_2(X0,a245) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c5_1(X0) | ndr1_1(X0) | ~c1_2(X0,a252) | ~ndr1_0 | ~sP3 is false, set ~c1_2(X0,a252) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c3_1(X0) | ndr1_1(X0) | ~c1_2(X0,a246) | ~ndr1_0 | ~sP4 is false, set ~c1_2(X0,a246) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever ~c5_0 | c2_1(X40) | ~c1_2(X40,a203) | ndr1_1(X40) | ~ndr1_0 is false, set ~c1_2(X40,a203) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c3_1(X0) | c1_2(X0,a245) | ndr1_1(X0) | ~ndr1_0 | ~sP4 is false, set c1_2(X0,a245) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c5_1(X0) | c1_2(X0,a251) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set c1_2(X0,a251) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c5_0 | c3_1(X49) | ~c3_2(X49,a216) | ndr1_1(X49) | ~ndr1_0 is false, set ~c3_2(X49,a216) to true
% 8.76/1.96 for all groundings,
% 8.76/1.96 whenever c5_1(X0) | ndr1_1(X0) | c2_2(X0,a252) | ~ndr1_0 | ~sP3 is false, set c2_2(X0,a252) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c3_1(X49) | c2_2(X49,a216) | ndr1_1(X49) | ~ndr1_0 is false, set c2_2(X49,a216) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c1_0 | ~c2_0 | c3_2(X3,a175) | ndr1_1(X3) | ~ndr1_0 is false, set c3_2(X3,a175) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c1_0 | ~c2_0 | ndr1_1(X3) | c3_2(X3,a176) | ~ndr1_0 is false, set c3_2(X3,a176) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c3_1(X49) | ndr1_1(X49) | c3_2(X49,a217) | ~ndr1_0 is false, set c3_2(X49,a217) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_1(X0) | ndr1_1(X0) | ~c4_2(X0,a246) | ~ndr1_0 | ~sP4 is false, set ~c4_2(X0,a246) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c1_0 | ~c2_0 | ~c4_2(X3,a175) | ndr1_1(X3) | ~ndr1_0 is false, set ~c4_2(X3,a175) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_1(X0) | ndr1_1(X0) | ~c5_2(X0,a246) | ~ndr1_0 | ~sP4 is false, set ~c5_2(X0,a246) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c1_0 | ~c2_0 | ndr1_1(X3) | ~c5_2(X3,a176) | ~ndr1_0 is false, set ~c5_2(X3,a176) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_1(X0) | ~c5_2(X0,a251) | ndr1_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c5_2(X0,a251) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c3_1(X49) | ndr1_1(X49) | ~c2_2(X49,a217) | ~ndr1_0 is false, set ~c2_2(X49,a217) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(a225,X60) | ~c2_2(a225,X60) | ~ndr1_1(a225) | ndr1_0 is false, set ~c2_2(a225,X60) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | ndr1_0 | ~c2_2(a226,X62) | ~c3_2(a226,X62) | ~c4_2(a226,X62) | ~ndr1_1(a226) is false, set ~c2_2(a226,X62) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | ndr1_0 | c1_2(a226,X61) | ~c2_2(a226,X61) | ~c4_2(a226,X61) | ~ndr1_1(a226) is false, set ~c2_2(a226,X61) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c1_0 | ~c2_0 | ndr1_1(X3) | ~c2_2(X3,a176) | ~ndr1_0 is false, set ~c2_2(X3,a176) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c5_0 | c2_1(X40) | ndr1_1(X40) | ~c2_2(X40,a204) | ~ndr1_0 is false, set ~c2_2(X40,a204) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c3_0 | c5_1(X84) | c4_2(X84,X85) | ~c1_2(X84,X85) | ~c2_2(X84,X85) | ~ndr1_1(X84) | ~c1_2(X84,X86) | ~c5_2(X84,X86) | ~ndr1_1(X84) | ~ndr1_0 | ndr1_0 is false, set c5_1(X84) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c4_1(a225) | ndr1_0 is false, set c4_1(a225) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | ~c4_1(X37) | ~c5_1(X37) | ndr1_1(X37) | ~ndr1_0 | ndr1_0 is false, set c3_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | ~c4_1(X37) | ~c5_1(X37) | c5_2(X37,a198) | ~ndr1_0 | ndr1_0 is false, set c3_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | ~c4_1(X37) | ~c5_1(X37) | ~c1_2(X37,a198) | ~ndr1_0 | ndr1_0 is false, set c3_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | ndr1_0 | ~c1_1(a201) is false, set ~c1_1(a201) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c4_1(X105) | ~c1_1(X105) | ~ndr1_0 | ~c3_1(X106) | ~c5_1(X106) | c2_2(X106,X107) | c3_2(X106,X107) | ~c5_2(X106,X107) | ~ndr1_1(X106) | ~ndr1_0 | ndr1_0 is false, set ~c1_1(X105) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | c2_1(a200) | ndr1_0 is false, set c2_1(a200) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c2_1(X41) | c5_1(X41) | c3_2(X41,X42) | ~c2_2(X41,X42) | ~c4_2(X41,X42) | ~ndr1_1(X41) | ~ndr1_0 | c4_1(X43) | c2_2(X43,X44) | ~c1_2(X43,X44) | ~c3_2(X43,X44) | ~ndr1_1(X43) | ndr1_1(X43) | ~ndr1_0 is false, set c2_1(X41) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | ndr1_0 | c2_1(a201) is false, set c2_1(a201) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c1_0 | c4_1(X64) | ~c1_1(X64) | c1_2(X64,X65) | ~c4_2(X64,X65) | ~ndr1_1(X64) | ~ndr1_0 | ndr1_0 is false, set ~c1_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c1_0 | c4_1(X66) | c3_2(X66,X67) | ~c4_2(X66,X67) | ~c5_2(X66,X67) | ~ndr1_1(X66) | ndr1_1(X66) | ~ndr1_0 | c5_1(X68) | ~c4_1(X68) | c2_2(X68,X69) | ~c3_2(X68,X69) | ~ndr1_1(X68) | ~ndr1_0 is false, set ~c1_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | c1_1(X30) | c2_1(X30) | ndr1_1(X30) | ~ndr1_0 | ~c1_2(X31,X32) | ~c2_2(X31,X32) | ~ndr1_1(X31) | ~c3_2(X31,X33) | ~c4_2(X31,X33) | ~c5_2(X31,X33) | ~ndr1_1(X31) | ndr1_1(X31) | ~ndr1_0 is false, set c1_1(X30) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | c1_1(X30) | c2_1(X30) | c1_2(X30,a195) | ~ndr1_0 | ~c1_2(X31,X32) | ~c2_2(X31,X32) | ~ndr1_1(X31) | ~c3_2(X31,X33) | ~c4_2(X31,X33) | ~c5_2(X31,X33) | ~ndr1_1(X31) | ndr1_1(X31) | ~ndr1_0 is false, set c1_1(X30) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c1_1(X87) | ~c2_1(X87) | c1_2(X87,X88) | c3_2(X87,X88) | ~c4_2(X87,X88) | ~ndr1_1(X87) | ~ndr1_0 | c1_1(X89) | ~c2_1(X89) | c1_2(X89,X90) | c4_2(X89,X90) | ~ndr1_1(X89) | ~ndr1_0 | ndr1_0 is false, set c1_1(X87) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | c1_1(X30) | c2_1(X30) | c3_2(X30,a195) | ~ndr1_0 | ~c1_2(X31,X32) | ~c2_2(X31,X32) | ~ndr1_1(X31) | ~c3_2(X31,X33) | ~c4_2(X31,X33) | ~c5_2(X31,X33) | ~ndr1_1(X31) | ndr1_1(X31) | ~ndr1_0 is false, set c1_1(X30) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | c1_1(X30) | c2_1(X30) | c5_2(X30,a195) | ~ndr1_0 | ~c1_2(X31,X32) | ~c2_2(X31,X32) | ~ndr1_1(X31) | ~c3_2(X31,X33) | ~c4_2(X31,X33) | ~c5_2(X31,X33) | ~ndr1_1(X31) | ndr1_1(X31) | ~ndr1_0 is false, set c1_1(X30) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c3_1(a225) | ndr1_0 is false, set c3_1(a225) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c2_1(X92) | c3_1(X92) | c3_2(X92,X93) | ~c2_2(X92,X93) | ~c4_2(X92,X93) | ~ndr1_1(X92) | ~ndr1_0 | ~c4_1(X94) | ~c1_2(X94,X95) | ~c2_2(X94,X95) | ~c5_2(X94,X95) | ~ndr1_1(X94) | ~ndr1_0 | ndr1_0 is false, set c3_1(X92) to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c3_0 | c5_0 | ~c5_1(X24) | c3_2(X24,X25) | c4_2(X24,X25) | ~c1_2(X24,X25) | ~ndr1_1(X24) | ndr1_1(X24) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(X52,X53) | c5_2(X52,X53) | ~c4_2(X52,X53) | ~ndr1_1(X52) | c2_2(X52,X54) | ~c1_2(X52,X54) | ~c5_2(X52,X54) | ~ndr1_1(X52) | ndr1_1(X52) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(X55,X56) | ~c5_2(X55,X56) | ~ndr1_1(X55) | ndr1_1(X55) | ndr1_1(X55) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(X55,X56) | ~c5_2(X55,X56) | ~ndr1_1(X55) | ndr1_1(X55) | c3_2(X55,a223) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(X55,X56) | ~c5_2(X55,X56) | ~ndr1_1(X55) | ndr1_1(X55) | c2_2(X55,a223) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(X55,X56) | ~c5_2(X55,X56) | ~ndr1_1(X55) | c1_2(X55,a222) | ndr1_1(X55) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(X55,X56) | ~c5_2(X55,X56) | ~ndr1_1(X55) | ndr1_1(X55) | ~c5_2(X55,a223) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c1_2(X55,X56) | ~c5_2(X55,X56) | ~ndr1_1(X55) | ~c2_2(X55,a222) | ndr1_1(X55) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | c2_2(X57,X58) | ~c3_2(X57,X58) | ~c5_2(X57,X58) | ~ndr1_1(X57) | c3_2(X57,X59) | c5_2(X57,X59) | ~c4_2(X57,X59) | ~ndr1_1(X57) | ndr1_1(X57) | ~ndr1_0 is false, set c5_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c2_0 | ~c5_0 | ~c4_1(X15) | c3_2(X15,X16) | ~c4_2(X15,X16) | ~ndr1_1(X15) | ndr1_1(X15) | ~ndr1_0 is false, set c2_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c2_0 | ~c5_1(X18) | c3_2(X18,X19) | c4_2(X18,X19) | c5_2(X18,X19) | ~ndr1_1(X18) | ndr1_1(X18) | ~ndr1_0 is false, set c2_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c2_0 | c5_0 | c5_1(X12) | c1_2(X12,X13) | ~c4_2(X12,X13) | ~ndr1_1(X12) | ndr1_1(X12) | ~ndr1_0 is false, set c2_0 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP4 | c4_1(X104) | ~c3_1(X104) | ndr1_1(X104) | ~ndr1_0 | ndr1_0 is false, set sP4 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP4 | c4_1(X104) | ~c3_1(X104) | c3_2(X104,a247) | ~ndr1_0 | ndr1_0 is false, set sP4 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP4 | c4_1(X104) | ~c3_1(X104) | ~c4_2(X104,a247) | ~ndr1_0 | ndr1_0 is false, set sP4 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | ndr1_0 | ~c3_1(a255) is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | c1_1(a253) | ndr1_0 is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | ndr1_0 | ndr1_0 is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | ndr1_1(a253) | ndr1_0 is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | c3_2(a253,a254) | ndr1_0 is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | c2_2(a253,a254) | ndr1_0 is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | c5_2(a253,a254) | ndr1_0 is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever sP3 | ~c4_1(a253) | ndr1_0 is false, set sP3 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ndr1_0 | ~sP2 is false, set ~sP2 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c1_0 | ~c5_1(X70) | c1_2(X70,X71) | ~c3_2(X70,X71) | ~ndr1_1(X70) | ndr1_1(X70) | ~ndr1_0 | sP5 is false, set sP5 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c4_1(X45) | c2_2(X45,X46) | ~c1_2(X45,X46) | ~ndr1_1(X45) | ndr1_1(X45) | ~ndr1_0 | sP8 is false, set sP8 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c2_1(X114) | c1_2(X114,a256) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c2_1(X114) | c3_2(X114,a256) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c2_1(X114) | ndr1_1(X114) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever c5_0 | ~c1_1(X50) | c1_2(X50,X51) | c4_2(X50,X51) | c5_2(X50,X51) | ~ndr1_1(X50) | ndr1_1(X50) | ~ndr1_0 | sP6 is false, set sP6 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ndr1_0 | ~sP6 is false, set ~sP6 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ndr1_0 | ~sP8 is false, set ~sP8 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ndr1_0 | ~sP7 is false, set ~sP7 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ndr1_0 | ~sP5 is false, set ~sP5 to true
% 10.93/2.15 for all groundings,
% 10.93/2.15 whenever ~c4_0 is false, set ~c4_0 to true
% 10.93/2.15 % SZS output end Definitions and Model Updates.
% 10.93/2.15 % (4132324)------------------------------
% 10.93/2.15 % (4132324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.15 % (4132324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.15 % (4132324)CaDiCaL version: 2.1.3
% 10.93/2.15 % (4132324)Termination reason: Satisfiable
% 10.93/2.15 % (4132324)Time elapsed: 0.939 s
% 10.93/2.15 % (4132324)Peak memory usage: 133 MB
% 10.93/2.15 % (4132324)Instructions burned: 1261 (million)
% 10.93/2.15 % (4132324)------------------------------
% 10.93/2.15 % (4132324)------------------------------
% 10.93/2.15 % (4132307)Success in time 1.506 s
% 10.93/2.15 % Vampire exiting
%------------------------------------------------------------------------------