%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN518-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:00:48 PM UTC 2026
% Result : Satisfiable 5.10s 1.56s
% Output : Saturation 6.84s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u477,negated_conjecture,
~ c2_0 ).
cnf(u483,negated_conjecture,
ndr1_0 ).
cnf(u491,negated_conjecture,
~ c3_0 ).
cnf(u498,negated_conjecture,
( ~ c4_2(X0,X1)
| c3_1(X0)
| c1_2(X0,X1)
| c5_2(X0,X3)
| c2_2(X0,X3)
| c1_2(X0,X3)
| ~ ndr1_1(X0) ) ).
cnf(u510,negated_conjecture,
c1_0 ).
cnf(u521,negated_conjecture,
( ~ c2_2(X0,X2)
| c1_2(X0,X1)
| ~ c4_1(X0)
| ~ c1_2(X0,X2)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u533,negated_conjecture,
~ c4_0 ).
cnf(u573,negated_conjecture,
( ~ c4_1(X0)
| c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u588,negated_conjecture,
( ~ c2_2(X0,X1)
| c4_2(X0,X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u603,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_1(X0)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u608,negated_conjecture,
~ ndr1_1(a1070) ).
cnf(u649,negated_conjecture,
~ c5_0 ).
cnf(u653,negated_conjecture,
( ~ c5_2(X2,a1134)
| c1_1(X2)
| c1_2(X2,X3)
| c5_2(X2,X3)
| ~ ndr1_1(X2) ) ).
cnf(u656,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u710,negated_conjecture,
~ c4_2(a1080,a1081) ).
cnf(u718,negated_conjecture,
~ c5_2(a1080,a1081) ).
cnf(u726,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u730,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c1_1(X0)
| ~ c3_2(X0,a1038)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u733,negated_conjecture,
ssSkC7 ).
cnf(u738,negated_conjecture,
( ~ c2_2(X0,a1038)
| c2_2(X0,X1)
| ~ c1_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u742,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c1_1(X0)
| ~ c4_2(X0,a1038)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u758,negated_conjecture,
c4_1(a1080) ).
cnf(u763,negated_conjecture,
c1_1(a1080) ).
cnf(u768,negated_conjecture,
ndr1_1(a1080) ).
cnf(u782,negated_conjecture,
ndr1_1(a1051) ).
cnf(u786,negated_conjecture,
( ~ c2_2(a1051,X1)
| c4_2(a1051,X1)
| ~ c5_2(a1051,X1) ) ).
cnf(u793,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_1(X0)
| c4_2(X0,X1)
| ~ c3_2(X0,a1101)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u797,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_1(X0)
| c4_2(X0,X1)
| ~ c1_2(X0,a1101)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u801,negated_conjecture,
( ~ c2_2(X0,X1)
| c3_1(X0)
| c4_2(X0,X1)
| ~ c5_2(X0,a1101)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u805,negated_conjecture,
ssSkC18 ).
cnf(u809,negated_conjecture,
( ~ c5_2(X0,a1108)
| c2_2(X0,X1)
| ~ ssSkP5(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u813,negated_conjecture,
( ~ c3_2(X0,a1138)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u816,negated_conjecture,
ssSkC23 ).
cnf(u821,negated_conjecture,
~ ssSkC17 ).
cnf(u825,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_2(X0,a1093)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ ssSkP4(X0) ) ).
cnf(u833,negated_conjecture,
ssSkC5 ).
cnf(u865,negated_conjecture,
( ~ c5_2(X0,X1)
| c4_2(X0,a1108)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ ssSkP5(X0) ) ).
cnf(u869,negated_conjecture,
( ~ c3_2(X0,X1)
| c2_2(X0,a1138)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u876,negated_conjecture,
ssSkC27 ).
cnf(u885,negated_conjecture,
( ~ c5_2(X0,X1)
| c2_2(X0,a1093)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ ssSkP4(X0) ) ).
cnf(u889,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_2(X0,a1093)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ ssSkP4(X0) ) ).
cnf(u901,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_1(X0)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u931,negated_conjecture,
ssSkC16 ).
cnf(u942,negated_conjecture,
( ~ c3_2(X0,X1)
| c2_2(X0,X1)
| ~ c4_2(X0,a1034)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u946,negated_conjecture,
( ~ c5_2(X0,a1034)
| c2_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u955,negated_conjecture,
~ c4_1(a1070) ).
cnf(u971,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_1(X0)
| c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u975,negated_conjecture,
( ~ c3_2(X0,X1)
| c1_2(X0,a1034)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u1002,negated_conjecture,
ssSkC15 ).
cnf(u1008,negated_conjecture,
~ ndr1_1(a1112) ).
cnf(u1014,negated_conjecture,
ssSkC19 ).
cnf(u1034,negated_conjecture,
ssSkC20 ).
cnf(u1051,negated_conjecture,
ndr1_1(a1010) ).
cnf(u1055,negated_conjecture,
( ~ c2_2(a1010,X0)
| c3_2(a1010,X0)
| ~ c1_2(a1010,X0) ) ).
cnf(u1058,negated_conjecture,
ssSkC2 ).
cnf(u1072,negated_conjecture,
~ ndr1_1(a1025) ).
cnf(u1078,negated_conjecture,
ssSkC3 ).
cnf(u1088,negated_conjecture,
~ ndr1_1(a1033) ).
cnf(u1094,negated_conjecture,
ssSkC6 ).
cnf(u1099,negated_conjecture,
ndr1_1(a1049) ).
cnf(u1103,negated_conjecture,
( ~ c2_2(a1049,X0)
| c1_2(a1049,X0)
| ~ c3_2(a1049,X0) ) ).
cnf(u1108,negated_conjecture,
~ ndr1_1(a1050) ).
cnf(u1136,negated_conjecture,
~ ndr1_1(a1103) ).
cnf(u1148,negated_conjecture,
ssSkC4 ).
cnf(u1151,negated_conjecture,
ndr1_1(a1026) ).
cnf(u1168,negated_conjecture,
ssSkC24 ).
cnf(u1180,negated_conjecture,
ssSkC25 ).
cnf(u1183,negated_conjecture,
ndr1_1(a1147) ).
cnf(u1187,negated_conjecture,
( ~ c2_2(a1147,X0)
| c3_2(a1147,X0)
| ~ c5_2(a1147,X0) ) ).
cnf(u1192,negated_conjecture,
ssSkC26 ).
cnf(u1211,negated_conjecture,
~ ndr1_1(a1062) ).
cnf(u1217,negated_conjecture,
ssSkC11 ).
cnf(u1221,negated_conjecture,
ssSkC10 ).
cnf(u1249,negated_conjecture,
ssSkC21 ).
cnf(u1255,negated_conjecture,
~ ndr1_1(a1129) ).
cnf(u1261,negated_conjecture,
ssSkC22 ).
cnf(u1267,negated_conjecture,
ssSkC9 ).
cnf(u1278,negated_conjecture,
ndr1_1(a1059) ).
cnf(u1282,negated_conjecture,
( ~ c5_2(a1059,X0)
| c1_2(a1059,X0)
| c3_2(a1059,X0) ) ).
cnf(u1290,negated_conjecture,
ndr1_1(a1000) ).
cnf(u1294,negated_conjecture,
( ~ c1_2(a1000,X0)
| c2_2(a1000,X0)
| c5_2(a1000,X0) ) ).
cnf(u1298,negated_conjecture,
( c1_2(a1075,X0)
| c4_2(a1075,X0)
| c5_2(a1075,X0) ) ).
cnf(u1301,negated_conjecture,
ndr1_1(a1075) ).
cnf(u1305,negated_conjecture,
ssSkC12 ).
cnf(u1331,negated_conjecture,
~ ndr1_1(a1063) ).
cnf(u1350,negated_conjecture,
( ~ c4_2(X0,a1006)
| c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1353,negated_conjecture,
ssSkC1 ).
cnf(u1357,negated_conjecture,
ssSkC0 ).
cnf(u1362,negated_conjecture,
( ~ c3_2(X0,a1006)
| c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1378,negated_conjecture,
( ~ c3_2(X0,a1120)
| c3_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1395,negated_conjecture,
~ c4_2(a1051,a1052) ).
cnf(u1440,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| c4_2(X0,a1120) ) ).
cnf(u1444,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| c5_2(X0,a1120) ) ).
cnf(u1472,negated_conjecture,
( ~ c5_2(X0,a1128)
| c3_1(X0)
| ~ ssSkP6(X0) ) ).
cnf(u1476,negated_conjecture,
( ~ c4_2(X0,a1128)
| c3_1(X0)
| ~ ssSkP6(X0) ) ).
cnf(u1485,negated_conjecture,
~ c2_1(a1051) ).
cnf(u1490,negated_conjecture,
c1_2(a1051,a1052) ).
cnf(u1495,negated_conjecture,
c5_2(a1051,a1052) ).
cnf(u1509,negated_conjecture,
~ ndr1_1(a1113) ).
cnf(u1517,negated_conjecture,
ssSkC14 ).
cnf(u1532,negated_conjecture,
( ~ c1_1(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u1540,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1586,negated_conjecture,
( ~ ssSkP6(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u1661,negated_conjecture,
~ c5_2(a1104,a1105) ).
cnf(u1687,negated_conjecture,
~ c2_2(a1153,a1154) ).
cnf(u1693,negated_conjecture,
~ c3_2(a1010,a1011) ).
cnf(u1698,negated_conjecture,
~ c5_2(a1010,a1011) ).
cnf(u1703,negated_conjecture,
~ c1_2(a1010,a1012) ).
cnf(u1708,negated_conjecture,
~ c5_2(a1010,a1012) ).
cnf(u1739,negated_conjecture,
~ c5_1(a1033) ).
cnf(u1744,negated_conjecture,
~ c2_1(a1050) ).
cnf(u1749,negated_conjecture,
~ c2_2(a1054,a1055) ).
cnf(u1754,negated_conjecture,
~ c4_2(a1054,a1055) ).
cnf(u1759,negated_conjecture,
~ c1_2(a1067,a1068) ).
cnf(u1764,negated_conjecture,
~ c1_2(a1075,a1076) ).
cnf(u1769,negated_conjecture,
~ c4_2(a1075,a1076) ).
cnf(u1774,negated_conjecture,
~ c2_2(a1075,a1076) ).
cnf(u1784,negated_conjecture,
~ c4_2(a1084,a1086) ).
cnf(u1789,negated_conjecture,
~ c2_2(a1084,a1086) ).
cnf(u1809,negated_conjecture,
~ c2_1(a1104) ).
cnf(u1814,negated_conjecture,
c3_2(a1104,a1105) ).
cnf(u1854,negated_conjecture,
~ c3_1(a1149) ).
cnf(u1859,negated_conjecture,
c3_2(a1149,a1150) ).
cnf(u1864,negated_conjecture,
c4_2(a1149,a1150) ).
cnf(u1869,negated_conjecture,
~ c4_1(a1153) ).
cnf(u1874,negated_conjecture,
c5_2(a1153,a1154) ).
cnf(u1879,negated_conjecture,
c4_2(a1153,a1154) ).
cnf(u1894,negated_conjecture,
ssSkC8 ).
cnf(u1928,negated_conjecture,
~ c1_2(a1059,a1060) ).
cnf(u1948,negated_conjecture,
ssSkC13 ).
cnf(u1982,negated_conjecture,
~ c5_2(a1000,a1001) ).
cnf(u1987,negated_conjecture,
~ c4_2(a1000,a1001) ).
cnf(u1992,negated_conjecture,
c2_2(a1010,a1011) ).
cnf(u1997,negated_conjecture,
c2_2(a1010,a1012) ).
cnf(u2027,negated_conjecture,
c3_1(a1033) ).
cnf(u2032,negated_conjecture,
~ c4_1(a1046) ).
cnf(u2037,negated_conjecture,
~ c5_1(a1046) ).
cnf(u2042,negated_conjecture,
~ c3_1(a1049) ).
cnf(u2047,negated_conjecture,
c4_2(a1054,a1056) ).
cnf(u2052,negated_conjecture,
c5_2(a1054,a1056) ).
cnf(u2057,negated_conjecture,
c3_2(a1054,a1056) ).
cnf(u2062,negated_conjecture,
~ c5_1(a1062) ).
cnf(u2067,negated_conjecture,
~ c1_1(a1063) ).
cnf(u2072,negated_conjecture,
~ c4_1(a1067) ).
cnf(u2077,negated_conjecture,
~ c3_1(a1067) ).
cnf(u2082,negated_conjecture,
c3_2(a1067,a1068) ).
cnf(u2087,negated_conjecture,
c2_2(a1067,a1068) ).
cnf(u2092,negated_conjecture,
~ c2_1(a1079) ).
cnf(u2097,negated_conjecture,
~ c1_1(a1079) ).
cnf(u2102,negated_conjecture,
c3_2(a1084,a1085) ).
cnf(u2107,negated_conjecture,
c2_2(a1084,a1085) ).
cnf(u2112,negated_conjecture,
c1_2(a1084,a1085) ).
cnf(u2117,negated_conjecture,
c3_2(a1084,a1086) ).
cnf(u2132,negated_conjecture,
~ c5_1(a1097) ).
cnf(u2137,negated_conjecture,
~ c2_1(a1097) ).
cnf(u2142,negated_conjecture,
c3_2(a1097,a1098) ).
cnf(u2147,negated_conjecture,
c5_2(a1097,a1098) ).
cnf(u2152,negated_conjecture,
c1_2(a1097,a1098) ).
cnf(u2158,negated_conjecture,
ndr1_1(a1104) ).
cnf(u2165,negated_conjecture,
~ c2_1(a1129) ).
cnf(u2185,negated_conjecture,
~ c2_2(a1141,a1142) ).
cnf(u2190,negated_conjecture,
~ c3_2(a1141,a1143) ).
cnf(u2200,negated_conjecture,
c5_1(a1149) ).
cnf(u2205,negated_conjecture,
ndr1_1(a1149) ).
cnf(u2210,negated_conjecture,
c2_1(a1153) ).
cnf(u2215,negated_conjecture,
ndr1_1(a1153) ).
cnf(u2239,negated_conjecture,
c3_1(a1026) ).
cnf(u2275,negated_conjecture,
c2_2(a1059,a1060) ).
cnf(u2279,negated_conjecture,
~ c5_2(a1059,a1060) ).
cnf(u2285,negated_conjecture,
c1_2(a1059,a1061) ).
cnf(u2290,negated_conjecture,
c3_2(a1059,a1061) ).
cnf(u2335,negated_conjecture,
c2_2(a1147,a1148) ).
cnf(u2340,negated_conjecture,
c4_2(a1147,a1148) ).
cnf(u2344,negated_conjecture,
~ c5_2(a1147,a1148) ).
cnf(u2359,negated_conjecture,
~ c2_1(a1000) ).
cnf(u2364,negated_conjecture,
c3_2(a1000,a1001) ).
cnf(u2376,negated_conjecture,
c2_1(a1046) ).
cnf(u2381,negated_conjecture,
c5_1(a1049) ).
cnf(u2386,negated_conjecture,
c2_1(a1054) ).
cnf(u2391,negated_conjecture,
ndr1_1(a1054) ).
cnf(u2396,negated_conjecture,
c4_1(a1062) ).
cnf(u2401,negated_conjecture,
ndr1_1(a1067) ).
cnf(u2417,negated_conjecture,
ndr1_1(a1084) ).
cnf(u2423,negated_conjecture,
ndr1_1(a1097) ).
cnf(u2428,negated_conjecture,
c5_1(a1103) ).
cnf(u2433,negated_conjecture,
c2_1(a1112) ).
cnf(u2439,negated_conjecture,
~ c4_1(a1121) ).
cnf(u2444,negated_conjecture,
~ c1_1(a1121) ).
cnf(u2450,negated_conjecture,
c4_1(a1129) ).
cnf(u2461,negated_conjecture,
~ c5_1(a1141) ).
cnf(u2466,negated_conjecture,
c1_2(a1141,a1142) ).
cnf(u2471,negated_conjecture,
c1_2(a1141,a1143) ).
cnf(u2476,negated_conjecture,
c4_2(a1141,a1143) ).
cnf(u2619,negated_conjecture,
c2_1(a1113) ).
cnf(u2624,negated_conjecture,
c1_1(a1113) ).
cnf(u2629,negated_conjecture,
c3_1(a1121) ).
cnf(u2635,negated_conjecture,
ndr1_1(a1141) ).
cnf(u2714,negated_conjecture,
c2_2(a1049,a1128) ).
cnf(u2719,negated_conjecture,
c1_2(a1067,a1127) ).
cnf(u2732,negated_conjecture,
~ c3_2(a1049,a1128) ).
cnf(u2735,negated_conjecture,
~ c1_2(a1049,a1128) ).
cnf(u2763,negated_conjecture,
~ c3_2(a1153,a1154) ).
cnf(u2766,negated_conjecture,
~ c1_2(a1153,a1154) ).
cnf(u2789,negated_conjecture,
~ c1_1(a1010) ).
cnf(u2807,negated_conjecture,
~ c1_1(a1084) ).
cnf(u2811,negated_conjecture,
~ c3_1(a1084) ).
cnf(u2820,negated_conjecture,
~ c1_1(a1059) ).
cnf(u2823,negated_conjecture,
c3_1(a1059) ).
cnf(u2835,negated_conjecture,
c1_2(a1084,a1127) ).
cnf(u2869,negated_conjecture,
~ c1_1(a1147) ).
cnf(u2905,negated_conjecture,
~ c1_1(a1051) ).
cnf(u2978,negated_conjecture,
~ c1_1(a1054) ).
cnf(u3015,negated_conjecture,
~ c1_1(a1097) ).
cnf(u3087,negated_conjecture,
~ c3_2(a1147,a1148) ).
cnf(u3099,negated_conjecture,
c4_2(a1062,a1120) ).
cnf(u3108,negated_conjecture,
c5_2(a1062,a1120) ).
cnf(u3117,negated_conjecture,
~ c1_1(a1129) ).
cnf(u3126,negated_conjecture,
c4_2(a1129,a1120) ).
cnf(u3135,negated_conjecture,
c5_2(a1129,a1120) ).
cnf(u3156,negated_conjecture,
~ c3_1(a1153) ).
cnf(u3162,negated_conjecture,
~ c3_1(a1075) ).
cnf(u3184,negated_conjecture,
~ c3_2(a1010,a1012) ).
cnf(u3194,negated_conjecture,
~ c3_2(a1059,a1060) ).
cnf(u3218,negated_conjecture,
~ c4_2(a1104,a1105) ).
cnf(u3233,negated_conjecture,
~ c4_2(a1097,a1098) ).
cnf(u3237,negated_conjecture,
~ c4_2(a1097,a1034) ).
cnf(u3245,negated_conjecture,
c4_2(a1059,a1061) ).
cnf(u3250,negated_conjecture,
~ c4_2(a1059,a1034) ).
cnf(u3259,negated_conjecture,
~ c4_2(a1149,a1034) ).
cnf(u3268,negated_conjecture,
~ c4_2(a1054,a1034) ).
cnf(u3272,negated_conjecture,
c2_2(a1054,a1056) ).
cnf(u3297,negated_conjecture,
c1_2(a1059,a1034) ).
cnf(u3302,negated_conjecture,
c1_2(a1149,a1034) ).
cnf(u3337,negated_conjecture,
c3_1(a1080) ).
cnf(u3394,negated_conjecture,
~ c4_1(a1147) ).
cnf(u3402,negated_conjecture,
~ c4_1(a1054) ).
cnf(u3410,negated_conjecture,
~ c4_1(a1084) ).
cnf(u3441,negated_conjecture,
~ c3_2(a1097,a1038) ).
cnf(u3474,negated_conjecture,
~ c3_2(a1067,a1101) ).
cnf(u3483,negated_conjecture,
~ c3_2(a1084,a1101) ).
cnf(u3502,negated_conjecture,
~ c1_2(a1067,a1101) ).
cnf(u3507,negated_conjecture,
~ c1_2(a1084,a1101) ).
cnf(u3526,negated_conjecture,
~ c5_2(a1067,a1101) ).
cnf(u3531,negated_conjecture,
~ c5_2(a1084,a1101) ).
cnf(u3549,negated_conjecture,
~ ssSkP4(a1051) ).
cnf(u3567,negated_conjecture,
~ ssSkP4(a1097) ).
cnf(u3571,negated_conjecture,
~ c4_2(a1097,a1093) ).
cnf(u3589,negated_conjecture,
~ c3_2(a1051,a1092) ).
cnf(u3592,negated_conjecture,
~ c1_2(a1051,a1092) ).
cnf(u3602,negated_conjecture,
~ c4_1(a1051) ).
cnf(u3621,negated_conjecture,
~ ssSkP5(a1051) ).
cnf(u3630,negated_conjecture,
~ ssSkP5(a1097) ).
cnf(u3661,negated_conjecture,
~ c3_1(a1104) ).
cnf(u3679,negated_conjecture,
~ c3_1(a1000) ).
cnf(u3717,negated_conjecture,
~ c1_2(a1097,a1092) ).
cnf(u3729,negated_conjecture,
~ c3_2(a1097,a1092) ).
cnf(u3755,negated_conjecture,
( c1_2(a1051,X0)
| c5_2(a1051,X0)
| c2_2(a1051,X0) ) ).
cnf(u3766,negated_conjecture,
( c1_2(a1147,X0)
| c5_2(a1147,X0)
| c2_2(a1147,X0) ) ).
cnf(u3774,negated_conjecture,
( c1_2(a1149,X0)
| c5_2(a1149,X0)
| c2_2(a1149,X0) ) ).
cnf(u3783,negated_conjecture,
( c1_2(a1097,X0)
| c5_2(a1097,X0)
| c2_2(a1097,X0) ) ).
cnf(u2672,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_1(X0)
| c1_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u2727,negated_conjecture,
~ c1_2(a1010,a1011) ).
cnf(clause151,negated_conjecture,
( ssSkP0(X0)
| c5_2(X0,a1003) ) ).
cnf(clause116,negated_conjecture,
( ssSkP6(X0)
| c1_2(X0,a1127) ) ).
cnf(clause123,negated_conjecture,
( ssSkP4(X0)
| c4_2(X0,a1092) ) ).
cnf(clause227,negated_conjecture,
( ~ c1_2(X0,a1003)
| ssSkP0(X0) ) ).
cnf(u3638,negated_conjecture,
c1_2(a1097,a1107) ).
cnf(clause55,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause208,negated_conjecture,
( ~ c4_2(X0,a1107)
| ssSkP5(X0) ) ).
cnf(clause203,negated_conjecture,
( ~ c4_2(X0,a1127)
| ssSkP6(X0) ) ).
cnf(u2747,negated_conjecture,
c5_2(a1075,a1076) ).
cnf(clause77,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u2660,negated_conjecture,
( c3_1(X0)
| ndr1_1(X0) ) ).
cnf(clause210,negated_conjecture,
( ~ c1_2(X0,a1092)
| ssSkP4(X0) ) ).
cnf(clause121,negated_conjecture,
( ssSkP5(X0)
| c1_2(X0,a1107) ) ).
cnf(clause225,negated_conjecture,
( ~ c4_2(X0,a1029)
| ssSkP1(X0) ) ).
cnf(clause128,negated_conjecture,
( ssSkP2(X0)
| c3_2(X0,a1087) ) ).
cnf(u2769,negated_conjecture,
c1_2(a1054,a1056) ).
cnf(u3702,negated_conjecture,
c2_2(a1097,a1092) ).
cnf(clause53,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(clause125,negated_conjecture,
( ssSkP3(X0)
| c5_2(X0,a1090) ) ).
cnf(u2682,negated_conjecture,
c5_1(a1113) ).
cnf(clause56,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u2770,negated_conjecture,
~ c3_2(a1075,a1076) ).
cnf(u3701,negated_conjecture,
c4_2(a1097,a1092) ).
cnf(u3780,negated_conjecture,
( c1_2(a1153,X0)
| c2_2(a1153,X0)
| c5_2(a1153,X0) ) ).
cnf(clause127,negated_conjecture,
( ssSkP2(X0)
| c5_2(X0,a1087) ) ).
cnf(u3636,negated_conjecture,
c1_2(a1051,a1107) ).
cnf(clause71,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(clause48,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u3329,negated_conjecture,
c5_1(a1080) ).
cnf(u3095,negated_conjecture,
~ c1_1(a1062) ).
cnf(u3190,negated_conjecture,
c5_1(a1067) ).
cnf(clause122,negated_conjecture,
( ssSkP4(X0)
| c2_2(X0,a1092) ) ).
cnf(clause124,negated_conjecture,
( ssSkP3(X0)
| c2_2(X0,a1090) ) ).
cnf(u3574,negated_conjecture,
c2_2(a1051,a1092) ).
cnf(clause144,negated_conjecture,
( ssSkP1(X0)
| c3_2(X0,a1029) ) ).
cnf(clause204,negated_conjecture,
( ~ c5_2(X0,a1127)
| ssSkP6(X0) ) ).
cnf(clause54,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause211,negated_conjecture,
( ~ c1_2(X0,a1090)
| ssSkP3(X0) ) ).
cnf(u3573,negated_conjecture,
c4_2(a1051,a1092) ).
cnf(clause126,negated_conjecture,
( ssSkP2(X0)
| c1_2(X0,a1087) ) ).
cnf(clause143,negated_conjecture,
( ssSkP1(X0)
| c2_2(X0,a1029) ) ).
cnf(clause150,negated_conjecture,
( ssSkP0(X0)
| c3_2(X0,a1003) ) ).
cnf(clause209,negated_conjecture,
( ~ c5_2(X0,a1107)
| ssSkP5(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN518-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.19 % Computer : n008.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.19 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Mon Sep 28 16:24:09 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.22 Running first-order theorem proving
% 0.06/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.10/1.56 % (2377181)Input is clausal, will run a generic CNF schedule.
% 5.10/1.56 % (2377188)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3895610379:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.10/1.56 % (2377187)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2846831214:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.10/1.56 % (2377186)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=3473616687:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.10/1.56 % (2377191)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2298811877:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.10/1.56 % (2377192)dis-21_1_sil=8000:lcm=predicate:random_seed=1956075971: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)
% 5.10/1.56 % (2377190)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2606834316:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.10/1.56 % (2377189)lrs+10_1_sil=8000:sp=occurrence:random_seed=2259999370:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.10/1.56 % (2377191)Refutation not found, incomplete strategy
% 5.10/1.56 % (2377191)------------------------------
% 5.10/1.56 % (2377191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377191)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377191)Termination reason: Refutation not found, incomplete strategy
% 5.10/1.56 % (2377191)Time elapsed: 0.023 s
% 5.10/1.56 % (2377191)Peak memory usage: 90 MB
% 5.10/1.56 % (2377191)Instructions burned: 37 (million)
% 5.10/1.56 % (2377189)Instruction limit reached!
% 5.10/1.56 % (2377189)------------------------------
% 5.10/1.56 % (2377189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377189)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377189)Termination reason: Instruction limit
% 5.10/1.56 % (2377189)Termination phase: Saturation
% 5.10/1.56 % (2377189)Time elapsed: 0.060 s
% 5.10/1.56 % (2377189)Peak memory usage: 90 MB
% 5.10/1.56 % (2377189)Instructions burned: 108 (million)
% 5.10/1.56 % (2377192)Instruction limit reached!
% 5.10/1.56 % (2377192)------------------------------
% 5.10/1.56 % (2377192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377192)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377192)Termination reason: Instruction limit
% 5.10/1.56 % (2377192)Termination phase: Saturation
% 5.10/1.56 % (2377192)Time elapsed: 0.065 s
% 5.10/1.56 % (2377192)Peak memory usage: 90 MB
% 5.10/1.56 % (2377192)Instructions burned: 118 (million)
% 5.10/1.56 % (2377190)Instruction limit reached!
% 5.10/1.56 % (2377190)------------------------------
% 5.10/1.56 % (2377190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377190)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377190)Termination reason: Instruction limit
% 5.10/1.56 % (2377190)Termination phase: Saturation
% 5.10/1.56 % (2377190)Time elapsed: 0.065 s
% 5.10/1.56 % (2377190)Peak memory usage: 90 MB
% 5.10/1.56 % (2377190)Instructions burned: 116 (million)
% 5.10/1.56 % (2377201)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=963395674:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 5.10/1.56 % (2377200)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=1756879631:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.10/1.56 % (2377202)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=361255802:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.10/1.56 % (2377201)Refutation not found, incomplete strategy
% 5.10/1.56 % (2377201)------------------------------
% 5.10/1.56 % (2377201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377201)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377201)Termination reason: Refutation not found, incomplete strategy
% 5.10/1.56 % (2377201)Time elapsed: 0.032 s
% 5.10/1.56 % (2377201)Peak memory usage: 90 MB
% 5.10/1.56 % (2377201)Instructions burned: 58 (million)
% 5.10/1.56 % (2377191)------------------------------
% 5.10/1.56 % (2377191)------------------------------
% 5.10/1.56 % (2377200)Instruction limit reached!
% 5.10/1.56 % (2377200)------------------------------
% 5.10/1.56 % (2377200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377200)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377200)Termination reason: Instruction limit
% 5.10/1.56 % (2377200)Termination phase: Saturation
% 5.10/1.56 % (2377200)Time elapsed: 0.078 s
% 5.10/1.56 % (2377200)Peak memory usage: 90 MB
% 5.10/1.56 % (2377200)Instructions burned: 143 (million)
% 5.10/1.56 % (2377202)Instruction limit reached!
% 5.10/1.56 % (2377202)------------------------------
% 5.10/1.56 % (2377202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377202)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377202)Termination reason: Instruction limit
% 5.10/1.56 % (2377202)Termination phase: Saturation
% 5.10/1.56 % (2377202)Time elapsed: 0.116 s
% 5.10/1.56 % (2377202)Peak memory usage: 91 MB
% 5.10/1.56 % (2377202)Instructions burned: 219 (million)
% 5.10/1.56 % (2377206)lrs+10_64_to=lpo:sil=8000:random_seed=3335444401:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.10/1.56 % (2377206)First to succeed.
% 5.10/1.56 % (2377206)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2377181"
% 5.10/1.56 % (2377207)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=884360364:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.10/1.56 % (2377207)Refutation not found, incomplete strategy
% 5.10/1.56 % (2377207)------------------------------
% 5.10/1.56 % (2377207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377207)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377207)Termination reason: Refutation not found, incomplete strategy
% 5.10/1.56 % (2377207)Time elapsed: 0.019 s
% 5.10/1.56 % (2377207)Peak memory usage: 89 MB
% 5.10/1.56 % (2377207)Instructions burned: 29 (million)
% 5.10/1.56 % (2377201)------------------------------
% 5.10/1.56 % (2377201)------------------------------
% 5.10/1.56 % (2377208)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1176955932:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 5.10/1.56 % (2377208)Also succeeded, but the first one will report.
% 5.10/1.56 % (2377211)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3510551805:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.10/1.56 % (2377187)Refutation not found, incomplete strategy
% 5.10/1.56 % (2377187)------------------------------
% 5.10/1.56 % (2377187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.10/1.56 % (2377187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.10/1.56 % (2377187)CaDiCaL version: 2.1.3
% 5.10/1.56 % (2377187)Termination reason: Refutation not found, incomplete strategy
% 5.10/1.56 % (2377187)Time elapsed: 0.689 s
% 5.10/1.56 % (2377187)Peak memory usage: 130 MB
% 5.10/1.56 % (2377187)Instructions burned: 1070 (million)
% 5.10/1.56 % SZS status Satisfiable for theBenchmark
% 5.10/1.56 % SZS output start Saturation.
% See solution above
% 6.84/1.75 % SZS output start Definitions and Model Updates.
% 6.84/1.75 % SZS output end Definitions and Model Updates.
% 6.84/1.75 % (2377206)------------------------------
% 6.84/1.75 % (2377206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.84/1.75 % (2377206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.84/1.75 % (2377206)CaDiCaL version: 2.1.3
% 6.84/1.75 % (2377206)Termination reason: Satisfiable
% 6.84/1.75 % (2377206)Time elapsed: 0.025 s
% 6.84/1.75 % (2377206)Peak memory usage: 90 MB
% 6.84/1.75 % (2377206)Instructions burned: 38 (million)
% 6.84/1.75 % (2377206)------------------------------
% 6.84/1.75 % (2377206)------------------------------
% 6.84/1.75 % (2377181)Success in time 0.894 s
% 6.84/1.75 % Vampire exiting
%------------------------------------------------------------------------------