%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN426-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:36 PM UTC 2026
% Result : Satisfiable 10.21s 2.30s
% Output : Saturation 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u727,negated_conjecture,
( ~ c2_2(X6,X7)
| c10_1(X6)
| c6_2(X6,X7)
| c10_2(X6,X7)
| ~ c6_1(X6)
| ~ ndr1_1(X6) ) ).
cnf(u733,negated_conjecture,
ndr1_0 ).
cnf(u741,negated_conjecture,
c3_0 ).
cnf(u752,negated_conjecture,
( ~ c6_2(X0,X3)
| c8_2(X0,X3)
| c10_2(X0,X3)
| c10_2(X0,X2)
| c4_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c8_2(X0,X2)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u759,negated_conjecture,
( ~ c3_2(X0,X1)
| c2_1(X0)
| c10_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u778,negated_conjecture,
( ~ c6_2(X0,X1)
| c3_1(X0)
| c8_2(X0,X2)
| c3_2(X0,X2)
| ~ c7_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u781,negated_conjecture,
ssSkC27 ).
cnf(u793,negated_conjecture,
( ~ c3_1(X2)
| c4_1(X2)
| ~ c10_1(X2) ) ).
cnf(u806,negated_conjecture,
~ c9_0 ).
cnf(u821,negated_conjecture,
c2_0 ).
cnf(u836,negated_conjecture,
~ c1_0 ).
cnf(u858,negated_conjecture,
ndr1_1(a422) ).
cnf(u862,negated_conjecture,
( ~ c6_2(a422,X1)
| c4_2(a422,X1)
| c3_2(a422,X1) ) ).
cnf(u865,negated_conjecture,
( ~ ndr1_1(X0)
| c5_2(X0,X2)
| c4_2(X0,X2)
| c1_2(X0,X2)
| ~ c6_1(X0)
| ~ c2_1(X0) ) ).
cnf(u868,negated_conjecture,
ssSkC39 ).
cnf(u901,negated_conjecture,
~ c7_0 ).
cnf(u904,negated_conjecture,
( ~ c1_2(X1,X2)
| c4_1(X1)
| c5_2(X1,X2)
| c3_2(X1,X2)
| ~ c8_1(X1)
| ~ ndr1_1(X1) ) ).
cnf(u938,negated_conjecture,
~ c6_0 ).
cnf(u947,negated_conjecture,
c8_0 ).
cnf(u950,negated_conjecture,
c4_0 ).
cnf(u972,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,X2)
| c10_2(X0,X2)
| c9_2(X0,X1)
| c6_2(X0,X1)
| ~ c4_2(X0,a286)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u976,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,X2)
| c10_2(X0,X2)
| c9_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_2(X0,a286)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1012,negated_conjecture,
( ~ c1_2(X0,X1)
| c2_2(X0,a286)
| c8_2(X0,X2)
| c10_2(X0,X2)
| c9_2(X0,X1)
| c6_2(X0,X1)
| ~ c3_2(X0,X2)
| ~ ndr1_1(X0) ) ).
cnf(u1016,negated_conjecture,
( ~ c9_2(X1,X2)
| c7_1(X1)
| ~ c9_1(X1)
| ~ ndr1_1(X1)
| ~ c2_2(X1,X2) ) ).
cnf(u1019,negated_conjecture,
ssSkC25 ).
cnf(u1045,negated_conjecture,
( ~ c7_2(X0,X1)
| c3_1(X0)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1049,negated_conjecture,
( ~ c3_2(X0,X1)
| c3_1(X0)
| c5_2(X0,X2)
| ~ c9_2(X0,X2)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1)
| ~ c10_2(X0,X1) ) ).
cnf(u1053,negated_conjecture,
~ c10_0 ).
cnf(u1057,negated_conjecture,
ndr1_1(a223) ).
cnf(u1061,negated_conjecture,
( ~ c7_2(a223,X1)
| ~ c8_2(a223,X1)
| ~ c1_2(a223,X1) ) ).
cnf(u1080,negated_conjecture,
ndr1_1(a401) ).
cnf(u1084,negated_conjecture,
( ~ c10_2(a401,X1)
| ~ c2_2(a401,X1)
| ~ c1_2(a401,X1) ) ).
cnf(u1090,negated_conjecture,
ssSkC32 ).
cnf(u1102,negated_conjecture,
( ~ c7_1(X0)
| ~ c8_1(X0)
| ~ c3_1(X0) ) ).
cnf(u1105,negated_conjecture,
ssSkC36 ).
cnf(u1133,negated_conjecture,
( ~ c7_2(X0,a338)
| c8_1(X0)
| c10_2(X0,X1)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c9_2(X0,X1) ) ).
cnf(u1140,negated_conjecture,
ssSkC21 ).
cnf(u1153,negated_conjecture,
( ~ c3_2(X0,X1)
| c2_1(X0)
| c9_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1156,negated_conjecture,
ssSkC26 ).
cnf(u1207,negated_conjecture,
( ~ c4_2(a401,X1)
| c8_2(a401,X1)
| ~ c2_2(a401,X1) ) ).
cnf(u1241,negated_conjecture,
( ~ c9_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a338)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1245,negated_conjecture,
( ~ c9_2(X0,X1)
| c8_1(X0)
| c10_2(X0,a338)
| c10_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c8_2(X0,X1) ) ).
cnf(u1249,negated_conjecture,
( ~ c6_2(X0,a359)
| c8_1(X0)
| c3_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1252,negated_conjecture,
ssSkC20 ).
cnf(u1257,negated_conjecture,
( ~ c5_2(X0,X1)
| c8_1(X0)
| c3_2(X0,X1)
| ~ c2_2(X0,a359)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1) ) ).
cnf(u1261,negated_conjecture,
( ~ c10_2(X0,a359)
| c8_1(X0)
| c3_2(X0,X1)
| ~ c2_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c5_2(X0,X1) ) ).
cnf(u1278,negated_conjecture,
ssSkC8 ).
cnf(u1320,negated_conjecture,
~ c10_1(a422) ).
cnf(u1324,negated_conjecture,
c1_1(a422) ).
cnf(u1329,negated_conjecture,
~ ssSkC4 ).
cnf(u1333,negated_conjecture,
( ~ c6_2(X0,X1)
| c10_1(X0)
| c8_2(X0,X1)
| ~ c10_2(X0,a270)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u1338,negated_conjecture,
ssSkC10 ).
cnf(u1350,negated_conjecture,
ssSkC13 ).
cnf(u1362,negated_conjecture,
ssSkC22 ).
cnf(u1377,negated_conjecture,
~ ssSkC29 ).
cnf(u1381,negated_conjecture,
( ~ c6_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ c7_1(X0)
| ~ c9_2(X0,a392)
| ~ ndr1_1(X0) ) ).
cnf(u1412,negated_conjecture,
( ~ c6_2(X0,X1)
| c10_1(X0)
| c3_2(X0,a270)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u1416,negated_conjecture,
( ~ c6_2(X0,X1)
| c10_1(X0)
| c1_2(X0,a270)
| c8_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u1424,negated_conjecture,
( ~ c6_2(X0,X1)
| c3_2(X0,a392)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1428,negated_conjecture,
( ~ c6_2(X0,X1)
| c2_2(X0,a392)
| c7_2(X0,X1)
| c2_2(X0,X1)
| ~ c7_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1435,negated_conjecture,
( ~ ndr1_1(X0)
| c4_1(X0)
| c6_2(X0,X2)
| c3_2(X0,X2)
| c2_2(X0,X2) ) ).
cnf(u1443,negated_conjecture,
( ~ c8_2(a401,X1)
| c5_2(a401,X1) ) ).
cnf(u1447,negated_conjecture,
~ ssSkC1 ).
cnf(u1451,negated_conjecture,
( ~ c7_2(X0,a228)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ c8_2(X0,X1)
| ~ ndr1_1(X0) ) ).
cnf(u1455,negated_conjecture,
~ ssSkC31 ).
cnf(u1459,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ c8_2(X0,a396)
| ~ ndr1_1(X0) ) ).
cnf(u1467,negated_conjecture,
( ~ c6_2(X0,X1)
| c9_2(X0,X1)
| c10_2(X0,X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1475,negated_conjecture,
ssSkC6 ).
cnf(u1479,negated_conjecture,
( ~ c7_2(X0,X1)
| c3_2(X0,X1)
| ~ c5_2(X0,a280)
| ~ ndr1_1(X0)
| ~ ssSkP8(X0) ) ).
cnf(u1483,negated_conjecture,
( ~ c4_2(X0,a280)
| c3_2(X0,X1)
| ~ ssSkP8(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1) ) ).
cnf(u1495,negated_conjecture,
( ~ c8_2(X0,X1)
| c4_2(X0,a228)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1499,negated_conjecture,
( ~ c8_2(X0,X1)
| c3_2(X0,a228)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1503,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_2(X0,a396)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1507,negated_conjecture,
( ~ c7_2(X0,X1)
| c2_2(X0,a396)
| c6_2(X0,X1)
| ~ c8_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u1523,negated_conjecture,
ndr1_1(a222) ).
cnf(u1527,negated_conjecture,
( ~ c2_2(a222,X0)
| c3_2(a222,X0)
| ~ c1_2(a222,X0) ) ).
cnf(u1531,negated_conjecture,
ndr1_1(a309) ).
cnf(u1535,negated_conjecture,
( ~ c4_2(a309,X0)
| c5_2(a309,X0)
| ~ c10_2(a309,X0) ) ).
cnf(u1539,negated_conjecture,
ndr1_1(a318) ).
cnf(u1543,negated_conjecture,
( ~ c4_2(a318,X0)
| ~ c7_2(a318,X0)
| ~ c10_2(a318,X0) ) ).
cnf(u1546,negated_conjecture,
ssSkC12 ).
cnf(u1559,negated_conjecture,
ndr1_1(a342) ).
cnf(u1563,negated_conjecture,
( ~ c3_2(a342,X0)
| c8_2(a342,X0)
| c6_2(a342,X0) ) ).
cnf(u1575,negated_conjecture,
~ ssSkC18 ).
cnf(u1579,negated_conjecture,
~ ssSkC19 ).
cnf(u1583,negated_conjecture,
ndr1_1(a355) ).
cnf(u1587,negated_conjecture,
( ~ c6_2(a355,X0)
| ~ c8_2(a355,X0)
| ~ c4_2(a355,X0) ) ).
cnf(u1591,negated_conjecture,
ndr1_1(a400) ).
cnf(u1600,negated_conjecture,
ssSkC41 ).
cnf(u1622,negated_conjecture,
ssSkC2 ).
cnf(u1659,negated_conjecture,
( ~ c6_2(a309,X0)
| c9_2(a309,X0)
| c10_2(a309,X0) ) ).
cnf(u1671,negated_conjecture,
~ ssSkC11 ).
cnf(u1679,negated_conjecture,
ndr1_1(a357) ).
cnf(u1683,negated_conjecture,
( ~ c8_2(a357,X0)
| c5_2(a357,X0)
| c4_2(a357,X0) ) ).
cnf(u1687,negated_conjecture,
( ~ c9_2(a357,X0)
| c4_2(a357,X0)
| c10_2(a357,X0) ) ).
cnf(u1711,negated_conjecture,
ssSkC24 ).
cnf(u1716,negated_conjecture,
~ ssSkC23 ).
cnf(u1764,negated_conjecture,
ndr1_1(a281) ).
cnf(u1768,negated_conjecture,
( ~ c3_2(a281,X0)
| c7_2(a281,X0)
| ~ c2_2(a281,X0) ) ).
cnf(u1797,negated_conjecture,
ssSkC35 ).
cnf(u1802,negated_conjecture,
~ ssSkC34 ).
cnf(u1815,negated_conjecture,
( ~ c8_1(X0)
| ~ c1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1834,negated_conjecture,
~ c10_2(a223,a224) ).
cnf(u1839,negated_conjecture,
~ c1_2(a223,a224) ).
cnf(u1863,negated_conjecture,
~ ssSkC3 ).
cnf(u1871,negated_conjecture,
( ~ c7_2(X0,a347)
| c7_1(X0)
| c1_1(X0) ) ).
cnf(u1886,negated_conjecture,
~ ssSkC7 ).
cnf(u1890,negated_conjecture,
( ~ c9_2(X0,a292)
| ~ c6_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1894,negated_conjecture,
( ~ c1_2(X0,a292)
| ~ c6_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1898,negated_conjecture,
( ~ c9_2(X0,a313)
| ~ c6_1(X0)
| ~ c5_1(X0) ) ).
cnf(u1902,negated_conjecture,
~ ssSkC37 ).
cnf(u1906,negated_conjecture,
( ~ c6_2(X0,a416)
| ~ c5_1(X0)
| ~ c1_1(X0) ) ).
cnf(u1933,negated_conjecture,
ssSkC15 ).
cnf(u1947,negated_conjecture,
~ c7_1(a223) ).
cnf(u1952,negated_conjecture,
c9_2(a223,a224) ).
cnf(u1972,negated_conjecture,
( ~ c9_2(X0,a291)
| c5_1(X0)
| ~ ssSkP9(X0) ) ).
cnf(u1976,negated_conjecture,
( ~ c6_2(X0,a291)
| c5_1(X0)
| ~ ssSkP9(X0) ) ).
cnf(u1980,negated_conjecture,
( ~ c5_2(X0,a291)
| c5_1(X0)
| ~ ssSkP9(X0) ) ).
cnf(u1988,negated_conjecture,
ssSkC9 ).
cnf(u1996,negated_conjecture,
( ~ c6_2(X0,a312)
| c9_1(X0)
| ~ ssSkP15(X0) ) ).
cnf(u2000,negated_conjecture,
( ~ c9_2(X0,a345)
| c9_1(X0)
| c7_1(X0) ) ).
cnf(u2004,negated_conjecture,
~ ssSkC17 ).
cnf(u2012,negated_conjecture,
( c1_1(X0)
| c7_1(X0)
| c2_2(X0,a347) ) ).
cnf(u2016,negated_conjecture,
( ~ c2_2(X0,a354)
| c8_1(X0)
| ~ c9_1(X0) ) ).
cnf(u2032,negated_conjecture,
ssSkC28 ).
cnf(u2055,negated_conjecture,
~ ssSkC0 ).
cnf(u2059,negated_conjecture,
( ~ c7_2(X0,a226)
| ~ c5_1(X0)
| ~ ssSkP0(X0) ) ).
cnf(u2063,negated_conjecture,
( ~ c4_2(X0,a226)
| ~ c5_1(X0)
| ~ ssSkP0(X0) ) ).
cnf(u2067,negated_conjecture,
~ ssSkC5 ).
cnf(u2071,negated_conjecture,
( ~ c4_2(X0,a274)
| c3_1(X0)
| ~ c4_1(X0) ) ).
cnf(u2079,negated_conjecture,
( ~ c6_1(X0)
| c7_2(X0,a292)
| ~ c5_1(X0) ) ).
cnf(u2095,negated_conjecture,
( ~ c6_1(X0)
| c3_2(X0,a313)
| ~ c5_1(X0) ) ).
cnf(u2103,negated_conjecture,
( ~ c8_2(X0,a373)
| c1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u2107,negated_conjecture,
( ~ c1_2(X0,a373)
| c1_1(X0)
| ~ c8_1(X0) ) ).
cnf(u2116,negated_conjecture,
ssSkC30 ).
cnf(u2123,negated_conjecture,
( ~ c5_2(X0,a405)
| c9_1(X0)
| ~ c2_1(X0) ) ).
cnf(u2127,negated_conjecture,
( ~ c1_1(X0)
| c9_2(X0,a416)
| ~ c5_1(X0) ) ).
cnf(u2194,negated_conjecture,
( c1_1(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u2198,negated_conjecture,
( ~ c9_1(X0)
| c8_1(X0)
| c10_2(X0,a354) ) ).
cnf(u2202,negated_conjecture,
( ~ c9_1(X0)
| c8_1(X0)
| c1_2(X0,a354) ) ).
cnf(u2210,negated_conjecture,
( ~ ssSkP0(X0)
| c6_2(X0,a226)
| ~ c5_1(X0) ) ).
cnf(u2214,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| c3_2(X0,a274) ) ).
cnf(u2218,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| c2_2(X0,a274) ) ).
cnf(u2230,negated_conjecture,
( ~ c6_1(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2247,negated_conjecture,
( ~ c5_2(X0,a349)
| c7_1(X0)
| ~ ssSkP16(X0) ) ).
cnf(u2251,negated_conjecture,
( ~ c2_2(X0,a349)
| c7_1(X0)
| ~ ssSkP16(X0) ) ).
cnf(u2255,negated_conjecture,
( ~ c1_2(X0,a349)
| c7_1(X0)
| ~ ssSkP16(X0) ) ).
cnf(u2271,negated_conjecture,
( ~ c8_1(X0)
| c1_1(X0)
| c3_2(X0,a373) ) ).
cnf(u2311,negated_conjecture,
( ~ c2_1(X0)
| c9_1(X0)
| c4_2(X0,a405) ) ).
cnf(u2315,negated_conjecture,
( ~ c1_1(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2323,negated_conjecture,
ndr1_1(a262) ).
cnf(u2327,negated_conjecture,
( ~ c4_2(a262,X0)
| c5_2(a262,X0) ) ).
cnf(u2347,negated_conjecture,
( ~ c4_2(X0,a261)
| c5_1(X0)
| ~ ssSkP4(X0) ) ).
cnf(u2351,negated_conjecture,
( ~ c1_2(X0,a261)
| c5_1(X0)
| ~ ssSkP4(X0) ) ).
cnf(u2363,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| c6_2(X0,a273) ) ).
cnf(u2367,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| c5_2(X0,a273) ) ).
cnf(u2371,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| c2_2(X0,a273) ) ).
cnf(u2379,negated_conjecture,
( ~ ssSkP9(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u2387,negated_conjecture,
( ~ ssSkP15(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u2391,negated_conjecture,
( c9_1(X0)
| ndr1_1(X0)
| c7_1(X0) ) ).
cnf(u2395,negated_conjecture,
( ~ c9_1(X0)
| c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u2407,negated_conjecture,
( ~ ssSkP0(X0)
| ndr1_1(X0)
| ~ c5_1(X0) ) ).
cnf(u2411,negated_conjecture,
( ~ c4_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u2435,negated_conjecture,
( ~ c8_1(X0)
| c1_1(X0)
| ndr1_1(X0) ) ).
cnf(u2455,negated_conjecture,
( ~ c2_1(X0)
| c9_1(X0)
| ndr1_1(X0) ) ).
cnf(u2479,negated_conjecture,
( ~ c9_2(X0,a344)
| c4_1(X0) ) ).
cnf(u2483,negated_conjecture,
~ ssSkC33 ).
cnf(u2487,negated_conjecture,
( ~ c3_2(X0,a402)
| c8_1(X0) ) ).
cnf(u2491,negated_conjecture,
( ~ c1_2(X0,a402)
| c8_1(X0) ) ).
cnf(u2495,negated_conjecture,
( ~ ssSkP4(X0)
| c5_1(X0)
| c7_2(X0,a261) ) ).
cnf(u2503,negated_conjecture,
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_1(X0) ) ).
cnf(u2516,negated_conjecture,
ssSkC14 ).
cnf(u2527,negated_conjecture,
( ~ ssSkP16(X0)
| c7_1(X0)
| ndr1_1(X0) ) ).
cnf(u2552,negated_conjecture,
( c4_1(X0)
| c6_2(X0,a344) ) ).
cnf(u2556,negated_conjecture,
( c4_1(X0)
| c1_2(X0,a344) ) ).
cnf(u2560,negated_conjecture,
( c8_1(X0)
| c2_2(X0,a402) ) ).
cnf(u2564,negated_conjecture,
( ~ ssSkP4(X0)
| c5_1(X0)
| ndr1_1(X0) ) ).
cnf(u2568,negated_conjecture,
~ c3_2(X0,a268) ).
cnf(u2572,negated_conjecture,
~ c2_2(X0,a268) ).
cnf(u2648,negated_conjecture,
c3_1(a342) ).
cnf(u2654,negated_conjecture,
~ c2_1(a342) ).
cnf(u2688,negated_conjecture,
( ndr1_1(X0)
| c4_1(X0) ) ).
cnf(u2692,negated_conjecture,
( c8_1(X0)
| ndr1_1(X0) ) ).
cnf(u2696,negated_conjecture,
c4_2(X0,a268) ).
cnf(u2716,negated_conjecture,
~ c7_1(a222) ).
cnf(u2721,negated_conjecture,
~ c1_1(a222) ).
cnf(u2786,negated_conjecture,
~ c6_1(a309) ).
cnf(u2826,negated_conjecture,
~ c8_1(a340) ).
cnf(u2829,negated_conjecture,
ssSkC16 ).
cnf(u2835,negated_conjecture,
c9_2(a340,a341) ).
cnf(u2840,negated_conjecture,
c7_2(a340,a341) ).
cnf(u2845,negated_conjecture,
c1_2(a340,a341) ).
cnf(u2913,negated_conjecture,
ssSkC38 ).
cnf(u2934,negated_conjecture,
~ c9_2(a355,a356) ).
cnf(u2939,negated_conjecture,
~ c7_2(a355,a356) ).
cnf(u2944,negated_conjecture,
~ c10_2(a355,a356) ).
cnf(u2993,negated_conjecture,
~ ssSkC42 ).
cnf(u2998,negated_conjecture,
~ c7_2(a427,a428) ).
cnf(u3003,negated_conjecture,
~ c10_2(a427,a428) ).
cnf(u3007,negated_conjecture,
ndr1_1(X0) ).
cnf(u3119,negated_conjecture,
~ c4_2(a281,a282) ).
cnf(u3190,negated_conjecture,
~ c8_1(a318) ).
cnf(u3195,negated_conjecture,
~ c10_1(a318) ).
cnf(u3206,negated_conjecture,
ndr1_1(a340) ).
cnf(u3212,negated_conjecture,
~ c9_1(a357) ).
cnf(u3273,negated_conjecture,
~ c8_1(a425) ).
cnf(u3276,negated_conjecture,
ssSkC40 ).
cnf(u3282,negated_conjecture,
c6_2(a425,a426) ).
cnf(u3287,negated_conjecture,
c5_2(a425,a426) ).
cnf(u3366,negated_conjecture,
c3_1(a400) ).
cnf(u3382,negated_conjecture,
c9_2(a427,a428) ).
cnf(u3446,negated_conjecture,
~ c5_1(a259) ).
cnf(u3451,negated_conjecture,
~ c4_1(a259) ).
cnf(u3456,negated_conjecture,
~ c6_1(a262) ).
cnf(u3481,negated_conjecture,
~ c5_1(a281) ).
cnf(u3486,negated_conjecture,
c8_2(a281,a282) ).
cnf(u3568,negated_conjecture,
c7_1(a425) ).
cnf(u3573,negated_conjecture,
ndr1_1(a425) ).
cnf(u3630,negated_conjecture,
c3_1(a355) ).
cnf(u3711,negated_conjecture,
c10_1(a427) ).
cnf(u3716,negated_conjecture,
ndr1_1(a427) ).
cnf(u3741,negated_conjecture,
c1_1(a262) ).
cnf(u3848,negated_conjecture,
~ c8_1(a259) ).
cnf(u3904,negated_conjecture,
~ c5_1(a422) ).
cnf(u3926,negated_conjecture,
~ c8_1(a357) ).
cnf(u3950,negated_conjecture,
~ c10_1(a355) ).
cnf(u4018,negated_conjecture,
~ c5_1(a262) ).
cnf(u4038,negated_conjecture,
~ c1_2(a222,a347) ).
cnf(u4048,negated_conjecture,
~ c10_2(a309,a268) ).
cnf(u4058,negated_conjecture,
~ c10_2(a318,a268) ).
cnf(u4071,negated_conjecture,
c8_2(a357,a312) ).
cnf(u4081,negated_conjecture,
c5_2(a357,a312) ).
cnf(u4093,negated_conjecture,
~ c2_2(a427,a428) ).
cnf(u4106,negated_conjecture,
~ c2_2(a340,a341) ).
cnf(u4109,negated_conjecture,
c9_1(a340) ).
cnf(u4123,negated_conjecture,
~ c9_1(a223) ).
cnf(u4156,negated_conjecture,
c4_2(a223,a311) ).
cnf(u4167,negated_conjecture,
~ ssSkP8(a340) ).
cnf(u4200,negated_conjecture,
~ c8_1(a222) ).
cnf(u4213,negated_conjecture,
~ c8_1(a281) ).
cnf(u4258,negated_conjecture,
~ c6_1(a222) ).
cnf(u4271,negated_conjecture,
~ c6_1(a425) ).
cnf(u4289,negated_conjecture,
~ c6_1(a340) ).
cnf(u4306,negated_conjecture,
~ c6_1(a318) ).
cnf(u4343,negated_conjecture,
~ c2_1(a425) ).
cnf(u4351,negated_conjecture,
c10_2(a425,a426) ).
cnf(u4364,negated_conjecture,
~ c3_1(a259) ).
cnf(u4367,negated_conjecture,
~ c10_2(a259,a344) ).
cnf(u4382,negated_conjecture,
~ c8_2(a223,a224) ).
cnf(u4389,negated_conjecture,
~ c8_1(a223) ).
cnf(u4395,negated_conjecture,
~ c8_2(a427,a428) ).
cnf(u4408,negated_conjecture,
~ c8_2(a340,a341) ).
cnf(u4431,negated_conjecture,
~ c2_2(a357,a312) ).
cnf(u4448,negated_conjecture,
~ c2_2(a425,a359) ).
cnf(u4464,negated_conjecture,
~ c7_2(a259,a268) ).
cnf(u4468,negated_conjecture,
~ c10_2(a259,a270) ).
cnf(u4472,negated_conjecture,
c8_2(a259,a268) ).
cnf(u4481,negated_conjecture,
~ c7_2(a259,a344) ).
cnf(u4485,negated_conjecture,
c8_2(a259,a344) ).
cnf(u4490,negated_conjecture,
~ c7_2(a425,a426) ).
cnf(u4494,negated_conjecture,
~ c10_2(a425,a270) ).
cnf(u4497,negated_conjecture,
~ c8_2(a425,a426) ).
cnf(u4510,negated_conjecture,
~ c9_2(a259,a392) ).
cnf(u4514,negated_conjecture,
~ c7_1(a259) ).
cnf(u4525,negated_conjecture,
~ c9_2(a425,a392) ).
cnf(u4567,negated_conjecture,
c3_2(a425,a392) ).
cnf(u4578,negated_conjecture,
c2_2(a425,a392) ).
cnf(u4595,negated_conjecture,
( ~ c1_2(a425,X0)
| c9_2(a425,X0)
| c6_2(a425,X0) ) ).
cnf(u4602,negated_conjecture,
~ c8_2(a425,a392) ).
cnf(u4616,negated_conjecture,
~ c5_2(a425,a392) ).
cnf(u4624,negated_conjecture,
c6_2(a425,a392) ).
cnf(u4643,negated_conjecture,
~ c10_2(a259,a268) ).
cnf(u4660,negated_conjecture,
( ~ c3_2(a259,X1)
| ~ c7_2(a259,X1)
| c4_2(a259,X1) ) ).
cnf(u4668,negated_conjecture,
( ~ c3_2(a425,X1)
| ~ c7_2(a425,X1)
| c4_2(a425,X1) ) ).
cnf(u4682,negated_conjecture,
c1_2(a342,a344) ).
cnf(u4701,negated_conjecture,
~ c10_1(a400) ).
cnf(u4719,negated_conjecture,
~ c10_1(a342) ).
cnf(u4745,negated_conjecture,
c4_2(a422,a260) ).
cnf(u4749,negated_conjecture,
c7_2(a422,a261) ).
cnf(u4754,negated_conjecture,
c4_2(a259,a260) ).
cnf(u4763,negated_conjecture,
c4_2(a262,a260) ).
cnf(u4772,negated_conjecture,
c4_2(a281,a260) ).
cnf(u4794,negated_conjecture,
c10_2(a259,a260) ).
cnf(u4799,negated_conjecture,
c10_2(a262,a260) ).
cnf(u4804,negated_conjecture,
c10_2(a281,a260) ).
cnf(u4821,negated_conjecture,
~ c6_1(a357) ).
cnf(u4840,negated_conjecture,
~ c6_1(a281) ).
cnf(u4859,negated_conjecture,
~ c6_1(a259) ).
cnf(u4892,negated_conjecture,
~ c7_2(a425,a392) ).
cnf(u4906,negated_conjecture,
~ c8_1(a342) ).
cnf(u4934,negated_conjecture,
~ c8_1(a422) ).
cnf(u4964,negated_conjecture,
~ c5_2(a422,a280) ).
cnf(u5013,negated_conjecture,
~ ssSkP15(a259) ).
cnf(u5036,negated_conjecture,
~ ssSkP9(a259) ).
cnf(u5049,negated_conjecture,
ssSkP18(a259) ).
cnf(u5061,negated_conjecture,
( ~ c7_2(a259,X0)
| c3_2(a259,X0)
| c8_2(a259,X0)
| c2_2(a259,X0) ) ).
cnf(u5072,negated_conjecture,
( ~ c8_2(a259,X0)
| ~ c10_2(a259,X0)
| c3_2(a259,X0)
| c2_2(a259,X0) ) ).
cnf(u5080,negated_conjecture,
c3_2(a259,a359) ).
cnf(u5206,negated_conjecture,
~ c2_2(a262,a260) ).
cnf(u5244,negated_conjecture,
c8_2(a259,a359) ).
cnf(u5258,negated_conjecture,
~ c7_2(a259,a359) ).
cnf(u5269,negated_conjecture,
~ c5_2(a259,a359) ).
cnf(u5281,negated_conjecture,
~ c2_2(a401,a260) ).
cnf(u5304,negated_conjecture,
c5_2(a309,a260) ).
cnf(u5321,negated_conjecture,
~ c7_2(a318,a260) ).
cnf(u5345,negated_conjecture,
~ c2_2(a309,a260) ).
cnf(u5365,negated_conjecture,
c10_2(a223,a260) ).
cnf(u5368,negated_conjecture,
~ c7_2(a223,a261) ).
cnf(u5373,negated_conjecture,
c2_2(a223,a347) ).
cnf(u5377,negated_conjecture,
c9_2(a223,a416) ).
cnf(u5388,negated_conjecture,
~ c6_1(a223) ).
cnf(u5423,negated_conjecture,
~ c8_2(a223,a416) ).
cnf(u5449,negated_conjecture,
~ c6_1(a342) ).
cnf(u5479,negated_conjecture,
c2_2(a223,a402) ).
cnf(u5504,negated_conjecture,
~ c1_2(a223,a261) ).
cnf(u5536,negated_conjecture,
~ c5_2(a223,a280) ).
cnf(u5564,negated_conjecture,
c5_1(a223) ).
cnf(u5568,negated_conjecture,
c1_1(a223) ).
cnf(u5602,negated_conjecture,
c6_2(a223,a225) ).
cnf(u5605,negated_conjecture,
~ c6_2(a223,a226) ).
cnf(u5611,negated_conjecture,
c7_2(a223,a225) ).
cnf(u5649,negated_conjecture,
~ c2_1(a223) ).
cnf(u5710,negated_conjecture,
~ c10_2(a223,a225) ).
cnf(u5722,negated_conjecture,
c8_2(a223,a225) ).
cnf(u5754,negated_conjecture,
~ c6_1(a422) ).
cnf(u5776,negated_conjecture,
c2_2(a259,a290) ).
cnf(u5793,negated_conjecture,
~ c5_2(a259,a280) ).
cnf(u5802,negated_conjecture,
~ c2_2(a259,a359) ).
cnf(u5824,negated_conjecture,
c2_2(a400,a402) ).
cnf(u5828,negated_conjecture,
c10_2(a400,a260) ).
cnf(u5841,negated_conjecture,
c2_2(a355,a402) ).
cnf(u5876,negated_conjecture,
~ c6_1(a400) ).
cnf(u5892,negated_conjecture,
~ c6_1(a355) ).
cnf(clause98,negated_conjecture,
( ssSkP2(X0)
| ndr1_1(X0) ) ).
cnf(u4232,negated_conjecture,
~ c3_2(a281,a402) ).
cnf(u4127,negated_conjecture,
( c4_1(X0)
| c6_2(X0,X1)
| c3_2(X0,X1)
| c2_2(X0,X1) ) ).
cnf(clause314,negated_conjecture,
( ~ c3_2(X0,a225)
| ssSkP0(X0) ) ).
cnf(clause94,negated_conjecture,
( ssSkP5(X0)
| ndr1_1(X0) ) ).
cnf(u3830,negated_conjecture,
~ c3_2(a425,a402) ).
cnf(u5859,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| c2_2(X0,a274) ) ).
cnf(clause87,negated_conjecture,
( ssSkP12(X0)
| ndr1_1(X0) ) ).
cnf(u4920,negated_conjecture,
c2_2(a342,a402) ).
cnf(u4916,negated_conjecture,
~ c3_2(a342,a402) ).
cnf(clause201,negated_conjecture,
( ssSkP3(X0)
| c1_2(X0,a254) ) ).
cnf(clause288,negated_conjecture,
( ~ c3_2(X0,a365)
| ssSkP17(X0) ) ).
cnf(u5729,negated_conjecture,
~ ssSkP0(a223) ).
cnf(clause100,negated_conjecture,
( ssSkP0(X0)
| ndr1_1(X0) ) ).
cnf(clause91,negated_conjecture,
( ssSkP8(X0)
| ndr1_1(X0) ) ).
cnf(u3897,negated_conjecture,
( ~ c5_1(X0)
| c9_2(X0,a416)
| c7_1(X0)
| c2_2(X0,a347) ) ).
cnf(clause93,negated_conjecture,
( ssSkP6(X0)
| ndr1_1(X0) ) ).
cnf(u3972,negated_conjecture,
( c3_1(X0)
| c3_2(X0,a274)
| c6_2(X0,a344) ) ).
cnf(u4984,negated_conjecture,
c2_2(a422,a402) ).
cnf(clause73,negated_conjecture,
( ssSkP17(X0)
| ndr1_1(X0) ) ).
cnf(u4981,negated_conjecture,
~ c1_2(a422,a402) ).
cnf(clause76,negated_conjecture,
( ssSkP16(X0)
| ndr1_1(X0) ) ).
cnf(u5082,negated_conjecture,
~ c9_2(a259,a311) ).
cnf(u5813,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,a274)
| c6_2(X0,a344) ) ).
cnf(clause191,negated_conjecture,
( ssSkP9(X0)
| c5_2(X0,a290) ) ).
cnf(clause305,negated_conjecture,
( ~ c2_2(X0,a279)
| ssSkP8(X0) ) ).
cnf(u4178,negated_conjecture,
~ c8_2(a340,a279) ).
cnf(u3876,negated_conjecture,
~ c7_2(a222,a347) ).
cnf(clause180,negated_conjecture,
( ssSkP15(X0)
| c4_2(X0,a311) ) ).
cnf(clause299,negated_conjecture,
( ~ c9_2(X0,a307)
| ssSkP14(X0) ) ).
cnf(u4149,negated_conjecture,
~ c9_2(a223,a345) ).
cnf(clause301,negated_conjecture,
( ~ c3_2(X0,a300)
| ssSkP11(X0) ) ).
cnf(u5815,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c2_2(X0,a274)
| c6_2(X0,a344) ) ).
cnf(u4031,negated_conjecture,
( c5_1(X0)
| c7_2(X0,a261)
| c4_2(X0,a260) ) ).
cnf(u5552,negated_conjecture,
~ c3_2(a223,a402) ).
cnf(u5817,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,a274) ) ).
cnf(u3829,negated_conjecture,
~ c3_2(a318,a402) ).
cnf(u3891,negated_conjecture,
( ~ c6_1(X0)
| c4_2(X0,X2)
| c1_2(X0,X2)
| c5_2(X0,X2)
| ~ c2_1(X0) ) ).
cnf(clause309,negated_conjecture,
( ~ c10_2(X0,a271)
| ssSkP5(X0) ) ).
cnf(u4730,negated_conjecture,
( ~ c5_1(X0)
| c2_2(X0,a402)
| c9_2(X0,a416)
| c3_2(X0,a373) ) ).
cnf(u5858,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c2_2(X0,a274)
| c6_2(X0,a344) ) ).
cnf(u5814,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c2_2(X0,a274)
| c1_2(X0,a344) ) ).
cnf(u3977,negated_conjecture,
( ~ c5_1(X0)
| c2_2(X0,a402)
| c7_1(X0)
| c2_2(X0,a347) ) ).
cnf(clause208,negated_conjecture,
( ssSkP1(X0)
| c8_2(X0,a231) ) ).
cnf(u3837,negated_conjecture,
c2_2(a340,a402) ).
cnf(u4177,negated_conjecture,
~ c9_2(a340,a279) ).
cnf(clause202,negated_conjecture,
( ssSkP3(X0)
| c2_2(X0,a254) ) ).
cnf(clause171,negated_conjecture,
( ssSkP16(X0)
| c9_2(X0,a348) ) ).
cnf(clause195,negated_conjecture,
( ssSkP6(X0)
| c2_2(X0,a275) ) ).
cnf(clause160,negated_conjecture,
( ssSkP20(X0)
| c1_2(X0,a393) ) ).
cnf(clause198,negated_conjecture,
( ssSkP5(X0)
| c8_2(X0,a271) ) ).
cnf(clause197,negated_conjecture,
( ssSkP5(X0)
| c3_2(X0,a271) ) ).
cnf(clause210,negated_conjecture,
( ssSkP0(X0)
| c7_2(X0,a225) ) ).
cnf(clause310,negated_conjecture,
( ~ c3_2(X0,a260)
| ssSkP4(X0) ) ).
cnf(u4139,negated_conjecture,
c1_2(a340,a354) ).
cnf(u5855,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,a274)
| c1_2(X0,a344) ) ).
cnf(clause188,negated_conjecture,
( ssSkP11(X0)
| c2_2(X0,a300) ) ).
cnf(u3975,negated_conjecture,
( c1_1(X0)
| c3_2(X0,a373)
| c2_2(X0,a402) ) ).
cnf(clause99,negated_conjecture,
( ssSkP1(X0)
| ndr1_1(X0) ) ).
cnf(u3956,negated_conjecture,
~ c9_2(a259,a344) ).
cnf(clause292,negated_conjecture,
( ~ c3_2(X0,a348)
| ssSkP16(X0) ) ).
cnf(clause88,negated_conjecture,
( ssSkP11(X0)
| ndr1_1(X0) ) ).
cnf(clause181,negated_conjecture,
( ssSkP14(X0)
| c1_2(X0,a307) ) ).
cnf(clause95,negated_conjecture,
( ssSkP4(X0)
| ndr1_1(X0) ) ).
cnf(clause286,negated_conjecture,
( ~ c2_2(X0,a367)
| ssSkP18(X0) ) ).
cnf(u5094,negated_conjecture,
c7_2(a259,a290) ).
cnf(u5739,negated_conjecture,
~ c3_2(a223,a225) ).
cnf(u5860,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,a274) ) ).
cnf(clause313,negated_conjecture,
( ~ c9_2(X0,a231)
| ssSkP1(X0) ) ).
cnf(u5088,negated_conjecture,
( c7_1(X0)
| c2_2(X0,a402)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c10_2(X0,a260) ) ).
cnf(clause307,negated_conjecture,
( ~ c9_2(X0,a279)
| ssSkP8(X0) ) ).
cnf(u5471,negated_conjecture,
( ~ c3_1(X0)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c4_2(X0,a260)
| c2_2(X0,a402) ) ).
cnf(u4917,negated_conjecture,
~ c1_2(a342,a402) ).
cnf(u4734,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c6_2(X0,a226)
| c6_2(X0,a225) ) ).
cnf(u3851,negated_conjecture,
( ~ c7_2(X0,X1)
| c3_1(X0)
| c2_2(X0,X1)
| c1_2(X0,X1)
| ~ c8_1(X0) ) ).
cnf(u3974,negated_conjecture,
( c3_1(X0)
| c2_2(X0,a274)
| c6_2(X0,a344) ) ).
cnf(u4009,negated_conjecture,
( ~ c3_2(X0,X2)
| c2_2(X0,a286)
| c8_2(X0,X2)
| c10_2(X0,X2)
| c9_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u3838,negated_conjecture,
c2_2(a318,a402) ).
cnf(u4179,negated_conjecture,
~ c2_2(a340,a279) ).
cnf(clause84,negated_conjecture,
( ssSkP15(X0)
| ndr1_1(X0) ) ).
cnf(u3833,negated_conjecture,
~ c1_2(a425,a402) ).
cnf(u4329,negated_conjecture,
~ c3_2(a259,a402) ).
cnf(u4032,negated_conjecture,
( c5_1(X0)
| c7_2(X0,a261)
| c10_2(X0,a260) ) ).
cnf(u4227,negated_conjecture,
c2_2(a357,a402) ).
cnf(u5086,negated_conjecture,
c4_2(a259,a311) ).
cnf(clause186,negated_conjecture,
( ssSkP12(X0)
| c5_2(X0,a302) ) ).
cnf(clause185,negated_conjecture,
( ssSkP13(X0)
| c8_2(X0,a305) ) ).
cnf(u4243,negated_conjecture,
c2_2(a222,a402) ).
cnf(clause209,negated_conjecture,
( ssSkP0(X0)
| c6_2(X0,a225) ) ).
cnf(clause182,negated_conjecture,
( ssSkP14(X0)
| c6_2(X0,a307) ) ).
cnf(u3893,negated_conjecture,
c2_2(a222,a347) ).
cnf(clause303,negated_conjecture,
( ~ c5_2(X0,a298)
| ssSkP10(X0) ) ).
cnf(u4813,negated_conjecture,
( c3_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| c3_2(X0,a274) ) ).
cnf(u4007,negated_conjecture,
( ~ c4_2(X0,a286)
| c8_2(X0,X2)
| c10_2(X0,X2)
| c9_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,X2) ) ).
cnf(u3828,negated_conjecture,
~ c3_2(a340,a402) ).
cnf(clause89,negated_conjecture,
( ssSkP10(X0)
| ndr1_1(X0) ) ).
cnf(clause161,negated_conjecture,
( ssSkP20(X0)
| c7_2(X0,a393) ) ).
cnf(clause283,negated_conjecture,
( ~ c8_2(X0,a378)
| ssSkP19(X0) ) ).
cnf(u3971,negated_conjecture,
( c3_1(X0)
| c3_2(X0,a274)
| c1_2(X0,a344) ) ).
cnf(clause285,negated_conjecture,
( ~ c1_2(X0,a367)
| ssSkP18(X0) ) ).
cnf(u5812,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,a274)
| c1_2(X0,a344) ) ).
cnf(u3831,negated_conjecture,
~ c1_2(a340,a402) ).
cnf(clause279,negated_conjecture,
( ~ c3_2(X0,a393)
| ssSkP20(X0) ) ).
cnf(u4806,negated_conjecture,
( c7_1(X0)
| c9_2(X0,a416)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c10_2(X0,a260) ) ).
cnf(u4008,negated_conjecture,
( ~ c3_2(X0,X2)
| c8_2(X0,X2)
| c10_2(X0,X2)
| c9_2(X0,X1)
| c6_2(X0,X1)
| ~ c1_2(X0,a286)
| ~ c1_2(X0,X1) ) ).
cnf(u5089,negated_conjecture,
( c7_1(X0)
| c2_2(X0,a402)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c4_2(X0,a260) ) ).
cnf(u4988,negated_conjecture,
( c10_2(X0,a260)
| c3_2(X0,a373)
| c7_2(X0,a261)
| c2_2(X0,a402) ) ).
cnf(u4779,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c6_2(X0,a226)
| c7_2(X0,a225) ) ).
cnf(u4733,negated_conjecture,
( ~ c5_1(X0)
| c2_2(X0,a402)
| c3_2(X0,a373) ) ).
cnf(clause96,negated_conjecture,
( ssSkP3(X0)
| ndr1_1(X0) ) ).
cnf(u5379,negated_conjecture,
( ~ c8_1(X0)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c4_2(X0,a260)
| c9_2(X0,a416)
| ~ c3_1(X0) ) ).
cnf(clause312,negated_conjecture,
( ~ c2_2(X0,a232)
| ssSkP2(X0) ) ).
cnf(u5625,negated_conjecture,
~ c6_2(a223,a416) ).
cnf(u4980,negated_conjecture,
~ c3_2(a422,a402) ).
cnf(u4811,negated_conjecture,
( c6_2(a259,X0)
| c3_2(a259,X0)
| c2_2(a259,X0) ) ).
cnf(clause206,negated_conjecture,
( ssSkP2(X0)
| c8_2(X0,a232) ) ).
cnf(clause205,negated_conjecture,
( ssSkP2(X0)
| c4_2(X0,a232) ) ).
cnf(clause86,negated_conjecture,
( ssSkP13(X0)
| ndr1_1(X0) ) ).
cnf(u4333,negated_conjecture,
c2_2(a259,a402) ).
cnf(clause192,negated_conjecture,
( ssSkP9(X0)
| c7_2(X0,a290) ) ).
cnf(clause199,negated_conjecture,
( ssSkP4(X0)
| c10_2(X0,a260) ) ).
cnf(u4989,negated_conjecture,
( c4_2(X0,a260)
| c3_2(X0,a373)
| c7_2(X0,a261)
| c2_2(X0,a402) ) ).
cnf(u4807,negated_conjecture,
( c7_1(X0)
| c9_2(X0,a416)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c4_2(X0,a260) ) ).
cnf(u4239,negated_conjecture,
~ c3_2(a222,a402) ).
cnf(u4735,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c6_2(X0,a226)
| c7_2(X0,a225) ) ).
cnf(u5856,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,a274)
| c6_2(X0,a344) ) ).
cnf(clause304,negated_conjecture,
( ~ c9_2(X0,a298)
| ssSkP10(X0) ) ).
cnf(u3969,negated_conjecture,
( ~ c5_1(X0)
| c6_2(X0,a226)
| c6_2(X0,a225) ) ).
cnf(clause66,negated_conjecture,
( ssSkP20(X0)
| ndr1_1(X0) ) ).
cnf(clause298,negated_conjecture,
( ~ c9_2(X0,a311)
| ssSkP15(X0) ) ).
cnf(u5358,negated_conjecture,
( ~ c8_1(X0)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c10_2(X0,a260)
| c9_2(X0,a416)
| ~ c3_1(X0) ) ).
cnf(clause300,negated_conjecture,
( ~ c8_2(X0,a302)
| ssSkP12(X0) ) ).
cnf(clause90,negated_conjecture,
( ssSkP9(X0)
| ndr1_1(X0) ) ).
cnf(u3839,negated_conjecture,
c2_2(a425,a402) ).
cnf(u4125,negated_conjecture,
c6_2(a259,a268) ).
cnf(clause92,negated_conjecture,
( ssSkP7(X0)
| ndr1_1(X0) ) ).
cnf(clause196,negated_conjecture,
( ssSkP6(X0)
| c7_2(X0,a275) ) ).
cnf(clause170,negated_conjecture,
( ssSkP17(X0)
| c4_2(X0,a365) ) ).
cnf(clause85,negated_conjecture,
( ssSkP14(X0)
| ndr1_1(X0) ) ).
cnf(clause72,negated_conjecture,
( ssSkP18(X0)
| ndr1_1(X0) ) ).
cnf(u5096,negated_conjecture,
c1_2(a259,a290) ).
cnf(u5857,negated_conjecture,
( c4_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c2_2(X0,a274)
| c1_2(X0,a344) ) ).
cnf(clause68,negated_conjecture,
( ssSkP19(X0)
| ndr1_1(X0) ) ).
cnf(u4223,negated_conjecture,
~ c3_2(a357,a402) ).
cnf(u3863,negated_conjecture,
( ~ c1_1(X0)
| ~ c5_1(X0)
| c2_2(X0,a402) ) ).
cnf(clause311,negated_conjecture,
( ~ c3_2(X0,a254)
| ssSkP3(X0) ) ).
cnf(u4330,negated_conjecture,
~ c1_2(a259,a402) ).
cnf(u4778,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c6_2(X0,a226)
| c6_2(X0,a225) ) ).
cnf(clause297,negated_conjecture,
( ~ c2_2(X0,a311)
| ssSkP15(X0) ) ).
cnf(u5553,negated_conjecture,
~ c1_2(a223,a402) ).
cnf(clause293,negated_conjecture,
( ~ c4_2(X0,a348)
| ssSkP16(X0) ) ).
cnf(u3958,negated_conjecture,
c6_2(a259,a344) ).
cnf(u4030,negated_conjecture,
c5_2(a262,a268) ).
cnf(u4812,negated_conjecture,
( c3_1(X0)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| c2_2(X0,a274) ) ).
cnf(u5466,negated_conjecture,
( ~ c3_1(X0)
| c2_2(X0,a347)
| c7_2(X0,a261)
| c10_2(X0,a260)
| c2_2(X0,a402) ) ).
cnf(u4224,negated_conjecture,
~ c1_2(a357,a402) ).
cnf(u3973,negated_conjecture,
( c3_1(X0)
| c2_2(X0,a274)
| c1_2(X0,a344) ) ).
cnf(clause187,negated_conjecture,
( ssSkP12(X0)
| c9_2(X0,a302) ) ).
cnf(clause190,negated_conjecture,
( ssSkP9(X0)
| c1_2(X0,a290) ) ).
cnf(u5083,negated_conjecture,
~ c2_2(a259,a311) ).
cnf(clause189,negated_conjecture,
( ssSkP11(X0)
| c4_2(X0,a300) ) ).
cnf(u4240,negated_conjecture,
~ c1_2(a222,a402) ).
cnf(clause183,negated_conjecture,
( ssSkP13(X0)
| c5_2(X0,a305) ) ).
cnf(u4233,negated_conjecture,
~ c1_2(a281,a402) ).
cnf(clause200,negated_conjecture,
( ssSkP4(X0)
| c4_2(X0,a260) ) ).
cnf(u4140,negated_conjecture,
c10_2(a340,a354) ).
cnf(clause169,negated_conjecture,
( ssSkP17(X0)
| c2_2(X0,a365) ) ).
cnf(u4236,negated_conjecture,
c2_2(a281,a402) ).
cnf(clause207,negated_conjecture,
( ssSkP1(X0)
| c10_2(X0,a231) ) ).
cnf(u5738,negated_conjecture,
~ c1_2(a223,a225) ).
cnf(clause194,negated_conjecture,
( ssSkP7(X0)
| c9_2(X0,a277) ) ).
cnf(u4141,negated_conjecture,
~ c2_2(a340,a354) ).
cnf(u3968,negated_conjecture,
( ~ c5_1(X0)
| c6_2(X0,a226)
| c7_2(X0,a225) ) ).
cnf(clause193,negated_conjecture,
( ssSkP7(X0)
| c1_2(X0,a277) ) ).
cnf(clause166,negated_conjecture,
( ssSkP19(X0)
| c7_2(X0,a378) ) ).
cnf(u5095,negated_conjecture,
c5_2(a259,a290) ).
cnf(u3832,negated_conjecture,
~ c1_2(a318,a402) ).
cnf(clause165,negated_conjecture,
( ssSkP19(X0)
| c2_2(X0,a378) ) ).
cnf(clause287,negated_conjecture,
( ~ c6_2(X0,a367)
| ssSkP18(X0) ) ).
cnf(u4987,negated_conjecture,
c5_2(a262,a260) ).
cnf(clause306,negated_conjecture,
( ~ c8_2(X0,a279)
| ssSkP8(X0) ) ).
cnf(u5816,negated_conjecture,
( c10_2(X0,a260)
| c7_2(X0,a261)
| c2_2(X0,a347)
| c2_2(X0,a402)
| c3_2(X0,X1)
| c2_2(X0,X1)
| c6_2(X0,X1)
| c2_2(X0,a274) ) ).
cnf(clause308,negated_conjecture,
( ~ c10_2(X0,a277)
| ssSkP7(X0) ) ).
cnf(u3963,negated_conjecture,
c1_2(a259,a344) ).
cnf(clause184,negated_conjecture,
( ssSkP13(X0)
| c6_2(X0,a305) ) ).
cnf(clause302,negated_conjecture,
( ~ c1_2(X0,a298)
| ssSkP10(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN426-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.09/0.19 % Computer : n007.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 15:54:10 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 9.91/2.12 % (2523420)Input is clausal, will run a generic CNF schedule.
% 9.91/2.12 % (2523426)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=541504667:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.91/2.12 % (2523430)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=35256733:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.91/2.12 % (2523431)dis-21_1_sil=8000:lcm=predicate:random_seed=1516294849: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)
% 9.91/2.12 % (2523425)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=3639281235:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.91/2.12 % (2523429)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=835082296:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.91/2.12 % (2523428)lrs+10_1_sil=8000:sp=occurrence:random_seed=4178573269:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.91/2.12 % (2523427)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=687343105:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.91/2.12 % (2523428)Instruction limit reached!
% 9.91/2.12 % (2523428)------------------------------
% 9.91/2.12 % (2523428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.91/2.12 % (2523428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/2.12 % (2523428)CaDiCaL version: 2.1.3
% 9.91/2.12 % (2523428)Termination reason: Instruction limit
% 9.91/2.12 % (2523428)Termination phase: Saturation
% 9.91/2.12 % (2523428)Time elapsed: 0.060 s
% 9.91/2.12 % (2523428)Peak memory usage: 91 MB
% 9.91/2.12 % (2523428)Instructions burned: 107 (million)
% 9.91/2.12 % (2523431)Instruction limit reached!
% 9.91/2.12 % (2523431)------------------------------
% 9.91/2.12 % (2523431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.91/2.12 % (2523431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/2.12 % (2523431)CaDiCaL version: 2.1.3
% 9.91/2.12 % (2523431)Termination reason: Instruction limit
% 9.91/2.12 % (2523431)Termination phase: Saturation
% 9.91/2.12 % (2523431)Time elapsed: 0.064 s
% 9.91/2.12 % (2523431)Peak memory usage: 91 MB
% 9.91/2.12 % (2523431)Instructions burned: 117 (million)
% 9.91/2.12 % (2523429)Instruction limit reached!
% 9.91/2.12 % (2523429)------------------------------
% 9.91/2.12 % (2523429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.91/2.12 % (2523429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/2.12 % (2523429)CaDiCaL version: 2.1.3
% 9.91/2.12 % (2523429)Termination reason: Instruction limit
% 9.91/2.12 % (2523429)Termination phase: Saturation
% 9.91/2.12 % (2523429)Time elapsed: 0.064 s
% 9.91/2.12 % (2523429)Peak memory usage: 90 MB
% 9.91/2.12 % (2523429)Instructions burned: 115 (million)
% 9.91/2.12 % (2523430)Refutation not found, incomplete strategy
% 9.91/2.12 % (2523430)------------------------------
% 9.91/2.12 % (2523430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.91/2.12 % (2523430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.91/2.12 % (2523430)CaDiCaL version: 2.1.3
% 9.91/2.12 % (2523430)Termination reason: Refutation not found, incomplete strategy
% 9.91/2.12 % (2523430)Time elapsed: 0.068 s
% 9.91/2.12 % (2523430)Peak memory usage: 92 MB
% 9.91/2.12 % (2523430)Instructions burned: 116 (million)
% 9.91/2.12 % (2523439)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=3166086814:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.91/2.12 % (2523441)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1203003241:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.91/2.12 % (2523440)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=98665652: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)
% 9.91/2.12 % (2523440)Refutation not found, incomplete strategy
% 9.91/2.12 % (2523440)------------------------------
% 9.91/2.12 % (2523440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523440)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523440)Termination reason: Refutation not found, incomplete strategy
% 10.21/2.30 % (2523440)Time elapsed: 0.047 s
% 10.21/2.30 % (2523440)Peak memory usage: 91 MB
% 10.21/2.30 % (2523440)Instructions burned: 84 (million)
% 10.21/2.30 % (2523430)------------------------------
% 10.21/2.30 % (2523430)------------------------------
% 10.21/2.30 % (2523439)Instruction limit reached!
% 10.21/2.30 % (2523439)------------------------------
% 10.21/2.30 % (2523439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523439)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523439)Termination reason: Instruction limit
% 10.21/2.30 % (2523439)Termination phase: Saturation
% 10.21/2.30 % (2523439)Time elapsed: 0.080 s
% 10.21/2.30 % (2523439)Peak memory usage: 91 MB
% 10.21/2.30 % (2523439)Instructions burned: 143 (million)
% 10.21/2.30 % (2523441)Instruction limit reached!
% 10.21/2.30 % (2523441)------------------------------
% 10.21/2.30 % (2523441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523441)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523441)Termination reason: Instruction limit
% 10.21/2.30 % (2523441)Termination phase: Saturation
% 10.21/2.30 % (2523441)Time elapsed: 0.119 s
% 10.21/2.30 % (2523441)Peak memory usage: 92 MB
% 10.21/2.30 % (2523441)Instructions burned: 219 (million)
% 10.21/2.30 % (2523426)Refutation not found, incomplete strategy
% 10.21/2.30 % (2523426)------------------------------
% 10.21/2.30 % (2523426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523426)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523426)Termination reason: Refutation not found, incomplete strategy
% 10.21/2.30 % (2523426)Time elapsed: 0.407 s
% 10.21/2.30 % (2523426)Peak memory usage: 137 MB
% 10.21/2.30 % (2523426)Instructions burned: 1118 (million)
% 10.21/2.30 % (2523446)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=507513154:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 10.21/2.30 % (2523445)lrs+10_64_to=lpo:sil=8000:random_seed=1093657951:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 10.21/2.30 % (2523426)------------------------------
% 10.21/2.30 % (2523426)------------------------------
% 10.21/2.30 % (2523440)------------------------------
% 10.21/2.30 % (2523440)------------------------------
% 10.21/2.30 % (2523447)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1322144424:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 10.21/2.30 % (2523445)Instruction limit reached!
% 10.21/2.30 % (2523445)------------------------------
% 10.21/2.30 % (2523445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523445)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523445)Termination reason: Instruction limit
% 10.21/2.30 % (2523445)Termination phase: Saturation
% 10.21/2.30 % (2523445)Time elapsed: 0.071 s
% 10.21/2.30 % (2523445)Peak memory usage: 91 MB
% 10.21/2.30 % (2523445)Instructions burned: 127 (million)
% 10.21/2.30 % (2523446)Refutation not found, incomplete strategy
% 10.21/2.30 % (2523446)------------------------------
% 10.21/2.30 % (2523446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523446)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523446)Termination reason: Refutation not found, incomplete strategy
% 10.21/2.30 % (2523446)Time elapsed: 0.076 s
% 10.21/2.30 % (2523446)Peak memory usage: 91 MB
% 10.21/2.30 % (2523446)Instructions burned: 128 (million)
% 10.21/2.30 % (2523447)Instruction limit reached!
% 10.21/2.30 % (2523447)------------------------------
% 10.21/2.30 % (2523447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523447)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523447)Termination reason: Instruction limit
% 10.21/2.30 % (2523447)Termination phase: Saturation
% 10.21/2.30 % (2523447)Time elapsed: 0.094 s
% 10.21/2.30 % (2523447)Peak memory usage: 92 MB
% 10.21/2.30 % (2523447)Instructions burned: 157 (million)
% 10.21/2.30 % (2523450)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=747174306:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 10.21/2.30 % (2523452)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3179167240:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 10.21/2.30 % (2523453)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2395511324:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 10.21/2.30 % (2523452)Refutation not found, incomplete strategy
% 10.21/2.30 % (2523452)------------------------------
% 10.21/2.30 % (2523452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523452)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523452)Termination reason: Refutation not found, incomplete strategy
% 10.21/2.30 % (2523452)Time elapsed: 0.032 s
% 10.21/2.30 % (2523452)Peak memory usage: 90 MB
% 10.21/2.30 % (2523452)Instructions burned: 55 (million)
% 10.21/2.30 % (2523453)Instruction limit reached!
% 10.21/2.30 % (2523453)------------------------------
% 10.21/2.30 % (2523453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523453)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523453)Termination reason: Instruction limit
% 10.21/2.30 % (2523453)Termination phase: Saturation
% 10.21/2.30 % (2523453)Time elapsed: 0.060 s
% 10.21/2.30 % (2523453)Peak memory usage: 91 MB
% 10.21/2.30 % (2523453)Instructions burned: 108 (million)
% 10.21/2.30 % (2523454)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=32980116:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 10.21/2.30 % (2523446)------------------------------
% 10.21/2.30 % (2523446)------------------------------
% 10.21/2.30 % (2523454)Refutation not found, incomplete strategy
% 10.21/2.30 % (2523454)------------------------------
% 10.21/2.30 % (2523454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523454)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523454)Termination reason: Refutation not found, incomplete strategy
% 10.21/2.30 % (2523454)Time elapsed: 0.052 s
% 10.21/2.30 % (2523454)Peak memory usage: 89 MB
% 10.21/2.30 % (2523454)Instructions burned: 98 (million)
% 10.21/2.30 % (2523458)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2768111678:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 10.21/2.30 % (2523452)------------------------------
% 10.21/2.30 % (2523452)------------------------------
% 10.21/2.30 % (2523460)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3010036643:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 10.21/2.30 % (2523460)Instruction limit reached!
% 10.21/2.30 % (2523460)------------------------------
% 10.21/2.30 % (2523460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523460)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523460)Termination reason: Instruction limit
% 10.21/2.30 % (2523460)Termination phase: Saturation
% 10.21/2.30 % (2523460)Time elapsed: 0.074 s
% 10.21/2.30 % (2523460)Peak memory usage: 91 MB
% 10.21/2.30 % (2523460)Instructions burned: 135 (million)
% 10.21/2.30 % (2523454)------------------------------
% 10.21/2.30 % (2523454)------------------------------
% 10.21/2.30 % (2523462)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4025239676:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 10.21/2.30 % (2523462)First to succeed.
% 10.21/2.30 % (2523462)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2523420"
% 10.21/2.30 % (2523464)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3476314848:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 10.21/2.30 % (2523465)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=970377436:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 10.21/2.30 % (2523464)Instruction limit reached!
% 10.21/2.30 % (2523464)------------------------------
% 10.21/2.30 % (2523464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523464)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523464)Termination reason: Instruction limit
% 10.21/2.30 % (2523464)Termination phase: Saturation
% 10.21/2.30 % (2523464)Time elapsed: 0.105 s
% 10.21/2.30 % (2523464)Peak memory usage: 93 MB
% 10.21/2.30 % (2523464)Instructions burned: 192 (million)
% 10.21/2.30 % (2523465)Instruction limit reached!
% 10.21/2.30 % (2523465)------------------------------
% 10.21/2.30 % (2523465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.21/2.30 % (2523465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.21/2.30 % (2523465)CaDiCaL version: 2.1.3
% 10.21/2.30 % (2523465)Termination reason: Instruction limit
% 10.21/2.30 % (2523465)Termination phase: Saturation
% 10.21/2.30 % (2523465)Time elapsed: 0.117 s
% 10.21/2.30 % (2523465)Peak memory usage: 91 MB
% 10.21/2.30 % (2523465)Instructions burned: 265 (million)
% 10.21/2.30 % SZS status Satisfiable for theBenchmark
% 10.21/2.30 % SZS output start Saturation.
% See solution above
% 0.20/2.50 % SZS output start Definitions and Model Updates.
% 0.20/2.50 for all inputs,
% 0.20/2.50 define c5_0 := $false
% 0.20/2.50 % SZS output end Definitions and Model Updates.
% 0.20/2.50 % (2523462)------------------------------
% 0.20/2.50 % (2523462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/2.50 % (2523462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/2.50 % (2523462)CaDiCaL version: 2.1.3
% 0.20/2.50 % (2523462)Termination reason: Satisfiable
% 0.20/2.50 % (2523462)Time elapsed: 0.061 s
% 0.20/2.50 % (2523462)Peak memory usage: 92 MB
% 0.20/2.50 % (2523462)Instructions burned: 100 (million)
% 0.20/2.50 % (2523462)------------------------------
% 0.20/2.50 % (2523462)------------------------------
% 0.20/2.50 % (2523420)Success in time 1.621 s
% 0.20/2.50 % Vampire exiting
%------------------------------------------------------------------------------