%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRA014+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 : Sun Sep 27 07:19:23 AM UTC 2026
% Result : Theorem 0.94s 0.65s
% Output : CNFRefutation 0.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 6
% Syntax : Number of formulae : 306 ( 25 unt; 0 def)
% Number of atoms : 1009 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 914 ( 211 ~; 690 |; 9 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 73 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(red_clique,axiom,
! [A,B,C] :
( ( red(A,C)
& red(B,C)
& red(A,B) )
=> goal ),
file('theBenchmark.p',red_clique) ).
fof(green_clique,axiom,
! [A,B,C] :
( ( green(A,C)
& green(B,C)
& green(A,B) )
=> goal ),
file('theBenchmark.p',green_clique) ).
fof(ordering,axiom,
( less_than(n5,n6)
& less_than(n4,n5)
& less_than(n3,n4)
& less_than(n2,n3)
& less_than(n1,n2) ),
file('theBenchmark.p',ordering) ).
fof(less_than_transitive,axiom,
! [A,B,C] :
( ( less_than(B,C)
& less_than(A,B) )
=> less_than(A,C) ),
file('theBenchmark.p',less_than_transitive) ).
fof(partition,axiom,
! [A,B] :
( less_than(A,B)
=> ( green(A,B)
| red(A,B) ) ),
file('theBenchmark.p',partition) ).
fof(goal_to_be_proved,conjecture,
goal,
file('theBenchmark.p',goal_to_be_proved) ).
fof(goal_to_be_proved_neg,negated_conjecture,
~ goal,
inference(assume_negation,[status(cth)],[goal_to_be_proved]) ).
cnf(c_7,plain,
( goal
| ~ red(A,C)
| ~ red(B,C)
| ~ red(A,B) ),
inference(clausify,[status(thm)],[red_clique]) ).
cnf(c_8,plain,
( goal
| ~ green(A,C)
| ~ green(B,C)
| ~ green(A,B) ),
inference(clausify,[status(thm)],[green_clique]) ).
cnf(c_9,plain,
less_than(n1,n2),
inference(clausify,[status(thm)],[ordering]) ).
cnf(c_10,plain,
less_than(n2,n3),
inference(clausify,[status(thm)],[ordering]) ).
cnf(c_11,plain,
less_than(n3,n4),
inference(clausify,[status(thm)],[ordering]) ).
cnf(c_12,plain,
less_than(n4,n5),
inference(clausify,[status(thm)],[ordering]) ).
cnf(c_13,plain,
less_than(n5,n6),
inference(clausify,[status(thm)],[ordering]) ).
cnf(c_14,plain,
( less_than(A,C)
| ~ less_than(B,C)
| ~ less_than(A,B) ),
inference(clausify,[status(thm)],[less_than_transitive]) ).
cnf(c_15,plain,
( green(A,B)
| red(A,B)
| ~ less_than(A,B) ),
inference(clausify,[status(thm)],[partition]) ).
cnf(c_16,negated_conjecture,
~ goal,
inference(clausify,[status(thm)],[goal_to_be_proved_neg]) ).
cnf(c_19,negated_conjecture,
( ~ green(A,C)
| ~ green(B,C)
| ~ green(A,B) ),
inference(resolve,[status(thm)],[c_16,c_8]) ).
cnf(c_20,negated_conjecture,
( ~ red(A,C)
| ~ red(B,C)
| ~ red(A,B) ),
inference(resolve,[status(thm)],[c_16,c_7]) ).
cnf(c_22,plain,
( less_than(n4,A)
| ~ less_than(n5,A) ),
inference(resolve,[status(thm)],[c_14,c_12]) ).
cnf(c_23,plain,
( less_than(n3,A)
| ~ less_than(n4,A) ),
inference(resolve,[status(thm)],[c_14,c_11]) ).
cnf(c_24,plain,
( less_than(n2,A)
| ~ less_than(n3,A) ),
inference(resolve,[status(thm)],[c_14,c_10]) ).
cnf(c_25,plain,
( less_than(n1,A)
| ~ less_than(n2,A) ),
inference(resolve,[status(thm)],[c_14,c_9]) ).
cnf(c_31,plain,
( green(n5,n6)
| red(n5,n6) ),
inference(resolve,[status(thm)],[c_15,c_13]) ).
cnf(c_32,plain,
( green(n4,n5)
| red(n4,n5) ),
inference(resolve,[status(thm)],[c_15,c_12]) ).
cnf(c_33,plain,
( green(n3,n4)
| red(n3,n4) ),
inference(resolve,[status(thm)],[c_15,c_11]) ).
cnf(c_34,plain,
( green(n2,n3)
| red(n2,n3) ),
inference(resolve,[status(thm)],[c_15,c_10]) ).
cnf(c_35,plain,
( green(n1,n2)
| red(n1,n2) ),
inference(resolve,[status(thm)],[c_15,c_9]) ).
cnf(c_37,plain,
less_than(n4,n6),
inference(resolve,[status(thm)],[c_22,c_13]) ).
cnf(c_38,plain,
less_than(n3,n5),
inference(resolve,[status(thm)],[c_23,c_12]) ).
cnf(c_47,plain,
less_than(n3,n6),
inference(resolve,[status(thm)],[c_37,c_23]) ).
cnf(c_48,plain,
( green(n4,n6)
| red(n4,n6) ),
inference(resolve,[status(thm)],[c_37,c_15]) ).
cnf(c_52,plain,
( green(n3,n5)
| red(n3,n5) ),
inference(resolve,[status(thm)],[c_38,c_15]) ).
cnf(c_55,plain,
( green(n3,n6)
| red(n3,n6) ),
inference(resolve,[status(thm)],[c_47,c_15]) ).
cnf(c_58,plain,
less_than(n2,n6),
inference(resolve,[status(thm)],[c_24,c_47]) ).
cnf(c_59,plain,
less_than(n2,n5),
inference(resolve,[status(thm)],[c_24,c_38]) ).
cnf(c_60,plain,
less_than(n2,n4),
inference(resolve,[status(thm)],[c_24,c_11]) ).
cnf(c_64,plain,
less_than(n1,n3),
inference(resolve,[status(thm)],[c_25,c_10]) ).
cnf(c_66,plain,
less_than(n1,n6),
inference(resolve,[status(thm)],[c_58,c_25]) ).
cnf(c_67,plain,
( green(n2,n6)
| red(n2,n6) ),
inference(resolve,[status(thm)],[c_58,c_15]) ).
cnf(c_71,plain,
less_than(n1,n5),
inference(resolve,[status(thm)],[c_59,c_25]) ).
cnf(c_72,plain,
( green(n2,n5)
| red(n2,n5) ),
inference(resolve,[status(thm)],[c_59,c_15]) ).
cnf(c_76,plain,
less_than(n1,n4),
inference(resolve,[status(thm)],[c_60,c_25]) ).
cnf(c_77,plain,
( green(n2,n4)
| red(n2,n4) ),
inference(resolve,[status(thm)],[c_60,c_15]) ).
cnf(c_80,plain,
( green(n1,n3)
| red(n1,n3) ),
inference(resolve,[status(thm)],[c_64,c_15]) ).
cnf(c_83,plain,
( green(n1,n6)
| red(n1,n6) ),
inference(resolve,[status(thm)],[c_66,c_15]) ).
cnf(c_86,plain,
( green(n1,n5)
| red(n1,n5) ),
inference(resolve,[status(thm)],[c_71,c_15]) ).
cnf(c_89,plain,
( green(n1,n4)
| red(n1,n4) ),
inference(resolve,[status(thm)],[c_76,c_15]) ).
cnf(c_93,plain,
( ~ red(A,n6)
| ~ red(A,n5)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_31,c_20]) ).
cnf(c_96,plain,
( ~ red(A,n5)
| ~ red(A,n4)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_32,c_20]) ).
cnf(c_99,plain,
( ~ red(A,n4)
| ~ red(A,n3)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_33,c_20]) ).
cnf(c_100,plain,
( ~ red(n3,A)
| ~ red(n4,A)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_33,c_20]) ).
cnf(c_102,plain,
( ~ red(A,n3)
| ~ red(A,n2)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_34,c_20]) ).
cnf(c_103,plain,
( ~ red(n2,A)
| ~ red(n3,A)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_34,c_20]) ).
cnf(c_106,plain,
( ~ red(n1,A)
| ~ red(n2,A)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_35,c_20]) ).
cnf(c_108,plain,
( ~ red(A,n6)
| ~ red(A,n4)
| green(n4,n6) ),
inference(resolve,[status(thm)],[c_48,c_20]) ).
cnf(c_111,plain,
( ~ red(A,n5)
| ~ red(A,n3)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_52,c_20]) ).
cnf(c_114,plain,
( ~ red(A,n6)
| ~ red(A,n3)
| green(n3,n6) ),
inference(resolve,[status(thm)],[c_55,c_20]) ).
cnf(c_141,plain,
( green(n1,n5)
| ~ red(n1,n6)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_93,c_86]) ).
cnf(c_142,plain,
( green(n2,n5)
| ~ red(n2,n6)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_93,c_72]) ).
cnf(c_143,plain,
( green(n3,n5)
| ~ red(n3,n6)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_93,c_52]) ).
cnf(c_144,plain,
( green(n4,n5)
| ~ red(n4,n6)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_93,c_32]) ).
cnf(c_153,plain,
( green(n1,n4)
| ~ red(n1,n5)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_96,c_89]) ).
cnf(c_154,plain,
( green(n2,n4)
| ~ red(n2,n5)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_96,c_77]) ).
cnf(c_155,plain,
( green(n3,n4)
| ~ red(n3,n5)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_96,c_33]) ).
cnf(c_164,plain,
( green(n1,n3)
| ~ red(n1,n4)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_99,c_80]) ).
cnf(c_165,plain,
( green(n2,n3)
| ~ red(n2,n4)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_99,c_34]) ).
cnf(c_168,plain,
( green(n4,n6)
| ~ red(n3,n6)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_100,c_48]) ).
cnf(c_175,plain,
( green(n1,n2)
| ~ red(n1,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_102,c_35]) ).
cnf(c_177,plain,
( green(n3,n6)
| ~ red(n2,n6)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_103,c_55]) ).
cnf(c_178,plain,
( green(n3,n5)
| ~ red(n2,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_103,c_52]) ).
cnf(c_186,plain,
( green(n2,n4)
| ~ red(n1,n4)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_106,c_77]) ).
cnf(c_187,plain,
( green(n2,n5)
| ~ red(n1,n5)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_106,c_72]) ).
cnf(c_188,plain,
( green(n2,n6)
| ~ red(n1,n6)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_106,c_67]) ).
cnf(c_196,plain,
( green(n1,n4)
| ~ red(n1,n6)
| green(n4,n6) ),
inference(resolve,[status(thm)],[c_108,c_89]) ).
cnf(c_197,plain,
( green(n2,n4)
| ~ red(n2,n6)
| green(n4,n6) ),
inference(resolve,[status(thm)],[c_108,c_77]) ).
cnf(c_204,plain,
( green(n1,n3)
| ~ red(n1,n5)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_111,c_80]) ).
cnf(c_210,plain,
( green(n1,n3)
| ~ red(n1,n6)
| green(n3,n6) ),
inference(resolve,[status(thm)],[c_114,c_80]) ).
cnf(c_237,plain,
( green(n1,n6)
| green(n1,n5)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_141,c_83]) ).
cnf(c_238,plain,
( green(n2,n6)
| green(n2,n5)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_142,c_67]) ).
cnf(c_239,plain,
( green(n3,n6)
| green(n3,n5)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_143,c_55]) ).
cnf(c_240,plain,
( green(n4,n6)
| green(n4,n5)
| green(n5,n6) ),
inference(resolve,[status(thm)],[c_144,c_48]) ).
cnf(c_241,plain,
( green(n1,n5)
| green(n1,n4)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_153,c_86]) ).
cnf(c_242,plain,
( green(n2,n5)
| green(n2,n4)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_154,c_72]) ).
cnf(c_243,plain,
( green(n3,n5)
| green(n3,n4)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_155,c_52]) ).
cnf(c_244,plain,
( green(n1,n4)
| green(n1,n3)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_164,c_89]) ).
cnf(c_245,plain,
( green(n2,n4)
| green(n2,n3)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_165,c_77]) ).
cnf(c_246,plain,
( green(n3,n6)
| green(n4,n6)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_168,c_55]) ).
cnf(c_247,plain,
( green(n1,n3)
| green(n1,n2)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_175,c_80]) ).
cnf(c_248,plain,
( green(n2,n6)
| green(n3,n6)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_177,c_67]) ).
cnf(c_249,plain,
( green(n2,n5)
| green(n3,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_178,c_72]) ).
cnf(c_250,plain,
( green(n1,n4)
| green(n2,n4)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_186,c_89]) ).
cnf(c_251,plain,
( green(n1,n5)
| green(n2,n5)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_187,c_86]) ).
cnf(c_252,plain,
( green(n1,n6)
| green(n2,n6)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_188,c_83]) ).
cnf(c_253,plain,
( green(n1,n6)
| green(n1,n4)
| green(n4,n6) ),
inference(resolve,[status(thm)],[c_196,c_83]) ).
cnf(c_254,plain,
( green(n2,n6)
| green(n2,n4)
| green(n4,n6) ),
inference(resolve,[status(thm)],[c_197,c_67]) ).
cnf(c_255,plain,
( green(n1,n5)
| green(n1,n3)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_204,c_86]) ).
cnf(c_256,plain,
( green(n1,n6)
| green(n1,n3)
| green(n3,n6) ),
inference(resolve,[status(thm)],[c_210,c_83]) ).
cnf(c_261,plain,
( ~ green(A,n6)
| ~ green(A,n5)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_238,c_19]) ).
cnf(c_264,plain,
( ~ green(A,n6)
| ~ green(A,n5)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_239,c_19]) ).
cnf(c_267,plain,
( ~ green(A,n6)
| ~ green(A,n5)
| green(n4,n6)
| green(n4,n5) ),
inference(resolve,[status(thm)],[c_240,c_19]) ).
cnf(c_273,plain,
( ~ green(A,n5)
| ~ green(A,n4)
| green(n2,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_242,c_19]) ).
cnf(c_276,plain,
( ~ green(A,n5)
| ~ green(A,n4)
| green(n3,n5)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_243,c_19]) ).
cnf(c_278,plain,
( ~ green(A,n4)
| ~ green(n1,A)
| green(n1,n3)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_244,c_19]) ).
cnf(c_282,plain,
( ~ green(A,n4)
| ~ green(A,n3)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_245,c_19]) ).
cnf(c_283,plain,
( ~ green(n3,A)
| ~ green(n4,A)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_245,c_19]) ).
cnf(c_285,plain,
( ~ green(A,n6)
| ~ green(A,n4)
| green(n3,n6)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_246,c_19]) ).
cnf(c_289,plain,
( ~ green(n1,A)
| ~ green(n3,A)
| green(n1,n2)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_247,c_19]) ).
cnf(c_298,plain,
( ~ green(n1,A)
| ~ green(n4,A)
| green(n2,n4)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_250,c_19]) ).
cnf(c_309,plain,
( ~ green(A,n6)
| ~ green(A,n4)
| green(n2,n6)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_254,c_19]) ).
cnf(c_1225,plain,
( green(n2,n5)
| green(n1,n2)
| ~ green(n1,n6)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_261,c_251]) ).
cnf(c_336,plain,
( green(n1,n2)
| ~ green(n1,n6)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1225]) ).
cnf(c_1226,plain,
( green(n2,n5)
| green(n2,n3)
| ~ green(n3,n6)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_261,c_249]) ).
cnf(c_337,plain,
( green(n2,n3)
| ~ green(n3,n6)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1226]) ).
cnf(c_1227,plain,
( green(n2,n5)
| green(n2,n4)
| ~ green(n4,n6)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_261,c_242]) ).
cnf(c_339,plain,
( green(n2,n4)
| ~ green(n4,n6)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1227]) ).
cnf(c_1228,plain,
( green(n1,n3)
| green(n3,n5)
| ~ green(n1,n6)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_264,c_255]) ).
cnf(c_352,plain,
( green(n1,n3)
| ~ green(n1,n6)
| green(n3,n6)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1228]) ).
cnf(c_1229,plain,
( green(n3,n5)
| green(n3,n4)
| ~ green(n4,n6)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_264,c_243]) ).
cnf(c_354,plain,
( green(n3,n4)
| ~ green(n4,n6)
| green(n3,n6)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1229]) ).
cnf(c_1230,plain,
( green(n2,n4)
| green(n1,n2)
| ~ green(n1,n5)
| green(n2,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_273,c_250]) ).
cnf(c_389,plain,
( green(n1,n2)
| ~ green(n1,n5)
| green(n2,n5)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1230]) ).
cnf(c_1231,plain,
( green(n2,n4)
| green(n2,n3)
| ~ green(n3,n5)
| green(n2,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_273,c_245]) ).
cnf(c_390,plain,
( green(n2,n3)
| ~ green(n3,n5)
| green(n2,n5)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1231]) ).
cnf(c_1232,plain,
( green(n1,n3)
| green(n3,n4)
| ~ green(n1,n5)
| green(n3,n5)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_276,c_244]) ).
cnf(c_402,plain,
( green(n1,n3)
| ~ green(n1,n5)
| green(n3,n5)
| green(n3,n4) ),
inference(copy,[status(thm)],[c_1232]) ).
cnf(c_1233,plain,
( green(n1,n2)
| green(n2,n3)
| ~ green(n1,n4)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_282,c_247]) ).
cnf(c_420,plain,
( green(n1,n2)
| ~ green(n1,n4)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1233]) ).
cnf(c_1234,plain,
( green(n2,n6)
| green(n2,n4)
| ~ green(n3,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_283,c_254]) ).
cnf(c_422,plain,
( green(n2,n6)
| ~ green(n3,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1234]) ).
cnf(c_1235,plain,
( green(n2,n5)
| green(n2,n3)
| ~ green(n1,n5)
| green(n1,n2)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_289,c_249]) ).
cnf(c_434,plain,
( green(n2,n5)
| ~ green(n1,n5)
| green(n1,n2)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1235]) ).
cnf(c_1236,plain,
( green(n2,n6)
| green(n2,n3)
| ~ green(n1,n6)
| green(n1,n2)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_289,c_248]) ).
cnf(c_435,plain,
( green(n2,n6)
| ~ green(n1,n6)
| green(n1,n2)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1236]) ).
cnf(c_1237,plain,
( green(n2,n6)
| green(n2,n4)
| ~ green(n1,n6)
| green(n2,n4)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_298,c_254]) ).
cnf(c_454,plain,
( green(n2,n6)
| ~ green(n1,n6)
| green(n2,n4)
| green(n1,n2) ),
inference(copy,[status(thm)],[c_1237]) ).
cnf(c_1238,plain,
( green(n2,n6)
| green(n1,n2)
| green(n1,n2)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_336,c_252]) ).
cnf(c_1239,plain,
( green(n2,n6)
| green(n1,n2)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1238]) ).
cnf(c_477,plain,
( green(n1,n2)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1239]) ).
cnf(c_487,plain,
( ~ green(n2,n4)
| green(n1,n3)
| green(n3,n4)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_477,c_278]) ).
cnf(c_491,plain,
( ~ green(n1,A)
| ~ green(n2,A)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_477,c_19]) ).
cnf(c_1240,plain,
( green(n2,n6)
| green(n2,n3)
| green(n2,n3)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_337,c_248]) ).
cnf(c_1241,plain,
( green(n2,n6)
| green(n2,n3)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1240]) ).
cnf(c_492,plain,
( green(n2,n3)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1241]) ).
cnf(c_502,plain,
( ~ green(A,n6)
| ~ green(n2,A)
| green(n2,n3)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_492,c_19]) ).
cnf(c_503,plain,
( ~ green(A,n6)
| ~ green(A,n2)
| green(n2,n3)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_492,c_19]) ).
cnf(c_1242,plain,
( green(n2,n6)
| green(n2,n4)
| green(n2,n4)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_339,c_254]) ).
cnf(c_1243,plain,
( green(n2,n6)
| green(n2,n4)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1242]) ).
cnf(c_505,plain,
( green(n2,n4)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1243]) ).
cnf(c_514,plain,
( ~ green(A,n6)
| ~ green(n2,A)
| green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_505,c_19]) ).
cnf(c_515,plain,
( ~ green(A,n6)
| ~ green(A,n2)
| green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_505,c_19]) ).
cnf(c_1244,plain,
( green(n1,n3)
| green(n3,n6)
| green(n1,n3)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_352,c_256]) ).
cnf(c_1245,plain,
( green(n1,n3)
| green(n1,n3)
| green(n3,n6)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1244]) ).
cnf(c_517,plain,
( green(n1,n3)
| green(n3,n6)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1245]) ).
cnf(c_525,plain,
( ~ green(A,n3)
| ~ green(n1,A)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_517,c_19]) ).
cnf(c_1246,plain,
( green(n3,n6)
| green(n3,n4)
| green(n3,n4)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_354,c_246]) ).
cnf(c_1247,plain,
( green(n3,n6)
| green(n3,n4)
| green(n3,n6)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1246]) ).
cnf(c_529,plain,
( green(n3,n4)
| green(n3,n6)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1247]) ).
cnf(c_541,plain,
( ~ green(A,n6)
| ~ green(A,n3)
| green(n3,n4)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_529,c_19]) ).
cnf(c_1248,plain,
( green(n2,n5)
| green(n1,n2)
| green(n1,n2)
| green(n2,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_389,c_251]) ).
cnf(c_1249,plain,
( green(n2,n5)
| green(n1,n2)
| green(n2,n5)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1248]) ).
cnf(c_557,plain,
( green(n1,n2)
| green(n2,n5)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1249]) ).
cnf(c_568,plain,
( ~ green(n1,A)
| ~ green(n2,A)
| green(n2,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_557,c_19]) ).
cnf(c_1250,plain,
( green(n2,n5)
| green(n2,n3)
| green(n2,n3)
| green(n2,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_390,c_249]) ).
cnf(c_1251,plain,
( green(n2,n5)
| green(n2,n3)
| green(n2,n5)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1250]) ).
cnf(c_569,plain,
( green(n2,n3)
| green(n2,n5)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1251]) ).
cnf(c_577,plain,
( ~ green(A,n5)
| ~ green(A,n2)
| green(n2,n3)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_569,c_19]) ).
cnf(c_578,plain,
( ~ green(n2,A)
| ~ green(n5,A)
| green(n2,n3)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_569,c_19]) ).
cnf(c_1252,plain,
( green(n1,n3)
| green(n3,n5)
| green(n1,n3)
| green(n3,n5)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_402,c_255]) ).
cnf(c_1253,plain,
( green(n1,n3)
| green(n1,n3)
| green(n3,n5)
| green(n3,n4) ),
inference(copy,[status(thm)],[c_1252]) ).
cnf(c_579,plain,
( green(n1,n3)
| green(n3,n5)
| green(n3,n4) ),
inference(copy,[status(thm)],[c_1253]) ).
cnf(c_590,plain,
( ~ green(A,n3)
| ~ green(n1,A)
| green(n3,n5)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_579,c_19]) ).
cnf(c_1254,plain,
( green(n2,n4)
| green(n1,n2)
| green(n1,n2)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_420,c_250]) ).
cnf(c_1255,plain,
( green(n2,n4)
| green(n1,n2)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1254]) ).
cnf(c_606,plain,
( green(n1,n2)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1255]) ).
cnf(c_619,plain,
( ~ green(n1,A)
| ~ green(n2,A)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_606,c_19]) ).
cnf(c_1256,plain,
( green(n2,n6)
| green(n2,n3)
| green(n2,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_422,c_248]) ).
cnf(c_1257,plain,
( green(n2,n6)
| green(n2,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1256]) ).
cnf(c_622,plain,
( green(n2,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1257]) ).
cnf(c_1258,plain,
( green(n2,n5)
| green(n1,n2)
| green(n2,n5)
| green(n1,n2)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_434,c_251]) ).
cnf(c_1259,plain,
( green(n2,n5)
| green(n2,n5)
| green(n1,n2)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1258]) ).
cnf(c_636,plain,
( green(n2,n5)
| green(n1,n2)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1259]) ).
cnf(c_648,plain,
( ~ green(n1,A)
| ~ green(n2,A)
| green(n2,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_636,c_19]) ).
cnf(c_1260,plain,
( green(n2,n6)
| green(n1,n2)
| green(n2,n6)
| green(n1,n2)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_435,c_252]) ).
cnf(c_1261,plain,
( green(n2,n6)
| green(n2,n6)
| green(n1,n2)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1260]) ).
cnf(c_650,plain,
( green(n2,n6)
| green(n1,n2)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1261]) ).
cnf(c_661,plain,
( ~ green(n1,A)
| ~ green(n2,A)
| green(n2,n6)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_650,c_19]) ).
cnf(c_1262,plain,
( green(n2,n6)
| green(n1,n2)
| green(n2,n6)
| green(n2,n4)
| green(n1,n2) ),
inference(resolve,[status(thm)],[c_454,c_252]) ).
cnf(c_1263,plain,
( green(n2,n6)
| green(n2,n6)
| green(n2,n4)
| green(n1,n2) ),
inference(copy,[status(thm)],[c_1262]) ).
cnf(c_663,plain,
( green(n2,n6)
| green(n2,n4)
| green(n1,n2) ),
inference(copy,[status(thm)],[c_1263]) ).
cnf(c_1264,plain,
( green(n2,n5)
| green(n2,n3)
| ~ green(n1,n6)
| green(n2,n3)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_503,c_636]) ).
cnf(c_1265,plain,
( green(n2,n5)
| ~ green(n1,n6)
| green(n2,n3)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1264]) ).
cnf(c_682,plain,
( ~ green(n1,n6)
| green(n2,n3)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1265]) ).
cnf(c_684,plain,
( green(n1,n4)
| green(n4,n6)
| green(n2,n3)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_682,c_253]) ).
cnf(c_1266,plain,
( green(n2,n5)
| green(n2,n4)
| ~ green(n1,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_515,c_557]) ).
cnf(c_1267,plain,
( green(n2,n5)
| ~ green(n1,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1266]) ).
cnf(c_689,plain,
( ~ green(n1,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1267]) ).
cnf(c_691,plain,
( green(n1,n3)
| green(n3,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_689,c_256]) ).
cnf(c_694,plain,
( green(n2,n6)
| green(n2,n4)
| ~ green(n2,n3)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_525,c_663]) ).
cnf(c_1268,plain,
( green(n3,n5)
| green(n3,n4)
| ~ green(n1,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_541,c_579]) ).
cnf(c_1269,plain,
( green(n3,n5)
| ~ green(n1,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1268]) ).
cnf(c_701,plain,
( ~ green(n1,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1269]) ).
cnf(c_703,plain,
( green(n2,n6)
| green(n1,n2)
| green(n3,n4)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_701,c_252]) ).
cnf(c_1270,plain,
( green(n2,n4)
| green(n2,n3)
| ~ green(n1,n5)
| green(n2,n3)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_577,c_606]) ).
cnf(c_1271,plain,
( green(n2,n4)
| ~ green(n1,n5)
| green(n2,n3)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1270]) ).
cnf(c_715,plain,
( ~ green(n1,n5)
| green(n2,n3)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1271]) ).
cnf(c_1272,plain,
( green(n2,n4)
| green(n2,n3)
| ~ green(n5,n6)
| green(n2,n3)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_578,c_622]) ).
cnf(c_1273,plain,
( green(n2,n4)
| ~ green(n5,n6)
| green(n2,n3)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1272]) ).
cnf(c_718,plain,
( ~ green(n5,n6)
| green(n2,n3)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1273]) ).
cnf(c_1274,plain,
( green(n2,n4)
| green(n2,n3)
| ~ green(n1,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_619,c_622]) ).
cnf(c_1275,plain,
( green(n2,n4)
| ~ green(n1,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1274]) ).
cnf(c_727,plain,
( ~ green(n1,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1275]) ).
cnf(c_730,plain,
( green(n1,n5)
| green(n5,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_727,c_237]) ).
cnf(c_1276,plain,
( ~ green(n2,n3)
| green(n2,n5)
| green(n2,n4)
| green(n3,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_691,c_568]) ).
cnf(c_1277,plain,
( ~ green(n2,n3)
| green(n2,n5)
| green(n3,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1276]) ).
cnf(c_755,plain,
( ~ green(n2,n3)
| green(n3,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1277]) ).
cnf(c_1278,plain,
( ~ green(n2,n3)
| green(n3,n5)
| green(n3,n4)
| green(n2,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_703,c_590]) ).
cnf(c_1279,plain,
( ~ green(n2,n3)
| green(n3,n5)
| green(n2,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1278]) ).
cnf(c_794,plain,
( ~ green(n2,n3)
| green(n2,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1279]) ).
cnf(c_1280,plain,
( green(n2,n3)
| green(n2,n4)
| green(n5,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_730,c_715]) ).
cnf(c_1281,plain,
( green(n2,n3)
| green(n5,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1280]) ).
cnf(c_843,plain,
( green(n5,n6)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1281]) ).
cnf(c_1282,plain,
( green(n2,n3)
| green(n2,n4)
| green(n2,n4)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_843,c_718]) ).
cnf(c_1283,plain,
( green(n2,n3)
| green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1282]) ).
cnf(c_844,plain,
( green(n2,n4)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1283]) ).
cnf(c_1284,plain,
( ~ green(n1,n4)
| green(n2,n6)
| green(n2,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_844,c_661]) ).
cnf(c_845,plain,
( ~ green(n1,n4)
| green(n2,n6)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1284]) ).
cnf(c_1285,plain,
( ~ green(n1,n4)
| green(n2,n5)
| green(n2,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_844,c_648]) ).
cnf(c_846,plain,
( ~ green(n1,n4)
| green(n2,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1285]) ).
cnf(c_1286,plain,
( ~ green(n4,n6)
| green(n2,n3)
| green(n2,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_844,c_502]) ).
cnf(c_850,plain,
( ~ green(n4,n6)
| green(n2,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1286]) ).
cnf(c_857,plain,
( ~ green(n2,A)
| ~ green(n4,A)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_844,c_19]) ).
cnf(c_1287,plain,
( green(n4,n6)
| green(n2,n3)
| green(n2,n5)
| green(n2,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_846,c_684]) ).
cnf(c_1288,plain,
( green(n4,n6)
| green(n2,n3)
| green(n2,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1287]) ).
cnf(c_861,plain,
( green(n4,n6)
| green(n2,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1288]) ).
cnf(c_1289,plain,
( green(n2,n5)
| green(n2,n3)
| green(n2,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_861,c_850]) ).
cnf(c_1290,plain,
( green(n2,n5)
| green(n2,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1289]) ).
cnf(c_867,plain,
( green(n2,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1290]) ).
cnf(c_1291,plain,
( ~ green(n4,n5)
| green(n2,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_867,c_857]) ).
cnf(c_868,plain,
( ~ green(n4,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1291]) ).
cnf(c_1292,plain,
( ~ green(n1,n5)
| green(n2,n6)
| green(n2,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_867,c_661]) ).
cnf(c_870,plain,
( ~ green(n1,n5)
| green(n2,n6)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1292]) ).
cnf(c_877,plain,
( ~ green(n2,n6)
| green(n4,n6)
| green(n4,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_867,c_267]) ).
cnf(c_884,plain,
( green(n1,n4)
| green(n4,n5)
| green(n2,n6)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_870,c_241]) ).
cnf(c_1293,plain,
( green(n2,n6)
| green(n2,n3)
| green(n4,n5)
| green(n2,n6)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_884,c_845]) ).
cnf(c_1294,plain,
( green(n2,n6)
| green(n4,n5)
| green(n2,n6)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1293]) ).
cnf(c_921,plain,
( green(n4,n5)
| green(n2,n6)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1294]) ).
cnf(c_1295,plain,
( green(n2,n3)
| green(n2,n6)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_921,c_868]) ).
cnf(c_924,plain,
( green(n2,n6)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1295]) ).
cnf(c_1296,plain,
( green(n4,n6)
| green(n4,n5)
| green(n2,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_924,c_877]) ).
cnf(c_928,plain,
( green(n4,n6)
| green(n4,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1296]) ).
cnf(c_1297,plain,
( ~ green(n4,n6)
| green(n2,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_924,c_857]) ).
cnf(c_929,plain,
( ~ green(n4,n6)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1297]) ).
cnf(c_1298,plain,
( green(n2,n3)
| green(n4,n5)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_928,c_929]) ).
cnf(c_958,plain,
( green(n4,n5)
| green(n2,n3) ),
inference(copy,[status(thm)],[c_1298]) ).
cnf(c_1299,plain,
( green(n2,n3)
| green(n2,n3) ),
inference(resolve,[status(thm)],[c_958,c_868]) ).
cnf(c_961,plain,
green(n2,n3),
inference(copy,[status(thm)],[c_1299]) ).
cnf(c_962,plain,
( green(n2,n6)
| green(n3,n4)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_961,c_794]) ).
cnf(c_963,plain,
( green(n3,n6)
| green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_961,c_755]) ).
cnf(c_965,plain,
( green(n2,n6)
| green(n2,n4)
| green(n3,n6)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_961,c_694]) ).
cnf(c_980,plain,
( ~ green(n1,n3)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_961,c_491]) ).
cnf(c_983,plain,
( ~ green(n2,A)
| ~ green(n3,A) ),
inference(resolve,[status(thm)],[c_961,c_19]) ).
cnf(c_1300,plain,
( ~ green(n2,n3)
| green(n2,n4)
| green(n2,n5)
| green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_963,c_514]) ).
cnf(c_1301,plain,
( ~ green(n2,n3)
| green(n2,n4)
| green(n2,n4)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1300]) ).
cnf(c_1302,plain,
( ~ green(n2,n3)
| green(n2,n4)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1301]) ).
cnf(c_1002,plain,
( green(n2,n4)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_961,c_1302]) ).
cnf(c_1003,plain,
( ~ green(n3,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1002,c_983]) ).
cnf(c_1013,plain,
( ~ green(A,n5)
| ~ green(n2,A)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1002,c_19]) ).
cnf(c_1015,plain,
( ~ green(n2,A)
| ~ green(n5,A)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1002,c_19]) ).
cnf(c_1016,plain,
( green(n2,n6)
| green(n3,n4)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1003,c_962]) ).
cnf(c_1303,plain,
( ~ green(n3,n6)
| green(n2,n6)
| green(n2,n4)
| green(n2,n6)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1016,c_309]) ).
cnf(c_1304,plain,
( ~ green(n3,n6)
| green(n2,n6)
| green(n2,n6)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1303]) ).
cnf(c_1019,plain,
( ~ green(n3,n6)
| green(n2,n6)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1304]) ).
cnf(c_1305,plain,
( green(n2,n6)
| green(n2,n4)
| green(n2,n6)
| green(n2,n4)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_965,c_1019]) ).
cnf(c_1306,plain,
( green(n2,n6)
| green(n2,n6)
| green(n2,n4)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1305]) ).
cnf(c_1027,plain,
( green(n2,n6)
| green(n2,n4)
| green(n3,n5) ),
inference(copy,[status(thm)],[c_1306]) ).
cnf(c_1307,plain,
( ~ green(n2,n3)
| green(n2,n4)
| green(n2,n6)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1027,c_1013]) ).
cnf(c_1308,plain,
( ~ green(n2,n3)
| green(n2,n6)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1307]) ).
cnf(c_1029,plain,
( green(n2,n6)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_961,c_1308]) ).
cnf(c_1309,plain,
( ~ green(n5,n6)
| green(n2,n4)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1029,c_1015]) ).
cnf(c_1030,plain,
( ~ green(n5,n6)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1309]) ).
cnf(c_1046,plain,
( ~ green(A,n6)
| ~ green(n2,A)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1029,c_19]) ).
cnf(c_1050,plain,
( green(n3,n6)
| green(n3,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1030,c_239]) ).
cnf(c_1310,plain,
( ~ green(n2,n3)
| green(n2,n4)
| green(n3,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1050,c_1046]) ).
cnf(c_1311,plain,
( ~ green(n2,n3)
| green(n3,n5)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1310]) ).
cnf(c_1070,plain,
( green(n3,n5)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_961,c_1311]) ).
cnf(c_1312,plain,
( ~ green(n2,n3)
| green(n2,n4)
| green(n2,n4) ),
inference(resolve,[status(thm)],[c_1070,c_1013]) ).
cnf(c_1313,plain,
( ~ green(n2,n3)
| green(n2,n4) ),
inference(copy,[status(thm)],[c_1312]) ).
cnf(c_1072,plain,
green(n2,n4),
inference(resolve,[status(thm)],[c_961,c_1313]) ).
cnf(c_1074,plain,
( green(n1,n3)
| green(n3,n4)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_1072,c_487]) ).
cnf(c_1075,plain,
~ green(n3,n4),
inference(resolve,[status(thm)],[c_1072,c_983]) ).
cnf(c_1314,plain,
( ~ green(n2,n6)
| green(n3,n6)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_1072,c_285]) ).
cnf(c_1080,plain,
( ~ green(n2,n6)
| green(n3,n6) ),
inference(resolve,[status(thm)],[c_1075,c_1314]) ).
cnf(c_1315,plain,
( ~ green(n2,n5)
| green(n3,n5)
| green(n3,n4) ),
inference(resolve,[status(thm)],[c_1072,c_276]) ).
cnf(c_1083,plain,
( ~ green(n2,n5)
| green(n3,n5) ),
inference(resolve,[status(thm)],[c_1075,c_1315]) ).
cnf(c_1087,plain,
( green(n1,n3)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_1075,c_1074]) ).
cnf(c_1316,plain,
( green(n2,n6)
| green(n2,n5)
| green(n2,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_1087,c_980]) ).
cnf(c_1317,plain,
( green(n2,n6)
| green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1316]) ).
cnf(c_1185,plain,
( green(n2,n6)
| green(n2,n5) ),
inference(copy,[status(thm)],[c_1317]) ).
cnf(c_1190,plain,
( green(n3,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_1185,c_1080]) ).
cnf(c_1191,plain,
( ~ green(n3,n6)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_1185,c_983]) ).
cnf(c_1318,plain,
( green(n2,n5)
| green(n2,n5) ),
inference(resolve,[status(thm)],[c_1191,c_1190]) ).
cnf(c_1218,plain,
green(n2,n5),
inference(copy,[status(thm)],[c_1318]) ).
cnf(c_1220,plain,
green(n3,n5),
inference(resolve,[status(thm)],[c_1218,c_1083]) ).
cnf(c_1319,plain,
~ green(n3,n5),
inference(resolve,[status(thm)],[c_1218,c_983]) ).
cnf(c_1224,plain,
$false,
inference(resolve,[status(thm)],[c_1220,c_1319]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRA014+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n003.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Fri Sep 25 13:50:37 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/0.43 % Process 309563 was started by sandbox2 on n003,
% 0.14/0.43 % Fri Sep 25 13:50:37 2026
% 0.14/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/0.44
% 0.14/0.44 % From the command line: assign(max_seconds, 300).
% 0.94/0.65
% 0.94/0.65 % given #500 (W,wt=14): 880 green(n2,n3) | -green(A,n2) | -green(A,n5). [resolve(867,b,19,b)].
% 0.94/0.65
% 0.94/0.65 % SZS status Theorem for theBenchmark
% 0.94/0.65
% 0.94/0.65 % Proof 1 at 0.13 (+ 0.06) seconds.
% 0.94/0.65 % Length of proof is 210.
% 0.94/0.65 % Level of proof is 41.
% 0.94/0.65 % Maximum clause weight is 20.000.
% 0.94/0.65 % Given clauses 686.
% 0.94/0.65
% 0.94/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------