%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN908-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 7.45s 1.49s
% Output : Saturation 7.45s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1373,negated_conjecture,
~ ssSkC20 ).
cnf(u1378,negated_conjecture,
ssSkP1191(skc41) ).
cnf(u1382,negated_conjecture,
( ssSkP1022(X0)
| ~ ssSkP1042(X0) ) ).
cnf(u1386,negated_conjecture,
( ssPv47(X0)
| ~ ssSkP1042(X0) ) ).
cnf(u1390,negated_conjecture,
( ssSkP1032(X0)
| ~ ssSkP1043(X0) ) ).
cnf(u1394,negated_conjecture,
( ssPv11(X0)
| ~ ssSkP1043(X0) ) ).
cnf(u1398,negated_conjecture,
( ssSkP1025(X0)
| ~ ssSkP1044(X0) ) ).
cnf(u1402,negated_conjecture,
( ssPv45(X0)
| ~ ssSkP1044(X0) ) ).
cnf(u1406,negated_conjecture,
( ssSkP1023(X0)
| ~ ssSkP1045(X0) ) ).
cnf(u1410,negated_conjecture,
( ssPv26(X0)
| ~ ssSkP1045(X0) ) ).
cnf(u1414,negated_conjecture,
( ssSkP1028(X0)
| ~ ssSkP1046(X0) ) ).
cnf(u1418,negated_conjecture,
( ssPv44(X0)
| ~ ssSkP1046(X0) ) ).
cnf(u1422,negated_conjecture,
( ssSkP1027(X0)
| ~ ssSkP1047(X0) ) ).
cnf(u1426,negated_conjecture,
( ssPv13(X0)
| ~ ssSkP1047(X0) ) ).
cnf(u1430,negated_conjecture,
( ssSkP1031(X0)
| ~ ssSkP1048(X0) ) ).
cnf(u1434,negated_conjecture,
( ssPv43(X0)
| ~ ssSkP1048(X0) ) ).
cnf(u1438,negated_conjecture,
( ssSkP1030(X0)
| ~ ssSkP1049(X0) ) ).
cnf(u1442,negated_conjecture,
( ssPv25(X0)
| ~ ssSkP1049(X0) ) ).
cnf(u1446,negated_conjecture,
( ssSkP1034(X0)
| ~ ssSkP1050(X0) ) ).
cnf(u1450,negated_conjecture,
( ssPv42(X0)
| ~ ssSkP1050(X0) ) ).
cnf(u1454,negated_conjecture,
( ssSkP1037(X0)
| ~ ssSkP1052(X0) ) ).
cnf(u1458,negated_conjecture,
( ssPv41(X0)
| ~ ssSkP1052(X0) ) ).
cnf(u1462,negated_conjecture,
( ssSkP1036(X0)
| ~ ssSkP1053(X0) ) ).
cnf(u1466,negated_conjecture,
( ssPv16(X0)
| ~ ssSkP1053(X0) ) ).
cnf(u1470,negated_conjecture,
( ssSkP1040(X0)
| ~ ssSkP1054(X0) ) ).
cnf(u1474,negated_conjecture,
( ssPv32(X0)
| ~ ssSkP1054(X0) ) ).
cnf(u1478,negated_conjecture,
( ssSkP1041(X0)
| ~ ssSkP1055(X0) ) ).
cnf(u1482,negated_conjecture,
( ssPv12(X0)
| ~ ssSkP1055(X0) ) ).
cnf(u1486,negated_conjecture,
( ssSkP1024(X0)
| ~ ssSkP1056(X0) ) ).
cnf(u1490,negated_conjecture,
( ssPv31(X0)
| ~ ssSkP1056(X0) ) ).
cnf(u1494,negated_conjecture,
( ssSkP1026(X0)
| ~ ssSkP1057(X0) ) ).
cnf(u1498,negated_conjecture,
( ssPv15(X0)
| ~ ssSkP1057(X0) ) ).
cnf(u1502,negated_conjecture,
( ssSkP1029(X0)
| ~ ssSkP1058(X0) ) ).
cnf(u1506,negated_conjecture,
( ssPv30(X0)
| ~ ssSkP1058(X0) ) ).
cnf(u1510,negated_conjecture,
( ssSkP1039(X0)
| ~ ssSkP1059(X0) ) ).
cnf(u1514,negated_conjecture,
( ssPv9(X0)
| ~ ssSkP1059(X0) ) ).
cnf(u1518,negated_conjecture,
( ssSkP1033(X0)
| ~ ssSkP1060(X0) ) ).
cnf(u1522,negated_conjecture,
( ssPv29(X0)
| ~ ssSkP1060(X0) ) ).
cnf(u1526,negated_conjecture,
( ssSkP1035(X0)
| ~ ssSkP1061(X0) ) ).
cnf(u1530,negated_conjecture,
( ssPv14(X0)
| ~ ssSkP1061(X0) ) ).
cnf(u1534,negated_conjecture,
( ssSkP1038(X0)
| ~ ssSkP1062(X0) ) ).
cnf(u1538,negated_conjecture,
( ssPv27(X0)
| ~ ssSkP1062(X0) ) ).
cnf(u1542,negated_conjecture,
( ssSkP999(X0)
| ~ ssSkP1063(X0) ) ).
cnf(u1546,negated_conjecture,
( ssSkP1051(X0)
| ~ ssSkP1063(X0) ) ).
cnf(u1550,negated_conjecture,
( ssSkP1084(X0)
| ~ ssSkP1085(X0) ) ).
cnf(u1554,negated_conjecture,
( ssSkP1086(X0)
| ~ ssSkP1087(X0) ) ).
cnf(u1558,negated_conjecture,
( ssSkP1088(X0)
| ~ ssSkP1089(X0) ) ).
cnf(u1562,negated_conjecture,
( ssSkP1090(X0)
| ~ ssSkP1091(X0) ) ).
cnf(u1566,negated_conjecture,
( ssSkP1092(X0)
| ~ ssSkP1093(X0) ) ).
cnf(u1570,negated_conjecture,
( ssSkP1094(X0)
| ~ ssSkP1095(X0) ) ).
cnf(u1574,negated_conjecture,
( ssSkP1083(X0)
| ~ ssSkP1097(X0) ) ).
cnf(u1578,negated_conjecture,
( ssSkP1096(X0)
| ~ ssSkP1097(X0) ) ).
cnf(u1582,negated_conjecture,
( ssSkP1098(X0)
| ~ ssSkP1099(X0) ) ).
cnf(u1586,negated_conjecture,
( ssSkP1082(X0)
| ~ ssSkP1101(X0) ) ).
cnf(u1590,negated_conjecture,
( ssSkP1100(X0)
| ~ ssSkP1101(X0) ) ).
cnf(u1594,negated_conjecture,
( ssSkP1081(X0)
| ~ ssSkP1103(X0) ) ).
cnf(u1598,negated_conjecture,
( ssSkP1102(X0)
| ~ ssSkP1103(X0) ) ).
cnf(u1602,negated_conjecture,
( ssSkP1080(X0)
| ~ ssSkP1105(X0) ) ).
cnf(u1606,negated_conjecture,
( ssSkP1104(X0)
| ~ ssSkP1105(X0) ) ).
cnf(u1610,negated_conjecture,
( ssSkP1079(X0)
| ~ ssSkP1107(X0) ) ).
cnf(u1614,negated_conjecture,
( ssSkP1106(X0)
| ~ ssSkP1107(X0) ) ).
cnf(u1618,negated_conjecture,
( ssSkP1078(X0)
| ~ ssSkP1109(X0) ) ).
cnf(u1622,negated_conjecture,
( ssSkP1108(X0)
| ~ ssSkP1109(X0) ) ).
cnf(u1626,negated_conjecture,
( ssSkP1077(X0)
| ~ ssSkP1111(X0) ) ).
cnf(u1630,negated_conjecture,
( ssSkP1110(X0)
| ~ ssSkP1111(X0) ) ).
cnf(u1634,negated_conjecture,
( ssSkP1112(X0)
| ~ ssSkP1113(X0) ) ).
cnf(u1638,negated_conjecture,
( ssSkP1114(X0)
| ~ ssSkP1115(X0) ) ).
cnf(u1642,negated_conjecture,
( ssSkP1116(X0)
| ~ ssSkP1117(X0) ) ).
cnf(u1646,negated_conjecture,
( ssSkP1118(X0)
| ~ ssSkP1119(X0) ) ).
cnf(u1650,negated_conjecture,
( ssSkP1120(X0)
| ~ ssSkP1121(X0) ) ).
cnf(u1654,negated_conjecture,
( ssSkP1122(X0)
| ~ ssSkP1123(X0) ) ).
cnf(u1658,negated_conjecture,
( ssSkP1124(X0)
| ~ ssSkP1125(X0) ) ).
cnf(u1662,negated_conjecture,
( ssSkP1126(X0)
| ~ ssSkP1127(X0) ) ).
cnf(u1666,negated_conjecture,
( ssSkP1076(X0)
| ~ ssSkP1129(X0) ) ).
cnf(u1670,negated_conjecture,
( ssSkP1128(X0)
| ~ ssSkP1129(X0) ) ).
cnf(u1674,negated_conjecture,
( ssSkP1075(X0)
| ~ ssSkP1131(X0) ) ).
cnf(u1678,negated_conjecture,
( ssSkP1130(X0)
| ~ ssSkP1131(X0) ) ).
cnf(u1682,negated_conjecture,
( ssSkP1074(X0)
| ~ ssSkP1133(X0) ) ).
cnf(u1686,negated_conjecture,
( ssSkP1132(X0)
| ~ ssSkP1133(X0) ) ).
cnf(u1690,negated_conjecture,
( ssSkP1134(X0)
| ~ ssSkP1135(X0) ) ).
cnf(u1694,negated_conjecture,
( ssSkP1073(X0)
| ~ ssSkP1137(X0) ) ).
cnf(u1698,negated_conjecture,
( ssSkP1136(X0)
| ~ ssSkP1137(X0) ) ).
cnf(u1702,negated_conjecture,
( ssSkP1072(X0)
| ~ ssSkP1139(X0) ) ).
cnf(u1706,negated_conjecture,
( ssSkP1138(X0)
| ~ ssSkP1139(X0) ) ).
cnf(u1710,negated_conjecture,
( ssSkP1071(X0)
| ~ ssSkP1141(X0) ) ).
cnf(u1714,negated_conjecture,
( ssSkP1140(X0)
| ~ ssSkP1141(X0) ) ).
cnf(u1718,negated_conjecture,
( ssSkP1070(X0)
| ~ ssSkP1143(X0) ) ).
cnf(u1722,negated_conjecture,
( ssSkP1142(X0)
| ~ ssSkP1143(X0) ) ).
cnf(u1726,negated_conjecture,
( ssSkP1144(X0)
| ~ ssSkP1145(X0) ) ).
cnf(u1730,negated_conjecture,
( ssSkP1146(X0)
| ~ ssSkP1147(X0) ) ).
cnf(u1734,negated_conjecture,
( ssSkP1148(X0)
| ~ ssSkP1149(X0) ) ).
cnf(u1738,negated_conjecture,
( ssSkP1150(X0)
| ~ ssSkP1151(X0) ) ).
cnf(u1742,negated_conjecture,
( ssSkP1152(X0)
| ~ ssSkP1153(X0) ) ).
cnf(u1746,negated_conjecture,
( ssSkP1154(X0)
| ~ ssSkP1155(X0) ) ).
cnf(u1750,negated_conjecture,
( ssSkP1156(X0)
| ~ ssSkP1157(X0) ) ).
cnf(u1754,negated_conjecture,
( ssSkP1158(X0)
| ~ ssSkP1159(X0) ) ).
cnf(u1758,negated_conjecture,
( ssSkP1069(X0)
| ~ ssSkP1161(X0) ) ).
cnf(u1762,negated_conjecture,
( ssSkP1160(X0)
| ~ ssSkP1161(X0) ) ).
cnf(u1766,negated_conjecture,
( ssSkP1068(X0)
| ~ ssSkP1163(X0) ) ).
cnf(u1770,negated_conjecture,
( ssSkP1162(X0)
| ~ ssSkP1163(X0) ) ).
cnf(u1774,negated_conjecture,
( ssSkP1067(X0)
| ~ ssSkP1165(X0) ) ).
cnf(u1778,negated_conjecture,
( ssSkP1164(X0)
| ~ ssSkP1165(X0) ) ).
cnf(u1782,negated_conjecture,
( ssSkP1066(X0)
| ~ ssSkP1167(X0) ) ).
cnf(u1786,negated_conjecture,
( ssSkP1166(X0)
| ~ ssSkP1167(X0) ) ).
cnf(u1790,negated_conjecture,
( ssSkP1065(X0)
| ~ ssSkP1169(X0) ) ).
cnf(u1794,negated_conjecture,
( ssSkP1168(X0)
| ~ ssSkP1169(X0) ) ).
cnf(u1798,negated_conjecture,
( ssSkP1170(X0)
| ~ ssSkP1171(X0) ) ).
cnf(u1802,negated_conjecture,
( ssSkP1064(X0)
| ~ ssSkP1173(X0) ) ).
cnf(u1806,negated_conjecture,
( ssSkP1172(X0)
| ~ ssSkP1173(X0) ) ).
cnf(u1810,negated_conjecture,
( ssSkP1174(X0)
| ~ ssSkP1175(X0) ) ).
cnf(u1814,negated_conjecture,
( ssSkP1176(X0)
| ~ ssSkP1177(X0) ) ).
cnf(u1818,negated_conjecture,
( ssSkP1178(X0)
| ~ ssSkP1179(X0) ) ).
cnf(u1822,negated_conjecture,
( ssSkP1180(X0)
| ~ ssSkP1181(X0) ) ).
cnf(u1826,negated_conjecture,
( ssSkP1182(X0)
| ~ ssSkP1183(X0) ) ).
cnf(u1830,negated_conjecture,
( ssSkP1184(X0)
| ~ ssSkP1185(X0) ) ).
cnf(u1834,negated_conjecture,
( ssSkP1186(X0)
| ~ ssSkP1187(X0) ) ).
cnf(u1838,negated_conjecture,
( ssSkP1188(X0)
| ~ ssSkP1189(X0) ) ).
cnf(u1842,negated_conjecture,
( ssSkP1190(X0)
| ~ ssSkP1191(X0) ) ).
cnf(u1846,negated_conjecture,
( ssSkP1001(skf116(X0))
| ~ ssSkP1022(X0) ) ).
cnf(u1850,negated_conjecture,
( ssSkP1019(skf117(X0))
| ~ ssSkP1023(X0) ) ).
cnf(u1854,negated_conjecture,
( ssSkP1012(skf118(X0))
| ~ ssSkP1024(X0) ) ).
cnf(u1858,negated_conjecture,
( ssSkP1005(skf119(X0))
| ~ ssSkP1025(X0) ) ).
cnf(u1862,negated_conjecture,
( ssSkP1010(skf120(X0))
| ~ ssSkP1026(X0) ) ).
cnf(u1866,negated_conjecture,
( ssSkP1020(skf121(X0))
| ~ ssSkP1027(X0) ) ).
cnf(u1870,negated_conjecture,
( ssSkP1009(skf122(X0))
| ~ ssSkP1028(X0) ) ).
cnf(u1874,negated_conjecture,
( ssSkP1018(skf123(X0))
| ~ ssSkP1029(X0) ) ).
cnf(u1878,negated_conjecture,
( ssSkP1008(skf124(X0))
| ~ ssSkP1030(X0) ) ).
cnf(u1882,negated_conjecture,
( ssSkP1013(skf125(X0))
| ~ ssSkP1031(X0) ) ).
cnf(u1886,negated_conjecture,
( ssSkP1015(skf126(X0))
| ~ ssSkP1032(X0) ) ).
cnf(u1890,negated_conjecture,
( ssSkP1004(skf127(X0))
| ~ ssSkP1033(X0) ) ).
cnf(u1894,negated_conjecture,
( ssSkP1017(skf128(X0))
| ~ ssSkP1034(X0) ) ).
cnf(u1898,negated_conjecture,
( ssSkP1003(skf129(X0))
| ~ ssSkP1035(X0) ) ).
cnf(u1902,negated_conjecture,
( ssSkP1016(skf130(X0))
| ~ ssSkP1036(X0) ) ).
cnf(u1906,negated_conjecture,
( ssSkP1002(skf131(X0))
| ~ ssSkP1037(X0) ) ).
cnf(u1910,negated_conjecture,
( ssSkP1011(skf132(X0))
| ~ ssSkP1038(X0) ) ).
cnf(u1914,negated_conjecture,
( ssSkP1014(skf133(X0))
| ~ ssSkP1039(X0) ) ).
cnf(u1918,negated_conjecture,
( ssSkP1007(skf134(X0))
| ~ ssSkP1040(X0) ) ).
cnf(u1922,negated_conjecture,
( ssSkP1006(skf135(X0))
| ~ ssSkP1041(X0) ) ).
cnf(u1926,negated_conjecture,
( ssSkP1042(skf136(X0))
| ~ ssSkP1064(X0) ) ).
cnf(u1930,negated_conjecture,
( ssSkP1044(skf137(X0))
| ~ ssSkP1065(X0) ) ).
cnf(u1934,negated_conjecture,
( ssSkP1046(skf138(X0))
| ~ ssSkP1066(X0) ) ).
cnf(u1938,negated_conjecture,
( ssSkP1048(skf139(X0))
| ~ ssSkP1067(X0) ) ).
cnf(u1942,negated_conjecture,
( ssSkP1050(skf140(X0))
| ~ ssSkP1068(X0) ) ).
cnf(u1946,negated_conjecture,
( ssSkP1052(skf141(X0))
| ~ ssSkP1069(X0) ) ).
cnf(u1950,negated_conjecture,
( ssSkP1054(skf142(X0))
| ~ ssSkP1070(X0) ) ).
cnf(u1954,negated_conjecture,
( ssSkP1056(skf143(X0))
| ~ ssSkP1071(X0) ) ).
cnf(u1958,negated_conjecture,
( ssSkP1058(skf144(X0))
| ~ ssSkP1072(X0) ) ).
cnf(u1962,negated_conjecture,
( ssSkP1060(skf145(X0))
| ~ ssSkP1073(X0) ) ).
cnf(u1966,negated_conjecture,
( ssSkP1062(skf146(X0))
| ~ ssSkP1074(X0) ) ).
cnf(u1970,negated_conjecture,
( ssSkP1045(skf147(X0))
| ~ ssSkP1075(X0) ) ).
cnf(u1974,negated_conjecture,
( ssSkP1049(skf148(X0))
| ~ ssSkP1076(X0) ) ).
cnf(u1978,negated_conjecture,
( ssSkP1053(skf149(X0))
| ~ ssSkP1077(X0) ) ).
cnf(u1982,negated_conjecture,
( ssSkP1057(skf150(X0))
| ~ ssSkP1078(X0) ) ).
cnf(u1986,negated_conjecture,
( ssSkP1061(skf151(X0))
| ~ ssSkP1079(X0) ) ).
cnf(u1990,negated_conjecture,
( ssSkP1047(skf152(X0))
| ~ ssSkP1080(X0) ) ).
cnf(u1994,negated_conjecture,
( ssSkP1055(skf153(X0))
| ~ ssSkP1081(X0) ) ).
cnf(u1998,negated_conjecture,
( ssSkP1043(skf154(X0))
| ~ ssSkP1082(X0) ) ).
cnf(u2002,negated_conjecture,
( ssSkP1059(skf155(X0))
| ~ ssSkP1083(X0) ) ).
cnf(u2006,negated_conjecture,
( ~ ssPv47(skf96(X0))
| ~ ssSkP1001(X0) ) ).
cnf(u2010,negated_conjecture,
( ~ ssPv41(skf97(X0))
| ~ ssSkP1002(X0) ) ).
cnf(u2014,negated_conjecture,
( ~ ssPv14(skf98(X0))
| ~ ssSkP1003(X0) ) ).
cnf(u2018,negated_conjecture,
( ~ ssPv29(skf99(X0))
| ~ ssSkP1004(X0) ) ).
cnf(u2022,negated_conjecture,
( ~ ssPv45(skf100(X0))
| ~ ssSkP1005(X0) ) ).
cnf(u2026,negated_conjecture,
( ~ ssPv12(skf101(X0))
| ~ ssSkP1006(X0) ) ).
cnf(u2030,negated_conjecture,
( ~ ssPv32(skf102(X0))
| ~ ssSkP1007(X0) ) ).
cnf(u2034,negated_conjecture,
( ~ ssPv25(skf103(X0))
| ~ ssSkP1008(X0) ) ).
cnf(u2038,negated_conjecture,
( ~ ssPv44(skf104(X0))
| ~ ssSkP1009(X0) ) ).
cnf(u2042,negated_conjecture,
( ~ ssPv15(skf105(X0))
| ~ ssSkP1010(X0) ) ).
cnf(u2046,negated_conjecture,
( ~ ssPv27(skf106(X0))
| ~ ssSkP1011(X0) ) ).
cnf(u2050,negated_conjecture,
( ~ ssPv31(skf107(X0))
| ~ ssSkP1012(X0) ) ).
cnf(u2054,negated_conjecture,
( ~ ssPv43(skf108(X0))
| ~ ssSkP1013(X0) ) ).
cnf(u2058,negated_conjecture,
( ~ ssPv9(skf109(X0))
| ~ ssSkP1014(X0) ) ).
cnf(u2062,negated_conjecture,
( ~ ssPv11(skf110(X0))
| ~ ssSkP1015(X0) ) ).
cnf(u2066,negated_conjecture,
( ~ ssPv16(skf111(X0))
| ~ ssSkP1016(X0) ) ).
cnf(u2070,negated_conjecture,
( ~ ssPv42(skf112(X0))
| ~ ssSkP1017(X0) ) ).
cnf(u2074,negated_conjecture,
( ~ ssPv30(skf113(X0))
| ~ ssSkP1018(X0) ) ).
cnf(u2078,negated_conjecture,
( ~ ssPv26(skf114(X0))
| ~ ssSkP1019(X0) ) ).
cnf(u2082,negated_conjecture,
( ~ ssPv13(skf115(X0))
| ~ ssSkP1020(X0) ) ).
cnf(u2106,negated_conjecture,
( ~ ssSkP1042(skf96(X0))
| ~ ssSkP1001(X0) ) ).
cnf(u2110,negated_conjecture,
( ~ ssSkP1052(skf97(X0))
| ~ ssSkP1002(X0) ) ).
cnf(u2114,negated_conjecture,
( ~ ssSkP1061(skf98(X0))
| ~ ssSkP1003(X0) ) ).
cnf(u2118,negated_conjecture,
( ~ ssSkP1060(skf99(X0))
| ~ ssSkP1004(X0) ) ).
cnf(u2122,negated_conjecture,
( ~ ssSkP1044(skf100(X0))
| ~ ssSkP1005(X0) ) ).
cnf(u2126,negated_conjecture,
( ~ ssSkP1055(skf101(X0))
| ~ ssSkP1006(X0) ) ).
cnf(u2130,negated_conjecture,
( ~ ssSkP1054(skf102(X0))
| ~ ssSkP1007(X0) ) ).
cnf(u2134,negated_conjecture,
( ~ ssSkP1049(skf103(X0))
| ~ ssSkP1008(X0) ) ).
cnf(u2138,negated_conjecture,
( ssRr(X0,skf95(X0))
| ~ ssSkP999(X0) ) ).
cnf(u2142,negated_conjecture,
( ~ ssSkP1046(skf104(X0))
| ~ ssSkP1009(X0) ) ).
cnf(u2146,negated_conjecture,
( ~ ssSkP1057(skf105(X0))
| ~ ssSkP1010(X0) ) ).
cnf(u2150,negated_conjecture,
( ~ ssSkP1062(skf106(X0))
| ~ ssSkP1011(X0) ) ).
cnf(u2154,negated_conjecture,
( ~ ssSkP1056(skf107(X0))
| ~ ssSkP1012(X0) ) ).
cnf(u2158,negated_conjecture,
( ~ ssSkP1048(skf108(X0))
| ~ ssSkP1013(X0) ) ).
cnf(u2162,negated_conjecture,
( ~ ssSkP1059(skf109(X0))
| ~ ssSkP1014(X0) ) ).
cnf(u2166,negated_conjecture,
( ~ ssSkP1043(skf110(X0))
| ~ ssSkP1015(X0) ) ).
cnf(u2170,negated_conjecture,
( ~ ssSkP1053(skf111(X0))
| ~ ssSkP1016(X0) ) ).
cnf(u2174,negated_conjecture,
( ~ ssSkP1050(skf112(X0))
| ~ ssSkP1017(X0) ) ).
cnf(u2178,negated_conjecture,
( ~ ssSkP1058(skf113(X0))
| ~ ssSkP1018(X0) ) ).
cnf(u2182,negated_conjecture,
( ~ ssSkP1045(skf114(X0))
| ~ ssSkP1019(X0) ) ).
cnf(u2186,negated_conjecture,
( ~ ssSkP1047(skf115(X0))
| ~ ssSkP1020(X0) ) ).
cnf(u2190,negated_conjecture,
( ssRr(X0,skf96(X0))
| ~ ssSkP1001(X0) ) ).
cnf(u2194,negated_conjecture,
( ssRr(X0,skf97(X0))
| ~ ssSkP1002(X0) ) ).
cnf(u2198,negated_conjecture,
( ssRr(X0,skf98(X0))
| ~ ssSkP1003(X0) ) ).
cnf(u2202,negated_conjecture,
( ssRr(X0,skf99(X0))
| ~ ssSkP1004(X0) ) ).
cnf(u2206,negated_conjecture,
( ssRr(X0,skf100(X0))
| ~ ssSkP1005(X0) ) ).
cnf(u2210,negated_conjecture,
( ssRr(X0,skf101(X0))
| ~ ssSkP1006(X0) ) ).
cnf(u2214,negated_conjecture,
( ssRr(X0,skf102(X0))
| ~ ssSkP1007(X0) ) ).
cnf(u2218,negated_conjecture,
( ssRr(X0,skf103(X0))
| ~ ssSkP1008(X0) ) ).
cnf(u2222,negated_conjecture,
( ssRr(X0,skf104(X0))
| ~ ssSkP1009(X0) ) ).
cnf(u2226,negated_conjecture,
( ssRr(X0,skf105(X0))
| ~ ssSkP1010(X0) ) ).
cnf(u2230,negated_conjecture,
( ssRr(X0,skf106(X0))
| ~ ssSkP1011(X0) ) ).
cnf(u2234,negated_conjecture,
( ssRr(X0,skf107(X0))
| ~ ssSkP1012(X0) ) ).
cnf(u2238,negated_conjecture,
( ssRr(X0,skf108(X0))
| ~ ssSkP1013(X0) ) ).
cnf(u2242,negated_conjecture,
( ssRr(X0,skf109(X0))
| ~ ssSkP1014(X0) ) ).
cnf(u2246,negated_conjecture,
( ssRr(X0,skf110(X0))
| ~ ssSkP1015(X0) ) ).
cnf(u2250,negated_conjecture,
( ssRr(X0,skf111(X0))
| ~ ssSkP1016(X0) ) ).
cnf(u2254,negated_conjecture,
( ssRr(X0,skf112(X0))
| ~ ssSkP1017(X0) ) ).
cnf(u2258,negated_conjecture,
( ssRr(X0,skf113(X0))
| ~ ssSkP1018(X0) ) ).
cnf(u2262,negated_conjecture,
( ssRr(X0,skf114(X0))
| ~ ssSkP1019(X0) ) ).
cnf(u2266,negated_conjecture,
( ssRr(X0,skf115(X0))
| ~ ssSkP1020(X0) ) ).
cnf(u2270,negated_conjecture,
( ssRr(skf116(X0),X0)
| ~ ssSkP1022(X0) ) ).
cnf(u2274,negated_conjecture,
( ssRr(skf117(X0),X0)
| ~ ssSkP1023(X0) ) ).
cnf(u2278,negated_conjecture,
( ssRr(skf118(X0),X0)
| ~ ssSkP1024(X0) ) ).
cnf(u2282,negated_conjecture,
( ssRr(skf119(X0),X0)
| ~ ssSkP1025(X0) ) ).
cnf(u2286,negated_conjecture,
( ssRr(skf120(X0),X0)
| ~ ssSkP1026(X0) ) ).
cnf(u2290,negated_conjecture,
( ssRr(skf121(X0),X0)
| ~ ssSkP1027(X0) ) ).
cnf(u2294,negated_conjecture,
( ssRr(skf122(X0),X0)
| ~ ssSkP1028(X0) ) ).
cnf(u2298,negated_conjecture,
( ssRr(skf123(X0),X0)
| ~ ssSkP1029(X0) ) ).
cnf(u2302,negated_conjecture,
( ssRr(skf124(X0),X0)
| ~ ssSkP1030(X0) ) ).
cnf(u2306,negated_conjecture,
( ssRr(skf125(X0),X0)
| ~ ssSkP1031(X0) ) ).
cnf(u2310,negated_conjecture,
( ssRr(skf126(X0),X0)
| ~ ssSkP1032(X0) ) ).
cnf(u2314,negated_conjecture,
( ssRr(skf127(X0),X0)
| ~ ssSkP1033(X0) ) ).
cnf(u2318,negated_conjecture,
( ssRr(skf128(X0),X0)
| ~ ssSkP1034(X0) ) ).
cnf(u2322,negated_conjecture,
( ssRr(skf129(X0),X0)
| ~ ssSkP1035(X0) ) ).
cnf(u2326,negated_conjecture,
( ssRr(skf130(X0),X0)
| ~ ssSkP1036(X0) ) ).
cnf(u2330,negated_conjecture,
( ssRr(skf131(X0),X0)
| ~ ssSkP1037(X0) ) ).
cnf(u2334,negated_conjecture,
( ssRr(skf132(X0),X0)
| ~ ssSkP1038(X0) ) ).
cnf(u2338,negated_conjecture,
( ssRr(skf133(X0),X0)
| ~ ssSkP1039(X0) ) ).
cnf(u2342,negated_conjecture,
( ssRr(skf134(X0),X0)
| ~ ssSkP1040(X0) ) ).
cnf(u2346,negated_conjecture,
( ssRr(skf135(X0),X0)
| ~ ssSkP1041(X0) ) ).
cnf(u2350,negated_conjecture,
( ssRr(X0,skf136(X0))
| ~ ssSkP1064(X0) ) ).
cnf(u2354,negated_conjecture,
( ssRr(X0,skf137(X0))
| ~ ssSkP1065(X0) ) ).
cnf(u2358,negated_conjecture,
( ssRr(X0,skf138(X0))
| ~ ssSkP1066(X0) ) ).
cnf(u2362,negated_conjecture,
( ssRr(X0,skf139(X0))
| ~ ssSkP1067(X0) ) ).
cnf(u2366,negated_conjecture,
( ssRr(X0,skf140(X0))
| ~ ssSkP1068(X0) ) ).
cnf(u2370,negated_conjecture,
( ssRr(X0,skf141(X0))
| ~ ssSkP1069(X0) ) ).
cnf(u2374,negated_conjecture,
( ssRr(X0,skf142(X0))
| ~ ssSkP1070(X0) ) ).
cnf(u2378,negated_conjecture,
( ssRr(X0,skf143(X0))
| ~ ssSkP1071(X0) ) ).
cnf(u2382,negated_conjecture,
( ssRr(X0,skf144(X0))
| ~ ssSkP1072(X0) ) ).
cnf(u2386,negated_conjecture,
( ssRr(X0,skf145(X0))
| ~ ssSkP1073(X0) ) ).
cnf(u2390,negated_conjecture,
( ssRr(X0,skf146(X0))
| ~ ssSkP1074(X0) ) ).
cnf(u2394,negated_conjecture,
( ssRr(X0,skf147(X0))
| ~ ssSkP1075(X0) ) ).
cnf(u2398,negated_conjecture,
( ssRr(X0,skf148(X0))
| ~ ssSkP1076(X0) ) ).
cnf(u2402,negated_conjecture,
( ssRr(X0,skf149(X0))
| ~ ssSkP1077(X0) ) ).
cnf(u2406,negated_conjecture,
( ssRr(X0,skf150(X0))
| ~ ssSkP1078(X0) ) ).
cnf(u2410,negated_conjecture,
( ssRr(X0,skf151(X0))
| ~ ssSkP1079(X0) ) ).
cnf(u2414,negated_conjecture,
( ssRr(X0,skf152(X0))
| ~ ssSkP1080(X0) ) ).
cnf(u2418,negated_conjecture,
( ssRr(X0,skf153(X0))
| ~ ssSkP1081(X0) ) ).
cnf(u2422,negated_conjecture,
( ssRr(X0,skf154(X0))
| ~ ssSkP1082(X0) ) ).
cnf(u2426,negated_conjecture,
( ssRr(X0,skf155(X0))
| ~ ssSkP1083(X0) ) ).
cnf(u2430,negated_conjecture,
( ssRr(X0,skf156(X0))
| ~ ssSkP1085(X0) ) ).
cnf(u2434,negated_conjecture,
( ssRr(X0,skf157(X0))
| ~ ssSkP1087(X0) ) ).
cnf(u2438,negated_conjecture,
( ssRr(X0,skf158(X0))
| ~ ssSkP1089(X0) ) ).
cnf(u2442,negated_conjecture,
( ssRr(X0,skf159(X0))
| ~ ssSkP1091(X0) ) ).
cnf(u2446,negated_conjecture,
( ssRr(X0,skf160(X0))
| ~ ssSkP1093(X0) ) ).
cnf(u2450,negated_conjecture,
( ssRr(X0,skf161(X0))
| ~ ssSkP1095(X0) ) ).
cnf(u2454,negated_conjecture,
( ssRr(X0,skf162(X0))
| ~ ssSkP1099(X0) ) ).
cnf(u2458,negated_conjecture,
( ssRr(X0,skf163(X0))
| ~ ssSkP1113(X0) ) ).
cnf(u2462,negated_conjecture,
( ssRr(X0,skf164(X0))
| ~ ssSkP1115(X0) ) ).
cnf(u2466,negated_conjecture,
( ssRr(X0,skf165(X0))
| ~ ssSkP1117(X0) ) ).
cnf(u2470,negated_conjecture,
( ssRr(X0,skf166(X0))
| ~ ssSkP1119(X0) ) ).
cnf(u2474,negated_conjecture,
( ssRr(X0,skf167(X0))
| ~ ssSkP1121(X0) ) ).
cnf(u2478,negated_conjecture,
( ssRr(X0,skf168(X0))
| ~ ssSkP1123(X0) ) ).
cnf(u2482,negated_conjecture,
( ssRr(X0,skf169(X0))
| ~ ssSkP1125(X0) ) ).
cnf(u2486,negated_conjecture,
( ssRr(X0,skf170(X0))
| ~ ssSkP1127(X0) ) ).
cnf(u2490,negated_conjecture,
( ssRr(X0,skf171(X0))
| ~ ssSkP1135(X0) ) ).
cnf(u2494,negated_conjecture,
( ssRr(X0,skf172(X0))
| ~ ssSkP1145(X0) ) ).
cnf(u2498,negated_conjecture,
( ssRr(X0,skf173(X0))
| ~ ssSkP1147(X0) ) ).
cnf(u2502,negated_conjecture,
( ssRr(X0,skf174(X0))
| ~ ssSkP1149(X0) ) ).
cnf(u2506,negated_conjecture,
( ssRr(X0,skf175(X0))
| ~ ssSkP1151(X0) ) ).
cnf(u2510,negated_conjecture,
( ssRr(X0,skf176(X0))
| ~ ssSkP1153(X0) ) ).
cnf(u2514,negated_conjecture,
( ssRr(X0,skf177(X0))
| ~ ssSkP1155(X0) ) ).
cnf(u2518,negated_conjecture,
( ssRr(X0,skf178(X0))
| ~ ssSkP1157(X0) ) ).
cnf(u2522,negated_conjecture,
( ssRr(X0,skf179(X0))
| ~ ssSkP1159(X0) ) ).
cnf(u2526,negated_conjecture,
( ssRr(X0,skf180(X0))
| ~ ssSkP1171(X0) ) ).
cnf(u2530,negated_conjecture,
( ssRr(X0,skf181(X0))
| ~ ssSkP1175(X0) ) ).
cnf(u2534,negated_conjecture,
( ssRr(X0,skf182(X0))
| ~ ssSkP1177(X0) ) ).
cnf(u2538,negated_conjecture,
( ssRr(X0,skf183(X0))
| ~ ssSkP1179(X0) ) ).
cnf(u2542,negated_conjecture,
( ssRr(X0,skf184(X0))
| ~ ssSkP1181(X0) ) ).
cnf(u2546,negated_conjecture,
( ssRr(X0,skf185(X0))
| ~ ssSkP1183(X0) ) ).
cnf(u2550,negated_conjecture,
( ssRr(X0,skf186(X0))
| ~ ssSkP1185(X0) ) ).
cnf(u2554,negated_conjecture,
( ssRr(X0,skf187(X0))
| ~ ssSkP1187(X0) ) ).
cnf(u2558,negated_conjecture,
( ssRr(X0,skf188(X0))
| ~ ssSkP1189(X0) ) ).
cnf(u2562,negated_conjecture,
( ssRr(X0,skf189(X0))
| ~ ssSkP1191(X0) ) ).
cnf(u2566,negated_conjecture,
( ssSkP1189(X0)
| ~ ssSkP1190(X1)
| ~ ssSkP1021(X0,X1) ) ).
cnf(u2570,negated_conjecture,
( ssSkP1187(X0)
| ~ ssSkP1188(X1)
| ~ ssSkP1021(X0,X1) ) ).
cnf(u2574,negated_conjecture,
( ssSkP1021(X2,X0)
| ~ ssSkP1000(X2,X1)
| ~ ssRr(X0,X1) ) ).
cnf(u2578,negated_conjecture,
( ssSkP1000(X2,X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ) ).
cnf(u2582,negated_conjecture,
( ssSkP1185(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1186(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2586,negated_conjecture,
( ssSkP1183(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1184(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2590,negated_conjecture,
( ssSkP1181(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1182(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2594,negated_conjecture,
( ssSkP1179(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1180(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2598,negated_conjecture,
( ssSkP1177(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1178(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2602,negated_conjecture,
( ssSkP1175(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1176(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2606,negated_conjecture,
( ssSkP1173(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1174(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2610,negated_conjecture,
( ssSkP1171(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1172(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2614,negated_conjecture,
( ssSkP1169(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1170(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2618,negated_conjecture,
( ssSkP1167(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1168(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2622,negated_conjecture,
( ssSkP1165(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1166(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2626,negated_conjecture,
( ssSkP1163(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1164(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2630,negated_conjecture,
( ssSkP1161(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1162(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2634,negated_conjecture,
( ssSkP1159(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1160(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2638,negated_conjecture,
( ssSkP1157(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1158(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2642,negated_conjecture,
( ssSkP1155(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1156(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2646,negated_conjecture,
( ssSkP1153(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1154(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2650,negated_conjecture,
( ssSkP1151(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1152(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2654,negated_conjecture,
( ssSkP1149(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1150(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2658,negated_conjecture,
( ssSkP1147(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1148(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2662,negated_conjecture,
( ssSkP1145(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1146(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2666,negated_conjecture,
( ssSkP1143(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1144(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2670,negated_conjecture,
( ssSkP1141(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1142(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2674,negated_conjecture,
( ssSkP1139(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1140(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2678,negated_conjecture,
( ssSkP1137(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1138(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2682,negated_conjecture,
( ssSkP1135(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1136(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2686,negated_conjecture,
( ssSkP1133(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1134(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2690,negated_conjecture,
( ssSkP1131(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1132(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2694,negated_conjecture,
( ssSkP1129(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1130(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2698,negated_conjecture,
( ssSkP1127(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1128(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2702,negated_conjecture,
( ssSkP1125(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1126(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2706,negated_conjecture,
( ssSkP1123(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1124(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2710,negated_conjecture,
( ssSkP1121(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1122(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2714,negated_conjecture,
( ssSkP1119(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1120(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2718,negated_conjecture,
( ssSkP1117(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1118(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2722,negated_conjecture,
( ssSkP1115(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1116(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2726,negated_conjecture,
( ssSkP1113(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1114(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2730,negated_conjecture,
( ssSkP1111(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1112(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2734,negated_conjecture,
( ssSkP1109(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1110(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2738,negated_conjecture,
( ssSkP1107(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1108(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2742,negated_conjecture,
( ssSkP1105(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1106(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2746,negated_conjecture,
( ssSkP1103(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1104(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2750,negated_conjecture,
( ssSkP1101(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1102(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2754,negated_conjecture,
( ssSkP1099(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1100(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2758,negated_conjecture,
( ssSkP1097(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1098(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2762,negated_conjecture,
( ssSkP1095(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1096(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2766,negated_conjecture,
( ssSkP1093(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1094(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2770,negated_conjecture,
( ssSkP1091(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1092(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2774,negated_conjecture,
( ssSkP1089(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1090(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2778,negated_conjecture,
( ssSkP1087(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1088(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2782,negated_conjecture,
( ssSkP1085(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1086(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2786,negated_conjecture,
( ssSkP1063(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1084(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u2790,negated_conjecture,
( ssSkP999(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP1051(X3)
| ~ ssRr(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN908-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 17:11:34 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.12 Running first-order theorem proving
% 0.09/0.12 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.06/1.28 % (3516908)Input is clausal, will run a generic CNF schedule.
% 6.06/1.28 % (3516917)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=385442236:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.06/1.28 % (3516913)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=1985083544:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.06/1.28 % (3516919)dis-21_1_sil=8000:lcm=predicate:random_seed=208776804: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)
% 6.06/1.28 % (3516915)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3475459237:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.06/1.28 % (3516916)lrs+10_1_sil=8000:sp=occurrence:random_seed=1956848192:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.06/1.28 % (3516914)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1890370979:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.06/1.28 % (3516918)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2040621452:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.06/1.28 % (3516918)Refutation not found, incomplete strategy
% 6.06/1.28 % (3516918)------------------------------
% 6.06/1.28 % (3516918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.06/1.28 % (3516918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.28 % (3516918)CaDiCaL version: 2.1.3
% 6.06/1.28 % (3516918)Termination reason: Refutation not found, incomplete strategy
% 6.06/1.28 % (3516918)Time elapsed: 0.008 s
% 6.06/1.28 % (3516918)Peak memory usage: 90 MB
% 6.06/1.28 % (3516918)Instructions burned: 25 (million)
% 6.06/1.28 % (3516919)Instruction limit reached!
% 6.06/1.28 % (3516919)------------------------------
% 6.06/1.28 % (3516919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.06/1.28 % (3516919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.28 % (3516919)CaDiCaL version: 2.1.3
% 6.06/1.28 % (3516919)Termination reason: Instruction limit
% 6.06/1.28 % (3516919)Termination phase: Saturation
% 6.06/1.28 % (3516919)Time elapsed: 0.023 s
% 6.06/1.28 % (3516919)Peak memory usage: 90 MB
% 6.06/1.28 % (3516919)Instructions burned: 119 (million)
% 6.06/1.28 % (3516916)Instruction limit reached!
% 6.06/1.28 % (3516916)------------------------------
% 6.06/1.28 % (3516916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.06/1.28 % (3516916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.28 % (3516916)CaDiCaL version: 2.1.3
% 6.06/1.28 % (3516916)Termination reason: Instruction limit
% 6.06/1.28 % (3516916)Termination phase: Saturation
% 6.06/1.28 % (3516916)Time elapsed: 0.026 s
% 6.06/1.28 % (3516916)Peak memory usage: 91 MB
% 6.06/1.28 % (3516916)Instructions burned: 111 (million)
% 6.06/1.28 % (3516917)Instruction limit reached!
% 6.06/1.28 % (3516917)------------------------------
% 6.06/1.28 % (3516917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.06/1.28 % (3516917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.06/1.28 % (3516917)CaDiCaL version: 2.1.3
% 6.06/1.28 % (3516917)Termination reason: Instruction limit
% 6.06/1.28 % (3516917)Termination phase: Saturation
% 6.06/1.28 % (3516917)Time elapsed: 0.028 s
% 6.06/1.28 % (3516917)Peak memory usage: 90 MB
% 6.06/1.28 % (3516917)Instructions burned: 116 (million)
% 6.06/1.28 % (3516929)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3022398404:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 6.06/1.28 % (3516928)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2721280007:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 6.06/1.28 % (3516927)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=1802719151:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.06/1.28 % (3516918)------------------------------
% 6.06/1.28 % (3516918)------------------------------
% 6.06/1.28 % (3516928)Instruction limit reached!
% 6.06/1.28 % (3516928)------------------------------
% 7.45/1.49 % (3516928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516928)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516928)Termination reason: Instruction limit
% 7.45/1.49 % (3516928)Termination phase: Saturation
% 7.45/1.49 % (3516928)Time elapsed: 0.050 s
% 7.45/1.49 % (3516928)Peak memory usage: 90 MB
% 7.45/1.49 % (3516928)Instructions burned: 189 (million)
% 7.45/1.49 % (3516929)Instruction limit reached!
% 7.45/1.49 % (3516929)------------------------------
% 7.45/1.49 % (3516929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516929)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516929)Termination reason: Instruction limit
% 7.45/1.49 % (3516929)Termination phase: Saturation
% 7.45/1.49 % (3516929)Time elapsed: 0.051 s
% 7.45/1.49 % (3516929)Peak memory usage: 93 MB
% 7.45/1.49 % (3516929)Instructions burned: 223 (million)
% 7.45/1.49 % (3516927)Instruction limit reached!
% 7.45/1.49 % (3516927)------------------------------
% 7.45/1.49 % (3516927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516927)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516927)Termination reason: Instruction limit
% 7.45/1.49 % (3516927)Termination phase: Saturation
% 7.45/1.49 % (3516927)Time elapsed: 0.035 s
% 7.45/1.49 % (3516927)Peak memory usage: 91 MB
% 7.45/1.49 % (3516927)Instructions burned: 144 (million)
% 7.45/1.49 % (3516933)lrs+10_64_to=lpo:sil=8000:random_seed=4173940553:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.45/1.49 % (3516936)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=74700177:i=3394:sd=4:ss=included:sgt=64_2997 on theBenchmark for (2997ds/3394Mi)
% 7.45/1.49 % (3516934)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1903600455:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 7.45/1.49 % (3516935)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2195919177:i=157:gtg=all_2997 on theBenchmark for (2997ds/157Mi)
% 7.45/1.49 % (3516934)Refutation not found, incomplete strategy
% 7.45/1.49 % (3516934)------------------------------
% 7.45/1.49 % (3516934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516934)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516934)Termination reason: Refutation not found, incomplete strategy
% 7.45/1.49 % (3516934)Time elapsed: 0.005 s
% 7.45/1.49 % (3516934)Peak memory usage: 90 MB
% 7.45/1.49 % (3516934)Instructions burned: 14 (million)
% 7.45/1.49 % (3516933)Instruction limit reached!
% 7.45/1.49 % (3516933)------------------------------
% 7.45/1.49 % (3516933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516933)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516933)Termination reason: Instruction limit
% 7.45/1.49 % (3516933)Termination phase: Saturation
% 7.45/1.49 % (3516933)Time elapsed: 0.040 s
% 7.45/1.49 % (3516933)Peak memory usage: 95 MB
% 7.45/1.49 % (3516933)Instructions burned: 130 (million)
% 7.45/1.49 % (3516935)Instruction limit reached!
% 7.45/1.49 % (3516935)------------------------------
% 7.45/1.49 % (3516935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516935)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516935)Termination reason: Instruction limit
% 7.45/1.49 % (3516935)Termination phase: Saturation
% 7.45/1.49 % (3516935)Time elapsed: 0.038 s
% 7.45/1.49 % (3516935)Peak memory usage: 91 MB
% 7.45/1.49 % (3516935)Instructions burned: 159 (million)
% 7.45/1.49 % (3516941)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=2728308438:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2996 on theBenchmark for (2996ds/106Mi)
% 7.45/1.49 % (3516942)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3539375723:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 7.45/1.49 % (3516941)Instruction limit reached!
% 7.45/1.49 % (3516941)------------------------------
% 7.45/1.49 % (3516941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516941)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516941)Termination reason: Instruction limit
% 7.45/1.49 % (3516941)Termination phase: Saturation
% 7.45/1.49 % (3516941)Time elapsed: 0.030 s
% 7.45/1.49 % (3516941)Peak memory usage: 91 MB
% 7.45/1.49 % (3516941)Instructions burned: 108 (million)
% 7.45/1.49 % (3516934)------------------------------
% 7.45/1.49 % (3516934)------------------------------
% 7.45/1.49 % (3516942)Instruction limit reached!
% 7.45/1.49 % (3516942)------------------------------
% 7.45/1.49 % (3516942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516942)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516942)Termination reason: Instruction limit
% 7.45/1.49 % (3516942)Termination phase: Saturation
% 7.45/1.49 % (3516942)Time elapsed: 0.033 s
% 7.45/1.49 % (3516942)Peak memory usage: 94 MB
% 7.45/1.49 % (3516942)Instructions burned: 108 (million)
% 7.45/1.49 % (3516945)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2186806678:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 7.45/1.49 % (3516945)Refutation not found, incomplete strategy
% 7.45/1.49 % (3516945)------------------------------
% 7.45/1.49 % (3516945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516945)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516945)Termination reason: Refutation not found, incomplete strategy
% 7.45/1.49 % (3516945)Time elapsed: 0.009 s
% 7.45/1.49 % (3516945)Peak memory usage: 90 MB
% 7.45/1.49 % (3516945)Instructions burned: 33 (million)
% 7.45/1.49 % (3516946)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=625260924:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi)
% 7.45/1.49 % (3516947)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3520321435:i=134:sd=2:doe=on:ss=axioms:sgt=14_2994 on theBenchmark for (2994ds/134Mi)
% 7.45/1.49 % (3516947)Refutation not found, incomplete strategy
% 7.45/1.49 % (3516947)------------------------------
% 7.45/1.49 % (3516947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516947)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516947)Termination reason: Refutation not found, incomplete strategy
% 7.45/1.49 % (3516947)Time elapsed: 0.008 s
% 7.45/1.49 % (3516947)Peak memory usage: 90 MB
% 7.45/1.49 % (3516947)Instructions burned: 26 (million)
% 7.45/1.49 % (3516945)------------------------------
% 7.45/1.49 % (3516945)------------------------------
% 7.45/1.49 % (3516947)------------------------------
% 7.45/1.49 % (3516947)------------------------------
% 7.45/1.49 % (3516951)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=595389512:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 7.45/1.49 % (3516952)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3725963742:i=191:fgj=on:bd=all_2992 on theBenchmark for (2992ds/191Mi)
% 7.45/1.49 % (3516952)Instruction limit reached!
% 7.45/1.49 % (3516952)------------------------------
% 7.45/1.49 % (3516952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516952)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516952)Termination reason: Instruction limit
% 7.45/1.49 % (3516952)Termination phase: Saturation
% 7.45/1.49 % (3516952)Time elapsed: 0.048 s
% 7.45/1.49 % (3516952)Peak memory usage: 94 MB
% 7.45/1.49 % (3516952)Instructions burned: 195 (million)
% 7.45/1.49 % (3516951)Instruction limit reached!
% 7.45/1.49 % (3516951)------------------------------
% 7.45/1.49 % (3516951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516951)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516951)Termination reason: Instruction limit
% 7.45/1.49 % (3516951)Termination phase: Saturation
% 7.45/1.49 % (3516951)Time elapsed: 0.134 s
% 7.45/1.49 % (3516951)Peak memory usage: 94 MB
% 7.45/1.49 % (3516951)Instructions burned: 500 (million)
% 7.45/1.49 % (3516955)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=718035999:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 7.45/1.49 % (3516955)First to succeed.
% 7.45/1.49 % (3516955)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3516908"
% 7.45/1.49 % (3516956)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=414997781:cond=on:i=156:bs=on:gtg=exists_all:er=known_2990 on theBenchmark for (2990ds/156Mi)
% 7.45/1.49 % (3516956)Instruction limit reached!
% 7.45/1.49 % (3516956)------------------------------
% 7.45/1.49 % (3516956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.49 % (3516956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.49 % (3516956)CaDiCaL version: 2.1.3
% 7.45/1.49 % (3516956)Termination reason: Instruction limit
% 7.45/1.49 % (3516956)Termination phase: Saturation
% 7.45/1.49 % (3516956)Time elapsed: 0.039 s
% 7.45/1.49 % (3516956)Peak memory usage: 91 MB
% 7.45/1.49 % (3516956)Instructions burned: 160 (million)
% 7.45/1.49 % SZS status Satisfiable for theBenchmark
% 7.45/1.49 % SZS output start Saturation.
% See solution above
% 7.45/1.49 % SZS output start Definitions and Model Updates.
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv23(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv18(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv38(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv40(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP630(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP631(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC13 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP682(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP681(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP680(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP679(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP678(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP677(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP676(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP675(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP674(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP673(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP672(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP671(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP670(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP669(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP668(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP667(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP666(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP665(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP664(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP663(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP662(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP661(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP660(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP659(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP658(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP657(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP952(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP953(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC19 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP998(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP997(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP996(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP995(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP994(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP993(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP992(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP991(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP990(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP989(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP988(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP987(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP986(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP985(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP984(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP983(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP982(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP981(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP980(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP979(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP978(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP977(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP976(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP975(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP974(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP973(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP972(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP971(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP970(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP969(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP968(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP967(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP966(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP965(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP964(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP963(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP962(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP961(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP960(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP959(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP958(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP957(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP954(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP955(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP956(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv17(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP632(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP633(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP634(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP635(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP636(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP637(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP638(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP639(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP640(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP641(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP642(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP643(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP644(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP645(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP646(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP647(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP648(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP649(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP650(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP651(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP652(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP653(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP654(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP655(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP656(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv33(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP484(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP485(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC10 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP527(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP526(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP525(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP524(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP523(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP522(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP521(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP520(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP519(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP486(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP487(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP488(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP489(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP490(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP491(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP492(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP493(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP494(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP495(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP496(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP497(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP498(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP499(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP500(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP501(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP502(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP503(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP504(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP505(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP506(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP507(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP508(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP509(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP510(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP511(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP512(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP513(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP514(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP515(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP516(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP517(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP518(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP423(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP424(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC9 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP483(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP482(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP481(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP480(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP479(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP478(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP477(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP476(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP475(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP729(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP730(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC15 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP789(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP788(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP787(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP786(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP785(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP784(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP783(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP782(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP781(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP780(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP779(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP778(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP777(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP776(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP775(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP774(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP773(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP772(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP771(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP770(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP769(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP768(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP767(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP766(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP765(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP764(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP763(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP762(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP761(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP760(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP759(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP758(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP757(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP756(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP755(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP754(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP753(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP752(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP751(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP750(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP749(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP748(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP747(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP746(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP745(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP744(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP743(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP742(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP741(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP740(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP739(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP738(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP737(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP736(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP735(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP734(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP733(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP732(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP731(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv1(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP425(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP426(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP427(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP428(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP429(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP430(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP431(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP432(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP433(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP434(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP435(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP436(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP437(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP438(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP439(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP440(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP441(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP442(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP443(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP444(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP445(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP446(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP447(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP448(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP449(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP450(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP451(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP452(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP453(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP454(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP455(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP456(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP457(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP458(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP459(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP460(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP461(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP462(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP463(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP464(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP465(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP466(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP467(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP468(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP469(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP470(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP471(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP472(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP473(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP474(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP37(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP38(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC1 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP71(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP70(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP0(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP1(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC0 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP36(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP35(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP2(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP3(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP4(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP5(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP6(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP7(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP8(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP9(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP10(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP11(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP12(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP13(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP14(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP15(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP16(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP17(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP18(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP19(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP20(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP21(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP22(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP23(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP24(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP25(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP26(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP27(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP28(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP29(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP30(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP31(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP32(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP33(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP34(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv56(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP69(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP68(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP67(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP66(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP65(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP64(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP63(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP62(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP39(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP40(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP41(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP42(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP43(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP44(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP45(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP46(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP47(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP48(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP49(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP50(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP51(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP52(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP53(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP54(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP55(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP56(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP57(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP58(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP59(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP60(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP61(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv49(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv51(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv54(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv24(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv19(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP683(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP684(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC14 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP728(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP727(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP726(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP725(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP724(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP723(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP722(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP721(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP720(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP719(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP718(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP717(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP716(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP715(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP714(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP713(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP712(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP711(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP710(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP709(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP685(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP686(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP687(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP688(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP689(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP690(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP691(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP692(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP693(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP694(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP695(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP696(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP697(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP698(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP699(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP700(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP701(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP702(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP703(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP704(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP705(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP706(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP707(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP708(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv39(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv36(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP314(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP315(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC7 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP362(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP361(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP360(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP359(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP358(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP357(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP356(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP355(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP790(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP791(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC16 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP840(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP839(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP838(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP837(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP836(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP835(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP834(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP833(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP832(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP831(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP830(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP829(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP828(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP827(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP826(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP825(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP824(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP823(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP822(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP821(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP820(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP819(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP818(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP817(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP816(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP815(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP814(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP813(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP812(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP811(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP810(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP809(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP808(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP807(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP806(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP805(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP804(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP803(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP802(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP792(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP793(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP794(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP795(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP796(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP797(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP798(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP799(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP800(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP801(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP528(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP529(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC11 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP580(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP579(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP578(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP577(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP576(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP575(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP574(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP573(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP572(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP571(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP570(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP569(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP568(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP567(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP566(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP565(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP564(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP563(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP562(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP561(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP560(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP559(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP558(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP557(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP556(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP555(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP554(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP553(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP552(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP551(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP550(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP549(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP548(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP547(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP546(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP545(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP544(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP543(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP542(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP541(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP530(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP531(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP532(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP533(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP534(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP535(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP536(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP537(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP538(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP539(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP540(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv20(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP316(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP317(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP318(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP319(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP320(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP321(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP322(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP323(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP324(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP325(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP326(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP327(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP328(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP329(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP330(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP331(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP332(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP333(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP334(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP335(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP336(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP337(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP338(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP339(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP340(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP341(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP342(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP343(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP344(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP345(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP346(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP347(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP348(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP349(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP350(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP351(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP352(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP353(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP354(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv50(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP126(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP127(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC3 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP174(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP173(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP172(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP171(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP170(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP128(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP129(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP130(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP131(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP132(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP133(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP134(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP135(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP136(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP137(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP138(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP139(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP140(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP141(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP142(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP143(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP144(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP145(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP146(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP147(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP148(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP149(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP150(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP151(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP152(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP153(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP154(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP155(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP156(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP157(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP158(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP159(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP160(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP161(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP162(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP163(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP164(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP165(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP166(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP167(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP168(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP169(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv53(X0) := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP897(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP898(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC18 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP951(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP950(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP949(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP948(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP947(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP946(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP945(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP944(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP943(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP942(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP941(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP940(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP939(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP938(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP937(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP936(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP935(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP934(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP933(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP932(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP931(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP930(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP929(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP928(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP927(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP926(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP925(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP924(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP923(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP922(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP921(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP920(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP919(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP918(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP917(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP916(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP915(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP914(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP913(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP912(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP911(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP910(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP909(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP908(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP907(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP906(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP905(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP904(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP903(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP902(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP901(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP900(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP899(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv7(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP363(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP364(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC8 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP422(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP421(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP420(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP419(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP418(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP417(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP416(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP415(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP414(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP413(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP412(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP411(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP410(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP409(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP408(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP407(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP406(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP405(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP404(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP403(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP402(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP401(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP400(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP399(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP398(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP397(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP396(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP395(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP394(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP393(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP392(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP391(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP390(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP389(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP388(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP387(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP386(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP385(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP384(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP383(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP382(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP381(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP380(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP379(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP378(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP377(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP376(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP375(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP374(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP373(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP372(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP371(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP370(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP369(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP368(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP367(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP366(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP365(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssPv2(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP72(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP73(X0,X1) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkC2 := $false
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP125(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP124(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP123(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP122(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP121(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP120(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP119(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP118(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP117(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP116(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP115(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP114(X0) := $true
% 7.45/1.49 for all inputs,
% 7.45/1.49 define ssSkP113(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP112(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP111(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP110(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP109(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP108(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP107(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP106(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP105(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP104(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP103(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP102(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP101(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP100(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP99(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP98(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP97(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP96(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP95(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP94(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP93(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP92(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP91(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP90(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP89(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP88(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP87(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP86(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP85(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP84(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP83(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP82(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP81(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP80(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP79(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP78(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP77(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP76(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP75(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP74(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssPv8(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP256(X0,X1) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP257(X0,X1) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkC6 := $false
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP313(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP312(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP311(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP310(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP309(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP308(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP200(X0,X1) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP201(X0,X1) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkC5 := $false
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP255(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP254(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP253(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP252(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP251(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP250(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP841(X0,X1) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP842(X0,X1) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkC17 := $false
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP896(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP895(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP894(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP893(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP892(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP891(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP890(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP889(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP888(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP887(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP886(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP885(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP884(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP883(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP882(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP881(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP880(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP879(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP878(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP877(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP876(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP875(X0) := $true
% 7.45/1.50 for all inputs,
% 7.45/1.50 define ssSkP874(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP873(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP872(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP871(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP870(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP869(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP868(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP867(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP866(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP865(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP864(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP863(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP862(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP861(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP860(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP859(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP858(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP857(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP856(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP855(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP854(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP853(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP852(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP851(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP850(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP849(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP848(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP847(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP846(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP845(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP844(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP843(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssPv6(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP202(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP203(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP204(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP205(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP206(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP207(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP208(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP209(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP210(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP211(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP212(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP213(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP214(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP215(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP216(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP217(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP218(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP219(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP220(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP221(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP222(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP223(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP224(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP225(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP226(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP227(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP228(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP229(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP230(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP231(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP232(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP233(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP234(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP235(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP236(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP237(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP238(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP239(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP240(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP241(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP242(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP243(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP244(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP245(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP246(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP247(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP248(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP249(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP175(X0,X1) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP176(X0,X1) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkC4 := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP199(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP198(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP197(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP196(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP195(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP194(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP581(X0,X1) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP582(X0,X1) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkC12 := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP629(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP628(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP627(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP626(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP625(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP624(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP623(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP622(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP621(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP620(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP619(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP618(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP617(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP616(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP615(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP614(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP613(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP612(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP611(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP610(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP609(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP608(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP583(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP584(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP585(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP586(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP587(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP588(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP589(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP590(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP591(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP592(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP593(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP594(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP595(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP596(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP597(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP598(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP599(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP600(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP601(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP602(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP603(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP604(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP605(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP606(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP607(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssPv37(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP177(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP178(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP179(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP180(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP181(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP182(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP183(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP184(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP185(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP186(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP187(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP188(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP189(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP190(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP191(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP192(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP193(X0) := $false
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssPv52(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP307(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP306(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP305(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP304(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP303(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP302(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP301(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP300(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP299(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP298(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP297(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP296(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP295(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP294(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP293(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP292(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP291(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP290(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP289(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP288(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP287(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP286(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP285(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP284(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP283(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP282(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP281(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP280(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP279(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP278(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP277(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP276(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP275(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP274(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP273(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP272(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP271(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP270(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP269(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP268(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP267(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP266(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP265(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP264(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP263(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP262(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP261(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP260(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP259(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssSkP258(X0) := $true
% 8.40/1.58 for all inputs,
% 8.40/1.58 define ssPv4(X0) := $false
% 8.40/1.58 % SZS output end Definitions and Model Updates.
% 8.40/1.58 % (3516955)------------------------------
% 8.40/1.58 % (3516955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.40/1.58 % (3516955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/1.58 % (3516955)CaDiCaL version: 2.1.3
% 8.40/1.58 % (3516955)Termination reason: Satisfiable
% 8.40/1.58 % (3516955)Time elapsed: 0.013 s
% 8.40/1.58 % (3516955)Peak memory usage: 90 MB
% 8.40/1.58 % (3516955)Instructions burned: 40 (million)
% 8.40/1.58 % (3516955)------------------------------
% 8.40/1.58 % (3516955)------------------------------
% 8.40/1.58 % (3516908)Success in time 1.179 s
% 8.40/1.58 % Vampire exiting
%------------------------------------------------------------------------------