%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRA018+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 09:55:22 AM UTC 2026
% Result : CounterSatisfiable 159.90s 23.47s
% Output : Saturation 160.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u78,axiom,
red(n16,n17) ).
cnf(u41102,axiom,
~ green(n16,n17) ).
cnf(u45280,axiom,
~ red(n15,n16) ).
cnf(u88,axiom,
green(n15,n16) ).
cnf(u92,axiom,
red(n14,n15) ).
cnf(u6027,axiom,
~ green(n14,n15) ).
cnf(u4998,axiom,
~ red(n13,n14) ).
cnf(u102,axiom,
green(n13,n14) ).
cnf(u106,axiom,
red(n12,n13) ).
cnf(u11140,axiom,
~ green(n12,n13) ).
cnf(u113,axiom,
red(n11,n12) ).
cnf(u1645,axiom,
~ green(n11,n12) ).
cnf(u6285,axiom,
~ red(n10,n11) ).
cnf(u123,axiom,
green(n10,n11) ).
cnf(u898,axiom,
~ red(n9,n10) ).
cnf(u130,axiom,
green(n9,n10) ).
cnf(u21099,axiom,
~ red(n8,n9) ).
cnf(u137,axiom,
green(n8,n9) ).
cnf(u141,axiom,
red(n7,n8) ).
cnf(u3044,axiom,
~ green(n7,n8) ).
cnf(u1318,axiom,
~ red(n6,n7) ).
cnf(u151,axiom,
green(n6,n7) ).
cnf(u155,axiom,
red(n5,n6) ).
cnf(u2635,axiom,
~ green(n5,n6) ).
cnf(u162,axiom,
red(n4,n5) ).
cnf(u10251,axiom,
~ green(n4,n5) ).
cnf(u1820,axiom,
~ red(n3,n4) ).
cnf(u172,axiom,
green(n3,n4) ).
cnf(u9977,axiom,
~ red(n2,n3) ).
cnf(u179,axiom,
green(n2,n3) ).
cnf(u9004,axiom,
~ red(n1,n2) ).
cnf(u186,axiom,
green(n1,n2) ).
cnf(u211,negated_conjecture,
~ red(n2,n2) ).
cnf(u218,axiom,
red(n11,n13) ).
cnf(u10824,axiom,
~ green(n11,n13) ).
cnf(u7184,axiom,
~ red(n13,n15) ).
cnf(u232,axiom,
green(n13,n15) ).
cnf(u241,axiom,
red(n10,n12) ).
cnf(u11774,axiom,
~ green(n10,n12) ).
cnf(u254,axiom,
red(n7,n9) ).
cnf(u1605,axiom,
~ green(n7,n9) ).
cnf(u844,axiom,
~ red(n12,n14) ).
cnf(u270,axiom,
green(n12,n14) ).
cnf(u278,axiom,
red(n11,n14) ).
cnf(u1673,axiom,
~ green(n11,n14) ).
cnf(u6668,axiom,
~ red(n11,n15) ).
cnf(u290,axiom,
green(n11,n15) ).
cnf(u13876,axiom,
~ red(n6,n8) ).
cnf(u306,axiom,
green(n6,n8) ).
cnf(u315,axiom,
red(n9,n11) ).
cnf(u1301,axiom,
~ green(n9,n11) ).
cnf(u2624,axiom,
~ red(n5,n7) ).
cnf(u330,axiom,
green(n5,n7) ).
cnf(u340,axiom,
red(n8,n10) ).
cnf(u5981,axiom,
~ green(n8,n10) ).
cnf(u1585,axiom,
~ red(n7,n10) ).
cnf(u354,axiom,
green(n7,n10) ).
cnf(u1614,axiom,
~ red(n7,n11) ).
cnf(u364,axiom,
green(n7,n11) ).
cnf(u842,axiom,
~ red(n7,n12) ).
cnf(u378,axiom,
green(n7,n12) ).
cnf(u9976,axiom,
~ red(n3,n5) ).
cnf(u392,axiom,
green(n3,n5) ).
cnf(u402,axiom,
red(n4,n6) ).
cnf(u4240,axiom,
~ green(n4,n6) ).
cnf(u11788,axiom,
~ red(n3,n6) ).
cnf(u416,axiom,
green(n3,n6) ).
cnf(u423,axiom,
red(n3,n7) ).
cnf(u1298,axiom,
~ green(n3,n7) ).
cnf(u937,axiom,
~ red(n3,n8) ).
cnf(u440,axiom,
green(n3,n8) ).
cnf(u450,axiom,
red(n1,n3) ).
cnf(u3096,axiom,
~ green(n1,n3) ).
cnf(u9770,axiom,
~ red(n2,n4) ).
cnf(u468,axiom,
green(n2,n4) ).
cnf(u2140,axiom,
~ red(n1,n4) ).
cnf(u479,axiom,
green(n1,n4) ).
cnf(u486,axiom,
red(n1,n5) ).
cnf(u1004,axiom,
~ green(n1,n5) ).
cnf(u500,axiom,
red(n1,n6) ).
cnf(u2662,axiom,
~ green(n1,n6) ).
cnf(u511,axiom,
red(n7,n13) ).
cnf(u865,axiom,
~ green(n7,n13) ).
cnf(u4033,axiom,
~ red(n1,n7) ).
cnf(u524,axiom,
green(n1,n7) ).
cnf(u534,negated_conjecture,
~ red(n4,n4) ).
cnf(u546,negated_conjecture,
~ red(n6,n6) ).
cnf(u563,negated_conjecture,
~ red(n10,n10) ).
cnf(u576,negated_conjecture,
~ red(n12,n12) ).
cnf(u585,negated_conjecture,
~ red(n15,n15) ).
cnf(u595,negated_conjecture,
~ red(n11,n11) ).
cnf(u607,negated_conjecture,
~ red(n14,n14) ).
cnf(u621,negated_conjecture,
~ red(n8,n8) ).
cnf(u631,negated_conjecture,
( ~ red(X0,n6)
| ~ red(n4,X0)
| ~ red(X0,n5) ) ).
cnf(u639,axiom,
red(n3,n9) ).
cnf(u1020,axiom,
~ green(n3,n9) ).
cnf(u1241,negated_conjecture,
red(n3,n10) ).
cnf(u679,negated_conjecture,
( ~ green(X0,n7)
| ~ green(n6,X0)
| ~ green(X0,n8) ) ).
cnf(u688,negated_conjecture,
~ green(n6,n6) ).
cnf(u696,negated_conjecture,
~ red(n7,n14) ).
cnf(u708,negated_conjecture,
~ green(n4,n4) ).
cnf(u717,negated_conjecture,
~ green(n7,n7) ).
cnf(u727,axiom,
red(n7,n15) ).
cnf(u2496,axiom,
~ green(n7,n15) ).
cnf(u740,axiom,
red(n1,n8) ).
cnf(u2785,axiom,
~ green(n1,n8) ).
cnf(u27369,axiom,
~ red(n1,n9) ).
cnf(u753,axiom,
green(n1,n9) ).
cnf(u760,axiom,
red(n1,n10) ).
cnf(u3802,axiom,
~ green(n1,n10) ).
cnf(u1407,axiom,
~ red(n1,n11) ).
cnf(u773,axiom,
green(n1,n11) ).
cnf(u2604,axiom,
~ red(n1,n12) ).
cnf(u783,axiom,
green(n1,n12) ).
cnf(u790,axiom,
red(n1,n13) ).
cnf(u2761,axiom,
~ green(n1,n13) ).
cnf(u800,axiom,
red(n1,n14) ).
cnf(u12906,axiom,
~ green(n1,n14) ).
cnf(u809,axiom,
red(n1,n15) ).
cnf(u1722,axiom,
~ green(n1,n15) ).
cnf(u847,negated_conjecture,
( ~ red(n12,X0)
| ~ red(X0,n13)
| ~ red(X0,n14) ) ).
cnf(u878,negated_conjecture,
~ green(n14,n14) ).
cnf(u908,negated_conjecture,
~ green(n9,n9) ).
cnf(u914,negated_conjecture,
( ~ green(n11,X0)
| ~ green(X0,n13)
| ~ green(X0,n15) ) ).
cnf(u924,negated_conjecture,
~ green(n12,n12) ).
cnf(u6193,axiom,
~ red(n3,n11) ).
cnf(u952,axiom,
green(n3,n11) ).
cnf(u959,axiom,
red(n3,n12) ).
cnf(u1135,axiom,
~ green(n3,n12) ).
cnf(u969,axiom,
red(n3,n13) ).
cnf(u3248,axiom,
~ green(n3,n13) ).
cnf(u979,axiom,
red(n3,n14) ).
cnf(u5446,axiom,
~ green(n3,n14) ).
cnf(u4502,axiom,
~ red(n3,n15) ).
cnf(u991,axiom,
green(n3,n15) ).
cnf(u1019,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u4230,negated_conjecture,
red(n6,n10) ).
cnf(u1696,negated_conjecture,
red(n8,n11) ).
cnf(u1054,negated_conjecture,
( ~ red(n8,X0)
| ~ red(X0,n9)
| ~ red(X0,n11) ) ).
cnf(u2538,negated_conjecture,
red(n4,n7) ).
cnf(u1065,negated_conjecture,
( ~ red(X0,n5)
| ~ red(n4,X0)
| ~ red(X0,n7) ) ).
cnf(u4748,negated_conjecture,
green(n8,n12) ).
cnf(u1084,negated_conjecture,
~ green(n8,n13) ).
cnf(u1115,negated_conjecture,
~ red(n8,n14) ).
cnf(u1122,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X0,n9)
| ~ red(X0,n8) ) ).
cnf(u1130,negated_conjecture,
~ green(n9,n12) ).
cnf(u1133,negated_conjecture,
( ~ green(n9,X0)
| ~ green(X0,n10)
| ~ green(X0,n12) ) ).
cnf(u1150,axiom,
red(n8,n15) ).
cnf(u1712,axiom,
~ green(n8,n15) ).
cnf(u5320,axiom,
~ red(n12,n15) ).
cnf(u1163,axiom,
green(n12,n15) ).
cnf(u16829,axiom,
~ red(n9,n13) ).
cnf(u1179,axiom,
green(n9,n13) ).
cnf(u1770,negated_conjecture,
red(n9,n14) ).
cnf(u1209,negated_conjecture,
( ~ green(n12,X0)
| ~ green(X0,n13)
| ~ green(X0,n15) ) ).
cnf(u1225,axiom,
red(n9,n15) ).
cnf(u2270,axiom,
~ green(n9,n15) ).
cnf(u1929,axiom,
~ green(n3,n10) ).
cnf(u3846,negated_conjecture,
green(n10,n13) ).
cnf(u1259,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n11)
| ~ green(X0,n13) ) ).
cnf(u1270,negated_conjecture,
~ green(n8,n7) ).
cnf(u1280,negated_conjecture,
~ red(n7,n6) ).
cnf(u1288,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X0,n9)
| ~ green(X0,n7) ) ).
cnf(u1304,negated_conjecture,
( ~ green(n9,X0)
| ~ green(X0,n10)
| ~ green(X0,n11) ) ).
cnf(u1316,negated_conjecture,
~ red(n7,n7) ).
cnf(u1420,negated_conjecture,
~ green(n11,n11) ).
cnf(u9156,axiom,
~ red(n5,n8) ).
cnf(u1430,axiom,
green(n5,n8) ).
cnf(u1439,negated_conjecture,
~ red(n5,n10) ).
cnf(u20245,axiom,
~ red(n5,n9) ).
cnf(u1453,axiom,
green(n5,n9) ).
cnf(u1675,negated_conjecture,
red(n5,n11) ).
cnf(u1474,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u1850,negated_conjecture,
green(n5,n12) ).
cnf(u1486,negated_conjecture,
~ green(n5,n11) ).
cnf(u1511,axiom,
red(n5,n13) ).
cnf(u4653,axiom,
~ green(n5,n13) ).
cnf(u1521,axiom,
red(n5,n14) ).
cnf(u1540,axiom,
~ green(n5,n14) ).
cnf(u5328,axiom,
~ red(n5,n15) ).
cnf(u1533,axiom,
green(n5,n15) ).
cnf(u1580,negated_conjecture,
~ red(n10,n14) ).
cnf(u1588,negated_conjecture,
( ~ red(n7,X0)
| ~ red(X0,n8)
| ~ red(X0,n10) ) ).
cnf(u1608,negated_conjecture,
( ~ green(X0,n9)
| ~ green(n7,X0)
| ~ green(X0,n8) ) ).
cnf(u1649,negated_conjecture,
~ green(n12,n11) ).
cnf(u1684,negated_conjecture,
~ green(n5,n5) ).
cnf(u1693,axiom,
red(n8,n13) ).
cnf(u1701,axiom,
~ green(n8,n11) ).
cnf(u1733,negated_conjecture,
~ green(n15,n15) ).
cnf(u1736,negated_conjecture,
~ green(n15,n13) ).
cnf(u5643,axiom,
~ green(n9,n14) ).
cnf(u1794,axiom,
green(n5,n10) ).
cnf(u1855,axiom,
~ red(n5,n12) ).
cnf(u2491,negated_conjecture,
green(n10,n15) ).
cnf(u1925,negated_conjecture,
~ green(n3,n3) ).
cnf(u1938,negated_conjecture,
~ green(n6,n9) ).
cnf(u1941,negated_conjecture,
( ~ green(X0,n7)
| ~ green(n6,X0)
| ~ green(X0,n9) ) ).
cnf(u1980,negated_conjecture,
~ green(n4,n9) ).
cnf(u1990,axiom,
red(n4,n8) ).
cnf(u2949,axiom,
~ green(n4,n8) ).
cnf(u2000,negated_conjecture,
~ green(n4,n10) ).
cnf(u2561,negated_conjecture,
red(n4,n10) ).
cnf(u2031,axiom,
red(n4,n11) ).
cnf(u2100,axiom,
~ green(n4,n11) ).
cnf(u2216,axiom,
~ red(n4,n12) ).
cnf(u2044,axiom,
green(n4,n12) ).
cnf(u9890,axiom,
~ red(n4,n13) ).
cnf(u2055,axiom,
green(n4,n13) ).
cnf(u5168,axiom,
~ red(n4,n14) ).
cnf(u2065,axiom,
green(n4,n14) ).
cnf(u5353,axiom,
~ red(n4,n15) ).
cnf(u2074,axiom,
green(n4,n15) ).
cnf(u2104,negated_conjecture,
~ green(n7,n4) ).
cnf(u2117,axiom,
red(n4,n9) ).
cnf(u2128,negated_conjecture,
~ green(n4,n3) ).
cnf(u2143,negated_conjecture,
( ~ red(X0,n2)
| ~ red(n1,X0)
| ~ red(X0,n4) ) ).
cnf(u2168,axiom,
green(n8,n14) ).
cnf(u2179,axiom,
green(n10,n14) ).
cnf(u2279,negated_conjecture,
~ green(n13,n11) ).
cnf(u2282,negated_conjecture,
~ green(n13,n10) ).
cnf(u2294,negated_conjecture,
~ green(n14,n11) ).
cnf(u2297,negated_conjecture,
~ green(n14,n10) ).
cnf(u9003,axiom,
~ red(n2,n5) ).
cnf(u2307,axiom,
green(n2,n5) ).
cnf(u2314,negated_conjecture,
~ red(n2,n6) ).
cnf(u2321,negated_conjecture,
~ red(n2,n7) ).
cnf(u3304,negated_conjecture,
green(n2,n9) ).
cnf(u2355,negated_conjecture,
~ green(n4,n2) ).
cnf(u2362,axiom,
red(n2,n8) ).
cnf(u3318,axiom,
~ green(n2,n8) ).
cnf(u2372,negated_conjecture,
~ green(n2,n10) ).
cnf(u2390,axiom,
red(n2,n11) ).
cnf(u2810,axiom,
~ green(n2,n11) ).
cnf(u2400,axiom,
red(n2,n12) ).
cnf(u5718,axiom,
~ green(n2,n12) ).
cnf(u22244,axiom,
~ red(n2,n13) ).
cnf(u2413,axiom,
green(n2,n13) ).
cnf(u2420,axiom,
red(n2,n14) ).
cnf(u11448,axiom,
~ green(n2,n14) ).
cnf(u2429,axiom,
red(n2,n15) ).
cnf(u2585,axiom,
~ green(n2,n15) ).
cnf(u2477,axiom,
red(n2,n10) ).
cnf(u5348,axiom,
~ red(n10,n15) ).
cnf(u5258,axiom,
~ green(n4,n7) ).
cnf(u2569,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X0,n13)
| ~ green(X0,n11) ) ).
cnf(u2590,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X0,n14)
| ~ green(X0,n13) ) ).
cnf(u2661,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X0,n7)
| ~ green(X0,n6) ) ).
cnf(u2667,axiom,
green(n2,n7) ).
cnf(u2672,axiom,
green(n7,n14) ).
cnf(u2760,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X0,n14)
| ~ green(X0,n13) ) ).
cnf(u2819,negated_conjecture,
( ~ red(X0,n6)
| ~ red(n1,X0)
| ~ red(X0,n5) ) ).
cnf(u2823,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X0,n8)
| ~ red(X0,n6) ) ).
cnf(u2847,negated_conjecture,
~ green(n13,n13) ).
cnf(u2855,negated_conjecture,
( ~ green(n13,X0)
| ~ green(X0,n14)
| ~ green(X0,n15) ) ).
cnf(u2880,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X0,n13)
| ~ green(X0,n12) ) ).
cnf(u2912,negated_conjecture,
~ green(n15,n11) ).
cnf(u2915,negated_conjecture,
~ green(n15,n10) ).
cnf(u3030,negated_conjecture,
( ~ red(X0,n11)
| ~ red(n2,X0)
| ~ red(X0,n12) ) ).
cnf(u3043,negated_conjecture,
~ green(n8,n8) ).
cnf(u3099,negated_conjecture,
( ~ green(X0,n2)
| ~ green(n1,X0)
| ~ green(X0,n3) ) ).
cnf(u3138,negated_conjecture,
~ green(n10,n10) ).
cnf(u15664,axiom,
~ red(n2,n9) ).
cnf(u3321,negated_conjecture,
~ green(n7,n2) ).
cnf(u3347,axiom,
red(n9,n12) ).
cnf(u3432,negated_conjecture,
( ~ green(X0,n5)
| ~ green(n3,X0)
| ~ green(X0,n4) ) ).
cnf(u3609,negated_conjecture,
~ green(n10,n9) ).
cnf(u3619,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X0,n14)
| ~ green(X0,n13) ) ).
cnf(u3841,negated_conjecture,
( ~ red(X0,n9)
| ~ red(n8,X0)
| ~ red(X0,n10) ) ).
cnf(u11630,axiom,
~ red(n10,n13) ).
cnf(u3935,negated_conjecture,
~ red(n14,n10) ).
cnf(u3942,negated_conjecture,
~ red(n13,n10) ).
cnf(u3945,negated_conjecture,
~ red(n13,n8) ).
cnf(u3990,negated_conjecture,
~ red(n11,n10) ).
cnf(u4018,negated_conjecture,
( ~ red(X0,n9)
| ~ red(n4,X0)
| ~ red(X0,n7) ) ).
cnf(u4023,negated_conjecture,
( ~ red(X0,n9)
| ~ red(n3,X0)
| ~ red(X0,n7) ) ).
cnf(u4074,axiom,
red(n6,n9) ).
cnf(u4286,negated_conjecture,
green(n6,n11) ).
cnf(u4103,negated_conjecture,
~ green(n6,n12) ).
cnf(u4114,axiom,
red(n6,n12) ).
cnf(u9390,axiom,
~ red(n6,n13) ).
cnf(u4125,axiom,
green(n6,n13) ).
cnf(u4271,axiom,
~ red(n6,n14) ).
cnf(u4135,axiom,
green(n6,n14) ).
cnf(u4142,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X0,n14)
| ~ green(X0,n13) ) ).
cnf(u4147,negated_conjecture,
~ green(n6,n15) ).
cnf(u4209,negated_conjecture,
~ green(n5,n4) ).
cnf(u4353,axiom,
~ green(n6,n10) ).
cnf(u4243,negated_conjecture,
( ~ green(X0,n5)
| ~ green(n4,X0)
| ~ green(X0,n6) ) ).
cnf(u6250,axiom,
~ red(n6,n11) ).
cnf(u4300,axiom,
green(n2,n6) ).
cnf(u4304,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X0,n7)
| ~ green(X0,n6) ) ).
cnf(u4329,axiom,
red(n6,n15) ).
cnf(u4384,negated_conjecture,
( ~ red(X0,n9)
| ~ red(n6,X0)
| ~ red(X0,n7) ) ).
cnf(u4554,negated_conjecture,
( ~ red(n9,X0)
| ~ red(X0,n11)
| ~ red(X0,n12) ) ).
cnf(u4750,axiom,
~ red(n8,n12) ).
cnf(u4753,negated_conjecture,
( ~ red(n8,X0)
| ~ red(X0,n11)
| ~ red(X0,n12) ) ).
cnf(u4861,negated_conjecture,
~ green(n7,n3) ).
cnf(u4885,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X0,n15)
| ~ red(X0,n14) ) ).
cnf(u4917,negated_conjecture,
~ red(n12,n10) ).
cnf(u4949,negated_conjecture,
~ green(n6,n5) ).
cnf(u4984,negated_conjecture,
~ green(n6,n3) ).
cnf(u5158,negated_conjecture,
~ green(n14,n12) ).
cnf(u5239,negated_conjecture,
~ red(n15,n10) ).
cnf(u5261,negated_conjecture,
( ~ green(X0,n7)
| ~ green(n4,X0)
| ~ green(X0,n5) ) ).
cnf(u5433,negated_conjecture,
( ~ green(X0,n7)
| ~ green(n5,X0)
| ~ green(X0,n6) ) ).
cnf(u5444,negated_conjecture,
( ~ green(n6,X0)
| ~ green(X0,n13)
| ~ green(X0,n14) ) ).
cnf(u5721,negated_conjecture,
~ green(n5,n2) ).
cnf(u5785,negated_conjecture,
~ green(n4,n1) ).
cnf(u5984,negated_conjecture,
( ~ green(n8,X0)
| ~ green(X0,n9)
| ~ green(X0,n10) ) ).
cnf(u5998,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X0,n12)
| ~ red(X0,n11) ) ).
cnf(u6030,negated_conjecture,
~ green(n14,n13) ).
cnf(u6192,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X0,n12)
| ~ red(X0,n11) ) ).
cnf(u6649,negated_conjecture,
( ~ red(X0,n3)
| ~ red(n1,X0)
| ~ red(X0,n2) ) ).
cnf(u7187,negated_conjecture,
( ~ red(n13,X0)
| ~ red(X0,n14)
| ~ red(X0,n15) ) ).
cnf(u7212,negated_conjecture,
~ green(n7,n6) ).
cnf(u7326,negated_conjecture,
~ green(n6,n1) ).
cnf(u7419,negated_conjecture,
~ red(n3,n3) ).
cnf(u7784,negated_conjecture,
~ red(n12,n11) ).
cnf(u7874,negated_conjecture,
~ green(n13,n9) ).
cnf(u8095,negated_conjecture,
~ red(n14,n11) ).
cnf(u8102,negated_conjecture,
~ red(n13,n11) ).
cnf(u8105,negated_conjecture,
~ red(n13,n9) ).
cnf(u8229,negated_conjecture,
~ red(n15,n14) ).
cnf(u8232,negated_conjecture,
~ red(n15,n13) ).
cnf(u8327,negated_conjecture,
~ red(n13,n12) ).
cnf(u8391,axiom,
red(n15,n17) ).
cnf(u41300,axiom,
~ green(n15,n17) ).
cnf(u8405,negated_conjecture,
~ green(n16,n15) ).
cnf(u8425,axiom,
red(n14,n16) ).
cnf(u41100,axiom,
~ green(n14,n16) ).
cnf(u40548,axiom,
~ red(n13,n16) ).
cnf(u8435,axiom,
green(n13,n16) ).
cnf(u63897,axiom,
~ red(n12,n16) ).
cnf(u8442,axiom,
green(n12,n16) ).
cnf(u65612,axiom,
~ red(n11,n16) ).
cnf(u8449,axiom,
green(n11,n16) ).
cnf(u8453,axiom,
red(n10,n16) ).
cnf(u40213,axiom,
~ green(n10,n16) ).
cnf(u41901,axiom,
~ red(n9,n16) ).
cnf(u8463,axiom,
green(n9,n16) ).
cnf(u41895,axiom,
~ red(n8,n16) ).
cnf(u8470,axiom,
green(n8,n16) ).
cnf(u8474,axiom,
red(n7,n16) ).
cnf(u51285,axiom,
~ green(n7,n16) ).
cnf(u40192,axiom,
~ red(n6,n16) ).
cnf(u8484,axiom,
green(n6,n16) ).
cnf(u8488,axiom,
red(n5,n16) ).
cnf(u51041,axiom,
~ green(n5,n16) ).
cnf(u8495,axiom,
red(n4,n16) ).
cnf(u40146,axiom,
~ green(n4,n16) ).
cnf(u8502,axiom,
red(n3,n16) ).
cnf(u41986,axiom,
~ green(n3,n16) ).
cnf(u8509,axiom,
red(n2,n16) ).
cnf(u41683,axiom,
~ green(n2,n16) ).
cnf(u41462,axiom,
~ red(n1,n16) ).
cnf(u8519,axiom,
green(n1,n16) ).
cnf(u41095,negated_conjecture,
green(n14,n17) ).
cnf(u8528,negated_conjecture,
( ~ green(n14,X0)
| ~ green(X0,n16)
| ~ green(X0,n17) ) ).
cnf(u41090,negated_conjecture,
green(n1,n17) ).
cnf(u40828,negated_conjecture,
green(n3,n17) ).
cnf(u8555,negated_conjecture,
~ green(n12,n17) ).
cnf(u8564,negated_conjecture,
~ green(n5,n17) ).
cnf(u8573,negated_conjecture,
~ green(n7,n17) ).
cnf(u40957,negated_conjecture,
green(n9,n17) ).
cnf(u8589,negated_conjecture,
( ~ green(n9,X0)
| ~ green(X0,n16)
| ~ green(X0,n17) ) ).
cnf(u8593,negated_conjecture,
~ green(n16,n11) ).
cnf(u8596,negated_conjecture,
~ green(n16,n10) ).
cnf(u8600,negated_conjecture,
~ green(n16,n12) ).
cnf(u8604,negated_conjecture,
~ green(n16,n14) ).
cnf(u8607,negated_conjecture,
~ green(n16,n13) ).
cnf(u8615,negated_conjecture,
~ red(n16,n15) ).
cnf(u8618,negated_conjecture,
~ red(n16,n14) ).
cnf(u8628,negated_conjecture,
~ red(n16,n12) ).
cnf(u8631,negated_conjecture,
~ red(n16,n11) ).
cnf(u8677,negated_conjecture,
~ green(n17,n16) ).
cnf(u8680,negated_conjecture,
~ green(n17,n17) ).
cnf(u40952,negated_conjecture,
green(n4,n17) ).
cnf(u8737,negated_conjecture,
~ green(n2,n17) ).
cnf(u8751,negated_conjecture,
~ green(n6,n17) ).
cnf(u40925,negated_conjecture,
green(n11,n17) ).
cnf(u8770,negated_conjecture,
( ~ green(n11,X0)
| ~ green(X0,n16)
| ~ green(X0,n17) ) ).
cnf(u8799,negated_conjecture,
~ red(n16,n10) ).
cnf(u8810,negated_conjecture,
~ red(n16,n13) ).
cnf(u8827,negated_conjecture,
~ green(n13,n17) ).
cnf(u41378,negated_conjecture,
green(n8,n17) ).
cnf(u41025,negated_conjecture,
green(n10,n17) ).
cnf(u9159,negated_conjecture,
( ~ red(X0,n6)
| ~ red(n5,X0)
| ~ red(X0,n8) ) ).
cnf(u9170,negated_conjecture,
~ red(n9,n8) ).
cnf(u9190,negated_conjecture,
~ red(n4,n1) ).
cnf(u9194,negated_conjecture,
~ red(n1,n1) ).
cnf(u9383,negated_conjecture,
( ~ red(n11,X0)
| ~ red(X0,n12)
| ~ red(X0,n13) ) ).
cnf(u9423,negated_conjecture,
( ~ red(X0,n12)
| ~ red(n3,X0)
| ~ red(X0,n13) ) ).
cnf(u9941,negated_conjecture,
( ~ green(X0,n2)
| ~ green(n1,X0)
| ~ green(X0,n12) ) ).
cnf(u9999,negated_conjecture,
~ red(n14,n13) ).
cnf(u10290,negated_conjecture,
( ~ red(n11,X0)
| ~ red(X0,n12)
| ~ red(X0,n14) ) ).
cnf(u10419,negated_conjecture,
~ red(n6,n3) ).
cnf(u10478,negated_conjecture,
~ green(n7,n5) ).
cnf(u10493,negated_conjecture,
~ green(n2,n1) ).
cnf(u10557,negated_conjecture,
~ green(n12,n10) ).
cnf(u10560,negated_conjecture,
~ green(n12,n9) ).
cnf(u10714,negated_conjecture,
~ red(n4,n2) ).
cnf(u10847,negated_conjecture,
( ~ red(n2,X0)
| ~ red(X0,n14)
| ~ red(X0,n15) ) ).
cnf(u11022,negated_conjecture,
~ red(n9,n9) ).
cnf(u11155,negated_conjecture,
~ red(n6,n1) ).
cnf(u11633,negated_conjecture,
( ~ red(n10,X0)
| ~ red(X0,n12)
| ~ red(X0,n13) ) ).
cnf(u12021,negated_conjecture,
~ red(n5,n5) ).
cnf(u12195,negated_conjecture,
~ red(n15,n11) ).
cnf(u12198,negated_conjecture,
~ red(n15,n9) ).
cnf(u12352,negated_conjecture,
~ red(n15,n12) ).
cnf(u12493,negated_conjecture,
~ red(n13,n13) ).
cnf(u13298,negated_conjecture,
~ green(n15,n14) ).
cnf(u13301,negated_conjecture,
~ green(n15,n12) ).
cnf(u13664,negated_conjecture,
( ~ green(X0,n2)
| ~ green(n1,X0)
| ~ green(X0,n4) ) ).
cnf(u13819,negated_conjecture,
~ red(n3,n2) ).
cnf(u13875,negated_conjecture,
~ red(n8,n7) ).
cnf(u13945,negated_conjecture,
~ green(n2,n2) ).
cnf(u14075,negated_conjecture,
~ green(n11,n10) ).
cnf(u14078,negated_conjecture,
~ green(n11,n9) ).
cnf(u14418,negated_conjecture,
( ~ green(X0,n3)
| ~ green(n2,X0)
| ~ green(X0,n9) ) ).
cnf(u14492,negated_conjecture,
( ~ green(X0,n3)
| ~ green(n2,X0)
| ~ green(X0,n5) ) ).
cnf(u15784,negated_conjecture,
~ red(n4,n3) ).
cnf(u17164,negated_conjecture,
~ green(n6,n2) ).
cnf(u18288,negated_conjecture,
~ green(n16,n9) ).
cnf(u18332,negated_conjecture,
~ red(n2,n1) ).
cnf(u18336,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X0,n8)
| ~ red(X0,n7) ) ).
cnf(u18341,negated_conjecture,
~ red(n3,n1) ).
cnf(u18403,negated_conjecture,
~ red(n5,n4) ).
cnf(u18408,negated_conjecture,
~ green(n6,n4) ).
cnf(u18660,negated_conjecture,
( ~ red(n9,X0)
| ~ red(X0,n14)
| ~ red(X0,n15) ) ).
cnf(u18744,negated_conjecture,
~ green(n7,n1) ).
cnf(u18758,negated_conjecture,
~ green(n3,n1) ).
cnf(u18953,negated_conjecture,
~ green(n13,n12) ).
cnf(u19036,negated_conjecture,
~ red(n5,n2) ).
cnf(u20114,negated_conjecture,
~ red(n5,n1) ).
cnf(u21328,negated_conjecture,
( ~ red(X0,n8)
| ~ red(n7,X0)
| ~ red(X0,n9) ) ).
cnf(u22401,negated_conjecture,
~ green(n1,n1) ).
cnf(u22731,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X0,n11)
| ~ green(X0,n10) ) ).
cnf(u22930,negated_conjecture,
( ~ green(X0,n12)
| ~ green(X0,n16)
| ~ green(X0,n15) ) ).
cnf(u23418,negated_conjecture,
~ green(n3,n2) ).
cnf(u23491,negated_conjecture,
~ red(n8,n3) ).
cnf(u24377,negated_conjecture,
~ red(n8,n1) ).
cnf(u26564,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X0,n16)
| ~ red(X0,n15) ) ).
cnf(u27372,negated_conjecture,
~ red(n7,n1) ).
cnf(u28238,negated_conjecture,
~ red(n7,n3) ).
cnf(u28396,negated_conjecture,
~ red(n7,n5) ).
cnf(u28563,negated_conjecture,
~ red(n8,n4) ).
cnf(u30062,negated_conjecture,
~ red(n5,n3) ).
cnf(u31581,negated_conjecture,
~ red(n7,n2) ).
cnf(u32046,negated_conjecture,
~ red(n10,n9) ).
cnf(u33083,negated_conjecture,
( ~ red(X0,n3)
| ~ red(n2,X0)
| ~ red(X0,n5) ) ).
cnf(u33303,negated_conjecture,
~ red(n8,n2) ).
cnf(u33438,negated_conjecture,
~ red(n8,n6) ).
cnf(u36862,negated_conjecture,
( ~ green(X0,n15)
| ~ green(n4,X0)
| ~ green(X0,n13) ) ).
cnf(u37088,negated_conjecture,
~ red(n7,n4) ).
cnf(u37107,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n12)
| ~ red(X0,n11) ) ).
cnf(u40149,negated_conjecture,
( ~ green(X0,n5)
| ~ green(n4,X0)
| ~ green(X0,n16) ) ).
cnf(u40190,negated_conjecture,
( ~ red(n7,X0)
| ~ red(X0,n14)
| ~ red(X0,n16) ) ).
cnf(u40195,negated_conjecture,
( ~ red(n6,X0)
| ~ red(X0,n14)
| ~ red(X0,n16) ) ).
cnf(u40200,negated_conjecture,
( ~ red(n5,X0)
| ~ red(X0,n14)
| ~ red(X0,n16) ) ).
cnf(u40206,negated_conjecture,
( ~ red(X0,n16)
| ~ red(n3,X0)
| ~ red(X0,n14) ) ).
cnf(u40216,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n12)
| ~ green(X0,n16) ) ).
cnf(u40221,negated_conjecture,
( ~ green(n8,X0)
| ~ green(X0,n12)
| ~ green(X0,n16) ) ).
cnf(u40235,negated_conjecture,
( ~ green(n11,X0)
| ~ green(X0,n13)
| ~ green(X0,n16) ) ).
cnf(u40240,negated_conjecture,
( ~ green(n9,X0)
| ~ green(X0,n13)
| ~ green(X0,n16) ) ).
cnf(u40672,negated_conjecture,
~ red(n16,n16) ).
cnf(u40793,negated_conjecture,
~ red(n17,n14) ).
cnf(u40796,negated_conjecture,
~ red(n17,n13) ).
cnf(u40806,negated_conjecture,
~ red(n17,n12) ).
cnf(u41765,axiom,
~ red(n3,n17) ).
cnf(u40852,negated_conjecture,
~ red(n17,n15) ).
cnf(u40857,axiom,
red(n12,n17) ).
cnf(u40873,negated_conjecture,
~ green(n17,n15) ).
cnf(u40876,negated_conjecture,
~ green(n17,n13) ).
cnf(u40884,axiom,
red(n2,n17) ).
cnf(u40916,negated_conjecture,
~ red(n17,n11) ).
cnf(u40923,negated_conjecture,
~ red(n17,n16) ).
cnf(u45764,axiom,
~ red(n11,n17) ).
cnf(u41339,axiom,
~ red(n4,n17) ).
cnf(u41839,axiom,
~ red(n9,n17) ).
cnf(u40973,negated_conjecture,
~ green(n17,n11) ).
cnf(u40976,negated_conjecture,
~ green(n17,n10) ).
cnf(u40980,negated_conjecture,
~ green(n17,n12) ).
cnf(u40997,axiom,
red(n5,n17) ).
cnf(u41323,axiom,
~ red(n10,n17) ).
cnf(u69676,axiom,
~ red(n1,n17) ).
cnf(u47048,axiom,
~ red(n14,n17) ).
cnf(u41105,negated_conjecture,
~ green(n16,n16) ).
cnf(u41134,axiom,
red(n13,n17) ).
cnf(u41159,axiom,
red(n6,n17) ).
cnf(u41326,negated_conjecture,
( ~ red(n10,X0)
| ~ red(X0,n14)
| ~ red(X0,n17) ) ).
cnf(u41383,axiom,
~ red(n8,n17) ).
cnf(u41386,negated_conjecture,
( ~ red(n8,X0)
| ~ red(X0,n15)
| ~ red(X0,n17) ) ).
cnf(u41440,negated_conjecture,
~ red(n17,n8) ).
cnf(u41446,axiom,
red(n7,n17) ).
cnf(u41454,negated_conjecture,
( ~ red(n7,X0)
| ~ red(X0,n14)
| ~ red(X0,n17) ) ).
cnf(u41458,negated_conjecture,
( ~ red(n7,X0)
| ~ red(X0,n15)
| ~ red(X0,n17) ) ).
cnf(u41469,negated_conjecture,
( ~ red(X0,n8)
| ~ red(n1,X0)
| ~ red(X0,n16) ) ).
cnf(u41473,negated_conjecture,
~ red(n9,n1) ).
cnf(u41686,negated_conjecture,
( ~ green(X0,n3)
| ~ green(n2,X0)
| ~ green(X0,n16) ) ).
cnf(u41768,negated_conjecture,
( ~ red(X0,n17)
| ~ red(n3,X0)
| ~ red(X0,n14) ) ).
cnf(u41842,negated_conjecture,
( ~ red(n9,X0)
| ~ red(X0,n14)
| ~ red(X0,n17) ) ).
cnf(u41898,negated_conjecture,
( ~ red(n8,X0)
| ~ red(X0,n10)
| ~ red(X0,n16) ) ).
cnf(u41904,negated_conjecture,
( ~ red(n9,X0)
| ~ red(X0,n11)
| ~ red(X0,n16) ) ).
cnf(u41989,negated_conjecture,
( ~ green(X0,n16)
| ~ green(n3,X0)
| ~ green(X0,n5) ) ).
cnf(u42001,negated_conjecture,
( ~ red(n6,X0)
| ~ red(X0,n11)
| ~ red(X0,n16) ) ).
cnf(u42424,negated_conjecture,
( ~ red(n10,X0)
| ~ red(X0,n11)
| ~ red(X0,n16) ) ).
cnf(u42760,negated_conjecture,
( ~ red(X0,n14)
| ~ red(n3,X0)
| ~ red(X0,n10) ) ).
cnf(u43346,negated_conjecture,
~ red(n6,n2) ).
cnf(u44156,negated_conjecture,
( ~ red(X0,n17)
| ~ red(n2,X0)
| ~ red(X0,n16) ) ).
cnf(u44162,negated_conjecture,
( ~ red(n15,X0)
| ~ red(X0,n16)
| ~ red(X0,n17) ) ).
cnf(u45767,negated_conjecture,
( ~ red(n11,X0)
| ~ red(X0,n16)
| ~ red(X0,n17) ) ).
cnf(u49901,negated_conjecture,
( ~ red(n9,X0)
| ~ red(X0,n11)
| ~ red(X0,n13) ) ).
cnf(u51432,negated_conjecture,
~ green(n10,n7) ).
cnf(u52455,negated_conjecture,
( ~ red(X0,n12)
| ~ red(n3,X0)
| ~ red(X0,n10) ) ).
cnf(u53238,negated_conjecture,
~ red(n13,n6) ).
cnf(u54481,negated_conjecture,
~ green(n15,n5) ).
cnf(u55857,negated_conjecture,
~ green(n9,n8) ).
cnf(u56480,negated_conjecture,
~ green(n5,n3) ).
cnf(u60244,negated_conjecture,
~ red(n6,n4) ).
cnf(u61195,negated_conjecture,
~ green(n14,n5) ).
cnf(u61516,negated_conjecture,
~ red(n6,n5) ).
cnf(u62102,negated_conjecture,
~ red(n13,n4) ).
cnf(u63872,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X0,n17)
| ~ red(X0,n16) ) ).
cnf(u63976,negated_conjecture,
( ~ red(n6,X0)
| ~ red(X0,n11)
| ~ red(X0,n13) ) ).
cnf(u69192,negated_conjecture,
~ green(n5,n1) ).
cnf(u70022,negated_conjecture,
( ~ green(n7,X0)
| ~ green(X0,n12)
| ~ green(X0,n14) ) ).
cnf(u71980,negated_conjecture,
( ~ red(n13,X0)
| ~ red(X0,n16)
| ~ red(X0,n17) ) ).
cnf(u73554,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X0,n10)
| ~ green(X0,n9) ) ).
cnf(u73810,negated_conjecture,
( ~ green(X0,n4)
| ~ green(n3,X0)
| ~ green(X0,n6) ) ).
cnf(u75574,negated_conjecture,
~ red(n8,n5) ).
cnf(u78779,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n12)
| ~ green(X0,n14) ) ).
cnf(u79829,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X0,n11)
| ~ red(X0,n10) ) ).
cnf(u81889,negated_conjecture,
( ~ red(X0,n5)
| ~ red(n1,X0)
| ~ red(X0,n4) ) ).
cnf(u82846,negated_conjecture,
( ~ red(X0,n7)
| ~ red(n5,X0)
| ~ red(X0,n9) ) ).
cnf(u85410,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X0,n11)
| ~ green(X0,n10) ) ).
cnf(u86737,negated_conjecture,
~ green(n9,n7) ).
cnf(u45285,negated_conjecture,
~ green(n11,n5) ).
cnf(u2405,axiom,
less_than(n2,n14) ).
cnf(u86631,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X0,n14)
| ~ green(n7,X0) ) ).
cnf(u86548,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X0,n16)
| ~ red(X0,n17) ) ).
cnf(u86378,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X0,n15)
| ~ green(n3,X0) ) ).
cnf(u85366,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(X0,X1) ) ).
cnf(u33,axiom,
less_than(n3,n4) ).
cnf(u87664,axiom,
( ~ less_than(X0,n6)
| red(X0,n11)
| green(X0,n11) ) ).
cnf(u1091,axiom,
( less_than(X0,n12)
| ~ less_than(X0,n8) ) ).
cnf(u40717,axiom,
( ~ less_than(X0,n6)
| ~ less_than(X1,X0)
| less_than(X1,n9) ) ).
cnf(u86043,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X1,n2)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1) ) ).
cnf(u40551,axiom,
( ~ less_than(X0,n14)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u87483,axiom,
( ~ less_than(X0,n11)
| ~ less_than(X1,X0)
| less_than(X1,n14) ) ).
cnf(u2339,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n7) ) ).
cnf(u87729,axiom,
( ~ less_than(X0,n9)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u40462,axiom,
( ~ less_than(X0,n10)
| ~ less_than(X1,X0)
| less_than(X1,n12) ) ).
cnf(u86920,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n13)
| ~ red(n7,X0) ) ).
cnf(u87478,axiom,
( ~ less_than(X0,n7)
| ~ less_than(X1,X0)
| less_than(X1,n10) ) ).
cnf(u40459,axiom,
( ~ less_than(X0,n6)
| ~ less_than(X1,X0)
| less_than(X1,n8) ) ).
cnf(u321,axiom,
less_than(n5,n7) ).
cnf(u86964,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n15)
| ~ red(n1,X0) ) ).
cnf(u86836,negated_conjecture,
~ green(n8,n1) ).
cnf(u87515,axiom,
( ~ less_than(X0,n5)
| ~ less_than(X1,X0)
| less_than(X1,n16) ) ).
cnf(u86348,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,n16)
| ~ red(X1,n16)
| ~ red(X0,X1) ) ).
cnf(u2047,axiom,
less_than(n4,n14) ).
cnf(u747,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n9) ) ).
cnf(u88348,axiom,
( ~ less_than(X0,n6)
| red(X0,n13)
| green(X0,n13) ) ).
cnf(u39,axiom,
( ~ less_than(X1,X2)
| ~ less_than(X0,X1)
| less_than(X0,X2) ) ).
cnf(u86050,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,X1) ) ).
cnf(u372,axiom,
( less_than(X0,n12)
| ~ less_than(X0,n7) ) ).
cnf(u2301,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n5) ) ).
cnf(u86818,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n12)
| ~ red(n6,X0) ) ).
cnf(u40481,axiom,
( ~ less_than(X0,n7)
| green(X0,n9)
| red(X0,n9) ) ).
cnf(u87372,axiom,
( ~ less_than(X1,n10)
| less_than(X0,n14)
| ~ less_than(X0,X1) ) ).
cnf(u40724,axiom,
( ~ less_than(X0,n12)
| green(X0,n15)
| red(X0,n15) ) ).
cnf(u87384,axiom,
( ~ less_than(X1,n8)
| less_than(X0,n13)
| ~ less_than(X0,X1) ) ).
cnf(u8124,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n7) ) ).
cnf(u86383,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n17)
| ~ green(X0,n14) ) ).
cnf(u87150,negated_conjecture,
( ~ red(n7,X0)
| ~ red(X0,n17)
| ~ red(X0,n13) ) ).
cnf(u4107,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n11) ) ).
cnf(u1466,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n10) ) ).
cnf(u86283,negated_conjecture,
( ~ green(X0,n13)
| ~ green(X0,n15)
| ~ green(X0,n16) ) ).
cnf(u86131,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n15)
| ~ red(X1,n15)
| ~ red(X0,X1) ) ).
cnf(u86871,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n17)
| ~ green(X0,n11) ) ).
cnf(u86013,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n2)
| ~ green(X1,n2)
| ~ green(X0,X1) ) ).
cnf(u84672,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X0,n15)
| ~ green(X1,n15)
| ~ green(X0,X1) ) ).
cnf(u85753,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,X1) ) ).
cnf(u26,axiom,
less_than(n10,n11) ).
cnf(u40738,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n17) ) ).
cnf(u86726,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X0,n6)
| ~ green(n2,X0) ) ).
cnf(u86103,negated_conjecture,
( ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,X1) ) ).
cnf(u2049,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n13) ) ).
cnf(u85223,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X1,n2)
| ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,X1) ) ).
cnf(u418,axiom,
less_than(n3,n8) ).
cnf(u88532,axiom,
( ~ less_than(X0,n4)
| red(X0,n14)
| green(X0,n14) ) ).
cnf(u4105,axiom,
less_than(n6,n12) ).
cnf(u1464,axiom,
less_than(n5,n11) ).
cnf(u27,axiom,
less_than(n9,n10) ).
cnf(u954,axiom,
less_than(n3,n13) ).
cnf(u86160,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X0,n7)
| ~ red(X0,n8) ) ).
cnf(u86520,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n15)
| ~ green(X0,n11) ) ).
cnf(u86159,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,X1) ) ).
cnf(u40474,axiom,
( ~ less_than(X0,n13)
| ~ less_than(X1,X0)
| less_than(X1,n16) ) ).
cnf(u24,axiom,
less_than(n12,n13) ).
cnf(u86381,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,n16)
| ~ red(X1,n16)
| ~ red(X0,X1) ) ).
cnf(u410,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n6) ) ).
cnf(u86568,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X0,n12)
| ~ green(n1,X0) ) ).
cnf(u86147,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X0,n14)
| ~ red(X0,n15) ) ).
cnf(u755,axiom,
less_than(n1,n11) ).
cnf(u86185,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,X1) ) ).
cnf(u86222,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n10)
| ~ red(n1,X0) ) ).
cnf(u443,axiom,
( ~ less_than(X0,n16)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u4094,axiom,
( less_than(X0,n10)
| ~ less_than(X0,n6) ) ).
cnf(u88610,axiom,
( ~ less_than(X0,n5)
| red(X0,n15)
| green(X0,n15) ) ).
cnf(u86166,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1) ) ).
cnf(u4111,axiom,
( less_than(X0,n12)
| ~ less_than(X0,n6) ) ).
cnf(u25,axiom,
less_than(n11,n12) ).
cnf(u85285,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,X1) ) ).
cnf(u87349,axiom,
( ~ less_than(X1,n6)
| less_than(X0,n10)
| ~ less_than(X0,X1) ) ).
cnf(u2415,axiom,
less_than(n2,n15) ).
cnf(u86646,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X0,n13)
| ~ green(n2,X0) ) ).
cnf(u85904,negated_conjecture,
( ~ red(X1,n8)
| ~ red(X1,n7)
| ~ red(X0,n8)
| ~ red(X0,n7)
| ~ red(X0,X1) ) ).
cnf(u84483,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1) ) ).
cnf(u86915,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(n3,X0) ) ).
cnf(u86194,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,n15)
| ~ red(X1,n15)
| ~ red(X0,X1) ) ).
cnf(u310,axiom,
less_than(n9,n12) ).
cnf(u86191,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,X1) ) ).
cnf(u86900,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X0,n13)
| ~ red(n1,X0) ) ).
cnf(u86312,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X0,n10)
| ~ red(X0,n12) ) ).
cnf(u86779,negated_conjecture,
( ~ red(X0,n14)
| ~ red(X0,n16)
| ~ red(n2,X0) ) ).
cnf(u1755,axiom,
less_than(n10,n15) ).
cnf(u87482,axiom,
( ~ less_than(X0,n11)
| green(X0,n14)
| red(X0,n14) ) ).
cnf(u30,axiom,
less_than(n6,n7) ).
cnf(u86962,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n15)
| ~ red(n7,X0) ) ).
cnf(u86985,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X0,n17)
| ~ green(n1,X0) ) ).
cnf(u88399,axiom,
( ~ less_than(X0,n5)
| red(X0,n11)
| green(X0,n11) ) ).
cnf(u1987,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n8) ) ).
cnf(u86164,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X0,n12)
| ~ red(X0,n13) ) ).
cnf(u85240,negated_conjecture,
( ~ green(X1,n9)
| ~ green(X1,n8)
| ~ green(X0,n9)
| ~ green(X0,n8)
| ~ green(X0,X1) ) ).
cnf(u87702,axiom,
( ~ less_than(X0,n8)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u31,axiom,
less_than(n5,n6) ).
cnf(u84723,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,X1) ) ).
cnf(u87575,axiom,
( ~ less_than(X0,n11)
| green(X0,n15)
| red(X0,n15) ) ).
cnf(u2387,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n11) ) ).
cnf(u87135,negated_conjecture,
( ~ red(X0,n10)
| ~ red(X0,n16)
| ~ red(n3,X0) ) ).
cnf(u85914,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,X1) ) ).
cnf(u497,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n6) ) ).
cnf(u516,axiom,
less_than(n1,n8) ).
cnf(u86006,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X0,n15)
| ~ green(n3,X0) ) ).
cnf(u84328,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X0,n15)
| ~ green(X1,n15)
| ~ green(X0,X1) ) ).
cnf(u85900,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X0,X1) ) ).
cnf(u28,axiom,
less_than(n8,n9) ).
cnf(u1566,axiom,
less_than(n10,n14) ).
cnf(u86318,negated_conjecture,
( ~ red(n8,X0)
| ~ red(X0,n13)
| ~ red(X0,n11) ) ).
cnf(u87357,axiom,
( ~ less_than(X1,n10)
| less_than(X0,n15)
| ~ less_than(X0,X1) ) ).
cnf(u1422,axiom,
less_than(n5,n9) ).
cnf(u447,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n3) ) ).
cnf(u420,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n7) ) ).
cnf(u87691,axiom,
( ~ less_than(X0,n4)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u87479,axiom,
( ~ less_than(X0,n11)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u87468,axiom,
less_than(n3,n16) ).
cnf(u86067,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,X1) ) ).
cnf(u29,axiom,
less_than(n7,n8) ).
cnf(u86319,negated_conjecture,
( ~ red(X0,n11)
| ~ red(X0,n13)
| ~ red(n5,X0) ) ).
cnf(u86039,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,X1) ) ).
cnf(u964,axiom,
less_than(n3,n14) ).
cnf(u261,axiom,
less_than(n12,n14) ).
cnf(u86883,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X0,n10)
| ~ red(n1,X0) ) ).
cnf(u721,axiom,
( less_than(X0,n14)
| ~ less_than(X0,n7) ) ).
cnf(u298,axiom,
less_than(n6,n9) ).
cnf(u40735,axiom,
( ~ less_than(X1,n12)
| ~ less_than(X0,X1)
| less_than(X0,n17) ) ).
cnf(u797,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n14) ) ).
cnf(u86140,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,X1) ) ).
cnf(u86824,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n11)
| ~ red(n4,X0) ) ).
cnf(u2036,axiom,
less_than(n4,n13) ).
cnf(u86767,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X0,n16)
| ~ green(n1,X0) ) ).
cnf(u445,axiom,
less_than(n1,n3) ).
cnf(u86662,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X0,n15)
| ~ green(n5,X0) ) ).
cnf(u2326,axiom,
less_than(n2,n7) ).
cnf(u85927,negated_conjecture,
( ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,X1) ) ).
cnf(u40714,axiom,
( ~ less_than(X0,n4)
| ~ less_than(X1,X0)
| less_than(X1,n7) ) ).
cnf(u40472,axiom,
( ~ less_than(X0,n12)
| ~ less_than(X1,X0)
| less_than(X1,n14) ) ).
cnf(u85390,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,n15)
| ~ red(X1,n15)
| ~ red(X0,X1) ) ).
cnf(u87999,axiom,
( ~ less_than(X0,n4)
| red(X0,n10)
| green(X0,n10) ) ).
cnf(u946,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n11) ) ).
cnf(u86130,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n15)
| ~ red(X1,n15)
| ~ red(X0,X1) ) ).
cnf(u8130,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n13) ) ).
cnf(u1445,axiom,
less_than(n5,n10) ).
cnf(u86046,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1) ) ).
cnf(u86037,negated_conjecture,
( ~ red(X0,n11)
| ~ red(X0,n12)
| ~ red(X0,n13) ) ).
cnf(u86093,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1) ) ).
cnf(u86391,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u86072,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,X1) ) ).
cnf(u86921,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n13)
| ~ red(n1,X0) ) ).
cnf(u87851,axiom,
( ~ less_than(X0,n6)
| ~ less_than(X1,X0)
| less_than(X1,n15) ) ).
cnf(u408,axiom,
less_than(n3,n7) ).
cnf(u1147,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n8) ) ).
cnf(u86177,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,X1) ) ).
cnf(u87776,axiom,
( ~ less_than(X0,n9)
| green(X0,n15)
| red(X0,n15) ) ).
cnf(u85244,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,X1) ) ).
cnf(u40618,axiom,
( ~ less_than(X0,n12)
| red(X0,n16)
| green(X0,n16) ) ).
cnf(u86954,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n15)
| ~ red(n6,X0) ) ).
cnf(u22,axiom,
less_than(n14,n15) ).
cnf(u785,axiom,
less_than(n1,n14) ).
cnf(u86940,negated_conjecture,
( ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(n2,X0) ) ).
cnf(u40742,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n6) ) ).
cnf(u358,axiom,
( less_than(X0,n11)
| ~ less_than(X0,n7) ) ).
cnf(u4129,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n14) ) ).
cnf(u85116,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X0,X1) ) ).
cnf(u87643,axiom,
( ~ less_than(X0,n4)
| red(X0,n9)
| green(X0,n9) ) ).
cnf(u86267,negated_conjecture,
( ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u88279,axiom,
( ~ less_than(X1,n5)
| ~ less_than(X0,X1)
| less_than(X0,n12) ) ).
cnf(u86083,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X0,X1) ) ).
cnf(u23,axiom,
less_than(n13,n14) ).
cnf(u86649,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X0,n9)
| ~ green(n2,X0) ) ).
cnf(u86813,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X0,n9)
| ~ red(n4,X0) ) ).
cnf(u87568,axiom,
( ~ less_than(X0,n6)
| ~ less_than(X1,X0)
| less_than(X1,n16) ) ).
cnf(u87567,axiom,
( ~ less_than(X0,n6)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u300,axiom,
( less_than(X0,n8)
| ~ less_than(X0,n6) ) ).
cnf(u40747,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n11) ) ).
cnf(u87348,axiom,
( ~ less_than(X1,n5)
| less_than(X0,n10)
| ~ less_than(X0,X1) ) ).
cnf(u87404,axiom,
( ~ less_than(X1,n6)
| less_than(X0,n11)
| ~ less_than(X0,X1) ) ).
cnf(u636,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n9) ) ).
cnf(u85228,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1) ) ).
cnf(u40733,axiom,
( ~ less_than(X0,n5)
| green(X0,n8)
| red(X0,n8) ) ).
cnf(u86417,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X0,n16)
| ~ red(X0,n17) ) ).
cnf(u86081,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(X0,X1) ) ).
cnf(u356,axiom,
less_than(n7,n12) ).
cnf(u86310,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X0,n10)
| ~ red(X0,n12) ) ).
cnf(u84394,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X1,n2)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,X1) ) ).
cnf(u40554,axiom,
( ~ less_than(X1,n12)
| less_than(X0,n16)
| ~ less_than(X0,X1) ) ).
cnf(u86181,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(X0,X1) ) ).
cnf(u20,axiom,
less_than(n16,n17) ).
cnf(u88057,axiom,
( ~ less_than(X0,n7)
| green(X0,n15)
| red(X0,n15) ) ).
cnf(u87069,negated_conjecture,
( ~ red(n6,X0)
| ~ red(X0,n17)
| ~ red(X0,n12) ) ).
cnf(u495,axiom,
less_than(n1,n7) ).
cnf(u86819,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n12)
| ~ red(n3,X0) ) ).
cnf(u21,axiom,
less_than(n15,n16) ).
cnf(u2377,axiom,
less_than(n2,n10) ).
cnf(u2395,axiom,
less_than(n2,n13) ).
cnf(u1972,axiom,
( less_than(X0,n7)
| ~ less_than(X0,n4) ) ).
cnf(u1506,axiom,
less_than(n5,n14) ).
cnf(u86392,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u2028,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n11) ) ).
cnf(u40475,axiom,
( ~ less_than(X0,n13)
| green(X0,n15)
| red(X0,n15) ) ).
cnf(u2337,axiom,
less_than(n2,n8) ).
cnf(u346,axiom,
less_than(n7,n11) ).
cnf(u85905,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(X0,X1) ) ).
cnf(u87905,axiom,
( ~ less_than(X1,n5)
| less_than(X0,n11)
| ~ less_than(X0,X1) ) ).
cnf(u8128,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n11) ) ).
cnf(u86396,negated_conjecture,
( ~ red(X0,n15)
| ~ red(X1,n15)
| ~ red(X0,n17)
| ~ red(X1,n17)
| ~ red(X0,X1) ) ).
cnf(u86057,negated_conjecture,
( ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,n15)
| ~ green(X1,n15)
| ~ green(X0,X1) ) ).
cnf(u88162,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n16)
| ~ less_than(X0,X1) ) ).
cnf(u85263,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,n15)
| ~ green(X1,n15)
| ~ green(X0,X1) ) ).
cnf(u40461,axiom,
( ~ less_than(X0,n10)
| green(X0,n12)
| red(X0,n12) ) ).
cnf(u86113,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n14)
| ~ green(X0,n13) ) ).
cnf(u87731,axiom,
( ~ less_than(X0,n6)
| green(X0,n12)
| red(X0,n12) ) ).
cnf(u462,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n4) ) ).
cnf(u1504,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n12) ) ).
cnf(u86066,negated_conjecture,
( ~ red(X1,n15)
| ~ red(X1,n14)
| ~ red(X0,n15)
| ~ red(X0,n14)
| ~ red(X0,X1) ) ).
cnf(u8123,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n6) ) ).
cnf(u458,axiom,
less_than(n1,n4) ).
cnf(u1168,axiom,
( less_than(X0,n12)
| ~ less_than(X0,n9) ) ).
cnf(u88439,axiom,
( ~ less_than(X0,n5)
| green(X0,n12)
| red(X0,n12) ) ).
cnf(u8118,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n16) ) ).
cnf(u86122,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u40740,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n4) ) ).
cnf(u86957,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X0,n11)
| ~ red(n4,X0) ) ).
cnf(u86509,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X0,n14)
| ~ green(n6,X0) ) ).
cnf(u251,axiom,
( less_than(X0,n9)
| ~ less_than(X0,n7) ) ).
cnf(u87690,axiom,
( ~ less_than(X0,n4)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u86421,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X0,n16)
| ~ red(X0,n17) ) ).
cnf(u483,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n5) ) ).
cnf(u85888,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X0,n15)
| ~ green(X1,n15)
| ~ green(X0,X1) ) ).
cnf(u86036,negated_conjecture,
( ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,X1) ) ).
cnf(u348,axiom,
( less_than(X0,n10)
| ~ less_than(X0,n7) ) ).
cnf(u86943,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X0,n14)
| ~ red(n1,X0) ) ).
cnf(u40718,axiom,
( ~ less_than(X0,n10)
| ~ less_than(X1,X0)
| less_than(X1,n16) ) ).
cnf(u248,axiom,
( ~ less_than(X0,n15)
| ~ less_than(X1,X0)
| less_than(X1,n16) ) ).
cnf(u86119,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1) ) ).
cnf(u86882,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X0,n10)
| ~ red(n4,X0) ) ).
cnf(u40745,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n9) ) ).
cnf(u85052,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,X1) ) ).
cnf(u87601,axiom,
( ~ less_than(X0,n4)
| red(X0,n8)
| green(X0,n8) ) ).
cnf(u40478,axiom,
( ~ less_than(X0,n11)
| green(X0,n13)
| red(X0,n13) ) ).
cnf(u87565,axiom,
( ~ less_than(X0,n6)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u777,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n12) ) ).
cnf(u40552,axiom,
( ~ less_than(X0,n14)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u82959,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X1,n2)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,X1) ) ).
cnf(u86499,negated_conjecture,
( ~ green(n4,X0)
| ~ green(X0,n15)
| ~ green(X0,n12) ) ).
cnf(u249,axiom,
less_than(n7,n9) ).
cnf(u88075,axiom,
( ~ less_than(X0,n6)
| ~ less_than(X1,X0)
| less_than(X1,n14) ) ).
cnf(u87121,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X0,n16)
| ~ red(n4,X0) ) ).
cnf(u2397,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n12) ) ).
cnf(u87513,axiom,
( ~ less_than(X0,n5)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u86467,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X0,n12)
| ~ green(n1,X0) ) ).
cnf(u481,axiom,
less_than(n1,n6) ).
cnf(u40698,axiom,
( ~ less_than(X1,n11)
| less_than(X0,n16)
| ~ less_than(X0,X1) ) ).
cnf(u942,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n10) ) ).
cnf(u86825,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n11)
| ~ red(n2,X0) ) ).
cnf(u1142,axiom,
( less_than(X0,n14)
| ~ less_than(X0,n8) ) ).
cnf(u86082,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(X0,X1) ) ).
cnf(u87580,axiom,
( ~ less_than(X0,n7)
| green(X0,n11)
| red(X0,n11) ) ).
cnf(u86201,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X0,n8)
| ~ green(n3,X0) ) ).
cnf(u40476,axiom,
( ~ less_than(X0,n13)
| ~ less_than(X1,X0)
| less_than(X1,n15) ) ).
cnf(u85821,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1) ) ).
cnf(u86117,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,X1) ) ).
cnf(u40473,axiom,
( ~ less_than(X0,n13)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u85911,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X0,X1) ) ).
cnf(u87397,axiom,
( ~ less_than(X1,n5)
| less_than(X0,n9)
| ~ less_than(X0,X1) ) ).
cnf(u86534,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X0,n11)
| ~ green(n1,X0) ) ).
cnf(u86872,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X0,n17)
| ~ green(n3,X0) ) ).
cnf(u86443,negated_conjecture,
( ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(X0,n16)
| ~ red(X1,n16)
| ~ red(X0,X1) ) ).
cnf(u86498,negated_conjecture,
( ~ green(X0,n12)
| ~ green(X0,n15)
| ~ green(n5,X0) ) ).
cnf(u460,axiom,
less_than(n2,n5) ).
cnf(u1140,axiom,
less_than(n8,n15) ).
cnf(u87338,axiom,
( ~ less_than(X1,n8)
| less_than(X0,n12)
| ~ less_than(X0,X1) ) ).
cnf(u795,axiom,
less_than(n1,n15) ).
cnf(u86291,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,n16)
| ~ green(X1,n16)
| ~ green(X0,X1) ) ).
cnf(u8116,axiom,
( ~ less_than(X1,n15)
| less_than(X0,n17)
| ~ less_than(X0,X1) ) ).
cnf(u86384,negated_conjecture,
( ~ green(n4,X0)
| ~ green(X0,n17)
| ~ green(X0,n14) ) ).
cnf(u8121,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n16) ) ).
cnf(u40716,axiom,
( ~ less_than(X0,n6)
| green(X0,n9)
| red(X0,n9) ) ).
cnf(u86976,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X0,n17)
| ~ green(n9,X0) ) ).
cnf(u84734,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,X1) ) ).
cnf(u2385,axiom,
less_than(n2,n12) ).
cnf(u40730,axiom,
( ~ less_than(X0,n9)
| green(X0,n12)
| red(X0,n12) ) ).
cnf(u87591,axiom,
( ~ less_than(X0,n8)
| red(X0,n12)
| green(X0,n12) ) ).
cnf(u87443,axiom,
less_than(n1,n16) ).
cnf(u87499,axiom,
( ~ less_than(X1,n11)
| less_than(X0,n17)
| ~ less_than(X0,X1) ) ).
cnf(u85358,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1) ) ).
cnf(u86390,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1) ) ).
cnf(u40721,axiom,
( ~ less_than(X0,n10)
| ~ less_than(X1,X0)
| less_than(X1,n13) ) ).
cnf(u87358,axiom,
( ~ less_than(X1,n11)
| less_than(X0,n15)
| ~ less_than(X0,X1) ) ).
cnf(u86346,negated_conjecture,
( ~ green(n8,X0)
| ~ green(X0,n17)
| ~ green(X0,n14) ) ).
cnf(u87484,axiom,
( ~ less_than(X0,n10)
| red(X0,n17)
| green(X0,n17) ) ).
cnf(u86893,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X0,n10)
| ~ red(n1,X0) ) ).
cnf(u84037,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,n10)
| ~ red(X1,n10)
| ~ red(X0,X1) ) ).
cnf(u86599,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X0,n14)
| ~ green(n6,X0) ) ).
cnf(u86224,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,n15)
| ~ red(X1,n15)
| ~ red(X0,X1) ) ).
cnf(u87891,axiom,
( ~ less_than(X1,n8)
| less_than(X0,n15)
| ~ less_than(X0,X1) ) ).
cnf(u86910,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X0,n15)
| ~ red(n1,X0) ) ).
cnf(u86055,negated_conjecture,
( ~ green(X1,n10)
| ~ green(X1,n7)
| ~ green(X0,n10)
| ~ green(X0,n7)
| ~ green(X0,X1) ) ).
cnf(u1217,axiom,
( less_than(X0,n14)
| ~ less_than(X0,n9) ) ).
cnf(u86168,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1) ) ).
cnf(u2021,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n10) ) ).
cnf(u87149,negated_conjecture,
( ~ red(n12,X0)
| ~ red(X0,n17)
| ~ red(X0,n13) ) ).
cnf(u87514,axiom,
( ~ less_than(X0,n5)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u88585,axiom,
( ~ less_than(X1,n5)
| less_than(X0,n13)
| ~ less_than(X0,X1) ) ).
cnf(u1985,axiom,
less_than(n4,n9) ).
cnf(u40479,axiom,
( ~ less_than(X0,n11)
| ~ less_than(X1,X0)
| less_than(X1,n13) ) ).
cnf(u86400,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u2426,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n15) ) ).
cnf(u473,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n4) ) ).
cnf(u83521,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1) ) ).
cnf(u1527,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n15) ) ).
cnf(u284,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n11) ) ).
cnf(u956,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n12) ) ).
cnf(u85221,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,X1) ) ).
cnf(u87136,negated_conjecture,
( ~ red(X0,n10)
| ~ red(X0,n16)
| ~ red(n2,X0) ) ).
cnf(u735,axiom,
less_than(n1,n9) ).
cnf(u86489,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X0,n13)
| ~ green(n9,X0) ) ).
cnf(u86830,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X0,n16)
| ~ green(n8,X0) ) ).
cnf(u247,axiom,
( ~ less_than(X0,n15)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u8127,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n10) ) ).
cnf(u4119,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n13) ) ).
cnf(u2379,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n9) ) ).
cnf(u396,axiom,
less_than(n4,n6) ).
cnf(u309,axiom,
less_than(n9,n11) ).
cnf(u84608,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,X1) ) ).
cnf(u84701,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,X1) ) ).
cnf(u86406,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X0,n7)
| ~ green(n2,X0) ) ).
cnf(u40749,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n13) ) ).
cnf(u86967,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X0,n13)
| ~ red(n1,X0) ) ).
cnf(u86993,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X0,n17)
| ~ green(n3,X0) ) ).
cnf(u86766,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X0,n16)
| ~ green(n6,X0) ) ).
cnf(u1970,axiom,
less_than(n4,n8) ).
cnf(u86141,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,X1) ) ).
cnf(u2026,axiom,
less_than(n4,n12) ).
cnf(u787,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n13) ) ).
cnf(u40727,axiom,
( ~ less_than(X0,n8)
| green(X0,n11)
| red(X0,n11) ) ).
cnf(u4117,axiom,
less_than(n6,n14) ).
cnf(u386,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n5) ) ).
cnf(u87682,axiom,
less_than(n1,n17) ).
cnf(u334,axiom,
less_than(n8,n10) ).
cnf(u944,axiom,
less_than(n3,n12) ).
cnf(u86282,negated_conjecture,
( ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,n16)
| ~ green(X1,n16)
| ~ green(X0,X1) ) ).
cnf(u87498,axiom,
( ~ less_than(X1,n10)
| less_than(X0,n17)
| ~ less_than(X0,X1) ) ).
cnf(u40728,axiom,
( ~ less_than(X0,n8)
| ~ less_than(X1,X0)
| less_than(X1,n11) ) ).
cnf(u384,axiom,
less_than(n3,n5) ).
cnf(u4062,axiom,
less_than(n6,n10) ).
cnf(u88596,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n12)
| ~ less_than(X0,X1) ) ).
cnf(u297,axiom,
less_than(n6,n8) ).
cnf(u235,axiom,
less_than(n10,n12) ).
cnf(u84800,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,X1) ) ).
cnf(u88218,axiom,
( ~ less_than(X0,n4)
| red(X0,n16)
| green(X0,n16) ) ).
cnf(u40455,axiom,
( ~ less_than(X0,n4)
| green(X0,n6)
| red(X0,n6) ) ).
cnf(u2383,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n10) ) ).
cnf(u86262,negated_conjecture,
( ~ green(X1,n16)
| ~ green(X1,n15)
| ~ green(X0,n16)
| ~ green(X0,n15)
| ~ green(X0,X1) ) ).
cnf(u86253,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,n16)
| ~ green(X1,n16)
| ~ green(X0,X1) ) ).
cnf(u1508,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n13) ) ).
cnf(u85884,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1) ) ).
cnf(u40494,axiom,
( ~ less_than(X0,n9)
| green(X0,n11)
| red(X0,n11) ) ).
cnf(u87385,axiom,
( ~ less_than(X1,n9)
| less_than(X0,n13)
| ~ less_than(X0,X1) ) ).
cnf(u1103,axiom,
( less_than(X0,n13)
| ~ less_than(X0,n8) ) ).
cnf(u87477,axiom,
( ~ less_than(X0,n7)
| green(X0,n10)
| red(X0,n10) ) ).
cnf(u86324,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n11)
| ~ red(n4,X0) ) ).
cnf(u84677,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,X1) ) ).
cnf(u806,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n15) ) ).
cnf(u86138,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X0,n16)
| ~ green(X1,n16)
| ~ green(X0,X1) ) ).
cnf(u2381,axiom,
less_than(n2,n11) ).
cnf(u40491,axiom,
( ~ less_than(X0,n5)
| green(X0,n7)
| red(X0,n7) ) ).
cnf(u1070,axiom,
( less_than(X0,n11)
| ~ less_than(X0,n8) ) ).
cnf(u2007,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n9) ) ).
cnf(u86054,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,X1) ) ).
cnf(u86873,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X0,n17)
| ~ green(n1,X0) ) ).
cnf(u238,axiom,
( less_than(X0,n12)
| ~ less_than(X0,n10) ) ).
cnf(u87728,axiom,
( ~ less_than(X0,n9)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u40739,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n3) ) ).
cnf(u86129,negated_conjecture,
( ~ green(X0,n1)
| ~ green(X1,n1)
| ~ green(X0,n16)
| ~ green(X1,n16)
| ~ green(X0,X1) ) ).
cnf(u88271,axiom,
( ~ less_than(X1,n4)
| ~ less_than(X0,X1)
| less_than(X0,n11) ) ).
cnf(u4064,axiom,
( less_than(X0,n9)
| ~ less_than(X0,n6) ) ).
cnf(u40678,axiom,
( ~ less_than(X0,n13)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u87727,axiom,
( ~ less_than(X0,n9)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u1518,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n14) ) ).
cnf(u86521,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X0,n15)
| ~ green(n3,X0) ) ).
cnf(u8125,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n8) ) ).
cnf(u40734,axiom,
( ~ less_than(X0,n5)
| ~ less_than(X1,X0)
| less_than(X1,n8) ) ).
cnf(u86898,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X0,n14)
| ~ red(n1,X0) ) ).
cnf(u1068,axiom,
less_than(n8,n12) ).
cnf(u86213,negated_conjecture,
( ~ green(n8,X0)
| ~ green(X0,n14)
| ~ green(X0,n12) ) ).
cnf(u8387,axiom,
( ~ less_than(X0,n15)
| red(X0,n17)
| green(X0,n17) ) ).
cnf(u724,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n7) ) ).
cnf(u471,axiom,
less_than(n1,n5) ).
cnf(u85993,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(X0,X1) ) ).
cnf(u1173,axiom,
( less_than(X0,n13)
| ~ less_than(X0,n9) ) ).
cnf(u58,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n15) ) ).
cnf(u86287,negated_conjecture,
( ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,n16)
| ~ green(X1,n16)
| ~ green(X0,X1) ) ).
cnf(u40725,axiom,
( ~ less_than(X0,n12)
| ~ less_than(X1,X0)
| less_than(X1,n15) ) ).
cnf(u40553,axiom,
( ~ less_than(X0,n14)
| ~ less_than(X1,X0)
| less_than(X1,n16) ) ).
cnf(u236,axiom,
less_than(n10,n13) ).
cnf(u82709,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,X1) ) ).
cnf(u86658,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X0,n11)
| ~ green(n3,X0) ) ).
cnf(u87590,axiom,
( ~ less_than(X0,n7)
| red(X0,n12)
| green(X0,n12) ) ).
cnf(u322,axiom,
less_than(n5,n8) ).
cnf(u84889,negated_conjecture,
( ~ red(X1,n12)
| ~ red(X1,n11)
| ~ red(X0,n12)
| ~ red(X0,n11)
| ~ red(X0,X1) ) ).
cnf(u86077,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X0,n8)
| ~ green(X0,n9) ) ).
cnf(u87878,axiom,
( ~ less_than(X1,n6)
| less_than(X0,n13)
| ~ less_than(X0,X1) ) ).
cnf(u59,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n16) ) ).
cnf(u1516,axiom,
less_than(n5,n15) ).
cnf(u1424,axiom,
( less_than(X0,n8)
| ~ less_than(X0,n5) ) ).
cnf(u84849,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,X1) ) ).
cnf(u2068,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n15) ) ).
cnf(u4109,axiom,
less_than(n6,n13) ).
cnf(u56,axiom,
( ~ less_than(X0,n13)
| less_than(X0,n14) ) ).
cnf(u506,axiom,
less_than(n7,n14) ).
cnf(u86133,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,X1) ) ).
cnf(u88043,axiom,
( ~ less_than(X0,n8)
| green(X0,n15)
| red(X0,n15) ) ).
cnf(u87108,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X0,n16)
| ~ red(n4,X0) ) ).
cnf(u226,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n13) ) ).
cnf(u264,axiom,
( less_than(X0,n14)
| ~ less_than(X0,n12) ) ).
cnf(u86098,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X1,n2)
| ~ green(X0,n7)
| ~ green(X1,n7)
| ~ green(X0,X1) ) ).
cnf(u1891,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n10) ) ).
cnf(u1089,axiom,
less_than(n8,n13) ).
cnf(u85030,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n10)
| ~ red(n2,X0) ) ).
cnf(u86089,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X0,X1) ) ).
cnf(u87688,axiom,
( ~ less_than(X0,n7)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u57,axiom,
( ~ less_than(X0,n14)
| less_than(X0,n15) ) ).
cnf(u86541,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X0,n13)
| ~ green(n2,X0) ) ).
cnf(u86275,negated_conjecture,
( ~ green(X0,n11)
| ~ green(X0,n15)
| ~ green(X0,n16) ) ).
cnf(u87747,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n10)
| ~ less_than(X0,X1) ) ).
cnf(u459,axiom,
less_than(n2,n4) ).
cnf(u86860,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X0,n17)
| ~ green(n3,X0) ) ).
cnf(u2417,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n14) ) ).
cnf(u2005,axiom,
less_than(n4,n10) ).
cnf(u1171,axiom,
less_than(n9,n14) ).
cnf(u87546,axiom,
( ~ less_than(X1,n9)
| ~ less_than(X0,X1)
| less_than(X0,n16) ) ).
cnf(u88570,axiom,
( ~ less_than(X0,n4)
| green(X0,n12)
| red(X0,n12) ) ).
cnf(u224,axiom,
less_than(n13,n15) ).
cnf(u2019,axiom,
less_than(n4,n11) ).
cnf(u83887,negated_conjecture,
( ~ red(X1,n13)
| ~ red(X1,n12)
| ~ red(X0,n13)
| ~ red(X0,n12)
| ~ red(X0,X1) ) ).
cnf(u2059,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n14) ) ).
cnf(u87678,axiom,
( ~ less_than(X0,n3)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u85284,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,X1) ) ).
cnf(u86179,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,n15)
| ~ red(X1,n15)
| ~ red(X0,X1) ) ).
cnf(u86065,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,X1) ) ).
cnf(u88822,axiom,
( ~ less_than(X1,n5)
| ~ less_than(X0,X1)
| less_than(X0,n15) ) ).
cnf(u86152,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u4092,axiom,
less_than(n6,n11) ).
cnf(u87577,axiom,
( ~ less_than(X0,n7)
| less_than(X1,n16)
| ~ less_than(X1,X0) ) ).
cnf(u40746,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n10) ) ).
cnf(u87607,axiom,
( ~ less_than(X0,n10)
| red(X0,n15)
| green(X0,n15) ) ).
cnf(u86429,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X0,n13)
| ~ green(n2,X0) ) ).
cnf(u86457,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,n17)
| ~ red(X1,n17)
| ~ red(X0,X1) ) ).
cnf(u940,axiom,
less_than(n3,n11) ).
cnf(u86533,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X0,n11)
| ~ green(n6,X0) ) ).
cnf(u2057,axiom,
less_than(n4,n15) ).
cnf(u86809,negated_conjecture,
( ~ green(X0,n13)
| ~ green(X0,n16)
| ~ green(n6,X0) ) ).
cnf(u86547,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,n17)
| ~ red(X1,n17)
| ~ red(X0,X1) ) ).
cnf(u40492,axiom,
( ~ less_than(X0,n5)
| ~ less_than(X1,X0)
| less_than(X1,n7) ) ).
cnf(u40737,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n17) ) ).
cnf(u324,axiom,
( less_than(X0,n7)
| ~ less_than(X0,n5) ) ).
cnf(u86278,negated_conjecture,
( ~ red(X0,n14)
| ~ red(X1,n14)
| ~ red(X0,n16)
| ~ red(X1,n16)
| ~ red(X0,X1) ) ).
cnf(u719,axiom,
less_than(n7,n15) ).
cnf(u974,axiom,
less_than(n3,n15) ).
cnf(u88729,axiom,
( ~ less_than(X0,n5)
| green(X0,n13)
| red(X0,n13) ) ).
cnf(u86233,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(X0,n16)
| ~ green(X1,n16)
| ~ green(X0,X1) ) ).
cnf(u85232,negated_conjecture,
( ~ green(X1,n11)
| ~ green(X1,n10)
| ~ green(X0,n11)
| ~ green(X0,n10)
| ~ green(X0,X1) ) ).
cnf(u50,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n8) ) ).
cnf(u508,axiom,
( ~ less_than(X0,n7)
| less_than(X0,n13) ) ).
cnf(u85063,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,n12)
| ~ green(X1,n12)
| ~ green(X0,X1) ) ).
cnf(u86214,negated_conjecture,
( ~ green(n4,X0)
| ~ green(X0,n14)
| ~ green(X0,n12) ) ).
cnf(u87651,axiom,
( ~ less_than(X0,n9)
| red(X0,n14)
| green(X0,n14) ) ).
cnf(u88515,axiom,
( ~ less_than(X0,n4)
| red(X0,n11)
| green(X0,n11) ) ).
cnf(u40482,axiom,
( ~ less_than(X0,n7)
| ~ less_than(X1,X0)
| less_than(X1,n9) ) ).
cnf(u518,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n7) ) ).
cnf(u51,axiom,
( ~ less_than(X0,n8)
| less_than(X0,n9) ) ).
cnf(u86078,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X0,n9)
| ~ green(n5,X0) ) ).
cnf(u87850,axiom,
( ~ less_than(X0,n6)
| green(X0,n15)
| red(X0,n15) ) ).
cnf(u40495,axiom,
( ~ less_than(X0,n9)
| ~ less_than(X1,X0)
| less_than(X1,n11) ) ).
cnf(u88074,axiom,
( ~ less_than(X0,n6)
| green(X0,n14)
| red(X0,n14) ) ).
cnf(u86001,negated_conjecture,
( ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,n15)
| ~ green(X1,n15)
| ~ green(X0,X1) ) ).
cnf(u765,axiom,
less_than(n1,n12) ).
cnf(u8131,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n14) ) ).
cnf(u87623,axiom,
( ~ less_than(X0,n9)
| red(X0,n13)
| green(X0,n13) ) ).
cnf(u86069,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,n15)
| ~ green(X1,n15)
| ~ green(X0,X1) ) ).
cnf(u86416,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n17)
| ~ red(X1,n17)
| ~ red(X0,X1) ) ).
cnf(u48,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n6) ) ).
cnf(u87151,negated_conjecture,
( ~ red(n5,X0)
| ~ red(X0,n17)
| ~ red(X0,n13) ) ).
cnf(u87755,axiom,
( ~ less_than(X1,n7)
| less_than(X0,n14)
| ~ less_than(X0,X1) ) ).
cnf(u87777,axiom,
( ~ less_than(X0,n9)
| ~ less_than(X1,X0)
| less_than(X1,n15) ) ).
cnf(u86953,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n15)
| ~ red(n7,X0) ) ).
cnf(u8122,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n5) ) ).
cnf(u87756,axiom,
( ~ less_than(X1,n8)
| less_than(X0,n14)
| ~ less_than(X0,X1) ) ).
cnf(u86076,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,X1) ) ).
cnf(u395,axiom,
less_than(n3,n6) ).
cnf(u49,axiom,
( ~ less_than(X0,n6)
| less_than(X0,n7) ) ).
cnf(u86311,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X0,n10)
| ~ red(X0,n12) ) ).
cnf(u757,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n10) ) ).
cnf(u40468,axiom,
( ~ less_than(X0,n8)
| green(X0,n10)
| red(X0,n10) ) ).
cnf(u88775,axiom,
( ~ less_than(X0,n4)
| green(X0,n13)
| red(X0,n13) ) ).
cnf(u87134,negated_conjecture,
( ~ red(X0,n10)
| ~ red(X0,n16)
| ~ red(n4,X0) ) ).
cnf(u87405,axiom,
( ~ less_than(X1,n7)
| less_than(X0,n11)
| ~ less_than(X0,X1) ) ).
cnf(u40744,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n8) ) ).
cnf(u88533,axiom,
( ~ less_than(X0,n5)
| red(X0,n14)
| green(X0,n14) ) ).
cnf(u54,axiom,
( ~ less_than(X0,n11)
| less_than(X0,n12) ) ).
cnf(u86939,negated_conjecture,
( ~ red(X0,n11)
| ~ red(X0,n14)
| ~ red(n5,X0) ) ).
cnf(u86032,negated_conjecture,
( ~ red(X1,n12)
| ~ red(X1,n10)
| ~ red(X0,n12)
| ~ red(X0,n10)
| ~ red(X0,X1) ) ).
cnf(u87516,axiom,
( ~ less_than(X0,n10)
| red(X0,n16)
| green(X0,n16) ) ).
cnf(u262,axiom,
less_than(n12,n15) ).
cnf(u88209,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n15)
| ~ less_than(X0,X1) ) ).
cnf(u84367,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,n11)
| ~ green(X1,n11)
| ~ green(X0,X1) ) ).
cnf(u86759,negated_conjecture,
( ~ red(n6,X0)
| ~ red(X0,n17)
| ~ red(X0,n15) ) ).
cnf(u337,axiom,
( less_than(X0,n10)
| ~ less_than(X0,n8) ) ).
cnf(u1215,axiom,
less_than(n9,n15) ).
cnf(u87161,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X0,n17)
| ~ red(n5,X0) ) ).
cnf(u87578,axiom,
( ~ less_than(X0,n7)
| ~ less_than(X1,X0)
| less_than(X1,n13) ) ).
cnf(u2328,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n6) ) ).
cnf(u40743,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n7) ) ).
cnf(u85384,negated_conjecture,
( ~ red(X0,n6)
| ~ red(X1,n6)
| ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,X1) ) ).
cnf(u434,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n8) ) ).
cnf(u55,axiom,
( ~ less_than(X0,n12)
| less_than(X0,n13) ) ).
cnf(u86188,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,n9)
| ~ red(X1,n9)
| ~ red(X0,X1) ) ).
cnf(u86420,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,n17)
| ~ red(X1,n17)
| ~ red(X0,X1) ) ).
cnf(u40713,axiom,
( ~ less_than(X0,n4)
| green(X0,n7)
| red(X0,n7) ) ).
cnf(u775,axiom,
less_than(n1,n13) ).
cnf(u1447,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n9) ) ).
cnf(u86760,negated_conjecture,
( ~ red(X0,n15)
| ~ red(X0,n17)
| ~ red(n2,X0) ) ).
cnf(u86393,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u86029,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,X1) ) ).
cnf(u260,axiom,
less_than(n11,n14) ).
cnf(u86085,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X1,n6)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,X1) ) ).
cnf(u52,axiom,
( ~ less_than(X0,n9)
| less_than(X0,n10) ) ).
cnf(u86831,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X0,n16)
| ~ green(n1,X0) ) ).
cnf(u985,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n15) ) ).
cnf(u40550,axiom,
( ~ less_than(X0,n14)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u966,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n13) ) ).
cnf(u86297,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,n16)
| ~ red(X1,n16)
| ~ red(X0,X1) ) ).
cnf(u53,axiom,
( ~ less_than(X0,n10)
| less_than(X0,n11) ) ).
cnf(u88674,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n14)
| ~ less_than(X0,X1) ) ).
cnf(u444,axiom,
( ~ less_than(X0,n16)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u87768,axiom,
( ~ less_than(X0,n8)
| green(X0,n14)
| red(X0,n14) ) ).
cnf(u1502,axiom,
less_than(n5,n13) ).
cnf(u40458,axiom,
( ~ less_than(X0,n6)
| green(X0,n8)
| red(X0,n8) ) ).
cnf(u399,axiom,
( less_than(X0,n6)
| ~ less_than(X0,n4) ) ).
cnf(u88551,axiom,
( ~ less_than(X0,n4)
| red(X0,n15)
| green(X0,n15) ) ).
cnf(u1166,axiom,
less_than(n9,n13) ).
cnf(u2038,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n12) ) ).
cnf(u1222,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n9) ) ).
cnf(u42,negated_conjecture,
( ~ green(X2,X3)
| ~ green(X0,X2)
| ~ green(X1,X2)
| ~ green(X0,X3)
| ~ green(X1,X3)
| ~ green(X0,X1) ) ).
cnf(u87621,axiom,
( ~ less_than(X0,n7)
| red(X0,n13)
| green(X0,n13) ) ).
cnf(u86225,negated_conjecture,
( ~ red(X0,n9)
| ~ red(X0,n14)
| ~ red(X0,n15) ) ).
cnf(u2359,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n8) ) ).
cnf(u87635,axiom,
( ~ less_than(X0,n6)
| red(X0,n10)
| green(X0,n10) ) ).
cnf(u87512,axiom,
( ~ less_than(X0,n5)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u8129,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n12) ) ).
cnf(u85569,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n16)
| ~ red(X1,n16)
| ~ red(X0,X1) ) ).
cnf(u40471,axiom,
( ~ less_than(X0,n12)
| green(X0,n14)
| red(X0,n14) ) ).
cnf(u86126,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,X1) ) ).
cnf(u737,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n8) ) ).
cnf(u634,axiom,
less_than(n3,n10) ).
cnf(u397,axiom,
less_than(n4,n7) ).
cnf(u43,negated_conjecture,
( ~ red(X2,X3)
| ~ red(X0,X2)
| ~ red(X1,X2)
| ~ red(X0,X3)
| ~ red(X1,X3)
| ~ red(X0,X1) ) ).
cnf(u8120,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n16) ) ).
cnf(u86017,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,X1) ) ).
cnf(u84892,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,X1) ) ).
cnf(u86061,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X1,n2)
| ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,X1) ) ).
cnf(u275,axiom,
( less_than(X0,n14)
| ~ less_than(X0,n11) ) ).
cnf(u87652,axiom,
( ~ less_than(X0,n10)
| red(X0,n14)
| green(X0,n14) ) ).
cnf(u8119,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n16) ) ).
cnf(u40,axiom,
( ~ less_than(X0,X1)
| green(X0,X1)
| red(X0,X1) ) ).
cnf(u2357,axiom,
less_than(n2,n9) ).
cnf(u40755,axiom,
( ~ less_than(X0,n12)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u87686,axiom,
( ~ less_than(X0,n7)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u86026,negated_conjecture,
( ~ green(X0,n13)
| ~ green(X1,n13)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,X1) ) ).
cnf(u86409,negated_conjecture,
( ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,n17)
| ~ red(X1,n17)
| ~ red(X0,X1) ) ).
cnf(u86861,negated_conjecture,
( ~ green(X0,n4)
| ~ green(X0,n17)
| ~ green(n1,X0) ) ).
cnf(u84468,negated_conjecture,
( ~ green(X0,n10)
| ~ green(X1,n10)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,X1) ) ).
cnf(u432,axiom,
less_than(n3,n9) ).
cnf(u87396,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n9)
| ~ less_than(X0,X1) ) ).
cnf(u87566,axiom,
( ~ less_than(X0,n6)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u4127,axiom,
less_than(n6,n15) ).
cnf(u41,negated_conjecture,
~ goal ).
cnf(u40741,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n5) ) ).
cnf(u976,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n14) ) ).
cnf(u86886,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X0,n13)
| ~ red(n3,X0) ) ).
cnf(u1757,axiom,
( less_than(X0,n14)
| ~ less_than(X0,n10) ) ).
cnf(u40677,axiom,
( ~ less_than(X0,n13)
| green(X0,n17)
| red(X0,n17) ) ).
cnf(u86163,negated_conjecture,
( ~ red(X0,n3)
| ~ red(X1,n3)
| ~ red(X0,n13)
| ~ red(X1,n13)
| ~ red(X0,X1) ) ).
cnf(u87070,negated_conjecture,
( ~ red(X0,n12)
| ~ red(X0,n17)
| ~ red(n2,X0) ) ).
cnf(u86794,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X0,n16)
| ~ green(n6,X0) ) ).
cnf(u273,axiom,
less_than(n11,n15) ).
cnf(u40750,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n14) ) ).
cnf(u86023,negated_conjecture,
( ~ green(X1,n3)
| ~ green(X1,n2)
| ~ green(X0,n3)
| ~ green(X0,n2)
| ~ green(X0,X1) ) ).
cnf(u86207,negated_conjecture,
( ~ green(n10,X0)
| ~ green(X0,n15)
| ~ green(X0,n13) ) ).
cnf(u46,axiom,
( ~ less_than(X0,n3)
| less_than(X0,n4) ) ).
cnf(u86107,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X0,n4)
| ~ green(n2,X0) ) ).
cnf(u40720,axiom,
( ~ less_than(X0,n10)
| green(X0,n13)
| red(X0,n13) ) ).
cnf(u87732,axiom,
( ~ less_than(X0,n6)
| ~ less_than(X1,X0)
| less_than(X1,n12) ) ).
cnf(u87838,axiom,
( ~ less_than(X0,n7)
| green(X0,n14)
| red(X0,n14) ) ).
cnf(u86329,negated_conjecture,
( ~ red(X0,n12)
| ~ red(X1,n12)
| ~ red(X0,n17)
| ~ red(X1,n17)
| ~ red(X0,X1) ) ).
cnf(u47,axiom,
( ~ less_than(X0,n4)
| less_than(X0,n5) ) ).
cnf(u84611,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X1,n5)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(X0,X1) ) ).
cnf(u4153,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n6) ) ).
cnf(u86403,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X1,n9)
| ~ green(X0,n17)
| ~ green(X1,n17)
| ~ green(X0,X1) ) ).
cnf(u87634,axiom,
( ~ less_than(X0,n5)
| red(X0,n10)
| green(X0,n10) ) ).
cnf(u86080,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(X0,X1) ) ).
cnf(u85930,negated_conjecture,
( ~ red(X0,n4)
| ~ red(X1,n4)
| ~ red(X0,n7)
| ~ red(X1,n7)
| ~ red(X0,X1) ) ).
cnf(u745,axiom,
less_than(n1,n10) ).
cnf(u86005,negated_conjecture,
( ~ green(X0,n3)
| ~ green(X1,n3)
| ~ green(X0,n4)
| ~ green(X1,n4)
| ~ green(X0,X1) ) ).
cnf(u87545,axiom,
( ~ less_than(X1,n8)
| ~ less_than(X0,X1)
| less_than(X0,n16) ) ).
cnf(u40456,axiom,
( ~ less_than(X0,n4)
| ~ less_than(X1,X0)
| less_than(X1,n6) ) ).
cnf(u88584,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n13)
| ~ less_than(X0,X1) ) ).
cnf(u40469,axiom,
( ~ less_than(X0,n8)
| ~ less_than(X1,X0)
| less_than(X1,n10) ) ).
cnf(u86557,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X0,n9)
| ~ green(n1,X0) ) ).
cnf(u44,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n2) ) ).
cnf(u86105,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X1,n8)
| ~ green(X0,n14)
| ~ green(X1,n14)
| ~ green(X0,X1) ) ).
cnf(u86984,negated_conjecture,
( ~ green(X0,n9)
| ~ green(X0,n17)
| ~ green(n8,X0) ) ).
cnf(u86114,negated_conjecture,
( ~ green(n4,X0)
| ~ green(X0,n14)
| ~ green(X0,n13) ) ).
cnf(u87703,axiom,
( ~ less_than(X0,n8)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u86161,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n10)
| ~ red(n4,X0) ) ).
cnf(u335,axiom,
less_than(n8,n11) ).
cnf(u86641,negated_conjecture,
( ~ green(X0,n8)
| ~ green(X0,n12)
| ~ green(n5,X0) ) ).
cnf(u86785,negated_conjecture,
( ~ green(X0,n12)
| ~ green(X0,n16)
| ~ green(n1,X0) ) ).
cnf(u45,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n3) ) ).
cnf(u87704,axiom,
( ~ less_than(X0,n8)
| green(X0,n16)
| red(X0,n16) ) ).
cnf(u215,axiom,
( less_than(X0,n13)
| ~ less_than(X0,n11) ) ).
cnf(u1494,axiom,
( ~ less_than(X0,n5)
| less_than(X0,n11) ) ).
cnf(u767,axiom,
( ~ less_than(X0,n1)
| less_than(X0,n11) ) ).
cnf(u88841,axiom,
( ~ less_than(X1,n5)
| ~ less_than(X0,X1)
| less_than(X0,n14) ) ).
cnf(u1568,axiom,
( less_than(X0,n13)
| ~ less_than(X0,n10) ) ).
cnf(u86963,negated_conjecture,
( ~ red(X0,n8)
| ~ red(X0,n15)
| ~ red(n2,X0) ) ).
cnf(u34,axiom,
less_than(n2,n3) ).
cnf(u86938,negated_conjecture,
( ~ red(n9,X0)
| ~ red(X0,n14)
| ~ red(X0,n11) ) ).
cnf(u87485,axiom,
( ~ less_than(X0,n11)
| red(X0,n17)
| green(X0,n17) ) ).
cnf(u8117,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n15) ) ).
cnf(u85873,negated_conjecture,
( ~ green(X0,n6)
| ~ green(X0,n7)
| ~ green(n2,X0) ) ).
cnf(u86221,negated_conjecture,
( ~ red(X0,n1)
| ~ red(X1,n1)
| ~ red(X0,n8)
| ~ red(X1,n8)
| ~ red(X0,X1) ) ).
cnf(u86502,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X0,n8)
| ~ green(n3,X0) ) ).
cnf(u8126,axiom,
( less_than(X0,n16)
| ~ less_than(X0,n9) ) ).
cnf(u370,axiom,
less_than(n7,n13) ).
cnf(u2299,axiom,
less_than(n2,n6) ).
cnf(u86739,negated_conjecture,
( ~ green(X0,n5)
| ~ green(X0,n7)
| ~ green(X0,n10) ) ).
cnf(u86084,negated_conjecture,
( ~ red(X0,n5)
| ~ red(X1,n5)
| ~ red(X0,n11)
| ~ red(X1,n11)
| ~ red(X0,X1) ) ).
cnf(u333,axiom,
less_than(n7,n10) ).
cnf(u87622,axiom,
( ~ less_than(X0,n8)
| red(X0,n13)
| green(X0,n13) ) ).
cnf(u87687,axiom,
( ~ less_than(X0,n7)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u87122,negated_conjecture,
( ~ red(X0,n7)
| ~ red(X0,n16)
| ~ red(n3,X0) ) ).
cnf(u40731,axiom,
( ~ less_than(X0,n9)
| ~ less_than(X1,X0)
| less_than(X1,n12) ) ).
cnf(u87371,axiom,
( ~ less_than(X1,n9)
| less_than(X0,n14)
| ~ less_than(X0,X1) ) ).
cnf(u46677,negated_conjecture,
~ green(n8,n5) ).
cnf(u35,axiom,
less_than(n1,n2) ).
cnf(u2407,axiom,
( ~ less_than(X0,n2)
| less_than(X0,n13) ) ).
cnf(u87332,axiom,
( ~ less_than(X1,n4)
| less_than(X0,n8)
| ~ less_than(X0,X1) ) ).
cnf(u213,axiom,
less_than(n11,n13) ).
cnf(u86567,negated_conjecture,
( ~ green(X0,n7)
| ~ green(X0,n12)
| ~ green(n5,X0) ) ).
cnf(u1492,axiom,
less_than(n5,n12) ).
cnf(u312,axiom,
( less_than(X0,n11)
| ~ less_than(X0,n9) ) ).
cnf(u86268,negated_conjecture,
( ~ red(X1,n17)
| ~ red(X1,n16)
| ~ red(X0,n17)
| ~ red(X0,n16)
| ~ red(X0,X1) ) ).
cnf(u86636,negated_conjecture,
( ~ green(X0,n2)
| ~ green(X0,n7)
| ~ green(n1,X0) ) ).
cnf(u1101,axiom,
less_than(n8,n14) ).
cnf(u87475,axiom,
( ~ less_than(X0,n7)
| ~ less_than(X1,X0)
| less_than(X1,n12) ) ).
cnf(u87644,axiom,
( ~ less_than(X0,n5)
| red(X0,n9)
| green(X0,n9) ) ).
cnf(u87679,axiom,
( ~ less_than(X0,n3)
| ~ less_than(X1,X0)
| less_than(X1,n17) ) ).
cnf(u86294,negated_conjecture,
( ~ red(X0,n2)
| ~ red(X1,n2)
| ~ red(X0,n16)
| ~ red(X1,n16)
| ~ red(X0,X1) ) ).
cnf(u40748,axiom,
( less_than(X0,n17)
| ~ less_than(X0,n12) ) ).
cnf(u87890,axiom,
( ~ less_than(X1,n7)
| less_than(X0,n15)
| ~ less_than(X0,X1) ) ).
cnf(u32,axiom,
less_than(n4,n5) ).
cnf(u1157,axiom,
( less_than(X0,n15)
| ~ less_than(X0,n12) ) ).
cnf(u87455,axiom,
less_than(n2,n16) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA018+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n008.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 08:49:54 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.44 Running first-order theorem proving
% 0.13/0.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.08/2.61 % (932283)Detected formulas, will run a generic FOF schedule.
% 12.08/2.61 % (932395)dis-21_1_sil=8000:lcm=predicate:random_seed=595040881:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.08/2.61 % (932395)Instruction limit reached!
% 12.08/2.61 % (932395)------------------------------
% 12.08/2.61 % (932395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.08/2.61 % (932395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.08/2.61 % (932395)CaDiCaL version: 2.1.3
% 12.08/2.61 % (932395)Termination reason: Instruction limit
% 12.08/2.61 % (932395)Termination phase: Saturation
% 12.08/2.61 % (932395)Time elapsed: 0.031 s
% 12.08/2.61 % (932395)Peak memory usage: 88 MB
% 12.08/2.61 % (932395)Instructions burned: 135 (million)
% 12.08/2.61 % (932394)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3724185556:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.08/2.61 % (932393)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3000219206:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.08/2.61 % (932391)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2492579040:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.08/2.61 % (932390)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=476201063:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.08/2.61 % (932389)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3248519902:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.08/2.61 % (932393)Refutation not found, incomplete strategy
% 12.08/2.61 % (932393)------------------------------
% 12.08/2.61 % (932393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.08/2.61 % (932393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.08/2.61 % (932393)CaDiCaL version: 2.1.3
% 12.08/2.61 % (932393)Termination reason: Refutation not found, incomplete strategy
% 12.08/2.61 % (932393)Time elapsed: 0.0000 s
% 12.08/2.61 % (932393)Peak memory usage: 86 MB
% 12.08/2.61 % (932392)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2411436796:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.08/2.61 % (932392)Refutation not found, incomplete strategy
% 12.08/2.61 % (932392)------------------------------
% 12.08/2.61 % (932392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.08/2.61 % (932392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.08/2.61 % (932392)CaDiCaL version: 2.1.3
% 12.08/2.61 % (932392)Termination reason: Refutation not found, incomplete strategy
% 12.08/2.61 % (932392)Time elapsed: 0.001 s
% 12.08/2.61 % (932392)Peak memory usage: 86 MB
% 12.08/2.61 % (932394)Instruction limit reached!
% 12.08/2.61 % (932394)------------------------------
% 12.08/2.61 % (932394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.08/2.61 % (932394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.08/2.61 % (932394)CaDiCaL version: 2.1.3
% 12.08/2.61 % (932394)Termination reason: Instruction limit
% 12.08/2.61 % (932394)Termination phase: Saturation
% 12.08/2.61 % (932394)Time elapsed: 0.070 s
% 12.08/2.61 % (932394)Peak memory usage: 88 MB
% 12.08/2.61 % (932394)Instructions burned: 139 (million)
% 12.08/2.61 % (932402)lrs+10_1_sil=8000:sp=occurrence:random_seed=3196840281:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.08/2.61 % (932402)Instruction limit reached!
% 12.08/2.61 % (932402)------------------------------
% 12.08/2.61 % (932402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.08/2.61 % (932402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.08/2.61 % (932402)CaDiCaL version: 2.1.3
% 12.08/2.61 % (932402)Termination reason: Instruction limit
% 12.08/2.61 % (932402)Termination phase: Saturation
% 12.08/2.61 % (932402)Time elapsed: 0.114 s
% 12.08/2.61 % (932402)Peak memory usage: 91 MB
% 12.08/2.61 % (932402)Instructions burned: 288 (million)
% 12.08/2.61 % (932393)------------------------------
% 12.08/2.61 % (932393)------------------------------
% 12.08/2.61 % (932410)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2118139662:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 20.50/3.80 % (932410)Refutation not found, incomplete strategy
% 20.50/3.80 % (932410)------------------------------
% 20.50/3.80 % (932410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.80 % (932410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.80 % (932410)CaDiCaL version: 2.1.3
% 20.50/3.80 % (932410)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.80 % (932410)Time elapsed: 0.001 s
% 20.50/3.80 % (932410)Peak memory usage: 87 MB
% 20.50/3.80 % (932392)------------------------------
% 20.50/3.80 % (932392)------------------------------
% 20.50/3.80 % (932436)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3220388248:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 20.50/3.80 % (932436)Refutation not found, incomplete strategy
% 20.50/3.80 % (932436)------------------------------
% 20.50/3.80 % (932436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.80 % (932436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.80 % (932436)CaDiCaL version: 2.1.3
% 20.50/3.80 % (932436)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.80 % (932436)Time elapsed: 0.0000 s
% 20.50/3.80 % (932436)Peak memory usage: 87 MB
% 20.50/3.80 % (932443)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1927506694:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 20.50/3.80 % (932443)Refutation not found, incomplete strategy
% 20.50/3.80 % (932443)------------------------------
% 20.50/3.80 % (932443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.80 % (932443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.80 % (932443)CaDiCaL version: 2.1.3
% 20.50/3.80 % (932443)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.80 % (932443)Time elapsed: 0.009 s
% 20.50/3.80 % (932443)Peak memory usage: 88 MB
% 20.50/3.80 % (932443)Instructions burned: 17 (million)
% 20.50/3.80 % (932451)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2292679667:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.50/3.80 % (932451)Refutation not found, incomplete strategy
% 20.50/3.80 % (932451)------------------------------
% 20.50/3.80 % (932451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.80 % (932451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.80 % (932451)CaDiCaL version: 2.1.3
% 20.50/3.80 % (932451)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.80 % (932451)Time elapsed: 0.001 s
% 20.50/3.80 % (932451)Peak memory usage: 86 MB
% 20.50/3.80 % (932436)------------------------------
% 20.50/3.80 % (932436)------------------------------
% 20.50/3.80 % (932410)------------------------------
% 20.50/3.80 % (932410)------------------------------
% 20.50/3.80 % (932534)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3005991992:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 20.50/3.80 % (932443)------------------------------
% 20.50/3.80 % (932443)------------------------------
% 20.50/3.80 % (932451)------------------------------
% 20.50/3.80 % (932451)------------------------------
% 20.50/3.80 % (932538)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=234131254:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 20.50/3.80 % (932538)Instruction limit reached!
% 20.50/3.80 % (932538)------------------------------
% 20.50/3.80 % (932538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.80 % (932538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.80 % (932538)CaDiCaL version: 2.1.3
% 20.50/3.80 % (932538)Termination reason: Instruction limit
% 20.50/3.80 % (932538)Termination phase: Saturation
% 20.50/3.80 % (932538)Time elapsed: 0.060 s
% 20.50/3.80 % (932538)Peak memory usage: 89 MB
% 20.50/3.80 % (932538)Instructions burned: 114 (million)
% 20.50/3.80 % (932551)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=396755150:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 20.50/3.80 % (932553)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=481640669:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 20.50/3.80 % (932551)Instruction limit reached!
% 20.50/3.80 % (932551)------------------------------
% 37.96/6.24 % (932551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.96/6.24 % (932551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.96/6.24 % (932551)CaDiCaL version: 2.1.3
% 37.96/6.24 % (932551)Termination reason: Instruction limit
% 37.96/6.24 % (932551)Termination phase: Saturation
% 37.96/6.24 % (932551)Time elapsed: 0.064 s
% 37.96/6.24 % (932551)Peak memory usage: 89 MB
% 37.96/6.24 % (932551)Instructions burned: 127 (million)
% 37.96/6.24 % (932574)lrs+10_1_sil=8000:sp=occurrence:random_seed=1638234783:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 37.96/6.24 % (932553)Instruction limit reached!
% 37.96/6.24 % (932553)------------------------------
% 37.96/6.24 % (932553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.96/6.24 % (932553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.96/6.24 % (932553)CaDiCaL version: 2.1.3
% 37.96/6.24 % (932553)Termination reason: Instruction limit
% 37.96/6.24 % (932553)Termination phase: Saturation
% 37.96/6.24 % (932553)Time elapsed: 0.057 s
% 37.96/6.24 % (932553)Peak memory usage: 90 MB
% 37.96/6.24 % (932553)Instructions burned: 115 (million)
% 37.96/6.24 % (932604)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1683409221:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 37.96/6.24 % (932604)Refutation not found, incomplete strategy
% 37.96/6.24 % (932604)------------------------------
% 37.96/6.24 % (932604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.96/6.24 % (932604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.96/6.24 % (932604)CaDiCaL version: 2.1.3
% 37.96/6.24 % (932604)Termination reason: Refutation not found, incomplete strategy
% 37.96/6.24 % (932604)Time elapsed: 0.001 s
% 37.96/6.24 % (932604)Peak memory usage: 87 MB
% 37.96/6.24 % (932606)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2465467034:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 37.96/6.24 % (932604)------------------------------
% 37.96/6.24 % (932604)------------------------------
% 37.96/6.24 % (932574)Instruction limit reached!
% 37.96/6.24 % (932574)------------------------------
% 37.96/6.24 % (932574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.96/6.24 % (932574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.96/6.24 % (932574)CaDiCaL version: 2.1.3
% 37.96/6.24 % (932574)Termination reason: Instruction limit
% 37.96/6.24 % (932574)Termination phase: Saturation
% 37.96/6.24 % (932574)Time elapsed: 0.464 s
% 37.96/6.24 % (932574)Peak memory usage: 93 MB
% 37.96/6.24 % (932574)Instructions burned: 908 (million)
% 37.96/6.24 % (932609)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=205344090:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 37.96/6.24 % (932609)Refutation not found, incomplete strategy
% 37.96/6.24 % (932609)------------------------------
% 37.96/6.24 % (932609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.96/6.24 % (932609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.96/6.24 % (932609)CaDiCaL version: 2.1.3
% 37.96/6.24 % (932609)Termination reason: Refutation not found, incomplete strategy
% 37.96/6.24 % (932609)Time elapsed: 0.022 s
% 37.96/6.24 % (932609)Peak memory usage: 89 MB
% 37.96/6.24 % (932609)Instructions burned: 44 (million)
% 37.96/6.24 % (932610)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2182205821:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 37.96/6.24 % (932610)Refutation not found, incomplete strategy
% 37.96/6.24 % (932610)------------------------------
% 37.96/6.24 % (932610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.96/6.24 % (932610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.96/6.24 % (932610)CaDiCaL version: 2.1.3
% 37.96/6.24 % (932610)Termination reason: Refutation not found, incomplete strategy
% 37.96/6.24 % (932610)Time elapsed: 0.001 s
% 37.96/6.24 % (932610)Peak memory usage: 87 MB
% 37.96/6.24 % (932534)Instruction limit reached!
% 37.96/6.24 % (932534)------------------------------
% 37.96/6.24 % (932534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.96/6.24 % (932534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.96/6.24 % (932534)CaDiCaL version: 2.1.3
% 37.96/6.24 % (932534)Termination reason: Instruction limit
% 62.02/9.60 % (932534)Termination phase: Saturation
% 62.02/9.60 % (932534)Time elapsed: 0.915 s
% 62.02/9.60 % (932534)Peak memory usage: 139 MB
% 62.02/9.60 % (932534)Instructions burned: 2350 (million)
% 62.02/9.60 % (932613)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3119865450:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 62.02/9.60 % (932609)------------------------------
% 62.02/9.60 % (932609)------------------------------
% 62.02/9.60 % (932610)------------------------------
% 62.02/9.60 % (932610)------------------------------
% 62.02/9.60 % (932615)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1197396956:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 62.02/9.60 % (932615)Refutation not found, incomplete strategy
% 62.02/9.60 % (932615)------------------------------
% 62.02/9.60 % (932615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.02/9.60 % (932615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.02/9.60 % (932615)CaDiCaL version: 2.1.3
% 62.02/9.60 % (932615)Termination reason: Refutation not found, incomplete strategy
% 62.02/9.60 % (932615)Time elapsed: 0.002 s
% 62.02/9.60 % (932615)Peak memory usage: 88 MB
% 62.02/9.60 % (932615)Instructions burned: 1 (million)
% 62.02/9.60 % (932616)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2949072016:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 62.02/9.60 % (932616)Instruction limit reached!
% 62.02/9.60 % (932616)------------------------------
% 62.02/9.60 % (932616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.02/9.60 % (932616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.02/9.60 % (932616)CaDiCaL version: 2.1.3
% 62.02/9.60 % (932616)Termination reason: Instruction limit
% 62.02/9.60 % (932616)Termination phase: Saturation
% 62.02/9.60 % (932616)Time elapsed: 0.072 s
% 62.02/9.60 % (932616)Peak memory usage: 90 MB
% 62.02/9.60 % (932616)Instructions burned: 134 (million)
% 62.02/9.60 % (932615)------------------------------
% 62.02/9.60 % (932615)------------------------------
% 62.02/9.60 % (932619)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2019247121:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 62.02/9.60 % (932619)Refutation not found, incomplete strategy
% 62.02/9.60 % (932619)------------------------------
% 62.02/9.60 % (932619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.02/9.60 % (932619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.02/9.60 % (932619)CaDiCaL version: 2.1.3
% 62.02/9.60 % (932619)Termination reason: Refutation not found, incomplete strategy
% 62.02/9.60 % (932619)Time elapsed: 0.001 s
% 62.02/9.60 % (932619)Peak memory usage: 87 MB
% 62.02/9.60 % (932620)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1299489096:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 62.02/9.60 % (932620)Refutation not found, incomplete strategy
% 62.02/9.60 % (932620)------------------------------
% 62.02/9.60 % (932620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.02/9.60 % (932620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.02/9.60 % (932620)CaDiCaL version: 2.1.3
% 62.02/9.60 % (932620)Termination reason: Refutation not found, incomplete strategy
% 62.02/9.60 % (932620)Time elapsed: 0.001 s
% 62.02/9.60 % (932620)Peak memory usage: 86 MB
% 62.02/9.60 % (932619)------------------------------
% 62.02/9.60 % (932619)------------------------------
% 62.02/9.60 % (932620)------------------------------
% 62.02/9.60 % (932620)------------------------------
% 62.02/9.60 % (932623)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=305689918:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 62.02/9.60 % (932624)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1008599902:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 62.02/9.60 % (932624)Refutation not found, incomplete strategy
% 62.02/9.60 % (932624)------------------------------
% 62.02/9.60 % (932624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.22/13.74 % (932624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.74 % (932624)CaDiCaL version: 2.1.3
% 91.22/13.74 % (932624)Termination reason: Refutation not found, incomplete strategy
% 91.22/13.74 % (932624)Time elapsed: 0.035 s
% 91.22/13.74 % (932624)Peak memory usage: 90 MB
% 91.22/13.74 % (932624)Instructions burned: 59 (million)
% 91.22/13.74 % (932624)------------------------------
% 91.22/13.74 % (932624)------------------------------
% 91.22/13.74 % (932627)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2812164009:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 91.22/13.74 % (932606)Instruction limit reached!
% 91.22/13.74 % (932606)------------------------------
% 91.22/13.74 % (932606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.22/13.74 % (932606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.74 % (932606)CaDiCaL version: 2.1.3
% 91.22/13.74 % (932606)Termination reason: Instruction limit
% 91.22/13.74 % (932606)Termination phase: Saturation
% 91.22/13.74 % (932606)Time elapsed: 2.537 s
% 91.22/13.74 % (932606)Peak memory usage: 136 MB
% 91.22/13.74 % (932606)Instructions burned: 5204 (million)
% 91.22/13.74 % (932629)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2728850585:i=667:av=off:fsr=off_2962 on theBenchmark for (2962ds/667Mi)
% 91.22/13.74 % (932629)Refutation not found, incomplete strategy
% 91.22/13.74 % (932629)------------------------------
% 91.22/13.74 % (932629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.22/13.74 % (932629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.74 % (932629)CaDiCaL version: 2.1.3
% 91.22/13.74 % (932629)Termination reason: Refutation not found, incomplete strategy
% 91.22/13.74 % (932629)Time elapsed: 0.001 s
% 91.22/13.74 % (932629)Peak memory usage: 87 MB
% 91.22/13.74 % (932629)------------------------------
% 91.22/13.74 % (932629)------------------------------
% 91.22/13.74 % (932631)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=374398071:s2a=on:i=185:s2at=1.8:fdi=4_2958 on theBenchmark for (2958ds/185Mi)
% 91.22/13.74 % (932631)Instruction limit reached!
% 91.22/13.74 % (932631)------------------------------
% 91.22/13.74 % (932631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.22/13.74 % (932631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.74 % (932631)CaDiCaL version: 2.1.3
% 91.22/13.74 % (932631)Termination reason: Instruction limit
% 91.22/13.74 % (932631)Termination phase: Saturation
% 91.22/13.74 % (932631)Time elapsed: 0.102 s
% 91.22/13.74 % (932631)Peak memory usage: 90 MB
% 91.22/13.74 % (932631)Instructions burned: 186 (million)
% 91.22/13.74 % (932633)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1332637092:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2955 on theBenchmark for (2955ds/193Mi)
% 91.22/13.74 % (932633)Refutation not found, incomplete strategy
% 91.22/13.74 % (932633)------------------------------
% 91.22/13.74 % (932633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.22/13.74 % (932633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.74 % (932633)CaDiCaL version: 2.1.3
% 91.22/13.74 % (932633)Termination reason: Refutation not found, incomplete strategy
% 91.22/13.74 % (932633)Time elapsed: 0.001 s
% 91.22/13.74 % (932633)Peak memory usage: 86 MB
% 91.22/13.74 % (932633)------------------------------
% 91.22/13.74 % (932633)------------------------------
% 91.22/13.74 % (932635)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4108763399:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2951 on theBenchmark for (2951ds/4850Mi)
% 91.22/13.74 % (932613)Instruction limit reached!
% 91.22/13.74 % (932613)------------------------------
% 91.22/13.74 % (932613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.22/13.74 % (932613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.22/13.74 % (932613)CaDiCaL version: 2.1.3
% 91.22/13.74 % (932613)Termination reason: Instruction limit
% 91.22/13.74 % (932613)Termination phase: Saturation
% 91.22/13.74 % (932613)Time elapsed: 3.367 s
% 91.22/13.74 % (932613)Peak memory usage: 164 MB
% 91.22/13.74 % (932613)Instructions burned: 13198 (million)
% 91.22/13.74 % (932637)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2838097271:i=12111:sd=1:ss=included_2947 on theBenchmark for (2947ds/12111Mi)
% 103.98/15.59 % (932623)Instruction limit reached!
% 103.98/15.59 % (932623)------------------------------
% 103.98/15.59 % (932623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.98/15.59 % (932623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.98/15.59 % (932623)CaDiCaL version: 2.1.3
% 103.98/15.59 % (932623)Termination reason: Instruction limit
% 103.98/15.59 % (932623)Termination phase: Saturation
% 103.98/15.59 % (932623)Time elapsed: 4.144 s
% 103.98/15.59 % (932623)Peak memory usage: 148 MB
% 103.98/15.59 % (932623)Instructions burned: 6061 (million)
% 103.98/15.59 % (932635)Instruction limit reached!
% 103.98/15.59 % (932635)------------------------------
% 103.98/15.59 % (932635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.98/15.59 % (932635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.98/15.59 % (932635)CaDiCaL version: 2.1.3
% 103.98/15.59 % (932635)Termination reason: Instruction limit
% 103.98/15.59 % (932635)Termination phase: Saturation
% 103.98/15.59 % (932635)Time elapsed: 1.954 s
% 103.98/15.59 % (932635)Peak memory usage: 90 MB
% 103.98/15.59 % (932635)Instructions burned: 4852 (million)
% 103.98/15.59 % (932639)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=55160434:i=319:kws=precedence:fsr=off_2930 on theBenchmark for (2930ds/319Mi)
% 103.98/15.59 % (932640)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3337702159:i=2064:ep=RST_2930 on theBenchmark for (2930ds/2064Mi)
% 103.98/15.59 % (932640)Refutation not found, incomplete strategy
% 103.98/15.59 % (932640)------------------------------
% 103.98/15.59 % (932640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.98/15.59 % (932640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.98/15.59 % (932640)CaDiCaL version: 2.1.3
% 103.98/15.59 % (932640)Termination reason: Refutation not found, incomplete strategy
% 103.98/15.59 % (932640)Time elapsed: 0.001 s
% 103.98/15.59 % (932640)Peak memory usage: 87 MB
% 103.98/15.59 % (932639)Instruction limit reached!
% 103.98/15.59 % (932639)------------------------------
% 103.98/15.59 % (932639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.98/15.59 % (932639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.98/15.59 % (932639)CaDiCaL version: 2.1.3
% 103.98/15.59 % (932639)Termination reason: Instruction limit
% 103.98/15.59 % (932639)Termination phase: Saturation
% 103.98/15.59 % (932639)Time elapsed: 0.156 s
% 103.98/15.59 % (932639)Peak memory usage: 90 MB
% 103.98/15.59 % (932639)Instructions burned: 319 (million)
% 103.98/15.59 % (932640)------------------------------
% 103.98/15.59 % (932640)------------------------------
% 103.98/15.59 % (932643)dis-1011_128_sil=32000:random_seed=2897851233:i=3706:ep=RST:av=off_2927 on theBenchmark for (2927ds/3706Mi)
% 103.98/15.59 % (932644)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4163283388:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2926 on theBenchmark for (2926ds/757Mi)
% 103.98/15.59 % (932644)Refutation not found, incomplete strategy
% 103.98/15.59 % (932644)------------------------------
% 103.98/15.59 % (932644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.98/15.59 % (932644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.98/15.59 % (932644)CaDiCaL version: 2.1.3
% 103.98/15.59 % (932644)Termination reason: Refutation not found, incomplete strategy
% 103.98/15.59 % (932644)Time elapsed: 0.001 s
% 103.98/15.59 % (932644)Peak memory usage: 86 MB
% 103.98/15.59 % (932644)------------------------------
% 103.98/15.59 % (932644)------------------------------
% 103.98/15.59 % (932647)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2635597670:i=13913:ss=axioms:sgt=8_2921 on theBenchmark for (2921ds/13913Mi)
% 103.98/15.59 % (932637)Instruction limit reached!
% 103.98/15.59 % (932637)------------------------------
% 103.98/15.59 % (932637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.98/15.59 % (932637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.98/15.59 % (932637)CaDiCaL version: 2.1.3
% 103.98/15.59 % (932637)Termination reason: Instruction limit
% 103.98/15.59 % (932637)Termination phase: Saturation
% 103.98/15.59 % (932637)Time elapsed: 3.205 s
% 103.98/15.59 % (932637)Peak memory usage: 278 MB
% 103.98/15.59 % (932637)Instructions burned: 12112 (million)
% 103.98/15.59 % (932649)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1634085442:i=9925:aac=none_2914 on theBenchmark for (2914ds/9925Mi)
% 112.92/16.83 % (932643)Instruction limit reached!
% 112.92/16.83 % (932643)------------------------------
% 112.92/16.83 % (932643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.92/16.83 % (932643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.92/16.83 % (932643)CaDiCaL version: 2.1.3
% 112.92/16.83 % (932643)Termination reason: Instruction limit
% 112.92/16.83 % (932643)Termination phase: Saturation
% 112.92/16.83 % (932643)Time elapsed: 1.501 s
% 112.92/16.83 % (932643)Peak memory usage: 88 MB
% 112.92/16.83 % (932643)Instructions burned: 3706 (million)
% 112.92/16.83 % (932651)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3082285410:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2910 on theBenchmark for (2910ds/2479Mi)
% 112.92/16.83 % (932651)Refutation not found, incomplete strategy
% 112.92/16.83 % (932651)------------------------------
% 112.92/16.83 % (932651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.92/16.83 % (932651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.92/16.83 % (932651)CaDiCaL version: 2.1.3
% 112.92/16.83 % (932651)Termination reason: Refutation not found, incomplete strategy
% 112.92/16.83 % (932651)Time elapsed: 0.001 s
% 112.92/16.83 % (932651)Peak memory usage: 86 MB
% 112.92/16.83 % (932651)------------------------------
% 112.92/16.83 % (932651)------------------------------
% 112.92/16.83 % (932653)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=218814632:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2906 on theBenchmark for (2906ds/440Mi)
% 112.92/16.83 % (932653)Instruction limit reached!
% 112.92/16.83 % (932653)------------------------------
% 112.92/16.83 % (932653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.92/16.83 % (932653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.92/16.83 % (932653)CaDiCaL version: 2.1.3
% 112.92/16.83 % (932653)Termination reason: Instruction limit
% 112.92/16.83 % (932653)Termination phase: Saturation
% 112.92/16.83 % (932653)Time elapsed: 0.147 s
% 112.92/16.83 % (932653)Peak memory usage: 88 MB
% 112.92/16.83 % (932653)Instructions burned: 443 (million)
% 112.92/16.83 % (932655)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=690384887:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2903 on theBenchmark for (2903ds/11145Mi)
% 112.92/16.83 [W927 08:50:05.047857491 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.92/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.92/16.83 [W927 08:50:05.047953128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.92/16.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.92/16.83 % (932627)Instruction limit reached!
% 112.92/16.83 % (932627)------------------------------
% 112.92/16.83 % (932627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.92/16.83 % (932627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.92/16.83 % (932627)CaDiCaL version: 2.1.3
% 112.92/16.83 % (932627)Termination reason: Instruction limit
% 112.92/16.83 % (932627)Termination phase: Saturation
% 112.92/16.83 % (932627)Time elapsed: 8.244 s
% 112.92/16.83 % (932627)Peak memory usage: 175 MB
% 112.92/16.83 % (932627)Instructions burned: 14155 (million)
% 112.92/16.83 % (932657)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4147102576:cts=off:i=3034:av=off:er=known:fsd=on_2884 on theBenchmark for (2884ds/3034Mi)
% 112.92/16.83 % (932649)Instruction limit reached!
% 112.92/16.83 % (932649)------------------------------
% 112.92/16.83 % (932649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.92/16.83 % (932649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.92/16.83 % (932649)CaDiCaL version: 2.1.3
% 112.92/16.83 % (932649)Termination reason: Instruction limit
% 112.92/16.83 % (932649)Termination phase: Saturation
% 112.92/16.83 % (932649)Time elapsed: 4.137 s
% 112.92/16.83 % (932649)Peak memory usage: 183 MB
% 112.92/16.83 % (932649)Instructions burned: 9927 (million)
% 117.20/17.48 % (932659)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2157936920:st=2:s2a=on:i=524:s2at=2:ss=axioms_2871 on theBenchmark for (2871ds/524Mi)
% 117.20/17.48 % (932659)Refutation not found, incomplete strategy
% 117.20/17.48 % (932659)------------------------------
% 117.20/17.48 % (932659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.20/17.48 % (932659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.20/17.48 % (932659)CaDiCaL version: 2.1.3
% 117.20/17.48 % (932659)Termination reason: Refutation not found, incomplete strategy
% 117.20/17.48 % (932659)Time elapsed: 0.001 s
% 117.20/17.48 % (932659)Peak memory usage: 88 MB
% 117.20/17.48 % (932659)Instructions burned: 1 (million)
% 117.20/17.48 % (932659)------------------------------
% 117.20/17.48 % (932659)------------------------------
% 117.20/17.48 % (932657)Instruction limit reached!
% 117.20/17.48 % (932657)------------------------------
% 117.20/17.48 % (932657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.20/17.48 % (932657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.20/17.48 % (932657)CaDiCaL version: 2.1.3
% 117.20/17.48 % (932657)Termination reason: Instruction limit
% 117.20/17.48 % (932657)Termination phase: Saturation
% 117.20/17.48 % (932657)Time elapsed: 1.522 s
% 117.20/17.48 % (932657)Peak memory usage: 142 MB
% 117.20/17.48 % (932657)Instructions burned: 3034 (million)
% 117.20/17.48 % (932670)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3655427869:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2868 on theBenchmark for (2868ds/1016Mi)
% 117.20/17.48 % (932670)Refutation not found, incomplete strategy
% 117.20/17.48 % (932670)------------------------------
% 117.20/17.48 % (932670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.20/17.48 % (932670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.20/17.48 % (932670)CaDiCaL version: 2.1.3
% 117.20/17.48 % (932670)Termination reason: Refutation not found, incomplete strategy
% 117.20/17.48 % (932670)Time elapsed: 0.0000 s
% 117.20/17.48 % (932670)Peak memory usage: 87 MB
% 117.20/17.48 % (932670)------------------------------
% 117.20/17.48 % (932670)------------------------------
% 117.20/17.48 % (932715)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1677358363:i=14123:bd=preordered:ins=4_2867 on theBenchmark for (2867ds/14123Mi)
% 117.20/17.48 % (932787)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=238416679:i=5781:kws=precedence:bd=all:rawr=on_2865 on theBenchmark for (2865ds/5781Mi)
% 117.20/17.48 % (932655)Instruction limit reached!
% 117.20/17.48 % (932655)------------------------------
% 117.20/17.48 % (932655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.20/17.48 % (932655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.20/17.48 % (932655)CaDiCaL version: 2.1.3
% 117.20/17.48 % (932655)Termination reason: Instruction limit
% 117.20/17.48 % (932655)Termination phase: Saturation
% 117.20/17.48 % (932655)Time elapsed: 3.857 s
% 117.20/17.48 % (932655)Peak memory usage: 131 MB
% 117.20/17.48 % (932655)Instructions burned: 11147 (million)
% 117.20/17.48 % (932799)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2535453112:i=2448:gtgl=5:bd=preordered:gtg=all_2863 on theBenchmark for (2863ds/2448Mi)
% 117.20/17.48 % (932799)Refutation not found, incomplete strategy
% 117.20/17.48 % (932799)------------------------------
% 117.20/17.48 % (932799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.20/17.48 % (932799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.20/17.48 % (932799)CaDiCaL version: 2.1.3
% 117.20/17.48 % (932799)Termination reason: Refutation not found, incomplete strategy
% 117.20/17.48 % (932799)Time elapsed: 0.702 s
% 117.20/17.48 % (932799)Peak memory usage: 129 MB
% 117.20/17.48 % (932799)Instructions burned: 1038 (million)
% 117.20/17.48 % (932647)Instruction limit reached!
% 117.20/17.48 % (932647)------------------------------
% 117.20/17.48 % (932647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.20/17.48 % (932647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.20/17.48 % (932647)CaDiCaL version: 2.1.3
% 117.20/17.48 % (932647)Termination reason: Instruction limit
% 117.20/17.48 % (932647)Termination phase: Saturation
% 117.20/17.48 % (932647)Time elapsed: 6.731 s
% 117.20/17.48 % (932647)Peak memory usage: 167 MB
% 117.20/17.48 % (932647)Instructions burned: 13914 (million)
% 121.95/18.07 % (932799)------------------------------
% 121.95/18.07 % (932799)------------------------------
% 121.95/18.07 % (932915)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=356368777:i=3223:kws=precedence:fgj=on:av=off_2852 on theBenchmark for (2852ds/3223Mi)
% 121.95/18.07 % (932924)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=785246370:st=5.6:i=2033:sd=3:ss=axioms_2851 on theBenchmark for (2851ds/2033Mi)
% 121.95/18.07 % (932787)Instruction limit reached!
% 121.95/18.07 % (932787)------------------------------
% 121.95/18.07 % (932787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.95/18.07 % (932787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.95/18.07 % (932787)CaDiCaL version: 2.1.3
% 121.95/18.07 % (932787)Termination reason: Instruction limit
% 121.95/18.07 % (932787)Termination phase: Saturation
% 121.95/18.07 % (932787)Time elapsed: 2.046 s
% 121.95/18.07 % (932787)Peak memory usage: 115 MB
% 121.95/18.07 % (932787)Instructions burned: 5782 (million)
% 121.95/18.07 % (932940)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3444174172:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2844 on theBenchmark for (2844ds/2055Mi)
% 121.95/18.07 % (932924)Refutation not found, incomplete strategy
% 121.95/18.07 % (932924)------------------------------
% 121.95/18.07 % (932924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.95/18.07 % (932924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.95/18.07 % (932924)CaDiCaL version: 2.1.3
% 121.95/18.07 % (932924)Termination reason: Refutation not found, incomplete strategy
% 121.95/18.07 % (932924)Time elapsed: 0.758 s
% 121.95/18.07 % (932924)Peak memory usage: 127 MB
% 121.95/18.07 % (932924)Instructions burned: 847 (million)
% 121.95/18.07 [W927 08:50:11.779471422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.95/18.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.95/18.07 [W927 08:50:11.779498614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.95/18.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.95/18.07 [W927 08:50:11.779518829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.95/18.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.95/18.07 [W927 08:50:11.779525147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.95/18.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.95/18.07 [W927 08:50:11.779538059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.95/18.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.95/18.07 [W927 08:50:11.779543462 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.95/18.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.95/18.07 [W927 08:50:11.779556412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.95/18.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.95/18.07 [W927 08:50:11.779596971 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.779676340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.779697028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.779721073 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.779737505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 % (932924)------------------------------
% 135.03/19.93 % (932924)------------------------------
% 135.03/19.93 % (932940)Refutation not found, incomplete strategy
% 135.03/19.93 % (932940)------------------------------
% 135.03/19.93 % (932940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.03/19.93 % (932940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.03/19.93 % (932940)CaDiCaL version: 2.1.3
% 135.03/19.93 % (932940)Termination reason: Refutation not found, incomplete strategy
% 135.03/19.93 % (932940)Time elapsed: 0.312 s
% 135.03/19.93 % (932940)Peak memory usage: 126 MB
% 135.03/19.93 % (932940)Instructions burned: 822 (million)
% 135.03/19.93 % (932982)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=533932052:i=21611:sd=3:ss=axioms_2839 on theBenchmark for (2839ds/21611Mi)
% 135.03/19.93 % (932940)------------------------------
% 135.03/19.93 % (932940)------------------------------
% 135.03/19.93 % (933050)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1397077656:i=4835:sd=13:ss=axioms:sgt=23_2837 on theBenchmark for (2837ds/4835Mi)
% 135.03/19.93 [W927 08:50:11.432907498 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.432950351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.432987915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.432999022 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.433037285 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.03/19.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.03/19.93 [W927 08:50:11.433049228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 156.20/22.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 156.20/22.97 [W927 08:50:11.433074995 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 156.20/22.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 156.20/22.97 [W927 08:50:11.433085408 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 156.20/22.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 156.20/22.97 [W927 08:50:11.433108915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 156.20/22.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 156.20/22.97 [W927 08:50:11.433119298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 156.20/22.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 156.20/22.97 [W927 08:50:11.433143982 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 156.20/22.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 156.20/22.97 [W927 08:50:11.433153948 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 156.20/22.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 156.20/22.97 % (932982)Refutation not found, incomplete strategy
% 156.20/22.97 % (932982)------------------------------
% 156.20/22.97 % (932982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.20/22.97 % (932982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.20/22.97 % (932982)CaDiCaL version: 2.1.3
% 156.20/22.97 % (932982)Termination reason: Refutation not found, incomplete strategy
% 156.20/22.97 % (932982)Time elapsed: 0.543 s
% 156.20/22.97 % (932982)Peak memory usage: 125 MB
% 156.20/22.97 % (932982)Instructions burned: 822 (million)
% 156.20/22.97 % (932915)Instruction limit reached!
% 156.20/22.97 % (932915)------------------------------
% 156.20/22.97 % (932915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.20/22.97 % (932915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.20/22.97 % (932915)CaDiCaL version: 2.1.3
% 156.20/22.97 % (932915)Termination reason: Instruction limit
% 156.20/22.97 % (932915)Termination phase: Saturation
% 156.20/22.97 % (932915)Time elapsed: 1.881 s
% 156.20/22.97 % (932915)Peak memory usage: 132 MB
% 156.20/22.97 % (932915)Instructions burned: 3224 (million)
% 156.20/22.97 % (932982)------------------------------
% 156.20/22.97 % (932982)------------------------------
% 156.20/22.97 % (933057)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3725027991:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2831 on theBenchmark for (2831ds/797Mi)
% 156.20/22.97 % (933058)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2463733300:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2829 on theBenchmark for (2829ds/2326Mi)
% 156.20/22.97 % (933058)Refutation not found, incomplete strategy
% 156.20/22.97 % (933058)------------------------------
% 156.20/22.97 % (933058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.20/22.97 % (933058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.20/22.97 % (933058)CaDiCaL version: 2.1.3
% 156.20/22.97 % (933058)Termination reason: Refutation not found, incomplete strategy
% 156.20/22.97 % (933058)Time elapsed: 0.001 s
% 156.20/22.97 % (933058)Peak memory usage: 88 MB
% 159.90/23.47 % (933058)------------------------------
% 159.90/23.47 % (933058)------------------------------
% 159.90/23.47 % (933057)Instruction limit reached!
% 159.90/23.47 % (933057)------------------------------
% 159.90/23.47 % (933057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933057)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933057)Termination reason: Instruction limit
% 159.90/23.47 % (933057)Termination phase: Saturation
% 159.90/23.47 % (933057)Time elapsed: 0.396 s
% 159.90/23.47 % (933057)Peak memory usage: 99 MB
% 159.90/23.47 % (933057)Instructions burned: 797 (million)
% 159.90/23.47 % (933062)lrs+10_1_sil=32000:sp=occurrence:random_seed=196459619:st=2:i=33334:sd=3:ss=included:sgt=32_2825 on theBenchmark for (2825ds/33334Mi)
% 159.90/23.47 % (933061)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2988134690:i=6038:nm=6_2825 on theBenchmark for (2825ds/6038Mi)
% 159.90/23.47 % (933050)Instruction limit reached!
% 159.90/23.47 % (933050)------------------------------
% 159.90/23.47 % (933050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933050)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933050)Termination reason: Instruction limit
% 159.90/23.47 % (933050)Termination phase: Saturation
% 159.90/23.47 % (933050)Time elapsed: 1.443 s
% 159.90/23.47 % (933050)Peak memory usage: 105 MB
% 159.90/23.47 % (933050)Instructions burned: 4836 (million)
% 159.90/23.47 % (933065)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3394134715:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2822 on theBenchmark for (2822ds/1008Mi)
% 159.90/23.47 % (933065)Refutation not found, incomplete strategy
% 159.90/23.47 % (933065)------------------------------
% 159.90/23.47 % (933065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933065)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933065)Termination reason: Refutation not found, incomplete strategy
% 159.90/23.47 % (933065)Time elapsed: 0.004 s
% 159.90/23.47 % (933065)Peak memory usage: 88 MB
% 159.90/23.47 % (933065)Instructions burned: 14 (million)
% 159.90/23.47 % (933065)------------------------------
% 159.90/23.47 % (933065)------------------------------
% 159.90/23.47 % (933061)Refutation not found, incomplete strategy
% 159.90/23.47 % (933061)------------------------------
% 159.90/23.47 % (933061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933061)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933061)Termination reason: Refutation not found, incomplete strategy
% 159.90/23.47 % (933061)Time elapsed: 0.595 s
% 159.90/23.47 % (933061)Peak memory usage: 127 MB
% 159.90/23.47 % (933061)Instructions burned: 846 (million)
% 159.90/23.47 % (933067)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=1734559205:i=8327:s2at=5:bd=preordered_2819 on theBenchmark for (2819ds/8327Mi)
% 159.90/23.47 % (933061)------------------------------
% 159.90/23.47 % (933061)------------------------------
% 159.90/23.47 % (933111)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2625663297:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2815 on theBenchmark for (2815ds/1083Mi)
% 159.90/23.47 % (933111)Refutation not found, incomplete strategy
% 159.90/23.47 % (933111)------------------------------
% 159.90/23.47 % (933111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933111)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933111)Termination reason: Refutation not found, incomplete strategy
% 159.90/23.47 % (933111)Time elapsed: 0.007 s
% 159.90/23.47 % (933111)Peak memory usage: 88 MB
% 159.90/23.47 % (933111)Instructions burned: 13 (million)
% 159.90/23.47 % (933111)------------------------------
% 159.90/23.47 % (933111)------------------------------
% 159.90/23.47 % (933113)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=777570824:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2811 on theBenchmark for (2811ds/1084Mi)
% 159.90/23.47 % (933113)Refutation not found, incomplete strategy
% 159.90/23.47 % (933113)------------------------------
% 159.90/23.47 % (933113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933113)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933113)Termination reason: Refutation not found, incomplete strategy
% 159.90/23.47 % (933113)Time elapsed: 0.0000 s
% 159.90/23.47 % (933113)Peak memory usage: 86 MB
% 159.90/23.47 % (933113)------------------------------
% 159.90/23.47 % (933113)------------------------------
% 159.90/23.47 % (933115)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4195607963:i=6995:s2at=5:gtg=all_2807 on theBenchmark for (2807ds/6995Mi)
% 159.90/23.47 % (933067)Instruction limit reached!
% 159.90/23.47 % (933067)------------------------------
% 159.90/23.47 % (933067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933067)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933067)Termination reason: Instruction limit
% 159.90/23.47 % (933067)Termination phase: Saturation
% 159.90/23.47 % (933067)Time elapsed: 3.202 s
% 159.90/23.47 % (933067)Peak memory usage: 170 MB
% 159.90/23.47 % (933067)Instructions burned: 8329 (million)
% 159.90/23.47 % (933117)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1376844555:st=2:i=6225:sd=15:ss=axioms_2785 on theBenchmark for (2785ds/6225Mi)
% 159.90/23.47 % (933117)Refutation not found, incomplete strategy
% 159.90/23.47 % (933117)------------------------------
% 159.90/23.47 % (933117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933117)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933117)Termination reason: Refutation not found, incomplete strategy
% 159.90/23.47 % (933117)Time elapsed: 0.001 s
% 159.90/23.47 % (933117)Peak memory usage: 88 MB
% 159.90/23.47 % (933117)------------------------------
% 159.90/23.47 % (933117)------------------------------
% 159.90/23.47 % (933119)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=340475693:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2782 on theBenchmark for (2782ds/3372Mi)
% 159.90/23.47 [W927 08:50:17.921897378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.921933888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.921954329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.921961488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.921974925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.921980444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.921994437 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.922006610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.922020364 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.922026235 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.922039087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 [W927 08:50:17.922044802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.90/23.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.90/23.47 % (933119)Refutation not found, incomplete strategy
% 159.90/23.47 % (933119)------------------------------
% 159.90/23.47 % (933119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.90/23.47 % (933119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.90/23.47 % (933119)CaDiCaL version: 2.1.3
% 159.90/23.47 % (933119)Termination reason: Refutation not found, incomplete strategy
% 159.90/23.47 % (933119)Time elapsed: 0.315 s
% 159.90/23.47 % (933119)Peak memory usage: 126 MB
% 159.90/23.47 % (933119)Instructions burned: 826 (million)
% 159.90/23.47 % (932390)First to succeed.
% 159.90/23.47 % (932390)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-932283"
% 159.90/23.47 % (933119)------------------------------
% 159.90/23.47 % (933119)------------------------------
% 159.90/23.47 % (933121)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3109153133:st=2.3:i=26457:sd=10:ss=included:sgt=8_2776 on theBenchmark for (2776ds/26457Mi)
% 159.90/23.47 % SZS status CounterSatisfiable for theBenchmark
% 159.90/23.47 % SZS output start Saturation.
% See solution above
% 160.60/23.67 % SZS output start Definitions and Model Updates.
% 160.60/23.67 for all groundings,
% 160.60/23.67 whenever goal | ~red(X0,X1) | ~green(X0,X1) is false, set ~red(X0,X1) to true
% 160.60/23.67 % SZS output end Definitions and Model Updates.
% 160.60/23.67 % (932390)------------------------------
% 160.60/23.67 % (932390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.60/23.67 % (932390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.60/23.67 % (932390)CaDiCaL version: 2.1.3
% 160.60/23.67 % (932390)Termination reason: Satisfiable
% 160.60/23.67 % (932390)Time elapsed: 22.119 s
% 160.60/23.67 % (932390)Peak memory usage: 207 MB
% 160.60/23.67 % (932390)Instructions burned: 32999 (million)
% 160.60/23.67 % (932390)------------------------------
% 160.60/23.67 % (932390)------------------------------
% 160.60/23.67 % (932283)Success in time 22.58 s
% 160.60/23.67 % Vampire exiting
%------------------------------------------------------------------------------