%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN904-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:56 PM UTC 2026
% Result : Satisfiable 8.07s 1.51s
% Output : Saturation 8.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u590,negated_conjecture,
~ ssSkC10 ).
cnf(u595,negated_conjecture,
ssSkP479(skc21) ).
cnf(u599,negated_conjecture,
( ssSkP372(X0)
| ~ ssSkP384(X0) ) ).
cnf(u603,negated_conjecture,
( ssPv31(X0)
| ~ ssSkP384(X0) ) ).
cnf(u607,negated_conjecture,
( ssSkP379(X0)
| ~ ssSkP385(X0) ) ).
cnf(u611,negated_conjecture,
( ssPv10(X0)
| ~ ssSkP385(X0) ) ).
cnf(u615,negated_conjecture,
( ssSkP375(X0)
| ~ ssSkP386(X0) ) ).
cnf(u619,negated_conjecture,
( ssPv30(X0)
| ~ ssSkP386(X0) ) ).
cnf(u623,negated_conjecture,
( ssSkP376(X0)
| ~ ssSkP387(X0) ) ).
cnf(u627,negated_conjecture,
( ssPv15(X0)
| ~ ssSkP387(X0) ) ).
cnf(u631,negated_conjecture,
( ssSkP378(X0)
| ~ ssSkP388(X0) ) ).
cnf(u635,negated_conjecture,
( ssPv29(X0)
| ~ ssSkP388(X0) ) ).
cnf(u639,negated_conjecture,
( ssSkP374(X0)
| ~ ssSkP389(X0) ) ).
cnf(u643,negated_conjecture,
( ssPv12(X0)
| ~ ssSkP389(X0) ) ).
cnf(u647,negated_conjecture,
( ssSkP381(X0)
| ~ ssSkP390(X0) ) ).
cnf(u651,negated_conjecture,
( ssPv28(X0)
| ~ ssSkP390(X0) ) ).
cnf(u655,negated_conjecture,
( ssSkP383(X0)
| ~ ssSkP391(X0) ) ).
cnf(u659,negated_conjecture,
( ssPv14(X0)
| ~ ssSkP391(X0) ) ).
cnf(u663,negated_conjecture,
( ssSkP373(X0)
| ~ ssSkP392(X0) ) ).
cnf(u667,negated_conjecture,
( ssPv27(X0)
| ~ ssSkP392(X0) ) ).
cnf(u671,negated_conjecture,
( ssSkP377(X0)
| ~ ssSkP394(X0) ) ).
cnf(u675,negated_conjecture,
( ssPv26(X0)
| ~ ssSkP394(X0) ) ).
cnf(u679,negated_conjecture,
( ssSkP380(X0)
| ~ ssSkP395(X0) ) ).
cnf(u683,negated_conjecture,
( ssPv13(X0)
| ~ ssSkP395(X0) ) ).
cnf(u687,negated_conjecture,
( ssSkP382(X0)
| ~ ssSkP396(X0) ) ).
cnf(u691,negated_conjecture,
( ssPv25(X0)
| ~ ssSkP396(X0) ) ).
cnf(u695,negated_conjecture,
( ssSkP357(X0)
| ~ ssSkP397(X0) ) ).
cnf(u699,negated_conjecture,
( ssSkP393(X0)
| ~ ssSkP397(X0) ) ).
cnf(u703,negated_conjecture,
( ssSkP410(X0)
| ~ ssSkP411(X0) ) ).
cnf(u707,negated_conjecture,
( ssSkP412(X0)
| ~ ssSkP413(X0) ) ).
cnf(u711,negated_conjecture,
( ssSkP414(X0)
| ~ ssSkP415(X0) ) ).
cnf(u715,negated_conjecture,
( ssSkP416(X0)
| ~ ssSkP417(X0) ) ).
cnf(u719,negated_conjecture,
( ssSkP409(X0)
| ~ ssSkP419(X0) ) ).
cnf(u723,negated_conjecture,
( ssSkP418(X0)
| ~ ssSkP419(X0) ) ).
cnf(u727,negated_conjecture,
( ssSkP420(X0)
| ~ ssSkP421(X0) ) ).
cnf(u731,negated_conjecture,
( ssSkP408(X0)
| ~ ssSkP423(X0) ) ).
cnf(u735,negated_conjecture,
( ssSkP422(X0)
| ~ ssSkP423(X0) ) ).
cnf(u739,negated_conjecture,
( ssSkP407(X0)
| ~ ssSkP425(X0) ) ).
cnf(u743,negated_conjecture,
( ssSkP424(X0)
| ~ ssSkP425(X0) ) ).
cnf(u747,negated_conjecture,
( ssSkP406(X0)
| ~ ssSkP427(X0) ) ).
cnf(u751,negated_conjecture,
( ssSkP426(X0)
| ~ ssSkP427(X0) ) ).
cnf(u755,negated_conjecture,
( ssSkP405(X0)
| ~ ssSkP429(X0) ) ).
cnf(u759,negated_conjecture,
( ssSkP428(X0)
| ~ ssSkP429(X0) ) ).
cnf(u763,negated_conjecture,
( ssSkP430(X0)
| ~ ssSkP431(X0) ) ).
cnf(u767,negated_conjecture,
( ssSkP432(X0)
| ~ ssSkP433(X0) ) ).
cnf(u771,negated_conjecture,
( ssSkP434(X0)
| ~ ssSkP435(X0) ) ).
cnf(u775,negated_conjecture,
( ssSkP436(X0)
| ~ ssSkP437(X0) ) ).
cnf(u779,negated_conjecture,
( ssSkP438(X0)
| ~ ssSkP439(X0) ) ).
cnf(u783,negated_conjecture,
( ssSkP440(X0)
| ~ ssSkP441(X0) ) ).
cnf(u787,negated_conjecture,
( ssSkP442(X0)
| ~ ssSkP443(X0) ) ).
cnf(u791,negated_conjecture,
( ssSkP444(X0)
| ~ ssSkP445(X0) ) ).
cnf(u795,negated_conjecture,
( ssSkP446(X0)
| ~ ssSkP447(X0) ) ).
cnf(u799,negated_conjecture,
( ssSkP404(X0)
| ~ ssSkP449(X0) ) ).
cnf(u803,negated_conjecture,
( ssSkP448(X0)
| ~ ssSkP449(X0) ) ).
cnf(u807,negated_conjecture,
( ssSkP403(X0)
| ~ ssSkP451(X0) ) ).
cnf(u811,negated_conjecture,
( ssSkP450(X0)
| ~ ssSkP451(X0) ) ).
cnf(u815,negated_conjecture,
( ssSkP402(X0)
| ~ ssSkP453(X0) ) ).
cnf(u819,negated_conjecture,
( ssSkP452(X0)
| ~ ssSkP453(X0) ) ).
cnf(u823,negated_conjecture,
( ssSkP401(X0)
| ~ ssSkP455(X0) ) ).
cnf(u827,negated_conjecture,
( ssSkP454(X0)
| ~ ssSkP455(X0) ) ).
cnf(u831,negated_conjecture,
( ssSkP400(X0)
| ~ ssSkP457(X0) ) ).
cnf(u835,negated_conjecture,
( ssSkP456(X0)
| ~ ssSkP457(X0) ) ).
cnf(u839,negated_conjecture,
( ssSkP399(X0)
| ~ ssSkP459(X0) ) ).
cnf(u843,negated_conjecture,
( ssSkP458(X0)
| ~ ssSkP459(X0) ) ).
cnf(u847,negated_conjecture,
( ssSkP398(X0)
| ~ ssSkP461(X0) ) ).
cnf(u851,negated_conjecture,
( ssSkP460(X0)
| ~ ssSkP461(X0) ) ).
cnf(u855,negated_conjecture,
( ssSkP462(X0)
| ~ ssSkP463(X0) ) ).
cnf(u859,negated_conjecture,
( ssSkP464(X0)
| ~ ssSkP465(X0) ) ).
cnf(u863,negated_conjecture,
( ssSkP466(X0)
| ~ ssSkP467(X0) ) ).
cnf(u867,negated_conjecture,
( ssSkP468(X0)
| ~ ssSkP469(X0) ) ).
cnf(u871,negated_conjecture,
( ssSkP470(X0)
| ~ ssSkP471(X0) ) ).
cnf(u875,negated_conjecture,
( ssSkP472(X0)
| ~ ssSkP473(X0) ) ).
cnf(u879,negated_conjecture,
( ssSkP474(X0)
| ~ ssSkP475(X0) ) ).
cnf(u883,negated_conjecture,
( ssSkP476(X0)
| ~ ssSkP477(X0) ) ).
cnf(u887,negated_conjecture,
( ssSkP478(X0)
| ~ ssSkP479(X0) ) ).
cnf(u891,negated_conjecture,
( ssSkP359(skf73(X0))
| ~ ssSkP372(X0) ) ).
cnf(u895,negated_conjecture,
( ssSkP365(skf74(X0))
| ~ ssSkP373(X0) ) ).
cnf(u899,negated_conjecture,
( ssSkP369(skf75(X0))
| ~ ssSkP374(X0) ) ).
cnf(u903,negated_conjecture,
( ssSkP363(skf76(X0))
| ~ ssSkP375(X0) ) ).
cnf(u907,negated_conjecture,
( ssSkP362(skf77(X0))
| ~ ssSkP376(X0) ) ).
cnf(u911,negated_conjecture,
( ssSkP370(skf78(X0))
| ~ ssSkP377(X0) ) ).
cnf(u915,negated_conjecture,
( ssSkP367(skf79(X0))
| ~ ssSkP378(X0) ) ).
cnf(u919,negated_conjecture,
( ssSkP368(skf80(X0))
| ~ ssSkP379(X0) ) ).
cnf(u923,negated_conjecture,
( ssSkP364(skf81(X0))
| ~ ssSkP380(X0) ) ).
cnf(u927,negated_conjecture,
( ssSkP360(skf82(X0))
| ~ ssSkP381(X0) ) ).
cnf(u931,negated_conjecture,
( ssSkP366(skf83(X0))
| ~ ssSkP382(X0) ) ).
cnf(u935,negated_conjecture,
( ssSkP361(skf84(X0))
| ~ ssSkP383(X0) ) ).
cnf(u939,negated_conjecture,
( ssSkP384(skf85(X0))
| ~ ssSkP398(X0) ) ).
cnf(u943,negated_conjecture,
( ssSkP386(skf86(X0))
| ~ ssSkP399(X0) ) ).
cnf(u947,negated_conjecture,
( ssSkP388(skf87(X0))
| ~ ssSkP400(X0) ) ).
cnf(u951,negated_conjecture,
( ssSkP390(skf88(X0))
| ~ ssSkP401(X0) ) ).
cnf(u955,negated_conjecture,
( ssSkP392(skf89(X0))
| ~ ssSkP402(X0) ) ).
cnf(u959,negated_conjecture,
( ssSkP394(skf90(X0))
| ~ ssSkP403(X0) ) ).
cnf(u963,negated_conjecture,
( ssSkP396(skf91(X0))
| ~ ssSkP404(X0) ) ).
cnf(u967,negated_conjecture,
( ssSkP387(skf92(X0))
| ~ ssSkP405(X0) ) ).
cnf(u971,negated_conjecture,
( ssSkP391(skf93(X0))
| ~ ssSkP406(X0) ) ).
cnf(u975,negated_conjecture,
( ssSkP395(skf94(X0))
| ~ ssSkP407(X0) ) ).
cnf(u979,negated_conjecture,
( ssSkP389(skf95(X0))
| ~ ssSkP408(X0) ) ).
cnf(u983,negated_conjecture,
( ssSkP385(skf96(X0))
| ~ ssSkP409(X0) ) ).
cnf(u987,negated_conjecture,
( ~ ssPv31(skf61(X0))
| ~ ssSkP359(X0) ) ).
cnf(u991,negated_conjecture,
( ~ ssPv28(skf62(X0))
| ~ ssSkP360(X0) ) ).
cnf(u995,negated_conjecture,
( ~ ssPv14(skf63(X0))
| ~ ssSkP361(X0) ) ).
cnf(u999,negated_conjecture,
( ~ ssPv15(skf64(X0))
| ~ ssSkP362(X0) ) ).
cnf(u1003,negated_conjecture,
( ~ ssPv30(skf65(X0))
| ~ ssSkP363(X0) ) ).
cnf(u1007,negated_conjecture,
( ~ ssPv13(skf66(X0))
| ~ ssSkP364(X0) ) ).
cnf(u1011,negated_conjecture,
( ~ ssPv27(skf67(X0))
| ~ ssSkP365(X0) ) ).
cnf(u1015,negated_conjecture,
( ~ ssPv25(skf68(X0))
| ~ ssSkP366(X0) ) ).
cnf(u1019,negated_conjecture,
( ~ ssPv29(skf69(X0))
| ~ ssSkP367(X0) ) ).
cnf(u1023,negated_conjecture,
( ~ ssPv10(skf70(X0))
| ~ ssSkP368(X0) ) ).
cnf(u1027,negated_conjecture,
( ~ ssPv12(skf71(X0))
| ~ ssSkP369(X0) ) ).
cnf(u1031,negated_conjecture,
( ~ ssPv26(skf72(X0))
| ~ ssSkP370(X0) ) ).
cnf(u1047,negated_conjecture,
( ~ ssSkP384(skf61(X0))
| ~ ssSkP359(X0) ) ).
cnf(u1051,negated_conjecture,
( ~ ssSkP390(skf62(X0))
| ~ ssSkP360(X0) ) ).
cnf(u1055,negated_conjecture,
( ~ ssSkP391(skf63(X0))
| ~ ssSkP361(X0) ) ).
cnf(u1059,negated_conjecture,
( ~ ssSkP387(skf64(X0))
| ~ ssSkP362(X0) ) ).
cnf(u1063,negated_conjecture,
( ~ ssSkP386(skf65(X0))
| ~ ssSkP363(X0) ) ).
cnf(u1067,negated_conjecture,
( ~ ssSkP395(skf66(X0))
| ~ ssSkP364(X0) ) ).
cnf(u1071,negated_conjecture,
( ~ ssSkP392(skf67(X0))
| ~ ssSkP365(X0) ) ).
cnf(u1075,negated_conjecture,
( ~ ssSkP396(skf68(X0))
| ~ ssSkP366(X0) ) ).
cnf(u1079,negated_conjecture,
( ~ ssSkP388(skf69(X0))
| ~ ssSkP367(X0) ) ).
cnf(u1083,negated_conjecture,
( ~ ssSkP385(skf70(X0))
| ~ ssSkP368(X0) ) ).
cnf(u1087,negated_conjecture,
( ssRr(X0,skf60(X0))
| ~ ssSkP357(X0) ) ).
cnf(u1091,negated_conjecture,
( ~ ssSkP389(skf71(X0))
| ~ ssSkP369(X0) ) ).
cnf(u1095,negated_conjecture,
( ~ ssSkP394(skf72(X0))
| ~ ssSkP370(X0) ) ).
cnf(u1099,negated_conjecture,
( ssRr(X0,skf61(X0))
| ~ ssSkP359(X0) ) ).
cnf(u1103,negated_conjecture,
( ssRr(X0,skf62(X0))
| ~ ssSkP360(X0) ) ).
cnf(u1107,negated_conjecture,
( ssRr(X0,skf63(X0))
| ~ ssSkP361(X0) ) ).
cnf(u1111,negated_conjecture,
( ssRr(X0,skf64(X0))
| ~ ssSkP362(X0) ) ).
cnf(u1115,negated_conjecture,
( ssRr(X0,skf65(X0))
| ~ ssSkP363(X0) ) ).
cnf(u1119,negated_conjecture,
( ssRr(X0,skf66(X0))
| ~ ssSkP364(X0) ) ).
cnf(u1123,negated_conjecture,
( ssRr(X0,skf67(X0))
| ~ ssSkP365(X0) ) ).
cnf(u1127,negated_conjecture,
( ssRr(X0,skf68(X0))
| ~ ssSkP366(X0) ) ).
cnf(u1131,negated_conjecture,
( ssRr(X0,skf69(X0))
| ~ ssSkP367(X0) ) ).
cnf(u1135,negated_conjecture,
( ssRr(X0,skf70(X0))
| ~ ssSkP368(X0) ) ).
cnf(u1139,negated_conjecture,
( ssRr(X0,skf71(X0))
| ~ ssSkP369(X0) ) ).
cnf(u1143,negated_conjecture,
( ssRr(X0,skf72(X0))
| ~ ssSkP370(X0) ) ).
cnf(u1147,negated_conjecture,
( ssRr(skf73(X0),X0)
| ~ ssSkP372(X0) ) ).
cnf(u1151,negated_conjecture,
( ssRr(skf74(X0),X0)
| ~ ssSkP373(X0) ) ).
cnf(u1155,negated_conjecture,
( ssRr(skf75(X0),X0)
| ~ ssSkP374(X0) ) ).
cnf(u1159,negated_conjecture,
( ssRr(skf76(X0),X0)
| ~ ssSkP375(X0) ) ).
cnf(u1163,negated_conjecture,
( ssRr(skf77(X0),X0)
| ~ ssSkP376(X0) ) ).
cnf(u1167,negated_conjecture,
( ssRr(skf78(X0),X0)
| ~ ssSkP377(X0) ) ).
cnf(u1171,negated_conjecture,
( ssRr(skf79(X0),X0)
| ~ ssSkP378(X0) ) ).
cnf(u1175,negated_conjecture,
( ssRr(skf80(X0),X0)
| ~ ssSkP379(X0) ) ).
cnf(u1179,negated_conjecture,
( ssRr(skf81(X0),X0)
| ~ ssSkP380(X0) ) ).
cnf(u1183,negated_conjecture,
( ssRr(skf82(X0),X0)
| ~ ssSkP381(X0) ) ).
cnf(u1187,negated_conjecture,
( ssRr(skf83(X0),X0)
| ~ ssSkP382(X0) ) ).
cnf(u1191,negated_conjecture,
( ssRr(skf84(X0),X0)
| ~ ssSkP383(X0) ) ).
cnf(u1195,negated_conjecture,
( ssRr(X0,skf85(X0))
| ~ ssSkP398(X0) ) ).
cnf(u1199,negated_conjecture,
( ssRr(X0,skf86(X0))
| ~ ssSkP399(X0) ) ).
cnf(u1203,negated_conjecture,
( ssRr(X0,skf87(X0))
| ~ ssSkP400(X0) ) ).
cnf(u1207,negated_conjecture,
( ssRr(X0,skf88(X0))
| ~ ssSkP401(X0) ) ).
cnf(u1211,negated_conjecture,
( ssRr(X0,skf89(X0))
| ~ ssSkP402(X0) ) ).
cnf(u1215,negated_conjecture,
( ssRr(X0,skf90(X0))
| ~ ssSkP403(X0) ) ).
cnf(u1219,negated_conjecture,
( ssRr(X0,skf91(X0))
| ~ ssSkP404(X0) ) ).
cnf(u1223,negated_conjecture,
( ssRr(X0,skf92(X0))
| ~ ssSkP405(X0) ) ).
cnf(u1227,negated_conjecture,
( ssRr(X0,skf93(X0))
| ~ ssSkP406(X0) ) ).
cnf(u1231,negated_conjecture,
( ssRr(X0,skf94(X0))
| ~ ssSkP407(X0) ) ).
cnf(u1235,negated_conjecture,
( ssRr(X0,skf95(X0))
| ~ ssSkP408(X0) ) ).
cnf(u1239,negated_conjecture,
( ssRr(X0,skf96(X0))
| ~ ssSkP409(X0) ) ).
cnf(u1243,negated_conjecture,
( ssRr(X0,skf97(X0))
| ~ ssSkP411(X0) ) ).
cnf(u1247,negated_conjecture,
( ssRr(X0,skf98(X0))
| ~ ssSkP413(X0) ) ).
cnf(u1251,negated_conjecture,
( ssRr(X0,skf99(X0))
| ~ ssSkP415(X0) ) ).
cnf(u1255,negated_conjecture,
( ssRr(X0,skf100(X0))
| ~ ssSkP417(X0) ) ).
cnf(u1259,negated_conjecture,
( ssRr(X0,skf101(X0))
| ~ ssSkP421(X0) ) ).
cnf(u1263,negated_conjecture,
( ssRr(X0,skf102(X0))
| ~ ssSkP431(X0) ) ).
cnf(u1267,negated_conjecture,
( ssRr(X0,skf103(X0))
| ~ ssSkP433(X0) ) ).
cnf(u1271,negated_conjecture,
( ssRr(X0,skf104(X0))
| ~ ssSkP435(X0) ) ).
cnf(u1275,negated_conjecture,
( ssRr(X0,skf105(X0))
| ~ ssSkP437(X0) ) ).
cnf(u1279,negated_conjecture,
( ssRr(X0,skf106(X0))
| ~ ssSkP439(X0) ) ).
cnf(u1283,negated_conjecture,
( ssRr(X0,skf107(X0))
| ~ ssSkP441(X0) ) ).
cnf(u1287,negated_conjecture,
( ssRr(X0,skf108(X0))
| ~ ssSkP443(X0) ) ).
cnf(u1291,negated_conjecture,
( ssRr(X0,skf109(X0))
| ~ ssSkP445(X0) ) ).
cnf(u1295,negated_conjecture,
( ssRr(X0,skf110(X0))
| ~ ssSkP447(X0) ) ).
cnf(u1299,negated_conjecture,
( ssRr(X0,skf111(X0))
| ~ ssSkP463(X0) ) ).
cnf(u1303,negated_conjecture,
( ssRr(X0,skf112(X0))
| ~ ssSkP465(X0) ) ).
cnf(u1307,negated_conjecture,
( ssRr(X0,skf113(X0))
| ~ ssSkP467(X0) ) ).
cnf(u1311,negated_conjecture,
( ssRr(X0,skf114(X0))
| ~ ssSkP469(X0) ) ).
cnf(u1315,negated_conjecture,
( ssRr(X0,skf115(X0))
| ~ ssSkP471(X0) ) ).
cnf(u1319,negated_conjecture,
( ssRr(X0,skf116(X0))
| ~ ssSkP473(X0) ) ).
cnf(u1323,negated_conjecture,
( ssRr(X0,skf117(X0))
| ~ ssSkP475(X0) ) ).
cnf(u1327,negated_conjecture,
( ssRr(X0,skf118(X0))
| ~ ssSkP477(X0) ) ).
cnf(u1331,negated_conjecture,
( ssRr(X0,skf119(X0))
| ~ ssSkP479(X0) ) ).
cnf(u1335,negated_conjecture,
( ssSkP477(X0)
| ~ ssSkP478(X1)
| ~ ssSkP371(X0,X1) ) ).
cnf(u1339,negated_conjecture,
( ssSkP475(X0)
| ~ ssSkP476(X1)
| ~ ssSkP371(X0,X1) ) ).
cnf(u1343,negated_conjecture,
( ssSkP371(X2,X0)
| ~ ssSkP358(X2,X1)
| ~ ssRr(X0,X1) ) ).
cnf(u1347,negated_conjecture,
( ssSkP358(X2,X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ) ).
cnf(u1351,negated_conjecture,
( ssSkP473(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP474(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1355,negated_conjecture,
( ssSkP471(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP472(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1359,negated_conjecture,
( ssSkP469(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP470(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1363,negated_conjecture,
( ssSkP467(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP468(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1367,negated_conjecture,
( ssSkP465(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP466(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1371,negated_conjecture,
( ssSkP463(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP464(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1375,negated_conjecture,
( ssSkP461(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP462(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1379,negated_conjecture,
( ssSkP459(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP460(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1383,negated_conjecture,
( ssSkP457(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP458(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1387,negated_conjecture,
( ssSkP455(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP456(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1391,negated_conjecture,
( ssSkP453(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP454(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1395,negated_conjecture,
( ssSkP451(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP452(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1399,negated_conjecture,
( ssSkP449(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP450(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1403,negated_conjecture,
( ssSkP447(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP448(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1407,negated_conjecture,
( ssSkP445(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP446(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1411,negated_conjecture,
( ssSkP443(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP444(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1415,negated_conjecture,
( ssSkP441(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP442(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1419,negated_conjecture,
( ssSkP439(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP440(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1423,negated_conjecture,
( ssSkP437(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP438(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1427,negated_conjecture,
( ssSkP435(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP436(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1431,negated_conjecture,
( ssSkP433(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP434(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1435,negated_conjecture,
( ssSkP431(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP432(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1439,negated_conjecture,
( ssSkP429(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP430(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1443,negated_conjecture,
( ssSkP427(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP428(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1447,negated_conjecture,
( ssSkP425(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP426(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1451,negated_conjecture,
( ssSkP423(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP424(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1455,negated_conjecture,
( ssSkP421(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP422(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1459,negated_conjecture,
( ssSkP419(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP420(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1463,negated_conjecture,
( ssSkP417(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP418(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1467,negated_conjecture,
( ssSkP415(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP416(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1471,negated_conjecture,
( ssSkP413(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP414(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1475,negated_conjecture,
( ssSkP411(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP412(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1479,negated_conjecture,
( ssSkP397(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP410(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1483,negated_conjecture,
( ssSkP357(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP393(X3)
| ~ ssRr(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN904-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.11 % Computer : n012.cluster.edu
% 0.06/0.11 % Model : x86_64 x86_64
% 0.06/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.11 % Memory : 8046.5625MB
% 0.06/0.11 % OS : Linux 6.8.0-71-generic
% 0.06/0.11 % CPULimit : 300
% 0.06/0.11 % WCLimit : 300
% 0.06/0.11 % DateTime : Mon Sep 28 17:11:19 UTC 2026
% 0.06/0.12 % CPUTime :
% 0.06/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.13 Running first-order theorem proving
% 0.06/0.13 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.05/1.30 % (3516186)Input is clausal, will run a generic CNF schedule.
% 6.05/1.30 % (3516192)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1056935239:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.05/1.30 % (3516193)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=552191030:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.05/1.30 % (3516194)lrs+10_1_sil=8000:sp=occurrence:random_seed=3386338723:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.05/1.30 % (3516191)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=926361537:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.05/1.30 % (3516196)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=60882594:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.05/1.30 % (3516195)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1088648426:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.05/1.30 % (3516197)dis-21_1_sil=8000:lcm=predicate:random_seed=2040524559: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.05/1.30 % (3516196)Refutation not found, incomplete strategy
% 6.05/1.30 % (3516196)------------------------------
% 6.05/1.30 % (3516196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.30 % (3516196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.30 % (3516196)CaDiCaL version: 2.1.3
% 6.05/1.30 % (3516196)Termination reason: Refutation not found, incomplete strategy
% 6.05/1.30 % (3516196)Time elapsed: 0.004 s
% 6.05/1.30 % (3516196)Peak memory usage: 89 MB
% 6.05/1.30 % (3516196)Instructions burned: 13 (million)
% 6.05/1.30 % (3516194)Instruction limit reached!
% 6.05/1.30 % (3516194)------------------------------
% 6.05/1.30 % (3516194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.30 % (3516194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.30 % (3516194)CaDiCaL version: 2.1.3
% 6.05/1.30 % (3516194)Termination reason: Instruction limit
% 6.05/1.30 % (3516194)Termination phase: Saturation
% 6.05/1.30 % (3516194)Time elapsed: 0.026 s
% 6.05/1.30 % (3516194)Peak memory usage: 90 MB
% 6.05/1.30 % (3516194)Instructions burned: 109 (million)
% 6.05/1.30 % (3516197)Instruction limit reached!
% 6.05/1.30 % (3516197)------------------------------
% 6.05/1.30 % (3516197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.30 % (3516197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.30 % (3516197)CaDiCaL version: 2.1.3
% 6.05/1.30 % (3516197)Termination reason: Instruction limit
% 6.05/1.30 % (3516197)Termination phase: Saturation
% 6.05/1.30 % (3516197)Time elapsed: 0.022 s
% 6.05/1.30 % (3516197)Peak memory usage: 88 MB
% 6.05/1.30 % (3516197)Instructions burned: 122 (million)
% 6.05/1.30 % (3516195)Instruction limit reached!
% 6.05/1.30 % (3516195)------------------------------
% 6.05/1.30 % (3516195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.30 % (3516195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.30 % (3516195)CaDiCaL version: 2.1.3
% 6.05/1.30 % (3516195)Termination reason: Instruction limit
% 6.05/1.30 % (3516195)Termination phase: Saturation
% 6.05/1.30 % (3516195)Time elapsed: 0.029 s
% 6.05/1.30 % (3516195)Peak memory usage: 89 MB
% 6.05/1.30 % (3516195)Instructions burned: 115 (million)
% 6.05/1.30 % (3516206)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2467503643: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.05/1.30 % (3516205)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=1284267762:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.05/1.30 % (3516207)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3410629898:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 6.05/1.30 % (3516205)Instruction limit reached!
% 6.05/1.30 % (3516205)------------------------------
% 6.05/1.30 % (3516205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516205)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516205)Termination reason: Instruction limit
% 8.07/1.51 % (3516205)Termination phase: Saturation
% 8.07/1.51 % (3516205)Time elapsed: 0.037 s
% 8.07/1.51 % (3516205)Peak memory usage: 90 MB
% 8.07/1.51 % (3516205)Instructions burned: 144 (million)
% 8.07/1.51 % (3516196)------------------------------
% 8.07/1.51 % (3516196)------------------------------
% 8.07/1.51 % (3516206)Instruction limit reached!
% 8.07/1.51 % (3516206)------------------------------
% 8.07/1.51 % (3516206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516206)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516206)Termination reason: Instruction limit
% 8.07/1.51 % (3516206)Termination phase: Saturation
% 8.07/1.51 % (3516206)Time elapsed: 0.052 s
% 8.07/1.51 % (3516206)Peak memory usage: 89 MB
% 8.07/1.51 % (3516206)Instructions burned: 192 (million)
% 8.07/1.51 % (3516207)Instruction limit reached!
% 8.07/1.51 % (3516207)------------------------------
% 8.07/1.51 % (3516207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516207)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516207)Termination reason: Instruction limit
% 8.07/1.51 % (3516207)Termination phase: Saturation
% 8.07/1.51 % (3516207)Time elapsed: 0.051 s
% 8.07/1.51 % (3516207)Peak memory usage: 91 MB
% 8.07/1.51 % (3516207)Instructions burned: 219 (million)
% 8.07/1.51 % (3516211)lrs+10_64_to=lpo:sil=8000:random_seed=827524302:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 8.07/1.51 % (3516212)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2902991823:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 8.07/1.51 % (3516213)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=304332491:i=157:gtg=all_2997 on theBenchmark for (2997ds/157Mi)
% 8.07/1.51 % (3516212)Refutation not found, incomplete strategy
% 8.07/1.51 % (3516212)------------------------------
% 8.07/1.51 % (3516212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516212)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516212)Termination reason: Refutation not found, incomplete strategy
% 8.07/1.51 % (3516212)Time elapsed: 0.003 s
% 8.07/1.51 % (3516212)Peak memory usage: 88 MB
% 8.07/1.51 % (3516212)Instructions burned: 8 (million)
% 8.07/1.51 % (3516214)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=456429141:i=3394:sd=4:ss=included:sgt=64_2997 on theBenchmark for (2997ds/3394Mi)
% 8.07/1.51 % (3516211)Instruction limit reached!
% 8.07/1.51 % (3516211)------------------------------
% 8.07/1.51 % (3516211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516211)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516211)Termination reason: Instruction limit
% 8.07/1.51 % (3516211)Termination phase: Saturation
% 8.07/1.51 % (3516211)Time elapsed: 0.040 s
% 8.07/1.51 % (3516211)Peak memory usage: 92 MB
% 8.07/1.51 % (3516211)Instructions burned: 129 (million)
% 8.07/1.51 % (3516213)Instruction limit reached!
% 8.07/1.51 % (3516213)------------------------------
% 8.07/1.51 % (3516213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516213)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516213)Termination reason: Instruction limit
% 8.07/1.51 % (3516213)Termination phase: Saturation
% 8.07/1.51 % (3516213)Time elapsed: 0.039 s
% 8.07/1.51 % (3516213)Peak memory usage: 91 MB
% 8.07/1.51 % (3516213)Instructions burned: 159 (million)
% 8.07/1.51 % (3516219)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=1131649623:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2996 on theBenchmark for (2996ds/106Mi)
% 8.07/1.51 % (3516220)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3469380841:i=107_2996 on theBenchmark for (2996ds/107Mi)
% 8.07/1.51 % (3516212)------------------------------
% 8.07/1.51 % (3516212)------------------------------
% 8.07/1.51 % (3516219)Instruction limit reached!
% 8.07/1.51 % (3516219)------------------------------
% 8.07/1.51 % (3516219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516219)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516219)Termination reason: Instruction limit
% 8.07/1.51 % (3516219)Termination phase: Saturation
% 8.07/1.51 % (3516219)Time elapsed: 0.031 s
% 8.07/1.51 % (3516219)Peak memory usage: 90 MB
% 8.07/1.51 % (3516219)Instructions burned: 108 (million)
% 8.07/1.51 % (3516220)Instruction limit reached!
% 8.07/1.51 % (3516220)------------------------------
% 8.07/1.51 % (3516220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516220)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516220)Termination reason: Instruction limit
% 8.07/1.51 % (3516220)Termination phase: Saturation
% 8.07/1.51 % (3516220)Time elapsed: 0.032 s
% 8.07/1.51 % (3516220)Peak memory usage: 93 MB
% 8.07/1.51 % (3516220)Instructions burned: 107 (million)
% 8.07/1.51 % (3516223)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3501345260:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 8.07/1.51 % (3516224)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=932043729:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi)
% 8.07/1.51 % (3516223)Refutation not found, incomplete strategy
% 8.07/1.51 % (3516223)------------------------------
% 8.07/1.51 % (3516223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516223)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516223)Termination reason: Refutation not found, incomplete strategy
% 8.07/1.51 % (3516223)Time elapsed: 0.004 s
% 8.07/1.51 % (3516223)Peak memory usage: 88 MB
% 8.07/1.51 % (3516223)Instructions burned: 16 (million)
% 8.07/1.51 % (3516225)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4207917641:i=134:sd=2:doe=on:ss=axioms:sgt=14_2994 on theBenchmark for (2994ds/134Mi)
% 8.07/1.51 % (3516225)Refutation not found, incomplete strategy
% 8.07/1.51 % (3516225)------------------------------
% 8.07/1.51 % (3516225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516225)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516225)Termination reason: Refutation not found, incomplete strategy
% 8.07/1.51 % (3516225)Time elapsed: 0.005 s
% 8.07/1.51 % (3516225)Peak memory usage: 89 MB
% 8.07/1.51 % (3516225)Instructions burned: 14 (million)
% 8.07/1.51 % (3516223)------------------------------
% 8.07/1.51 % (3516223)------------------------------
% 8.07/1.51 % (3516225)------------------------------
% 8.07/1.51 % (3516225)------------------------------
% 8.07/1.51 % (3516229)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=770670627:i=499:bd=all_2992 on theBenchmark for (2992ds/499Mi)
% 8.07/1.51 % (3516230)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1212646180:i=191:fgj=on:bd=all_2992 on theBenchmark for (2992ds/191Mi)
% 8.07/1.51 % (3516230)Instruction limit reached!
% 8.07/1.51 % (3516230)------------------------------
% 8.07/1.51 % (3516230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516230)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516230)Termination reason: Instruction limit
% 8.07/1.51 % (3516230)Termination phase: Saturation
% 8.07/1.51 % (3516230)Time elapsed: 0.050 s
% 8.07/1.51 % (3516230)Peak memory usage: 92 MB
% 8.07/1.51 % (3516230)Instructions burned: 194 (million)
% 8.07/1.51 % (3516229)Instruction limit reached!
% 8.07/1.51 % (3516229)------------------------------
% 8.07/1.51 % (3516229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516229)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516229)Termination reason: Instruction limit
% 8.07/1.51 % (3516229)Termination phase: Saturation
% 8.07/1.51 % (3516229)Time elapsed: 0.136 s
% 8.07/1.51 % (3516229)Peak memory usage: 93 MB
% 8.07/1.51 % (3516229)Instructions burned: 500 (million)
% 8.07/1.51 % (3516233)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1479376641:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 8.07/1.51 % (3516233)First to succeed.
% 8.07/1.51 % (3516233)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3516186"
% 8.07/1.51 % (3516234)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2368875806:cond=on:i=156:bs=on:gtg=exists_all:er=known_2990 on theBenchmark for (2990ds/156Mi)
% 8.07/1.51 % (3516234)Instruction limit reached!
% 8.07/1.51 % (3516234)------------------------------
% 8.07/1.51 % (3516234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.07/1.51 % (3516234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.07/1.51 % (3516234)CaDiCaL version: 2.1.3
% 8.07/1.51 % (3516234)Termination reason: Instruction limit
% 8.07/1.51 % (3516234)Termination phase: Saturation
% 8.07/1.51 % (3516234)Time elapsed: 0.036 s
% 8.07/1.51 % (3516234)Peak memory usage: 89 MB
% 8.07/1.51 % (3516234)Instructions burned: 158 (million)
% 8.07/1.51 % SZS status Satisfiable for theBenchmark
% 8.07/1.51 % SZS output start Saturation.
% See solution above
% 8.07/1.51 % SZS output start Definitions and Model Updates.
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv19(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv34(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv39(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP282(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP283(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkC8 := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP315(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP314(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP313(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP312(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP311(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP310(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP309(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP308(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP307(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP306(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP305(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP304(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP303(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP302(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP301(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP300(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP299(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP298(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP297(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP296(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP295(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP284(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP285(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP286(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP287(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP288(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP289(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP290(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP291(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP292(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP293(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP294(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv22(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv20(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP42(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP43(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkC1 := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP75(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP74(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP73(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP72(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP71(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP70(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP69(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP68(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP67(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP66(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP44(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP45(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP46(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP47(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP48(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP49(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP50(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP51(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP52(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP53(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP54(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP55(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP56(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP57(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP58(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP59(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP60(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP61(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP62(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP63(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP64(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP65(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv33(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP0(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP1(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkC0 := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP41(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP40(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP200(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP240(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP241(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkC7 := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP281(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP280(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP279(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP278(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP277(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP276(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP198(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP199(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkC6 := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP239(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP238(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP237(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP236(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP235(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP234(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP201(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP202(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP203(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP204(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP205(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP206(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP207(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP208(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP209(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP210(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP211(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP212(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP213(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP214(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP215(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP216(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP217(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP218(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP219(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP220(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP221(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP222(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP223(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP224(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP225(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP226(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP227(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP228(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP229(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP230(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP231(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP232(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP233(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP177(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP178(X0,X1) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkC5 := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP197(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP196(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP195(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP194(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP193(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP192(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP179(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP180(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP181(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP182(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP183(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP184(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP185(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP186(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP187(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP188(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP189(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP190(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP191(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv36(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP275(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP274(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP273(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP272(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP271(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP270(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP269(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP268(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP267(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP266(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP265(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP264(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP263(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP262(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP261(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP260(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP259(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP258(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP257(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP256(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP255(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP254(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP253(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP252(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP251(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP250(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP249(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP248(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP247(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP246(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP245(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP244(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP243(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP242(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssPv4(X0) := $true
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP2(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP3(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP4(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP5(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP6(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP7(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP8(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP9(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP10(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP11(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP12(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP13(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP14(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP15(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP16(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP17(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP18(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP19(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP20(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP21(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP22(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP23(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP24(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP25(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP26(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP27(X0) := $false
% 8.07/1.51 for all inputs,
% 8.07/1.51 define ssSkP28(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP29(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP30(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP31(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP32(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP33(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP34(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP35(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP36(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP37(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP38(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP39(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssPv40(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP316(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP317(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkC9 := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP356(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP355(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP354(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP353(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP352(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP351(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP350(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP349(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP348(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP347(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP346(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP345(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP344(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP343(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP342(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP341(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP340(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP339(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP338(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP337(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP336(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP335(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP334(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP333(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP332(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP331(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP330(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP329(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP328(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP327(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP326(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP325(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP324(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP323(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP322(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP321(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP320(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP319(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP318(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssPv5(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP116(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP117(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkC3 := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP144(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP143(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP142(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP141(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP140(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP145(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP146(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkC4 := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP176(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP175(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP174(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP173(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP172(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP147(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP148(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP149(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP150(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP151(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP152(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP153(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP154(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP155(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP156(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP157(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP158(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP159(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP160(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP161(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP162(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP163(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP164(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP165(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP166(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP167(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP168(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP169(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP170(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP171(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssPv37(X0) := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP139(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP138(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP137(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP136(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP135(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP134(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP133(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP132(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP131(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP130(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP129(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP128(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP127(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP126(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP125(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP124(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP123(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP122(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP121(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP120(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP119(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP118(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssPv17(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP76(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP77(X0,X1) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkC2 := $false
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP115(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP114(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP113(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP112(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP111(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP110(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP109(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP108(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP107(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP106(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP105(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP104(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP103(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP102(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP101(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP100(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP99(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP98(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP97(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP96(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP95(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP94(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP93(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP92(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP91(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP90(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP89(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP88(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP87(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP86(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP85(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP84(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP83(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP82(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP81(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP80(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP79(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssSkP78(X0) := $true
% 0.09/1.60 for all inputs,
% 0.09/1.60 define ssPv6(X0) := $false
% 0.09/1.60 % SZS output end Definitions and Model Updates.
% 0.09/1.60 % (3516233)------------------------------
% 0.09/1.60 % (3516233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.09/1.60 % (3516233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/1.60 % (3516233)CaDiCaL version: 2.1.3
% 0.09/1.60 % (3516233)Termination reason: Satisfiable
% 0.09/1.60 % (3516233)Time elapsed: 0.007 s
% 0.09/1.60 % (3516233)Peak memory usage: 89 MB
% 0.09/1.60 % (3516233)Instructions burned: 21 (million)
% 0.09/1.60 % (3516233)------------------------------
% 0.09/1.60 % (3516233)------------------------------
% 0.09/1.60 % (3516186)Success in time 1.186 s
% 0.09/1.60 % Vampire exiting
%------------------------------------------------------------------------------