%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MSC018+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 12:05:47 PM UTC 2026
% Result : CounterSatisfiable 0.16s 0.47s
% Output : Saturation 0.16s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2117,axiom,
~ s_contains(X0,s_g001) ).
cnf(u2120,axiom,
s_contains(X0,s_g002) ).
cnf(u2137,axiom,
s_contains(X0,s_g053) ).
cnf(u2144,axiom,
s_contains(X0,s_g054) ).
cnf(u2149,axiom,
s_contains(X0,s_g057) ).
cnf(u2154,axiom,
s_contains(X0,s_g061) ).
cnf(u2162,axiom,
s_contains(X0,s_g005) ).
cnf(u2174,axiom,
s_contains(X0,s_g021) ).
cnf(u2179,axiom,
s_contains(X0,s_g029) ).
cnf(u2197,axiom,
s_contains(X0,s_g030) ).
cnf(u2204,axiom,
s_contains(X0,s_g035) ).
cnf(u2209,axiom,
s_contains(X0,s_g143) ).
cnf(u2214,axiom,
s_contains(X0,s_g145) ).
cnf(u2219,axiom,
s_contains(X0,s_g034) ).
cnf(u2224,axiom,
s_contains(X0,s_g062) ).
cnf(u2232,axiom,
s_contains(X0,s_g039) ).
cnf(u2239,axiom,
s_contains(X0,s_g151) ).
cnf(u2244,axiom,
s_contains(X0,s_g154) ).
cnf(u2249,axiom,
s_contains(X0,s_g155) ).
cnf(u2464,axiom,
s_contains(X0,s_BZ) ).
cnf(u2480,axiom,
s_contains(X0,s_CR) ).
cnf(u2488,axiom,
s_contains(X0,s_GT) ).
cnf(u2496,axiom,
s_contains(X0,s_HN) ).
cnf(u2524,axiom,
s_contains(X0,s_NI) ).
cnf(u2532,axiom,
s_contains(X0,s_PA) ).
cnf(u2540,axiom,
s_contains(X0,s_SV) ).
cnf(u1226,axiom,
( ~ s_contains(X0,s_g009)
| s_contains(X0,s_g054) ) ).
cnf(u934,axiom,
s_contains(s_g150,s_g151) ).
cnf(u1225,axiom,
( ~ s_contains(X0,s_g009)
| s_contains(X0,s_g053) ) ).
cnf(u2376,axiom,
s_contains(X0,s_NC) ).
cnf(u2794,axiom,
s_contains(X0,s_GG) ).
cnf(u1181,axiom,
s_contains(s_g419,s_g029) ).
cnf(u2684,axiom,
s_contains(X0,s_BH) ).
cnf(u1345,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_HN) ) ).
cnf(u1105,axiom,
s_contains(s_g017,s_CD) ).
cnf(u1238,axiom,
( ~ s_contains(X0,s_g142)
| s_contains(X0,s_g145) ) ).
cnf(u1184,axiom,
s_contains(s_g053,s_NZ) ).
cnf(u2300,axiom,
s_contains(X0,s_MU) ).
cnf(u1009,axiom,
s_contains(s_g145,s_AZ) ).
cnf(u1140,axiom,
s_contains(s_g005,s_PE) ).
cnf(u2626,axiom,
s_contains(X0,s_CN) ).
cnf(u986,axiom,
s_contains(s_g030,s_MN) ).
cnf(u952,axiom,
s_contains(s_g011,s_SN) ).
cnf(u2822,axiom,
s_contains(X0,s_SE) ).
cnf(u1177,axiom,
s_contains(s_g003,s_g021) ).
cnf(u2746,axiom,
s_contains(X0,s_GR) ).
cnf(u1164,axiom,
s_contains(s_g029,s_KN) ).
cnf(u1133,axiom,
s_contains(s_g005,s_BR) ).
cnf(u1385,axiom,
( ~ s_contains(X0,s_g419)
| s_contains(X0,s_g013) ) ).
cnf(u1005,axiom,
s_contains(s_g143,s_KZ) ).
cnf(u2126,axiom,
s_contains(X0,s_g015) ).
cnf(u1234,axiom,
( ~ s_contains(X0,s_g019)
| s_contains(X0,s_g419) ) ).
cnf(u1136,axiom,
s_contains(s_g005,s_EC) ).
cnf(u1158,axiom,
s_contains(s_g029,s_DM) ).
cnf(u948,axiom,
s_contains(s_g011,s_NE) ).
cnf(u2776,axiom,
s_contains(X0,s_CZ) ).
cnf(u1143,axiom,
s_contains(s_g005,s_UY) ).
cnf(u1157,axiom,
s_contains(s_g029,s_CU) ).
cnf(u2668,axiom,
s_contains(X0,s_TM) ).
cnf(u2185,axiom,
s_contains(s_g001,s_g003) ).
cnf(u1083,axiom,
s_contains(s_g154,s_IE) ).
cnf(u1059,axiom,
s_contains(s_g039,s_SI) ).
cnf(u1160,axiom,
s_contains(s_g029,s_GD) ).
cnf(u1086,axiom,
s_contains(s_g154,s_LT) ).
cnf(u972,axiom,
s_contains(s_g014,s_RE) ).
cnf(u2256,axiom,
s_contains(X0,s_CI) ).
cnf(u1167,axiom,
s_contains(s_g029,s_MF) ).
cnf(u1085,axiom,
s_contains(s_g154,s_IS) ).
cnf(u1107,axiom,
s_contains(s_g017,s_CF) ).
cnf(u2772,axiom,
s_contains(X0,s_BG) ).
cnf(u996,axiom,
s_contains(s_g035,s_PH) ).
cnf(u2672,axiom,
s_contains(X0,s_KG) ).
cnf(u1153,axiom,
s_contains(s_g029,s_AW) ).
cnf(u2728,axiom,
s_contains(X0,s_LK) ).
cnf(u1109,axiom,
s_contains(s_g017,s_CM) ).
cnf(u1082,axiom,
s_contains(s_g154,s_GB) ).
cnf(u2444,axiom,
s_contains(X0,s_VE) ).
cnf(u1112,axiom,
s_contains(s_g017,s_ST) ).
cnf(u1011,axiom,
s_contains(s_g145,s_CY) ).
cnf(u1081,axiom,
s_contains(s_g154,s_FO) ).
cnf(u924,axiom,
s_contains(s_g019,s_g029) ).
cnf(u1068,axiom,
s_contains(s_g151,s_PL) ).
cnf(u1190,axiom,
s_contains(s_g057,s_FM) ).
cnf(u2438,axiom,
s_contains(X0,s_PY) ).
cnf(u2762,axiom,
s_contains(X0,s_PT) ).
cnf(u1106,axiom,
s_contains(s_g017,s_ZR) ).
cnf(u2724,axiom,
s_contains(X0,s_IN) ).
cnf(u2816,axiom,
s_contains(X0,s_LT) ).
cnf(u2302,axiom,
s_contains(X0,s_MW) ).
cnf(u1062,axiom,
s_contains(s_g039,s_YU) ).
cnf(u1092,axiom,
s_contains(s_g155,s_BE) ).
cnf(u962,axiom,
s_contains(s_g014,s_BI) ).
cnf(u1061,axiom,
s_contains(s_g039,s_VA) ).
cnf(u1007,axiom,
s_contains(s_g145,s_AE) ).
cnf(u2396,axiom,
s_contains(X0,s_PW) ).
cnf(u2798,axiom,
s_contains(X0,s_JE) ).
cnf(u1064,axiom,
s_contains(s_g151,s_BY) ).
cnf(u2780,axiom,
s_contains(X0,s_MD) ).
cnf(u1071,axiom,
s_contains(s_g151,s_SU) ).
cnf(u1186,axiom,
s_contains(s_g054,s_NC) ).
cnf(u2390,axiom,
s_contains(X0,s_MH) ).
cnf(u2507,axiom,
s_contains(s_g003,s_MX) ).
cnf(u1058,axiom,
s_contains(s_g039,s_PT) ).
cnf(u1346,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_MX) ) ).
cnf(u2574,axiom,
s_contains(X0,s_DO) ).
cnf(u987,axiom,
s_contains(s_g030,s_MO) ).
cnf(u2346,axiom,
s_contains(X0,s_CG) ).
cnf(u2636,axiom,
s_contains(X0,s_MN) ).
cnf(u914,axiom,
s_contains(s_g002,s_g015) ).
cnf(u957,axiom,
s_contains(s_g013,s_HN) ).
cnf(u959,axiom,
s_contains(s_g013,s_NI) ).
cnf(u2292,axiom,
s_contains(X0,s_ET) ).
cnf(u2790,axiom,
s_contains(X0,s_SK) ).
cnf(u2348,axiom,
s_contains(X0,s_CM) ).
cnf(u983,axiom,
s_contains(s_g030,s_JP) ).
cnf(u2342,axiom,
s_contains(X0,s_ZR) ).
cnf(u2264,axiom,
s_contains(X0,s_GN) ).
cnf(u2594,axiom,
s_contains(X0,s_MS) ).
cnf(u1148,axiom,
s_contains(s_g021,s_PM) ).
cnf(u939,axiom,
s_contains(s_g011,s_CI) ).
cnf(u2702,axiom,
s_contains(X0,s_PS) ).
cnf(u2258,axiom,
s_contains(X0,s_CV) ).
cnf(u2628,axiom,
s_contains(X0,s_HK) ).
cnf(u928,axiom,
s_contains(s_g142,s_g035) ).
cnf(u2418,axiom,
s_contains(X0,s_AR) ).
cnf(u1142,axiom,
s_contains(s_g005,s_SR) ).
cnf(u985,axiom,
s_contains(s_g030,s_KR) ).
cnf(u2276,axiom,
s_contains(X0,s_NG) ).
cnf(u1018,axiom,
s_contains(s_g145,s_OM) ).
cnf(u2420,axiom,
s_contains(X0,s_BO) ).
cnf(u2836,axiom,
s_contains(X0,s_FR) ).
cnf(u976,axiom,
s_contains(s_g014,s_TZ) ).
cnf(u2590,axiom,
s_contains(X0,s_MF) ).
cnf(u2690,axiom,
s_contains(X0,s_IL) ).
cnf(u2414,axiom,
s_contains(X0,s_WF) ).
cnf(u1241,axiom,
( ~ s_contains(X0,s_g150)
| s_contains(X0,s_g039) ) ).
cnf(u2720,axiom,
s_contains(X0,s_BD) ).
cnf(u981,axiom,
s_contains(s_g030,s_CN) ).
cnf(u2408,axiom,
s_contains(X0,s_TK) ).
cnf(u1014,axiom,
s_contains(s_g145,s_IQ) ).
cnf(u2630,axiom,
s_contains(X0,s_JP) ).
cnf(u1347,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_NI) ) ).
cnf(u937,axiom,
s_contains(s_g011,s_BF) ).
cnf(u2814,axiom,
s_contains(X0,s_IS) ).
cnf(u2506,axiom,
s_contains(s_g019,s_MX) ).
cnf(u1349,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_SV) ) ).
cnf(u2642,axiom,
s_contains(X0,s_BN) ).
cnf(u2658,axiom,
s_contains(X0,s_SG) ).
cnf(u961,axiom,
s_contains(s_g013,s_SV) ).
cnf(u2366,axiom,
s_contains(X0,s_ZA) ).
cnf(u1044,axiom,
s_contains(s_g015,s_TN) ).
cnf(u933,axiom,
s_contains(s_g150,s_g039) ).
cnf(u1124,axiom,
s_contains(s_g172,s_UA) ).
cnf(u2698,axiom,
s_contains(X0,s_LB) ).
cnf(u1244,axiom,
( ~ s_contains(X0,s_g150)
| s_contains(X0,s_g155) ) ).
cnf(u2336,axiom,
s_contains(X0,s_TN) ).
cnf(u2696,axiom,
s_contains(X0,s_KW) ).
cnf(u1235,axiom,
( ~ s_contains(X0,s_g142)
| s_contains(X0,s_g030) ) ).
cnf(u2398,axiom,
s_contains(X0,s_AS) ).
cnf(u2576,axiom,
s_contains(X0,s_GD) ).
cnf(u2654,axiom,
s_contains(X0,s_MY) ).
cnf(u1088,axiom,
s_contains(s_g154,s_NO) ).
cnf(u1231,axiom,
( ~ s_contains(X0,s_g019)
| s_contains(X0,s_g021) ) ).
cnf(u1057,axiom,
s_contains(s_g039,s_RS) ).
cnf(u913,axiom,
s_contains(s_g002,s_g014) ).
cnf(u2170,axiom,
s_contains(s_g001,s_g013) ).
cnf(u1095,axiom,
s_contains(s_g155,s_DD) ).
cnf(u1237,axiom,
( ~ s_contains(X0,s_g142)
| s_contains(X0,s_g143) ) ).
cnf(u2786,axiom,
s_contains(X0,s_RU) ).
cnf(u1035,axiom,
s_contains(s_g034,s_PK) ).
cnf(u2368,axiom,
s_contains(X0,s_AU) ).
cnf(u1240,axiom,
( ~ s_contains(X0,s_g142)
| s_contains(X0,s_g062) ) ).
cnf(u1038,axiom,
s_contains(s_g015,s_DZ) ).
cnf(u2826,axiom,
s_contains(X0,s_AT) ).
cnf(u2332,axiom,
s_contains(X0,s_MA) ).
cnf(u1196,axiom,
s_contains(s_g057,s_PW) ).
cnf(u2834,axiom,
s_contains(X0,s_DD) ).
cnf(u1037,axiom,
s_contains(s_g062,s_g143) ).
cnf(u1187,axiom,
s_contains(s_g054,s_PG) ).
cnf(u1040,axiom,
s_contains(s_g015,s_EH) ).
cnf(u1233,axiom,
( ~ s_contains(X0,s_g019)
| s_contains(X0,s_g003) ) ).
cnf(u1163,axiom,
s_contains(s_g029,s_JM) ).
cnf(u2808,axiom,
s_contains(X0,s_FO) ).
cnf(u1047,axiom,
s_contains(s_g039,s_BA) ).
cnf(u1189,axiom,
s_contains(s_g054,s_VU) ).
cnf(u2840,axiom,
s_contains(X0,s_LI) ).
cnf(u1008,axiom,
s_contains(s_g145,s_AM) ).
cnf(u1034,axiom,
s_contains(s_g034,s_NP) ).
cnf(u1192,axiom,
s_contains(s_g057,s_KI) ).
cnf(u963,axiom,
s_contains(s_g014,s_DJ) ).
cnf(u1033,axiom,
s_contains(s_g034,s_MV) ).
cnf(u1004,axiom,
s_contains(s_g143,s_KG) ).
cnf(u2602,axiom,
s_contains(X0,s_VC) ).
cnf(u1199,axiom,
s_contains(s_g061,s_NU) ).
cnf(u935,axiom,
s_contains(s_g150,s_g154) ).
cnf(u1139,axiom,
s_contains(s_g005,s_GY) ).
cnf(u2804,axiom,
s_contains(X0,s_EE) ).
cnf(u2254,axiom,
s_contains(X0,s_BJ) ).
cnf(u1185,axiom,
s_contains(s_g054,s_FJ) ).
cnf(u1172,axiom,
s_contains(s_g029,s_TT) ).
cnf(u1141,axiom,
s_contains(s_g005,s_PY) ).
cnf(u2442,axiom,
s_contains(X0,s_UY) ).
cnf(u984,axiom,
s_contains(s_g030,s_KP) ).
cnf(u1144,axiom,
s_contains(s_g005,s_VE) ).
cnf(u915,axiom,
s_contains(s_g002,s_g017) ).
cnf(u956,axiom,
s_contains(s_g013,s_GT) ).
cnf(u1151,axiom,
s_contains(s_g029,s_AI) ).
cnf(u2606,axiom,
s_contains(X0,s_VI) ).
cnf(u2688,axiom,
s_contains(X0,s_GE) ).
cnf(u2638,axiom,
s_contains(X0,s_MO) ).
cnf(u1138,axiom,
s_contains(s_g005,s_GF) ).
cnf(u2266,axiom,
s_contains(X0,s_GW) ).
cnf(u2552,axiom,
s_contains(X0,s_PM) ).
cnf(u1137,axiom,
s_contains(s_g005,s_FK) ).
cnf(u2738,axiom,
s_contains(X0,s_AL) ).
cnf(u2584,axiom,
s_contains(X0,s_KN) ).
cnf(u994,axiom,
s_contains(s_g035,s_BU) ).
cnf(u911,axiom,
s_contains(s_g001,s_g150) ).
cnf(u936,axiom,
s_contains(s_g150,s_g155) ).
cnf(u2546,axiom,
s_contains(X0,s_BM) ).
cnf(u2428,axiom,
s_contains(X0,s_EC) ).
cnf(u2644,axiom,
s_contains(X0,s_ID) ).
cnf(u2262,axiom,
s_contains(X0,s_GM) ).
cnf(u2656,axiom,
s_contains(X0,s_PH) ).
cnf(u2416,axiom,
s_contains(X0,s_WS) ).
cnf(u2422,axiom,
s_contains(X0,s_BR) ).
cnf(u1115,axiom,
s_contains(s_g172,s_AZ) ).
cnf(u2580,axiom,
s_contains(X0,s_HT) ).
cnf(u1118,axiom,
s_contains(s_g172,s_KG) ).
cnf(u2734,axiom,
s_contains(X0,s_PK) ).
cnf(u1019,axiom,
s_contains(s_g145,s_PS) ).
cnf(u946,axiom,
s_contains(s_g011,s_ML) ).
cnf(u1127,axiom,
s_contains(s_g018,s_LS) ).
cnf(u2410,axiom,
s_contains(X0,s_TO) ).
cnf(u2370,axiom,
s_contains(X0,s_NF) ).
cnf(u970,axiom,
s_contains(s_g014,s_MW) ).
cnf(u2768,axiom,
s_contains(X0,s_VA) ).
cnf(u2372,axiom,
s_contains(X0,s_NZ) ).
cnf(u2592,axiom,
s_contains(X0,s_MQ) ).
cnf(u2572,axiom,
s_contains(X0,s_DM) ).
cnf(u2296,axiom,
s_contains(X0,s_KM) ).
cnf(u1070,axiom,
s_contains(s_g151,s_RU) ).
cnf(u2770,axiom,
s_contains(X0,s_YU) ).
cnf(u909,axiom,
s_contains(s_g001,s_g019) ).
cnf(u990,axiom,
s_contains(s_g035,s_ID) ).
cnf(u2784,axiom,
s_contains(X0,s_RO) ).
cnf(u910,axiom,
s_contains(s_g001,s_g142) ).
cnf(u2290,axiom,
s_contains(X0,s_ER) ).
cnf(u2662,axiom,
s_contains(X0,s_TL) ).
cnf(u2322,axiom,
s_contains(X0,s_ZW) ).
cnf(u966,axiom,
s_contains(s_g014,s_KE) ).
cnf(u1017,axiom,
s_contains(s_g145,s_LB) ).
cnf(u2774,axiom,
s_contains(X0,s_BY) ).
cnf(u922,axiom,
s_contains(s_g019,s_g013) ).
cnf(u2766,axiom,
s_contains(X0,s_SM) ).
cnf(u2324,axiom,
s_contains(X0,s_DZ) ).
cnf(u2314,axiom,
s_contains(X0,s_TZ) ).
cnf(u2722,axiom,
s_contains(X0,s_BT) ).
cnf(u2700,axiom,
s_contains(X0,s_OM) ).
cnf(u1242,axiom,
( ~ s_contains(X0,s_g150)
| s_contains(X0,s_g151) ) ).
cnf(u1091,axiom,
s_contains(s_g155,s_AT) ).
cnf(u2596,axiom,
s_contains(X0,s_PR) ).
cnf(u1094,axiom,
s_contains(s_g155,s_DE) ).
cnf(u1013,axiom,
s_contains(s_g145,s_IL) ).
cnf(u2598,axiom,
s_contains(X0,s_TC) ).
cnf(u918,axiom,
s_contains(s_g009,s_g054) ).
cnf(u1166,axiom,
s_contains(s_g029,s_LC) ).
cnf(u2778,axiom,
s_contains(X0,s_HU) ).
cnf(u1067,axiom,
s_contains(s_g151,s_MD) ).
cnf(u1165,axiom,
s_contains(s_g029,s_KY) ).
cnf(u2686,axiom,
s_contains(X0,s_CY) ).
cnf(u2394,axiom,
s_contains(X0,s_NR) ).
cnf(u2828,axiom,
s_contains(X0,s_BE) ).
cnf(u2846,axiom,
s_contains(X0,s_NL) ).
cnf(u1168,axiom,
s_contains(s_g029,s_MQ) ).
cnf(u993,axiom,
s_contains(s_g035,s_MM) ).
cnf(u1175,axiom,
s_contains(s_g029,s_VI) ).
cnf(u2288,axiom,
s_contains(X0,s_DJ) ).
cnf(u1162,axiom,
s_contains(s_g029,s_HT) ).
cnf(u1161,axiom,
s_contains(s_g029,s_GP) ).
cnf(u2694,axiom,
s_contains(X0,s_JO) ).
cnf(u2730,axiom,
s_contains(X0,s_MV) ).
cnf(u1117,axiom,
s_contains(s_g172,s_GE) ).
cnf(u2604,axiom,
s_contains(X0,s_VG) ).
cnf(u960,axiom,
s_contains(s_g013,s_PA) ).
cnf(u1195,axiom,
s_contains(s_g057,s_NR) ).
cnf(u1198,axiom,
s_contains(s_g061,s_CK) ).
cnf(u1120,axiom,
s_contains(s_g172,s_MD) ).
cnf(u2358,axiom,
s_contains(X0,s_BW) ).
cnf(u945,axiom,
s_contains(s_g011,s_LR) ).
cnf(u2760,axiom,
s_contains(X0,s_RS) ).
cnf(u1076,axiom,
s_contains(s_g154,s_JE) ).
cnf(u1207,axiom,
( ~ s_contains(X1,X2)
| ~ s_contains(X0,X1)
| s_contains(X0,X2) ) ).
cnf(u1114,axiom,
s_contains(s_g172,s_AM) ).
cnf(u1052,axiom,
s_contains(s_g039,s_IT) ).
cnf(u1113,axiom,
s_contains(s_g017,s_TD) ).
cnf(u980,axiom,
s_contains(s_g014,s_ZW) ).
cnf(u1100,axiom,
s_contains(s_g155,s_MC) ).
cnf(u1069,axiom,
s_contains(s_g151,s_RO) ).
cnf(u1015,axiom,
s_contains(s_g145,s_JO) ).
cnf(u941,axiom,
s_contains(s_g011,s_GH) ).
cnf(u2756,axiom,
s_contains(X0,s_MT) ).
cnf(u1072,axiom,
s_contains(s_g151,s_SK) ).
cnf(u1043,axiom,
s_contains(s_g015,s_SD) ).
cnf(u1046,axiom,
s_contains(s_g039,s_AL) ).
cnf(u2712,axiom,
s_contains(X0,s_TR) ).
cnf(u1079,axiom,
s_contains(s_g154,s_EE) ).
cnf(u1093,axiom,
s_contains(s_g155,s_CH) ).
cnf(u1243,axiom,
( ~ s_contains(X0,s_g150)
| s_contains(X0,s_g154) ) ).
cnf(u1066,axiom,
s_contains(s_g151,s_HU) ).
cnf(u1055,axiom,
s_contains(s_g039,s_MT) ).
cnf(u1096,axiom,
s_contains(s_g155,s_FR) ).
cnf(u995,axiom,
s_contains(s_g035,s_MY) ).
cnf(u1065,axiom,
s_contains(s_g151,s_CZ) ).
cnf(u908,axiom,
s_contains(s_g001,s_g009) ).
cnf(u1103,axiom,
s_contains(s_g830,s_JE) ).
cnf(u2550,axiom,
s_contains(X0,s_GL) ).
cnf(u1090,axiom,
s_contains(s_g154,s_SJ) ).
cnf(u2708,axiom,
s_contains(X0,s_NT) ).
cnf(u2752,axiom,
s_contains(X0,s_ME) ).
cnf(u2312,axiom,
s_contains(X0,s_SO) ).
cnf(u2286,axiom,
s_contains(X0,s_BI) ).
cnf(u1089,axiom,
s_contains(s_g154,s_SE) ).
cnf(u1204,axiom,
s_contains(s_g061,s_TV) ).
cnf(u1045,axiom,
s_contains(s_g039,s_AD) ).
cnf(u1171,axiom,
s_contains(s_g029,s_TC) ).
cnf(u2676,axiom,
s_contains(X0,s_UZ) ).
cnf(u2380,axiom,
s_contains(X0,s_SB) ).
cnf(u1048,axiom,
s_contains(s_g039,s_ES) ).
cnf(u947,axiom,
s_contains(s_g011,s_MR) ).
cnf(u2562,axiom,
s_contains(X0,s_AW) ).
cnf(u1147,axiom,
s_contains(s_g021,s_GL) ).
cnf(u1016,axiom,
s_contains(s_g145,s_KW) ).
cnf(u1150,axiom,
s_contains(s_g029,s_AG) ).
cnf(u2374,axiom,
s_contains(X0,s_FJ) ).
cnf(u942,axiom,
s_contains(s_g011,s_GM) ).
cnf(u1042,axiom,
s_contains(s_g015,s_MA) ).
cnf(u2298,axiom,
s_contains(X0,s_MG) ).
cnf(u2648,axiom,
s_contains(X0,s_LA) ).
cnf(u971,axiom,
s_contains(s_g014,s_MZ) ).
cnf(u2330,axiom,
s_contains(X0,s_LY) ).
cnf(u2328,axiom,
s_contains(X0,s_EH) ).
cnf(u943,axiom,
s_contains(s_g011,s_GN) ).
cnf(u1170,axiom,
s_contains(s_g029,s_PR) ).
cnf(u991,axiom,
s_contains(s_g035,s_KH) ).
cnf(u932,axiom,
s_contains(s_g142,s_g062) ).
cnf(u2128,axiom,
s_contains(X0,s_g017) ).
cnf(u2294,axiom,
s_contains(X0,s_KE) ).
cnf(u2750,axiom,
s_contains(X0,s_IT) ).
cnf(u967,axiom,
s_contains(s_g014,s_KM) ).
cnf(u2326,axiom,
s_contains(X0,s_EG) ).
cnf(u2844,axiom,
s_contains(X0,s_MC) ).
cnf(u2122,axiom,
s_contains(X0,s_g011) ).
cnf(u1022,axiom,
s_contains(s_g145,s_NT) ).
cnf(u2570,axiom,
s_contains(X0,s_CU) ).
cnf(u923,axiom,
s_contains(s_g019,s_g021) ).
cnf(u2436,axiom,
s_contains(X0,s_PE) ).
cnf(u2812,axiom,
s_contains(X0,s_IE) ).
cnf(u2124,axiom,
s_contains(X0,s_g014) ).
cnf(u2402,axiom,
s_contains(X0,s_NU) ).
cnf(u1132,axiom,
s_contains(s_g005,s_BO) ).
cnf(u1343,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_CR) ) ).
cnf(u1002,axiom,
s_contains(s_g143,s_TM) ).
cnf(u2404,axiom,
s_contains(X0,s_PF) ).
cnf(u1178,axiom,
s_contains(s_g003,s_g029) ).
cnf(u2732,axiom,
s_contains(X0,s_NP) ).
cnf(u912,axiom,
s_contains(s_g002,s_g011) ).
cnf(u2802,axiom,
s_contains(X0,s_DK) ).
cnf(u2360,axiom,
s_contains(X0,s_LS) ).
cnf(u2578,axiom,
s_contains(X0,s_GP) ).
cnf(u1126,axiom,
s_contains(s_g018,s_BW) ).
cnf(u2515,axiom,
( ~ s_contains(X0,s_g419)
| s_contains(X0,s_MX) ) ).
cnf(u965,axiom,
s_contains(s_g014,s_ET) ).
cnf(u2354,axiom,
s_contains(X0,s_ST) ).
cnf(u998,axiom,
s_contains(s_g035,s_TH) ).
cnf(u921,axiom,
s_contains(s_g019,s_g005) ).
cnf(u954,axiom,
s_contains(s_g013,s_BZ) ).
cnf(u1342,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_BZ) ) ).
cnf(u2356,axiom,
s_contains(X0,s_TD) ).
cnf(u989,axiom,
s_contains(s_g035,s_BN) ).
cnf(u2830,axiom,
s_contains(X0,s_CH) ).
cnf(u2392,axiom,
s_contains(X0,s_MP) ).
cnf(u1122,axiom,
s_contains(s_g172,s_TJ) ).
cnf(u2350,axiom,
s_contains(X0,s_GA) ).
cnf(u917,axiom,
s_contains(s_g009,s_g053) ).
cnf(u950,axiom,
s_contains(s_g011,s_SH) ).
cnf(u969,axiom,
s_contains(s_g014,s_MU) ).
cnf(u2810,axiom,
s_contains(X0,s_GB) ).
cnf(u1228,axiom,
( ~ s_contains(X0,s_g009)
| s_contains(X0,s_g061) ) ).
cnf(u1197,axiom,
s_contains(s_g061,s_AS) ).
cnf(u2744,axiom,
s_contains(X0,s_GI) ).
cnf(u1200,axiom,
s_contains(s_g061,s_PF) ).
cnf(u1041,axiom,
s_contains(s_g015,s_LY) ).
cnf(u1012,axiom,
s_contains(s_g145,s_GE) ).
cnf(u1028,axiom,
s_contains(s_g034,s_BD) ).
cnf(u2320,axiom,
s_contains(X0,s_ZM) ).
cnf(u1194,axiom,
s_contains(s_g057,s_MP) ).
cnf(u2382,axiom,
s_contains(X0,s_VU) ).
cnf(u2560,axiom,
s_contains(X0,s_AN) ).
cnf(u1193,axiom,
s_contains(s_g057,s_MH) ).
cnf(u2634,axiom,
s_contains(X0,s_KR) ).
cnf(u1180,axiom,
s_contains(s_g419,s_g013) ).
cnf(u1149,axiom,
s_contains(s_g021,s_US) ).
cnf(u1021,axiom,
s_contains(s_g145,s_SA) ).
cnf(u1155,axiom,
s_contains(s_g029,s_BL) ).
cnf(u1078,axiom,
s_contains(s_g154,s_DK) ).
cnf(u2740,axiom,
s_contains(X0,s_BA) ).
cnf(u1024,axiom,
s_contains(s_g145,s_TR) ).
cnf(u1174,axiom,
s_contains(s_g029,s_VG) ).
cnf(u2792,axiom,
s_contains(X0,s_UA) ).
cnf(u1031,axiom,
s_contains(s_g034,s_IR) ).
cnf(u1173,axiom,
s_contains(s_g029,s_VC) ).
cnf(u2824,axiom,
s_contains(X0,s_SJ) ).
cnf(u1146,axiom,
s_contains(s_g021,s_CA) ).
cnf(u2508,axiom,
s_contains(s_g419,s_MX) ).
cnf(u1176,axiom,
s_contains(s_g003,s_g013) ).
cnf(u1145,axiom,
s_contains(s_g021,s_BM) ).
cnf(u988,axiom,
s_contains(s_g030,s_TW) ).
cnf(u2586,axiom,
s_contains(X0,s_KY) ).
cnf(u1183,axiom,
s_contains(s_g053,s_NF) ).
cnf(u2664,axiom,
s_contains(X0,s_TP) ).
cnf(u2652,axiom,
s_contains(X0,s_BU) ).
cnf(u919,axiom,
s_contains(s_g009,s_g057) ).
cnf(u1123,axiom,
s_contains(s_g172,s_TM) ).
cnf(u2566,axiom,
s_contains(X0,s_BL) ).
cnf(u992,axiom,
s_contains(s_g035,s_LA) ).
cnf(u2568,axiom,
s_contains(X0,s_BS) ).
cnf(u1169,axiom,
s_contains(s_g029,s_MS) ).
cnf(u1156,axiom,
s_contains(s_g029,s_BS) ).
cnf(u1125,axiom,
s_contains(s_g172,s_UZ) ).
cnf(u2284,axiom,
s_contains(X0,s_TG) ).
cnf(u968,axiom,
s_contains(s_g014,s_MG) ).
cnf(u1215,axiom,
( ~ s_contains(X0,s_g001)
| s_contains(X0,s_g002) ) ).
cnf(u1128,axiom,
s_contains(s_g018,s_NA) ).
cnf(u1191,axiom,
s_contains(s_g057,s_GU) ).
cnf(u1182,axiom,
s_contains(s_g053,s_AU) ).
cnf(u940,axiom,
s_contains(s_g011,s_CV) ).
cnf(u1135,axiom,
s_contains(s_g005,s_CO) ).
cnf(u1075,axiom,
s_contains(s_g154,s_IM) ).
cnf(u2660,axiom,
s_contains(X0,s_TH) ).
cnf(u2832,axiom,
s_contains(X0,s_DE) ).
cnf(u2190,axiom,
s_contains(s_g001,s_g419) ).
cnf(u1121,axiom,
s_contains(s_g172,s_RU) ).
cnf(u1131,axiom,
s_contains(s_g005,s_AR) ).
cnf(u1202,axiom,
s_contains(s_g061,s_TK) ).
cnf(u1108,axiom,
s_contains(s_g017,s_CG) ).
cnf(u1023,axiom,
s_contains(s_g145,s_SY) ).
cnf(u1077,axiom,
s_contains(s_g154,s_AX) ).
cnf(u2252,axiom,
s_contains(X0,s_BF) ).
cnf(u1201,axiom,
s_contains(s_g061,s_PN) ).
cnf(u2412,axiom,
s_contains(X0,s_TV) ).
cnf(u1080,axiom,
s_contains(s_g154,s_FI) ).
cnf(u2796,axiom,
s_contains(X0,s_IM) ).
cnf(u1087,axiom,
s_contains(s_g154,s_LV) ).
cnf(u2406,axiom,
s_contains(X0,s_PN) ).
cnf(u1074,axiom,
s_contains(s_g154,s_GG) ).
cnf(u2564,axiom,
s_contains(X0,s_BB) ).
cnf(u974,axiom,
s_contains(s_g014,s_SC) ).
cnf(u1003,axiom,
s_contains(s_g143,s_TJ) ).
cnf(u2362,axiom,
s_contains(X0,s_NA) ).
cnf(u1381,axiom,
( ~ s_contains(X0,s_g003)
| s_contains(X0,s_g013) ) ).
cnf(u1348,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_PA) ) ).
cnf(u930,axiom,
s_contains(s_g142,s_g145) ).
cnf(u2782,axiom,
s_contains(X0,s_PL) ).
cnf(u2400,axiom,
s_contains(X0,s_CK) ).
cnf(u2806,axiom,
s_contains(X0,s_FI) ).
cnf(u2364,axiom,
s_contains(X0,s_SZ) ).
cnf(u1099,axiom,
s_contains(s_g155,s_LU) ).
cnf(u2640,axiom,
s_contains(X0,s_TW) ).
cnf(u2718,axiom,
s_contains(X0,s_AF) ).
cnf(u944,axiom,
s_contains(s_g011,s_GW) ).
cnf(u978,axiom,
s_contains(s_g014,s_YT) ).
cnf(u2788,axiom,
s_contains(X0,s_SU) ).
cnf(u2280,axiom,
s_contains(X0,s_SL) ).
cnf(u926,axiom,
s_contains(s_g019,s_g419) ).
cnf(u2754,axiom,
s_contains(X0,s_MK) ).
cnf(u955,axiom,
s_contains(s_g013,s_CR) ).
cnf(u2736,axiom,
s_contains(X0,s_AD) ).
cnf(u2274,axiom,
s_contains(X0,s_NE) ).
cnf(u2306,axiom,
s_contains(X0,s_RE) ).
cnf(u1001,axiom,
s_contains(s_g035,s_VN) ).
cnf(u2748,axiom,
s_contains(X0,s_HR) ).
cnf(u2308,axiom,
s_contains(X0,s_RW) ).
cnf(u2424,axiom,
s_contains(X0,s_CL) ).
cnf(u2646,axiom,
s_contains(X0,s_KH) ).
cnf(u2706,axiom,
s_contains(X0,s_SA) ).
cnf(u2430,axiom,
s_contains(X0,s_FK) ).
cnf(u2304,axiom,
s_contains(X0,s_MZ) ).
cnf(u2742,axiom,
s_contains(X0,s_ES) ).
cnf(u997,axiom,
s_contains(s_g035,s_SG) ).
cnf(u2582,axiom,
s_contains(X0,s_JM) ).
cnf(u2674,axiom,
s_contains(X0,s_KZ) ).
cnf(u953,axiom,
s_contains(s_g011,s_TG) ).
cnf(u2764,axiom,
s_contains(X0,s_SI) ).
cnf(u1060,axiom,
s_contains(s_g039,s_SM) ).
cnf(u2513,axiom,
( ~ s_contains(X0,s_g003)
| s_contains(X0,s_MX) ) ).
cnf(u1152,axiom,
s_contains(s_g029,s_AN) ).
cnf(u964,axiom,
s_contains(s_g014,s_ER) ).
cnf(u2352,axiom,
s_contains(X0,s_GQ) ).
cnf(u1159,axiom,
s_contains(s_g029,s_DO) ).
cnf(u2384,axiom,
s_contains(X0,s_FM) ).
cnf(u1051,axiom,
s_contains(s_g039,s_HR) ).
cnf(u1054,axiom,
s_contains(s_g039,s_MK) ).
cnf(u949,axiom,
s_contains(s_g011,s_NG) ).
cnf(u2758,axiom,
s_contains(X0,s_CS) ).
cnf(u1102,axiom,
s_contains(s_g830,s_GG) ).
cnf(u2432,axiom,
s_contains(X0,s_GF) ).
cnf(u2714,axiom,
s_contains(X0,s_YE) ).
cnf(u1101,axiom,
s_contains(s_g155,s_NL) ).
cnf(u2682,axiom,
s_contains(X0,s_AZ) ).
cnf(u973,axiom,
s_contains(s_g014,s_RW) ).
cnf(u2548,axiom,
s_contains(X0,s_CA) ).
cnf(u1104,axiom,
s_contains(s_g017,s_AO) ).
cnf(u2378,axiom,
s_contains(X0,s_PG) ).
cnf(u1073,axiom,
s_contains(s_g151,s_UA) ).
cnf(u916,axiom,
s_contains(s_g002,s_g018) ).
cnf(u1111,axiom,
s_contains(s_g017,s_GQ) ).
cnf(u1098,axiom,
s_contains(s_g155,s_LI) ).
cnf(u2272,axiom,
s_contains(X0,s_MR) ).
cnf(u1179,axiom,
s_contains(s_g419,s_g005) ).
cnf(u1097,axiom,
s_contains(s_g155,s_FX) ).
cnf(u2318,axiom,
s_contains(X0,s_YT) ).
cnf(u2666,axiom,
s_contains(X0,s_VN) ).
cnf(u2680,axiom,
s_contains(X0,s_AM) ).
cnf(u2512,axiom,
( ~ s_contains(X0,s_g019)
| s_contains(X0,s_MX) ) ).
cnf(u1053,axiom,
s_contains(s_g039,s_ME) ).
cnf(u999,axiom,
s_contains(s_g035,s_TL) ).
cnf(u1203,axiom,
s_contains(s_g061,s_TO) ).
cnf(u2838,axiom,
s_contains(X0,s_FX) ).
cnf(u1056,axiom,
s_contains(s_g039,s_CS) ).
cnf(u1206,axiom,
s_contains(s_g061,s_WS) ).
cnf(u1344,axiom,
( ~ s_contains(X0,s_g013)
| s_contains(X0,s_GT) ) ).
cnf(u1236,axiom,
( ~ s_contains(X0,s_g142)
| s_contains(X0,s_g035) ) ).
cnf(u1063,axiom,
s_contains(s_g151,s_BG) ).
cnf(u1205,axiom,
s_contains(s_g061,s_WF) ).
cnf(u1227,axiom,
( ~ s_contains(X0,s_g009)
| s_contains(X0,s_g057) ) ).
cnf(u1050,axiom,
s_contains(s_g039,s_GR) ).
cnf(u2268,axiom,
s_contains(X0,s_LR) ).
cnf(u1208,negated_conjecture,
~ s_contains(s_g030,s_MX) ).
cnf(u979,axiom,
s_contains(s_g014,s_ZM) ).
cnf(u1049,axiom,
s_contains(s_g039,s_GI) ).
cnf(u1020,axiom,
s_contains(s_g145,s_QA) ).
cnf(u1036,axiom,
s_contains(s_g062,s_g034) ).
cnf(u951,axiom,
s_contains(s_g011,s_SL) ).
cnf(u1027,axiom,
s_contains(s_g034,s_AF) ).
cnf(u2692,axiom,
s_contains(X0,s_IQ) ).
cnf(u2726,axiom,
s_contains(X0,s_IR) ).
cnf(u2650,axiom,
s_contains(X0,s_MM) ).
cnf(u2270,axiom,
s_contains(X0,s_ML) ).
cnf(u1030,axiom,
s_contains(s_g034,s_IN) ).
cnf(u1032,axiom,
s_contains(s_g034,s_LK) ).
cnf(u1188,axiom,
s_contains(s_g054,s_SB) ).
cnf(u1029,axiom,
s_contains(s_g034,s_BT) ).
cnf(u975,axiom,
s_contains(s_g014,s_SO) ).
cnf(u1000,axiom,
s_contains(s_g035,s_TP) ).
cnf(u977,axiom,
s_contains(s_g014,s_UG) ).
cnf(u1110,axiom,
s_contains(s_g017,s_GA) ).
cnf(u1026,axiom,
s_contains(s_g145,s_YD) ).
cnf(u931,axiom,
s_contains(s_g142,s_g034) ).
cnf(u1039,axiom,
s_contains(s_g015,s_EG) ).
cnf(u2704,axiom,
s_contains(X0,s_QA) ).
cnf(u920,axiom,
s_contains(s_g009,s_g061) ).
cnf(u2282,axiom,
s_contains(X0,s_SN) ).
cnf(u2440,axiom,
s_contains(X0,s_SR) ).
cnf(u1025,axiom,
s_contains(s_g145,s_YE) ).
cnf(u2820,axiom,
s_contains(X0,s_NO) ).
cnf(u2842,axiom,
s_contains(X0,s_LU) ).
cnf(u2600,axiom,
s_contains(X0,s_TT) ).
cnf(u1010,axiom,
s_contains(s_g145,s_BH) ).
cnf(u927,axiom,
s_contains(s_g142,s_g030) ).
cnf(u1134,axiom,
s_contains(s_g005,s_CL) ).
cnf(u2434,axiom,
s_contains(X0,s_GY) ).
cnf(u2316,axiom,
s_contains(X0,s_UG) ).
cnf(u929,axiom,
s_contains(s_g142,s_g143) ).
cnf(u2818,axiom,
s_contains(X0,s_LV) ).
cnf(u2278,axiom,
s_contains(X0,s_SH) ).
cnf(u2426,axiom,
s_contains(X0,s_CO) ).
cnf(u2310,axiom,
s_contains(X0,s_SC) ).
cnf(u1154,axiom,
s_contains(s_g029,s_BB) ).
cnf(u1006,axiom,
s_contains(s_g143,s_UZ) ).
cnf(u907,axiom,
s_contains(s_g001,s_g002) ).
cnf(u2558,axiom,
s_contains(X0,s_AI) ).
cnf(u2588,axiom,
s_contains(X0,s_LC) ).
cnf(u1130,axiom,
s_contains(s_g018,s_ZA) ).
cnf(u2386,axiom,
s_contains(X0,s_GU) ).
cnf(u925,axiom,
s_contains(s_g019,s_g003) ).
cnf(u2260,axiom,
s_contains(X0,s_GH) ).
cnf(u1129,axiom,
s_contains(s_g018,s_SZ) ).
cnf(u2800,axiom,
s_contains(X0,s_AX) ).
cnf(u2678,axiom,
s_contains(X0,s_AE) ).
cnf(u2388,axiom,
s_contains(X0,s_KI) ).
cnf(u2505,axiom,
s_contains(s_g001,s_MX) ).
cnf(u958,axiom,
s_contains(s_g013,s_MX) ).
cnf(u2554,axiom,
s_contains(X0,s_US) ).
cnf(u2344,axiom,
s_contains(X0,s_CF) ).
cnf(u1116,axiom,
s_contains(s_g172,s_BY) ).
cnf(u2670,axiom,
s_contains(X0,s_TJ) ).
cnf(u2556,axiom,
s_contains(X0,s_AG) ).
cnf(u2632,axiom,
s_contains(X0,s_KP) ).
cnf(u2338,axiom,
s_contains(X0,s_AO) ).
cnf(u982,axiom,
s_contains(s_g030,s_HK) ).
cnf(u2716,axiom,
s_contains(X0,s_YD) ).
cnf(u1230,axiom,
( ~ s_contains(X0,s_g019)
| s_contains(X0,s_g013) ) ).
cnf(u938,axiom,
s_contains(s_g011,s_BJ) ).
cnf(u1229,axiom,
( ~ s_contains(X0,s_g019)
| s_contains(X0,s_g005) ) ).
cnf(u2340,axiom,
s_contains(X0,s_CD) ).
cnf(u2710,axiom,
s_contains(X0,s_SY) ).
cnf(u1232,axiom,
( ~ s_contains(X0,s_g019)
| s_contains(X0,s_g029) ) ).
cnf(u1119,axiom,
s_contains(s_g172,s_KZ) ).
cnf(u2334,axiom,
s_contains(X0,s_SD) ).
cnf(u1239,axiom,
( ~ s_contains(X0,s_g142)
| s_contains(X0,s_g034) ) ).
cnf(u2130,axiom,
s_contains(X0,s_g018) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MSC018+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n006.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 17:43:11 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.47 % (3200815)Will run a generic schedule for satisfiability detection.
% 0.16/0.47 % (3200822)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3312079491:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.16/0.47 % (3200821)% WARNING: option uhcvi not known.
% 0.16/0.47 % (3200821)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3804766936:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.16/0.47 % (3200823)dis+10_1_sil=32000:sp=arity:random_seed=658584523:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.16/0.47 % (3200825)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2453628:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.16/0.47 % (3200824)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3063858969:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.16/0.47 % (3200826)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2951926350:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.16/0.47 % (3200820)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1992993869_2999 on theBenchmark for (2999ds/0Mi)
% 0.16/0.47 % (3200822) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3200815-3200822"...
% 0.16/0.47 % (3200822)...printing done.
% 0.16/0.47 % Detected minimum model sizes of [1]
% 0.16/0.47 % Detected maximum model sizes of [280]
% 0.16/0.47 % TRYING [1]
% 0.16/0.47 % TRYING [2]
% 0.16/0.47 % SZS status CounterSatisfiable for theBenchmark
% 0.16/0.47 % SZS output start Saturation.
% See solution above
% 0.16/0.48 % SZS output start Definitions and Model Updates.
% 0.16/0.48 for all inputs,
% 0.16/0.48 define s_partOf(X0,X1) := $true
% 0.16/0.48 % SZS output end Definitions and Model Updates.
% 0.16/0.48 % (3200822)------------------------------
% 0.16/0.48 % (3200822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.48 % (3200822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.48 % (3200822)CaDiCaL version: 2.1.3
% 0.16/0.48 % (3200822)Termination reason: Satisfiable
% 0.16/0.48 % (3200822)Time elapsed: 0.014 s
% 0.16/0.48 % (3200822)Peak memory usage: 13 MB
% 0.16/0.48 % (3200822)Instructions burned: 42 (million)
% 0.16/0.48 % (3200815)Success in time 0.051 s
% 0.16/0.48 % Vampire exiting
%------------------------------------------------------------------------------