%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN547+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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:00:55 PM UTC 2026
% Result : CounterSatisfiable 6.29s 1.82s
% Output : Saturation 8.77s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u652,negated_conjecture,
~ c5_0 ).
cnf(u656,negated_conjecture,
c7_0 ).
cnf(u661,negated_conjecture,
c8_0 ).
cnf(u684,negated_conjecture,
ndr1_0 ).
cnf(u688,negated_conjecture,
( ~ c7_2(X129,a602)
| c7_1(X129)
| c2_1(X129) ) ).
cnf(u691,negated_conjecture,
~ c1_0 ).
cnf(u696,negated_conjecture,
( c4_2(X129,a602)
| c7_1(X129)
| c2_1(X129) ) ).
cnf(u700,negated_conjecture,
( c3_2(X129,a602)
| c7_1(X129)
| c2_1(X129) ) ).
cnf(u704,negated_conjecture,
( c7_1(X129)
| c2_1(X129)
| ndr1_1(X129) ) ).
cnf(u709,negated_conjecture,
c2_0 ).
cnf(u720,negated_conjecture,
( ~ c8_2(X125,X126)
| c4_1(X125)
| c8_1(X125)
| ~ ndr1_1(X125)
| c3_2(X125,X126)
| c1_2(X125,X126) ) ).
cnf(u725,negated_conjecture,
~ sP0 ).
cnf(u730,negated_conjecture,
~ ndr1_1(a600) ).
cnf(u738,negated_conjecture,
c3_1(a600) ).
cnf(u744,negated_conjecture,
c6_0 ).
cnf(u748,negated_conjecture,
~ sP1 ).
cnf(u806,negated_conjecture,
~ sP2 ).
cnf(u854,negated_conjecture,
( ~ c2_2(X116,X117)
| ~ c8_2(X116,X118)
| c6_2(X116,X118)
| c2_2(X116,X118)
| c6_1(X116)
| ~ ndr1_1(X116)
| ~ c4_2(X116,X117)
| c8_2(X116,X117) ) ).
cnf(u857,negated_conjecture,
~ sP4 ).
cnf(u925,negated_conjecture,
( ~ c2_2(X110,X111)
| c7_1(X110)
| ~ ndr1_1(X110)
| ~ c6_2(X110,X111)
| c4_1(X110)
| c7_2(X110,X111) ) ).
cnf(u942,negated_conjecture,
c8_1(a581) ).
cnf(u947,negated_conjecture,
~ c6_1(a581) ).
cnf(u952,negated_conjecture,
~ ndr1_1(a581) ).
cnf(u980,negated_conjecture,
sP5 ).
cnf(u983,negated_conjecture,
( ~ c8_2(X105,a576)
| c7_1(X105)
| ~ c1_1(X105) ) ).
cnf(u990,negated_conjecture,
( c4_2(X105,a576)
| c7_1(X105)
| ~ c1_1(X105) ) ).
cnf(u998,negated_conjecture,
( c8_2(X99,X100)
| ~ ndr1_1(X99)
| c6_2(X99,X100)
| c7_2(X99,X100)
| ~ c6_1(X99)
| c5_1(X99) ) ).
cnf(u1030,negated_conjecture,
( ~ c3_2(X95,X97)
| c1_2(X95,X97)
| c8_1(X95)
| c2_2(X95,X97)
| ~ ndr1_1(X95)
| ~ c7_2(X95,X96)
| c4_2(X95,X96)
| c5_2(X95,X96) ) ).
cnf(u1051,negated_conjecture,
( c5_2(X92,X93)
| ~ c4_1(X92)
| c2_2(X92,a572)
| ~ ndr1_1(X92)
| c2_2(X92,X93) ) ).
cnf(u1055,negated_conjecture,
( ~ c5_2(X92,a572)
| ~ c4_1(X92)
| c2_2(X92,X93)
| ~ ndr1_1(X92)
| c5_2(X92,X93) ) ).
cnf(u1059,negated_conjecture,
( ~ c6_2(X92,a572)
| ~ c4_1(X92)
| c2_2(X92,X93)
| ~ ndr1_1(X92)
| c5_2(X92,X93) ) ).
cnf(u1064,negated_conjecture,
c3_2(a570,a571) ).
cnf(u1069,negated_conjecture,
c1_2(a570,a571) ).
cnf(u1074,negated_conjecture,
c2_2(a570,a571) ).
cnf(u1079,negated_conjecture,
ndr1_1(a570) ).
cnf(u1084,negated_conjecture,
c5_1(a570) ).
cnf(u1089,negated_conjecture,
c4_1(a570) ).
cnf(u1094,negated_conjecture,
~ sP6 ).
cnf(u1099,negated_conjecture,
~ c4_1(a568) ).
cnf(u1104,negated_conjecture,
~ ndr1_1(a568) ).
cnf(u1112,negated_conjecture,
~ sP7 ).
cnf(u1116,negated_conjecture,
~ sP8 ).
cnf(u1121,negated_conjecture,
c5_1(a564) ).
cnf(u1126,negated_conjecture,
~ ndr1_1(a564) ).
cnf(u1134,negated_conjecture,
c7_1(a564) ).
cnf(u1166,negated_conjecture,
( ~ c2_2(X87,X89)
| ~ c8_1(X87)
| ~ c6_2(X87,X89)
| c3_2(X87,X89)
| ~ ndr1_1(X87)
| c8_2(X87,X88)
| c2_2(X87,X88)
| c7_2(X87,X88) ) ).
cnf(u1196,negated_conjecture,
c6_1(a558) ).
cnf(u1201,negated_conjecture,
c1_1(a558) ).
cnf(u1206,negated_conjecture,
( ~ c3_1(X86)
| c5_1(X86)
| ~ c6_1(X86) ) ).
cnf(u1255,negated_conjecture,
~ sP10 ).
cnf(u1278,negated_conjecture,
( ~ c7_2(X77,a548)
| ~ c1_1(X77)
| ~ c6_2(X77,X78)
| ~ ndr1_1(X77)
| c3_2(X77,X78)
| ~ c8_2(X77,X78) ) ).
cnf(u1281,negated_conjecture,
~ sP11 ).
cnf(u1286,negated_conjecture,
( ~ c8_2(X77,X78)
| ~ c1_1(X77)
| ~ c4_2(X77,a548)
| ~ ndr1_1(X77)
| c3_2(X77,X78)
| ~ c6_2(X77,X78) ) ).
cnf(u1290,negated_conjecture,
( ~ c8_2(X77,X78)
| ~ c1_1(X77)
| c2_2(X77,a548)
| ~ ndr1_1(X77)
| c3_2(X77,X78)
| ~ c6_2(X77,X78) ) ).
cnf(u1294,negated_conjecture,
~ sP12 ).
cnf(u1302,negated_conjecture,
( ~ c8_1(X75)
| ~ c2_1(X75) ) ).
cnf(u1329,negated_conjecture,
~ sP13 ).
cnf(u1333,negated_conjecture,
( c1_1(X73)
| c5_1(X73)
| c6_1(X73) ) ).
cnf(u1337,negated_conjecture,
~ sP14 ).
cnf(u1341,negated_conjecture,
~ sP15 ).
cnf(u1346,negated_conjecture,
c5_1(a536) ).
cnf(u1351,negated_conjecture,
~ c7_1(a536) ).
cnf(u1356,negated_conjecture,
~ ndr1_1(a536) ).
cnf(u1369,negated_conjecture,
~ c2_1(a534) ).
cnf(u1374,negated_conjecture,
c8_2(a534,a535) ).
cnf(u1379,negated_conjecture,
c4_2(a534,a535) ).
cnf(u1384,negated_conjecture,
~ c6_2(a534,a535) ).
cnf(u1389,negated_conjecture,
ndr1_1(a534) ).
cnf(u1394,negated_conjecture,
c8_1(a534) ).
cnf(u1399,negated_conjecture,
~ c3_1(a533) ).
cnf(u1427,negated_conjecture,
~ c6_1(a531) ).
cnf(u1432,negated_conjecture,
~ c5_1(a531) ).
cnf(u1437,negated_conjecture,
c4_1(a531) ).
cnf(u1445,negated_conjecture,
~ ndr1_1(a530) ).
cnf(u1475,negated_conjecture,
( ~ c6_2(X54,X55)
| ~ ndr1_1(X54)
| ~ c4_2(X54,X55)
| c8_1(X54)
| c3_2(X54,X55)
| ~ c4_1(X54) ) ).
cnf(u1491,negated_conjecture,
~ sP16 ).
cnf(u1497,negated_conjecture,
~ c1_2(a520,a521) ).
cnf(u1502,negated_conjecture,
c2_2(a520,a521) ).
cnf(u1507,negated_conjecture,
~ c4_2(a520,a521) ).
cnf(u1512,negated_conjecture,
ndr1_1(a520) ).
cnf(u1517,negated_conjecture,
~ c2_1(a520) ).
cnf(u1522,negated_conjecture,
~ c5_1(a520) ).
cnf(u1531,negated_conjecture,
~ sP17 ).
cnf(u1551,negated_conjecture,
( ~ c2_2(X51,a516)
| ~ ndr1_1(X51)
| ~ c4_2(X51,X52)
| c5_2(X51,X52)
| sP18(X51) ) ).
cnf(u1554,negated_conjecture,
~ sP20 ).
cnf(u1558,negated_conjecture,
~ sP19 ).
cnf(u1563,negated_conjecture,
( ~ c6_2(X51,a516)
| ~ ndr1_1(X51)
| ~ c4_2(X51,X52)
| c5_2(X51,X52)
| sP18(X51) ) ).
cnf(u1569,negated_conjecture,
c1_1(a508) ).
cnf(u1577,negated_conjecture,
~ c2_1(a508) ).
cnf(u1614,negated_conjecture,
~ sP21 ).
cnf(u1627,negated_conjecture,
~ sP23 ).
cnf(u1631,negated_conjecture,
~ sP24 ).
cnf(u1636,negated_conjecture,
~ c5_1(a491) ).
cnf(u1641,negated_conjecture,
~ ndr1_1(a491) ).
cnf(u1649,negated_conjecture,
~ c4_1(a491) ).
cnf(u1682,negated_conjecture,
~ sP25 ).
cnf(u1686,negated_conjecture,
( c4_2(X36,a487)
| ~ c2_1(X36)
| c5_1(X36) ) ).
cnf(u1690,negated_conjecture,
( c1_2(X36,a487)
| ~ c2_1(X36)
| c5_1(X36) ) ).
cnf(u1694,negated_conjecture,
( ~ c2_1(X36)
| ndr1_1(X36)
| c5_1(X36) ) ).
cnf(u1714,negated_conjecture,
~ sP27 ).
cnf(u1718,negated_conjecture,
( ~ c3_2(X33,X34)
| c8_2(X33,a481)
| c8_1(X33)
| ~ ndr1_1(X33)
| c4_2(X33,X34)
| ~ c6_2(X33,X34) ) ).
cnf(u1722,negated_conjecture,
( ~ c3_2(X33,X34)
| c2_2(X33,a481)
| c8_1(X33)
| ~ ndr1_1(X33)
| c4_2(X33,X34)
| ~ c6_2(X33,X34) ) ).
cnf(u1727,negated_conjecture,
sP28 ).
cnf(u1730,negated_conjecture,
( ~ c7_2(X31,a479)
| c3_2(X31,X32)
| ~ c8_1(X31)
| ~ ndr1_1(X31)
| ~ c8_2(X31,X32)
| c1_2(X31,X32) ) ).
cnf(u1750,negated_conjecture,
~ sP29 ).
cnf(u1755,negated_conjecture,
( ~ c3_2(X27,X28)
| ~ c3_1(X27)
| c8_1(X27)
| ~ ndr1_1(X27)
| c4_2(X27,X28)
| ~ c6_2(X27,X28) ) ).
cnf(u1777,negated_conjecture,
( ~ c1_2(X22,X23)
| ~ ndr1_1(X22)
| ~ c8_2(X22,X23)
| ~ c4_2(X22,X23) ) ).
cnf(u1796,negated_conjecture,
~ sP30 ).
cnf(u1833,negated_conjecture,
( c8_2(X14,X15)
| ~ c2_1(X14)
| c8_1(X14)
| ~ ndr1_1(X14)
| ~ c7_2(X14,X15)
| ~ c4_2(X14,X15) ) ).
cnf(u1851,negated_conjecture,
~ c8_1(a466) ).
cnf(u1856,negated_conjecture,
c1_1(a466) ).
cnf(u1861,negated_conjecture,
( c1_2(X12,X13)
| ~ ndr1_1(X12)
| c3_2(X12,X13)
| c7_2(X12,X13)
| c1_1(X12)
| c2_1(X12) ) ).
cnf(u1895,negated_conjecture,
~ sP31 ).
cnf(u1923,negated_conjecture,
~ sP32 ).
cnf(u1927,negated_conjecture,
( c7_2(X3,a459)
| ~ c3_1(X3)
| ~ c8_1(X3) ) ).
cnf(u1931,negated_conjecture,
( ~ c3_2(X3,a459)
| ~ c3_1(X3)
| ~ c8_1(X3) ) ).
cnf(u1935,negated_conjecture,
( ~ c6_2(X3,a459)
| ~ c3_1(X3)
| ~ c8_1(X3) ) ).
cnf(u1939,negated_conjecture,
( ~ c8_1(X3)
| ndr1_1(X3)
| ~ c3_1(X3) ) ).
cnf(u1943,negated_conjecture,
( ~ c7_2(X1,X2)
| ~ ndr1_1(X1)
| ~ c6_1(X1)
| c3_2(X1,X2)
| c2_1(X1) ) ).
cnf(u2057,axiom,
~ c8_2(a577,a579) ).
cnf(u2062,axiom,
~ c6_2(a577,a579) ).
cnf(u2067,axiom,
ndr1_1(a577) ).
cnf(u2072,axiom,
c6_2(a577,a578) ).
cnf(u2077,axiom,
c1_2(a577,a578) ).
cnf(u2082,axiom,
c8_2(a577,a578) ).
cnf(u2088,axiom,
~ c7_1(a577) ).
cnf(u2561,axiom,
( ~ c6_2(X0,a480)
| ~ c2_1(X0)
| c3_1(X0) ) ).
cnf(u2565,axiom,
( c4_2(X0,a480)
| ~ c2_1(X0)
| c3_1(X0) ) ).
cnf(u2569,axiom,
( c3_2(X0,a480)
| ~ c2_1(X0)
| c3_1(X0) ) ).
cnf(u2573,axiom,
( ~ c2_1(X0)
| ndr1_1(X0)
| c3_1(X0) ) ).
cnf(u2693,negated_conjecture,
~ c6_1(a520) ).
cnf(u2735,negated_conjecture,
~ c6_2(a520,a521) ).
cnf(u2748,negated_conjecture,
~ c6_2(a570,a571) ).
cnf(u2751,negated_conjecture,
~ c4_2(a570,a571) ).
cnf(u2778,negated_conjecture,
~ c3_2(a577,a578) ).
cnf(u2818,negated_conjecture,
~ c4_2(a577,a548) ).
cnf(u2821,negated_conjecture,
c1_1(a577) ).
cnf(u2827,negated_conjecture,
c2_2(a577,a548) ).
cnf(u2849,negated_conjecture,
~ c6_1(a600) ).
cnf(u2888,negated_conjecture,
~ c6_1(a577) ).
cnf(u2902,negated_conjecture,
~ c6_1(a534) ).
cnf(u2914,negated_conjecture,
c1_1(a520) ).
cnf(u2939,negated_conjecture,
~ c3_1(a577) ).
cnf(u2944,negated_conjecture,
c2_2(a577,a481) ).
cnf(u2948,negated_conjecture,
~ c8_2(a577,a481) ).
cnf(u2975,negated_conjecture,
~ c6_2(a577,a481) ).
cnf(u2993,negated_conjecture,
~ c6_2(a577,a548) ).
cnf(u3020,negated_conjecture,
~ c4_2(a577,a481) ).
cnf(u3102,negated_conjecture,
c7_2(a534,a535) ).
cnf(u3121,negated_conjecture,
c5_1(a534) ).
cnf(u3170,negated_conjecture,
~ c4_2(a534,a572) ).
cnf(u3149,negated_conjecture,
( c2_2(X0,a572)
| ~ c4_1(X0)
| ~ sP3(X0)
| c2_2(X0,a589) ) ).
cnf(u240,axiom,
( c1_2(X0,a555)
| ~ sP9(X0) ) ).
cnf(u3205,negated_conjecture,
( ~ c7_2(X0,X1)
| c6_2(X0,a480)
| c7_2(X0,a480)
| ~ c6_1(X0)
| c5_1(X0)
| ~ c2_1(X0)
| c1_2(X0,a480)
| c2_2(X0,a480)
| c4_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u239,axiom,
( ~ c4_2(X0,a555)
| ~ sP9(X0) ) ).
cnf(u3091,negated_conjecture,
( ~ c4_2(X0,a589)
| c1_1(X0)
| c2_1(X0)
| c3_2(X0,a589)
| ~ sP3(X0) ) ).
cnf(u242,axiom,
( ~ sP9(X0)
| ndr1_1(X0) ) ).
cnf(u142,axiom,
( c5_2(X0,a486)
| ~ sP26(X0) ) ).
cnf(u2808,negated_conjecture,
~ c3_1(a581) ).
cnf(u2833,negated_conjecture,
( ~ c7_2(X0,X1)
| c3_1(X0)
| c1_2(X0,a480)
| c2_2(X0,a480)
| ~ c2_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u2861,negated_conjecture,
( ~ c8_1(X0)
| ~ c3_1(X0)
| ~ c6_1(X0) ) ).
cnf(u160,axiom,
( ~ c2_2(X0,a493)
| ~ sP22(X0) ) ).
cnf(u186,axiom,
( ~ c2_2(X0,a515)
| ~ sP18(X0) ) ).
cnf(u3068,negated_conjecture,
( ~ c6_2(X0,a589)
| ~ c1_1(X0)
| ~ c4_2(X0,a548)
| c3_2(X0,a589)
| ~ sP3(X0) ) ).
cnf(u3235,negated_conjecture,
( c5_2(X0,a515)
| c7_1(X0)
| ~ c1_1(X0)
| c6_2(X0,a576)
| c1_2(X0,a576)
| c8_1(X0)
| c2_2(X0,a576)
| ~ c6_1(X0)
| c4_2(X0,a515)
| c5_1(X0)
| ~ sP18(X0) ) ).
cnf(u3159,negated_conjecture,
( ~ c4_2(X0,a572)
| c2_2(X0,a589)
| ~ c4_1(X0)
| c6_2(X0,a589)
| c6_1(X0)
| ~ sP3(X0)
| c8_2(X0,a572) ) ).
cnf(u2673,negated_conjecture,
( ~ c7_2(X14,X15)
| ~ c2_1(X14)
| ~ ndr1_1(X14)
| c8_2(X14,X15)
| ~ c4_2(X14,X15) ) ).
cnf(u3069,negated_conjecture,
( ~ c6_2(X0,a589)
| ~ c1_1(X0)
| c2_2(X0,a548)
| c3_2(X0,a589)
| ~ sP3(X0) ) ).
cnf(u271,axiom,
( ~ c7_2(X0,a589)
| ~ sP3(X0) ) ).
cnf(u3082,negated_conjecture,
( ~ c4_2(X0,a589)
| c8_1(X0)
| c3_2(X0,a589)
| ~ sP3(X0)
| c4_1(X0) ) ).
cnf(u3266,negated_conjecture,
( c5_2(X0,a515)
| ~ c1_1(X0)
| ~ c6_1(X0)
| ~ c4_1(X0)
| c1_2(X0,a576)
| c2_2(X0,a576)
| c5_1(X0)
| c4_2(X0,a515)
| c7_1(X0)
| ~ sP18(X0) ) ).
cnf(u162,axiom,
( ~ c6_2(X0,a493)
| ~ sP22(X0) ) ).
cnf(u241,axiom,
( c5_2(X0,a555)
| ~ sP9(X0) ) ).
cnf(u2875,negated_conjecture,
( c1_2(X0,X1)
| c8_1(X0)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c4_1(X0)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c6_1(X0)
| c5_1(X0) ) ).
cnf(u3125,negated_conjecture,
( c5_2(X0,a515)
| c2_2(X0,a602)
| c1_2(X0,a602)
| c4_2(X0,a515)
| c8_1(X0)
| c7_1(X0)
| c2_1(X0)
| ~ sP18(X0) ) ).
cnf(u3057,negated_conjecture,
( c7_2(X0,a487)
| ~ c2_1(X0)
| c6_2(X0,a487)
| c5_1(X0)
| ~ c6_1(X0) ) ).
cnf(u103,axiom,
( ~ sP33(X0)
| ndr1_1(X0) ) ).
cnf(u270,axiom,
( ~ c5_2(X0,a589)
| ~ sP3(X0) ) ).
cnf(u3222,negated_conjecture,
( c6_2(X0,a487)
| ~ c2_1(X0)
| c5_1(X0)
| ~ c6_1(X0) ) ).
cnf(u3078,negated_conjecture,
( c5_2(X0,a515)
| c1_2(X0,a480)
| c2_2(X0,a480)
| ~ c2_1(X0)
| c4_2(X0,a515)
| c3_1(X0)
| ~ sP18(X0) ) ).
cnf(u2879,negated_conjecture,
( ~ c8_2(X0,a487)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u184,axiom,
( ~ c3_2(X0,a515)
| ~ sP18(X0) ) ).
cnf(u2829,negated_conjecture,
~ c2_1(a581) ).
cnf(u3130,negated_conjecture,
( ~ c4_2(X0,a486)
| ~ sP26(X0)
| c8_1(X0)
| c3_2(X0,a486)
| ~ c4_1(X0) ) ).
cnf(u3070,negated_conjecture,
( c1_2(X0,a589)
| c4_1(X0)
| c8_1(X0)
| c3_2(X0,a589)
| ~ sP3(X0) ) ).
cnf(u3036,negated_conjecture,
( ~ c4_2(X0,a457)
| ~ c2_1(X0)
| c8_2(X0,a457)
| ~ sP33(X0) ) ).
cnf(u2775,negated_conjecture,
~ c4_2(a577,a578) ).
cnf(u2677,negated_conjecture,
( ~ c8_2(X0,X1)
| c3_2(X0,X1)
| c7_2(X0,X1)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_1(X0)
| ~ c4_2(X0,X1) ) ).
cnf(u101,axiom,
( c7_2(X0,a457)
| ~ sP33(X0) ) ).
cnf(u145,axiom,
( ~ sP26(X0)
| ndr1_1(X0) ) ).
cnf(u2725,negated_conjecture,
( ~ c7_2(X0,X1)
| c8_1(X0)
| c2_2(X0,a602)
| c1_2(X0,a602)
| c4_2(X0,X1)
| c5_2(X0,X1)
| c7_1(X0)
| c2_1(X0) ) ).
cnf(u3032,negated_conjecture,
( c6_2(X0,a576)
| ~ c6_1(X0)
| c5_1(X0)
| c7_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) ) ).
cnf(u3226,negated_conjecture,
( c3_2(X0,a487)
| c5_1(X0)
| ~ c6_1(X0)
| ~ c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u3072,negated_conjecture,
( ~ c8_2(X0,a493)
| ~ sP22(X0)
| ~ c4_2(X0,a493) ) ).
cnf(u187,axiom,
( ~ sP18(X0)
| ndr1_1(X0) ) ).
cnf(u3209,negated_conjecture,
( c3_2(X0,a576)
| c5_1(X0)
| c7_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| ~ c4_1(X0) ) ).
cnf(u3199,negated_conjecture,
( c3_2(X0,a480)
| c4_1(X0)
| c6_2(X0,a480)
| c7_2(X0,a480)
| ~ c6_1(X0)
| c5_1(X0)
| ~ c2_1(X0) ) ).
cnf(u272,axiom,
( c8_2(X0,a589)
| ~ sP3(X0) ) ).
cnf(u3092,negated_conjecture,
( ~ c4_2(X0,X1)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c6_2(X0,X1)
| c5_1(X0) ) ).
cnf(u3154,negated_conjecture,
( ~ c6_2(X0,a572)
| ~ sP3(X0)
| c2_2(X0,a589)
| ~ c8_1(X0)
| ~ c4_1(X0)
| c3_2(X0,a572)
| c8_2(X0,X1)
| c2_2(X0,X1)
| c7_2(X0,X1) ) ).
cnf(u163,axiom,
( ~ sP22(X0)
| ndr1_1(X0) ) ).
cnf(u3257,negated_conjecture,
( c5_2(X0,a515)
| c7_2(X0,a480)
| ~ c6_1(X0)
| c5_1(X0)
| c1_2(X0,a480)
| c2_2(X0,a480)
| c4_1(X0)
| c4_2(X0,a515)
| c6_2(X0,a480)
| ~ sP18(X0) ) ).
cnf(u3241,negated_conjecture,
( ~ c7_2(X0,X1)
| c7_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c6_1(X0)
| ~ c4_1(X0)
| c1_2(X0,a576)
| c2_2(X0,a576)
| c5_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u3147,negated_conjecture,
( ~ c7_2(X0,X1)
| c5_1(X0)
| c7_1(X0)
| ~ c1_1(X0)
| c6_2(X0,a576)
| c1_2(X0,a576)
| c8_1(X0)
| c2_2(X0,a576)
| ~ ndr1_1(X0)
| ~ c6_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u3135,negated_conjecture,
( ~ c4_2(X0,X1)
| ~ ndr1_1(X0)
| c3_2(X0,X1)
| c4_1(X0)
| c6_2(X0,X1)
| c7_2(X0,X1)
| ~ c6_1(X0)
| c5_1(X0)
| c8_1(X0) ) ).
cnf(u3189,negated_conjecture,
( ~ c8_2(X0,a486)
| ~ sP26(X0)
| ~ c4_2(X0,a486) ) ).
cnf(u100,axiom,
( c5_2(X0,a457)
| ~ sP33(X0) ) ).
cnf(u144,axiom,
( c6_2(X0,a486)
| ~ sP26(X0) ) ).
cnf(u2836,negated_conjecture,
( c7_2(X0,a576)
| c6_2(X0,a576)
| ~ ndr1_1(X0)
| ~ c6_1(X0)
| c5_1(X0)
| c7_1(X0)
| ~ c1_1(X0) ) ).
cnf(u185,axiom,
( c7_2(X0,a515)
| ~ sP18(X0) ) ).
cnf(u3029,negated_conjecture,
( c3_2(X0,a576)
| ~ c6_1(X0)
| c5_1(X0)
| c7_1(X0)
| ~ c1_1(X0)
| c6_2(X0,a576)
| c2_1(X0) ) ).
cnf(u3050,negated_conjecture,
c2_1(a536) ).
cnf(u3053,negated_conjecture,
c3_1(a536) ).
cnf(u143,axiom,
( c1_2(X0,a486)
| ~ sP26(X0) ) ).
cnf(u3075,negated_conjecture,
( ~ c4_2(X0,a493)
| ~ sP22(X0)
| c7_2(X0,a493)
| ~ c6_1(X0)
| c5_1(X0) ) ).
cnf(u102,axiom,
( ~ c6_2(X0,a457)
| ~ sP33(X0) ) ).
cnf(u3153,negated_conjecture,
( ~ c8_2(X0,X1)
| ~ sP3(X0)
| c2_2(X0,a589)
| ~ c4_1(X0)
| c6_2(X0,X1)
| c2_2(X0,X1)
| c6_1(X0)
| ~ c4_2(X0,a572)
| c8_2(X0,a572) ) ).
cnf(u273,axiom,
( ~ sP3(X0)
| ndr1_1(X0) ) ).
cnf(u3048,negated_conjecture,
( ~ sP18(X0)
| ~ c6_1(X0)
| c2_1(X0) ) ).
cnf(u161,axiom,
( c1_2(X0,a493)
| ~ sP22(X0) ) ).
cnf(u3035,negated_conjecture,
( c3_2(X0,a457)
| ~ c6_1(X0)
| ~ sP33(X0)
| c2_1(X0) ) ).
cnf(u3041,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ sP33(X0)
| c2_1(X0)
| c1_2(X0,a457)
| c8_1(X0)
| c2_2(X0,a457)
| ~ c6_1(X0)
| c4_2(X0,X1)
| c5_2(X0,X1) ) ).
cnf(u3047,negated_conjecture,
( ~ c4_2(X0,a515)
| ~ c2_1(X0)
| c8_2(X0,a515)
| ~ sP18(X0) ) ).
%------------------------------------------------------------------------------
%----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/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.18 % Computer : n018.cluster.edu
% 0.12/0.18 % Model : x86_64 x86_64
% 0.12/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.18 % Memory : 8046.5625MB
% 0.12/0.18 % OS : Linux 6.8.0-71-generic
% 0.12/0.18 % CPULimit : 300
% 0.12/0.18 % WCLimit : 300
% 0.12/0.18 % DateTime : Mon Sep 28 16:30:21 UTC 2026
% 0.12/0.18 % CPUTime :
% 0.12/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.21 Running first-order theorem proving
% 0.12/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.29/1.82 % (3522061)Detected formulas, will run a generic FOF schedule.
% 6.29/1.82 % (3522069)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1579775214:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.29/1.82 % (3522068)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3069537556:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.29/1.82 % (3522071)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2406354394:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.29/1.82 % (3522066)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2750401404:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.29/1.82 % (3522070)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2666415950:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.29/1.82 % (3522067)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3083524323:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.29/1.82 % (3522072)dis-21_1_sil=8000:lcm=predicate:random_seed=3755322675:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 6.29/1.82 % (3522069)Instruction limit reached!
% 6.29/1.82 % (3522069)------------------------------
% 6.29/1.82 % (3522069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522069)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522069)Termination reason: Instruction limit
% 6.29/1.82 % (3522069)Termination phase: Saturation
% 6.29/1.82 % (3522069)Time elapsed: 0.035 s
% 6.29/1.82 % (3522069)Peak memory usage: 90 MB
% 6.29/1.82 % (3522069)Instructions burned: 112 (million)
% 6.29/1.82 % (3522071)Refutation not found, incomplete strategy
% 6.29/1.82 % (3522071)------------------------------
% 6.29/1.82 % (3522071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522071)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522071)Termination reason: Refutation not found, incomplete strategy
% 6.29/1.82 % (3522071)Time elapsed: 0.017 s
% 6.29/1.82 % (3522071)Peak memory usage: 90 MB
% 6.29/1.82 % (3522071)Instructions burned: 26 (million)
% 6.29/1.82 % (3522070)Instruction limit reached!
% 6.29/1.82 % (3522070)------------------------------
% 6.29/1.82 % (3522070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522070)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522070)Termination reason: Instruction limit
% 6.29/1.82 % (3522070)Termination phase: Saturation
% 6.29/1.82 % (3522070)Time elapsed: 0.063 s
% 6.29/1.82 % (3522070)Peak memory usage: 88 MB
% 6.29/1.82 % (3522070)Instructions burned: 120 (million)
% 6.29/1.82 % (3522072)Instruction limit reached!
% 6.29/1.82 % (3522072)------------------------------
% 6.29/1.82 % (3522072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522072)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522072)Termination reason: Instruction limit
% 6.29/1.82 % (3522072)Termination phase: Saturation
% 6.29/1.82 % (3522072)Time elapsed: 0.069 s
% 6.29/1.82 % (3522072)Peak memory usage: 90 MB
% 6.29/1.82 % (3522072)Instructions burned: 129 (million)
% 6.29/1.82 % (3522080)lrs+10_1_sil=8000:sp=occurrence:random_seed=1782747044:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 6.29/1.82 % (3522080)Instruction limit reached!
% 6.29/1.82 % (3522080)------------------------------
% 6.29/1.82 % (3522080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522080)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522080)Termination reason: Instruction limit
% 6.29/1.82 % (3522080)Termination phase: Saturation
% 6.29/1.82 % (3522080)Time elapsed: 0.078 s
% 6.29/1.82 % (3522080)Peak memory usage: 92 MB
% 6.29/1.82 % (3522080)Instructions burned: 289 (million)
% 6.29/1.82 % (3522081)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2470386290:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.29/1.82 % (3522082)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1711926607:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.29/1.82 % (3522082)Refutation not found, incomplete strategy
% 6.29/1.82 % (3522082)------------------------------
% 6.29/1.82 % (3522082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522082)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522082)Termination reason: Refutation not found, incomplete strategy
% 6.29/1.82 % (3522082)Time elapsed: 0.017 s
% 6.29/1.82 % (3522082)Peak memory usage: 90 MB
% 6.29/1.82 % (3522082)Instructions burned: 25 (million)
% 6.29/1.82 % (3522081)Refutation not found, incomplete strategy
% 6.29/1.82 % (3522081)------------------------------
% 6.29/1.82 % (3522081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522081)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522081)Termination reason: Refutation not found, incomplete strategy
% 6.29/1.82 % (3522081)Time elapsed: 0.017 s
% 6.29/1.82 % (3522081)Peak memory usage: 90 MB
% 6.29/1.82 % (3522081)Instructions burned: 26 (million)
% 6.29/1.82 % (3522071)------------------------------
% 6.29/1.82 % (3522071)------------------------------
% 6.29/1.82 % (3522084)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1593943320:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 6.29/1.82 % (3522084)Refutation not found, incomplete strategy
% 6.29/1.82 % (3522084)------------------------------
% 6.29/1.82 % (3522084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522084)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522084)Termination reason: Refutation not found, incomplete strategy
% 6.29/1.82 % (3522084)Time elapsed: 0.010 s
% 6.29/1.82 % (3522084)Peak memory usage: 90 MB
% 6.29/1.82 % (3522084)Instructions burned: 27 (million)
% 6.29/1.82 % (3522087)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3813167154:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.29/1.82 % (3522084)------------------------------
% 6.29/1.82 % (3522084)------------------------------
% 6.29/1.82 % (3522081)------------------------------
% 6.29/1.82 % (3522081)------------------------------
% 6.29/1.82 % (3522082)------------------------------
% 6.29/1.82 % (3522082)------------------------------
% 6.29/1.82 % (3522087)Instruction limit reached!
% 6.29/1.82 % (3522087)------------------------------
% 6.29/1.82 % (3522087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522087)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522087)Termination reason: Instruction limit
% 6.29/1.82 % (3522087)Termination phase: Saturation
% 6.29/1.82 % (3522087)Time elapsed: 0.167 s
% 6.29/1.82 % (3522087)Peak memory usage: 91 MB
% 6.29/1.82 % (3522087)Instructions burned: 295 (million)
% 6.29/1.82 % (3522090)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1158399602:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 6.29/1.82 % (3522091)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2046023635:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 6.29/1.82 % (3522092)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=464517902:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 6.29/1.82 % (3522091)Refutation not found, incomplete strategy
% 6.29/1.82 % (3522091)------------------------------
% 6.29/1.82 % (3522091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522091)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522091)Termination reason: Refutation not found, incomplete strategy
% 6.29/1.82 % (3522091)Time elapsed: 0.049 s
% 6.29/1.82 % (3522091)Peak memory usage: 91 MB
% 6.29/1.82 % (3522091)Instructions burned: 79 (million)
% 6.29/1.82 % (3522092)Instruction limit reached!
% 6.29/1.82 % (3522092)------------------------------
% 6.29/1.82 % (3522092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522092)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522092)Termination reason: Instruction limit
% 6.29/1.82 % (3522092)Termination phase: Saturation
% 6.29/1.82 % (3522092)Time elapsed: 0.066 s
% 6.29/1.82 % (3522092)Peak memory usage: 89 MB
% 6.29/1.82 % (3522092)Instructions burned: 128 (million)
% 6.29/1.82 % (3522066)First to succeed.
% 6.29/1.82 % (3522066)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3522061"
% 6.29/1.82 % (3522067)Also succeeded, but the first one will report.
% 6.29/1.82 % (3522093)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=425900446:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 6.29/1.82 % (3522093)Refutation not found, incomplete strategy
% 6.29/1.82 % (3522093)------------------------------
% 6.29/1.82 % (3522093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.29/1.82 % (3522093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.29/1.82 % (3522093)CaDiCaL version: 2.1.3
% 6.29/1.82 % (3522093)Termination reason: Refutation not found, incomplete strategy
% 6.29/1.82 % (3522093)Time elapsed: 0.039 s
% 6.29/1.82 % (3522093)Peak memory usage: 90 MB
% 6.29/1.82 % (3522093)Instructions burned: 71 (million)
% 6.29/1.82 % (3522097)lrs+10_1_sil=8000:sp=occurrence:random_seed=2195166742:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 6.29/1.82 % (3522091)------------------------------
% 6.29/1.82 % (3522091)------------------------------
% 6.29/1.82 % SZS status CounterSatisfiable for theBenchmark
% 6.29/1.82 % SZS output start Saturation.
% See solution above
% 8.77/2.02 % SZS output start Definitions and Model Updates.
% 8.77/2.02 for all inputs,
% 8.77/2.02 define c4_0 := $false
% 8.77/2.02 for all inputs,
% 8.77/2.02 define c3_0 := $true
% 8.77/2.02 % SZS output end Definitions and Model Updates.
% 8.77/2.02 % (3522066)------------------------------
% 8.77/2.02 % (3522066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.77/2.02 % (3522066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.77/2.02 % (3522066)CaDiCaL version: 2.1.3
% 8.77/2.02 % (3522066)Termination reason: Satisfiable
% 8.77/2.02 % (3522066)Time elapsed: 0.734 s
% 8.77/2.02 % (3522066)Peak memory usage: 132 MB
% 8.77/2.02 % (3522066)Instructions burned: 1076 (million)
% 8.77/2.02 % (3522066)------------------------------
% 8.77/2.02 % (3522066)------------------------------
% 8.77/2.02 % (3522061)Success in time 1.172 s
% 8.77/2.02 % Vampire exiting
%------------------------------------------------------------------------------