%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN424-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 : n026.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 01:50:35 PM UTC 2026
% Result : Satisfiable 4.02s 1.24s
% Output : Saturation 4.56s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u770,negated_conjecture,
~ c2_0 ).
cnf(u777,negated_conjecture,
ndr1_0 ).
cnf(u781,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c10_1(X0)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u809,negated_conjecture,
~ c8_0 ).
cnf(u826,negated_conjecture,
( ~ c2_2(X0,X1)
| c4_1(X0)
| c5_2(X0,X2)
| c9_2(X0,X2)
| c10_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u829,negated_conjecture,
ssSkC28 ).
cnf(u838,negated_conjecture,
~ c6_0 ).
cnf(u845,negated_conjecture,
( ~ c6_2(X0,X1)
| c3_1(X0)
| c7_1(X0)
| c9_2(X0,X1)
| c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u849,negated_conjecture,
~ c10_0 ).
cnf(u853,negated_conjecture,
( ~ c4_2(X1,X2)
| c6_2(X1,X2)
| c9_2(X1,X2)
| ~ c2_1(X1)
| ~ c5_1(X1)
| ~ ndr1_1(X1) ) ).
cnf(u878,negated_conjecture,
~ c3_0 ).
cnf(u885,negated_conjecture,
( ~ c5_2(X0,X1)
| c3_1(X0)
| c10_1(X0)
| c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u909,negated_conjecture,
ndr1_1(a1098) ).
cnf(u913,negated_conjecture,
( ~ c2_2(a1098,X2)
| c3_2(a1098,X2)
| ~ c9_2(a1098,X2) ) ).
cnf(u916,negated_conjecture,
( ~ c4_2(X0,X1)
| c7_2(X0,X1)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u927,negated_conjecture,
( ~ c4_2(X0,X1)
| c8_1(X0)
| c5_1(X0)
| c6_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u932,negated_conjecture,
~ ndr1_1(a971) ).
cnf(u935,negated_conjecture,
( ~ c7_2(a971,X2)
| c1_2(a971,X2)
| c8_2(a971,X2) ) ).
cnf(u941,negated_conjecture,
ssSkC2 ).
cnf(u949,negated_conjecture,
( ~ c2_1(X0)
| c4_1(X0)
| ~ c7_1(X0) ) ).
cnf(u952,negated_conjecture,
ssSkC8 ).
cnf(u958,negated_conjecture,
c7_0 ).
cnf(u972,negated_conjecture,
( ~ c1_2(X0,X2)
| ~ c5_1(X0)
| ~ c8_2(X0,X2)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u976,negated_conjecture,
c9_0 ).
cnf(u980,negated_conjecture,
( ~ c1_2(X0,a965)
| c6_2(X0,X2)
| c10_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u984,negated_conjecture,
( ~ c2_2(X0,X2)
| c6_2(X0,X2)
| c10_2(X0,X1)
| ~ c4_2(X0,a965)
| ~ c6_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u989,negated_conjecture,
~ c5_0 ).
cnf(u1004,negated_conjecture,
( ~ c2_2(X0,X2)
| c10_2(X0,a965)
| c6_2(X0,X2)
| c10_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c4_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1018,negated_conjecture,
c1_0 ).
cnf(u1028,negated_conjecture,
( ~ c8_2(X0,X1)
| c10_1(X0)
| c2_2(X0,X1)
| ~ c5_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1042,negated_conjecture,
( ~ c7_2(X1,X2)
| c4_1(X1)
| c5_1(X1)
| c5_2(X1,X2)
| ~ ndr1_1(X1)
| ~ c6_2(X1,X2) ) ).
cnf(u1050,negated_conjecture,
~ ndr1_1(a1041) ).
cnf(u1059,negated_conjecture,
ssSkC18 ).
cnf(u1064,negated_conjecture,
c4_0 ).
cnf(u1068,negated_conjecture,
ndr1_1(a1124) ).
cnf(u1075,negated_conjecture,
( ~ c7_1(X0)
| c10_1(X0)
| c6_1(X0) ) ).
cnf(u1088,negated_conjecture,
( ~ c2_2(X0,a1109)
| c2_2(X0,X2)
| c10_2(X0,X2)
| c8_2(X0,X1)
| c10_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1092,negated_conjecture,
( ~ c1_2(X0,a1109)
| c2_2(X0,X2)
| c10_2(X0,X2)
| c8_2(X0,X1)
| c10_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1100,negated_conjecture,
( ~ c2_2(X0,X1)
| ~ c7_1(X0)
| ~ c5_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u1107,negated_conjecture,
( ~ c5_2(X0,X1)
| c6_2(X0,X1)
| c2_2(X0,X1)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1121,negated_conjecture,
ssSkC26 ).
cnf(u1132,negated_conjecture,
~ ssSkC38 ).
cnf(u1136,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c6_2(X0,a1129)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ssSkP5(X0) ) ).
cnf(u1140,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c4_2(X0,a1129)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ssSkP5(X0) ) ).
cnf(u1144,negated_conjecture,
( ~ c10_2(X0,X1)
| ~ c10_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c9_2(X0,X1) ) ).
cnf(u1152,negated_conjecture,
( ~ c7_2(X0,X1)
| c3_1(X0)
| c2_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1167,negated_conjecture,
ssSkC9 ).
cnf(u1195,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_1(X0)
| c4_2(X0,X1)
| ~ c8_2(X0,a1039)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1198,negated_conjecture,
ssSkC17 ).
cnf(u1203,negated_conjecture,
( ~ c5_2(X0,a1039)
| c1_1(X0)
| c4_2(X0,X1)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1207,negated_conjecture,
( ~ c7_2(X0,a1096)
| ~ c6_1(X0)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u1211,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c6_1(X0)
| ~ c4_2(X0,a1096)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1216,negated_conjecture,
~ c5_1(a1098) ).
cnf(u1220,negated_conjecture,
c8_1(a1098) ).
cnf(u1225,negated_conjecture,
( ~ c5_2(X0,a1102)
| c3_1(X0)
| c10_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1228,negated_conjecture,
ssSkC31 ).
cnf(u1233,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_1(X0)
| c10_2(X0,X1)
| ~ c4_2(X0,a1102)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1245,negated_conjecture,
( ~ c5_2(X0,X1)
| c8_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_1(X0)
| ~ c7_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1279,negated_conjecture,
( ~ c7_2(X0,X1)
| c1_2(X0,a1129)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ssSkP5(X0) ) ).
cnf(u1283,negated_conjecture,
~ ssSkC46 ).
cnf(u1287,negated_conjecture,
( ~ c5_2(X0,X1)
| c9_1(X0)
| c9_2(X0,X1)
| ~ c9_2(X0,a1159)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1291,negated_conjecture,
( ~ c10_1(X0)
| c10_2(X0,X1)
| c1_2(X0,X1)
| c6_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1299,negated_conjecture,
( ~ c5_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a1039)
| c4_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1304,negated_conjecture,
~ c1_2(a1043,a1044) ).
cnf(u1312,negated_conjecture,
~ c6_2(a1043,a1044) ).
cnf(u1321,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_2(X0,a1096)
| ~ c6_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u1325,negated_conjecture,
( ~ c1_2(X0,X1)
| c3_1(X0)
| c8_2(X0,a1102)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1329,negated_conjecture,
~ ssSkC21 ).
cnf(u1333,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ c9_2(X0,a1049)
| ~ ndr1_1(X0) ) ).
cnf(u1337,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_1(X0)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ c10_2(X0,a1049)
| ~ ndr1_1(X0) ) ).
cnf(u1341,negated_conjecture,
( ~ c5_2(X0,X1)
| c9_1(X0)
| c10_2(X0,a1159)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1345,negated_conjecture,
( ~ c5_2(X0,X1)
| c9_1(X0)
| c2_2(X0,a1159)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1349,negated_conjecture,
~ ssSkC51 ).
cnf(u1353,negated_conjecture,
( ~ c4_2(X0,a1182)
| c1_2(X0,X1)
| c10_2(X0,X1)
| ~ ssSkP11(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1357,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_2(X0,X1)
| c10_2(X0,X1)
| ~ c9_2(X0,a1182)
| ~ ndr1_1(X0)
| ~ ssSkP11(X0) ) ).
cnf(u1362,negated_conjecture,
~ c4_1(a971) ).
cnf(u1367,negated_conjecture,
~ c9_1(a971) ).
cnf(u1390,negated_conjecture,
c4_2(a1043,a1044) ).
cnf(u1405,negated_conjecture,
ssSkC19 ).
cnf(u1412,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_1(X0)
| c8_2(X0,a1049)
| c3_2(X0,X1)
| c4_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1416,negated_conjecture,
~ ssSkC29 ).
cnf(u1420,negated_conjecture,
( ~ c5_2(X0,a1084)
| c6_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1424,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,X1)
| ~ c2_1(X0)
| ~ c9_2(X0,a1084)
| ~ ndr1_1(X0) ) ).
cnf(u1428,negated_conjecture,
( ~ c1_2(X0,X1)
| c6_2(X0,X1)
| ~ c2_1(X0)
| ~ c2_2(X0,a1084)
| ~ ndr1_1(X0) ) ).
cnf(u1433,negated_conjecture,
ssSkC49 ).
cnf(u1436,negated_conjecture,
( ~ c1_2(X0,a1176)
| c9_1(X0)
| c7_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1440,negated_conjecture,
( ~ c8_2(X0,X1)
| c8_2(X0,a1182)
| c1_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP11(X0) ) ).
cnf(u1444,negated_conjecture,
( ~ c5_2(X0,a1063)
| c9_2(X0,X1)
| c6_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1448,negated_conjecture,
~ ssSkC24 ).
cnf(u1452,negated_conjecture,
( ~ c9_2(X0,a1063)
| c9_2(X0,X1)
| c6_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1456,negated_conjecture,
( ~ c6_1(X0)
| c9_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1465,negated_conjecture,
c5_1(a1043) ).
cnf(u1469,negated_conjecture,
~ c8_1(a1043) ).
cnf(u1474,negated_conjecture,
~ ndr1_1(a1043) ).
cnf(u1505,negated_conjecture,
( ~ ndr1_1(X0)
| c9_1(X0)
| c6_2(X0,a1176)
| c7_2(X0,X1)
| c4_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u1527,negated_conjecture,
~ ndr1_1(a962) ).
cnf(u1533,negated_conjecture,
ssSkC0 ).
cnf(u1543,negated_conjecture,
~ ndr1_1(a977) ).
cnf(u1549,negated_conjecture,
ssSkC5 ).
cnf(u1555,negated_conjecture,
~ ndr1_1(a995) ).
cnf(u1561,negated_conjecture,
ssSkC7 ).
cnf(u1573,negated_conjecture,
( ~ c1_1(X0)
| c3_1(X0) ) ).
cnf(u1577,negated_conjecture,
ndr1_1(a1008) ).
cnf(u1581,negated_conjecture,
( ~ c4_2(a1008,X0)
| c10_2(a1008,X0)
| c7_2(a1008,X0) ) ).
cnf(u1602,negated_conjecture,
~ ndr1_1(a1123) ).
cnf(u1608,negated_conjecture,
ssSkC37 ).
cnf(u1646,negated_conjecture,
ndr1_1(a1031) ).
cnf(u1650,negated_conjecture,
( ~ c2_2(a1031,X0)
| c4_2(a1031,X0)
| ~ c6_2(a1031,X0) ) ).
cnf(u1653,negated_conjecture,
ssSkC16 ).
cnf(u1663,negated_conjecture,
~ ndr1_1(a1046) ).
cnf(u1677,negated_conjecture,
ssSkC20 ).
cnf(u1691,negated_conjecture,
~ ndr1_1(a1095) ).
cnf(u1705,negated_conjecture,
ssSkC48 ).
cnf(u1711,negated_conjecture,
ssSkC35 ).
cnf(u1722,negated_conjecture,
~ ssSkC39 ).
cnf(u1726,negated_conjecture,
ndr1_1(a1131) ).
cnf(u1730,negated_conjecture,
( ~ c1_2(a1131,X0)
| c4_2(a1131,X0)
| ~ c3_2(a1131,X0) ) ).
cnf(u1739,negated_conjecture,
( ~ c2_1(X0)
| c2_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1751,negated_conjecture,
( ~ c1_2(X0,a1021)
| c8_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1755,negated_conjecture,
( ~ c9_2(X0,a1021)
| c8_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1760,negated_conjecture,
~ ndr1_1(a1024) ).
cnf(u1763,negated_conjecture,
( ~ c7_2(a1024,X0)
| c4_2(a1024,X0)
| c3_2(a1024,X0) ) ).
cnf(u1767,negated_conjecture,
~ ssSkC15 ).
cnf(u1772,negated_conjecture,
~ ndr1_1(a1033) ).
cnf(u1775,negated_conjecture,
( ~ c4_2(a1033,X0)
| c2_2(a1033,X0)
| c7_2(a1033,X0) ) ).
cnf(u1784,negated_conjecture,
~ ndr1_1(a1078) ).
cnf(u1790,negated_conjecture,
ssSkC27 ).
cnf(u1815,negated_conjecture,
( ~ c1_1(X0)
| c4_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1830,negated_conjecture,
ssSkC44 ).
cnf(u1836,negated_conjecture,
~ ndr1_1(a1170) ).
cnf(u1839,negated_conjecture,
( ~ c6_2(a1170,X0)
| c10_2(a1170,X0)
| c8_2(a1170,X0) ) ).
cnf(u1852,negated_conjecture,
ssSkC3 ).
cnf(u1871,negated_conjecture,
ndr1_1(a1022) ).
cnf(u1875,negated_conjecture,
( ~ c2_2(a1022,X0)
| c8_2(a1022,X0)
| c10_2(a1022,X0) ) ).
cnf(u1896,negated_conjecture,
ssSkC23 ).
cnf(u1907,negated_conjecture,
~ ssSkC41 ).
cnf(u1912,negated_conjecture,
~ ndr1_1(a1139) ).
cnf(u1928,negated_conjecture,
ssSkC45 ).
cnf(u1940,negated_conjecture,
~ ndr1_1(a973) ).
cnf(u1947,negated_conjecture,
ndr1_1(a1020) ).
cnf(u1951,negated_conjecture,
( ~ c1_2(a1020,X0)
| ~ c2_2(a1020,X0) ) ).
cnf(u1954,negated_conjecture,
ssSkC14 ).
cnf(u1960,negated_conjecture,
~ c6_2(a1106,a1107) ).
cnf(u1963,negated_conjecture,
( ~ c8_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1968,negated_conjecture,
~ c8_2(a1106,a1108) ).
cnf(u1973,negated_conjecture,
~ c3_2(a1106,a1108) ).
cnf(u1978,negated_conjecture,
~ c10_2(a1106,a1108) ).
cnf(u1990,negated_conjecture,
( ~ c5_2(X0,a969)
| c9_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1997,negated_conjecture,
ssSkC4 ).
cnf(u2006,negated_conjecture,
( ~ c2_2(X0,a979)
| c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2010,negated_conjecture,
( ~ c5_2(X0,a979)
| c2_1(X0)
| ~ c3_1(X0) ) ).
cnf(u2014,negated_conjecture,
( ~ c4_2(X0,a983)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2018,negated_conjecture,
( ~ c2_2(X0,a983)
| c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2022,negated_conjecture,
( ~ c10_1(X0)
| c8_1(X0)
| c5_2(X0,a1021) ) ).
cnf(u2027,negated_conjecture,
~ c3_1(a1041) ).
cnf(u2040,negated_conjecture,
~ c7_2(a1092,a1093) ).
cnf(u2046,negated_conjecture,
ssSkC30 ).
cnf(u2052,negated_conjecture,
~ c10_2(a1092,a1093) ).
cnf(u2057,negated_conjecture,
~ c4_2(a1092,a1093) ).
cnf(u2062,negated_conjecture,
~ c3_2(a1092,a1094) ).
cnf(u2067,negated_conjecture,
~ c5_2(a1092,a1094) ).
cnf(u2086,negated_conjecture,
~ c2_1(a1124) ).
cnf(u2093,negated_conjecture,
ndr1_1(a1130) ).
cnf(u2110,negated_conjecture,
( c4_2(a1131,X0)
| c3_2(a1131,X0)
| c6_2(a1131,X0) ) ).
cnf(u2122,negated_conjecture,
~ ndr1_1(a1146) ).
cnf(u2131,negated_conjecture,
c9_2(a1106,a1107) ).
cnf(u2136,negated_conjecture,
c4_2(a1106,a1107) ).
cnf(u2160,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| c7_2(X0,a979) ) ).
cnf(u2168,negated_conjecture,
( ~ c8_2(X0,a989)
| ~ c6_1(X0)
| ~ ssSkP0(X0) ) ).
cnf(u2172,negated_conjecture,
( ~ c6_2(X0,a989)
| ~ c6_1(X0)
| ~ ssSkP0(X0) ) ).
cnf(u2176,negated_conjecture,
( ~ c10_1(X0)
| c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u2189,negated_conjecture,
~ c10_1(a1092) ).
cnf(u2194,negated_conjecture,
c10_2(a1092,a1094) ).
cnf(u2218,negated_conjecture,
~ c7_1(a1124) ).
cnf(u2251,negated_conjecture,
~ ssSkC32 ).
cnf(u2255,negated_conjecture,
( ~ c2_2(X0,a1104)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2259,negated_conjecture,
( ~ c3_2(X0,a1104)
| c3_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2264,negated_conjecture,
ssSkC34 ).
cnf(u2267,negated_conjecture,
( ~ c9_2(X0,a1112)
| ~ c6_1(X0)
| ~ ssSkP4(X0) ) ).
cnf(u2271,negated_conjecture,
~ ssSkC42 ).
cnf(u2275,negated_conjecture,
( ~ c4_2(X0,a1142)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2279,negated_conjecture,
( ~ c8_2(X0,a1142)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2283,negated_conjecture,
( ~ c1_2(X0,a1142)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2287,negated_conjecture,
~ ssSkC50 ).
cnf(u2291,negated_conjecture,
( ~ c4_2(X0,a1178)
| ~ c1_1(X0)
| ~ ssSkP9(X0) ) ).
cnf(u2307,negated_conjecture,
~ ndr1_1(a1106) ).
cnf(u2312,negated_conjecture,
( ~ c7_1(X0)
| c10_1(X0)
| c3_1(X0) ) ).
cnf(u2316,negated_conjecture,
( ~ c3_1(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u2324,negated_conjecture,
( ~ c3_1(X0)
| c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u2328,negated_conjecture,
( ~ c2_1(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u2332,negated_conjecture,
( ~ ssSkP0(X0)
| c9_2(X0,a989)
| ~ c6_1(X0) ) ).
cnf(u2353,negated_conjecture,
ndr1_1(a1092) ).
cnf(u2357,negated_conjecture,
( ~ c4_2(X0,a1152)
| ~ c1_1(X0)
| ~ ssSkP6(X0) ) ).
cnf(u2361,negated_conjecture,
( ~ c10_2(X0,a1152)
| ~ c1_1(X0)
| ~ ssSkP6(X0) ) ).
cnf(u2385,negated_conjecture,
( ~ c6_2(X0,a976)
| c7_1(X0)
| c2_1(X0) ) ).
cnf(u2389,negated_conjecture,
( ~ c1_2(X0,a976)
| c7_1(X0)
| c2_1(X0) ) ).
cnf(u2394,negated_conjecture,
ssSkC12 ).
cnf(u2397,negated_conjecture,
( ~ c2_2(X0,a1012)
| c4_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u2405,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| c9_2(X0,a1104) ) ).
cnf(u2409,negated_conjecture,
( ~ ssSkP4(X0)
| c5_2(X0,a1112)
| ~ c6_1(X0) ) ).
cnf(u2413,negated_conjecture,
( ~ ssSkP4(X0)
| c7_2(X0,a1112)
| ~ c6_1(X0) ) ).
cnf(u2417,negated_conjecture,
( ~ c2_2(X0,a1122)
| c8_1(X0)
| c10_1(X0) ) ).
cnf(u2421,negated_conjecture,
( ~ c9_2(X0,a1122)
| c8_1(X0)
| c10_1(X0) ) ).
cnf(u2437,negated_conjecture,
( ~ c1_1(X0)
| c1_2(X0,a1178)
| ~ ssSkP9(X0) ) ).
cnf(u2441,negated_conjecture,
( ~ c1_1(X0)
| c2_2(X0,a1178)
| ~ ssSkP9(X0) ) ).
cnf(u2448,negated_conjecture,
ndr1_1(a980) ).
cnf(u2461,negated_conjecture,
( ~ ssSkP0(X0)
| ndr1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u2477,negated_conjecture,
( ~ c8_2(X0,a1105)
| c3_1(X0)
| c6_1(X0) ) ).
cnf(u2481,negated_conjecture,
( ~ c5_2(X0,a1105)
| c3_1(X0)
| c6_1(X0) ) ).
cnf(u2490,negated_conjecture,
( ~ c1_1(X0)
| c8_2(X0,a1152)
| ~ ssSkP6(X0) ) ).
cnf(u2534,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u2546,negated_conjecture,
( ~ c2_1(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u2554,negated_conjecture,
( ~ ssSkP9(X0)
| ndr1_1(X0)
| ~ c1_1(X0) ) ).
cnf(u2558,negated_conjecture,
( ~ c7_1(X0)
| c1_2(X0,a1113) ) ).
cnf(u2561,negated_conjecture,
ssSkC33 ).
cnf(u2566,negated_conjecture,
( ~ c7_1(X0)
| c3_2(X0,a1113) ) ).
cnf(u2570,negated_conjecture,
( ~ c7_1(X0)
| c6_2(X0,a1113) ) ).
cnf(u2602,negated_conjecture,
( ~ ssSkP6(X0)
| ndr1_1(X0)
| ~ c1_1(X0) ) ).
cnf(u2641,negated_conjecture,
~ c2_2(a1008,a1010) ).
cnf(u2646,negated_conjecture,
~ c6_2(a1008,a1010) ).
cnf(u2651,negated_conjecture,
~ c1_2(a1008,a1010) ).
cnf(u2670,negated_conjecture,
( ~ c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u2695,negated_conjecture,
c8_2(a1008,a1009) ).
cnf(u2700,negated_conjecture,
c3_2(a1008,a1009) ).
cnf(u2715,negated_conjecture,
~ c5_2(a1068,a1069) ).
cnf(u2718,negated_conjecture,
ssSkC25 ).
cnf(u2724,negated_conjecture,
~ c2_2(a1068,a1069) ).
cnf(u2729,negated_conjecture,
~ c2_2(a1068,a1070) ).
cnf(u2749,negated_conjecture,
~ c10_2(a1125,a1126) ).
cnf(u2754,negated_conjecture,
~ c3_2(a1125,a1126) ).
cnf(u2759,negated_conjecture,
~ c1_2(a1125,a1127) ).
cnf(u2764,negated_conjecture,
~ c6_2(a1133,a1134) ).
cnf(u2769,negated_conjecture,
~ c2_2(a1133,a1134) ).
cnf(u2784,negated_conjecture,
~ c1_2(a1144,a1145) ).
cnf(u2794,negated_conjecture,
~ c3_2(a1162,a1163) ).
cnf(u2799,negated_conjecture,
~ c10_2(a1162,a1163) ).
cnf(u2804,negated_conjecture,
~ c8_2(a1162,a1163) ).
cnf(u2809,negated_conjecture,
~ c5_2(a1162,a1164) ).
cnf(u2831,negated_conjecture,
ssSkC1 ).
cnf(u2837,negated_conjecture,
~ c1_1(a973) ).
cnf(u2842,negated_conjecture,
~ c1_1(a977) ).
cnf(u2846,negated_conjecture,
c4_2(a980,a981) ).
cnf(u2858,negated_conjecture,
~ c7_2(a1015,a1016) ).
cnf(u2861,negated_conjecture,
ssSkC13 ).
cnf(u2867,negated_conjecture,
~ c1_2(a1015,a1017) ).
cnf(u2872,negated_conjecture,
~ c7_2(a1031,a1032) ).
cnf(u2877,negated_conjecture,
~ c8_2(a1031,a1032) ).
cnf(u2907,negated_conjecture,
~ c3_1(a1068) ).
cnf(u2912,negated_conjecture,
c1_2(a1068,a1070) ).
cnf(u2917,negated_conjecture,
c8_2(a1068,a1070) ).
cnf(u2958,negated_conjecture,
~ c4_1(a1125) ).
cnf(u2963,negated_conjecture,
c8_2(a1125,a1126) ).
cnf(u2967,negated_conjecture,
~ c4_2(a1125,a1127) ).
cnf(u2973,negated_conjecture,
c5_2(a1125,a1127) ).
cnf(u2978,negated_conjecture,
~ c2_1(a1133) ).
cnf(u2983,negated_conjecture,
c5_2(a1133,a1134) ).
cnf(u2988,negated_conjecture,
~ c6_2(a1136,a1137) ).
cnf(u2991,negated_conjecture,
ssSkC40 ).
cnf(u2997,negated_conjecture,
~ c3_2(a1136,a1137) ).
cnf(u3007,negated_conjecture,
~ c10_1(a1144) ).
cnf(u3012,negated_conjecture,
~ c5_1(a1144) ).
cnf(u3017,negated_conjecture,
c3_2(a1144,a1145) ).
cnf(u3022,negated_conjecture,
c4_2(a1144,a1145) ).
cnf(u3042,negated_conjecture,
~ c6_1(a1162) ).
cnf(u3047,negated_conjecture,
c8_2(a1162,a1164) ).
cnf(u3052,negated_conjecture,
c4_2(a1162,a1164) ).
cnf(u3057,negated_conjecture,
~ c3_2(a1167,a1168) ).
cnf(u3060,negated_conjecture,
ssSkC47 ).
cnf(u3066,negated_conjecture,
~ c7_2(a1167,a1168) ).
cnf(u3071,negated_conjecture,
~ c10_2(a1167,a1168) ).
cnf(u3076,negated_conjecture,
~ c9_2(a1170,a1171) ).
cnf(u3121,negated_conjecture,
ssSkC10 ).
cnf(u3150,negated_conjecture,
~ c4_2(a1022,a1023) ).
cnf(u3155,negated_conjecture,
~ c8_2(a1022,a1023) ).
cnf(u3160,negated_conjecture,
~ c3_2(a1022,a1023) ).
cnf(u3250,negated_conjecture,
ssSkC36 ).
cnf(u3264,negated_conjecture,
~ c4_2(a1131,a1132) ).
cnf(u3307,negated_conjecture,
c9_1(a973) ).
cnf(u3312,negated_conjecture,
c9_1(a977) ).
cnf(u3322,negated_conjecture,
~ c7_1(a980) ).
cnf(u3327,negated_conjecture,
c5_2(a980,a981) ).
cnf(u3332,negated_conjecture,
c6_2(a980,a981) ).
cnf(u3338,negated_conjecture,
c3_2(a1015,a1016) ).
cnf(u3343,negated_conjecture,
c3_2(a1015,a1017) ).
cnf(u3348,negated_conjecture,
c9_2(a1015,a1017) ).
cnf(u3353,negated_conjecture,
c9_1(a1020) ).
cnf(u3358,negated_conjecture,
c3_1(a1020) ).
cnf(u3363,negated_conjecture,
~ c4_1(a1024) ).
cnf(u3367,negated_conjecture,
c8_1(a1024) ).
cnf(u3373,negated_conjecture,
c6_2(a1031,a1032) ).
cnf(u3378,negated_conjecture,
~ c7_1(a1033) ).
cnf(u3383,negated_conjecture,
c8_2(a1033,a1034) ).
cnf(u3388,negated_conjecture,
c5_2(a1033,a1034) ).
cnf(u3393,negated_conjecture,
c10_2(a1033,a1034) ).
cnf(u3398,negated_conjecture,
~ c9_1(a1046) ).
cnf(u3408,negated_conjecture,
~ ssSkC22 ).
cnf(u3412,negated_conjecture,
~ ndr1_1(a1068) ).
cnf(u3423,negated_conjecture,
~ c9_1(a1095) ).
cnf(u3433,negated_conjecture,
~ c1_1(a1120) ).
cnf(u3438,negated_conjecture,
c9_2(a1120,a1121) ).
cnf(u3443,negated_conjecture,
c1_2(a1120,a1121) ).
cnf(u3448,negated_conjecture,
c2_2(a1120,a1121) ).
cnf(u3453,negated_conjecture,
c5_1(a1123) ).
cnf(u3458,negated_conjecture,
ndr1_1(a1125) ).
cnf(u3463,negated_conjecture,
~ c8_1(a1130) ).
cnf(u3468,negated_conjecture,
~ c10_1(a1130) ).
cnf(u3472,negated_conjecture,
~ c7_1(a1133) ).
cnf(u3478,negated_conjecture,
ndr1_1(a1133) ).
cnf(u3483,negated_conjecture,
~ c9_1(a1136) ).
cnf(u3488,negated_conjecture,
c1_2(a1136,a1137) ).
cnf(u3507,negated_conjecture,
~ ndr1_1(a1144) ).
cnf(u3519,negated_conjecture,
ndr1_1(a1162) ).
cnf(u3524,negated_conjecture,
~ c7_1(a1167) ).
cnf(u3529,negated_conjecture,
c10_2(a1170,a1171) ).
cnf(u3534,negated_conjecture,
c6_2(a1170,a1171) ).
cnf(u3545,negated_conjecture,
~ c6_2(a1186,a1187) ).
cnf(u3550,negated_conjecture,
~ c1_2(a1186,a1188) ).
cnf(u3575,negated_conjecture,
~ c7_1(a991) ).
cnf(u3580,negated_conjecture,
~ c1_1(a991) ).
cnf(u3585,negated_conjecture,
~ c3_1(a991) ).
cnf(u3620,negated_conjecture,
ssSkC11 ).
cnf(u3654,negated_conjecture,
~ c9_1(a1022) ).
cnf(u3699,negated_conjecture,
~ c5_1(a1058) ).
cnf(u3704,negated_conjecture,
~ c10_1(a1058) ).
cnf(u3709,negated_conjecture,
~ c1_1(a1058) ).
cnf(u3724,negated_conjecture,
~ c5_1(a1062) ).
cnf(u3784,negated_conjecture,
c2_2(a1131,a1132) ).
cnf(u3794,negated_conjecture,
~ c10_1(a1139) ).
cnf(u3799,negated_conjecture,
~ c1_1(a1139) ).
cnf(u3804,negated_conjecture,
~ c1_1(a1146) ).
cnf(u3809,negated_conjecture,
~ c2_1(a1146) ).
cnf(u3854,negated_conjecture,
c10_1(a1007) ).
cnf(u3859,negated_conjecture,
ndr1_1(a1015) ).
cnf(u3901,negated_conjecture,
~ c10_1(a1078) ).
cnf(u3908,negated_conjecture,
c4_1(a1120) ).
cnf(u3913,negated_conjecture,
ndr1_1(a1120) ).
cnf(u3921,negated_conjecture,
c1_1(a1136) ).
cnf(u3926,negated_conjecture,
ndr1_1(a1136) ).
cnf(u3944,negated_conjecture,
ndr1_1(a1167) ).
cnf(u3948,negated_conjecture,
~ c2_1(a1170) ).
cnf(u3955,negated_conjecture,
c3_2(a1186,a1187) ).
cnf(u3960,negated_conjecture,
c3_2(a1186,a1188) ).
cnf(u4055,negated_conjecture,
c10_1(a1062) ).
cnf(u4162,negated_conjecture,
c3_1(a1186) ).
cnf(u4167,negated_conjecture,
ndr1_1(a1186) ).
cnf(u4229,negated_conjecture,
~ c6_1(a1133) ).
cnf(u4247,negated_conjecture,
c8_1(a1007) ).
cnf(u4271,negated_conjecture,
~ ndr1_1(a991) ).
cnf(u4317,negated_conjecture,
c10_1(a1098) ).
cnf(u4344,negated_conjecture,
~ c10_1(a1186) ).
cnf(u4415,negated_conjecture,
~ c2_1(a1106) ).
cnf(u4440,negated_conjecture,
~ c6_1(a1125) ).
cnf(u4460,negated_conjecture,
~ c9_2(a1120,a1084) ).
cnf(u4464,negated_conjecture,
~ c2_1(a1120) ).
cnf(u4467,negated_conjecture,
~ c6_2(a1120,a1121) ).
cnf(u4477,negated_conjecture,
~ c2_1(a1068) ).
cnf(u4502,negated_conjecture,
~ c2_1(a1043) ).
cnf(u4532,negated_conjecture,
~ c2_1(a1125) ).
cnf(u4535,negated_conjecture,
~ c8_2(a1125,a1127) ).
cnf(u4545,negated_conjecture,
~ c1_1(a1144) ).
cnf(u4595,negated_conjecture,
~ c7_1(a1170) ).
cnf(u4603,negated_conjecture,
~ c10_1(a1170) ).
cnf(u4636,negated_conjecture,
~ c3_2(a980,a981) ).
cnf(u4648,negated_conjecture,
~ c6_1(a1033) ).
cnf(u4664,negated_conjecture,
~ c9_2(a1033,a1034) ).
cnf(u4717,negated_conjecture,
c2_1(a980) ).
cnf(u4722,negated_conjecture,
c3_1(a980) ).
cnf(u4752,negated_conjecture,
c10_2(a1170,a983) ).
cnf(u4789,negated_conjecture,
~ c3_1(a1162) ).
cnf(u4816,negated_conjecture,
c9_2(a991,a989) ).
cnf(u4827,negated_conjecture,
c5_2(a991,a1112) ).
cnf(u4914,negated_conjecture,
~ c5_1(a1008) ).
cnf(u4928,negated_conjecture,
~ c5_1(a1125) ).
cnf(u4941,negated_conjecture,
~ c5_1(a1162) ).
cnf(u4949,negated_conjecture,
c10_1(a1162) ).
cnf(u4954,negated_conjecture,
~ c5_1(a1033) ).
cnf(u4959,negated_conjecture,
~ c5_1(a1068) ).
cnf(u4962,negated_conjecture,
~ c10_1(a1068) ).
cnf(u4977,negated_conjecture,
c8_1(a1120) ).
cnf(u4987,negated_conjecture,
~ c8_1(a1068) ).
cnf(u5016,negated_conjecture,
~ c1_2(a980,a981) ).
cnf(u5023,negated_conjecture,
~ c10_1(a980) ).
cnf(u5029,negated_conjecture,
~ c1_2(a1033,a1034) ).
cnf(u5034,negated_conjecture,
~ c1_2(a1133,a1134) ).
cnf(u5091,negated_conjecture,
c8_1(a1162) ).
cnf(u5095,negated_conjecture,
~ ndr1_1(a1007) ).
cnf(u5101,negated_conjecture,
ndr1_1(a1062) ).
cnf(u5105,negated_conjecture,
c8_1(a1062) ).
cnf(u5133,negated_conjecture,
~ ssSkP6(a1136) ).
cnf(u5142,negated_conjecture,
~ c5_1(a1136) ).
cnf(u5183,negated_conjecture,
~ c2_1(a1136) ).
cnf(u5316,negated_conjecture,
~ c6_1(a1068) ).
cnf(u5343,negated_conjecture,
c7_2(a1020,a979) ).
cnf(u5357,negated_conjecture,
c2_1(a1186) ).
cnf(u5388,negated_conjecture,
~ c7_1(a1186) ).
cnf(u5404,negated_conjecture,
c3_2(a1020,a979) ).
cnf(u5413,negated_conjecture,
~ c6_1(a1020) ).
cnf(u5427,negated_conjecture,
~ c3_2(a1136,a979) ).
cnf(u5454,negated_conjecture,
~ c2_1(a1131) ).
cnf(u5457,negated_conjecture,
~ c1_1(a1131) ).
cnf(u5470,negated_conjecture,
~ c5_1(a1131) ).
cnf(u5507,negated_conjecture,
c3_2(a1131,a1132) ).
cnf(u5516,negated_conjecture,
c8_1(a1131) ).
cnf(u5555,negated_conjecture,
c7_2(a980,a981) ).
cnf(u5564,negated_conjecture,
c9_2(a1031,a1032) ).
cnf(u5637,negated_conjecture,
~ c6_2(a1020,a979) ).
cnf(u5654,negated_conjecture,
~ c6_2(a1136,a979) ).
cnf(u5682,negated_conjecture,
~ c8_2(a980,a981) ).
cnf(u5742,negated_conjecture,
~ c8_2(a1068,a1021) ).
cnf(u5760,negated_conjecture,
~ c8_2(a1133,a1134) ).
cnf(u5764,negated_conjecture,
~ c8_2(a1133,a1039) ).
cnf(u5783,negated_conjecture,
~ c8_2(a1033,a1039) ).
cnf(u5787,negated_conjecture,
c4_2(a1033,a1034) ).
cnf(u5801,negated_conjecture,
~ c4_2(a1120,a1102) ).
cnf(u5808,negated_conjecture,
~ c3_1(a1120) ).
cnf(u5833,negated_conjecture,
c9_1(a1133) ).
cnf(u5840,negated_conjecture,
~ c9_2(a1033,a1159) ).
cnf(u5843,negated_conjecture,
~ c9_1(a1033) ).
cnf(u5866,negated_conjecture,
c7_2(a1033,a1034) ).
cnf(u5886,negated_conjecture,
c8_2(a1120,a1102) ).
cnf(u5893,negated_conjecture,
~ c5_1(a1120) ).
cnf(u5912,negated_conjecture,
~ c9_2(a1136,a1049) ).
cnf(u5925,negated_conjecture,
~ c9_2(a1020,a1049) ).
cnf(u5939,negated_conjecture,
~ c9_2(a980,a1049) ).
cnf(u5954,negated_conjecture,
~ c10_2(a1136,a1049) ).
cnf(u5959,negated_conjecture,
~ c10_2(a1020,a1049) ).
cnf(u5965,negated_conjecture,
~ c10_2(a980,a1049) ).
cnf(u6002,negated_conjecture,
~ ssSkP11(a1131) ).
cnf(u6023,negated_conjecture,
~ ssSkP11(a1008) ).
cnf(u6041,negated_conjecture,
~ ssSkP11(a1162) ).
cnf(u6045,negated_conjecture,
~ c9_2(a1162,a1182) ).
cnf(u6054,negated_conjecture,
~ ssSkP11(a1120) ).
cnf(u6058,negated_conjecture,
~ c9_2(a1120,a1182) ).
cnf(u6071,negated_conjecture,
~ ssSkP11(a1125) ).
cnf(u6075,negated_conjecture,
~ c9_2(a1125,a1182) ).
cnf(u6097,negated_conjecture,
c8_2(a1136,a1049) ).
cnf(u6119,negated_conjecture,
~ ssSkP5(a1020) ).
cnf(u6150,negated_conjecture,
~ ssSkP11(a1136) ).
cnf(u6383,negated_conjecture,
c9_1(a1031) ).
cnf(u6388,negated_conjecture,
( c7_2(a1120,X0)
| c3_2(a1120,X0)
| c4_2(a1120,X0) ) ).
cnf(u6395,negated_conjecture,
~ c9_1(a1120) ).
cnf(u6409,negated_conjecture,
c9_1(a1167) ).
cnf(u6422,negated_conjecture,
c9_1(a1062) ).
cnf(u6434,negated_conjecture,
c9_1(a1131) ).
cnf(u6486,negated_conjecture,
c7_2(a1022,a1176) ).
cnf(u6493,negated_conjecture,
~ ssSkP9(a1136) ).
cnf(u6536,negated_conjecture,
c6_2(a1098,a1176) ).
cnf(u6542,negated_conjecture,
c6_2(a1043,a1176) ).
cnf(u6547,negated_conjecture,
c6_2(a1124,a1176) ).
cnf(u6552,negated_conjecture,
c6_2(a1092,a1176) ).
cnf(u6557,negated_conjecture,
c6_2(a1008,a1176) ).
cnf(u6563,negated_conjecture,
c6_2(a1068,a1176) ).
cnf(u6568,negated_conjecture,
c6_2(a1125,a1176) ).
cnf(u6573,negated_conjecture,
c6_2(a1130,a1176) ).
cnf(u6583,negated_conjecture,
c6_2(a1162,a1176) ).
cnf(u6588,negated_conjecture,
c6_2(a980,a1176) ).
cnf(u6598,negated_conjecture,
c6_2(a1015,a1176) ).
cnf(u6631,negated_conjecture,
c6_2(a1186,a1176) ).
cnf(u6646,negated_conjecture,
c6_2(a1033,a1176) ).
cnf(u6651,negated_conjecture,
c6_2(a1136,a1176) ).
cnf(u6656,negated_conjecture,
c6_2(a1022,a1176) ).
cnf(u6668,negated_conjecture,
c7_1(a1098) ).
cnf(u6710,negated_conjecture,
c9_2(a1124,a1176) ).
cnf(u6717,negated_conjecture,
c9_2(a1092,a1176) ).
cnf(u6720,negated_conjecture,
~ c7_1(a1092) ).
cnf(u6741,negated_conjecture,
c9_2(a1008,a1176) ).
cnf(u6771,negated_conjecture,
c9_2(a1125,a1176) ).
cnf(u6774,negated_conjecture,
~ c7_1(a1125) ).
cnf(u6791,negated_conjecture,
c9_2(a1130,a1176) ).
cnf(u6798,negated_conjecture,
~ c3_1(a1130) ).
cnf(u6823,negated_conjecture,
c7_1(a1162) ).
cnf(u6865,negated_conjecture,
c9_2(a1015,a1176) ).
cnf(u6927,negated_conjecture,
~ c3_2(a1022,a1176) ).
cnf(u6932,negated_conjecture,
c8_2(a1022,a1049) ).
cnf(u6941,negated_conjecture,
~ c10_2(a1022,a1049) ).
cnf(u6946,negated_conjecture,
~ c9_2(a1022,a1049) ).
cnf(u6992,negated_conjecture,
~ c5_1(a1022) ).
cnf(u6997,negated_conjecture,
c4_1(a1022) ).
cnf(u7019,negated_conjecture,
~ ssSkP11(a1022) ).
cnf(u7054,negated_conjecture,
~ c2_2(a1098,a1113) ).
cnf(u7087,negated_conjecture,
~ c2_2(a1162,a1113) ).
cnf(u7131,negated_conjecture,
c3_2(a1120,a1128) ).
cnf(u7144,negated_conjecture,
( c4_2(a1120,X0)
| c3_2(a1120,X0) ) ).
cnf(u7166,negated_conjecture,
~ c6_1(a1120) ).
cnf(u7244,negated_conjecture,
~ c4_2(a1136,a1151) ).
cnf(u7260,negated_conjecture,
~ c4_2(a1120,a1121) ).
cnf(u7264,negated_conjecture,
~ c4_2(a1120,a965) ).
cnf(u7541,negated_conjecture,
~ c9_2(a1136,a1151) ).
cnf(u7553,negated_conjecture,
~ c9_2(a1131,a1132) ).
cnf(u5533,negated_conjecture,
~ c3_1(a1131) ).
cnf(clause112,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u7172,negated_conjecture,
c3_2(a1120,a1102) ).
cnf(u6160,negated_conjecture,
c3_2(a1136,a1181) ).
cnf(u5349,negated_conjecture,
c7_2(a1136,a979) ).
cnf(u6499,negated_conjecture,
c6_2(a1136,a1177) ).
cnf(clause336,negated_conjecture,
( ~ c1_2(X0,a1011)
| ssSkP1(X0) ) ).
cnf(u6161,negated_conjecture,
c9_2(a1136,a1181) ).
cnf(u4286,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,a1112)
| ndr1_1(X0) ) ).
cnf(u4285,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,a1112)
| c10_2(X0,a1111) ) ).
cnf(u6195,negated_conjecture,
c3_2(a1120,a1181) ).
cnf(clause87,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u4202,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0) ) ).
cnf(u6081,negated_conjecture,
c3_2(a1008,a1181) ).
cnf(clause226,negated_conjecture,
( ssSkP0(X0)
| c10_2(X0,a988) ) ).
cnf(clause67,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(clause191,negated_conjecture,
( ssSkP2(X0)
| c8_2(X0,a1076) ) ).
cnf(u4287,negated_conjecture,
( ~ c6_1(X0)
| c7_2(X0,a1112)
| c9_2(X0,a1111) ) ).
cnf(clause343,negated_conjecture,
( ~ c5_2(X0,a988)
| ssSkP0(X0) ) ).
cnf(clause299,negated_conjecture,
( ~ c9_2(X0,a1156)
| ssSkP7(X0) ) ).
cnf(clause301,negated_conjecture,
( ~ c5_2(X0,a1151)
| ssSkP6(X0) ) ).
cnf(u6673,negated_conjecture,
c3_2(a1098,a1113) ).
cnf(clause295,negated_conjecture,
( ~ c1_2(X0,a1179)
| ssSkP10(X0) ) ).
cnf(u6501,negated_conjecture,
c9_2(a1136,a1177) ).
cnf(clause171,negated_conjecture,
( ssSkP7(X0)
| c6_2(X0,a1156) ) ).
cnf(u6192,negated_conjecture,
c3_2(a1125,a1181) ).
cnf(clause173,negated_conjecture,
( ssSkP6(X0)
| c2_2(X0,a1151) ) ).
cnf(clause160,negated_conjecture,
( ssSkP11(X0)
| c9_2(X0,a1181) ) ).
cnf(u6193,negated_conjecture,
c9_2(a1125,a1181) ).
cnf(clause314,negated_conjecture,
( ~ c6_2(X0,a1076)
| ssSkP2(X0) ) ).
cnf(u4281,negated_conjecture,
( ~ c6_1(X0)
| c9_2(X0,a989)
| c1_2(X0,a988) ) ).
cnf(u4284,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,a1112)
| c9_2(X0,a1111) ) ).
cnf(u6828,negated_conjecture,
c3_2(a1162,a1113) ).
cnf(u6189,negated_conjecture,
c3_2(a1162,a1181) ).
cnf(u6196,negated_conjecture,
c9_2(a1120,a1181) ).
cnf(u7280,negated_conjecture,
c3_2(a1120,a1121) ).
cnf(clause313,negated_conjecture,
( ~ c9_2(X0,a1076)
| ssSkP2(X0) ) ).
cnf(u4334,negated_conjecture,
~ c3_1(a1098) ).
cnf(clause75,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u4333,negated_conjecture,
( ~ c4_2(X0,X1)
| c7_2(X0,X1)
| c8_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ).
cnf(u7069,negated_conjecture,
~ c8_2(a1098,a1113) ).
cnf(u5194,negated_conjecture,
~ c3_1(a1007) ).
cnf(u6008,negated_conjecture,
c9_2(a1131,a1181) ).
cnf(u5129,negated_conjecture,
c3_1(a1136) ).
cnf(u4288,negated_conjecture,
( ~ c6_1(X0)
| c7_2(X0,a1112)
| c10_2(X0,a1111) ) ).
cnf(u7269,negated_conjecture,
c3_2(a1120,a965) ).
cnf(u4283,negated_conjecture,
( ~ c6_1(X0)
| c9_2(X0,a989)
| ndr1_1(X0) ) ).
cnf(clause84,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause227,negated_conjecture,
( ssSkP0(X0)
| c1_2(X0,a988) ) ).
cnf(clause71,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u6190,negated_conjecture,
c9_2(a1162,a1181) ).
cnf(clause188,negated_conjecture,
( ssSkP3(X0)
| c3_2(X0,a1085) ) ).
cnf(clause337,negated_conjecture,
( ~ c7_2(X0,a1011)
| ssSkP1(X0) ) ).
cnf(clause182,negated_conjecture,
( ssSkP4(X0)
| c10_2(X0,a1111) ) ).
cnf(clause309,negated_conjecture,
( ~ c3_2(X0,a1111)
| ssSkP4(X0) ) ).
cnf(clause303,negated_conjecture,
( ~ c7_2(X0,a1128)
| ssSkP5(X0) ) ).
cnf(u4204,negated_conjecture,
( ~ c1_1(X0)
| ndr1_1(X0) ) ).
cnf(clause162,negated_conjecture,
( ssSkP10(X0)
| c8_2(X0,a1179) ) ).
cnf(clause161,negated_conjecture,
( ssSkP11(X0)
| c3_2(X0,a1181) ) ).
cnf(clause164,negated_conjecture,
( ssSkP9(X0)
| c8_2(X0,a1177) ) ).
cnf(u6827,negated_conjecture,
c6_2(a1162,a1113) ).
cnf(u5116,negated_conjecture,
( ~ c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u7035,negated_conjecture,
c9_2(a1022,a1181) ).
cnf(u4335,negated_conjecture,
~ c3_1(a1024) ).
cnf(u5300,negated_conjecture,
~ c3_1(a1062) ).
cnf(clause304,negated_conjecture,
( ~ c10_2(X0,a1128)
| ssSkP5(X0) ) ).
cnf(u7034,negated_conjecture,
c3_2(a1022,a1181) ).
cnf(clause66,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(clause298,negated_conjecture,
( ~ c10_2(X0,a1156)
| ssSkP7(X0) ) ).
cnf(clause68,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(clause300,negated_conjecture,
( ~ c3_2(X0,a1151)
| ssSkP6(X0) ) ).
cnf(u4282,negated_conjecture,
( ~ c6_1(X0)
| c9_2(X0,a989)
| c10_2(X0,a988) ) ).
cnf(clause294,negated_conjecture,
( ~ c2_2(X0,a1179)
| ssSkP10(X0) ) ).
cnf(clause89,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u4586,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0) ) ).
cnf(u4585,negated_conjecture,
( ~ c6_1(X0)
| c5_2(X0,X1)
| ~ c3_1(X0)
| c9_2(X0,X1) ) ).
cnf(clause72,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause79,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u6007,negated_conjecture,
c3_2(a1131,a1181) ).
cnf(u7102,negated_conjecture,
~ c8_2(a1162,a1113) ).
cnf(clause311,negated_conjecture,
( ~ c2_2(X0,a1085)
| ssSkP3(X0) ) ).
cnf(clause297,negated_conjecture,
( ~ c10_2(X0,a1157)
| ssSkP8(X0) ) ).
cnf(clause293,negated_conjecture,
( ~ c1_2(X0,a1181)
| ssSkP11(X0) ) ).
cnf(u6674,negated_conjecture,
c1_2(a1098,a1113) ).
cnf(u6082,negated_conjecture,
c9_2(a1008,a1181) ).
cnf(u5167,negated_conjecture,
c2_2(a1136,a1151) ).
cnf(u6829,negated_conjecture,
c1_2(a1162,a1113) ).
cnf(clause183,negated_conjecture,
( ssSkP4(X0)
| c9_2(X0,a1111) ) ).
cnf(clause213,negated_conjecture,
( ssSkP1(X0)
| c3_2(X0,a1011) ) ).
cnf(clause170,negated_conjecture,
( ssSkP8(X0)
| c6_2(X0,a1157) ) ).
cnf(clause169,negated_conjecture,
( ssSkP8(X0)
| c4_2(X0,a1157) ) ).
cnf(clause163,negated_conjecture,
( ssSkP9(X0)
| c9_2(X0,a1177) ) ).
cnf(u6672,negated_conjecture,
c6_2(a1098,a1113) ).
cnf(u4289,negated_conjecture,
( ~ c6_1(X0)
| c7_2(X0,a1112)
| ndr1_1(X0) ) ).
cnf(clause165,negated_conjecture,
( ssSkP9(X0)
| c6_2(X0,a1177) ) ).
cnf(clause312,negated_conjecture,
( ~ c9_2(X0,a1085)
| ssSkP3(X0) ) ).
cnf(clause104,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u6500,negated_conjecture,
c8_2(a1136,a1177) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN424-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n026.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Mon Sep 28 15:58:42 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 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
% 4.02/1.24 % (3978703)Input is clausal, will run a generic CNF schedule.
% 4.02/1.24 % (3978712)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4209946070:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.02/1.24 % (3978712)Instruction limit reached!
% 4.02/1.24 % (3978712)------------------------------
% 4.02/1.24 % (3978712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.24 % (3978712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.24 % (3978712)CaDiCaL version: 2.1.3
% 4.02/1.24 % (3978712)Termination reason: Instruction limit
% 4.02/1.24 % (3978712)Termination phase: Saturation
% 4.02/1.24 % (3978712)Time elapsed: 0.036 s
% 4.02/1.24 % (3978712)Peak memory usage: 91 MB
% 4.02/1.24 % (3978712)Instructions burned: 114 (million)
% 4.02/1.24 % (3978709)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1560807374:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.02/1.24 % (3978710)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4225979361:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.02/1.24 % (3978711)lrs+10_1_sil=8000:sp=occurrence:random_seed=4155708960:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.02/1.24 % (3978708)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=998300480:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.02/1.24 % (3978713)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=658289375:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.02/1.24 % (3978714)dis-21_1_sil=8000:lcm=predicate:random_seed=3832103190: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)
% 4.02/1.24 % (3978713)Refutation not found, incomplete strategy
% 4.02/1.24 % (3978713)------------------------------
% 4.02/1.24 % (3978713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.24 % (3978713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.24 % (3978713)CaDiCaL version: 2.1.3
% 4.02/1.24 % (3978713)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.24 % (3978713)Time elapsed: 0.038 s
% 4.02/1.24 % (3978713)Peak memory usage: 91 MB
% 4.02/1.24 % (3978713)Instructions burned: 63 (million)
% 4.02/1.24 % (3978711)Instruction limit reached!
% 4.02/1.24 % (3978711)------------------------------
% 4.02/1.24 % (3978711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.24 % (3978711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.24 % (3978711)CaDiCaL version: 2.1.3
% 4.02/1.24 % (3978711)Termination reason: Instruction limit
% 4.02/1.24 % (3978711)Termination phase: Saturation
% 4.02/1.24 % (3978711)Time elapsed: 0.064 s
% 4.02/1.24 % (3978711)Peak memory usage: 91 MB
% 4.02/1.24 % (3978711)Instructions burned: 108 (million)
% 4.02/1.24 % (3978714)Instruction limit reached!
% 4.02/1.24 % (3978714)------------------------------
% 4.02/1.24 % (3978714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.24 % (3978714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.24 % (3978714)CaDiCaL version: 2.1.3
% 4.02/1.24 % (3978714)Termination reason: Instruction limit
% 4.02/1.24 % (3978714)Termination phase: Saturation
% 4.02/1.24 % (3978714)Time elapsed: 0.067 s
% 4.02/1.24 % (3978714)Peak memory usage: 91 MB
% 4.02/1.24 % (3978714)Instructions burned: 118 (million)
% 4.02/1.24 % (3978717)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=2141343741:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 4.02/1.24 % (3978717)Instruction limit reached!
% 4.02/1.24 % (3978717)------------------------------
% 4.02/1.24 % (3978717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.24 % (3978717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.24 % (3978717)CaDiCaL version: 2.1.3
% 4.02/1.24 % (3978717)Termination reason: Instruction limit
% 4.02/1.24 % (3978717)Termination phase: Saturation
% 4.02/1.24 % (3978717)Time elapsed: 0.044 s
% 4.02/1.24 % (3978717)Peak memory usage: 91 MB
% 4.02/1.24 % (3978717)Instructions burned: 145 (million)
% 4.02/1.24 % (3978723)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=37982226: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)
% 4.02/1.24 % (3978726)lrs+10_64_to=lpo:sil=8000:random_seed=2865525281:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.02/1.24 % (3978725)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3773254567:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.02/1.24 % (3978726)First to succeed.
% 4.02/1.24 % (3978726)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3978703"
% 4.02/1.24 % (3978723)Refutation not found, incomplete strategy
% 4.02/1.24 % (3978723)------------------------------
% 4.02/1.24 % (3978723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.24 % (3978723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.24 % (3978723)CaDiCaL version: 2.1.3
% 4.02/1.24 % (3978723)Termination reason: Refutation not found, incomplete strategy
% 4.02/1.24 % (3978723)Time elapsed: 0.052 s
% 4.02/1.24 % (3978723)Peak memory usage: 91 MB
% 4.02/1.24 % (3978723)Instructions burned: 91 (million)
% 4.02/1.24 % (3978713)------------------------------
% 4.02/1.24 % (3978713)------------------------------
% 4.02/1.24 % (3978725)Instruction limit reached!
% 4.02/1.24 % (3978725)------------------------------
% 4.02/1.24 % (3978725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.24 % (3978725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.24 % (3978725)CaDiCaL version: 2.1.3
% 4.02/1.24 % (3978725)Termination reason: Instruction limit
% 4.02/1.24 % (3978725)Termination phase: Saturation
% 4.02/1.24 % (3978725)Time elapsed: 0.124 s
% 4.02/1.24 % (3978725)Peak memory usage: 93 MB
% 4.02/1.24 % (3978725)Instructions burned: 219 (million)
% 4.02/1.24 % SZS status Satisfiable for theBenchmark
% 4.02/1.24 % SZS output start Saturation.
% See solution above
% 4.56/1.44 % SZS output start Definitions and Model Updates.
% 4.56/1.44 % SZS output end Definitions and Model Updates.
% 4.56/1.44 % (3978726)------------------------------
% 4.56/1.44 % (3978726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.56/1.44 % (3978726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.56/1.44 % (3978726)CaDiCaL version: 2.1.3
% 4.56/1.44 % (3978726)Termination reason: Satisfiable
% 4.56/1.44 % (3978726)Time elapsed: 0.035 s
% 4.56/1.44 % (3978726)Peak memory usage: 92 MB
% 4.56/1.44 % (3978726)Instructions burned: 114 (million)
% 4.56/1.44 % (3978726)------------------------------
% 4.56/1.44 % (3978726)------------------------------
% 4.56/1.44 % (3978703)Success in time 0.571 s
% 4.56/1.44 % Vampire exiting
%------------------------------------------------------------------------------