%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN420-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:34 PM UTC 2026
% Result : Satisfiable 3.08s 0.98s
% Output : Saturation 4.41s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u608,negated_conjecture,
~ c3_0 ).
cnf(u612,negated_conjecture,
( ~ c8_2(X2,X4)
| c4_1(X2)
| c7_2(X2,X4)
| ~ c2_2(X2,X4)
| ~ c5_2(X2,X3)
| ~ ndr1_1(X2)
| ~ c9_2(X2,X3)
| ~ c6_2(X2,X3) ) ).
cnf(u615,negated_conjecture,
ndr1_0 ).
cnf(u623,negated_conjecture,
~ c2_0 ).
cnf(u627,negated_conjecture,
( ~ c2_2(X2,X3)
| c1_2(X2,X3)
| c8_2(X2,X3)
| c3_2(X2,X4)
| c4_2(X2,X4)
| c10_2(X2,X4)
| ~ c9_1(X2)
| ~ ndr1_1(X2) ) ).
cnf(u638,negated_conjecture,
( ~ c8_2(X2,X3)
| c5_2(X2,X3)
| ~ c10_1(X2)
| ~ c9_1(X2)
| ~ ndr1_1(X2)
| ~ c4_2(X2,X3) ) ).
cnf(u659,negated_conjecture,
( c9_2(X2,X3)
| c5_2(X2,X3)
| c3_2(X2,X3)
| ~ ndr1_1(X2)
| ~ c3_1(X2)
| ~ c1_1(X2) ) ).
cnf(u702,negated_conjecture,
c5_0 ).
cnf(u726,negated_conjecture,
~ c1_0 ).
cnf(u730,negated_conjecture,
( ~ c3_2(X2,X3)
| ~ c4_1(X2)
| ~ c10_1(X2)
| ~ ndr1_1(X2)
| ~ c2_2(X2,X3)
| ~ c10_2(X2,X3) ) ).
cnf(u738,negated_conjecture,
c8_0 ).
cnf(u753,negated_conjecture,
c9_0 ).
cnf(u800,negated_conjecture,
( ~ c3_2(X0,X1)
| c6_1(X0)
| c5_2(X0,X2)
| c4_2(X0,X2)
| c1_2(X0,X1)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u803,negated_conjecture,
ssSkC19 ).
cnf(u813,negated_conjecture,
c6_0 ).
cnf(u817,negated_conjecture,
( ~ c7_2(X0,X1)
| c9_2(X0,X2)
| c2_2(X0,X2)
| c2_2(X0,X1)
| c10_2(X0,X1)
| ~ c8_1(X0)
| ~ c5_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u832,negated_conjecture,
( ~ c4_2(X0,X1)
| c9_1(X0)
| c8_2(X0,X3)
| c1_2(X0,X3)
| c5_2(X0,X3)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u835,negated_conjecture,
ssSkC14 ).
cnf(u844,negated_conjecture,
( ~ c8_2(X0,X1)
| c10_1(X0)
| c7_2(X0,X2)
| c3_2(X0,X2)
| c5_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u847,negated_conjecture,
ssSkC16 ).
cnf(u870,negated_conjecture,
( ~ c10_2(X0,X1)
| c1_1(X0)
| c4_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u875,negated_conjecture,
~ c4_0 ).
cnf(u921,negated_conjecture,
( ~ c4_2(X0,X1)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u942,negated_conjecture,
( ~ c10_2(X0,X1)
| c1_2(X0,X2)
| c6_2(X0,X1)
| ~ c4_1(X0)
| ~ c9_2(X0,X2)
| ~ c6_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u972,negated_conjecture,
( ~ c4_2(X1,X2)
| c6_2(X1,X2)
| c1_2(X1,X2)
| ~ c6_1(X1)
| ~ c9_1(X1)
| ~ ndr1_1(X1) ) ).
cnf(u983,negated_conjecture,
( ~ c8_2(X0,X1)
| c9_2(X0,X1)
| ~ c4_1(X0)
| ~ c1_1(X0)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u986,negated_conjecture,
ssSkC4 ).
cnf(u1000,negated_conjecture,
( ~ c2_2(X1,X2)
| c1_1(X1)
| c3_1(X1)
| c3_2(X1,X2)
| c5_2(X1,X2)
| ~ ndr1_1(X1) ) ).
cnf(u1043,negated_conjecture,
( ~ c5_2(X0,X1)
| c6_2(X0,X1)
| c1_2(X0,X1)
| ~ c9_1(X0)
| ~ c1_2(X0,a419)
| ~ ndr1_1(X0) ) ).
cnf(u1047,negated_conjecture,
( ~ c5_2(X0,a419)
| c6_2(X0,X1)
| c1_2(X0,X1)
| ~ c9_1(X0)
| ~ c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1054,negated_conjecture,
( ~ ndr1_1(X0)
| c5_1(X0)
| c2_1(X0)
| c10_2(X0,X2)
| c7_2(X0,X2)
| c2_2(X0,X2) ) ).
cnf(u1057,negated_conjecture,
ssSkC18 ).
cnf(u1076,negated_conjecture,
c7_0 ).
cnf(u1080,negated_conjecture,
( ~ c5_2(X0,a316)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1084,negated_conjecture,
( ~ c3_2(X0,a316)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1103,negated_conjecture,
( ~ c7_2(X0,a400)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1106,negated_conjecture,
ssSkC25 ).
cnf(u1111,negated_conjecture,
( ~ c8_2(X0,a400)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_1(X0)
| ~ c7_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1115,negated_conjecture,
( ~ ssSkP7(X0)
| c10_2(X0,X1)
| ~ c10_2(X0,a447)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1141,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,a316)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1145,negated_conjecture,
( ~ c7_2(X0,X1)
| c2_2(X0,a400)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1149,negated_conjecture,
( ~ ssSkP7(X0)
| c3_2(X0,a447)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1153,negated_conjecture,
( ~ ssSkP7(X0)
| c7_2(X0,a447)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u1157,negated_conjecture,
~ ssSkC30 ).
cnf(u1161,negated_conjecture,
( ~ c10_2(X0,X1)
| c4_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_1(X0)
| ~ c2_2(X0,a411)
| ~ ndr1_1(X0) ) ).
cnf(u1165,negated_conjecture,
( ~ c10_2(X0,X1)
| c4_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_1(X0)
| ~ c7_2(X0,a411)
| ~ ndr1_1(X0) ) ).
cnf(u1169,negated_conjecture,
( ~ c2_2(X0,X1)
| c9_1(X0)
| c3_1(X0)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u1173,negated_conjecture,
( ~ c10_2(X0,X1)
| c3_2(X0,a411)
| c4_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1177,negated_conjecture,
~ ssSkC34 ).
cnf(u1181,negated_conjecture,
( ~ c2_2(X0,X1)
| c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c8_2(X0,a428)
| ~ ndr1_1(X0) ) ).
cnf(u1185,negated_conjecture,
( ~ c2_2(X0,X1)
| c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c1_2(X0,a428)
| ~ ndr1_1(X0) ) ).
cnf(u1189,negated_conjecture,
( ~ c2_2(X0,X1)
| c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c10_2(X0,a428)
| ~ ndr1_1(X0) ) ).
cnf(u1193,negated_conjecture,
c10_0 ).
cnf(u1211,negated_conjecture,
( ~ c4_2(X0,a276)
| c6_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1223,negated_conjecture,
( ~ c2_1(X1)
| c3_1(X1)
| ~ c10_1(X1) ) ).
cnf(u1234,negated_conjecture,
( ~ ndr1_1(X0)
| c6_1(X0)
| c2_2(X0,a276)
| c5_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(u1238,negated_conjecture,
ndr1_1(a381) ).
cnf(u1242,negated_conjecture,
( ~ c9_2(a381,X0)
| c8_2(a381,X0)
| ~ c10_2(a381,X0) ) ).
cnf(u1246,negated_conjecture,
( ~ c4_1(X1)
| c7_1(X1)
| ~ c1_1(X1) ) ).
cnf(u1249,negated_conjecture,
ssSkC1 ).
cnf(u1261,negated_conjecture,
ndr1_1(a278) ).
cnf(u1265,negated_conjecture,
( ~ c2_2(a278,X0)
| c4_2(a278,X0)
| ~ c7_2(a278,X0) ) ).
cnf(u1269,negated_conjecture,
ndr1_1(a325) ).
cnf(u1273,negated_conjecture,
( ~ c2_2(a325,X0)
| c4_2(a325,X0)
| ~ c6_2(a325,X0) ) ).
cnf(u1276,negated_conjecture,
ssSkC9 ).
cnf(u1288,negated_conjecture,
ssSkC31 ).
cnf(u1294,negated_conjecture,
ssSkC7 ).
cnf(u1306,negated_conjecture,
ssSkC27 ).
cnf(u1321,negated_conjecture,
ndr1_1(a277) ).
cnf(u1325,negated_conjecture,
( ~ c3_2(a277,X0)
| c10_2(a277,X0)
| ~ c4_2(a277,X0) ) ).
cnf(u1341,negated_conjecture,
ndr1_1(a329) ).
cnf(u1345,negated_conjecture,
( ~ c3_2(a329,X0)
| c2_2(a329,X0)
| ~ c7_2(a329,X0) ) ).
cnf(u1349,negated_conjecture,
ndr1_1(a384) ).
cnf(u1353,negated_conjecture,
( ~ c5_2(a384,X0)
| c6_2(a384,X0)
| c2_2(a384,X0) ) ).
cnf(u1364,negated_conjecture,
ssSkC36 ).
cnf(u1385,negated_conjecture,
~ ssSkC0 ).
cnf(u1389,negated_conjecture,
ndr1_1(a281) ).
cnf(u1393,negated_conjecture,
( ~ c8_2(a281,X0)
| c1_2(a281,X0)
| ~ c2_2(a281,X0) ) ).
cnf(u1413,negated_conjecture,
ndr1_1(a362) ).
cnf(u1434,negated_conjecture,
ssSkC32 ).
cnf(u1446,negated_conjecture,
ssSkC33 ).
cnf(u1449,negated_conjecture,
ndr1_1(a427) ).
cnf(u1461,negated_conjecture,
~ ssSkC37 ).
cnf(u1465,negated_conjecture,
ndr1_1(a441) ).
cnf(u1469,negated_conjecture,
( ~ c8_2(a441,X0)
| c7_2(a441,X0)
| ~ c5_2(a441,X0) ) ).
cnf(u1474,negated_conjecture,
ssSkC38 ).
cnf(u1496,negated_conjecture,
( ~ c2_1(X0)
| c8_1(X0)
| c3_1(X0) ) ).
cnf(u1500,negated_conjecture,
( ~ c6_2(a277,X0)
| c7_2(a277,X0)
| c4_2(a277,X0) ) ).
cnf(u1524,negated_conjecture,
( c8_2(a384,X0)
| c3_2(a384,X0)
| c4_2(a384,X0) ) ).
cnf(u1528,negated_conjecture,
ndr1_1(a398) ).
cnf(u1532,negated_conjecture,
( ~ c3_2(a398,X0)
| c2_2(a398,X0)
| c1_2(a398,X0) ) ).
cnf(u1543,negated_conjecture,
ssSkC29 ).
cnf(u1548,negated_conjecture,
~ ssSkC28 ).
cnf(u1552,negated_conjecture,
ndr1_1(a443) ).
cnf(u1573,negated_conjecture,
ssSkC10 ).
cnf(u1584,negated_conjecture,
ndr1_1(a406) ).
cnf(u1588,negated_conjecture,
( ~ c2_2(a406,X0)
| c9_2(a406,X0)
| c1_2(a406,X0) ) ).
cnf(u1600,negated_conjecture,
( ~ c4_2(a441,X0)
| c2_2(a441,X0)
| c5_2(a441,X0) ) ).
cnf(u1622,negated_conjecture,
( ~ c1_2(X0,a328)
| c6_1(X0)
| c3_1(X0) ) ).
cnf(u1629,negated_conjecture,
ssSkC11 ).
cnf(u1637,negated_conjecture,
ssSkC12 ).
cnf(u1650,negated_conjecture,
( ~ c2_2(X0,a342)
| c9_1(X0)
| ~ c7_1(X0) ) ).
cnf(u1654,negated_conjecture,
~ ssSkC13 ).
cnf(u1661,negated_conjecture,
ssSkC21 ).
cnf(u1670,negated_conjecture,
ssSkC22 ).
cnf(u1674,negated_conjecture,
( ~ c1_2(X0,a390)
| ~ c6_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u1678,negated_conjecture,
( ~ c5_2(X0,a390)
| ~ c6_1(X0)
| ~ ssSkP3(X0) ) ).
cnf(u1690,negated_conjecture,
~ ssSkC26 ).
cnf(u1694,negated_conjecture,
( ~ c2_2(X0,a402)
| ~ c2_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1698,negated_conjecture,
( ~ c9_2(X0,a402)
| ~ c2_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1760,negated_conjecture,
( ~ c6_1(X0)
| c9_2(X0,a390)
| ~ ssSkP3(X0) ) ).
cnf(u1776,negated_conjecture,
( ~ c5_2(X0,a440)
| c10_1(X0)
| ~ c9_1(X0) ) ).
cnf(u1797,negated_conjecture,
( ~ c2_1(X0)
| c7_2(X0,a402)
| ~ c10_1(X0) ) ).
cnf(u1806,negated_conjecture,
ssSkC35 ).
cnf(u1809,negated_conjecture,
( ~ c10_2(X0,a430)
| c5_1(X0)
| ~ c4_1(X0) ) ).
cnf(u1825,negated_conjecture,
( ~ c2_1(X0)
| c8_1(X0) ) ).
cnf(u1851,negated_conjecture,
ssSkC8 ).
cnf(u1856,negated_conjecture,
ndr1_1(a332) ).
cnf(u1860,negated_conjecture,
( ~ c3_2(a332,X0)
| ~ c10_2(a332,X0) ) ).
cnf(u1881,negated_conjecture,
( ~ c3_2(X0,a299)
| c8_1(X0)
| c9_1(X0) ) ).
cnf(u1884,negated_conjecture,
ssSkC3 ).
cnf(u1889,negated_conjecture,
~ ssSkC2 ).
cnf(u1893,negated_conjecture,
( ~ c4_2(X0,a312)
| c7_1(X0)
| c3_1(X0) ) ).
cnf(u1896,negated_conjecture,
ssSkC6 ).
cnf(u1901,negated_conjecture,
~ ssSkC5 ).
cnf(u1905,negated_conjecture,
( c6_1(X0)
| ndr1_1(X0)
| c3_1(X0) ) ).
cnf(u1917,negated_conjecture,
( ~ c7_1(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u1925,negated_conjecture,
( ~ ssSkP3(X0)
| ndr1_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1937,negated_conjecture,
( ~ c9_1(X0)
| c10_1(X0)
| c6_2(X0,a440) ) ).
cnf(u1941,negated_conjecture,
( ~ c9_1(X0)
| c10_1(X0)
| c1_2(X0,a440) ) ).
cnf(u1954,negated_conjecture,
ssSkC15 ).
cnf(u1969,negated_conjecture,
~ ssSkC23 ).
cnf(u1973,negated_conjecture,
( ~ c3_2(X0,a393)
| ~ ssSkP4(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1977,negated_conjecture,
( ~ c8_2(X0,a393)
| ~ ssSkP4(X0)
| ~ ssSkP5(X0) ) ).
cnf(u1985,negated_conjecture,
( ~ c2_1(X0)
| ndr1_1(X0)
| ~ c10_1(X0) ) ).
cnf(u2005,negated_conjecture,
ndr1_1(a272) ).
cnf(u2009,negated_conjecture,
( ~ c6_2(a272,X0)
| c1_2(a272,X0) ) ).
cnf(u2060,negated_conjecture,
( c7_1(X0)
| c5_2(X0,a312)
| c3_1(X0) ) ).
cnf(u2065,negated_conjecture,
( ~ c9_1(X0)
| c10_1(X0)
| ndr1_1(X0) ) ).
cnf(u2077,negated_conjecture,
( ~ ssSkP4(X0)
| c6_2(X0,a393)
| ~ ssSkP5(X0) ) ).
cnf(u2093,negated_conjecture,
( ~ c4_1(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u2102,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0)
| c9_1(X0) ) ).
cnf(u2106,negated_conjecture,
( c7_1(X0)
| ndr1_1(X0)
| c3_1(X0) ) ).
cnf(u2111,negated_conjecture,
~ c4_1(a431) ).
cnf(u2122,negated_conjecture,
( ~ ssSkP4(X0)
| ndr1_1(X0)
| ~ ssSkP5(X0) ) ).
cnf(u2139,negated_conjecture,
c5_2(a381,a382) ).
cnf(u2145,negated_conjecture,
~ c2_2(a381,a382) ).
cnf(u2150,negated_conjecture,
~ c3_2(a420,a421) ).
cnf(u2167,negated_conjecture,
c6_1(a431) ).
cnf(u2172,negated_conjecture,
c2_1(a431) ).
cnf(u2176,negated_conjecture,
( c7_1(X0)
| c4_1(X0) ) ).
cnf(u2206,negated_conjecture,
~ c4_2(a325,a326) ).
cnf(u2211,negated_conjecture,
c8_2(a381,a382) ).
cnf(u2216,negated_conjecture,
~ c6_2(a384,a385) ).
cnf(u2221,negated_conjecture,
~ c5_2(a384,a385) ).
cnf(u2231,negated_conjecture,
~ c8_1(a420) ).
cnf(u2236,negated_conjecture,
c10_2(a420,a421) ).
cnf(u2241,negated_conjecture,
c7_2(a420,a421) ).
cnf(u2280,negated_conjecture,
~ c4_1(a278) ).
cnf(u2285,negated_conjecture,
c8_2(a278,a279) ).
cnf(u2290,negated_conjecture,
c3_2(a278,a279) ).
cnf(u2295,negated_conjecture,
c4_2(a278,a279) ).
cnf(u2321,negated_conjecture,
~ c1_1(a325) ).
cnf(u2326,negated_conjecture,
c7_2(a325,a326) ).
cnf(u2331,negated_conjecture,
c5_2(a325,a326) ).
cnf(u2356,negated_conjecture,
c1_1(a381) ).
cnf(u2362,negated_conjecture,
c9_2(a384,a385) ).
cnf(u2397,negated_conjecture,
c7_1(a420) ).
cnf(u2402,negated_conjecture,
ndr1_1(a420) ).
cnf(u2432,negated_conjecture,
~ c4_2(a297,a298) ).
cnf(u2437,negated_conjecture,
~ c5_2(a297,a298) ).
cnf(u2447,negated_conjecture,
~ c7_2(a308,a309) ).
cnf(u2502,negated_conjecture,
~ c7_2(a339,a340) ).
cnf(u2507,negated_conjecture,
~ c3_2(a339,a340) ).
cnf(u2512,negated_conjecture,
~ c5_2(a339,a341) ).
cnf(u2517,negated_conjecture,
~ c9_2(a339,a341) ).
cnf(u2537,negated_conjecture,
ssSkC20 ).
cnf(u2598,negated_conjecture,
~ c4_2(a272,a273) ).
cnf(u2603,negated_conjecture,
~ c2_2(a272,a273) ).
cnf(u2608,negated_conjecture,
~ c5_1(a277) ).
cnf(u2651,negated_conjecture,
~ c3_2(a348,a349) ).
cnf(u2674,negated_conjecture,
ssSkC17 ).
cnf(u2690,negated_conjecture,
ssSkC24 ).
cnf(u2768,negated_conjecture,
c6_1(a445) ).
cnf(u2773,negated_conjecture,
c1_1(a445) ).
cnf(u2783,negated_conjecture,
~ c10_1(a281) ).
cnf(u2793,negated_conjecture,
~ c7_1(a296) ).
cnf(u2798,negated_conjecture,
~ c4_1(a297) ).
cnf(u2802,negated_conjecture,
c7_1(a297) ).
cnf(u2808,negated_conjecture,
c8_2(a297,a298) ).
cnf(u2828,negated_conjecture,
~ c10_1(a308) ).
cnf(u2833,negated_conjecture,
~ c5_1(a308) ).
cnf(u2838,negated_conjecture,
c1_2(a308,a309) ).
cnf(u2843,negated_conjecture,
c8_2(a308,a309) ).
cnf(u2913,negated_conjecture,
~ c6_1(a339) ).
cnf(u2918,negated_conjecture,
c9_2(a339,a340) ).
cnf(u2923,negated_conjecture,
c4_2(a339,a341) ).
cnf(u2948,negated_conjecture,
~ c5_1(a360) ).
cnf(u2953,negated_conjecture,
~ c6_1(a360) ).
cnf(u2957,negated_conjecture,
c7_1(a360) ).
cnf(u2963,negated_conjecture,
~ c10_1(a362) ).
cnf(u3008,negated_conjecture,
~ c3_1(a406) ).
cnf(u3027,negated_conjecture,
c7_1(a427) ).
cnf(u3051,negated_conjecture,
c1_2(a272,a273) ).
cnf(u3074,negated_conjecture,
c3_1(a329) ).
cnf(u3079,negated_conjecture,
c1_1(a329) ).
cnf(u3084,negated_conjecture,
~ c10_1(a332) ).
cnf(u3089,negated_conjecture,
~ c6_1(a332) ).
cnf(u3104,negated_conjecture,
~ c6_1(a348) ).
cnf(u3109,negated_conjecture,
c7_2(a348,a349) ).
cnf(u3114,negated_conjecture,
c6_2(a348,a349) ).
cnf(u3175,negated_conjecture,
c7_1(a398) ).
cnf(u3180,negated_conjecture,
c8_1(a398) ).
cnf(u3210,negated_conjecture,
c10_1(a296) ).
cnf(u3215,negated_conjecture,
c6_1(a296) ).
cnf(u3220,negated_conjecture,
ndr1_1(a297) ).
cnf(u3226,negated_conjecture,
ndr1_1(a308) ).
cnf(u3253,negated_conjecture,
ndr1_1(a339) ).
cnf(u3328,negated_conjecture,
c5_1(a272) ).
cnf(u3341,negated_conjecture,
ndr1_1(a348) ).
cnf(u3452,negated_conjecture,
~ c3_1(a360) ).
cnf(u3470,negated_conjecture,
~ c3_1(a348) ).
cnf(u3525,negated_conjecture,
~ c9_1(a420) ).
cnf(u3548,negated_conjecture,
~ ssSkP3(a445) ).
cnf(u3590,negated_conjecture,
~ ssSkP3(a431) ).
cnf(u3604,negated_conjecture,
~ c10_1(a431) ).
cnf(u3607,negated_conjecture,
~ c3_1(a431) ).
cnf(u3622,negated_conjecture,
~ ssSkP3(a296) ).
cnf(u3648,negated_conjecture,
~ c3_1(a296) ).
cnf(u3691,negated_conjecture,
c5_2(a296,a312) ).
cnf(u3702,negated_conjecture,
ssSkP7(a384) ).
cnf(u3719,negated_conjecture,
~ ssSkP4(a384) ).
cnf(u3732,negated_conjecture,
c4_2(a384,a274) ).
cnf(u3747,negated_conjecture,
~ c6_2(a431,a389) ).
cnf(u3753,negated_conjecture,
~ c3_1(a278) ).
cnf(u3760,negated_conjecture,
~ c6_2(a278,a279) ).
cnf(u3766,negated_conjecture,
~ c3_1(a384) ).
cnf(u3773,negated_conjecture,
~ c6_2(a384,a274) ).
cnf(u3779,negated_conjecture,
~ c3_1(a445) ).
cnf(u3786,negated_conjecture,
~ c6_2(a445,a389) ).
cnf(u3795,negated_conjecture,
~ c6_2(a296,a389) ).
cnf(u3801,negated_conjecture,
~ c3_1(a339) ).
cnf(u3808,negated_conjecture,
~ c6_2(a339,a341) ).
cnf(u3840,negated_conjecture,
c6_1(a420) ).
cnf(u3844,negated_conjecture,
( c3_2(a278,X0)
| c5_2(a278,X0) ) ).
cnf(u3864,negated_conjecture,
c6_1(a325) ).
cnf(u3884,negated_conjecture,
c2_2(a381,a276) ).
cnf(u3905,negated_conjecture,
c2_2(a348,a276) ).
cnf(u3912,negated_conjecture,
~ ssSkP3(a420) ).
cnf(u3923,negated_conjecture,
~ ssSkP3(a325) ).
cnf(u3939,negated_conjecture,
~ c3_1(a420) ).
cnf(u3946,negated_conjecture,
~ c6_2(a420,a389) ).
cnf(u3953,negated_conjecture,
~ c3_1(a325) ).
cnf(u3960,negated_conjecture,
~ c6_2(a325,a389) ).
cnf(u3969,negated_conjecture,
~ c9_1(a278) ).
cnf(u3974,negated_conjecture,
c8_1(a278) ).
cnf(u3987,negated_conjecture,
~ ssSkP4(a278) ).
cnf(u4025,negated_conjecture,
( c3_2(a360,X0)
| c5_2(a360,X0) ) ).
cnf(u4037,negated_conjecture,
c2_2(a332,a276) ).
cnf(u4045,negated_conjecture,
c2_2(a339,a276) ).
cnf(u4053,negated_conjecture,
c9_1(a360) ).
cnf(u4070,negated_conjecture,
~ ssSkP4(a360) ).
cnf(u4087,negated_conjecture,
c10_1(a360) ).
cnf(u4100,negated_conjecture,
( c10_2(a308,X0)
| c2_2(a308,X0)
| c7_2(a308,X0) ) ).
cnf(u4108,negated_conjecture,
( c10_2(a360,X0)
| c2_2(a360,X0)
| c7_2(a360,X0) ) ).
cnf(u4120,negated_conjecture,
c2_1(a277) ).
cnf(u4130,negated_conjecture,
~ c10_1(a277) ).
cnf(u4146,negated_conjecture,
~ c4_1(a308) ).
cnf(u4161,negated_conjecture,
~ c4_1(a360) ).
cnf(u4182,negated_conjecture,
( ~ c2_2(a384,X0)
| c1_2(a384,X0)
| c7_2(a384,X0) ) ).
cnf(u4194,negated_conjecture,
c7_2(a308,a428) ).
cnf(u4214,negated_conjecture,
c2_2(a360,a428) ).
cnf(u4217,negated_conjecture,
( ~ c2_2(a360,X0)
| c1_2(a360,X0)
| c7_2(a360,X0) ) ).
cnf(u4225,negated_conjecture,
~ ssSkP7(a360) ).
cnf(u4237,negated_conjecture,
~ ssSkP7(a278) ).
cnf(u4241,negated_conjecture,
~ c10_2(a278,a447) ).
cnf(u4284,negated_conjecture,
~ c4_2(a381,a382) ).
cnf(u4288,negated_conjecture,
~ c9_1(a381) ).
cnf(u4292,negated_conjecture,
~ c10_1(a381) ).
cnf(u4306,negated_conjecture,
~ c3_1(a381) ).
cnf(u4323,negated_conjecture,
c5_2(a329,a391) ).
cnf(u4335,negated_conjecture,
~ c10_1(a329) ).
cnf(u4356,negated_conjecture,
~ c2_1(a445) ).
cnf(u4388,negated_conjecture,
~ c1_2(a420,a421) ).
cnf(u4399,negated_conjecture,
~ c1_1(a420) ).
cnf(u4422,negated_conjecture,
~ c9_1(a384) ).
cnf(u4433,negated_conjecture,
~ c9_1(a431) ).
cnf(u4447,negated_conjecture,
~ c9_1(a325) ).
cnf(u4456,negated_conjecture,
~ c9_1(a445) ).
cnf(u4465,negated_conjecture,
~ c9_1(a296) ).
cnf(u4480,negated_conjecture,
~ c1_1(a384) ).
cnf(u4500,negated_conjecture,
c5_2(a332,a276) ).
cnf(u4514,negated_conjecture,
c5_2(a348,a276) ).
cnf(u4531,negated_conjecture,
c3_2(a339,a276) ).
cnf(u4534,negated_conjecture,
~ c1_1(a339) ).
cnf(u4544,negated_conjecture,
~ ssSkP7(a339) ).
cnf(u4577,negated_conjecture,
~ c4_1(a339) ).
cnf(u4596,negated_conjecture,
~ c7_2(a332,a276) ).
cnf(u4603,negated_conjecture,
~ c9_1(a332) ).
cnf(u4610,negated_conjecture,
~ c7_2(a348,a276) ).
cnf(u4617,negated_conjecture,
~ c9_1(a348) ).
cnf(u4623,negated_conjecture,
~ c7_2(a381,a276) ).
cnf(u4632,negated_conjecture,
~ c7_2(a339,a276) ).
cnf(u4639,negated_conjecture,
~ c9_1(a339) ).
cnf(u4664,negated_conjecture,
~ c9_1(a329) ).
cnf(u4690,negated_conjecture,
~ c1_2(a348,a419) ).
cnf(u4720,negated_conjecture,
~ c3_1(a272) ).
cnf(u4737,negated_conjecture,
~ c3_1(a308) ).
cnf(u4789,negated_conjecture,
~ c2_2(a278,a411) ).
cnf(u4793,negated_conjecture,
~ c1_1(a278) ).
cnf(u4806,negated_conjecture,
~ c2_2(a360,a411) ).
cnf(u4810,negated_conjecture,
~ c1_1(a360) ).
cnf(u4831,negated_conjecture,
~ c1_1(a308) ).
cnf(u4950,negated_conjecture,
~ c8_1(a325) ).
cnf(u4975,negated_conjecture,
~ c8_1(a445) ).
cnf(u4991,negated_conjecture,
~ c8_1(a329) ).
cnf(u5007,negated_conjecture,
~ c8_1(a296) ).
cnf(u5035,negated_conjecture,
c9_2(a431,a389) ).
cnf(u5054,negated_conjecture,
( ~ c5_2(a384,X1)
| ~ c6_2(a384,X1)
| ~ c9_2(a384,X1) ) ).
cnf(u5067,negated_conjecture,
~ c2_2(a278,a279) ).
cnf(u5075,negated_conjecture,
~ c2_2(a297,a298) ).
cnf(u5088,negated_conjecture,
~ c2_2(a308,a309) ).
cnf(u5134,negated_conjecture,
c1_2(a360,a428) ).
cnf(u5152,negated_conjecture,
( ~ c6_2(a278,X1)
| c5_2(a278,X1)
| c1_2(a278,X1) ) ).
cnf(u5160,negated_conjecture,
~ c6_2(a339,a276) ).
cnf(u5167,negated_conjecture,
( ~ c6_2(a360,X1)
| c5_2(a360,X1)
| c1_2(a360,X1) ) ).
cnf(u5193,negated_conjecture,
c10_1(a384) ).
cnf(u5200,negated_conjecture,
~ c5_2(a278,a279) ).
cnf(u5204,negated_conjecture,
( ~ c1_2(a278,X0)
| c7_2(a278,X0)
| c3_2(a278,X0) ) ).
cnf(u5209,negated_conjecture,
c6_2(a297,a298) ).
cnf(u5224,negated_conjecture,
( ~ c1_2(a308,X0)
| c7_2(a308,X0)
| c3_2(a308,X0) ) ).
cnf(u5240,negated_conjecture,
~ c4_1(a381) ).
cnf(u5252,negated_conjecture,
~ c8_1(a381) ).
cnf(u5278,negated_conjecture,
c7_2(a278,a446) ).
cnf(u5290,negated_conjecture,
ssSkP7(a308) ).
cnf(u5295,negated_conjecture,
~ c4_2(a308,a309) ).
cnf(u3616,negated_conjecture,
c4_1(a296) ).
cnf(u3479,negated_conjecture,
( ~ c9_2(X0,X2)
| c1_2(X0,X2)
| c6_2(X0,X1)
| ~ c4_1(X0)
| ~ c10_2(X0,X1)
| ~ c6_2(X0,X2) ) ).
cnf(clause286,negated_conjecture,
( ~ c3_2(X0,a274)
| ssSkP0(X0) ) ).
cnf(clause135,negated_conjecture,
( ssSkP7(X0)
| c1_2(X0,a446) ) ).
cnf(clause252,negated_conjecture,
( ~ c1_2(X0,a391)
| ssSkP4(X0) ) ).
cnf(clause93,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(u4252,negated_conjecture,
c1_2(a360,a446) ).
cnf(u4265,negated_conjecture,
c1_2(a278,a446) ).
cnf(clause67,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause70,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u3408,negated_conjecture,
ndr1_1(X0) ).
cnf(u3635,negated_conjecture,
c4_2(a296,a389) ).
cnf(u3932,negated_conjecture,
c5_2(a325,a389) ).
cnf(u3480,negated_conjecture,
( ~ c3_2(X0,X1)
| c10_2(X0,X1)
| ~ c10_2(X0,a447)
| ~ c4_2(X0,X1)
| ~ ssSkP7(X0) ) ).
cnf(u4878,negated_conjecture,
( ~ c10_2(X0,X1)
| c6_2(X0,X1)
| ~ c4_1(X0)
| c1_2(X0,a390)
| ~ c6_2(X0,a390)
| c3_2(X0,X2)
| c5_2(X0,X2)
| c2_2(X0,a276)
| c4_2(X0,a389) ) ).
cnf(clause253,negated_conjecture,
( ~ c9_2(X0,a391)
| ssSkP4(X0) ) ).
cnf(u3426,negated_conjecture,
( ~ c10_2(X0,a428)
| c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u3425,negated_conjecture,
( ~ c1_2(X0,a428)
| c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u3406,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0) ) ).
cnf(clause54,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(u3929,negated_conjecture,
c5_2(a420,a389) ).
cnf(clause195,negated_conjecture,
( ssSkP1(X0)
| c6_2(X0,a285) ) ).
cnf(clause154,negated_conjecture,
( ssSkP2(X0)
| c6_2(X0,a379) ) ).
cnf(clause150,negated_conjecture,
( ssSkP5(X0)
| c1_2(X0,a392) ) ).
cnf(clause143,negated_conjecture,
( ssSkP6(X0)
| c3_2(X0,a412) ) ).
cnf(u4271,negated_conjecture,
( c9_2(X0,a390)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c2_2(X0,a276)
| c5_2(X0,a389) ) ).
cnf(u4579,negated_conjecture,
c1_2(a339,a446) ).
cnf(u3482,negated_conjecture,
( ~ c3_2(X0,X1)
| c7_2(X0,a447)
| c10_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ ssSkP7(X0) ) ).
cnf(u3628,negated_conjecture,
c5_2(a431,a389) ).
cnf(u3554,negated_conjecture,
c5_2(a445,a389) ).
cnf(u3600,negated_conjecture,
c8_1(a431) ).
cnf(u4302,negated_conjecture,
( ~ c1_1(X0)
| c3_2(X0,a402)
| c5_2(X0,a402)
| ~ c2_1(X0)
| ~ c10_1(X0) ) ).
cnf(u3555,negated_conjecture,
c4_2(a445,a389) ).
cnf(u5282,negated_conjecture,
c3_2(a308,a309) ).
cnf(clause251,negated_conjecture,
( ~ c6_2(X0,a392)
| ssSkP5(X0) ) ).
cnf(clause254,negated_conjecture,
( ~ c2_2(X0,a391)
| ssSkP4(X0) ) ).
cnf(u3477,negated_conjecture,
( ~ c5_2(X0,X2)
| c9_2(X0,X2)
| c2_2(X0,X2)
| c2_2(X0,X1)
| c10_2(X0,X1)
| ~ c8_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(clause248,negated_conjecture,
( ~ c4_2(X0,a412)
| ssSkP6(X0) ) ).
cnf(u4300,negated_conjecture,
( ~ c3_1(X0)
| c3_2(X0,a391)
| c5_2(X0,a391)
| ~ c1_1(X0)
| ssSkP4(X0) ) ).
cnf(u3634,negated_conjecture,
c5_2(a296,a389) ).
cnf(u3478,negated_conjecture,
( ~ c4_2(X0,X1)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c3_1(X0) ) ).
cnf(clause285,negated_conjecture,
( ~ c8_2(X0,a274)
| ssSkP0(X0) ) ).
cnf(u4017,negated_conjecture,
( ~ ssSkP3(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c9_2(X0,a390)
| c2_2(X0,a276) ) ).
cnf(u3423,negated_conjecture,
( c5_1(X0)
| c2_1(X0)
| c10_2(X0,X2)
| c7_2(X0,X2)
| c2_2(X0,X2) ) ).
cnf(u3481,negated_conjecture,
( ~ c3_2(X0,X1)
| c3_2(X0,a447)
| c10_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ ssSkP7(X0) ) ).
cnf(clause155,negated_conjecture,
( ssSkP2(X0)
| c7_2(X0,a379) ) ).
cnf(clause144,negated_conjecture,
( ssSkP6(X0)
| c5_2(X0,a412) ) ).
cnf(clause151,negated_conjecture,
( ssSkP3(X0)
| c4_2(X0,a389) ) ).
cnf(u4266,negated_conjecture,
c10_2(a278,a446) ).
cnf(u4880,negated_conjecture,
( ~ c10_2(X0,X2)
| c6_2(X0,X2)
| ~ c4_1(X0)
| c1_2(X0,X1)
| ~ c6_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ).
cnf(clause134,negated_conjecture,
( ssSkP7(X0)
| c10_2(X0,a446) ) ).
cnf(clause90,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u4126,negated_conjecture,
c8_1(a277) ).
cnf(clause194,negated_conjecture,
( ssSkP1(X0)
| c7_2(X0,a285) ) ).
cnf(clause255,negated_conjecture,
( ~ c2_2(X0,a389)
| ssSkP3(X0) ) ).
cnf(clause61,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause242,negated_conjecture,
( ~ c8_2(X0,a446)
| ssSkP7(X0) ) ).
cnf(u3633,negated_conjecture,
~ c1_1(a296) ).
cnf(u3424,negated_conjecture,
( ~ c8_2(X0,a428)
| c6_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(clause66,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause65,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u3875,negated_conjecture,
( c6_1(X0)
| c2_2(X0,a276)
| c5_2(X0,X1)
| c3_2(X0,X1) ) ).
cnf(clause250,negated_conjecture,
( ~ c2_2(X0,a392)
| ssSkP5(X0) ) ).
cnf(u3993,negated_conjecture,
ssSkP0(a278) ).
cnf(u3930,negated_conjecture,
c4_2(a420,a389) ).
cnf(clause256,negated_conjecture,
( ~ c4_2(X0,a379)
| ssSkP2(X0) ) ).
cnf(u4580,negated_conjecture,
c10_2(a339,a446) ).
cnf(u4253,negated_conjecture,
c10_2(a360,a446) ).
cnf(u4272,negated_conjecture,
( c9_2(X0,a390)
| c3_2(X0,X1)
| c5_2(X0,X1)
| c2_2(X0,a276)
| c4_2(X0,a389) ) ).
cnf(u4879,negated_conjecture,
( ~ c10_2(X0,X1)
| c6_2(X0,X1)
| ~ c4_1(X0)
| c1_2(X0,a390)
| ~ c6_2(X0,a390)
| c3_2(X0,X2)
| c5_2(X0,X2)
| c2_2(X0,a276)
| c5_2(X0,a389) ) ).
cnf(u3629,negated_conjecture,
c4_2(a431,a389) ).
cnf(clause196,negated_conjecture,
( ssSkP1(X0)
| c1_2(X0,a285) ) ).
cnf(clause152,negated_conjecture,
( ssSkP3(X0)
| c5_2(X0,a389) ) ).
cnf(clause287,negated_conjecture,
( ~ c5_2(X0,a274)
| ssSkP0(X0) ) ).
cnf(u4076,negated_conjecture,
ssSkP0(a360) ).
cnf(u3933,negated_conjecture,
c4_2(a325,a389) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN420-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.17 % Computer : n001.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Mon Sep 28 16:01:34 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 Running first-order theorem proving
% 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.08/0.98 % (457228)Input is clausal, will run a generic CNF schedule.
% 3.08/0.98 % (457238)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2008825000:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.08/0.98 % (457239)dis-21_1_sil=8000:lcm=predicate:random_seed=313266446: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)
% 3.08/0.98 % (457234)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4064262072:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.08/0.98 % (457236)lrs+10_1_sil=8000:sp=occurrence:random_seed=3319450858:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.08/0.98 % (457233)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=3593832174:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.08/0.98 % (457235)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=86105239:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.08/0.98 % (457237)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3247988807:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.08/0.98 % (457238)Refutation not found, incomplete strategy
% 3.08/0.98 % (457238)------------------------------
% 3.08/0.98 % (457238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/0.98 % (457238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.98 % (457238)CaDiCaL version: 2.1.3
% 3.08/0.98 % (457238)Termination reason: Refutation not found, incomplete strategy
% 3.08/0.98 % (457238)Time elapsed: 0.033 s
% 3.08/0.98 % (457238)Peak memory usage: 91 MB
% 3.08/0.98 % (457238)Instructions burned: 103 (million)
% 3.08/0.98 % (457239)Instruction limit reached!
% 3.08/0.98 % (457239)------------------------------
% 3.08/0.98 % (457239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/0.98 % (457239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.98 % (457239)CaDiCaL version: 2.1.3
% 3.08/0.98 % (457239)Termination reason: Instruction limit
% 3.08/0.98 % (457239)Termination phase: Saturation
% 3.08/0.98 % (457239)Time elapsed: 0.065 s
% 3.08/0.98 % (457239)Peak memory usage: 91 MB
% 3.08/0.98 % (457239)Instructions burned: 119 (million)
% 3.08/0.98 % (457236)Instruction limit reached!
% 3.08/0.98 % (457236)------------------------------
% 3.08/0.98 % (457236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/0.98 % (457236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.98 % (457236)CaDiCaL version: 2.1.3
% 3.08/0.98 % (457236)Termination reason: Instruction limit
% 3.08/0.98 % (457236)Termination phase: Saturation
% 3.08/0.98 % (457236)Time elapsed: 0.062 s
% 3.08/0.98 % (457236)Peak memory usage: 91 MB
% 3.08/0.98 % (457236)Instructions burned: 107 (million)
% 3.08/0.98 % (457237)Instruction limit reached!
% 3.08/0.98 % (457237)------------------------------
% 3.08/0.98 % (457237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/0.98 % (457237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.98 % (457237)CaDiCaL version: 2.1.3
% 3.08/0.98 % (457237)Termination reason: Instruction limit
% 3.08/0.98 % (457237)Termination phase: Saturation
% 3.08/0.98 % (457237)Time elapsed: 0.067 s
% 3.08/0.98 % (457237)Peak memory usage: 90 MB
% 3.08/0.98 % (457237)Instructions burned: 115 (million)
% 3.08/0.98 % (457238)------------------------------
% 3.08/0.98 % (457238)------------------------------
% 3.08/0.98 % (457247)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=1422311081:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.08/0.98 % (457249)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3463947072:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.08/0.98 % (457248)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2530908908: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)
% 3.08/0.98 % (457248)Refutation not found, incomplete strategy
% 3.08/0.98 % (457248)------------------------------
% 3.08/0.98 % (457248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/0.98 % (457248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.98 % (457248)CaDiCaL version: 2.1.3
% 3.08/0.98 % (457248)Termination reason: Refutation not found, incomplete strategy
% 3.08/0.98 % (457248)Time elapsed: 0.041 s
% 3.08/0.98 % (457248)Peak memory usage: 90 MB
% 3.08/0.98 % (457248)Instructions burned: 72 (million)
% 3.08/0.98 % (457250)lrs+10_64_to=lpo:sil=8000:random_seed=1511558274:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 3.08/0.98 % (457247)Instruction limit reached!
% 3.08/0.98 % (457247)------------------------------
% 3.08/0.98 % (457247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/0.98 % (457247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.98 % (457247)CaDiCaL version: 2.1.3
% 3.08/0.98 % (457247)Termination reason: Instruction limit
% 3.08/0.98 % (457247)Termination phase: Saturation
% 3.08/0.98 % (457247)Time elapsed: 0.082 s
% 3.08/0.98 % (457247)Peak memory usage: 91 MB
% 3.08/0.98 % (457247)Instructions burned: 144 (million)
% 3.08/0.98 % (457250)First to succeed.
% 3.08/0.98 % (457250)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-457228"
% 3.08/0.98 % (457249)Instruction limit reached!
% 3.08/0.98 % (457249)------------------------------
% 3.08/0.98 % (457249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.08/0.98 % (457249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.08/0.98 % (457249)CaDiCaL version: 2.1.3
% 3.08/0.98 % (457249)Termination reason: Instruction limit
% 3.08/0.98 % (457249)Termination phase: Saturation
% 3.08/0.98 % (457249)Time elapsed: 0.121 s
% 3.08/0.98 % (457249)Peak memory usage: 92 MB
% 3.08/0.98 % (457249)Instructions burned: 219 (million)
% 3.08/0.98 % (457255)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2085459114:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 3.08/0.98 % SZS status Satisfiable for theBenchmark
% 3.08/0.98 % SZS output start Saturation.
% See solution above
% 4.41/1.18 % SZS output start Definitions and Model Updates.
% 4.41/1.18 % SZS output end Definitions and Model Updates.
% 4.41/1.18 % (457250)------------------------------
% 4.41/1.18 % (457250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.41/1.18 % (457250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.41/1.18 % (457250)CaDiCaL version: 2.1.3
% 4.41/1.18 % (457250)Termination reason: Satisfiable
% 4.41/1.18 % (457250)Time elapsed: 0.022 s
% 4.41/1.18 % (457250)Peak memory usage: 91 MB
% 4.41/1.18 % (457250)Instructions burned: 65 (million)
% 4.41/1.18 % (457250)------------------------------
% 4.41/1.18 % (457250)------------------------------
% 4.41/1.18 % (457228)Success in time 0.574 s
% 4.41/1.18 % Vampire exiting
%------------------------------------------------------------------------------