%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN422+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:07:49 PM UTC 2026
% Result : CounterSatisfiable 0.45s 0.28s
% Output : Saturation 0.45s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u790,negated_conjecture,
~ c8_1(a759) ).
cnf(u794,negated_conjecture,
c7_0 ).
cnf(u803,negated_conjecture,
~ c5_2(a759,a760) ).
cnf(u808,negated_conjecture,
c2_2(a759,a760) ).
cnf(u813,negated_conjecture,
~ c1_2(a759,a760) ).
cnf(u818,negated_conjecture,
ndr1_1(a759) ).
cnf(u822,negated_conjecture,
( ~ c6_2(a759,X125)
| c8_2(a759,X125)
| c7_2(a759,X125) ) ).
cnf(u827,negated_conjecture,
ndr1_0 ).
cnf(u832,negated_conjecture,
sP0 ).
cnf(u851,negated_conjecture,
ndr1_1(a756) ).
cnf(u860,negated_conjecture,
c6_1(a756) ).
cnf(u865,negated_conjecture,
ndr1_1(a755) ).
cnf(u873,negated_conjecture,
~ c10_0 ).
cnf(u881,negated_conjecture,
~ c6_1(a755) ).
cnf(u886,negated_conjecture,
~ c7_1(a755) ).
cnf(u890,negated_conjecture,
~ sP1 ).
cnf(u894,negated_conjecture,
~ sP2 ).
cnf(u898,negated_conjecture,
( ~ ndr1_1(X119)
| c2_2(X119,a751)
| c7_1(X119)
| ~ c8_2(X119,X120)
| c9_2(X119,X120)
| ~ c6_2(X119,X120) ) ).
cnf(u902,negated_conjecture,
( ~ ndr1_1(X119)
| c3_2(X119,a751)
| c7_1(X119)
| ~ c8_2(X119,X120)
| c9_2(X119,X120)
| ~ c6_2(X119,X120) ) ).
cnf(u907,negated_conjecture,
c6_0 ).
cnf(u910,negated_conjecture,
~ c2_0 ).
cnf(u914,negated_conjecture,
~ c4_0 ).
cnf(u919,negated_conjecture,
( ~ c2_1(X118)
| c9_1(X118) ) ).
cnf(u923,negated_conjecture,
~ sP4 ).
cnf(u927,negated_conjecture,
( ~ ndr1_1(X116)
| c10_2(X116,a748)
| c10_2(X116,X117)
| c5_2(X116,X117)
| c3_2(X116,X117)
| c8_1(X116) ) ).
cnf(u931,negated_conjecture,
( ~ ndr1_1(X116)
| c1_2(X116,a748)
| c10_2(X116,X117)
| c5_2(X116,X117)
| c3_2(X116,X117)
| c8_1(X116) ) ).
cnf(u935,negated_conjecture,
( ~ ndr1_1(X116)
| ~ c4_2(X116,a748)
| c10_2(X116,X117)
| c5_2(X116,X117)
| c3_2(X116,X117)
| c8_1(X116) ) ).
cnf(u939,negated_conjecture,
( ~ c2_1(X114)
| c9_2(X114,a747)
| ~ ndr1_1(X114)
| c5_2(X114,X115)
| c3_2(X114,X115)
| ~ c1_2(X114,X115) ) ).
cnf(u943,negated_conjecture,
( ~ c2_1(X114)
| ~ c1_2(X114,a747)
| ~ ndr1_1(X114)
| c5_2(X114,X115)
| c3_2(X114,X115)
| ~ c1_2(X114,X115) ) ).
cnf(u947,negated_conjecture,
( ~ c2_1(X114)
| c5_2(X114,a747)
| ~ ndr1_1(X114)
| c5_2(X114,X115)
| c3_2(X114,X115)
| ~ c1_2(X114,X115) ) ).
cnf(u952,negated_conjecture,
c8_0 ).
cnf(u985,negated_conjecture,
( ~ ndr1_1(X111)
| sP5(X111)
| ~ c10_2(X111,a743)
| c6_2(X111,X112)
| ~ c3_2(X111,X112)
| ~ c1_2(X111,X112) ) ).
cnf(u988,negated_conjecture,
~ sP6 ).
cnf(u993,negated_conjecture,
( ~ ndr1_1(X111)
| sP5(X111)
| ~ c9_2(X111,a743)
| c6_2(X111,X112)
| ~ c3_2(X111,X112)
| ~ c1_2(X111,X112) ) ).
cnf(u1001,negated_conjecture,
c9_0 ).
cnf(u1005,negated_conjecture,
~ sP7 ).
cnf(u1010,negated_conjecture,
~ c7_1(a739) ).
cnf(u1015,negated_conjecture,
~ c5_1(a739) ).
cnf(u1020,negated_conjecture,
~ c2_1(a739) ).
cnf(u1026,negated_conjecture,
~ c4_1(a737) ).
cnf(u1029,negated_conjecture,
~ sP8 ).
cnf(u1035,negated_conjecture,
c9_1(a737) ).
cnf(u1040,negated_conjecture,
c1_2(a737,a738) ).
cnf(u1045,negated_conjecture,
~ c4_2(a737,a738) ).
cnf(u1050,negated_conjecture,
c9_2(a737,a738) ).
cnf(u1055,negated_conjecture,
ndr1_1(a737) ).
cnf(u1060,negated_conjecture,
~ sP10 ).
cnf(u1076,negated_conjecture,
~ sP11 ).
cnf(u1081,negated_conjecture,
c1_1(a728) ).
cnf(u1086,negated_conjecture,
c6_1(a728) ).
cnf(u1091,negated_conjecture,
( ~ ndr1_1(X105)
| ~ c10_1(X105)
| ~ c4_1(X105)
| ~ c8_2(X105,X106)
| c3_2(X105,X106)
| ~ c4_2(X105,X106) ) ).
cnf(u1094,negated_conjecture,
~ sP12 ).
cnf(u1134,negated_conjecture,
~ sP13 ).
cnf(u1150,negated_conjecture,
~ sP15 ).
cnf(u1154,negated_conjecture,
~ sP16 ).
cnf(u1158,negated_conjecture,
( ~ c10_1(X96)
| sP14(X96)
| ~ c7_2(X96,a718) ) ).
cnf(u1162,negated_conjecture,
( ~ c10_1(X96)
| sP14(X96)
| ~ c8_2(X96,a718) ) ).
cnf(u1166,negated_conjecture,
( ~ c10_1(X96)
| sP14(X96)
| ndr1_1(X96) ) ).
cnf(u1182,negated_conjecture,
( ~ c6_1(X92)
| ~ c1_1(X92)
| ~ ndr1_1(X92)
| ~ c5_2(X92,X93)
| c7_2(X92,X93) ) ).
cnf(u1194,negated_conjecture,
sP19 ).
cnf(u1197,negated_conjecture,
( ~ c9_2(X89,a712)
| sP18(X89) ) ).
cnf(u1205,negated_conjecture,
( ~ c4_2(X89,a712)
| sP18(X89) ) ).
cnf(u1218,negated_conjecture,
~ c5_0 ).
cnf(u1237,negated_conjecture,
( ~ ndr1_1(X82)
| ~ c8_1(X82)
| ~ c5_2(X82,X84)
| ~ c7_2(X82,X84)
| c4_2(X82,X84)
| ~ c2_2(X82,X83)
| ~ c9_2(X82,X83)
| c1_2(X82,X83) ) ).
cnf(u1272,negated_conjecture,
~ c5_1(a708) ).
cnf(u1275,negated_conjecture,
~ sP20 ).
cnf(u1280,negated_conjecture,
ndr1_1(a708) ).
cnf(u1284,negated_conjecture,
( ~ c5_2(a708,X81)
| c7_2(a708,X81)
| c10_2(a708,X81) ) ).
cnf(u1289,negated_conjecture,
~ sP21 ).
cnf(u1294,negated_conjecture,
~ c3_1(a705) ).
cnf(u1298,negated_conjecture,
ndr1_1(a705) ).
cnf(u1307,negated_conjecture,
~ c9_1(a705) ).
cnf(u1312,negated_conjecture,
( ~ ndr1_1(X77)
| c10_2(X77,X79)
| ~ c1_2(X77,X79)
| c4_2(X77,X79)
| c1_1(X77)
| c6_2(X77,X78)
| ~ c8_2(X77,X78)
| c4_2(X77,X78) ) ).
cnf(u1315,negated_conjecture,
~ sP22 ).
cnf(u1334,negated_conjecture,
~ sP23 ).
cnf(u1339,negated_conjecture,
~ c10_1(a700) ).
cnf(u1344,negated_conjecture,
~ c9_1(a700) ).
cnf(u1349,negated_conjecture,
~ c7_1(a700) ).
cnf(u1355,negated_conjecture,
c9_1(a698) ).
cnf(u1359,negated_conjecture,
~ c2_1(a698) ).
cnf(u1365,negated_conjecture,
c1_2(a698,a699) ).
cnf(u1370,negated_conjecture,
~ c5_2(a698,a699) ).
cnf(u1375,negated_conjecture,
ndr1_1(a698) ).
cnf(u1380,negated_conjecture,
~ sP24 ).
cnf(u1389,negated_conjecture,
c3_0 ).
cnf(u1406,negated_conjecture,
~ sP25 ).
cnf(u1422,negated_conjecture,
ndr1_1(a690) ).
cnf(u1426,negated_conjecture,
( c7_2(a690,X75)
| c4_2(a690,X75)
| c2_2(a690,X75) ) ).
cnf(u1434,negated_conjecture,
c2_1(a690) ).
cnf(u1439,negated_conjecture,
~ c10_2(a690,a691) ).
cnf(u1444,negated_conjecture,
~ c9_2(a690,a691) ).
cnf(u1449,negated_conjecture,
~ c5_2(a690,a691) ).
cnf(u1473,negated_conjecture,
( ~ c3_1(X71)
| ~ c9_2(X71,X72)
| ~ c8_1(X71)
| ~ ndr1_1(X71)
| ~ c10_2(X71,X72)
| c6_2(X71,X72) ) ).
cnf(u1477,negated_conjecture,
( ~ c10_1(X69)
| ~ ndr1_1(X69)
| ~ c3_2(X69,X70)
| c5_2(X69,X70)
| ~ c8_2(X69,X70)
| ~ c8_1(X69) ) ).
cnf(u1483,negated_conjecture,
sP26 ).
cnf(u1526,negated_conjecture,
~ sP29 ).
cnf(u1548,negated_conjecture,
( ~ c6_1(X62)
| c3_1(X62)
| ~ c2_1(X62) ) ).
cnf(u1552,negated_conjecture,
( sP31(X61)
| sP30(X61)
| c8_2(X61,a675) ) ).
cnf(u1556,negated_conjecture,
( ~ c1_2(X61,a675)
| sP30(X61)
| sP31(X61) ) ).
cnf(u1560,negated_conjecture,
( sP31(X61)
| sP30(X61)
| c5_2(X61,a675) ) ).
cnf(u1564,negated_conjecture,
( ndr1_1(X61)
| sP30(X61)
| sP31(X61) ) ).
cnf(u1611,negated_conjecture,
~ sP32 ).
cnf(u1616,negated_conjecture,
c8_1(a670) ).
cnf(u1621,negated_conjecture,
c9_1(a670) ).
cnf(u1626,negated_conjecture,
~ c3_1(a670) ).
cnf(u1632,negated_conjecture,
~ sP33 ).
cnf(u1637,negated_conjecture,
~ c9_1(a668) ).
cnf(u1641,negated_conjecture,
ndr1_1(a668) ).
cnf(u1645,negated_conjecture,
( ~ c8_2(a668,X57)
| ~ c3_2(a668,X57)
| c2_2(a668,X57) ) ).
cnf(u1649,negated_conjecture,
( ~ c4_2(a668,X56)
| c1_2(a668,X56) ) ).
cnf(u1666,negated_conjecture,
~ sP34 ).
cnf(u1670,negated_conjecture,
ndr1_1(a665) ).
cnf(u1679,negated_conjecture,
~ c2_1(a665) ).
cnf(u1693,negated_conjecture,
~ sP35 ).
cnf(u1697,negated_conjecture,
( ~ ndr1_1(X47)
| ~ c9_1(X47)
| ~ c10_1(X47)
| ~ c8_2(X47,X48)
| ~ c7_2(X47,X48)
| c1_2(X47,X48) ) ).
cnf(u1718,negated_conjecture,
~ sP37 ).
cnf(u1723,negated_conjecture,
~ c6_1(a660) ).
cnf(u1728,negated_conjecture,
~ c10_1(a660) ).
cnf(u1733,negated_conjecture,
c5_1(a660) ).
cnf(u1745,negated_conjecture,
( ~ c4_1(X41)
| c7_1(X41)
| ~ c7_2(X41,a659) ) ).
cnf(u1749,negated_conjecture,
( ~ c4_1(X41)
| c7_1(X41)
| ~ c5_2(X41,a659) ) ).
cnf(u1753,negated_conjecture,
( ~ c4_1(X41)
| c7_1(X41)
| ~ c8_2(X41,a659) ) ).
cnf(u1757,negated_conjecture,
( c7_1(X41)
| ~ c4_1(X41)
| ndr1_1(X41) ) ).
cnf(u1761,negated_conjecture,
ndr1_1(a658) ).
cnf(u1765,negated_conjecture,
( ~ c3_2(a658,X40)
| ~ c4_2(a658,X40)
| ~ c5_2(a658,X40) ) ).
cnf(u1770,negated_conjecture,
c7_1(a658) ).
cnf(u1777,negated_conjecture,
sP38 ).
cnf(u1780,negated_conjecture,
ndr1_1(a655) ).
cnf(u1793,negated_conjecture,
c2_1(a655) ).
cnf(u1813,negated_conjecture,
~ sP39 ).
cnf(u1818,negated_conjecture,
~ c7_1(a651) ).
cnf(u1823,negated_conjecture,
~ c9_1(a651) ).
cnf(u1828,negated_conjecture,
~ c5_1(a651) ).
cnf(u1832,negated_conjecture,
~ sP40 ).
cnf(u1856,negated_conjecture,
c3_1(a648) ).
cnf(u1861,negated_conjecture,
~ c7_1(a648) ).
cnf(u1865,negated_conjecture,
ndr1_1(a648) ).
cnf(u1869,negated_conjecture,
( ~ c7_2(a648,X30)
| ~ c3_2(a648,X30) ) ).
cnf(u1874,negated_conjecture,
sP41 ).
cnf(u1877,negated_conjecture,
~ sP42 ).
cnf(u1886,negated_conjecture,
( ~ ndr1_1(X27)
| ~ c9_2(X27,X29)
| ~ c3_2(X27,X29)
| ~ c10_2(X27,X29)
| c10_1(X27)
| ~ c8_2(X27,X28)
| ~ c6_2(X27,X28)
| ~ c3_2(X27,X28) ) ).
cnf(u1961,negated_conjecture,
( ~ c6_1(X15)
| ~ c8_1(X15)
| ~ c8_2(X15,X16)
| ~ ndr1_1(X15)
| c1_2(X15,X16)
| c4_2(X15,X16) ) ).
cnf(u1968,negated_conjecture,
~ sP44 ).
cnf(u2014,negated_conjecture,
~ sP45 ).
cnf(u2018,negated_conjecture,
( ~ c7_1(X12)
| ~ c8_1(X12)
| ~ c2_2(X12,a627) ) ).
cnf(u2022,negated_conjecture,
( ~ c7_1(X12)
| ~ c8_1(X12)
| ~ c5_2(X12,a627) ) ).
cnf(u2026,negated_conjecture,
( ~ c7_1(X12)
| ~ c8_1(X12)
| ~ c10_2(X12,a627) ) ).
cnf(u2030,negated_conjecture,
( ~ c7_1(X12)
| ~ c8_1(X12)
| ndr1_1(X12) ) ).
cnf(u2034,negated_conjecture,
~ sP46 ).
cnf(u2050,negated_conjecture,
~ sP47 ).
cnf(u2054,negated_conjecture,
ndr1_1(a621) ).
cnf(u2058,negated_conjecture,
( ~ c2_2(a621,X10)
| c6_2(a621,X10)
| c1_2(a621,X10) ) ).
cnf(u2063,negated_conjecture,
c1_1(a621) ).
cnf(u2068,negated_conjecture,
~ c3_1(a621) ).
cnf(u2103,negated_conjecture,
~ sP48 ).
cnf(u2108,negated_conjecture,
~ c10_1(a617) ).
cnf(u2113,negated_conjecture,
c9_1(a617) ).
cnf(u2118,negated_conjecture,
c5_1(a617) ).
cnf(u2123,negated_conjecture,
~ sP49 ).
cnf(u2131,negated_conjecture,
~ sP50 ).
cnf(u2144,negated_conjecture,
~ sP51 ).
cnf(u2149,negated_conjecture,
~ c8_1(a609) ).
cnf(u2154,negated_conjecture,
~ c10_1(a609) ).
cnf(u2159,negated_conjecture,
~ c5_1(a609) ).
cnf(u2181,axiom,
c4_1(a758) ).
cnf(u2186,axiom,
c8_1(a758) ).
cnf(u2191,axiom,
c1_1(a758) ).
cnf(u2337,axiom,
ndr1_1(a733) ).
cnf(u2350,axiom,
~ c4_1(a733) ).
cnf(u2446,axiom,
( c6_2(X0,X1)
| ~ c8_1(X0)
| ~ c5_2(X0,a714)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u2450,axiom,
( c6_2(X0,X1)
| ~ c8_1(X0)
| c7_2(X0,a714)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u2454,axiom,
( c6_2(X0,X1)
| ~ c8_1(X0)
| c3_2(X0,a714)
| ~ ndr1_1(X0)
| c8_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u2596,axiom,
c2_2(a686,a688) ).
cnf(u2601,axiom,
c4_2(a686,a688) ).
cnf(u2606,axiom,
ndr1_1(a686) ).
cnf(u2611,axiom,
c8_1(a686) ).
cnf(u2616,axiom,
~ c8_2(a686,a687) ).
cnf(u2621,axiom,
c4_2(a686,a687) ).
cnf(u2626,axiom,
~ c1_2(a686,a687) ).
cnf(u2685,axiom,
ndr1_1(a669) ).
cnf(u2694,axiom,
~ c2_1(a669) ).
cnf(u2749,axiom,
c1_1(a656) ).
cnf(u2754,axiom,
c7_1(a656) ).
cnf(u2759,axiom,
c3_2(a656,a657) ).
cnf(u2764,axiom,
c6_2(a656,a657) ).
cnf(u2769,axiom,
ndr1_1(a656) ).
cnf(u2822,axiom,
c5_2(a645,a647) ).
cnf(u2827,axiom,
~ c3_2(a645,a647) ).
cnf(u2832,axiom,
~ c9_2(a645,a647) ).
cnf(u2837,axiom,
ndr1_1(a645) ).
cnf(u2842,axiom,
~ c5_2(a645,a646) ).
cnf(u2847,axiom,
~ c3_2(a645,a646) ).
cnf(u2852,axiom,
~ c9_2(a645,a646) ).
cnf(u2857,axiom,
( ~ c9_2(a645,X0)
| ~ c2_2(a645,X0)
| ~ c5_2(a645,X0) ) ).
cnf(u3161,negated_conjecture,
~ c2_1(a756) ).
cnf(u3197,negated_conjecture,
~ c4_1(a698) ).
cnf(u3201,negated_conjecture,
~ c10_1(a698) ).
cnf(u3213,negated_conjecture,
~ c10_1(a759) ).
cnf(u3236,negated_conjecture,
~ c9_1(a759) ).
cnf(u3272,negated_conjecture,
~ c10_1(a737) ).
cnf(u3300,negated_conjecture,
~ c2_1(a728) ).
cnf(u3318,negated_conjecture,
~ c8_1(a728) ).
cnf(u3330,negated_conjecture,
~ c8_1(a648) ).
cnf(u3364,negated_conjecture,
~ c8_1(a756) ).
cnf(u3371,negated_conjecture,
~ c2_2(a658,a627) ).
cnf(u3375,negated_conjecture,
~ c8_1(a658) ).
cnf(u3395,negated_conjecture,
~ c1_1(a756) ).
cnf(u3401,negated_conjecture,
~ c10_1(a670) ).
cnf(u3410,negated_conjecture,
~ c5_2(a670,a714) ).
cnf(u3413,negated_conjecture,
( ~ c7_2(a670,X0)
| c6_2(a670,X0)
| c8_2(a670,X0) ) ).
cnf(u3428,negated_conjecture,
( ~ c8_2(a759,X0)
| ~ c6_2(a759,X0)
| c9_2(a759,X0) ) ).
cnf(u3440,negated_conjecture,
( ~ c8_2(a737,X0)
| ~ c6_2(a737,X0)
| c9_2(a737,X0) ) ).
cnf(u3448,negated_conjecture,
c2_2(a737,a751) ).
cnf(u3452,negated_conjecture,
( ~ c8_2(a698,X0)
| ~ c6_2(a698,X0)
| c9_2(a698,X0) ) ).
cnf(u3479,negated_conjecture,
c8_1(a737) ).
cnf(u3490,negated_conjecture,
~ c8_1(a698) ).
cnf(u3494,negated_conjecture,
( c10_2(a698,X0)
| c3_2(a698,X0)
| c5_2(a698,X0) ) ).
cnf(u3502,negated_conjecture,
( c10_2(a759,X0)
| c3_2(a759,X0)
| c5_2(a759,X0) ) ).
cnf(u3518,negated_conjecture,
( ~ c7_2(a737,X0)
| c6_2(a737,X0)
| c8_2(a737,X0) ) ).
cnf(u3546,negated_conjecture,
( ~ c1_2(a690,X0)
| c5_2(a690,X0)
| c3_2(a690,X0) ) ).
cnf(u3566,negated_conjecture,
c9_2(a655,a747) ).
cnf(u3574,negated_conjecture,
~ c1_2(a655,a747) ).
cnf(u3582,negated_conjecture,
c5_2(a655,a747) ).
cnf(u3593,negated_conjecture,
c10_2(a759,a743) ).
cnf(u3598,negated_conjecture,
sP5(a759) ).
cnf(u3606,negated_conjecture,
~ c10_2(a737,a743) ).
cnf(u3618,negated_conjecture,
~ c10_2(a698,a743) ).
cnf(u3631,negated_conjecture,
~ c9_2(a759,a743) ).
cnf(u3636,negated_conjecture,
~ c9_2(a737,a743) ).
cnf(u3641,negated_conjecture,
~ c9_2(a698,a743) ).
cnf(u3649,negated_conjecture,
~ c7_2(a758,a659) ).
cnf(u3658,negated_conjecture,
~ c5_2(a758,a659) ).
cnf(u3663,negated_conjecture,
~ c8_2(a758,a659) ).
cnf(u3672,negated_conjecture,
~ c10_1(a758) ).
cnf(u3680,negated_conjecture,
~ c5_2(a758,a714) ).
cnf(u3688,negated_conjecture,
c7_2(a758,a714) ).
cnf(u3693,negated_conjecture,
c3_2(a758,a714) ).
cnf(u3704,negated_conjecture,
~ c10_1(a686) ).
cnf(u3712,negated_conjecture,
~ c5_2(a686,a714) ).
cnf(u3720,negated_conjecture,
c7_2(a686,a714) ).
cnf(u3725,negated_conjecture,
c3_2(a686,a714) ).
cnf(u3734,negated_conjecture,
~ c2_2(a656,a627) ).
cnf(u3737,negated_conjecture,
c8_1(a656) ).
cnf(u3743,negated_conjecture,
~ c5_2(a656,a627) ).
cnf(u3748,negated_conjecture,
~ c10_2(a656,a627) ).
cnf(u3767,negated_conjecture,
( ~ c7_2(a737,X0)
| c4_2(a737,X0)
| ~ c5_2(a737,X0) ) ).
cnf(u3779,negated_conjecture,
c1_1(a759) ).
cnf(u3786,negated_conjecture,
( ~ c8_2(a737,X1)
| c4_2(a737,X1)
| c6_2(a737,X1) ) ).
cnf(u3801,negated_conjecture,
c1_1(a698) ).
cnf(u3815,negated_conjecture,
( ~ c8_2(a759,X1)
| ~ c3_2(a759,X1)
| ~ c6_2(a759,X1) ) ).
cnf(u3822,negated_conjecture,
( ~ c8_2(a737,X1)
| ~ c3_2(a737,X1)
| ~ c6_2(a737,X1) ) ).
cnf(u3829,negated_conjecture,
( ~ c8_2(a698,X1)
| ~ c3_2(a698,X1)
| ~ c6_2(a698,X1) ) ).
cnf(u3845,negated_conjecture,
c3_2(a698,a743) ).
cnf(u3880,negated_conjecture,
( c10_2(a756,X0)
| c3_2(a756,X0)
| c5_2(a756,X0) ) ).
cnf(u3888,negated_conjecture,
( c10_2(a728,X0)
| c3_2(a728,X0)
| c5_2(a728,X0) ) ).
cnf(u3893,negated_conjecture,
c10_2(a658,a748) ).
cnf(u3896,negated_conjecture,
( c10_2(a658,X0)
| c3_2(a658,X0)
| c5_2(a658,X0) ) ).
cnf(u3912,negated_conjecture,
( c10_2(a648,X0)
| c3_2(a648,X0)
| c5_2(a648,X0) ) ).
cnf(u3920,negated_conjecture,
( c10_2(a609,X0)
| c3_2(a609,X0)
| c5_2(a609,X0) ) ).
cnf(u3929,negated_conjecture,
~ c10_1(a656) ).
cnf(u3940,negated_conjecture,
( ~ c7_2(a656,X0)
| c6_2(a656,X0)
| c8_2(a656,X0) ) ).
cnf(u3984,negated_conjecture,
~ c6_2(a759,a712) ).
cnf(u4006,negated_conjecture,
c9_2(a737,a713) ).
cnf(u4025,negated_conjecture,
~ c6_2(a698,a712) ).
cnf(u4043,negated_conjecture,
~ c3_2(a668,a712) ).
cnf(u4152,negated_conjecture,
~ c6_2(a759,a676) ).
cnf(u4174,negated_conjecture,
~ c6_2(a737,a676) ).
cnf(u4187,negated_conjecture,
c4_2(a737,a676) ).
cnf(u4201,negated_conjecture,
~ c6_2(a698,a676) ).
cnf(u4223,negated_conjecture,
~ c3_2(a668,a676) ).
cnf(u4240,negated_conjecture,
c6_2(a759,a744) ).
cnf(u4245,negated_conjecture,
c9_2(a759,a744) ).
cnf(u4256,negated_conjecture,
~ c3_2(a759,a744) ).
cnf(u4304,negated_conjecture,
c3_2(a756,a743) ).
cnf(u4316,negated_conjecture,
c5_2(a728,a743) ).
cnf(u4332,negated_conjecture,
c5_2(a658,a743) ).
cnf(u4359,negated_conjecture,
sP5(a648) ).
cnf(u4375,negated_conjecture,
sP5(a609) ).
cnf(u4399,negated_conjecture,
( ~ c7_2(a758,X0)
| c4_2(a758,X0)
| ~ c5_2(a758,X0) ) ).
cnf(u4403,negated_conjecture,
( ~ c9_2(a686,X1)
| c1_2(a686,X1)
| ~ c2_2(a686,X1) ) ).
cnf(u4410,negated_conjecture,
( ~ c9_2(a670,X1)
| c1_2(a670,X1)
| ~ c2_2(a670,X1) ) ).
cnf(u4417,negated_conjecture,
( ~ c9_2(a656,X1)
| c1_2(a656,X1)
| ~ c2_2(a656,X1) ) ).
cnf(u4445,negated_conjecture,
~ c9_2(a658,a748) ).
cnf(u4487,negated_conjecture,
c3_2(a690,a714) ).
cnf(u4506,negated_conjecture,
c7_2(a690,a714) ).
cnf(u4530,negated_conjecture,
~ c5_2(a690,a714) ).
cnf(u4559,negated_conjecture,
c1_2(a690,a748) ).
cnf(u4562,negated_conjecture,
( ~ c9_2(a690,X1)
| c1_2(a690,X1)
| ~ c2_2(a690,X1) ) ).
cnf(u4576,negated_conjecture,
~ c3_2(a690,a748) ).
cnf(u4589,negated_conjecture,
c5_2(a690,a748) ).
cnf(u4620,negated_conjecture,
c4_2(a690,a748) ).
cnf(u4626,negated_conjecture,
c8_1(a690) ).
cnf(u4639,negated_conjecture,
~ c10_1(a690) ).
cnf(u377,axiom,
( ~ sP9(X0)
| ~ c3_2(X0,a732) ) ).
cnf(u4377,negated_conjecture,
c9_2(a648,a744) ).
cnf(u3863,negated_conjecture,
( ~ c7_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a748)
| c6_2(X0,X2)
| c7_2(X0,a714)
| c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u3320,negated_conjecture,
( ~ c8_1(X69)
| ~ c3_2(X69,X70)
| c5_2(X69,X70)
| ~ c8_2(X69,X70)
| ~ c10_1(X69) ) ).
cnf(u3954,negated_conjecture,
( ~ c9_2(X0,a676)
| sP30(X0)
| c5_2(X0,a675) ) ).
cnf(u3144,negated_conjecture,
c9_1(a655) ).
cnf(u3126,negated_conjecture,
( ~ c10_1(X96)
| ndr1_1(X96) ) ).
cnf(u3962,negated_conjecture,
( ~ c9_2(X0,a677)
| c8_2(X0,a676)
| c8_2(X0,a675) ) ).
cnf(u288,axiom,
( ~ sP28(X0)
| ndr1_1(X0) ) ).
cnf(u250,axiom,
( ~ sP36(X0)
| ndr1_1(X0) ) ).
cnf(u287,axiom,
( ~ sP28(X0)
| c6_2(X0,a683) ) ).
cnf(u249,axiom,
( ~ sP36(X0)
| ~ c6_2(X0,a662) ) ).
cnf(u4272,negated_conjecture,
( ~ c6_2(X0,a676)
| c5_2(X0,a675)
| c7_1(X0)
| c2_2(X0,a751)
| c9_2(X0,a676)
| c2_2(X0,a677) ) ).
cnf(u401,axiom,
( ~ sP5(X0)
| c9_2(X0,a744) ) ).
cnf(u4470,negated_conjecture,
( ~ c1_2(X0,X1)
| c5_2(X0,a675)
| c5_2(X0,a677)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a676)
| c10_2(X0,X1)
| c4_2(X0,a676) ) ).
cnf(u3957,negated_conjecture,
( ~ c5_2(X0,a676)
| sP30(X0)
| c5_2(X0,a675) ) ).
cnf(u4460,negated_conjecture,
( ~ c6_2(X0,a676)
| c8_2(X0,a675)
| c7_1(X0)
| c3_2(X0,a751)
| c9_2(X0,a676)
| c5_2(X0,a677) ) ).
cnf(u353,axiom,
( ~ sP14(X0)
| c2_2(X0,a719) ) ).
cnf(u203,axiom,
( ~ sP43(X0)
| ndr1_1(X0) ) ).
cnf(u4383,negated_conjecture,
c9_2(a609,a744) ).
cnf(u4388,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c9_2(X0,X2)
| c1_2(X0,X2)
| c10_2(X0,X3)
| c5_2(X0,X3)
| c3_2(X0,X3)
| c10_2(X0,a748) ) ).
cnf(u3864,negated_conjecture,
( ~ c7_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a748)
| c6_2(X0,X2)
| ~ c5_2(X0,a714)
| c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u376,axiom,
( ~ sP9(X0)
| c4_2(X0,a732) ) ).
cnf(u3965,negated_conjecture,
( c8_2(X0,a676)
| c5_2(X0,a677)
| c5_2(X0,a675) ) ).
cnf(u3323,negated_conjecture,
( ~ c8_1(X0)
| c6_2(X0,X1)
| c3_2(X0,a714)
| c8_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u3952,negated_conjecture,
( sP30(X0)
| c8_2(X0,a676)
| c5_2(X0,a675) ) ).
cnf(u343,axiom,
( ~ sP17(X0)
| c3_2(X0,a716) ) ).
cnf(u4471,negated_conjecture,
( ~ c6_2(X0,a676)
| c5_2(X0,a675)
| c7_1(X0)
| c3_2(X0,a751)
| c9_2(X0,a676)
| c5_2(X0,a677) ) ).
cnf(u4143,negated_conjecture,
( ~ c6_2(X0,a676)
| c8_2(X0,a675)
| c7_1(X0)
| c3_2(X0,a751)
| c9_2(X0,a676)
| c2_2(X0,a677) ) ).
cnf(u3322,negated_conjecture,
( ~ c8_1(X0)
| c6_2(X0,X1)
| c7_2(X0,a714)
| c8_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u3953,negated_conjecture,
( sP30(X0)
| c8_2(X0,a676)
| c8_2(X0,a675) ) ).
cnf(u3471,negated_conjecture,
( c8_1(X0)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a748) ) ).
cnf(u4422,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a676)
| c10_2(X0,X1)
| c4_2(X0,a676)
| c2_2(X0,a677)
| c5_2(X0,a675) ) ).
cnf(u3769,negated_conjecture,
( ~ c8_2(X0,X2)
| ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,X2)
| c10_2(X0,X1)
| c4_2(X0,X2) ) ).
cnf(u410,axiom,
( ~ sP3(X0)
| ndr1_1(X0) ) ).
cnf(u3806,negated_conjecture,
( ~ c10_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c9_2(X0,X1)
| c10_1(X0)
| ~ c8_2(X0,X2)
| ~ c6_2(X0,X2)
| ~ c3_2(X0,X2) ) ).
cnf(u202,axiom,
( ~ sP43(X0)
| ~ c4_2(X0,a636) ) ).
cnf(u3335,negated_conjecture,
( ~ c10_1(X0)
| ~ c9_1(X0)
| ~ c8_2(X0,X1)
| ~ c7_2(X0,X1)
| c1_2(X0,X1) ) ).
cnf(u201,axiom,
( ~ sP43(X0)
| c10_2(X0,a636) ) ).
cnf(u4378,negated_conjecture,
c6_2(a648,a744) ).
cnf(u344,axiom,
( ~ sP17(X0)
| c2_2(X0,a716) ) ).
cnf(u4387,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ c5_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c9_2(X0,X2)
| c1_2(X0,X2)
| c10_2(X0,X3)
| c5_2(X0,X3)
| c3_2(X0,X3)
| c1_2(X0,a748) ) ).
cnf(u338,axiom,
( ~ sP18(X0)
| c9_2(X0,a713) ) ).
cnf(u3530,negated_conjecture,
( c8_1(X0)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,a748) ) ).
cnf(u340,axiom,
( ~ sP18(X0)
| ~ c6_2(X0,a713) ) ).
cnf(u271,axiom,
( ~ sP30(X0)
| c2_2(X0,a677) ) ).
cnf(u4271,negated_conjecture,
( ~ c6_2(X0,a676)
| c5_2(X0,a675)
| c7_1(X0)
| c3_2(X0,a751)
| c9_2(X0,a676)
| c2_2(X0,a677) ) ).
cnf(u407,axiom,
( ~ sP3(X0)
| ~ c10_2(X0,a750) ) ).
cnf(u290,axiom,
( ~ sP27(X0)
| c3_2(X0,a685) ) ).
cnf(u4472,negated_conjecture,
( ~ c6_2(X0,a676)
| c5_2(X0,a675)
| c7_1(X0)
| c2_2(X0,a751)
| c9_2(X0,a676)
| c5_2(X0,a677) ) ).
cnf(u292,axiom,
( ~ sP27(X0)
| ndr1_1(X0) ) ).
cnf(u409,axiom,
( ~ sP3(X0)
| c2_2(X0,a750) ) ).
cnf(u4379,negated_conjecture,
c8_2(a648,a744) ).
cnf(u286,axiom,
( ~ sP28(X0)
| ~ c4_2(X0,a683) ) ).
cnf(u3462,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_1(X0)
| c3_2(X0,a751)
| c9_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u4276,negated_conjecture,
( ~ c10_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,a748)
| ~ c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u4425,negated_conjecture,
c7_2(a728,a743) ).
cnf(u3964,negated_conjecture,
( c8_2(X0,a676)
| c5_2(X0,a677)
| c8_2(X0,a675) ) ).
cnf(u355,axiom,
( ~ sP14(X0)
| ~ c7_2(X0,a719) ) ).
cnf(u3321,negated_conjecture,
( ~ c8_1(X0)
| c6_2(X0,X1)
| ~ c5_2(X0,a714)
| c8_2(X0,X1)
| ~ c7_2(X0,X1) ) ).
cnf(u3534,negated_conjecture,
( ~ c4_2(X0,a748)
| c10_2(X0,X1)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c8_1(X0) ) ).
cnf(u3336,negated_conjecture,
( ~ c4_1(X0)
| ~ c10_1(X0)
| ~ c8_2(X0,X1)
| c3_2(X0,X1)
| ~ c4_2(X0,X1) ) ).
cnf(u272,axiom,
( ~ sP30(X0)
| ~ c9_2(X0,a677) ) ).
cnf(u247,axiom,
( ~ sP36(X0)
| ~ c2_2(X0,a662) ) ).
cnf(u399,axiom,
( ~ sP5(X0)
| c8_2(X0,a744) ) ).
cnf(u3422,negated_conjecture,
( ~ c8_2(X0,X1)
| c7_1(X0)
| c2_2(X0,a751)
| c9_2(X0,X1)
| ~ c6_2(X0,X1) ) ).
cnf(u268,axiom,
( ~ sP31(X0)
| ~ c9_2(X0,a676) ) ).
cnf(u400,axiom,
( ~ sP5(X0)
| c6_2(X0,a744) ) ).
cnf(u4461,negated_conjecture,
( ~ c6_2(X0,a676)
| c8_2(X0,a675)
| c7_1(X0)
| c2_2(X0,a751)
| c9_2(X0,a676)
| c5_2(X0,a677) ) ).
cnf(u289,axiom,
( ~ sP27(X0)
| ~ c6_2(X0,a685) ) ).
cnf(u285,axiom,
( ~ sP28(X0)
| c5_2(X0,a683) ) ).
cnf(u4459,negated_conjecture,
( ~ c1_2(X0,X1)
| c8_2(X0,a675)
| c5_2(X0,a677)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a676)
| c10_2(X0,X1)
| c4_2(X0,a676) ) ).
cnf(u3624,negated_conjecture,
( ~ c1_2(X0,X1)
| ~ c9_2(X0,a743)
| c6_2(X0,X1)
| ~ c3_2(X0,X1)
| sP5(X0) ) ).
cnf(u3961,negated_conjecture,
( c8_2(X0,a676)
| c2_2(X0,a677)
| c5_2(X0,a675) ) ).
cnf(u342,axiom,
( ~ sP17(X0)
| c1_2(X0,a716) ) ).
cnf(u3388,negated_conjecture,
( ~ c5_2(a728,X0)
| c7_2(a728,X0) ) ).
cnf(u3958,negated_conjecture,
( ~ c5_2(X0,a676)
| sP30(X0)
| c8_2(X0,a675) ) ).
cnf(u3865,negated_conjecture,
( ~ c10_1(X0)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a748)
| ~ c3_2(X0,X2)
| c5_2(X0,X2)
| ~ c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u3960,negated_conjecture,
( c8_2(X0,a676)
| c2_2(X0,a677)
| c8_2(X0,a675) ) ).
cnf(u248,axiom,
( ~ sP36(X0)
| c10_2(X0,a662) ) ).
cnf(u4275,negated_conjecture,
( ~ c7_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,a748)
| c6_2(X0,X2)
| ~ c5_2(X0,a714)
| c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u274,axiom,
( ~ sP30(X0)
| ndr1_1(X0) ) ).
cnf(u270,axiom,
( ~ sP31(X0)
| ndr1_1(X0) ) ).
cnf(u4385,negated_conjecture,
c8_2(a609,a744) ).
cnf(u4423,negated_conjecture,
( ~ c1_2(X0,X1)
| c4_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a676)
| c10_2(X0,X1)
| c4_2(X0,a676)
| c2_2(X0,a677)
| c8_2(X0,a675) ) ).
cnf(u4274,negated_conjecture,
( ~ c7_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,a748)
| c6_2(X0,X2)
| c7_2(X0,a714)
| c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u4144,negated_conjecture,
( ~ c6_2(X0,a676)
| c8_2(X0,a675)
| c7_1(X0)
| c2_2(X0,a751)
| c9_2(X0,a676)
| c2_2(X0,a677) ) ).
cnf(u345,axiom,
( ~ sP17(X0)
| ndr1_1(X0) ) ).
cnf(u339,axiom,
( ~ sP18(X0)
| ~ c10_2(X0,a713) ) ).
cnf(u341,axiom,
( ~ sP18(X0)
| ndr1_1(X0) ) ).
cnf(u3324,negated_conjecture,
c9_1(a690) ).
cnf(u291,axiom,
( ~ sP27(X0)
| c10_2(X0,a685) ) ).
cnf(u3584,negated_conjecture,
( ~ c10_2(X0,a743)
| sP5(X0)
| c6_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ c1_2(X0,X1) ) ).
cnf(u3750,negated_conjecture,
( ~ c8_1(X0)
| ~ c5_2(X0,X1)
| ~ c7_2(X0,X1)
| c4_2(X0,X1)
| ~ c2_2(X0,X2)
| ~ c9_2(X0,X2)
| c1_2(X0,X2) ) ).
cnf(u3260,negated_conjecture,
ndr1_1(X61) ).
cnf(u3963,negated_conjecture,
( ~ c9_2(X0,a677)
| c8_2(X0,a676)
| c5_2(X0,a675) ) ).
cnf(u4384,negated_conjecture,
c6_2(a609,a744) ).
cnf(u378,axiom,
( ~ sP9(X0)
| ndr1_1(X0) ) ).
cnf(u408,axiom,
( ~ sP3(X0)
| ~ c8_2(X0,a750) ) ).
cnf(u402,axiom,
( ~ sP5(X0)
| ndr1_1(X0) ) ).
cnf(u4233,negated_conjecture,
c8_2(a759,a744) ).
cnf(u200,axiom,
( ~ sP43(X0)
| c8_2(X0,a636) ) ).
cnf(u3862,negated_conjecture,
( ~ c7_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c10_2(X0,a748)
| c6_2(X0,X2)
| c3_2(X0,a714)
| c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u354,axiom,
( ~ sP14(X0)
| ~ c4_2(X0,a719) ) ).
cnf(u3955,negated_conjecture,
( ~ c9_2(X0,a676)
| sP30(X0)
| c8_2(X0,a675) ) ).
cnf(u356,axiom,
( ~ sP14(X0)
| ndr1_1(X0) ) ).
cnf(u273,axiom,
( ~ sP30(X0)
| c5_2(X0,a677) ) ).
cnf(u4273,negated_conjecture,
( ~ c7_2(X0,X2)
| c5_2(X0,X1)
| c3_2(X0,X1)
| c1_2(X0,a748)
| c6_2(X0,X2)
| c3_2(X0,a714)
| c8_2(X0,X2)
| c10_2(X0,X1) ) ).
cnf(u267,axiom,
( ~ sP31(X0)
| c8_2(X0,a676) ) ).
cnf(u269,axiom,
( ~ sP31(X0)
| ~ c5_2(X0,a676) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN422+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.17 % Computer : n002.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 15:58:07 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20 Running first-order model finding
% 0.07/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.45/0.28 % (475476)Will run a generic schedule for satisfiability detection.
% 0.45/0.28 % (475487)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1116473089:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.45/0.28 % (475481)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=783897155_2999 on theBenchmark for (2999ds/0Mi)
% 0.45/0.28 % (475483)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3218471670:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.45/0.28 % (475482)% WARNING: option uhcvi not known.
% 0.45/0.28 % (475484)dis+10_1_sil=32000:sp=arity:random_seed=2263067063:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.45/0.28 % (475485)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3050134458:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.45/0.28 % (475486)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3928915491:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.45/0.28 % (475482)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=184764517:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.45/0.28 % Detected minimum model sizes of [1]
% 0.45/0.28 % Detected maximum model sizes of [153]
% 0.45/0.28 % TRYING [1]
% 0.45/0.28 % TRYING [2]
% 0.45/0.28 % (475486) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-475476-475486"...
% 0.45/0.28 % (475487)Instruction limit reached!
% 0.45/0.28 % (475487)------------------------------
% 0.45/0.28 % (475487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.28 % (475487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.28 % (475487)CaDiCaL version: 2.1.3
% 0.45/0.28 % (475487)Termination reason: Instruction limit
% 0.45/0.28 % (475487)Termination phase: Saturation
% 0.45/0.28 % (475487)Time elapsed: 0.047 s
% 0.45/0.28 % (475487)Peak memory usage: 16 MB
% 0.45/0.28 % (475487)Instructions burned: 160 (million)
% 0.45/0.28 % (475486)...printing done.
% 0.45/0.28 % Finite Model Found!
% 0.45/0.28 % SZS status CounterSatisfiable for theBenchmark
% 0.45/0.28 % SZS status CounterSatisfiable for theBenchmark
% 0.45/0.28 % SZS output start Saturation.
% See solution above
% 0.45/0.29 % SZS output start Definitions and Model Updates.
% 0.45/0.29 % SZS output end Definitions and Model Updates.
% 0.45/0.29 % (475486)------------------------------
% 0.45/0.29 % (475486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.29 % (475486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.29 % (475486)CaDiCaL version: 2.1.3
% 0.45/0.29 % (475486)Termination reason: Satisfiable
% 0.45/0.29 % (475486)Time elapsed: 0.040 s
% 0.45/0.29 % (475486)Peak memory usage: 14 MB
% 0.45/0.29 % (475486)Instructions burned: 67 (million)
% 0.45/0.29 % (475476)Success in time 0.078 s
% 0.45/0.29 % Vampire exiting
%------------------------------------------------------------------------------