%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN418+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 01:50:33 PM UTC 2026
% Result : CounterSatisfiable 3.59s 1.15s
% Output : Saturation 3.98s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u722,negated_conjecture,
~ c5_0 ).
cnf(u726,negated_conjecture,
( ~ c2_2(X124,X125)
| c3_1(X124)
| c2_2(X124,X126)
| c10_2(X124,X126)
| ~ c7_2(X124,X126)
| ~ ndr1_1(X124)
| ~ c7_2(X124,X125)
| ~ c1_2(X124,X125) ) ).
cnf(u729,negated_conjecture,
ndr1_0 ).
cnf(u737,negated_conjecture,
~ sP0 ).
cnf(u741,negated_conjecture,
( ~ c5_2(X121,a145)
| ~ c1_1(X121)
| c9_1(X121) ) ).
cnf(u748,negated_conjecture,
( c1_2(X121,a145)
| ~ c1_1(X121)
| c9_1(X121) ) ).
cnf(u752,negated_conjecture,
( c3_2(X121,a145)
| ~ c1_1(X121)
| c9_1(X121) ) ).
cnf(u756,negated_conjecture,
( ~ c1_1(X121)
| c9_1(X121)
| ndr1_1(X121) ) ).
cnf(u760,negated_conjecture,
~ c2_0 ).
cnf(u764,negated_conjecture,
( ~ c3_2(X118,X119)
| c2_1(X118)
| ~ ndr1_1(X118)
| c8_2(X118,X119)
| c7_2(X118,X119) ) ).
cnf(u771,negated_conjecture,
~ c3_0 ).
cnf(u775,negated_conjecture,
~ c1_0 ).
cnf(u780,negated_conjecture,
c6_0 ).
cnf(u788,negated_conjecture,
c9_0 ).
cnf(u796,negated_conjecture,
~ c4_0 ).
cnf(u801,negated_conjecture,
c10_0 ).
cnf(u827,negated_conjecture,
c8_0 ).
cnf(u849,negated_conjecture,
~ sP1 ).
cnf(u870,negated_conjecture,
~ c8_1(a136) ).
cnf(u875,negated_conjecture,
~ c10_2(a136,a137) ).
cnf(u880,negated_conjecture,
~ c5_2(a136,a137) ).
cnf(u885,negated_conjecture,
c2_2(a136,a137) ).
cnf(u890,negated_conjecture,
ndr1_1(a136) ).
cnf(u895,negated_conjecture,
c7_1(a136) ).
cnf(u901,negated_conjecture,
c3_2(a134,a135) ).
cnf(u906,negated_conjecture,
~ c6_2(a134,a135) ).
cnf(u911,negated_conjecture,
~ c8_2(a134,a135) ).
cnf(u916,negated_conjecture,
ndr1_1(a134) ).
cnf(u921,negated_conjecture,
c10_1(a134) ).
cnf(u925,negated_conjecture,
( ~ c2_2(a134,X110)
| ~ c5_2(a134,X110)
| ~ c7_2(a134,X110) ) ).
cnf(u930,negated_conjecture,
~ sP2 ).
cnf(u934,negated_conjecture,
~ sP3 ).
cnf(u938,negated_conjecture,
( ~ c7_2(X107,X108)
| c2_2(X107,a131)
| c2_2(X107,X109)
| c9_2(X107,X109)
| ~ c6_2(X107,X109)
| ~ ndr1_1(X107)
| ~ c6_2(X107,X108)
| c9_2(X107,X108) ) ).
cnf(u942,negated_conjecture,
( ~ c7_2(X107,X108)
| ~ c1_2(X107,a131)
| c2_2(X107,X109)
| c9_2(X107,X109)
| ~ c6_2(X107,X109)
| ~ ndr1_1(X107)
| ~ c6_2(X107,X108)
| c9_2(X107,X108) ) ).
cnf(u946,negated_conjecture,
( ~ c10_2(X107,a131)
| ~ c7_2(X107,X108)
| c2_2(X107,X109)
| c9_2(X107,X109)
| ~ c6_2(X107,X109)
| ~ ndr1_1(X107)
| ~ c6_2(X107,X108)
| c9_2(X107,X108) ) ).
cnf(u961,negated_conjecture,
( c5_1(X102)
| c1_1(X102) ) ).
cnf(u977,negated_conjecture,
~ c4_1(a128) ).
cnf(u982,negated_conjecture,
~ c1_1(a128) ).
cnf(u986,negated_conjecture,
ndr1_1(a128) ).
cnf(u990,negated_conjecture,
( ~ c4_2(a128,X98)
| c6_2(a128,X98)
| ~ c1_2(a128,X98) ) ).
cnf(u995,negated_conjecture,
ndr1_1(a127) ).
cnf(u1004,negated_conjecture,
~ c2_1(a127) ).
cnf(u1009,negated_conjecture,
c4_1(a127) ).
cnf(u1022,negated_conjecture,
~ sP4 ).
cnf(u1033,negated_conjecture,
( ~ c2_2(X94,X95)
| c5_1(X94)
| c7_1(X94)
| ~ ndr1_1(X94)
| c10_2(X94,X95)
| c4_2(X94,X95) ) ).
cnf(u1038,negated_conjecture,
~ sP5 ).
cnf(u1043,negated_conjecture,
~ c10_1(a121) ).
cnf(u1048,negated_conjecture,
~ c6_1(a121) ).
cnf(u1053,negated_conjecture,
~ c9_1(a121) ).
cnf(u1058,negated_conjecture,
~ sP6 ).
cnf(u1062,negated_conjecture,
( c5_2(X93,a118)
| ~ c2_1(X93)
| ~ c4_1(X93) ) ).
cnf(u1066,negated_conjecture,
( ~ c9_2(X93,a118)
| ~ c2_1(X93)
| ~ c4_1(X93) ) ).
cnf(u1070,negated_conjecture,
( ~ c2_2(X93,a118)
| ~ c2_1(X93)
| ~ c4_1(X93) ) ).
cnf(u1074,negated_conjecture,
( ~ c2_1(X93)
| ndr1_1(X93)
| ~ c4_1(X93) ) ).
cnf(u1099,negated_conjecture,
ndr1_1(a114) ).
cnf(u1103,negated_conjecture,
( ~ c8_2(a114,X92)
| c1_2(a114,X92)
| c10_2(a114,X92) ) ).
cnf(u1108,negated_conjecture,
~ c4_2(a114,a115) ).
cnf(u1113,negated_conjecture,
c2_2(a114,a115) ).
cnf(u1118,negated_conjecture,
~ c5_2(a114,a115) ).
cnf(u1124,negated_conjecture,
~ c1_1(a114) ).
cnf(u1129,negated_conjecture,
~ sP7 ).
cnf(u1133,negated_conjecture,
( ~ c4_2(X90,X91)
| ~ ndr1_1(X90)
| c8_2(X90,X91)
| ~ c3_2(X90,a111)
| c10_2(X90,X91) ) ).
cnf(u1137,negated_conjecture,
( ~ c4_2(X90,X91)
| ~ ndr1_1(X90)
| c8_2(X90,X91)
| c4_2(X90,a111)
| c10_2(X90,X91) ) ).
cnf(u1141,negated_conjecture,
( ~ c4_2(X90,X91)
| ~ ndr1_1(X90)
| c8_2(X90,X91)
| c5_2(X90,a111)
| c10_2(X90,X91) ) ).
cnf(u1145,negated_conjecture,
( ~ c3_1(X88)
| ~ ndr1_1(X88)
| ~ c6_2(X88,X89)
| ~ c3_2(X88,X89)
| ~ c7_2(X88,X89)
| c8_1(X88) ) ).
cnf(u1158,negated_conjecture,
sP8 ).
cnf(u1161,negated_conjecture,
~ sP9 ).
cnf(u1169,negated_conjecture,
( ~ c5_2(X80,X81)
| ~ c5_1(X80)
| c9_1(X80)
| ~ ndr1_1(X80)
| c3_2(X80,X81)
| c10_2(X80,X81) ) ).
cnf(u1181,negated_conjecture,
~ sP10 ).
cnf(u1186,negated_conjecture,
c9_2(a100,a101) ).
cnf(u1191,negated_conjecture,
~ c5_2(a100,a101) ).
cnf(u1196,negated_conjecture,
~ c6_2(a100,a101) ).
cnf(u1201,negated_conjecture,
ndr1_1(a100) ).
cnf(u1206,negated_conjecture,
c9_1(a100) ).
cnf(u1210,negated_conjecture,
( ~ c7_2(a100,X79)
| c2_2(a100,X79)
| ~ c3_2(a100,X79) ) ).
cnf(u1215,negated_conjecture,
~ sP11 ).
cnf(u1264,negated_conjecture,
~ c7_0 ).
cnf(u1269,negated_conjecture,
~ c2_1(a93) ).
cnf(u1274,negated_conjecture,
~ c8_1(a93) ).
cnf(u1279,negated_conjecture,
~ c2_2(a93,a94) ).
cnf(u1284,negated_conjecture,
~ c7_2(a93,a94) ).
cnf(u1289,negated_conjecture,
c4_2(a93,a94) ).
cnf(u1294,negated_conjecture,
ndr1_1(a93) ).
cnf(u1299,negated_conjecture,
( ~ c4_2(X76,X77)
| ~ ndr1_1(X76)
| ~ c8_2(X76,X77)
| ~ c6_2(X76,X77)
| ~ c8_1(X76)
| c10_2(X76,a92) ) ).
cnf(u1302,negated_conjecture,
~ sP12 ).
cnf(u1307,negated_conjecture,
( ~ c4_2(X76,X77)
| ~ ndr1_1(X76)
| ~ c8_2(X76,X77)
| ~ c6_2(X76,X77)
| ~ c8_1(X76)
| c9_2(X76,a92) ) ).
cnf(u1311,negated_conjecture,
( ~ c4_2(X76,X77)
| ~ ndr1_1(X76)
| ~ c8_2(X76,X77)
| ~ c6_2(X76,X77)
| ~ c8_1(X76)
| c8_2(X76,a92) ) ).
cnf(u1315,negated_conjecture,
( c4_2(X75,a89)
| ~ c6_1(X75)
| c4_1(X75) ) ).
cnf(u1318,negated_conjecture,
~ sP13 ).
cnf(u1323,negated_conjecture,
( c10_2(X75,a89)
| ~ c6_1(X75)
| c4_1(X75) ) ).
cnf(u1327,negated_conjecture,
( ~ c9_2(X75,a89)
| ~ c6_1(X75)
| c4_1(X75) ) ).
cnf(u1331,negated_conjecture,
( ~ c6_1(X75)
| ndr1_1(X75)
| c4_1(X75) ) ).
cnf(u1335,negated_conjecture,
( ~ c8_2(X74,a84)
| sP14(X74)
| sP15(X74) ) ).
cnf(u1339,negated_conjecture,
( c5_2(X74,a84)
| sP14(X74)
| sP15(X74) ) ).
cnf(u1343,negated_conjecture,
( c9_2(X74,a84)
| sP14(X74)
| sP15(X74) ) ).
cnf(u1347,negated_conjecture,
( ndr1_1(X74)
| sP14(X74)
| sP15(X74) ) ).
cnf(u1351,negated_conjecture,
( ~ c2_2(X72,X73)
| ~ c3_1(X72)
| c6_2(X72,a83)
| ~ ndr1_1(X72)
| ~ c5_2(X72,X73)
| ~ c3_2(X72,X73) ) ).
cnf(u1402,negated_conjecture,
c4_1(a77) ).
cnf(u1407,negated_conjecture,
c5_2(a77,a78) ).
cnf(u1412,negated_conjecture,
~ c8_2(a77,a78) ).
cnf(u1417,negated_conjecture,
~ c1_2(a77,a78) ).
cnf(u1422,negated_conjecture,
ndr1_1(a77) ).
cnf(u1427,negated_conjecture,
~ c2_1(a77) ).
cnf(u1432,negated_conjecture,
~ sP17 ).
cnf(u1437,negated_conjecture,
~ c2_1(a75) ).
cnf(u1442,negated_conjecture,
~ c9_1(a75) ).
cnf(u1446,negated_conjecture,
ndr1_1(a75) ).
cnf(u1450,negated_conjecture,
( ~ c6_2(a75,X68)
| c4_2(a75,X68)
| ~ c5_2(a75,X68) ) ).
cnf(u1470,negated_conjecture,
ndr1_1(X67) ).
cnf(u1479,negated_conjecture,
~ c7_1(a73) ).
cnf(u1484,negated_conjecture,
~ c4_1(a73) ).
cnf(u1488,negated_conjecture,
ndr1_1(a73) ).
cnf(u1492,negated_conjecture,
( ~ c10_2(a73,X61)
| ~ c7_2(a73,X61)
| c5_2(a73,X61) ) ).
cnf(u1500,negated_conjecture,
( ~ c8_2(X59,X60)
| c10_1(X59)
| ~ ndr1_1(X59)
| ~ c7_2(X59,X60)
| c10_2(X59,X60)
| c1_1(X59) ) ).
cnf(u1532,negated_conjecture,
( ~ c5_2(X54,X55)
| ~ c1_1(X54)
| ~ ndr1_1(X54)
| c2_2(X54,X55)
| c3_2(X54,X55)
| ~ c3_2(X54,a70) ) ).
cnf(u1535,negated_conjecture,
~ sP18 ).
cnf(u1540,negated_conjecture,
( ~ c4_2(X54,a70)
| ~ c1_1(X54)
| ~ ndr1_1(X54)
| c2_2(X54,X55)
| c3_2(X54,X55)
| ~ c5_2(X54,X55) ) ).
cnf(u1544,negated_conjecture,
( ~ c5_2(X54,a70)
| ~ c1_1(X54)
| ~ ndr1_1(X54)
| c2_2(X54,X55)
| c3_2(X54,X55)
| ~ c5_2(X54,X55) ) ).
cnf(u1548,negated_conjecture,
~ sP19 ).
cnf(u1553,negated_conjecture,
c4_1(a66) ).
cnf(u1558,negated_conjecture,
~ c9_1(a66) ).
cnf(u1562,negated_conjecture,
ndr1_1(a66) ).
cnf(u1566,negated_conjecture,
( c1_2(a66,X53)
| c3_2(a66,X53) ) ).
cnf(u1583,negated_conjecture,
~ sP23 ).
cnf(u1590,negated_conjecture,
( ~ c3_1(X49)
| c8_1(X49) ) ).
cnf(u1599,negated_conjecture,
~ c9_1(a59) ).
cnf(u1602,negated_conjecture,
~ sP25 ).
cnf(u1607,negated_conjecture,
ndr1_1(a59) ).
cnf(u1624,negated_conjecture,
~ sP26 ).
cnf(u1629,negated_conjecture,
~ c10_1(a55) ).
cnf(u1634,negated_conjecture,
~ c6_1(a55) ).
cnf(u1662,negated_conjecture,
( ~ c7_2(X41,X42)
| c3_2(X41,a52)
| c10_1(X41)
| ~ ndr1_1(X41)
| c10_2(X41,X42) ) ).
cnf(u1666,negated_conjecture,
( ~ c9_2(X41,a52)
| c10_2(X41,X42)
| c10_1(X41)
| ~ ndr1_1(X41)
| ~ c7_2(X41,X42) ) ).
cnf(u1670,negated_conjecture,
( ~ c7_2(X41,X42)
| c8_2(X41,a52)
| c10_1(X41)
| ~ ndr1_1(X41)
| c10_2(X41,X42) ) ).
cnf(u1675,negated_conjecture,
c2_1(a51) ).
cnf(u1680,negated_conjecture,
c6_1(a51) ).
cnf(u1684,negated_conjecture,
ndr1_1(a51) ).
cnf(u1688,negated_conjecture,
( ~ c4_2(a51,X40)
| ~ c9_2(a51,X40)
| ~ c1_2(a51,X40) ) ).
cnf(u1698,negated_conjecture,
( ~ c2_1(X37)
| c3_1(X37)
| ~ c8_1(X37) ) ).
cnf(u1708,negated_conjecture,
~ sP28 ).
cnf(u1712,negated_conjecture,
( ~ c8_1(X34)
| c1_1(X34) ) ).
cnf(u1729,negated_conjecture,
c3_1(a44) ).
cnf(u1734,negated_conjecture,
c4_1(a44) ).
cnf(u1738,negated_conjecture,
ndr1_1(a44) ).
cnf(u1759,negated_conjecture,
~ sP29 ).
cnf(u1777,negated_conjecture,
~ sP31 ).
cnf(u1781,negated_conjecture,
( ~ c4_2(X26,X28)
| c3_2(X26,X28)
| c5_2(X26,X28)
| ~ c2_2(X26,X27)
| ~ c3_2(X26,a39)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c10_2(X26,X27) ) ).
cnf(u1784,negated_conjecture,
~ sP30 ).
cnf(u1789,negated_conjecture,
( ~ c4_2(X26,X28)
| c3_2(X26,X28)
| c5_2(X26,X28)
| ~ c2_2(X26,X27)
| ~ c9_2(X26,a39)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c10_2(X26,X27) ) ).
cnf(u1793,negated_conjecture,
( ~ c4_2(X26,X28)
| c3_2(X26,X28)
| c5_2(X26,X28)
| ~ c2_2(X26,X27)
| c2_2(X26,a39)
| ~ ndr1_1(X26)
| ~ c5_2(X26,X27)
| c10_2(X26,X27) ) ).
cnf(u1797,negated_conjecture,
~ sP32 ).
cnf(u1801,negated_conjecture,
~ sP33 ).
cnf(u1805,negated_conjecture,
ndr1_1(a31) ).
cnf(u1809,negated_conjecture,
( ~ c2_2(a31,X25)
| c6_2(a31,X25)
| c1_2(a31,X25) ) ).
cnf(u1814,negated_conjecture,
~ c5_1(a31) ).
cnf(u1819,negated_conjecture,
c8_2(a31,a32) ).
cnf(u1824,negated_conjecture,
c3_2(a31,a32) ).
cnf(u1829,negated_conjecture,
~ c7_2(a31,a32) ).
cnf(u1942,negated_conjecture,
sP34 ).
cnf(u1945,negated_conjecture,
~ sP35 ).
cnf(u1954,negated_conjecture,
c3_1(a18) ).
cnf(u1957,negated_conjecture,
~ sP36 ).
cnf(u1962,negated_conjecture,
ndr1_1(a18) ).
cnf(u1970,negated_conjecture,
~ c6_1(a18) ).
cnf(u2001,negated_conjecture,
~ sP37 ).
cnf(u2017,negated_conjecture,
~ sP38 ).
cnf(u2021,negated_conjecture,
( ~ c10_2(X3,X4)
| ~ ndr1_1(X3)
| ~ c1_2(X3,X4)
| c10_1(X3)
| c3_2(X3,X4)
| ~ c7_1(X3) ) ).
cnf(u2037,negated_conjecture,
~ sP39 ).
cnf(u2042,negated_conjecture,
~ c4_1(a6) ).
cnf(u2047,negated_conjecture,
~ c6_1(a6) ).
cnf(u2052,negated_conjecture,
c10_1(a6) ).
cnf(u2057,negated_conjecture,
( ~ c7_1(X0)
| c6_1(X0) ) ).
cnf(u2060,negated_conjecture,
~ sP40 ).
cnf(u2290,axiom,
~ c2_2(a108,a110) ).
cnf(u2295,axiom,
c3_2(a108,a110) ).
cnf(u2300,axiom,
ndr1_1(a108) ).
cnf(u2304,axiom,
( ~ c2_2(a108,X0)
| ~ c7_2(a108,X0) ) ).
cnf(u2309,axiom,
~ c2_2(a108,a109) ).
cnf(u2314,axiom,
c1_2(a108,a109) ).
cnf(u2319,axiom,
~ c7_2(a108,a109) ).
cnf(u2746,axiom,
c8_1(a22) ).
cnf(u2751,axiom,
~ c2_2(a22,a24) ).
cnf(u2756,axiom,
~ c1_2(a22,a24) ).
cnf(u2761,axiom,
~ c6_2(a22,a24) ).
cnf(u2766,axiom,
ndr1_1(a22) ).
cnf(u2771,axiom,
c10_2(a22,a23) ).
cnf(u2776,axiom,
c7_2(a22,a23) ).
cnf(u2781,axiom,
c2_2(a22,a23) ).
cnf(u3034,negated_conjecture,
~ c8_1(a51) ).
cnf(u3045,negated_conjecture,
~ c6_1(a128) ).
cnf(u3060,negated_conjecture,
~ c6_1(a73) ).
cnf(u3080,negated_conjecture,
c7_2(a134,a135) ).
cnf(u3095,negated_conjecture,
c10_2(a93,a94) ).
cnf(u3099,negated_conjecture,
~ c3_2(a93,a111) ).
cnf(u3122,negated_conjecture,
c10_2(a114,a115) ).
cnf(u3125,negated_conjecture,
~ c7_1(a114) ).
cnf(u3153,negated_conjecture,
~ c5_1(a77) ).
cnf(u3166,negated_conjecture,
~ c7_1(a93) ).
cnf(u3197,negated_conjecture,
~ c1_2(a114,a115) ).
cnf(u3224,negated_conjecture,
~ c3_2(a77,a70) ).
cnf(u3259,negated_conjecture,
~ c7_2(a136,a137) ).
cnf(u3277,negated_conjecture,
~ c3_2(a93,a39) ).
cnf(u3284,negated_conjecture,
c5_2(a93,a94) ).
cnf(u3293,negated_conjecture,
~ c9_2(a93,a39) ).
cnf(u3311,negated_conjecture,
~ c3_2(a93,a70) ).
cnf(u3321,negated_conjecture,
~ c7_2(a108,a110) ).
cnf(u3326,negated_conjecture,
c8_2(a108,a110) ).
cnf(u3386,negated_conjecture,
~ c7_1(a66) ).
cnf(u3415,negated_conjecture,
~ c7_1(a22) ).
cnf(u3418,negated_conjecture,
~ c3_2(a22,a23) ).
cnf(u3427,negated_conjecture,
~ c1_2(a22,a23) ).
cnf(u3442,negated_conjecture,
~ c6_2(a22,a23) ).
cnf(u3498,negated_conjecture,
~ c7_2(a73,a50) ).
cnf(u3519,negated_conjecture,
~ c7_2(a134,a58) ).
cnf(u3540,negated_conjecture,
~ sP24(a31) ).
cnf(u3563,negated_conjecture,
~ c7_2(a73,a58) ).
cnf(u3581,negated_conjecture,
~ c3_2(a100,a60) ).
cnf(u3618,negated_conjecture,
~ sP24(a114) ).
cnf(u3647,negated_conjecture,
~ c1_2(a51,a65) ).
cnf(u3655,negated_conjecture,
~ sP20(a51) ).
cnf(u3667,negated_conjecture,
~ sP20(a128) ).
cnf(u3684,negated_conjecture,
~ c7_2(a73,a80) ).
cnf(u3711,negated_conjecture,
~ sP15(a114) ).
cnf(u3717,negated_conjecture,
~ c5_2(a75,a85) ).
cnf(u3768,axiom,
~ sP24(a108) ).
cnf(u3794,negated_conjecture,
~ c6_2(a66,a60) ).
cnf(u3552,negated_conjecture,
( ~ c3_2(X0,a70)
| ~ c1_1(X0)
| c2_2(X0,a60)
| c3_2(X0,a60)
| ~ sP22(X0) ) ).
cnf(u240,axiom,
( c4_2(X0,a65)
| ~ sP20(X0) ) ).
cnf(u232,axiom,
( c7_2(X0,a60)
| ~ sP22(X0) ) ).
cnf(u3212,negated_conjecture,
( ~ c1_2(X0,a84)
| c3_2(X0,a84)
| ~ c5_1(X0)
| sP14(X0)
| sP15(X0)
| c9_1(X0)
| c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u3761,negated_conjecture,
( ~ c8_2(X0,a111)
| ~ sP20(X0)
| c10_2(X0,a65)
| c8_2(X0,a65)
| ~ c6_2(X0,a111)
| ~ c8_1(X0)
| c8_2(X0,a92) ) ).
cnf(u3627,negated_conjecture,
( ~ c3_2(X0,a70)
| ~ c1_1(X0)
| c2_2(X0,a65)
| c3_2(X0,a65)
| ~ sP20(X0) ) ).
cnf(u3183,negated_conjecture,
( ~ c8_2(X0,a89)
| ~ c6_2(X0,a89)
| ~ c8_1(X0)
| c10_2(X0,a92)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u3626,negated_conjecture,
( c10_2(X0,a65)
| ~ c5_1(X0)
| c9_1(X0)
| c3_2(X0,a65)
| ~ sP20(X0) ) ).
cnf(u3136,negated_conjecture,
( c10_2(X0,a118)
| c9_1(X0)
| c3_2(X0,a118)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u3020,negated_conjecture,
c8_1(a18) ).
cnf(u3018,negated_conjecture,
c1_1(a31) ).
cnf(u3021,negated_conjecture,
c1_1(a44) ).
cnf(u239,axiom,
( c5_2(X0,a65)
| ~ sP20(X0) ) ).
cnf(u259,axiom,
( c10_2(X0,a80)
| ~ sP16(X0) ) ).
cnf(u267,axiom,
( ~ c10_2(X0,a86)
| ~ sP14(X0) ) ).
cnf(u3592,negated_conjecture,
( c10_2(X0,a60)
| c8_2(X0,a52)
| c10_1(X0)
| ~ sP22(X0) ) ).
cnf(u260,axiom,
( ~ sP16(X0)
| ndr1_1(X0) ) ).
cnf(u3234,negated_conjecture,
c1_1(a22) ).
cnf(u3135,negated_conjecture,
( c10_2(X0,a84)
| c9_1(X0)
| c3_2(X0,a84)
| ~ c5_1(X0)
| sP14(X0)
| sP15(X0) ) ).
cnf(u268,axiom,
( ~ sP14(X0)
| ndr1_1(X0) ) ).
cnf(u3595,negated_conjecture,
( ~ c6_2(X0,a60)
| c2_2(X0,a131)
| c2_2(X0,X1)
| c9_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ sP22(X0) ) ).
cnf(u3201,negated_conjecture,
( ~ c8_2(X0,a89)
| ~ c6_2(X0,a89)
| ~ c8_1(X0)
| c9_2(X0,a92)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u241,axiom,
( ~ sP20(X0)
| ndr1_1(X0) ) ).
cnf(u3510,negated_conjecture,
( ~ c5_2(X0,a58)
| c5_2(X0,a89)
| c3_2(X0,a89)
| ~ c3_2(X0,a39)
| ~ sP24(X0)
| c10_2(X0,a58)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u3544,negated_conjecture,
( ~ c7_2(X0,a58)
| c3_1(X0)
| c2_2(X0,X1)
| c10_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ sP24(X0)
| ~ c1_2(X0,a58) ) ).
cnf(u3591,negated_conjecture,
( c10_2(X0,a60)
| c3_2(X0,a52)
| c10_1(X0)
| ~ sP22(X0) ) ).
cnf(u3180,negated_conjecture,
( ~ c1_2(X0,a89)
| c10_1(X0)
| c3_2(X0,a89)
| ~ c7_1(X0)
| c4_1(X0) ) ).
cnf(u225,axiom,
( ~ sP24(X0)
| ndr1_1(X0) ) ).
cnf(u211,axiom,
( c10_2(X0,a50)
| ~ sP27(X0) ) ).
cnf(u3674,negated_conjecture,
( ~ c1_2(X0,a60)
| c10_1(X0)
| ~ sP22(X0)
| c8_2(X0,a52)
| c3_2(X0,a60)
| ~ c7_1(X0) ) ).
cnf(u235,axiom,
( ~ c8_2(X0,a63)
| ~ sP21(X0) ) ).
cnf(u258,axiom,
( ~ c4_2(X0,a80)
| ~ sP16(X0) ) ).
cnf(u214,axiom,
( ~ sP27(X0)
| ndr1_1(X0) ) ).
cnf(u3022,negated_conjecture,
c1_1(a18) ).
cnf(u3658,negated_conjecture,
( c4_2(X0,a111)
| c8_2(X0,a65)
| ~ sP20(X0)
| c10_2(X0,a65) ) ).
cnf(u3288,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,a89)
| c3_2(X0,a89)
| ~ c9_2(X0,a39)
| ~ c5_2(X0,X1)
| c10_2(X0,X1)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u233,axiom,
( ~ sP22(X0)
| ndr1_1(X0) ) ).
cnf(u3509,negated_conjecture,
( ~ c9_2(X0,a39)
| c5_2(X0,a89)
| c3_2(X0,a89)
| ~ sP24(X0)
| ~ c5_2(X0,a58)
| c10_2(X0,a58)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u3297,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,a89)
| c3_2(X0,a89)
| c2_2(X0,a39)
| ~ c5_2(X0,X1)
| c10_2(X0,X1)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u257,axiom,
( c3_2(X0,a80)
| ~ sP16(X0) ) ).
cnf(u3631,negated_conjecture,
( ~ c1_2(X0,a60)
| c10_1(X0)
| ~ sP22(X0)
| c3_2(X0,a52)
| c3_2(X0,a60)
| ~ c7_1(X0) ) ).
cnf(u236,axiom,
( ~ c7_2(X0,a63)
| ~ sP21(X0) ) ).
cnf(u264,axiom,
( ~ sP15(X0)
| ndr1_1(X0) ) ).
cnf(u3596,negated_conjecture,
( ~ c1_2(X0,a131)
| ~ sP22(X0)
| c2_2(X0,X1)
| c9_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c6_2(X0,a60) ) ).
cnf(u3019,negated_conjecture,
c8_1(a44) ).
cnf(u3659,negated_conjecture,
( ~ c3_2(X0,a111)
| c8_2(X0,a65)
| ~ sP20(X0)
| c10_2(X0,a65) ) ).
cnf(u3023,negated_conjecture,
c6_1(a136) ).
cnf(u212,axiom,
( c8_2(X0,a50)
| ~ sP27(X0) ) ).
cnf(u224,axiom,
( c3_2(X0,a58)
| ~ sP24(X0) ) ).
cnf(u3204,negated_conjecture,
( ~ c8_2(X0,a89)
| ~ c6_2(X0,a89)
| ~ c8_1(X0)
| c8_2(X0,a92)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u3508,negated_conjecture,
( ~ c5_2(X0,a58)
| c5_2(X0,a89)
| c3_2(X0,a89)
| c2_2(X0,a39)
| ~ sP24(X0)
| c10_2(X0,a58)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u3729,negated_conjecture,
( ~ c1_2(X0,a65)
| c5_2(X0,a111)
| ~ sP20(X0)
| c8_2(X0,a65)
| c10_1(X0)
| c3_2(X0,a65)
| ~ c7_1(X0) ) ).
cnf(u3763,negated_conjecture,
( ~ c8_2(X0,a111)
| ~ sP20(X0)
| c10_2(X0,a65)
| c8_2(X0,a65)
| ~ c6_2(X0,a111)
| ~ c8_1(X0)
| c10_2(X0,a92) ) ).
cnf(u3781,negated_conjecture,
( ~ c1_2(X0,a65)
| c9_1(X0)
| c3_2(X0,a65)
| ~ sP20(X0)
| ~ c5_1(X0)
| c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u263,axiom,
( c6_2(X0,a85)
| ~ sP15(X0) ) ).
cnf(u3233,negated_conjecture,
( ~ c1_2(X0,a118)
| c3_2(X0,a118)
| ~ c5_1(X0)
| ~ c2_1(X0)
| ~ c4_1(X0)
| c9_1(X0)
| c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u3551,negated_conjecture,
( c10_2(X0,a60)
| ~ c5_1(X0)
| c9_1(X0)
| c3_2(X0,a60)
| ~ sP22(X0) ) ).
cnf(u223,axiom,
( ~ c4_2(X0,a58)
| ~ sP24(X0) ) ).
cnf(u3155,negated_conjecture,
c1_1(a77) ).
cnf(u3548,negated_conjecture,
( c8_2(X0,a58)
| c2_1(X0)
| ~ sP24(X0)
| c7_2(X0,a58) ) ).
cnf(u3777,negated_conjecture,
( ~ c1_2(X0,a60)
| c9_1(X0)
| c3_2(X0,a60)
| ~ sP22(X0)
| ~ c5_1(X0)
| c10_1(X0)
| ~ c7_1(X0) ) ).
cnf(u3657,negated_conjecture,
( c10_2(X0,a65)
| c8_2(X0,a65)
| c5_2(X0,a111)
| ~ sP20(X0) ) ).
cnf(u231,axiom,
( ~ c9_2(X0,a60)
| ~ sP22(X0) ) ).
cnf(u3693,negated_conjecture,
( c8_2(X0,a85)
| c2_1(X0)
| ~ sP15(X0)
| c7_2(X0,a85) ) ).
cnf(u213,axiom,
( c1_2(X0,a50)
| ~ sP27(X0) ) ).
cnf(u230,axiom,
( c5_2(X0,a60)
| ~ sP22(X0) ) ).
cnf(u234,axiom,
( c3_2(X0,a63)
| ~ sP21(X0) ) ).
cnf(u265,axiom,
( ~ c8_2(X0,a86)
| ~ sP14(X0) ) ).
cnf(u3074,negated_conjecture,
( c8_2(X0,a145)
| c2_1(X0)
| c7_2(X0,a145)
| ~ c1_1(X0)
| c9_1(X0) ) ).
cnf(u3219,negated_conjecture,
( ~ c3_2(X0,a70)
| c3_2(X0,a118)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c4_1(X0) ) ).
cnf(u238,axiom,
( ~ c6_2(X0,a65)
| ~ sP20(X0) ) ).
cnf(u261,axiom,
( ~ c9_2(X0,a85)
| ~ sP15(X0) ) ).
cnf(u3762,negated_conjecture,
( ~ c8_2(X0,a111)
| ~ sP20(X0)
| c10_2(X0,a65)
| c8_2(X0,a65)
| ~ c6_2(X0,a111)
| ~ c8_1(X0)
| c9_2(X0,a92) ) ).
cnf(u3546,negated_conjecture,
( ~ c5_2(X0,a58)
| ~ c3_1(X0)
| c6_2(X0,a83)
| ~ sP24(X0) ) ).
cnf(u3216,negated_conjecture,
( ~ c3_2(X0,a70)
| c2_2(X0,a84)
| c3_2(X0,a84)
| ~ c1_1(X0)
| sP14(X0)
| sP15(X0) ) ).
cnf(u266,axiom,
( ~ c2_2(X0,a86)
| ~ sP14(X0) ) ).
cnf(u3545,negated_conjecture,
( c10_2(X0,a58)
| c5_1(X0)
| c7_1(X0)
| ~ sP24(X0) ) ).
cnf(u222,axiom,
( c2_2(X0,a58)
| ~ sP24(X0) ) ).
cnf(u262,axiom,
( c3_2(X0,a85)
| ~ sP15(X0) ) ).
cnf(u3600,negated_conjecture,
( ~ sP21(X0)
| c2_1(X0) ) ).
cnf(u3272,negated_conjecture,
( ~ c2_2(X0,X1)
| c5_2(X0,a89)
| c3_2(X0,a89)
| ~ c3_2(X0,a39)
| ~ c5_2(X0,X1)
| c10_2(X0,X1)
| ~ c6_1(X0)
| c4_1(X0) ) ).
cnf(u237,axiom,
( ~ sP21(X0)
| ndr1_1(X0) ) ).
cnf(u3670,negated_conjecture,
( c8_2(X0,a80)
| c2_1(X0)
| ~ sP16(X0)
| c7_2(X0,a80) ) ).
cnf(u3504,negated_conjecture,
( c3_2(X0,a50)
| c10_1(X0)
| ~ sP27(X0)
| ~ c7_1(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN418+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 15:55:32 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.59/1.15 % (2039574)Detected formulas, will run a generic FOF schedule.
% 3.59/1.15 % (2039582)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3665058696:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.59/1.15 % (2039582)Instruction limit reached!
% 3.59/1.15 % (2039582)------------------------------
% 3.59/1.15 % (2039582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.15 % (2039582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.15 % (2039582)CaDiCaL version: 2.1.3
% 3.59/1.15 % (2039582)Termination reason: Instruction limit
% 3.59/1.15 % (2039582)Termination phase: Saturation
% 3.59/1.15 % (2039582)Time elapsed: 0.037 s
% 3.59/1.15 % (2039582)Peak memory usage: 91 MB
% 3.59/1.15 % (2039582)Instructions burned: 109 (million)
% 3.59/1.15 % (2039583)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2158914434:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.59/1.15 % (2039584)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3154172158:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.59/1.15 % (2039579)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=904303581:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.59/1.15 % (2039580)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=2423443446:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.59/1.15 % (2039581)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=2826934335:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.59/1.15 % (2039585)dis-21_1_sil=8000:lcm=predicate:random_seed=3315065229: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)
% 3.59/1.15 % (2039584)Refutation not found, incomplete strategy
% 3.59/1.15 % (2039584)------------------------------
% 3.59/1.15 % (2039584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.15 % (2039584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.15 % (2039584)CaDiCaL version: 2.1.3
% 3.59/1.15 % (2039584)Termination reason: Refutation not found, incomplete strategy
% 3.59/1.15 % (2039584)Time elapsed: 0.023 s
% 3.59/1.15 % (2039584)Peak memory usage: 90 MB
% 3.59/1.15 % (2039584)Instructions burned: 35 (million)
% 3.59/1.15 % (2039583)Instruction limit reached!
% 3.59/1.15 % (2039583)------------------------------
% 3.59/1.15 % (2039583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.15 % (2039583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.15 % (2039583)CaDiCaL version: 2.1.3
% 3.59/1.15 % (2039583)Termination reason: Instruction limit
% 3.59/1.15 % (2039583)Termination phase: Saturation
% 3.59/1.15 % (2039583)Time elapsed: 0.062 s
% 3.59/1.15 % (2039583)Peak memory usage: 88 MB
% 3.59/1.15 % (2039583)Instructions burned: 120 (million)
% 3.59/1.15 % (2039585)Instruction limit reached!
% 3.59/1.15 % (2039585)------------------------------
% 3.59/1.15 % (2039585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.15 % (2039585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.15 % (2039585)CaDiCaL version: 2.1.3
% 3.59/1.15 % (2039585)Termination reason: Instruction limit
% 3.59/1.15 % (2039585)Termination phase: Saturation
% 3.59/1.15 % (2039585)Time elapsed: 0.072 s
% 3.59/1.15 % (2039585)Peak memory usage: 91 MB
% 3.59/1.15 % (2039585)Instructions burned: 130 (million)
% 3.59/1.15 % (2039593)lrs+10_1_sil=8000:sp=occurrence:random_seed=2090061585:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.59/1.15 % (2039593)First to succeed.
% 3.59/1.15 % (2039593)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2039574"
% 3.59/1.15 % (2039594)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1433044648:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.59/1.15 % (2039595)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2168922797:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 3.59/1.15 % (2039594)Refutation not found, incomplete strategy
% 3.59/1.15 % (2039594)------------------------------
% 3.59/1.15 % (2039594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.15 % (2039594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.15 % (2039594)CaDiCaL version: 2.1.3
% 3.59/1.15 % (2039594)Termination reason: Refutation not found, incomplete strategy
% 3.59/1.15 % (2039594)Time elapsed: 0.020 s
% 3.59/1.15 % (2039594)Peak memory usage: 90 MB
% 3.59/1.15 % (2039594)Instructions burned: 32 (million)
% 3.59/1.15 % (2039595)Refutation not found, incomplete strategy
% 3.59/1.15 % (2039595)------------------------------
% 3.59/1.15 % (2039595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.59/1.15 % (2039595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.59/1.15 % (2039595)CaDiCaL version: 2.1.3
% 3.59/1.15 % (2039595)Termination reason: Refutation not found, incomplete strategy
% 3.59/1.15 % (2039595)Time elapsed: 0.020 s
% 3.59/1.15 % (2039595)Peak memory usage: 90 MB
% 3.59/1.15 % (2039595)Instructions burned: 30 (million)
% 3.59/1.15 % (2039584)------------------------------
% 3.59/1.15 % (2039584)------------------------------
% 3.59/1.15 % SZS status CounterSatisfiable for theBenchmark
% 3.59/1.15 % SZS output start Saturation.
% See solution above
% 3.98/1.35 % SZS output start Definitions and Model Updates.
% 3.98/1.35 % SZS output end Definitions and Model Updates.
% 3.98/1.35 % (2039593)------------------------------
% 3.98/1.35 % (2039593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.98/1.35 % (2039593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/1.35 % (2039593)CaDiCaL version: 2.1.3
% 3.98/1.35 % (2039593)Termination reason: Satisfiable
% 3.98/1.35 % (2039593)Time elapsed: 0.017 s
% 3.98/1.35 % (2039593)Peak memory usage: 90 MB
% 3.98/1.35 % (2039593)Instructions burned: 47 (million)
% 3.98/1.35 % (2039593)------------------------------
% 3.98/1.35 % (2039593)------------------------------
% 3.98/1.35 % (2039574)Success in time 0.477 s
% 3.98/1.35 % Vampire exiting
%------------------------------------------------------------------------------