%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN418+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 : n018.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:48 PM UTC 2026
% Result : CounterSatisfiable 0.41s 0.29s
% Output : Saturation 0.41s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1576,negated_conjecture,
( c1_1(X54)
| ~ sP7(X54)
| c6_1(X54)
| c2_2(X54,X55)
| ~ c6_2(X54,X55)
| ~ c4_2(X54,X55)
| ~ ndr1_1(X54) ) ).
cnf(u1579,negated_conjecture,
ndr1_0 ).
cnf(u1585,negated_conjecture,
~ c7_0 ).
cnf(u1591,negated_conjecture,
c10_0 ).
cnf(u1597,negated_conjecture,
c8_0 ).
cnf(u1624,negated_conjecture,
c6_0 ).
cnf(u1632,negated_conjecture,
~ sP3 ).
cnf(u1636,negated_conjecture,
( ~ c6_2(a31,X27)
| ~ c2_2(a31,X27)
| ~ c1_2(a31,X27) ) ).
cnf(u1639,negated_conjecture,
ndr1_1(a31) ).
cnf(u1644,negated_conjecture,
c9_0 ).
cnf(u1651,negated_conjecture,
ndr1_1(a41) ).
cnf(u1655,negated_conjecture,
( ~ c8_2(X36,X38)
| c5_2(X36,a42)
| c2_2(X36,X37)
| ~ c7_2(X36,X37)
| ~ c3_2(X36,X37)
| ~ ndr1_1(X36)
| ~ c9_2(X36,X38) ) ).
cnf(u1659,negated_conjecture,
( ~ c8_2(X36,X38)
| ~ c4_2(X36,a42)
| c2_2(X36,X37)
| ~ c7_2(X36,X37)
| ~ c3_2(X36,X37)
| ~ ndr1_1(X36)
| ~ c9_2(X36,X38) ) ).
cnf(u1663,negated_conjecture,
( ~ c8_2(X36,X38)
| c10_2(X36,a42)
| c2_2(X36,X37)
| ~ c7_2(X36,X37)
| ~ c3_2(X36,X37)
| ~ ndr1_1(X36)
| ~ c9_2(X36,X38) ) ).
cnf(u1668,negated_conjecture,
~ c10_1(a41) ).
cnf(u1675,negated_conjecture,
~ c5_0 ).
cnf(u1681,negated_conjecture,
c3_0 ).
cnf(u1694,negated_conjecture,
( ndr1_1(X44)
| ~ sP8(X44)
| c1_1(X44)
| c7_2(X44,a49) ) ).
cnf(u1698,negated_conjecture,
( ndr1_1(X44)
| ~ sP8(X44)
| c1_1(X44)
| c3_2(X44,a49) ) ).
cnf(u1702,negated_conjecture,
( ndr1_1(X44)
| ~ sP8(X44)
| c1_1(X44)
| c5_2(X44,a49) ) ).
cnf(u1706,negated_conjecture,
( ndr1_1(X44)
| ~ sP8(X44)
| c1_1(X44) ) ).
cnf(u1710,negated_conjecture,
( ~ sP8(X44)
| ~ c1_2(X44,a50)
| c1_1(X44)
| c7_2(X44,a49) ) ).
cnf(u1714,negated_conjecture,
( ~ sP8(X44)
| ~ c1_2(X44,a50)
| c1_1(X44)
| c3_2(X44,a49) ) ).
cnf(u1718,negated_conjecture,
( ~ sP8(X44)
| ~ c1_2(X44,a50)
| c1_1(X44)
| c5_2(X44,a49) ) ).
cnf(u1722,negated_conjecture,
( ~ c1_2(X44,a50)
| ~ sP8(X44)
| c1_1(X44)
| ndr1_1(X44) ) ).
cnf(u1726,negated_conjecture,
( ~ sP8(X44)
| c8_2(X44,a50)
| c1_1(X44)
| c7_2(X44,a49) ) ).
cnf(u1730,negated_conjecture,
( ~ sP8(X44)
| c8_2(X44,a50)
| c1_1(X44)
| c3_2(X44,a49) ) ).
cnf(u1734,negated_conjecture,
( ~ sP8(X44)
| c8_2(X44,a50)
| c1_1(X44)
| c5_2(X44,a49) ) ).
cnf(u1738,negated_conjecture,
( c8_2(X44,a50)
| ~ sP8(X44)
| c1_1(X44)
| ndr1_1(X44) ) ).
cnf(u1742,negated_conjecture,
( ~ sP8(X44)
| ~ c10_2(X44,a50)
| c1_1(X44)
| c7_2(X44,a49) ) ).
cnf(u1746,negated_conjecture,
( ~ sP8(X44)
| ~ c10_2(X44,a50)
| c1_1(X44)
| c3_2(X44,a49) ) ).
cnf(u1750,negated_conjecture,
( ~ sP8(X44)
| ~ c10_2(X44,a50)
| c1_1(X44)
| c5_2(X44,a49) ) ).
cnf(u1754,negated_conjecture,
( ~ c10_2(X44,a50)
| ~ sP8(X44)
| c1_1(X44)
| ndr1_1(X44) ) ).
cnf(u1762,negated_conjecture,
( c8_2(X50,a52)
| ~ c10_2(X50,X51)
| ~ c7_2(X50,X51)
| ~ ndr1_1(X50)
| c10_1(X50) ) ).
cnf(u1766,negated_conjecture,
( ~ c9_2(X50,a52)
| ~ c10_2(X50,X51)
| ~ c7_2(X50,X51)
| ~ ndr1_1(X50)
| c10_1(X50) ) ).
cnf(u1770,negated_conjecture,
( ~ c3_2(X50,a52)
| ~ c10_2(X50,X51)
| ~ c7_2(X50,X51)
| ~ ndr1_1(X50)
| c10_1(X50) ) ).
cnf(u1777,negated_conjecture,
( c10_1(X71)
| c1_1(X71)
| ~ c8_2(X71,X72)
| ~ c10_2(X71,X72)
| ~ c7_2(X71,X72)
| ~ ndr1_1(X71) ) ).
cnf(u1817,negated_conjecture,
( ~ c5_2(X74,X76)
| c9_2(X74,X75)
| c2_2(X74,X75)
| ~ c8_2(X74,X75)
| ~ ndr1_1(X74)
| c8_1(X74)
| c7_2(X74,X76)
| ~ c6_2(X74,X76) ) ).
cnf(u1834,negated_conjecture,
ndr1_1(X79) ).
cnf(u1850,negated_conjecture,
( ~ c7_1(X84)
| ~ c5_2(X84,X85)
| c8_2(X84,X85)
| c3_2(X84,X85)
| ~ ndr1_1(X84)
| c10_1(X84) ) ).
cnf(u1883,negated_conjecture,
( ~ c3_1(X86)
| ~ c2_2(X86,X87)
| c3_2(X86,X87)
| ~ c5_2(X86,X87)
| ~ ndr1_1(X86)
| ~ c6_2(X86,a83) ) ).
cnf(u1887,negated_conjecture,
( ~ c5_1(X95)
| ~ c3_2(X95,X96)
| ~ c10_2(X95,X96)
| ~ c5_2(X95,X96)
| ~ ndr1_1(X95)
| c9_1(X95) ) ).
cnf(u1902,negated_conjecture,
( c7_1(X101)
| c9_2(X101,X102)
| ~ c6_2(X101,X102)
| ~ c8_2(X101,X102)
| ~ ndr1_1(X101)
| c3_2(X101,X103)
| c8_2(X101,X103)
| c7_2(X101,X103) ) ).
cnf(u1905,negated_conjecture,
~ c4_0 ).
cnf(u1910,negated_conjecture,
( ~ ndr1_1(X104)
| ~ c3_1(X104)
| c8_1(X104)
| ~ c7_2(X104,X105)
| c3_2(X104,X105)
| c6_2(X104,X105) ) ).
cnf(u1913,negated_conjecture,
c1_0 ).
cnf(u1922,negated_conjecture,
( c7_2(X116,X118)
| ~ c9_2(X116,X117)
| ~ c1_2(X116,X117)
| c2_2(X116,X117)
| ~ ndr1_1(X116)
| c4_1(X116)
| c8_2(X116,X118)
| ~ c9_2(X116,X118) ) ).
cnf(u1940,negated_conjecture,
( ~ ndr1_1(X122)
| c5_1(X122)
| ~ c7_2(X122,a130)
| c8_2(X122,X123)
| ~ c10_2(X122,X123)
| c6_2(X122,X123) ) ).
cnf(u1943,negated_conjecture,
c2_0 ).
cnf(u1948,negated_conjecture,
( ~ ndr1_1(X122)
| c5_1(X122)
| ~ c1_2(X122,a130)
| c8_2(X122,X123)
| ~ c10_2(X122,X123)
| c6_2(X122,X123) ) ).
cnf(u1953,negated_conjecture,
~ sP0 ).
cnf(u1972,negated_conjecture,
( ~ c4_1(X133)
| c2_2(X133,X134)
| ~ c8_2(X133,X134)
| c7_2(X133,X134)
| ~ ndr1_1(X133)
| ~ c8_1(X133) ) ).
cnf(u1976,negated_conjecture,
( ~ c7_1(X135)
| c7_2(X135,X136)
| c6_2(X135,X136)
| c8_2(X135,X136)
| ~ ndr1_1(X135) ) ).
cnf(u1983,negated_conjecture,
( ~ c1_1(X142)
| c5_1(X142)
| c8_2(X142,X143)
| ~ c6_2(X142,X143)
| ~ c2_2(X142,X143)
| ~ ndr1_1(X142) ) ).
cnf(u1990,negated_conjecture,
( c7_1(X0)
| ~ sP9(X0)
| c6_1(X0) ) ).
cnf(u1994,negated_conjecture,
( sP21(X3)
| c10_1(X3)
| c7_1(X3) ) ).
cnf(u2157,negated_conjecture,
~ sP5 ).
cnf(u2164,negated_conjecture,
( ~ c3_1(X17)
| ~ c3_2(X17,a25) ) ).
cnf(u2168,negated_conjecture,
( ~ c3_1(X17)
| c5_2(X17,a25) ) ).
cnf(u2172,negated_conjecture,
( c8_2(X17,a25)
| ~ c3_1(X17) ) ).
cnf(u2176,negated_conjecture,
( ~ c3_1(X17)
| ndr1_1(X17) ) ).
cnf(u2188,negated_conjecture,
( c6_2(a28,X23)
| c7_2(a28,X23)
| ~ c3_2(a28,X23) ) ).
cnf(u2191,negated_conjecture,
ndr1_1(a28) ).
cnf(u2196,negated_conjecture,
( c1_2(a28,X24)
| c5_2(a28,X24)
| ~ c8_2(a28,X24) ) ).
cnf(u2207,negated_conjecture,
( sP19(X29)
| sP17(X29)
| sP18(X29) ) ).
cnf(u2270,negated_conjecture,
~ sP2 ).
cnf(u2274,negated_conjecture,
( ~ c8_1(X43)
| c1_1(X43) ) ).
cnf(u2389,negated_conjecture,
( ~ c3_1(X59)
| c8_1(X59) ) ).
cnf(u2510,negated_conjecture,
ndr1_1(a66) ).
cnf(u2514,negated_conjecture,
( ndr1_1(X65)
| ~ c10_1(X65)
| ~ c8_1(X65) ) ).
cnf(u2518,negated_conjecture,
( ~ c4_2(X65,a67)
| ~ c10_1(X65)
| ~ c8_1(X65) ) ).
cnf(u2522,negated_conjecture,
( ~ c8_1(X65)
| ~ c10_1(X65)
| ~ c2_2(X65,a67) ) ).
cnf(u2526,negated_conjecture,
( ~ c8_1(X65)
| ~ c10_1(X65)
| c1_2(X65,a67) ) ).
cnf(u2539,negated_conjecture,
~ c9_1(a66) ).
cnf(u2550,negated_conjecture,
( ~ c1_1(X66)
| c3_2(X66,a70)
| sP25(X67,X66) ) ).
cnf(u2554,negated_conjecture,
( ~ c1_1(X66)
| c4_2(X66,a70)
| sP25(X67,X66) ) ).
cnf(u2558,negated_conjecture,
( ~ c1_1(X66)
| ~ c5_2(X66,a70)
| sP25(X67,X66) ) ).
cnf(u2562,negated_conjecture,
( ~ c1_1(X66)
| ndr1_1(X66)
| sP25(X67,X66) ) ).
cnf(u2606,negated_conjecture,
( ~ c4_2(a75,X80)
| ~ c5_2(a75,X80)
| c6_2(a75,X80) ) ).
cnf(u2609,negated_conjecture,
ndr1_1(a75) ).
cnf(u2630,negated_conjecture,
~ c2_1(a75) ).
cnf(u2638,negated_conjecture,
~ c9_1(a75) ).
cnf(u2693,negated_conjecture,
( ndr1_1(X88)
| sP13(X88)
| ~ c9_2(X88,a85) ) ).
cnf(u2697,negated_conjecture,
( ndr1_1(X88)
| sP13(X88)
| ~ c3_2(X88,a85) ) ).
cnf(u2701,negated_conjecture,
( ndr1_1(X88)
| sP13(X88)
| ~ c6_2(X88,a85) ) ).
cnf(u2705,negated_conjecture,
( ndr1_1(X88)
| sP13(X88) ) ).
cnf(u2709,negated_conjecture,
( c10_2(X88,a86)
| sP13(X88)
| ~ c9_2(X88,a85) ) ).
cnf(u2713,negated_conjecture,
( c10_2(X88,a86)
| sP13(X88)
| ~ c3_2(X88,a85) ) ).
cnf(u2717,negated_conjecture,
( c10_2(X88,a86)
| sP13(X88)
| ~ c6_2(X88,a85) ) ).
cnf(u2721,negated_conjecture,
( c10_2(X88,a86)
| sP13(X88)
| ndr1_1(X88) ) ).
cnf(u2725,negated_conjecture,
( ~ c2_2(X88,a86)
| sP13(X88)
| ~ c9_2(X88,a85) ) ).
cnf(u2729,negated_conjecture,
( ~ c2_2(X88,a86)
| sP13(X88)
| ~ c3_2(X88,a85) ) ).
cnf(u2733,negated_conjecture,
( ~ c2_2(X88,a86)
| sP13(X88)
| ~ c6_2(X88,a85) ) ).
cnf(u2737,negated_conjecture,
( ~ c2_2(X88,a86)
| sP13(X88)
| ndr1_1(X88) ) ).
cnf(u2741,negated_conjecture,
( ~ c8_2(X88,a86)
| sP13(X88)
| ~ c9_2(X88,a85) ) ).
cnf(u2745,negated_conjecture,
( ~ c8_2(X88,a86)
| sP13(X88)
| ~ c3_2(X88,a85) ) ).
cnf(u2749,negated_conjecture,
( ~ c8_2(X88,a86)
| sP13(X88)
| ~ c6_2(X88,a85) ) ).
cnf(u2753,negated_conjecture,
( ~ c8_2(X88,a86)
| sP13(X88)
| ndr1_1(X88) ) ).
cnf(u2812,negated_conjecture,
( ~ c10_2(X91,a92)
| ~ c8_1(X91)
| sP23(X92,X91) ) ).
cnf(u2816,negated_conjecture,
( ~ c8_1(X91)
| sP23(X92,X91)
| c9_2(X91,a92) ) ).
cnf(u2820,negated_conjecture,
( ~ c8_1(X91)
| sP23(X92,X91)
| c8_2(X91,a92) ) ).
cnf(u2824,negated_conjecture,
( sP23(X92,X91)
| ~ c8_1(X91)
| ndr1_1(X91) ) ).
cnf(u2936,negated_conjecture,
sP1 ).
cnf(u2940,negated_conjecture,
( ~ c7_2(a108,X99)
| ~ c2_2(a108,X99) ) ).
cnf(u2943,negated_conjecture,
ndr1_1(a108) ).
cnf(u3000,negated_conjecture,
( ~ c8_2(a114,X108)
| ~ c10_2(a114,X108)
| ~ c1_2(a114,X108) ) ).
cnf(u3003,negated_conjecture,
ndr1_1(a114) ).
cnf(u3069,negated_conjecture,
~ c9_1(a121) ).
cnf(u3074,negated_conjecture,
~ c6_1(a121) ).
cnf(u3079,negated_conjecture,
~ c10_1(a121) ).
cnf(u3094,negated_conjecture,
ndr1_1(a128) ).
cnf(u3099,negated_conjecture,
( ~ sP12(X124)
| ~ sP10(X124)
| ~ sP11(X124) ) ).
cnf(u3166,negated_conjecture,
( ~ c7_1(X139)
| c6_1(X139) ) ).
cnf(u3209,negated_conjecture,
~ sP6 ).
cnf(u3214,negated_conjecture,
c6_1(a1) ).
cnf(u3219,negated_conjecture,
c9_1(a1) ).
cnf(u3224,negated_conjecture,
~ c6_2(a1,a2) ).
cnf(u3229,negated_conjecture,
~ c5_2(a1,a2) ).
cnf(u3234,negated_conjecture,
c3_2(a1,a2) ).
cnf(u3239,negated_conjecture,
ndr1_1(a1) ).
cnf(u3244,negated_conjecture,
~ sP4 ).
cnf(u3249,negated_conjecture,
~ c7_1(a19) ).
cnf(u3254,negated_conjecture,
~ c8_2(a19,a21) ).
cnf(u3259,negated_conjecture,
c2_2(a19,a21) ).
cnf(u3264,negated_conjecture,
ndr1_1(a19) ).
cnf(u3269,negated_conjecture,
c4_2(a19,a20) ).
cnf(u3274,negated_conjecture,
c9_2(a19,a20) ).
cnf(u3279,negated_conjecture,
c2_2(a19,a20) ).
cnf(u3286,negated_conjecture,
~ c5_1(a31) ).
cnf(u3291,negated_conjecture,
c8_2(a31,a32) ).
cnf(u3296,negated_conjecture,
~ c3_2(a31,a32) ).
cnf(u3301,negated_conjecture,
~ c7_2(a31,a32) ).
cnf(u3307,negated_conjecture,
( ~ c4_1(X45)
| c10_1(X45) ) ).
cnf(u3414,negated_conjecture,
~ c4_1(a6) ).
cnf(u3419,negated_conjecture,
~ c6_1(a6) ).
cnf(u3424,negated_conjecture,
c10_1(a6) ).
cnf(u3560,negated_conjecture,
~ c10_1(a28) ).
cnf(u3784,negated_conjecture,
~ c10_1(a55) ).
cnf(u3792,negated_conjecture,
~ c6_1(a55) ).
cnf(u3843,negated_conjecture,
~ c2_1(a93) ).
cnf(u3848,negated_conjecture,
~ c8_1(a93) ).
cnf(u3853,negated_conjecture,
~ c2_2(a93,a94) ).
cnf(u3858,negated_conjecture,
~ c7_2(a93,a94) ).
cnf(u3863,negated_conjecture,
~ c4_2(a93,a94) ).
cnf(u3868,negated_conjecture,
ndr1_1(a93) ).
cnf(u3987,negated_conjecture,
~ c2_2(a108,a110) ).
cnf(u3992,negated_conjecture,
~ c3_2(a108,a110) ).
cnf(u3998,negated_conjecture,
~ c2_2(a108,a109) ).
cnf(u4003,negated_conjecture,
~ c1_2(a108,a109) ).
cnf(u4008,negated_conjecture,
~ c7_2(a108,a109) ).
cnf(u4015,negated_conjecture,
c4_2(a114,a115) ).
cnf(u4020,negated_conjecture,
c2_2(a114,a115) ).
cnf(u4025,negated_conjecture,
~ c5_2(a114,a115) ).
cnf(u4031,negated_conjecture,
~ c1_1(a114) ).
cnf(u4159,negated_conjecture,
~ c4_1(a128) ).
cnf(u4164,negated_conjecture,
~ c1_1(a128) ).
cnf(u4317,negated_conjecture,
~ c3_1(a114) ).
cnf(u4346,negated_conjecture,
c2_2(a1,a2) ).
cnf(u4378,negated_conjecture,
~ c8_2(a28,a130) ).
cnf(u4410,negated_conjecture,
~ c6_2(a31,a32) ).
cnf(u4420,negated_conjecture,
sP11(a31) ).
cnf(u4439,negated_conjecture,
c4_1(a19) ).
cnf(u4360,negated_conjecture,
( ~ sP21(X3)
| c10_2(X3,X4)
| ~ c3_2(X3,X4)
| c1_2(X3,X4) ) ).
cnf(u4355,negated_conjecture,
( ~ c7_2(X124,X125)
| c9_2(X124,X125)
| c6_2(X124,X125)
| sP12(X124) ) ).
cnf(u4354,negated_conjecture,
( ~ c7_2(X36,X37)
| c10_2(X36,a42)
| c2_2(X36,X37)
| ~ c8_2(X36,X38)
| ~ c3_2(X36,X37)
| ~ c9_2(X36,X38) ) ).
cnf(u66,negated_conjecture,
( ~ sP14(X60)
| c9_2(X60,a61) ) ).
cnf(u4361,negated_conjecture,
( c10_2(X0,X1)
| ~ c3_2(X0,X1)
| c1_2(X0,X1)
| c10_1(X0)
| c7_1(X0) ) ).
cnf(u63,negated_conjecture,
( ~ sP15(X60)
| c7_2(X60,a60) ) ).
cnf(u4310,negated_conjecture,
( ~ c1_2(X122,a130)
| c5_1(X122)
| c8_2(X122,X123)
| ~ c10_2(X122,X123)
| c6_2(X122,X123) ) ).
cnf(u4368,negated_conjecture,
( ~ sP23(X92,X91)
| c6_2(X91,X92)
| c4_2(X91,X92)
| ~ c8_2(X91,X92) ) ).
cnf(u88,negated_conjecture,
( ~ sP13(X88)
| ~ c8_2(X88,a84) ) ).
cnf(u4391,negated_conjecture,
( ~ c7_2(X71,X72)
| c1_1(X71)
| ~ c8_2(X71,X72)
| ~ c10_2(X71,X72)
| c10_1(X71) ) ).
cnf(u4352,negated_conjecture,
( ~ c7_2(X36,X37)
| c5_2(X36,a42)
| c2_2(X36,X37)
| ~ c8_2(X36,X38)
| ~ c3_2(X36,X37)
| ~ c9_2(X36,X38) ) ).
cnf(u4366,negated_conjecture,
( ~ sP22(X107,X106)
| c4_2(X106,X107)
| ~ c10_2(X106,X107)
| c8_2(X106,X107) ) ).
cnf(u29,negated_conjecture,
( ~ sP18(X29)
| ~ c9_2(X29,a39) ) ).
cnf(u4372,negated_conjecture,
( sP27(X33,X32)
| c6_2(X32,X33)
| ~ c8_2(X32,X33)
| c3_2(X32,X33) ) ).
cnf(u4312,negated_conjecture,
( ~ sP9(X0)
| c6_1(X0) ) ).
cnf(u4365,negated_conjecture,
( ~ c7_1(X135)
| c7_2(X135,X136)
| c6_2(X135,X136)
| c8_2(X135,X136) ) ).
cnf(u4311,negated_conjecture,
( ~ c8_1(X133)
| c2_2(X133,X134)
| ~ c8_2(X133,X134)
| c7_2(X133,X134)
| ~ c4_1(X133) ) ).
cnf(u4369,negated_conjecture,
( ~ sP24(X82,X81)
| ~ c5_2(X81,X82)
| c7_2(X81,X82)
| c1_2(X81,X82) ) ).
cnf(u1551,negated_conjecture,
( ~ sP18(X29)
| c3_2(X29,a39) ) ).
cnf(u4308,negated_conjecture,
( ~ c7_1(X84)
| ~ c5_2(X84,X85)
| c8_2(X84,X85)
| c3_2(X84,X85)
| c10_1(X84) ) ).
cnf(u31,negated_conjecture,
( ~ sP18(X29)
| ndr1_1(X29) ) ).
cnf(u62,negated_conjecture,
( ~ sP15(X60)
| ~ c9_2(X60,a60) ) ).
cnf(u4358,negated_conjecture,
( ~ c5_2(X29,X30)
| ~ c10_2(X29,X30)
| ~ c2_2(X29,X30)
| ~ sP19(X29) ) ).
cnf(u4373,negated_conjecture,
( sP28(X7,X6)
| ~ c8_2(X6,X7)
| ~ c4_2(X6,X7)
| c1_2(X6,X7) ) ).
cnf(u4359,negated_conjecture,
( ~ c7_2(X8,X9)
| ~ c1_2(X8,X9)
| ~ c2_2(X8,X9)
| sP20(X8) ) ).
cnf(u4399,negated_conjecture,
( ~ c3_1(X0)
| ~ c6_2(X0,a25)
| c7_1(X0)
| c3_2(X0,X1)
| c8_2(X0,X1)
| c7_2(X0,X1)
| c9_2(X0,a25) ) ).
cnf(u91,negated_conjecture,
( ~ sP13(X88)
| ndr1_1(X88) ) ).
cnf(u4327,negated_conjecture,
( c6_2(X124,X126)
| c9_2(X124,X126)
| c2_2(X124,X126)
| sP11(X124) ) ).
cnf(u67,negated_conjecture,
( ~ sP14(X60)
| ndr1_1(X60) ) ).
cnf(u1493,negated_conjecture,
( sP10(X124)
| ndr1_1(X124) ) ).
cnf(u4396,negated_conjecture,
( ~ c5_2(X74,X76)
| c9_2(X74,X75)
| c2_2(X74,X75)
| ~ c8_2(X74,X75)
| c8_1(X74)
| c7_2(X74,X76)
| ~ c6_2(X74,X76) ) ).
cnf(u4393,negated_conjecture,
( ~ c1_1(X142)
| c5_1(X142)
| c8_2(X142,X143)
| ~ c6_2(X142,X143)
| ~ c2_2(X142,X143) ) ).
cnf(u30,negated_conjecture,
( ~ sP18(X29)
| c2_2(X29,a39) ) ).
cnf(u1494,negated_conjecture,
( c10_2(X124,a131)
| sP10(X124) ) ).
cnf(u4357,negated_conjecture,
( ~ sP17(X29)
| c5_2(X29,X31)
| c4_2(X29,X31)
| ~ c3_2(X29,X31) ) ).
cnf(u4394,negated_conjecture,
( ~ c3_1(X86)
| ~ c2_2(X86,X87)
| c3_2(X86,X87)
| ~ c5_2(X86,X87)
| ~ c6_2(X86,a83) ) ).
cnf(u4426,negated_conjecture,
( ~ c9_2(X116,X118)
| ~ c9_2(X116,X117)
| ~ c1_2(X116,X117)
| c2_2(X116,X117)
| c4_1(X116)
| c8_2(X116,X118)
| c7_2(X116,X118) ) ).
cnf(u4397,negated_conjecture,
( ~ c8_2(X101,X102)
| c9_2(X101,X102)
| ~ c6_2(X101,X102)
| c7_1(X101)
| c3_2(X101,X103)
| c8_2(X101,X103)
| c7_2(X101,X103) ) ).
cnf(u89,negated_conjecture,
( ~ sP13(X88)
| c5_2(X88,a84) ) ).
cnf(u4395,negated_conjecture,
( ~ sP7(X54)
| c1_1(X54)
| c6_1(X54)
| c2_2(X54,X55)
| ~ c6_2(X54,X55)
| ~ c4_2(X54,X55) ) ).
cnf(u4367,negated_conjecture,
( ~ c8_1(X0)
| c1_2(X0,a92)
| c10_1(X0)
| c7_1(X0)
| ~ c3_2(X0,a92)
| sP23(X1,X0) ) ).
cnf(u4353,negated_conjecture,
( ~ c4_2(X36,a42)
| ~ c8_2(X36,X38)
| c2_2(X36,X37)
| ~ c7_2(X36,X37)
| ~ c3_2(X36,X37)
| ~ c9_2(X36,X38) ) ).
cnf(u4370,negated_conjecture,
( ~ sP25(X67,X66)
| ~ c3_2(X66,X67)
| ~ c5_2(X66,X67)
| c2_2(X66,X67) ) ).
cnf(u65,negated_conjecture,
( ~ sP14(X60)
| ~ c5_2(X60,a61) ) ).
cnf(u4371,negated_conjecture,
( sP26(X34,X32)
| ~ c2_2(X32,X34)
| ~ c9_2(X32,X34)
| c7_2(X32,X34) ) ).
cnf(u1495,negated_conjecture,
( c1_2(X124,a131)
| sP10(X124) ) ).
cnf(u4392,negated_conjecture,
( ~ c5_1(X95)
| ~ c3_2(X95,X96)
| ~ c10_2(X95,X96)
| ~ c5_2(X95,X96)
| c9_1(X95) ) ).
cnf(u1496,negated_conjecture,
( c2_2(X124,a131)
| sP10(X124) ) ).
cnf(u4364,negated_conjecture,
( ~ c3_2(X50,a52)
| ~ c10_2(X50,X51)
| ~ c7_2(X50,X51)
| c10_1(X50) ) ).
cnf(u4362,negated_conjecture,
( ~ c7_2(X50,X51)
| ~ c10_2(X50,X51)
| c8_2(X50,a52)
| c10_1(X50) ) ).
cnf(u4363,negated_conjecture,
( ~ c9_2(X50,a52)
| ~ c10_2(X50,X51)
| ~ c7_2(X50,X51)
| c10_1(X50) ) ).
cnf(u4309,negated_conjecture,
( ~ c7_2(X122,a130)
| c5_1(X122)
| c8_2(X122,X123)
| ~ c10_2(X122,X123)
| c6_2(X122,X123) ) ).
cnf(u64,negated_conjecture,
( ~ sP15(X60)
| ndr1_1(X60) ) ).
cnf(u4444,negated_conjecture,
c10_1(a19) ).
cnf(u90,negated_conjecture,
( ~ sP13(X88)
| c9_2(X88,a84) ) ).
cnf(u61,negated_conjecture,
( ~ sP15(X60)
| c5_2(X60,a60) ) ).
cnf(u4356,negated_conjecture,
( ~ sP16(X60)
| c5_2(X60,X61)
| c7_2(X60,X61)
| c1_2(X60,X61) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN418+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.09/0.17 % Computer : n018.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 15:57:25 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/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.41/0.29 % (3506362)Will run a generic schedule for satisfiability detection.
% 0.41/0.29 % (3506371)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3708859354:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.41/0.29 % (3506367)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1272051074_2999 on theBenchmark for (2999ds/0Mi)
% 0.41/0.29 % (3506370)dis+10_1_sil=32000:sp=arity:random_seed=765572720:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.41/0.29 % (3506369)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3925813978:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.41/0.29 % (3506372)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2488767076:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.41/0.29 % (3506373)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3501446598:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.41/0.29 % (3506368)% WARNING: option uhcvi not known.
% 0.41/0.29 % (3506368)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=386322878:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.41/0.29 % (3506371)Instruction limit reached!
% 0.41/0.29 % (3506371)------------------------------
% 0.41/0.29 % (3506371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.41/0.29 % (3506371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.41/0.29 % (3506371)CaDiCaL version: 2.1.3
% 0.41/0.29 % (3506371)Termination reason: Instruction limit
% 0.41/0.29 % (3506371)Termination phase: Blocked clause elimination
% 0.41/0.29 % (3506371)Time elapsed: 0.030 s
% 0.41/0.29 % (3506371)Peak memory usage: 12 MB
% 0.41/0.29 % (3506371)Instructions burned: 119 (million)
% 0.41/0.29 % Detected minimum model sizes of [1]
% 0.41/0.29 % Detected maximum model sizes of [146]
% 0.41/0.29 % TRYING [1]
% 0.41/0.29 % TRYING [2]
% 0.41/0.29 % (3506381)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2075653582:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.41/0.29 % (3506368) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3506362-3506368"...
% 0.41/0.29 % Finite Model Found!
% 0.41/0.29 % SZS status CounterSatisfiable for theBenchmark
% 0.41/0.29 % (3506368)...printing done.
% 0.41/0.29 % (3506367) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3506362-3506367"...
% 0.41/0.29 % SZS status CounterSatisfiable for theBenchmark
% 0.41/0.29 % SZS output start Saturation.
% See solution above
% 0.41/0.29 % SZS output start Definitions and Model Updates.
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP28"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP27"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP26"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP20"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP12"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP11"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP10"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP6"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP4"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP3"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP2"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "sP1"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c9_0"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c4_0"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c2_0"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c1_0"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c3_0"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c4_2"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c10_2"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c7_1"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c1_2"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c6_2"
% 0.41/0.29 globally flip the polarity of every occurrence of predicate "c3_2"
% 0.41/0.29 % SZS output end Definitions and Model Updates.
% 0.41/0.29 % (3506368)------------------------------
% 0.41/0.29 % (3506368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.41/0.29 % (3506368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.41/0.29 % (3506368)CaDiCaL version: 2.1.3
% 0.41/0.29 % (3506368)Termination reason: Satisfiable
% 0.41/0.29 % (3506368)Time elapsed: 0.031 s
% 0.41/0.29 % (3506368)Peak memory usage: 14 MB
% 0.41/0.29 % (3506368)Instructions burned: 47 (million)
% 0.41/0.29 % (3506362)Success in time 0.075 s
% 0.41/0.29 % Vampire exiting
%------------------------------------------------------------------------------