%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN425+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 : 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 01:50:35 PM UTC 2026
% Result : CounterSatisfiable 5.08s 1.43s
% Output : Saturation 5.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u988,negated_conjecture,
c10_0 ).
cnf(u1012,negated_conjecture,
ndr1_1(a1363) ).
cnf(u998,negated_conjecture,
~ c6_1(a1363) ).
cnf(u1002,negated_conjecture,
c2_2(a1363,a1364) ).
cnf(u1006,negated_conjecture,
~ c1_2(a1363,a1364) ).
cnf(u1010,negated_conjecture,
~ c7_2(a1363,a1364) ).
cnf(u1016,negated_conjecture,
ndr1_0 ).
cnf(u1234,negated_conjecture,
~ c2_0 ).
cnf(u1023,negated_conjecture,
c1_0 ).
cnf(u1027,negated_conjecture,
~ c6_0 ).
cnf(u1032,negated_conjecture,
~ c8_0 ).
cnf(u1036,negated_conjecture,
( ~ c8_1(X166)
| ~ ndr1_1(X166)
| ~ c4_2(X166,X167)
| c5_2(X166,X167)
| c9_2(X166,X167)
| c10_2(X166,a1362) ) ).
cnf(u1040,negated_conjecture,
( ~ c3_2(X166,a1362)
| ~ ndr1_1(X166)
| ~ c4_2(X166,X167)
| c5_2(X166,X167)
| c9_2(X166,X167)
| ~ c8_1(X166) ) ).
cnf(u1044,negated_conjecture,
( ~ c8_1(X166)
| ~ ndr1_1(X166)
| ~ c4_2(X166,X167)
| c5_2(X166,X167)
| c9_2(X166,X167)
| c4_2(X166,a1362) ) ).
cnf(u1052,negated_conjecture,
sP0 ).
cnf(u1070,negated_conjecture,
sP1 ).
cnf(u1096,negated_conjecture,
~ c7_1(a1354) ).
cnf(u1099,negated_conjecture,
~ c3_1(a1353) ).
cnf(u1103,negated_conjecture,
c4_1(a1354) ).
cnf(u1107,negated_conjecture,
~ c5_1(a1353) ).
cnf(u1121,negated_conjecture,
( ~ c2_2(X162,a1352)
| c3_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1125,negated_conjecture,
( c10_2(X162,a1352)
| c3_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1129,negated_conjecture,
( ~ c8_2(X162,a1352)
| c3_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1133,negated_conjecture,
( ~ c2_2(X162,a1352)
| c8_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1137,negated_conjecture,
( c10_2(X162,a1352)
| c8_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1141,negated_conjecture,
( ~ c8_2(X162,a1352)
| c8_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1145,negated_conjecture,
( ~ c2_2(X162,a1352)
| c10_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1149,negated_conjecture,
( c10_2(X162,a1352)
| c10_2(X162,a1351)
| c2_1(X162) ) ).
cnf(u1153,negated_conjecture,
( c10_2(X162,a1351)
| ~ c8_2(X162,a1352)
| c2_1(X162) ) ).
cnf(u1157,negated_conjecture,
( c2_1(X162)
| ndr1_1(X162) ) ).
cnf(u1164,negated_conjecture,
( c7_2(a1350,X161)
| c6_2(a1350,X161)
| c1_2(a1350,X161) ) ).
cnf(u2468,negated_conjecture,
~ sP2 ).
cnf(u1174,negated_conjecture,
~ c10_1(a1350) ).
cnf(u1188,negated_conjecture,
~ c2_2(a1346,a1347) ).
cnf(u1193,negated_conjecture,
~ c4_2(a1346,a1347) ).
cnf(u1197,negated_conjecture,
c6_2(a1346,a1347) ).
cnf(u1201,negated_conjecture,
ndr1_1(a1346) ).
cnf(u1206,negated_conjecture,
( ~ c5_2(a1346,X158)
| c9_2(a1346,X158)
| ~ c10_2(a1346,X158) ) ).
cnf(u1210,negated_conjecture,
( ~ c6_2(a1346,X157)
| c8_2(a1346,X157)
| ~ c10_2(a1346,X157) ) ).
cnf(u2484,negated_conjecture,
~ sP3 ).
cnf(u1221,negated_conjecture,
( ~ c2_2(a1343,X156)
| c3_2(a1343,X156)
| ~ c5_2(a1343,X156) ) ).
cnf(u2513,negated_conjecture,
~ sP4 ).
cnf(u1228,negated_conjecture,
~ c1_1(a1343) ).
cnf(u1232,negated_conjecture,
c3_1(a1343) ).
cnf(u1241,negated_conjecture,
( ~ c1_1(X153)
| ~ c5_1(X153)
| c4_1(X153) ) ).
cnf(u1246,negated_conjecture,
~ c3_0 ).
cnf(u1250,negated_conjecture,
( ~ c9_2(X151,a1340)
| c6_1(X151)
| ~ c1_2(X151,X152)
| ~ ndr1_1(X151)
| ~ c7_2(X151,X152)
| ~ c2_2(X151,X152) ) ).
cnf(u1254,negated_conjecture,
( ~ c1_2(X151,X152)
| c6_1(X151)
| c6_2(X151,a1340)
| ~ ndr1_1(X151)
| ~ c7_2(X151,X152)
| ~ c2_2(X151,X152) ) ).
cnf(u1258,negated_conjecture,
( ~ c2_2(X151,a1340)
| c6_1(X151)
| ~ c1_2(X151,X152)
| ~ ndr1_1(X151)
| ~ c7_2(X151,X152)
| ~ c2_2(X151,X152) ) ).
cnf(u1288,negated_conjecture,
~ c3_1(a1335) ).
cnf(u2531,negated_conjecture,
~ sP5 ).
cnf(u1295,negated_conjecture,
c8_2(a1335,a1336) ).
cnf(u1299,negated_conjecture,
~ c2_2(a1335,a1336) ).
cnf(u1303,negated_conjecture,
ndr1_1(a1335) ).
cnf(u1337,negated_conjecture,
( ~ c10_1(X141)
| c1_2(X141,X143)
| c3_2(X141,X143)
| ~ c5_2(X141,X143)
| ~ ndr1_1(X141)
| c7_2(X141,X142)
| c2_2(X141,X142)
| c10_2(X141,X142) ) ).
cnf(u1349,negated_conjecture,
c10_1(a1327) ).
cnf(u1366,negated_conjecture,
ndr1_1(a1327) ).
cnf(u1356,negated_conjecture,
( ~ c3_2(a1327,X139)
| ~ c10_2(a1327,X139)
| ~ c2_2(a1327,X139) ) ).
cnf(u1360,negated_conjecture,
~ c3_2(a1327,a1328) ).
cnf(u1364,negated_conjecture,
c8_2(a1327,a1328) ).
cnf(u2558,negated_conjecture,
~ sP6 ).
cnf(u1377,negated_conjecture,
( ~ c2_1(X137)
| ~ ndr1_1(X137)
| c8_2(X137,X138)
| c6_2(X137,X138)
| c3_2(X137,X138)
| c7_1(X137) ) ).
cnf(u1404,negated_conjecture,
sP7 ).
cnf(u1407,negated_conjecture,
( ~ c10_1(X134)
| ~ c2_1(X134)
| ~ c2_2(X134,a1317) ) ).
cnf(u1411,negated_conjecture,
( ~ c10_1(X134)
| ~ c2_1(X134)
| ~ c6_2(X134,a1317) ) ).
cnf(u1419,negated_conjecture,
~ c5_1(a1316) ).
cnf(u1429,negated_conjecture,
~ c8_1(a1316) ).
cnf(u1445,negated_conjecture,
( c10_2(X131,a1314)
| ~ c3_2(X131,a1313)
| ~ c7_1(X131) ) ).
cnf(u1449,negated_conjecture,
( ~ c3_2(X131,a1313)
| c4_2(X131,a1314)
| ~ c7_1(X131) ) ).
cnf(u1453,negated_conjecture,
( ~ c3_2(X131,a1313)
| ~ c5_2(X131,a1314)
| ~ c7_1(X131) ) ).
cnf(u1457,negated_conjecture,
( c10_2(X131,a1314)
| c1_2(X131,a1313)
| ~ c7_1(X131) ) ).
cnf(u1461,negated_conjecture,
( c1_2(X131,a1313)
| c4_2(X131,a1314)
| ~ c7_1(X131) ) ).
cnf(u1465,negated_conjecture,
( ~ c5_2(X131,a1314)
| c1_2(X131,a1313)
| ~ c7_1(X131) ) ).
cnf(u1469,negated_conjecture,
( ~ c2_2(X131,a1313)
| c10_2(X131,a1314)
| ~ c7_1(X131) ) ).
cnf(u1473,negated_conjecture,
( ~ c2_2(X131,a1313)
| c4_2(X131,a1314)
| ~ c7_1(X131) ) ).
cnf(u1477,negated_conjecture,
( ~ c5_2(X131,a1314)
| ~ c2_2(X131,a1313)
| ~ c7_1(X131) ) ).
cnf(u1481,negated_conjecture,
( ~ c7_1(X131)
| ndr1_1(X131) ) ).
cnf(u1485,negated_conjecture,
( ~ c4_1(X129)
| ~ c4_2(X129,a1312)
| c9_2(X129,X130)
| ~ ndr1_1(X129)
| ~ c10_2(X129,X130)
| ~ c1_2(X129,X130) ) ).
cnf(u1489,negated_conjecture,
( ~ c4_1(X129)
| c6_2(X129,a1312)
| c9_2(X129,X130)
| ~ ndr1_1(X129)
| ~ c10_2(X129,X130)
| ~ c1_2(X129,X130) ) ).
cnf(u1493,negated_conjecture,
( ~ c3_2(X129,a1312)
| c9_2(X129,X130)
| ~ c4_1(X129)
| ~ ndr1_1(X129)
| ~ c10_2(X129,X130)
| ~ c1_2(X129,X130) ) ).
cnf(u1511,negated_conjecture,
( c6_1(X121)
| ~ c3_1(X121)
| ~ c8_1(X121) ) ).
cnf(u1515,negated_conjecture,
~ c5_1(a1311) ).
cnf(u1518,negated_conjecture,
( ~ c3_1(X119)
| c8_1(X119)
| ~ c2_2(X119,a1310) ) ).
cnf(u1529,negated_conjecture,
~ c4_1(a1311) ).
cnf(u1533,negated_conjecture,
( ~ c3_1(X119)
| c8_1(X119)
| ~ c3_2(X119,a1310) ) ).
cnf(u1539,negated_conjecture,
( ~ c3_1(X119)
| c8_1(X119)
| c1_2(X119,a1310) ) ).
cnf(u1545,negated_conjecture,
( ~ c3_1(X119)
| c8_1(X119)
| ndr1_1(X119) ) ).
cnf(u1562,negated_conjecture,
( ~ c8_1(X113)
| ~ c10_1(X113)
| ~ c7_1(X113) ) ).
cnf(u1590,negated_conjecture,
( ~ c9_2(X111,a1302)
| c1_1(X111)
| ~ c4_1(X111) ) ).
cnf(u1597,negated_conjecture,
( ~ c1_2(X111,a1302)
| c1_1(X111)
| ~ c4_1(X111) ) ).
cnf(u1601,negated_conjecture,
( ~ c4_1(X111)
| ndr1_1(X111)
| c1_1(X111) ) ).
cnf(u1617,negated_conjecture,
( ~ c3_2(X108,a1300)
| ~ c10_1(X108)
| ~ c2_1(X108) ) ).
cnf(u1620,negated_conjecture,
sP9 ).
cnf(u1624,negated_conjecture,
( ~ c10_1(X108)
| c1_2(X108,a1300)
| ~ c2_1(X108) ) ).
cnf(u1628,negated_conjecture,
( c5_2(X108,a1300)
| ~ c10_1(X108)
| ~ c2_1(X108) ) ).
cnf(u2690,negated_conjecture,
~ sP10 ).
cnf(u1636,negated_conjecture,
( ~ c10_2(X104,a1292)
| c3_2(X104,X106)
| c1_2(X104,X106)
| c9_2(X104,X106)
| ~ c7_2(X104,X105)
| ~ ndr1_1(X104)
| ~ c10_2(X104,X105)
| c6_2(X104,X105) ) ).
cnf(u1640,negated_conjecture,
( ~ c7_2(X104,X105)
| c3_2(X104,X106)
| c1_2(X104,X106)
| c9_2(X104,X106)
| c8_2(X104,a1292)
| ~ ndr1_1(X104)
| ~ c10_2(X104,X105)
| c6_2(X104,X105) ) ).
cnf(u1644,negated_conjecture,
( ~ c6_2(X104,a1292)
| c3_2(X104,X106)
| c1_2(X104,X106)
| c9_2(X104,X106)
| ~ c7_2(X104,X105)
| ~ ndr1_1(X104)
| ~ c10_2(X104,X105)
| c6_2(X104,X105) ) ).
cnf(u1679,negated_conjecture,
~ ndr1_1(a1288) ).
cnf(u2712,negated_conjecture,
~ sP11 ).
cnf(u2763,negated_conjecture,
~ sP13 ).
cnf(u2734,negated_conjecture,
~ sP12 ).
cnf(u1734,negated_conjecture,
( ~ c8_2(a1278,X98)
| ~ c10_2(a1278,X98)
| c3_2(a1278,X98) ) ).
cnf(u1738,negated_conjecture,
c7_1(a1278) ).
cnf(u1742,negated_conjecture,
( ~ c3_2(a1278,X97)
| c1_2(a1278,X97)
| ~ c8_2(a1278,X97) ) ).
cnf(u1746,negated_conjecture,
( c6_1(X96)
| ~ c4_1(X96)
| ~ c2_1(X96) ) ).
cnf(u1753,negated_conjecture,
( ~ c4_1(X93)
| ~ c8_2(X93,X94)
| c10_2(X93,X95)
| ~ c9_2(X93,X95)
| ~ c4_2(X93,X95)
| ~ ndr1_1(X93)
| ~ c6_2(X93,X94)
| c5_2(X93,X94) ) ).
cnf(u1826,negated_conjecture,
~ c7_2(a1270,a1271) ).
cnf(u1830,negated_conjecture,
c4_2(a1270,a1271) ).
cnf(u1834,negated_conjecture,
c8_2(a1270,a1271) ).
cnf(u1838,negated_conjecture,
ndr1_1(a1270) ).
cnf(u1842,negated_conjecture,
c9_1(a1270) ).
cnf(u1846,negated_conjecture,
~ c10_1(a1270) ).
cnf(u1851,negated_conjecture,
~ c4_1(a1269) ).
cnf(u1858,negated_conjecture,
c7_1(a1269) ).
cnf(u1948,negated_conjecture,
c5_2(a1252,a1254) ).
cnf(u1952,negated_conjecture,
c2_2(a1252,a1254) ).
cnf(u1956,negated_conjecture,
~ c10_2(a1252,a1254) ).
cnf(u1960,negated_conjecture,
ndr1_1(a1252) ).
cnf(u1964,negated_conjecture,
~ c6_2(a1252,a1253) ).
cnf(u1968,negated_conjecture,
c5_2(a1252,a1253) ).
cnf(u1972,negated_conjecture,
~ c2_2(a1252,a1253) ).
cnf(u1978,negated_conjecture,
( ~ c3_2(a1252,X73)
| c8_2(a1252,X73)
| ~ c4_2(a1252,X73) ) ).
cnf(u1999,negated_conjecture,
( ~ c3_2(X69,X71)
| ~ c2_1(X69)
| c7_2(X69,X71)
| c3_2(X69,X70)
| c10_2(X69,X71)
| ~ ndr1_1(X69)
| c7_2(X69,X70)
| c5_2(X69,X70) ) ).
cnf(u2032,negated_conjecture,
( ~ c6_2(X63,X64)
| c9_1(X63)
| ~ ndr1_1(X63)
| ~ c9_2(X63,X64)
| ~ c5_2(X63,X64) ) ).
cnf(u2040,negated_conjecture,
( ~ c9_2(X57,a1246)
| c7_1(X57) ) ).
cnf(u2043,negated_conjecture,
sP16 ).
cnf(u2894,negated_conjecture,
~ sP17 ).
cnf(u2050,negated_conjecture,
( c5_2(X57,a1246)
| c7_1(X57) ) ).
cnf(u2054,negated_conjecture,
( ~ c1_2(X57,a1246)
| c7_1(X57) ) ).
cnf(u2062,negated_conjecture,
~ c3_1(a1241) ).
cnf(u2096,negated_conjecture,
( ~ c3_1(X52)
| c8_1(X52) ) ).
cnf(u2915,negated_conjecture,
~ sP18 ).
cnf(u2160,negated_conjecture,
( ~ c7_2(X46,a1231)
| ~ ndr1_1(X46)
| c9_2(X46,X47)
| ~ c5_2(X46,X47)
| ~ c3_2(X46,X47)
| ~ c5_1(X46) ) ).
cnf(u2956,negated_conjecture,
~ sP19 ).
cnf(u2167,negated_conjecture,
( ~ c3_2(X46,X47)
| ~ ndr1_1(X46)
| c9_2(X46,X47)
| ~ c5_2(X46,X47)
| c6_2(X46,a1231)
| ~ c5_1(X46) ) ).
cnf(u2171,negated_conjecture,
( ~ c3_2(X46,X47)
| ~ ndr1_1(X46)
| c9_2(X46,X47)
| ~ c5_2(X46,X47)
| c9_2(X46,a1231)
| ~ c5_1(X46) ) ).
cnf(u2187,negated_conjecture,
c2_1(a1223) ).
cnf(u2978,negated_conjecture,
~ sP20 ).
cnf(u2194,negated_conjecture,
~ ndr1_1(a1223) ).
cnf(u2201,negated_conjecture,
~ c4_1(a1223) ).
cnf(u3019,negated_conjecture,
~ sP21 ).
cnf(u2212,negated_conjecture,
~ c6_1(a1220) ).
cnf(u2216,negated_conjecture,
c2_1(a1220) ).
cnf(u2224,negated_conjecture,
( ~ c1_2(X32,X33)
| ~ c4_2(X32,X34)
| c2_2(X32,X34)
| ~ c7_2(X32,X34)
| ~ ndr1_1(X32)
| c4_2(X32,X33)
| c4_1(X32)
| c9_2(X32,X33) ) ).
cnf(u2238,negated_conjecture,
~ c2_2(a1211,a1212) ).
cnf(u2242,negated_conjecture,
~ c8_2(a1211,a1212) ).
cnf(u2246,negated_conjecture,
c10_2(a1211,a1212) ).
cnf(u2250,negated_conjecture,
ndr1_1(a1211) ).
cnf(u2254,negated_conjecture,
~ c10_1(a1211) ).
cnf(u2259,negated_conjecture,
( ~ c7_2(a1211,X27)
| c1_2(a1211,X27)
| c2_2(a1211,X27) ) ).
cnf(u2268,negated_conjecture,
( ~ c9_2(X21,X22)
| ~ c10_2(X21,X23)
| ~ c7_2(X21,X23)
| c3_2(X21,X23)
| ~ ndr1_1(X21)
| c7_1(X21)
| c10_2(X21,X22)
| c6_2(X21,X22) ) ).
cnf(u2275,negated_conjecture,
c9_1(a1207) ).
cnf(u2299,negated_conjecture,
~ c8_1(a1207) ).
cnf(u2342,negated_conjecture,
~ ndr1_1(a1200) ).
cnf(u2372,negated_conjecture,
( c6_1(X4)
| ~ c1_1(X4)
| c10_1(X4) ) ).
cnf(u3046,negated_conjecture,
~ sP22 ).
cnf(u2392,axiom,
( ~ c10_2(X0,a1360)
| c8_1(X0)
| c7_2(X0,a1359) ) ).
cnf(u2396,axiom,
( c7_2(X0,a1359)
| c8_1(X0)
| c9_2(X0,a1360) ) ).
cnf(u2400,axiom,
( c7_2(X0,a1359)
| c8_1(X0)
| c6_2(X0,a1360) ) ).
cnf(u2404,axiom,
( ~ c10_2(X0,a1360)
| c8_1(X0)
| c1_2(X0,a1359) ) ).
cnf(u2408,axiom,
( c9_2(X0,a1360)
| c8_1(X0)
| c1_2(X0,a1359) ) ).
cnf(u2412,axiom,
( c6_2(X0,a1360)
| c8_1(X0)
| c1_2(X0,a1359) ) ).
cnf(u2416,axiom,
( ~ c10_2(X0,a1360)
| c8_1(X0)
| ~ c4_2(X0,a1359) ) ).
cnf(u2420,axiom,
( ~ c4_2(X0,a1359)
| c8_1(X0)
| c9_2(X0,a1360) ) ).
cnf(u2424,axiom,
( ~ c4_2(X0,a1359)
| c8_1(X0)
| c6_2(X0,a1360) ) ).
cnf(u2428,axiom,
( c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u2433,axiom,
( ~ c4_2(X0,a1355)
| c1_2(X0,a1356)
| c8_1(X0) ) ).
cnf(u2437,axiom,
( ~ c4_2(X0,a1356)
| c8_1(X0)
| ~ c4_2(X0,a1355) ) ).
cnf(u2441,axiom,
( ~ c5_2(X0,a1356)
| c8_1(X0)
| ~ c4_2(X0,a1355) ) ).
cnf(u2445,axiom,
( c6_2(X0,a1355)
| c1_2(X0,a1356)
| c8_1(X0) ) ).
cnf(u2449,axiom,
( ~ c4_2(X0,a1356)
| c8_1(X0)
| c6_2(X0,a1355) ) ).
cnf(u2453,axiom,
( ~ c5_2(X0,a1356)
| c8_1(X0)
| c6_2(X0,a1355) ) ).
cnf(u2457,axiom,
( c9_2(X0,a1355)
| c1_2(X0,a1356)
| c8_1(X0) ) ).
cnf(u2461,axiom,
( ~ c4_2(X0,a1356)
| c8_1(X0)
| c9_2(X0,a1355) ) ).
cnf(u2465,axiom,
( ~ c5_2(X0,a1356)
| c8_1(X0)
| c9_2(X0,a1355) ) ).
cnf(u2602,axiom,
( ~ c1_2(X0,X1)
| c8_2(X0,a1319)
| ~ ndr1_1(X0)
| c3_2(X0,a1318)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2606,axiom,
( ~ c1_2(X0,X1)
| c1_2(X0,a1319)
| ~ ndr1_1(X0)
| c3_2(X0,a1318)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2610,axiom,
( ~ c6_2(X0,a1319)
| c3_2(X0,a1318)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2614,axiom,
( ~ c1_2(X0,X1)
| c8_2(X0,a1319)
| ~ ndr1_1(X0)
| c7_2(X0,a1318)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2618,axiom,
( ~ c1_2(X0,X1)
| c1_2(X0,a1319)
| ~ ndr1_1(X0)
| c7_2(X0,a1318)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2622,axiom,
( ~ c6_2(X0,a1319)
| c7_2(X0,a1318)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2626,axiom,
( ~ c8_2(X0,a1318)
| c8_2(X0,a1319)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2630,axiom,
( ~ c8_2(X0,a1318)
| c1_2(X0,a1319)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u2634,axiom,
( ~ c6_2(X0,a1319)
| ~ c8_2(X0,a1318)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| c3_2(X0,X1)
| c9_2(X0,X1) ) ).
cnf(u3116,axiom,
sP8 ).
cnf(u2662,axiom,
ndr1_1(a1307) ).
cnf(u2644,axiom,
( ~ c3_2(a1307,X1)
| c5_2(a1307,X1)
| ~ c9_2(a1307,X1) ) ).
cnf(u2648,axiom,
( ~ c4_2(a1307,X0)
| ~ c5_2(a1307,X0)
| ~ c6_2(a1307,X0) ) ).
cnf(u2652,axiom,
c7_2(a1307,a1308) ).
cnf(u2656,axiom,
c5_2(a1307,a1308) ).
cnf(u2660,axiom,
~ c4_2(a1307,a1308) ).
cnf(u2668,axiom,
~ c5_1(a1298) ).
cnf(u2672,axiom,
~ c4_1(a1298) ).
cnf(u2676,axiom,
c5_2(a1298,a1299) ).
cnf(u2680,axiom,
c4_2(a1298,a1299) ).
cnf(u2684,axiom,
c3_2(a1298,a1299) ).
cnf(u2688,axiom,
ndr1_1(a1298) ).
cnf(u2800,axiom,
~ sP14 ).
cnf(u2843,axiom,
~ sP15 ).
cnf(u2872,axiom,
~ c10_1(a1244) ).
cnf(u2876,axiom,
c2_1(a1244) ).
cnf(u2880,axiom,
c7_2(a1244,a1245) ).
cnf(u2884,axiom,
c4_2(a1244,a1245) ).
cnf(u2888,axiom,
c6_2(a1244,a1245) ).
cnf(u2892,axiom,
ndr1_1(a1244) ).
cnf(u3074,axiom,
~ sP23 ).
cnf(u3103,negated_conjecture,
( c6_1(X125)
| c9_1(X125)
| c7_1(X125) ) ).
cnf(u3110,negated_conjecture,
( ~ c10_1(X115)
| c6_1(X115)
| ~ ndr1_1(X115)
| c3_2(X115,X116)
| ~ c5_2(X115,X116)
| c7_2(X115,X116) ) ).
cnf(u3144,negated_conjecture,
( ~ c1_2(X84,a1260)
| c9_1(X84)
| ~ c7_1(X84) ) ).
cnf(u3151,negated_conjecture,
( ~ c4_2(X84,a1260)
| c9_1(X84)
| ~ c7_1(X84) ) ).
cnf(u3155,negated_conjecture,
( c9_2(X84,a1260)
| c9_1(X84)
| ~ c7_1(X84) ) ).
cnf(u3159,negated_conjecture,
( ndr1_1(X84)
| c9_1(X84)
| ~ c7_1(X84) ) ).
cnf(u3166,negated_conjecture,
( ~ c1_2(X78,X80)
| c2_2(X78,X81)
| c8_2(X78,X81)
| ~ c4_2(X78,X81)
| ~ c5_2(X78,X79)
| c8_2(X78,X80)
| ~ c4_2(X78,X80)
| ~ ndr1_1(X78)
| c4_2(X78,X79)
| c3_2(X78,X79) ) ).
cnf(u3193,negated_conjecture,
( ~ c2_2(a1247,X58)
| c5_2(a1247,X58)
| ~ c10_2(a1247,X58) ) ).
cnf(u3197,negated_conjecture,
c9_1(a1247) ).
cnf(u3201,negated_conjecture,
c6_1(a1247) ).
cnf(u3213,negated_conjecture,
( ~ c1_1(X40)
| ~ c8_2(X40,a1224)
| c7_1(X40) ) ).
cnf(u3217,negated_conjecture,
( c10_2(X40,a1224)
| ~ c1_1(X40)
| c7_1(X40) ) ).
cnf(u3221,negated_conjecture,
( ~ c1_2(X40,a1224)
| ~ c1_1(X40)
| c7_1(X40) ) ).
cnf(u3225,negated_conjecture,
( ndr1_1(X40)
| ~ c1_1(X40)
| c7_1(X40) ) ).
cnf(u3232,negated_conjecture,
( c5_1(X30)
| ~ c2_1(X30)
| c4_1(X30) ) ).
cnf(u3257,negated_conjecture,
c3_1(a1214) ).
cnf(u3264,negated_conjecture,
( c7_2(a1214,X29)
| ~ c5_2(a1214,X29) ) ).
cnf(u3268,negated_conjecture,
c1_1(a1214) ).
cnf(u3276,negated_conjecture,
( ~ c1_2(a1210,X26)
| c2_2(a1210,X26)
| c5_2(a1210,X26) ) ).
cnf(u3280,negated_conjecture,
~ c9_1(a1210) ).
cnf(u3284,negated_conjecture,
c10_1(a1210) ).
cnf(u3290,negated_conjecture,
( ~ c8_1(X10)
| c3_1(X10)
| ~ c1_2(X10,X11)
| ~ ndr1_1(X10)
| c4_2(X10,X11)
| c9_2(X10,X11) ) ).
cnf(u3301,negated_conjecture,
~ c10_2(a1346,a1347) ).
cnf(u3311,negated_conjecture,
~ c10_2(a1346,a1246) ).
cnf(u3981,negated_conjecture,
~ c2_1(a1363) ).
cnf(u3382,negated_conjecture,
~ c2_1(a1327) ).
cnf(u3393,negated_conjecture,
c6_1(a1327) ).
cnf(u3402,negated_conjecture,
~ c5_1(a1327) ).
cnf(u3433,negated_conjecture,
~ c10_2(a1307,a1308) ).
cnf(u3455,negated_conjecture,
~ c2_1(a1353) ).
cnf(u3850,negated_conjecture,
~ c7_1(a1214) ).
cnf(u3467,negated_conjecture,
~ c8_2(a1214,a1224) ).
cnf(u3471,negated_conjecture,
c4_1(a1214) ).
cnf(u3474,negated_conjecture,
~ c5_1(a1214) ).
cnf(u3485,negated_conjecture,
( c2_2(a1327,X1)
| c10_2(a1327,X1)
| c7_2(a1327,X1) ) ).
cnf(u3498,negated_conjecture,
~ c7_1(a1327) ).
cnf(u3519,negated_conjecture,
~ c10_2(a1346,a1355) ).
cnf(u3917,negated_conjecture,
~ c7_2(a1298,a1299) ).
cnf(u3581,negated_conjecture,
~ c2_1(a1298) ).
cnf(u3589,negated_conjecture,
~ c2_1(a1316) ).
cnf(u3597,negated_conjecture,
~ c10_2(a1346,a1300) ).
cnf(u3617,negated_conjecture,
~ c7_1(a1343) ).
cnf(u3691,negated_conjecture,
~ c7_1(a1210) ).
cnf(u3710,negated_conjecture,
~ c2_1(a1210) ).
cnf(u3723,negated_conjecture,
( c7_2(a1210,X0)
| c3_2(a1210,X0)
| ~ c5_2(a1210,X0) ) ).
cnf(u3726,negated_conjecture,
c6_1(a1210) ).
cnf(u3730,negated_conjecture,
( c2_2(a1210,X1)
| c10_2(a1210,X1)
| c7_2(a1210,X1) ) ).
cnf(u3764,negated_conjecture,
( ~ c5_2(a1210,X0)
| c6_2(a1210,X0)
| ~ c10_2(a1210,X0)
| c3_2(a1210,X0) ) ).
cnf(u3774,negated_conjecture,
~ c5_2(a1210,a1231) ).
cnf(u3783,negated_conjecture,
c9_2(a1220,a1300) ).
cnf(u3802,negated_conjecture,
~ c10_2(a1210,a1246) ).
cnf(u3819,negated_conjecture,
c7_1(a1220) ).
cnf(u3839,negated_conjecture,
~ c5_2(a1220,a1300) ).
cnf(u3871,negated_conjecture,
~ c1_1(a1220) ).
cnf(u3883,negated_conjecture,
~ c7_1(a1211) ).
cnf(u3941,negated_conjecture,
( ~ c4_2(a1354,X1)
| c10_2(a1354,X1)
| ~ c9_2(a1354,X1) ) ).
cnf(u3948,negated_conjecture,
( ~ c1_2(a1354,X0)
| c9_2(a1354,X0)
| ~ c10_2(a1354,X0) ) ).
cnf(u3975,negated_conjecture,
c7_1(a1363) ).
cnf(u3991,negated_conjecture,
~ c1_1(a1363) ).
cnf(u4005,negated_conjecture,
( ~ c4_2(a1343,X0)
| c9_2(a1343,X0)
| c5_2(a1343,X0) ) ).
cnf(u4027,negated_conjecture,
c8_2(a1350,a1292) ).
cnf(u4056,negated_conjecture,
ndr1_1(a1354) ).
cnf(u4073,negated_conjecture,
~ c5_2(a1346,a1347) ).
cnf(u4085,negated_conjecture,
~ c5_2(a1244,a1245) ).
cnf(u4105,negated_conjecture,
c7_1(a1244) ).
cnf(u4126,negated_conjecture,
( ~ c4_2(a1214,X0)
| c9_2(a1214,X0)
| c5_2(a1214,X0) ) ).
cnf(u4137,negated_conjecture,
c8_2(a1214,a1292) ).
cnf(u4219,negated_conjecture,
( ~ c8_2(a1214,X0)
| c5_2(a1214,X0)
| ~ c6_2(a1214,X0) ) ).
cnf(u4226,negated_conjecture,
c6_2(a1214,a1312) ).
cnf(u4230,negated_conjecture,
~ c4_2(a1214,a1312) ).
cnf(u4236,negated_conjecture,
~ c5_2(a1214,a1312) ).
cnf(u4247,negated_conjecture,
~ c6_2(a1214,a1292) ).
cnf(u4268,negated_conjecture,
c4_2(a1244,a1314) ).
cnf(u3396,negated_conjecture,
c8_1(a1343) ).
cnf(u719,negated_conjecture,
c9_0 ).
cnf(u4258,negated_conjecture,
( ~ c10_2(X0,a1318)
| c9_2(X0,a1313)
| c4_2(X0,a1314)
| ~ c7_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X1)
| c9_2(X0,X1)
| c8_2(X0,a1292)
| c1_2(X0,a1319)
| c6_2(X0,a1318) ) ).
cnf(u3448,negated_conjecture,
( ~ c10_2(X0,a1359)
| c9_2(X0,a1360)
| c3_2(X0,X1)
| c1_2(X0,X1)
| c9_2(X0,X1)
| c8_2(X0,a1292)
| c8_1(X0)
| c6_2(X0,a1359) ) ).
cnf(u3959,negated_conjecture,
~ c2_1(a1311) ).
cnf(u3205,negated_conjecture,
~ c5_2(a1226,a1227) ).
cnf(u3445,negated_conjecture,
( ~ c10_2(X0,a1359)
| c6_2(X0,a1360)
| c3_2(X0,X1)
| c1_2(X0,X1)
| c9_2(X0,X1)
| c8_2(X0,a1292)
| c8_1(X0)
| c6_2(X0,a1359) ) ).
cnf(u3824,negated_conjecture,
~ c3_1(a1220) ).
cnf(u3980,negated_conjecture,
~ c3_1(a1363) ).
cnf(u4096,negated_conjecture,
ndr1_1(a1278) ).
cnf(u4049,negated_conjecture,
( c7_2(X0,a1318)
| c1_2(X0,a1319)
| c9_2(X0,a1313)
| c4_2(X0,a1314)
| ~ c7_1(X0) ) ).
cnf(u3562,negated_conjecture,
c8_1(a1214) ).
cnf(u4048,negated_conjecture,
( c9_2(X0,a1313)
| c3_2(X0,a1318)
| c8_2(X0,a1319)
| c4_2(X0,a1314)
| ~ c7_1(X0) ) ).
cnf(u3206,negated_conjecture,
~ c8_2(a1226,a1227) ).
cnf(u3207,negated_conjecture,
ndr1_1(a1226) ).
cnf(u4116,negated_conjecture,
ndr1_1(a1214) ).
cnf(u4045,negated_conjecture,
( ~ c1_1(X40)
| ndr1_1(X40) ) ).
cnf(u4069,negated_conjecture,
( ~ c5_2(X0,a1355)
| c9_1(X0)
| c1_2(X0,a1356)
| c8_1(X0) ) ).
cnf(u3963,negated_conjecture,
~ c10_1(a1220) ).
cnf(u4095,negated_conjecture,
ndr1_1(a1269) ).
cnf(u4050,negated_conjecture,
( c9_2(X0,a1313)
| c3_2(X0,a1318)
| c1_2(X0,a1319)
| c4_2(X0,a1314)
| ~ c7_1(X0) ) ).
cnf(u317,negated_conjecture,
~ c7_0 ).
cnf(u3208,negated_conjecture,
c7_1(a1226) ).
cnf(u4047,negated_conjecture,
( c7_2(X0,a1318)
| c8_2(X0,a1319)
| c9_2(X0,a1313)
| c4_2(X0,a1314)
| ~ c7_1(X0) ) ).
cnf(u4093,negated_conjecture,
ndr1_1(a1220) ).
cnf(u688,negated_conjecture,
~ c5_0 ).
cnf(u3563,negated_conjecture,
ndr1_1(a1316) ).
cnf(u482,negated_conjecture,
c4_0 ).
cnf(u3204,negated_conjecture,
~ c6_2(a1226,a1227) ).
cnf(u4254,negated_conjecture,
( ~ c10_2(X0,a1318)
| c9_2(X0,a1313)
| c4_2(X0,a1314)
| ~ c7_1(X0)
| c3_2(X0,X1)
| c1_2(X0,X1)
| c9_2(X0,X1)
| c8_2(X0,a1292)
| c8_2(X0,a1319)
| c6_2(X0,a1318) ) ).
cnf(u3209,negated_conjecture,
~ c9_1(a1226) ).
cnf(u4070,negated_conjecture,
( ~ c5_2(X0,a1360)
| c9_1(X0)
| c8_1(X0)
| c1_2(X0,a1359) ) ).
cnf(u4046,negated_conjecture,
( ~ c4_2(X0,a1313)
| c8_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c5_2(X0,X2)
| c8_2(X0,a1313)
| c2_2(X0,X1)
| c4_2(X0,X2)
| c3_2(X0,X2)
| c4_2(X0,a1314)
| ~ c7_1(X0) ) ).
cnf(u3845,negated_conjecture,
ndr1_1(a1353) ).
cnf(u4111,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_2(X0,X1)
| ~ c7_2(X0,X1)
| c4_2(X0,a1313)
| c4_1(X0)
| c9_2(X0,a1313)
| c4_2(X0,a1314)
| ~ c7_1(X0) ) ).
cnf(u3901,negated_conjecture,
ndr1_1(a1210) ).
cnf(u3826,negated_conjecture,
ndr1_1(a1207) ).
cnf(u3825,negated_conjecture,
~ c4_1(a1220) ).
cnf(u3960,negated_conjecture,
ndr1_1(a1311) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN425+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.07/0.18 % Computer : n019.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 15:56:03 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/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
% 5.08/1.43 % (4120193)Detected formulas, will run a generic FOF schedule.
% 5.08/1.43 % (4120199)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=3494834592:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.08/1.43 % (4120203)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1473302628:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.08/1.43 % (4120200)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=1750061145:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.08/1.43 % (4120198)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=3246809746:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.08/1.43 % (4120202)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2630661136:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.08/1.43 % (4120204)dis-21_1_sil=8000:lcm=predicate:random_seed=367156773: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)
% 5.08/1.43 % (4120201)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3732138486:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.08/1.43 % (4120203)Refutation not found, incomplete strategy
% 5.08/1.43 % (4120203)------------------------------
% 5.08/1.43 % (4120203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120203)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120203)Termination reason: Refutation not found, incomplete strategy
% 5.08/1.43 % (4120203)Time elapsed: 0.036 s
% 5.08/1.43 % (4120203)Peak memory usage: 91 MB
% 5.08/1.43 % (4120203)Instructions burned: 59 (million)
% 5.08/1.43 % (4120202)Instruction limit reached!
% 5.08/1.43 % (4120202)------------------------------
% 5.08/1.43 % (4120202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120202)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120202)Termination reason: Instruction limit
% 5.08/1.43 % (4120202)Termination phase: Saturation
% 5.08/1.43 % (4120202)Time elapsed: 0.063 s
% 5.08/1.43 % (4120202)Peak memory usage: 89 MB
% 5.08/1.43 % (4120202)Instructions burned: 121 (million)
% 5.08/1.43 % (4120201)Instruction limit reached!
% 5.08/1.43 % (4120201)------------------------------
% 5.08/1.43 % (4120201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120201)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120201)Termination reason: Instruction limit
% 5.08/1.43 % (4120201)Termination phase: Saturation
% 5.08/1.43 % (4120201)Time elapsed: 0.063 s
% 5.08/1.43 % (4120201)Peak memory usage: 91 MB
% 5.08/1.43 % (4120201)Instructions burned: 111 (million)
% 5.08/1.43 % (4120204)Instruction limit reached!
% 5.08/1.43 % (4120204)------------------------------
% 5.08/1.43 % (4120204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120204)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120204)Termination reason: Instruction limit
% 5.08/1.43 % (4120204)Termination phase: Saturation
% 5.08/1.43 % (4120204)Time elapsed: 0.073 s
% 5.08/1.43 % (4120204)Peak memory usage: 91 MB
% 5.08/1.43 % (4120204)Instructions burned: 130 (million)
% 5.08/1.43 % (4120213)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2961761000:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.08/1.43 % (4120212)lrs+10_1_sil=8000:sp=occurrence:random_seed=1697370576:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.08/1.43 % (4120214)lrs+1011_1_sil=32000:sp=occurrence:random_seed=138967406:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.08/1.43 % (4120213)Refutation not found, incomplete strategy
% 5.08/1.43 % (4120213)------------------------------
% 5.08/1.43 % (4120213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120213)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120213)Termination reason: Refutation not found, incomplete strategy
% 5.08/1.43 % (4120213)Time elapsed: 0.024 s
% 5.08/1.43 % (4120213)Peak memory usage: 90 MB
% 5.08/1.43 % (4120213)Instructions burned: 38 (million)
% 5.08/1.43 % (4120214)Refutation not found, incomplete strategy
% 5.08/1.43 % (4120214)------------------------------
% 5.08/1.43 % (4120214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120214)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120214)Termination reason: Refutation not found, incomplete strategy
% 5.08/1.43 % (4120214)Time elapsed: 0.025 s
% 5.08/1.43 % (4120214)Peak memory usage: 90 MB
% 5.08/1.43 % (4120214)Instructions burned: 38 (million)
% 5.08/1.43 % (4120203)------------------------------
% 5.08/1.43 % (4120203)------------------------------
% 5.08/1.43 % (4120212)Instruction limit reached!
% 5.08/1.43 % (4120212)------------------------------
% 5.08/1.43 % (4120212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120212)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120212)Termination reason: Instruction limit
% 5.08/1.43 % (4120212)Termination phase: Saturation
% 5.08/1.43 % (4120212)Time elapsed: 0.149 s
% 5.08/1.43 % (4120212)Peak memory usage: 93 MB
% 5.08/1.43 % (4120212)Instructions burned: 286 (million)
% 5.08/1.43 % (4120199)First to succeed.
% 5.08/1.43 % (4120199)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4120193"
% 5.08/1.43 % (4120218)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=463309026:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.08/1.43 % (4120218)Refutation not found, incomplete strategy
% 5.08/1.43 % (4120218)------------------------------
% 5.08/1.43 % (4120218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.08/1.43 % (4120218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.08/1.43 % (4120218)CaDiCaL version: 2.1.3
% 5.08/1.43 % (4120218)Termination reason: Refutation not found, incomplete strategy
% 5.08/1.43 % (4120218)Time elapsed: 0.026 s
% 5.08/1.43 % (4120218)Peak memory usage: 91 MB
% 5.08/1.43 % (4120218)Instructions burned: 39 (million)
% 5.08/1.43 % (4120214)------------------------------
% 5.08/1.43 % (4120214)------------------------------
% 5.08/1.43 % (4120213)------------------------------
% 5.08/1.43 % (4120213)------------------------------
% 5.08/1.43 % (4120219)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1306467926:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.08/1.43 % SZS status CounterSatisfiable for theBenchmark
% 5.08/1.43 % SZS output start Saturation.
% See solution above
% 5.08/1.43 % SZS output start Definitions and Model Updates.
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c5_2(X0,a1280) | c1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~c5_2(X0,a1280) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c5_2(X0,a1279) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~c5_2(X0,a1279) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c8_1(X0) | ndr1_1(X0) | ~c5_2(X0,a1356) | ~ndr1_0 | ~sP1 is false, set ~c5_2(X0,a1356) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c10_0 | ndr1_1(X131) | ~c7_1(X131) | ~c5_2(X131,a1314) | ~ndr1_0 | c6_0 is false, set ~c5_2(X131,a1314) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c10_0 | ~c3_2(X131,a1313) | ~c7_1(X131) | ndr1_1(X131) | ~ndr1_0 | c6_0 is false, set ~c3_2(X131,a1313) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_2(X0,a1233) | ~c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set ~c3_2(X0,a1233) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_1(X0) | ~c3_2(X0,a1266) | ndr1_1(X0) | ~ndr1_0 | ~sP14 is false, set ~c3_2(X0,a1266) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c7_2(X0,a1279) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~c7_2(X0,a1279) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c8_1(X0) | ndr1_1(X0) | c1_2(X0,a1356) | ~ndr1_0 | ~sP1 is false, set c1_2(X0,a1356) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c1_2(X0,a1359) | ndr1_1(X0) | c8_1(X0) | ~ndr1_0 | ~sP0 is false, set c1_2(X0,a1359) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c10_0 | c1_2(X131,a1313) | ~c7_1(X131) | ndr1_1(X131) | ~ndr1_0 | c6_0 is false, set c1_2(X131,a1313) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c1_2(X0,a1344) | ndr1_1(X0) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set c1_2(X0,a1344) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c8_1(X0) | ~c4_2(X0,a1355) | ndr1_1(X0) | ~ndr1_0 | ~sP1 is false, set ~c4_2(X0,a1355) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c8_1(X0) | ndr1_1(X0) | ~c4_2(X0,a1356) | ~ndr1_0 | ~sP1 is false, set ~c4_2(X0,a1356) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c4_2(a1287,X99) | c1_2(a1287,X99) | ~ndr1_1(a1287) | ndr1_0 | c10_0 is false, set ~c4_2(a1287,X99) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c4_2(X0,a1345) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set ~c4_2(X0,a1345) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c4_2(X0,a1222) | c6_1(X0) | ~ndr1_0 | ~sP20 is false, set ~c4_2(X0,a1222) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c4_2(X0,a1359) | ndr1_1(X0) | c8_1(X0) | ~ndr1_0 | ~sP0 is false, set ~c4_2(X0,a1359) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_1(X0) | c8_2(X0,a1266) | ndr1_1(X0) | ~ndr1_0 | ~sP14 is false, set c8_2(X0,a1266) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c8_2(X162,a1351) | c2_1(X162) | ndr1_1(X162) | ~ndr1_0 is false, set c8_2(X162,a1351) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c5_1(X0) | c4_2(X0,a1234) | ~ndr1_0 | ~sP18 is false, set c4_2(X0,a1234) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c4_2(X0,a1221) | ndr1_1(X0) | c6_1(X0) | ~ndr1_0 | ~sP20 is false, set c4_2(X0,a1221) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | c4_2(X0,a1280) | c1_1(X0) | ~ndr1_0 | ~sP12 is false, set c4_2(X0,a1280) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c10_0 | ndr1_1(X131) | ~c7_1(X131) | c4_2(X131,a1314) | ~ndr1_0 | c6_0 is false, set c4_2(X131,a1314) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c4_2(X0,a1344) | ndr1_1(X0) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set c4_2(X0,a1344) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | ~c2_0 | ~c8_1(a1316) is false, set ~c8_1(a1316) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c8_1(a1207) | ~c2_0 | ndr1_0 is false, set ~c8_1(a1207) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | c9_2(X0,a1360) | c8_1(X0) | ~ndr1_0 | ~sP0 is false, set c9_2(X0,a1360) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c9_2(X0,a1233) | ~c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set c9_2(X0,a1233) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c9_2(X0,a1344) | ndr1_1(X0) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set c9_2(X0,a1344) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c8_1(X0) | c9_2(X0,a1355) | ndr1_1(X0) | ~ndr1_0 | ~sP1 is false, set c9_2(X0,a1355) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c8_2(X0,a1221) | ndr1_1(X0) | c6_1(X0) | ~ndr1_0 | ~sP20 is false, set ~c8_2(X0,a1221) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c8_2(X0,a1325) | ~c2_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c8_2(X0,a1325) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X162) | c2_1(X162) | ~c8_2(X162,a1352) | ~ndr1_0 is false, set ~c8_2(X162,a1352) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c2_1(X0) | ~c9_2(X0,a1326) | ~ndr1_0 | ~sP6 is false, set ~c9_2(X0,a1326) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c2_1(X0) | ~c1_2(X0,a1326) | ~ndr1_0 | ~sP6 is false, set ~c1_2(X0,a1326) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c1_2(X0,a1325) | ~c2_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c1_2(X0,a1325) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | ~c2_0 | ~c10_2(a1208,X20) | ~c4_2(a1208,X20) | ~ndr1_1(a1208) is false, set ~c10_2(a1208,X20) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_0 | ndr1_0 | ~c9_2(a1241,X56) | ~c10_2(a1241,X56) | ~ndr1_1(a1241) is false, set ~c10_2(a1241,X56) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c6_2(a1207,X19) | c8_2(a1207,X19) | ~c4_2(a1207,X19) | ~ndr1_1(a1207) | ~c2_0 | ndr1_0 is false, set ~c6_2(a1207,X19) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c7_2(a1287,X100) | ~c6_2(a1287,X100) | ~c1_2(a1287,X100) | ~ndr1_1(a1287) | ndr1_0 | c10_0 is false, set ~c6_2(a1287,X100) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c5_2(a1315,X133) | ~c6_2(a1315,X133) | ~c9_2(a1315,X133) | ~ndr1_1(a1315) | ~c2_0 | ndr1_0 is false, set ~c6_2(a1315,X133) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c10_2(X0,a1325) | ~c2_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP6 is false, set ~c10_2(X0,a1325) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c5_1(X0) | ~c10_2(X0,a1234) | ~ndr1_0 | ~sP18 is false, set ~c10_2(X0,a1234) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c10_2(X0,a1360) | c8_1(X0) | ~ndr1_0 | ~sP0 is false, set ~c10_2(X0,a1360) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_0 | c6_2(a1240,X53) | c4_2(a1240,X53) | c5_2(a1240,X53) | ~ndr1_1(a1240) | ndr1_0 is false, set c6_2(a1240,X53) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c8_1(X0) | c6_2(X0,a1355) | ndr1_1(X0) | ~ndr1_0 | ~sP1 is false, set c6_2(X0,a1355) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | c6_2(X0,a1360) | c8_1(X0) | ~ndr1_0 | ~sP0 is false, set c6_2(X0,a1360) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_2(X0,a1221) | ndr1_1(X0) | c6_1(X0) | ~ndr1_0 | ~sP20 is false, set c10_2(X0,a1221) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_2(X0,a1233) | ~c5_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP18 is false, set c10_2(X0,a1233) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_2(X162,a1351) | c2_1(X162) | ndr1_1(X162) | ~ndr1_0 is false, set c10_2(X162,a1351) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c10_0 | ndr1_1(X131) | ~c7_1(X131) | c10_2(X131,a1314) | ~ndr1_0 | c6_0 is false, set c10_2(X131,a1314) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X162) | c2_1(X162) | c10_2(X162,a1352) | ~ndr1_0 is false, set c10_2(X162,a1352) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c2_1(X0) | c2_2(X0,a1326) | ~ndr1_0 | ~sP6 is false, set c2_2(X0,a1326) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | c2_2(X0,a1222) | c6_1(X0) | ~ndr1_0 | ~sP20 is false, set c2_2(X0,a1222) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_1(X0) | ndr1_1(X0) | c3_2(X0,a1267) | ~ndr1_0 | ~sP14 is false, set c3_2(X0,a1267) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_0 | ~c5_2(a1240,X54) | c3_2(a1240,X54) | c4_2(a1240,X54) | ~ndr1_1(a1240) | ndr1_0 is false, set c3_2(a1240,X54) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | c3_2(a1288,X101) | ~c1_2(a1288,X101) | c8_2(a1288,X101) | ~ndr1_1(a1288) | c10_0 is false, set c3_2(a1288,X101) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c3_2(X162,a1351) | c2_1(X162) | ndr1_1(X162) | ~ndr1_0 is false, set c3_2(X162,a1351) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | c5_2(X0,a1222) | c6_1(X0) | ~ndr1_0 | ~sP20 is false, set c5_2(X0,a1222) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_1(X0) | ndr1_1(X0) | c5_2(X0,a1267) | ~ndr1_0 | ~sP14 is false, set c5_2(X0,a1267) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_1(X0) | c5_2(X0,a1266) | ndr1_1(X0) | ~ndr1_0 | ~sP14 is false, set c5_2(X0,a1266) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | c5_2(X0,a1345) | c3_1(X0) | ~ndr1_0 | ~sP3 is false, set c5_2(X0,a1345) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | ~c8_2(a1288,X102) | c4_2(a1288,X102) | c5_2(a1288,X102) | ~ndr1_1(a1288) | c10_0 is false, set c5_2(a1288,X102) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c5_2(a1353,X163) | c3_2(a1353,X163) | c2_2(a1353,X163) | ~ndr1_1(a1353) | ndr1_0 is false, set c5_2(a1353,X163) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c10_1(X0) | ndr1_1(X0) | ~c2_2(X0,a1267) | ~ndr1_0 | ~sP14 is false, set ~c2_2(X0,a1267) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X162) | c2_1(X162) | ~c2_2(X162,a1352) | ~ndr1_0 is false, set ~c2_2(X162,a1352) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c2_2(X0,a1279) | ndr1_1(X0) | c1_1(X0) | ~ndr1_0 | ~sP12 is false, set ~c2_2(X0,a1279) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | c1_2(a1288,X103) | c3_2(a1288,X103) | ~c2_2(a1288,X103) | ~ndr1_1(a1288) | c10_0 is false, set ~c2_2(a1288,X103) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c10_0 | ~c2_2(X131,a1313) | ~c7_1(X131) | ndr1_1(X131) | ~ndr1_0 | c6_0 is false, set ~c2_2(X131,a1313) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c8_2(a1315,X132) | ~c2_2(a1315,X132) | ~ndr1_1(a1315) | ~c2_0 | ndr1_0 is false, set ~c2_2(a1315,X132) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_1(a1353) | ndr1_0 is false, set ~c3_1(a1353) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_0 | ndr1_0 | ~c3_1(a1241) is false, set ~c3_1(a1241) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | ~c2_0 | ~c5_1(a1316) is false, set ~c5_1(a1316) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c5_1(a1353) | ndr1_0 is false, set ~c5_1(a1353) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c3_1(a1287) | ndr1_0 | c10_0 is false, set c3_1(a1287) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c8_0 | ~c8_2(X93,X94) | c5_2(X93,X94) | ~c6_2(X93,X94) | ~ndr1_1(X93) | ~c4_2(X93,X95) | ~c9_2(X93,X95) | c10_2(X93,X95) | ~ndr1_1(X93) | ~c4_1(X93) | ~ndr1_0 | ndr1_0 is false, set ~c4_1(X93) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c5_2(X78,X79) | c3_2(X78,X79) | c4_2(X78,X79) | ~ndr1_1(X78) | ~c4_2(X78,X80) | c8_2(X78,X80) | ~c1_2(X78,X80) | ~ndr1_1(X78) | ~c4_2(X78,X81) | c8_2(X78,X81) | c2_2(X78,X81) | ~ndr1_1(X78) | ~ndr1_0 | c7_0 | ndr1_0 is false, set c7_0 to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c9_2(X129,X130) | ~c1_2(X129,X130) | ~c10_2(X129,X130) | ~ndr1_1(X129) | ~c4_1(X129) | ndr1_1(X129) | ~ndr1_0 | c8_0 | ~c2_0 is false, set c8_0 to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | c4_1(a1354) is false, set c4_1(a1354) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | ~c7_1(X113) | ~c8_1(X113) | ~c10_1(X113) | ~ndr1_0 | c6_0 is false, set ~c7_1(X113) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_0 | ~c7_1(a1240) | ndr1_0 is false, set ~c7_1(a1240) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_0 | ~c7_1(a1354) is false, set ~c7_1(a1354) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ~c3_0 | ndr1_0 | c6_2(a1241,X55) | ~c8_2(a1241,X55) | c7_2(a1241,X55) | ~ndr1_1(a1241) is false, set c7_2(a1241,X55) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever c7_2(X0,a1359) | ndr1_1(X0) | c8_1(X0) | ~ndr1_0 | ~sP0 is false, set c7_2(X0,a1359) to true
% 5.08/1.43 for all groundings,
% 5.08/1.43 whenever ndr1_1(X0) | ~c5_1(X0) | c7_2(X0,a1234) | ~ndr1_0 | ~sP18 is false, set c7_2(X0,a1234) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c8_1(X166) | ndr1_1(X166) | c9_2(X166,X167) | c5_2(X166,X167) | ~c4_2(X166,X167) | ~ndr1_1(X166) | ~ndr1_0 | c10_0 | ~c8_0 is false, set c10_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c8_2(X109,X110) | ~c1_2(X109,X110) | ~c9_2(X109,X110) | ~ndr1_1(X109) | ndr1_1(X109) | ~ndr1_0 | c1_1(X111) | ~c4_1(X111) | ndr1_1(X111) | ~ndr1_0 is false, set c1_1(X111) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c8_2(X109,X110) | ~c1_2(X109,X110) | ~c9_2(X109,X110) | ~ndr1_1(X109) | ndr1_1(X109) | ~ndr1_0 | c1_1(X111) | ~c4_1(X111) | ~c9_2(X111,a1302) | ~ndr1_0 is false, set c1_1(X111) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c8_2(X109,X110) | ~c1_2(X109,X110) | ~c9_2(X109,X110) | ~ndr1_1(X109) | ndr1_1(X109) | ~ndr1_0 | c1_1(X111) | ~c4_1(X111) | ~c1_2(X111,a1302) | ~ndr1_0 is false, set c1_1(X111) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c10_1(a1315) | ~c2_0 | ndr1_0 is false, set c10_1(a1315) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | ~c2_0 | c10_1(a1208) is false, set c10_1(a1208) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c6_0 | ndr1_0 | c9_1(X14) | c1_1(X14) | c6_2(X14,X15) | ~c2_2(X14,X15) | c4_2(X14,X15) | ~ndr1_1(X14) | ~ndr1_0 is false, set c9_1(X14) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | ~c2_0 | c9_1(a1208) is false, set c9_1(a1208) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c9_1(a1207) | ~c2_0 | ndr1_0 is false, set c9_1(a1207) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c2_1(X30) | c4_1(X30) | c5_1(X30) | ~ndr1_0 | c7_0 | ndr1_0 is false, set ~c2_1(X30) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | ndr1_0 | c3_2(X69,X70) | c5_2(X69,X70) | c7_2(X69,X70) | ~ndr1_1(X69) | c10_2(X69,X71) | ~c3_2(X69,X71) | c7_2(X69,X71) | ~ndr1_1(X69) | ~c2_1(X69) | ~ndr1_0 is false, set ~c2_1(X69) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | c8_2(a1250,X68) | ~c7_2(a1250,X68) | c5_2(a1250,X68) | ~ndr1_1(a1250) | c3_2(X69,X70) | c5_2(X69,X70) | c7_2(X69,X70) | ~ndr1_1(X69) | c10_2(X69,X71) | ~c3_2(X69,X71) | c7_2(X69,X71) | ~ndr1_1(X69) | ~c2_1(X69) | ~ndr1_0 is false, set ~c2_1(X69) to true
% 6.01/1.62 for all groundings, until fixed point,
% 6.01/1.62 whenever ndr1_0 | c2_1(a1250) | c3_2(X69,X70) | c5_2(X69,X70) | c7_2(X69,X70) | ~ndr1_1(X69) | c10_2(X69,X71) | ~c3_2(X69,X71) | c7_2(X69,X71) | ~ndr1_1(X69) | ~c2_1(X69) | ~ndr1_0 is false, set ~c2_1(X69) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c3_2(a1249,X67) | c6_2(a1249,X67) | c5_2(a1249,X67) | ~ndr1_1(a1249) | ndr1_0 | c3_2(X69,X70) | c5_2(X69,X70) | c7_2(X69,X70) | ~ndr1_1(X69) | c10_2(X69,X71) | ~c3_2(X69,X71) | c7_2(X69,X71) | ~ndr1_1(X69) | ~c2_1(X69) | ~ndr1_0 is false, set ~c2_1(X69) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c4_1(a1249) | ndr1_0 | c3_2(X69,X70) | c5_2(X69,X70) | c7_2(X69,X70) | ~ndr1_1(X69) | c10_2(X69,X71) | ~c3_2(X69,X71) | c7_2(X69,X71) | ~ndr1_1(X69) | ~c2_1(X69) | ~ndr1_0 is false, set ~c2_1(X69) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c1_1(a1249) | ndr1_0 | c3_2(X69,X70) | c5_2(X69,X70) | c7_2(X69,X70) | ~ndr1_1(X69) | c10_2(X69,X71) | ~c3_2(X69,X71) | c7_2(X69,X71) | ~ndr1_1(X69) | ~c2_1(X69) | ~ndr1_0 is false, set ~c2_1(X69) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | ~c3_1(X52) | c8_1(X52) | ~ndr1_0 | c8_0 is false, set c8_1(X52) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_1(X89) | ~c9_1(X89) | c8_1(X89) | ~ndr1_0 | ~c2_0 | ndr1_0 is false, set c8_1(X89) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c7_2(X89,a1268) | ~c9_1(X89) | c8_1(X89) | ~ndr1_0 | ~c2_0 | ndr1_0 is false, set c8_1(X89) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c9_2(X89,a1268) | ~c9_1(X89) | c8_1(X89) | ~ndr1_0 | ~c2_0 | ndr1_0 is false, set c8_1(X89) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c8_2(X89,a1268) | ~c9_1(X89) | c8_1(X89) | ~ndr1_0 | ~c2_0 | ndr1_0 is false, set c8_1(X89) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c3_1(X119) | ndr1_1(X119) | c8_1(X119) | ~ndr1_0 | c2_0 | ndr1_0 is false, set c8_1(X119) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c3_1(X119) | c1_2(X119,a1310) | c8_1(X119) | ~ndr1_0 | c2_0 | ndr1_0 is false, set c8_1(X119) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c3_1(X119) | ~c2_2(X119,a1310) | c8_1(X119) | ~ndr1_0 | c2_0 | ndr1_0 is false, set c8_1(X119) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c3_1(X119) | ~c3_2(X119,a1310) | c8_1(X119) | ~ndr1_0 | c2_0 | ndr1_0 is false, set c8_1(X119) to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c7_2(X147,X148) | ~c6_2(X147,X148) | c1_2(X147,X148) | ~ndr1_1(X147) | ndr1_1(X147) | c6_2(X147,X149) | c5_2(X147,X149) | ~ndr1_1(X147) | ~ndr1_0 | ~c7_0 is false, set ~c7_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c1_0 | ~c10_1(X141) | c10_2(X141,X142) | c2_2(X141,X142) | c7_2(X141,X142) | ~ndr1_1(X141) | ~c5_2(X141,X143) | c3_2(X141,X143) | c1_2(X141,X143) | ~ndr1_1(X141) | ~ndr1_0 | c2_2(X144,X145) | ~c8_2(X144,X145) | c5_2(X144,X145) | ~ndr1_1(X144) | ~c2_1(X144) | ndr1_1(X144) | ~ndr1_0 is false, set ~c1_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever sP0 | ndr1_0 | ~c10_0 is false, set sP0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c8_0 | sP1 | ndr1_0 is false, set sP1 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c2_1(X137) | c7_1(X137) | c3_2(X137,X138) | c6_2(X137,X138) | c8_2(X137,X138) | ~ndr1_1(X137) | ~ndr1_0 | ndr1_0 | sP6 is false, set sP6 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | c4_0 | sP14 is false, set sP14 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever sP18 | ndr1_0 | c1_0 is false, set sP18 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever sP20 | ndr1_0 | c6_0 is false, set sP20 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | sP12 | sP13 is false, set sP12 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever sP4 | ndr1_0 | sP3 is false, set sP3 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | ~sP2 is false, set ~sP2 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c7_1(X85) | c10_1(X85) | ~c3_1(X85) | ~ndr1_0 | c1_0 | ndr1_0 is false, set c1_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c9_0 | ndr1_1(X24) | c7_2(X24,X25) | ~c1_2(X24,X25) | c9_2(X24,X25) | ~ndr1_1(X24) | c5_1(X24) | ~ndr1_0 | ~c6_0 is false, set c9_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c4_2(X5,a1196) | c5_2(X5,X6) | ~c9_2(X5,X6) | c7_2(X5,X6) | ~ndr1_1(X5) | ndr1_1(X5) | ~ndr1_0 | c4_0 | c3_0 is false, set c4_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ~c6_2(X5,a1196) | c5_2(X5,X6) | ~c9_2(X5,X6) | c7_2(X5,X6) | ~ndr1_1(X5) | ndr1_1(X5) | ~ndr1_0 | c4_0 | c3_0 is false, set c4_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_0 | c2_2(X8,X9) | ~c9_2(X8,X9) | c7_2(X8,X9) | ~ndr1_1(X8) | c8_1(X8) | c5_1(X8) | ~ndr1_0 | c4_0 is false, set c4_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c4_0 | c1_1(X37) | ndr1_1(X37) | ~c6_2(X37,X38) | c4_2(X37,X38) | ~ndr1_1(X37) | ~ndr1_0 | c9_0 is false, set c4_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever c8_2(X5,a1196) | c5_2(X5,X6) | ~c9_2(X5,X6) | c7_2(X5,X6) | ~ndr1_1(X5) | ndr1_1(X5) | ~ndr1_0 | c4_0 | c3_0 is false, set c4_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_1(X5) | c5_2(X5,X6) | ~c9_2(X5,X6) | c7_2(X5,X6) | ~ndr1_1(X5) | ~c4_2(X5,a1197) | ~ndr1_0 | c4_0 | c3_0 is false, set c4_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_1(X5) | c5_2(X5,X6) | ~c9_2(X5,X6) | c7_2(X5,X6) | ~ndr1_1(X5) | ~c10_2(X5,a1197) | ~ndr1_0 | c4_0 | c3_0 is false, set c4_0 to true
% 6.01/1.62 for all groundings,
% 6.01/1.62 whenever ndr1_1(X5) | c5_2(X5,X6) | ~c9_2(X5,X6) | c7_2(X5,X6) | ~ndr1_1(X5) | c6_2(X5,a1197) | ~ndr1_0 | c4_0 | c3_0 is false, set c4_0 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_1(X5) | c5_2(X5,X6) | ~c9_2(X5,X6) | c7_2(X5,X6) | ~ndr1_1(X5) | ndr1_1(X5) | ~ndr1_0 | c4_0 | c3_0 is false, set c4_0 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c7_2(X104,X105) | c6_2(X104,X105) | ~c10_2(X104,X105) | ~ndr1_1(X104) | ndr1_1(X104) | c9_2(X104,X106) | c1_2(X104,X106) | c3_2(X104,X106) | ~ndr1_1(X104) | ~ndr1_0 | sP10 is false, set sP10 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever sP19 | ndr1_1(X46) | ~c5_1(X46) | ~c3_2(X46,X47) | ~c5_2(X46,X47) | c9_2(X46,X47) | ~ndr1_1(X46) | ~ndr1_0 is false, set sP19 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c6_0 | ~c1_2(X90,X91) | c10_2(X90,X91) | c7_2(X90,X91) | ~ndr1_1(X90) | c6_1(X90) | c10_1(X90) | ~ndr1_0 | ndr1_0 is false, set c6_1(X90) to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever c7_0 | ~c10_1(X115) | c7_2(X115,X116) | ~c5_2(X115,X116) | c3_2(X115,X116) | ~ndr1_1(X115) | c6_1(X115) | ~ndr1_0 | ndr1_1(X117) | ~c2_1(X117) | c10_2(X117,X118) | c3_2(X117,X118) | ~c6_2(X117,X118) | ~ndr1_1(X117) | ~ndr1_0 is false, set c6_1(X115) to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c2_0 | c3_0 | ~c1_2(X151,X152) | ~c2_2(X151,X152) | ~c7_2(X151,X152) | ~ndr1_1(X151) | ndr1_1(X151) | c6_1(X151) | ~ndr1_0 is false, set c6_1(X151) to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c1_2(X159,X160) | c4_2(X159,X160) | c3_2(X159,X160) | ~ndr1_1(X159) | c5_1(X159) | ndr1_1(X159) | ~ndr1_0 | sP2 | ~c10_1(a1350) is false, set sP2 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c1_2(X159,X160) | c4_2(X159,X160) | c3_2(X159,X160) | ~ndr1_1(X159) | c5_1(X159) | c4_2(X159,a1348) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c1_2(X159,X160) | c4_2(X159,X160) | c3_2(X159,X160) | ~ndr1_1(X159) | c5_1(X159) | ~c8_2(X159,a1348) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_0 | ~sP10 is false, set ~sP10 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_0 | ~sP9 is false, set ~sP9 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_0 | ~sP16 is false, set ~sP16 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c1_2(X159,X160) | c4_2(X159,X160) | c3_2(X159,X160) | ~ndr1_1(X159) | c5_1(X159) | ndr1_1(X159) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c1_2(X159,X160) | c4_2(X159,X160) | c3_2(X159,X160) | ~ndr1_1(X159) | c5_1(X159) | ndr1_1(X159) | ~ndr1_0 | sP2 | c1_2(a1350,X161) | c7_2(a1350,X161) | c6_2(a1350,X161) | ~ndr1_1(a1350) is false, set sP2 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c1_2(X159,X160) | c4_2(X159,X160) | c3_2(X159,X160) | ~ndr1_1(X159) | c5_1(X159) | c5_2(X159,a1348) | ~ndr1_0 | sP2 | ndr1_0 is false, set sP2 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_0 | ~sP17 is false, set ~sP17 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_0 | ~sP22 is false, set ~sP22 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_0 | ~sP19 is false, set ~sP19 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever c3_2(X0,a1318) | c9_2(X0,X1) | c3_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever c7_2(X0,a1318) | c9_2(X0,X1) | c3_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ~c8_2(X0,a1318) | c9_2(X0,X1) | c3_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_1(X0) | c9_2(X0,X1) | c3_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | c8_2(X0,a1319) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_1(X0) | c9_2(X0,X1) | c3_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | c1_2(X0,a1319) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_1(X0) | c9_2(X0,X1) | c3_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ~c6_2(X0,a1319) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 6.01/1.63 for all groundings,
% 6.01/1.63 whenever ndr1_1(X0) | c9_2(X0,X1) | c3_2(X0,X1) | ~c1_2(X0,X1) | ~ndr1_1(X0) | ndr1_1(X0) | ~ndr1_0 | ~sP7 is false, set ~sP7 to true
% 6.01/1.63 % SZS output end Definitions and Model Updates.
% 6.01/1.63 % (4120199)------------------------------
% 6.01/1.63 % (4120199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.63 % (4120199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.63 % (4120199)CaDiCaL version: 2.1.3
% 6.01/1.63 % (4120199)Termination reason: Satisfiable
% 6.01/1.63 % (4120199)Time elapsed: 0.467 s
% 6.01/1.63 % (4120199)Peak memory usage: 135 MB
% 6.01/1.63 % (4120199)Instructions burned: 1276 (million)
% 6.01/1.63 % (4120199)------------------------------
% 6.01/1.63 % (4120199)------------------------------
% 6.01/1.63 % (4120193)Success in time 0.77 s
% 6.01/1.63 % Vampire exiting
%------------------------------------------------------------------------------