%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRA024+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:29 AM UTC 2026
% Result : CounterSatisfiable 5.71s 1.27s
% Output : Saturation 5.71s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u105,axiom,
~ less_than(X0,n1) ).
cnf(u173,axiom,
~ green(X0,n1) ).
cnf(u206,axiom,
~ red(X0,n1) ).
cnf(u209,axiom,
~ red(X0,n2) ).
cnf(u364,axiom,
~ red(X0,n4) ).
cnf(u390,axiom,
~ red(n2,n2) ).
cnf(u436,axiom,
~ red(n2,n3) ).
cnf(u441,axiom,
green(n2,n3) ).
cnf(u446,axiom,
~ red(X0,n3) ).
cnf(u482,axiom,
( ~ red(X2,n4)
| ~ red(X2,X0)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n2)
| ~ red(X0,n2)
| ~ red(X1,n3)
| ~ red(X0,n3)
| ~ red(X2,n3)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n2) ) ).
cnf(u494,axiom,
~ red(n3,n3) ).
cnf(u502,axiom,
red(n4,n5) ).
cnf(u505,axiom,
~ green(n4,n5) ).
cnf(u520,axiom,
~ red(n5,n6) ).
cnf(u525,axiom,
green(n5,n6) ).
cnf(u530,axiom,
~ red(n6,n7) ).
cnf(u535,axiom,
green(n6,n7) ).
cnf(u548,axiom,
~ red(n7,n8) ).
cnf(u553,axiom,
green(n7,n8) ).
cnf(u564,axiom,
~ green(X0,n5) ).
cnf(u580,axiom,
~ red(n4,n4) ).
cnf(u591,axiom,
~ red(n5,n5) ).
cnf(u594,axiom,
( ~ red(X2,n6)
| ~ red(X2,X0)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u601,axiom,
red(n8,n9) ).
cnf(u604,axiom,
~ green(n8,n9) ).
cnf(u640,axiom,
~ red(n6,n6) ).
cnf(u651,axiom,
~ red(n7,n7) ).
cnf(u654,axiom,
( ~ red(X2,n8)
| ~ red(X2,X0)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u661,axiom,
red(n9,n10) ).
cnf(u664,axiom,
~ green(n9,n10) ).
cnf(u671,axiom,
red(n10,n11) ).
cnf(u674,axiom,
~ green(n10,n11) ).
cnf(u694,axiom,
~ green(X0,n9) ).
cnf(u710,axiom,
~ red(n8,n8) ).
cnf(u713,axiom,
( ~ red(X2,n9)
| ~ red(X2,X0)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X2,n8)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u721,axiom,
~ red(n9,n9) ).
cnf(u724,axiom,
( ~ red(X2,n10)
| ~ red(X2,X0)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u838,axiom,
~ green(n5,n5) ).
cnf(u841,axiom,
( ~ green(X2,n6)
| ~ green(X2,X0)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u877,axiom,
~ green(n2,n2) ).
cnf(u984,axiom,
~ green(n3,n2) ).
cnf(u987,axiom,
( ~ green(X2,n5)
| ~ green(X2,X0)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n2) ) ).
cnf(u996,axiom,
~ green(X0,n11) ).
cnf(u1014,axiom,
~ green(n4,n4) ).
cnf(u1029,axiom,
~ green(n6,n6) ).
cnf(u1041,axiom,
~ green(n7,n7) ).
cnf(u1044,axiom,
( ~ green(X2,n8)
| ~ green(X2,X0)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X2,n7)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u1055,axiom,
~ green(n8,n8) ).
cnf(u1058,axiom,
( ~ green(X2,n9)
| ~ green(X2,X0)
| ~ green(X1,n9)
| ~ green(X0,n9)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X2,n8)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u1065,axiom,
~ green(n9,n9) ).
cnf(u1068,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n9)
| ~ green(X0,n9)
| ~ green(X2,n9)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u1076,axiom,
~ red(n10,n10) ).
cnf(u1079,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X2,n10)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u1183,axiom,
~ green(n9,X1) ).
cnf(u1275,axiom,
~ green(n10,n10) ).
cnf(u1288,axiom,
~ green(n3,n3) ).
cnf(u1358,axiom,
( ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n7,X0)
| ~ red(X1,n7) ) ).
cnf(u1410,axiom,
~ green(n4,n6) ).
cnf(u1413,axiom,
( ~ green(X2,n7)
| ~ green(X2,X0)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n6) ) ).
cnf(u1421,axiom,
~ green(n6,n4) ).
cnf(u1441,axiom,
~ green(n3,n6) ).
cnf(u1447,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n4)
| ~ green(X0,n6)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(n3,X0)
| ~ green(X1,n4)
| ~ green(X1,n6) ) ).
cnf(u1453,axiom,
( ~ green(X2,n7)
| ~ green(X2,X0)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n6) ) ).
cnf(u1462,axiom,
~ green(n6,n3) ).
cnf(u1832,axiom,
red(n3,n5) ).
cnf(u1835,axiom,
~ green(n3,n5) ).
cnf(u1855,axiom,
~ green(n11,n11) ).
cnf(u1858,axiom,
~ green(n11,X0) ).
cnf(u1908,axiom,
green(n8,n10) ).
cnf(u1912,axiom,
( ~ green(X2,n11)
| ~ green(X2,X0)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X2,n8)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n10) ) ).
cnf(u1921,axiom,
~ green(n9,n8) ).
cnf(u1929,axiom,
~ green(n10,n8) ).
cnf(u1979,axiom,
green(n6,n10) ).
cnf(u1983,axiom,
green(n6,n8) ).
cnf(u2001,axiom,
~ green(n6,n9) ).
cnf(u2004,axiom,
( ~ green(X2,n11)
| ~ green(X2,X0)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X1,n9)
| ~ green(X0,n9)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X2,n6)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n9) ) ).
cnf(u2015,axiom,
~ green(n8,n6) ).
cnf(u2044,axiom,
~ green(n9,n6) ).
cnf(u2055,axiom,
~ green(n7,n6) ).
cnf(u2063,axiom,
~ green(n10,n9) ).
cnf(u2067,axiom,
~ green(n10,n6) ).
cnf(u2070,axiom,
~ green(n10,X1) ).
cnf(u2111,axiom,
~ green(n5,n9) ).
cnf(u2114,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n6)
| ~ green(X0,n9)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(n5,X0)
| ~ green(X1,n6)
| ~ green(X1,n9) ) ).
cnf(u2124,axiom,
green(n5,n10) ).
cnf(u2132,axiom,
green(n5,n8) ).
cnf(u2136,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n8)
| ~ green(X0,n10)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(n5,X0)
| ~ green(X1,n8)
| ~ green(X1,n10) ) ).
cnf(u2143,axiom,
( ~ green(X2,n11)
| ~ green(X2,X0)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n8) ) ).
cnf(u2167,axiom,
~ green(n7,n5) ).
cnf(u2183,axiom,
~ green(n9,n5) ).
cnf(u2196,axiom,
~ red(n10,n7) ).
cnf(u2200,axiom,
~ red(n10,n8) ).
cnf(u2207,axiom,
red(n7,n9) ).
cnf(u2211,axiom,
( ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n7,X0)
| ~ red(X1,n9) ) ).
cnf(u2233,axiom,
~ green(n4,n8) ).
cnf(u2261,axiom,
~ red(n1,n3) ).
cnf(u2266,axiom,
green(n1,n3) ).
cnf(u2356,axiom,
( ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(n7,X0)
| ~ green(X1,n7) ) ).
cnf(u2408,axiom,
green(n3,n4) ).
cnf(u2412,axiom,
( ~ green(X2,n5)
| ~ green(X2,X0)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n4) ) ).
cnf(u2440,axiom,
~ red(n5,n7) ).
cnf(u2445,axiom,
green(n5,n7) ).
cnf(u2462,axiom,
~ red(n8,n7) ).
cnf(u2479,axiom,
~ green(n4,n3) ).
cnf(u2500,axiom,
green(n7,n10) ).
cnf(u2508,axiom,
( ~ green(X0,n7)
| ~ green(n5,X0)
| ~ green(X0,n11)
| ~ green(X0,n10)
| ~ green(X0,n8) ) ).
cnf(u2514,axiom,
~ green(n5,n4) ).
cnf(u2612,axiom,
red(n2,n5) ).
cnf(u2615,axiom,
~ green(n2,n5) ).
cnf(u2625,axiom,
( ~ red(n10,X1)
| ~ red(X0,X1)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n10,X0)
| ~ red(X1,n10) ) ).
cnf(u2670,axiom,
( ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n9,X0)
| ~ red(X1,n10) ) ).
cnf(u2703,axiom,
~ red(n11,n10) ).
cnf(u2706,axiom,
( ~ red(n10,X0)
| ~ red(X0,n10) ) ).
cnf(u2756,axiom,
~ red(n4,n7) ).
cnf(u2761,axiom,
green(n4,n7) ).
cnf(u2839,axiom,
( ~ green(X2,n4)
| ~ green(X2,X0)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X2,n2)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n3) ) ).
cnf(u2888,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u2894,axiom,
( ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n9,X0)
| ~ red(X1,n9) ) ).
cnf(u2901,axiom,
~ red(n11,n9) ).
cnf(u2905,axiom,
~ red(n11,n11) ).
cnf(u2913,axiom,
~ red(n10,n9) ).
cnf(u2939,axiom,
~ red(n7,n10) ).
cnf(u2973,axiom,
red(n1,n5) ).
cnf(u2976,axiom,
~ green(n1,n5) ).
cnf(u2994,axiom,
red(n2,n6) ).
cnf(u2997,axiom,
~ green(n2,n6) ).
cnf(u3028,axiom,
~ green(n5,n3) ).
cnf(u3031,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n6)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(n5,X0)
| ~ green(X1,n3)
| ~ green(X1,n6) ) ).
cnf(u3042,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n5,X0)
| ~ red(X1,n7) ) ).
cnf(u3079,axiom,
~ red(n5,n4) ).
cnf(u3089,axiom,
red(n4,n6) ).
cnf(u3093,axiom,
( ~ red(X2,n7)
| ~ red(X2,X0)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X2,n4)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n6) ) ).
cnf(u3125,axiom,
~ green(n4,n2) ).
cnf(u3190,axiom,
~ red(n7,n5) ).
cnf(u3197,axiom,
~ red(n7,n6) ).
cnf(u3211,axiom,
red(n4,n8) ).
cnf(u3256,axiom,
~ red(n9,n7) ).
cnf(u3260,axiom,
~ red(n9,n8) ).
cnf(u3281,axiom,
green(n2,n4) ).
cnf(u3288,axiom,
( ~ green(n2,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n4)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(n2,X0)
| ~ green(X1,n3)
| ~ green(X1,n4) ) ).
cnf(u3296,axiom,
green(n1,n4) ).
cnf(u3300,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n4)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(n1,X0)
| ~ green(X1,n3)
| ~ green(X1,n4) ) ).
cnf(u3304,axiom,
( ~ green(X2,n5)
| ~ green(X2,X0)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n2) ) ).
cnf(u3391,axiom,
~ red(n11,n7) ).
cnf(u3395,axiom,
~ red(n11,n8) ).
cnf(u3445,axiom,
~ red(n5,n2) ).
cnf(u3491,axiom,
( ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n8,X0)
| ~ red(X1,n9) ) ).
cnf(u3499,axiom,
red(n6,n9) ).
cnf(u3506,axiom,
( ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n6,X0)
| ~ red(X1,n9) ) ).
cnf(u3515,axiom,
( ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n7,X0)
| ~ red(X1,n9) ) ).
cnf(u3522,axiom,
( ~ green(n6,X1)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(n6,X0)
| ~ green(X1,n7) ) ).
cnf(u3655,axiom,
red(n3,n7) ).
cnf(u3658,axiom,
~ green(n3,n7) ).
cnf(u3697,axiom,
red(n2,n7) ).
cnf(u3700,axiom,
~ green(n2,n7) ).
cnf(u3714,axiom,
red(n3,n8) ).
cnf(u3717,axiom,
~ green(n3,n8) ).
cnf(u3726,axiom,
green(n1,n2) ).
cnf(u3730,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n2)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(n1,X0)
| ~ green(X1,n3)
| ~ green(X1,n2) ) ).
cnf(u3752,axiom,
~ green(n5,n2) ).
cnf(u3804,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n2)
| ~ green(X0,n3)
| ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(n1,X0)
| ~ green(X1,n2)
| ~ green(X1,n3) ) ).
cnf(u3814,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n4)
| ~ green(X0,n2)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(n1,X0)
| ~ green(X1,n4)
| ~ green(X1,n2) ) ).
cnf(u3824,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n2)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X0,X1)
| ~ green(X0,n4)
| ~ green(X1,n2)
| ~ green(X1,n4) ) ).
cnf(u3834,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n2)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X1,n2)
| ~ green(X1,n3) ) ).
cnf(u4002,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n4,X0)
| ~ red(X1,n7) ) ).
cnf(u4013,axiom,
( ~ red(X2,n9)
| ~ red(X2,X0)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n6) ) ).
cnf(u4032,axiom,
~ red(n8,n5) ).
cnf(u4039,axiom,
~ red(n8,n6) ).
cnf(u4049,axiom,
red(n1,n6) ).
cnf(u4052,axiom,
~ green(n1,n6) ).
cnf(u4082,axiom,
~ red(n9,n5) ).
cnf(u4103,axiom,
~ red(n5,n10) ).
cnf(u4111,axiom,
( ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n9,X0)
| ~ green(X1,n9) ) ).
cnf(u4116,axiom,
( ~ red(n4,X0)
| ~ red(X0,n5)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u4119,axiom,
red(n5,n9) ).
cnf(u4163,axiom,
( ~ red(n7,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n10) ) ).
cnf(u4175,axiom,
~ red(n8,n10) ).
cnf(u4178,axiom,
( ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n8,X0)
| ~ red(X1,n10) ) ).
cnf(u4203,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n5,X0)
| ~ red(X1,n9) ) ).
cnf(u4223,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n8)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(n5,X0)
| ~ green(X1,n8) ) ).
cnf(u4233,axiom,
~ green(n7,n9) ).
cnf(u4236,axiom,
( ~ green(n5,X0)
| ~ green(X0,n7)
| ~ green(X0,n9)
| ~ green(X0,n8) ) ).
cnf(u4312,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X2,n8)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n6) ) ).
cnf(u4344,axiom,
( ~ green(n8,X1)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n8,X0)
| ~ green(X1,n9) ) ).
cnf(u4356,axiom,
~ red(n10,n6) ).
cnf(u4378,axiom,
( ~ red(X2,n10)
| ~ red(X2,X0)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X2,n8)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n6) ) ).
cnf(u4389,axiom,
~ red(n6,n8) ).
cnf(u4431,axiom,
~ green(n7,n4) ).
cnf(u4434,axiom,
( ~ green(X2,n9)
| ~ green(X2,X0)
| ~ green(X1,n9)
| ~ green(X0,n9)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X2,n7)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n4) ) ).
cnf(u4467,axiom,
~ red(n5,n8) ).
cnf(u4470,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n6)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n5,X0)
| ~ red(X1,n8)
| ~ red(X1,n6) ) ).
cnf(u4499,axiom,
( ~ red(X2,n10)
| ~ red(X2,X0)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n8) ) ).
cnf(u4510,axiom,
~ red(n6,n5) ).
cnf(u4522,axiom,
~ red(n6,n10) ).
cnf(u4567,axiom,
red(n1,n7) ).
cnf(u4570,axiom,
~ green(n1,n7) ).
cnf(u4620,axiom,
red(n2,n8) ).
cnf(u4653,axiom,
~ green(n8,n4) ).
cnf(u4660,axiom,
~ green(n8,n3) ).
cnf(u4687,axiom,
~ red(n4,n10) ).
cnf(u4692,axiom,
green(n4,n10) ).
cnf(u4782,axiom,
~ red(n11,n6) ).
cnf(u4812,axiom,
red(n1,n8) ).
cnf(u4845,axiom,
( ~ green(n2,X1)
| ~ green(X0,X1)
| ~ green(X0,n8)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(n2,X0)
| ~ green(X1,n8) ) ).
cnf(u4874,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n2,X0)
| ~ red(X1,n7) ) ).
cnf(u4883,axiom,
red(n4,n9) ).
cnf(u4910,axiom,
~ red(n9,n4) ).
cnf(u4931,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n3)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X1,n3)
| ~ red(X1,n6) ) ).
cnf(u4935,axiom,
~ red(n5,n3) ).
cnf(u4953,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n3)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X1,n3)
| ~ red(X1,n6) ) ).
cnf(u4957,axiom,
~ red(n4,n3) ).
cnf(u5102,axiom,
( ~ green(n1,X0)
| ~ green(X0,n4)
| ~ green(X0,n3)
| ~ green(X0,n7)
| ~ green(X0,n2) ) ).
cnf(u5110,axiom,
( ~ green(n2,X1)
| ~ green(n2,X0)
| ~ green(X0,n3)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X0,X1)
| ~ green(X0,n4)
| ~ green(X1,n3)
| ~ green(X1,n4) ) ).
cnf(u5123,axiom,
( ~ green(X2,n7)
| ~ green(X2,X0)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X2,n2)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n3) ) ).
cnf(u5160,axiom,
red(n3,n9) ).
cnf(u5179,axiom,
( ~ red(n5,X0)
| ~ red(X0,n6)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u5187,axiom,
( ~ red(n4,X0)
| ~ red(X0,n5)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u5195,axiom,
( ~ red(n4,X0)
| ~ red(X0,n6)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u5207,axiom,
( ~ red(n2,X0)
| ~ red(X0,n6)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u5214,axiom,
( ~ red(n3,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n3,X0)
| ~ red(X1,n7) ) ).
cnf(u5223,axiom,
( ~ red(n3,X0)
| ~ red(X0,n6)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u5230,axiom,
( ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n6,X0)
| ~ red(X1,n7) ) ).
cnf(u5237,axiom,
( ~ red(X2,n10)
| ~ red(X2,X0)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n7) ) ).
cnf(u5252,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n1,X0)
| ~ red(X1,n7) ) ).
cnf(u5261,axiom,
( ~ red(n1,X0)
| ~ red(X0,n6)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u5268,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n7) ) ).
cnf(u5279,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X0,n7)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n5,X0)
| ~ red(X1,n6)
| ~ red(X1,n7) ) ).
cnf(u5285,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n7) ) ).
cnf(u5306,axiom,
( ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n6,X0)
| ~ red(X1,n9) ) ).
cnf(u5314,axiom,
( ~ red(n6,X0)
| ~ red(X0,n8)
| ~ red(X0,n11)
| ~ red(X0,n9) ) ).
cnf(u5339,axiom,
( ~ red(n6,X0)
| ~ red(X0,n7)
| ~ red(X0,n11)
| ~ red(X0,n9) ) ).
cnf(u5408,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n5,X0)
| ~ red(X1,n9) ) ).
cnf(u5435,axiom,
( ~ red(n5,X0)
| ~ red(X0,n6)
| ~ red(X0,n11)
| ~ red(X0,n9) ) ).
cnf(u5517,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(n5,X0)
| ~ green(X1,n7) ) ).
cnf(u5677,axiom,
red(n3,n6) ).
cnf(u5681,axiom,
( ~ red(n3,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n3,X0)
| ~ red(X1,n7)
| ~ red(X1,n6) ) ).
cnf(u5704,axiom,
( ~ red(n3,X0)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n6)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(n3,X1)
| ~ red(X1,n4)
| ~ red(X1,n6) ) ).
cnf(u5812,axiom,
( ~ red(n8,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n10) ) ).
cnf(u5827,axiom,
red(n3,n10) ).
cnf(u5987,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X2,n6)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n8) ) ).
cnf(u5997,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n6)
| ~ green(X0,n8)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n5,X0)
| ~ green(X1,n6)
| ~ green(X1,n8) ) ).
cnf(u6006,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n7) ) ).
cnf(u6078,axiom,
red(n2,n10) ).
cnf(u6222,axiom,
( ~ green(n5,X0)
| ~ green(X0,n6)
| ~ green(X0,n8)
| ~ green(X0,n7) ) ).
cnf(u6278,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X2,n6)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n7) ) ).
cnf(u6309,axiom,
red(n1,n10) ).
cnf(u6395,axiom,
( ~ red(n2,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u6410,axiom,
( ~ red(n2,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n8) ) ).
cnf(u1553,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n8) ) ).
cnf(u1940,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n11) ) ).
cnf(u1567,axiom,
less_than(n6,n9) ).
cnf(u1566,axiom,
less_than(n5,n9) ).
cnf(u5650,axiom,
( ~ green(X3,n10)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X1,n4)
| ~ green(X3,n4)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u51,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n2) ) ).
cnf(u5667,axiom,
( ~ red(n3,X1)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u404,axiom,
less_than(n2,n5) ).
cnf(u38,axiom,
( ~ red(X4,X5)
| ~ 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)
| ~ red(X0,X5)
| ~ red(X1,X5)
| ~ red(X2,X5)
| ~ red(X3,X5)
| ~ red(X0,X1) ) ).
cnf(u1426,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n7) ) ).
cnf(u5567,axiom,
( ~ red(n4,X1)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n4,X0)
| ~ red(X0,X1) ) ).
cnf(u2217,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n11) ) ).
cnf(u6059,axiom,
( ~ red(n1,X1)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u6330,axiom,
( ~ red(n1,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u5041,axiom,
( ~ green(X3,n4)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n2)
| ~ green(X2,n2)
| ~ green(X1,n2)
| ~ green(X3,n2)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X1,n4)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u6099,axiom,
( ~ red(n2,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u5612,axiom,
( ~ green(X3,n10)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n7)
| ~ green(X2,n7)
| ~ green(X1,n7)
| ~ green(X3,n7)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1481,axiom,
less_than(n4,n8) ).
cnf(u5847,axiom,
( ~ red(n3,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u1753,axiom,
less_than(n6,n11) ).
cnf(u1661,axiom,
less_than(n7,n10) ).
cnf(u1642,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n9) ) ).
cnf(u1659,axiom,
less_than(n5,n10) ).
cnf(u1551,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n8) ) ).
cnf(u6520,axiom,
( ~ red(n1,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u896,axiom,
less_than(n3,n6) ).
cnf(u6180,axiom,
( ~ red(n3,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n8) ) ).
cnf(u22,axiom,
less_than(n8,n9) ).
cnf(u6536,axiom,
( ~ red(n1,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n6) ) ).
cnf(u35,negated_conjecture,
~ goal ).
cnf(u405,axiom,
less_than(n3,n5) ).
cnf(u60,axiom,
( ~ less_than(X0,n10)
| less_than(X0,n11) ) ).
cnf(u6328,axiom,
( ~ red(n1,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u2247,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n11) ) ).
cnf(u328,axiom,
less_than(n1,n4) ).
cnf(u1731,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n10) ) ).
cnf(u861,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n5) ) ).
cnf(u1737,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n10) ) ).
cnf(u1751,axiom,
less_than(n4,n11) ).
cnf(u5740,axiom,
red(n2,n9) ).
cnf(u1756,axiom,
less_than(n9,n11) ).
cnf(u5633,axiom,
( ~ red(n1,X1)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u1754,axiom,
less_than(n7,n11) ).
cnf(u1662,axiom,
less_than(n8,n10) ).
cnf(u1522,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n8) ) ).
cnf(u6393,axiom,
( ~ red(n2,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u2958,axiom,
( ~ red(X3,n11)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n8)
| ~ red(X2,n8)
| ~ red(X1,n8)
| ~ red(X3,n8)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u29,axiom,
less_than(n1,n2) ).
cnf(u4743,axiom,
red(n5,n11) ).
cnf(u2522,axiom,
( ~ red(X3,n11)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n10)
| ~ red(X2,n10)
| ~ red(X1,n10)
| ~ red(X3,n10)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u5913,axiom,
( ~ red(n4,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n4,X0)
| ~ red(X0,X1) ) ).
cnf(u5939,axiom,
( ~ red(n4,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n6) ) ).
cnf(u59,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n10) ) ).
cnf(u4286,axiom,
( ~ red(X3,n11)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X1,n6)
| ~ red(X3,n6)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2096,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n11) ) ).
cnf(u34,axiom,
( ~ less_than(X0,X1)
| green(X0,X1)
| red(X0,X1) ) ).
cnf(u6182,axiom,
( ~ red(n3,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n6) ) ).
cnf(u57,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n8) ) ).
cnf(u3774,axiom,
( ~ red(X3,n8)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n3)
| ~ red(X2,n3)
| ~ red(X1,n3)
| ~ red(X3,n3)
| ~ red(X0,n8)
| ~ red(X2,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u6047,axiom,
red(n1,n9) ).
cnf(u6537,axiom,
( ~ red(n1,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n5) ) ).
cnf(u5473,axiom,
( ~ red(X3,n9)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X1,n6)
| ~ red(X3,n6)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X1,n9)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u329,axiom,
less_than(n2,n4) ).
cnf(u5709,axiom,
( ~ green(X3,n4)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X1,n3)
| ~ green(X3,n3)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X1,n4)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1890,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n11) ) ).
cnf(u1735,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n10) ) ).
cnf(u6098,axiom,
( ~ red(n2,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u3379,axiom,
red(n7,n11) ).
cnf(u864,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n5) ) ).
cnf(u5458,axiom,
( ~ red(n4,X1)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n4,X0)
| ~ red(X0,X1) ) ).
cnf(u1755,axiom,
less_than(n8,n11) ).
cnf(u1646,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n9) ) ).
cnf(u5850,axiom,
( ~ red(n3,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u1121,axiom,
less_than(n1,n7) ).
cnf(u1656,axiom,
less_than(n2,n10) ).
cnf(u6411,axiom,
( ~ red(n2,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n7) ) ).
cnf(u2953,axiom,
red(n8,n11) ).
cnf(u1564,axiom,
less_than(n3,n9) ).
cnf(u5396,axiom,
( ~ red(X3,n9)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X1,n7)
| ~ red(X3,n7)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X1,n9)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2597,axiom,
( ~ red(X3,n11)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X1,n9)
| ~ red(X3,n9)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2595,axiom,
red(n9,n11) ).
cnf(u28,axiom,
less_than(n2,n3) ).
cnf(u6534,axiom,
( ~ red(n1,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n8) ) ).
cnf(u6165,axiom,
( ~ red(n3,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u6039,axiom,
( ~ green(X3,n7)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X1,n4)
| ~ green(X3,n4)
| ~ green(X0,n7)
| ~ green(X2,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u58,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n9) ) ).
cnf(u3358,axiom,
~ red(n1,n4) ).
cnf(u6057,axiom,
( ~ red(n1,X1)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u1429,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n7) ) ).
cnf(u6452,axiom,
( ~ red(n2,X0)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X0,n9) ) ).
cnf(u5916,axiom,
( ~ red(n4,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n4,X0)
| ~ red(X0,X1) ) ).
cnf(u403,axiom,
less_than(n1,n5) ).
cnf(u1368,axiom,
( ~ green(X3,n8)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n7)
| ~ green(X2,n7)
| ~ green(X1,n7)
| ~ green(X3,n7)
| ~ green(X0,n8)
| ~ green(X2,n8)
| ~ green(X1,n8)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u3386,axiom,
( ~ red(X3,n11)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X1,n7)
| ~ red(X3,n7)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u56,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n7) ) ).
cnf(u1124,axiom,
less_than(n4,n7) ).
cnf(u5725,axiom,
( ~ red(n3,X1)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u1479,axiom,
less_than(n2,n8) ).
cnf(u1371,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n7) ) ).
cnf(u1739,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n10) ) ).
cnf(u359,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n4) ) ).
cnf(u6491,axiom,
red(n1,n11) ).
cnf(u1640,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n9) ) ).
cnf(u5752,axiom,
( ~ red(n2,X1)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u6097,axiom,
( ~ red(n2,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u1402,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n7) ) ).
cnf(u1122,axiom,
less_than(n2,n7) ).
cnf(u6367,axiom,
red(n2,n11) ).
cnf(u6394,axiom,
( ~ red(n2,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u52,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n3) ) ).
cnf(u6137,axiom,
red(n3,n11) ).
cnf(u6183,axiom,
( ~ red(n3,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n5) ) ).
cnf(u27,axiom,
less_than(n3,n4) ).
cnf(u1943,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n11) ) ).
cnf(u897,axiom,
less_than(n4,n6) ).
cnf(u6181,axiom,
( ~ red(n3,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n7) ) ).
cnf(u25,axiom,
less_than(n5,n6) ).
cnf(u2093,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n11) ) ).
cnf(u5534,axiom,
( ~ red(X3,n9)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X1,n5)
| ~ red(X3,n5)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X1,n9)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1725,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n10) ) ).
cnf(u6238,axiom,
( ~ red(n3,X0)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X0,n9) ) ).
cnf(u6331,axiom,
( ~ red(n1,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u6576,axiom,
( ~ red(n1,X0)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X0,n9) ) ).
cnf(u6100,axiom,
( ~ red(n2,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u6517,axiom,
( ~ red(n1,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u1483,axiom,
less_than(n6,n8) ).
cnf(u5384,axiom,
( ~ green(X3,n10)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n8)
| ~ green(X2,n8)
| ~ green(X1,n8)
| ~ green(X3,n8)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1748,axiom,
less_than(n1,n11) ).
cnf(u1887,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n11) ) ).
cnf(u1125,axiom,
less_than(n5,n7) ).
cnf(u1752,axiom,
less_than(n5,n11) ).
cnf(u1660,axiom,
less_than(n6,n10) ).
cnf(u895,axiom,
less_than(n2,n6) ).
cnf(u6392,axiom,
( ~ red(n2,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u26,axiom,
less_than(n4,n5) ).
cnf(u36,axiom,
( ~ green(X0,X1)
| ~ red(X0,X1) ) ).
cnf(u6166,axiom,
( ~ red(n3,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u5888,axiom,
red(n4,n11) ).
cnf(u6016,axiom,
( ~ green(X3,n8)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n6)
| ~ green(X2,n6)
| ~ green(X1,n6)
| ~ green(X3,n6)
| ~ green(X0,n8)
| ~ green(X2,n8)
| ~ green(X1,n8)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u24,axiom,
less_than(n6,n7) ).
cnf(u55,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n6) ) ).
cnf(u1562,axiom,
less_than(n1,n9) ).
cnf(u1568,axiom,
less_than(n7,n9) ).
cnf(u53,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n4) ) ).
cnf(u6516,axiom,
( ~ red(n1,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u5937,axiom,
( ~ red(n4,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n8) ) ).
cnf(u6329,axiom,
( ~ red(n1,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u1604,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n9) ) ).
cnf(u1749,axiom,
less_than(n2,n11) ).
cnf(u4755,axiom,
( ~ red(X3,n11)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X1,n5)
| ~ red(X3,n5)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1638,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n9) ) ).
cnf(u1644,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n9) ) ).
cnf(u5750,axiom,
( ~ red(n2,X1)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u5848,axiom,
( ~ red(n3,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u6518,axiom,
( ~ red(n1,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u894,axiom,
less_than(n1,n6) ).
cnf(u6519,axiom,
( ~ red(n1,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u20,axiom,
less_than(n10,n11) ).
cnf(u5150,axiom,
( ~ green(X3,n3)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n2)
| ~ green(X2,n2)
| ~ green(X1,n2)
| ~ green(X3,n2)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X1,n3)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1657,axiom,
less_than(n3,n10) ).
cnf(u33,axiom,
( ~ less_than(X1,X2)
| ~ less_than(X0,X1)
| less_than(X0,X2) ) ).
cnf(u6164,axiom,
( ~ red(n3,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u6413,axiom,
( ~ red(n2,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n5) ) ).
cnf(u1565,axiom,
less_than(n4,n9) ).
cnf(u6396,axiom,
( ~ red(n2,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u5940,axiom,
( ~ red(n4,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n5) ) ).
cnf(u1563,axiom,
less_than(n2,n9) ).
cnf(u294,axiom,
less_than(n1,n3) ).
cnf(u37,axiom,
( ~ green(X4,X5)
| ~ 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)
| ~ green(X0,X5)
| ~ green(X1,X5)
| ~ green(X2,X5)
| ~ green(X3,X5)
| ~ green(X0,X1) ) ).
cnf(u3215,axiom,
( ~ red(X3,n8)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n4)
| ~ red(X2,n4)
| ~ red(X1,n4)
| ~ red(X3,n4)
| ~ red(X0,n8)
| ~ red(X2,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u6162,axiom,
( ~ red(n3,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u6299,axiom,
( ~ green(X3,n7)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n6)
| ~ green(X2,n6)
| ~ green(X1,n6)
| ~ green(X3,n6)
| ~ green(X0,n7)
| ~ green(X2,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1697,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n10) ) ).
cnf(u54,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n5) ) ).
cnf(u5042,axiom,
~ red(n2,n4) ).
cnf(u3150,axiom,
( ~ red(X3,n5)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n3)
| ~ red(X2,n3)
| ~ red(X1,n3)
| ~ red(X3,n3)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X1,n5)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1733,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n10) ) ).
cnf(u4530,axiom,
( ~ green(X3,n10)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n6)
| ~ green(X2,n6)
| ~ green(X1,n6)
| ~ green(X3,n6)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1478,axiom,
less_than(n1,n8) ).
cnf(u1750,axiom,
less_than(n3,n11) ).
cnf(u1482,axiom,
less_than(n5,n8) ).
cnf(u1110,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n6) ) ).
cnf(u4278,axiom,
red(n6,n11) ).
cnf(u1480,axiom,
less_than(n3,n8) ).
cnf(u1108,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n6) ) ).
cnf(u5596,axiom,
( ~ red(n2,X1)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u1123,axiom,
less_than(n3,n7) ).
cnf(u1112,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n6) ) ).
cnf(u6412,axiom,
( ~ red(n2,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n6) ) ).
cnf(u6535,axiom,
( ~ red(n1,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n7) ) ).
cnf(u1655,axiom,
less_than(n1,n10) ).
cnf(u5849,axiom,
( ~ red(n3,X1)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u6163,axiom,
( ~ red(n3,X1)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(n3,X0)
| ~ red(X0,X1) ) ).
cnf(u1549,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n8) ) ).
cnf(u23,axiom,
less_than(n7,n8) ).
cnf(u21,axiom,
less_than(n9,n10) ).
cnf(u1658,axiom,
less_than(n4,n10) ).
cnf(u1547,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n8) ) ).
cnf(u6286,axiom,
( ~ green(n5,X1)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(n5,X0)
| ~ green(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA024+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.14/0.39 % Computer : n017.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Sun Sep 27 08:45:35 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.17/0.43 Running first-order model finding
% 0.17/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.71/1.27 % (2246088)Will run a generic schedule for satisfiability detection.
% 5.71/1.27 % (2246097)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4036923817:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 5.71/1.27 % (2246095)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1583225674_3000 on theBenchmark for (3000ds/0Mi)
% 5.71/1.27 % (2246100)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=668112060:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 5.71/1.27 % (2246101)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2405590194:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 5.71/1.27 % Detected minimum model sizes of [1]
% 5.71/1.27 % Detected maximum model sizes of [11]
% 5.71/1.27 % TRYING [1]
% 5.71/1.27 % (2246098)dis+10_1_sil=32000:sp=arity:random_seed=2831074194:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 5.71/1.27 % TRYING [2]
% 5.71/1.27 % TRYING [3]
% 5.71/1.27 % (2246099)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1542983401:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 5.71/1.27 % TRYING [4]
% 5.71/1.27 % (2246096)% WARNING: option uhcvi not known.
% 5.71/1.27 % (2246096)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=50185576:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 5.71/1.27 % TRYING [5]
% 5.71/1.27 % (2246098)Instruction limit reached!
% 5.71/1.27 % (2246098)------------------------------
% 5.71/1.27 % (2246098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246098)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246098)Termination reason: Instruction limit
% 5.71/1.27 % (2246098)Termination phase: Saturation
% 5.71/1.27 % (2246098)Time elapsed: 0.073 s
% 5.71/1.27 % (2246098)Peak memory usage: 11 MB
% 5.71/1.27 % (2246098)Instructions burned: 104 (million)
% 5.71/1.27 % (2246101)Instruction limit reached!
% 5.71/1.27 % (2246101)------------------------------
% 5.71/1.27 % (2246101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246101)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246101)Termination reason: Instruction limit
% 5.71/1.27 % (2246101)Termination phase: Saturation
% 5.71/1.27 % (2246101)Time elapsed: 0.080 s
% 5.71/1.27 % (2246101)Peak memory usage: 11 MB
% 5.71/1.27 % (2246101)Instructions burned: 159 (million)
% 5.71/1.27 % (2246099)Instruction limit reached!
% 5.71/1.27 % (2246099)------------------------------
% 5.71/1.27 % (2246099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246099)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246099)Termination reason: Instruction limit
% 5.71/1.27 % (2246099)Termination phase: Saturation
% 5.71/1.27 % (2246099)Time elapsed: 0.082 s
% 5.71/1.27 % (2246099)Peak memory usage: 11 MB
% 5.71/1.27 % (2246099)Instructions burned: 117 (million)
% 5.71/1.27 % (2246100)Instruction limit reached!
% 5.71/1.27 % (2246100)------------------------------
% 5.71/1.27 % (2246100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246100)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246100)Termination reason: Instruction limit
% 5.71/1.27 % (2246100)Termination phase: Saturation
% 5.71/1.27 % (2246100)Time elapsed: 0.089 s
% 5.71/1.27 % (2246100)Peak memory usage: 11 MB
% 5.71/1.27 % (2246100)Instructions burned: 131 (million)
% 5.71/1.27 % (2246120)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2848025646:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.71/1.27 % (2246122)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=475161974:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.71/1.27 % (2246124)ott-21_1_sil=16000:fs=off:random_seed=3619861631:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.71/1.27 % (2246118)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1865008293:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 5.71/1.27 % Detected minimum model sizes of [1]
% 5.71/1.27 % Detected maximum model sizes of [11]
% 5.71/1.27 % TRYING [1]
% 5.71/1.27 % TRYING [2]
% 5.71/1.27 % TRYING [3]
% 5.71/1.27 % TRYING [4]
% 5.71/1.27 % (2246120)Instruction limit reached!
% 5.71/1.27 % (2246120)------------------------------
% 5.71/1.27 % (2246120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246120)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246120)Termination reason: Instruction limit
% 5.71/1.27 % (2246120)Termination phase: Saturation
% 5.71/1.27 % (2246120)Time elapsed: 0.077 s
% 5.71/1.27 % (2246120)Peak memory usage: 12 MB
% 5.71/1.27 % (2246120)Instructions burned: 133 (million)
% 5.71/1.27 % TRYING [6]
% 5.71/1.27 % TRYING [5]
% 5.71/1.27 % (2246135)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1585155080:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.71/1.27 % (2246124)Instruction limit reached!
% 5.71/1.27 % (2246124)------------------------------
% 5.71/1.27 % (2246124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246124)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246124)Termination reason: Instruction limit
% 5.71/1.27 % (2246124)Termination phase: Saturation
% 5.71/1.27 % (2246124)Time elapsed: 0.150 s
% 5.71/1.27 % (2246124)Peak memory usage: 12 MB
% 5.71/1.27 % (2246124)Instructions burned: 180 (million)
% 5.71/1.27 % (2246142)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1049878065:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 5.71/1.27 % Detected minimum model sizes of [1]
% 5.71/1.27 % Detected maximum model sizes of [11]
% 5.71/1.27 % TRYING [1]
% 5.71/1.27 % TRYING [2]
% 5.71/1.27 % TRYING [3]
% 5.71/1.27 % TRYING [4]
% 5.71/1.27 % TRYING [6]
% 5.71/1.27 % TRYING [5]
% 5.71/1.27 % TRYING [6]
% 5.71/1.27 % (2246135)Instruction limit reached!
% 5.71/1.27 % (2246135)------------------------------
% 5.71/1.27 % (2246135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246135)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246135)Termination reason: Instruction limit
% 5.71/1.27 % (2246135)Termination phase: Saturation
% 5.71/1.27 % (2246135)Time elapsed: 0.319 s
% 5.71/1.27 % (2246135)Peak memory usage: 12 MB
% 5.71/1.27 % (2246135)Instructions burned: 477 (million)
% 5.71/1.27 % (2246118)Instruction limit reached!
% 5.71/1.27 % (2246118)------------------------------
% 5.71/1.27 % (2246118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246118)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246118)Termination reason: Instruction limit
% 5.71/1.27 % (2246118)Termination phase: Finite model building constraint generation
% 5.71/1.27 % (2246118)Time elapsed: 0.423 s
% 5.71/1.27 % (2246118)Peak memory usage: 21 MB
% 5.71/1.27 % (2246118)Instructions burned: 715 (million)
% 5.71/1.27 % (2246165)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2100003677:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 5.71/1.27 % (2246167)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=142963651:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 5.71/1.27 % Detected minimum model sizes of [1]
% 5.71/1.27 % Detected maximum model sizes of [11]
% 5.71/1.27 % fmb_start_size (= 14) larger than a detected sort maximum size!
% 5.71/1.27 % (2246167)Refutation not found, incomplete strategy
% 5.71/1.27 % (2246167)------------------------------
% 5.71/1.27 % (2246167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246167)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246167)Termination reason: Refutation not found, incomplete strategy
% 5.71/1.27 % (2246167)Time elapsed: 0.001 s
% 5.71/1.27 % (2246167)Peak memory usage: 10 MB
% 5.71/1.27 % (2246167)Instructions burned: 1 (million)
% 5.71/1.27 % (2246122)Instruction limit reached!
% 5.71/1.27 % (2246122)------------------------------
% 5.71/1.27 % (2246122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246122)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246122)Termination reason: Instruction limit
% 5.71/1.27 % (2246122)Termination phase: Saturation
% 5.71/1.27 % (2246122)Time elapsed: 0.475 s
% 5.71/1.27 % (2246122)Peak memory usage: 13 MB
% 5.71/1.27 % (2246122)Instructions burned: 685 (million)
% 5.71/1.27 % (2246167)------------------------------
% 5.71/1.27 % (2246167)------------------------------
% 5.71/1.27 % (2246173)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2966977402:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 5.71/1.27 % (2246172)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1927234041:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 5.71/1.27 % TRYING [7]
% 5.71/1.27 % (2246142)Instruction limit reached!
% 5.71/1.27 % (2246142)------------------------------
% 5.71/1.27 % (2246142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.27 % (2246142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.27 % (2246142)CaDiCaL version: 2.1.3
% 5.71/1.27 % (2246142)Termination reason: Instruction limit
% 5.71/1.27 % (2246142)Termination phase: Finite model building constraint generation
% 5.71/1.27 % (2246142)Time elapsed: 0.452 s
% 5.71/1.27 % (2246142)Peak memory usage: 24 MB
% 5.71/1.27 % (2246142)Instructions burned: 866 (million)
% 5.71/1.27 % (2246097) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2246088-2246097"...
% 5.71/1.27 % (2246097)...printing done.
% 5.71/1.27 % SZS status CounterSatisfiable for theBenchmark
% 5.71/1.27 % SZS output start Saturation.
% See solution above
% 5.71/1.28 % SZS output start Definitions and Model Updates.
% 5.71/1.28 % SZS output end Definitions and Model Updates.
% 5.71/1.28 % (2246097)------------------------------
% 5.71/1.28 % (2246097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.71/1.28 % (2246097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.71/1.28 % (2246097)CaDiCaL version: 2.1.3
% 5.71/1.28 % (2246097)Termination reason: Satisfiable
% 5.71/1.28 % (2246097)Time elapsed: 0.800 s
% 5.71/1.28 % (2246097)Peak memory usage: 15 MB
% 5.71/1.28 % (2246097)Instructions burned: 1123 (million)
% 5.71/1.28 % (2246088)Success in time 0.832 s
% 5.71/1.28 % Vampire exiting
%------------------------------------------------------------------------------