%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% 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:17:26 PM UTC 2026
% Result : Satisfiable 0.03s 0.20s
% Output : Saturation 0.03s
% 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(u495,negated_conjecture,
( ~ c1_1(X2)
| c5_2(X2,X4)
| c2_2(X2,X4)
| c3_2(X2,X4)
| ~ ndr1_1(X2)
| ~ c2_2(X2,a999) ) ).
cnf(u502,negated_conjecture,
( ~ c1_1(X2)
| c1_2(X2,a999)
| c5_2(X2,X4)
| c2_2(X2,X4)
| c3_2(X2,X4)
| ~ ndr1_1(X2) ) ).
cnf(u506,negated_conjecture,
( ~ c1_1(X2)
| c3_2(X2,a999)
| c5_2(X2,X4)
| c2_2(X2,X4)
| c3_2(X2,X4)
| ~ ndr1_1(X2) ) ).
cnf(u510,negated_conjecture,
c1_0 ).
cnf(u521,negated_conjecture,
( ~ c4_1(X0)
| c1_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ c2_2(X0,X2)
| ~ 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,
( ~ c1_1(X0)
| c4_2(X0,X1)
| ~ c3_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u603,negated_conjecture,
( ~ c1_1(X0)
| c5_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u608,negated_conjecture,
~ ndr1_1(a1070) ).
cnf(u649,negated_conjecture,
~ c5_0 ).
cnf(u653,negated_conjecture,
( ~ ndr1_1(X2)
| c1_1(X2)
| c1_2(X2,X3)
| c5_2(X2,X3)
| ~ c5_2(X2,a1134) ) ).
cnf(u656,negated_conjecture,
( ~ ndr1_1(X0)
| c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u713,negated_conjecture,
( ~ c2_1(X0)
| c1_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u726,negated_conjecture,
( ~ c4_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u730,negated_conjecture,
( ~ c1_1(X0)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c3_2(X0,a1038)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u733,negated_conjecture,
ssSkC7 ).
cnf(u738,negated_conjecture,
( ~ c1_1(X0)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,a1038)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u742,negated_conjecture,
( ~ c1_1(X0)
| c2_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c4_2(X0,a1038)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
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,
( ~ ndr1_1(X0)
| c3_1(X0)
| c4_2(X0,X1)
| ~ c3_2(X0,a1101)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u797,negated_conjecture,
( ~ ndr1_1(X0)
| c3_1(X0)
| c4_2(X0,X1)
| ~ c1_2(X0,a1101)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u801,negated_conjecture,
( ~ ndr1_1(X0)
| c3_1(X0)
| c4_2(X0,X1)
| ~ c5_2(X0,a1101)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u806,negated_conjecture,
~ ssSkC18 ).
cnf(u809,negated_conjecture,
( ~ ssSkP5(X0)
| c2_2(X0,X1)
| ~ c5_2(X0,a1108)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u813,negated_conjecture,
( ~ c3_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c3_2(X0,a1138)
| ~ ndr1_1(X0) ) ).
cnf(u816,negated_conjecture,
ssSkC23 ).
cnf(u821,negated_conjecture,
~ ssSkC17 ).
cnf(u825,negated_conjecture,
( ~ ssSkP4(X0)
| c2_2(X0,X1)
| ~ c4_2(X0,a1093)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u829,negated_conjecture,
( ~ ndr1_1(X0)
| c3_1(X0)
| c5_2(X0,X1)
| ~ c3_2(X0,a1106)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u833,negated_conjecture,
ssSkC5 ).
cnf(u869,negated_conjecture,
( ~ c3_1(X0)
| c2_2(X0,a1138)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u876,negated_conjecture,
ssSkC27 ).
cnf(u885,negated_conjecture,
( ~ ssSkP4(X0)
| c2_2(X0,a1093)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u889,negated_conjecture,
( ~ ssSkP4(X0)
| c1_2(X0,a1093)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u893,negated_conjecture,
( ~ ndr1_1(X0)
| c3_1(X0)
| c4_2(X0,a1106)
| c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u897,negated_conjecture,
( ~ ndr1_1(X0)
| c3_1(X0)
| c5_2(X0,a1106)
| c5_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u901,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| c1_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u931,negated_conjecture,
ssSkC16 ).
cnf(u942,negated_conjecture,
( ~ ndr1_1(X0)
| c2_2(X0,X1)
| ~ c4_2(X0,a1034)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u946,negated_conjecture,
( ~ ndr1_1(X0)
| c2_2(X0,X1)
| ~ c5_2(X0,a1034)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u955,negated_conjecture,
~ c4_1(a1070) ).
cnf(u971,negated_conjecture,
( ~ ndr1_1(X0)
| c5_1(X0)
| c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u975,negated_conjecture,
( ~ ndr1_1(X0)
| c1_2(X0,a1034)
| c2_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c3_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(u1052,negated_conjecture,
~ ndr1_1(a1010) ).
cnf(u1055,negated_conjecture,
( ~ c2_2(a1010,X0)
| c3_2(a1010,X0)
| ~ c1_2(a1010,X0) ) ).
cnf(u1059,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(u1100,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(u1152,negated_conjecture,
~ ndr1_1(a1026) ).
cnf(u1168,negated_conjecture,
ssSkC24 ).
cnf(u1179,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(u1191,negated_conjecture,
~ ssSkC26 ).
cnf(u1195,negated_conjecture,
ndr1_1(a1151) ).
cnf(u1199,negated_conjecture,
( ~ c2_2(a1151,X0)
| c5_2(a1151,X0)
| ~ c1_2(a1151,X0) ) ).
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(u1266,negated_conjecture,
~ ssSkC9 ).
cnf(u1271,negated_conjecture,
~ ndr1_1(a1053) ).
cnf(u1278,negated_conjecture,
ndr1_1(a1059) ).
cnf(u1282,negated_conjecture,
( ~ c5_2(a1059,X0)
| c1_2(a1059,X0)
| c3_2(a1059,X0) ) ).
cnf(u1286,negated_conjecture,
( ~ c2_2(a1147,X0)
| c3_2(a1147,X0)
| c1_2(a1147,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,
( c5_2(a1075,X0)
| c4_2(a1075,X0)
| c1_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,
( ~ c1_1(X0)
| c5_1(X0)
| ~ c4_2(X0,a1006) ) ).
cnf(u1353,negated_conjecture,
ssSkC1 ).
cnf(u1357,negated_conjecture,
ssSkC0 ).
cnf(u1362,negated_conjecture,
( ~ c1_1(X0)
| c5_1(X0)
| ~ c3_2(X0,a1006) ) ).
cnf(u1378,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| ~ c3_2(X0,a1120) ) ).
cnf(u1395,negated_conjecture,
~ c4_2(a1051,a1052) ).
cnf(u1421,negated_conjecture,
~ ndr1_1(a1009) ).
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,
( ~ ssSkP6(X0)
| c3_1(X0)
| ~ c5_2(X0,a1128) ) ).
cnf(u1476,negated_conjecture,
( ~ ssSkP6(X0)
| c3_1(X0)
| ~ c4_2(X0,a1128) ) ).
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(u1516,negated_conjecture,
~ ssSkC14 ).
cnf(u1524,negated_conjecture,
~ ndr1_1(a1083) ).
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(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(u1853,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(u1977,negated_conjecture,
~ c1_2(a1151,a1152) ).
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(u2204,negated_conjecture,
~ ndr1_1(a1149) ).
cnf(u2210,negated_conjecture,
c2_1(a1153) ).
cnf(u2214,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(u2310,negated_conjecture,
~ c1_1(a1083) ).
cnf(u2335,negated_conjecture,
c2_2(a1147,a1148) ).
cnf(u2340,negated_conjecture,
c4_2(a1147,a1148) ).
cnf(u2345,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(u2390,negated_conjecture,
~ ndr1_1(a1054) ).
cnf(u2396,negated_conjecture,
c4_1(a1062) ).
cnf(u2401,negated_conjecture,
ndr1_1(a1067) ).
cnf(u2416,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(u2486,negated_conjecture,
c2_1(a1009) ).
cnf(u2526,negated_conjecture,
c4_1(a1053) ).
cnf(u2531,negated_conjecture,
c1_1(a1053) ).
cnf(u2567,negated_conjecture,
c2_1(a1083) ).
cnf(u2594,negated_conjecture,
c5_1(a1151) ).
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(u2723,negated_conjecture,
c2_2(a1049,a1128) ).
cnf(u2728,negated_conjecture,
c1_2(a1067,a1127) ).
cnf(u2738,negated_conjecture,
~ c3_2(a1049,a1128) ).
cnf(u2756,negated_conjecture,
c1_2(a1075,a1127) ).
cnf(u2759,negated_conjecture,
~ c3_1(a1075) ).
cnf(u2807,negated_conjecture,
~ c5_2(a1051,a1134) ).
cnf(u2819,negated_conjecture,
~ c5_2(a1104,a1134) ).
cnf(u2831,negated_conjecture,
~ c5_2(a1149,a1134) ).
cnf(u2843,negated_conjecture,
~ c5_2(a1153,a1134) ).
cnf(u2855,negated_conjecture,
~ c5_2(a1026,a1134) ).
cnf(u2867,negated_conjecture,
~ c5_2(a1010,a1134) ).
cnf(u2879,negated_conjecture,
~ c5_2(a1049,a1134) ).
cnf(u2891,negated_conjecture,
~ c5_2(a1054,a1134) ).
cnf(u2903,negated_conjecture,
~ c5_2(a1067,a1134) ).
cnf(u2915,negated_conjecture,
~ c5_2(a1075,a1134) ).
cnf(u2922,negated_conjecture,
c1_1(a1075) ).
cnf(u2927,negated_conjecture,
~ c5_2(a1084,a1134) ).
cnf(u2939,negated_conjecture,
~ c5_2(a1097,a1134) ).
cnf(u2951,negated_conjecture,
~ c5_2(a1059,a1134) ).
cnf(u2963,negated_conjecture,
~ c5_2(a1147,a1134) ).
cnf(u2975,negated_conjecture,
~ c5_2(a1000,a1134) ).
cnf(u2987,negated_conjecture,
~ c5_2(a1141,a1134) ).
cnf(u3102,negated_conjecture,
~ c3_2(a1062,a1120) ).
cnf(u3106,negated_conjecture,
c3_1(a1062) ).
cnf(u3111,negated_conjecture,
c4_2(a1062,a1120) ).
cnf(u3116,negated_conjecture,
c5_2(a1062,a1120) ).
cnf(u3145,negated_conjecture,
( ~ c5_2(a1149,X0)
| c1_2(a1149,X0) ) ).
cnf(u3149,negated_conjecture,
( ~ c5_2(a1026,X0)
| c1_2(a1026,X0) ) ).
cnf(u3154,negated_conjecture,
~ ndr1_1(a1121) ).
cnf(u3177,negated_conjecture,
( ~ c2_2(a1051,X0)
| c1_2(a1051,X0)
| ~ c3_2(a1051,X0) ) ).
cnf(u3185,negated_conjecture,
( ~ c2_2(a1104,X0)
| c1_2(a1104,X0)
| ~ c3_2(a1104,X0) ) ).
cnf(u3229,negated_conjecture,
c5_1(a1067) ).
cnf(u3237,negated_conjecture,
c5_1(a1075) ).
cnf(u3241,negated_conjecture,
( ~ c2_2(a1084,X0)
| c1_2(a1084,X0)
| ~ c3_2(a1084,X0) ) ).
cnf(u3250,negated_conjecture,
( ~ c2_2(a1059,X0)
| c1_2(a1059,X0)
| ~ c3_2(a1059,X0) ) ).
cnf(u3263,negated_conjecture,
c5_1(a1000) ).
cnf(u3268,negated_conjecture,
( ~ c2_2(a1147,X0)
| c1_2(a1147,X0) ) ).
cnf(u3280,negated_conjecture,
~ c5_2(a1151,a1134) ).
cnf(u3302,negated_conjecture,
c3_1(a1053) ).
cnf(u3335,negated_conjecture,
~ c4_2(a1051,a1034) ).
cnf(u3338,negated_conjecture,
( ~ c3_2(a1051,X0)
| c2_2(a1051,X0)
| ~ c4_2(a1051,X0) ) ).
cnf(u3343,negated_conjecture,
~ c4_2(a1104,a1034) ).
cnf(u3346,negated_conjecture,
( ~ c3_2(a1104,X0)
| c2_2(a1104,X0)
| ~ c4_2(a1104,X0) ) ).
cnf(u3351,negated_conjecture,
~ c4_2(a1149,a1034) ).
cnf(u3359,negated_conjecture,
~ c4_2(a1049,a1034) ).
cnf(u3367,negated_conjecture,
~ c4_2(a1067,a1034) ).
cnf(u3375,negated_conjecture,
~ c4_2(a1075,a1034) ).
cnf(u3383,negated_conjecture,
~ c4_2(a1084,a1034) ).
cnf(u3391,negated_conjecture,
~ c4_2(a1097,a1034) ).
cnf(u3399,negated_conjecture,
~ c4_2(a1059,a1034) ).
cnf(u3407,negated_conjecture,
~ c4_2(a1147,a1034) ).
cnf(u3410,negated_conjecture,
( ~ c3_2(a1147,X0)
| c2_2(a1147,X0)
| ~ c4_2(a1147,X0) ) ).
cnf(u3415,negated_conjecture,
~ c4_2(a1151,a1034) ).
cnf(u3418,negated_conjecture,
( ~ c3_2(a1151,X0)
| c2_2(a1151,X0)
| ~ c4_2(a1151,X0) ) ).
cnf(u3423,negated_conjecture,
~ c4_2(a1000,a1034) ).
cnf(u3426,negated_conjecture,
( ~ c3_2(a1000,X0)
| c2_2(a1000,X0)
| ~ c4_2(a1000,X0) ) ).
cnf(u3431,negated_conjecture,
~ c4_2(a1141,a1034) ).
cnf(u3434,negated_conjecture,
( ~ c3_2(a1141,X0)
| c2_2(a1141,X0)
| ~ c4_2(a1141,X0) ) ).
cnf(u3453,negated_conjecture,
~ c5_2(a1051,a1034) ).
cnf(u3458,negated_conjecture,
~ c5_2(a1104,a1034) ).
cnf(u3463,negated_conjecture,
~ c5_2(a1149,a1034) ).
cnf(u3468,negated_conjecture,
~ c5_2(a1049,a1034) ).
cnf(u3473,negated_conjecture,
~ c5_2(a1067,a1034) ).
cnf(u3478,negated_conjecture,
~ c5_2(a1075,a1034) ).
cnf(u3483,negated_conjecture,
~ c5_2(a1084,a1034) ).
cnf(u3488,negated_conjecture,
~ c5_2(a1097,a1034) ).
cnf(u3493,negated_conjecture,
~ c5_2(a1059,a1034) ).
cnf(u3498,negated_conjecture,
~ c5_2(a1147,a1034) ).
cnf(u3503,negated_conjecture,
~ c5_2(a1151,a1034) ).
cnf(u3508,negated_conjecture,
~ c5_2(a1000,a1034) ).
cnf(u3513,negated_conjecture,
~ c5_2(a1141,a1034) ).
cnf(u3551,negated_conjecture,
c1_2(a1067,a1034) ).
cnf(u3556,negated_conjecture,
c1_2(a1075,a1034) ).
cnf(u3561,negated_conjecture,
c1_2(a1084,a1034) ).
cnf(u3566,negated_conjecture,
c1_2(a1097,a1034) ).
cnf(u3571,negated_conjecture,
c1_2(a1059,a1034) ).
cnf(u3603,negated_conjecture,
~ c1_1(a1129) ).
cnf(u3617,negated_conjecture,
c3_1(a1129) ).
cnf(u3640,negated_conjecture,
~ ndr1_1(a1046) ).
cnf(u3685,negated_conjecture,
~ c3_2(a1051,a1101) ).
cnf(u3692,negated_conjecture,
c3_1(a1051) ).
cnf(u3697,negated_conjecture,
~ c3_2(a1104,a1101) ).
cnf(u3710,negated_conjecture,
~ c3_2(a1075,a1101) ).
cnf(u3718,negated_conjecture,
~ c3_2(a1084,a1101) ).
cnf(u3730,negated_conjecture,
~ c3_2(a1097,a1101) ).
cnf(u3742,negated_conjecture,
~ c3_2(a1059,a1101) ).
cnf(u3754,negated_conjecture,
~ c3_2(a1147,a1101) ).
cnf(u3766,negated_conjecture,
~ c3_2(a1151,a1101) ).
cnf(u3778,negated_conjecture,
~ c3_2(a1000,a1101) ).
cnf(u3784,negated_conjecture,
~ c3_1(a1000) ).
cnf(u3790,negated_conjecture,
~ c3_2(a1141,a1101) ).
cnf(u3802,negated_conjecture,
~ c3_2(a1067,a1101) ).
cnf(u3821,negated_conjecture,
~ c1_2(a1051,a1101) ).
cnf(u3826,negated_conjecture,
~ c1_2(a1104,a1101) ).
cnf(u3832,negated_conjecture,
~ c1_2(a1075,a1101) ).
cnf(u3837,negated_conjecture,
~ c1_2(a1084,a1101) ).
cnf(u3842,negated_conjecture,
~ c1_2(a1097,a1101) ).
cnf(u3847,negated_conjecture,
~ c1_2(a1059,a1101) ).
cnf(u3852,negated_conjecture,
~ c1_2(a1147,a1101) ).
cnf(u3857,negated_conjecture,
~ c1_2(a1151,a1101) ).
cnf(u3862,negated_conjecture,
~ c1_2(a1000,a1101) ).
cnf(u3867,negated_conjecture,
~ c1_2(a1141,a1101) ).
cnf(u3872,negated_conjecture,
~ c1_2(a1067,a1101) ).
cnf(u3878,negated_conjecture,
c1_2(a1075,a1134) ).
cnf(u3894,negated_conjecture,
~ c5_2(a1051,a1101) ).
cnf(u3899,negated_conjecture,
~ c5_2(a1104,a1101) ).
cnf(u3905,negated_conjecture,
~ c5_2(a1075,a1101) ).
cnf(u3910,negated_conjecture,
~ c5_2(a1084,a1101) ).
cnf(u3915,negated_conjecture,
~ c5_2(a1097,a1101) ).
cnf(u3920,negated_conjecture,
~ c5_2(a1059,a1101) ).
cnf(u3925,negated_conjecture,
~ c5_2(a1147,a1101) ).
cnf(u3930,negated_conjecture,
~ c5_2(a1151,a1101) ).
cnf(u3935,negated_conjecture,
~ c5_2(a1000,a1101) ).
cnf(u3940,negated_conjecture,
~ c5_2(a1141,a1101) ).
cnf(u3945,negated_conjecture,
~ c5_2(a1067,a1101) ).
cnf(u4098,negated_conjecture,
~ c4_2(a1104,a1105) ).
cnf(u4127,negated_conjecture,
~ c5_2(a1051,a1108) ).
cnf(u4135,negated_conjecture,
( ~ c5_2(a1104,X0)
| c2_2(a1104,X0)
| ~ c1_2(a1104,X0) ) ).
cnf(u4139,negated_conjecture,
~ c5_2(a1104,a1108) ).
cnf(u4147,negated_conjecture,
( ~ c5_2(a1067,X0)
| c2_2(a1067,X0)
| ~ c1_2(a1067,X0) ) ).
cnf(u4151,negated_conjecture,
~ c5_2(a1067,a1108) ).
cnf(u4163,negated_conjecture,
~ c5_2(a1075,a1108) ).
cnf(u4175,negated_conjecture,
~ c5_2(a1084,a1108) ).
cnf(u4183,negated_conjecture,
( ~ c5_2(a1097,X0)
| c2_2(a1097,X0)
| ~ c1_2(a1097,X0) ) ).
cnf(u4187,negated_conjecture,
~ c5_2(a1097,a1108) ).
cnf(u4200,negated_conjecture,
~ c5_2(a1147,a1108) ).
cnf(u4212,negated_conjecture,
~ c5_2(a1151,a1108) ).
cnf(u4221,negated_conjecture,
( ~ c5_2(a1141,X0)
| c2_2(a1141,X0)
| ~ c1_2(a1141,X0) ) ).
cnf(u4225,negated_conjecture,
~ c5_2(a1141,a1108) ).
cnf(u4233,negated_conjecture,
( ~ c5_2(a1059,X0)
| c2_2(a1059,X0) ) ).
cnf(u4237,negated_conjecture,
~ c5_2(a1059,a1108) ).
cnf(u4245,negated_conjecture,
( ~ c1_2(a1000,X0)
| c2_2(a1000,X0) ) ).
cnf(u4249,negated_conjecture,
~ c5_2(a1000,a1108) ).
cnf(u4269,negated_conjecture,
~ c4_2(a1051,a1093) ).
cnf(u4278,negated_conjecture,
~ c4_2(a1104,a1093) ).
cnf(u4287,negated_conjecture,
~ c4_2(a1067,a1093) ).
cnf(u4296,negated_conjecture,
~ c4_2(a1075,a1093) ).
cnf(u4305,negated_conjecture,
~ c4_2(a1084,a1093) ).
cnf(u4314,negated_conjecture,
~ c4_2(a1097,a1093) ).
cnf(u4324,negated_conjecture,
~ c4_2(a1147,a1093) ).
cnf(u4333,negated_conjecture,
~ c4_2(a1151,a1093) ).
cnf(u4343,negated_conjecture,
~ c4_2(a1141,a1093) ).
cnf(u4352,negated_conjecture,
~ c4_2(a1059,a1093) ).
cnf(u4357,negated_conjecture,
c4_2(a1000,a1092) ).
cnf(u4361,negated_conjecture,
~ c4_2(a1000,a1093) ).
cnf(u4403,negated_conjecture,
c4_2(a1075,a1108) ).
cnf(u4456,negated_conjecture,
~ c3_2(a1051,a1106) ).
cnf(u4464,negated_conjecture,
~ c3_2(a1104,a1106) ).
cnf(u4473,negated_conjecture,
~ c3_2(a1075,a1106) ).
cnf(u4481,negated_conjecture,
~ c3_2(a1084,a1106) ).
cnf(u4489,negated_conjecture,
~ c3_2(a1097,a1106) ).
cnf(u4497,negated_conjecture,
~ c3_2(a1059,a1106) ).
cnf(u4507,negated_conjecture,
~ c3_2(a1141,a1106) ).
cnf(u4510,negated_conjecture,
( ~ c2_2(a1141,X0)
| c5_2(a1141,X0)
| ~ c1_2(a1141,X0) ) ).
cnf(u4515,negated_conjecture,
~ c3_2(a1067,a1106) ).
cnf(u4518,negated_conjecture,
( ~ c2_2(a1067,X0)
| c5_2(a1067,X0)
| ~ c1_2(a1067,X0) ) ).
cnf(u4523,negated_conjecture,
~ c3_2(a1147,a1106) ).
cnf(u4531,negated_conjecture,
~ c3_2(a1000,a1106) ).
cnf(u4534,negated_conjecture,
( ~ c1_2(a1000,X0)
| c5_2(a1000,X0) ) ).
cnf(u4555,negated_conjecture,
c4_2(a1104,a1106) ).
cnf(u4561,negated_conjecture,
c4_2(a1075,a1106) ).
cnf(u4566,negated_conjecture,
c4_2(a1084,a1106) ).
cnf(u4571,negated_conjecture,
c4_2(a1097,a1106) ).
cnf(u4576,negated_conjecture,
c4_2(a1059,a1106) ).
cnf(u4593,negated_conjecture,
c4_2(a1147,a1106) ).
cnf(u4598,negated_conjecture,
c4_2(a1000,a1106) ).
cnf(u4610,negated_conjecture,
( ~ c5_2(a1051,X0)
| c1_2(a1051,X0) ) ).
cnf(u4616,negated_conjecture,
~ c3_2(a1051,a1138) ).
cnf(u4624,negated_conjecture,
c2_2(a1051,a1138) ).
cnf(u4641,negated_conjecture,
c5_2(a1104,a1106) ).
cnf(u4646,negated_conjecture,
c5_2(a1075,a1106) ).
cnf(u4651,negated_conjecture,
c5_2(a1084,a1106) ).
cnf(u4656,negated_conjecture,
c5_2(a1097,a1106) ).
cnf(u4661,negated_conjecture,
c5_2(a1059,a1106) ).
cnf(u4673,negated_conjecture,
( ~ c5_2(a1000,X0)
| c1_2(a1000,X0) ) ).
cnf(u4789,negated_conjecture,
c2_2(a1147,a1093) ).
cnf(u4794,negated_conjecture,
c2_2(a1151,a1093) ).
cnf(u4800,negated_conjecture,
c2_2(a1141,a1093) ).
cnf(u4805,negated_conjecture,
c2_2(a1051,a1093) ).
cnf(u4813,negated_conjecture,
c2_2(a1075,a1093) ).
cnf(u4861,negated_conjecture,
c1_2(a1147,a1093) ).
cnf(u4866,negated_conjecture,
c1_2(a1151,a1093) ).
cnf(u4870,negated_conjecture,
~ c1_2(a1141,a1093) ).
cnf(u4876,negated_conjecture,
c1_2(a1051,a1093) ).
cnf(u4881,negated_conjecture,
c1_2(a1075,a1093) ).
cnf(u4905,negated_conjecture,
~ c4_2(a1075,a1038) ).
cnf(u4913,negated_conjecture,
~ c2_2(a1075,a1038) ).
cnf(u4918,negated_conjecture,
~ c3_2(a1075,a1038) ).
cnf(u4927,negated_conjecture,
c3_2(a1075,a999) ).
cnf(u4932,negated_conjecture,
c1_2(a1075,a999) ).
cnf(u4937,negated_conjecture,
~ c2_2(a1075,a999) ).
cnf(u4956,negated_conjecture,
~ c5_2(a1051,a1138) ).
cnf(u4969,negated_conjecture,
~ c5_2(a1147,a1093) ).
cnf(u4980,negated_conjecture,
c5_2(a1147,a1106) ).
cnf(u4990,negated_conjecture,
~ c3_2(a1141,a1093) ).
cnf(u5003,negated_conjecture,
~ c3_2(a1051,a1093) ).
cnf(u5020,negated_conjecture,
~ c1_2(a1104,a1106) ).
cnf(u5036,negated_conjecture,
~ c1_2(a1097,a1106) ).
cnf(clause56,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u2686,negated_conjecture,
( ~ c5_2(X0,a1128)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u2772,negated_conjecture,
( ~ c5_2(a1075,X0)
| c1_2(a1075,X0)
| ~ c3_2(a1075,X0) ) ).
cnf(u4073,negated_conjecture,
c4_2(a1075,a1101) ).
cnf(u2780,negated_conjecture,
( ~ c5_2(a1104,X0)
| c1_2(a1104,X0)
| ~ c3_2(a1104,X0) ) ).
cnf(u5042,negated_conjecture,
c2_2(a1097,a1098) ).
cnf(clause225,negated_conjecture,
( ~ c4_2(X0,a1029)
| ssSkP1(X0) ) ).
cnf(u3275,negated_conjecture,
( ~ c5_2(a1151,X0)
| c1_2(a1151,X0)
| ~ c3_2(a1151,X0) ) ).
cnf(u4999,negated_conjecture,
~ c5_2(a1051,a1093) ).
cnf(u3294,negated_conjecture,
c5_1(a1053) ).
cnf(u5005,negated_conjecture,
c2_2(a1059,a1106) ).
cnf(u2767,negated_conjecture,
( ~ c5_2(a1000,X0)
| c1_2(a1000,X0)
| ~ c3_2(a1000,X0) ) ).
cnf(u2745,negated_conjecture,
c3_2(a1147,a1148) ).
cnf(u3098,negated_conjecture,
~ c1_1(a1062) ).
cnf(u3957,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c4_2(X0,a1093)
| c2_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c4_2(X0,a1092) ) ).
cnf(u3947,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c5_2(X0,a1108)
| c2_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c1_2(X0,a1107) ) ).
cnf(clause208,negated_conjecture,
( ~ c4_2(X0,a1107)
| ssSkP5(X0) ) ).
cnf(u4085,negated_conjecture,
( ~ c3_2(a1075,X0)
| c1_2(a1075,X0)
| c4_2(a1075,X0) ) ).
cnf(u2688,negated_conjecture,
( ~ c4_2(X0,a1128)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(clause227,negated_conjecture,
( ~ c1_2(X0,a1003)
| ssSkP0(X0) ) ).
cnf(u2773,negated_conjecture,
( ~ c5_2(a1067,X0)
| c1_2(a1067,X0)
| ~ c3_2(a1067,X0) ) ).
cnf(u3247,negated_conjecture,
( ~ c2_2(a1097,X0)
| ~ c3_2(a1097,X0)
| c1_2(a1097,X0) ) ).
cnf(clause204,negated_conjecture,
( ~ c5_2(X0,a1127)
| ssSkP6(X0) ) ).
cnf(clause123,negated_conjecture,
( ssSkP4(X0)
| c4_2(X0,a1092) ) ).
cnf(clause126,negated_conjecture,
( ssSkP2(X0)
| c1_2(X0,a1087) ) ).
cnf(clause125,negated_conjecture,
( ssSkP3(X0)
| c5_2(X0,a1090) ) ).
cnf(u4093,negated_conjecture,
~ c3_2(a1059,a1060) ).
cnf(clause150,negated_conjecture,
( ssSkP0(X0)
| c3_2(X0,a1003) ) ).
cnf(u2770,negated_conjecture,
( ~ c5_2(a1097,X0)
| c1_2(a1097,X0)
| ~ c3_2(a1097,X0) ) ).
cnf(clause143,negated_conjecture,
( ssSkP1(X0)
| c2_2(X0,a1029) ) ).
cnf(u2766,negated_conjecture,
( ~ c5_2(a1141,X0)
| c1_2(a1141,X0)
| ~ c3_2(a1141,X0) ) ).
cnf(clause54,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause53,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(clause77,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause71,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u2672,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| c1_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u4984,negated_conjecture,
c5_2(a1151,a1093) ).
cnf(clause210,negated_conjecture,
( ~ c1_2(X0,a1092)
| ssSkP4(X0) ) ).
cnf(u2693,negated_conjecture,
~ c1_2(a1010,a1011) ).
cnf(clause209,negated_conjecture,
( ~ c5_2(X0,a1107)
| ssSkP5(X0) ) ).
cnf(clause203,negated_conjecture,
( ~ c4_2(X0,a1127)
| ssSkP6(X0) ) ).
cnf(u3971,negated_conjecture,
( ~ ndr1_1(X0)
| c2_2(X0,X1)
| c2_2(X0,a1093)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,a1092) ) ).
cnf(u3974,negated_conjecture,
( ~ ndr1_1(X0)
| c2_2(X0,X1)
| c1_2(X0,a1093)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,a1092) ) ).
cnf(clause127,negated_conjecture,
( ssSkP2(X0)
| c5_2(X0,a1087) ) ).
cnf(clause116,negated_conjecture,
( ssSkP6(X0)
| c1_2(X0,a1127) ) ).
cnf(u3265,negated_conjecture,
( ~ c2_2(a1141,X0)
| ~ c3_2(a1141,X0)
| c1_2(a1141,X0) ) ).
cnf(u4074,negated_conjecture,
c1_2(a1147,a1148) ).
cnf(clause144,negated_conjecture,
( ssSkP1(X0)
| c3_2(X0,a1029) ) ).
cnf(clause55,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause151,negated_conjecture,
( ssSkP0(X0)
| c5_2(X0,a1003) ) ).
cnf(u3958,negated_conjecture,
( ~ ndr1_1(X0)
| ~ c4_2(X0,a1093)
| c2_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c2_2(X0,a1092) ) ).
cnf(clause48,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u2768,negated_conjecture,
( ~ c5_2(a1147,X0)
| c1_2(a1147,X0)
| ~ c3_2(a1147,X0) ) ).
cnf(u2781,negated_conjecture,
( ~ c5_2(a1051,X0)
| c1_2(a1051,X0)
| ~ c3_2(a1051,X0) ) ).
cnf(u3970,negated_conjecture,
( ~ ndr1_1(X0)
| c2_2(X0,X1)
| c2_2(X0,a1093)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c4_2(X0,a1092) ) ).
cnf(u2682,negated_conjecture,
c5_1(a1113) ).
cnf(u2685,negated_conjecture,
( ~ c5_2(X0,a1128)
| c3_1(X0)
| c1_2(X0,a1127) ) ).
cnf(clause124,negated_conjecture,
( ssSkP3(X0)
| c2_2(X0,a1090) ) ).
cnf(u4741,negated_conjecture,
c1_2(a1059,a1106) ).
cnf(u2687,negated_conjecture,
( ~ c4_2(X0,a1128)
| c3_1(X0)
| c1_2(X0,a1127) ) ).
cnf(u3973,negated_conjecture,
( ~ ndr1_1(X0)
| c2_2(X0,X1)
| c1_2(X0,a1093)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c4_2(X0,a1092) ) ).
cnf(clause211,negated_conjecture,
( ~ c1_2(X0,a1090)
| ssSkP3(X0) ) ).
cnf(clause122,negated_conjecture,
( ssSkP4(X0)
| c2_2(X0,a1092) ) ).
cnf(clause121,negated_conjecture,
( ssSkP5(X0)
| c1_2(X0,a1107) ) ).
cnf(clause128,negated_conjecture,
( ssSkP2(X0)
| c3_2(X0,a1087) ) ).
cnf(u2782,negated_conjecture,
( ~ c5_2(a1059,X0)
| c1_2(a1059,X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN518-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.03/0.13 % Computer : n012.cluster.edu
% 0.03/0.13 % Model : x86_64 x86_64
% 0.03/0.13 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.13 % Memory : 8046.5625MB
% 0.03/0.13 % OS : Linux 6.8.0-71-generic
% 0.03/0.13 % CPULimit : 300
% 0.03/0.13 % WCLimit : 300
% 0.03/0.13 % DateTime : Mon Sep 28 16:23:04 UTC 2026
% 0.03/0.13 % CPUTime :
% 0.03/0.13 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.03/0.15 Running first-order model finding
% 0.03/0.15 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.20 % (3494689)Will run a generic schedule for satisfiability detection.
% 0.03/0.20 % (3494695)% WARNING: option uhcvi not known.
% 0.03/0.20 % (3494697)dis+10_1_sil=32000:sp=arity:random_seed=521309442:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.03/0.20 % (3494694)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2681809177_2999 on theBenchmark for (2999ds/0Mi)
% 0.03/0.20 % (3494696)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=999502796:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.03/0.20 % (3494695)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1136444177:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.03/0.20 % (3494698)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2724661166:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.03/0.20 % (3494699)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1415092685:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.03/0.20 % (3494700)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2264089548:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.03/0.20 % Detected minimum model sizes of [1]
% 0.03/0.20 % Detected maximum model sizes of [151]
% 0.03/0.20 % TRYING [1]
% 0.03/0.20 % TRYING [2]
% 0.03/0.20 % TRYING [3]
% 0.03/0.20 % (3494699) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3494689-3494699"...
% 0.03/0.20 % (3494699)...printing done.
% 0.03/0.20 % SZS status Satisfiable for theBenchmark
% 0.03/0.20 % SZS output start Saturation.
% See solution above
% 0.03/0.20 % SZS output start Definitions and Model Updates.
% 0.03/0.20 % SZS output end Definitions and Model Updates.
% 0.03/0.20 % (3494699)------------------------------
% 0.03/0.20 % (3494699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.03/0.20 % (3494699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.03/0.20 % (3494699)CaDiCaL version: 2.1.3
% 0.03/0.20 % (3494699)Termination reason: Satisfiable
% 0.03/0.20 % (3494699)Time elapsed: 0.022 s
% 0.03/0.20 % (3494699)Peak memory usage: 14 MB
% 0.03/0.20 % (3494699)Instructions burned: 67 (million)
% 0.03/0.20 % (3494689)Success in time 0.049 s
% 0.03/0.20 % Vampire exiting
%------------------------------------------------------------------------------