%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN720-1 : TPTP v9.3.1. Released v2.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:17:58 PM UTC 2026
% Result : Satisfiable 0.20s 0.28s
% Output : Saturation 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u376,axiom,
k1(b) ).
cnf(u381,axiom,
m2(b) ).
cnf(u421,axiom,
s1(X0) ).
cnf(u430,axiom,
l3(X0,X0) ).
cnf(u436,axiom,
n5(X0,X0) ).
cnf(u442,axiom,
l1(X0,X0) ).
cnf(u454,axiom,
~ l0(b) ).
cnf(u464,axiom,
m1(X0,X0,X0) ).
cnf(u475,axiom,
n1(X0,X0,X0) ).
cnf(u485,axiom,
p1(X0,X0,X0) ).
cnf(u499,axiom,
n2(X0) ).
cnf(u531,axiom,
n3(X0) ).
cnf(u543,axiom,
p2(X0,X0,X0) ).
cnf(u562,axiom,
r3(X0,X0,X0) ).
cnf(u570,axiom,
l4(X0) ).
cnf(u584,axiom,
k3(X0,X0,X0) ).
cnf(u636,axiom,
p1(X0,X0,X1) ).
cnf(u650,axiom,
q1(X0,X1,X1) ).
cnf(u660,axiom,
( ~ s0(X0)
| m2(X0) ) ).
cnf(u685,axiom,
k3(X0,X0,X1) ).
cnf(u698,axiom,
k2(X0,X0) ).
cnf(u739,axiom,
k2(c,b) ).
cnf(u744,axiom,
p3(b,c,b) ).
cnf(u752,axiom,
l5(X0) ).
cnf(u755,axiom,
( l5(X0)
| ~ k1(X0) ) ).
cnf(u759,axiom,
m1(X0,X1,X0) ).
cnf(u774,axiom,
n1(X0,X0,X1) ).
cnf(u789,axiom,
n1(X0,c,X0) ).
cnf(u805,axiom,
~ m0(b,c,e) ).
cnf(u814,axiom,
q1(X0,b,b) ).
cnf(u838,axiom,
p1(d,b,e) ).
cnf(u843,axiom,
p2(d,b,b) ).
cnf(u867,axiom,
s2(X0) ).
cnf(u881,axiom,
k3(X0,X1,X0) ).
cnf(u942,axiom,
p2(X0,X1,X0) ).
cnf(u972,axiom,
r3(X0,X1,X0) ).
cnf(u985,axiom,
k5(X0) ).
cnf(u988,axiom,
( k5(X0)
| ~ r3(X2,X0,X0) ) ).
cnf(u1041,axiom,
s1(a) ).
cnf(u1046,axiom,
s2(d) ).
cnf(u1056,axiom,
( ~ q0(X0,X1)
| s1(X0) ) ).
cnf(u1091,axiom,
q1(X0,X0,X1) ).
cnf(u1106,axiom,
l3(X0,X1) ).
cnf(u1116,axiom,
m4(X0,X1) ).
cnf(u1129,axiom,
n4(X0,X0) ).
cnf(u1140,axiom,
p3(X0,X0,X0) ).
cnf(u1177,axiom,
s4(X0) ).
cnf(u1184,axiom,
p5(X0,X1,X0) ).
cnf(u1196,axiom,
( l1(X0,X0)
| ~ k1(X0) ) ).
cnf(u1219,axiom,
m1(X0,X1,X1) ).
cnf(u1222,axiom,
( ~ m0(X1,X1,X0)
| m1(X0,X1,X1) ) ).
cnf(u1227,axiom,
n1(X0,e,e) ).
cnf(u1262,axiom,
m1(X0,X0,e) ).
cnf(u1276,axiom,
n1(X0,X1,X0) ).
cnf(u1284,axiom,
~ p0(a,b) ).
cnf(u1287,axiom,
n1(a,X0,b) ).
cnf(u1294,axiom,
p1(X0,b,X1) ).
cnf(u1333,axiom,
q1(X0,X1,X0) ).
cnf(u1344,axiom,
~ s0(e) ).
cnf(u1353,axiom,
p2(e,X0,X1) ).
cnf(u1385,axiom,
p2(X0,X1,X1) ).
cnf(u1403,axiom,
q3(X0,X1) ).
cnf(u1427,axiom,
m3(X0,c,X0) ).
cnf(u1453,axiom,
n4(X0,X1) ).
cnf(u1467,axiom,
p4(X0,X0,X1) ).
cnf(u1471,axiom,
l1(b,c) ).
cnf(u1476,axiom,
~ k3(c,e,b) ).
cnf(u1487,axiom,
s5(X0) ).
cnf(u1491,axiom,
r4(X0) ).
cnf(u1498,axiom,
r3(d,b,c) ).
cnf(u1503,axiom,
n5(b,e) ).
cnf(u1508,axiom,
n5(d,X0) ).
cnf(u1519,axiom,
p4(X0,X1,X0) ).
cnf(u1555,axiom,
r1(X0) ).
cnf(u1568,axiom,
q1(d,X1,d) ).
cnf(u1608,axiom,
r2(X0) ).
cnf(u1615,axiom,
m3(X0,X1,X0) ).
cnf(u1632,axiom,
p2(X0,X0,d) ).
cnf(u1645,axiom,
p3(X0,X1,X2) ).
cnf(u1666,axiom,
p2(a,X0,d) ).
cnf(u1689,axiom,
l1(X0,X1) ).
cnf(u1692,axiom,
( l1(X0,X1)
| ~ m0(X1,X0,X2)
| ~ p0(X2,X0) ) ).
cnf(u1740,axiom,
p1(X0,X1,X0) ).
cnf(u1743,axiom,
( p1(X0,X1,X0)
| ~ p1(X1,X3,X0) ) ).
cnf(u1749,axiom,
p1(X0,X1,X2) ).
cnf(u1768,axiom,
( q1(X0,X1,X1)
| ~ l0(X0) ) ).
cnf(u1774,axiom,
k2(X0,X1) ).
cnf(u1831,axiom,
p5(X0,X0,X1) ).
cnf(u1837,axiom,
q2(X0,c,X1) ).
cnf(u1878,axiom,
l2(X0,X1) ).
cnf(u1891,axiom,
p2(X0,e,X1) ).
cnf(u1954,axiom,
n1(X0,d,b) ).
cnf(u1989,axiom,
m3(X0,X1,X1) ).
cnf(u1993,axiom,
p4(X0,X1,X1) ).
cnf(u2020,axiom,
m1(X0,X0,c) ).
cnf(u2030,axiom,
n1(X0,X1,X1) ).
cnf(u2038,axiom,
~ q0(e,c) ).
cnf(u2055,axiom,
r3(X0,X1,X2) ).
cnf(u2069,axiom,
s3(X0,X1) ).
cnf(u2102,axiom,
~ r0(c) ).
cnf(u2105,axiom,
m1(X0,X1,c) ).
cnf(u2119,axiom,
m1(X0,a,X1) ).
cnf(u2175,axiom,
q4(X0,X1) ).
cnf(u2216,axiom,
q2(X0,X1,X0) ).
cnf(u2265,axiom,
n5(X0,X1) ).
cnf(rule_059,axiom,
( ~ m0(X2,X3,X3)
| n1(X0,X0,X1)
| ~ m0(X1,X2,X0) ) ).
cnf(u1505,axiom,
( ~ k3(d,X0,a)
| n5(d,X0) ) ).
cnf(u952,axiom,
( p2(X0,X1,X0)
| ~ r0(X1)
| ~ l0(X0) ) ).
cnf(u1134,axiom,
m3(X0,X0,X0) ).
cnf(u1005,axiom,
( ~ q2(b,X0,b)
| s2(X0) ) ).
cnf(u1827,axiom,
( q2(X0,c,X1)
| ~ k1(X1)
| ~ l2(X1,X0) ) ).
cnf(u695,axiom,
k2(e,e) ).
cnf(u444,axiom,
l1(b,b) ).
cnf(u1107,axiom,
( r3(X0,X1,X1)
| ~ l2(c,X0) ) ).
cnf(rule_036,axiom,
( ~ m0(b,X1,X0)
| n1(X0,X0,X1) ) ).
cnf(u1081,axiom,
( m1(X0,X0,e)
| ~ k0(X0) ) ).
cnf(u720,axiom,
q1(c,c,c) ).
cnf(u1399,axiom,
( ~ q2(X0,c,c)
| m3(X0,c,X0) ) ).
cnf(u449,axiom,
l1(a,a) ).
cnf(u716,axiom,
k2(b,b) ).
cnf(u2017,axiom,
( ~ p0(X1,X0)
| ~ n0(X1,X1)
| m1(X0,X0,c) ) ).
cnf(u1071,axiom,
( p2(X1,X0,X1)
| ~ r0(X0) ) ).
cnf(u1328,axiom,
r3(d,b,d) ).
cnf(rule_244,axiom,
( p3(X0,X0,X0)
| ~ n2(X0) ) ).
cnf(u1984,axiom,
p3(X0,X1,X1) ).
cnf(rule_011,axiom,
( ~ n0(X1,X1)
| ~ k0(X0)
| m1(X0,X0,X1) ) ).
cnf(rule_240,axiom,
( ~ p2(X1,X2,X0)
| n3(X0) ) ).
cnf(u395,axiom,
k1(a) ).
cnf(rule_005,axiom,
( ~ m0(X1,X1,X0)
| m1(X0,X1,X0) ) ).
cnf(rule_194,axiom,
( k3(X0,X0,X1)
| ~ k2(X1,X0) ) ).
cnf(rule_035,axiom,
( m1(X0,X1,X0)
| ~ r0(X0)
| ~ l0(X1) ) ).
cnf(u1642,axiom,
( ~ k3(X1,X2,X0)
| p3(X0,X1,X2) ) ).
cnf(rule_007,axiom,
( ~ p0(X2,X1)
| m1(X0,X1,X0)
| ~ r0(X0) ) ).
cnf(axiom_32,axiom,
k0(b) ).
cnf(u391,axiom,
k1(c) ).
cnf(u2096,axiom,
k4(e) ).
cnf(rule_032,axiom,
( m1(X0,X0,X0)
| ~ s0(X0) ) ).
cnf(rule_001,axiom,
( ~ n0(X1,X0)
| k1(X0) ) ).
cnf(axiom_26,axiom,
n0(d,c) ).
cnf(axiom_28,axiom,
k0(e) ).
cnf(axiom_19,axiom,
m0(X0,d,X1) ).
cnf(axiom_21,axiom,
q0(b,e) ).
cnf(axiom_8,axiom,
m0(e,d,e) ).
cnf(axiom_15,axiom,
n0(a,b) ).
cnf(axiom_2,axiom,
q0(e,d) ).
cnf(axiom_1,axiom,
s0(d) ).
cnf(rule_287,axiom,
( ~ k3(X0,X0,X1)
| p4(X0,X1,X0) ) ).
cnf(u1398,axiom,
m3(X0,e,e) ).
cnf(u1579,axiom,
q1(X0,e,X0) ).
cnf(u1422,axiom,
q2(X0,X0,X0) ).
cnf(u1008,axiom,
( q1(X0,X0,X0)
| ~ k1(X0) ) ).
cnf(u1612,axiom,
( m3(X0,X1,X0)
| ~ k2(c,X1) ) ).
cnf(u460,axiom,
m1(e,e,e) ).
cnf(u763,axiom,
m1(X0,d,X0) ).
cnf(u1593,axiom,
( ~ q0(X0,X1)
| r1(X0) ) ).
cnf(rule_170,axiom,
( ~ n1(X0,e,e)
| p2(X0,e,X0) ) ).
cnf(rule_057,axiom,
( n1(X0,X0,X0)
| ~ r0(X0) ) ).
cnf(rule_166,axiom,
( ~ m1(a,X0,d)
| ~ n0(X0,d)
| p2(a,X0,d) ) ).
cnf(u780,axiom,
n1(X0,X0,d) ).
cnf(rule_129,axiom,
( ~ q1(X1,X0,X0)
| k2(X0,X0) ) ).
cnf(axiom_4,axiom,
m0(e,d,a) ).
cnf(rule_159,axiom,
( p2(X0,X0,X0)
| ~ k1(X0) ) ).
cnf(rule_116,axiom,
( q1(X0,X0,X0)
| ~ r0(X0) ) ).
cnf(rule_085,axiom,
( ~ p0(X1,X0)
| p1(X0,X0,X0) ) ).
cnf(u1875,axiom,
( ~ l2(X1,X1)
| ~ n0(e,X1)
| l2(X0,X1) ) ).
cnf(u2048,axiom,
( ~ r3(X2,X0,X0)
| r3(X0,X1,X2) ) ).
cnf(u1972,axiom,
m2(d) ).
cnf(rule_068,axiom,
( p1(X0,X0,X0)
| ~ k0(X0) ) ).
cnf(u2137,axiom,
( ~ q2(X3,X1,X0)
| q4(X0,X1) ) ).
cnf(rule_067,axiom,
( ~ q0(X1,X0)
| p1(X0,X0,X0) ) ).
cnf(rule_105,axiom,
( q1(X0,X0,X1)
| ~ s0(X0)
| ~ p0(X1,d) ) ).
cnf(rule_092,axiom,
( ~ p0(X3,X0)
| ~ n0(X2,X1)
| q1(X0,X1,X0) ) ).
cnf(u581,axiom,
n2(b) ).
cnf(u1825,axiom,
( p5(X0,X0,X1)
| ~ l2(X0,X0) ) ).
cnf(rule_141,axiom,
( ~ q1(X0,a,X0)
| p2(X0,a,X0) ) ).
cnf(rule_063,axiom,
( p1(X0,X0,X1)
| ~ n0(d,X0)
| ~ k0(X1) ) ).
cnf(u734,axiom,
q1(a,a,a) ).
cnf(u2114,axiom,
p5(X0,X1,X1) ).
cnf(rule_044,axiom,
( ~ p0(X1,X2)
| ~ p0(X0,X0)
| n1(X0,X1,X0) ) ).
cnf(u1716,axiom,
( ~ p0(X1,X1)
| n1(X0,d,X1)
| ~ r0(X0) ) ).
cnf(u2116,axiom,
( m1(X0,a,X1)
| ~ q0(X0,X1) ) ).
cnf(rule_002,axiom,
( ~ n0(X1,X0)
| l1(X0,X0) ) ).
cnf(u389,axiom,
k1(e) ).
cnf(u1350,axiom,
( ~ p1(X0,X1,e)
| p2(e,X0,X1) ) ).
cnf(u2066,axiom,
( ~ q2(X2,X0,X2)
| s3(X0,X1)
| ~ m0(X2,X3,X1) ) ).
cnf(axiom_34,axiom,
n0(c,d) ).
cnf(u1270,axiom,
m1(X0,d,d) ).
cnf(u1580,axiom,
q1(X0,b,X0) ).
cnf(rule_039,axiom,
( ~ m0(X1,X0,c)
| n1(X0,c,X0) ) ).
cnf(u1272,axiom,
m1(e,b,b) ).
cnf(u1069,axiom,
( m1(X0,X1,X0)
| ~ r0(X0) ) ).
cnf(u1581,axiom,
q1(X0,c,X0) ).
cnf(u724,axiom,
q1(e,e,e) ).
cnf(u715,axiom,
q1(b,b,b) ).
cnf(u1103,axiom,
( l3(X0,X1)
| ~ r0(X0) ) ).
cnf(u472,axiom,
n1(c,c,c) ).
cnf(u1016,axiom,
n2(c) ).
cnf(axiom_36,axiom,
q0(a,b) ).
cnf(u947,axiom,
p2(b,e,b) ).
cnf(axiom_30,axiom,
n0(e,e) ).
cnf(u1335,axiom,
( ~ n0(X0,X1)
| q1(X2,X1,X2) ) ).
cnf(rule_040,axiom,
( ~ m0(X0,X1,e)
| n1(X0,e,e)
| ~ k1(X0) ) ).
cnf(u443,axiom,
l1(e,e) ).
cnf(u1629,axiom,
( ~ m0(X1,X0,d)
| p2(X0,X0,d) ) ).
cnf(axiom_33,axiom,
q0(d,c) ).
cnf(u608,axiom,
n2(d) ).
cnf(axiom_27,axiom,
m0(e,b,c) ).
cnf(axiom_29,axiom,
q0(d,b) ).
cnf(rule_299,axiom,
( ~ p3(X1,X2,X3)
| s4(X0)
| ~ l1(X0,X2) ) ).
cnf(axiom_16,axiom,
m0(c,b,a) ).
cnf(axiom_23,axiom,
m0(a,e,e) ).
cnf(u2213,axiom,
( ~ q2(X1,X2,X0)
| ~ n1(X1,X0,X2)
| q2(X0,X1,X0) ) ).
cnf(u1484,axiom,
( ~ p0(X3,X0)
| r4(X0) ) ).
cnf(axiom_10,axiom,
p0(b,d) ).
cnf(rule_279,axiom,
( ~ s3(a,X0)
| ~ l2(X2,X1)
| m4(X0,X1) ) ).
cnf(axiom_9,axiom,
r0(b) ).
cnf(rule_137,axiom,
( ~ p1(X1,X2,X0)
| n2(X0) ) ).
cnf(axiom_12,axiom,
m0(a,X0,a) ).
cnf(axiom_3,axiom,
n0(d,e) ).
cnf(u1450,axiom,
( ~ p3(X0,X1,X1)
| n4(X0,X1) ) ).
cnf(u1246,axiom,
( ~ m1(b,X0,e)
| n1(e,e,X0) ) ).
cnf(axiom_6,axiom,
q0(b,b) ).
cnf(axiom_5,axiom,
s0(b) ).
cnf(rule_082,axiom,
( ~ p1(X2,X0,X3)
| ~ m0(X2,X0,X3)
| p1(X0,X1,X2) ) ).
cnf(u765,axiom,
m1(e,b,e) ).
cnf(u1535,axiom,
( ~ q0(X0,X0)
| ~ k1(X1)
| m1(X0,X1,X1) ) ).
cnf(u1611,axiom,
m3(X0,X0,X1) ).
cnf(u778,axiom,
n1(e,e,b) ).
cnf(u1724,axiom,
( ~ m0(X1,X2,X0)
| n1(X0,X0,X1) ) ).
cnf(u1334,axiom,
( ~ n0(X0,X1)
| q1(d,X1,d) ) ).
cnf(u604,axiom,
p1(d,d,d) ).
cnf(u1990,axiom,
( ~ r3(X1,X1,X0)
| p4(X0,X1,X1) ) ).
cnf(u1605,axiom,
( ~ l0(X0)
| r2(X0) ) ).
cnf(rule_186,axiom,
( q2(X0,X0,X1)
| ~ l1(X1,X0) ) ).
cnf(u396,axiom,
k1(d) ).
cnf(u1449,axiom,
k4(c) ).
cnf(rule_314,axiom,
( n5(X0,X0)
| ~ r4(X0) ) ).
cnf(u580,axiom,
n2(e) ).
cnf(u504,axiom,
( ~ k0(X0)
| n2(X0) ) ).
cnf(u1379,axiom,
r3(e,X0,e) ).
cnf(rule_100,axiom,
( ~ n0(X1,X0)
| q1(X0,X0,X0) ) ).
cnf(rule_069,axiom,
( p1(X0,X0,X1)
| ~ p0(X1,X0) ) ).
cnf(u461,axiom,
m1(c,c,c) ).
cnf(u2204,axiom,
p2(b,c,a) ).
cnf(rule_093,axiom,
( ~ q0(X1,X0)
| q1(X0,X0,X0) ) ).
cnf(u512,axiom,
n2(a) ).
cnf(rule_095,axiom,
( q1(X0,X1,X1)
| ~ p0(X1,X0) ) ).
cnf(rule_021,axiom,
( m1(X0,X1,X0)
| ~ l0(X0)
| ~ k0(X1) ) ).
cnf(rule_210,axiom,
( k3(X0,X0,X0)
| ~ n2(X0) ) ).
cnf(axiom_37,axiom,
n0(b,a) ).
cnf(rule_206,axiom,
( ~ p2(X1,X0,X0)
| k3(X0,X1,X0) ) ).
cnf(u1720,axiom,
( n1(X0,d,b)
| ~ r0(X0) ) ).
cnf(u718,axiom,
q1(d,d,d) ).
cnf(axiom_35,axiom,
m0(d,e,c) ).
cnf(axiom_38,axiom,
m0(b,a,a) ).
cnf(u953,axiom,
( p2(X0,X1,X0)
| ~ l0(X1)
| ~ k0(X0) ) ).
cnf(u1986,axiom,
( m3(X0,X1,X1)
| ~ m2(X1) ) ).
cnf(rule_277,axiom,
( ~ p3(X1,X2,X0)
| l4(X0) ) ).
cnf(axiom_24,axiom,
l0(c) ).
cnf(axiom_31,axiom,
m0(b,b,e) ).
cnf(axiom_18,axiom,
p0(c,b) ).
cnf(u1652,axiom,
p3(X0,X0,X1) ).
cnf(axiom_17,axiom,
q0(X0,d) ).
cnf(u1464,axiom,
( p4(X0,X0,X1)
| ~ r0(X0) ) ).
cnf(u2046,axiom,
m3(c,b,d) ).
cnf(u1391,axiom,
( q2(X0,X1,X1)
| ~ k0(X1) ) ).
cnf(rule_255,axiom,
( ~ q2(X2,X0,X1)
| q3(X0,X1)
| ~ n0(X2,X0) ) ).
cnf(u2210,axiom,
p2(a,c,b) ).
cnf(u951,axiom,
p2(d,X0,d) ).
cnf(rule_267,axiom,
( ~ p2(X0,X2,X1)
| r3(X0,X1,X0) ) ).
cnf(u2262,axiom,
( ~ n5(X4,X1)
| n5(X0,X1) ) ).
cnf(u450,axiom,
l1(d,d) ).
cnf(rule_218,axiom,
( l3(X0,X0)
| ~ r2(X0) ) ).
cnf(u640,axiom,
( ~ p0(X0,X1)
| n2(X0) ) ).
cnf(u511,axiom,
p1(a,a,a) ).
cnf(axiom_11,axiom,
n0(e,b) ).
cnf(rule_176,axiom,
( ~ m1(X1,X0,X1)
| p2(X0,X1,X0) ) ).
cnf(u1586,axiom,
q1(X0,d,X0) ).
cnf(axiom_20,axiom,
l0(a) ).
cnf(u1585,axiom,
q1(X0,a,X0) ).
cnf(u599,axiom,
p1(c,c,c) ).
cnf(axiom_14,axiom,
p0(b,X0) ).
cnf(axiom_13,axiom,
r0(e) ).
cnf(rule_156,axiom,
( ~ q1(a,X1,X0)
| ~ n1(e,X0,a)
| p2(X0,e,X1) ) ).
cnf(rule_125,axiom,
( ~ p0(X0,X0)
| s1(X0) ) ).
cnf(axiom_7,axiom,
n0(d,b) ).
cnf(rule_127,axiom,
( ~ m1(X2,X1,X0)
| k2(X0,X1)
| ~ k1(X3)
| ~ k2(X3,X1) ) ).
cnf(rule_083,axiom,
( ~ m1(X0,X1,b)
| p1(X0,b,X1)
| ~ k0(X1) ) ).
cnf(u445,axiom,
l1(c,c) ).
cnf(u598,axiom,
p1(b,b,b) ).
cnf(u597,axiom,
p1(e,e,e) ).
cnf(rule_097,axiom,
( q1(X0,X0,X0)
| ~ s0(X0) ) ).
cnf(u2149,axiom,
( ~ q2(X3,d,X0)
| p3(X0,X1,X2) ) ).
cnf(u425,axiom,
s1(b) ).
cnf(rule_066,axiom,
( ~ n0(X1,X0)
| p1(X0,X0,X0) ) ).
cnf(u811,axiom,
( q1(X0,b,b)
| ~ s0(X0) ) ).
cnf(rule_264,axiom,
( r3(X0,X0,X0)
| ~ s2(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN720-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20 % Computer : n026.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Mon Sep 28 16:51:42 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.28 % (4012644)Will run a generic schedule for satisfiability detection.
% 0.20/0.28 % (4012651)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1407429412:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.28 % (4012650)% WARNING: option uhcvi not known.
% 0.20/0.28 % (4012649)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1126703442_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.28 % (4012650)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3164723417:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.28 % (4012654)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2836574223:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.28 % (4012652)dis+10_1_sil=32000:sp=arity:random_seed=2853831301:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.28 % (4012653)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2095619970:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.28 % (4012655)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4079906111:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.28 % (4012651) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4012644-4012651"...
% 0.20/0.28 % (4012651)...printing done.
% 0.20/0.28 % SZS status Satisfiable for theBenchmark
% 0.20/0.28 % SZS output start Saturation.
% See solution above
% 0.20/0.29 % SZS output start Definitions and Model Updates.
% 0.20/0.29 for all inputs,
% 0.20/0.29 define m5(X0,X1) := $true
% 0.20/0.29 for all inputs,
% 0.20/0.29 define q5(X0,X1) := $true
% 0.20/0.29 for all inputs,
% 0.20/0.29 define r5(X0,X1) := $true
% 0.20/0.29 % SZS output end Definitions and Model Updates.
% 0.20/0.29 % (4012651)------------------------------
% 0.20/0.29 % (4012651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.29 % (4012651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.29 % (4012651)CaDiCaL version: 2.1.3
% 0.20/0.29 % (4012651)Termination reason: Satisfiable
% 0.20/0.29 % (4012651)Time elapsed: 0.020 s
% 0.20/0.29 % (4012651)Peak memory usage: 13 MB
% 0.20/0.29 % (4012651)Instructions burned: 52 (million)
% 0.20/0.29 % (4012644)Success in time 0.049 s
% 0.20/0.29 % Vampire exiting
%------------------------------------------------------------------------------