%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN547+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 02:17:33 PM UTC 2026
% Result : CounterSatisfiable 0.07s 0.29s
% Output : Saturation 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1351,negated_conjecture,
~ sP7 ).
cnf(u1357,negated_conjecture,
~ ndr1_0 ).
cnf(u1367,negated_conjecture,
~ sP2 ).
cnf(u1374,negated_conjecture,
~ c8_0 ).
cnf(u1382,negated_conjecture,
( ~ c6_1(X1)
| ndr1_1(X1)
| c2_1(X1)
| c3_2(X1,X2)
| ~ c7_2(X1,X2) ) ).
cnf(u1400,negated_conjecture,
~ c2_0 ).
cnf(u1404,negated_conjecture,
~ c6_0 ).
cnf(u1416,negated_conjecture,
( ~ c1_2(X9,a465)
| ~ c6_2(X9,X10)
| c5_2(X9,X10)
| ~ c7_2(X9,X10)
| ndr1_1(X9)
| ~ c8_1(X9) ) ).
cnf(u1426,negated_conjecture,
( ~ c6_2(X9,X10)
| ~ c8_1(X9)
| c5_2(X9,X10)
| ~ c7_2(X9,X10)
| ndr1_1(X9)
| ~ c5_2(X9,a465) ) ).
cnf(u1430,negated_conjecture,
( ~ c7_2(X9,a465)
| ~ c6_2(X9,X10)
| c5_2(X9,X10)
| ~ c7_2(X9,X10)
| ndr1_1(X9)
| ~ c8_1(X9) ) ).
cnf(u1437,negated_conjecture,
( c8_1(X17)
| ~ ndr1_1(X17)
| ~ c6_1(X17) ) ).
cnf(u1441,negated_conjecture,
( ~ c6_1(X17)
| c8_2(X17,a467)
| c8_1(X17) ) ).
cnf(u1445,negated_conjecture,
( ~ c2_2(X17,a467)
| c8_1(X17)
| ~ c6_1(X17) ) ).
cnf(u1449,negated_conjecture,
( c3_2(X17,a467)
| c8_1(X17)
| ~ c6_1(X17) ) ).
cnf(u1466,negated_conjecture,
c7_0 ).
cnf(u1491,negated_conjecture,
( ~ c7_1(X27)
| c6_1(X27)
| ndr1_1(X27)
| c1_2(X27,X28)
| ~ c4_2(X27,X28)
| ~ c6_2(X27,X28) ) ).
cnf(u1514,negated_conjecture,
c1_0 ).
cnf(u1538,negated_conjecture,
( ~ ndr1_1(X47)
| sP9(X47)
| sP18(X47)
| ~ c7_2(X47,a492) ) ).
cnf(u1542,negated_conjecture,
( ~ ndr1_1(X47)
| sP9(X47)
| sP18(X47)
| ~ c6_2(X47,a492) ) ).
cnf(u1546,negated_conjecture,
( ~ ndr1_1(X47)
| sP9(X47)
| sP18(X47)
| ~ c4_2(X47,a492) ) ).
cnf(u1550,negated_conjecture,
( ~ ndr1_1(X47)
| sP9(X47)
| sP18(X47) ) ).
cnf(u1554,negated_conjecture,
( ~ c6_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c7_2(X47,a492) ) ).
cnf(u1558,negated_conjecture,
( ~ c6_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c6_2(X47,a492) ) ).
cnf(u1562,negated_conjecture,
( ~ c6_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c4_2(X47,a492) ) ).
cnf(u1566,negated_conjecture,
( ~ c6_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ ndr1_1(X47) ) ).
cnf(u1570,negated_conjecture,
( c1_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c7_2(X47,a492) ) ).
cnf(u1574,negated_conjecture,
( c1_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c6_2(X47,a492) ) ).
cnf(u1578,negated_conjecture,
( c1_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c4_2(X47,a492) ) ).
cnf(u1582,negated_conjecture,
( c1_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ ndr1_1(X47) ) ).
cnf(u1586,negated_conjecture,
( c2_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c7_2(X47,a492) ) ).
cnf(u1590,negated_conjecture,
( c2_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c6_2(X47,a492) ) ).
cnf(u1594,negated_conjecture,
( c2_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ c4_2(X47,a492) ) ).
cnf(u1598,negated_conjecture,
( c2_2(X47,a493)
| sP9(X47)
| sP18(X47)
| ~ ndr1_1(X47) ) ).
cnf(u1610,negated_conjecture,
c8_1(a501) ).
cnf(u1618,negated_conjecture,
~ c6_1(a501) ).
cnf(u1623,negated_conjecture,
~ c5_1(a501) ).
cnf(u1627,negated_conjecture,
( ~ c4_1(X59)
| ndr1_1(X59)
| c4_2(X59,X60)
| ~ c3_2(X59,X60)
| ~ c7_2(X59,X60) ) ).
cnf(u1640,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| ~ c3_2(X62,a515)
| ~ ndr1_1(X62) ) ).
cnf(u1644,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| c7_2(X62,a515)
| ~ ndr1_1(X62) ) ).
cnf(u1648,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| c2_2(X62,a515)
| ~ ndr1_1(X62) ) ).
cnf(u1652,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| ~ ndr1_1(X62) ) ).
cnf(u1656,negated_conjecture,
( ~ c3_2(X62,a515)
| sP8(X62)
| ~ sP19(X63,X62)
| ~ c6_2(X62,a516) ) ).
cnf(u1660,negated_conjecture,
( ~ c6_2(X62,a516)
| sP8(X62)
| c7_2(X62,a515)
| ~ sP19(X63,X62) ) ).
cnf(u1664,negated_conjecture,
( ~ c6_2(X62,a516)
| sP8(X62)
| c2_2(X62,a515)
| ~ sP19(X63,X62) ) ).
cnf(u1668,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| ~ ndr1_1(X62)
| ~ c6_2(X62,a516) ) ).
cnf(u1672,negated_conjecture,
( ~ c3_2(X62,a515)
| sP8(X62)
| ~ sP19(X63,X62)
| c2_2(X62,a516) ) ).
cnf(u1676,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| c7_2(X62,a515)
| c2_2(X62,a516) ) ).
cnf(u1680,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| c2_2(X62,a515)
| c2_2(X62,a516) ) ).
cnf(u1684,negated_conjecture,
( ~ sP19(X63,X62)
| sP8(X62)
| ~ ndr1_1(X62)
| c2_2(X62,a516) ) ).
cnf(u1688,negated_conjecture,
( ~ c4_1(X65)
| ~ c8_1(X65)
| ndr1_1(X65)
| c3_2(X65,X66)
| ~ c6_2(X65,X66)
| c4_2(X65,X66) ) ).
cnf(u1711,negated_conjecture,
c5_0 ).
cnf(u1727,negated_conjecture,
( ~ c5_1(X78)
| c3_2(X78,X79)
| ~ c8_2(X78,X79)
| ~ c1_2(X78,X79)
| ndr1_1(X78)
| ~ c7_2(X78,X80)
| c3_2(X78,X80)
| c6_2(X78,X80) ) ).
cnf(u1749,negated_conjecture,
~ c3_1(a533) ).
cnf(u1770,negated_conjecture,
( ~ c6_2(X84,X85)
| ~ c1_2(X84,X85)
| ~ c3_2(X84,X85)
| c6_1(X84)
| ndr1_1(X84)
| c1_2(X84,X86)
| c7_2(X84,X86)
| c2_2(X84,X86) ) ).
cnf(u1799,negated_conjecture,
sP6 ).
cnf(u1803,negated_conjecture,
( c5_2(a536,X87)
| c3_2(a536,X87)
| ~ c7_2(a536,X87) ) ).
cnf(u1818,negated_conjecture,
( ~ c5_1(X107)
| ~ c6_1(X107)
| ~ c3_1(X107) ) ).
cnf(u1834,negated_conjecture,
( ~ c2_2(X108,X109)
| c8_1(X108)
| c7_2(X108,X109)
| c2_2(X108,X110)
| c8_2(X108,X109)
| ndr1_1(X108)
| c3_2(X108,X110)
| ~ c6_2(X108,X110) ) ).
cnf(u1859,negated_conjecture,
sP3 ).
cnf(u1870,negated_conjecture,
( ~ c6_2(X116,a572)
| ~ c2_2(X116,X117)
| c5_2(X116,X117)
| ndr1_1(X116)
| ~ c4_1(X116) ) ).
cnf(u1874,negated_conjecture,
( ~ c4_1(X116)
| ~ c2_2(X116,X117)
| c5_2(X116,X117)
| ndr1_1(X116)
| ~ c5_2(X116,a572) ) ).
cnf(u1878,negated_conjecture,
( c5_2(X116,X117)
| ~ c2_2(X116,X117)
| ~ c4_1(X116)
| ndr1_1(X116)
| ~ c2_2(X116,a572) ) ).
cnf(u1889,negated_conjecture,
( ~ c2_2(X119,X121)
| ~ c8_1(X119)
| c5_2(X119,X120)
| ~ c4_2(X119,X120)
| ~ c7_2(X119,X120)
| ndr1_1(X119)
| c1_2(X119,X121)
| ~ c3_2(X119,X121) ) ).
cnf(u1907,negated_conjecture,
( ~ c5_1(X123)
| ~ c6_1(X123)
| ndr1_1(X123)
| c8_2(X123,X124)
| c7_2(X123,X124)
| c6_2(X123,X124) ) ).
cnf(u1935,negated_conjecture,
~ sP1 ).
cnf(u1939,negated_conjecture,
( ~ c8_2(X129,a576)
| c7_1(X129)
| ~ c1_1(X129) ) ).
cnf(u1943,negated_conjecture,
( ~ c4_2(X129,a576)
| c7_1(X129)
| ~ c1_1(X129) ) ).
cnf(u1947,negated_conjecture,
( ~ c1_1(X129)
| c7_1(X129)
| ~ ndr1_1(X129) ) ).
cnf(u1970,negated_conjecture,
( ~ c6_2(X135,X136)
| c4_1(X135)
| c7_2(X135,X136)
| c2_2(X135,X136)
| c7_1(X135)
| ndr1_1(X135) ) ).
cnf(u1989,negated_conjecture,
( ~ c8_2(a587,X140)
| sP12(X140)
| ~ c5_2(a587,X140)
| c1_2(a587,X140) ) ).
cnf(u2002,negated_conjecture,
~ sP0 ).
cnf(u2013,negated_conjecture,
( ~ c8_2(X154,X155)
| c4_1(X154)
| c1_2(X154,X155)
| c3_2(X154,X155)
| ndr1_1(X154)
| ~ c8_1(X154) ) ).
cnf(u2084,negated_conjecture,
( c7_2(X3,a459)
| ~ c3_1(X3)
| c8_1(X3) ) ).
cnf(u2091,negated_conjecture,
( ~ c3_2(X3,a459)
| ~ c3_1(X3)
| c8_1(X3) ) ).
cnf(u2095,negated_conjecture,
( ~ c6_2(X3,a459)
| ~ c3_1(X3)
| c8_1(X3) ) ).
cnf(u2099,negated_conjecture,
( ~ c3_1(X3)
| ~ ndr1_1(X3)
| c8_1(X3) ) ).
cnf(u2207,negated_conjecture,
( c5_2(a475,X31)
| ~ c8_2(a475,X31)
| ~ c4_2(a475,X31) ) ).
cnf(u2210,negated_conjecture,
~ ndr1_1(a475) ).
cnf(u2215,negated_conjecture,
( ~ c7_2(X34,a479)
| sP14(X34)
| c8_1(X34) ) ).
cnf(u2218,negated_conjecture,
( ~ c2_1(X36)
| ~ ndr1_1(X36)
| c3_1(X36) ) ).
cnf(u2222,negated_conjecture,
( c6_2(X34,a479)
| sP14(X34)
| c8_1(X34) ) ).
cnf(u2230,negated_conjecture,
( c3_2(X36,a480)
| ~ c2_1(X36)
| c3_1(X36) ) ).
cnf(u2236,negated_conjecture,
( ~ c4_2(X36,a480)
| ~ c2_1(X36)
| c3_1(X36) ) ).
cnf(u2242,negated_conjecture,
( ~ c6_2(X36,a480)
| ~ c2_1(X36)
| c3_1(X36) ) ).
cnf(u2248,negated_conjecture,
( ~ c2_2(a482,X39)
| ~ c8_2(a482,X39)
| ~ c6_2(a482,X39) ) ).
cnf(u2251,negated_conjecture,
~ ndr1_1(a482) ).
cnf(u2320,negated_conjecture,
( ~ c4_2(X41,a487)
| ~ c2_1(X41)
| ~ c5_1(X41) ) ).
cnf(u2328,negated_conjecture,
( c1_2(X41,a487)
| ~ c2_1(X41)
| ~ c5_1(X41) ) ).
cnf(u2332,negated_conjecture,
( ~ c5_1(X41)
| ~ c2_1(X41)
| ~ ndr1_1(X41) ) ).
cnf(u2376,negated_conjecture,
~ sP9(X47) ).
cnf(u2420,negated_conjecture,
( ~ c8_2(a514,X61)
| c6_2(a514,X61)
| c4_2(a514,X61) ) ).
cnf(u2460,negated_conjecture,
ndr1_1(a530) ).
cnf(u2515,negated_conjecture,
sP5 ).
cnf(u2522,negated_conjecture,
~ sP4 ).
cnf(u2526,negated_conjecture,
( ~ c2_1(X93)
| c8_1(X93) ) ).
cnf(u2586,negated_conjecture,
( sP13(X97)
| ~ c1_1(X97)
| ~ ndr1_1(X97) ) ).
cnf(u2590,negated_conjecture,
( ~ c2_2(X97,a548)
| sP13(X97)
| ~ c1_1(X97) ) ).
cnf(u2594,negated_conjecture,
( c4_2(X97,a548)
| sP13(X97)
| ~ c1_1(X97) ) ).
cnf(u2598,negated_conjecture,
( ~ c7_2(X97,a548)
| sP13(X97)
| ~ c1_1(X97) ) ).
cnf(u2638,negated_conjecture,
( ~ c2_2(a552,X99)
| c6_2(a552,X99)
| c8_2(a552,X99) ) ).
cnf(u2649,negated_conjecture,
( c2_2(X100,a553)
| ~ c4_1(X100)
| c5_1(X100) ) ).
cnf(u2653,negated_conjecture,
( c7_2(X100,a553)
| ~ c4_1(X100)
| c5_1(X100) ) ).
cnf(u2657,negated_conjecture,
( ~ c3_2(X100,a553)
| ~ c4_1(X100)
| c5_1(X100) ) ).
cnf(u2662,negated_conjecture,
c6_1(a552) ).
cnf(u2670,negated_conjecture,
c8_1(a552) ).
cnf(u2747,negated_conjecture,
c6_1(a565) ).
cnf(u2752,negated_conjecture,
c3_1(a565) ).
cnf(u2757,negated_conjecture,
c2_1(a565) ).
cnf(u2793,negated_conjecture,
( ~ c2_2(a581,X133)
| c7_2(a581,X133)
| c8_2(a581,X133) ) ).
cnf(u2797,negated_conjecture,
ndr1_1(a581) ).
cnf(u2818,negated_conjecture,
( ~ sP17(X144,X143)
| ~ sP16(X145,X143)
| c6_1(X143) ) ).
cnf(u2886,negated_conjecture,
ndr1_1(a592) ).
cnf(u2913,negated_conjecture,
~ c6_1(a592) ).
cnf(u2928,negated_conjecture,
~ c5_1(a601) ).
cnf(u2933,negated_conjecture,
~ c1_1(a601) ).
cnf(u2938,negated_conjecture,
c7_1(a601) ).
cnf(u2972,negated_conjecture,
~ c5_1(a536) ).
cnf(u2977,negated_conjecture,
~ c7_1(a536) ).
cnf(u3050,negated_conjecture,
c8_1(a466) ).
cnf(u3055,negated_conjecture,
c1_1(a466) ).
cnf(u3071,negated_conjecture,
c7_2(a475,a477) ).
cnf(u3076,negated_conjecture,
c6_2(a475,a477) ).
cnf(u3081,negated_conjecture,
~ c4_2(a475,a477) ).
cnf(u3087,negated_conjecture,
c7_2(a475,a476) ).
cnf(u3092,negated_conjecture,
~ c3_2(a475,a476) ).
cnf(u3097,negated_conjecture,
c5_2(a475,a476) ).
cnf(u3104,negated_conjecture,
c4_2(a482,a484) ).
cnf(u3109,negated_conjecture,
~ c6_2(a482,a484) ).
cnf(u3114,negated_conjecture,
c5_2(a482,a484) ).
cnf(u3120,negated_conjecture,
c8_2(a482,a483) ).
cnf(u3125,negated_conjecture,
~ c2_2(a482,a483) ).
cnf(u3130,negated_conjecture,
c3_2(a482,a483) ).
cnf(u3211,negated_conjecture,
~ c5_1(a514) ).
cnf(u3221,negated_conjecture,
~ c1_1(a514) ).
cnf(u3287,negated_conjecture,
~ c1_2(a520,a521) ).
cnf(u3292,negated_conjecture,
~ c2_2(a520,a521) ).
cnf(u3297,negated_conjecture,
c4_2(a520,a521) ).
cnf(u3302,negated_conjecture,
~ ndr1_1(a520) ).
cnf(u3307,negated_conjecture,
~ c2_1(a520) ).
cnf(u3312,negated_conjecture,
c5_1(a520) ).
cnf(u3516,negated_conjecture,
c3_2(a570,a571) ).
cnf(u3521,negated_conjecture,
c1_2(a570,a571) ).
cnf(u3526,negated_conjecture,
~ c2_2(a570,a571) ).
cnf(u3531,negated_conjecture,
~ ndr1_1(a570) ).
cnf(u3536,negated_conjecture,
~ c5_1(a570) ).
cnf(u3541,negated_conjecture,
c4_1(a570) ).
cnf(u3584,negated_conjecture,
~ c8_1(a581) ).
cnf(u3589,negated_conjecture,
~ c6_1(a581) ).
cnf(u3751,negated_conjecture,
~ c3_1(a520) ).
cnf(u3755,negated_conjecture,
~ c6_1(a520) ).
cnf(u3789,negated_conjecture,
~ c4_1(a482) ).
cnf(u3838,negated_conjecture,
sP15(a570) ).
cnf(u3859,negated_conjecture,
c4_2(a482,a483) ).
cnf(u3869,negated_conjecture,
c5_2(a570,a572) ).
cnf(u3873,negated_conjecture,
( c5_2(a570,X0)
| ~ c2_2(a570,X0) ) ).
cnf(u3880,negated_conjecture,
~ ndr1_1(a466) ).
cnf(u3919,negated_conjecture,
( c1_2(a601,X0)
| ~ c6_2(a601,X0)
| ~ c4_2(a601,X0) ) ).
cnf(u3922,negated_conjecture,
~ ndr1_1(a601) ).
cnf(u3939,negated_conjecture,
~ c8_1(a570) ).
cnf(u3962,negated_conjecture,
c5_2(a475,a465) ).
cnf(u3971,negated_conjecture,
~ c8_1(a475) ).
cnf(u3977,negated_conjecture,
( ~ c7_2(a520,X1)
| c6_2(a520,X1)
| c3_2(a520,X1) ) ).
cnf(u4029,negated_conjecture,
~ c3_2(a475,a477) ).
cnf(u4049,negated_conjecture,
~ c8_1(a601) ).
cnf(u4081,negated_conjecture,
~ c8_2(a482,a479) ).
cnf(u4105,negated_conjecture,
sP10(a475) ).
cnf(u4140,negated_conjecture,
( ~ c7_2(a552,X0)
| c3_2(a552,X0) ) ).
cnf(u4162,negated_conjecture,
~ c4_1(a552) ).
cnf(u4171,negated_conjecture,
sP15(a552) ).
cnf(u4191,negated_conjecture,
sP10(a570) ).
cnf(u4202,negated_conjecture,
c2_2(a475,a477) ).
cnf(u4262,negated_conjecture,
c8_1(a587) ).
cnf(u4265,negated_conjecture,
~ c3_2(a587,a479) ).
cnf(u4273,negated_conjecture,
c2_2(a587,a479) ).
cnf(u4277,negated_conjecture,
~ sP14(a514) ).
cnf(u4282,negated_conjecture,
sP15(a514) ).
cnf(u4316,negated_conjecture,
~ c7_2(a587,a479) ).
cnf(u3810,negated_conjecture,
( c5_2(X0,X1)
| c7_2(X0,a515)
| c2_2(X0,a516)
| c4_2(X0,X1)
| sP8(X0)
| ndr1_1(X0) ) ).
cnf(u3811,negated_conjecture,
( c5_2(X0,X1)
| c2_2(X0,a515)
| c2_2(X0,a516)
| c4_2(X0,X1)
| sP8(X0)
| ndr1_1(X0) ) ).
cnf(u3803,negated_conjecture,
( c1_2(X47,a493)
| sP18(X47)
| ~ c7_2(X47,a492) ) ).
cnf(u3800,negated_conjecture,
( ~ c7_2(X47,a492)
| sP18(X47)
| ~ c6_2(X47,a493) ) ).
cnf(u3743,negated_conjecture,
c8_1(a565) ).
cnf(u4195,negated_conjecture,
( c2_2(X0,a479)
| c8_2(X0,X1)
| c7_2(X0,X1)
| ndr1_1(X0)
| c3_2(X0,a479)
| c8_1(X0)
| c4_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0) ) ).
cnf(u3806,negated_conjecture,
( ~ c7_2(X47,a492)
| sP18(X47)
| c2_2(X47,a493) ) ).
cnf(u4494,negated_conjecture,
( ~ c6_2(X0,X3)
| c4_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X2)
| sP10(X0)
| c4_2(X0,X1)
| c8_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X3)
| c3_2(X0,X3)
| c2_2(X0,a479) ) ).
cnf(u1339,negated_conjecture,
( c5_2(X141,X142)
| ndr1_1(X141)
| c2_2(X141,X142)
| sP11(X141) ) ).
cnf(u3824,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_2(X0,X1)
| ndr1_1(X0)
| sP15(X0)
| c4_2(X0,X1)
| sP10(X0) ) ).
cnf(u3915,negated_conjecture,
( c4_2(X0,a467)
| ~ c6_1(X0)
| c8_1(X0)
| c6_2(X0,a467)
| sP15(X0) ) ).
cnf(u4372,negated_conjecture,
( c2_2(X0,a479)
| c4_2(X0,X2)
| c8_2(X0,X1)
| c8_1(X0)
| c6_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X1)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0) ) ).
cnf(u4250,negated_conjecture,
( c2_2(X0,a479)
| c4_2(X0,X1)
| c2_2(X0,X2)
| c3_2(X0,a479)
| c8_1(X0)
| c7_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X2)
| ndr1_1(X0)
| c6_1(X0)
| c8_2(X0,X2) ) ).
cnf(u1345,negated_conjecture,
( c2_2(X7,X8)
| c4_2(X7,X8)
| c6_2(X7,X8)
| ndr1_1(X7)
| sP15(X7) ) ).
cnf(u4570,negated_conjecture,
( ~ sP18(X0)
| c2_2(X0,a479)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X2)
| sP10(X0)
| c4_2(X0,X1)
| sP15(X0)
| c7_2(X0,X1)
| sP14(X0)
| ~ c5_2(X0,X1)
| c3_2(X0,X1)
| c4_2(X0,X2) ) ).
cnf(u4514,negated_conjecture,
( ~ c6_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| c4_2(X0,a479)
| c8_2(X0,a479)
| c2_2(X0,X2)
| c3_2(X0,X2)
| c4_2(X0,X1) ) ).
cnf(u4426,negated_conjecture,
( ~ sP18(X0)
| c2_2(X0,a479)
| c7_2(X0,X2)
| c6_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X1)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c7_2(X0,X1)
| c8_1(X0)
| ~ c5_2(X0,X1)
| c3_2(X0,X1)
| c4_2(X0,X2) ) ).
cnf(u3744,negated_conjecture,
( ~ ndr1_1(X47)
| sP18(X47) ) ).
cnf(u3745,negated_conjecture,
sP18(a530) ).
cnf(u4460,negated_conjecture,
( c2_2(X0,a479)
| c4_2(X0,X1)
| c2_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| c4_2(X0,X2)
| c8_2(X0,X2) ) ).
cnf(u3802,negated_conjecture,
( ~ c6_2(X47,a493)
| sP18(X47)
| ~ c4_2(X47,a492) ) ).
cnf(u4576,negated_conjecture,
( ~ c6_2(X0,X3)
| c8_2(X0,X2)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| c4_2(X0,X2)
| sP15(X0)
| c7_2(X0,X2)
| sP14(X0)
| c2_2(X0,X3)
| c8_2(X0,a479)
| c3_2(X0,X3)
| c4_2(X0,X1) ) ).
cnf(u4411,negated_conjecture,
( c4_2(X0,X1)
| c8_2(X0,X2)
| c2_2(X0,a479)
| c7_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X2)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c7_2(X0,X2)
| c8_1(X0) ) ).
cnf(u4101,negated_conjecture,
( c4_2(X0,a459)
| sP15(X0)
| sP10(X0)
| ~ c3_1(X0)
| c8_1(X0) ) ).
cnf(u1336,negated_conjecture,
( ~ c2_2(X148,X149)
| ndr1_1(X148)
| c6_2(X148,X149)
| ~ c7_2(X148,X149)
| sP10(X148) ) ).
cnf(u1341,negated_conjecture,
( ~ sP13(X97)
| c3_2(X97,X98)
| ~ c8_2(X97,X98)
| ~ c6_2(X97,X98)
| ndr1_1(X97) ) ).
cnf(u4214,negated_conjecture,
( c5_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c7_2(X0,X1)
| c1_2(X0,a480)
| sP15(X0)
| ~ c2_1(X0)
| c3_1(X0) ) ).
cnf(u3950,negated_conjecture,
( c2_2(X0,a479)
| c4_1(X0)
| c7_1(X0)
| ndr1_1(X0)
| sP14(X0)
| c8_1(X0) ) ).
cnf(u4408,negated_conjecture,
( ~ c6_2(X0,X3)
| c8_2(X0,X2)
| c8_1(X0)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X2)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X2)
| sP10(X0)
| c2_2(X0,X3)
| c8_2(X0,a479)
| c3_2(X0,X3)
| c4_2(X0,X1) ) ).
cnf(u4243,negated_conjecture,
( ~ sP18(X0)
| c7_2(X0,X1)
| ndr1_1(X0)
| c3_2(X0,a479)
| c8_1(X0)
| c4_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| ~ c5_2(X0,X1)
| c3_2(X0,X1)
| c2_2(X0,a479) ) ).
cnf(u1344,negated_conjecture,
( ~ sP14(X34)
| ~ c8_2(X34,X35)
| c1_2(X34,X35)
| c3_2(X34,X35)
| ndr1_1(X34) ) ).
cnf(u3875,negated_conjecture,
( ~ sP16(X2,X0)
| c8_2(X0,X1)
| c4_2(X0,X1)
| ndr1_1(X0)
| c2_2(X0,X1)
| c6_1(X0) ) ).
cnf(u4465,negated_conjecture,
( ~ c6_2(X0,X4)
| c4_2(X0,X2)
| c4_2(X0,X3)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X3)
| sP10(X0)
| c4_2(X0,X1)
| c6_2(X0,X2)
| c8_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X4)
| c3_2(X0,X4)
| c2_2(X0,a479) ) ).
cnf(u3814,negated_conjecture,
( ~ c4_1(X0)
| c6_2(X0,a553)
| sP10(X0)
| ndr1_1(X0)
| c5_1(X0) ) ).
cnf(u3864,negated_conjecture,
( ~ c7_2(a570,X0)
| ~ c3_2(a570,X0)
| c4_2(a570,X0) ) ).
cnf(u4016,negated_conjecture,
( ~ c3_2(X0,a479)
| ~ c1_2(X0,a479)
| c6_1(X0)
| ndr1_1(X0)
| c1_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X1)
| sP14(X0)
| c8_1(X0) ) ).
cnf(u3746,negated_conjecture,
sP18(a592) ).
cnf(u3807,negated_conjecture,
( ~ c6_2(X47,a492)
| sP18(X47)
| c2_2(X47,a493) ) ).
cnf(u4357,negated_conjecture,
( c2_2(X0,a479)
| c4_2(X0,X1)
| c3_2(X0,a479)
| c8_1(X0)
| c7_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c4_2(X0,a479)
| ndr1_1(X0)
| c6_1(X0)
| c8_2(X0,a479) ) ).
cnf(u4075,negated_conjecture,
( ~ c6_2(X0,X1)
| c7_1(X0)
| ndr1_1(X0)
| sP14(X0)
| c8_1(X0)
| c2_2(X0,X1)
| c8_2(X0,a479)
| c3_2(X0,X1)
| c4_1(X0) ) ).
cnf(u4501,negated_conjecture,
( ~ c6_2(X0,X3)
| c2_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| c4_2(X0,X2)
| c8_2(X0,X2)
| c2_2(X0,X3)
| c8_2(X0,a479)
| c3_2(X0,X3)
| c4_2(X0,X1) ) ).
cnf(u1346,negated_conjecture,
( sP19(X63,X62)
| c4_2(X62,X63)
| c5_2(X62,X63)
| ndr1_1(X62) ) ).
cnf(u4432,negated_conjecture,
( ~ c6_2(X0,X3)
| c8_2(X0,X2)
| c7_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X2)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c7_2(X0,X2)
| c8_1(X0)
| c2_2(X0,X3)
| c8_2(X0,a479)
| c3_2(X0,X3)
| c4_2(X0,X1) ) ).
cnf(u3805,negated_conjecture,
( c1_2(X47,a493)
| sP18(X47)
| ~ c4_2(X47,a492) ) ).
cnf(u4122,negated_conjecture,
( ~ c8_2(X0,X2)
| c4_2(X0,X1)
| ndr1_1(X0)
| c2_2(X0,X1)
| c6_1(X0)
| c8_2(X0,X1)
| c6_2(X0,X2)
| ~ c2_2(X0,X2) ) ).
cnf(u3801,negated_conjecture,
( ~ c6_2(X47,a493)
| sP18(X47)
| ~ c6_2(X47,a492) ) ).
cnf(u4542,negated_conjecture,
( c4_2(X0,X1)
| c8_2(X0,X2)
| c2_2(X0,a479)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| c4_2(X0,X2)
| sP15(X0)
| c7_2(X0,X2)
| sP14(X0) ) ).
cnf(u4398,negated_conjecture,
( ~ sP18(X0)
| c4_2(X0,X2)
| c8_1(X0)
| c6_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X1)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| ~ c5_2(X0,X1)
| c3_2(X0,X1)
| c2_2(X0,a479) ) ).
cnf(u3861,negated_conjecture,
sP18(a581) ).
cnf(u4037,negated_conjecture,
( ~ c6_2(X0,X2)
| c7_2(X0,X1)
| c2_2(X0,X2)
| c8_2(X0,X1)
| ndr1_1(X0)
| c3_2(X0,X2)
| c8_1(X0)
| c4_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0) ) ).
cnf(u4371,negated_conjecture,
( ~ c6_2(X0,X3)
| c2_2(X0,X2)
| c3_2(X0,a479)
| c8_1(X0)
| c7_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X2)
| ndr1_1(X0)
| c6_1(X0)
| c8_2(X0,X2)
| c2_2(X0,X3)
| c8_2(X0,a479)
| c3_2(X0,X3)
| c4_2(X0,X1) ) ).
cnf(u4386,negated_conjecture,
( ~ c6_2(X0,X2)
| c3_2(X0,a479)
| c8_1(X0)
| c7_2(X0,X1)
| c6_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c4_2(X0,a479)
| ndr1_1(X0)
| c6_1(X0)
| c8_2(X0,a479)
| c2_2(X0,X2)
| c3_2(X0,X2)
| c4_2(X0,X1) ) ).
cnf(u1337,negated_conjecture,
( sP16(X145,X143)
| ~ c8_2(X143,X145)
| c6_2(X143,X145)
| ~ c2_2(X143,X145)
| ndr1_1(X143) ) ).
cnf(u3808,negated_conjecture,
( ~ c4_2(X47,a492)
| sP18(X47)
| c2_2(X47,a493) ) ).
cnf(u4362,negated_conjecture,
( ~ c6_2(X0,X3)
| c4_2(X0,X2)
| c3_2(X0,a479)
| c8_1(X0)
| c7_2(X0,X2)
| c6_2(X0,X2)
| sP15(X0)
| sP14(X0)
| c4_2(X0,X1)
| ndr1_1(X0)
| c6_1(X0)
| c8_2(X0,X1)
| c7_2(X0,X1)
| c2_2(X0,X3)
| c3_2(X0,X3)
| c2_2(X0,a479) ) ).
cnf(u4405,negated_conjecture,
( c2_2(X0,a479)
| c4_2(X0,X2)
| c4_2(X0,X1)
| c2_2(X0,X3)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| c4_2(X0,X3)
| c6_2(X0,X2)
| c8_2(X0,X3) ) ).
cnf(u1338,negated_conjecture,
( sP17(X144,X143)
| c2_2(X143,X144)
| c8_2(X143,X144)
| c4_2(X143,X144)
| ndr1_1(X143) ) ).
cnf(u4040,negated_conjecture,
( ~ c3_2(X0,X2)
| c5_2(X0,X1)
| ~ c4_2(X0,X1)
| ~ c7_2(X0,X1)
| ndr1_1(X0)
| c1_2(X0,X2)
| ~ c8_1(X0)
| c4_2(X0,X2)
| c6_2(X0,X2)
| sP15(X0) ) ).
cnf(u3804,negated_conjecture,
( c1_2(X47,a493)
| sP18(X47)
| ~ c6_2(X47,a492) ) ).
cnf(u4526,negated_conjecture,
( c4_2(X0,X1)
| c4_2(X0,X2)
| c8_2(X0,X3)
| c2_2(X0,a479)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X2)
| sP10(X0)
| c4_2(X0,X3)
| c6_2(X0,X1)
| sP15(X0)
| c7_2(X0,X3)
| sP14(X0) ) ).
cnf(u1347,negated_conjecture,
( ~ c8_2(X47,X48)
| ndr1_1(X47)
| ~ c5_2(X47,X48)
| c3_2(X47,X48)
| ~ sP18(X47) ) ).
cnf(u4472,negated_conjecture,
( ~ c6_2(X0,X4)
| c4_2(X0,X2)
| c2_2(X0,X3)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X2)
| sP10(X0)
| c4_2(X0,X3)
| c6_2(X0,X1)
| c8_2(X0,X3)
| c2_2(X0,X4)
| c8_2(X0,a479)
| c3_2(X0,X4)
| c4_2(X0,X1) ) ).
cnf(u4546,negated_conjecture,
( ~ sP18(X0)
| c4_2(X0,X3)
| c2_2(X0,a479)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X3)
| sP10(X0)
| c4_2(X0,X1)
| c6_2(X0,X2)
| sP15(X0)
| c7_2(X0,X1)
| sP14(X0)
| ~ c5_2(X0,X1)
| c3_2(X0,X1)
| c4_2(X0,X2) ) ).
cnf(u4489,negated_conjecture,
( c2_2(X0,a479)
| c4_2(X0,X1)
| sP15(X0)
| sP14(X0)
| c8_1(X0)
| ndr1_1(X0)
| c6_1(X0)
| c3_2(X0,a479)
| c6_2(X0,X1)
| sP10(X0)
| c4_2(X0,a479)
| c8_2(X0,a479) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN547+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.17 % Computer : n007.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Mon Sep 28 16:26:07 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.29 % (2535295)Will run a generic schedule for satisfiability detection.
% 0.07/0.29 % (2535301)% WARNING: option uhcvi not known.
% 0.07/0.29 % (2535301)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1937462189:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.07/0.29 % (2535302)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3448048352:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.07/0.29 % (2535303)dis+10_1_sil=32000:sp=arity:random_seed=1377753876:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.07/0.29 % (2535300)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3743540042_2999 on theBenchmark for (2999ds/0Mi)
% 0.07/0.29 % (2535304)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1608665689:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.07/0.29 % (2535305)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=385594110:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.07/0.29 % (2535301) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2535295-2535301"...
% 0.07/0.29 % (2535301)...printing done.
% 0.07/0.29 % SZS status CounterSatisfiable for theBenchmark
% 0.07/0.29 % SZS output start Saturation.
% See solution above
% 0.07/0.30 % SZS output start Definitions and Model Updates.
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP19"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP17"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP16"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP15"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP12"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP11"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP10"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP9"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP8"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP5"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP4"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP3"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "sP1"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c3_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c4_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c5_1"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c5_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c2_2"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c6_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c8_1"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c8_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c1_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c7_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c2_0"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "c4_2"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "ndr1_1"
% 0.07/0.30 globally flip the polarity of every occurrence of predicate "ndr1_0"
% 0.07/0.30 for all inputs,
% 0.07/0.30 define c4_0 := $false
% 0.07/0.30 for all inputs,
% 0.07/0.30 define c3_0 := $true
% 0.07/0.30 % SZS output end Definitions and Model Updates.
% 0.07/0.30 % (2535301)------------------------------
% 0.07/0.30 % (2535301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.30 % (2535301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.30 % (2535301)CaDiCaL version: 2.1.3
% 0.07/0.30 % (2535301)Termination reason: Satisfiable
% 0.07/0.30 % (2535301)Time elapsed: 0.036 s
% 0.07/0.30 % (2535301)Peak memory usage: 14 MB
% 0.07/0.30 % (2535301)Instructions burned: 76 (million)
% 0.07/0.30 % (2535295)Success in time 0.063 s
% 0.07/0.30 % Vampire exiting
%------------------------------------------------------------------------------