%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRA025+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 : n016.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.97s 1.43s
% Output : Saturation 5.97s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u120,axiom,
~ less_than(X0,n1) ).
cnf(u200,axiom,
~ green(X0,n1) ).
cnf(u239,axiom,
~ red(X0,n1) ).
cnf(u242,axiom,
~ red(X0,n2) ).
cnf(u325,axiom,
~ red(X0,n3) ).
cnf(u347,axiom,
~ red(n2,n2) ).
cnf(u405,axiom,
~ green(n2,n2) ).
cnf(u408,axiom,
( ~ green(X2,n3)
| ~ green(X2,X0)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X2,n2)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u522,axiom,
red(n4,n5) ).
cnf(u525,axiom,
~ green(n4,n5) ).
cnf(u530,axiom,
~ green(X0,n4) ).
cnf(u581,axiom,
~ red(n5,n6) ).
cnf(u586,axiom,
green(n5,n6) ).
cnf(u592,axiom,
red(n6,n7) ).
cnf(u595,axiom,
~ green(n6,n7) ).
cnf(u601,axiom,
~ red(X0,n6) ).
cnf(u631,axiom,
~ red(n4,n4) ).
cnf(u634,axiom,
( ~ red(X2,n5)
| ~ red(X2,X0)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X2,n4)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u645,axiom,
~ green(n4,n4) ).
cnf(u659,axiom,
~ green(n5,n5) ).
cnf(u662,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(u683,axiom,
~ red(n6,n6) ).
cnf(u696,axiom,
~ green(n3,n3) ).
cnf(u704,axiom,
red(n7,n8) ).
cnf(u707,axiom,
~ green(n7,n8) ).
cnf(u723,axiom,
red(n8,n9) ).
cnf(u726,axiom,
~ green(n8,n9) ).
cnf(u732,axiom,
~ red(n9,n10) ).
cnf(u737,axiom,
green(n9,n10) ).
cnf(u745,axiom,
~ red(X0,n10) ).
cnf(u758,axiom,
~ green(X0,n8) ).
cnf(u774,axiom,
~ red(n7,n7) ).
cnf(u785,axiom,
~ red(n8,n8) ).
cnf(u788,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(u792,axiom,
~ red(n10,n11) ).
cnf(u797,axiom,
green(n10,n11) ).
cnf(u803,axiom,
red(n11,n12) ).
cnf(u806,axiom,
~ green(n11,n12) ).
cnf(u842,axiom,
~ red(n9,n9) ).
cnf(u860,axiom,
~ green(n6,n6) ).
cnf(u872,axiom,
~ green(n7,n7) ).
cnf(u884,axiom,
~ green(n8,n8) ).
cnf(u887,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(u896,axiom,
~ green(n9,n9) ).
cnf(u910,axiom,
~ green(n10,n10) ).
cnf(u913,axiom,
( ~ green(X2,n11)
| ~ green(X2,X0)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u937,axiom,
~ red(n11,n11) ).
cnf(u945,axiom,
red(n12,n13) ).
cnf(u948,axiom,
~ green(n12,n13) ).
cnf(u964,axiom,
red(n13,n14) ).
cnf(u967,axiom,
~ green(n13,n14) ).
cnf(u1000,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(n5,X0)
| ~ green(X1,n5) ) ).
cnf(u1019,axiom,
~ red(n5,n5) ).
cnf(u1163,axiom,
~ green(n11,n11) ).
cnf(u1166,axiom,
( ~ green(X2,n12)
| ~ green(X2,X0)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X2,n11)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u1173,axiom,
~ red(n12,n12) ).
cnf(u1269,axiom,
~ green(n12,n5) ).
cnf(u1273,axiom,
~ green(n12,n6) ).
cnf(u1301,axiom,
~ green(X0,n14) ).
cnf(u1322,axiom,
~ green(n12,n12) ).
cnf(u1325,axiom,
( ~ green(X2,n13)
| ~ green(X2,X0)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X2,n12)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u1330,axiom,
~ green(n12,X1) ).
cnf(u1333,axiom,
( ~ green(n12,X1)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n12,X0)
| ~ green(X1,n12) ) ).
cnf(u1355,axiom,
~ green(n13,n13) ).
cnf(u1358,axiom,
( ~ green(X2,n14)
| ~ green(X2,X0)
| ~ green(X1,n14)
| ~ green(X0,n14)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X2,n13)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u1476,axiom,
~ green(n13,X1) ).
cnf(u1493,axiom,
( ~ green(n12,X0)
| ~ green(X0,n12)
| ~ green(X0,n13) ) ).
cnf(u1514,axiom,
~ red(n13,n13) ).
cnf(u1517,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X2,n13)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u1524,axiom,
red(n3,n4) ).
cnf(u1527,axiom,
~ green(n3,n4) ).
cnf(u1622,axiom,
green(n5,n7) ).
cnf(u1626,axiom,
( ~ green(X2,n8)
| ~ green(X2,X0)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n7) ) ).
cnf(u1637,axiom,
~ green(n7,n5) ).
cnf(u1651,axiom,
~ green(n4,n7) ).
cnf(u1657,axiom,
( ~ green(n4,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n7)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(n4,X0)
| ~ green(X1,n5)
| ~ green(X1,n7) ) ).
cnf(u1797,axiom,
~ green(n9,n13) ).
cnf(u1800,axiom,
green(n9,n12) ).
cnf(u1811,axiom,
~ green(n9,n8) ).
cnf(u1819,axiom,
~ green(n9,n5) ).
cnf(u1823,axiom,
~ green(n9,n6) ).
cnf(u2010,axiom,
green(n10,n13) ).
cnf(u2015,axiom,
~ green(n10,n12) ).
cnf(u2020,axiom,
~ green(n10,n5) ).
cnf(u2024,axiom,
~ green(n10,n6) ).
cnf(u2091,axiom,
~ red(n10,n10) ).
cnf(u2215,axiom,
~ red(n11,n10) ).
cnf(u2230,axiom,
~ green(n11,X1) ).
cnf(u2233,axiom,
( ~ green(n11,X1)
| ~ green(X0,X1)
| ~ green(X0,n11)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n11,X0)
| ~ green(X1,n11) ) ).
cnf(u2444,axiom,
~ red(n12,n11) ).
cnf(u2609,axiom,
( ~ green(n10,X1)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n10,X0)
| ~ green(X1,n12) ) ).
cnf(u2696,axiom,
~ green(n14,n8) ).
cnf(u2700,axiom,
red(n8,n14) ).
cnf(u2721,axiom,
~ green(n14,n5) ).
cnf(u2728,axiom,
( ~ green(n5,X0)
| ~ green(X0,n14)
| ~ green(X0,n6)
| ~ green(X0,n5) ) ).
cnf(u2732,axiom,
red(n5,n14) ).
cnf(u2824,axiom,
~ green(n14,n13) ).
cnf(u2836,axiom,
~ green(n11,n13) ).
cnf(u2867,axiom,
~ green(n5,n13) ).
cnf(u2870,axiom,
( ~ green(n5,X0)
| ~ green(X0,X1)
| ~ green(X0,n13)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(n5,X1)
| ~ green(X1,n13) ) ).
cnf(u2876,axiom,
green(n5,n10) ).
cnf(u2931,axiom,
~ red(n3,n3) ).
cnf(u2934,axiom,
( ~ red(X2,n4)
| ~ red(X2,X0)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n3)
| ~ red(X0,n3)
| ~ red(X2,n3)
| ~ red(X2,X1)
| ~ red(X0,X1) ) ).
cnf(u3058,axiom,
~ red(n4,n2) ).
cnf(u3164,axiom,
~ red(n9,n12) ).
cnf(u3167,axiom,
( ~ red(X2,n13)
| ~ red(X2,X0)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n12) ) ).
cnf(u3175,axiom,
~ red(n12,n9) ).
cnf(u3245,axiom,
( ~ green(X2,n13)
| ~ green(X2,X0)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X2,X1)
| ~ green(X0,X1) ) ).
cnf(u3250,axiom,
( ~ green(n10,X1)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n10,X0)
| ~ green(X1,n10) ) ).
cnf(u3320,axiom,
~ green(n10,n9) ).
cnf(u3344,axiom,
~ green(n11,n10) ).
cnf(u3356,axiom,
red(n3,n5) ).
cnf(u3359,axiom,
~ green(n3,n5) ).
cnf(u3382,axiom,
red(n6,n8) ).
cnf(u3385,axiom,
~ green(n6,n8) ).
cnf(u3392,axiom,
( ~ red(n3,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(n3,X0)
| ~ red(X1,n4) ) ).
cnf(u3451,axiom,
~ red(n8,n10) ).
cnf(u3456,axiom,
green(n8,n10) ).
cnf(u3516,axiom,
~ red(n11,n9) ).
cnf(u3519,axiom,
( ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n12)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(n11,X0)
| ~ red(X1,n9)
| ~ red(X1,n12) ) ).
cnf(u3532,axiom,
( ~ red(X2,n13)
| ~ red(X2,X0)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n9) ) ).
cnf(u3596,axiom,
~ red(n13,n12) ).
cnf(u3600,axiom,
~ red(n13,n9) ).
cnf(u3692,axiom,
~ green(n13,n10) ).
cnf(u3721,axiom,
~ red(n14,n12) ).
cnf(u3725,axiom,
~ red(n14,n9) ).
cnf(u3729,axiom,
~ red(n14,n13) ).
cnf(u3777,axiom,
~ red(n6,n4) ).
cnf(u3781,axiom,
~ red(n6,n5) ).
cnf(u3800,axiom,
red(n5,n8) ).
cnf(u3803,axiom,
~ green(n5,n8) ).
cnf(u3814,axiom,
~ red(n7,n5) ).
cnf(u3817,axiom,
( ~ red(X2,n8)
| ~ red(X2,X0)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n5) ) ).
cnf(u3834,axiom,
~ red(n7,n6) ).
cnf(u3837,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(u3874,axiom,
~ red(n2,n3) ).
cnf(u3877,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n3)
| ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(n2,X0)
| ~ red(X1,n3) ) ).
cnf(u3891,axiom,
~ green(n7,n6) ).
cnf(u3902,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(n3,X0)
| ~ green(X1,n5) ) ).
cnf(u3911,axiom,
~ green(n6,n5) ).
cnf(u3917,axiom,
( ~ green(n6,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n7)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(n6,X0)
| ~ green(X1,n5)
| ~ green(X1,n7) ) ).
cnf(u3926,axiom,
( ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n6,X0)
| ~ red(X1,n8) ) ).
cnf(u4002,axiom,
red(n2,n5) ).
cnf(u4005,axiom,
~ green(n2,n5) ).
cnf(u4056,axiom,
green(n5,n12) ).
cnf(u4075,axiom,
( ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n9,X0)
| ~ red(X1,n10) ) ).
cnf(u4096,axiom,
green(n9,n11) ).
cnf(u4100,axiom,
( ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(X0,n11)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n9,X0)
| ~ green(X1,n11) ) ).
cnf(u4112,axiom,
~ red(n7,n9) ).
cnf(u4115,axiom,
( ~ red(n6,X0)
| ~ red(X0,n7)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u4130,axiom,
~ red(n13,n5) ).
cnf(u4133,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X2,n13)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n5) ) ).
cnf(u4140,axiom,
red(n5,n13) ).
cnf(u4194,axiom,
~ red(n9,n11) ).
cnf(u4223,axiom,
~ red(n12,n5) ).
cnf(u4226,axiom,
( ~ red(n12,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n5)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n12,X0)
| ~ red(X1,n13)
| ~ red(X1,n5) ) ).
cnf(u4230,axiom,
( ~ green(n4,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(n4,X0)
| ~ green(X1,n5) ) ).
cnf(u4240,axiom,
~ red(n14,n5) ).
cnf(u4244,axiom,
~ red(n14,n14) ).
cnf(u4258,axiom,
~ red(n5,n12) ).
cnf(u4268,axiom,
~ red(n8,n6) ).
cnf(u4272,axiom,
~ red(n8,n7) ).
cnf(u4279,axiom,
( ~ red(X2,n8)
| ~ red(X2,X0)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n5) ) ).
cnf(u4283,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X2,n12)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n5) ) ).
cnf(u4291,axiom,
~ red(n4,n6) ).
cnf(u4294,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(u4344,axiom,
~ red(n7,n10) ).
cnf(u4349,axiom,
green(n7,n10) ).
cnf(u4358,axiom,
~ red(n10,n8) ).
cnf(u4361,axiom,
( ~ red(n7,X0)
| ~ red(X0,n10)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u4365,axiom,
~ red(n10,n9) ).
cnf(u4377,axiom,
~ red(n8,n11) ).
cnf(u4382,axiom,
green(n8,n11) ).
cnf(u4409,axiom,
( ~ red(n10,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n12)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(n10,X0)
| ~ red(X1,n9)
| ~ red(X1,n12) ) ).
cnf(u4417,axiom,
( ~ green(n9,X0)
| ~ green(X0,n12)
| ~ green(X0,n11) ) ).
cnf(u4426,axiom,
( ~ red(n10,X1)
| ~ red(n10,X0)
| ~ red(X0,n11)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X1,n12) ) ).
cnf(u4561,axiom,
~ red(n11,n5) ).
cnf(u4564,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n5) ) ).
cnf(u4571,axiom,
~ green(n13,n12) ).
cnf(u4578,axiom,
( ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n9,X0)
| ~ green(X1,n10) ) ).
cnf(u4640,axiom,
~ red(n1,n5) ).
cnf(u4645,axiom,
green(n1,n5) ).
cnf(u4655,axiom,
( ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(X0,n10)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n8,X0)
| ~ red(X1,n10) ) ).
cnf(u4663,axiom,
( ~ red(n8,X0)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n10) ) ).
cnf(u4733,axiom,
~ red(n14,n8) ).
cnf(u4742,axiom,
~ red(n14,n10) ).
cnf(u4746,axiom,
~ red(n14,n11) ).
cnf(u4754,axiom,
~ red(n14,n4) ).
cnf(u4775,axiom,
~ red(n12,n10) ).
cnf(u4809,axiom,
red(n10,n12) ).
cnf(u4813,axiom,
( ~ red(X2,n13)
| ~ red(X2,X0)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X2,n10)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n12) ) ).
cnf(u4841,axiom,
~ red(n9,n8) ).
cnf(u4848,axiom,
~ red(n9,n7) ).
cnf(u4882,axiom,
~ red(n3,n7) ).
cnf(u4887,axiom,
green(n3,n7) ).
cnf(u4942,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n4)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X1,n4)
| ~ red(X1,n6) ) ).
cnf(u4946,axiom,
~ red(n5,n4) ).
cnf(u4967,axiom,
~ red(n7,n4) ).
cnf(u5058,axiom,
~ red(n3,n6) ).
cnf(u5072,axiom,
( ~ red(X2,n10)
| ~ red(X2,X0)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X2,n8)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n7) ) ).
cnf(u5076,axiom,
( ~ red(X2,n10)
| ~ red(X2,X0)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n7) ) ).
cnf(u5146,axiom,
red(n4,n8) ).
cnf(u5149,axiom,
~ green(n4,n8) ).
cnf(u5250,axiom,
red(n7,n11) ).
cnf(u5253,axiom,
~ green(n7,n11) ).
cnf(u5290,axiom,
~ red(n8,n12) ).
cnf(u5295,axiom,
green(n8,n12) ).
cnf(u5307,axiom,
( ~ green(n8,X1)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(n8,X0)
| ~ green(X1,n10) ) ).
cnf(u5356,axiom,
~ green(n11,n9) ).
cnf(u5359,axiom,
( ~ green(n7,X0)
| ~ green(X0,n11)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u5377,axiom,
~ green(n11,n8) ).
cnf(u5396,axiom,
green(n7,n9) ).
cnf(u5400,axiom,
( ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n7,X0)
| ~ green(X1,n9) ) ).
cnf(u5410,axiom,
( ~ red(X2,n8)
| ~ red(X2,X0)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n4) ) ).
cnf(u5426,axiom,
~ red(n5,n7) ).
cnf(u5537,axiom,
red(n6,n9) ).
cnf(u5540,axiom,
~ green(n6,n9) ).
cnf(u5552,axiom,
~ red(n5,n9) ).
cnf(u5557,axiom,
green(n5,n9) ).
cnf(u5589,axiom,
~ red(n6,n10) ).
cnf(u5594,axiom,
green(n6,n10) ).
cnf(u5613,axiom,
( ~ green(n6,X1)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n6,X0)
| ~ green(X1,n9) ) ).
cnf(u5686,axiom,
~ red(n10,n5) ).
cnf(u5700,axiom,
~ red(n5,n10) ).
cnf(u5703,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n10) ) ).
cnf(u5740,axiom,
~ red(n3,n2) ).
cnf(u5744,axiom,
green(n1,n2) ).
cnf(u5748,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n2)
| ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(n1,X0)
| ~ green(X1,n2) ) ).
cnf(u5778,axiom,
~ red(n8,n4) ).
cnf(u5782,axiom,
~ red(n8,n5) ).
cnf(u5852,axiom,
~ green(n4,n3) ).
cnf(u5855,axiom,
( ~ green(X0,X1)
| ~ green(X2,X0)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X2,n4)
| ~ green(X2,X1)
| ~ green(X2,n5)
| ~ green(X2,n3) ) ).
cnf(u5859,axiom,
red(n1,n4) ).
cnf(u5863,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(n1,X0)
| ~ red(X1,n4) ) ).
cnf(u5867,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(n1,X0)
| ~ green(X1,n5) ) ).
cnf(u5890,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n5,X0)
| ~ red(X1,n8) ) ).
cnf(u5902,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n6)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X1,n6)
| ~ red(X1,n7) ) ).
cnf(u5916,axiom,
( ~ red(X2,n8)
| ~ red(X2,X0)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ 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(u5949,axiom,
~ green(n8,n5) ).
cnf(u5953,axiom,
~ green(n8,n6) ).
cnf(u6055,axiom,
~ red(n2,n6) ).
cnf(u6060,axiom,
green(n2,n6) ).
cnf(u6092,axiom,
red(n2,n7) ).
cnf(u6095,axiom,
~ green(n2,n7) ).
cnf(u6150,axiom,
red(n3,n8) ).
cnf(u6153,axiom,
~ green(n3,n8) ).
cnf(u6180,axiom,
~ red(n4,n9) ).
cnf(u6185,axiom,
green(n4,n9) ).
cnf(u6255,axiom,
red(n6,n11) ).
cnf(u6258,axiom,
~ green(n6,n11) ).
cnf(u6338,axiom,
~ red(n7,n12) ).
cnf(u6343,axiom,
green(n7,n12) ).
cnf(u6363,axiom,
~ red(n12,n8) ).
cnf(u6375,axiom,
~ red(n11,n8) ).
cnf(u6382,axiom,
~ red(n11,n7) ).
cnf(u6395,axiom,
( ~ red(X2,n12)
| ~ red(X2,X0)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n7) ) ).
cnf(u6399,axiom,
~ red(n8,n13) ).
cnf(u6404,axiom,
green(n8,n13) ).
cnf(u6427,axiom,
~ red(n13,n10) ).
cnf(u6431,axiom,
~ red(n13,n11) ).
cnf(u6504,axiom,
~ red(n9,n5) ).
cnf(u6535,axiom,
~ red(n1,n7) ).
cnf(u6540,axiom,
green(n1,n7) ).
cnf(u6552,axiom,
red(n2,n8) ).
cnf(u6555,axiom,
~ green(n2,n8) ).
cnf(u6590,axiom,
~ red(n5,n3) ).
cnf(u6598,axiom,
~ red(n7,n3) ).
cnf(u6607,axiom,
~ red(n4,n10) ).
cnf(u6612,axiom,
green(n4,n10) ).
cnf(u6668,axiom,
~ red(n5,n11) ).
cnf(u6673,axiom,
green(n5,n11) ).
cnf(u6752,axiom,
red(n7,n13) ).
cnf(u6755,axiom,
~ green(n7,n13) ).
cnf(u6809,axiom,
~ red(n12,n7) ).
cnf(u6825,axiom,
~ red(n10,n7) ).
cnf(u6944,axiom,
~ red(n13,n8) ).
cnf(u6979,axiom,
red(n1,n8) ).
cnf(u6982,axiom,
~ green(n1,n8) ).
cnf(u7001,axiom,
( ~ red(n3,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n3,X0)
| ~ red(X1,n8) ) ).
cnf(u7008,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n7)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n5,X0)
| ~ red(X1,n8)
| ~ red(X1,n7) ) ).
cnf(u7028,axiom,
~ green(n4,n2) ).
cnf(u7031,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(u7038,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(u7048,axiom,
~ green(n9,n7) ).
cnf(u7067,axiom,
( ~ red(n8,X0)
| ~ red(X0,n12)
| ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(X0,n9) ) ).
cnf(u7076,axiom,
( ~ red(n6,X0)
| ~ red(X0,n11)
| ~ red(X0,n8)
| ~ red(X0,n12)
| ~ red(X0,n7) ) ).
cnf(u7086,axiom,
( ~ red(n7,X1)
| ~ red(n7,X0)
| ~ red(X0,n8)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n8)
| ~ red(X1,n11) ) ).
cnf(u7096,axiom,
( ~ red(n9,X1)
| ~ red(n9,X0)
| ~ red(X0,n11)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X1,n12) ) ).
cnf(u7105,axiom,
( ~ red(n7,X1)
| ~ red(n7,X0)
| ~ red(X0,n11)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X1,n12) ) ).
cnf(u7115,axiom,
( ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X0,n9)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(n7,X0)
| ~ red(X1,n11)
| ~ red(X1,n9) ) ).
cnf(u7135,axiom,
( ~ red(X2,n12)
| ~ red(X2,X0)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n11) ) ).
cnf(u7189,axiom,
( ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n7,X0)
| ~ red(X1,n9)
| ~ red(X1,n11) ) ).
cnf(u7211,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n11) ) ).
cnf(u7235,axiom,
( ~ red(n1,X0)
| ~ red(X0,n2)
| ~ red(X0,n4)
| ~ red(X0,n3) ) ).
cnf(u7238,axiom,
red(n2,n4) ).
cnf(u7244,axiom,
~ green(n6,n2) ).
cnf(u7248,axiom,
~ green(n6,n3) ).
cnf(u7263,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ 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(u7271,axiom,
( ~ red(X2,n13)
| ~ red(X2,X0)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n11) ) ).
cnf(u7301,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n8)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X0,X1)
| ~ red(X0,n10)
| ~ red(X1,n8)
| ~ red(X1,n10) ) ).
cnf(u7520,axiom,
( ~ green(n4,X0)
| ~ green(X0,n6)
| ~ green(X0,n8)
| ~ green(X0,n7)
| ~ green(X0,n5) ) ).
cnf(u7528,axiom,
~ green(n3,n2) ).
cnf(u7545,axiom,
~ green(n5,n2) ).
cnf(u7548,axiom,
( ~ green(X2,n7)
| ~ green(X2,X0)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n2) ) ).
cnf(u7618,axiom,
~ red(n1,n3) ).
cnf(u7621,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n3)
| ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(n1,X0)
| ~ red(X1,n3) ) ).
cnf(u7794,axiom,
~ green(n11,n5) ).
cnf(u7872,axiom,
~ green(n7,n2) ).
cnf(u7911,axiom,
~ green(n8,n7) ).
cnf(u7914,axiom,
( ~ green(n1,X0)
| ~ green(X0,n6)
| ~ green(X0,n2)
| ~ green(X0,n7)
| ~ green(X0,n8) ) ).
cnf(u7918,axiom,
~ green(n8,n2) ).
cnf(u7968,axiom,
~ red(n3,n9) ).
cnf(u7973,axiom,
green(n3,n9) ).
cnf(u8015,axiom,
red(n2,n9) ).
cnf(u8018,axiom,
~ green(n2,n9) ).
cnf(u8081,axiom,
~ red(n9,n3) ).
cnf(u8085,axiom,
~ red(n9,n4) ).
cnf(u8093,axiom,
red(n6,n12) ).
cnf(u8096,axiom,
~ green(n6,n12) ).
cnf(u8114,axiom,
~ red(n3,n10) ).
cnf(u8119,axiom,
green(n3,n10) ).
cnf(u8196,axiom,
~ red(n6,n13) ).
cnf(u8201,axiom,
green(n6,n13) ).
cnf(u8329,axiom,
( ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n7,X0)
| ~ green(X1,n12) ) ).
cnf(u8340,axiom,
red(n9,n13) ).
cnf(u8344,axiom,
( ~ red(n7,X0)
| ~ red(X0,n12)
| ~ red(X0,n9)
| ~ red(X0,n13)
| ~ red(X0,n11) ) ).
cnf(u8364,axiom,
( ~ red(n9,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n9,X0)
| ~ red(X1,n13) ) ).
cnf(u8420,axiom,
red(n1,n9) ).
cnf(u8436,axiom,
~ red(n2,n10) ).
cnf(u8441,axiom,
green(n2,n10) ).
cnf(u8455,axiom,
~ red(n10,n3) ).
cnf(u8459,axiom,
~ red(n10,n4) ).
cnf(u8462,axiom,
( ~ red(n2,X0)
| ~ red(X0,n10)
| ~ red(X0,n4)
| ~ red(X0,n3) ) ).
cnf(u8475,axiom,
~ green(n7,n3) ).
cnf(u8504,axiom,
~ green(n5,n3) ).
cnf(u8537,axiom,
green(n2,n3) ).
cnf(u8564,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n2,X0)
| ~ red(X1,n8) ) ).
cnf(u8572,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n7)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n2,X0)
| ~ red(X1,n9)
| ~ red(X1,n7) ) ).
cnf(u8581,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n2,X0)
| ~ red(X1,n7)
| ~ red(X1,n6) ) ).
cnf(u8589,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n7)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n2,X0)
| ~ red(X1,n8)
| ~ red(X1,n7) ) ).
cnf(u8597,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n5)
| ~ red(X0,n8)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(n2,X0)
| ~ red(X1,n5)
| ~ red(X1,n8) ) ).
cnf(u8615,axiom,
~ red(n9,n6) ).
cnf(u8627,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n11)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n5,X0)
| ~ green(X1,n11) ) ).
cnf(u8636,axiom,
( ~ red(n8,X0)
| ~ red(X0,n12)
| ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(X0,n10) ) ).
cnf(u8645,axiom,
( ~ red(n10,X1)
| ~ red(n10,X0)
| ~ red(X0,n11)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X1,n12) ) ).
cnf(u8662,axiom,
( ~ red(n10,X1)
| ~ red(n10,X0)
| ~ red(X0,n6)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n6)
| ~ red(X1,n12) ) ).
cnf(u8666,axiom,
~ red(n10,n6) ).
cnf(u8695,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X2,n10)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n12) ) ).
cnf(u8717,axiom,
~ red(n8,n3) ).
cnf(u9061,axiom,
~ red(n11,n4) ).
cnf(u9101,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n3)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X1,n3)
| ~ red(X1,n6) ) ).
cnf(u9105,axiom,
~ red(n4,n3) ).
cnf(u9148,axiom,
red(n4,n12) ).
cnf(u9151,axiom,
~ green(n4,n12) ).
cnf(u9173,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n3)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n3)
| ~ green(X1,n7) ) ).
cnf(u9176,axiom,
green(n1,n3) ).
cnf(u9267,axiom,
( ~ green(n5,X0)
| ~ green(X0,n7)
| ~ green(X0,n13)
| ~ green(X0,n12) ) ).
cnf(u9302,axiom,
( ~ red(n8,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n8,X0)
| ~ red(X1,n13) ) ).
cnf(u9339,axiom,
( ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n7,X0)
| ~ red(X1,n13) ) ).
cnf(u9493,axiom,
( ~ red(n2,X0)
| ~ red(X0,n3)
| ~ red(X0,n5)
| ~ red(X0,n4) ) ).
cnf(u9548,axiom,
~ green(n4,n11) ).
cnf(u9575,axiom,
( ~ red(n2,X0)
| ~ red(X0,n4)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u9596,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n4,X0)
| ~ red(X1,n8) ) ).
cnf(u9605,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n7)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(n3,X0)
| ~ green(X1,n5)
| ~ green(X1,n7) ) ).
cnf(u9617,axiom,
( ~ green(n3,X1)
| ~ green(n3,X0)
| ~ green(X0,n6)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X1,n7) ) ).
cnf(u9620,axiom,
green(n3,n6) ).
cnf(u9629,axiom,
red(n4,n7) ).
cnf(u9637,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n6)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X1,n7) ) ).
cnf(u9640,axiom,
green(n1,n6) ).
cnf(u9653,axiom,
( ~ green(n1,X0)
| ~ green(X0,n7)
| ~ green(X0,n3)
| ~ green(X0,n8)
| ~ green(X0,n6) ) ).
cnf(u9676,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n2)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(n1,X0)
| ~ green(X1,n5)
| ~ green(X1,n2) ) ).
cnf(u9687,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n1,X0)
| ~ red(X1,n8) ) ).
cnf(u9694,axiom,
~ red(n1,n6) ).
cnf(u9697,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n1,X0)
| ~ red(X1,n7)
| ~ red(X1,n6) ) ).
cnf(u9707,axiom,
( ~ red(n1,X1)
| ~ red(n1,X0)
| ~ red(X0,n2)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X1,n2)
| ~ red(X1,n7) ) ).
cnf(u9711,axiom,
~ red(n1,n2) ).
cnf(u9749,axiom,
~ red(n8,n2) ).
cnf(u9763,axiom,
green(n4,n6) ).
cnf(u9787,axiom,
( ~ red(n2,X0)
| ~ red(X0,n7)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u9797,axiom,
( ~ red(n2,X0)
| ~ red(X0,n3)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u9801,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(n2,X0)
| ~ red(X1,n4) ) ).
cnf(u9812,axiom,
( ~ red(n7,X1)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(n7,X0)
| ~ red(X1,n8) ) ).
cnf(u9824,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n6)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(n2,X0)
| ~ red(X1,n4)
| ~ red(X1,n6) ) ).
cnf(u9836,axiom,
( ~ red(n7,X1)
| ~ red(n7,X0)
| ~ red(X0,n8)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n8)
| ~ red(X1,n11) ) ).
cnf(u9856,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n8) ) ).
cnf(u9867,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X0,n8)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n5,X0)
| ~ red(X1,n6)
| ~ red(X1,n8) ) ).
cnf(u9877,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n8) ) ).
cnf(u9889,axiom,
~ red(n13,n7) ).
cnf(u9896,axiom,
( ~ red(X2,n13)
| ~ red(X2,X0)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n8) ) ).
cnf(u9961,axiom,
red(n11,n13) ).
cnf(u9965,axiom,
( ~ red(n10,X0)
| ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u9974,axiom,
( ~ red(n9,X0)
| ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u9981,axiom,
( ~ red(n8,X0)
| ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u9998,axiom,
( ~ green(n7,X0)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X0,n12) ) ).
cnf(u10005,axiom,
~ red(n11,n6) ).
cnf(u10012,axiom,
( ~ red(n11,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n11,X0)
| ~ red(X1,n13) ) ).
cnf(u10051,axiom,
( ~ red(X2,n6)
| ~ red(X2,X0)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n2)
| ~ red(X0,n2)
| ~ red(X2,n2)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n4) ) ).
cnf(u10105,axiom,
( ~ green(n9,X1)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n9,X0)
| ~ green(X1,n12) ) ).
cnf(u10112,axiom,
( ~ green(n9,X0)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X0,n12) ) ).
cnf(u10264,axiom,
~ red(n6,n3) ).
cnf(u10369,axiom,
~ green(n10,n8) ).
cnf(u10372,axiom,
( ~ green(X2,n12)
| ~ green(X2,X0)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n8) ) ).
cnf(u10472,axiom,
( ~ green(n3,X1)
| ~ green(n3,X0)
| ~ green(X0,n6)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X1,n7) ) ).
cnf(u10502,axiom,
red(n4,n11) ).
cnf(u10506,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n5)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n5)
| ~ red(X1,n11) ) ).
cnf(u10521,axiom,
( ~ red(X2,n12)
| ~ red(X2,X0)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n4) ) ).
cnf(u10565,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n6)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(n1,X0)
| ~ red(X1,n4)
| ~ red(X1,n6) ) ).
cnf(u10577,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n6)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n1,X0)
| ~ red(X1,n4)
| ~ red(X1,n6) ) ).
cnf(u10589,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X0,n5)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n1,X0)
| ~ red(X1,n6)
| ~ red(X1,n5) ) ).
cnf(u10643,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n6)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X1,n11) ) ).
cnf(u10762,axiom,
~ red(n3,n11) ).
cnf(u10767,axiom,
green(n3,n11) ).
cnf(u10842,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n3)
| ~ red(X0,n3)
| ~ red(X1,n10)
| ~ red(X0,n10)
| ~ red(X2,n10)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n3) ) ).
cnf(u10854,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n8)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(n3,X0)
| ~ green(X1,n8) ) ).
cnf(u10870,axiom,
( ~ green(n6,X1)
| ~ green(n6,X0)
| ~ green(X0,n4)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n4)
| ~ green(X1,n7) ) ).
cnf(u10874,axiom,
~ green(n6,n4) ).
cnf(u10883,axiom,
( ~ green(n3,X1)
| ~ green(n3,X0)
| ~ green(X0,n4)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n4)
| ~ green(X1,n7) ) ).
cnf(u10899,axiom,
( ~ red(n1,X0)
| ~ red(X0,n3)
| ~ red(X0,n5)
| ~ red(X0,n4) ) ).
cnf(u10903,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n4)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n1,X0)
| ~ red(X1,n7)
| ~ red(X1,n4) ) ).
cnf(u11173,axiom,
( ~ green(n6,X1)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n6,X0)
| ~ green(X1,n12) ) ).
cnf(u11207,axiom,
( ~ red(n5,X0)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u11216,axiom,
( ~ red(n4,X0)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u11225,axiom,
( ~ red(n2,X0)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u11236,axiom,
( ~ red(n1,X0)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u11274,axiom,
~ red(n10,n13) ).
cnf(u11277,axiom,
( ~ red(n10,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n10,X0)
| ~ red(X1,n13) ) ).
cnf(u11281,axiom,
( ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n6,X0)
| ~ red(X1,n9)
| ~ red(X1,n11) ) ).
cnf(u11291,axiom,
( ~ red(n6,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n6,X0)
| ~ red(X1,n9)
| ~ red(X1,n11) ) ).
cnf(u11308,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(u11317,axiom,
( ~ red(X2,n11)
| ~ red(X2,X0)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n9) ) ).
cnf(u11336,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n6)
| ~ red(X0,n6)
| ~ red(X2,n6)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n9) ) ).
cnf(u11365,axiom,
( ~ green(n6,X0)
| ~ green(X0,n7)
| ~ green(X0,n13)
| ~ green(X0,n10) ) ).
cnf(u11372,axiom,
( ~ green(n6,X0)
| ~ green(X0,n7)
| ~ green(X0,n13)
| ~ green(X0,n12) ) ).
cnf(u11551,axiom,
~ red(n1,n10) ).
cnf(u11556,axiom,
green(n1,n10) ).
cnf(u11743,axiom,
~ red(n3,n12) ).
cnf(u11748,axiom,
green(n3,n12) ).
cnf(u11788,axiom,
~ red(n4,n13) ).
cnf(u11793,axiom,
green(n4,n13) ).
cnf(u12215,axiom,
( ~ red(n4,X0)
| ~ red(X0,n11)
| ~ red(X0,n5)
| ~ red(X0,n12)
| ~ red(X0,n6) ) ).
cnf(u12225,axiom,
( ~ red(n4,X0)
| ~ red(X0,n5)
| ~ red(X0,n11)
| ~ red(X0,n6)
| ~ red(X0,n8) ) ).
cnf(u12257,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n11)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X1,n12) ) ).
cnf(u12276,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n10)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n10)
| ~ red(X1,n11) ) ).
cnf(u12287,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n8)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n8)
| ~ red(X1,n11) ) ).
cnf(u12306,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n6)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X1,n11) ) ).
cnf(u12317,axiom,
( ~ red(n5,X1)
| ~ red(n5,X0)
| ~ red(X0,n6)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X1,n11) ) ).
cnf(u12328,axiom,
( ~ red(X2,n12)
| ~ red(X2,X0)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n11) ) ).
cnf(u12465,axiom,
red(n2,n12) ).
cnf(u12524,axiom,
~ red(n12,n3) ).
cnf(u12528,axiom,
~ red(n12,n4) ).
cnf(u12676,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n5,X0)
| ~ green(X1,n12) ) ).
cnf(u12766,axiom,
~ red(n3,n13) ).
cnf(u12771,axiom,
green(n3,n13) ).
cnf(u12849,axiom,
( ~ red(n11,X1)
| ~ red(n11,X0)
| ~ red(X0,n3)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n3)
| ~ red(X1,n12) ) ).
cnf(u12853,axiom,
~ red(n11,n3) ).
cnf(u13120,axiom,
~ red(n2,n11) ).
cnf(u13123,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n5)
| ~ red(X0,n11)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n2,X0)
| ~ red(X1,n5)
| ~ red(X1,n11) ) ).
cnf(u13146,axiom,
~ red(n13,n6) ).
cnf(u13153,axiom,
~ red(n13,n4) ).
cnf(u13245,axiom,
( ~ red(X2,n13)
| ~ red(X2,X0)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n3)
| ~ red(X0,n3)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n3) ) ).
cnf(u13296,axiom,
( ~ green(n2,X1)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(n2,X0)
| ~ green(X1,n10) ) ).
cnf(u13307,axiom,
red(n1,n11) ).
cnf(u13310,axiom,
~ green(n1,n11) ).
cnf(u13414,axiom,
~ red(n1,n12) ).
cnf(u13419,axiom,
green(n1,n12) ).
cnf(u13440,axiom,
( ~ green(n3,X0)
| ~ green(X0,n5)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u13450,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n5,X0)
| ~ green(X1,n10) ) ).
cnf(u13471,axiom,
( ~ green(n5,X1)
| ~ green(n5,X0)
| ~ green(X0,n7)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X1,n7)
| ~ green(X1,n10) ) ).
cnf(u13488,axiom,
( ~ green(X2,n12)
| ~ green(X2,X0)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n10) ) ).
cnf(u13533,axiom,
( ~ green(n1,X0)
| ~ green(X0,n5)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u13549,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n5)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n1,X0)
| ~ red(X1,n7)
| ~ red(X1,n5) ) ).
cnf(u13575,axiom,
( ~ red(n1,X1)
| ~ red(n1,X0)
| ~ red(X0,n5)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X1,n5)
| ~ red(X1,n6) ) ).
cnf(u13604,axiom,
~ green(n10,n3) ).
cnf(u13625,axiom,
( ~ red(n1,X1)
| ~ red(X0,X1)
| ~ red(X0,n5)
| ~ red(X0,n8)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n1,X0)
| ~ red(X1,n5)
| ~ red(X1,n8) ) ).
cnf(u13665,axiom,
~ green(n5,n4) ).
cnf(u13668,axiom,
( ~ green(X2,n7)
| ~ green(X2,X0)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n4)
| ~ green(X0,n4)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n4) ) ).
cnf(u13677,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n4)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(n3,X0)
| ~ green(X1,n5)
| ~ green(X1,n4) ) ).
cnf(u13705,axiom,
~ green(n8,n4) ).
cnf(u13721,axiom,
~ red(n11,n2) ).
cnf(u13724,axiom,
( ~ red(X2,n12)
| ~ red(X2,X0)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n2)
| ~ red(X0,n2)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n2) ) ).
cnf(u13758,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n5)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(n4,X0)
| ~ red(X1,n7)
| ~ red(X1,n5) ) ).
cnf(u13768,axiom,
( ~ red(n2,X1)
| ~ red(n2,X0)
| ~ red(X0,n6)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n6)
| ~ red(X1,n11) ) ).
cnf(u13780,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n2,X0)
| ~ red(X1,n9)
| ~ red(X1,n11) ) ).
cnf(u13801,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n8)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n8)
| ~ red(X1,n11) ) ).
cnf(u13818,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X0,n5)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n4,X0)
| ~ red(X1,n11)
| ~ red(X1,n5) ) ).
cnf(u13828,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n11)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n11)
| ~ red(X1,n12) ) ).
cnf(u13838,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X0,n7)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n2,X0)
| ~ red(X1,n11)
| ~ red(X1,n7) ) ).
cnf(u13850,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n4,X0)
| ~ red(X1,n7)
| ~ red(X1,n8) ) ).
cnf(u13860,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X0,n7)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n4,X0)
| ~ red(X1,n11)
| ~ red(X1,n7) ) ).
cnf(u13869,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X0,n4)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n2,X0)
| ~ red(X1,n11)
| ~ red(X1,n4) ) ).
cnf(u13888,axiom,
( ~ green(n5,X0)
| ~ green(X0,n9)
| ~ green(X0,n12)
| ~ green(X0,n11) ) ).
cnf(u13903,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n7)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n7)
| ~ red(X1,n11) ) ).
cnf(u13924,axiom,
~ red(n6,n2) ).
cnf(u13931,axiom,
( ~ red(X2,n12)
| ~ red(X2,X0)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n2)
| ~ red(X0,n2)
| ~ red(X2,n2)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n4) ) ).
cnf(u13944,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X2,n4)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n11) ) ).
cnf(u13958,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X2,n4)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n7) ) ).
cnf(u14090,axiom,
( ~ red(n1,X0)
| ~ red(X0,n4)
| ~ red(X0,n8)
| ~ red(X0,n5)
| ~ red(X0,n7) ) ).
cnf(u14102,axiom,
( ~ red(n1,X0)
| ~ red(X0,n4)
| ~ red(X0,n11)
| ~ red(X0,n8)
| ~ red(X0,n5) ) ).
cnf(u14201,axiom,
( ~ red(X2,n7)
| ~ red(X2,X0)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n2)
| ~ red(X0,n2)
| ~ red(X2,n2)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n4) ) ).
cnf(u14237,axiom,
( ~ red(n2,X0)
| ~ red(X0,n4)
| ~ red(X0,n12)
| ~ red(X0,n7)
| ~ red(X0,n11) ) ).
cnf(u14248,axiom,
( ~ red(n2,X0)
| ~ red(X0,n4)
| ~ red(X0,n12)
| ~ red(X0,n11)
| ~ red(X0,n5) ) ).
cnf(u14542,axiom,
~ red(n5,n2) ).
cnf(u14840,axiom,
green(n2,n11) ).
cnf(u14844,axiom,
( ~ green(n1,X0)
| ~ green(X0,n2)
| ~ green(X0,n12)
| ~ green(X0,n11) ) ).
cnf(u14849,axiom,
red(n2,n13) ).
cnf(u14852,axiom,
~ green(n2,n13) ).
cnf(u14996,axiom,
( ~ red(n10,X1)
| ~ red(n10,X0)
| ~ red(X0,n2)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n2)
| ~ red(X1,n12) ) ).
cnf(u15126,axiom,
red(n1,n13) ).
cnf(u15399,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n13) ) ).
cnf(u15668,axiom,
( ~ green(n2,X1)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(n2,X0)
| ~ green(X1,n12) ) ).
cnf(u15696,axiom,
( ~ green(n5,X1)
| ~ green(n5,X0)
| ~ green(X0,n6)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n6)
| ~ green(X1,n7) ) ).
cnf(u15707,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n6)
| ~ green(X0,n7)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n5,X0)
| ~ green(X1,n6)
| ~ green(X1,n7) ) ).
cnf(u15718,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X2,n2)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n6) ) ).
cnf(u15732,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n2)
| ~ green(X0,n6)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n1,X0)
| ~ green(X1,n2)
| ~ green(X1,n6) ) ).
cnf(u15741,axiom,
( ~ green(X2,n13)
| ~ green(X2,X0)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n6)
| ~ green(X0,n6)
| ~ green(X1,n2)
| ~ green(X0,n2)
| ~ green(X2,n2)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n6) ) ).
cnf(u15759,axiom,
~ green(n9,n2) ).
cnf(u15844,axiom,
( ~ red(n8,X0)
| ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u15851,axiom,
( ~ red(n1,X0)
| ~ red(X0,n7)
| ~ red(X0,n13)
| ~ red(X0,n11)
| ~ red(X0,n9) ) ).
cnf(u15884,axiom,
( ~ red(n7,X0)
| ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u15898,axiom,
( ~ red(n4,X0)
| ~ red(X0,n7)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u15902,axiom,
( ~ green(n8,X1)
| ~ green(X0,X1)
| ~ green(X0,n11)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n8,X0)
| ~ green(X1,n11) ) ).
cnf(u15909,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n5,X0)
| ~ red(X1,n13) ) ).
cnf(u15927,axiom,
( ~ green(n7,X1)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X0,n8)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n7,X0)
| ~ green(X1,n10)
| ~ green(X1,n8) ) ).
cnf(u15935,axiom,
( ~ green(n3,X1)
| ~ green(n3,X0)
| ~ green(X0,n5)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n5)
| ~ green(X1,n7) ) ).
cnf(u16010,axiom,
( ~ red(n4,X0)
| ~ red(X0,n5)
| ~ red(X0,n14)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u16020,axiom,
( ~ red(n4,X0)
| ~ red(X0,n11)
| ~ red(X0,n5)
| ~ red(X0,n14)
| ~ red(X0,n7) ) ).
cnf(u16030,axiom,
( ~ red(n1,X0)
| ~ red(X0,n7)
| ~ red(X0,n4)
| ~ red(X0,n11)
| ~ red(X0,n3) ) ).
cnf(u16062,axiom,
( ~ red(n1,X0)
| ~ red(X0,n3)
| ~ red(X0,n13)
| ~ red(X0,n7)
| ~ red(X0,n11) ) ).
cnf(u16074,axiom,
( ~ red(n2,X0)
| ~ red(X0,n3)
| ~ red(X0,n14)
| ~ red(X0,n4)
| ~ red(X0,n7) ) ).
cnf(u16085,axiom,
( ~ red(n1,X0)
| ~ red(X0,n3)
| ~ red(X0,n8)
| ~ red(X0,n4)
| ~ red(X0,n7) ) ).
cnf(u16098,axiom,
( ~ red(n1,X0)
| ~ red(X0,n5)
| ~ red(X0,n13)
| ~ red(X0,n7)
| ~ red(X0,n11) ) ).
cnf(u16120,axiom,
( ~ red(n5,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n11)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(n5,X0)
| ~ red(X1,n7)
| ~ red(X1,n11) ) ).
cnf(u16158,axiom,
( ~ red(n5,X0)
| ~ red(X0,n7)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u16214,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n11)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n3,X0)
| ~ green(X1,n11) ) ).
cnf(u16266,axiom,
( ~ red(n4,X0)
| ~ red(X0,n5)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u16308,axiom,
( ~ red(n1,X0)
| ~ red(X0,n3)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u16319,axiom,
( ~ red(n4,X0)
| ~ red(X0,n11)
| ~ red(X0,n7)
| ~ red(X0,n14)
| ~ red(X0,n8) ) ).
cnf(u16333,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(n4,X0)
| ~ red(X1,n9)
| ~ red(X1,n11) ) ).
cnf(u16345,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n4,X0)
| ~ red(X1,n9)
| ~ red(X1,n11) ) ).
cnf(u16366,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n7)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X1,n7)
| ~ red(X1,n9) ) ).
cnf(u16378,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n10)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n3,X0)
| ~ green(X1,n5)
| ~ green(X1,n10) ) ).
cnf(u16387,axiom,
( ~ red(n2,X1)
| ~ red(n2,X0)
| ~ red(X0,n5)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X1,n8) ) ).
cnf(u16399,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n7)
| ~ red(X1,n8) ) ).
cnf(u16421,axiom,
( ~ green(n3,X1)
| ~ green(n3,X0)
| ~ green(X0,n4)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n6)
| ~ green(X1,n4)
| ~ green(X1,n6) ) ).
cnf(u16434,axiom,
~ green(n2,n4) ).
cnf(u16438,axiom,
( ~ red(n1,X1)
| ~ red(n1,X0)
| ~ red(X0,n4)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X1,n4)
| ~ red(X1,n7) ) ).
cnf(u16451,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n7)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n4)
| ~ red(X1,n7) ) ).
cnf(u16462,axiom,
( ~ red(n2,X1)
| ~ red(n2,X0)
| ~ red(X0,n4)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n4)
| ~ red(X1,n12) ) ).
cnf(u16473,axiom,
( ~ red(n3,X1)
| ~ red(n3,X0)
| ~ red(X0,n4)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n4)
| ~ red(X1,n8) ) ).
cnf(u16479,axiom,
( ~ red(n2,X1)
| ~ red(n2,X0)
| ~ red(X0,n4)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n4)
| ~ red(X1,n8) ) ).
cnf(u16498,axiom,
( ~ green(n2,X1)
| ~ green(n2,X0)
| ~ green(X0,n3)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n6)
| ~ green(X1,n3)
| ~ green(X1,n6) ) ).
cnf(u16510,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n9) ) ).
cnf(u16537,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n5)
| ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n4,X0)
| ~ red(X1,n5)
| ~ red(X1,n9) ) ).
cnf(u16567,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n7) ) ).
cnf(u16628,axiom,
( ~ red(n1,X0)
| ~ red(X0,n4)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u16646,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n3,X0)
| ~ green(X1,n9) ) ).
cnf(u16663,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n10)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n1,X0)
| ~ green(X1,n5)
| ~ green(X1,n10) ) ).
cnf(u16679,axiom,
( ~ green(n3,X1)
| ~ green(n3,X0)
| ~ green(X0,n7)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X1,n7)
| ~ green(X1,n9) ) ).
cnf(u16687,axiom,
( ~ green(X2,n12)
| ~ green(X2,X0)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X1,n9)
| ~ green(X0,n9)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n9) ) ).
cnf(u16702,axiom,
( ~ green(X2,n12)
| ~ green(X2,X0)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X1,n7)
| ~ green(X0,n7)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n7) ) ).
cnf(u16719,axiom,
( ~ green(n3,X1)
| ~ green(n3,X0)
| ~ green(X0,n5)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n5)
| ~ green(X1,n7) ) ).
cnf(u16727,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X2,n4)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n9) ) ).
cnf(u16744,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n4)
| ~ red(X1,n9) ) ).
cnf(u16767,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n5) ) ).
cnf(u16780,axiom,
( ~ green(X2,n12)
| ~ green(X2,X0)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X2,n3)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n5) ) ).
cnf(u16790,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n3)
| ~ red(X0,n3)
| ~ red(X2,n3)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n8) ) ).
cnf(u16918,axiom,
( ~ green(n4,X1)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n4,X0)
| ~ green(X1,n9) ) ).
cnf(u16926,axiom,
( ~ green(n5,X1)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n5,X0)
| ~ green(X1,n9) ) ).
cnf(u16963,axiom,
( ~ green(n5,X1)
| ~ green(n5,X0)
| ~ green(X0,n7)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X1,n7)
| ~ green(X1,n9) ) ).
cnf(u16973,axiom,
( ~ green(X2,n12)
| ~ green(X2,X0)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X1,n9)
| ~ green(X0,n9)
| ~ green(X1,n5)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n9) ) ).
cnf(u16983,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n9)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n1,X0)
| ~ green(X1,n5)
| ~ green(X1,n9) ) ).
cnf(u16991,axiom,
( ~ green(n3,X1)
| ~ green(X0,X1)
| ~ green(X0,n5)
| ~ green(X0,n9)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n3,X0)
| ~ green(X1,n5)
| ~ green(X1,n9) ) ).
cnf(u17016,axiom,
( ~ green(n2,X0)
| ~ green(X0,n3)
| ~ green(X0,n11)
| ~ green(X0,n10) ) ).
cnf(u17042,axiom,
( ~ green(n4,X0)
| ~ green(X0,n6)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u17049,axiom,
( ~ green(n3,X0)
| ~ green(X0,n6)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u17056,axiom,
( ~ green(n5,X0)
| ~ green(X0,n6)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u17089,axiom,
( ~ red(n2,X0)
| ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u17099,axiom,
( ~ red(n2,X0)
| ~ red(X0,n7)
| ~ red(X0,n14)
| ~ red(X0,n13) ) ).
cnf(u17151,axiom,
( ~ red(n2,X0)
| ~ red(X0,n8)
| ~ red(X0,n3)
| ~ red(X0,n14)
| ~ red(X0,n4) ) ).
cnf(u17162,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n6)
| ~ red(X1,n9) ) ).
cnf(u17175,axiom,
( ~ red(n2,X1)
| ~ red(n2,X0)
| ~ red(X0,n6)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n6)
| ~ red(X1,n12) ) ).
cnf(u17188,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n10)
| ~ red(X0,n12)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n10)
| ~ red(X1,n12) ) ).
cnf(u17201,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n5)
| ~ red(X0,n10)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n5)
| ~ red(X1,n10) ) ).
cnf(u17214,axiom,
( ~ red(n2,X1)
| ~ red(n2,X0)
| ~ red(X0,n6)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n6)
| ~ red(X1,n8) ) ).
cnf(u17227,axiom,
( ~ red(n2,X1)
| ~ red(X0,X1)
| ~ red(X0,n3)
| ~ red(X0,n8)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(n2,X0)
| ~ red(X1,n3)
| ~ red(X1,n8) ) ).
cnf(u17258,axiom,
( ~ red(n2,X1)
| ~ red(n2,X0)
| ~ red(X0,n6)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n7)
| ~ red(X1,n6)
| ~ red(X1,n7) ) ).
cnf(u17350,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n3)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n6)
| ~ green(X1,n3)
| ~ green(X1,n6) ) ).
cnf(u17358,axiom,
( ~ green(n1,X0)
| ~ green(X0,n6)
| ~ green(X0,n2)
| ~ green(X0,n10)
| ~ green(X0,n3) ) ).
cnf(u17365,axiom,
( ~ red(n3,X1)
| ~ red(n3,X0)
| ~ red(X0,n5)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X1,n8) ) ).
cnf(u17372,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n9)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n1,X0)
| ~ green(X1,n3)
| ~ green(X1,n9) ) ).
cnf(u17380,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n5)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n1,X0)
| ~ green(X1,n3)
| ~ green(X1,n5) ) ).
cnf(u17388,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n5)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n1,X0)
| ~ green(X1,n3)
| ~ green(X1,n5) ) ).
cnf(u17396,axiom,
( ~ green(X0,X1)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X1,n8)
| ~ green(X0,n8)
| ~ green(X2,n8)
| ~ green(X2,X1)
| ~ green(X2,n10)
| ~ green(X2,n3) ) ).
cnf(u17402,axiom,
( ~ red(n3,X0)
| ~ red(X0,n8)
| ~ red(X0,n4)
| ~ red(X0,n14)
| ~ red(X0,n5) ) ).
cnf(u17408,axiom,
( ~ red(n2,X0)
| ~ red(X0,n4)
| ~ red(X0,n14)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u17418,axiom,
( ~ red(n2,X0)
| ~ red(X0,n8)
| ~ red(X0,n4)
| ~ red(X0,n14)
| ~ red(X0,n5) ) ).
cnf(u17428,axiom,
( ~ red(n4,X1)
| ~ red(X0,X1)
| ~ red(X0,n5)
| ~ red(X0,n8)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(n4,X0)
| ~ red(X1,n5)
| ~ red(X1,n8) ) ).
cnf(u17439,axiom,
( ~ red(n4,X1)
| ~ red(n4,X0)
| ~ red(X0,n5)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X1,n8) ) ).
cnf(u17450,axiom,
( ~ red(X2,n14)
| ~ red(X2,X0)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X2,n4)
| ~ red(X2,X1)
| ~ red(X0,X1)
| ~ red(X2,n8) ) ).
cnf(u17475,axiom,
( ~ green(n2,X0)
| ~ green(X0,n3)
| ~ green(X0,n13)
| ~ green(X0,n12) ) ).
cnf(u17526,axiom,
( ~ green(n1,X0)
| ~ green(X0,n3)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u18471,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n6)
| ~ green(X0,n7)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n1,X0)
| ~ green(X1,n6)
| ~ green(X1,n7) ) ).
cnf(u18498,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n7)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(n1,X0)
| ~ green(X1,n3)
| ~ green(X1,n7) ) ).
cnf(u18509,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n5)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n5)
| ~ green(X1,n7) ) ).
cnf(u18520,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n5)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n7)
| ~ green(X1,n5)
| ~ green(X1,n7) ) ).
cnf(u18531,axiom,
( ~ green(n1,X1)
| ~ green(X0,X1)
| ~ green(X0,n3)
| ~ green(X0,n7)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(n1,X0)
| ~ green(X1,n3)
| ~ green(X1,n7) ) ).
cnf(u18542,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n7)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X1,n7)
| ~ green(X1,n9) ) ).
cnf(u18576,axiom,
( ~ red(n1,X1)
| ~ red(n1,X0)
| ~ red(X0,n2)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X1,n2)
| ~ red(X1,n4) ) ).
cnf(u18619,axiom,
( ~ red(n1,X1)
| ~ red(n1,X0)
| ~ red(X0,n2)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X1,n2)
| ~ red(X1,n9) ) ).
cnf(u18661,axiom,
( ~ red(n1,X1)
| ~ red(n1,X0)
| ~ red(X0,n2)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n4)
| ~ red(X1,n2)
| ~ red(X1,n4) ) ).
cnf(u18713,axiom,
( ~ red(n1,X1)
| ~ red(n1,X0)
| ~ red(X0,n2)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n9)
| ~ red(X1,n2)
| ~ red(X1,n9) ) ).
cnf(u18739,axiom,
( ~ red(n10,X1)
| ~ red(n10,X0)
| ~ red(X0,n2)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n2)
| ~ red(X1,n12) ) ).
cnf(u18769,axiom,
( ~ red(X0,n2)
| ~ red(n7,X0)
| ~ red(n7,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n2)
| ~ red(X1,n8) ) ).
cnf(u18897,axiom,
~ green(n9,n3) ).
cnf(u18900,axiom,
( ~ green(X2,n10)
| ~ green(X2,X0)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X1,n3)
| ~ green(X0,n3)
| ~ green(X1,n9)
| ~ green(X0,n9)
| ~ green(X2,n9)
| ~ green(X2,X1)
| ~ green(X0,X1)
| ~ green(X2,n3) ) ).
cnf(u18927,axiom,
( ~ green(n1,X1)
| ~ green(n1,X0)
| ~ green(X0,n7)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X1,n7)
| ~ green(X1,n9) ) ).
cnf(u11925,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u36,axiom,
( ~ less_than(X1,X2)
| ~ less_than(X0,X1)
| less_than(X0,X2) ) ).
cnf(u18044,axiom,
( ~ green(X2,n9)
| ~ green(X2,n3)
| ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X2,n7)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u10065,axiom,
( ~ red(X3,n8)
| ~ 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,n8)
| ~ red(X2,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u18371,axiom,
( ~ red(n1,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u8255,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2641,axiom,
less_than(n2,n14) ).
cnf(u2161,axiom,
less_than(n8,n11) ).
cnf(u1391,axiom,
less_than(n1,n8) ).
cnf(u32,axiom,
less_than(n1,n2) ).
cnf(u5669,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2625,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n13) ) ).
cnf(u2395,axiom,
( ~ less_than(X0,n10)
| less_than(X0,n12) ) ).
cnf(u63,axiom,
( ~ less_than(X0,n10)
| less_than(X0,n11) ) ).
cnf(u2342,axiom,
less_than(n5,n12) ).
cnf(u15792,axiom,
( ~ green(n5,X0)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X0,n6) ) ).
cnf(u29,axiom,
less_than(n4,n5) ).
cnf(u40,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(u10031,axiom,
( ~ red(X3,n8)
| ~ 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,n8)
| ~ red(X2,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u18179,axiom,
( ~ green(X2,n13)
| ~ green(X2,n3)
| ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X2,n6)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,X1)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u25,axiom,
less_than(n8,n9) ).
cnf(u14668,axiom,
( ~ green(X3,n12)
| ~ 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,n12)
| ~ green(X2,n12)
| ~ green(X1,n12)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2343,axiom,
less_than(n6,n12) ).
cnf(u14138,axiom,
( ~ green(X3,n11)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n9)
| ~ green(X2,n9)
| ~ green(X1,n9)
| ~ green(X3,n9)
| ~ green(X0,n11)
| ~ green(X2,n11)
| ~ green(X1,n11)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2643,axiom,
less_than(n4,n14) ).
cnf(u2889,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n14) ) ).
cnf(u474,axiom,
less_than(n3,n5) ).
cnf(u17753,axiom,
( ~ green(X3,n9)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X1,n5)
| ~ green(X3,n5)
| ~ green(X0,n9)
| ~ green(X2,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2154,axiom,
less_than(n1,n11) ).
cnf(u37,axiom,
( ~ less_than(X0,X1)
| green(X0,X1)
| red(X0,X1) ) ).
cnf(u2139,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n10) ) ).
cnf(u2339,axiom,
less_than(n2,n12) ).
cnf(u16108,axiom,
( ~ red(n6,X1)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(n6,X0)
| ~ red(X0,X1) ) ).
cnf(u1611,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n8) ) ).
cnf(u22,axiom,
less_than(n11,n12) ).
cnf(u17073,axiom,
( ~ red(n2,X0)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X0,n12) ) ).
cnf(u1062,axiom,
less_than(n4,n6) ).
cnf(u2482,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n12) ) ).
cnf(u1939,axiom,
less_than(n4,n10) ).
cnf(u2644,axiom,
less_than(n5,n14) ).
cnf(u1583,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n8) ) ).
cnf(u18118,axiom,
( ~ green(X3,n11)
| ~ 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,n11)
| ~ green(X2,n11)
| ~ green(X1,n11)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u6485,axiom,
red(n9,n14) ).
cnf(u11387,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(u2159,axiom,
less_than(n6,n11) ).
cnf(u2645,axiom,
less_than(n6,n14) ).
cnf(u14706,axiom,
( ~ green(n4,X0)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X0,n6) ) ).
cnf(u2494,axiom,
less_than(n2,n13) ).
cnf(u2325,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n11) ) ).
cnf(u10131,axiom,
( ~ green(X3,n12)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n9)
| ~ green(X2,n9)
| ~ green(X1,n9)
| ~ green(X3,n9)
| ~ green(X0,n12)
| ~ green(X2,n12)
| ~ green(X1,n12)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u11152,axiom,
( ~ green(n6,X1)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(n6,X0)
| ~ green(X0,X1) ) ).
cnf(u2855,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n14) ) ).
cnf(u14301,axiom,
( ~ red(X2,n11)
| ~ red(X2,n4)
| ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u15184,axiom,
( ~ red(n1,X1)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u17820,axiom,
( ~ green(n8,X1)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(n8,X0)
| ~ green(X0,X1) ) ).
cnf(u1376,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n7) ) ).
cnf(u14143,axiom,
( ~ green(n9,X1)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(n9,X0)
| ~ green(X0,X1) ) ).
cnf(u2851,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n14) ) ).
cnf(u17295,axiom,
( ~ red(X3,n13)
| ~ 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,n13)
| ~ red(X2,n13)
| ~ red(X1,n13)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1919,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n9) ) ).
cnf(u2649,axiom,
less_than(n10,n14) ).
cnf(u4126,axiom,
( ~ red(X3,n14)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n13)
| ~ red(X2,n13)
| ~ red(X1,n13)
| ~ red(X3,n13)
| ~ red(X0,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1941,axiom,
less_than(n6,n10) ).
cnf(u10487,axiom,
( ~ red(X3,n12)
| ~ 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,n12)
| ~ red(X2,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2347,axiom,
less_than(n10,n12) ).
cnf(u1690,axiom,
less_than(n2,n9) ).
cnf(u17770,axiom,
( ~ green(X3,n6)
| ~ 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,n6)
| ~ green(X2,n6)
| ~ green(X1,n6)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1691,axiom,
less_than(n3,n9) ).
cnf(u18409,axiom,
( ~ red(X2,n14)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n4)
| ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u16658,axiom,
( ~ green(X3,n9)
| ~ 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,n9)
| ~ green(X2,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u18181,axiom,
( ~ green(n3,X1)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n12)
| ~ green(X0,n12)
| ~ green(n3,X0)
| ~ green(X0,X1) ) ).
cnf(u1938,axiom,
less_than(n3,n10) ).
cnf(u10539,axiom,
( ~ green(X3,n6)
| ~ 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,n6)
| ~ green(X2,n6)
| ~ green(X1,n6)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u14045,axiom,
( ~ red(X3,n12)
| ~ 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,n12)
| ~ red(X2,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2503,axiom,
less_than(n11,n13) ).
cnf(u17953,axiom,
( ~ green(X2,n11)
| ~ green(X2,n5)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X2,n9)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u64,axiom,
( ~ less_than(X0,n11)
| less_than(X0,n12) ) ).
cnf(u2321,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n11) ) ).
cnf(u18417,axiom,
( ~ red(X2,n8)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n5)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u16934,axiom,
( ~ green(n5,X0)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X0,n7) ) ).
cnf(u2853,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n14) ) ).
cnf(u2499,axiom,
less_than(n7,n13) ).
cnf(u358,axiom,
less_than(n1,n3) ).
cnf(u18419,axiom,
( ~ red(X2,n13)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n9)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u1210,axiom,
less_than(n5,n7) ).
cnf(u1692,axiom,
less_than(n4,n9) ).
cnf(u1208,axiom,
less_than(n3,n7) ).
cnf(u1193,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n6) ) ).
cnf(u13223,axiom,
( ~ red(X3,n13)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X3,n11)
| ~ red(X0,n13)
| ~ red(X2,n13)
| ~ red(X1,n13)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1940,axiom,
less_than(n5,n10) ).
cnf(u17900,axiom,
( ~ red(n2,X1)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u17949,axiom,
( ~ green(X3,n11)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X1,n5)
| ~ green(X3,n5)
| ~ green(X0,n11)
| ~ green(X2,n11)
| ~ green(X1,n11)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2137,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n10) ) ).
cnf(u2476,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n12) ) ).
cnf(u7398,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(u2646,axiom,
less_than(n7,n14) ).
cnf(u5335,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(u1195,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n6) ) ).
cnf(u61,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n9) ) ).
cnf(u65,axiom,
( ~ less_than(X0,n12)
| less_than(X0,n13) ) ).
cnf(u4217,axiom,
( ~ red(X3,n14)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n12)
| ~ red(X2,n12)
| ~ red(X1,n12)
| ~ red(X3,n12)
| ~ red(X0,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u17819,axiom,
( ~ green(n8,X1)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(n8,X0)
| ~ green(X0,X1) ) ).
cnf(u18132,axiom,
( ~ green(n3,X0)
| ~ green(X0,n10)
| ~ green(X0,n11)
| ~ green(X0,n9) ) ).
cnf(u2792,axiom,
( ~ red(X3,n13)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n12)
| ~ red(X2,n12)
| ~ red(X1,n12)
| ~ red(X3,n12)
| ~ red(X0,n13)
| ~ red(X2,n13)
| ~ red(X1,n13)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u57,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n5) ) ).
cnf(u17679,axiom,
( ~ green(X3,n11)
| ~ 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,n11)
| ~ green(X2,n11)
| ~ green(X1,n11)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u18296,axiom,
red(n1,n14) ).
cnf(u18416,axiom,
( ~ red(X2,n8)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2058,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n10) ) ).
cnf(u1380,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n7) ) ).
cnf(u14051,axiom,
( ~ red(n10,X0)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X0,n12) ) ).
cnf(u18418,axiom,
( ~ red(X2,n13)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u1050,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n5) ) ).
cnf(u1393,axiom,
less_than(n3,n8) ).
cnf(u18046,axiom,
( ~ green(n3,X0)
| ~ green(X0,n11)
| ~ green(X0,n12)
| ~ green(X0,n9) ) ).
cnf(u2805,axiom,
( ~ less_than(X0,n11)
| less_than(X0,n14) ) ).
cnf(u18369,axiom,
( ~ red(n1,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u2244,axiom,
( ~ red(X3,n12)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X3,n11)
| ~ red(X0,n12)
| ~ red(X2,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2650,axiom,
less_than(n11,n14) ).
cnf(u27,axiom,
less_than(n6,n7) ).
cnf(u15357,axiom,
( ~ red(n2,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u4538,axiom,
( ~ red(X3,n14)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X3,n11)
| ~ red(X0,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u8077,axiom,
( ~ red(X3,n9)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n2)
| ~ red(X2,n2)
| ~ red(X1,n2)
| ~ red(X3,n2)
| ~ red(X0,n9)
| ~ red(X2,n9)
| ~ red(X1,n9)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u12504,axiom,
( ~ red(X3,n12)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n2)
| ~ red(X2,n2)
| ~ red(X1,n2)
| ~ red(X3,n2)
| ~ red(X0,n12)
| ~ red(X2,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1943,axiom,
less_than(n8,n10) ).
cnf(u8033,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(u54,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n2) ) ).
cnf(u39,axiom,
( ~ green(X0,X1)
| ~ red(X0,X1) ) ).
cnf(u20,axiom,
less_than(n13,n14) ).
cnf(u2887,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n14) ) ).
cnf(u18412,axiom,
( ~ red(X2,n14)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n9)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u1942,axiom,
less_than(n7,n10) ).
cnf(u1060,axiom,
less_than(n2,n6) ).
cnf(u17022,axiom,
( ~ red(X2,n8)
| ~ red(X2,n6)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u18421,axiom,
( ~ red(X2,n13)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n12)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2160,axiom,
less_than(n7,n11) ).
cnf(u2345,axiom,
less_than(n8,n12) ).
cnf(u18410,axiom,
( ~ red(X2,n14)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n5)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2500,axiom,
less_than(n8,n13) ).
cnf(u16173,axiom,
( ~ red(n6,X1)
| ~ red(X1,n7)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,n7)
| ~ red(n6,X0) ) ).
cnf(u16755,axiom,
( ~ green(X2,n10)
| ~ green(X2,n5)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X2,n7)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u2157,axiom,
less_than(n4,n11) ).
cnf(u18420,axiom,
( ~ red(X2,n13)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n5)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u28,axiom,
less_than(n5,n6) ).
cnf(u16526,axiom,
( ~ red(n2,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u2497,axiom,
less_than(n5,n13) ).
cnf(u24,axiom,
less_than(n9,n10) ).
cnf(u16503,axiom,
( ~ red(X2,n11)
| ~ red(X2,n6)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u18368,axiom,
( ~ red(n1,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u2327,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n11) ) ).
cnf(u2627,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n13) ) ).
cnf(u473,axiom,
less_than(n2,n5) ).
cnf(u420,axiom,
less_than(n1,n4) ).
cnf(u8778,axiom,
( ~ red(X3,n5)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n2)
| ~ red(X2,n2)
| ~ red(X1,n2)
| ~ red(X3,n2)
| ~ red(X0,n5)
| ~ red(X2,n5)
| ~ red(X1,n5)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1695,axiom,
less_than(n7,n9) ).
cnf(u21,axiom,
less_than(n12,n13) ).
cnf(u1061,axiom,
less_than(n3,n6) ).
cnf(u2598,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n13) ) ).
cnf(u18415,axiom,
( ~ red(X2,n8)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n4)
| ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,X1)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u1937,axiom,
less_than(n2,n10) ).
cnf(u2493,axiom,
less_than(n1,n13) ).
cnf(u2621,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n13) ) ).
cnf(u12742,axiom,
( ~ green(X3,n12)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X1,n5)
| ~ green(X3,n5)
| ~ green(X0,n12)
| ~ green(X2,n12)
| ~ green(X1,n12)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2647,axiom,
less_than(n8,n14) ).
cnf(u1923,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n9) ) ).
cnf(u1027,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n5) ) ).
cnf(u1680,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n8) ) ).
cnf(u2143,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n10) ) ).
cnf(u8887,axiom,
( ~ red(X3,n7)
| ~ red(X2,X1)
| ~ red(X0,X3)
| ~ red(X2,X3)
| ~ red(X1,X3)
| ~ red(X0,n2)
| ~ red(X2,n2)
| ~ red(X1,n2)
| ~ red(X3,n2)
| ~ red(X0,n7)
| ~ red(X2,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u11933,axiom,
( ~ red(X2,n14)
| ~ red(X2,n5)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X2,n8)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2478,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n12) ) ).
cnf(u11056,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1694,axiom,
less_than(n6,n9) ).
cnf(u18912,axiom,
( ~ green(X2,n10)
| ~ green(X2,n7)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X2,n9)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u1394,axiom,
less_than(n4,n8) ).
cnf(u18414,axiom,
( ~ red(X2,n14)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n8)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2338,axiom,
less_than(n1,n12) ).
cnf(u1689,axiom,
less_than(n1,n9) ).
cnf(u18485,axiom,
( ~ green(n1,X0)
| ~ green(X0,n6)
| ~ green(X0,n7)
| ~ green(X0,n10)
| ~ green(X0,n3) ) ).
cnf(u1936,axiom,
less_than(n1,n10) ).
cnf(u2158,axiom,
less_than(n5,n11) ).
cnf(u11062,axiom,
( ~ red(X2,n14)
| ~ red(X2,n6)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X2,n12)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u1925,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n9) ) ).
cnf(u2810,axiom,
( ~ less_than(X0,n10)
| less_than(X0,n14) ) ).
cnf(u7258,axiom,
( ~ green(X3,n10)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n9)
| ~ green(X2,n9)
| ~ green(X1,n9)
| ~ green(X3,n9)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u8544,axiom,
( ~ red(X2,n14)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X2,n11)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u6856,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u12928,axiom,
( ~ red(X2,n14)
| ~ red(X2,n4)
| ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X2,n12)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u1207,axiom,
less_than(n2,n7) ).
cnf(u11148,axiom,
( ~ green(X3,n13)
| ~ 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,n13)
| ~ green(X2,n13)
| ~ green(X1,n13)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2502,axiom,
less_than(n10,n13) ).
cnf(u2474,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n12) ) ).
cnf(u2162,axiom,
less_than(n9,n11) ).
cnf(u2651,axiom,
less_than(n12,n14) ).
cnf(u59,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n7) ) ).
cnf(u18367,axiom,
( ~ red(n1,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u14291,axiom,
( ~ red(X3,n11)
| ~ 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,n11)
| ~ red(X2,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u11058,axiom,
( ~ red(X2,n14)
| ~ red(X2,n6)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X2,n8)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u15003,axiom,
red(n3,n14) ).
cnf(u2317,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n11) ) ).
cnf(u1382,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n7) ) ).
cnf(u18192,axiom,
( ~ green(n3,X0)
| ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(X0,n6) ) ).
cnf(u17021,axiom,
( ~ red(X2,n14)
| ~ red(X2,n6)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2346,axiom,
less_than(n9,n12) ).
cnf(u2640,axiom,
less_than(n1,n14) ).
cnf(u16050,axiom,
( ~ red(X3,n7)
| ~ 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,n7)
| ~ red(X2,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2340,axiom,
less_than(n3,n12) ).
cnf(u12869,axiom,
red(n4,n14) ).
cnf(u15872,axiom,
( ~ red(n7,X0)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X0,n11) ) ).
cnf(u15257,axiom,
red(n2,n14) ).
cnf(u18554,axiom,
( ~ green(n1,X0)
| ~ green(X0,n7)
| ~ green(X0,n12)
| ~ green(X0,n5)
| ~ green(X0,n9) ) ).
cnf(u5657,axiom,
red(n10,n14) ).
cnf(u448,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n4) ) ).
cnf(u11431,axiom,
( ~ green(X3,n12)
| ~ 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,n12)
| ~ green(X2,n12)
| ~ green(X1,n12)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u12939,axiom,
( ~ red(n4,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n5)
| ~ red(X0,n5)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(n4,X0)
| ~ red(X0,X1) ) ).
cnf(u60,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n8) ) ).
cnf(u11028,axiom,
red(n6,n14) ).
cnf(u41,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(u18913,axiom,
( ~ green(X2,n10)
| ~ green(X2,n5)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X2,n9)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u1206,axiom,
less_than(n1,n7) ).
cnf(u18374,axiom,
( ~ red(n1,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n11)
| ~ red(X0,n11)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n1,X0)
| ~ red(X0,X1) ) ).
cnf(u56,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n4) ) ).
cnf(u4213,axiom,
red(n12,n14) ).
cnf(u17722,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(u30,axiom,
less_than(n3,n4) ).
cnf(u4541,axiom,
( ~ red(X2,n14)
| ~ red(X2,n11)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X2,n12)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u8230,axiom,
red(n7,n14) ).
cnf(u10461,axiom,
( ~ green(X3,n10)
| ~ 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,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2498,axiom,
less_than(n6,n13) ).
cnf(u2554,axiom,
( ~ less_than(X0,n11)
| less_than(X0,n13) ) ).
cnf(u16128,axiom,
( ~ red(n6,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(n6,X0)
| ~ red(X0,X1) ) ).
cnf(u2155,axiom,
less_than(n2,n11) ).
cnf(u26,axiom,
less_than(n7,n8) ).
cnf(u16670,axiom,
( ~ green(X2,n12)
| ~ green(X2,n7)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X2,n9)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u16890,axiom,
( ~ red(n2,X0)
| ~ red(X0,n5)
| ~ red(X0,n12)
| ~ red(X0,n14)
| ~ red(X0,n4) ) ).
cnf(u7725,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(u4459,axiom,
( ~ red(n12,X1)
| ~ red(X1,n14)
| ~ red(X0,n14)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(n12,X0)
| ~ red(X0,X1) ) ).
cnf(u18038,axiom,
( ~ green(X3,n9)
| ~ 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,n9)
| ~ green(X2,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1927,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n9) ) ).
cnf(u38,negated_conjecture,
~ goal ).
cnf(u18080,axiom,
( ~ green(X3,n10)
| ~ 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,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u23,axiom,
less_than(n10,n11) ).
cnf(u18555,axiom,
( ~ green(n1,X0)
| ~ green(X0,n7)
| ~ green(X0,n12)
| ~ green(X0,n3)
| ~ green(X0,n9) ) ).
cnf(u8508,axiom,
( ~ red(X2,n12)
| ~ red(X2,n6)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X2,n11)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2648,axiom,
less_than(n9,n14) ).
cnf(u2623,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n13) ) ).
cnf(u16002,axiom,
( ~ red(X3,n13)
| ~ 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,n13)
| ~ red(X2,n13)
| ~ red(X1,n13)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u17663,axiom,
( ~ green(n3,X0)
| ~ green(X0,n9)
| ~ green(X0,n10)
| ~ green(X0,n7) ) ).
cnf(u2495,axiom,
less_than(n3,n13) ).
cnf(u1059,axiom,
less_than(n1,n6) ).
cnf(u2329,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n11) ) ).
cnf(u2250,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n11) ) ).
cnf(u2156,axiom,
less_than(n3,n11) ).
cnf(u2849,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n14) ) ).
cnf(u31,axiom,
less_than(n2,n3) ).
cnf(u17899,axiom,
( ~ red(n2,X1)
| ~ red(X1,n8)
| ~ red(X0,n8)
| ~ red(X1,n4)
| ~ red(X0,n4)
| ~ red(X1,n7)
| ~ red(X0,n7)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u2141,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n10) ) ).
cnf(u2341,axiom,
less_than(n4,n12) ).
cnf(u17952,axiom,
( ~ green(n5,X1)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(n5,X0)
| ~ green(X0,X1) ) ).
cnf(u18388,axiom,
( ~ red(n1,X0)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X0,n9) ) ).
cnf(u18004,axiom,
( ~ red(X3,n13)
| ~ 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,n13)
| ~ red(X2,n13)
| ~ red(X1,n13)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1629,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n8) ) ).
cnf(u16208,axiom,
( ~ green(X2,n10)
| ~ green(X2,n4)
| ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X2,n6)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u2472,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n12) ) ).
cnf(u15039,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1392,axiom,
less_than(n2,n8) ).
cnf(u2642,axiom,
less_than(n3,n14) ).
cnf(u11065,axiom,
( ~ red(n6,X1)
| ~ red(X1,n11)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,n11)
| ~ red(n6,X0) ) ).
cnf(u2592,axiom,
( ~ less_than(X0,n10)
| less_than(X0,n13) ) ).
cnf(u12914,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u14696,axiom,
( ~ green(n4,X1)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(n4,X0)
| ~ green(X0,X1) ) ).
cnf(u1862,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n9) ) ).
cnf(u2484,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n12) ) ).
cnf(u1395,axiom,
less_than(n5,n8) ).
cnf(u16957,axiom,
( ~ red(X3,n8)
| ~ 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,n8)
| ~ red(X2,n8)
| ~ red(X1,n8)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1614,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n8) ) ).
cnf(u2145,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n10) ) ).
cnf(u17652,axiom,
( ~ green(X3,n7)
| ~ 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,n7)
| ~ green(X2,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u1921,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n9) ) ).
cnf(u6497,axiom,
( ~ red(X3,n14)
| ~ 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,n14)
| ~ red(X2,n14)
| ~ red(X1,n14)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u10386,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(u18177,axiom,
( ~ green(X3,n13)
| ~ 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,n13)
| ~ green(X2,n13)
| ~ green(X1,n13)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u17074,axiom,
( ~ red(n2,X0)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X0,n5) ) ).
cnf(u17963,axiom,
( ~ green(n5,X0)
| ~ green(X0,n10)
| ~ green(X0,n11)
| ~ green(X0,n9) ) ).
cnf(u2344,axiom,
less_than(n7,n12) ).
cnf(u18180,axiom,
( ~ green(n3,X1)
| ~ green(X1,n13)
| ~ green(X0,n13)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(n3,X0)
| ~ green(X0,X1) ) ).
cnf(u1693,axiom,
less_than(n5,n9) ).
cnf(u2857,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n14) ) ).
cnf(u2631,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n13) ) ).
cnf(u8110,axiom,
( ~ red(X3,n12)
| ~ 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,n12)
| ~ red(X2,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u2629,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n13) ) ).
cnf(u2800,axiom,
( ~ less_than(X0,n12)
| less_than(X0,n14) ) ).
cnf(u18411,axiom,
( ~ red(X2,n14)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n7)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2602,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n13) ) ).
cnf(u2323,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n11) ) ).
cnf(u17757,axiom,
( ~ green(X2,n9)
| ~ green(X2,n5)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X2,n7)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u4530,axiom,
red(n11,n14) ).
cnf(u14388,axiom,
( ~ green(X3,n10)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X1,n5)
| ~ green(X3,n5)
| ~ green(X0,n10)
| ~ green(X2,n10)
| ~ green(X1,n10)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u472,axiom,
less_than(n1,n5) ).
cnf(u1378,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n7) ) ).
cnf(u1209,axiom,
less_than(n4,n7) ).
cnf(u2480,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n12) ) ).
cnf(u18484,axiom,
( ~ green(n1,X0)
| ~ green(X0,n6)
| ~ green(X0,n7)
| ~ green(X0,n10)
| ~ green(X0,n5) ) ).
cnf(u2319,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n11) ) ).
cnf(u10018,axiom,
( ~ red(n11,X0)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X0,n12) ) ).
cnf(u18283,axiom,
( ~ red(n2,X1)
| ~ red(X1,n13)
| ~ red(X0,n13)
| ~ red(X1,n12)
| ~ red(X0,n12)
| ~ red(X1,n9)
| ~ red(X0,n9)
| ~ red(n2,X0)
| ~ red(X0,X1) ) ).
cnf(u9401,axiom,
( ~ green(X3,n12)
| ~ 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,n12)
| ~ green(X2,n12)
| ~ green(X1,n12)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u2496,axiom,
less_than(n4,n13) ).
cnf(u13227,axiom,
( ~ red(X2,n13)
| ~ red(X2,n11)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X2,n12)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u13578,axiom,
( ~ green(X2,n10)
| ~ green(X2,n3)
| ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X2,n6)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,X1)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u18413,axiom,
( ~ red(X2,n14)
| ~ red(X2,n2)
| ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X2,n12)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2891,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n14) ) ).
cnf(u2501,axiom,
less_than(n9,n13) ).
cnf(u4218,axiom,
( ~ red(X2,n14)
| ~ red(X2,n12)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X2,n13)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u16710,axiom,
( ~ green(X2,n12)
| ~ green(X2,n5)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X2,n7)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u2135,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n10) ) ).
cnf(u62,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n10) ) ).
cnf(u66,axiom,
( ~ less_than(X0,n13)
| less_than(X0,n14) ) ).
cnf(u16552,axiom,
( ~ green(X3,n7)
| ~ green(X2,X1)
| ~ green(X0,X3)
| ~ green(X2,X3)
| ~ green(X1,X3)
| ~ green(X0,n5)
| ~ green(X2,n5)
| ~ green(X1,n5)
| ~ green(X3,n5)
| ~ green(X0,n7)
| ~ green(X2,n7)
| ~ green(X1,n7)
| ~ green(X0,X1)
| ~ green(X0,X2) ) ).
cnf(u14174,axiom,
( ~ red(X3,n7)
| ~ 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,n7)
| ~ red(X2,n7)
| ~ red(X1,n7)
| ~ red(X0,X1)
| ~ red(X0,X2) ) ).
cnf(u1396,axiom,
less_than(n6,n8) ).
cnf(u58,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n6) ) ).
cnf(u421,axiom,
less_than(n2,n4) ).
cnf(u11060,axiom,
( ~ red(X2,n14)
| ~ red(X2,n6)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X2,n11)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X2,X1)
| ~ red(X2,X0) ) ).
cnf(u2470,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n12) ) ).
cnf(u17923,axiom,
( ~ red(n2,X0)
| ~ red(X0,n5)
| ~ red(X0,n7)
| ~ red(X0,n8)
| ~ red(X0,n4) ) ).
cnf(u18121,axiom,
( ~ green(n3,X1)
| ~ green(X1,n11)
| ~ green(X0,n11)
| ~ green(X1,n10)
| ~ green(X0,n10)
| ~ green(n3,X0)
| ~ green(X0,X1) ) ).
cnf(u18387,axiom,
( ~ red(n1,X0)
| ~ red(X0,n13)
| ~ red(X0,n14)
| ~ red(X0,n11) ) ).
cnf(u1197,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n6) ) ).
cnf(u18122,axiom,
( ~ green(X2,n11)
| ~ green(X2,n3)
| ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X2,n9)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X2,X1)
| ~ green(X2,X0) ) ).
cnf(u55,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n3) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA025+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 % Computer : n016.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 08:54:47 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 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
% 5.17/1.30 % (2333524)Will run a generic schedule for satisfiability detection.
% 5.17/1.30 % (2333531)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1589256278:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.17/1.30 % (2333530)% WARNING: option uhcvi not known.
% 5.17/1.30 % (2333532)dis+10_1_sil=32000:sp=arity:random_seed=2754790656:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.17/1.30 % (2333529)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=811949552_2999 on theBenchmark for (2999ds/0Mi)
% 5.17/1.30 % (2333530)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2254377326:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.17/1.30 % (2333533)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3467784709:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.17/1.30 % (2333535)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1440961912:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.17/1.30 % (2333534)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2968712324:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.17/1.30 % Detected minimum model sizes of [1]
% 5.17/1.30 % Detected maximum model sizes of [14]
% 5.17/1.30 % TRYING [1]
% 5.17/1.30 % TRYING [2]
% 5.17/1.30 % TRYING [3]
% 5.17/1.30 % TRYING [4]
% 5.17/1.30 % TRYING [5]
% 5.17/1.30 % (2333533)Instruction limit reached!
% 5.17/1.30 % (2333533)------------------------------
% 5.17/1.30 % (2333533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.30 % (2333533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.30 % (2333533)CaDiCaL version: 2.1.3
% 5.17/1.30 % (2333533)Termination reason: Instruction limit
% 5.17/1.30 % (2333533)Termination phase: Saturation
% 5.17/1.30 % (2333533)Time elapsed: 0.040 s
% 5.17/1.30 % (2333533)Peak memory usage: 11 MB
% 5.17/1.30 % (2333533)Instructions burned: 117 (million)
% 5.17/1.30 % (2333532)Instruction limit reached!
% 5.17/1.30 % (2333532)------------------------------
% 5.17/1.30 % (2333532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.30 % (2333532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.30 % (2333532)CaDiCaL version: 2.1.3
% 5.17/1.30 % (2333532)Termination reason: Instruction limit
% 5.17/1.30 % (2333532)Termination phase: Saturation
% 5.17/1.30 % (2333532)Time elapsed: 0.043 s
% 5.17/1.30 % (2333532)Peak memory usage: 12 MB
% 5.17/1.30 % (2333532)Instructions burned: 103 (million)
% 5.17/1.30 % (2333534)Instruction limit reached!
% 5.17/1.30 % (2333534)------------------------------
% 5.17/1.30 % (2333534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.30 % (2333534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.30 % (2333534)CaDiCaL version: 2.1.3
% 5.17/1.30 % (2333534)Termination reason: Instruction limit
% 5.17/1.30 % (2333534)Termination phase: Saturation
% 5.17/1.30 % (2333534)Time elapsed: 0.051 s
% 5.17/1.30 % (2333534)Peak memory usage: 11 MB
% 5.17/1.30 % (2333534)Instructions burned: 134 (million)
% 5.17/1.30 % (2333535)Instruction limit reached!
% 5.17/1.30 % (2333535)------------------------------
% 5.17/1.30 % (2333535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.17/1.30 % (2333535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.17/1.30 % (2333535)CaDiCaL version: 2.1.3
% 5.17/1.30 % (2333535)Termination reason: Instruction limit
% 5.17/1.30 % (2333535)Termination phase: Saturation
% 5.17/1.30 % (2333535)Time elapsed: 0.058 s
% 5.17/1.30 % (2333535)Peak memory usage: 12 MB
% 5.17/1.30 % (2333535)Instructions burned: 167 (million)
% 5.17/1.30 % (2333543)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=261780657:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.17/1.30 % Detected minimum model sizes of [1]
% 5.17/1.30 % Detected maximum model sizes of [14]
% 5.17/1.30 % TRYING [1]
% 5.17/1.30 % (2333544)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=574824844:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.17/1.30 % TRYING [2]
% 5.17/1.30 % TRYING [3]
% 5.17/1.30 % TRYING [4]
% 5.17/1.30 % (2333545)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=3842469126:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.17/1.30 % (2333546)ott-21_1_sil=16000:fs=off:random_seed=4109955853:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.17/1.30 % TRYING [5]
% 5.17/1.30 % TRYING [6]
% 5.97/1.43 % (2333544)Instruction limit reached!
% 5.97/1.43 % (2333544)------------------------------
% 5.97/1.43 % (2333544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333544)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333544)Termination reason: Instruction limit
% 5.97/1.43 % (2333544)Termination phase: Saturation
% 5.97/1.43 % (2333544)Time elapsed: 0.049 s
% 5.97/1.43 % (2333544)Peak memory usage: 12 MB
% 5.97/1.43 % (2333544)Instructions burned: 132 (million)
% 5.97/1.43 % (2333551)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=230200286:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.97/1.43 % (2333546)Instruction limit reached!
% 5.97/1.43 % (2333546)------------------------------
% 5.97/1.43 % (2333546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333546)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333546)Termination reason: Instruction limit
% 5.97/1.43 % (2333546)Termination phase: Saturation
% 5.97/1.43 % (2333546)Time elapsed: 0.088 s
% 5.97/1.43 % (2333546)Peak memory usage: 13 MB
% 5.97/1.43 % (2333546)Instructions burned: 182 (million)
% 5.97/1.43 % TRYING [6]
% 5.97/1.43 % (2333553)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1493388646:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.97/1.43 % Detected minimum model sizes of [1]
% 5.97/1.43 % Detected maximum model sizes of [14]
% 5.97/1.43 % TRYING [1]
% 5.97/1.43 % TRYING [2]
% 5.97/1.43 % TRYING [3]
% 5.97/1.43 % TRYING [4]
% 5.97/1.43 % TRYING [5]
% 5.97/1.43 % (2333543)Instruction limit reached!
% 5.97/1.43 % (2333543)------------------------------
% 5.97/1.43 % (2333543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333543)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333543)Termination reason: Instruction limit
% 5.97/1.43 % (2333543)Termination phase: Finite model building constraint generation
% 5.97/1.43 % (2333543)Time elapsed: 0.251 s
% 5.97/1.43 % (2333543)Peak memory usage: 20 MB
% 5.97/1.43 % (2333543)Instructions burned: 717 (million)
% 5.97/1.43 % (2333551)Instruction limit reached!
% 5.97/1.43 % (2333551)------------------------------
% 5.97/1.43 % (2333551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333551)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333551)Termination reason: Instruction limit
% 5.97/1.43 % (2333551)Termination phase: Saturation
% 5.97/1.43 % (2333551)Time elapsed: 0.180 s
% 5.97/1.43 % (2333551)Peak memory usage: 12 MB
% 5.97/1.43 % (2333551)Instructions burned: 478 (million)
% 5.97/1.43 % TRYING [6]
% 5.97/1.43 % (2333555)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3211659457:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 5.97/1.43 % (2333556)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3453976095:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 5.97/1.43 % Detected minimum model sizes of [1]
% 5.97/1.43 % Detected maximum model sizes of [14]
% 5.97/1.43 % TRYING [14]
% 5.97/1.43 % TRYING [7]
% 5.97/1.43 % (2333545)Instruction limit reached!
% 5.97/1.43 % (2333545)------------------------------
% 5.97/1.43 % (2333545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333545)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333545)Termination reason: Instruction limit
% 5.97/1.43 % (2333545)Termination phase: Saturation
% 5.97/1.43 % (2333545)Time elapsed: 0.291 s
% 5.97/1.43 % (2333545)Peak memory usage: 14 MB
% 5.97/1.43 % (2333545)Instructions burned: 686 (million)
% 5.97/1.43 % (2333559)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=1284538462:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 5.97/1.43 % (2333553)Instruction limit reached!
% 5.97/1.43 % (2333553)------------------------------
% 5.97/1.43 % (2333553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333553)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333553)Termination reason: Instruction limit
% 5.97/1.43 % (2333553)Termination phase: Finite model building constraint generation
% 5.97/1.43 % (2333553)Time elapsed: 0.305 s
% 5.97/1.43 % (2333553)Peak memory usage: 24 MB
% 5.97/1.43 % (2333553)Instructions burned: 865 (million)
% 5.97/1.43 % (2333561)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1823836094:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.97/1.43 % (2333556)Instruction limit reached!
% 5.97/1.43 % (2333556)------------------------------
% 5.97/1.43 % (2333556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333556)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333556)Termination reason: Instruction limit
% 5.97/1.43 % (2333556)Termination phase: Finite model building constraint generation
% 5.97/1.43 % (2333556)Time elapsed: 0.276 s
% 5.97/1.43 % (2333556)Peak memory usage: 34 MB
% 5.97/1.43 % (2333556)Instructions burned: 889 (million)
% 5.97/1.43 % (2333559)Instruction limit reached!
% 5.97/1.43 % (2333559)------------------------------
% 5.97/1.43 % (2333559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333559)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333559)Termination reason: Instruction limit
% 5.97/1.43 % (2333559)Termination phase: Saturation
% 5.97/1.43 % (2333559)Time elapsed: 0.237 s
% 5.97/1.43 % (2333559)Peak memory usage: 14 MB
% 5.97/1.43 % (2333559)Instructions burned: 692 (million)
% 5.97/1.43 % (2333563)fmb+10_1_sil=64000:random_seed=1137773706:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 5.97/1.43 % Detected minimum model sizes of [1]
% 5.97/1.43 % Detected maximum model sizes of [14]
% 5.97/1.43 % TRYING [1]
% 5.97/1.43 % TRYING [2]
% 5.97/1.43 % TRYING [3]
% 5.97/1.43 % TRYING [4]
% 5.97/1.43 % (2333564)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3576939376:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 5.97/1.43 % Detected minimum model sizes of [1]
% 5.97/1.43 % Detected maximum model sizes of [14]
% 5.97/1.43 % fmb_start_size (= 20) larger than a detected sort maximum size!
% 5.97/1.43 % (2333564)Refutation not found, incomplete strategy
% 5.97/1.43 % (2333564)------------------------------
% 5.97/1.43 % (2333564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333564)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333564)Termination reason: Refutation not found, incomplete strategy
% 5.97/1.43 % (2333564)Time elapsed: 0.001 s
% 5.97/1.43 % (2333564)Peak memory usage: 10 MB
% 5.97/1.43 % (2333564)Instructions burned: 1 (million)
% 5.97/1.43 % (2333564)------------------------------
% 5.97/1.43 % (2333564)------------------------------
% 5.97/1.43 % (2333567)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3683136307:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 5.97/1.43 % Detected minimum model sizes of [1]
% 5.97/1.43 % Detected maximum model sizes of [14]
% 5.97/1.43 % TRYING [8]
% 5.97/1.43 % TRYING [5]
% 5.97/1.43 % TRYING [6]
% 5.97/1.43 % (2333555)Instruction limit reached!
% 5.97/1.43 % (2333555)------------------------------
% 5.97/1.43 % (2333555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333555)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333555)Termination reason: Instruction limit
% 5.97/1.43 % (2333555)Termination phase: Saturation
% 5.97/1.43 % (2333555)Time elapsed: 0.460 s
% 5.97/1.43 % (2333555)Peak memory usage: 14 MB
% 5.97/1.43 % (2333555)Instructions burned: 1181 (million)
% 5.97/1.43 % (2333561)Instruction limit reached!
% 5.97/1.43 % (2333561)------------------------------
% 5.97/1.43 % (2333561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.43 % (2333561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.43 % (2333561)CaDiCaL version: 2.1.3
% 5.97/1.43 % (2333561)Termination reason: Instruction limit
% 5.97/1.43 % (2333561)Termination phase: Saturation
% 5.97/1.43 % (2333561)Time elapsed: 0.291 s
% 5.97/1.43 % (2333561)Peak memory usage: 12 MB
% 5.97/1.43 % (2333561)Instructions burned: 881 (million)
% 5.97/1.43 % (2333569)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2583311835:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 5.97/1.43 % (2333570)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=985618397:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 5.97/1.43 % (2333531) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2333524-2333531"...
% 5.97/1.43 % (2333531)...printing done.
% 5.97/1.43 % SZS status CounterSatisfiable for theBenchmark
% 5.97/1.43 % SZS output start Saturation.
% See solution above
% 5.97/1.44 % SZS output start Definitions and Model Updates.
% 5.97/1.44 % SZS output end Definitions and Model Updates.
% 5.97/1.44 % (2333531)------------------------------
% 5.97/1.44 % (2333531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.97/1.44 % (2333531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.97/1.44 % (2333531)CaDiCaL version: 2.1.3
% 5.97/1.44 % (2333531)Termination reason: Satisfiable
% 5.97/1.44 % (2333531)Time elapsed: 0.958 s
% 5.97/1.44 % (2333531)Peak memory usage: 20 MB
% 5.97/1.44 % (2333531)Instructions burned: 4351 (million)
% 5.97/1.44 % (2333524)Success in time 0.992 s
% 5.97/1.44 % Vampire exiting
%------------------------------------------------------------------------------