%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRA020+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 10:08:28 AM UTC 2026
% Result : CounterSatisfiable 0.44s 0.51s
% Output : Saturation 0.44s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u62,axiom,
red(n10,n11) ).
cnf(u65,axiom,
~ green(n10,n11) ).
cnf(u71,axiom,
red(n9,n10) ).
cnf(u74,axiom,
~ green(n9,n10) ).
cnf(u80,axiom,
red(n8,n9) ).
cnf(u89,axiom,
red(n7,n8) ).
cnf(u98,axiom,
red(n6,n7) ).
cnf(u101,axiom,
~ green(n6,n7) ).
cnf(u107,axiom,
red(n5,n6) ).
cnf(u110,axiom,
~ green(n5,n6) ).
cnf(u116,axiom,
red(n4,n5) ).
cnf(u125,axiom,
red(n3,n4) ).
cnf(u134,axiom,
red(n2,n3) ).
cnf(u143,axiom,
red(n1,n2) ).
cnf(u161,negated_conjecture,
~ red(n8,n10) ).
cnf(u172,negated_conjecture,
~ red(n7,n9) ).
cnf(u179,negated_conjecture,
( ~ red(X0,X1)
| ~ red(n6,X0)
| ~ red(n6,X1)
| ~ red(n8,X1)
| ~ red(n7,X1)
| ~ red(n8,X0)
| ~ red(n7,X0) ) ).
cnf(u182,negated_conjecture,
red(n6,n8) ).
cnf(u194,negated_conjecture,
~ red(n5,n7) ).
cnf(u205,negated_conjecture,
~ red(n4,n6) ).
cnf(u212,negated_conjecture,
( ~ red(X0,X1)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n5,X1)
| ~ red(n4,X1)
| ~ red(n5,X0)
| ~ red(n4,X0) ) ).
cnf(u215,negated_conjecture,
red(n3,n5) ).
cnf(u223,negated_conjecture,
( ~ red(X0,X1)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n4,X1)
| ~ red(n3,X1)
| ~ red(n4,X0)
| ~ red(n3,X0) ) ).
cnf(u226,negated_conjecture,
red(n2,n4) ).
cnf(u238,negated_conjecture,
~ red(n1,n3) ).
cnf(u295,axiom,
red(n9,n11) ).
cnf(u308,negated_conjecture,
~ green(n1,n5) ).
cnf(u314,axiom,
~ red(n1,n4) ).
cnf(u319,axiom,
green(n1,n4) ).
cnf(u327,axiom,
red(n2,n5) ).
cnf(u339,negated_conjecture,
green(n2,n6) ).
cnf(u348,axiom,
red(n3,n6) ).
cnf(u360,axiom,
red(n4,n7) ).
cnf(u372,negated_conjecture,
green(n3,n7) ).
cnf(u381,axiom,
red(n5,n8) ).
cnf(u384,axiom,
~ green(n5,n8) ).
cnf(u393,axiom,
red(n6,n9) ).
cnf(u396,axiom,
~ green(n6,n9) ).
cnf(u402,negated_conjecture,
( ~ green(X0,X1)
| ~ green(n4,X0)
| ~ green(n4,X1)
| ~ green(n8,X1)
| ~ green(n6,X1)
| ~ green(n8,X0)
| ~ green(n6,X0) ) ).
cnf(u405,negated_conjecture,
green(n4,n8) ).
cnf(u414,axiom,
red(n7,n10) ).
cnf(u425,axiom,
~ red(n8,n11) ).
cnf(u430,axiom,
green(n8,n11) ).
cnf(u435,negated_conjecture,
( ~ green(X0,X1)
| ~ green(n5,X0)
| ~ green(n5,X1)
| ~ green(n9,X1)
| ~ green(n7,X1)
| ~ green(n9,X0)
| ~ green(n7,X0) ) ).
cnf(u438,negated_conjecture,
green(n5,n9) ).
cnf(u456,negated_conjecture,
green(n6,n10) ).
cnf(u483,negated_conjecture,
( ~ red(X0,X1)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n5,X1)
| ~ red(n4,X1)
| ~ red(n5,X0)
| ~ red(n4,X0) ) ).
cnf(u486,negated_conjecture,
red(n1,n5) ).
cnf(u512,negated_conjecture,
~ red(n4,n9) ).
cnf(u516,negated_conjecture,
~ red(n5,n9) ).
cnf(u519,negated_conjecture,
red(n4,n11) ).
cnf(u524,negated_conjecture,
~ red(n5,n11) ).
cnf(u527,negated_conjecture,
red(n3,n11) ).
cnf(u532,negated_conjecture,
~ red(n3,n9) ).
cnf(u537,negated_conjecture,
~ red(n4,n10) ).
cnf(u540,negated_conjecture,
red(n5,n10) ).
cnf(u544,negated_conjecture,
red(n3,n10) ).
cnf(u554,negated_conjecture,
~ red(n4,n2) ).
cnf(u558,negated_conjecture,
~ red(n5,n2) ).
cnf(u562,negated_conjecture,
~ red(n4,n3) ).
cnf(u580,negated_conjecture,
~ red(n4,n1) ).
cnf(u593,negated_conjecture,
~ red(n4,n8) ).
cnf(u597,negated_conjecture,
~ red(n3,n8) ).
cnf(u604,negated_conjecture,
~ red(n4,n4) ).
cnf(u615,negated_conjecture,
~ red(n5,n5) ).
cnf(u628,negated_conjecture,
~ red(n2,n6) ).
cnf(u677,negated_conjecture,
~ red(n3,n7) ).
cnf(u681,negated_conjecture,
~ red(n2,n8) ).
cnf(u685,negated_conjecture,
~ red(n2,n7) ).
cnf(u716,negated_conjecture,
green(n1,n7) ).
cnf(u742,negated_conjecture,
~ red(n1,n7) ).
cnf(u771,negated_conjecture,
red(n1,n6) ).
cnf(u786,negated_conjecture,
~ green(n1,n6) ).
cnf(u824,negated_conjecture,
~ green(n1,n9) ).
cnf(u878,negated_conjecture,
green(n7,n11) ).
cnf(u882,negated_conjecture,
green(n5,n11) ).
cnf(u902,negated_conjecture,
~ green(n9,n1) ).
cnf(u906,negated_conjecture,
~ green(n7,n5) ).
cnf(u938,negated_conjecture,
~ green(n7,n6) ).
cnf(u951,negated_conjecture,
~ green(n9,n7) ).
cnf(u965,negated_conjecture,
~ green(n5,n2) ).
cnf(u971,negated_conjecture,
~ green(n9,n9) ).
cnf(u989,negated_conjecture,
~ red(n6,n11) ).
cnf(u1044,negated_conjecture,
~ green(n1,n8) ).
cnf(u1076,negated_conjecture,
~ red(n2,n10) ).
cnf(u1098,negated_conjecture,
~ green(n4,n11) ).
cnf(u1179,negated_conjecture,
~ green(n6,n2) ).
cnf(u1197,negated_conjecture,
~ green(n8,n1) ).
cnf(u1210,negated_conjecture,
~ green(n6,n6) ).
cnf(u1219,negated_conjecture,
~ green(n6,n4) ).
cnf(u1237,negated_conjecture,
~ green(n8,n8) ).
cnf(u1360,negated_conjecture,
red(n1,n11) ).
cnf(u1364,negated_conjecture,
red(n2,n11) ).
cnf(u1405,negated_conjecture,
~ green(n2,n11) ).
cnf(u1421,axiom,
red(n2,n9) ).
cnf(u1424,axiom,
~ green(n2,n9) ).
cnf(u1442,negated_conjecture,
green(n1,n10) ).
cnf(u1459,negated_conjecture,
~ red(n7,n11) ).
cnf(u1486,negated_conjecture,
~ green(n1,n11) ).
cnf(u1490,negated_conjecture,
~ green(n3,n11) ).
cnf(u1611,negated_conjecture,
~ red(n1,n10) ).
cnf(u1626,negated_conjecture,
~ green(n3,n10) ).
cnf(u1634,negated_conjecture,
~ red(n6,n10) ).
cnf(u1692,negated_conjecture,
~ red(n7,n5) ).
cnf(u1704,negated_conjecture,
~ red(n8,n6) ).
cnf(u1727,negated_conjecture,
~ red(n6,n4) ).
cnf(u1732,negated_conjecture,
~ red(n7,n3) ).
cnf(u1771,negated_conjecture,
~ red(n6,n1) ).
cnf(u1794,negated_conjecture,
~ red(n8,n8) ).
cnf(u1576,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n8,X0)
| ~ green(n4,X0)
| ~ green(n4,X1)
| ~ green(n8,X1)
| ~ green(n10,X1)
| ~ green(X0,X1) ) ).
cnf(u377,axiom,
( ~ less_than(n8,X0)
| less_than(n5,X0) ) ).
cnf(u1410,negated_conjecture,
red(n1,n8) ).
cnf(u755,axiom,
( ~ less_than(n8,X0)
| less_than(n4,X0) ) ).
cnf(u1324,axiom,
less_than(n1,n10) ).
cnf(u1827,axiom,
( ~ less_than(n11,X0)
| less_than(n2,X0) ) ).
cnf(u1318,negated_conjecture,
green(n3,n9) ).
cnf(u1086,negated_conjecture,
( ~ green(n11,X0)
| ~ green(n6,X0)
| ~ green(n6,X1)
| ~ green(n11,X1)
| ~ green(X0,X1)
| ~ green(n6,X2)
| ~ green(n11,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1109,axiom,
less_than(n2,n10) ).
cnf(u1082,negated_conjecture,
green(n6,n11) ).
cnf(u1081,axiom,
( ~ less_than(n11,X0)
| less_than(n6,X0) ) ).
cnf(u1851,axiom,
( ~ less_than(n11,X0)
| less_than(n1,X0) ) ).
cnf(u727,negated_conjecture,
( ~ green(n7,X0)
| ~ green(n3,X0)
| ~ green(n3,X1)
| ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(n3,X2)
| ~ green(n7,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1865,negated_conjecture,
( ~ green(n4,X0)
| ~ green(n1,X0)
| ~ green(n1,X1)
| ~ green(n4,X1)
| ~ green(X0,X1)
| ~ green(n1,X2)
| ~ green(n4,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u25,axiom,
less_than(n5,n6) ).
cnf(u449,axiom,
less_than(n2,n7) ).
cnf(u1538,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n2,X0)
| ~ green(n2,X1)
| ~ green(n10,X1)
| ~ green(X0,X1)
| ~ green(n2,X2)
| ~ green(n10,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1328,axiom,
( ~ less_than(n10,X0)
| less_than(n4,X0) ) ).
cnf(u1878,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n6,X0)
| ~ red(n8,X0)
| ~ red(n1,X0) ) ).
cnf(u249,axiom,
( ~ less_than(n4,X0)
| less_than(n2,X0) ) ).
cnf(u635,negated_conjecture,
( ~ red(n5,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(n2,X2)
| ~ red(n5,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u243,axiom,
( ~ less_than(n3,X0)
| less_than(n1,X0) ) ).
cnf(u464,axiom,
less_than(n4,n9) ).
cnf(u245,negated_conjecture,
( ~ green(n3,X0)
| ~ green(n1,X0)
| ~ green(n1,X1)
| ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(n1,X2)
| ~ green(n3,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u43,axiom,
( ~ less_than(n6,X0)
| less_than(n5,X0) ) ).
cnf(u46,axiom,
( ~ less_than(n9,X0)
| less_than(n8,X0) ) ).
cnf(u1845,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n2,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n2,X1)
| ~ red(n9,X1)
| ~ red(X0,X1) ) ).
cnf(u45,axiom,
( ~ less_than(n8,X0)
| less_than(n7,X0) ) ).
cnf(u39,axiom,
( ~ less_than(n2,X0)
| less_than(n1,X0) ) ).
cnf(u26,axiom,
less_than(n4,n5) ).
cnf(u219,axiom,
less_than(n5,n7) ).
cnf(u862,negated_conjecture,
( ~ red(n10,X0)
| ~ red(n7,X0)
| ~ red(n7,X1)
| ~ red(n10,X1)
| ~ red(X0,X1)
| ~ red(n7,X2)
| ~ red(n10,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1494,negated_conjecture,
red(n1,n9) ).
cnf(u28,axiom,
less_than(n2,n3) ).
cnf(u22,axiom,
less_than(n8,n9) ).
cnf(u1057,axiom,
less_than(n3,n10) ).
cnf(u21,axiom,
less_than(n9,n10) ).
cnf(u1271,negated_conjecture,
( ~ red(n5,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(n1,X2)
| ~ red(n5,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u323,axiom,
( ~ less_than(n5,X0)
| less_than(n2,X0) ) ).
cnf(u1815,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n8,X0)
| ~ red(n6,X0)
| ~ red(n6,X1)
| ~ red(n8,X1)
| ~ red(n9,X1)
| ~ red(X0,X1) ) ).
cnf(u1258,axiom,
( ~ less_than(n7,X0)
| less_than(n1,X0) ) ).
cnf(u1821,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n1,X0)
| ~ green(n1,X1)
| ~ green(n10,X1)
| ~ green(X0,X1)
| ~ green(n1,X2)
| ~ green(n10,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u281,negated_conjecture,
( ~ green(n9,X0)
| ~ green(n7,X0)
| ~ green(n7,X1)
| ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(n7,X2)
| ~ green(n9,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1409,axiom,
( ~ less_than(n8,X0)
| less_than(n1,X0) ) ).
cnf(u277,axiom,
less_than(n6,n9) ).
cnf(u1394,negated_conjecture,
( ~ green(n11,X0)
| ~ green(n8,X0)
| ~ green(n8,X1)
| ~ green(n11,X1)
| ~ green(X0,X1)
| ~ green(n8,X2)
| ~ green(n11,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1527,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(n3,X2)
| ~ red(n11,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u808,axiom,
less_than(n3,n9) ).
cnf(u1033,negated_conjecture,
green(n3,n8) ).
cnf(u1469,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n4,X0)
| ~ red(n4,X1)
| ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(n4,X2)
| ~ red(n11,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u410,axiom,
( ~ less_than(n10,X0)
| less_than(n7,X0) ) ).
cnf(u1493,axiom,
( ~ less_than(n9,X0)
| less_than(n1,X0) ) ).
cnf(u1332,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n4,X0)
| ~ green(n4,X1)
| ~ green(n10,X1)
| ~ green(X0,X1)
| ~ green(n4,X2)
| ~ green(n10,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u208,axiom,
less_than(n3,n5) ).
cnf(u752,axiom,
less_than(n2,n8) ).
cnf(u1445,axiom,
less_than(n1,n11) ).
cnf(u321,axiom,
less_than(n1,n5) ).
cnf(u197,axiom,
less_than(n1,n3) ).
cnf(u153,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n8,X0)
| ~ red(n8,X1)
| ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(n8,X2)
| ~ red(n9,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u344,axiom,
( ~ less_than(n6,X0)
| less_than(n3,X0) ) ).
cnf(u1613,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n6,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n6,X1)
| ~ red(n9,X1)
| ~ red(X0,X1) ) ).
cnf(u496,negated_conjecture,
( ~ red(n5,X0)
| ~ red(n3,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n3,X1)
| ~ red(n5,X1)
| ~ red(X0,X1) ) ).
cnf(u186,negated_conjecture,
( ~ red(n3,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n3,X1)
| ~ red(X0,X1)
| ~ red(n2,X2)
| ~ red(n3,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u271,axiom,
less_than(n5,n8) ).
cnf(u815,negated_conjecture,
( ~ green(n9,X0)
| ~ green(n5,X0)
| ~ green(n5,X1)
| ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(n5,X2)
| ~ green(n9,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u40,axiom,
( ~ less_than(n3,X0)
| less_than(n2,X0) ) ).
cnf(u1844,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(n2,X2)
| ~ red(n9,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u286,negated_conjecture,
green(n8,n10) ).
cnf(u696,negated_conjecture,
( ~ green(n6,X0)
| ~ green(n2,X0)
| ~ green(n2,X1)
| ~ green(n6,X1)
| ~ green(X0,X1)
| ~ green(n2,X2)
| ~ green(n6,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u375,axiom,
less_than(n4,n8) ).
cnf(u1912,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n8,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n8,X1)
| ~ red(n9,X1)
| ~ red(X0,X1) ) ).
cnf(u1069,negated_conjecture,
( ~ red(n10,X0)
| ~ red(n5,X0)
| ~ red(n5,X1)
| ~ red(n10,X1)
| ~ red(X0,X1)
| ~ red(n5,X2)
| ~ red(n10,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u47,axiom,
( ~ less_than(n10,X0)
| less_than(n9,X0) ) ).
cnf(u34,axiom,
( ~ less_than(X0,X1)
| green(X0,X1)
| red(X0,X1) ) ).
cnf(u1322,negated_conjecture,
( ~ green(n9,X0)
| ~ green(n3,X0)
| ~ green(n3,X1)
| ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(n3,X2)
| ~ green(n9,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1502,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(n1,X2)
| ~ red(n9,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1308,axiom,
( ~ less_than(n8,X0)
| less_than(n2,X0) ) ).
cnf(u1114,axiom,
less_than(n3,n11) ).
cnf(u735,negated_conjecture,
( ~ red(n7,X0)
| ~ red(n4,X0)
| ~ red(n4,X1)
| ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(n4,X2)
| ~ red(n7,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1906,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n8,X0)
| ~ green(n2,X0)
| ~ green(n2,X1)
| ~ green(n8,X1)
| ~ green(n10,X1)
| ~ green(X0,X1) ) ).
cnf(u490,axiom,
( ~ less_than(n5,X0)
| less_than(n1,X0) ) ).
cnf(u1417,axiom,
( ~ less_than(n9,X0)
| less_than(n2,X0) ) ).
cnf(u1052,negated_conjecture,
( ~ green(n9,X0)
| ~ green(n4,X0)
| ~ green(n4,X1)
| ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(n4,X2)
| ~ green(n9,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u704,negated_conjecture,
( ~ red(n6,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(n3,X2)
| ~ red(n6,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u839,axiom,
( ~ less_than(n10,X0)
| less_than(n6,X0) ) ).
cnf(u442,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n9,X0)
| ~ red(n9,X1)
| ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(n9,X2)
| ~ red(n11,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u422,axiom,
( ~ less_than(n11,X0)
| less_than(n8,X0) ) ).
cnf(u1046,axiom,
less_than(n2,n9) ).
cnf(u253,axiom,
less_than(n2,n5) ).
cnf(u33,axiom,
( ~ less_than(X0,X1)
| less_than(X0,X2)
| ~ less_than(X1,X2) ) ).
cnf(u36,negated_conjecture,
( ~ green(X0,X1)
| ~ red(X0,X1) ) ).
cnf(u639,axiom,
( ~ less_than(n6,X0)
| less_than(n2,X0) ) ).
cnf(u240,axiom,
less_than(n8,n10) ).
cnf(u247,axiom,
less_than(n1,n4) ).
cnf(u1862,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(n1,X2)
| ~ red(n11,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u268,negated_conjecture,
green(n5,n7) ).
cnf(u230,axiom,
less_than(n7,n9) ).
cnf(u262,negated_conjecture,
green(n4,n6) ).
cnf(u229,axiom,
less_than(n6,n8) ).
cnf(u420,axiom,
less_than(n7,n11) ).
cnf(u27,axiom,
less_than(n3,n4) ).
cnf(u185,negated_conjecture,
( ~ red(n4,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(n3,X2)
| ~ red(n4,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u29,axiom,
less_than(n1,n2) ).
cnf(u1498,negated_conjecture,
green(n2,n10) ).
cnf(u23,axiom,
less_than(n7,n8) ).
cnf(u1317,axiom,
( ~ less_than(n9,X0)
| less_than(n3,X0) ) ).
cnf(u175,negated_conjecture,
( ~ red(n5,X0)
| ~ red(n4,X0)
| ~ red(n4,X1)
| ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(n4,X2)
| ~ red(n5,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1478,negated_conjecture,
( ~ green(n11,X0)
| ~ green(n7,X0)
| ~ green(n7,X1)
| ~ green(n11,X1)
| ~ green(X0,X1)
| ~ green(n7,X2)
| ~ green(n11,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u289,axiom,
less_than(n8,n11) ).
cnf(u164,negated_conjecture,
( ~ red(n7,X0)
| ~ red(n6,X0)
| ~ red(n6,X1)
| ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(n6,X2)
| ~ red(n7,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u283,axiom,
less_than(n7,n10) ).
cnf(u1002,negated_conjecture,
( ~ green(n6,X0)
| ~ green(n4,X0)
| ~ green(n4,X1)
| ~ green(n6,X1)
| ~ green(X0,X1)
| ~ green(n4,X2)
| ~ green(n6,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u285,axiom,
( ~ less_than(n10,X0)
| less_than(n8,X0) ) ).
cnf(u1430,axiom,
( ~ less_than(n10,X0)
| less_than(n3,X0) ) ).
cnf(u1824,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n10,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n10,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u279,axiom,
( ~ less_than(n9,X0)
| less_than(n7,X0) ) ).
cnf(u1388,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n10,X0)
| ~ red(n9,X0)
| ~ red(n9,X1)
| ~ red(n10,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u265,axiom,
less_than(n4,n7) ).
cnf(u1521,negated_conjecture,
( ~ red(n6,X0)
| ~ red(n5,X0)
| ~ red(n5,X1)
| ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(n5,X2)
| ~ red(n6,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1804,negated_conjecture,
( ~ red(n10,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n10,X1)
| ~ red(X0,X1)
| ~ red(n3,X2)
| ~ red(n10,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u259,axiom,
less_than(n3,n6) ).
cnf(u774,negated_conjecture,
( ~ green(n8,X0)
| ~ green(n4,X0)
| ~ green(n4,X1)
| ~ green(n8,X1)
| ~ green(X0,X1)
| ~ green(n4,X2)
| ~ green(n8,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u261,axiom,
( ~ less_than(n6,X0)
| less_than(n4,X0) ) ).
cnf(u1340,axiom,
( ~ less_than(n11,X0)
| less_than(n5,X0) ) ).
cnf(u1024,axiom,
( ~ less_than(n7,X0)
| less_than(n2,X0) ) ).
cnf(u836,axiom,
less_than(n4,n10) ).
cnf(u1497,axiom,
( ~ less_than(n10,X0)
| less_than(n2,X0) ) ).
cnf(u1336,axiom,
less_than(n2,n11) ).
cnf(u1810,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n6,X0)
| ~ green(n6,X1)
| ~ green(n10,X1)
| ~ green(X0,X1)
| ~ green(n6,X2)
| ~ green(n10,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1855,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n2,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n2,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u1920,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n9,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n9,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u1896,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n5,X0)
| ~ red(n6,X0)
| ~ red(n1,X0) ) ).
cnf(u1449,axiom,
( ~ less_than(n11,X0)
| less_than(n4,X0) ) ).
cnf(u645,negated_conjecture,
( ~ red(n4,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(n2,X2)
| ~ red(n4,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1838,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(n2,X2)
| ~ red(n11,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1078,axiom,
less_than(n4,n11) ).
cnf(u699,negated_conjecture,
( ~ red(n5,X0)
| ~ red(n4,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n4,X1)
| ~ red(n5,X1)
| ~ red(X0,X1) ) ).
cnf(u495,negated_conjecture,
( ~ red(n5,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(n3,X2)
| ~ red(n5,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1387,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n10,X0)
| ~ red(n10,X1)
| ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(n10,X2)
| ~ red(n11,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u342,axiom,
less_than(n2,n6) ).
cnf(u974,axiom,
less_than(n5,n11) ).
cnf(u461,axiom,
less_than(n3,n8) ).
cnf(u803,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n5,X0)
| ~ red(n5,X1)
| ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(n5,X2)
| ~ red(n8,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1857,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n2,X0)
| ~ red(n9,X0)
| ~ red(n1,X0) ) ).
cnf(u1813,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n6,X0)
| ~ green(n2,X0)
| ~ green(n2,X1)
| ~ green(n6,X1)
| ~ green(n10,X1)
| ~ green(X0,X1) ) ).
cnf(u722,axiom,
( ~ less_than(n7,X0)
| less_than(n3,X0) ) ).
cnf(u280,negated_conjecture,
green(n7,n9) ).
cnf(u255,axiom,
( ~ less_than(n5,X0)
| less_than(n3,X0) ) ).
cnf(u446,axiom,
less_than(n1,n6) ).
cnf(u1657,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n6,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n6,X1)
| ~ red(n8,X1)
| ~ red(X0,X1) ) ).
cnf(u48,axiom,
( ~ less_than(n11,X0)
| less_than(n10,X0) ) ).
cnf(u241,axiom,
less_than(n9,n11) ).
cnf(u1871,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n4,X0)
| ~ green(n1,X0)
| ~ green(n1,X1)
| ~ green(n4,X1)
| ~ green(n10,X1)
| ~ green(X0,X1) ) ).
cnf(u1530,negated_conjecture,
( ~ green(n11,X0)
| ~ green(n5,X0)
| ~ green(n5,X1)
| ~ green(n11,X1)
| ~ green(X0,X1)
| ~ green(n5,X2)
| ~ green(n11,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u244,negated_conjecture,
green(n1,n3) ).
cnf(u42,axiom,
( ~ less_than(n5,X0)
| less_than(n4,X0) ) ).
cnf(u41,axiom,
( ~ less_than(n4,X0)
| less_than(n3,X0) ) ).
cnf(u1510,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n4,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n4,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u44,axiom,
( ~ less_than(n7,X0)
| less_than(n6,X0) ) ).
cnf(u387,axiom,
less_than(n5,n9) ).
cnf(u1917,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n9,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n9,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u997,axiom,
( ~ less_than(n6,X0)
| less_than(n1,X0) ) ).
cnf(u35,negated_conjecture,
~ goal ).
cnf(u1278,negated_conjecture,
( ~ green(n7,X0)
| ~ green(n1,X0)
| ~ green(n1,X1)
| ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(n1,X2)
| ~ green(n7,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u38,negated_conjecture,
( ~ red(X0,X1)
| ~ red(X0,X2)
| ~ red(X1,X2)
| ~ red(X0,X3)
| ~ red(X1,X3)
| ~ red(X2,X3)
| ~ red(X0,X4)
| ~ red(X1,X4)
| ~ red(X2,X4)
| ~ red(X3,X4) ) ).
cnf(u389,axiom,
( ~ less_than(n9,X0)
| less_than(n6,X0) ) ).
cnf(u37,negated_conjecture,
( ~ green(X0,X1)
| ~ green(X0,X2)
| ~ green(X1,X2)
| ~ green(X0,X3)
| ~ green(X1,X3)
| ~ green(X2,X3)
| ~ green(X0,X4)
| ~ green(X1,X4)
| ~ green(X2,X4)
| ~ green(X3,X4) ) ).
cnf(u1615,axiom,
( ~ less_than(n10,X0)
| less_than(n1,X0) ) ).
cnf(u24,axiom,
less_than(n6,n7) ).
cnf(u1506,axiom,
( ~ less_than(n11,X0)
| less_than(n3,X0) ) ).
cnf(u977,axiom,
( ~ less_than(n11,X0)
| less_than(n7,X0) ) ).
cnf(u1312,negated_conjecture,
( ~ green(n8,X0)
| ~ green(n2,X0)
| ~ green(n2,X1)
| ~ green(n8,X1)
| ~ green(X0,X1)
| ~ green(n2,X2)
| ~ green(n8,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u152,negated_conjecture,
( ~ red(n10,X0)
| ~ red(n9,X0)
| ~ red(n9,X1)
| ~ red(n10,X1)
| ~ red(X0,X1)
| ~ red(n9,X2)
| ~ red(n10,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1831,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n4,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n4,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u311,axiom,
( ~ less_than(n4,X0)
| less_than(n1,X0) ) ).
cnf(u1104,axiom,
less_than(n1,n9) ).
cnf(u1060,axiom,
( ~ less_than(n10,X0)
| less_than(n5,X0) ) ).
cnf(u291,axiom,
( ~ less_than(n11,X0)
| less_than(n9,X0) ) ).
cnf(u719,axiom,
less_than(n1,n7) ).
cnf(u1655,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n6,X0)
| ~ red(n6,X1)
| ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(n6,X2)
| ~ red(n8,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1263,negated_conjecture,
( ~ green(n7,X0)
| ~ green(n3,X0)
| ~ green(n1,X0)
| ~ green(n1,X1)
| ~ green(n3,X1)
| ~ green(n7,X1)
| ~ green(X0,X1) ) ).
cnf(u1890,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n5,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n5,X1)
| ~ red(n8,X1)
| ~ red(X0,X1) ) ).
cnf(u475,axiom,
less_than(n6,n11) ).
cnf(u1050,negated_conjecture,
green(n4,n9) ).
cnf(u1049,axiom,
( ~ less_than(n9,X0)
| less_than(n4,X0) ) ).
cnf(u1020,negated_conjecture,
( ~ red(n6,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(n1,X2)
| ~ red(n6,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u1567,negated_conjecture,
( ~ green(n9,X0)
| ~ green(n7,X0)
| ~ green(n3,X0)
| ~ green(n3,X1)
| ~ green(n7,X1)
| ~ green(n9,X1)
| ~ green(X0,X1) ) ).
cnf(u1036,negated_conjecture,
( ~ green(n8,X0)
| ~ green(n3,X0)
| ~ green(n3,X1)
| ~ green(n8,X1)
| ~ green(X0,X1)
| ~ green(n3,X2)
| ~ green(n8,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1027,negated_conjecture,
( ~ green(n7,X0)
| ~ green(n2,X0)
| ~ green(n2,X1)
| ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(n2,X2)
| ~ green(n7,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1329,negated_conjecture,
green(n4,n10) ).
cnf(u1509,negated_conjecture,
( ~ green(n11,X0)
| ~ green(n7,X0)
| ~ green(n5,X0)
| ~ green(n5,X1)
| ~ green(n7,X1)
| ~ green(n11,X1)
| ~ green(X0,X1) ) ).
cnf(u1029,axiom,
less_than(n1,n8) ).
cnf(u1032,axiom,
( ~ less_than(n8,X0)
| less_than(n3,X0) ) ).
cnf(u1309,negated_conjecture,
green(n2,n8) ).
cnf(u218,axiom,
less_than(n4,n6) ).
cnf(u1025,negated_conjecture,
green(n2,n7) ).
cnf(u408,axiom,
less_than(n6,n10) ).
cnf(u1522,negated_conjecture,
( ~ red(n6,X0)
| ~ red(n5,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n5,X1)
| ~ red(n6,X1)
| ~ red(X0,X1) ) ).
cnf(u20,axiom,
less_than(n10,n11) ).
cnf(u207,axiom,
less_than(n2,n4) ).
cnf(u163,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n7,X0)
| ~ red(n7,X1)
| ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(n7,X2)
| ~ red(n8,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u354,axiom,
less_than(n3,n7) ).
cnf(u1656,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n6,X0)
| ~ red(n5,X0)
| ~ red(n5,X1)
| ~ red(n6,X1)
| ~ red(n8,X1)
| ~ red(X0,X1) ) ).
cnf(u1889,negated_conjecture,
( ~ red(n6,X0)
| ~ red(n5,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n5,X1)
| ~ red(n6,X1)
| ~ red(X0,X1) ) ).
cnf(u196,negated_conjecture,
( ~ red(n2,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(n1,X2)
| ~ red(n2,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u356,axiom,
( ~ less_than(n7,X0)
| less_than(n4,X0) ) ).
cnf(u1832,negated_conjecture,
( ~ red(n11,X0)
| ~ red(n3,X0)
| ~ red(n2,X0)
| ~ red(n2,X1)
| ~ red(n3,X1)
| ~ red(n11,X1)
| ~ red(X0,X1) ) ).
cnf(u1264,negated_conjecture,
( ~ red(n5,X0)
| ~ red(n2,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n2,X1)
| ~ red(n5,X1)
| ~ red(X0,X1) ) ).
cnf(u287,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n8,X0)
| ~ green(n8,X1)
| ~ green(n10,X1)
| ~ green(X0,X1)
| ~ green(n8,X2)
| ~ green(n10,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1619,negated_conjecture,
( ~ red(n10,X0)
| ~ red(n5,X0)
| ~ red(n3,X0)
| ~ red(n3,X1)
| ~ red(n5,X1)
| ~ red(n10,X1)
| ~ red(X0,X1) ) ).
cnf(u467,axiom,
less_than(n5,n10) ).
cnf(u831,negated_conjecture,
( ~ red(n9,X0)
| ~ red(n6,X0)
| ~ red(n6,X1)
| ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(n6,X2)
| ~ red(n9,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
cnf(u273,axiom,
( ~ less_than(n8,X0)
| less_than(n6,X0) ) ).
cnf(u1812,negated_conjecture,
( ~ green(n10,X0)
| ~ green(n6,X0)
| ~ green(n4,X0)
| ~ green(n4,X1)
| ~ green(n6,X1)
| ~ green(n10,X1)
| ~ green(X0,X1) ) ).
cnf(u267,axiom,
( ~ less_than(n7,X0)
| less_than(n5,X0) ) ).
cnf(u811,axiom,
( ~ less_than(n9,X0)
| less_than(n5,X0) ) ).
cnf(u269,negated_conjecture,
( ~ green(n7,X0)
| ~ green(n5,X0)
| ~ green(n5,X1)
| ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(n5,X2)
| ~ green(n7,X2)
| ~ green(X0,X2)
| ~ green(X1,X2) ) ).
cnf(u1414,negated_conjecture,
( ~ red(n8,X0)
| ~ red(n1,X0)
| ~ red(n1,X1)
| ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(n1,X2)
| ~ red(n8,X2)
| ~ red(X0,X2)
| ~ red(X1,X2) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA020+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n011.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 08:49:15 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42 Running first-order model finding
% 0.10/0.42 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.44/0.51 % (2104400)Will run a generic schedule for satisfiability detection.
% 0.44/0.51 % (2104405)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=363028886_2999 on theBenchmark for (2999ds/0Mi)
% 0.44/0.51 % Detected minimum model sizes of [1]
% 0.44/0.51 % Detected maximum model sizes of [11]
% 0.44/0.51 % TRYING [1]
% 0.44/0.51 % TRYING [2]
% 0.44/0.51 % TRYING [3]
% 0.44/0.51 % TRYING [4]
% 0.44/0.51 % TRYING [5]
% 0.44/0.51 % (2104406)% WARNING: option uhcvi not known.
% 0.44/0.51 % (2104408)dis+10_1_sil=32000:sp=arity:random_seed=4187292189:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.44/0.51 % (2104407)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=8364389:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.44/0.51 % (2104411)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1003335972:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.44/0.51 % (2104409)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1625079088:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.44/0.51 % (2104410)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2038693868:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.44/0.51 % (2104406)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3604694904:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.44/0.51 % TRYING [6]
% 0.44/0.51 % TRYING [7]
% 0.44/0.51 % (2104410) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2104400-2104410"...
% 0.44/0.51 % (2104409)Instruction limit reached!
% 0.44/0.51 % (2104409)------------------------------
% 0.44/0.51 % (2104409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.51 % (2104409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.51 % (2104409)CaDiCaL version: 2.1.3
% 0.44/0.51 % (2104409)Termination reason: Instruction limit
% 0.44/0.51 % (2104409)Termination phase: Saturation
% 0.44/0.51 % (2104409)Time elapsed: 0.045 s
% 0.44/0.51 % (2104409)Peak memory usage: 11 MB
% 0.44/0.51 % (2104409)Instructions burned: 116 (million)
% 0.44/0.51 % (2104410)...printing done.
% 0.44/0.51 % SZS status CounterSatisfiable for theBenchmark
% 0.44/0.51 % SZS output start Saturation.
% See solution above
% 0.44/0.51 % SZS output start Definitions and Model Updates.
% 0.44/0.51 % SZS output end Definitions and Model Updates.
% 0.44/0.51 % (2104410)------------------------------
% 0.44/0.51 % (2104410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.51 % (2104410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.51 % (2104410)CaDiCaL version: 2.1.3
% 0.44/0.51 % (2104410)Termination reason: Satisfiable
% 0.44/0.51 % (2104410)Time elapsed: 0.045 s
% 0.44/0.51 % (2104410)Peak memory usage: 12 MB
% 0.44/0.51 % (2104410)Instructions burned: 87 (million)
% 0.44/0.51 % (2104400)Success in time 0.079 s
% 0.44/0.51 % Vampire exiting
%------------------------------------------------------------------------------