%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN421+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 : n009.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.19s 0.30s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u1748,negated_conjecture,
( ~ c4_2(X118,X119)
| sP5(X118)
| c3_2(X118,a604)
| c6_1(X118)
| c2_2(X118,X119)
| ndr1_1(X118)
| c6_2(X118,X119) ) ).
cnf(u1751,negated_conjecture,
ndr1_0 ).
cnf(u1756,negated_conjecture,
( ~ c4_2(X118,X119)
| sP5(X118)
| c10_2(X118,a604)
| c6_1(X118)
| c2_2(X118,X119)
| ndr1_1(X118)
| c6_2(X118,X119) ) ).
cnf(u1760,negated_conjecture,
( ~ c6_2(X118,a604)
| sP5(X118)
| ndr1_1(X118)
| c6_1(X118)
| c2_2(X118,X119)
| ~ c4_2(X118,X119)
| c6_2(X118,X119) ) ).
cnf(u1764,negated_conjecture,
c4_0 ).
cnf(u1768,negated_conjecture,
( ~ c9_2(X4,a459)
| c10_1(X4)
| c10_2(X4,X5)
| ~ c2_2(X4,X5)
| ~ c7_2(X4,X5)
| ndr1_1(X4) ) ).
cnf(u1772,negated_conjecture,
( ~ c2_2(X4,a459)
| c10_1(X4)
| c10_2(X4,X5)
| ~ c2_2(X4,X5)
| ~ c7_2(X4,X5)
| ndr1_1(X4) ) ).
cnf(u1776,negated_conjecture,
( ~ c8_2(X4,a459)
| c10_1(X4)
| c10_2(X4,X5)
| ~ c2_2(X4,X5)
| ~ c7_2(X4,X5)
| ndr1_1(X4) ) ).
cnf(u1780,negated_conjecture,
( ~ c7_1(X6)
| c7_2(X6,X7)
| c8_2(X6,X7)
| c3_2(X6,X7)
| ndr1_1(X6)
| c6_1(X6) ) ).
cnf(u1783,negated_conjecture,
~ c1_0 ).
cnf(u1787,negated_conjecture,
c3_0 ).
cnf(u1796,negated_conjecture,
~ c9_0 ).
cnf(u1800,negated_conjecture,
c2_0 ).
cnf(u1808,negated_conjecture,
( ~ c1_1(X26)
| ~ c3_1(X26)
| c6_2(X26,X27)
| c10_2(X26,X27)
| c1_2(X26,X27)
| ndr1_1(X26) ) ).
cnf(u1837,negated_conjecture,
c5_0 ).
cnf(u1840,negated_conjecture,
c6_0 ).
cnf(u1848,negated_conjecture,
c8_0 ).
cnf(u1856,negated_conjecture,
( ~ c1_1(X35)
| c10_2(X35,X36)
| c7_2(X35,X36)
| ~ c9_2(X35,X36)
| ndr1_1(X35)
| c9_1(X35) ) ).
cnf(u1887,negated_conjecture,
~ c10_0 ).
cnf(u1893,negated_conjecture,
sP3 ).
cnf(u1908,negated_conjecture,
( c1_1(X61)
| ~ ndr1_1(X61) ) ).
cnf(u1960,negated_conjecture,
sP2 ).
cnf(u1964,negated_conjecture,
( ~ c6_1(X62)
| ~ c2_1(X62)
| ~ c3_2(X62,a536) ) ).
cnf(u1968,negated_conjecture,
( ~ c6_1(X62)
| ~ c2_1(X62)
| c9_2(X62,a536) ) ).
cnf(u1972,negated_conjecture,
( ~ c6_1(X62)
| ~ c2_1(X62)
| c4_2(X62,a536) ) ).
cnf(u1976,negated_conjecture,
( ~ c6_1(X62)
| ~ c2_1(X62)
| ~ ndr1_1(X62) ) ).
cnf(u2030,negated_conjecture,
( ~ c10_1(X120)
| ~ c3_2(X120,X121)
| ~ c6_2(X120,X121)
| ~ c2_2(X120,X121)
| ndr1_1(X120)
| ~ c1_1(X120) ) ).
cnf(u2059,negated_conjecture,
( ~ c2_1(X122)
| c7_1(X122)
| c6_1(X122) ) ).
cnf(u2063,negated_conjecture,
c7_0 ).
cnf(u2089,negated_conjecture,
( c1_1(X1)
| ~ ndr1_1(X1)
| c5_1(X1) ) ).
cnf(u2093,negated_conjecture,
( c9_2(X1,a450)
| c1_1(X1)
| c5_1(X1) ) ).
cnf(u2097,negated_conjecture,
( c8_2(X1,a450)
| c1_1(X1)
| c5_1(X1) ) ).
cnf(u2101,negated_conjecture,
( ~ c6_2(X1,a450)
| c1_1(X1)
| c5_1(X1) ) ).
cnf(u2114,negated_conjecture,
~ c3_1(a449) ).
cnf(u2319,negated_conjecture,
( ~ c6_2(X18,a474)
| c10_1(X18)
| c9_1(X18) ) ).
cnf(u2327,negated_conjecture,
( ~ c7_2(X18,a474)
| c10_1(X18)
| c9_1(X18) ) ).
cnf(u2331,negated_conjecture,
( ~ c8_2(X18,a474)
| c10_1(X18)
| c9_1(X18) ) ).
cnf(u2335,negated_conjecture,
( ~ ndr1_1(X18)
| c10_1(X18)
| c9_1(X18) ) ).
cnf(u2364,negated_conjecture,
~ sP4 ).
cnf(u2473,negated_conjecture,
( ~ sP19(X29)
| sP20(X29)
| c1_1(X29) ) ).
cnf(u2531,negated_conjecture,
( c10_1(X38)
| ~ c3_1(X38)
| c6_1(X38) ) ).
cnf(u2535,negated_conjecture,
( ~ sP18(X40)
| ~ c1_1(X40)
| ~ sP17(X40) ) ).
cnf(u2598,negated_conjecture,
( ~ c2_2(X44,a512)
| sP14(X44)
| sP13(X44) ) ).
cnf(u2606,negated_conjecture,
( c1_2(X44,a512)
| sP14(X44)
| sP13(X44) ) ).
cnf(u2610,negated_conjecture,
( ~ c7_2(X44,a512)
| sP14(X44)
| sP13(X44) ) ).
cnf(u2614,negated_conjecture,
( ~ ndr1_1(X44)
| sP14(X44)
| sP13(X44) ) ).
cnf(u2644,negated_conjecture,
( ~ c5_1(X48)
| c9_1(X48) ) ).
cnf(u2651,negated_conjecture,
~ ndr1_1(a517) ).
cnf(u2656,negated_conjecture,
~ c8_1(a519) ).
cnf(u2661,negated_conjecture,
c9_2(a519,a520) ).
cnf(u2666,negated_conjecture,
c7_2(a519,a520) ).
cnf(u2671,negated_conjecture,
c5_2(a519,a520) ).
cnf(u2676,negated_conjecture,
~ ndr1_1(a519) ).
cnf(u2681,negated_conjecture,
c9_1(a519) ).
cnf(u2702,negated_conjecture,
( ~ c7_2(X57,a527)
| c6_1(X57)
| ~ c9_1(X57) ) ).
cnf(u2709,negated_conjecture,
( c9_2(X57,a527)
| c6_1(X57)
| ~ c9_1(X57) ) ).
cnf(u2713,negated_conjecture,
( ~ c8_2(X57,a527)
| c6_1(X57)
| ~ c9_1(X57) ) ).
cnf(u2717,negated_conjecture,
( ~ ndr1_1(X57)
| c6_1(X57)
| ~ c9_1(X57) ) ).
cnf(u2806,negated_conjecture,
~ sP1 ).
cnf(u2882,negated_conjecture,
( c8_2(X66,a544)
| ~ c5_1(X66) ) ).
cnf(u2889,negated_conjecture,
( ~ c4_2(X66,a544)
| ~ c5_1(X66) ) ).
cnf(u2893,negated_conjecture,
( c9_2(X66,a544)
| ~ c5_1(X66) ) ).
cnf(u2897,negated_conjecture,
( ~ ndr1_1(X66)
| ~ c5_1(X66) ) ).
cnf(u2919,negated_conjecture,
~ c5_1(a547) ).
cnf(u2936,negated_conjecture,
~ c6_1(a547) ).
cnf(u3024,negated_conjecture,
( sP25(X88,X87)
| c2_1(X87)
| ~ c7_1(X87) ) ).
cnf(u3068,negated_conjecture,
( ~ c7_1(X90)
| ~ c5_1(X90)
| c9_1(X90) ) ).
cnf(u3080,negated_conjecture,
( ~ sP10(X92)
| c5_1(X92)
| sP9(X92) ) ).
cnf(u3121,negated_conjecture,
( ~ sP7(X98)
| ~ c10_2(X98,a568)
| ~ sP6(X98) ) ).
cnf(u3129,negated_conjecture,
( ~ sP7(X98)
| c9_2(X98,a568)
| ~ sP6(X98) ) ).
cnf(u3133,negated_conjecture,
( ~ ndr1_1(X98)
| ~ sP7(X98)
| ~ sP6(X98) ) ).
cnf(u3177,negated_conjecture,
( ~ c7_2(X102,a574)
| c6_1(X102)
| ~ c8_1(X102) ) ).
cnf(u3181,negated_conjecture,
( ~ c4_2(X102,a574)
| c6_1(X102)
| ~ c8_1(X102) ) ).
cnf(u3185,negated_conjecture,
( c6_2(X102,a574)
| c6_1(X102)
| ~ c8_1(X102) ) ).
cnf(u3189,negated_conjecture,
( ~ ndr1_1(X102)
| c6_1(X102)
| ~ c8_1(X102) ) ).
cnf(u3209,negated_conjecture,
( sP24(X110,X109)
| c7_2(X109,a589)
| c10_1(X109) ) ).
cnf(u3216,negated_conjecture,
( ~ c10_2(X109,a589)
| sP24(X110,X109)
| c10_1(X109) ) ).
cnf(u3220,negated_conjecture,
( sP24(X110,X109)
| c2_2(X109,a589)
| c10_1(X109) ) ).
cnf(u3224,negated_conjecture,
( ~ ndr1_1(X109)
| sP24(X110,X109)
| c10_1(X109) ) ).
cnf(u3249,negated_conjecture,
( ~ c7_2(X112,a591)
| ~ c9_1(X112)
| c1_1(X112) ) ).
cnf(u3253,negated_conjecture,
~ c8_1(a592) ).
cnf(u3260,negated_conjecture,
( ~ c1_2(X112,a591)
| ~ c9_1(X112)
| c1_1(X112) ) ).
cnf(u3264,negated_conjecture,
( ~ ndr1_1(X112)
| ~ c9_1(X112)
| c1_1(X112) ) ).
cnf(u3335,negated_conjecture,
( ~ c7_2(a601,X116)
| ~ c4_2(a601,X116)
| c6_2(a601,X116) ) ).
cnf(u3377,negated_conjecture,
~ c5_1(a601) ).
cnf(u3382,negated_conjecture,
~ c10_1(a601) ).
cnf(u3420,negated_conjecture,
~ c2_2(a478,a480) ).
cnf(u3425,negated_conjecture,
c4_2(a478,a480) ).
cnf(u3430,negated_conjecture,
~ c7_2(a478,a480) ).
cnf(u3435,negated_conjecture,
~ ndr1_1(a478) ).
cnf(u3440,negated_conjecture,
c8_2(a478,a479) ).
cnf(u3445,negated_conjecture,
~ c1_2(a478,a479) ).
cnf(u3450,negated_conjecture,
c3_2(a478,a479) ).
cnf(u3456,negated_conjecture,
~ c7_1(a478) ).
cnf(u3545,negated_conjecture,
( c9_1(X107)
| ~ c5_1(X107)
| ~ c10_1(X107) ) ).
cnf(u3569,negated_conjecture,
sP0 ).
cnf(u3574,negated_conjecture,
c9_1(a585) ).
cnf(u3579,negated_conjecture,
c5_1(a585) ).
cnf(u3627,negated_conjecture,
~ c10_2(a460,a461) ).
cnf(u3632,negated_conjecture,
c3_2(a460,a461) ).
cnf(u3637,negated_conjecture,
~ c4_2(a460,a461) ).
cnf(u3642,negated_conjecture,
~ ndr1_1(a460) ).
cnf(u3647,negated_conjecture,
~ c6_1(a460) ).
cnf(u3651,negated_conjecture,
~ c7_1(a460) ).
cnf(u3799,negated_conjecture,
~ c2_1(a488) ).
cnf(u3804,negated_conjecture,
~ c9_1(a488) ).
cnf(u3928,negated_conjecture,
~ c1_2(a517,a518) ).
cnf(u3938,negated_conjecture,
~ c8_2(a517,a518) ).
cnf(u4017,negated_conjecture,
~ c8_2(a523,a524) ).
cnf(u4022,negated_conjecture,
~ c4_2(a523,a524) ).
cnf(u4027,negated_conjecture,
c2_2(a523,a524) ).
cnf(u4032,negated_conjecture,
~ ndr1_1(a523) ).
cnf(u4037,negated_conjecture,
~ c4_1(a523) ).
cnf(u4042,negated_conjecture,
c3_1(a523) ).
cnf(u4178,negated_conjecture,
~ c3_2(a551,a552) ).
cnf(u4183,negated_conjecture,
c6_2(a551,a552) ).
cnf(u4188,negated_conjecture,
~ c2_2(a551,a552) ).
cnf(u4193,negated_conjecture,
~ ndr1_1(a551) ).
cnf(u4198,negated_conjecture,
~ c9_1(a551) ).
cnf(u4203,negated_conjecture,
c8_1(a551) ).
cnf(u4258,negated_conjecture,
c3_1(a571) ).
cnf(u4263,negated_conjecture,
c8_2(a571,a572) ).
cnf(u4268,negated_conjecture,
c9_2(a571,a572) ).
cnf(u4273,negated_conjecture,
~ ndr1_1(a571) ).
cnf(u4278,negated_conjecture,
~ c5_1(a571) ).
cnf(u4290,negated_conjecture,
~ c5_1(a575) ).
cnf(u4295,negated_conjecture,
~ c7_1(a575) ).
cnf(u4300,negated_conjecture,
~ c5_2(a575,a576) ).
cnf(u4305,negated_conjecture,
c9_2(a575,a576) ).
cnf(u4310,negated_conjecture,
c8_2(a575,a576) ).
cnf(u4315,negated_conjecture,
~ ndr1_1(a575) ).
cnf(u4332,negated_conjecture,
~ c8_1(a577) ).
cnf(u4581,negated_conjecture,
~ c3_1(a601) ).
cnf(u4620,negated_conjecture,
~ c9_2(a478,a479) ).
cnf(u4626,negated_conjecture,
sP21(a571) ).
cnf(u4699,negated_conjecture,
~ c1_2(a575,a576) ).
cnf(u4712,negated_conjecture,
~ c2_2(a575,a576) ).
cnf(u4720,negated_conjecture,
sP21(a575) ).
cnf(u4739,negated_conjecture,
c6_1(a478) ).
cnf(u4768,negated_conjecture,
~ c2_1(a478) ).
cnf(u4790,negated_conjecture,
~ c1_2(a460,a461) ).
cnf(u1711,negated_conjecture,
( ~ sP20(X29)
| ~ c2_2(X29,a496) ) ).
cnf(u40,negated_conjecture,
( ~ sP20(X29)
| c6_2(X29,a496) ) ).
cnf(u1740,negated_conjecture,
( c5_2(X40,X41)
| ndr1_1(X40)
| ~ c2_2(X40,X41)
| ~ c7_2(X40,X41)
| sP17(X40) ) ).
cnf(u1664,negated_conjecture,
( c6_2(X98,a567)
| sP7(X98) ) ).
cnf(u1736,negated_conjecture,
( ~ sP26(X65,X64)
| c2_2(X64,X65)
| c6_2(X64,X65)
| c7_2(X64,X65)
| ndr1_1(X64) ) ).
cnf(u1737,negated_conjecture,
( ~ c10_2(X59,X60)
| ndr1_1(X59)
| c1_2(X59,X60)
| sP12(X59) ) ).
cnf(u1742,negated_conjecture,
( ~ c2_2(X29,X30)
| ~ c8_2(X29,X30)
| ndr1_1(X29)
| ~ c5_2(X29,X30)
| sP19(X29) ) ).
cnf(u4584,negated_conjecture,
( ~ sP6(X98)
| ~ ndr1_1(X98) ) ).
cnf(u1666,negated_conjecture,
( ~ sP8(X95)
| ~ ndr1_1(X95) ) ).
cnf(u1735,negated_conjecture,
( ~ sP11(X69)
| ~ c2_2(X69,X70)
| c10_2(X69,X70)
| c3_2(X69,X70)
| ndr1_1(X69) ) ).
cnf(u1732,negated_conjecture,
( ~ sP9(X92)
| c10_2(X92,X94)
| ~ c3_2(X92,X94)
| c5_2(X92,X94)
| ndr1_1(X92) ) ).
cnf(u1739,negated_conjecture,
( ~ sP15(X42)
| ~ c3_2(X42,X43)
| ~ c6_2(X42,X43)
| ~ c4_2(X42,X43)
| ndr1_1(X42) ) ).
cnf(u1701,negated_conjecture,
( c10_2(X40,a506)
| sP18(X40) ) ).
cnf(u1729,negated_conjecture,
( ~ sP23(X114,X113)
| c1_2(X113,X114)
| c2_2(X113,X114)
| c3_2(X113,X114)
| ndr1_1(X113) ) ).
cnf(u1734,negated_conjecture,
( ~ sP25(X88,X87)
| c4_2(X87,X88)
| ~ c6_2(X87,X88)
| ~ c3_2(X87,X88)
| ndr1_1(X87) ) ).
cnf(u4622,negated_conjecture,
( sP21(X0)
| c1_1(X0)
| c5_1(X0) ) ).
cnf(u1662,negated_conjecture,
( ~ ndr1_1(X98)
| sP7(X98) ) ).
cnf(u56,negated_conjecture,
( ~ sP16(X42)
| c6_2(X42,a507) ) ).
cnf(u1710,negated_conjecture,
( ~ sP20(X29)
| ~ ndr1_1(X29) ) ).
cnf(u1725,negated_conjecture,
( ~ sP22(X2)
| ~ c7_2(X2,a451) ) ).
cnf(u41,negated_conjecture,
( ~ sP20(X29)
| ~ c10_2(X29,a496) ) ).
cnf(u1703,negated_conjecture,
( c9_2(X40,a506)
| sP18(X40) ) ).
cnf(u1738,negated_conjecture,
( ~ sP13(X44)
| c10_2(X44,X45)
| c4_2(X44,X45)
| ndr1_1(X44) ) ).
cnf(u1700,negated_conjecture,
( ~ ndr1_1(X40)
| sP18(X40) ) ).
cnf(u4632,negated_conjecture,
( ~ c7_1(X0)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1)
| ndr1_1(X0)
| c2_1(X0)
| c4_2(X0,X1) ) ).
cnf(u4588,negated_conjecture,
( ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ndr1_1(X0)
| c2_2(X0,a589)
| c10_1(X0) ) ).
cnf(u4583,negated_conjecture,
( sP13(X44)
| ~ ndr1_1(X44) ) ).
cnf(u1733,negated_conjecture,
( ~ c10_2(X92,X93)
| ndr1_1(X92)
| c5_2(X92,X93)
| c8_2(X92,X93)
| sP10(X92) ) ).
cnf(u1665,negated_conjecture,
( ~ c3_2(X98,a567)
| sP7(X98) ) ).
cnf(u1697,negated_conjecture,
( ~ sP14(X44)
| c5_2(X44,a511) ) ).
cnf(u4728,negated_conjecture,
( ~ c1_1(X0)
| ~ c6_2(X0,X1)
| ~ c2_2(X0,X1)
| ndr1_1(X0)
| ~ c3_2(X0,X1)
| ~ c3_1(X0)
| c6_1(X0) ) ).
cnf(u1702,negated_conjecture,
( ~ c3_2(X40,a506)
| sP18(X40) ) ).
cnf(u1667,negated_conjecture,
( ~ sP8(X95)
| c2_2(X95,a564) ) ).
cnf(u4605,negated_conjecture,
( c5_2(X0,a506)
| sP21(X0)
| c6_2(X0,a506)
| sP10(X0)
| sP18(X0) ) ).
cnf(u1730,negated_conjecture,
( ~ sP24(X110,X109)
| ~ c3_2(X109,X110)
| ~ c1_2(X109,X110)
| ndr1_1(X109) ) ).
cnf(u1745,negated_conjecture,
( ~ c8_2(X8,X9)
| ndr1_1(X8)
| ~ c9_2(X8,X9)
| c6_2(X8,X9)
| sP21(X8) ) ).
cnf(u59,negated_conjecture,
( ~ sP14(X44)
| c6_2(X44,a511) ) ).
cnf(u1699,negated_conjecture,
( ~ sP16(X42)
| c4_2(X42,a507) ) ).
cnf(u1731,negated_conjecture,
( c5_2(X98,X99)
| c7_2(X98,X99)
| ~ c1_2(X98,X99)
| ndr1_1(X98)
| sP6(X98) ) ).
cnf(u1743,negated_conjecture,
( sP28(X23,X22)
| c4_2(X22,X23)
| c6_2(X22,X23)
| c8_2(X22,X23)
| ndr1_1(X22) ) ).
cnf(u1724,negated_conjecture,
( ~ sP22(X2)
| ~ c4_2(X2,a451) ) ).
cnf(u4607,negated_conjecture,
( c6_2(X0,a544)
| sP21(X0)
| ~ c5_1(X0) ) ).
cnf(u54,negated_conjecture,
( ~ sP16(X42)
| c3_2(X42,a507) ) ).
cnf(u4591,negated_conjecture,
( c8_2(X0,a506)
| c5_2(X0,a506)
| sP10(X0)
| sP18(X0) ) ).
cnf(u1741,negated_conjecture,
( ~ sP27(X32,X31)
| ~ c8_2(X31,X32)
| ~ c1_2(X31,X32)
| ~ c6_2(X31,X32)
| ndr1_1(X31) ) ).
cnf(u4594,negated_conjecture,
( ~ c8_2(X0,a567)
| ~ c5_2(X0,a567)
| sP19(X0)
| sP7(X0) ) ).
cnf(u1696,negated_conjecture,
( ~ sP14(X44)
| ~ ndr1_1(X44) ) ).
cnf(u1723,negated_conjecture,
( ~ sP22(X2)
| ~ ndr1_1(X2) ) ).
cnf(u4589,negated_conjecture,
( ~ c3_2(X0,X1)
| ~ c1_2(X0,X1)
| ndr1_1(X0)
| c7_2(X0,a589)
| c10_1(X0) ) ).
cnf(u90,negated_conjecture,
( ~ sP8(X95)
| ~ c9_2(X95,a564) ) ).
cnf(u1744,negated_conjecture,
( ~ sP29(X10,X8)
| c6_2(X8,X10)
| ~ c1_2(X8,X10)
| ~ c7_2(X8,X10)
| ndr1_1(X8) ) ).
cnf(u1663,negated_conjecture,
( c2_2(X98,a567)
| sP7(X98) ) ).
cnf(u1698,negated_conjecture,
( ~ sP16(X42)
| ~ ndr1_1(X42) ) ).
cnf(u4586,negated_conjecture,
( c1_2(X0,a506)
| sP12(X0)
| sP18(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN421+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n009.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 15:55:30 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 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.19/0.30 % (3183572)Will run a generic schedule for satisfiability detection.
% 0.19/0.30 % (3183581)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1361386972:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.30 % (3183578)% WARNING: option uhcvi not known.
% 0.19/0.30 % (3183577)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=844490671_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.30 % (3183578)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3637777851:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.30 % (3183579)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1445426484:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.30 % (3183580)dis+10_1_sil=32000:sp=arity:random_seed=1514408079:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.30 % (3183583)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=87256318:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.30 % (3183582)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4059736990:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.30 % (3183581)Instruction limit reached!
% 0.19/0.30 % (3183581)------------------------------
% 0.19/0.30 % (3183581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.30 % (3183581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.30 % (3183581)CaDiCaL version: 2.1.3
% 0.19/0.30 % (3183581)Termination reason: Instruction limit
% 0.19/0.30 % (3183581)Termination phase: Saturation
% 0.19/0.30 % (3183581)Time elapsed: 0.031 s
% 0.19/0.30 % (3183581)Peak memory usage: 13 MB
% 0.19/0.30 % (3183581)Instructions burned: 119 (million)
% 0.19/0.30 % (3183578) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3183572-3183578"...
% 0.19/0.30 % Detected minimum model sizes of [1]
% 0.19/0.30 % Detected maximum model sizes of [159]
% 0.19/0.30 % TRYING [1]
% 0.19/0.30 % (3183578)...printing done.
% 0.19/0.30 % TRYING [2]
% 0.19/0.30 % SZS status CounterSatisfiable for theBenchmark
% 0.19/0.30 % SZS output start Saturation.
% See solution above
% 0.19/0.30 % SZS output start Definitions and Model Updates.
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP28"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP21"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP19"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP18"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP17"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP12"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP10"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP7"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP6"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP5"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP4"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "sP3"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c8_0"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c10_0"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c5_2"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c3_0"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c6_1"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c7_1"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c2_1"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c4_1"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c7_0"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c2_2"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c7_2"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c2_0"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c9_0"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c6_0"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c1_1"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c5_1"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c8_2"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c4_2"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "ndr1_1"
% 0.19/0.30 globally flip the polarity of every occurrence of predicate "c3_1"
% 0.19/0.30 % SZS output end Definitions and Model Updates.
% 0.19/0.30 % (3183578)------------------------------
% 0.19/0.30 % (3183578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.30 % (3183578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.30 % (3183578)CaDiCaL version: 2.1.3
% 0.19/0.30 % (3183578)Termination reason: Satisfiable
% 0.19/0.30 % (3183578)Time elapsed: 0.029 s
% 0.19/0.30 % (3183578)Peak memory usage: 14 MB
% 0.19/0.30 % (3183578)Instructions burned: 48 (million)
% 0.19/0.30 % (3183572)Success in time 0.07 s
% 0.19/0.30 % Vampire exiting
%------------------------------------------------------------------------------