%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO579+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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:31:42 PM UTC 2026
% Result : CounterSatisfiable 0.20s 0.27s
% Output : Saturation 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u477,axiom,
sP69(sK66) ).
cnf(u483,axiom,
( ~ b48_buttercup10107(X7)
| ~ k04_buttercup10100(X7) ) ).
cnf(u538,axiom,
b48_buttercup10102(sK54) ).
cnf(u548,axiom,
( ~ b48_buttercup10102(X7)
| ~ k04_buttercup10100(X7) ) ).
cnf(u553,axiom,
~ k04_buttercup10100(sK54) ).
cnf(u558,axiom,
~ b48_buttercup10102(sK53) ).
cnf(u563,axiom,
k04_buttercup10100(sK53) ).
cnf(u567,axiom,
~ b48_buttercup10102(sK52) ).
cnf(u573,axiom,
k04_buttercup10100(sK52) ).
cnf(u613,axiom,
( ~ b48_buttercup10110(X7)
| ~ k04_buttercup10100(X7) ) ).
cnf(u652,axiom,
sP44(sK42) ).
cnf(u668,axiom,
b48_buttercup10108(sK32) ).
cnf(u678,axiom,
( ~ b48_buttercup10108(X7)
| ~ k04_buttercup10100(X7) ) ).
cnf(u683,axiom,
~ k04_buttercup10100(sK32) ).
cnf(u688,axiom,
~ b48_buttercup10108(sK31) ).
cnf(u693,axiom,
k04_buttercup10100(sK31) ).
cnf(u697,axiom,
~ b48_buttercup10108(sK30) ).
cnf(u703,axiom,
k04_buttercup10100(sK30) ).
cnf(u732,axiom,
~ b48_buttercup10109(sK22) ).
cnf(u737,axiom,
sP27(sK24) ).
cnf(u743,axiom,
( ~ b48_buttercup10109(X7)
| ~ k04_buttercup10619(X7) ) ).
cnf(u748,axiom,
~ k04_buttercup10619(sK22) ).
cnf(u753,axiom,
~ b48_buttercup10109(sK21) ).
cnf(u758,axiom,
k04_buttercup10619(sK21) ).
cnf(u762,axiom,
~ b48_buttercup10109(sK20) ).
cnf(u768,axiom,
k04_buttercup10619(sK20) ).
cnf(u782,axiom,
sP25(sK23) ).
cnf(u808,axiom,
( ~ b48_buttercup10111(X7)
| ~ k04_buttercup10619(X7) ) ).
cnf(u863,axiom,
b48_buttercup10104(sK2) ).
cnf(u873,axiom,
( ~ b48_buttercup10104(X7)
| ~ k04_buttercup10100(X7) ) ).
cnf(u878,axiom,
~ k04_buttercup10100(sK2) ).
cnf(u883,axiom,
~ b48_buttercup10104(sK1) ).
cnf(u888,axiom,
k04_buttercup10100(sK1) ).
cnf(u892,axiom,
~ b48_buttercup10104(sK0) ).
cnf(u898,axiom,
k04_buttercup10100(sK0) ).
cnf(u996,negated_conjecture,
~ b48_buttercup10102(sK83) ).
cnf(u1000,negated_conjecture,
~ b48_buttercup10104(sK83) ).
cnf(u1004,negated_conjecture,
~ b48_buttercup10107(sK83) ).
cnf(u1008,negated_conjecture,
~ b48_buttercup10108(sK83) ).
cnf(u1012,negated_conjecture,
~ b48_buttercup10109(sK83) ).
cnf(u1016,negated_conjecture,
~ b48_buttercup10110(sK83) ).
cnf(u1021,negated_conjecture,
b48_buttercup10111(sK83) ).
cnf(u1026,axiom,
b48_buttercup10102(sK75) ).
cnf(u1055,axiom,
b48_buttercup10102(sK51) ).
cnf(u1083,axiom,
~ b48_buttercup10102(sK19) ).
cnf(u1087,axiom,
~ b48_buttercup10104(sK19) ).
cnf(u1091,axiom,
~ b48_buttercup10107(sK19) ).
cnf(u1095,axiom,
~ b48_buttercup10108(sK19) ).
cnf(u1099,axiom,
~ b48_buttercup10109(sK19) ).
cnf(u1103,axiom,
~ b48_buttercup10110(sK19) ).
cnf(u1108,axiom,
b48_buttercup10111(sK19) ).
cnf(u1243,axiom,
~ b48_buttercup10102(sK49) ).
cnf(u1247,axiom,
~ b48_buttercup10104(sK49) ).
cnf(u1252,axiom,
b48_buttercup10108(sK49) ).
cnf(u1377,axiom,
~ b48_buttercup10108(sK29) ).
cnf(u1382,axiom,
b48_buttercup10109(sK29) ).
cnf(u1405,axiom,
~ b48_buttercup10109(sK49) ).
cnf(u344,axiom,
( ~ sP59(X4)
| ~ b48_buttercup10102(X4) ) ).
cnf(u240,axiom,
( ~ sP27(X4)
| k04_buttercup10619(X4) ) ).
cnf(u339,axiom,
k04_buttercup10622(sK50) ).
cnf(u984,axiom,
k04_buttercup10619(sK79) ).
cnf(u448,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u928,axiom,
k04_buttercup10619(sK50) ).
cnf(u936,axiom,
( ~ b48_buttercup10102(X0)
| k04_buttercup10619(X0) ) ).
cnf(u1148,axiom,
k04_buttercup10100(sK66) ).
cnf(u951,axiom,
~ k04_buttercup10100(sK73) ).
cnf(u942,axiom,
~ b48_buttercup10102(sK73) ).
cnf(u986,axiom,
k04_buttercup10619(sK77) ).
cnf(u430,axiom,
( ~ b48_buttercup10104(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u442,axiom,
( ~ b48_buttercup10108(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u1124,axiom,
k04_buttercup10619(sK54) ).
cnf(u1467,axiom,
~ b48_buttercup10102(sK29) ).
cnf(u276,axiom,
( ~ sP35(X6)
| b48_buttercup10108(X6) ) ).
cnf(u172,axiom,
( ~ sP8(X3)
| k04_buttercup10100(X3)
| ~ b48_buttercup10104(X3) ) ).
cnf(u348,axiom,
( ~ sP57(X6)
| b48_buttercup10102(X6) ) ).
cnf(u343,axiom,
( ~ sP60(X3)
| k04_buttercup10100(X3)
| ~ b48_buttercup10102(X3) ) ).
cnf(u932,axiom,
k04_buttercup10100(sK76) ).
cnf(u976,axiom,
~ k04_buttercup10100(sK80) ).
cnf(u927,axiom,
k04_buttercup10619(sK49) ).
cnf(u302,axiom,
( ~ sP46(X4)
| ~ b48_buttercup10110(X4) ) ).
cnf(u971,axiom,
~ b48_buttercup10104(sK76) ).
cnf(u930,axiom,
k04_buttercup10619(sK74) ).
cnf(u374,axiom,
~ b48_buttercup10102(sK61) ).
cnf(u242,axiom,
( ~ sP25(X6)
| ~ k04_buttercup10619(X6) ) ).
cnf(u933,axiom,
( ~ b48_buttercup10104(X0)
| k04_buttercup10619(X0) ) ).
cnf(u1213,axiom,
~ b48_buttercup10107(sK74) ).
cnf(u1178,axiom,
~ b48_buttercup10104(sK32) ).
cnf(u1179,axiom,
~ b48_buttercup10102(sK32) ).
cnf(u336,axiom,
k04_buttercup10622(sK49) ).
cnf(u1463,axiom,
~ k04_buttercup10619(sK29) ).
cnf(u331,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u206,axiom,
( ~ sP17(X4)
| ~ b48_buttercup10111(X4) ) ).
cnf(u975,axiom,
~ b48_buttercup10110(sK76) ).
cnf(u176,axiom,
( ~ sP5(X6)
| ~ k04_buttercup10100(X6) ) ).
cnf(u305,axiom,
( ~ sP44(X6)
| ~ k04_buttercup10100(X6) ) ).
cnf(u978,axiom,
~ k04_buttercup10100(sK78) ).
cnf(u422,axiom,
( ~ k04_buttercup10620(X0)
| ~ k04_buttercup10622(X0) ) ).
cnf(u981,axiom,
~ k04_buttercup10619(sK82) ).
cnf(u409,axiom,
k04_buttercup10619(sK72) ).
cnf(u411,axiom,
k04_buttercup10622(sK74) ).
cnf(u1325,axiom,
~ b48_buttercup10102(sK42) ).
cnf(u469,negated_conjecture,
b48_buttercup10098(sK83) ).
cnf(u929,axiom,
k04_buttercup10619(sK61) ).
cnf(u1327,axiom,
~ b48_buttercup10107(sK42) ).
cnf(u205,axiom,
( ~ sP18(X3)
| k04_buttercup10619(X3)
| ~ b48_buttercup10111(X3) ) ).
cnf(u268,axiom,
( ~ b48_buttercup10111(X0)
| k04_buttercup10100(X0) ) ).
cnf(u208,axiom,
( ~ sP16(X5)
| b48_buttercup10111(X5)
| ~ k04_buttercup10619(X5) ) ).
cnf(u335,axiom,
~ b48_buttercup10110(sK49) ).
cnf(u1418,axiom,
k04_buttercup10100(sK23) ).
cnf(u203,axiom,
~ b48_buttercup10109(sK9) ).
cnf(u338,axiom,
~ b48_buttercup10108(sK50) ).
cnf(u423,axiom,
( ~ k04_buttercup10619(X0)
| ~ k04_buttercup10100(X0) ) ).
cnf(u410,axiom,
k04_buttercup10620(sK73) ).
cnf(u415,axiom,
b48_buttercup10102(sK78) ).
cnf(u1330,axiom,
k04_buttercup10619(sK42) ).
cnf(u969,axiom,
~ b48_buttercup10109(sK77) ).
cnf(u177,axiom,
( ~ sP5(X6)
| b48_buttercup10104(X6) ) ).
cnf(u457,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u966,axiom,
~ b48_buttercup10104(sK77) ).
cnf(u418,axiom,
b48_buttercup10108(sK81) ).
cnf(u1122,axiom,
k04_buttercup10619(sK51) ).
cnf(u416,axiom,
b48_buttercup10104(sK79) ).
cnf(u444,axiom,
( ~ b48_buttercup10108(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u379,axiom,
( ~ sP69(X4)
| ~ b48_buttercup10107(X4) ) ).
cnf(u956,axiom,
~ b48_buttercup10104(sK80) ).
cnf(u1176,axiom,
k04_buttercup10619(sK32) ).
cnf(u207,axiom,
( ~ sP17(X4)
| k04_buttercup10619(X4) ) ).
cnf(u270,axiom,
k04_buttercup10100(sK29) ).
cnf(u342,axiom,
b48_buttercup10098(sK51) ).
cnf(u210,axiom,
( ~ sP15(X6)
| b48_buttercup10111(X6) ) ).
cnf(u238,axiom,
( ~ sP28(X3)
| k04_buttercup10619(X3)
| ~ b48_buttercup10109(X3) ) ).
cnf(u1300,axiom,
~ k04_buttercup10100(sK42) ).
cnf(u458,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10109(X0) ) ).
cnf(u1212,axiom,
~ b48_buttercup10107(sK61) ).
cnf(u1317,axiom,
k04_buttercup10100(sK19) ).
cnf(u461,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u963,axiom,
~ b48_buttercup10107(sK82) ).
cnf(u383,axiom,
( ~ sP67(X6)
| b48_buttercup10107(X6) ) ).
cnf(u464,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10109(X0) ) ).
cnf(u944,axiom,
~ b48_buttercup10110(sK73) ).
cnf(u1120,axiom,
k04_buttercup10619(sK81) ).
cnf(u1259,axiom,
~ k04_buttercup10100(sK21) ).
cnf(u958,axiom,
~ b48_buttercup10102(sK81) ).
cnf(u945,axiom,
~ b48_buttercup10104(sK73) ).
cnf(u273,axiom,
( ~ sP37(X4)
| k04_buttercup10100(X4) ) ).
cnf(u333,axiom,
k04_buttercup10622(sK48) ).
cnf(u449,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u304,axiom,
( ~ sP45(X5)
| b48_buttercup10110(X5)
| ~ k04_buttercup10100(X5) ) ).
cnf(u1177,axiom,
~ b48_buttercup10107(sK32) ).
cnf(u954,axiom,
~ b48_buttercup10102(sK80) ).
cnf(u408,axiom,
k04_buttercup10100(sK71) ).
cnf(u468,negated_conjecture,
k04_buttercup10100(sK83) ).
cnf(u948,axiom,
~ k04_buttercup10100(sK50) ).
cnf(u463,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u943,axiom,
~ b48_buttercup10108(sK73) ).
cnf(u987,axiom,
~ k04_buttercup10100(sK77) ).
cnf(u934,axiom,
( ~ b48_buttercup10110(X0)
| k04_buttercup10619(X0) ) ).
cnf(u946,axiom,
~ k04_buttercup10100(sK48) ).
cnf(u949,axiom,
~ k04_buttercup10100(sK61) ).
cnf(u202,axiom,
( ~ b48_buttercup10109(X0)
| k04_buttercup10100(X0) ) ).
cnf(u437,axiom,
( ~ b48_buttercup10107(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u173,axiom,
( ~ sP7(X4)
| ~ b48_buttercup10104(X4) ) ).
cnf(u164,axiom,
( ~ k04_buttercup10622(X0)
| k04_buttercup10619(X0) ) ).
cnf(u340,axiom,
( b48_buttercup10098(X0)
| ~ k04_buttercup10100(X0) ) ).
cnf(u275,axiom,
( ~ sP35(X6)
| ~ k04_buttercup10100(X6) ) ).
cnf(u303,axiom,
( ~ sP46(X4)
| k04_buttercup10100(X4) ) ).
cnf(u236,axiom,
~ k04_buttercup10619(sK19) ).
cnf(u412,axiom,
b48_buttercup10098(sK75) ).
cnf(u347,axiom,
( ~ sP57(X6)
| ~ k04_buttercup10100(X6) ) ).
cnf(u456,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u968,axiom,
~ b48_buttercup10108(sK77) ).
cnf(u243,axiom,
( ~ sP25(X6)
| b48_buttercup10109(X6) ) ).
cnf(u931,axiom,
k04_buttercup10100(sK82) ).
cnf(u306,axiom,
( ~ sP44(X6)
| b48_buttercup10110(X6) ) ).
cnf(u378,axiom,
( ~ sP70(X3)
| k04_buttercup10100(X3)
| ~ b48_buttercup10107(X3) ) ).
cnf(u373,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u925,axiom,
k04_buttercup10619(sK73) ).
cnf(u937,axiom,
( ~ b48_buttercup10107(X0)
| k04_buttercup10619(X0) ) ).
cnf(u381,axiom,
( ~ sP68(X5)
| b48_buttercup10107(X5)
| ~ k04_buttercup10100(X5) ) ).
cnf(u1110,axiom,
( b48_buttercup10110(X0)
| b48_buttercup10109(X0)
| b48_buttercup10108(X0)
| b48_buttercup10107(X0)
| b48_buttercup10104(X0)
| b48_buttercup10102(X0)
| ~ k04_buttercup10619(X0) ) ).
cnf(u341,axiom,
~ k04_buttercup10100(sK51) ).
cnf(u1269,axiom,
~ b48_buttercup10109(sK24) ).
cnf(u1294,axiom,
( b48_buttercup10111(X0)
| b48_buttercup10110(X0)
| b48_buttercup10109(X0)
| b48_buttercup10108(X0)
| b48_buttercup10104(X0)
| ~ k04_buttercup10100(X0) ) ).
cnf(u239,axiom,
( ~ sP27(X4)
| ~ b48_buttercup10109(X4) ) ).
cnf(u175,axiom,
( ~ sP6(X5)
| b48_buttercup10104(X5)
| ~ k04_buttercup10100(X5) ) ).
cnf(u455,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u935,axiom,
( ~ b48_buttercup10108(X0)
| k04_buttercup10619(X0) ) ).
cnf(u967,axiom,
~ b48_buttercup10107(sK77) ).
cnf(u982,axiom,
~ k04_buttercup10619(sK76) ).
cnf(u926,axiom,
k04_buttercup10619(sK48) ).
cnf(u970,axiom,
~ b48_buttercup10102(sK76) ).
cnf(u414,axiom,
b48_buttercup10110(sK77) ).
cnf(u1138,axiom,
k04_buttercup10619(sK2) ).
cnf(u413,axiom,
b48_buttercup10111(sK76) ).
cnf(u973,axiom,
~ b48_buttercup10108(sK76) ).
cnf(u985,axiom,
~ k04_buttercup10100(sK79) ).
cnf(u451,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u272,axiom,
( ~ sP37(X4)
| ~ b48_buttercup10108(X4) ) ).
cnf(u1268,axiom,
k04_buttercup10619(sK24) ).
cnf(u332,axiom,
~ b48_buttercup10104(sK48) ).
cnf(u163,axiom,
( ~ k04_buttercup10620(X0)
| k04_buttercup10619(X0) ) ).
cnf(u960,axiom,
~ b48_buttercup10107(sK81) ).
cnf(u235,axiom,
( b48_buttercup10098(X0)
| ~ k04_buttercup10619(X0) ) ).
cnf(u1149,axiom,
~ b48_buttercup10107(sK66) ).
cnf(u460,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u972,axiom,
~ b48_buttercup10107(sK76) ).
cnf(u301,axiom,
( ~ sP47(X3)
| k04_buttercup10100(X3)
| ~ b48_buttercup10110(X3) ) ).
cnf(u974,axiom,
~ b48_buttercup10109(sK76) ).
cnf(u1159,axiom,
~ k04_buttercup10100(sK81) ).
cnf(u345,axiom,
( ~ sP59(X4)
| k04_buttercup10100(X4) ) ).
cnf(u1126,axiom,
k04_buttercup10619(sK78) ).
cnf(u961,axiom,
~ b48_buttercup10102(sK82) ).
cnf(u417,axiom,
b48_buttercup10107(sK80) ).
cnf(u241,axiom,
( ~ sP26(X5)
| b48_buttercup10109(X5)
| ~ k04_buttercup10619(X5) ) ).
cnf(u1162,axiom,
k04_buttercup10619(sK80) ).
cnf(u1466,axiom,
~ b48_buttercup10104(sK29) ).
cnf(u1326,axiom,
~ b48_buttercup10104(sK42) ).
cnf(u377,axiom,
( ~ k04_buttercup10620(X0)
| b48_buttercup10107(X0) ) ).
cnf(u376,axiom,
( k04_buttercup10620(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u436,axiom,
( ~ b48_buttercup10107(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u271,axiom,
( ~ sP38(X3)
| k04_buttercup10100(X3)
| ~ b48_buttercup10108(X3) ) ).
cnf(u204,axiom,
k04_buttercup10100(sK9) ).
cnf(u443,axiom,
( ~ b48_buttercup10108(X0)
| ~ b48_buttercup10104(X0) ) ).
cnf(u1209,axiom,
~ b48_buttercup10107(sK48) ).
cnf(u964,axiom,
~ b48_buttercup10108(sK82) ).
cnf(u1416,axiom,
~ b48_buttercup10104(sK23) ).
cnf(u1125,axiom,
k04_buttercup10619(sK75) ).
cnf(u274,axiom,
( ~ sP36(X5)
| b48_buttercup10108(X5)
| ~ k04_buttercup10100(X5) ) ).
cnf(u334,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10110(X0) ) ).
cnf(u346,axiom,
( ~ sP58(X5)
| b48_buttercup10102(X5)
| ~ k04_buttercup10100(X5) ) ).
cnf(u962,axiom,
~ b48_buttercup10104(sK82) ).
cnf(u450,axiom,
( ~ b48_buttercup10109(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u1299,axiom,
b48_buttercup10110(sK42) ).
cnf(u465,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10110(X0) ) ).
cnf(u462,axiom,
( ~ b48_buttercup10111(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u380,axiom,
( ~ sP69(X4)
| k04_buttercup10100(X4) ) ).
cnf(u375,axiom,
k04_buttercup10622(sK61) ).
cnf(u1271,axiom,
~ k04_buttercup10100(sK24) ).
cnf(u419,axiom,
b48_buttercup10109(sK82) ).
cnf(u959,axiom,
~ b48_buttercup10104(sK81) ).
cnf(u941,axiom,
( ~ k04_buttercup10622(X0)
| ~ b48_buttercup10107(X0) ) ).
cnf(u1413,axiom,
~ k04_buttercup10619(sK23) ).
cnf(u950,axiom,
~ k04_buttercup10100(sK72) ).
cnf(u1415,axiom,
~ b48_buttercup10107(sK23) ).
cnf(u174,axiom,
( ~ sP7(X4)
| k04_buttercup10100(X4) ) ).
cnf(u337,axiom,
( k04_buttercup10622(X0)
| ~ b48_buttercup10108(X0) ) ).
cnf(u1308,negated_conjecture,
~ k04_buttercup10619(sK83) ).
cnf(u454,axiom,
( ~ b48_buttercup10110(X0)
| ~ b48_buttercup10102(X0) ) ).
cnf(u1210,axiom,
~ b48_buttercup10107(sK49) ).
cnf(u1329,axiom,
~ b48_buttercup10109(sK42) ).
cnf(u1412,axiom,
b48_buttercup10109(sK23) ).
cnf(u1139,axiom,
~ b48_buttercup10102(sK2) ).
cnf(u1211,axiom,
~ b48_buttercup10107(sK50) ).
cnf(u965,axiom,
~ b48_buttercup10102(sK77) ).
cnf(u1465,axiom,
~ b48_buttercup10107(sK29) ).
cnf(u940,axiom,
~ k04_buttercup10622(sK73) ).
cnf(u952,axiom,
~ k04_buttercup10100(sK74) ).
cnf(u1414,axiom,
~ b48_buttercup10108(sK23) ).
cnf(u467,axiom,
( ~ b48_buttercup10098(X0)
| b48_buttercup10111(X0)
| b48_buttercup10110(X0)
| b48_buttercup10109(X0)
| b48_buttercup10108(X0)
| b48_buttercup10107(X0)
| b48_buttercup10104(X0)
| b48_buttercup10102(X0) ) ).
cnf(u947,axiom,
~ k04_buttercup10100(sK49) ).
cnf(u1328,axiom,
~ b48_buttercup10108(sK42) ).
cnf(u938,axiom,
b48_buttercup10107(sK73) ).
cnf(u382,axiom,
( ~ sP67(X6)
| ~ k04_buttercup10100(X6) ) ).
cnf(u953,axiom,
~ b48_buttercup10102(sK79) ).
cnf(u269,axiom,
~ b48_buttercup10111(sK29) ).
cnf(u1417,axiom,
~ b48_buttercup10102(sK23) ).
cnf(u1265,axiom,
~ k04_buttercup10100(sK20) ).
cnf(u209,axiom,
( ~ sP15(X6)
| ~ k04_buttercup10619(X6) ) ).
cnf(u237,axiom,
b48_buttercup10098(sK19) ).
cnf(u1226,axiom,
~ k04_buttercup10100(sK75) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO579+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n026.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 17:51:42 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/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.20/0.27 % (4096009)Will run a generic schedule for satisfiability detection.
% 0.20/0.27 % (4096018)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2272466843:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.27 % (4096015)% WARNING: option uhcvi not known.
% 0.20/0.27 % (4096015)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2206872688:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.27 % (4096017)dis+10_1_sil=32000:sp=arity:random_seed=162566400:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.27 % (4096014)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1332919739_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.27 % (4096016)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2685041843:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.27 % (4096019)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=420748053:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.27 % (4096020)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2649490177:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.27 % (4096018) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4096009-4096018"...
% 0.20/0.27 % (4096018)...printing done.
% 0.20/0.27 % Detected minimum model sizes of [1]
% 0.20/0.27 % Detected maximum model sizes of [56]
% 0.20/0.27 % SZS status CounterSatisfiable for theBenchmark
% 0.20/0.27 % SZS output start Saturation.
% See solution above
% 0.20/0.27 % SZS output start Definitions and Model Updates.
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~k04_buttercup10619(X0) | k04_buttercup10622(X0) | k04_buttercup10620(X0) is false, set k04_buttercup10622(X0) to true
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~b48_buttercup10111(X0) | b48_buttercup10098(X0) is false, set b48_buttercup10098(X0) to true
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~b48_buttercup10110(X0) | b48_buttercup10098(X0) is false, set b48_buttercup10098(X0) to true
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~b48_buttercup10109(X0) | b48_buttercup10098(X0) is false, set b48_buttercup10098(X0) to true
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~b48_buttercup10108(X0) | b48_buttercup10098(X0) is false, set b48_buttercup10098(X0) to true
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~b48_buttercup10107(X0) | b48_buttercup10098(X0) is false, set b48_buttercup10098(X0) to true
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~b48_buttercup10104(X0) | b48_buttercup10098(X0) is false, set b48_buttercup10098(X0) to true
% 0.20/0.27 for all groundings,
% 0.20/0.27 whenever ~b48_buttercup10102(X0) | b48_buttercup10098(X0) is false, set b48_buttercup10098(X0) to true
% 0.20/0.27 % SZS output end Definitions and Model Updates.
% 0.20/0.27 % (4096018)------------------------------
% 0.20/0.27 % (4096018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.27 % (4096018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.27 % (4096018)CaDiCaL version: 2.1.3
% 0.20/0.27 % (4096018)Termination reason: Satisfiable
% 0.20/0.27 % (4096018)Time elapsed: 0.011 s
% 0.20/0.27 % (4096018)Peak memory usage: 12 MB
% 0.20/0.27 % (4096018)Instructions burned: 35 (million)
% 0.20/0.27 % (4096009)Success in time 0.04 s
% 0.20/0.27 % Vampire exiting
%------------------------------------------------------------------------------