%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN422-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 : n007.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 6.31s 1.50s
% Output : Saturation 6.31s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u533,negated_conjecture,
c9_0 ).
cnf(u539,negated_conjecture,
ndr1_0 ).
cnf(u543,negated_conjecture,
( ~ c4_2(X0,X1)
| c9_2(X0,X2)
| c7_2(X0,X1)
| ~ c5_1(X0)
| ~ c10_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u555,negated_conjecture,
c5_0 ).
cnf(u562,negated_conjecture,
( ~ c5_2(X0,X2)
| c8_1(X0)
| ~ c2_2(X0,X2)
| ~ c7_2(X0,X1)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1)
| ~ c2_2(X0,X1) ) ).
cnf(u571,negated_conjecture,
c3_0 ).
cnf(u604,negated_conjecture,
( ~ c2_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,X1)
| ~ c6_1(X0)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u608,negated_conjecture,
c10_0 ).
cnf(u613,negated_conjecture,
~ ndr1_1(a755) ).
cnf(u623,negated_conjecture,
~ c2_0 ).
cnf(u631,negated_conjecture,
( ~ c8_2(X0,X2)
| c10_1(X0)
| ~ c10_2(X0,X1)
| ~ c6_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1)
| ~ c3_2(X0,X1) ) ).
cnf(u641,negated_conjecture,
~ c1_0 ).
cnf(u658,negated_conjecture,
~ c7_0 ).
cnf(u679,negated_conjecture,
( ~ c8_2(X0,X2)
| c1_1(X0)
| c4_2(X0,X2)
| c6_2(X0,X2)
| c10_2(X0,X1)
| c4_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u682,negated_conjecture,
ssSkC19 ).
cnf(u738,negated_conjecture,
( ~ c4_2(X0,X1)
| c3_2(X0,X1)
| ~ c10_1(X0)
| ~ c4_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u741,negated_conjecture,
ssSkC26 ).
cnf(u750,negated_conjecture,
~ c6_0 ).
cnf(u761,negated_conjecture,
( ~ c10_2(X0,X1)
| c2_1(X0)
| c2_2(X0,X1)
| c5_2(X0,X1)
| ~ c9_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u769,negated_conjecture,
c8_0 ).
cnf(u777,negated_conjecture,
~ ssSkC0 ).
cnf(u797,negated_conjecture,
~ ssSkC9 ).
cnf(u806,negated_conjecture,
c4_0 ).
cnf(u810,negated_conjecture,
( ~ c8_2(X0,X1)
| c3_2(X0,X2)
| c8_2(X0,X2)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ c10_2(X0,a667)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u818,negated_conjecture,
( ~ c4_2(X0,X1)
| c8_2(X0,X2)
| c6_2(X0,X2)
| c5_2(X0,X1)
| ~ c4_1(X0)
| ~ c9_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u837,negated_conjecture,
( ~ c8_2(X0,X1)
| c6_2(X0,a667)
| c3_2(X0,X2)
| c8_2(X0,X2)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u841,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_2(X0,a667)
| c3_2(X0,X2)
| c8_2(X0,X2)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u857,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_2(X0,X1)
| ~ c9_1(X0)
| ~ c10_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u860,negated_conjecture,
ssSkC12 ).
cnf(u876,negated_conjecture,
( ~ c1_1(X0)
| c5_1(X0)
| c4_2(X0,X2)
| c6_2(X0,X2)
| c8_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u899,negated_conjecture,
( ~ c9_2(X0,X1)
| c2_1(X0)
| ~ c6_1(X0)
| ~ ndr1_1(X0)
| ~ c1_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u907,negated_conjecture,
( ~ c8_2(X0,X1)
| c1_2(X0,X1)
| c4_2(X0,X1)
| ~ c8_1(X0)
| ~ c6_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u910,negated_conjecture,
ssSkC6 ).
cnf(u946,negated_conjecture,
ssSkC22 ).
cnf(u951,negated_conjecture,
ssSkC32 ).
cnf(u955,negated_conjecture,
( ~ c4_2(X0,X1)
| c9_2(X0,X1)
| ~ c10_2(X0,a750)
| ~ ndr1_1(X0)
| ~ ssSkP11(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u959,negated_conjecture,
( ~ c4_2(X0,X1)
| c9_2(X0,X1)
| ~ c8_2(X0,a750)
| ~ ndr1_1(X0)
| ~ ssSkP11(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u964,negated_conjecture,
~ c6_1(a755) ).
cnf(u969,negated_conjecture,
~ c7_1(a755) ).
cnf(u973,negated_conjecture,
( ~ c8_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_1(X0)
| ~ c10_1(X0)
| ~ ndr1_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u992,negated_conjecture,
( ~ c1_2(X0,a671)
| c3_2(X0,X1)
| c7_2(X0,X1)
| c10_2(X0,X1)
| ~ c3_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u995,negated_conjecture,
ssSkC15 ).
cnf(u1026,negated_conjecture,
( ~ c4_2(X0,X1)
| c2_2(X0,a750)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP11(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1030,negated_conjecture,
( ~ c9_2(X0,X1)
| c6_2(X0,X1)
| ~ c3_1(X0)
| ~ c8_1(X0)
| ~ ndr1_1(X0)
| ~ c10_2(X0,X1) ) ).
cnf(u1034,negated_conjecture,
( ~ c3_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_1(X0)
| ~ c2_2(X0,a638)
| ~ ndr1_1(X0) ) ).
cnf(u1043,negated_conjecture,
( ~ c4_2(X0,a654)
| c6_2(X0,X1)
| c10_2(X0,X1)
| ~ c4_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1047,negated_conjecture,
( ~ c9_2(X0,a654)
| c6_2(X0,X1)
| c10_2(X0,X1)
| ~ c4_1(X0)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1051,negated_conjecture,
( ~ c3_1(X0)
| c2_2(X0,a671)
| c3_2(X0,X1)
| c7_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1055,negated_conjecture,
( ~ c3_1(X0)
| c8_2(X0,a671)
| c3_2(X0,X1)
| c7_2(X0,X1)
| c10_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1067,negated_conjecture,
( ~ c1_2(X0,a747)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c2_1(X0)
| ~ c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1071,negated_conjecture,
~ ssSkC25 ).
cnf(u1075,negated_conjecture,
( ~ c9_2(X0,a722)
| c6_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1079,negated_conjecture,
( ~ c5_2(X0,a722)
| c6_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1091,negated_conjecture,
~ ssSkC33 ).
cnf(u1095,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_1(X0)
| c2_2(X0,a751)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u1099,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_1(X0)
| c3_2(X0,a751)
| c9_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u1103,negated_conjecture,
( c7_2(a690,X1)
| c4_2(a690,X1)
| c2_2(a690,X1) ) ).
cnf(u1109,negated_conjecture,
ndr1_1(a690) ).
cnf(u1114,negated_conjecture,
( ~ c5_2(X0,X1)
| c5_1(X0)
| c1_1(X0)
| c10_2(X0,X1)
| c3_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1118,negated_conjecture,
( ~ c3_2(X0,X1)
| c3_1(X0)
| c10_1(X0)
| c5_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c6_2(X0,X1) ) ).
cnf(u1122,negated_conjecture,
( ~ c3_2(X0,X1)
| c1_2(X0,a638)
| c6_2(X0,X1)
| ~ c1_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1126,negated_conjecture,
( ~ c2_2(X0,X1)
| c1_2(X0,a654)
| c6_2(X0,X1)
| c10_2(X0,X1)
| ~ c4_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1134,negated_conjecture,
ssSkC31 ).
cnf(u1138,negated_conjecture,
( ~ c3_2(X0,X1)
| c8_2(X0,a744)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP10(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1142,negated_conjecture,
( ~ c3_2(X0,X1)
| c6_2(X0,a744)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP10(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1146,negated_conjecture,
( ~ c3_2(X0,X1)
| c9_2(X0,a744)
| c6_2(X0,X1)
| ~ ndr1_1(X0)
| ~ ssSkP10(X0)
| ~ c1_2(X0,X1) ) ).
cnf(u1150,negated_conjecture,
( ~ c1_2(X0,X1)
| c9_2(X0,a747)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1154,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_2(X0,a747)
| c5_2(X0,X1)
| c3_2(X0,X1)
| ~ c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1158,negated_conjecture,
( ~ c2_2(X0,X1)
| c6_1(X0)
| c8_2(X0,a722)
| c4_2(X0,X1)
| c5_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1174,negated_conjecture,
( ~ c10_2(X0,X1)
| c8_1(X0)
| c5_2(X0,X1)
| c1_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1179,negated_conjecture,
~ ndr1_1(a618) ).
cnf(u1185,negated_conjecture,
ssSkC2 ).
cnf(u1197,negated_conjecture,
ssSkC7 ).
cnf(u1203,negated_conjecture,
~ ndr1_1(a658) ).
cnf(u1231,negated_conjecture,
~ ndr1_1(a733) ).
cnf(u1237,negated_conjecture,
ssSkC28 ).
cnf(u1250,negated_conjecture,
~ ssSkC20 ).
cnf(u1255,negated_conjecture,
~ ndr1_1(a705) ).
cnf(u1310,negated_conjecture,
ssSkC10 ).
cnf(u1322,negated_conjecture,
ssSkC13 ).
cnf(u1325,negated_conjecture,
ndr1_1(a665) ).
cnf(u1338,negated_conjecture,
~ ndr1_1(a668) ).
cnf(u1346,negated_conjecture,
~ ndr1_1(a696) ).
cnf(u1357,negated_conjecture,
( ~ c4_1(X0)
| ~ c6_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1380,negated_conjecture,
~ ndr1_1(a708) ).
cnf(u1386,negated_conjecture,
ssSkC21 ).
cnf(u1392,negated_conjecture,
ssSkC3 ).
cnf(u1419,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| ~ c6_1(X0) ) ).
cnf(u1423,negated_conjecture,
( ~ c3_1(X0)
| c1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1452,negated_conjecture,
~ ndr1_1(a756) ).
cnf(u1460,negated_conjecture,
ssSkC5 ).
cnf(u1486,negated_conjecture,
ssSkC34 ).
cnf(u1491,negated_conjecture,
( ~ c2_2(X0,a613)
| c10_1(X0)
| c2_1(X0) ) ).
cnf(u1494,negated_conjecture,
ssSkC1 ).
cnf(u1499,negated_conjecture,
( ~ c1_1(X0)
| c7_1(X0)
| c5_2(X0,a650) ) ).
cnf(u1502,negated_conjecture,
ssSkC8 ).
cnf(u1507,negated_conjecture,
( ~ c1_1(X0)
| c7_1(X0)
| c1_2(X0,a650) ) ).
cnf(u1511,negated_conjecture,
( ~ c1_1(X0)
| c7_1(X0)
| c7_2(X0,a650) ) ).
cnf(u1515,negated_conjecture,
( ~ c7_2(X0,a666)
| c7_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1536,negated_conjecture,
~ c10_2(a690,a691) ).
cnf(u1541,negated_conjecture,
~ c9_2(a690,a691) ).
cnf(u1546,negated_conjecture,
~ c5_2(a690,a691) ).
cnf(u1558,negated_conjecture,
~ ssSkC23 ).
cnf(u1562,negated_conjecture,
( ~ c4_2(X0,a719)
| ~ c10_1(X0)
| ~ ssSkP8(X0) ) ).
cnf(u1566,negated_conjecture,
( ~ c7_2(X0,a719)
| ~ c10_1(X0)
| ~ ssSkP8(X0) ) ).
cnf(u1578,negated_conjecture,
~ ndr1_1(a614) ).
cnf(u1614,negated_conjecture,
( c2_1(X0)
| c10_1(X0)
| c9_2(X0,a613) ) ).
cnf(u1618,negated_conjecture,
( ~ c1_1(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u1622,negated_conjecture,
ssSkC11 ).
cnf(u1626,negated_conjecture,
( ~ c2_2(X0,a662)
| ~ c8_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u1630,negated_conjecture,
( ~ c6_2(X0,a662)
| ~ c8_1(X0)
| ~ ssSkP1(X0) ) ).
cnf(u1634,negated_conjecture,
( ~ c3_1(X0)
| c7_1(X0)
| c3_2(X0,a666) ) ).
cnf(u1638,negated_conjecture,
( ~ c3_1(X0)
| c7_1(X0)
| c8_2(X0,a666) ) ).
cnf(u1654,negated_conjecture,
~ ssSkC4 ).
cnf(u1658,negated_conjecture,
( ~ c9_2(X0,a624)
| c2_1(X0)
| c4_1(X0) ) ).
cnf(u1666,negated_conjecture,
( ~ ssSkP8(X0)
| c2_2(X0,a719)
| ~ c10_1(X0) ) ).
cnf(u1671,negated_conjecture,
ssSkC24 ).
cnf(u1702,negated_conjecture,
( c2_1(X0)
| c10_1(X0)
| ndr1_1(X0) ) ).
cnf(u1706,negated_conjecture,
( ~ ssSkP1(X0)
| c10_2(X0,a662)
| ~ c8_1(X0) ) ).
cnf(u1710,negated_conjecture,
( ~ c3_1(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u1715,negated_conjecture,
c2_1(a690) ).
cnf(u1724,negated_conjecture,
( c2_1(X0)
| c5_2(X0,a624)
| c4_1(X0) ) ).
cnf(u1728,negated_conjecture,
( ~ ssSkP8(X0)
| ndr1_1(X0)
| ~ c10_1(X0) ) ).
cnf(u1748,negated_conjecture,
( ~ ssSkP1(X0)
| ndr1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u1752,negated_conjecture,
( c2_1(X0)
| ndr1_1(X0)
| c4_1(X0) ) ).
cnf(u1769,negated_conjecture,
~ c5_2(a614,a615) ).
cnf(u1774,negated_conjecture,
~ c1_2(a614,a616) ).
cnf(u1804,negated_conjecture,
~ c8_2(a686,a687) ).
cnf(u1809,negated_conjecture,
~ c1_2(a686,a687) ).
cnf(u1814,negated_conjecture,
~ c5_2(a698,a699) ).
cnf(u1832,negated_conjecture,
ssSkC27 ).
cnf(u1841,negated_conjecture,
ssSkC29 ).
cnf(u1867,negated_conjecture,
c3_2(a614,a615) ).
cnf(u1872,negated_conjecture,
c10_2(a614,a616) ).
cnf(u1877,negated_conjecture,
c9_2(a614,a616) ).
cnf(u1882,negated_conjecture,
~ c8_1(a622) ).
cnf(u1887,negated_conjecture,
c2_2(a622,a623) ).
cnf(u1892,negated_conjecture,
c1_2(a622,a623) ).
cnf(u1897,negated_conjecture,
c6_2(a622,a623) ).
cnf(u1937,negated_conjecture,
c3_2(a656,a657) ).
cnf(u1942,negated_conjecture,
c6_2(a656,a657) ).
cnf(u1967,negated_conjecture,
c4_2(a686,a687) ).
cnf(u1972,negated_conjecture,
c2_2(a686,a688) ).
cnf(u1977,negated_conjecture,
c4_2(a686,a688) ).
cnf(u1982,negated_conjecture,
c1_2(a698,a699) ).
cnf(u2022,negated_conjecture,
~ c4_1(a733) ).
cnf(u2117,negated_conjecture,
ssSkC16 ).
cnf(u2159,negated_conjecture,
~ c4_1(a608) ).
cnf(u2164,negated_conjecture,
~ c10_1(a608) ).
cnf(u2169,negated_conjecture,
~ c9_1(a608) ).
cnf(u2175,negated_conjecture,
c3_1(a618) ).
cnf(u2180,negated_conjecture,
c4_1(a622) ).
cnf(u2185,negated_conjecture,
ndr1_1(a622) ).
cnf(u2220,negated_conjecture,
c1_1(a656) ).
cnf(u2225,negated_conjecture,
c7_1(a656) ).
cnf(u2230,negated_conjecture,
ndr1_1(a656) ).
cnf(u2251,negated_conjecture,
c8_1(a686) ).
cnf(u2256,negated_conjecture,
ndr1_1(a686) ).
cnf(u2276,negated_conjecture,
c9_1(a698) ).
cnf(u2281,negated_conjecture,
c2_1(a698) ).
cnf(u2286,negated_conjecture,
ndr1_1(a698) ).
cnf(u2292,negated_conjecture,
~ c5_1(a708) ).
cnf(u2365,negated_conjecture,
~ c8_1(a609) ).
cnf(u2370,negated_conjecture,
~ c10_1(a609) ).
cnf(u2375,negated_conjecture,
~ c5_1(a609) ).
cnf(u2425,negated_conjecture,
~ c7_1(a651) ).
cnf(u2430,negated_conjecture,
~ c9_1(a651) ).
cnf(u2435,negated_conjecture,
~ c5_1(a651) ).
cnf(u2450,negated_conjecture,
~ c2_1(a665) ).
cnf(u2455,negated_conjecture,
~ c9_1(a668) ).
cnf(u2480,negated_conjecture,
~ c1_1(a696) ).
cnf(u2485,negated_conjecture,
~ c10_1(a700) ).
cnf(u2490,negated_conjecture,
~ c9_1(a700) ).
cnf(u2495,negated_conjecture,
~ c7_1(a700) ).
cnf(u2510,negated_conjecture,
~ c3_1(a705) ).
cnf(u2515,negated_conjecture,
~ c9_1(a705) ).
cnf(u2550,negated_conjecture,
~ c7_1(a739) ).
cnf(u2555,negated_conjecture,
~ c5_1(a739) ).
cnf(u2560,negated_conjecture,
~ c2_1(a739) ).
cnf(u2575,negated_conjecture,
ssSkC35 ).
cnf(u2618,negated_conjecture,
c7_1(a658) ).
cnf(u2654,negated_conjecture,
c4_1(a758) ).
cnf(u2659,negated_conjecture,
c8_1(a758) ).
cnf(u2664,negated_conjecture,
c1_1(a758) ).
cnf(u2796,negated_conjecture,
c6_1(a756) ).
cnf(u2836,negated_conjecture,
~ c5_1(a665) ).
cnf(u2840,negated_conjecture,
~ c3_1(a665) ).
cnf(u2847,negated_conjecture,
~ c5_1(a758) ).
cnf(u2851,negated_conjecture,
~ c6_1(a758) ).
cnf(u2857,negated_conjecture,
~ c6_1(a690) ).
cnf(u2860,negated_conjecture,
~ c3_1(a690) ).
cnf(u2878,negated_conjecture,
~ c5_1(a622) ).
cnf(u2882,negated_conjecture,
~ c6_1(a622) ).
cnf(u2889,negated_conjecture,
~ c6_1(a698) ).
cnf(u2899,negated_conjecture,
~ c8_1(a618) ).
cnf(u2927,negated_conjecture,
~ c8_1(a756) ).
cnf(u2939,negated_conjecture,
c5_2(a758,a650) ).
cnf(u2950,negated_conjecture,
c1_2(a758,a650) ).
cnf(u2957,negated_conjecture,
c7_2(a758,a650) ).
cnf(u2965,negated_conjecture,
c9_2(a739,a613) ).
cnf(u2974,negated_conjecture,
c9_2(a665,a613) ).
cnf(u2993,negated_conjecture,
c4_1(a739) ).
cnf(u3002,negated_conjecture,
c4_1(a665) ).
cnf(u3013,negated_conjecture,
~ c6_1(a665) ).
cnf(u3020,negated_conjecture,
c5_2(a686,a661) ).
cnf(u3029,negated_conjecture,
c5_2(a758,a661) ).
cnf(u3054,negated_conjecture,
ssSkP8(a690) ).
cnf(u3068,negated_conjecture,
~ c10_1(a690) ).
cnf(u3100,negated_conjecture,
~ c3_1(a686) ).
cnf(u3120,negated_conjecture,
~ c8_2(a686,a688) ).
cnf(u3124,negated_conjecture,
~ c4_1(a686) ).
cnf(u3138,negated_conjecture,
( c4_2(a656,X0)
| c8_2(a656,X0)
| c6_2(a656,X0) ) ).
cnf(u3150,negated_conjecture,
~ ssSkP8(a758) ).
cnf(u3154,negated_conjecture,
~ c10_1(a758) ).
cnf(u3171,negated_conjecture,
~ ssSkP8(a656) ).
cnf(u3174,negated_conjecture,
c10_1(a656) ).
cnf(u3213,negated_conjecture,
~ c6_1(a739) ).
cnf(u3236,negated_conjecture,
~ c3_1(a739) ).
cnf(u3249,negated_conjecture,
c3_2(a686,a661) ).
cnf(u3256,negated_conjecture,
~ c1_1(a686) ).
cnf(u3260,negated_conjecture,
~ c5_1(a686) ).
cnf(u3307,negated_conjecture,
~ ssSkP11(a656) ).
cnf(u3311,negated_conjecture,
~ c10_2(a656,a750) ).
cnf(u3319,negated_conjecture,
~ ssSkP11(a758) ).
cnf(u3336,negated_conjecture,
~ ssSkP11(a686) ).
cnf(u3389,negated_conjecture,
~ c4_1(a656) ).
cnf(u3398,negated_conjecture,
c8_2(a758,a654) ).
cnf(u3401,negated_conjecture,
~ c6_2(a758,a654) ).
cnf(u3433,negated_conjecture,
c1_2(a758,a654) ).
cnf(u3476,negated_conjecture,
~ c1_2(a686,a661) ).
cnf(u3501,negated_conjecture,
~ c2_1(a622) ).
cnf(u3519,negated_conjecture,
c3_2(a698,a699) ).
cnf(u3533,negated_conjecture,
c9_2(a622,a613) ).
cnf(u3558,negated_conjecture,
~ c1_1(a698) ).
cnf(u3561,negated_conjecture,
~ c6_2(a698,a699) ).
cnf(u3581,negated_conjecture,
~ ssSkP10(a698) ).
cnf(u3621,negated_conjecture,
c4_2(a622,a623) ).
cnf(u3642,negated_conjecture,
~ c8_2(a622,a623) ).
cnf(u3647,negated_conjecture,
~ ssSkP11(a622) ).
cnf(u3709,negated_conjecture,
~ c10_2(a758,a667) ).
cnf(u3728,negated_conjecture,
~ c2_1(a758) ).
cnf(u3752,negated_conjecture,
~ c10_2(a758,a613) ).
cnf(clause240,negated_conjecture,
( ~ c5_2(X0,a682)
| ssSkP4(X0) ) ).
cnf(clause75,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause49,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(u2911,negated_conjecture,
ndr1_1(a739) ).
cnf(clause63,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause239,negated_conjecture,
( ~ c10_2(X0,a682)
| ssSkP4(X0) ) ).
cnf(clause251,negated_conjecture,
( ~ c2_2(X0,a635)
| ssSkP0(X0) ) ).
cnf(clause70,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(clause242,negated_conjecture,
( ~ c9_2(X0,a676)
| ssSkP3(X0) ) ).
cnf(clause129,negated_conjecture,
( ssSkP9(X0)
| c3_2(X0,a731) ) ).
cnf(clause148,negated_conjecture,
( ssSkP4(X0)
| c3_2(X0,a682) ) ).
cnf(clause62,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u3668,negated_conjecture,
c7_2(a622,a749) ).
cnf(clause58,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(clause231,negated_conjecture,
( ~ c8_2(X0,a718)
| ssSkP8(X0) ) ).
cnf(clause118,negated_conjecture,
( ssSkP11(X0)
| c6_2(X0,a749) ) ).
cnf(clause234,negated_conjecture,
( ~ c4_2(X0,a712)
| ssSkP6(X0) ) ).
cnf(u3367,negated_conjecture,
c6_2(a656,a749) ).
cnf(u2985,negated_conjecture,
( ~ c8_1(X0)
| c10_2(X0,a662)
| c5_2(X0,a661) ) ).
cnf(u3744,negated_conjecture,
c9_2(a758,a613) ).
cnf(clause147,negated_conjecture,
( ssSkP5(X0)
| c7_2(X0,a684) ) ).
cnf(clause166,negated_conjecture,
( ssSkP0(X0)
| c8_2(X0,a635) ) ).
cnf(clause225,negated_conjecture,
( ~ c9_2(X0,a743)
| ssSkP10(X0) ) ).
cnf(u2829,negated_conjecture,
( ~ c8_1(X0)
| ndr1_1(X0) ) ).
cnf(clause244,negated_conjecture,
( ~ c1_2(X0,a661)
| ssSkP1(X0) ) ).
cnf(u2989,negated_conjecture,
( ~ c6_1(X0)
| c4_1(X0)
| c3_1(X0)
| c5_2(X0,a624) ) ).
cnf(clause151,negated_conjecture,
( ssSkP2(X0)
| c8_2(X0,a675) ) ).
cnf(u3667,negated_conjecture,
c6_2(a622,a749) ).
cnf(clause53,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(clause56,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u2961,negated_conjecture,
( ~ c6_1(X0)
| c9_2(X0,a613)
| c3_1(X0)
| c10_1(X0) ) ).
cnf(clause232,negated_conjecture,
( ~ c7_2(X0,a718)
| ssSkP8(X0) ) ).
cnf(u2916,negated_conjecture,
c7_1(a618) ).
cnf(u3352,negated_conjecture,
c7_2(a686,a749) ).
cnf(u3354,negated_conjecture,
c6_2(a758,a749) ).
cnf(clause130,negated_conjecture,
( ssSkP9(X0)
| c9_2(X0,a731) ) ).
cnf(clause145,negated_conjecture,
( ssSkP5(X0)
| c6_2(X0,a684) ) ).
cnf(clause243,negated_conjecture,
( ~ c1_2(X0,a675)
| ssSkP2(X0) ) ).
cnf(u3368,negated_conjecture,
c7_2(a656,a749) ).
cnf(clause149,negated_conjecture,
( ssSkP3(X0)
| c8_2(X0,a676) ) ).
cnf(u2873,negated_conjecture,
( ~ c8_2(X0,X1)
| c5_2(X0,X1)
| ~ c8_1(X0)
| ~ c10_1(X0)
| ~ c3_2(X0,X1) ) ).
cnf(u2933,negated_conjecture,
c7_1(a756) ).
cnf(clause224,negated_conjecture,
( ~ c5_2(X0,a749)
| ssSkP11(X0) ) ).
cnf(u2828,negated_conjecture,
( ~ c10_1(X0)
| ndr1_1(X0) ) ).
cnf(clause65,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u2921,negated_conjecture,
c3_1(a756) ).
cnf(clause50,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(clause235,negated_conjecture,
( ~ c9_2(X0,a712)
| ssSkP6(X0) ) ).
cnf(clause226,negated_conjecture,
( ~ c10_2(X0,a743)
| ssSkP10(X0) ) ).
cnf(u3351,negated_conjecture,
c6_2(a686,a749) ).
cnf(clause241,negated_conjecture,
( ~ c5_2(X0,a676)
| ssSkP3(X0) ) ).
cnf(u2910,negated_conjecture,
( ~ c6_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(clause132,negated_conjecture,
( ssSkP6(X0)
| c8_2(X0,a712) ) ).
cnf(clause57,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause167,negated_conjecture,
( ssSkP0(X0)
| c3_2(X0,a635) ) ).
cnf(u3355,negated_conjecture,
c7_2(a758,a749) ).
cnf(clause245,negated_conjecture,
( ~ c6_2(X0,a661)
| ssSkP1(X0) ) ).
cnf(clause155,negated_conjecture,
( ssSkP1(X0)
| c5_2(X0,a661) ) ).
cnf(clause146,negated_conjecture,
( ssSkP5(X0)
| c1_2(X0,a684) ) ).
cnf(clause117,negated_conjecture,
( ssSkP11(X0)
| c7_2(X0,a749) ) ).
cnf(u3135,negated_conjecture,
( c4_2(a758,X0)
| c6_2(a758,X0)
| c8_2(a758,X0) ) ).
cnf(u2830,negated_conjecture,
ndr1_1(a758) ).
cnf(clause233,negated_conjecture,
( ~ c3_2(X0,a715)
| ssSkP7(X0) ) ).
cnf(clause64,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(clause131,negated_conjecture,
( ssSkP7(X0)
| c10_2(X0,a715) ) ).
cnf(clause150,negated_conjecture,
( ssSkP2(X0)
| c5_2(X0,a675) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN422-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n007.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 15:53:25 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 4.96/1.50 % (2522076)Input is clausal, will run a generic CNF schedule.
% 4.96/1.50 % (2522085)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3880990050:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.96/1.50 % (2522084)lrs+10_1_sil=8000:sp=occurrence:random_seed=3447587527:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.96/1.50 % (2522083)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2249353333:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.96/1.50 % (2522082)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4053076895:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.96/1.50 % (2522081)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=3359750076:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.96/1.50 % (2522085)Instruction limit reached!
% 4.96/1.50 % (2522085)------------------------------
% 6.31/1.50 % (2522085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522085)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522085)Termination reason: Instruction limit
% 6.31/1.50 % (2522085)Termination phase: Saturation
% 6.31/1.50 % (2522085)Time elapsed: 0.037 s
% 6.31/1.50 % (2522085)Peak memory usage: 90 MB
% 6.31/1.50 % (2522085)Instructions burned: 117 (million)
% 6.31/1.50 % (2522087)dis-21_1_sil=8000:lcm=predicate:random_seed=291017090: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)
% 6.31/1.50 % (2522086)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2945960324:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.31/1.50 % (2522086)Refutation not found, incomplete strategy
% 6.31/1.50 % (2522086)------------------------------
% 6.31/1.50 % (2522086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522086)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522086)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.50 % (2522086)Time elapsed: 0.022 s
% 6.31/1.50 % (2522086)Peak memory usage: 90 MB
% 6.31/1.50 % (2522086)Instructions burned: 35 (million)
% 6.31/1.50 % (2522084)Instruction limit reached!
% 6.31/1.50 % (2522084)------------------------------
% 6.31/1.50 % (2522084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522084)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522084)Termination reason: Instruction limit
% 6.31/1.50 % (2522084)Termination phase: Saturation
% 6.31/1.50 % (2522084)Time elapsed: 0.059 s
% 6.31/1.50 % (2522084)Peak memory usage: 91 MB
% 6.31/1.50 % (2522084)Instructions burned: 107 (million)
% 6.31/1.50 % (2522087)Instruction limit reached!
% 6.31/1.50 % (2522087)------------------------------
% 6.31/1.50 % (2522087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522087)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522087)Termination reason: Instruction limit
% 6.31/1.50 % (2522087)Termination phase: Saturation
% 6.31/1.50 % (2522087)Time elapsed: 0.064 s
% 6.31/1.50 % (2522087)Peak memory usage: 90 MB
% 6.31/1.50 % (2522087)Instructions burned: 118 (million)
% 6.31/1.50 % (2522093)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=2604284655:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 6.31/1.50 % (2522096)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1012553109: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)
% 6.31/1.50 % (2522093)Instruction limit reached!
% 6.31/1.50 % (2522093)------------------------------
% 6.31/1.50 % (2522093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522093)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522093)Termination reason: Instruction limit
% 6.31/1.50 % (2522093)Termination phase: Saturation
% 6.31/1.50 % (2522093)Time elapsed: 0.079 s
% 6.31/1.50 % (2522093)Peak memory usage: 91 MB
% 6.31/1.50 % (2522093)Instructions burned: 145 (million)
% 6.31/1.50 % (2522086)------------------------------
% 6.31/1.50 % (2522086)------------------------------
% 6.31/1.50 % (2522097)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=270907200:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.31/1.50 % (2522096)Refutation not found, incomplete strategy
% 6.31/1.50 % (2522096)------------------------------
% 6.31/1.50 % (2522096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522096)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522096)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.50 % (2522096)Time elapsed: 0.035 s
% 6.31/1.50 % (2522096)Peak memory usage: 90 MB
% 6.31/1.50 % (2522096)Instructions burned: 60 (million)
% 6.31/1.50 % (2522097)Instruction limit reached!
% 6.31/1.50 % (2522097)------------------------------
% 6.31/1.50 % (2522097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522097)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522097)Termination reason: Instruction limit
% 6.31/1.50 % (2522097)Termination phase: Saturation
% 6.31/1.50 % (2522097)Time elapsed: 0.114 s
% 6.31/1.50 % (2522097)Peak memory usage: 92 MB
% 6.31/1.50 % (2522097)Instructions burned: 221 (million)
% 6.31/1.50 % (2522102)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=893756701:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.31/1.50 % (2522100)lrs+10_64_to=lpo:sil=8000:random_seed=4118574788:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.31/1.50 % (2522102)Refutation not found, incomplete strategy
% 6.31/1.50 % (2522102)------------------------------
% 6.31/1.50 % (2522102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522102)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522102)Termination reason: Refutation not found, incomplete strategy
% 6.31/1.50 % (2522102)Time elapsed: 0.010 s
% 6.31/1.50 % (2522102)Peak memory usage: 89 MB
% 6.31/1.50 % (2522102)Instructions burned: 27 (million)
% 6.31/1.50 % (2522100)First to succeed.
% 6.31/1.50 % (2522100)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2522076"
% 6.31/1.50 % (2522096)------------------------------
% 6.31/1.50 % (2522096)------------------------------
% 6.31/1.50 % (2522103)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4243145400:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.31/1.50 % (2522102)------------------------------
% 6.31/1.50 % (2522102)------------------------------
% 6.31/1.50 % (2522103)Instruction limit reached!
% 6.31/1.50 % (2522103)------------------------------
% 6.31/1.50 % (2522103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.50 % (2522103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.50 % (2522103)CaDiCaL version: 2.1.3
% 6.31/1.50 % (2522103)Termination reason: Instruction limit
% 6.31/1.50 % (2522103)Termination phase: Saturation
% 6.31/1.50 % (2522103)Time elapsed: 0.085 s
% 6.31/1.50 % (2522103)Peak memory usage: 92 MB
% 6.31/1.50 % (2522103)Instructions burned: 158 (million)
% 6.31/1.50 % (2522106)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2256962111:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 6.31/1.50 % SZS status Satisfiable for theBenchmark
% 6.31/1.50 % SZS output start Saturation.
% See solution above
% 6.31/1.59 % SZS output start Definitions and Model Updates.
% 6.31/1.59 % SZS output end Definitions and Model Updates.
% 6.31/1.59 % (2522100)------------------------------
% 6.31/1.59 % (2522100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.31/1.59 % (2522100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.31/1.59 % (2522100)CaDiCaL version: 2.1.3
% 6.31/1.59 % (2522100)Termination reason: Satisfiable
% 6.31/1.59 % (2522100)Time elapsed: 0.026 s
% 6.31/1.59 % (2522100)Peak memory usage: 90 MB
% 6.31/1.59 % (2522100)Instructions burned: 40 (million)
% 6.31/1.59 % (2522100)------------------------------
% 6.31/1.59 % (2522100)------------------------------
% 6.31/1.59 % (2522076)Success in time 0.833 s
% 6.31/1.59 % Vampire exiting
%------------------------------------------------------------------------------