%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n019.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:34 PM UTC 2026
% Result : CounterSatisfiable 2.88s 1.13s
% Output : Saturation 3.78s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u757,negated_conjecture,
~ c2_0 ).
cnf(u760,negated_conjecture,
c10_0 ).
cnf(u842,negated_conjecture,
ndr1_0 ).
cnf(u773,negated_conjecture,
~ c7_0 ).
cnf(u788,negated_conjecture,
c4_0 ).
cnf(u796,negated_conjecture,
~ c9_0 ).
cnf(u2085,negated_conjecture,
~ sP1 ).
cnf(u2058,negated_conjecture,
~ sP0 ).
cnf(u829,negated_conjecture,
~ ndr1_1(a601) ).
cnf(u836,negated_conjecture,
~ c10_1(a601) ).
cnf(u840,negated_conjecture,
c5_1(a601) ).
cnf(u2098,negated_conjecture,
~ sP2 ).
cnf(u2125,negated_conjecture,
~ sP3 ).
cnf(u873,negated_conjecture,
c1_0 ).
cnf(u2156,negated_conjecture,
~ sP4 ).
cnf(u2169,negated_conjecture,
~ sP5 ).
cnf(u883,negated_conjecture,
( ~ c9_1(X93)
| c7_2(X93,a591)
| ~ c1_1(X93) ) ).
cnf(u887,negated_conjecture,
( ~ c9_1(X93)
| ~ c1_2(X93,a591)
| ~ c1_1(X93) ) ).
cnf(u891,negated_conjecture,
( ~ c9_1(X93)
| ndr1_1(X93)
| ~ c1_1(X93) ) ).
cnf(u2179,negated_conjecture,
~ sP6 ).
cnf(u898,negated_conjecture,
( c10_1(X91)
| ~ ndr1_1(X91)
| ~ c3_2(X91,X92)
| ~ c1_2(X91,X92)
| ~ c7_2(X91,a589) ) ).
cnf(u930,negated_conjecture,
~ c3_0 ).
cnf(u905,negated_conjecture,
( c10_1(X91)
| ~ ndr1_1(X91)
| ~ c3_2(X91,X92)
| ~ c1_2(X91,X92)
| ~ c10_2(X91,a589) ) ).
cnf(u909,negated_conjecture,
( c10_1(X91)
| ~ ndr1_1(X91)
| ~ c3_2(X91,X92)
| ~ c1_2(X91,X92)
| ~ c2_2(X91,a589) ) ).
cnf(u1088,negated_conjecture,
~ c5_0 ).
cnf(u2196,negated_conjecture,
~ sP7 ).
cnf(u973,negated_conjecture,
~ c8_0 ).
cnf(u923,negated_conjecture,
c9_1(a585) ).
cnf(u927,negated_conjecture,
~ c5_1(a585) ).
cnf(u1033,negated_conjecture,
~ c6_1(a577) ).
cnf(u2231,negated_conjecture,
~ sP8 ).
cnf(u1041,negated_conjecture,
~ c8_1(a577) ).
cnf(u1045,negated_conjecture,
~ c1_1(a577) ).
cnf(u1051,negated_conjecture,
( ~ c8_1(X84)
| c7_2(X84,a574)
| ~ c6_1(X84) ) ).
cnf(u1056,negated_conjecture,
( ~ c8_1(X84)
| c4_2(X84,a574)
| ~ c6_1(X84) ) ).
cnf(u1060,negated_conjecture,
( ~ c8_1(X84)
| c6_2(X84,a574)
| ~ c6_1(X84) ) ).
cnf(u1064,negated_conjecture,
( ~ c8_1(X84)
| ndr1_1(X84)
| ~ c6_1(X84) ) ).
cnf(u1090,negated_conjecture,
c6_0 ).
cnf(u2257,negated_conjecture,
~ sP10 ).
cnf(u1118,negated_conjecture,
( sP9(X80)
| ~ c10_2(X80,a568)
| ~ ndr1_1(X80)
| ~ c7_2(X80,X81)
| ~ c1_2(X80,X81)
| ~ c5_2(X80,X81) ) ).
cnf(u1122,negated_conjecture,
( sP9(X80)
| c9_2(X80,a568)
| ~ ndr1_1(X80)
| ~ c7_2(X80,X81)
| ~ c1_2(X80,X81)
| ~ c5_2(X80,X81) ) ).
cnf(u1127,negated_conjecture,
sP12 ).
cnf(u1171,negated_conjecture,
( c7_1(X74)
| c5_1(X74)
| c9_1(X74) ) ).
cnf(u1192,negated_conjecture,
( ~ c2_1(X71)
| ~ ndr1_1(X71)
| ~ c4_2(X71,X72)
| ~ c6_2(X71,X72)
| ~ c3_2(X71,X72)
| c7_1(X71) ) ).
cnf(u2296,negated_conjecture,
~ sP13 ).
cnf(u1250,negated_conjecture,
( ~ c6_1(X64)
| c1_2(X64,X66)
| c4_2(X64,X66)
| ~ c3_2(X64,X66)
| ~ c6_2(X64,X65)
| ~ ndr1_1(X64)
| c2_2(X64,X65)
| c5_2(X64,X65) ) ).
cnf(u1323,negated_conjecture,
c9_1(a550) ).
cnf(u1327,negated_conjecture,
~ ndr1_1(a550) ).
cnf(u2313,negated_conjecture,
~ sP14 ).
cnf(u1355,negated_conjecture,
c5_1(a547) ).
cnf(u2330,negated_conjecture,
~ sP15 ).
cnf(u1362,negated_conjecture,
c6_1(a547) ).
cnf(u1368,negated_conjecture,
( c2_1(X54)
| c7_1(X54)
| ~ c10_2(X54,a545) ) ).
cnf(u2347,negated_conjecture,
~ sP16 ).
cnf(u1375,negated_conjecture,
( c2_1(X54)
| c7_1(X54)
| ~ c4_2(X54,a545) ) ).
cnf(u1379,negated_conjecture,
( c2_1(X54)
| c7_1(X54)
| ndr1_1(X54) ) ).
cnf(u1383,negated_conjecture,
( sP17(X52)
| ~ ndr1_1(X52)
| ~ c2_2(X52,X53)
| c6_2(X52,X53)
| ~ c7_2(X52,X53)
| ~ c6_2(X52,a542) ) ).
cnf(u1387,negated_conjecture,
( sP17(X52)
| ~ ndr1_1(X52)
| ~ c2_2(X52,X53)
| c6_2(X52,X53)
| ~ c7_2(X52,X53)
| c5_2(X52,a542) ) ).
cnf(u1391,negated_conjecture,
( sP17(X52)
| ~ ndr1_1(X52)
| ~ c2_2(X52,X53)
| c6_2(X52,X53)
| ~ c7_2(X52,X53)
| c1_2(X52,a542) ) ).
cnf(u2364,negated_conjecture,
~ sP18 ).
cnf(u2400,negated_conjecture,
~ sP19 ).
cnf(u1414,negated_conjecture,
( c2_1(X51)
| c6_1(X51)
| ~ c3_2(X51,a536) ) ).
cnf(u1418,negated_conjecture,
( c2_1(X51)
| c6_1(X51)
| c9_2(X51,a536) ) ).
cnf(u1422,negated_conjecture,
( c2_1(X51)
| c6_1(X51)
| ~ c4_2(X51,a536) ) ).
cnf(u1426,negated_conjecture,
( c2_1(X51)
| c6_1(X51)
| ndr1_1(X51) ) ).
cnf(u2414,negated_conjecture,
~ sP21 ).
cnf(u2449,negated_conjecture,
~ sP23 ).
cnf(u1482,negated_conjecture,
( ~ c4_1(X46)
| c6_2(X46,a526)
| ~ c1_1(X46) ) ).
cnf(u1486,negated_conjecture,
( ~ c4_1(X46)
| ~ c2_2(X46,a526)
| ~ c1_1(X46) ) ).
cnf(u1490,negated_conjecture,
( ~ c4_1(X46)
| ~ c9_2(X46,a526)
| ~ c1_1(X46) ) ).
cnf(u1494,negated_conjecture,
( ~ c4_1(X46)
| ndr1_1(X46)
| ~ c1_1(X46) ) ).
cnf(u2466,negated_conjecture,
~ sP24 ).
cnf(u1518,negated_conjecture,
c7_1(a521) ).
cnf(u1522,negated_conjecture,
~ c9_2(a521,a522) ).
cnf(u1526,negated_conjecture,
c6_2(a521,a522) ).
cnf(u1530,negated_conjecture,
c1_2(a521,a522) ).
cnf(u1534,negated_conjecture,
ndr1_1(a521) ).
cnf(u1538,negated_conjecture,
~ c10_1(a521) ).
cnf(u2492,negated_conjecture,
~ sP25 ).
cnf(u1546,negated_conjecture,
~ c1_2(a517,a518) ).
cnf(u1550,negated_conjecture,
c9_2(a517,a518) ).
cnf(u1554,negated_conjecture,
c8_2(a517,a518) ).
cnf(u1558,negated_conjecture,
ndr1_1(a517) ).
cnf(u1562,negated_conjecture,
c9_1(a517) ).
cnf(u1567,negated_conjecture,
( c4_2(a517,X42)
| ~ c10_2(a517,X42) ) ).
cnf(u1572,negated_conjecture,
( c7_1(X39)
| ~ c2_2(X39,X41)
| c4_2(X39,X41)
| c3_2(X39,X41)
| ~ ndr1_1(X39)
| c2_2(X39,X40)
| c10_2(X39,X40)
| ~ c4_2(X39,X40) ) ).
cnf(u2518,negated_conjecture,
~ sP27 ).
cnf(u2535,negated_conjecture,
~ sP29 ).
cnf(u2561,negated_conjecture,
~ sP30 ).
cnf(u1630,negated_conjecture,
( c9_2(X33,a506)
| c1_1(X33)
| ~ ndr1_1(X33)
| ~ c5_2(X33,X34)
| c2_2(X33,X34)
| c7_2(X33,X34) ) ).
cnf(u1634,negated_conjecture,
( ~ c5_2(X33,X34)
| c1_1(X33)
| ~ ndr1_1(X33)
| ~ c3_2(X33,a506)
| c2_2(X33,X34)
| c7_2(X33,X34) ) ).
cnf(u1638,negated_conjecture,
( ~ c5_2(X33,X34)
| c1_1(X33)
| ~ ndr1_1(X33)
| c10_2(X33,a506)
| c2_2(X33,X34)
| c7_2(X33,X34) ) ).
cnf(u1646,negated_conjecture,
( c3_1(X31)
| c10_1(X31)
| ~ c6_1(X31) ) ).
cnf(u1674,negated_conjecture,
( ~ c9_2(X28,X29)
| c1_1(X28)
| c9_1(X28)
| ~ ndr1_1(X28)
| c10_2(X28,X29)
| ~ c7_2(X28,X29) ) ).
cnf(u2574,negated_conjecture,
~ sP31 ).
cnf(u2609,negated_conjecture,
~ sP33 ).
cnf(u2622,negated_conjecture,
~ sP34 ).
cnf(u1719,negated_conjecture,
~ ndr1_1(a493) ).
cnf(u1726,negated_conjecture,
c9_1(a493) ).
cnf(u1731,negated_conjecture,
( c3_1(X21)
| c1_1(X21)
| ~ ndr1_1(X21)
| c1_2(X21,X22)
| c10_2(X21,X22)
| c6_2(X21,X22) ) ).
cnf(u2648,negated_conjecture,
~ sP35 ).
cnf(u1811,negated_conjecture,
sP37 ).
cnf(u2710,negated_conjecture,
~ sP38 ).
cnf(u2745,negated_conjecture,
~ sP39 ).
cnf(u2763,negated_conjecture,
~ sP40 ).
cnf(u2789,negated_conjecture,
~ sP41 ).
cnf(u2806,negated_conjecture,
~ sP42 ).
cnf(u1923,negated_conjecture,
sP43 ).
cnf(u1967,negated_conjecture,
( c10_1(X2)
| c8_2(X2,a459)
| ~ ndr1_1(X2)
| c7_2(X2,X3)
| c2_2(X2,X3)
| c10_2(X2,X3) ) ).
cnf(u1971,negated_conjecture,
( c10_1(X2)
| c2_2(X2,a459)
| ~ ndr1_1(X2)
| c7_2(X2,X3)
| c2_2(X2,X3)
| c10_2(X2,X3) ) ).
cnf(u1975,negated_conjecture,
( c10_1(X2)
| ~ c9_2(X2,a459)
| ~ ndr1_1(X2)
| c7_2(X2,X3)
| c2_2(X2,X3)
| c10_2(X2,X3) ) ).
cnf(u2854,negated_conjecture,
~ sP44 ).
cnf(u2871,negated_conjecture,
~ sP47 ).
cnf(u2282,axiom,
~ ndr1_1(a566) ).
cnf(u2289,axiom,
~ c3_1(a566) ).
cnf(u2677,axiom,
~ c7_2(a481,a483) ).
cnf(u2681,axiom,
c10_2(a481,a483) ).
cnf(u2685,axiom,
c5_2(a481,a483) ).
cnf(u2689,axiom,
ndr1_1(a481) ).
cnf(u2693,axiom,
c6_2(a481,a482) ).
cnf(u2697,axiom,
c10_2(a481,a482) ).
cnf(u2701,axiom,
c4_2(a481,a482) ).
cnf(u2707,axiom,
( ~ c5_2(a481,X0)
| ~ c7_2(a481,X0)
| ~ c3_2(a481,X0) ) ).
cnf(u2840,axiom,
~ c7_1(a463) ).
cnf(u2844,axiom,
~ c9_1(a463) ).
cnf(u2848,axiom,
~ ndr1_1(a463) ).
cnf(u2894,negated_conjecture,
~ c1_1(a585) ).
cnf(u3090,negated_conjecture,
~ ndr1_1(a585) ).
cnf(u2901,negated_conjecture,
~ c1_1(a550) ).
cnf(u2906,negated_conjecture,
~ c1_1(a493) ).
cnf(u2915,negated_conjecture,
~ c1_1(a517) ).
cnf(u2932,negated_conjecture,
~ c7_2(a521,a589) ).
cnf(u2935,negated_conjecture,
( ~ c3_2(a521,X0)
| ~ c1_2(a521,X0) ) ).
cnf(u2974,negated_conjecture,
c10_2(a521,a589) ).
cnf(u2948,negated_conjecture,
~ c2_2(a521,a589) ).
cnf(u2967,negated_conjecture,
( c7_2(a521,X0)
| c10_2(a521,X0)
| c2_2(a521,X0) ) ).
cnf(u2984,negated_conjecture,
~ c6_1(a566) ).
cnf(u2995,negated_conjecture,
c5_1(a463) ).
cnf(u3023,negated_conjecture,
~ ndr1_1(a547) ).
cnf(u3038,negated_conjecture,
c2_2(a481,a483) ).
cnf(u3064,negated_conjecture,
~ c3_2(a481,a542) ).
cnf(u3109,negated_conjecture,
~ ndr1_1(a577) ).
cnf(u3125,negated_conjecture,
~ c3_2(a517,a506) ).
cnf(u3128,negated_conjecture,
c4_2(a517,a543) ).
cnf(u3131,negated_conjecture,
( ~ c7_2(a517,X0)
| ~ c2_2(a517,X0)
| c6_2(a517,X0) ) ).
cnf(u3177,negated_conjecture,
( c9_2(X0,a568)
| ~ c3_2(X0,a567)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u345,axiom,
( ~ sP9(X0)
| ndr1_1(X0) ) ).
cnf(u2955,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| c6_1(X0)
| ~ c4_2(X0,a536) ) ).
cnf(u276,axiom,
( ~ sP22(X0)
| c6_2(X0,a530) ) ).
cnf(u3054,negated_conjecture,
( c5_2(X0,a542)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c4_2(X0,a543) ) ).
cnf(u343,axiom,
( ~ sP9(X0)
| c6_2(X0,a567) ) ).
cnf(u3206,negated_conjecture,
( c9_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c1_1(X0)
| ~ c2_2(X0,a567)
| c10_2(X0,a568)
| ~ c7_2(X0,a568) ) ).
cnf(u142,axiom,
( ~ sP45(X0)
| c9_2(X0,a452) ) ).
cnf(u201,axiom,
( ~ sP36(X0)
| ~ c1_2(X0,a486) ) ).
cnf(u2959,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c10_2(X0,a545) ) ).
cnf(u292,axiom,
( ~ sP20(X0)
| ~ c4_2(X0,a532) ) ).
cnf(u3210,negated_conjecture,
( c4_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c7_2(X0,a542)
| ~ c1_2(X0,a542)
| ~ c2_2(X0,a567)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c10_2(X0,a568) ) ).
cnf(u290,axiom,
( ~ sP20(X0)
| ~ c1_2(X0,a532) ) ).
cnf(u293,axiom,
( ~ sP20(X0)
| ndr1_1(X0) ) ).
cnf(u3158,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c1_2(X0,a543)
| ~ ndr1_1(X0)
| c10_2(X0,a506)
| c2_2(X0,a542)
| c7_2(X0,a542) ) ).
cnf(u3184,negated_conjecture,
( c4_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c7_2(X0,a542)
| ~ c1_2(X0,a542)
| ~ c3_2(X0,a567)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c10_2(X0,a568) ) ).
cnf(u246,axiom,
( ~ sP28(X0)
| c3_2(X0,a508) ) ).
cnf(u145,axiom,
( ~ sP45(X0)
| ndr1_1(X0) ) ).
cnf(u335,axiom,
( ~ sP11(X0)
| ndr1_1(X0) ) ).
cnf(u309,axiom,
( ~ sP17(X0)
| c1_2(X0,a543) ) ).
cnf(u249,axiom,
( ~ sP28(X0)
| ndr1_1(X0) ) ).
cnf(u256,axiom,
( ~ sP26(X0)
| c7_2(X0,a512) ) ).
cnf(u140,axiom,
( ~ sP46(X0)
| ~ c1_2(X0,a453) ) ).
cnf(u3150,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| c1_2(X0,a543)
| c1_2(X0,a542) ) ).
cnf(u3151,negated_conjecture,
( c5_2(X0,a542)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c1_2(X0,a543) ) ).
cnf(u3055,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| c4_2(X0,a543)
| ~ c6_2(X0,a542) ) ).
cnf(u311,axiom,
( ~ sP17(X0)
| ndr1_1(X0) ) ).
cnf(u2953,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| c6_1(X0)
| ~ c3_2(X0,a536) ) ).
cnf(u3185,negated_conjecture,
( c1_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c7_2(X0,a542)
| ~ c1_2(X0,a542)
| ~ c3_2(X0,a567)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c10_2(X0,a568) ) ).
cnf(u333,axiom,
( ~ sP11(X0)
| ~ c3_2(X0,a565) ) ).
cnf(u3190,negated_conjecture,
( c9_2(X0,a568)
| c6_2(X0,a567)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u3152,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| c1_2(X0,a543)
| ~ c6_2(X0,a542) ) ).
cnf(u255,axiom,
( ~ sP26(X0)
| c1_2(X0,a512) ) ).
cnf(u139,axiom,
( ~ sP46(X0)
| c4_2(X0,a453) ) ).
cnf(u199,axiom,
( ~ sP36(X0)
| ~ c9_2(X0,a486) ) ).
cnf(u3060,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c4_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c3_2(X0,a506)
| c2_2(X0,a542)
| c7_2(X0,a542) ) ).
cnf(u202,axiom,
( ~ sP36(X0)
| ndr1_1(X0) ) ).
cnf(u3061,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c4_2(X0,a543)
| ~ ndr1_1(X0)
| c10_2(X0,a506)
| c2_2(X0,a542)
| c7_2(X0,a542) ) ).
cnf(u257,axiom,
( ~ sP26(X0)
| ndr1_1(X0) ) ).
cnf(u3211,negated_conjecture,
( c1_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c7_2(X0,a542)
| ~ c1_2(X0,a542)
| ~ c2_2(X0,a567)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c10_2(X0,a568) ) ).
cnf(u3174,negated_conjecture,
( ~ c5_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c1_2(X0,a542) ) ).
cnf(u221,axiom,
( ~ sP32(X0)
| c9_2(X0,a497) ) ).
cnf(u3175,negated_conjecture,
( ~ c5_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c5_2(X0,a542) ) ).
cnf(u2954,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| c6_1(X0)
| c9_2(X0,a536) ) ).
cnf(u279,axiom,
( ~ sP22(X0)
| ndr1_1(X0) ) ).
cnf(u224,axiom,
( ~ sP32(X0)
| ndr1_1(X0) ) ).
cnf(u3204,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c2_2(X0,a567) ) ).
cnf(u247,axiom,
( ~ sP28(X0)
| c2_2(X0,a508) ) ).
cnf(u3193,negated_conjecture,
( c9_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c1_1(X0)
| c6_2(X0,a567)
| c10_2(X0,a568)
| ~ c7_2(X0,a568) ) ).
cnf(u310,axiom,
( ~ sP17(X0)
| ~ c5_2(X0,a543) ) ).
cnf(u344,axiom,
( ~ sP9(X0)
| ~ c2_2(X0,a567) ) ).
cnf(u3198,negated_conjecture,
( c1_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c7_2(X0,a542)
| ~ c1_2(X0,a542)
| c6_2(X0,a567)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c10_2(X0,a568) ) ).
cnf(u342,axiom,
( ~ sP9(X0)
| ~ c3_2(X0,a567) ) ).
cnf(u332,axiom,
( ~ sP11(X0)
| ~ c5_2(X0,a565) ) ).
cnf(u200,axiom,
( ~ sP36(X0)
| ~ c2_2(X0,a486) ) ).
cnf(u223,axiom,
( ~ sP32(X0)
| ~ c4_2(X0,a497) ) ).
cnf(u254,axiom,
( ~ sP26(X0)
| c2_2(X0,a512) ) ).
cnf(u141,axiom,
( ~ sP46(X0)
| ndr1_1(X0) ) ).
cnf(u144,axiom,
( ~ sP45(X0)
| ~ c2_2(X0,a452) ) ).
cnf(u3203,negated_conjecture,
( c9_2(X0,a568)
| ~ c2_2(X0,a567)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1) ) ).
cnf(u334,axiom,
( ~ sP11(X0)
| c4_2(X0,a565) ) ).
cnf(u277,axiom,
( ~ sP22(X0)
| ~ c1_2(X0,a530) ) ).
cnf(u3176,negated_conjecture,
( ~ c5_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c6_2(X0,a542) ) ).
cnf(u3180,negated_conjecture,
( c9_1(X0)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c5_2(X0,X1)
| c1_1(X0)
| ~ c3_2(X0,a567)
| c10_2(X0,a568)
| ~ c7_2(X0,a568) ) ).
cnf(u308,axiom,
( ~ sP17(X0)
| c4_2(X0,a543) ) ).
cnf(u2958,negated_conjecture,
( c7_1(X0)
| ~ c4_2(X0,X1)
| ~ c6_2(X0,X1)
| ~ c3_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c4_2(X0,a545) ) ).
cnf(u3053,negated_conjecture,
( ~ c7_2(X0,X1)
| ~ ndr1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| c4_2(X0,a543)
| c1_2(X0,a542) ) ).
cnf(u143,axiom,
( ~ sP45(X0)
| c1_2(X0,a452) ) ).
cnf(u3197,negated_conjecture,
( c4_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c7_2(X0,a542)
| ~ c1_2(X0,a542)
| c6_2(X0,a567)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| ~ c10_2(X0,a568) ) ).
cnf(u248,axiom,
( ~ sP28(X0)
| c7_2(X0,a508) ) ).
cnf(u278,axiom,
( ~ sP22(X0)
| c9_2(X0,a530) ) ).
cnf(u3191,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| c6_2(X0,a567) ) ).
cnf(u291,axiom,
( ~ sP20(X0)
| c9_2(X0,a532) ) ).
cnf(u222,axiom,
( ~ sP32(X0)
| c2_2(X0,a497) ) ).
cnf(u3157,negated_conjecture,
( c1_1(X0)
| ~ c2_2(X0,X1)
| c6_2(X0,X1)
| ~ c7_2(X0,X1)
| c1_2(X0,a543)
| ~ ndr1_1(X0)
| ~ c3_2(X0,a506)
| c2_2(X0,a542)
| c7_2(X0,a542) ) ).
cnf(u3178,negated_conjecture,
( ~ c5_2(X0,X1)
| ~ c10_2(X0,a568)
| ~ ndr1_1(X0)
| ~ c7_2(X0,X1)
| ~ c1_2(X0,X1)
| ~ c3_2(X0,a567) ) ).
%------------------------------------------------------------------------------
%----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 THM
% 0.09/0.20 % Computer : n019.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 15:55:48 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 2.88/1.13 % (4119348)Detected formulas, will run a generic FOF schedule.
% 2.88/1.13 % (4119462)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1419769453:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.88/1.13 % (4119462)Instruction limit reached!
% 2.88/1.13 % (4119462)------------------------------
% 2.88/1.13 % (4119462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.88/1.13 % (4119462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/1.13 % (4119462)CaDiCaL version: 2.1.3
% 2.88/1.13 % (4119462)Termination reason: Instruction limit
% 2.88/1.13 % (4119462)Termination phase: Saturation
% 2.88/1.13 % (4119462)Time elapsed: 0.035 s
% 2.88/1.13 % (4119462)Peak memory usage: 89 MB
% 2.88/1.13 % (4119462)Instructions burned: 122 (million)
% 2.88/1.13 % (4119463)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3836023113:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.88/1.13 % (4119459)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=3836304830:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.88/1.13 % (4119461)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2054362883:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.88/1.13 % (4119458)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=1963389717:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.88/1.13 % (4119460)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=1575252619:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.88/1.13 % (4119464)dis-21_1_sil=8000:lcm=predicate:random_seed=2362696224: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)
% 2.88/1.13 % (4119463)Refutation not found, incomplete strategy
% 2.88/1.13 % (4119463)------------------------------
% 2.88/1.13 % (4119463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.88/1.13 % (4119463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/1.13 % (4119463)CaDiCaL version: 2.1.3
% 2.88/1.13 % (4119463)Termination reason: Refutation not found, incomplete strategy
% 2.88/1.13 % (4119463)Time elapsed: 0.018 s
% 2.88/1.13 % (4119463)Peak memory usage: 90 MB
% 2.88/1.13 % (4119463)Instructions burned: 27 (million)
% 2.88/1.13 % (4119464)First to succeed.
% 2.88/1.13 % (4119464)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4119348"
% 2.88/1.13 % (4119461)Instruction limit reached!
% 2.88/1.13 % (4119461)------------------------------
% 2.88/1.13 % (4119461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.88/1.13 % (4119461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/1.13 % (4119461)CaDiCaL version: 2.1.3
% 2.88/1.13 % (4119461)Termination reason: Instruction limit
% 2.88/1.13 % (4119461)Termination phase: Saturation
% 2.88/1.13 % (4119461)Time elapsed: 0.061 s
% 2.88/1.13 % (4119461)Peak memory usage: 90 MB
% 2.88/1.13 % (4119461)Instructions burned: 109 (million)
% 2.88/1.13 % (4119486)lrs+10_1_sil=8000:sp=occurrence:random_seed=3666449425:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.88/1.13 % (4119486)Also succeeded, but the first one will report.
% 2.88/1.13 % (4119520)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1705335572:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.88/1.13 % (4119520)Refutation not found, incomplete strategy
% 2.88/1.13 % (4119520)------------------------------
% 2.88/1.13 % (4119520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.88/1.13 % (4119520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.88/1.13 % (4119520)CaDiCaL version: 2.1.3
% 2.88/1.13 % (4119520)Termination reason: Refutation not found, incomplete strategy
% 2.88/1.13 % (4119520)Time elapsed: 0.019 s
% 2.88/1.13 % (4119520)Peak memory usage: 90 MB
% 2.88/1.13 % (4119520)Instructions burned: 28 (million)
% 2.88/1.13 % (4119463)------------------------------
% 2.88/1.13 % (4119463)------------------------------
% 2.88/1.13 % SZS status CounterSatisfiable for theBenchmark
% 2.88/1.13 % SZS output start Saturation.
% See solution above
% 3.78/1.33 % SZS output start Definitions and Model Updates.
% 3.78/1.33 % SZS output end Definitions and Model Updates.
% 3.78/1.33 % (4119464)------------------------------
% 3.78/1.33 % (4119464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.78/1.33 % (4119464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.78/1.33 % (4119464)CaDiCaL version: 2.1.3
% 3.78/1.33 % (4119464)Termination reason: Satisfiable
% 3.78/1.33 % (4119464)Time elapsed: 0.022 s
% 3.78/1.33 % (4119464)Peak memory usage: 90 MB
% 3.78/1.33 % (4119464)Instructions burned: 34 (million)
% 3.78/1.33 % (4119464)------------------------------
% 3.78/1.33 % (4119464)------------------------------
% 3.78/1.33 % (4119348)Success in time 0.438 s
% 3.78/1.33 % Vampire exiting
%------------------------------------------------------------------------------