%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN905-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 02:05:56 PM UTC 2026
% Result : Satisfiable 5.21s 2.31s
% Output : Saturation 5.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u811,negated_conjecture,
~ ssSkC10 ).
cnf(u816,negated_conjecture,
ssSkP678(skc21) ).
cnf(u820,negated_conjecture,
( ssSkP532(X0)
| ~ ssSkP545(X0) ) ).
cnf(u824,negated_conjecture,
( ssPv48(X0)
| ~ ssSkP545(X0) ) ).
cnf(u828,negated_conjecture,
( ssSkP533(X0)
| ~ ssSkP546(X0) ) ).
cnf(u832,negated_conjecture,
( ssPv25(X0)
| ~ ssSkP546(X0) ) ).
cnf(u836,negated_conjecture,
( ssSkP535(X0)
| ~ ssSkP547(X0) ) ).
cnf(u840,negated_conjecture,
( ssPv47(X0)
| ~ ssSkP547(X0) ) ).
cnf(u844,negated_conjecture,
( ssSkP542(X0)
| ~ ssSkP548(X0) ) ).
cnf(u848,negated_conjecture,
( ssPv9(X0)
| ~ ssSkP548(X0) ) ).
cnf(u852,negated_conjecture,
( ssSkP538(X0)
| ~ ssSkP549(X0) ) ).
cnf(u856,negated_conjecture,
( ssPv46(X0)
| ~ ssSkP549(X0) ) ).
cnf(u860,negated_conjecture,
( ssSkP539(X0)
| ~ ssSkP550(X0) ) ).
cnf(u864,negated_conjecture,
( ssPv16(X0)
| ~ ssSkP550(X0) ) ).
cnf(u868,negated_conjecture,
( ssSkP541(X0)
| ~ ssSkP551(X0) ) ).
cnf(u872,negated_conjecture,
( ssPv41(X0)
| ~ ssSkP551(X0) ) ).
cnf(u876,negated_conjecture,
( ssSkP537(X0)
| ~ ssSkP552(X0) ) ).
cnf(u880,negated_conjecture,
( ssPv11(X0)
| ~ ssSkP552(X0) ) ).
cnf(u884,negated_conjecture,
( ssSkP544(X0)
| ~ ssSkP553(X0) ) ).
cnf(u888,negated_conjecture,
( ssPv30(X0)
| ~ ssSkP553(X0) ) ).
cnf(u892,negated_conjecture,
( ssSkP534(X0)
| ~ ssSkP554(X0) ) ).
cnf(u896,negated_conjecture,
( ssPv14(X0)
| ~ ssSkP554(X0) ) ).
cnf(u900,negated_conjecture,
( ssSkP536(X0)
| ~ ssSkP555(X0) ) ).
cnf(u904,negated_conjecture,
( ssPv29(X0)
| ~ ssSkP555(X0) ) ).
cnf(u908,negated_conjecture,
( ssSkP540(X0)
| ~ ssSkP557(X0) ) ).
cnf(u912,negated_conjecture,
( ssPv28(X0)
| ~ ssSkP557(X0) ) ).
cnf(u916,negated_conjecture,
( ssSkP543(X0)
| ~ ssSkP558(X0) ) ).
cnf(u920,negated_conjecture,
( ssPv12(X0)
| ~ ssSkP558(X0) ) ).
cnf(u924,negated_conjecture,
( ssSkP516(X0)
| ~ ssSkP559(X0) ) ).
cnf(u928,negated_conjecture,
( ssSkP556(X0)
| ~ ssSkP559(X0) ) ).
cnf(u932,negated_conjecture,
( ssSkP573(X0)
| ~ ssSkP574(X0) ) ).
cnf(u936,negated_conjecture,
( ssSkP575(X0)
| ~ ssSkP576(X0) ) ).
cnf(u940,negated_conjecture,
( ssSkP577(X0)
| ~ ssSkP578(X0) ) ).
cnf(u944,negated_conjecture,
( ssSkP579(X0)
| ~ ssSkP580(X0) ) ).
cnf(u948,negated_conjecture,
( ssSkP581(X0)
| ~ ssSkP582(X0) ) ).
cnf(u952,negated_conjecture,
( ssSkP572(X0)
| ~ ssSkP584(X0) ) ).
cnf(u956,negated_conjecture,
( ssSkP583(X0)
| ~ ssSkP584(X0) ) ).
cnf(u960,negated_conjecture,
( ssSkP585(X0)
| ~ ssSkP586(X0) ) ).
cnf(u964,negated_conjecture,
( ssSkP571(X0)
| ~ ssSkP588(X0) ) ).
cnf(u968,negated_conjecture,
( ssSkP587(X0)
| ~ ssSkP588(X0) ) ).
cnf(u972,negated_conjecture,
( ssSkP570(X0)
| ~ ssSkP590(X0) ) ).
cnf(u976,negated_conjecture,
( ssSkP589(X0)
| ~ ssSkP590(X0) ) ).
cnf(u980,negated_conjecture,
( ssSkP591(X0)
| ~ ssSkP592(X0) ) ).
cnf(u984,negated_conjecture,
( ssSkP569(X0)
| ~ ssSkP594(X0) ) ).
cnf(u988,negated_conjecture,
( ssSkP593(X0)
| ~ ssSkP594(X0) ) ).
cnf(u992,negated_conjecture,
( ssSkP595(X0)
| ~ ssSkP596(X0) ) ).
cnf(u996,negated_conjecture,
( ssSkP568(X0)
| ~ ssSkP598(X0) ) ).
cnf(u1000,negated_conjecture,
( ssSkP597(X0)
| ~ ssSkP598(X0) ) ).
cnf(u1004,negated_conjecture,
( ssSkP599(X0)
| ~ ssSkP600(X0) ) ).
cnf(u1008,negated_conjecture,
( ssSkP601(X0)
| ~ ssSkP602(X0) ) ).
cnf(u1012,negated_conjecture,
( ssSkP603(X0)
| ~ ssSkP604(X0) ) ).
cnf(u1016,negated_conjecture,
( ssSkP605(X0)
| ~ ssSkP606(X0) ) ).
cnf(u1020,negated_conjecture,
( ssSkP607(X0)
| ~ ssSkP608(X0) ) ).
cnf(u1024,negated_conjecture,
( ssSkP609(X0)
| ~ ssSkP610(X0) ) ).
cnf(u1028,negated_conjecture,
( ssSkP611(X0)
| ~ ssSkP612(X0) ) ).
cnf(u1032,negated_conjecture,
( ssSkP613(X0)
| ~ ssSkP614(X0) ) ).
cnf(u1036,negated_conjecture,
( ssSkP567(X0)
| ~ ssSkP616(X0) ) ).
cnf(u1040,negated_conjecture,
( ssSkP615(X0)
| ~ ssSkP616(X0) ) ).
cnf(u1044,negated_conjecture,
( ssSkP617(X0)
| ~ ssSkP618(X0) ) ).
cnf(u1048,negated_conjecture,
( ssSkP619(X0)
| ~ ssSkP620(X0) ) ).
cnf(u1052,negated_conjecture,
( ssSkP566(X0)
| ~ ssSkP622(X0) ) ).
cnf(u1056,negated_conjecture,
( ssSkP621(X0)
| ~ ssSkP622(X0) ) ).
cnf(u1060,negated_conjecture,
( ssSkP565(X0)
| ~ ssSkP624(X0) ) ).
cnf(u1064,negated_conjecture,
( ssSkP623(X0)
| ~ ssSkP624(X0) ) ).
cnf(u1068,negated_conjecture,
( ssSkP564(X0)
| ~ ssSkP626(X0) ) ).
cnf(u1072,negated_conjecture,
( ssSkP625(X0)
| ~ ssSkP626(X0) ) ).
cnf(u1076,negated_conjecture,
( ssSkP627(X0)
| ~ ssSkP628(X0) ) ).
cnf(u1080,negated_conjecture,
( ssSkP629(X0)
| ~ ssSkP630(X0) ) ).
cnf(u1084,negated_conjecture,
( ssSkP631(X0)
| ~ ssSkP632(X0) ) ).
cnf(u1088,negated_conjecture,
( ssSkP633(X0)
| ~ ssSkP634(X0) ) ).
cnf(u1092,negated_conjecture,
( ssSkP635(X0)
| ~ ssSkP636(X0) ) ).
cnf(u1096,negated_conjecture,
( ssSkP637(X0)
| ~ ssSkP638(X0) ) ).
cnf(u1100,negated_conjecture,
( ssSkP639(X0)
| ~ ssSkP640(X0) ) ).
cnf(u1104,negated_conjecture,
( ssSkP641(X0)
| ~ ssSkP642(X0) ) ).
cnf(u1108,negated_conjecture,
( ssSkP643(X0)
| ~ ssSkP644(X0) ) ).
cnf(u1112,negated_conjecture,
( ssSkP645(X0)
| ~ ssSkP646(X0) ) ).
cnf(u1116,negated_conjecture,
( ssSkP563(X0)
| ~ ssSkP648(X0) ) ).
cnf(u1120,negated_conjecture,
( ssSkP647(X0)
| ~ ssSkP648(X0) ) ).
cnf(u1124,negated_conjecture,
( ssSkP649(X0)
| ~ ssSkP650(X0) ) ).
cnf(u1128,negated_conjecture,
( ssSkP651(X0)
| ~ ssSkP652(X0) ) ).
cnf(u1132,negated_conjecture,
( ssSkP653(X0)
| ~ ssSkP654(X0) ) ).
cnf(u1136,negated_conjecture,
( ssSkP655(X0)
| ~ ssSkP656(X0) ) ).
cnf(u1140,negated_conjecture,
( ssSkP562(X0)
| ~ ssSkP658(X0) ) ).
cnf(u1144,negated_conjecture,
( ssSkP657(X0)
| ~ ssSkP658(X0) ) ).
cnf(u1148,negated_conjecture,
( ssSkP561(X0)
| ~ ssSkP660(X0) ) ).
cnf(u1152,negated_conjecture,
( ssSkP659(X0)
| ~ ssSkP660(X0) ) ).
cnf(u1156,negated_conjecture,
( ssSkP560(X0)
| ~ ssSkP662(X0) ) ).
cnf(u1160,negated_conjecture,
( ssSkP661(X0)
| ~ ssSkP662(X0) ) ).
cnf(u1164,negated_conjecture,
( ssSkP663(X0)
| ~ ssSkP664(X0) ) ).
cnf(u1168,negated_conjecture,
( ssSkP665(X0)
| ~ ssSkP666(X0) ) ).
cnf(u1172,negated_conjecture,
( ssSkP667(X0)
| ~ ssSkP668(X0) ) ).
cnf(u1176,negated_conjecture,
( ssSkP669(X0)
| ~ ssSkP670(X0) ) ).
cnf(u1180,negated_conjecture,
( ssSkP671(X0)
| ~ ssSkP672(X0) ) ).
cnf(u1184,negated_conjecture,
( ssSkP673(X0)
| ~ ssSkP674(X0) ) ).
cnf(u1188,negated_conjecture,
( ssSkP675(X0)
| ~ ssSkP676(X0) ) ).
cnf(u1192,negated_conjecture,
( ssSkP677(X0)
| ~ ssSkP678(X0) ) ).
cnf(u1196,negated_conjecture,
( ssSkP518(skf94(X0))
| ~ ssSkP532(X0) ) ).
cnf(u1200,negated_conjecture,
( ssSkP529(skf95(X0))
| ~ ssSkP533(X0) ) ).
cnf(u1204,negated_conjecture,
( ssSkP524(skf96(X0))
| ~ ssSkP534(X0) ) ).
cnf(u1208,negated_conjecture,
( ssSkP522(skf97(X0))
| ~ ssSkP535(X0) ) ).
cnf(u1212,negated_conjecture,
( ssSkP528(skf98(X0))
| ~ ssSkP536(X0) ) ).
cnf(u1216,negated_conjecture,
( ssSkP520(skf99(X0))
| ~ ssSkP537(X0) ) ).
cnf(u1220,negated_conjecture,
( ssSkP526(skf100(X0))
| ~ ssSkP538(X0) ) ).
cnf(u1224,negated_conjecture,
( ssSkP525(skf101(X0))
| ~ ssSkP539(X0) ) ).
cnf(u1228,negated_conjecture,
( ssSkP521(skf102(X0))
| ~ ssSkP540(X0) ) ).
cnf(u1232,negated_conjecture,
( ssSkP530(skf103(X0))
| ~ ssSkP541(X0) ) ).
cnf(u1236,negated_conjecture,
( ssSkP519(skf104(X0))
| ~ ssSkP542(X0) ) ).
cnf(u1240,negated_conjecture,
( ssSkP527(skf105(X0))
| ~ ssSkP543(X0) ) ).
cnf(u1244,negated_conjecture,
( ssSkP523(skf106(X0))
| ~ ssSkP544(X0) ) ).
cnf(u1248,negated_conjecture,
( ssSkP545(skf107(X0))
| ~ ssSkP560(X0) ) ).
cnf(u1252,negated_conjecture,
( ssSkP547(skf108(X0))
| ~ ssSkP561(X0) ) ).
cnf(u1256,negated_conjecture,
( ssSkP549(skf109(X0))
| ~ ssSkP562(X0) ) ).
cnf(u1260,negated_conjecture,
( ssSkP551(skf110(X0))
| ~ ssSkP563(X0) ) ).
cnf(u1264,negated_conjecture,
( ssSkP553(skf111(X0))
| ~ ssSkP564(X0) ) ).
cnf(u1268,negated_conjecture,
( ssSkP555(skf112(X0))
| ~ ssSkP565(X0) ) ).
cnf(u1272,negated_conjecture,
( ssSkP557(skf113(X0))
| ~ ssSkP566(X0) ) ).
cnf(u1276,negated_conjecture,
( ssSkP546(skf114(X0))
| ~ ssSkP567(X0) ) ).
cnf(u1280,negated_conjecture,
( ssSkP550(skf115(X0))
| ~ ssSkP568(X0) ) ).
cnf(u1284,negated_conjecture,
( ssSkP554(skf116(X0))
| ~ ssSkP569(X0) ) ).
cnf(u1288,negated_conjecture,
( ssSkP558(skf117(X0))
| ~ ssSkP570(X0) ) ).
cnf(u1292,negated_conjecture,
( ssSkP552(skf118(X0))
| ~ ssSkP571(X0) ) ).
cnf(u1296,negated_conjecture,
( ssSkP548(skf119(X0))
| ~ ssSkP572(X0) ) ).
cnf(u1300,negated_conjecture,
( ~ ssPv48(skf81(X0))
| ~ ssSkP518(X0) ) ).
cnf(u1304,negated_conjecture,
( ~ ssPv9(skf82(X0))
| ~ ssSkP519(X0) ) ).
cnf(u1308,negated_conjecture,
( ~ ssPv11(skf83(X0))
| ~ ssSkP520(X0) ) ).
cnf(u1312,negated_conjecture,
( ~ ssPv28(skf84(X0))
| ~ ssSkP521(X0) ) ).
cnf(u1316,negated_conjecture,
( ~ ssPv47(skf85(X0))
| ~ ssSkP522(X0) ) ).
cnf(u1320,negated_conjecture,
( ~ ssPv30(skf86(X0))
| ~ ssSkP523(X0) ) ).
cnf(u1324,negated_conjecture,
( ~ ssPv14(skf87(X0))
| ~ ssSkP524(X0) ) ).
cnf(u1328,negated_conjecture,
( ~ ssPv16(skf88(X0))
| ~ ssSkP525(X0) ) ).
cnf(u1332,negated_conjecture,
( ~ ssPv46(skf89(X0))
| ~ ssSkP526(X0) ) ).
cnf(u1336,negated_conjecture,
( ~ ssPv12(skf90(X0))
| ~ ssSkP527(X0) ) ).
cnf(u1340,negated_conjecture,
( ~ ssPv29(skf91(X0))
| ~ ssSkP528(X0) ) ).
cnf(u1344,negated_conjecture,
( ~ ssPv25(skf92(X0))
| ~ ssSkP529(X0) ) ).
cnf(u1348,negated_conjecture,
( ~ ssPv41(skf93(X0))
| ~ ssSkP530(X0) ) ).
cnf(u1365,negated_conjecture,
( ~ ssSkP545(skf81(X0))
| ~ ssSkP518(X0) ) ).
cnf(u1369,negated_conjecture,
( ~ ssSkP548(skf82(X0))
| ~ ssSkP519(X0) ) ).
cnf(u1373,negated_conjecture,
( ~ ssSkP552(skf83(X0))
| ~ ssSkP520(X0) ) ).
cnf(u1377,negated_conjecture,
( ~ ssSkP557(skf84(X0))
| ~ ssSkP521(X0) ) ).
cnf(u1381,negated_conjecture,
( ~ ssSkP547(skf85(X0))
| ~ ssSkP522(X0) ) ).
cnf(u1385,negated_conjecture,
( ~ ssSkP553(skf86(X0))
| ~ ssSkP523(X0) ) ).
cnf(u1389,negated_conjecture,
( ~ ssSkP554(skf87(X0))
| ~ ssSkP524(X0) ) ).
cnf(u1393,negated_conjecture,
( ~ ssSkP550(skf88(X0))
| ~ ssSkP525(X0) ) ).
cnf(u1397,negated_conjecture,
( ~ ssSkP549(skf89(X0))
| ~ ssSkP526(X0) ) ).
cnf(u1401,negated_conjecture,
( ~ ssSkP558(skf90(X0))
| ~ ssSkP527(X0) ) ).
cnf(u1405,negated_conjecture,
( ~ ssSkP555(skf91(X0))
| ~ ssSkP528(X0) ) ).
cnf(u1409,negated_conjecture,
( ~ ssSkP546(skf92(X0))
| ~ ssSkP529(X0) ) ).
cnf(u1413,negated_conjecture,
( ~ ssSkP551(skf93(X0))
| ~ ssSkP530(X0) ) ).
cnf(u1417,negated_conjecture,
( ssRr(X0,skf80(X0))
| ~ ssSkP516(X0) ) ).
cnf(u1421,negated_conjecture,
( ssRr(X0,skf81(X0))
| ~ ssSkP518(X0) ) ).
cnf(u1425,negated_conjecture,
( ssRr(X0,skf82(X0))
| ~ ssSkP519(X0) ) ).
cnf(u1429,negated_conjecture,
( ssRr(X0,skf83(X0))
| ~ ssSkP520(X0) ) ).
cnf(u1433,negated_conjecture,
( ssRr(X0,skf84(X0))
| ~ ssSkP521(X0) ) ).
cnf(u1437,negated_conjecture,
( ssRr(X0,skf85(X0))
| ~ ssSkP522(X0) ) ).
cnf(u1441,negated_conjecture,
( ssRr(X0,skf86(X0))
| ~ ssSkP523(X0) ) ).
cnf(u1445,negated_conjecture,
( ssRr(X0,skf87(X0))
| ~ ssSkP524(X0) ) ).
cnf(u1449,negated_conjecture,
( ssRr(X0,skf88(X0))
| ~ ssSkP525(X0) ) ).
cnf(u1453,negated_conjecture,
( ssRr(X0,skf89(X0))
| ~ ssSkP526(X0) ) ).
cnf(u1457,negated_conjecture,
( ssRr(X0,skf90(X0))
| ~ ssSkP527(X0) ) ).
cnf(u1461,negated_conjecture,
( ssRr(X0,skf91(X0))
| ~ ssSkP528(X0) ) ).
cnf(u1465,negated_conjecture,
( ssRr(X0,skf92(X0))
| ~ ssSkP529(X0) ) ).
cnf(u1469,negated_conjecture,
( ssRr(X0,skf93(X0))
| ~ ssSkP530(X0) ) ).
cnf(u1473,negated_conjecture,
( ssRr(skf94(X0),X0)
| ~ ssSkP532(X0) ) ).
cnf(u1477,negated_conjecture,
( ssRr(skf95(X0),X0)
| ~ ssSkP533(X0) ) ).
cnf(u1481,negated_conjecture,
( ssRr(skf96(X0),X0)
| ~ ssSkP534(X0) ) ).
cnf(u1485,negated_conjecture,
( ssRr(skf97(X0),X0)
| ~ ssSkP535(X0) ) ).
cnf(u1489,negated_conjecture,
( ssRr(skf98(X0),X0)
| ~ ssSkP536(X0) ) ).
cnf(u1493,negated_conjecture,
( ssRr(skf99(X0),X0)
| ~ ssSkP537(X0) ) ).
cnf(u1497,negated_conjecture,
( ssRr(skf100(X0),X0)
| ~ ssSkP538(X0) ) ).
cnf(u1501,negated_conjecture,
( ssRr(skf101(X0),X0)
| ~ ssSkP539(X0) ) ).
cnf(u1505,negated_conjecture,
( ssRr(skf102(X0),X0)
| ~ ssSkP540(X0) ) ).
cnf(u1509,negated_conjecture,
( ssRr(skf103(X0),X0)
| ~ ssSkP541(X0) ) ).
cnf(u1513,negated_conjecture,
( ssRr(skf104(X0),X0)
| ~ ssSkP542(X0) ) ).
cnf(u1517,negated_conjecture,
( ssRr(skf105(X0),X0)
| ~ ssSkP543(X0) ) ).
cnf(u1521,negated_conjecture,
( ssRr(skf106(X0),X0)
| ~ ssSkP544(X0) ) ).
cnf(u1525,negated_conjecture,
( ssRr(X0,skf107(X0))
| ~ ssSkP560(X0) ) ).
cnf(u1529,negated_conjecture,
( ssRr(X0,skf108(X0))
| ~ ssSkP561(X0) ) ).
cnf(u1533,negated_conjecture,
( ssRr(X0,skf109(X0))
| ~ ssSkP562(X0) ) ).
cnf(u1537,negated_conjecture,
( ssRr(X0,skf110(X0))
| ~ ssSkP563(X0) ) ).
cnf(u1541,negated_conjecture,
( ssRr(X0,skf111(X0))
| ~ ssSkP564(X0) ) ).
cnf(u1545,negated_conjecture,
( ssRr(X0,skf112(X0))
| ~ ssSkP565(X0) ) ).
cnf(u1549,negated_conjecture,
( ssRr(X0,skf113(X0))
| ~ ssSkP566(X0) ) ).
cnf(u1553,negated_conjecture,
( ssRr(X0,skf114(X0))
| ~ ssSkP567(X0) ) ).
cnf(u1557,negated_conjecture,
( ssRr(X0,skf115(X0))
| ~ ssSkP568(X0) ) ).
cnf(u1561,negated_conjecture,
( ssRr(X0,skf116(X0))
| ~ ssSkP569(X0) ) ).
cnf(u1565,negated_conjecture,
( ssRr(X0,skf117(X0))
| ~ ssSkP570(X0) ) ).
cnf(u1569,negated_conjecture,
( ssRr(X0,skf118(X0))
| ~ ssSkP571(X0) ) ).
cnf(u1573,negated_conjecture,
( ssRr(X0,skf119(X0))
| ~ ssSkP572(X0) ) ).
cnf(u1577,negated_conjecture,
( ssRr(X0,skf120(X0))
| ~ ssSkP574(X0) ) ).
cnf(u1581,negated_conjecture,
( ssRr(X0,skf121(X0))
| ~ ssSkP576(X0) ) ).
cnf(u1585,negated_conjecture,
( ssRr(X0,skf122(X0))
| ~ ssSkP578(X0) ) ).
cnf(u1589,negated_conjecture,
( ssRr(X0,skf123(X0))
| ~ ssSkP580(X0) ) ).
cnf(u1593,negated_conjecture,
( ssRr(X0,skf124(X0))
| ~ ssSkP582(X0) ) ).
cnf(u1597,negated_conjecture,
( ssRr(X0,skf125(X0))
| ~ ssSkP586(X0) ) ).
cnf(u1601,negated_conjecture,
( ssRr(X0,skf126(X0))
| ~ ssSkP592(X0) ) ).
cnf(u1605,negated_conjecture,
( ssRr(X0,skf127(X0))
| ~ ssSkP596(X0) ) ).
cnf(u1609,negated_conjecture,
( ssRr(X0,skf128(X0))
| ~ ssSkP600(X0) ) ).
cnf(u1613,negated_conjecture,
( ssRr(X0,skf129(X0))
| ~ ssSkP602(X0) ) ).
cnf(u1617,negated_conjecture,
( ssRr(X0,skf130(X0))
| ~ ssSkP604(X0) ) ).
cnf(u1621,negated_conjecture,
( ssRr(X0,skf131(X0))
| ~ ssSkP606(X0) ) ).
cnf(u1625,negated_conjecture,
( ssRr(X0,skf132(X0))
| ~ ssSkP608(X0) ) ).
cnf(u1629,negated_conjecture,
( ssRr(X0,skf133(X0))
| ~ ssSkP610(X0) ) ).
cnf(u1633,negated_conjecture,
( ssRr(X0,skf134(X0))
| ~ ssSkP612(X0) ) ).
cnf(u1637,negated_conjecture,
( ssRr(X0,skf135(X0))
| ~ ssSkP614(X0) ) ).
cnf(u1641,negated_conjecture,
( ssRr(X0,skf136(X0))
| ~ ssSkP618(X0) ) ).
cnf(u1645,negated_conjecture,
( ssRr(X0,skf137(X0))
| ~ ssSkP620(X0) ) ).
cnf(u1649,negated_conjecture,
( ssRr(X0,skf138(X0))
| ~ ssSkP628(X0) ) ).
cnf(u1653,negated_conjecture,
( ssRr(X0,skf139(X0))
| ~ ssSkP630(X0) ) ).
cnf(u1657,negated_conjecture,
( ssRr(X0,skf140(X0))
| ~ ssSkP632(X0) ) ).
cnf(u1661,negated_conjecture,
( ssRr(X0,skf141(X0))
| ~ ssSkP634(X0) ) ).
cnf(u1665,negated_conjecture,
( ssRr(X0,skf142(X0))
| ~ ssSkP636(X0) ) ).
cnf(u1669,negated_conjecture,
( ssRr(X0,skf143(X0))
| ~ ssSkP638(X0) ) ).
cnf(u1673,negated_conjecture,
( ssRr(X0,skf144(X0))
| ~ ssSkP640(X0) ) ).
cnf(u1677,negated_conjecture,
( ssRr(X0,skf145(X0))
| ~ ssSkP642(X0) ) ).
cnf(u1681,negated_conjecture,
( ssRr(X0,skf146(X0))
| ~ ssSkP644(X0) ) ).
cnf(u1685,negated_conjecture,
( ssRr(X0,skf147(X0))
| ~ ssSkP646(X0) ) ).
cnf(u1689,negated_conjecture,
( ssRr(X0,skf148(X0))
| ~ ssSkP650(X0) ) ).
cnf(u1693,negated_conjecture,
( ssRr(X0,skf149(X0))
| ~ ssSkP652(X0) ) ).
cnf(u1697,negated_conjecture,
( ssRr(X0,skf150(X0))
| ~ ssSkP654(X0) ) ).
cnf(u1701,negated_conjecture,
( ssRr(X0,skf151(X0))
| ~ ssSkP656(X0) ) ).
cnf(u1705,negated_conjecture,
( ssRr(X0,skf152(X0))
| ~ ssSkP664(X0) ) ).
cnf(u1709,negated_conjecture,
( ssRr(X0,skf153(X0))
| ~ ssSkP666(X0) ) ).
cnf(u1713,negated_conjecture,
( ssRr(X0,skf154(X0))
| ~ ssSkP668(X0) ) ).
cnf(u1717,negated_conjecture,
( ssRr(X0,skf155(X0))
| ~ ssSkP670(X0) ) ).
cnf(u1721,negated_conjecture,
( ssRr(X0,skf156(X0))
| ~ ssSkP672(X0) ) ).
cnf(u1725,negated_conjecture,
( ssRr(X0,skf157(X0))
| ~ ssSkP674(X0) ) ).
cnf(u1729,negated_conjecture,
( ssRr(X0,skf158(X0))
| ~ ssSkP676(X0) ) ).
cnf(u1733,negated_conjecture,
( ssRr(X0,skf159(X0))
| ~ ssSkP678(X0) ) ).
cnf(u1737,negated_conjecture,
( ssSkP676(X0)
| ~ ssSkP677(X1)
| ~ ssSkP531(X0,X1) ) ).
cnf(u1741,negated_conjecture,
( ssSkP674(X0)
| ~ ssSkP675(X1)
| ~ ssSkP531(X0,X1) ) ).
cnf(u1745,negated_conjecture,
( ssSkP531(X2,X0)
| ~ ssSkP517(X2,X1)
| ~ ssRr(X0,X1) ) ).
cnf(u1749,negated_conjecture,
( ssSkP517(X2,X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ) ).
cnf(u1753,negated_conjecture,
( ssSkP672(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP673(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1757,negated_conjecture,
( ssSkP670(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP671(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1761,negated_conjecture,
( ssSkP668(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP669(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1765,negated_conjecture,
( ssSkP666(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP667(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1769,negated_conjecture,
( ssSkP664(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP665(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1773,negated_conjecture,
( ssSkP662(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP663(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1777,negated_conjecture,
( ssSkP660(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP661(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1781,negated_conjecture,
( ssSkP658(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP659(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1785,negated_conjecture,
( ssSkP656(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP657(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1789,negated_conjecture,
( ssSkP654(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP655(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1793,negated_conjecture,
( ssSkP652(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP653(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1797,negated_conjecture,
( ssSkP650(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP651(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1801,negated_conjecture,
( ssSkP648(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP649(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1805,negated_conjecture,
( ssSkP646(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP647(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1809,negated_conjecture,
( ssSkP644(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP645(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1813,negated_conjecture,
( ssSkP642(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP643(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1817,negated_conjecture,
( ssSkP640(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP641(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1821,negated_conjecture,
( ssSkP638(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP639(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1825,negated_conjecture,
( ssSkP636(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP637(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1829,negated_conjecture,
( ssSkP634(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP635(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1833,negated_conjecture,
( ssSkP632(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP633(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1837,negated_conjecture,
( ssSkP630(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP631(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1841,negated_conjecture,
( ssSkP628(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP629(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1845,negated_conjecture,
( ssSkP626(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP627(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1849,negated_conjecture,
( ssSkP624(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP625(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1853,negated_conjecture,
( ssSkP622(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP623(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1857,negated_conjecture,
( ssSkP620(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP621(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1861,negated_conjecture,
( ssSkP618(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP619(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1865,negated_conjecture,
( ssSkP616(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP617(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1869,negated_conjecture,
( ssSkP614(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP615(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1873,negated_conjecture,
( ssSkP612(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP613(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1877,negated_conjecture,
( ssSkP610(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP611(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1881,negated_conjecture,
( ssSkP608(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP609(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1885,negated_conjecture,
( ssSkP606(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP607(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1889,negated_conjecture,
( ssSkP604(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP605(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1893,negated_conjecture,
( ssSkP602(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP603(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1897,negated_conjecture,
( ssSkP600(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP601(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1901,negated_conjecture,
( ssSkP598(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP599(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1905,negated_conjecture,
( ssSkP596(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP597(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1909,negated_conjecture,
( ssSkP594(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP595(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1913,negated_conjecture,
( ssSkP592(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP593(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1917,negated_conjecture,
( ssSkP590(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP591(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1921,negated_conjecture,
( ssSkP588(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP589(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1925,negated_conjecture,
( ssSkP586(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP587(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1929,negated_conjecture,
( ssSkP584(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP585(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1933,negated_conjecture,
( ssSkP582(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP583(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1937,negated_conjecture,
( ssSkP580(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP581(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1941,negated_conjecture,
( ssSkP578(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP579(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1945,negated_conjecture,
( ssSkP576(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP577(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1949,negated_conjecture,
( ssSkP574(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP575(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1953,negated_conjecture,
( ssSkP559(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP573(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1957,negated_conjecture,
( ssSkP516(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP556(X3)
| ~ ssRr(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN905-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.17 % Computer : n014.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 17:11:00 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 Running first-order theorem proving
% 0.10/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.65/1.91 % (1924348)Input is clausal, will run a generic CNF schedule.
% 9.65/1.91 % (1924358)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3164993338:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.65/1.91 % (1924358)Refutation not found, incomplete strategy
% 9.65/1.91 % (1924358)------------------------------
% 9.65/1.91 % (1924358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/1.91 % (1924358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/1.91 % (1924358)CaDiCaL version: 2.1.3
% 9.65/1.91 % (1924358)Termination reason: Refutation not found, incomplete strategy
% 9.65/1.91 % (1924358)Time elapsed: 0.006 s
% 9.65/1.91 % (1924358)Peak memory usage: 89 MB
% 9.65/1.91 % (1924358)Instructions burned: 17 (million)
% 9.65/1.91 % (1924356)lrs+10_1_sil=8000:sp=occurrence:random_seed=2852826112:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.65/1.91 % (1924355)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2069461145:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.65/1.91 % (1924359)dis-21_1_sil=8000:lcm=predicate:random_seed=3807419230: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)
% 9.65/1.91 % (1924353)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=3768757211:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.65/1.91 % (1924354)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3871629350:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.65/1.91 % (1924357)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1509812450:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.65/1.91 % (1924359)Instruction limit reached!
% 9.65/1.91 % (1924359)------------------------------
% 9.65/1.91 % (1924359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/1.91 % (1924359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/1.91 % (1924359)CaDiCaL version: 2.1.3
% 9.65/1.91 % (1924359)Termination reason: Instruction limit
% 9.65/1.91 % (1924359)Termination phase: Saturation
% 9.65/1.91 % (1924359)Time elapsed: 0.042 s
% 9.65/1.91 % (1924359)Peak memory usage: 89 MB
% 9.65/1.91 % (1924359)Instructions burned: 117 (million)
% 9.65/1.91 % (1924356)Instruction limit reached!
% 9.65/1.91 % (1924356)------------------------------
% 9.65/1.91 % (1924356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/1.91 % (1924356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/1.91 % (1924356)CaDiCaL version: 2.1.3
% 9.65/1.91 % (1924356)Termination reason: Instruction limit
% 9.65/1.91 % (1924356)Termination phase: Saturation
% 9.65/1.91 % (1924356)Time elapsed: 0.047 s
% 9.65/1.91 % (1924356)Peak memory usage: 90 MB
% 9.65/1.91 % (1924356)Instructions burned: 107 (million)
% 9.65/1.91 % (1924357)Instruction limit reached!
% 9.65/1.91 % (1924357)------------------------------
% 9.65/1.91 % (1924357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.65/1.91 % (1924357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.65/1.91 % (1924357)CaDiCaL version: 2.1.3
% 9.65/1.91 % (1924357)Termination reason: Instruction limit
% 9.65/1.91 % (1924357)Termination phase: Saturation
% 9.65/1.91 % (1924357)Time elapsed: 0.052 s
% 9.65/1.91 % (1924357)Peak memory usage: 89 MB
% 9.65/1.91 % (1924357)Instructions burned: 117 (million)
% 9.65/1.91 % (1924358)------------------------------
% 9.65/1.91 % (1924358)------------------------------
% 9.65/1.91 % (1924367)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=2367806534:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.65/1.91 % (1924368)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3586705674: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)
% 9.65/1.91 % (1924369)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=995975918:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.65/1.91 % (1924370)lrs+10_64_to=lpo:sil=8000:random_seed=2714510788:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 5.21/2.31 % (1924367)Instruction limit reached!
% 5.21/2.31 % (1924367)------------------------------
% 5.21/2.31 % (1924367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924367)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924367)Termination reason: Instruction limit
% 5.21/2.31 % (1924367)Termination phase: Saturation
% 5.21/2.31 % (1924367)Time elapsed: 0.066 s
% 5.21/2.31 % (1924367)Peak memory usage: 90 MB
% 5.21/2.31 % (1924367)Instructions burned: 145 (million)
% 5.21/2.31 % (1924370)Instruction limit reached!
% 5.21/2.31 % (1924370)------------------------------
% 5.21/2.31 % (1924370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924370)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924370)Termination reason: Instruction limit
% 5.21/2.31 % (1924370)Termination phase: Saturation
% 5.21/2.31 % (1924370)Time elapsed: 0.037 s
% 5.21/2.31 % (1924370)Peak memory usage: 94 MB
% 5.21/2.31 % (1924370)Instructions burned: 127 (million)
% 5.21/2.31 % (1924368)Instruction limit reached!
% 5.21/2.31 % (1924368)------------------------------
% 5.21/2.31 % (1924368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924368)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924368)Termination reason: Instruction limit
% 5.21/2.31 % (1924368)Termination phase: Saturation
% 5.21/2.31 % (1924368)Time elapsed: 0.094 s
% 5.21/2.31 % (1924368)Peak memory usage: 89 MB
% 5.21/2.31 % (1924368)Instructions burned: 189 (million)
% 5.21/2.31 % (1924369)Instruction limit reached!
% 5.21/2.31 % (1924369)------------------------------
% 5.21/2.31 % (1924369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924369)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924369)Termination reason: Instruction limit
% 5.21/2.31 % (1924369)Termination phase: Saturation
% 5.21/2.31 % (1924369)Time elapsed: 0.095 s
% 5.21/2.31 % (1924369)Peak memory usage: 92 MB
% 5.21/2.31 % (1924369)Instructions burned: 221 (million)
% 5.21/2.31 % (1924376)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2938965420:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.21/2.31 % (1924375)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3853810190:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.21/2.31 % (1924375)Refutation not found, incomplete strategy
% 5.21/2.31 % (1924375)------------------------------
% 5.21/2.31 % (1924375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924375)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924375)Termination reason: Refutation not found, incomplete strategy
% 5.21/2.31 % (1924375)Time elapsed: 0.007 s
% 5.21/2.31 % (1924375)Peak memory usage: 89 MB
% 5.21/2.31 % (1924375)Instructions burned: 11 (million)
% 5.21/2.31 % (1924377)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=911888098:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.21/2.31 % (1924376)Instruction limit reached!
% 5.21/2.31 % (1924376)------------------------------
% 5.21/2.31 % (1924376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924376)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924376)Termination reason: Instruction limit
% 5.21/2.31 % (1924376)Termination phase: Saturation
% 5.21/2.31 % (1924376)Time elapsed: 0.040 s
% 5.21/2.31 % (1924376)Peak memory usage: 91 MB
% 5.21/2.31 % (1924376)Instructions burned: 174 (million)
% 5.21/2.31 % (1924378)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3846431152:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 5.21/2.31 % (1924378)Instruction limit reached!
% 5.21/2.31 % (1924378)------------------------------
% 5.21/2.31 % (1924378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924378)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924378)Termination reason: Instruction limit
% 5.21/2.31 % (1924378)Termination phase: Saturation
% 5.21/2.31 % (1924378)Time elapsed: 0.056 s
% 5.21/2.31 % (1924378)Peak memory usage: 91 MB
% 5.21/2.31 % (1924378)Instructions burned: 107 (million)
% 5.21/2.31 % (1924382)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1455951178:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.21/2.31 % (1924382)Instruction limit reached!
% 5.21/2.31 % (1924382)------------------------------
% 5.21/2.31 % (1924382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924382)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924382)Termination reason: Instruction limit
% 5.21/2.31 % (1924382)Termination phase: Saturation
% 5.21/2.31 % (1924382)Time elapsed: 0.033 s
% 5.21/2.31 % (1924382)Peak memory usage: 93 MB
% 5.21/2.31 % (1924382)Instructions burned: 108 (million)
% 5.21/2.31 % (1924375)------------------------------
% 5.21/2.31 % (1924375)------------------------------
% 5.21/2.31 % (1924384)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2578352586:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 5.21/2.31 % (1924384)Refutation not found, incomplete strategy
% 5.21/2.31 % (1924384)------------------------------
% 5.21/2.31 % (1924384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924384)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924384)Termination reason: Refutation not found, incomplete strategy
% 5.21/2.31 % (1924384)Time elapsed: 0.011 s
% 5.21/2.31 % (1924384)Peak memory usage: 89 MB
% 5.21/2.31 % (1924384)Instructions burned: 22 (million)
% 5.21/2.31 % (1924386)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4169553773:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 5.21/2.31 % (1924387)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3632564644:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 5.21/2.31 % (1924387)Refutation not found, incomplete strategy
% 5.21/2.31 % (1924387)------------------------------
% 5.21/2.31 % (1924387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924387)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924387)Termination reason: Refutation not found, incomplete strategy
% 5.21/2.31 % (1924387)Time elapsed: 0.012 s
% 5.21/2.31 % (1924387)Peak memory usage: 89 MB
% 5.21/2.31 % (1924387)Instructions burned: 20 (million)
% 5.21/2.31 % (1924384)------------------------------
% 5.21/2.31 % (1924384)------------------------------
% 5.21/2.31 % (1924387)------------------------------
% 5.21/2.31 % (1924387)------------------------------
% 5.21/2.31 % (1924391)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=402803202:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 5.21/2.31 % (1924392)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=451260950:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 5.21/2.31 % (1924392)Instruction limit reached!
% 5.21/2.31 % (1924392)------------------------------
% 5.21/2.31 % (1924392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924392)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924392)Termination reason: Instruction limit
% 5.21/2.31 % (1924392)Termination phase: Saturation
% 5.21/2.31 % (1924392)Time elapsed: 0.086 s
% 5.21/2.31 % (1924392)Peak memory usage: 93 MB
% 5.21/2.31 % (1924392)Instructions burned: 193 (million)
% 5.21/2.31 % (1924391)Instruction limit reached!
% 5.21/2.31 % (1924391)------------------------------
% 5.21/2.31 % (1924391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924391)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924391)Termination reason: Instruction limit
% 5.21/2.31 % (1924391)Termination phase: Saturation
% 5.21/2.31 % (1924391)Time elapsed: 0.244 s
% 5.21/2.31 % (1924391)Peak memory usage: 93 MB
% 5.21/2.31 % (1924391)Instructions burned: 501 (million)
% 5.21/2.31 % (1924395)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2511068888:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 5.21/2.31 % (1924395)First to succeed.
% 5.21/2.31 % (1924395)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1924348"
% 5.21/2.31 % (1924396)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2342728832:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 5.21/2.31 % (1924396)Instruction limit reached!
% 5.21/2.31 % (1924396)------------------------------
% 5.21/2.31 % (1924396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.21/2.31 % (1924396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.21/2.31 % (1924396)CaDiCaL version: 2.1.3
% 5.21/2.31 % (1924396)Termination reason: Instruction limit
% 5.21/2.31 % (1924396)Termination phase: Saturation
% 5.21/2.31 % (1924396)Time elapsed: 0.065 s
% 5.21/2.31 % (1924396)Peak memory usage: 89 MB
% 5.21/2.31 % (1924396)Instructions burned: 157 (million)
% 5.21/2.31 % (1924399)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1629178567:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 5.21/2.31 % SZS status Satisfiable for theBenchmark
% 5.21/2.31 % SZS output start Saturation.
% See solution above
% 5.21/2.32 % SZS output start Definitions and Model Updates.
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv20(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv34(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv24(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv17(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv53(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP191(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP192(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkC4 := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP236(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP235(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP234(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP233(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP232(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP231(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP230(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP229(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP228(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP227(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP226(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP225(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP224(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP223(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP222(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP221(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP220(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP219(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP218(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP217(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP216(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP215(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP214(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP213(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP212(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP211(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP210(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP209(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP208(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP207(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP206(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP205(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP204(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP203(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP202(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP201(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP200(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP193(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP194(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP195(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP196(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP197(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP198(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP199(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv22(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP237(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP238(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkC5 := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP287(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP286(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP285(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP284(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP283(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP282(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP281(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP280(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP279(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP278(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP277(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP276(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP275(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP274(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP273(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP272(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP271(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP270(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP269(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP268(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP239(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP240(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP241(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP242(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP243(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP244(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP245(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP246(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP247(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP248(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP249(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP250(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP251(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP252(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP253(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP254(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP255(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP256(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP257(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP258(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP259(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP260(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP261(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP262(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP263(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP264(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP265(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP266(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP267(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP288(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP289(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkC6 := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP347(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP346(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP345(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP344(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP343(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP342(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP341(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP340(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP339(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP338(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP337(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP336(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP335(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP334(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP333(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP332(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP331(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP330(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP329(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP456(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP457(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkC9 := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP515(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP514(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP513(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP512(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP511(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP510(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP509(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP508(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP507(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP506(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP505(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP504(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP503(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP502(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP501(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP500(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP499(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP498(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP497(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP496(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP495(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP494(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP493(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP492(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP491(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP490(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP489(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP488(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP487(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP486(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP485(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP484(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP483(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP482(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP481(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP480(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP479(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP478(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP477(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP476(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP475(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP474(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP473(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP472(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP471(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP470(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP469(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP468(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP467(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP466(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP465(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP464(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP463(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP462(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP461(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP460(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP459(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP458(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP0(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP1(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkC0 := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP59(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP58(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP57(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP56(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP55(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP54(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP53(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP52(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP51(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP50(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP49(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP48(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP47(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP46(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP45(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP44(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP43(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP42(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP41(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP40(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP39(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP38(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP37(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP36(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP35(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP34(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP33(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP32(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP31(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP30(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP29(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP28(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP27(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP26(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP25(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP24(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP23(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP22(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP21(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP20(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP19(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP18(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP17(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP16(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP15(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP14(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP13(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP12(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP11(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP10(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP9(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP8(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP7(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP6(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP5(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP4(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP3(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP2(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv2(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP290(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP291(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP292(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP293(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP294(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP295(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP296(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP297(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP298(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP299(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP300(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP301(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP302(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP303(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP304(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP305(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP306(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP307(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP308(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP309(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP310(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP311(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP312(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP313(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP314(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP315(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP316(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP317(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP318(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP319(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP320(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP321(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP322(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP323(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP324(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP325(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP326(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP327(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP328(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv39(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP101(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP102(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkC2 := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP148(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP147(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP146(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP145(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP144(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP143(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP142(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP141(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP149(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP150(X0,X1) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkC3 := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP190(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP189(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP188(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP187(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP186(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP185(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP184(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP183(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP182(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP181(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP180(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP179(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP178(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP177(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP176(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP175(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP174(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP173(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP172(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP171(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP170(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP169(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP168(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP167(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP151(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP152(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP153(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP154(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP155(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP156(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP157(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP158(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP159(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP160(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP161(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP162(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP163(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP164(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP165(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP166(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssPv36(X0) := $true
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP103(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP104(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP105(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP106(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP107(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP108(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP109(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP110(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP111(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP112(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP113(X0) := $false
% 5.21/2.32 for all inputs,
% 5.21/2.32 define ssSkP114(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP115(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP116(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP117(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP118(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP119(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP120(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP121(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP122(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP123(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP124(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP125(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP126(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP127(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP128(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP129(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP130(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP131(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP132(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP133(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP134(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP135(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP136(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP137(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP138(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP139(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP140(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssPv50(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssPv52(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP348(X0,X1) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP349(X0,X1) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkC7 := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP401(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP400(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP399(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP398(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP397(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP396(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP395(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP394(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP393(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP392(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP391(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP390(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP389(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP388(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP387(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP386(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP385(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP384(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP383(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP382(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP381(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP380(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP379(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP378(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP377(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP376(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP375(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP374(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP373(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP372(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP371(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP370(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP369(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP368(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP367(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP366(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP365(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP364(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP363(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP362(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP361(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP360(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP359(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP358(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP357(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP356(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP355(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP354(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP353(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP352(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP351(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP350(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP402(X0,X1) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP403(X0,X1) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkC8 := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP455(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP454(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP453(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP452(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP451(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP450(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP449(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP448(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP447(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP446(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP445(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP444(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP443(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP442(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP441(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP440(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP439(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP438(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP437(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP436(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP435(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP434(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP433(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP432(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP431(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP430(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP429(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP428(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP427(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP426(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP425(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP424(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP423(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP422(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP421(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP420(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP419(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP418(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP417(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP416(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP415(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP414(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP413(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP412(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP411(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP410(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP409(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP408(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP407(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP406(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP405(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP404(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssPv8(X0) := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP60(X0,X1) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP61(X0,X1) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkC1 := $false
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP100(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP99(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP98(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP97(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP96(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP95(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP94(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP93(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP92(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP91(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP90(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP89(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP88(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP87(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP86(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP85(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP84(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP83(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP82(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP81(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP80(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP79(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP78(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP77(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP76(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP75(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP74(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP73(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP72(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP71(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP70(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP69(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP68(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP67(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP66(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP65(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP64(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP63(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssSkP62(X0) := $true
% 0.17/2.50 for all inputs,
% 0.17/2.50 define ssPv21(X0) := $false
% 0.17/2.50 % SZS output end Definitions and Model Updates.
% 0.17/2.50 % (1924395)------------------------------
% 0.17/2.50 % (1924395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/2.50 % (1924395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/2.50 % (1924395)CaDiCaL version: 2.1.3
% 0.17/2.50 % (1924395)Termination reason: Satisfiable
% 0.17/2.50 % (1924395)Time elapsed: 0.017 s
% 0.17/2.50 % (1924395)Peak memory usage: 89 MB
% 0.17/2.50 % (1924395)Instructions burned: 29 (million)
% 0.17/2.50 % (1924395)------------------------------
% 0.17/2.50 % (1924395)------------------------------
% 0.17/2.50 % (1924348)Success in time 1.915 s
% 0.17/2.50 % Vampire exiting
%------------------------------------------------------------------------------