%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN427-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 : n014.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:36 PM UTC 2026
% Result : Satisfiable 4.14s 1.23s
% Output : Saturation 4.63s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u768,negated_conjecture,
c9_0 ).
cnf(u779,negated_conjecture,
ndr1_0 ).
cnf(u783,negated_conjecture,
( ~ c2_2(X0,X2)
| c5_2(X0,X2)
| c5_2(X0,X1)
| ~ c8_1(X0)
| ~ c8_2(X0,X1)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u787,negated_conjecture,
~ c1_0 ).
cnf(u794,negated_conjecture,
( ~ c10_2(X0,X2)
| c4_1(X0)
| c6_2(X0,X2)
| c7_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u801,negated_conjecture,
( ~ c7_2(X1,X2)
| c3_1(X1)
| c3_2(X1,X2)
| ~ c8_1(X1)
| ~ ndr1_1(X1)
| ~ c9_2(X1,X2) ) ).
cnf(u812,negated_conjecture,
~ c4_0 ).
cnf(u819,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_1(X0)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u842,negated_conjecture,
( ~ c6_2(X1,X2)
| c2_1(X1)
| c1_2(X1,X2)
| ~ ndr1_1(X1)
| ~ c7_2(X1,X2) ) ).
cnf(u852,negated_conjecture,
( ~ c1_1(X3)
| ~ c3_1(X3)
| ~ c6_1(X3) ) ).
cnf(u867,negated_conjecture,
( c2_1(X4)
| ndr1_1(X4)
| c6_1(X4) ) ).
cnf(u883,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_1(X0)
| c7_2(X0,X1)
| c5_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u897,negated_conjecture,
ndr1_1(a1691) ).
cnf(u901,negated_conjecture,
( ~ c7_2(a1691,X2)
| ~ c5_2(a1691,X2)
| ~ c9_2(a1691,X2) ) ).
cnf(u915,negated_conjecture,
c2_0 ).
cnf(u940,negated_conjecture,
c5_0 ).
cnf(u947,negated_conjecture,
( ~ c5_2(X0,X1)
| c7_1(X0)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u980,negated_conjecture,
~ ssSkC8 ).
cnf(u984,negated_conjecture,
( ~ c10_2(X0,a1608)
| c5_2(X0,X2)
| c3_2(X0,X1)
| c6_2(X0,X1)
| ~ c10_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u989,negated_conjecture,
c3_0 ).
cnf(u1003,negated_conjecture,
( ~ c10_2(X0,X1)
| c5_2(X0,a1608)
| c5_2(X0,X2)
| c3_2(X0,X1)
| c6_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1007,negated_conjecture,
( ~ c10_2(X0,X1)
| c7_2(X0,a1608)
| c5_2(X0,X2)
| c3_2(X0,X1)
| c6_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1022,negated_conjecture,
~ ssSkC26 ).
cnf(u1038,negated_conjecture,
~ ssSkC45 ).
cnf(u1042,negated_conjecture,
( ~ c2_2(X0,X2)
| c9_2(X0,X2)
| c10_2(X0,X2)
| ~ c6_2(X0,a1772)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1046,negated_conjecture,
( ~ c2_2(X0,a1772)
| c9_2(X0,X2)
| c10_2(X0,X2)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1050,negated_conjecture,
~ c8_0 ).
cnf(u1054,negated_conjecture,
( ~ c7_2(X0,X2)
| c5_2(X0,X2)
| c10_2(X0,X2)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ c9_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1058,negated_conjecture,
c10_0 ).
cnf(u1069,negated_conjecture,
( ~ c6_1(X0)
| c2_1(X0)
| c4_1(X0) ) ).
cnf(u1080,negated_conjecture,
( ~ c6_1(X0)
| c9_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1099,negated_conjecture,
~ ssSkC44 ).
cnf(u1103,negated_conjecture,
( ~ c6_2(X0,X2)
| c4_2(X0,X2)
| c9_2(X0,X2)
| c10_2(X0,X1)
| ~ c8_2(X0,a1761)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1107,negated_conjecture,
( ~ c6_2(X0,X2)
| c4_2(X0,X2)
| c9_2(X0,X2)
| c10_2(X0,X1)
| ~ c3_2(X0,a1761)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1111,negated_conjecture,
( ~ c2_2(X0,X2)
| c3_2(X0,a1772)
| c9_2(X0,X2)
| c10_2(X0,X2)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1119,negated_conjecture,
( ~ c1_2(X0,X1)
| c10_1(X0)
| c5_1(X0)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1128,negated_conjecture,
( ~ c6_2(X0,X1)
| c1_2(X0,X1)
| ~ c9_2(X0,a1765)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ ssSkP9(X0) ) ).
cnf(u1132,negated_conjecture,
( ~ c6_2(X0,X1)
| c1_2(X0,X1)
| ~ c4_2(X0,a1765)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ ssSkP9(X0) ) ).
cnf(u1136,negated_conjecture,
( ~ c6_2(X0,X1)
| c1_2(X0,X1)
| ~ c3_2(X0,a1765)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ ssSkP9(X0) ) ).
cnf(u1148,negated_conjecture,
( ~ c6_2(X0,X2)
| c5_2(X0,a1761)
| c4_2(X0,X2)
| c9_2(X0,X2)
| c10_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1157,negated_conjecture,
~ c6_0 ).
cnf(u1174,negated_conjecture,
( ~ c10_2(X0,a1717)
| c3_2(X0,X1)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1177,negated_conjecture,
ssSkC31 ).
cnf(u1182,negated_conjecture,
( ~ c10_2(X0,X1)
| c3_2(X0,X1)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ c9_2(X0,a1717)
| ~ ndr1_1(X0) ) ).
cnf(u1190,negated_conjecture,
( ~ c10_2(X0,a1751)
| c5_2(X0,X1)
| c2_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1194,negated_conjecture,
( ~ c1_2(X0,a1751)
| c5_2(X0,X1)
| c2_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1198,negated_conjecture,
~ ssSkC6 ).
cnf(u1202,negated_conjecture,
( ~ c7_2(X0,X1)
| c3_2(X0,X1)
| ~ c8_1(X0)
| ~ c4_2(X0,a1602)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1206,negated_conjecture,
~ ssSkC42 ).
cnf(u1210,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_1(X0)
| ~ c4_2(X0,a1753)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1214,negated_conjecture,
c7_0 ).
cnf(u1218,negated_conjecture,
( ~ c6_2(X0,X1)
| c10_2(X0,X1)
| c7_2(X0,X1)
| ~ c2_1(X0)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1235,negated_conjecture,
( ~ c3_1(X0)
| c7_2(X0,a1751)
| c5_2(X0,X1)
| c2_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1239,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_2(X0,a1780)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1243,negated_conjecture,
( ~ c2_2(X0,X1)
| c7_2(X0,a1780)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1247,negated_conjecture,
( ~ c2_2(X0,X1)
| c6_2(X0,a1780)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1254,negated_conjecture,
ssSkC58 ).
cnf(u1263,negated_conjecture,
( ~ c7_2(X0,X1)
| c2_2(X0,a1602)
| c3_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1267,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_1(X0)
| c6_2(X0,a1753)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1271,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_1(X0)
| c8_2(X0,a1753)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1275,negated_conjecture,
~ ssSkC49 ).
cnf(u1279,negated_conjecture,
( ~ c1_2(X0,a1792)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c8_2(X0,X1) ) ).
cnf(u1287,negated_conjecture,
~ ssSkC12 ).
cnf(u1291,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_1(X0)
| c3_2(X0,X1)
| c10_2(X0,X1)
| ~ c5_2(X0,a1625)
| ~ ndr1_1(X0) ) ).
cnf(u1295,negated_conjecture,
~ ssSkC34 ).
cnf(u1299,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_1(X0)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c9_2(X0,a1728)
| ~ ndr1_1(X0) ) ).
cnf(u1303,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_1(X0)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ c3_2(X0,a1728)
| ~ ndr1_1(X0) ) ).
cnf(u1308,negated_conjecture,
ssSkC46 ).
cnf(u1316,negated_conjecture,
~ c1_1(a1691) ).
cnf(u1321,negated_conjecture,
~ c6_1(a1691) ).
cnf(u1325,negated_conjecture,
~ ssSkC5 ).
cnf(u1329,negated_conjecture,
( ~ c6_2(X0,a1600)
| c5_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1333,negated_conjecture,
( ~ c7_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_2(X0,a1600)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1337,negated_conjecture,
( ~ c7_2(X0,X1)
| c4_2(X0,a1792)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c8_2(X0,X1) ) ).
cnf(u1341,negated_conjecture,
( ~ c7_2(X0,X1)
| c5_2(X0,a1792)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c8_2(X0,X1) ) ).
cnf(u1345,negated_conjecture,
( ~ c6_2(X0,X1)
| c7_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1378,negated_conjecture,
~ ndr1_1(a1681) ).
cnf(u1393,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_1(X0)
| c6_2(X0,a1625)
| c3_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1397,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_1(X0)
| c9_2(X0,a1625)
| c3_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1401,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_1(X0)
| c5_2(X0,a1728)
| c1_2(X0,X1)
| c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1405,negated_conjecture,
~ ssSkC41 ).
cnf(u1409,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_1(X0)
| ~ c7_2(X0,a1749)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1421,negated_conjecture,
( ~ c1_1(X1)
| c4_1(X1)
| ~ c7_1(X1) ) ).
cnf(u1428,negated_conjecture,
( ~ c10_2(X0,X1)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1447,negated_conjecture,
( ~ c7_2(X0,X1)
| c9_2(X0,a1600)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1495,negated_conjecture,
ssSkC32 ).
cnf(u1506,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_1(X0)
| c5_2(X0,a1749)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1510,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_1(X0)
| c8_2(X0,a1749)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1550,negated_conjecture,
~ ssSkC21 ).
cnf(u1554,negated_conjecture,
ndr1_1(a1700) ).
cnf(u1558,negated_conjecture,
( ~ c10_2(a1700,X0)
| c6_2(a1700,X0)
| ~ c3_2(a1700,X0) ) ).
cnf(u1573,negated_conjecture,
ssSkC29 ).
cnf(u1578,negated_conjecture,
~ ssSkC28 ).
cnf(u1582,negated_conjecture,
ndr1_1(a1745) ).
cnf(u1586,negated_conjecture,
( ~ c6_2(a1745,X0)
| c4_2(a1745,X0)
| ~ c8_2(a1745,X0) ) ).
cnf(u1589,negated_conjecture,
ssSkC39 ).
cnf(u1598,negated_conjecture,
ndr1_1(a1752) ).
cnf(u1602,negated_conjecture,
( ~ c6_2(a1752,X0)
| c2_2(a1752,X0)
| ~ c1_2(a1752,X0) ) ).
cnf(u1607,negated_conjecture,
ssSkC19 ).
cnf(u1610,negated_conjecture,
( ~ c7_2(X0,a1658)
| c9_1(X0)
| c8_2(X0,X1)
| c9_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1614,negated_conjecture,
( ~ c9_2(X0,a1658)
| c9_1(X0)
| c8_2(X0,X1)
| c9_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1619,negated_conjecture,
ssSkC27 ).
cnf(u1631,negated_conjecture,
ssSkC30 ).
cnf(u1649,negated_conjecture,
( ~ c2_2(X0,a1768)
| c4_1(X0)
| c8_1(X0) ) ).
cnf(u1653,negated_conjecture,
( ~ c5_2(X0,a1768)
| c4_1(X0)
| c8_1(X0) ) ).
cnf(u1657,negated_conjecture,
ndr1_1(a1620) ).
cnf(u1661,negated_conjecture,
( ~ c9_2(a1620,X0)
| c10_2(a1620,X0)
| c4_2(a1620,X0) ) ).
cnf(u1664,negated_conjecture,
ssSkC10 ).
cnf(u1669,negated_conjecture,
( ~ c4_2(X0,a1653)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u1698,negated_conjecture,
~ ndr1_1(a1708) ).
cnf(u1712,negated_conjecture,
ssSkC43 ).
cnf(u1738,negated_conjecture,
ssSkC25 ).
cnf(u1749,negated_conjecture,
~ ssSkC33 ).
cnf(u1753,negated_conjecture,
ndr1_1(a1721) ).
cnf(u1757,negated_conjecture,
( ~ c5_2(a1721,X0)
| c4_2(a1721,X0)
| ~ c9_2(a1721,X0) ) ).
cnf(u1770,negated_conjecture,
ssSkC54 ).
cnf(u1781,negated_conjecture,
( ~ c3_1(X1)
| c10_1(X1)
| c8_1(X1) ) ).
cnf(u1788,negated_conjecture,
( ~ c3_2(X0,a1614)
| c3_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u1799,negated_conjecture,
~ ssSkC13 ).
cnf(u1803,negated_conjecture,
( c5_1(X1)
| c3_2(X1,a1634)
| c2_1(X1) ) ).
cnf(u1811,negated_conjecture,
( c4_1(X1)
| c3_2(X1,a1768)
| c8_1(X1) ) ).
cnf(u1825,negated_conjecture,
( ~ c2_1(X0)
| c6_2(X0,a1653)
| ~ c3_1(X0) ) ).
cnf(u1829,negated_conjecture,
ndr1_1(a1668) ).
cnf(u1833,negated_conjecture,
( ~ c3_2(a1668,X0)
| c8_2(a1668,X0)
| ~ c9_2(a1668,X0) ) ).
cnf(u1852,negated_conjecture,
ssSkC35 ).
cnf(u1889,negated_conjecture,
ndr1_1(a1813) ).
cnf(u1893,negated_conjecture,
( ~ c8_2(a1813,X0)
| c9_2(a1813,X0)
| c10_2(a1813,X0) ) ).
cnf(u1896,negated_conjecture,
ssSkC53 ).
cnf(u1902,negated_conjecture,
ssSkC9 ).
cnf(u1913,negated_conjecture,
~ ssSkC16 ).
cnf(u1917,negated_conjecture,
ndr1_1(a1644) ).
cnf(u1921,negated_conjecture,
( ~ c8_2(a1644,X0)
| c9_2(a1644,X0)
| c4_2(a1644,X0) ) ).
cnf(u1925,negated_conjecture,
~ ssSkC24 ).
cnf(u1929,negated_conjecture,
ndr1_1(a1692) ).
cnf(u1933,negated_conjecture,
( ~ c6_2(a1692,X0)
| c9_2(a1692,X0)
| c3_2(a1692,X0) ) ).
cnf(u1941,negated_conjecture,
~ ssSkC47 ).
cnf(u1945,negated_conjecture,
ndr1_1(a1784) ).
cnf(u1949,negated_conjecture,
( ~ c7_2(a1784,X0)
| c1_2(a1784,X0)
| c9_2(a1784,X0) ) ).
cnf(u1954,negated_conjecture,
ssSkC48 ).
cnf(u1965,negated_conjecture,
~ ssSkC56 ).
cnf(u1969,negated_conjecture,
ndr1_1(a1820) ).
cnf(u1973,negated_conjecture,
( ~ c10_2(a1820,X0)
| c5_2(a1820,X0)
| c9_2(a1820,X0) ) ).
cnf(u1981,negated_conjecture,
( ndr1_1(X1)
| c5_1(X1)
| c2_1(X1) ) ).
cnf(u1985,negated_conjecture,
( ndr1_1(X1)
| c4_1(X1)
| c8_1(X1) ) ).
cnf(u1994,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2011,negated_conjecture,
( ~ c4_1(X0)
| c8_2(X0,a1742)
| ~ c10_1(X0) ) ).
cnf(u2014,negated_conjecture,
ssSkC38 ).
cnf(u2019,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,a1742)
| ~ c10_1(X0) ) ).
cnf(u2023,negated_conjecture,
( ~ c4_1(X0)
| c7_2(X0,a1742)
| ~ c10_1(X0) ) ).
cnf(u2031,negated_conjecture,
( ~ ssSkP1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u2042,negated_conjecture,
ssSkC40 ).
cnf(u2085,negated_conjecture,
( ~ c9_1(X0)
| c3_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2109,negated_conjecture,
ssSkC37 ).
cnf(u2113,negated_conjecture,
ssSkC36 ).
cnf(u2117,negated_conjecture,
( ~ c2_2(X0,a1738)
| ~ c10_1(X0)
| ~ ssSkP6(X0) ) ).
cnf(u2121,negated_conjecture,
( ~ c4_2(X0,a1738)
| ~ c10_1(X0)
| ~ ssSkP6(X0) ) ).
cnf(u2125,negated_conjecture,
( ~ c4_1(X0)
| ndr1_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2150,negated_conjecture,
ssSkC7 ).
cnf(u2162,negated_conjecture,
ssSkC15 ).
cnf(u2169,negated_conjecture,
( ~ c10_2(X0,a1666)
| c6_1(X0)
| ~ c8_1(X0) ) ).
cnf(u2186,negated_conjecture,
ssSkC2 ).
cnf(u2198,negated_conjecture,
~ ssSkC3 ).
cnf(u2201,negated_conjecture,
( ~ ssSkP0(X0)
| c7_1(X0)
| c3_2(X0,a1596) ) ).
cnf(u2205,negated_conjecture,
( ~ ssSkP0(X0)
| c7_1(X0)
| c5_2(X0,a1596) ) ).
cnf(u2225,negated_conjecture,
( ~ c8_2(X0,a1665)
| c3_1(X0)
| c8_1(X0) ) ).
cnf(u2228,negated_conjecture,
ssSkC20 ).
cnf(u2233,negated_conjecture,
( ~ c7_2(X0,a1665)
| c3_1(X0)
| c8_1(X0) ) ).
cnf(u2237,negated_conjecture,
( ~ c9_2(X0,a1665)
| c3_1(X0)
| c8_1(X0) ) ).
cnf(u2251,negated_conjecture,
( ~ ssSkP6(X0)
| c9_2(X0,a1738)
| ~ c10_1(X0) ) ).
cnf(u2263,negated_conjecture,
~ ssSkC1 ).
cnf(u2267,negated_conjecture,
( ~ c10_1(X0)
| c8_1(X0)
| c10_2(X0,a1586) ) ).
cnf(u2271,negated_conjecture,
( ~ c10_1(X0)
| c8_1(X0)
| c8_2(X0,a1586) ) ).
cnf(u2275,negated_conjecture,
( ~ c10_1(X0)
| c8_1(X0)
| c9_2(X0,a1586) ) ).
cnf(u2280,negated_conjecture,
ssSkC4 ).
cnf(u2296,negated_conjecture,
ssSkC11 ).
cnf(u2311,negated_conjecture,
( ~ c8_1(X0)
| c6_1(X0)
| c3_2(X0,a1666) ) ).
cnf(u2316,negated_conjecture,
ssSkC23 ).
cnf(u2319,negated_conjecture,
( ~ c9_1(X0)
| c2_1(X0)
| c10_2(X0,a1676) ) ).
cnf(u2323,negated_conjecture,
( ~ c9_1(X0)
| c2_1(X0)
| c8_2(X0,a1676) ) ).
cnf(u2327,negated_conjecture,
( ~ c2_2(X0,a1709)
| c2_1(X0)
| c8_1(X0) ) ).
cnf(u2331,negated_conjecture,
( ~ c5_2(X0,a1709)
| c2_1(X0)
| c8_1(X0) ) ).
cnf(u2335,negated_conjecture,
~ ssSkC51 ).
cnf(u2339,negated_conjecture,
( ~ c10_2(X0,a1801)
| c5_1(X0)
| ~ ssSkP14(X0) ) ).
cnf(u2343,negated_conjecture,
( ~ c4_2(X0,a1801)
| c5_1(X0)
| ~ ssSkP14(X0) ) ).
cnf(u2354,negated_conjecture,
ssSkC22 ).
cnf(u2363,negated_conjecture,
~ ssSkC17 ).
cnf(u2367,negated_conjecture,
( c9_2(a1647,X0)
| c4_2(a1647,X0) ) ).
cnf(u2370,negated_conjecture,
ndr1_1(a1647) ).
cnf(u2388,negated_conjecture,
( ~ ssSkP6(X0)
| ndr1_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2404,negated_conjecture,
( ~ c10_1(X0)
| c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u2424,negated_conjecture,
( ~ c8_1(X0)
| c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u2432,negated_conjecture,
( c8_1(X0)
| c2_1(X0)
| c6_2(X0,a1709) ) ).
cnf(u2448,negated_conjecture,
( ~ ssSkP14(X0)
| c5_1(X0)
| c6_2(X0,a1801) ) ).
cnf(u2461,negated_conjecture,
ssSkC18 ).
cnf(u2472,negated_conjecture,
( c3_1(X0)
| ndr1_1(X0)
| c8_1(X0) ) ).
cnf(u2488,negated_conjecture,
( c8_1(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u2493,negated_conjecture,
( ~ ssSkP14(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u2507,negated_conjecture,
~ c8_2(a1683,a1684) ).
cnf(u2512,negated_conjecture,
~ c6_2(a1683,a1684) ).
cnf(u2550,negated_conjecture,
ssSkC0 ).
cnf(u2556,negated_conjecture,
~ c8_2(a1611,a1612) ).
cnf(u2561,negated_conjecture,
~ c4_2(a1611,a1612) ).
cnf(u2576,negated_conjecture,
~ c4_2(a1620,a1621) ).
cnf(u2581,negated_conjecture,
~ c8_2(a1620,a1621) ).
cnf(u2611,negated_conjecture,
~ c2_1(a1683) ).
cnf(u2616,negated_conjecture,
c5_2(a1683,a1684) ).
cnf(u2630,negated_conjecture,
~ c7_2(a1700,a1701) ).
cnf(u2640,negated_conjecture,
~ c1_1(a1705) ).
cnf(u2645,negated_conjecture,
~ c9_1(a1705) ).
cnf(u2650,negated_conjecture,
~ c3_1(a1705) ).
cnf(u2660,negated_conjecture,
~ c4_2(a1745,a1746) ).
cnf(u2665,negated_conjecture,
~ c6_2(a1745,a1746) ).
cnf(u2670,negated_conjecture,
~ c9_2(a1798,a1799) ).
cnf(u2673,negated_conjecture,
ssSkC50 ).
cnf(u2754,negated_conjecture,
~ c5_1(a1611) ).
cnf(u2759,negated_conjecture,
c9_2(a1611,a1612) ).
cnf(u2779,negated_conjecture,
c7_2(a1620,a1621) ).
cnf(u2787,negated_conjecture,
ssSkC14 ).
cnf(u2839,negated_conjecture,
c3_1(a1681) ).
cnf(u2844,negated_conjecture,
c8_1(a1681) ).
cnf(u2849,negated_conjecture,
c8_1(a1683) ).
cnf(u2854,negated_conjecture,
ndr1_1(a1683) ).
cnf(u2884,negated_conjecture,
~ c7_1(a1700) ).
cnf(u2889,negated_conjecture,
c9_2(a1700,a1701) ).
cnf(u2894,negated_conjecture,
c4_2(a1700,a1701) ).
cnf(u2910,negated_conjecture,
~ c8_1(a1745) ).
cnf(u2915,negated_conjecture,
c1_2(a1745,a1746) ).
cnf(u2920,negated_conjecture,
~ c9_1(a1752) ).
cnf(u2925,negated_conjecture,
~ c8_1(a1752) ).
cnf(u2970,negated_conjecture,
~ c6_1(a1798) ).
cnf(u2975,negated_conjecture,
~ c1_1(a1798) ).
cnf(u2980,negated_conjecture,
c10_2(a1798,a1799) ).
cnf(u2985,negated_conjecture,
c5_2(a1798,a1799) ).
cnf(u3003,negated_conjecture,
ssSkC52 ).
cnf(u3022,negated_conjecture,
ssSkC55 ).
cnf(u3036,negated_conjecture,
ssSkC57 ).
cnf(u3052,negated_conjecture,
~ c3_2(a1593,a1594) ).
cnf(u3057,negated_conjecture,
~ c8_2(a1593,a1594) ).
cnf(u3062,negated_conjecture,
~ c10_2(a1593,a1594) ).
cnf(u3072,negated_conjecture,
~ c5_2(a1631,a1632) ).
cnf(u3077,negated_conjecture,
~ c1_2(a1631,a1632) ).
cnf(u3082,negated_conjecture,
~ c3_2(a1631,a1633) ).
cnf(u3132,negated_conjecture,
~ c9_2(a1692,a1693) ).
cnf(u3157,negated_conjecture,
~ c2_2(a1721,a1722) ).
cnf(u3162,negated_conjecture,
~ c4_2(a1721,a1722) ).
cnf(u3167,negated_conjecture,
~ c8_2(a1721,a1722) ).
cnf(u3252,negated_conjecture,
~ c9_2(a1820,a1821) ).
cnf(u3257,negated_conjecture,
~ c1_2(a1820,a1821) ).
cnf(u3295,negated_conjecture,
c10_1(a1611) ).
cnf(u3300,negated_conjecture,
ndr1_1(a1611) ).
cnf(u3310,negated_conjecture,
c3_1(a1620) ).
cnf(u3371,negated_conjecture,
~ c1_2(a1659,a1661) ).
cnf(u3543,negated_conjecture,
ndr1_1(a1798) ).
cnf(u3584,negated_conjecture,
~ c5_1(a1813) ).
cnf(u3589,negated_conjecture,
~ c4_1(a1813) ).
cnf(u3634,negated_conjecture,
~ c6_1(a1593) ).
cnf(u3649,negated_conjecture,
c9_2(a1631,a1632) ).
cnf(u3654,negated_conjecture,
c9_2(a1631,a1633) ).
cnf(u3659,negated_conjecture,
c4_2(a1631,a1633) ).
cnf(u3689,negated_conjecture,
~ c9_1(a1644) ).
cnf(u3694,negated_conjecture,
~ c6_1(a1644) ).
cnf(u3699,negated_conjecture,
~ c4_1(a1647) ).
cnf(u3704,negated_conjecture,
~ c2_1(a1647) ).
cnf(u3739,negated_conjecture,
~ c8_1(a1692) ).
cnf(u3744,negated_conjecture,
c10_2(a1692,a1693) ).
cnf(u3749,negated_conjecture,
c4_2(a1692,a1693) ).
cnf(u3759,negated_conjecture,
~ c3_1(a1698) ).
cnf(u3764,negated_conjecture,
~ c6_1(a1698) ).
cnf(u3779,negated_conjecture,
~ c3_1(a1721) ).
cnf(u3859,negated_conjecture,
~ c10_1(a1784) ).
cnf(u3864,negated_conjecture,
~ c2_1(a1784) ).
cnf(u3924,negated_conjecture,
~ c7_1(a1820) ).
cnf(u3929,negated_conjecture,
c8_2(a1820,a1821) ).
cnf(u4038,negated_conjecture,
~ c5_1(a1659) ).
cnf(u4043,negated_conjecture,
c3_2(a1659,a1660) ).
cnf(u4048,negated_conjecture,
c5_2(a1659,a1660) ).
cnf(u4053,negated_conjecture,
c4_2(a1659,a1660) ).
cnf(u4058,negated_conjecture,
c9_2(a1659,a1661) ).
cnf(u4063,negated_conjecture,
c4_2(a1659,a1661) ).
cnf(u4068,negated_conjecture,
~ c6_1(a1668) ).
cnf(u4176,negated_conjecture,
c9_1(a1593) ).
cnf(u4181,negated_conjecture,
ndr1_1(a1593) ).
cnf(u4197,negated_conjecture,
c5_1(a1631) ).
cnf(u4202,negated_conjecture,
ndr1_1(a1631) ).
cnf(u4346,negated_conjecture,
ndr1_1(a1659) ).
cnf(u4375,negated_conjecture,
~ c10_1(a1698) ).
cnf(u4385,negated_conjecture,
c10_1(a1705) ).
cnf(u4400,negated_conjecture,
c8_1(a1620) ).
cnf(u4404,negated_conjecture,
c10_1(a1620) ).
cnf(u4419,negated_conjecture,
c4_1(a1681) ).
cnf(u4422,negated_conjecture,
~ c2_1(a1681) ).
cnf(u4439,negated_conjecture,
c5_1(a1681) ).
cnf(u4444,negated_conjecture,
c9_1(a1681) ).
cnf(u4498,negated_conjecture,
c10_1(a1700) ).
cnf(u4502,negated_conjecture,
c8_1(a1700) ).
cnf(u4506,negated_conjecture,
~ c10_1(a1820) ).
cnf(u4510,negated_conjecture,
~ c8_1(a1820) ).
cnf(u4515,negated_conjecture,
~ c10_1(a1767) ).
cnf(u4519,negated_conjecture,
~ c8_1(a1767) ).
cnf(u4568,negated_conjecture,
~ c5_1(a1784) ).
cnf(u4596,negated_conjecture,
ssSkP1(a1647) ).
cnf(u4605,negated_conjecture,
ssSkP5(a1647) ).
cnf(u4614,negated_conjecture,
ssSkP11(a1647) ).
cnf(u4631,negated_conjecture,
~ c2_1(a1611) ).
cnf(u4636,negated_conjecture,
c6_2(a1611,a1634) ).
cnf(u4640,negated_conjecture,
~ c2_1(a1813) ).
cnf(u4645,negated_conjecture,
c6_2(a1813,a1634) ).
cnf(u4651,negated_conjecture,
c2_1(a1767) ).
cnf(u4668,negated_conjecture,
c3_2(a1611,a1634) ).
cnf(u4677,negated_conjecture,
~ c3_1(a1767) ).
cnf(u4686,negated_conjecture,
~ c3_1(a1813) ).
cnf(u4740,negated_conjecture,
~ c8_1(a1813) ).
cnf(u4751,negated_conjecture,
c8_1(a1647) ).
cnf(u4755,negated_conjecture,
c3_2(a1647,a1768) ).
cnf(u4760,negated_conjecture,
c3_2(a1813,a1768) ).
cnf(u4769,negated_conjecture,
~ c10_1(a1681) ).
cnf(u4801,negated_conjecture,
c10_2(a1705,a1586) ).
cnf(u4805,negated_conjecture,
c8_1(a1705) ).
cnf(u4809,negated_conjecture,
~ c10_2(a1611,a1586) ).
cnf(u4814,negated_conjecture,
c8_1(a1611) ).
cnf(u4828,negated_conjecture,
c8_1(a1698) ).
cnf(u4838,negated_conjecture,
c10_2(a1767,a1586) ).
cnf(u4857,negated_conjecture,
c8_2(a1611,a1586) ).
cnf(u4862,negated_conjecture,
c8_2(a1767,a1586) ).
cnf(u4894,negated_conjecture,
c3_2(a1705,a1666) ).
cnf(u4903,negated_conjecture,
c3_2(a1683,a1666) ).
cnf(u4912,negated_conjecture,
c3_2(a1620,a1666) ).
cnf(u4925,negated_conjecture,
c6_1(a1700) ).
cnf(u4930,negated_conjecture,
c3_2(a1647,a1666) ).
cnf(u4950,negated_conjecture,
c4_2(a1647,a1665) ).
cnf(u4969,negated_conjecture,
c3_2(a1611,a1666) ).
cnf(u4982,negated_conjecture,
c4_1(a1700) ).
cnf(u4986,negated_conjecture,
c2_1(a1700) ).
cnf(u4991,negated_conjecture,
~ c5_1(a1700) ).
cnf(u5023,negated_conjecture,
~ c3_1(a1700) ).
cnf(u5048,negated_conjecture,
c6_2(a1752,a1709) ).
cnf(u5066,negated_conjecture,
c6_2(a1745,a1709) ).
cnf(u5080,negated_conjecture,
c2_1(a1692) ).
cnf(u5085,negated_conjecture,
c6_2(a1820,a1709) ).
cnf(u5089,negated_conjecture,
c2_1(a1820) ).
cnf(u5100,negated_conjecture,
~ c3_1(a1692) ).
cnf(u5136,negated_conjecture,
c6_2(a1700,a1595) ).
cnf(u5140,negated_conjecture,
c3_2(a1700,a1596) ).
cnf(u5145,negated_conjecture,
c6_2(a1820,a1595) ).
cnf(u5149,negated_conjecture,
c3_2(a1820,a1596) ).
cnf(u5158,negated_conjecture,
c3_2(a1767,a1596) ).
cnf(u5166,negated_conjecture,
c4_2(a1700,a1595) ).
cnf(u5171,negated_conjecture,
c4_2(a1820,a1595) ).
cnf(u5187,negated_conjecture,
c5_2(a1767,a1596) ).
cnf(u5203,negated_conjecture,
c3_2(a1700,a1595) ).
cnf(u5208,negated_conjecture,
c5_2(a1820,a1596) ).
cnf(u5218,negated_conjecture,
c8_2(a1705,a1737) ).
cnf(u5231,negated_conjecture,
c9_2(a1611,a1738) ).
cnf(u5236,negated_conjecture,
c8_2(a1620,a1737) ).
cnf(u5245,negated_conjecture,
c8_2(a1700,a1737) ).
cnf(u5268,negated_conjecture,
c2_2(a1611,a1800) ).
cnf(u5277,negated_conjecture,
c2_2(a1700,a1800) ).
cnf(u5286,negated_conjecture,
c2_2(a1813,a1800) ).
cnf(u5295,negated_conjecture,
c2_2(a1784,a1800) ).
cnf(u5304,negated_conjecture,
c2_2(a1767,a1800) ).
cnf(u5315,negated_conjecture,
~ c8_2(a1745,a1709) ).
cnf(u5325,negated_conjecture,
~ c1_2(a1752,a1709) ).
cnf(u5349,negated_conjecture,
c7_1(a1683) ).
cnf(u5354,negated_conjecture,
c1_2(a1798,a1799) ).
cnf(u5392,negated_conjecture,
c6_2(a1813,a1709) ).
cnf(u5397,negated_conjecture,
c3_2(a1784,a1666) ).
cnf(u5429,negated_conjecture,
~ c7_2(a1820,a1595) ).
cnf(u5432,negated_conjecture,
~ c1_2(a1820,a1595) ).
cnf(u5439,negated_conjecture,
~ c7_2(a1745,a1709) ).
cnf(u5442,negated_conjecture,
~ c1_2(a1745,a1709) ).
cnf(u5450,negated_conjecture,
~ c7_2(a1820,a1709) ).
cnf(u5453,negated_conjecture,
~ c1_2(a1820,a1709) ).
cnf(u5461,negated_conjecture,
~ c7_2(a1611,a1634) ).
cnf(u5470,negated_conjecture,
~ c7_2(a1752,a1709) ).
cnf(u5475,negated_conjecture,
~ c7_2(a1813,a1709) ).
cnf(u5484,negated_conjecture,
~ c7_2(a1647,a1709) ).
cnf(u5493,negated_conjecture,
~ c7_2(a1813,a1634) ).
cnf(u5502,negated_conjecture,
~ c7_2(a1784,a1634) ).
cnf(u5518,negated_conjecture,
~ c8_2(a1745,a1746) ).
cnf(u5527,negated_conjecture,
~ c8_2(a1798,a1799) ).
cnf(u5531,negated_conjecture,
~ c7_2(a1798,a1749) ).
cnf(u5540,negated_conjecture,
~ c8_2(a1820,a1596) ).
cnf(u5544,negated_conjecture,
~ c7_2(a1820,a1749) ).
cnf(u5557,negated_conjecture,
c5_1(a1705) ).
cnf(u5566,negated_conjecture,
c2_2(a1705,a1586) ).
cnf(u5571,negated_conjecture,
~ c5_1(a1692) ).
cnf(u5588,negated_conjecture,
c2_2(a1692,a1800) ).
cnf(u5649,negated_conjecture,
( c9_2(a1647,X0)
| c8_2(a1647,X0) ) ).
cnf(u5829,negated_conjecture,
c9_1(a1820) ).
cnf(u5873,negated_conjecture,
~ c2_1(a1659) ).
cnf(u5878,negated_conjecture,
c6_2(a1659,a1634) ).
cnf(u5883,negated_conjecture,
c3_2(a1659,a1634) ).
cnf(u5892,negated_conjecture,
c6_2(a1659,a1801) ).
cnf(u5899,negated_conjecture,
c1_2(a1659,a1660) ).
cnf(u5903,negated_conjecture,
c7_1(a1659) ).
cnf(u5910,negated_conjecture,
~ c7_2(a1659,a1634) ).
cnf(u5925,negated_conjecture,
~ c8_2(a1659,a1660) ).
cnf(u5946,negated_conjecture,
~ c7_2(a1659,a1801) ).
cnf(u5980,negated_conjecture,
c5_1(a1820) ).
cnf(u6027,negated_conjecture,
~ c8_2(a1700,a1600) ).
cnf(u6040,negated_conjecture,
~ c4_2(a1700,a1742) ).
cnf(u6055,negated_conjecture,
c9_2(a1700,a1600) ).
cnf(u6065,negated_conjecture,
~ c9_2(a1700,a1742) ).
cnf(u6068,negated_conjecture,
~ c3_2(a1700,a1742) ).
cnf(u6077,negated_conjecture,
~ c3_2(a1620,a1621) ).
cnf(u6085,negated_conjecture,
~ c5_1(a1620) ).
cnf(u6100,negated_conjecture,
~ c1_1(a1745) ).
cnf(u6125,negated_conjecture,
~ c3_2(a1745,a1746) ).
cnf(u6138,negated_conjecture,
~ c9_2(a1659,a1660) ).
cnf(u6141,negated_conjecture,
~ c10_1(a1659) ).
cnf(u6167,negated_conjecture,
c8_1(a1659) ).
cnf(u6176,negated_conjecture,
~ c10_2(a1659,a1801) ).
cnf(u6187,negated_conjecture,
~ c7_2(a1700,a1595) ).
cnf(u6192,negated_conjecture,
c10_2(a1700,a1595) ).
cnf(u6205,negated_conjecture,
c3_2(a1659,a1666) ).
cnf(u6248,negated_conjecture,
~ ssSkP9(a1813) ).
cnf(u6262,negated_conjecture,
~ ssSkP9(a1659) ).
cnf(u6277,negated_conjecture,
~ ssSkP9(a1611) ).
cnf(u6287,negated_conjecture,
~ ssSkP9(a1784) ).
cnf(u6297,negated_conjecture,
~ ssSkP9(a1752) ).
cnf(u6300,negated_conjecture,
c3_2(a1752,a1709) ).
cnf(u6310,negated_conjecture,
~ ssSkP9(a1745) ).
cnf(u6313,negated_conjecture,
c3_2(a1745,a1709) ).
cnf(u6318,negated_conjecture,
~ c9_2(a1745,a1765) ).
cnf(u6323,negated_conjecture,
~ ssSkP9(a1820) ).
cnf(u6337,negated_conjecture,
~ ssSkP9(a1700) ).
cnf(u6341,negated_conjecture,
~ c9_2(a1700,a1765) ).
cnf(u6421,negated_conjecture,
~ c9_2(a1798,a1717) ).
cnf(u6451,negated_conjecture,
~ c9_2(a1705,a1717) ).
cnf(u6454,negated_conjecture,
~ c6_2(a1705,a1586) ).
cnf(u6458,negated_conjecture,
~ c3_2(a1705,a1586) ).
cnf(u6464,negated_conjecture,
~ c9_2(a1611,a1717) ).
cnf(u6485,negated_conjecture,
~ c4_2(a1700,a1602) ).
cnf(u6512,negated_conjecture,
( c5_2(a1620,X0)
| c4_2(a1620,X0)
| c2_2(a1620,X0) ) ).
cnf(u6526,negated_conjecture,
c7_1(a1620) ).
cnf(u6541,negated_conjecture,
~ c10_1(a1593) ).
cnf(u6544,negated_conjecture,
~ c3_1(a1593) ).
cnf(u6554,negated_conjecture,
c2_1(a1593) ).
cnf(u6622,negated_conjecture,
~ c4_1(a1705) ).
cnf(u6635,negated_conjecture,
~ c3_2(a1611,a1800) ).
cnf(u6654,negated_conjecture,
~ c3_2(a1784,a1800) ).
cnf(u6658,negated_conjecture,
~ c4_1(a1784) ).
cnf(u6675,negated_conjecture,
~ c4_1(a1692) ).
cnf(u6692,negated_conjecture,
~ c4_1(a1767) ).
cnf(u6705,negated_conjecture,
~ c3_2(a1700,a1800) ).
cnf(u6709,negated_conjecture,
c9_2(a1700,a1800) ).
cnf(u6728,negated_conjecture,
c8_1(a1784) ).
cnf(u6784,negated_conjecture,
~ c3_2(a1700,a1602) ).
cnf(u6788,negated_conjecture,
c9_2(a1700,a1602) ).
cnf(u6844,negated_conjecture,
~ c5_2(a1813,a1625) ).
cnf(u6848,negated_conjecture,
c10_2(a1813,a1709) ).
cnf(u6853,negated_conjecture,
~ c5_2(a1820,a1625) ).
cnf(u6862,negated_conjecture,
~ c5_2(a1659,a1625) ).
cnf(u6866,negated_conjecture,
c9_1(a1659) ).
cnf(u6876,negated_conjecture,
~ c5_2(a1752,a1625) ).
cnf(u6885,negated_conjecture,
~ c5_2(a1745,a1625) ).
cnf(u6897,negated_conjecture,
~ c9_2(a1620,a1728) ).
cnf(u6901,negated_conjecture,
c2_2(a1620,a1621) ).
cnf(u6913,negated_conjecture,
~ c3_2(a1620,a1728) ).
cnf(u6999,negated_conjecture,
~ c3_1(a1820) ).
cnf(u7035,negated_conjecture,
~ c9_2(a1659,a1717) ).
cnf(u7383,negated_conjecture,
c3_2(a1620,a1634) ).
cnf(u7388,negated_conjecture,
c2_2(a1620,a1800) ).
cnf(u7404,negated_conjecture,
~ c3_2(a1620,a1800) ).
cnf(u7471,negated_conjecture,
~ c6_2(a1611,a1772) ).
cnf(u7483,negated_conjecture,
~ c6_2(a1620,a1772) ).
cnf(u7496,negated_conjecture,
~ c6_2(a1700,a1772) ).
cnf(u7514,negated_conjecture,
~ c6_2(a1813,a1772) ).
cnf(u7522,negated_conjecture,
c9_2(a1813,a1800) ).
cnf(u7526,negated_conjecture,
( ~ c1_2(a1784,X0)
| ~ c8_2(a1784,X0) ) ).
cnf(u7530,negated_conjecture,
~ c6_2(a1784,a1772) ).
cnf(u7538,negated_conjecture,
( ~ c1_2(a1692,X0)
| ~ c8_2(a1692,X0) ) ).
cnf(u7542,negated_conjecture,
~ c6_2(a1692,a1772) ).
cnf(u7550,negated_conjecture,
( ~ c1_2(a1767,X0)
| ~ c8_2(a1767,X0) ) ).
cnf(u7554,negated_conjecture,
~ c6_2(a1767,a1772) ).
cnf(u7562,negated_conjecture,
~ c10_2(a1700,a1742) ).
cnf(u7586,negated_conjecture,
~ c8_2(a1611,a1761) ).
cnf(u7602,negated_conjecture,
~ c8_2(a1813,a1761) ).
cnf(u7618,negated_conjecture,
~ c8_2(a1659,a1761) ).
cnf(u7634,negated_conjecture,
~ c8_2(a1752,a1761) ).
cnf(u7641,negated_conjecture,
c9_2(a1752,a1709) ).
cnf(u7650,negated_conjecture,
~ c8_2(a1745,a1761) ).
cnf(u7657,negated_conjecture,
c9_2(a1745,a1709) ).
cnf(u7671,negated_conjecture,
~ c8_2(a1820,a1761) ).
cnf(u7674,negated_conjecture,
( ~ c3_2(a1820,X0)
| c10_2(a1820,X0) ) ).
cnf(u7714,negated_conjecture,
~ c3_2(a1611,a1761) ).
cnf(u7719,negated_conjecture,
~ c3_2(a1813,a1761) ).
cnf(u7724,negated_conjecture,
~ c3_2(a1659,a1761) ).
cnf(u7729,negated_conjecture,
~ c3_2(a1752,a1761) ).
cnf(u7734,negated_conjecture,
~ c3_2(a1745,a1761) ).
cnf(u7740,negated_conjecture,
~ c3_2(a1820,a1761) ).
cnf(u7775,negated_conjecture,
c3_2(a1611,a1772) ).
cnf(u7780,negated_conjecture,
c3_2(a1620,a1772) ).
cnf(u7786,negated_conjecture,
c3_2(a1700,a1772) ).
cnf(u7820,negated_conjecture,
~ c9_2(a1700,a1717) ).
cnf(u7848,negated_conjecture,
c5_2(a1611,a1761) ).
cnf(u7853,negated_conjecture,
c5_2(a1813,a1761) ).
cnf(u7858,negated_conjecture,
c5_2(a1659,a1761) ).
cnf(u7862,negated_conjecture,
~ c5_2(a1752,a1761) ).
cnf(u7882,negated_conjecture,
c1_2(a1611,a1761) ).
cnf(u7893,negated_conjecture,
c1_2(a1813,a1761) ).
cnf(u7984,negated_conjecture,
~ c3_2(a1611,a1764) ).
cnf(u7996,negated_conjecture,
~ c3_2(a1700,a1764) ).
cnf(u8008,negated_conjecture,
~ c3_2(a1784,a1764) ).
cnf(u8025,negated_conjecture,
~ c3_2(a1659,a1764) ).
cnf(u8059,negated_conjecture,
~ c7_2(a1705,a1586) ).
cnf(u8067,negated_conjecture,
~ c7_2(a1611,a1586) ).
cnf(u8075,negated_conjecture,
~ c7_2(a1798,a1799) ).
cnf(u8088,negated_conjecture,
~ c7_2(a1820,a1596) ).
cnf(u8104,negated_conjecture,
~ c7_2(a1659,a1676) ).
cnf(u8117,negated_conjecture,
~ c7_2(a1692,a1693) ).
cnf(u8129,negated_conjecture,
~ c7_2(a1767,a1586) ).
cnf(u8165,negated_conjecture,
( ~ c7_2(a1798,X0)
| c5_2(a1798,X0)
| ~ c8_2(a1798,X0) ) ).
cnf(u8174,negated_conjecture,
c3_2(a1692,a1693) ).
cnf(u8185,negated_conjecture,
( ~ c7_2(a1659,X0)
| c5_2(a1659,X0)
| ~ c8_2(a1659,X0) ) ).
cnf(u8193,negated_conjecture,
( ~ c7_2(a1767,X0)
| c5_2(a1767,X0)
| ~ c8_2(a1767,X0) ) ).
cnf(u8201,negated_conjecture,
( ~ c7_2(a1705,X0)
| c5_2(a1705,X0)
| ~ c8_2(a1705,X0) ) ).
cnf(clause56,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u4413,negated_conjecture,
c6_1(a1681) ).
cnf(u4764,negated_conjecture,
( ~ c10_1(X0)
| c8_2(X0,a1742)
| c3_2(X0,a1768)
| c8_1(X0) ) ).
cnf(u6771,negated_conjecture,
c2_2(a1700,a1602) ).
cnf(u4707,negated_conjecture,
c3_2(a1813,a1634) ).
cnf(clause314,negated_conjecture,
( ~ c8_2(X0,a1775)
| ssSkP11(X0) ) ).
cnf(u6364,negated_conjecture,
c2_2(a1784,a1764) ).
cnf(u6351,negated_conjecture,
c9_2(a1752,a1764) ).
cnf(clause210,negated_conjecture,
( ssSkP0(X0)
| c6_2(X0,a1595) ) ).
cnf(u5003,negated_conjecture,
c7_2(a1700,a1742) ).
cnf(u6356,negated_conjecture,
c2_2(a1813,a1764) ).
cnf(u4392,negated_conjecture,
ndr1_1(a1705) ).
cnf(u4547,negated_conjecture,
( c6_1(X0)
| ndr1_1(X0) ) ).
cnf(clause32,negated_conjecture,
( ssSkP12(X0)
| ndr1_1(X0) ) ).
cnf(clause70,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause347,negated_conjecture,
( ~ c10_2(X0,a1627)
| ssSkP3(X0) ) ).
cnf(u7022,negated_conjecture,
c10_2(a1659,a1676) ).
cnf(clause349,negated_conjecture,
( ~ c2_2(X0,a1623)
| ssSkP2(X0) ) ).
cnf(clause28,negated_conjecture,
( ssSkP14(X0)
| ndr1_1(X0) ) ).
cnf(u6531,negated_conjecture,
c1_2(a1767,a1596) ).
cnf(u4785,negated_conjecture,
( c7_1(X0)
| c5_2(X0,a1596)
| c6_2(X0,a1595) ) ).
cnf(u5001,negated_conjecture,
c8_2(a1700,a1742) ).
cnf(u4782,negated_conjecture,
( c7_1(X0)
| c3_2(X0,a1596)
| c4_2(X0,a1595) ) ).
cnf(u4781,negated_conjecture,
( c7_1(X0)
| c3_2(X0,a1596)
| c6_2(X0,a1595) ) ).
cnf(u6367,negated_conjecture,
c9_2(a1820,a1764) ).
cnf(u5032,negated_conjecture,
( c2_1(X0)
| c10_2(X0,a1676)
| ndr1_1(X0) ) ).
cnf(clause125,negated_conjecture,
( ssSkP16(X0)
| c1_2(X0,a1832) ) ).
cnf(u6991,negated_conjecture,
c4_2(a1745,a1764) ).
cnf(u4788,negated_conjecture,
( c7_1(X0)
| c5_2(X0,a1596)
| ndr1_1(X0) ) ).
cnf(u4776,negated_conjecture,
( ~ c10_1(X0)
| c2_2(X0,a1742)
| c3_2(X0,a1768)
| c8_1(X0) ) ).
cnf(u4783,negated_conjecture,
( c7_1(X0)
| c3_2(X0,a1596)
| c3_2(X0,a1595) ) ).
cnf(u7925,negated_conjecture,
c10_2(a1820,a1596) ).
cnf(clause208,negated_conjecture,
( ssSkP0(X0)
| c3_2(X0,a1595) ) ).
cnf(u4779,negated_conjecture,
( ~ c10_1(X0)
| c7_2(X0,a1742)
| c3_2(X0,a1768)
| c8_1(X0) ) ).
cnf(u4362,negated_conjecture,
ndr1_1(a1767) ).
cnf(clause154,negated_conjecture,
( ssSkP8(X0)
| c3_2(X0,a1762) ) ).
cnf(clause153,negated_conjecture,
( ssSkP9(X0)
| c9_2(X0,a1764) ) ).
cnf(clause126,negated_conjecture,
( ssSkP15(X0)
| c5_2(X0,a1829) ) ).
cnf(clause156,negated_conjecture,
( ssSkP7(X0)
| c4_2(X0,a1754) ) ).
cnf(clause316,negated_conjecture,
( ~ c2_2(X0,a1762)
| ssSkP8(X0) ) ).
cnf(clause150,negated_conjecture,
( ssSkP10(X0)
| c2_2(X0,a1773) ) ).
cnf(clause310,negated_conjecture,
( ~ c2_2(X0,a1777)
| ssSkP12(X0) ) ).
cnf(clause149,negated_conjecture,
( ssSkP10(X0)
| c5_2(X0,a1773) ) ).
cnf(u4579,negated_conjecture,
( c4_1(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(clause40,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u7023,negated_conjecture,
c8_2(a1659,a1676) ).
cnf(clause292,negated_conjecture,
( ~ c2_2(X0,a1829)
| ssSkP15(X0) ) ).
cnf(u6391,negated_conjecture,
c4_2(a1700,a1764) ).
cnf(u5037,negated_conjecture,
( c2_1(X0)
| c6_2(X0,a1709)
| c6_1(X0)
| c3_2(X0,a1666) ) ).
cnf(clause60,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(u5033,negated_conjecture,
c10_2(a1681,a1676) ).
cnf(u5360,negated_conjecture,
c1_2(a1820,a1596) ).
cnf(u6579,negated_conjecture,
~ c9_2(a1767,a1596) ).
cnf(clause34,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(u4936,negated_conjecture,
c3_2(a1698,a1666) ).
cnf(clause313,negated_conjecture,
( ~ c9_2(X0,a1775)
| ssSkP11(X0) ) ).
cnf(clause307,negated_conjecture,
( ~ c8_2(X0,a1793)
| ssSkP13(X0) ) ).
cnf(u6352,negated_conjecture,
c2_2(a1752,a1764) ).
cnf(clause332,negated_conjecture,
( ~ c3_2(X0,a1689)
| ssSkP5(X0) ) ).
cnf(u6363,negated_conjecture,
c9_2(a1784,a1764) ).
cnf(u4670,negated_conjecture,
c3_2(a1784,a1634) ).
cnf(u5035,negated_conjecture,
( c2_1(X0)
| c8_2(X0,a1676)
| ndr1_1(X0) ) ).
cnf(u6355,negated_conjecture,
c9_2(a1813,a1764) ).
cnf(clause311,negated_conjecture,
( ~ c8_2(X0,a1777)
| ssSkP12(X0) ) ).
cnf(u6719,negated_conjecture,
c3_2(a1692,a1768) ).
cnf(clause64,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause33,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(clause36,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u6389,negated_conjecture,
c9_2(a1700,a1764) ).
cnf(clause351,negated_conjecture,
( ~ c10_2(X0,a1623)
| ssSkP2(X0) ) ).
cnf(clause30,negated_conjecture,
( ssSkP13(X0)
| ndr1_1(X0) ) ).
cnf(clause16,negated_conjecture,
( ssSkP16(X0)
| ndr1_1(X0) ) ).
cnf(clause209,negated_conjecture,
( ssSkP0(X0)
| c4_2(X0,a1595) ) ).
cnf(u5002,negated_conjecture,
c2_2(a1700,a1742) ).
cnf(clause333,negated_conjecture,
( ~ c9_2(X0,a1689)
| ssSkP5(X0) ) ).
cnf(u4357,negated_conjecture,
( c5_1(X0)
| ndr1_1(X0) ) ).
cnf(clause6,negated_conjecture,
~ c7_1(a1767) ).
cnf(u6989,negated_conjecture,
c9_2(a1745,a1764) ).
cnf(clause164,negated_conjecture,
( ssSkP6(X0)
| c8_2(X0,a1737) ) ).
cnf(clause127,negated_conjecture,
( ssSkP15(X0)
| c4_2(X0,a1829) ) ).
cnf(u7826,negated_conjecture,
~ c8_2(a1767,a1596) ).
cnf(u6361,negated_conjecture,
c4_2(a1659,a1764) ).
cnf(clause350,negated_conjecture,
( ~ c6_2(X0,a1623)
| ssSkP2(X0) ) ).
cnf(u6357,negated_conjecture,
c4_2(a1813,a1764) ).
cnf(u6349,negated_conjecture,
c4_2(a1611,a1764) ).
cnf(u6365,negated_conjecture,
c4_2(a1784,a1764) ).
cnf(u6360,negated_conjecture,
c2_2(a1659,a1764) ).
cnf(clause308,negated_conjecture,
( ~ c5_2(X0,a1793)
| ssSkP13(X0) ) ).
cnf(clause192,negated_conjecture,
( ssSkP4(X0)
| c2_2(X0,a1648) ) ).
cnf(u5128,negated_conjecture,
( c8_2(X0,a1676)
| ndr1_1(X0) ) ).
cnf(u6359,negated_conjecture,
c9_2(a1659,a1764) ).
cnf(u4538,negated_conjecture,
ndr1_1(a1698) ).
cnf(clause346,negated_conjecture,
( ~ c7_2(X0,a1627)
| ssSkP3(X0) ) ).
cnf(clause158,negated_conjecture,
( ssSkP7(X0)
| c2_2(X0,a1754) ) ).
cnf(clause157,negated_conjecture,
( ssSkP7(X0)
| c8_2(X0,a1754) ) ).
cnf(clause348,negated_conjecture,
( ~ c1_2(X0,a1627)
| ssSkP3(X0) ) ).
cnf(clause151,negated_conjecture,
( ssSkP9(X0)
| c4_2(X0,a1764) ) ).
cnf(clause35,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(clause138,negated_conjecture,
( ssSkP14(X0)
| c2_2(X0,a1800) ) ).
cnf(clause68,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u5118,negated_conjecture,
( c10_2(X0,a1676)
| ndr1_1(X0) ) ).
cnf(clause322,negated_conjecture,
( ~ c10_2(X0,a1737)
| ssSkP6(X0) ) ).
cnf(u6390,negated_conjecture,
c2_2(a1700,a1764) ).
cnf(u6353,negated_conjecture,
c4_2(a1752,a1764) ).
cnf(u6369,negated_conjecture,
c4_2(a1820,a1764) ).
cnf(u4535,negated_conjecture,
( c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u4585,negated_conjecture,
( c9_1(X0)
| ndr1_1(X0) ) ).
cnf(clause44,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause65,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(clause315,negated_conjecture,
( ~ c4_2(X0,a1773)
| ssSkP10(X0) ) ).
cnf(u6722,negated_conjecture,
c3_2(a1767,a1768) ).
cnf(u4786,negated_conjecture,
( c7_1(X0)
| c5_2(X0,a1596)
| c4_2(X0,a1595) ) ).
cnf(clause317,negated_conjecture,
( ~ c10_2(X0,a1762)
| ssSkP8(X0) ) ).
cnf(clause353,negated_conjecture,
( ~ c1_2(X0,a1613)
| ssSkP1(X0) ) ).
cnf(clause152,negated_conjecture,
( ssSkP9(X0)
| c2_2(X0,a1764) ) ).
cnf(clause17,negated_conjecture,
( ssSkP15(X0)
| ndr1_1(X0) ) ).
cnf(u5108,negated_conjecture,
( c5_1(X0)
| c6_2(X0,a1801)
| c2_2(X0,a1800) ) ).
cnf(clause291,negated_conjecture,
( ~ c4_2(X0,a1832)
| ssSkP16(X0) ) ).
cnf(u6368,negated_conjecture,
c2_2(a1820,a1764) ).
cnf(u4787,negated_conjecture,
( c7_1(X0)
| c5_2(X0,a1596)
| c3_2(X0,a1595) ) ).
cnf(u4784,negated_conjecture,
( c7_1(X0)
| c3_2(X0,a1596)
| ndr1_1(X0) ) ).
cnf(u5374,negated_conjecture,
( ~ c3_1(X0)
| c6_1(X0)
| c3_2(X0,a1666)
| c6_2(X0,a1653)
| c6_2(X0,a1709) ) ).
cnf(u5036,negated_conjecture,
c8_2(a1681,a1676) ).
cnf(clause190,negated_conjecture,
( ssSkP4(X0)
| c10_2(X0,a1648) ) ).
cnf(u6348,negated_conjecture,
c2_2(a1611,a1764) ).
cnf(clause183,negated_conjecture,
( ssSkP5(X0)
| c1_2(X0,a1689) ) ).
cnf(clause207,negated_conjecture,
( ssSkP1(X0)
| c5_2(X0,a1613) ) ).
cnf(u4463,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0) ) ).
cnf(clause7,negated_conjecture,
~ c5_1(a1767) ).
cnf(clause354,negated_conjecture,
( ~ c9_2(X0,a1613)
| ssSkP1(X0) ) ).
cnf(u6347,negated_conjecture,
c9_2(a1611,a1764) ).
cnf(clause142,negated_conjecture,
( ssSkP13(X0)
| c2_2(X0,a1793) ) ).
cnf(u4356,negated_conjecture,
( ~ c10_1(X0)
| ndr1_1(X0) ) ).
cnf(u6990,negated_conjecture,
c2_2(a1745,a1764) ).
cnf(clause312,negated_conjecture,
( ~ c7_2(X0,a1775)
| ssSkP11(X0) ) ).
cnf(u4790,negated_conjecture,
( ~ c10_1(X0)
| c9_2(X0,a1738)
| c8_2(X0,a1737) ) ).
cnf(clause124,negated_conjecture,
( ssSkP16(X0)
| c7_2(X0,a1832) ) ).
cnf(clause148,negated_conjecture,
( ssSkP12(X0)
| c3_2(X0,a1777) ) ).
cnf(clause191,negated_conjecture,
( ssSkP4(X0)
| c3_2(X0,a1648) ) ).
cnf(clause302,negated_conjecture,
( ~ c10_2(X0,a1800)
| ssSkP14(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN427-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.09/0.18 % Computer : n014.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:55:46 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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
% 4.14/1.23 % (1894899)Input is clausal, will run a generic CNF schedule.
% 4.14/1.23 % (1894954)lrs+10_1_sil=8000:sp=occurrence:random_seed=2078159294:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.14/1.23 % (1894954)Instruction limit reached!
% 4.14/1.23 % (1894954)------------------------------
% 4.14/1.23 % (1894954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.14/1.23 % (1894954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/1.23 % (1894954)CaDiCaL version: 2.1.3
% 4.14/1.23 % (1894954)Termination reason: Instruction limit
% 4.14/1.23 % (1894954)Termination phase: Saturation
% 4.14/1.23 % (1894954)Time elapsed: 0.035 s
% 4.14/1.23 % (1894954)Peak memory usage: 92 MB
% 4.14/1.23 % (1894954)Instructions burned: 110 (million)
% 4.14/1.23 % (1894956)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=565636544:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.14/1.23 % (1894951)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=2392496984:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.14/1.23 % (1894952)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1633479284:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.14/1.23 % (1894955)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3670930139:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.14/1.23 % (1894957)dis-21_1_sil=8000:lcm=predicate:random_seed=1703440759:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 4.14/1.23 % (1894953)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3885884800:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.14/1.23 % (1894955)Instruction limit reached!
% 4.14/1.23 % (1894955)------------------------------
% 4.14/1.23 % (1894955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.14/1.23 % (1894955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/1.23 % (1894955)CaDiCaL version: 2.1.3
% 4.14/1.23 % (1894955)Termination reason: Instruction limit
% 4.14/1.23 % (1894955)Termination phase: Saturation
% 4.14/1.23 % (1894955)Time elapsed: 0.065 s
% 4.14/1.23 % (1894955)Peak memory usage: 91 MB
% 4.14/1.23 % (1894955)Instructions burned: 115 (million)
% 4.14/1.23 % (1894957)Instruction limit reached!
% 4.14/1.23 % (1894957)------------------------------
% 4.14/1.23 % (1894957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.14/1.23 % (1894957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/1.23 % (1894957)CaDiCaL version: 2.1.3
% 4.14/1.23 % (1894957)Termination reason: Instruction limit
% 4.14/1.23 % (1894957)Termination phase: Saturation
% 4.14/1.23 % (1894957)Time elapsed: 0.065 s
% 4.14/1.23 % (1894957)Peak memory usage: 91 MB
% 4.14/1.23 % (1894957)Instructions burned: 117 (million)
% 4.14/1.23 % (1894956)Refutation not found, incomplete strategy
% 4.14/1.23 % (1894956)------------------------------
% 4.14/1.23 % (1894956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.14/1.23 % (1894956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/1.23 % (1894956)CaDiCaL version: 2.1.3
% 4.14/1.23 % (1894956)Termination reason: Refutation not found, incomplete strategy
% 4.14/1.23 % (1894956)Time elapsed: 0.068 s
% 4.14/1.23 % (1894956)Peak memory usage: 92 MB
% 4.14/1.23 % (1894956)Instructions burned: 117 (million)
% 4.14/1.23 % (1894959)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1190180023:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 4.14/1.23 % (1894959)Instruction limit reached!
% 4.14/1.23 % (1894959)------------------------------
% 4.14/1.23 % (1894959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.14/1.23 % (1894959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/1.23 % (1894959)CaDiCaL version: 2.1.3
% 4.14/1.23 % (1894959)Termination reason: Instruction limit
% 4.14/1.23 % (1894959)Termination phase: Saturation
% 4.14/1.23 % (1894959)Time elapsed: 0.045 s
% 4.14/1.23 % (1894959)Peak memory usage: 92 MB
% 4.14/1.23 % (1894959)Instructions burned: 146 (million)
% 4.14/1.23 % (1894967)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4025666008:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.14/1.23 % (1894966)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2079314605:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 4.14/1.23 % (1894969)lrs+10_64_to=lpo:sil=8000:random_seed=2128524932:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.14/1.23 % (1894966)Refutation not found, incomplete strategy
% 4.14/1.23 % (1894966)------------------------------
% 4.14/1.23 % (1894966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.14/1.23 % (1894966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/1.23 % (1894966)CaDiCaL version: 2.1.3
% 4.14/1.23 % (1894969)First to succeed.
% 4.14/1.23 % (1894966)Termination reason: Refutation not found, incomplete strategy
% 4.14/1.23 % (1894966)Time elapsed: 0.053 s
% 4.14/1.23 % (1894966)Peak memory usage: 91 MB
% 4.14/1.23 % (1894966)Instructions burned: 94 (million)
% 4.14/1.23 % (1894969)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1894899"
% 4.14/1.23 % (1894967)Instruction limit reached!
% 4.14/1.23 % (1894967)------------------------------
% 4.14/1.23 % (1894967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.14/1.23 % (1894967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/1.23 % (1894967)CaDiCaL version: 2.1.3
% 4.14/1.23 % (1894967)Termination reason: Instruction limit
% 4.14/1.23 % (1894967)Termination phase: Saturation
% 4.14/1.23 % (1894967)Time elapsed: 0.118 s
% 4.14/1.23 % (1894967)Peak memory usage: 93 MB
% 4.14/1.23 % (1894967)Instructions burned: 219 (million)
% 4.14/1.23 % (1894956)------------------------------
% 4.14/1.23 % (1894956)------------------------------
% 4.14/1.23 % SZS status Satisfiable for theBenchmark
% 4.14/1.23 % SZS output start Saturation.
% See solution above
% 4.63/1.43 % SZS output start Definitions and Model Updates.
% 4.63/1.43 % SZS output end Definitions and Model Updates.
% 4.63/1.43 % (1894969)------------------------------
% 4.63/1.43 % (1894969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.43 % (1894969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.43 % (1894969)CaDiCaL version: 2.1.3
% 4.63/1.43 % (1894969)Termination reason: Satisfiable
% 4.63/1.43 % (1894969)Time elapsed: 0.040 s
% 4.63/1.43 % (1894969)Peak memory usage: 92 MB
% 4.63/1.43 % (1894969)Instructions burned: 130 (million)
% 4.63/1.43 % (1894969)------------------------------
% 4.63/1.43 % (1894969)------------------------------
% 4.63/1.43 % (1894899)Success in time 0.572 s
% 4.63/1.43 % Vampire exiting
%------------------------------------------------------------------------------