%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN907-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 : n001.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 14.19s 2.76s
% Output : Saturation 14.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u795,negated_conjecture,
~ ssSkC20 ).
cnf(u800,negated_conjecture,
ssSkP677(skc41) ).
cnf(u804,negated_conjecture,
( ssSkP591(X0)
| ~ ssSkP602(X0) ) ).
cnf(u808,negated_conjecture,
( ssPv24(X0)
| ~ ssSkP602(X0) ) ).
cnf(u812,negated_conjecture,
( ssSkP592(X0)
| ~ ssSkP603(X0) ) ).
cnf(u816,negated_conjecture,
( ssPv14(X0)
| ~ ssSkP603(X0) ) ).
cnf(u820,negated_conjecture,
( ssSkP594(X0)
| ~ ssSkP604(X0) ) ).
cnf(u824,negated_conjecture,
( ssPv23(X0)
| ~ ssSkP604(X0) ) ).
cnf(u828,negated_conjecture,
( ssSkP601(X0)
| ~ ssSkP605(X0) ) ).
cnf(u832,negated_conjecture,
( ssPv6(X0)
| ~ ssSkP605(X0) ) ).
cnf(u836,negated_conjecture,
( ssSkP597(X0)
| ~ ssSkP606(X0) ) ).
cnf(u840,negated_conjecture,
( ssPv22(X0)
| ~ ssSkP606(X0) ) ).
cnf(u844,negated_conjecture,
( ssSkP599(X0)
| ~ ssSkP607(X0) ) ).
cnf(u848,negated_conjecture,
( ssPv8(X0)
| ~ ssSkP607(X0) ) ).
cnf(u852,negated_conjecture,
( ssSkP600(X0)
| ~ ssSkP608(X0) ) ).
cnf(u856,negated_conjecture,
( ssPv21(X0)
| ~ ssSkP608(X0) ) ).
cnf(u860,negated_conjecture,
( ssSkP593(X0)
| ~ ssSkP610(X0) ) ).
cnf(u864,negated_conjecture,
( ssPv16(X0)
| ~ ssSkP610(X0) ) ).
cnf(u868,negated_conjecture,
( ssSkP596(X0)
| ~ ssSkP611(X0) ) ).
cnf(u872,negated_conjecture,
( ssPv7(X0)
| ~ ssSkP611(X0) ) ).
cnf(u876,negated_conjecture,
( ssSkP598(X0)
| ~ ssSkP612(X0) ) ).
cnf(u880,negated_conjecture,
( ssPv15(X0)
| ~ ssSkP612(X0) ) ).
cnf(u884,negated_conjecture,
( ssSkP595(X0)
| ~ ssSkP613(X0) ) ).
cnf(u888,negated_conjecture,
( ssPv5(X0)
| ~ ssSkP613(X0) ) ).
cnf(u892,negated_conjecture,
( ssSkP577(X0)
| ~ ssSkP614(X0) ) ).
cnf(u896,negated_conjecture,
( ssSkP609(X0)
| ~ ssSkP614(X0) ) ).
cnf(u900,negated_conjecture,
( ssSkP626(X0)
| ~ ssSkP627(X0) ) ).
cnf(u904,negated_conjecture,
( ssSkP628(X0)
| ~ ssSkP629(X0) ) ).
cnf(u908,negated_conjecture,
( ssSkP625(X0)
| ~ ssSkP631(X0) ) ).
cnf(u912,negated_conjecture,
( ssSkP630(X0)
| ~ ssSkP631(X0) ) ).
cnf(u916,negated_conjecture,
( ssSkP624(X0)
| ~ ssSkP633(X0) ) ).
cnf(u920,negated_conjecture,
( ssSkP632(X0)
| ~ ssSkP633(X0) ) ).
cnf(u924,negated_conjecture,
( ssSkP623(X0)
| ~ ssSkP635(X0) ) ).
cnf(u928,negated_conjecture,
( ssSkP634(X0)
| ~ ssSkP635(X0) ) ).
cnf(u932,negated_conjecture,
( ssSkP622(X0)
| ~ ssSkP637(X0) ) ).
cnf(u936,negated_conjecture,
( ssSkP636(X0)
| ~ ssSkP637(X0) ) ).
cnf(u940,negated_conjecture,
( ssSkP638(X0)
| ~ ssSkP639(X0) ) ).
cnf(u944,negated_conjecture,
( ssSkP640(X0)
| ~ ssSkP641(X0) ) ).
cnf(u948,negated_conjecture,
( ssSkP642(X0)
| ~ ssSkP643(X0) ) ).
cnf(u952,negated_conjecture,
( ssSkP644(X0)
| ~ ssSkP645(X0) ) ).
cnf(u956,negated_conjecture,
( ssSkP646(X0)
| ~ ssSkP647(X0) ) ).
cnf(u960,negated_conjecture,
( ssSkP621(X0)
| ~ ssSkP649(X0) ) ).
cnf(u964,negated_conjecture,
( ssSkP648(X0)
| ~ ssSkP649(X0) ) ).
cnf(u968,negated_conjecture,
( ssSkP620(X0)
| ~ ssSkP651(X0) ) ).
cnf(u972,negated_conjecture,
( ssSkP650(X0)
| ~ ssSkP651(X0) ) ).
cnf(u976,negated_conjecture,
( ssSkP619(X0)
| ~ ssSkP653(X0) ) ).
cnf(u980,negated_conjecture,
( ssSkP652(X0)
| ~ ssSkP653(X0) ) ).
cnf(u984,negated_conjecture,
( ssSkP654(X0)
| ~ ssSkP655(X0) ) ).
cnf(u988,negated_conjecture,
( ssSkP656(X0)
| ~ ssSkP657(X0) ) ).
cnf(u992,negated_conjecture,
( ssSkP658(X0)
| ~ ssSkP659(X0) ) ).
cnf(u996,negated_conjecture,
( ssSkP660(X0)
| ~ ssSkP661(X0) ) ).
cnf(u1000,negated_conjecture,
( ssSkP618(X0)
| ~ ssSkP663(X0) ) ).
cnf(u1004,negated_conjecture,
( ssSkP662(X0)
| ~ ssSkP663(X0) ) ).
cnf(u1008,negated_conjecture,
( ssSkP617(X0)
| ~ ssSkP665(X0) ) ).
cnf(u1012,negated_conjecture,
( ssSkP664(X0)
| ~ ssSkP665(X0) ) ).
cnf(u1016,negated_conjecture,
( ssSkP616(X0)
| ~ ssSkP667(X0) ) ).
cnf(u1020,negated_conjecture,
( ssSkP666(X0)
| ~ ssSkP667(X0) ) ).
cnf(u1024,negated_conjecture,
( ssSkP615(X0)
| ~ ssSkP669(X0) ) ).
cnf(u1028,negated_conjecture,
( ssSkP668(X0)
| ~ ssSkP669(X0) ) ).
cnf(u1032,negated_conjecture,
( ssSkP670(X0)
| ~ ssSkP671(X0) ) ).
cnf(u1036,negated_conjecture,
( ssSkP672(X0)
| ~ ssSkP673(X0) ) ).
cnf(u1040,negated_conjecture,
( ssSkP674(X0)
| ~ ssSkP675(X0) ) ).
cnf(u1044,negated_conjecture,
( ssSkP676(X0)
| ~ ssSkP677(X0) ) ).
cnf(u1048,negated_conjecture,
( ssSkP579(skf61(X0))
| ~ ssSkP591(X0) ) ).
cnf(u1052,negated_conjecture,
( ssSkP589(skf62(X0))
| ~ ssSkP592(X0) ) ).
cnf(u1056,negated_conjecture,
( ssSkP586(skf63(X0))
| ~ ssSkP593(X0) ) ).
cnf(u1060,negated_conjecture,
( ssSkP583(skf64(X0))
| ~ ssSkP594(X0) ) ).
cnf(u1064,negated_conjecture,
( ssSkP584(skf65(X0))
| ~ ssSkP595(X0) ) ).
cnf(u1068,negated_conjecture,
( ssSkP580(skf66(X0))
| ~ ssSkP596(X0) ) ).
cnf(u1072,negated_conjecture,
( ssSkP587(skf67(X0))
| ~ ssSkP597(X0) ) ).
cnf(u1076,negated_conjecture,
( ssSkP582(skf68(X0))
| ~ ssSkP598(X0) ) ).
cnf(u1080,negated_conjecture,
( ssSkP588(skf69(X0))
| ~ ssSkP599(X0) ) ).
cnf(u1084,negated_conjecture,
( ssSkP581(skf70(X0))
| ~ ssSkP600(X0) ) ).
cnf(u1088,negated_conjecture,
( ssSkP585(skf71(X0))
| ~ ssSkP601(X0) ) ).
cnf(u1092,negated_conjecture,
( ssSkP602(skf72(X0))
| ~ ssSkP615(X0) ) ).
cnf(u1096,negated_conjecture,
( ssSkP604(skf73(X0))
| ~ ssSkP616(X0) ) ).
cnf(u1100,negated_conjecture,
( ssSkP606(skf74(X0))
| ~ ssSkP617(X0) ) ).
cnf(u1104,negated_conjecture,
( ssSkP608(skf75(X0))
| ~ ssSkP618(X0) ) ).
cnf(u1108,negated_conjecture,
( ssSkP610(skf76(X0))
| ~ ssSkP619(X0) ) ).
cnf(u1112,negated_conjecture,
( ssSkP612(skf77(X0))
| ~ ssSkP620(X0) ) ).
cnf(u1116,negated_conjecture,
( ssSkP603(skf78(X0))
| ~ ssSkP621(X0) ) ).
cnf(u1120,negated_conjecture,
( ssSkP607(skf79(X0))
| ~ ssSkP622(X0) ) ).
cnf(u1124,negated_conjecture,
( ssSkP611(skf80(X0))
| ~ ssSkP623(X0) ) ).
cnf(u1128,negated_conjecture,
( ssSkP605(skf81(X0))
| ~ ssSkP624(X0) ) ).
cnf(u1132,negated_conjecture,
( ssSkP613(skf82(X0))
| ~ ssSkP625(X0) ) ).
cnf(u1136,negated_conjecture,
( ~ ssPv24(skf50(X0))
| ~ ssSkP579(X0) ) ).
cnf(u1140,negated_conjecture,
( ~ ssPv7(skf51(X0))
| ~ ssSkP580(X0) ) ).
cnf(u1144,negated_conjecture,
( ~ ssPv21(skf52(X0))
| ~ ssSkP581(X0) ) ).
cnf(u1148,negated_conjecture,
( ~ ssPv15(skf53(X0))
| ~ ssSkP582(X0) ) ).
cnf(u1152,negated_conjecture,
( ~ ssPv23(skf54(X0))
| ~ ssSkP583(X0) ) ).
cnf(u1156,negated_conjecture,
( ~ ssPv5(skf55(X0))
| ~ ssSkP584(X0) ) ).
cnf(u1160,negated_conjecture,
( ~ ssPv6(skf56(X0))
| ~ ssSkP585(X0) ) ).
cnf(u1164,negated_conjecture,
( ~ ssPv16(skf57(X0))
| ~ ssSkP586(X0) ) ).
cnf(u1168,negated_conjecture,
( ~ ssPv22(skf58(X0))
| ~ ssSkP587(X0) ) ).
cnf(u1172,negated_conjecture,
( ~ ssPv8(skf59(X0))
| ~ ssSkP588(X0) ) ).
cnf(u1176,negated_conjecture,
( ~ ssPv14(skf60(X0))
| ~ ssSkP589(X0) ) ).
cnf(u1191,negated_conjecture,
( ~ ssSkP602(skf50(X0))
| ~ ssSkP579(X0) ) ).
cnf(u1195,negated_conjecture,
( ~ ssSkP611(skf51(X0))
| ~ ssSkP580(X0) ) ).
cnf(u1199,negated_conjecture,
( ~ ssSkP608(skf52(X0))
| ~ ssSkP581(X0) ) ).
cnf(u1203,negated_conjecture,
( ~ ssSkP612(skf53(X0))
| ~ ssSkP582(X0) ) ).
cnf(u1207,negated_conjecture,
( ~ ssSkP604(skf54(X0))
| ~ ssSkP583(X0) ) ).
cnf(u1211,negated_conjecture,
( ~ ssSkP613(skf55(X0))
| ~ ssSkP584(X0) ) ).
cnf(u1215,negated_conjecture,
( ~ ssSkP605(skf56(X0))
| ~ ssSkP585(X0) ) ).
cnf(u1219,negated_conjecture,
( ssRr(X0,skf49(X0))
| ~ ssSkP577(X0) ) ).
cnf(u1223,negated_conjecture,
( ~ ssSkP610(skf57(X0))
| ~ ssSkP586(X0) ) ).
cnf(u1227,negated_conjecture,
( ~ ssSkP606(skf58(X0))
| ~ ssSkP587(X0) ) ).
cnf(u1231,negated_conjecture,
( ~ ssSkP607(skf59(X0))
| ~ ssSkP588(X0) ) ).
cnf(u1235,negated_conjecture,
( ~ ssSkP603(skf60(X0))
| ~ ssSkP589(X0) ) ).
cnf(u1239,negated_conjecture,
( ssRr(X0,skf50(X0))
| ~ ssSkP579(X0) ) ).
cnf(u1243,negated_conjecture,
( ssRr(X0,skf51(X0))
| ~ ssSkP580(X0) ) ).
cnf(u1247,negated_conjecture,
( ssRr(X0,skf52(X0))
| ~ ssSkP581(X0) ) ).
cnf(u1251,negated_conjecture,
( ssRr(X0,skf53(X0))
| ~ ssSkP582(X0) ) ).
cnf(u1255,negated_conjecture,
( ssRr(X0,skf54(X0))
| ~ ssSkP583(X0) ) ).
cnf(u1259,negated_conjecture,
( ssRr(X0,skf55(X0))
| ~ ssSkP584(X0) ) ).
cnf(u1263,negated_conjecture,
( ssRr(X0,skf56(X0))
| ~ ssSkP585(X0) ) ).
cnf(u1267,negated_conjecture,
( ssRr(X0,skf57(X0))
| ~ ssSkP586(X0) ) ).
cnf(u1271,negated_conjecture,
( ssRr(X0,skf58(X0))
| ~ ssSkP587(X0) ) ).
cnf(u1275,negated_conjecture,
( ssRr(X0,skf59(X0))
| ~ ssSkP588(X0) ) ).
cnf(u1279,negated_conjecture,
( ssRr(X0,skf60(X0))
| ~ ssSkP589(X0) ) ).
cnf(u1283,negated_conjecture,
( ssRr(skf61(X0),X0)
| ~ ssSkP591(X0) ) ).
cnf(u1287,negated_conjecture,
( ssRr(skf62(X0),X0)
| ~ ssSkP592(X0) ) ).
cnf(u1291,negated_conjecture,
( ssRr(skf63(X0),X0)
| ~ ssSkP593(X0) ) ).
cnf(u1295,negated_conjecture,
( ssRr(skf64(X0),X0)
| ~ ssSkP594(X0) ) ).
cnf(u1299,negated_conjecture,
( ssRr(skf65(X0),X0)
| ~ ssSkP595(X0) ) ).
cnf(u1303,negated_conjecture,
( ssRr(skf66(X0),X0)
| ~ ssSkP596(X0) ) ).
cnf(u1307,negated_conjecture,
( ssRr(skf67(X0),X0)
| ~ ssSkP597(X0) ) ).
cnf(u1311,negated_conjecture,
( ssRr(skf68(X0),X0)
| ~ ssSkP598(X0) ) ).
cnf(u1315,negated_conjecture,
( ssRr(skf69(X0),X0)
| ~ ssSkP599(X0) ) ).
cnf(u1319,negated_conjecture,
( ssRr(skf70(X0),X0)
| ~ ssSkP600(X0) ) ).
cnf(u1323,negated_conjecture,
( ssRr(skf71(X0),X0)
| ~ ssSkP601(X0) ) ).
cnf(u1327,negated_conjecture,
( ssRr(X0,skf72(X0))
| ~ ssSkP615(X0) ) ).
cnf(u1331,negated_conjecture,
( ssRr(X0,skf73(X0))
| ~ ssSkP616(X0) ) ).
cnf(u1335,negated_conjecture,
( ssRr(X0,skf74(X0))
| ~ ssSkP617(X0) ) ).
cnf(u1339,negated_conjecture,
( ssRr(X0,skf75(X0))
| ~ ssSkP618(X0) ) ).
cnf(u1343,negated_conjecture,
( ssRr(X0,skf76(X0))
| ~ ssSkP619(X0) ) ).
cnf(u1347,negated_conjecture,
( ssRr(X0,skf77(X0))
| ~ ssSkP620(X0) ) ).
cnf(u1351,negated_conjecture,
( ssRr(X0,skf78(X0))
| ~ ssSkP621(X0) ) ).
cnf(u1355,negated_conjecture,
( ssRr(X0,skf79(X0))
| ~ ssSkP622(X0) ) ).
cnf(u1359,negated_conjecture,
( ssRr(X0,skf80(X0))
| ~ ssSkP623(X0) ) ).
cnf(u1363,negated_conjecture,
( ssRr(X0,skf81(X0))
| ~ ssSkP624(X0) ) ).
cnf(u1367,negated_conjecture,
( ssRr(X0,skf82(X0))
| ~ ssSkP625(X0) ) ).
cnf(u1371,negated_conjecture,
( ssRr(X0,skf83(X0))
| ~ ssSkP627(X0) ) ).
cnf(u1375,negated_conjecture,
( ssRr(X0,skf84(X0))
| ~ ssSkP629(X0) ) ).
cnf(u1379,negated_conjecture,
( ssRr(X0,skf85(X0))
| ~ ssSkP639(X0) ) ).
cnf(u1383,negated_conjecture,
( ssRr(X0,skf86(X0))
| ~ ssSkP641(X0) ) ).
cnf(u1387,negated_conjecture,
( ssRr(X0,skf87(X0))
| ~ ssSkP643(X0) ) ).
cnf(u1391,negated_conjecture,
( ssRr(X0,skf88(X0))
| ~ ssSkP645(X0) ) ).
cnf(u1395,negated_conjecture,
( ssRr(X0,skf89(X0))
| ~ ssSkP647(X0) ) ).
cnf(u1399,negated_conjecture,
( ssRr(X0,skf90(X0))
| ~ ssSkP655(X0) ) ).
cnf(u1403,negated_conjecture,
( ssRr(X0,skf91(X0))
| ~ ssSkP657(X0) ) ).
cnf(u1407,negated_conjecture,
( ssRr(X0,skf92(X0))
| ~ ssSkP659(X0) ) ).
cnf(u1411,negated_conjecture,
( ssRr(X0,skf93(X0))
| ~ ssSkP661(X0) ) ).
cnf(u1415,negated_conjecture,
( ssRr(X0,skf94(X0))
| ~ ssSkP671(X0) ) ).
cnf(u1419,negated_conjecture,
( ssRr(X0,skf95(X0))
| ~ ssSkP673(X0) ) ).
cnf(u1423,negated_conjecture,
( ssRr(X0,skf96(X0))
| ~ ssSkP675(X0) ) ).
cnf(u1427,negated_conjecture,
( ssRr(X0,skf97(X0))
| ~ ssSkP677(X0) ) ).
cnf(u1431,negated_conjecture,
( ssSkP675(X0)
| ~ ssSkP676(X1)
| ~ ssSkP590(X0,X1) ) ).
cnf(u1435,negated_conjecture,
( ssSkP673(X0)
| ~ ssSkP674(X1)
| ~ ssSkP590(X0,X1) ) ).
cnf(u1439,negated_conjecture,
( ssSkP590(X2,X0)
| ~ ssSkP578(X2,X1)
| ~ ssRr(X0,X1) ) ).
cnf(u1443,negated_conjecture,
( ssSkP578(X2,X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ) ).
cnf(u1447,negated_conjecture,
( ssSkP671(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP672(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1451,negated_conjecture,
( ssSkP669(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP670(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1455,negated_conjecture,
( ssSkP667(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP668(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1459,negated_conjecture,
( ssSkP665(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP666(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1463,negated_conjecture,
( ssSkP663(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP664(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1467,negated_conjecture,
( ssSkP661(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP662(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1471,negated_conjecture,
( ssSkP659(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP660(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1475,negated_conjecture,
( ssSkP657(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP658(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1479,negated_conjecture,
( ssSkP655(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP656(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1483,negated_conjecture,
( ssSkP653(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP654(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1487,negated_conjecture,
( ssSkP651(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP652(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1491,negated_conjecture,
( ssSkP649(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP650(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1495,negated_conjecture,
( ssSkP647(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP648(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1499,negated_conjecture,
( ssSkP645(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP646(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1503,negated_conjecture,
( ssSkP643(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP644(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1507,negated_conjecture,
( ssSkP641(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP642(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1511,negated_conjecture,
( ssSkP639(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP640(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1515,negated_conjecture,
( ssSkP637(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP638(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1519,negated_conjecture,
( ssSkP635(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP636(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1523,negated_conjecture,
( ssSkP633(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP634(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1527,negated_conjecture,
( ssSkP631(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP632(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1531,negated_conjecture,
( ssSkP629(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP630(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1535,negated_conjecture,
( ssSkP627(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP628(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1539,negated_conjecture,
( ssSkP614(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP626(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1543,negated_conjecture,
( ssSkP577(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP609(X3)
| ~ ssRr(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN907-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n001.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 17:17:48 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 12.40/2.48 % (498821)Input is clausal, will run a generic CNF schedule.
% 12.40/2.48 % (498828)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4128566095:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.40/2.48 % (498832)dis-21_1_sil=8000:lcm=predicate:random_seed=3070876482: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)
% 12.40/2.48 % (498826)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=1716625363:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.40/2.48 % (498830)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=297750913:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.40/2.48 % (498829)lrs+10_1_sil=8000:sp=occurrence:random_seed=3716093956:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.40/2.48 % (498827)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2320933038:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.40/2.48 % (498831)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3730124943:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.40/2.48 % (498831)Refutation not found, incomplete strategy
% 12.40/2.48 % (498831)------------------------------
% 12.40/2.48 % (498831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.48 % (498831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.48 % (498831)CaDiCaL version: 2.1.3
% 12.40/2.48 % (498831)Termination reason: Refutation not found, incomplete strategy
% 12.40/2.48 % (498831)Time elapsed: 0.009 s
% 12.40/2.48 % (498831)Peak memory usage: 89 MB
% 12.40/2.48 % (498831)Instructions burned: 14 (million)
% 12.40/2.48 % (498832)Instruction limit reached!
% 12.40/2.48 % (498832)------------------------------
% 12.40/2.48 % (498832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.48 % (498832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.48 % (498832)CaDiCaL version: 2.1.3
% 12.40/2.48 % (498832)Termination reason: Instruction limit
% 12.40/2.48 % (498832)Termination phase: Saturation
% 12.40/2.48 % (498832)Time elapsed: 0.042 s
% 12.40/2.48 % (498832)Peak memory usage: 89 MB
% 12.40/2.48 % (498832)Instructions burned: 118 (million)
% 12.40/2.48 % (498829)Instruction limit reached!
% 12.40/2.48 % (498829)------------------------------
% 12.40/2.48 % (498829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.48 % (498829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.48 % (498829)CaDiCaL version: 2.1.3
% 12.40/2.48 % (498829)Termination reason: Instruction limit
% 12.40/2.48 % (498829)Termination phase: Saturation
% 12.40/2.48 % (498829)Time elapsed: 0.051 s
% 12.40/2.48 % (498829)Peak memory usage: 90 MB
% 12.40/2.48 % (498829)Instructions burned: 107 (million)
% 12.40/2.48 % (498830)Instruction limit reached!
% 12.40/2.48 % (498830)------------------------------
% 12.40/2.48 % (498830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.48 % (498830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.48 % (498830)CaDiCaL version: 2.1.3
% 12.40/2.48 % (498830)Termination reason: Instruction limit
% 12.40/2.48 % (498830)Termination phase: Saturation
% 12.40/2.48 % (498830)Time elapsed: 0.054 s
% 12.40/2.48 % (498830)Peak memory usage: 89 MB
% 12.40/2.48 % (498830)Instructions burned: 116 (million)
% 12.40/2.48 % (498841)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2940294303:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 12.40/2.48 % (498840)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=2476245567:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.40/2.48 % (498842)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1692059820:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.40/2.48 % (498831)------------------------------
% 12.40/2.48 % (498831)------------------------------
% 12.40/2.48 % (498840)Instruction limit reached!
% 12.40/2.48 % (498840)------------------------------
% 12.40/2.48 % (498840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498840)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498840)Termination reason: Instruction limit
% 14.19/2.76 % (498840)Termination phase: Saturation
% 14.19/2.76 % (498840)Time elapsed: 0.069 s
% 14.19/2.76 % (498840)Peak memory usage: 90 MB
% 14.19/2.76 % (498840)Instructions burned: 144 (million)
% 14.19/2.76 % (498841)Instruction limit reached!
% 14.19/2.76 % (498841)------------------------------
% 14.19/2.76 % (498841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498841)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498841)Termination reason: Instruction limit
% 14.19/2.76 % (498841)Termination phase: Saturation
% 14.19/2.76 % (498841)Time elapsed: 0.097 s
% 14.19/2.76 % (498841)Peak memory usage: 89 MB
% 14.19/2.76 % (498841)Instructions burned: 191 (million)
% 14.19/2.76 % (498842)Instruction limit reached!
% 14.19/2.76 % (498842)------------------------------
% 14.19/2.76 % (498842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498842)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498842)Termination reason: Instruction limit
% 14.19/2.76 % (498842)Termination phase: Saturation
% 14.19/2.76 % (498842)Time elapsed: 0.098 s
% 14.19/2.76 % (498842)Peak memory usage: 92 MB
% 14.19/2.76 % (498842)Instructions burned: 220 (million)
% 14.19/2.76 % (498846)lrs+10_64_to=lpo:sil=8000:random_seed=1103075482:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 14.19/2.76 % (498847)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2773256882:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 14.19/2.76 % (498847)Refutation not found, incomplete strategy
% 14.19/2.76 % (498847)------------------------------
% 14.19/2.76 % (498847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498847)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498847)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.76 % (498847)Time elapsed: 0.006 s
% 14.19/2.76 % (498847)Peak memory usage: 89 MB
% 14.19/2.76 % (498847)Instructions burned: 8 (million)
% 14.19/2.76 % (498848)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2002882555:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 14.19/2.76 % (498849)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3436978244:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 14.19/2.76 % (498846)Instruction limit reached!
% 14.19/2.76 % (498846)------------------------------
% 14.19/2.76 % (498846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498846)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498846)Termination reason: Instruction limit
% 14.19/2.76 % (498846)Termination phase: Saturation
% 14.19/2.76 % (498846)Time elapsed: 0.072 s
% 14.19/2.76 % (498846)Peak memory usage: 93 MB
% 14.19/2.76 % (498846)Instructions burned: 126 (million)
% 14.19/2.76 % (498848)Instruction limit reached!
% 14.19/2.76 % (498848)------------------------------
% 14.19/2.76 % (498848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498848)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498848)Termination reason: Instruction limit
% 14.19/2.76 % (498848)Termination phase: Saturation
% 14.19/2.76 % (498848)Time elapsed: 0.073 s
% 14.19/2.76 % (498848)Peak memory usage: 92 MB
% 14.19/2.76 % (498848)Instructions burned: 158 (million)
% 14.19/2.76 % (498854)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=1347738999:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 14.19/2.76 % (498847)------------------------------
% 14.19/2.76 % (498847)------------------------------
% 14.19/2.76 % (498854)Instruction limit reached!
% 14.19/2.76 % (498854)------------------------------
% 14.19/2.76 % (498854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498854)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498854)Termination reason: Instruction limit
% 14.19/2.76 % (498854)Termination phase: Saturation
% 14.19/2.76 % (498854)Time elapsed: 0.057 s
% 14.19/2.76 % (498854)Peak memory usage: 90 MB
% 14.19/2.76 % (498854)Instructions burned: 108 (million)
% 14.19/2.76 % (498855)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=927374378:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 14.19/2.76 % (498855)Instruction limit reached!
% 14.19/2.76 % (498855)------------------------------
% 14.19/2.76 % (498855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498855)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498855)Termination reason: Instruction limit
% 14.19/2.76 % (498855)Termination phase: Saturation
% 14.19/2.76 % (498855)Time elapsed: 0.061 s
% 14.19/2.76 % (498855)Peak memory usage: 93 MB
% 14.19/2.76 % (498855)Instructions burned: 107 (million)
% 14.19/2.76 % (498857)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3952564501:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 14.19/2.76 % (498857)Refutation not found, incomplete strategy
% 14.19/2.76 % (498857)------------------------------
% 14.19/2.76 % (498857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498857)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498857)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.76 % (498857)Time elapsed: 0.010 s
% 14.19/2.76 % (498857)Peak memory usage: 89 MB
% 14.19/2.76 % (498857)Instructions burned: 18 (million)
% 14.19/2.76 % (498858)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2417878855:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 14.19/2.76 % (498860)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1460202064:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 14.19/2.76 % (498860)Refutation not found, incomplete strategy
% 14.19/2.76 % (498860)------------------------------
% 14.19/2.76 % (498860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498860)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498860)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.76 % (498860)Time elapsed: 0.009 s
% 14.19/2.76 % (498860)Peak memory usage: 89 MB
% 14.19/2.76 % (498860)Instructions burned: 14 (million)
% 14.19/2.76 % (498857)------------------------------
% 14.19/2.76 % (498857)------------------------------
% 14.19/2.76 % (498860)------------------------------
% 14.19/2.76 % (498860)------------------------------
% 14.19/2.76 % (498864)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2195491726:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 14.19/2.76 % (498865)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1280104700:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 14.19/2.76 % (498865)Instruction limit reached!
% 14.19/2.76 % (498865)------------------------------
% 14.19/2.76 % (498865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498865)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498865)Termination reason: Instruction limit
% 14.19/2.76 % (498865)Termination phase: Saturation
% 14.19/2.76 % (498865)Time elapsed: 0.096 s
% 14.19/2.76 % (498865)Peak memory usage: 93 MB
% 14.19/2.76 % (498865)Instructions burned: 193 (million)
% 14.19/2.76 % (498864)Instruction limit reached!
% 14.19/2.76 % (498864)------------------------------
% 14.19/2.76 % (498864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498864)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498864)Termination reason: Instruction limit
% 14.19/2.76 % (498864)Termination phase: Saturation
% 14.19/2.76 % (498864)Time elapsed: 0.258 s
% 14.19/2.76 % (498864)Peak memory usage: 93 MB
% 14.19/2.76 % (498864)Instructions burned: 499 (million)
% 14.19/2.76 % (498868)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=999110158:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 14.19/2.76 % (498868)First to succeed.
% 14.19/2.76 % (498868)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-498821"
% 14.19/2.76 % (498869)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=336703522:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 14.19/2.76 % (498869)Instruction limit reached!
% 14.19/2.76 % (498869)------------------------------
% 14.19/2.76 % (498869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.76 % (498869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.76 % (498869)CaDiCaL version: 2.1.3
% 14.19/2.76 % (498869)Termination reason: Instruction limit
% 14.19/2.76 % (498869)Termination phase: Saturation
% 14.19/2.76 % (498869)Time elapsed: 0.070 s
% 14.19/2.76 % (498869)Peak memory usage: 89 MB
% 14.19/2.76 % (498869)Instructions burned: 156 (million)
% 14.19/2.76 % SZS status Satisfiable for theBenchmark
% 14.19/2.76 % SZS output start Saturation.
% See solution above
% 14.19/2.76 % SZS output start Definitions and Model Updates.
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv17(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv18(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv12(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP219(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP220(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC8 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP246(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP245(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP244(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP243(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP242(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP241(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP240(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP239(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP238(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP237(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP236(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP235(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP221(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP222(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP223(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP224(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP225(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP226(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP227(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP228(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP229(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP230(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP231(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP232(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP233(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP234(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP488(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP489(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC17 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP515(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP514(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP513(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP512(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP511(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP510(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP509(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP508(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP507(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP506(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP505(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP490(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP491(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP492(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP493(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP494(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP495(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP496(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP497(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP498(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP499(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP500(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP501(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP502(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP503(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP504(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv19(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv11(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv26(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP39(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP40(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC2 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP63(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP62(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP61(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP314(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP312(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP313(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP134(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP131(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP132(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP133(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP516(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP517(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC18 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP543(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP542(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP541(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP540(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP539(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP538(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP537(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP536(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP535(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP534(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP533(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP532(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP531(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP530(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP529(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP528(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP527(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP526(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP525(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP524(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP523(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP522(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP521(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP518(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP519(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP520(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP247(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP248(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC9 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP279(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP278(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP277(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP276(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP275(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP274(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP273(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP272(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP271(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP270(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP269(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP268(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP267(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP266(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP265(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP264(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP263(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP262(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP261(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP260(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP259(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP258(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP257(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP431(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP432(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC15 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP463(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP462(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP461(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP460(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP459(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP458(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP457(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP456(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP455(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP454(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP453(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP452(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP451(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP450(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP449(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP448(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP447(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP446(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP445(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP444(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP443(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP442(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP441(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP440(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP439(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP438(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP437(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP436(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP435(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP434(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP433(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP368(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP369(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC13 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP400(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP399(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP398(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP397(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP396(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP395(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP394(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP393(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP392(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP391(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP390(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP389(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP388(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP387(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP386(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP385(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP384(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP383(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP382(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP381(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP380(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP379(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP378(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP377(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP376(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP375(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP374(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP373(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP372(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP337(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP338(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC12 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP367(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP366(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP365(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP364(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP363(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP362(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP361(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP360(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP359(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP358(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP357(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP356(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP355(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP354(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP353(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP352(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP351(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP350(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP349(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP348(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP347(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP346(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP345(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP344(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP343(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP342(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP341(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP340(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP339(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv3(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP371(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP370(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP96(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP97(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC4 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP128(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP127(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP126(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP125(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP124(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP129(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP130(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC5 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP156(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP155(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP154(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP153(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP152(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP135(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP136(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP137(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP138(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP139(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP140(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP141(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP142(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP143(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP144(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP145(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP146(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP147(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP148(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP149(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP150(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP151(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP157(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP158(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC6 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP185(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP184(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP183(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP182(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP181(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP159(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP160(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP161(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP162(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP163(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP164(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP165(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP166(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP167(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP168(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP169(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP170(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP171(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP172(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP173(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP174(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP175(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP176(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP177(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP178(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP179(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP180(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv25(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP123(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP122(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP121(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP120(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP119(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP118(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP117(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP116(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP115(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP114(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP113(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP112(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP111(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP110(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP109(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP108(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP107(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP106(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP105(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP104(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP103(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP102(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP101(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP100(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP99(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP98(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP186(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP187(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC7 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP218(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP217(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP216(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP215(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP214(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP213(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP212(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP211(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP210(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP209(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP208(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP207(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP310(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP311(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC11 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP336(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP335(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP334(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP333(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP332(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP331(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP330(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP329(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP328(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP327(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP326(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP315(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP316(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP317(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP318(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP319(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP320(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP321(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP322(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP323(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP324(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP325(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv20(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP206(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP205(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP204(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP203(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP202(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP201(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP200(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP199(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP198(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP197(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP196(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP195(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP194(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP193(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP192(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP191(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP190(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP189(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP188(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP544(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP545(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC19 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP576(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP575(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP574(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP573(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP572(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP571(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP570(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP569(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP568(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP567(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP566(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP565(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP564(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP563(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP562(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP561(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP560(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP559(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP558(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP557(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP556(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP464(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP465(X0,X1) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkC16 := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP487(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP486(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP485(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP484(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP483(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP482(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP481(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP480(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP479(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP478(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP477(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP476(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP475(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP474(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP473(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP472(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP471(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP470(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP469(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP468(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP467(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP466(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv10(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP555(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP554(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP553(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP552(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP551(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP550(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP549(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP548(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP547(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP546(X0) := $true
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssPv1(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP249(X0) := $false
% 14.19/2.76 for all inputs,
% 14.19/2.76 define ssSkP250(X0) := $false
% 14.19/2.76 for all inputs,
% 15.19/2.95 define ssSkP251(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP252(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP253(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP254(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP255(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP256(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssPv9(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP41(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP42(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP43(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP44(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP45(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP46(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP47(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP48(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP49(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP50(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP51(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP52(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP53(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP54(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP55(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP56(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP57(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP58(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP59(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP60(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssPv27(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP0(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP1(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkC0 := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP12(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP11(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP2(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP3(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP4(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP5(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP6(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP7(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP8(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP9(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP10(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP13(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP14(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkC1 := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP38(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP37(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP15(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP16(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP17(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP18(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP19(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP20(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP21(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP22(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP23(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP24(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP25(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP26(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP27(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP28(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP29(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP30(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP31(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP32(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP33(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP34(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP35(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP36(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssPv28(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP401(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP402(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkC14 := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP430(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP429(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP428(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP427(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP426(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP425(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP424(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP423(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP422(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP421(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP420(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP419(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP418(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP417(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP416(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP415(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP414(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP413(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP412(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP411(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP410(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP409(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP408(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP407(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP406(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP405(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP404(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP403(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP280(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP281(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkC10 := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP309(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP308(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP307(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP306(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP305(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP304(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP303(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP302(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP301(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP300(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP299(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP298(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP297(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP296(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP295(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP294(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP293(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP292(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP291(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP290(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP289(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP288(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP287(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP286(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP285(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP284(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP283(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP282(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssPv4(X0) := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP64(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP65(X0,X1) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkC3 := $false
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP95(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP94(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP93(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP92(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP91(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP90(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP89(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP88(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP87(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP86(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP85(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP84(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP83(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP82(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP81(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP80(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP79(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP78(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP77(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP76(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP75(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP74(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP73(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP72(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP71(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP70(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP69(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP68(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP67(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssSkP66(X0) := $true
% 15.19/2.95 for all inputs,
% 15.19/2.95 define ssPv2(X0) := $false
% 15.19/2.95 % SZS output end Definitions and Model Updates.
% 15.19/2.95 % (498868)------------------------------
% 15.19/2.95 % (498868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.19/2.95 % (498868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.19/2.95 % (498868)CaDiCaL version: 2.1.3
% 15.19/2.95 % (498868)Termination reason: Satisfiable
% 15.19/2.95 % (498868)Time elapsed: 0.013 s
% 15.19/2.95 % (498868)Peak memory usage: 89 MB
% 15.19/2.95 % (498868)Instructions burned: 19 (million)
% 15.19/2.95 % (498868)------------------------------
% 15.19/2.95 % (498868)------------------------------
% 15.19/2.95 % (498821)Success in time 2.071 s
% 15.19/2.95 % Vampire exiting
%------------------------------------------------------------------------------