%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRA014+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 01:22:53 PM UTC 2026
% Result : Theorem 5.24s 1.33s
% Output : Proof 5.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 162
% Number of leaves : 6
% Syntax : Number of formulae : 403 ( 22 unt; 0 def)
% Number of atoms : 1853 ( 0 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 1709 ( 259 ~;1429 |; 17 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 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 : 96 ( 0 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B] :
( less_than(A,B)
=> ( green(A,B)
| red(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',partition) ).
fof(f4_nnf,plain,
! [A,B] :
( green(A,B)
| red(A,B)
| ~ less_than(A,B) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B] :
( green(A,B)
| red(A,B)
| ~ less_than(A,B) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c8,plain,
( green(X0,X1)
| red(X0,X1)
| ~ less_than(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
fof(f2,axiom,
( less_than(n5,n6)
& less_than(n4,n5)
& less_than(n3,n4)
& less_than(n2,n3)
& less_than(n1,n2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordering) ).
fof(f2_nnf,plain,
( less_than(n5,n6)
& less_than(n4,n5)
& less_than(n3,n4)
& less_than(n2,n3)
& less_than(n1,n2) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( less_than(n5,n6)
& less_than(n4,n5)
& less_than(n3,n4)
& less_than(n2,n3)
& less_than(n1,n2) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
less_than(n1,n2),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p21,plain,
( green(n1,n2)
| red(n1,n2) ),
inference(resolution,[status(thm)],[c8,c2]) ).
fof(f1,axiom,
! [A,B,C] :
( ( green(A,C)
& green(B,C)
& green(A,B) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',green_clique) ).
fof(f1_nnf,plain,
! [A,B,C] :
( goal
| ~ green(A,C)
| ~ green(B,C)
| ~ green(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] :
( goal
| ~ green(A,C)
| ~ green(B,C)
| ~ green(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( goal
| ~ green(X0,X2)
| ~ green(X1,X2)
| ~ green(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p32,plain,
( goal
| ~ green(n1,X0)
| ~ green(n2,X0)
| red(n1,n2) ),
inference(resolution,[status(thm)],[p21,c1]) ).
cnf(c3,plain,
less_than(n2,n3),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p22,plain,
( green(n2,n3)
| red(n2,n3) ),
inference(resolution,[status(thm)],[c8,c3]) ).
cnf(p48,plain,
( red(n2,n3)
| goal
| ~ green(n1,n3)
| red(n1,n2) ),
inference(resolution,[status(thm)],[p32,p22]) ).
fof(f3,axiom,
! [A,B,C] :
( ( less_than(B,C)
& less_than(A,B) )
=> less_than(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_than_transitive) ).
fof(f3_nnf,plain,
! [A,B,C] :
( less_than(A,C)
| ~ less_than(B,C)
| ~ less_than(A,B) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B,C] :
( less_than(A,C)
| ~ less_than(B,C)
| ~ less_than(A,B) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c7,plain,
( less_than(X0,X2)
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p16,plain,
( less_than(n1,X0)
| ~ less_than(n2,X0) ),
inference(resolution,[status(thm)],[c7,c2]) ).
cnf(p28,plain,
less_than(n1,n3),
inference(resolution,[status(thm)],[p16,c3]) ).
cnf(p38,plain,
( green(n1,n3)
| red(n1,n3) ),
inference(resolution,[status(thm)],[p28,c8]) ).
cnf(p68,plain,
( red(n1,n3)
| red(n2,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p48,p38]) ).
fof(f0,axiom,
! [A,B,C] :
( ( red(A,C)
& red(B,C)
& red(A,B) )
=> goal ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',red_clique) ).
fof(f0_nnf,plain,
! [A,B,C] :
( goal
| ~ red(A,C)
| ~ red(B,C)
| ~ red(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B,C] :
( goal
| ~ red(A,C)
| ~ red(B,C)
| ~ red(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( goal
| ~ red(X0,X2)
| ~ red(X1,X2)
| ~ red(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p92,plain,
( goal
| ~ red(n2,X0)
| ~ red(n3,X0)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p68,c0]) ).
cnf(p114,plain,
( ~ red(n2,X0)
| ~ red(n3,X0)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p92]) ).
cnf(p53,plain,
( goal
| ~ green(n1,X0)
| ~ green(n3,X0)
| red(n1,n3) ),
inference(resolution,[status(thm)],[p38,c1]) ).
cnf(c4,plain,
less_than(n3,n4),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p18,plain,
( less_than(n3,X0)
| ~ less_than(n4,X0) ),
inference(resolution,[status(thm)],[c7,c4]) ).
cnf(c5,plain,
less_than(n4,n5),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p30,plain,
less_than(n3,n5),
inference(resolution,[status(thm)],[p18,c5]) ).
cnf(p43,plain,
( green(n3,n5)
| red(n3,n5) ),
inference(resolution,[status(thm)],[p30,c8]) ).
cnf(p75,plain,
( red(n3,n5)
| goal
| ~ green(n1,n5)
| red(n1,n3) ),
inference(resolution,[status(thm)],[p53,p43]) ).
cnf(p37,plain,
( less_than(n1,X0)
| ~ less_than(n3,X0) ),
inference(resolution,[status(thm)],[p28,c7]) ).
cnf(p52,plain,
less_than(n1,n5),
inference(resolution,[status(thm)],[p37,p30]) ).
cnf(p73,plain,
( green(n1,n5)
| red(n1,n5) ),
inference(resolution,[status(thm)],[p52,c8]) ).
cnf(p98,plain,
( red(n1,n5)
| red(n3,n5)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p75,p73]) ).
cnf(p135,plain,
( red(n1,n5)
| goal
| red(n1,n3)
| ~ red(n2,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p114,p98]) ).
cnf(p164,plain,
( red(n1,n5)
| red(n1,n3)
| ~ red(n2,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p135]) ).
cnf(p207,plain,
( red(n1,n5)
| ~ red(n2,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p164]) ).
cnf(p17,plain,
( less_than(n2,X0)
| ~ less_than(n3,X0) ),
inference(resolution,[status(thm)],[c7,c3]) ).
cnf(p44,plain,
less_than(n2,n5),
inference(resolution,[status(thm)],[p30,p17]) ).
cnf(p62,plain,
( green(n2,n5)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p44,c8]) ).
cnf(p84,plain,
( goal
| ~ green(n1,n5)
| red(n1,n2)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p62,p32]) ).
cnf(p108,plain,
( red(n1,n5)
| goal
| red(n1,n2)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p84,p73]) ).
cnf(p251,plain,
( red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p207,p108]) ).
cnf(p317,plain,
( red(n1,n5)
| goal
| red(n1,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p251]) ).
cnf(p405,plain,
( red(n1,n5)
| red(n1,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p317]) ).
cnf(p484,plain,
( red(n1,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p405]) ).
cnf(p544,plain,
( goal
| ~ red(n1,X0)
| ~ red(n5,X0)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p484,c0]) ).
cnf(p582,plain,
( ~ red(n1,X0)
| ~ red(n5,X0)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p544]) ).
cnf(p24,plain,
( green(n4,n5)
| red(n4,n5) ),
inference(resolution,[status(thm)],[c8,c5]) ).
cnf(p35,plain,
( goal
| ~ green(n4,X0)
| ~ green(n5,X0)
| red(n4,n5) ),
inference(resolution,[status(thm)],[p24,c1]) ).
cnf(c6,plain,
less_than(n5,n6),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p25,plain,
( green(n5,n6)
| red(n5,n6) ),
inference(resolution,[status(thm)],[c8,c6]) ).
cnf(p51,plain,
( red(n5,n6)
| goal
| ~ green(n4,n6)
| red(n4,n5) ),
inference(resolution,[status(thm)],[p35,p25]) ).
cnf(p19,plain,
( less_than(n4,X0)
| ~ less_than(n5,X0) ),
inference(resolution,[status(thm)],[c7,c5]) ).
cnf(p31,plain,
less_than(n4,n6),
inference(resolution,[status(thm)],[p19,c6]) ).
cnf(p46,plain,
( green(n4,n6)
| red(n4,n6) ),
inference(resolution,[status(thm)],[p31,c8]) ).
cnf(p71,plain,
( red(n4,n6)
| red(n5,n6)
| goal
| red(n4,n5) ),
inference(resolution,[status(thm)],[p51,p46]) ).
cnf(p611,plain,
( red(n4,n6)
| goal
| red(n4,n5)
| ~ red(n1,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p582,p71]) ).
cnf(p641,plain,
( red(n4,n6)
| red(n4,n5)
| ~ red(n1,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p611]) ).
cnf(p47,plain,
less_than(n3,n6),
inference(resolution,[status(thm)],[p31,p18]) ).
cnf(p67,plain,
less_than(n1,n6),
inference(resolution,[status(thm)],[p47,p37]) ).
cnf(p91,plain,
( green(n1,n6)
| red(n1,n6) ),
inference(resolution,[status(thm)],[p67,c8]) ).
cnf(p66,plain,
( green(n3,n6)
| red(n3,n6) ),
inference(resolution,[status(thm)],[p47,c8]) ).
cnf(p88,plain,
( goal
| ~ green(n1,n6)
| red(n1,n3)
| red(n3,n6) ),
inference(resolution,[status(thm)],[p66,p53]) ).
cnf(p113,plain,
( goal
| red(n1,n3)
| red(n3,n6)
| red(n1,n6) ),
inference(resolution,[status(thm)],[p91,p88]) ).
cnf(p136,plain,
( goal
| red(n1,n3)
| red(n1,n6)
| ~ red(n2,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p114,p113]) ).
cnf(p166,plain,
( red(n1,n3)
| red(n1,n6)
| ~ red(n2,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p136]) ).
cnf(p208,plain,
( red(n1,n6)
| ~ red(n2,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p166]) ).
cnf(p29,plain,
less_than(n2,n4),
inference(resolution,[status(thm)],[p17,c4]) ).
cnf(p39,plain,
( less_than(n2,X0)
| ~ less_than(n4,X0) ),
inference(resolution,[status(thm)],[p29,c7]) ).
cnf(p54,plain,
less_than(n2,n6),
inference(resolution,[status(thm)],[p39,p31]) ).
cnf(p77,plain,
( green(n2,n6)
| red(n2,n6) ),
inference(resolution,[status(thm)],[p54,c8]) ).
cnf(p100,plain,
( goal
| ~ green(n1,n6)
| red(n1,n2)
| red(n2,n6) ),
inference(resolution,[status(thm)],[p77,p32]) ).
cnf(p121,plain,
( red(n1,n6)
| goal
| red(n1,n2)
| red(n2,n6) ),
inference(resolution,[status(thm)],[p100,p91]) ).
cnf(p252,plain,
( red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p208,p121]) ).
cnf(p320,plain,
( red(n1,n6)
| goal
| red(n1,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p252]) ).
cnf(p407,plain,
( red(n1,n6)
| red(n1,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p320]) ).
cnf(p485,plain,
( red(n1,n6)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p407]) ).
cnf(p675,plain,
( red(n1,n3)
| goal
| red(n1,n2)
| red(n4,n6)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p641,p485]) ).
cnf(p710,plain,
( red(n1,n3)
| goal
| red(n4,n6)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p675]) ).
cnf(p755,plain,
( red(n1,n3)
| red(n4,n6)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p710]) ).
cnf(p795,plain,
( red(n4,n6)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p755]) ).
cnf(p23,plain,
( green(n3,n4)
| red(n3,n4) ),
inference(resolution,[status(thm)],[c8,c4]) ).
cnf(p74,plain,
( red(n3,n4)
| goal
| ~ green(n1,n4)
| red(n1,n3) ),
inference(resolution,[status(thm)],[p53,p23]) ).
cnf(p41,plain,
less_than(n1,n4),
inference(resolution,[status(thm)],[p29,p16]) ).
cnf(p58,plain,
( green(n1,n4)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p41,c8]) ).
cnf(p97,plain,
( red(n1,n4)
| red(n3,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p74,p58]) ).
cnf(p134,plain,
( red(n1,n4)
| goal
| red(n1,n3)
| ~ red(n2,n4)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p114,p97]) ).
cnf(p162,plain,
( red(n1,n4)
| red(n1,n3)
| ~ red(n2,n4)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p134]) ).
cnf(p206,plain,
( red(n1,n4)
| ~ red(n2,n4)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p162]) ).
cnf(p40,plain,
( green(n2,n4)
| red(n2,n4) ),
inference(resolution,[status(thm)],[p29,c8]) ).
cnf(p56,plain,
( goal
| ~ green(n1,n4)
| red(n1,n2)
| red(n2,n4) ),
inference(resolution,[status(thm)],[p40,p32]) ).
cnf(p81,plain,
( goal
| red(n1,n2)
| red(n2,n4)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p58,p56]) ).
cnf(p250,plain,
( goal
| red(n1,n2)
| red(n1,n4)
| red(n1,n4)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p206,p81]) ).
cnf(p314,plain,
( goal
| red(n1,n4)
| red(n1,n4)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p250]) ).
cnf(p403,plain,
( red(n1,n4)
| red(n1,n4)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p314]) ).
cnf(p483,plain,
( red(n1,n4)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p403]) ).
cnf(p543,plain,
( goal
| ~ red(n1,X0)
| ~ red(n4,X0)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p483,c0]) ).
cnf(p581,plain,
( ~ red(n1,X0)
| ~ red(n4,X0)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p543]) ).
cnf(p836,plain,
( ~ red(n1,n6)
| red(n1,n3)
| goal
| red(n1,n2)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p795,p581]) ).
cnf(p876,plain,
( ~ red(n1,n6)
| red(n1,n3)
| goal
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p836]) ).
cnf(p921,plain,
( ~ red(n1,n6)
| red(n1,n3)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p876]) ).
cnf(p955,plain,
( ~ red(n1,n6)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p921]) ).
cnf(p982,plain,
( red(n1,n3)
| goal
| red(n1,n2)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p955,p485]) ).
cnf(p1010,plain,
( red(n1,n3)
| goal
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p982]) ).
cnf(p1041,plain,
( red(n1,n3)
| red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1010]) ).
cnf(p1064,plain,
( red(n4,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1041]) ).
cnf(p1087,plain,
( ~ red(n1,n5)
| red(n1,n3)
| goal
| red(n1,n2)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1064,p581]) ).
cnf(p1115,plain,
( ~ red(n1,n5)
| red(n1,n3)
| goal
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1087]) ).
cnf(p1139,plain,
( ~ red(n1,n5)
| red(n1,n3)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1115]) ).
cnf(p1156,plain,
( ~ red(n1,n5)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1139]) ).
cnf(p1165,plain,
( red(n1,n3)
| goal
| red(n1,n2)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1156,p484]) ).
cnf(p1170,plain,
( red(n1,n3)
| goal
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1165]) ).
cnf(p1174,plain,
( red(n1,n3)
| red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1170]) ).
cnf(p1177,plain,
( red(n1,n3)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1174]) ).
cnf(p1178,plain,
( goal
| ~ red(n1,X0)
| ~ red(n3,X0)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1177,c0]) ).
cnf(p1179,plain,
( ~ red(n1,X0)
| ~ red(n3,X0)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1178]) ).
cnf(p105,plain,
( goal
| ~ red(n2,X0)
| ~ red(n4,X0)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p81,c0]) ).
cnf(p126,plain,
( ~ red(n2,X0)
| ~ red(n4,X0)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p105]) ).
cnf(p80,plain,
( goal
| ~ green(n1,X0)
| ~ green(n4,X0)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p58,c1]) ).
cnf(p103,plain,
( red(n4,n5)
| goal
| ~ green(n1,n5)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p80,p24]) ).
cnf(p124,plain,
( red(n1,n5)
| red(n4,n5)
| goal
| red(n1,n4) ),
inference(resolution,[status(thm)],[p103,p73]) ).
cnf(p152,plain,
( red(n1,n5)
| goal
| red(n1,n4)
| ~ red(n2,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p126,p124]) ).
cnf(p194,plain,
( red(n1,n5)
| goal
| ~ red(n2,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p152]) ).
cnf(p238,plain,
( red(n1,n5)
| ~ red(n2,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p194]) ).
cnf(p299,plain,
( red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p238,p108]) ).
cnf(p383,plain,
( red(n1,n5)
| goal
| red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p299]) ).
cnf(p466,plain,
( red(n1,n5)
| red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p383]) ).
cnf(p532,plain,
( red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p466]) ).
cnf(p573,plain,
( goal
| ~ red(n1,X0)
| ~ red(n5,X0)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p532,c0]) ).
cnf(p600,plain,
( ~ red(n1,X0)
| ~ red(n5,X0)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p573]) ).
cnf(p59,plain,
( goal
| ~ green(n3,X0)
| ~ green(n5,X0)
| red(n3,n5) ),
inference(resolution,[status(thm)],[p43,c1]) ).
cnf(p82,plain,
( red(n5,n6)
| goal
| ~ green(n3,n6)
| red(n3,n5) ),
inference(resolution,[status(thm)],[p59,p25]) ).
cnf(p106,plain,
( red(n3,n6)
| red(n5,n6)
| goal
| red(n3,n5) ),
inference(resolution,[status(thm)],[p82,p66]) ).
cnf(p631,plain,
( red(n3,n6)
| goal
| red(n3,n5)
| ~ red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p600,p106]) ).
cnf(p665,plain,
( red(n3,n6)
| red(n3,n5)
| ~ red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p631]) ).
cnf(p104,plain,
( red(n4,n6)
| goal
| ~ green(n1,n6)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p80,p46]) ).
cnf(p125,plain,
( red(n1,n6)
| red(n4,n6)
| goal
| red(n1,n4) ),
inference(resolution,[status(thm)],[p104,p91]) ).
cnf(p153,plain,
( red(n1,n6)
| goal
| red(n1,n4)
| ~ red(n2,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p126,p125]) ).
cnf(p196,plain,
( red(n1,n6)
| goal
| ~ red(n2,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p153]) ).
cnf(p239,plain,
( red(n1,n6)
| ~ red(n2,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p196]) ).
cnf(p300,plain,
( red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p239,p121]) ).
cnf(p386,plain,
( red(n1,n6)
| goal
| red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p300]) ).
cnf(p468,plain,
( red(n1,n6)
| red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p386]) ).
cnf(p533,plain,
( red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p468]) ).
cnf(p694,plain,
( goal
| red(n1,n2)
| red(n1,n4)
| red(n3,n6)
| red(n3,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(resolution,[status(thm)],[p665,p533]) ).
cnf(p740,plain,
( goal
| red(n1,n2)
| red(n3,n6)
| red(n3,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p694]) ).
cnf(p785,plain,
( goal
| red(n3,n6)
| red(n3,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p740]) ).
cnf(p823,plain,
( red(n3,n6)
| red(n3,n5)
| goal
| red(n1,n2)
| red(n1,n4) ),
inference(factoring,[status(thm)],[p785]) ).
cnf(p1185,plain,
( red(n3,n5)
| goal
| red(n1,n2)
| red(n1,n4)
| ~ red(n1,n6)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1179,p823]) ).
cnf(p1192,plain,
( red(n3,n5)
| goal
| red(n1,n4)
| ~ red(n1,n6)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1185]) ).
cnf(p1202,plain,
( red(n3,n5)
| red(n1,n4)
| ~ red(n1,n6)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1192]) ).
cnf(p1216,plain,
( goal
| red(n1,n2)
| red(n1,n4)
| red(n3,n5)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1202,p533]) ).
cnf(p1224,plain,
( goal
| red(n1,n4)
| red(n3,n5)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1216]) ).
cnf(p1241,plain,
( red(n1,n4)
| red(n3,n5)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1224]) ).
cnf(p1265,plain,
( red(n3,n5)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1241]) ).
cnf(p1278,plain,
( ~ red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1265,p1179]) ).
cnf(p1287,plain,
( ~ red(n1,n5)
| goal
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1278]) ).
cnf(p1300,plain,
( ~ red(n1,n5)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1287]) ).
cnf(p1313,plain,
( goal
| red(n1,n2)
| red(n1,n4)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1300,p532]) ).
cnf(p1318,plain,
( goal
| red(n1,n4)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1313]) ).
cnf(p1324,plain,
( red(n1,n4)
| red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1318]) ).
cnf(p1329,plain,
( red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1324]) ).
cnf(p1332,plain,
( goal
| ~ red(n1,X0)
| ~ red(n4,X0)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1329,c0]) ).
cnf(p1335,plain,
( ~ red(n1,X0)
| ~ red(n4,X0)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1332]) ).
cnf(p34,plain,
( goal
| ~ green(n3,X0)
| ~ green(n4,X0)
| red(n3,n4) ),
inference(resolution,[status(thm)],[p23,c1]) ).
cnf(p64,plain,
( goal
| ~ green(n3,n6)
| red(n3,n4)
| red(n4,n6) ),
inference(resolution,[status(thm)],[p46,p34]) ).
cnf(p89,plain,
( goal
| red(n3,n4)
| red(n4,n6)
| red(n3,n6) ),
inference(resolution,[status(thm)],[p66,p64]) ).
cnf(p1340,plain,
( goal
| red(n3,n4)
| red(n3,n6)
| ~ red(n1,n6)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1335,p89]) ).
cnf(p1347,plain,
( red(n3,n4)
| red(n3,n6)
| ~ red(n1,n6)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1340]) ).
cnf(p129,plain,
( goal
| ~ red(n2,X0)
| ~ red(n5,X0)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p108,c0]) ).
cnf(p157,plain,
( ~ red(n2,X0)
| ~ red(n5,X0)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p129]) ).
cnf(p96,plain,
( goal
| ~ green(n1,X0)
| ~ green(n5,X0)
| red(n1,n5) ),
inference(resolution,[status(thm)],[p73,c1]) ).
cnf(p118,plain,
( red(n5,n6)
| goal
| ~ green(n1,n6)
| red(n1,n5) ),
inference(resolution,[status(thm)],[p96,p25]) ).
cnf(p140,plain,
( red(n1,n6)
| red(n5,n6)
| goal
| red(n1,n5) ),
inference(resolution,[status(thm)],[p118,p91]) ).
cnf(p202,plain,
( red(n1,n6)
| goal
| red(n1,n5)
| ~ red(n2,n6)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p157,p140]) ).
cnf(p245,plain,
( red(n1,n6)
| red(n1,n5)
| ~ red(n2,n6)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p202]) ).
cnf(p308,plain,
( red(n1,n6)
| ~ red(n2,n6)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p245]) ).
cnf(p396,plain,
( red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p308,p121]) ).
cnf(p475,plain,
( red(n1,n6)
| goal
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p396]) ).
cnf(p539,plain,
( red(n1,n6)
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p475]) ).
cnf(p578,plain,
( red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p539]) ).
cnf(p1353,plain,
( red(n1,n5)
| goal
| red(n1,n2)
| red(n3,n4)
| red(n3,n6)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1347,p578]) ).
cnf(p1357,plain,
( red(n1,n5)
| goal
| red(n3,n4)
| red(n3,n6)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1353]) ).
cnf(p1365,plain,
( red(n1,n5)
| red(n3,n4)
| red(n3,n6)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1357]) ).
cnf(p1373,plain,
( ~ red(n1,n6)
| goal
| red(n1,n2)
| red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1365,p1179]) ).
cnf(p1383,plain,
( ~ red(n1,n6)
| goal
| red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1373]) ).
cnf(p1401,plain,
( ~ red(n1,n6)
| red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1383]) ).
cnf(p1413,plain,
( red(n1,n5)
| goal
| red(n1,n2)
| red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1401,p578]) ).
cnf(p1427,plain,
( red(n1,n5)
| goal
| red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1413]) ).
cnf(p1446,plain,
( red(n1,n5)
| red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1427]) ).
cnf(p1459,plain,
( red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1446]) ).
cnf(p1467,plain,
( ~ red(n1,n4)
| goal
| red(n1,n2)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1459,p1179]) ).
cnf(p1480,plain,
( ~ red(n1,n4)
| goal
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1467]) ).
cnf(p1496,plain,
( ~ red(n1,n4)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1480]) ).
cnf(p1505,plain,
( goal
| red(n1,n2)
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1496,p1329]) ).
cnf(p1512,plain,
( goal
| red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1505]) ).
cnf(p1521,plain,
( red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1512]) ).
cnf(p50,plain,
( red(n4,n5)
| goal
| ~ green(n3,n5)
| red(n3,n4) ),
inference(resolution,[status(thm)],[p34,p24]) ).
cnf(p70,plain,
( red(n3,n5)
| red(n4,n5)
| goal
| red(n3,n4) ),
inference(resolution,[status(thm)],[p50,p43]) ).
cnf(p1339,plain,
( red(n3,n5)
| goal
| red(n3,n4)
| ~ red(n1,n5)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1335,p70]) ).
cnf(p1346,plain,
( red(n3,n5)
| red(n3,n4)
| ~ red(n1,n5)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1339]) ).
cnf(p1531,plain,
( red(n3,n5)
| red(n3,n4)
| goal
| red(n1,n2)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1521,p1346]) ).
cnf(p1539,plain,
( red(n3,n5)
| red(n3,n4)
| goal
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1531]) ).
cnf(p1548,plain,
( red(n3,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1539]) ).
cnf(p1555,plain,
( ~ red(n1,n5)
| goal
| red(n1,n2)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1548,p1179]) ).
cnf(p1559,plain,
( ~ red(n1,n5)
| goal
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1555]) ).
cnf(p1566,plain,
( ~ red(n1,n5)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1559]) ).
cnf(p1573,plain,
( goal
| red(n1,n2)
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1566,p1521]) ).
cnf(p1579,plain,
( goal
| red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1573]) ).
cnf(p1587,plain,
( red(n3,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1579]) ).
cnf(p1595,plain,
( ~ red(n1,n4)
| goal
| red(n1,n2)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1587,p1179]) ).
cnf(p1602,plain,
( ~ red(n1,n4)
| goal
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1595]) ).
cnf(p1614,plain,
( ~ red(n1,n4)
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1602]) ).
cnf(p1624,plain,
( goal
| red(n1,n2)
| goal
| red(n1,n2) ),
inference(resolution,[status(thm)],[p1614,p1329]) ).
cnf(p1628,plain,
( goal
| goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1624]) ).
cnf(p1630,plain,
( goal
| red(n1,n2) ),
inference(factoring,[status(thm)],[p1628]) ).
cnf(p1631,plain,
( goal
| ~ red(n1,X0)
| ~ red(n2,X0)
| goal ),
inference(resolution,[status(thm)],[p1630,c0]) ).
cnf(p1632,plain,
( ~ red(n1,X0)
| ~ red(n2,X0)
| goal ),
inference(factoring,[status(thm)],[p1631]) ).
cnf(p119,plain,
( goal
| ~ red(n3,X0)
| ~ red(n4,X0)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p97,c0]) ).
cnf(p141,plain,
( ~ red(n3,X0)
| ~ red(n4,X0)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p119]) ).
cnf(p179,plain,
( red(n1,n5)
| goal
| red(n1,n4)
| ~ red(n3,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p141,p124]) ).
cnf(p217,plain,
( red(n1,n5)
| red(n1,n4)
| ~ red(n3,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p179]) ).
cnf(p269,plain,
( red(n1,n5)
| ~ red(n3,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p217]) ).
cnf(p348,plain,
( red(n1,n5)
| goal
| red(n1,n3)
| red(n1,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p269,p98]) ).
cnf(p426,plain,
( red(n1,n5)
| goal
| red(n1,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p348]) ).
cnf(p500,plain,
( red(n1,n5)
| red(n1,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p426]) ).
cnf(p556,plain,
( red(n1,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p500]) ).
cnf(p594,plain,
( goal
| ~ red(n1,X0)
| ~ red(n5,X0)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p556,c0]) ).
cnf(p624,plain,
( ~ red(n1,X0)
| ~ red(n5,X0)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p594]) ).
cnf(p83,plain,
( goal
| ~ green(n2,X0)
| ~ green(n5,X0)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p62,c1]) ).
cnf(p107,plain,
( red(n5,n6)
| goal
| ~ green(n2,n6)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p83,p25]) ).
cnf(p128,plain,
( red(n2,n6)
| red(n5,n6)
| goal
| red(n2,n5) ),
inference(resolution,[status(thm)],[p107,p77]) ).
cnf(p659,plain,
( red(n2,n6)
| goal
| red(n2,n5)
| ~ red(n1,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p624,p128]) ).
cnf(p690,plain,
( red(n2,n6)
| red(n2,n5)
| ~ red(n1,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p659]) ).
cnf(p180,plain,
( red(n1,n6)
| goal
| red(n1,n4)
| ~ red(n3,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p141,p125]) ).
cnf(p219,plain,
( red(n1,n6)
| red(n1,n4)
| ~ red(n3,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p180]) ).
cnf(p270,plain,
( red(n1,n6)
| ~ red(n3,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p219]) ).
cnf(p350,plain,
( goal
| red(n1,n3)
| red(n1,n6)
| red(n1,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p270,p113]) ).
cnf(p430,plain,
( goal
| red(n1,n6)
| red(n1,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p350]) ).
cnf(p503,plain,
( red(n1,n6)
| red(n1,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p430]) ).
cnf(p557,plain,
( red(n1,n6)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p503]) ).
cnf(p735,plain,
( red(n1,n4)
| goal
| red(n1,n3)
| red(n2,n6)
| red(n2,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p690,p557]) ).
cnf(p779,plain,
( red(n1,n4)
| goal
| red(n2,n6)
| red(n2,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p735]) ).
cnf(p819,plain,
( red(n1,n4)
| red(n2,n6)
| red(n2,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p779]) ).
cnf(p857,plain,
( red(n2,n6)
| red(n2,n5)
| red(n1,n4)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p819]) ).
cnf(p1638,plain,
( red(n2,n5)
| red(n1,n4)
| goal
| red(n1,n3)
| ~ red(n1,n6)
| goal ),
inference(resolution,[status(thm)],[p1632,p857]) ).
cnf(p1644,plain,
( red(n2,n5)
| red(n1,n4)
| red(n1,n3)
| ~ red(n1,n6)
| goal ),
inference(factoring,[status(thm)],[p1638]) ).
cnf(p1654,plain,
( red(n1,n4)
| goal
| red(n1,n3)
| red(n2,n5)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1644,p557]) ).
cnf(p1664,plain,
( red(n1,n4)
| red(n1,n3)
| red(n2,n5)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1654]) ).
cnf(p1679,plain,
( red(n1,n4)
| red(n2,n5)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1664]) ).
cnf(p1693,plain,
( red(n2,n5)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1679]) ).
cnf(p1708,plain,
( ~ red(n1,n5)
| goal
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1693,p1632]) ).
cnf(p1726,plain,
( ~ red(n1,n5)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1708]) ).
cnf(p1734,plain,
( red(n1,n4)
| goal
| red(n1,n3)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1726,p556]) ).
cnf(p1742,plain,
( red(n1,n4)
| red(n1,n3)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1734]) ).
cnf(p1751,plain,
( red(n1,n4)
| red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1742]) ).
cnf(p1761,plain,
( red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1751]) ).
cnf(p1766,plain,
( goal
| ~ red(n1,X0)
| ~ red(n4,X0)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1761,c0]) ).
cnf(p1771,plain,
( ~ red(n1,X0)
| ~ red(n4,X0)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1766]) ).
cnf(p55,plain,
( goal
| ~ green(n2,X0)
| ~ green(n4,X0)
| red(n2,n4) ),
inference(resolution,[status(thm)],[p40,c1]) ).
cnf(p79,plain,
( red(n4,n6)
| goal
| ~ green(n2,n6)
| red(n2,n4) ),
inference(resolution,[status(thm)],[p55,p46]) ).
cnf(p102,plain,
( red(n2,n6)
| red(n4,n6)
| goal
| red(n2,n4) ),
inference(resolution,[status(thm)],[p79,p77]) ).
cnf(p1779,plain,
( red(n2,n6)
| goal
| red(n2,n4)
| ~ red(n1,n6)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1771,p102]) ).
cnf(p1786,plain,
( red(n2,n6)
| red(n2,n4)
| ~ red(n1,n6)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1779]) ).
cnf(p120,plain,
( goal
| ~ red(n3,X0)
| ~ red(n5,X0)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p98,c0]) ).
cnf(p142,plain,
( ~ red(n3,X0)
| ~ red(n5,X0)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p120]) ).
cnf(p183,plain,
( red(n1,n6)
| goal
| red(n1,n5)
| ~ red(n3,n6)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p142,p140]) ).
cnf(p223,plain,
( red(n1,n6)
| red(n1,n5)
| ~ red(n3,n6)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p183]) ).
cnf(p275,plain,
( red(n1,n6)
| ~ red(n3,n6)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p223]) ).
cnf(p359,plain,
( goal
| red(n1,n3)
| red(n1,n6)
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(resolution,[status(thm)],[p275,p113]) ).
cnf(p438,plain,
( goal
| red(n1,n6)
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p359]) ).
cnf(p510,plain,
( red(n1,n6)
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p438]) ).
cnf(p559,plain,
( red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n3) ),
inference(factoring,[status(thm)],[p510]) ).
cnf(p1791,plain,
( red(n1,n5)
| goal
| red(n1,n3)
| red(n2,n6)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1786,p559]) ).
cnf(p1796,plain,
( red(n1,n5)
| red(n1,n3)
| red(n2,n6)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1791]) ).
cnf(p1801,plain,
( red(n1,n5)
| red(n2,n6)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1796]) ).
cnf(p1810,plain,
( ~ red(n1,n6)
| goal
| red(n1,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1801,p1632]) ).
cnf(p1825,plain,
( ~ red(n1,n6)
| red(n1,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1810]) ).
cnf(p1837,plain,
( red(n1,n5)
| goal
| red(n1,n3)
| red(n1,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1825,p559]) ).
cnf(p1844,plain,
( red(n1,n5)
| red(n1,n3)
| red(n1,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1837]) ).
cnf(p1853,plain,
( red(n1,n5)
| red(n1,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1844]) ).
cnf(p1863,plain,
( red(n1,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1853]) ).
cnf(p1868,plain,
( ~ red(n1,n4)
| goal
| red(n1,n5)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1863,p1632]) ).
cnf(p1872,plain,
( ~ red(n1,n4)
| red(n1,n5)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1868]) ).
cnf(p1877,plain,
( red(n1,n3)
| goal
| red(n1,n5)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1872,p1761]) ).
cnf(p1880,plain,
( red(n1,n3)
| red(n1,n5)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1877]) ).
cnf(p1883,plain,
( red(n1,n5)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1880]) ).
cnf(p78,plain,
( red(n4,n5)
| goal
| ~ green(n2,n5)
| red(n2,n4) ),
inference(resolution,[status(thm)],[p55,p24]) ).
cnf(p101,plain,
( red(n2,n5)
| red(n4,n5)
| goal
| red(n2,n4) ),
inference(resolution,[status(thm)],[p78,p62]) ).
cnf(p1778,plain,
( red(n2,n5)
| goal
| red(n2,n4)
| ~ red(n1,n5)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1771,p101]) ).
cnf(p1785,plain,
( red(n2,n5)
| red(n2,n4)
| ~ red(n1,n5)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1778]) ).
cnf(p1887,plain,
( red(n2,n5)
| red(n2,n4)
| red(n1,n3)
| goal
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1883,p1785]) ).
cnf(p1892,plain,
( red(n2,n5)
| red(n2,n4)
| red(n1,n3)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1887]) ).
cnf(p1900,plain,
( red(n2,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1892]) ).
cnf(p1908,plain,
( ~ red(n1,n5)
| goal
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1900,p1632]) ).
cnf(p1914,plain,
( ~ red(n1,n5)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1908]) ).
cnf(p1922,plain,
( red(n1,n3)
| goal
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1914,p1883]) ).
cnf(p1928,plain,
( red(n1,n3)
| red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1922]) ).
cnf(p1933,plain,
( red(n2,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1928]) ).
cnf(p1940,plain,
( ~ red(n1,n4)
| goal
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1933,p1632]) ).
cnf(p1946,plain,
( ~ red(n1,n4)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1940]) ).
cnf(p1955,plain,
( red(n1,n3)
| goal
| red(n1,n3)
| goal ),
inference(resolution,[status(thm)],[p1946,p1761]) ).
cnf(p1961,plain,
( red(n1,n3)
| red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1955]) ).
cnf(p1963,plain,
( red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p1961]) ).
cnf(p1964,plain,
( goal
| ~ red(n1,X0)
| ~ red(n3,X0)
| goal ),
inference(resolution,[status(thm)],[p1963,c0]) ).
cnf(p1966,plain,
( ~ red(n1,X0)
| ~ red(n3,X0)
| goal ),
inference(factoring,[status(thm)],[p1964]) ).
cnf(p33,plain,
( goal
| ~ green(n2,X0)
| ~ green(n3,X0)
| red(n2,n3) ),
inference(resolution,[status(thm)],[p22,c1]) ).
cnf(p60,plain,
( goal
| ~ green(n2,n5)
| red(n2,n3)
| red(n3,n5) ),
inference(resolution,[status(thm)],[p43,p33]) ).
cnf(p85,plain,
( goal
| red(n2,n3)
| red(n3,n5)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p62,p60]) ).
cnf(p1969,plain,
( goal
| red(n2,n3)
| red(n2,n5)
| ~ red(n1,n5)
| goal ),
inference(resolution,[status(thm)],[p1966,p85]) ).
cnf(p1976,plain,
( red(n2,n3)
| red(n2,n5)
| ~ red(n1,n5)
| goal ),
inference(factoring,[status(thm)],[p1969]) ).
cnf(p49,plain,
( red(n3,n4)
| goal
| ~ green(n2,n4)
| red(n2,n3) ),
inference(resolution,[status(thm)],[p33,p23]) ).
cnf(p69,plain,
( red(n2,n4)
| red(n3,n4)
| goal
| red(n2,n3) ),
inference(resolution,[status(thm)],[p49,p40]) ).
cnf(p93,plain,
( goal
| ~ red(n3,X0)
| ~ red(n4,X0)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(resolution,[status(thm)],[p69,c0]) ).
cnf(p115,plain,
( ~ red(n3,X0)
| ~ red(n4,X0)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(factoring,[status(thm)],[p93]) ).
cnf(p138,plain,
( red(n2,n6)
| goal
| red(n2,n4)
| ~ red(n3,n6)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(resolution,[status(thm)],[p115,p102]) ).
cnf(p170,plain,
( red(n2,n6)
| red(n2,n4)
| ~ red(n3,n6)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(factoring,[status(thm)],[p138]) ).
cnf(p210,plain,
( red(n2,n6)
| ~ red(n3,n6)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(factoring,[status(thm)],[p170]) ).
cnf(p87,plain,
( goal
| ~ green(n2,n6)
| red(n2,n3)
| red(n3,n6) ),
inference(resolution,[status(thm)],[p66,p33]) ).
cnf(p110,plain,
( red(n2,n6)
| goal
| red(n2,n3)
| red(n3,n6) ),
inference(resolution,[status(thm)],[p87,p77]) ).
cnf(p255,plain,
( red(n2,n6)
| goal
| red(n2,n3)
| red(n2,n6)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(resolution,[status(thm)],[p210,p110]) ).
cnf(p327,plain,
( red(n2,n6)
| goal
| red(n2,n6)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(factoring,[status(thm)],[p255]) ).
cnf(p412,plain,
( red(n2,n6)
| red(n2,n6)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(factoring,[status(thm)],[p327]) ).
cnf(p488,plain,
( red(n2,n6)
| red(n2,n4)
| goal
| red(n2,n3) ),
inference(factoring,[status(thm)],[p412]) ).
cnf(p1634,plain,
( red(n2,n4)
| goal
| red(n2,n3)
| ~ red(n1,n6)
| goal ),
inference(resolution,[status(thm)],[p1632,p488]) ).
cnf(p1640,plain,
( red(n2,n4)
| red(n2,n3)
| ~ red(n1,n6)
| goal ),
inference(factoring,[status(thm)],[p1634]) ).
cnf(p146,plain,
( goal
| ~ red(n4,X0)
| ~ red(n5,X0)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(resolution,[status(thm)],[p124,c0]) ).
cnf(p188,plain,
( ~ red(n4,X0)
| ~ red(n5,X0)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(factoring,[status(thm)],[p146]) ).
cnf(p231,plain,
( red(n1,n6)
| goal
| red(n1,n5)
| ~ red(n4,n6)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(resolution,[status(thm)],[p188,p140]) ).
cnf(p285,plain,
( red(n1,n6)
| red(n1,n5)
| ~ red(n4,n6)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(factoring,[status(thm)],[p231]) ).
cnf(p376,plain,
( red(n1,n6)
| ~ red(n4,n6)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(factoring,[status(thm)],[p285]) ).
cnf(p459,plain,
( red(n1,n6)
| goal
| red(n1,n4)
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(resolution,[status(thm)],[p376,p125]) ).
cnf(p527,plain,
( red(n1,n6)
| goal
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(factoring,[status(thm)],[p459]) ).
cnf(p570,plain,
( red(n1,n6)
| red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(factoring,[status(thm)],[p527]) ).
cnf(p598,plain,
( red(n1,n6)
| red(n1,n5)
| goal
| red(n1,n4) ),
inference(factoring,[status(thm)],[p570]) ).
cnf(p1647,plain,
( red(n1,n5)
| goal
| red(n1,n4)
| red(n2,n4)
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p1640,p598]) ).
cnf(p1657,plain,
( red(n1,n5)
| red(n1,n4)
| red(n2,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1647]) ).
cnf(p1670,plain,
( goal
| ~ red(n2,X0)
| ~ red(n4,X0)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p1657,c0]) ).
cnf(p1684,plain,
( ~ red(n2,X0)
| ~ red(n4,X0)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1670]) ).
cnf(p1700,plain,
( red(n1,n5)
| goal
| red(n1,n4)
| ~ red(n2,n5)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p1684,p124]) ).
cnf(p1712,plain,
( red(n1,n5)
| red(n1,n4)
| ~ red(n2,n5)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1700]) ).
cnf(p1728,plain,
( red(n1,n5)
| ~ red(n2,n5)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1712]) ).
cnf(p1739,plain,
( ~ red(n2,n5)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1728]) ).
cnf(p109,plain,
( goal
| ~ red(n3,X0)
| ~ red(n5,X0)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p85,c0]) ).
cnf(p130,plain,
( ~ red(n3,X0)
| ~ red(n5,X0)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(factoring,[status(thm)],[p109]) ).
cnf(p159,plain,
( red(n2,n6)
| goal
| red(n2,n5)
| ~ red(n3,n6)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p130,p128]) ).
cnf(p204,plain,
( red(n2,n6)
| goal
| ~ red(n3,n6)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(factoring,[status(thm)],[p159]) ).
cnf(p249,plain,
( red(n2,n6)
| ~ red(n3,n6)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(factoring,[status(thm)],[p204]) ).
cnf(p312,plain,
( red(n2,n6)
| goal
| red(n2,n3)
| red(n2,n6)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(resolution,[status(thm)],[p249,p110]) ).
cnf(p399,plain,
( red(n2,n6)
| goal
| red(n2,n6)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(factoring,[status(thm)],[p312]) ).
cnf(p480,plain,
( red(n2,n6)
| red(n2,n6)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(factoring,[status(thm)],[p399]) ).
cnf(p541,plain,
( red(n2,n6)
| goal
| red(n2,n3)
| red(n2,n5) ),
inference(factoring,[status(thm)],[p480]) ).
cnf(p1635,plain,
( goal
| red(n2,n3)
| red(n2,n5)
| ~ red(n1,n6)
| goal ),
inference(resolution,[status(thm)],[p1632,p541]) ).
cnf(p1641,plain,
( red(n2,n3)
| red(n2,n5)
| ~ red(n1,n6)
| goal ),
inference(factoring,[status(thm)],[p1635]) ).
cnf(p1650,plain,
( red(n1,n5)
| goal
| red(n1,n4)
| red(n2,n3)
| red(n2,n5)
| goal ),
inference(resolution,[status(thm)],[p1641,p598]) ).
cnf(p1660,plain,
( red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| red(n2,n5)
| goal ),
inference(factoring,[status(thm)],[p1650]) ).
cnf(p1748,plain,
( red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p1739,p1660]) ).
cnf(p1755,plain,
( red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1748]) ).
cnf(p1763,plain,
( red(n1,n5)
| red(n1,n4)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1755]) ).
cnf(p1769,plain,
( red(n1,n5)
| red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1763]) ).
cnf(p1775,plain,
( red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1769]) ).
cnf(p1782,plain,
( ~ red(n1,n3)
| goal
| red(n1,n5)
| red(n1,n4)
| goal ),
inference(resolution,[status(thm)],[p1775,p1632]) ).
cnf(p1789,plain,
( ~ red(n1,n3)
| red(n1,n5)
| red(n1,n4)
| goal ),
inference(factoring,[status(thm)],[p1782]) ).
cnf(p1965,plain,
( red(n1,n5)
| red(n1,n4)
| goal
| goal ),
inference(resolution,[status(thm)],[p1963,p1789]) ).
cnf(p1967,plain,
( red(n1,n5)
| red(n1,n4)
| goal ),
inference(factoring,[status(thm)],[p1965]) ).
cnf(p1982,plain,
( red(n1,n4)
| goal
| red(n2,n3)
| red(n2,n5)
| goal ),
inference(resolution,[status(thm)],[p1976,p1967]) ).
cnf(p1988,plain,
( red(n1,n4)
| red(n2,n3)
| red(n2,n5)
| goal ),
inference(factoring,[status(thm)],[p1982]) ).
cnf(p1996,plain,
( ~ red(n1,n5)
| goal
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p1988,p1632]) ).
cnf(p2002,plain,
( ~ red(n1,n5)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p1996]) ).
cnf(p2010,plain,
( red(n1,n4)
| goal
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p2002,p1967]) ).
cnf(p2015,plain,
( red(n1,n4)
| red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p2010]) ).
cnf(p2018,plain,
( red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p2015]) ).
cnf(p2023,plain,
( ~ red(n1,n3)
| goal
| red(n1,n4)
| goal ),
inference(resolution,[status(thm)],[p2018,p1632]) ).
cnf(p2027,plain,
( ~ red(n1,n3)
| red(n1,n4)
| goal ),
inference(factoring,[status(thm)],[p2023]) ).
cnf(p2032,plain,
( goal
| red(n1,n4)
| goal ),
inference(resolution,[status(thm)],[p2027,p1963]) ).
cnf(p2033,plain,
( red(n1,n4)
| goal ),
inference(factoring,[status(thm)],[p2032]) ).
cnf(p1968,plain,
( red(n2,n4)
| goal
| red(n2,n3)
| ~ red(n1,n4)
| goal ),
inference(resolution,[status(thm)],[p1966,p69]) ).
cnf(p1975,plain,
( red(n2,n4)
| red(n2,n3)
| ~ red(n1,n4)
| goal ),
inference(factoring,[status(thm)],[p1968]) ).
cnf(p2036,plain,
( red(n2,n4)
| red(n2,n3)
| goal
| goal ),
inference(resolution,[status(thm)],[p2033,p1975]) ).
cnf(p2039,plain,
( red(n2,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p2036]) ).
cnf(p2047,plain,
( ~ red(n1,n4)
| goal
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p2039,p1632]) ).
cnf(p2055,plain,
( ~ red(n1,n4)
| red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p2047]) ).
cnf(p2062,plain,
( goal
| red(n2,n3)
| goal ),
inference(resolution,[status(thm)],[p2055,p2033]) ).
cnf(p2064,plain,
( red(n2,n3)
| goal ),
inference(factoring,[status(thm)],[p2062]) ).
cnf(p2071,plain,
( ~ red(n1,n3)
| goal
| goal ),
inference(resolution,[status(thm)],[p2064,p1632]) ).
cnf(p2078,plain,
( ~ red(n1,n3)
| goal ),
inference(factoring,[status(thm)],[p2071]) ).
cnf(p2088,plain,
( goal
| goal ),
inference(resolution,[status(thm)],[p2078,p1963]) ).
cnf(p2089,plain,
goal,
inference(factoring,[status(thm)],[p2088]) ).
fof(f5,conjecture,
goal,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_to_be_proved) ).
fof(f5_neg,negated_conjecture,
~ goal,
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
~ goal,
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
~ goal,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c9,plain,
~ goal,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p2090,plain,
$false,
inference(resolution,[status(thm)],[p2089,c9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA014+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n003.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Wed Sep 23 12:46:35 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.24/1.33 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.24/1.33 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------