%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN909-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 : n005.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:57 PM UTC 2026
% Result : Satisfiable 12.80s 2.56s
% Output : Saturation 12.80s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1055,negated_conjecture,
~ ssSkC30 ).
cnf(u1060,negated_conjecture,
ssSkP913(skc61) ).
cnf(u1064,negated_conjecture,
( ssSkP824(X0)
| ~ ssSkP836(X0) ) ).
cnf(u1068,negated_conjecture,
( ssPv24(X0)
| ~ ssSkP836(X0) ) ).
cnf(u1072,negated_conjecture,
( ssSkP831(X0)
| ~ ssSkP837(X0) ) ).
cnf(u1076,negated_conjecture,
( ssPv5(X0)
| ~ ssSkP837(X0) ) ).
cnf(u1080,negated_conjecture,
( ssSkP827(X0)
| ~ ssSkP838(X0) ) ).
cnf(u1084,negated_conjecture,
( ssPv23(X0)
| ~ ssSkP838(X0) ) ).
cnf(u1088,negated_conjecture,
( ssSkP828(X0)
| ~ ssSkP839(X0) ) ).
cnf(u1092,negated_conjecture,
( ssPv13(X0)
| ~ ssSkP839(X0) ) ).
cnf(u1096,negated_conjecture,
( ssSkP830(X0)
| ~ ssSkP840(X0) ) ).
cnf(u1100,negated_conjecture,
( ssPv22(X0)
| ~ ssSkP840(X0) ) ).
cnf(u1104,negated_conjecture,
( ssSkP826(X0)
| ~ ssSkP841(X0) ) ).
cnf(u1108,negated_conjecture,
( ssPv6(X0)
| ~ ssSkP841(X0) ) ).
cnf(u1112,negated_conjecture,
( ssSkP833(X0)
| ~ ssSkP842(X0) ) ).
cnf(u1116,negated_conjecture,
( ssPv21(X0)
| ~ ssSkP842(X0) ) ).
cnf(u1120,negated_conjecture,
( ssSkP835(X0)
| ~ ssSkP843(X0) ) ).
cnf(u1124,negated_conjecture,
( ssPv8(X0)
| ~ ssSkP843(X0) ) ).
cnf(u1128,negated_conjecture,
( ssSkP825(X0)
| ~ ssSkP844(X0) ) ).
cnf(u1132,negated_conjecture,
( ssPv16(X0)
| ~ ssSkP844(X0) ) ).
cnf(u1136,negated_conjecture,
( ssSkP829(X0)
| ~ ssSkP846(X0) ) ).
cnf(u1140,negated_conjecture,
( ssPv15(X0)
| ~ ssSkP846(X0) ) ).
cnf(u1144,negated_conjecture,
( ssSkP832(X0)
| ~ ssSkP847(X0) ) ).
cnf(u1148,negated_conjecture,
( ssPv7(X0)
| ~ ssSkP847(X0) ) ).
cnf(u1152,negated_conjecture,
( ssSkP834(X0)
| ~ ssSkP848(X0) ) ).
cnf(u1156,negated_conjecture,
( ssPv14(X0)
| ~ ssSkP848(X0) ) ).
cnf(u1160,negated_conjecture,
( ssSkP809(X0)
| ~ ssSkP849(X0) ) ).
cnf(u1164,negated_conjecture,
( ssSkP845(X0)
| ~ ssSkP849(X0) ) ).
cnf(u1168,negated_conjecture,
( ssSkP862(X0)
| ~ ssSkP863(X0) ) ).
cnf(u1172,negated_conjecture,
( ssSkP864(X0)
| ~ ssSkP865(X0) ) ).
cnf(u1176,negated_conjecture,
( ssSkP861(X0)
| ~ ssSkP867(X0) ) ).
cnf(u1180,negated_conjecture,
( ssSkP866(X0)
| ~ ssSkP867(X0) ) ).
cnf(u1184,negated_conjecture,
( ssSkP860(X0)
| ~ ssSkP869(X0) ) ).
cnf(u1188,negated_conjecture,
( ssSkP868(X0)
| ~ ssSkP869(X0) ) ).
cnf(u1192,negated_conjecture,
( ssSkP859(X0)
| ~ ssSkP871(X0) ) ).
cnf(u1196,negated_conjecture,
( ssSkP870(X0)
| ~ ssSkP871(X0) ) ).
cnf(u1200,negated_conjecture,
( ssSkP858(X0)
| ~ ssSkP873(X0) ) ).
cnf(u1204,negated_conjecture,
( ssSkP872(X0)
| ~ ssSkP873(X0) ) ).
cnf(u1208,negated_conjecture,
( ssSkP874(X0)
| ~ ssSkP875(X0) ) ).
cnf(u1212,negated_conjecture,
( ssSkP876(X0)
| ~ ssSkP877(X0) ) ).
cnf(u1216,negated_conjecture,
( ssSkP878(X0)
| ~ ssSkP879(X0) ) ).
cnf(u1220,negated_conjecture,
( ssSkP880(X0)
| ~ ssSkP881(X0) ) ).
cnf(u1224,negated_conjecture,
( ssSkP857(X0)
| ~ ssSkP883(X0) ) ).
cnf(u1228,negated_conjecture,
( ssSkP882(X0)
| ~ ssSkP883(X0) ) ).
cnf(u1232,negated_conjecture,
( ssSkP856(X0)
| ~ ssSkP885(X0) ) ).
cnf(u1236,negated_conjecture,
( ssSkP884(X0)
| ~ ssSkP885(X0) ) ).
cnf(u1240,negated_conjecture,
( ssSkP855(X0)
| ~ ssSkP887(X0) ) ).
cnf(u1244,negated_conjecture,
( ssSkP886(X0)
| ~ ssSkP887(X0) ) ).
cnf(u1248,negated_conjecture,
( ssSkP854(X0)
| ~ ssSkP889(X0) ) ).
cnf(u1252,negated_conjecture,
( ssSkP888(X0)
| ~ ssSkP889(X0) ) ).
cnf(u1256,negated_conjecture,
( ssSkP890(X0)
| ~ ssSkP891(X0) ) ).
cnf(u1260,negated_conjecture,
( ssSkP892(X0)
| ~ ssSkP893(X0) ) ).
cnf(u1264,negated_conjecture,
( ssSkP894(X0)
| ~ ssSkP895(X0) ) ).
cnf(u1268,negated_conjecture,
( ssSkP896(X0)
| ~ ssSkP897(X0) ) ).
cnf(u1272,negated_conjecture,
( ssSkP853(X0)
| ~ ssSkP899(X0) ) ).
cnf(u1276,negated_conjecture,
( ssSkP898(X0)
| ~ ssSkP899(X0) ) ).
cnf(u1280,negated_conjecture,
( ssSkP852(X0)
| ~ ssSkP901(X0) ) ).
cnf(u1284,negated_conjecture,
( ssSkP900(X0)
| ~ ssSkP901(X0) ) ).
cnf(u1288,negated_conjecture,
( ssSkP851(X0)
| ~ ssSkP903(X0) ) ).
cnf(u1292,negated_conjecture,
( ssSkP902(X0)
| ~ ssSkP903(X0) ) ).
cnf(u1296,negated_conjecture,
( ssSkP850(X0)
| ~ ssSkP905(X0) ) ).
cnf(u1300,negated_conjecture,
( ssSkP904(X0)
| ~ ssSkP905(X0) ) ).
cnf(u1304,negated_conjecture,
( ssSkP906(X0)
| ~ ssSkP907(X0) ) ).
cnf(u1308,negated_conjecture,
( ssSkP908(X0)
| ~ ssSkP909(X0) ) ).
cnf(u1312,negated_conjecture,
( ssSkP910(X0)
| ~ ssSkP911(X0) ) ).
cnf(u1316,negated_conjecture,
( ssSkP912(X0)
| ~ ssSkP913(X0) ) ).
cnf(u1320,negated_conjecture,
( ssSkP811(skf64(X0))
| ~ ssSkP824(X0) ) ).
cnf(u1324,negated_conjecture,
( ssSkP817(skf65(X0))
| ~ ssSkP825(X0) ) ).
cnf(u1328,negated_conjecture,
( ssSkP821(skf66(X0))
| ~ ssSkP826(X0) ) ).
cnf(u1332,negated_conjecture,
( ssSkP815(skf67(X0))
| ~ ssSkP827(X0) ) ).
cnf(u1336,negated_conjecture,
( ssSkP814(skf68(X0))
| ~ ssSkP828(X0) ) ).
cnf(u1340,negated_conjecture,
( ssSkP822(skf69(X0))
| ~ ssSkP829(X0) ) ).
cnf(u1344,negated_conjecture,
( ssSkP819(skf70(X0))
| ~ ssSkP830(X0) ) ).
cnf(u1348,negated_conjecture,
( ssSkP820(skf71(X0))
| ~ ssSkP831(X0) ) ).
cnf(u1352,negated_conjecture,
( ssSkP816(skf72(X0))
| ~ ssSkP832(X0) ) ).
cnf(u1356,negated_conjecture,
( ssSkP812(skf73(X0))
| ~ ssSkP833(X0) ) ).
cnf(u1360,negated_conjecture,
( ssSkP818(skf74(X0))
| ~ ssSkP834(X0) ) ).
cnf(u1364,negated_conjecture,
( ssSkP813(skf75(X0))
| ~ ssSkP835(X0) ) ).
cnf(u1368,negated_conjecture,
( ssSkP836(skf76(X0))
| ~ ssSkP850(X0) ) ).
cnf(u1372,negated_conjecture,
( ssSkP838(skf77(X0))
| ~ ssSkP851(X0) ) ).
cnf(u1376,negated_conjecture,
( ssSkP840(skf78(X0))
| ~ ssSkP852(X0) ) ).
cnf(u1380,negated_conjecture,
( ssSkP842(skf79(X0))
| ~ ssSkP853(X0) ) ).
cnf(u1384,negated_conjecture,
( ssSkP844(skf80(X0))
| ~ ssSkP854(X0) ) ).
cnf(u1388,negated_conjecture,
( ssSkP846(skf81(X0))
| ~ ssSkP855(X0) ) ).
cnf(u1392,negated_conjecture,
( ssSkP848(skf82(X0))
| ~ ssSkP856(X0) ) ).
cnf(u1396,negated_conjecture,
( ssSkP839(skf83(X0))
| ~ ssSkP857(X0) ) ).
cnf(u1400,negated_conjecture,
( ssSkP843(skf84(X0))
| ~ ssSkP858(X0) ) ).
cnf(u1404,negated_conjecture,
( ssSkP847(skf85(X0))
| ~ ssSkP859(X0) ) ).
cnf(u1408,negated_conjecture,
( ssSkP841(skf86(X0))
| ~ ssSkP860(X0) ) ).
cnf(u1412,negated_conjecture,
( ssSkP837(skf87(X0))
| ~ ssSkP861(X0) ) ).
cnf(u1416,negated_conjecture,
( ~ ssPv24(skf52(X0))
| ~ ssSkP811(X0) ) ).
cnf(u1420,negated_conjecture,
( ~ ssPv21(skf53(X0))
| ~ ssSkP812(X0) ) ).
cnf(u1424,negated_conjecture,
( ~ ssPv8(skf54(X0))
| ~ ssSkP813(X0) ) ).
cnf(u1428,negated_conjecture,
( ~ ssPv13(skf55(X0))
| ~ ssSkP814(X0) ) ).
cnf(u1432,negated_conjecture,
( ~ ssPv23(skf56(X0))
| ~ ssSkP815(X0) ) ).
cnf(u1436,negated_conjecture,
( ~ ssPv7(skf57(X0))
| ~ ssSkP816(X0) ) ).
cnf(u1440,negated_conjecture,
( ~ ssPv16(skf58(X0))
| ~ ssSkP817(X0) ) ).
cnf(u1444,negated_conjecture,
( ~ ssPv14(skf59(X0))
| ~ ssSkP818(X0) ) ).
cnf(u1448,negated_conjecture,
( ~ ssPv22(skf60(X0))
| ~ ssSkP819(X0) ) ).
cnf(u1452,negated_conjecture,
( ~ ssPv5(skf61(X0))
| ~ ssSkP820(X0) ) ).
cnf(u1456,negated_conjecture,
( ~ ssPv6(skf62(X0))
| ~ ssSkP821(X0) ) ).
cnf(u1460,negated_conjecture,
( ~ ssPv15(skf63(X0))
| ~ ssSkP822(X0) ) ).
cnf(u1476,negated_conjecture,
( ~ ssSkP836(skf52(X0))
| ~ ssSkP811(X0) ) ).
cnf(u1480,negated_conjecture,
( ~ ssSkP842(skf53(X0))
| ~ ssSkP812(X0) ) ).
cnf(u1484,negated_conjecture,
( ~ ssSkP843(skf54(X0))
| ~ ssSkP813(X0) ) ).
cnf(u1488,negated_conjecture,
( ~ ssSkP839(skf55(X0))
| ~ ssSkP814(X0) ) ).
cnf(u1492,negated_conjecture,
( ~ ssSkP838(skf56(X0))
| ~ ssSkP815(X0) ) ).
cnf(u1496,negated_conjecture,
( ~ ssSkP847(skf57(X0))
| ~ ssSkP816(X0) ) ).
cnf(u1500,negated_conjecture,
( ~ ssSkP844(skf58(X0))
| ~ ssSkP817(X0) ) ).
cnf(u1504,negated_conjecture,
( ~ ssSkP848(skf59(X0))
| ~ ssSkP818(X0) ) ).
cnf(u1508,negated_conjecture,
( ~ ssSkP840(skf60(X0))
| ~ ssSkP819(X0) ) ).
cnf(u1512,negated_conjecture,
( ~ ssSkP837(skf61(X0))
| ~ ssSkP820(X0) ) ).
cnf(u1516,negated_conjecture,
( ~ ssSkP841(skf62(X0))
| ~ ssSkP821(X0) ) ).
cnf(u1520,negated_conjecture,
( ~ ssSkP846(skf63(X0))
| ~ ssSkP822(X0) ) ).
cnf(u1524,negated_conjecture,
( ssRr(X0,skf51(X0))
| ~ ssSkP809(X0) ) ).
cnf(u1528,negated_conjecture,
( ssRr(X0,skf52(X0))
| ~ ssSkP811(X0) ) ).
cnf(u1532,negated_conjecture,
( ssRr(X0,skf53(X0))
| ~ ssSkP812(X0) ) ).
cnf(u1536,negated_conjecture,
( ssRr(X0,skf54(X0))
| ~ ssSkP813(X0) ) ).
cnf(u1540,negated_conjecture,
( ssRr(X0,skf55(X0))
| ~ ssSkP814(X0) ) ).
cnf(u1544,negated_conjecture,
( ssRr(X0,skf56(X0))
| ~ ssSkP815(X0) ) ).
cnf(u1548,negated_conjecture,
( ssRr(X0,skf57(X0))
| ~ ssSkP816(X0) ) ).
cnf(u1552,negated_conjecture,
( ssRr(X0,skf58(X0))
| ~ ssSkP817(X0) ) ).
cnf(u1556,negated_conjecture,
( ssRr(X0,skf59(X0))
| ~ ssSkP818(X0) ) ).
cnf(u1560,negated_conjecture,
( ssRr(X0,skf60(X0))
| ~ ssSkP819(X0) ) ).
cnf(u1564,negated_conjecture,
( ssRr(X0,skf61(X0))
| ~ ssSkP820(X0) ) ).
cnf(u1568,negated_conjecture,
( ssRr(X0,skf62(X0))
| ~ ssSkP821(X0) ) ).
cnf(u1572,negated_conjecture,
( ssRr(X0,skf63(X0))
| ~ ssSkP822(X0) ) ).
cnf(u1576,negated_conjecture,
( ssRr(skf64(X0),X0)
| ~ ssSkP824(X0) ) ).
cnf(u1580,negated_conjecture,
( ssRr(skf65(X0),X0)
| ~ ssSkP825(X0) ) ).
cnf(u1584,negated_conjecture,
( ssRr(skf66(X0),X0)
| ~ ssSkP826(X0) ) ).
cnf(u1588,negated_conjecture,
( ssRr(skf67(X0),X0)
| ~ ssSkP827(X0) ) ).
cnf(u1592,negated_conjecture,
( ssRr(skf68(X0),X0)
| ~ ssSkP828(X0) ) ).
cnf(u1596,negated_conjecture,
( ssRr(skf69(X0),X0)
| ~ ssSkP829(X0) ) ).
cnf(u1600,negated_conjecture,
( ssRr(skf70(X0),X0)
| ~ ssSkP830(X0) ) ).
cnf(u1604,negated_conjecture,
( ssRr(skf71(X0),X0)
| ~ ssSkP831(X0) ) ).
cnf(u1608,negated_conjecture,
( ssRr(skf72(X0),X0)
| ~ ssSkP832(X0) ) ).
cnf(u1612,negated_conjecture,
( ssRr(skf73(X0),X0)
| ~ ssSkP833(X0) ) ).
cnf(u1616,negated_conjecture,
( ssRr(skf74(X0),X0)
| ~ ssSkP834(X0) ) ).
cnf(u1620,negated_conjecture,
( ssRr(skf75(X0),X0)
| ~ ssSkP835(X0) ) ).
cnf(u1624,negated_conjecture,
( ssRr(X0,skf76(X0))
| ~ ssSkP850(X0) ) ).
cnf(u1628,negated_conjecture,
( ssRr(X0,skf77(X0))
| ~ ssSkP851(X0) ) ).
cnf(u1632,negated_conjecture,
( ssRr(X0,skf78(X0))
| ~ ssSkP852(X0) ) ).
cnf(u1636,negated_conjecture,
( ssRr(X0,skf79(X0))
| ~ ssSkP853(X0) ) ).
cnf(u1640,negated_conjecture,
( ssRr(X0,skf80(X0))
| ~ ssSkP854(X0) ) ).
cnf(u1644,negated_conjecture,
( ssRr(X0,skf81(X0))
| ~ ssSkP855(X0) ) ).
cnf(u1648,negated_conjecture,
( ssRr(X0,skf82(X0))
| ~ ssSkP856(X0) ) ).
cnf(u1652,negated_conjecture,
( ssRr(X0,skf83(X0))
| ~ ssSkP857(X0) ) ).
cnf(u1656,negated_conjecture,
( ssRr(X0,skf84(X0))
| ~ ssSkP858(X0) ) ).
cnf(u1660,negated_conjecture,
( ssRr(X0,skf85(X0))
| ~ ssSkP859(X0) ) ).
cnf(u1664,negated_conjecture,
( ssRr(X0,skf86(X0))
| ~ ssSkP860(X0) ) ).
cnf(u1668,negated_conjecture,
( ssRr(X0,skf87(X0))
| ~ ssSkP861(X0) ) ).
cnf(u1672,negated_conjecture,
( ssRr(X0,skf88(X0))
| ~ ssSkP863(X0) ) ).
cnf(u1676,negated_conjecture,
( ssRr(X0,skf89(X0))
| ~ ssSkP865(X0) ) ).
cnf(u1680,negated_conjecture,
( ssRr(X0,skf90(X0))
| ~ ssSkP875(X0) ) ).
cnf(u1684,negated_conjecture,
( ssRr(X0,skf91(X0))
| ~ ssSkP877(X0) ) ).
cnf(u1688,negated_conjecture,
( ssRr(X0,skf92(X0))
| ~ ssSkP879(X0) ) ).
cnf(u1692,negated_conjecture,
( ssRr(X0,skf93(X0))
| ~ ssSkP881(X0) ) ).
cnf(u1696,negated_conjecture,
( ssRr(X0,skf94(X0))
| ~ ssSkP891(X0) ) ).
cnf(u1700,negated_conjecture,
( ssRr(X0,skf95(X0))
| ~ ssSkP893(X0) ) ).
cnf(u1704,negated_conjecture,
( ssRr(X0,skf96(X0))
| ~ ssSkP895(X0) ) ).
cnf(u1708,negated_conjecture,
( ssRr(X0,skf97(X0))
| ~ ssSkP897(X0) ) ).
cnf(u1712,negated_conjecture,
( ssRr(X0,skf98(X0))
| ~ ssSkP907(X0) ) ).
cnf(u1716,negated_conjecture,
( ssRr(X0,skf99(X0))
| ~ ssSkP909(X0) ) ).
cnf(u1720,negated_conjecture,
( ssRr(X0,skf100(X0))
| ~ ssSkP911(X0) ) ).
cnf(u1724,negated_conjecture,
( ssRr(X0,skf101(X0))
| ~ ssSkP913(X0) ) ).
cnf(u1728,negated_conjecture,
( ssSkP911(X0)
| ~ ssSkP912(X1)
| ~ ssSkP823(X0,X1) ) ).
cnf(u1732,negated_conjecture,
( ssSkP909(X0)
| ~ ssSkP910(X1)
| ~ ssSkP823(X0,X1) ) ).
cnf(u1736,negated_conjecture,
( ssSkP823(X2,X0)
| ~ ssSkP810(X2,X1)
| ~ ssRr(X0,X1) ) ).
cnf(u1740,negated_conjecture,
( ssSkP810(X2,X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ) ).
cnf(u1744,negated_conjecture,
( ssSkP907(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP908(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1748,negated_conjecture,
( ssSkP905(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP906(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1752,negated_conjecture,
( ssSkP903(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP904(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1756,negated_conjecture,
( ssSkP901(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP902(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1760,negated_conjecture,
( ssSkP899(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP900(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1764,negated_conjecture,
( ssSkP897(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP898(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1768,negated_conjecture,
( ssSkP895(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP896(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1772,negated_conjecture,
( ssSkP893(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP894(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1776,negated_conjecture,
( ssSkP891(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP892(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1780,negated_conjecture,
( ssSkP889(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP890(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1784,negated_conjecture,
( ssSkP887(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP888(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1788,negated_conjecture,
( ssSkP885(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP886(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1792,negated_conjecture,
( ssSkP883(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP884(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1796,negated_conjecture,
( ssSkP881(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP882(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1800,negated_conjecture,
( ssSkP879(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP880(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1804,negated_conjecture,
( ssSkP877(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP878(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1808,negated_conjecture,
( ssSkP875(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP876(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1812,negated_conjecture,
( ssSkP873(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP874(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1816,negated_conjecture,
( ssSkP871(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP872(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1820,negated_conjecture,
( ssSkP869(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP870(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1824,negated_conjecture,
( ssSkP867(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP868(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1828,negated_conjecture,
( ssSkP865(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP866(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1832,negated_conjecture,
( ssSkP863(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP864(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1836,negated_conjecture,
( ssSkP849(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP862(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1840,negated_conjecture,
( ssSkP809(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP845(X3)
| ~ ssRr(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN909-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.09/0.20 % Computer : n005.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 17:11:32 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 11.03/2.28 % (933071)Input is clausal, will run a generic CNF schedule.
% 11.03/2.28 % (933077)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1935091007:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.03/2.28 % (933078)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2236874306:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.03/2.28 % (933076)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=276784557:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.03/2.28 % (933081)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=236557399:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.03/2.28 % (933079)lrs+10_1_sil=8000:sp=occurrence:random_seed=1916990305:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.03/2.28 % (933082)dis-21_1_sil=8000:lcm=predicate:random_seed=874996889: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)
% 11.03/2.28 % (933080)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2364529474:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.03/2.28 % (933081)Refutation not found, incomplete strategy
% 11.03/2.28 % (933081)------------------------------
% 11.03/2.28 % (933081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.28 % (933081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.28 % (933081)CaDiCaL version: 2.1.3
% 11.03/2.28 % (933081)Termination reason: Refutation not found, incomplete strategy
% 11.03/2.28 % (933081)Time elapsed: 0.010 s
% 11.03/2.28 % (933081)Peak memory usage: 89 MB
% 11.03/2.28 % (933081)Instructions burned: 17 (million)
% 11.03/2.28 % (933082)Instruction limit reached!
% 11.03/2.28 % (933082)------------------------------
% 11.03/2.28 % (933082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.28 % (933082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.28 % (933082)CaDiCaL version: 2.1.3
% 11.03/2.28 % (933082)Termination reason: Instruction limit
% 11.03/2.28 % (933082)Termination phase: Saturation
% 11.03/2.28 % (933082)Time elapsed: 0.043 s
% 11.03/2.28 % (933082)Peak memory usage: 89 MB
% 11.03/2.28 % (933082)Instructions burned: 118 (million)
% 11.03/2.28 % (933079)Instruction limit reached!
% 11.03/2.28 % (933079)------------------------------
% 11.03/2.28 % (933079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.28 % (933079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.28 % (933079)CaDiCaL version: 2.1.3
% 11.03/2.28 % (933079)Termination reason: Instruction limit
% 11.03/2.28 % (933079)Termination phase: Saturation
% 11.03/2.28 % (933079)Time elapsed: 0.051 s
% 11.03/2.28 % (933079)Peak memory usage: 91 MB
% 11.03/2.28 % (933079)Instructions burned: 108 (million)
% 11.03/2.28 % (933080)Instruction limit reached!
% 11.03/2.28 % (933080)------------------------------
% 11.03/2.28 % (933080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.28 % (933080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.28 % (933080)CaDiCaL version: 2.1.3
% 11.03/2.28 % (933080)Termination reason: Instruction limit
% 11.03/2.28 % (933080)Termination phase: Saturation
% 11.03/2.28 % (933080)Time elapsed: 0.055 s
% 11.03/2.28 % (933080)Peak memory usage: 90 MB
% 11.03/2.28 % (933080)Instructions burned: 116 (million)
% 11.03/2.28 % (933090)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=2229818116:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.03/2.28 % (933091)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3516074105: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)
% 11.03/2.28 % (933092)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2537866686:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.03/2.28 % (933090)Instruction limit reached!
% 11.03/2.28 % (933090)------------------------------
% 11.03/2.28 % (933090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.28 % (933090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933090)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933090)Termination reason: Instruction limit
% 12.80/2.56 % (933090)Termination phase: Saturation
% 12.80/2.56 % (933090)Time elapsed: 0.070 s
% 12.80/2.56 % (933090)Peak memory usage: 91 MB
% 12.80/2.56 % (933090)Instructions burned: 144 (million)
% 12.80/2.56 % (933081)------------------------------
% 12.80/2.56 % (933081)------------------------------
% 12.80/2.56 % (933091)Instruction limit reached!
% 12.80/2.56 % (933091)------------------------------
% 12.80/2.56 % (933091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933091)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933091)Termination reason: Instruction limit
% 12.80/2.56 % (933091)Termination phase: Saturation
% 12.80/2.56 % (933091)Time elapsed: 0.095 s
% 12.80/2.56 % (933091)Peak memory usage: 90 MB
% 12.80/2.56 % (933091)Instructions burned: 189 (million)
% 12.80/2.56 % (933092)Instruction limit reached!
% 12.80/2.56 % (933092)------------------------------
% 12.80/2.56 % (933092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933092)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933092)Termination reason: Instruction limit
% 12.80/2.56 % (933092)Termination phase: Saturation
% 12.80/2.56 % (933092)Time elapsed: 0.097 s
% 12.80/2.56 % (933092)Peak memory usage: 92 MB
% 12.80/2.56 % (933092)Instructions burned: 219 (million)
% 12.80/2.56 % (933096)lrs+10_64_to=lpo:sil=8000:random_seed=2981880686:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 12.80/2.56 % (933097)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2984005323:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 12.80/2.56 % (933097)Refutation not found, incomplete strategy
% 12.80/2.56 % (933097)------------------------------
% 12.80/2.56 % (933097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933097)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933097)Termination reason: Refutation not found, incomplete strategy
% 12.80/2.56 % (933097)Time elapsed: 0.007 s
% 12.80/2.56 % (933097)Peak memory usage: 89 MB
% 12.80/2.56 % (933097)Instructions burned: 9 (million)
% 12.80/2.56 % (933099)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=938396512:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 12.80/2.56 % (933098)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=360732463:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.80/2.56 % (933096)Instruction limit reached!
% 12.80/2.56 % (933096)------------------------------
% 12.80/2.56 % (933096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933096)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933096)Termination reason: Instruction limit
% 12.80/2.56 % (933096)Termination phase: Saturation
% 12.80/2.56 % (933096)Time elapsed: 0.072 s
% 12.80/2.56 % (933096)Peak memory usage: 93 MB
% 12.80/2.56 % (933096)Instructions burned: 127 (million)
% 12.80/2.56 % (933098)Instruction limit reached!
% 12.80/2.56 % (933098)------------------------------
% 12.80/2.56 % (933098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933098)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933098)Termination reason: Instruction limit
% 12.80/2.56 % (933098)Termination phase: Saturation
% 12.80/2.56 % (933098)Time elapsed: 0.073 s
% 12.80/2.56 % (933098)Peak memory usage: 92 MB
% 12.80/2.56 % (933098)Instructions burned: 158 (million)
% 12.80/2.56 % (933104)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=2057932398:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 12.80/2.56 % (933105)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2957011485:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 12.80/2.56 % (933104)Instruction limit reached!
% 12.80/2.56 % (933104)------------------------------
% 12.80/2.56 % (933104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933104)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933104)Termination reason: Instruction limit
% 12.80/2.56 % (933104)Termination phase: Saturation
% 12.80/2.56 % (933104)Time elapsed: 0.057 s
% 12.80/2.56 % (933104)Peak memory usage: 91 MB
% 12.80/2.56 % (933104)Instructions burned: 107 (million)
% 12.80/2.56 % (933097)------------------------------
% 12.80/2.56 % (933097)------------------------------
% 12.80/2.56 % (933105)Instruction limit reached!
% 12.80/2.56 % (933105)------------------------------
% 12.80/2.56 % (933105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933105)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933105)Termination reason: Instruction limit
% 12.80/2.56 % (933105)Termination phase: Saturation
% 12.80/2.56 % (933105)Time elapsed: 0.060 s
% 12.80/2.56 % (933105)Peak memory usage: 93 MB
% 12.80/2.56 % (933105)Instructions burned: 108 (million)
% 12.80/2.56 % (933108)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3893260769:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 12.80/2.56 % (933108)Refutation not found, incomplete strategy
% 12.80/2.56 % (933108)------------------------------
% 12.80/2.56 % (933108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933108)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933108)Termination reason: Refutation not found, incomplete strategy
% 12.80/2.56 % (933108)Time elapsed: 0.012 s
% 12.80/2.56 % (933108)Peak memory usage: 89 MB
% 12.80/2.56 % (933108)Instructions burned: 23 (million)
% 12.80/2.56 % (933109)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1725017617:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 12.80/2.56 % (933110)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2953699947:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 12.80/2.56 % (933110)Refutation not found, incomplete strategy
% 12.80/2.56 % (933110)------------------------------
% 12.80/2.56 % (933110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933110)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933110)Termination reason: Refutation not found, incomplete strategy
% 12.80/2.56 % (933110)Time elapsed: 0.010 s
% 12.80/2.56 % (933110)Peak memory usage: 90 MB
% 12.80/2.56 % (933110)Instructions burned: 16 (million)
% 12.80/2.56 % (933108)------------------------------
% 12.80/2.56 % (933108)------------------------------
% 12.80/2.56 % (933110)------------------------------
% 12.80/2.56 % (933110)------------------------------
% 12.80/2.56 % (933114)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1211565104:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 12.80/2.56 % (933115)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1797270790:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 12.80/2.56 % (933115)Instruction limit reached!
% 12.80/2.56 % (933115)------------------------------
% 12.80/2.56 % (933115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933115)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933115)Termination reason: Instruction limit
% 12.80/2.56 % (933115)Termination phase: Saturation
% 12.80/2.56 % (933115)Time elapsed: 0.094 s
% 12.80/2.56 % (933115)Peak memory usage: 93 MB
% 12.80/2.56 % (933115)Instructions burned: 192 (million)
% 12.80/2.56 % (933114)Instruction limit reached!
% 12.80/2.56 % (933114)------------------------------
% 12.80/2.56 % (933114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933114)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933114)Termination reason: Instruction limit
% 12.80/2.56 % (933114)Termination phase: Saturation
% 12.80/2.56 % (933114)Time elapsed: 0.260 s
% 12.80/2.56 % (933114)Peak memory usage: 93 MB
% 12.80/2.56 % (933114)Instructions burned: 499 (million)
% 12.80/2.56 % (933118)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3707750877:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 12.80/2.56 % (933118)First to succeed.
% 12.80/2.56 % (933118)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-933071"
% 12.80/2.56 % (933119)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1216945491:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 12.80/2.56 % (933119)Instruction limit reached!
% 12.80/2.56 % (933119)------------------------------
% 12.80/2.56 % (933119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.56 % (933119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.56 % (933119)CaDiCaL version: 2.1.3
% 12.80/2.56 % (933119)Termination reason: Instruction limit
% 12.80/2.56 % (933119)Termination phase: Saturation
% 12.80/2.56 % (933119)Time elapsed: 0.071 s
% 12.80/2.56 % (933119)Peak memory usage: 90 MB
% 12.80/2.56 % (933119)Instructions burned: 157 (million)
% 12.80/2.56 % SZS status Satisfiable for theBenchmark
% 12.80/2.56 % SZS output start Saturation.
% See solution above
% 12.80/2.56 % SZS output start Definitions and Model Updates.
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP131(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP132(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC5 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP157(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP156(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP155(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP101(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP102(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC4 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP130(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP129(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP128(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP127(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP72(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP73(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC3 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP100(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP99(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP98(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP355(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP356(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC14 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP383(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP382(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP381(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP380(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP379(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP262(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP263(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC10 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP287(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP286(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP285(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP284(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP283(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP448(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP449(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC17 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP477(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP476(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP475(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP474(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP473(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP472(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP471(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP470(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP469(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP468(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP467(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP466(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP465(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP126(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP125(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP124(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP123(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP122(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP121(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP120(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP119(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP118(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP117(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP116(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP115(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP114(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP113(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP112(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP111(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP110(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP109(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP108(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP107(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP106(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP105(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP104(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP103(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv4(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP450(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP451(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP452(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP453(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP454(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP455(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP456(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP457(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP458(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP459(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP460(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP461(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP462(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP463(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP464(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv18(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP264(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP265(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP266(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP267(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP268(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP269(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP270(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP271(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP272(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP273(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP274(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP275(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP276(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP277(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP278(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP279(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP280(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP281(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP282(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv25(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP378(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP377(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP376(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP375(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP374(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP373(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP372(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP371(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP370(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP369(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP368(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP367(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP366(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP365(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP364(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP363(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP357(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP358(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP359(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP360(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP361(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP362(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP328(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP329(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC13 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP354(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP353(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP352(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP351(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP350(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP349(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP348(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP347(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP346(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP345(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP344(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP343(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP342(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP341(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP340(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP339(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP338(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP337(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP336(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP335(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP334(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP333(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP330(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP331(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP332(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv10(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP74(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP75(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP76(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP77(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP78(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP79(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP80(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP81(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP82(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP83(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP84(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP85(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP86(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP87(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP88(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP89(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP90(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP91(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP92(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP93(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP94(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP95(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP96(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP97(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv27(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP154(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP153(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP152(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP151(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP150(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP149(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP148(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP147(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP133(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP134(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP135(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP136(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP137(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP138(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP139(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP140(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP141(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP142(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP143(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP144(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP145(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP146(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP522(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP523(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC20 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP540(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP539(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP538(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP537(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP536(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP535(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP534(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP533(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP532(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP531(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP530(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP717(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP718(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC27 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP746(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP745(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP744(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP743(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP742(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP741(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP740(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP739(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP738(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP737(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP736(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP735(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP734(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP719(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP720(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP721(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP722(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP723(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP724(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP725(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP726(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP727(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP728(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP729(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP730(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP731(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP732(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP733(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP41(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP31(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP32(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP33(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP34(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP35(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP36(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP37(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP38(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP39(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP40(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP55(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP56(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC2 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP71(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP70(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP29(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP30(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC1 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP54(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP53(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP42(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP43(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP44(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP45(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP46(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP47(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP48(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP49(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP50(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP51(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP52(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv28(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP69(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP68(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP67(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP66(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP65(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP64(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP63(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP62(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP61(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP60(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP59(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP58(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP57(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP288(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP289(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC11 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP307(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP306(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP305(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP304(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP303(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP302(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP301(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP300(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP299(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP298(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP297(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP296(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP295(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP294(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP293(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP290(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP291(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP292(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv17(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP524(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP525(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP526(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP527(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP528(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP529(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP631(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP632(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC24 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP661(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP660(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP659(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP658(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP657(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP656(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP655(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP654(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP653(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP652(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP384(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP385(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC15 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP414(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP413(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP412(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP411(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP410(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP409(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP408(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP407(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP406(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP405(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP404(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP403(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP402(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP401(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP400(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP399(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP398(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP397(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP396(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP395(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP394(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP393(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP392(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP391(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP390(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP389(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP388(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP387(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP386(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP541(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP542(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC21 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP571(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP570(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP569(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP568(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP567(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP566(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP565(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP564(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP563(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP562(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP561(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP560(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP308(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP309(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC12 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP327(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP326(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP325(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP324(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP323(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP322(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP321(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP320(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP319(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP318(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP317(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP316(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP310(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP311(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP312(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP313(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP314(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP315(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv19(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP559(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP558(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP557(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP556(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP555(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP554(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP553(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP552(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP551(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP550(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP549(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP548(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP547(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP546(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP545(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP544(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP543(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP747(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP748(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC28 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP777(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP776(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP775(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP774(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP773(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP772(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP771(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP770(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP769(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP768(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP767(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP766(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP765(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP764(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP763(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP762(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP761(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP760(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP759(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP758(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP757(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP756(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP755(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP754(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP753(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP752(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP751(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP750(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP749(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP158(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP159(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC6 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP188(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP187(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP186(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP185(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP242(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP243(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC9 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP261(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP260(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP259(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP258(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP244(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP245(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP246(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP247(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP248(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP249(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP250(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP251(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP252(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP253(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP254(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP255(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP256(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP257(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP189(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP190(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC7 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP208(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP207(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP206(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP205(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP191(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP192(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP193(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP194(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP195(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP196(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP197(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP198(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP199(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP200(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP201(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP202(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP203(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP204(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP209(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP210(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC8 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP241(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP240(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP239(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP238(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP662(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP663(X0,X1) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkC25 := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP694(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP693(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP692(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP691(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP690(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP689(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP688(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP687(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP686(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP685(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP684(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP683(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP682(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP681(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP680(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP679(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP678(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP677(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP676(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP675(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP674(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP673(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP672(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP671(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP670(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP669(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP668(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP667(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP666(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP665(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP664(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssPv1(X0) := $true
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP211(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP212(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP213(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP214(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP215(X0) := $false
% 12.80/2.56 for all inputs,
% 12.80/2.56 define ssSkP216(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP217(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP218(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP219(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP220(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP221(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP222(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP223(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP224(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP225(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP226(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP227(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP228(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP229(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP230(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP231(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP232(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP233(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP234(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP235(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP236(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP237(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssPv26(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP184(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP183(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP182(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP181(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP180(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP179(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP178(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP177(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP176(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP175(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP174(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP173(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP172(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP171(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP170(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP169(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP168(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP167(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP166(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP165(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP164(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP163(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP162(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP161(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP160(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssPv3(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP633(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP634(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP635(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP636(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP637(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP638(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP639(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP640(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP641(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP642(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP643(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP644(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP645(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP646(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP647(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP648(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP649(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP650(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP651(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP415(X0,X1) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP416(X0,X1) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkC16 := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP447(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP446(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP445(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP444(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP443(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP442(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP441(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP440(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP439(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP438(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP437(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP417(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP418(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP419(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP420(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP421(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP422(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP423(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP424(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP425(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP426(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP427(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP428(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP429(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP430(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP431(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP432(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP433(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP434(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP435(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP436(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP503(X0,X1) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP504(X0,X1) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkC19 := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP521(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP520(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP519(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP518(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP517(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP516(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP515(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP514(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP513(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP512(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP511(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP505(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP506(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP507(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP508(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP509(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP510(X0) := $false
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssPv20(X0) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP0(X0,X1) := $true
% 12.80/2.57 for all inputs,
% 12.80/2.57 define ssSkP1(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkC0 := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP28(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP27(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP26(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP25(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP24(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP23(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP22(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP21(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP20(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP19(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP18(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP17(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP16(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP15(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP14(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP13(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP12(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP11(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP10(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP9(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP8(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP2(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP3(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP4(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP5(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP6(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP7(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP604(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP605(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkC23 := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP630(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP629(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP628(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP627(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP626(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP625(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP624(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP623(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP622(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP621(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP620(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP619(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP618(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP617(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP616(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP615(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP614(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP613(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP612(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP778(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP779(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkC29 := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP808(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP807(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP806(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP805(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP804(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP803(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP802(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP801(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP800(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP799(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP798(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP797(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP796(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP795(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP794(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP793(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP792(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP791(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP790(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP780(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP781(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP782(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP783(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP784(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP785(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP786(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP787(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP788(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP789(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP695(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP696(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkC26 := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP716(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP715(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP714(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP713(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP712(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP711(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP710(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP709(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP708(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP707(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP706(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP705(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP704(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP703(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP702(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP701(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP700(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP699(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP698(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP697(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssPv12(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP611(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP610(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP606(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP607(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP608(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP609(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssPv11(X0) := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP572(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP573(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkC22 := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP603(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP602(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP601(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP600(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP599(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP598(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP597(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP596(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP595(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP594(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP593(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP592(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP591(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP590(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP589(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP588(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP587(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP586(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP585(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP584(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP583(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP582(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP581(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP580(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP579(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP578(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP577(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP576(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP575(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP574(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssPv2(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP478(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP479(X0,X1) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkC18 := $false
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP502(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP501(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP500(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP499(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP498(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP497(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP496(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP495(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP494(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP493(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP492(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP491(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP490(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP489(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP488(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP487(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP486(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP485(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP484(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP483(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP482(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP481(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssSkP480(X0) := $true
% 13.68/2.66 for all inputs,
% 13.68/2.66 define ssPv9(X0) := $true
% 13.68/2.66 % SZS output end Definitions and Model Updates.
% 13.68/2.66 % (933118)------------------------------
% 13.68/2.66 % (933118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.68/2.66 % (933118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.68/2.66 % (933118)CaDiCaL version: 2.1.3
% 13.68/2.66 % (933118)Termination reason: Satisfiable
% 13.68/2.66 % (933118)Time elapsed: 0.015 s
% 13.68/2.66 % (933118)Peak memory usage: 90 MB
% 13.68/2.66 % (933118)Instructions burned: 22 (million)
% 13.68/2.66 % (933118)------------------------------
% 13.68/2.66 % (933118)------------------------------
% 13.68/2.66 % (933071)Success in time 1.877 s
% 13.68/2.66 % Vampire exiting
%------------------------------------------------------------------------------