%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRA014+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:22:33 EDT 2024
% Result : Theorem 164.78s 165.05s
% Output : Refutation 164.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GRA014+1 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n029.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 21:36:38 EDT 2024
% 0.15/0.37 % CPUTime :
% 164.78/165.05 % Version: 1.5
% 164.78/165.05 % SZS status Theorem
% 164.78/165.05 % SZS output start CNFRefutation
% 164.78/165.05 fof(goal_to_be_proved,conjecture,goal,file('/export/starexec/sandbox/benchmark/theBenchmark.p', goal_to_be_proved)).
% 164.78/165.05 fof(c0,negated_conjecture,(~goal),inference(assume_negation,[status(cth)],[goal_to_be_proved])).
% 164.78/165.05 fof(c1,negated_conjecture,~goal,inference(fof_simplification,[status(thm)],[c0])).
% 164.78/165.05 cnf(c2,negated_conjecture,~goal,inference(split_conjunct,[status(thm)],[c1])).
% 164.78/165.05 fof(ordering,axiom,((((less_than(n1,n2)&less_than(n2,n3))&less_than(n3,n4))&less_than(n4,n5))&less_than(n5,n6)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ordering)).
% 164.78/165.05 cnf(c10,plain,less_than(n2,n3),inference(split_conjunct,[status(thm)],[ordering])).
% 164.78/165.05 fof(partition,axiom,(![A]:(![B]:(less_than(A,B)=>(red(A,B)|green(A,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', partition)).
% 164.78/165.05 fof(c3,plain,(![A]:(![B]:(~less_than(A,B)|(red(A,B)|green(A,B))))),inference(fof_nnf,[status(thm)],[partition])).
% 164.78/165.05 fof(c4,plain,(![X2]:(![X3]:(~less_than(X2,X3)|(red(X2,X3)|green(X2,X3))))),inference(variable_rename,[status(thm)],[c3])).
% 164.78/165.05 cnf(c5,plain,~less_than(X14,X13)|red(X14,X13)|green(X14,X13),inference(split_conjunct,[status(thm)],[c4])).
% 164.78/165.05 cnf(c25,plain,red(n2,n3)|green(n2,n3),inference(resolution,[status(thm)],[c5, c10])).
% 164.78/165.05 cnf(c11,plain,less_than(n3,n4),inference(split_conjunct,[status(thm)],[ordering])).
% 164.78/165.05 cnf(c26,plain,red(n3,n4)|green(n3,n4),inference(resolution,[status(thm)],[c5, c11])).
% 164.78/165.05 fof(red_clique,axiom,(![A]:(![B]:(![C]:(((red(A,B)&red(B,C))&red(A,C))=>goal)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', red_clique)).
% 164.78/165.05 fof(c19,plain,(![A]:(![B]:(![C]:(((~red(A,B)|~red(B,C))|~red(A,C))|goal)))),inference(fof_nnf,[status(thm)],[red_clique])).
% 164.78/165.05 fof(c20,plain,((![A]:(![B]:(![C]:((~red(A,B)|~red(B,C))|~red(A,C)))))|goal),inference(shift_quantors,[status(thm)],[c19])).
% 164.78/165.05 fof(c22,plain,(![X10]:(![X11]:(![X12]:(((~red(X10,X11)|~red(X11,X12))|~red(X10,X12))|goal)))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X10]:(![X11]:(![X12]:((~red(X10,X11)|~red(X11,X12))|~red(X10,X12)))))|goal),inference(variable_rename,[status(thm)],[c20])).])).
% 164.78/165.05 cnf(c23,plain,~red(X28,X26)|~red(X26,X27)|~red(X28,X27)|goal,inference(split_conjunct,[status(thm)],[c22])).
% 164.78/165.05 fof(less_than_transitive,axiom,(![A]:(![B]:(![C]:((less_than(A,B)&less_than(B,C))=>less_than(A,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', less_than_transitive)).
% 164.78/165.05 fof(c6,plain,(![A]:(![B]:(![C]:((~less_than(A,B)|~less_than(B,C))|less_than(A,C))))),inference(fof_nnf,[status(thm)],[less_than_transitive])).
% 164.78/165.05 fof(c7,plain,(![X4]:(![X5]:(![X6]:((~less_than(X4,X5)|~less_than(X5,X6))|less_than(X4,X6))))),inference(variable_rename,[status(thm)],[c6])).
% 164.78/165.05 cnf(c8,plain,~less_than(X17,X16)|~less_than(X16,X15)|less_than(X17,X15),inference(split_conjunct,[status(thm)],[c7])).
% 164.78/165.05 cnf(c31,plain,~less_than(X20,n3)|less_than(X20,n4),inference(resolution,[status(thm)],[c8, c11])).
% 164.78/165.05 cnf(c35,plain,less_than(n2,n4),inference(resolution,[status(thm)],[c31, c10])).
% 164.78/165.05 cnf(c38,plain,red(n2,n4)|green(n2,n4),inference(resolution,[status(thm)],[c35, c5])).
% 164.78/165.05 cnf(c89,plain,green(n2,n4)|~red(n2,X60)|~red(X60,n4)|goal,inference(resolution,[status(thm)],[c38, c23])).
% 164.78/165.05 cnf(c141,plain,green(n2,n4)|~red(n2,n3)|goal|green(n3,n4),inference(resolution,[status(thm)],[c89, c26])).
% 164.78/165.05 cnf(c221,plain,green(n2,n4)|goal|green(n3,n4)|green(n2,n3),inference(resolution,[status(thm)],[c141, c25])).
% 164.78/165.05 cnf(c267,plain,green(n2,n4)|green(n3,n4)|green(n2,n3),inference(resolution,[status(thm)],[c221, c2])).
% 164.78/165.05 cnf(c12,plain,less_than(n4,n5),inference(split_conjunct,[status(thm)],[ordering])).
% 164.78/165.05 cnf(c27,plain,red(n4,n5)|green(n4,n5),inference(resolution,[status(thm)],[c5, c12])).
% 164.78/165.05 cnf(c33,plain,~less_than(X25,n4)|less_than(X25,n5),inference(resolution,[status(thm)],[c8, c12])).
% 164.78/165.05 cnf(c46,plain,less_than(n2,n5),inference(resolution,[status(thm)],[c33, c35])).
% 164.78/165.05 cnf(c51,plain,red(n2,n5)|green(n2,n5),inference(resolution,[status(thm)],[c46, c5])).
% 164.78/165.05 cnf(c97,plain,green(n2,n5)|~red(n2,X66)|~red(X66,n5)|goal,inference(resolution,[status(thm)],[c51, c23])).
% 164.78/165.05 cnf(c158,plain,green(n2,n5)|~red(n2,n4)|goal|green(n4,n5),inference(resolution,[status(thm)],[c97, c27])).
% 164.78/165.05 cnf(c230,plain,green(n2,n5)|goal|green(n4,n5)|green(n2,n4),inference(resolution,[status(thm)],[c158, c38])).
% 164.78/165.05 cnf(c600,plain,green(n2,n5)|green(n4,n5)|green(n2,n4),inference(resolution,[status(thm)],[c230, c2])).
% 164.78/165.05 fof(green_clique,axiom,(![A]:(![B]:(![C]:(((green(A,B)&green(B,C))&green(A,C))=>goal)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', green_clique)).
% 164.78/165.05 fof(c14,plain,(![A]:(![B]:(![C]:(((~green(A,B)|~green(B,C))|~green(A,C))|goal)))),inference(fof_nnf,[status(thm)],[green_clique])).
% 164.78/165.05 fof(c15,plain,((![A]:(![B]:(![C]:((~green(A,B)|~green(B,C))|~green(A,C)))))|goal),inference(shift_quantors,[status(thm)],[c14])).
% 164.78/165.05 fof(c17,plain,(![X7]:(![X8]:(![X9]:(((~green(X7,X8)|~green(X8,X9))|~green(X7,X9))|goal)))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X7]:(![X8]:(![X9]:((~green(X7,X8)|~green(X8,X9))|~green(X7,X9)))))|goal),inference(variable_rename,[status(thm)],[c15])).])).
% 164.78/165.05 cnf(c18,plain,~green(X21,X22)|~green(X22,X23)|~green(X21,X23)|goal,inference(split_conjunct,[status(thm)],[c17])).
% 164.78/165.05 cnf(c47,plain,less_than(n3,n5),inference(resolution,[status(thm)],[c33, c11])).
% 164.78/165.05 cnf(c53,plain,red(n3,n5)|green(n3,n5),inference(resolution,[status(thm)],[c47, c5])).
% 164.78/165.05 cnf(c157,plain,green(n2,n5)|~red(n2,n3)|goal|green(n3,n5),inference(resolution,[status(thm)],[c97, c53])).
% 164.78/165.05 cnf(c229,plain,green(n2,n5)|goal|green(n3,n5)|green(n2,n3),inference(resolution,[status(thm)],[c157, c25])).
% 164.78/165.05 cnf(c569,plain,green(n2,n5)|goal|green(n2,n3)|~green(n3,X129)|~green(X129,n5),inference(resolution,[status(thm)],[c229, c18])).
% 164.78/165.05 cnf(c2283,plain,green(n2,n5)|goal|green(n2,n3)|~green(n3,n4)|green(n2,n4),inference(resolution,[status(thm)],[c569, c600])).
% 164.78/165.05 cnf(c26843,plain,green(n2,n5)|goal|green(n2,n3)|green(n2,n4),inference(resolution,[status(thm)],[c2283, c267])).
% 164.78/165.05 cnf(c26888,plain,green(n2,n5)|green(n2,n3)|green(n2,n4),inference(resolution,[status(thm)],[c26843, c2])).
% 164.78/165.05 cnf(c13,plain,less_than(n5,n6),inference(split_conjunct,[status(thm)],[ordering])).
% 164.78/165.05 cnf(c34,plain,~less_than(X29,n5)|less_than(X29,n6),inference(resolution,[status(thm)],[c8, c13])).
% 164.78/165.05 cnf(c59,plain,less_than(n4,n6),inference(resolution,[status(thm)],[c34, c12])).
% 164.78/165.05 cnf(c67,plain,red(n4,n6)|green(n4,n6),inference(resolution,[status(thm)],[c59, c5])).
% 164.78/165.05 cnf(c58,plain,less_than(n2,n6),inference(resolution,[status(thm)],[c34, c46])).
% 164.78/165.05 cnf(c65,plain,red(n2,n6)|green(n2,n6),inference(resolution,[status(thm)],[c58, c5])).
% 164.78/165.05 cnf(c105,plain,green(n2,n6)|~red(n2,X74)|~red(X74,n6)|goal,inference(resolution,[status(thm)],[c65, c23])).
% 164.78/165.05 cnf(c193,plain,green(n2,n6)|~red(n2,n4)|goal|green(n4,n6),inference(resolution,[status(thm)],[c105, c67])).
% 164.78/165.05 cnf(c250,plain,green(n2,n6)|goal|green(n4,n6)|green(n2,n4),inference(resolution,[status(thm)],[c193, c38])).
% 164.78/165.05 cnf(c1338,plain,goal|green(n4,n6)|green(n2,n4)|~green(n2,X254)|~green(X254,n6),inference(resolution,[status(thm)],[c250, c18])).
% 164.78/165.05 cnf(c9,plain,less_than(n1,n2),inference(split_conjunct,[status(thm)],[ordering])).
% 164.78/165.05 cnf(c24,plain,red(n1,n2)|green(n1,n2),inference(resolution,[status(thm)],[c5, c9])).
% 164.78/165.05 cnf(c32,plain,~less_than(X24,n2)|less_than(X24,n3),inference(resolution,[status(thm)],[c8, c10])).
% 164.78/165.05 cnf(c40,plain,less_than(n1,n3),inference(resolution,[status(thm)],[c32, c9])).
% 164.78/165.05 cnf(c43,plain,less_than(n1,n4),inference(resolution,[status(thm)],[c40, c31])).
% 164.78/165.05 cnf(c44,plain,red(n1,n4)|green(n1,n4),inference(resolution,[status(thm)],[c43, c5])).
% 164.78/165.05 cnf(c95,plain,green(n1,n4)|~red(n1,X64)|~red(X64,n4)|goal,inference(resolution,[status(thm)],[c44, c23])).
% 164.78/165.05 cnf(c153,plain,green(n1,n4)|~red(n1,n2)|goal|green(n2,n4),inference(resolution,[status(thm)],[c95, c38])).
% 164.78/165.05 cnf(c226,plain,green(n1,n4)|goal|green(n2,n4)|green(n1,n2),inference(resolution,[status(thm)],[c153, c24])).
% 164.78/165.05 cnf(c452,plain,green(n1,n4)|green(n2,n4)|green(n1,n2),inference(resolution,[status(thm)],[c226, c2])).
% 164.78/165.05 cnf(c1340,plain,green(n2,n6)|green(n4,n6)|green(n2,n4),inference(resolution,[status(thm)],[c250, c2])).
% 164.78/165.05 cnf(c48,plain,less_than(n1,n5),inference(resolution,[status(thm)],[c33, c43])).
% 164.78/165.05 cnf(c57,plain,less_than(n1,n6),inference(resolution,[status(thm)],[c34, c48])).
% 164.78/165.05 cnf(c61,plain,red(n1,n6)|green(n1,n6),inference(resolution,[status(thm)],[c57, c5])).
% 164.78/165.05 cnf(c103,plain,green(n1,n6)|~red(n1,X72)|~red(X72,n6)|goal,inference(resolution,[status(thm)],[c61, c23])).
% 164.78/165.05 cnf(c183,plain,green(n1,n6)|~red(n1,n4)|goal|green(n4,n6),inference(resolution,[status(thm)],[c103, c67])).
% 164.78/165.05 cnf(c243,plain,green(n1,n6)|goal|green(n4,n6)|green(n1,n4),inference(resolution,[status(thm)],[c183, c44])).
% 164.78/165.05 cnf(c1079,plain,goal|green(n4,n6)|green(n1,n4)|~green(n1,X212)|~green(X212,n6),inference(resolution,[status(thm)],[c243, c18])).
% 164.78/165.05 cnf(c3332,plain,goal|green(n4,n6)|green(n1,n4)|~green(n1,n2)|green(n2,n4),inference(resolution,[status(thm)],[c1079, c1340])).
% 164.78/165.05 cnf(c66506,plain,goal|green(n4,n6)|green(n1,n4)|green(n2,n4),inference(resolution,[status(thm)],[c3332, c452])).
% 164.78/165.05 cnf(c66534,plain,green(n4,n6)|green(n1,n4)|green(n2,n4),inference(resolution,[status(thm)],[c66506, c2])).
% 164.78/165.05 cnf(c28,plain,red(n5,n6)|green(n5,n6),inference(resolution,[status(thm)],[c13, c5])).
% 164.78/165.05 cnf(c108,plain,green(n4,n6)|~red(n4,X76)|~red(X76,n6)|goal,inference(resolution,[status(thm)],[c67, c23])).
% 164.78/165.05 cnf(c205,plain,green(n4,n6)|~red(n4,n5)|goal|green(n5,n6),inference(resolution,[status(thm)],[c108, c28])).
% 164.78/165.05 cnf(c255,plain,green(n4,n6)|goal|green(n5,n6)|green(n4,n5),inference(resolution,[status(thm)],[c205, c27])).
% 164.78/165.05 cnf(c1525,plain,green(n4,n6)|green(n5,n6)|green(n4,n5),inference(resolution,[status(thm)],[c255, c2])).
% 164.78/165.05 cnf(c55,plain,red(n1,n5)|green(n1,n5),inference(resolution,[status(thm)],[c48, c5])).
% 164.78/165.05 cnf(c101,plain,green(n1,n5)|~red(n1,X70)|~red(X70,n5)|goal,inference(resolution,[status(thm)],[c55, c23])).
% 164.78/165.05 cnf(c175,plain,green(n1,n5)|~red(n1,n2)|goal|green(n2,n5),inference(resolution,[status(thm)],[c101, c51])).
% 164.78/165.05 cnf(c237,plain,green(n1,n5)|goal|green(n2,n5)|green(n1,n2),inference(resolution,[status(thm)],[c175, c24])).
% 164.78/165.05 cnf(c859,plain,green(n1,n5)|green(n2,n5)|green(n1,n2),inference(resolution,[status(thm)],[c237, c2])).
% 164.78/165.05 cnf(c195,plain,green(n2,n6)|~red(n2,n5)|goal|green(n5,n6),inference(resolution,[status(thm)],[c105, c28])).
% 164.78/165.05 cnf(c251,plain,green(n2,n6)|goal|green(n5,n6)|green(n2,n5),inference(resolution,[status(thm)],[c195, c51])).
% 164.78/165.05 cnf(c1377,plain,green(n2,n6)|green(n5,n6)|green(n2,n5),inference(resolution,[status(thm)],[c251, c2])).
% 164.78/165.05 cnf(c185,plain,green(n1,n6)|~red(n1,n5)|goal|green(n5,n6),inference(resolution,[status(thm)],[c103, c28])).
% 164.78/165.05 cnf(c244,plain,green(n1,n6)|goal|green(n5,n6)|green(n1,n5),inference(resolution,[status(thm)],[c185, c55])).
% 164.78/165.05 cnf(c1116,plain,goal|green(n5,n6)|green(n1,n5)|~green(n1,X218)|~green(X218,n6),inference(resolution,[status(thm)],[c244, c18])).
% 164.78/165.05 cnf(c3477,plain,goal|green(n5,n6)|green(n1,n5)|~green(n1,n2)|green(n2,n5),inference(resolution,[status(thm)],[c1116, c1377])).
% 164.78/165.05 cnf(c74667,plain,goal|green(n5,n6)|green(n1,n5)|green(n2,n5),inference(resolution,[status(thm)],[c3477, c859])).
% 164.78/165.05 cnf(c74891,plain,goal|green(n5,n6)|green(n1,n5)|~green(n2,X861)|~green(X861,n5),inference(resolution,[status(thm)],[c74667, c18])).
% 164.78/165.05 cnf(c41,plain,red(n1,n3)|green(n1,n3),inference(resolution,[status(thm)],[c40, c5])).
% 164.78/165.05 cnf(c173,plain,green(n1,n5)|~red(n1,n3)|goal|green(n3,n5),inference(resolution,[status(thm)],[c101, c53])).
% 164.78/165.05 cnf(c235,plain,green(n1,n5)|goal|green(n3,n5)|green(n1,n3),inference(resolution,[status(thm)],[c173, c41])).
% 164.78/165.05 cnf(c785,plain,green(n1,n5)|green(n3,n5)|green(n1,n3),inference(resolution,[status(thm)],[c235, c2])).
% 164.78/165.05 cnf(c60,plain,less_than(n3,n6),inference(resolution,[status(thm)],[c34, c47])).
% 164.78/165.05 cnf(c69,plain,red(n3,n6)|green(n3,n6),inference(resolution,[status(thm)],[c60, c5])).
% 164.78/165.05 cnf(c110,plain,green(n3,n6)|~red(n3,X78)|~red(X78,n6)|goal,inference(resolution,[status(thm)],[c69, c23])).
% 164.78/165.05 cnf(c215,plain,green(n3,n6)|~red(n3,n5)|goal|green(n5,n6),inference(resolution,[status(thm)],[c110, c28])).
% 164.78/165.05 cnf(c258,plain,green(n3,n6)|goal|green(n5,n6)|green(n3,n5),inference(resolution,[status(thm)],[c215, c53])).
% 164.78/165.05 cnf(c1636,plain,green(n3,n6)|green(n5,n6)|green(n3,n5),inference(resolution,[status(thm)],[c258, c2])).
% 164.78/165.05 cnf(c3498,plain,goal|green(n5,n6)|green(n1,n5)|~green(n1,n3)|green(n3,n5),inference(resolution,[status(thm)],[c1116, c1636])).
% 164.78/165.05 cnf(c77269,plain,goal|green(n5,n6)|green(n1,n5)|green(n3,n5),inference(resolution,[status(thm)],[c3498, c785])).
% 164.78/165.05 cnf(c77572,plain,goal|green(n5,n6)|green(n1,n5)|~green(n2,n3),inference(resolution,[status(thm)],[c77269, c74891])).
% 164.78/165.05 cnf(c77886,plain,goal|green(n5,n6)|green(n1,n5)|red(n2,n3),inference(resolution,[status(thm)],[c77572, c25])).
% 164.78/165.05 cnf(c77889,plain,green(n5,n6)|green(n1,n5)|red(n2,n3),inference(resolution,[status(thm)],[c77886, c2])).
% 164.78/165.05 cnf(c174,plain,green(n1,n5)|~red(n1,n4)|goal|green(n4,n5),inference(resolution,[status(thm)],[c101, c27])).
% 164.78/165.05 cnf(c236,plain,green(n1,n5)|goal|green(n4,n5)|green(n1,n4),inference(resolution,[status(thm)],[c174, c44])).
% 164.78/165.05 cnf(c822,plain,green(n1,n5)|green(n4,n5)|green(n1,n4),inference(resolution,[status(thm)],[c236, c2])).
% 164.78/165.05 cnf(c3482,plain,goal|green(n5,n6)|green(n1,n5)|~green(n1,n4)|green(n4,n5),inference(resolution,[status(thm)],[c1116, c1525])).
% 164.78/165.05 cnf(c75542,plain,goal|green(n5,n6)|green(n1,n5)|green(n4,n5),inference(resolution,[status(thm)],[c3482, c822])).
% 164.78/165.05 cnf(c75729,plain,goal|green(n5,n6)|green(n1,n5)|~green(n2,n4),inference(resolution,[status(thm)],[c75542, c74891])).
% 164.78/165.05 cnf(c76003,plain,goal|green(n5,n6)|green(n1,n5)|red(n2,n4),inference(resolution,[status(thm)],[c75729, c38])).
% 164.78/165.05 cnf(c76184,plain,goal|green(n5,n6)|green(n1,n5)|~red(n2,X873)|~red(X873,n4),inference(resolution,[status(thm)],[c76003, c23])).
% 164.78/165.05 cnf(c75560,plain,green(n5,n6)|green(n1,n5)|green(n4,n5),inference(resolution,[status(thm)],[c75542, c2])).
% 164.78/165.05 cnf(c77613,plain,goal|green(n5,n6)|green(n1,n5)|~green(n3,X880)|~green(X880,n5),inference(resolution,[status(thm)],[c77269, c18])).
% 164.78/165.05 cnf(c78618,plain,goal|green(n5,n6)|green(n1,n5)|~green(n3,n4),inference(resolution,[status(thm)],[c77613, c75560])).
% 164.78/165.05 cnf(c78699,plain,goal|green(n5,n6)|green(n1,n5)|red(n3,n4),inference(resolution,[status(thm)],[c78618, c26])).
% 164.78/165.05 cnf(c78916,plain,goal|green(n5,n6)|green(n1,n5)|~red(n2,n3),inference(resolution,[status(thm)],[c78699, c76184])).
% 164.78/165.05 cnf(c79148,plain,goal|green(n5,n6)|green(n1,n5),inference(resolution,[status(thm)],[c78916, c77889])).
% 164.78/165.05 cnf(c79296,plain,goal|green(n5,n6)|~green(n1,X883)|~green(X883,n5),inference(resolution,[status(thm)],[c79148, c18])).
% 164.78/165.05 cnf(c79802,plain,goal|green(n5,n6)|~green(n1,n4)|green(n4,n6),inference(resolution,[status(thm)],[c79296, c1525])).
% 164.78/165.05 cnf(c80207,plain,goal|green(n5,n6)|green(n4,n6)|green(n2,n4),inference(resolution,[status(thm)],[c79802, c66534])).
% 164.78/165.05 cnf(c91504,plain,goal|green(n4,n6)|green(n2,n4)|~green(n2,n5),inference(resolution,[status(thm)],[c80207, c1338])).
% 164.78/165.05 cnf(c95737,plain,goal|green(n4,n6)|green(n2,n4)|green(n2,n3),inference(resolution,[status(thm)],[c91504, c26888])).
% 164.78/165.05 cnf(c108886,plain,green(n4,n6)|green(n2,n4)|green(n2,n3),inference(resolution,[status(thm)],[c95737, c2])).
% 164.78/165.05 cnf(c192,plain,green(n2,n6)|~red(n2,n3)|goal|green(n3,n6),inference(resolution,[status(thm)],[c105, c69])).
% 164.78/165.05 cnf(c249,plain,green(n2,n6)|goal|green(n3,n6)|green(n2,n3),inference(resolution,[status(thm)],[c192, c25])).
% 164.78/165.05 cnf(c1301,plain,goal|green(n3,n6)|green(n2,n3)|~green(n2,X248)|~green(X248,n6),inference(resolution,[status(thm)],[c249, c18])).
% 164.78/165.05 cnf(c93,plain,green(n1,n3)|~red(n1,X62)|~red(X62,n3)|goal,inference(resolution,[status(thm)],[c41, c23])).
% 164.78/165.05 cnf(c147,plain,green(n1,n3)|~red(n1,n2)|goal|green(n2,n3),inference(resolution,[status(thm)],[c93, c25])).
% 164.78/165.05 cnf(c223,plain,green(n1,n3)|goal|green(n2,n3)|green(n1,n2),inference(resolution,[status(thm)],[c147, c24])).
% 164.78/165.05 cnf(c341,plain,green(n1,n3)|green(n2,n3)|green(n1,n2),inference(resolution,[status(thm)],[c223, c2])).
% 164.78/165.05 cnf(c1303,plain,green(n2,n6)|green(n3,n6)|green(n2,n3),inference(resolution,[status(thm)],[c249, c2])).
% 164.78/165.05 cnf(c182,plain,green(n1,n6)|~red(n1,n3)|goal|green(n3,n6),inference(resolution,[status(thm)],[c103, c69])).
% 164.78/165.05 cnf(c242,plain,green(n1,n6)|goal|green(n3,n6)|green(n1,n3),inference(resolution,[status(thm)],[c182, c41])).
% 164.78/165.05 cnf(c1042,plain,goal|green(n3,n6)|green(n1,n3)|~green(n1,X206)|~green(X206,n6),inference(resolution,[status(thm)],[c242, c18])).
% 164.78/165.05 cnf(c3221,plain,goal|green(n3,n6)|green(n1,n3)|~green(n1,n2)|green(n2,n3),inference(resolution,[status(thm)],[c1042, c1303])).
% 164.78/165.05 cnf(c62059,plain,goal|green(n3,n6)|green(n1,n3)|green(n2,n3),inference(resolution,[status(thm)],[c3221, c341])).
% 164.78/165.05 cnf(c62081,plain,green(n3,n6)|green(n1,n3)|green(n2,n3),inference(resolution,[status(thm)],[c62059, c2])).
% 164.78/165.05 cnf(c79738,plain,goal|green(n5,n6)|~green(n1,n3)|green(n3,n6),inference(resolution,[status(thm)],[c79296, c1636])).
% 164.78/165.05 cnf(c80144,plain,goal|green(n5,n6)|green(n3,n6)|green(n2,n3),inference(resolution,[status(thm)],[c79738, c62081])).
% 164.78/165.05 cnf(c88437,plain,goal|green(n3,n6)|green(n2,n3)|~green(n2,n5),inference(resolution,[status(thm)],[c80144, c1301])).
% 164.78/165.05 cnf(c94577,plain,goal|green(n3,n6)|green(n2,n3)|green(n2,n4),inference(resolution,[status(thm)],[c88437, c26888])).
% 164.78/165.05 cnf(c99217,plain,green(n3,n6)|green(n2,n3)|green(n2,n4),inference(resolution,[status(thm)],[c94577, c2])).
% 164.78/165.05 cnf(c213,plain,green(n3,n6)|~red(n3,n4)|goal|green(n4,n6),inference(resolution,[status(thm)],[c110, c67])).
% 164.78/165.05 cnf(c90,plain,red(n2,n4)|~green(n2,X61)|~green(X61,n4)|goal,inference(resolution,[status(thm)],[c38, c18])).
% 164.78/165.05 cnf(c145,plain,red(n2,n4)|~green(n2,n3)|goal|red(n3,n4),inference(resolution,[status(thm)],[c90, c26])).
% 164.78/165.05 cnf(c222,plain,red(n2,n4)|goal|red(n3,n4)|red(n2,n3),inference(resolution,[status(thm)],[c145, c25])).
% 164.78/165.05 cnf(c303,plain,goal|red(n3,n4)|red(n2,n3)|green(n2,n6)|green(n4,n6),inference(resolution,[status(thm)],[c222, c193])).
% 164.78/165.05 cnf(c2989,plain,goal|red(n2,n3)|green(n2,n6)|green(n4,n6)|green(n3,n6),inference(resolution,[status(thm)],[c303, c213])).
% 164.78/165.05 cnf(c53362,plain,goal|green(n2,n6)|green(n4,n6)|green(n3,n6),inference(resolution,[status(thm)],[c2989, c192])).
% 164.78/165.05 cnf(c53465,plain,green(n2,n6)|green(n4,n6)|green(n3,n6),inference(resolution,[status(thm)],[c53362, c2])).
% 164.78/165.05 cnf(c1044,plain,green(n1,n6)|green(n3,n6)|green(n1,n3),inference(resolution,[status(thm)],[c242, c2])).
% 164.78/165.05 cnf(c257,plain,green(n3,n6)|goal|green(n4,n6)|green(n3,n4),inference(resolution,[status(thm)],[c213, c26])).
% 164.78/165.05 cnf(c1599,plain,green(n3,n6)|green(n4,n6)|green(n3,n4),inference(resolution,[status(thm)],[c257, c2])).
% 164.78/165.05 cnf(c1090,plain,green(n1,n6)|goal|green(n4,n6)|~green(n1,X214)|~green(X214,n4),inference(resolution,[status(thm)],[c243, c18])).
% 164.78/165.05 cnf(c3407,plain,green(n1,n6)|goal|green(n4,n6)|~green(n1,n3)|green(n3,n6),inference(resolution,[status(thm)],[c1090, c1599])).
% 164.78/165.05 cnf(c69500,plain,green(n1,n6)|goal|green(n4,n6)|green(n3,n6),inference(resolution,[status(thm)],[c3407, c1044])).
% 164.78/165.05 cnf(c69551,plain,goal|green(n4,n6)|green(n3,n6)|~green(n1,X816)|~green(X816,n6),inference(resolution,[status(thm)],[c69500, c18])).
% 164.78/165.05 cnf(c70261,plain,goal|green(n4,n6)|green(n3,n6)|~green(n1,n2),inference(resolution,[status(thm)],[c69551, c53465])).
% 164.78/165.05 cnf(c563,plain,green(n2,n5)|green(n3,n5)|green(n2,n3),inference(resolution,[status(thm)],[c229, c2])).
% 164.78/165.05 cnf(c858,plain,goal|green(n2,n5)|green(n1,n2)|~green(n1,X176)|~green(X176,n5),inference(resolution,[status(thm)],[c237, c18])).
% 164.78/165.05 cnf(c2761,plain,goal|green(n2,n5)|green(n1,n2)|~green(n1,n3)|green(n2,n3),inference(resolution,[status(thm)],[c858, c563])).
% 164.78/165.05 cnf(c40501,plain,goal|green(n2,n5)|green(n1,n2)|green(n2,n3),inference(resolution,[status(thm)],[c2761, c341])).
% 164.78/165.05 cnf(c40510,plain,green(n2,n5)|green(n1,n2)|green(n2,n3),inference(resolution,[status(thm)],[c40501, c2])).
% 164.78/165.05 cnf(c94583,plain,goal|green(n3,n6)|green(n2,n3)|green(n1,n2),inference(resolution,[status(thm)],[c88437, c40510])).
% 164.78/165.05 cnf(c100141,plain,goal|green(n3,n6)|green(n2,n3)|green(n4,n6),inference(resolution,[status(thm)],[c94583, c70261])).
% 164.78/165.05 cnf(c114918,plain,goal|green(n3,n6)|green(n2,n3)|~green(n2,n4),inference(resolution,[status(thm)],[c100141, c1301])).
% 164.78/165.05 cnf(c125156,plain,goal|green(n3,n6)|green(n2,n3),inference(resolution,[status(thm)],[c114918, c99217])).
% 164.78/165.05 cnf(c125255,plain,goal|green(n2,n3)|~green(n3,X891)|~green(X891,n6),inference(resolution,[status(thm)],[c125156, c18])).
% 164.78/165.05 cnf(c125484,plain,goal|green(n2,n3)|~green(n3,n4)|green(n2,n4),inference(resolution,[status(thm)],[c125255, c108886])).
% 164.78/165.05 cnf(c142157,plain,goal|green(n2,n3)|green(n2,n4),inference(resolution,[status(thm)],[c125484, c267])).
% 164.78/165.05 cnf(c142172,plain,green(n2,n3)|green(n2,n4),inference(resolution,[status(thm)],[c142157, c2])).
% 164.78/165.05 cnf(c99,plain,green(n3,n5)|~red(n3,X68)|~red(X68,n5)|goal,inference(resolution,[status(thm)],[c53, c23])).
% 164.78/165.05 cnf(c166,plain,green(n3,n5)|~red(n3,n4)|goal|green(n4,n5),inference(resolution,[status(thm)],[c99, c27])).
% 164.78/165.05 cnf(c233,plain,green(n3,n5)|goal|green(n4,n5)|green(n3,n4),inference(resolution,[status(thm)],[c166, c26])).
% 164.78/165.05 cnf(c711,plain,green(n3,n5)|green(n4,n5)|green(n3,n4),inference(resolution,[status(thm)],[c233, c2])).
% 164.78/165.05 cnf(c562,plain,goal|green(n3,n5)|green(n2,n3)|~green(n2,X128)|~green(X128,n5),inference(resolution,[status(thm)],[c229, c18])).
% 164.78/165.05 cnf(c2251,plain,goal|green(n3,n5)|green(n2,n3)|~green(n2,n4)|green(n3,n4),inference(resolution,[status(thm)],[c562, c711])).
% 164.78/165.05 cnf(c26340,plain,goal|green(n3,n5)|green(n2,n3)|green(n3,n4),inference(resolution,[status(thm)],[c2251, c267])).
% 164.78/165.05 cnf(c26345,plain,green(n3,n5)|green(n2,n3)|green(n3,n4),inference(resolution,[status(thm)],[c26340, c2])).
% 164.78/165.05 cnf(c1308,plain,green(n2,n6)|goal|green(n2,n3)|~green(n3,X249)|~green(X249,n6),inference(resolution,[status(thm)],[c249, c18])).
% 164.78/165.05 cnf(c181,plain,green(n1,n6)|~red(n1,n2)|goal|green(n2,n6),inference(resolution,[status(thm)],[c103, c65])).
% 164.78/165.05 cnf(c241,plain,green(n1,n6)|goal|green(n2,n6)|green(n1,n2),inference(resolution,[status(thm)],[c181, c24])).
% 164.78/165.05 cnf(c1005,plain,goal|green(n2,n6)|green(n1,n2)|~green(n1,X200)|~green(X200,n6),inference(resolution,[status(thm)],[c241, c18])).
% 164.78/165.05 cnf(c3104,plain,goal|green(n2,n6)|green(n1,n2)|~green(n1,n3)|green(n2,n3),inference(resolution,[status(thm)],[c1005, c1303])).
% 164.78/165.05 cnf(c57976,plain,goal|green(n2,n6)|green(n1,n2)|green(n2,n3),inference(resolution,[status(thm)],[c3104, c341])).
% 164.78/165.05 cnf(c57985,plain,green(n2,n6)|green(n1,n2)|green(n2,n3),inference(resolution,[status(thm)],[c57976, c2])).
% 164.78/165.05 cnf(c79800,plain,goal|green(n5,n6)|~green(n1,n2)|green(n2,n6),inference(resolution,[status(thm)],[c79296, c1377])).
% 164.78/165.05 cnf(c80167,plain,goal|green(n5,n6)|green(n2,n6)|green(n2,n3),inference(resolution,[status(thm)],[c79800, c57985])).
% 164.78/165.05 cnf(c89599,plain,goal|green(n2,n6)|green(n2,n3)|~green(n3,n5),inference(resolution,[status(thm)],[c80167, c1308])).
% 164.78/165.05 cnf(c95039,plain,goal|green(n2,n6)|green(n2,n3)|green(n3,n4),inference(resolution,[status(thm)],[c89599, c26345])).
% 164.78/165.05 cnf(c103667,plain,green(n2,n6)|green(n2,n3)|green(n3,n4),inference(resolution,[status(thm)],[c95039, c2])).
% 164.78/165.05 cnf(c1007,plain,green(n1,n6)|green(n2,n6)|green(n1,n2),inference(resolution,[status(thm)],[c241, c2])).
% 164.78/165.05 cnf(c3408,plain,green(n1,n6)|goal|green(n4,n6)|~green(n1,n2)|green(n2,n6),inference(resolution,[status(thm)],[c1090, c1340])).
% 164.78/165.05 cnf(c71538,plain,green(n1,n6)|goal|green(n4,n6)|green(n2,n6),inference(resolution,[status(thm)],[c3408, c1007])).
% 164.78/165.05 cnf(c71592,plain,goal|green(n4,n6)|green(n2,n6)|~green(n1,X834)|~green(X834,n6),inference(resolution,[status(thm)],[c71538, c18])).
% 164.78/165.05 cnf(c72355,plain,goal|green(n4,n6)|green(n2,n6)|~green(n1,n3),inference(resolution,[status(thm)],[c71592, c53465])).
% 164.78/165.05 cnf(c784,plain,goal|green(n3,n5)|green(n1,n3)|~green(n1,X164)|~green(X164,n5),inference(resolution,[status(thm)],[c235, c18])).
% 164.78/165.05 cnf(c2626,plain,goal|green(n3,n5)|green(n1,n3)|~green(n1,n2)|green(n2,n3),inference(resolution,[status(thm)],[c784, c563])).
% 164.78/165.05 cnf(c30271,plain,goal|green(n3,n5)|green(n1,n3)|green(n2,n3),inference(resolution,[status(thm)],[c2626, c341])).
% 164.78/165.05 cnf(c30282,plain,green(n3,n5)|green(n1,n3)|green(n2,n3),inference(resolution,[status(thm)],[c30271, c2])).
% 164.78/165.05 cnf(c95053,plain,goal|green(n2,n6)|green(n2,n3)|green(n1,n3),inference(resolution,[status(thm)],[c89599, c30282])).
% 164.78/165.05 cnf(c104223,plain,goal|green(n2,n6)|green(n2,n3)|green(n4,n6),inference(resolution,[status(thm)],[c95053, c72355])).
% 164.78/165.05 cnf(c118059,plain,goal|green(n2,n6)|green(n2,n3)|~green(n3,n4),inference(resolution,[status(thm)],[c104223, c1308])).
% 164.78/165.05 cnf(c128224,plain,goal|green(n2,n6)|green(n2,n3),inference(resolution,[status(thm)],[c118059, c103667])).
% 164.78/165.05 cnf(c128283,plain,goal|green(n2,n3)|~green(n2,X895)|~green(X895,n6),inference(resolution,[status(thm)],[c128224, c18])).
% 164.78/165.05 cnf(c2756,plain,goal|green(n2,n5)|green(n1,n2)|~green(n1,n4)|green(n2,n4),inference(resolution,[status(thm)],[c858, c600])).
% 164.78/165.05 cnf(c39941,plain,goal|green(n2,n5)|green(n1,n2)|green(n2,n4),inference(resolution,[status(thm)],[c2756, c452])).
% 164.78/165.05 cnf(c39964,plain,green(n2,n5)|green(n1,n2)|green(n2,n4),inference(resolution,[status(thm)],[c39941, c2])).
% 164.78/165.06 cnf(c95741,plain,goal|green(n4,n6)|green(n2,n4)|green(n1,n2),inference(resolution,[status(thm)],[c91504, c39964])).
% 164.78/165.06 cnf(c109849,plain,goal|green(n4,n6)|green(n2,n4)|green(n3,n6),inference(resolution,[status(thm)],[c95741, c70261])).
% 164.78/165.06 cnf(c121985,plain,goal|green(n4,n6)|green(n2,n4)|~green(n2,n3),inference(resolution,[status(thm)],[c109849, c1338])).
% 164.78/165.06 cnf(c132086,plain,goal|green(n4,n6)|green(n2,n4),inference(resolution,[status(thm)],[c121985, c108886])).
% 164.78/165.06 cnf(c132229,plain,goal|green(n4,n6)|~green(n2,X904)|~green(X904,n4),inference(resolution,[status(thm)],[c132086, c18])).
% 164.78/165.06 cnf(c151,plain,green(n1,n4)|~red(n1,n3)|goal|green(n3,n4),inference(resolution,[status(thm)],[c95, c26])).
% 164.78/165.06 cnf(c225,plain,green(n1,n4)|goal|green(n3,n4)|green(n1,n3),inference(resolution,[status(thm)],[c151, c41])).
% 164.78/165.06 cnf(c415,plain,green(n1,n4)|green(n3,n4)|green(n1,n3),inference(resolution,[status(thm)],[c225, c2])).
% 164.78/165.06 cnf(c2627,plain,goal|green(n3,n5)|green(n1,n3)|~green(n1,n4)|green(n3,n4),inference(resolution,[status(thm)],[c784, c711])).
% 164.78/165.06 cnf(c30715,plain,goal|green(n3,n5)|green(n1,n3)|green(n3,n4),inference(resolution,[status(thm)],[c2627, c415])).
% 164.78/165.06 cnf(c30765,plain,goal|green(n3,n5)|green(n3,n4)|~green(n1,X437)|~green(X437,n3),inference(resolution,[status(thm)],[c30715, c18])).
% 164.78/165.06 cnf(c31018,plain,goal|green(n3,n5)|green(n3,n4)|~green(n1,n2),inference(resolution,[status(thm)],[c30765, c26345])).
% 164.78/165.06 cnf(c31070,plain,goal|green(n3,n5)|green(n3,n4)|red(n1,n2),inference(resolution,[status(thm)],[c31018, c24])).
% 164.78/165.06 cnf(c31080,plain,green(n3,n5)|green(n3,n4)|red(n1,n2),inference(resolution,[status(thm)],[c31070, c2])).
% 164.78/165.06 cnf(c1597,plain,goal|green(n4,n6)|green(n3,n4)|~green(n3,X296)|~green(X296,n6),inference(resolution,[status(thm)],[c257, c18])).
% 164.78/165.06 cnf(c3341,plain,goal|green(n4,n6)|green(n1,n4)|~green(n1,n3)|green(n3,n4),inference(resolution,[status(thm)],[c1079, c1599])).
% 164.78/165.06 cnf(c67285,plain,goal|green(n4,n6)|green(n1,n4)|green(n3,n4),inference(resolution,[status(thm)],[c3341, c415])).
% 164.78/165.06 cnf(c67289,plain,green(n4,n6)|green(n1,n4)|green(n3,n4),inference(resolution,[status(thm)],[c67285, c2])).
% 164.78/165.06 cnf(c80202,plain,goal|green(n5,n6)|green(n4,n6)|green(n3,n4),inference(resolution,[status(thm)],[c79802, c67289])).
% 164.78/165.06 cnf(c91099,plain,goal|green(n4,n6)|green(n3,n4)|~green(n3,n5),inference(resolution,[status(thm)],[c80202, c1597])).
% 164.78/165.06 cnf(c95321,plain,goal|green(n4,n6)|green(n3,n4)|red(n1,n2),inference(resolution,[status(thm)],[c91099, c31080])).
% 164.78/165.06 cnf(c107268,plain,green(n4,n6)|green(n3,n4)|red(n1,n2),inference(resolution,[status(thm)],[c95321, c2])).
% 164.78/165.06 cnf(c104,plain,red(n1,n6)|~green(n1,X73)|~green(X73,n6)|goal,inference(resolution,[status(thm)],[c61, c18])).
% 164.78/165.06 cnf(c1595,plain,goal|green(n4,n6)|green(n3,n4)|red(n1,n6)|~green(n1,n3),inference(resolution,[status(thm)],[c257, c104])).
% 164.78/165.06 cnf(c30721,plain,green(n3,n5)|green(n1,n3)|green(n3,n4),inference(resolution,[status(thm)],[c30715, c2])).
% 164.78/165.06 cnf(c95322,plain,goal|green(n4,n6)|green(n3,n4)|green(n1,n3),inference(resolution,[status(thm)],[c91099, c30721])).
% 164.78/165.06 cnf(c107788,plain,goal|green(n4,n6)|green(n3,n4)|red(n1,n6),inference(resolution,[status(thm)],[c95322, c1595])).
% 164.78/165.06 cnf(c119821,plain,goal|green(n3,n4)|red(n1,n6)|~green(n1,n4),inference(resolution,[status(thm)],[c107788, c104])).
% 164.78/165.06 cnf(c1602,plain,green(n3,n6)|goal|green(n3,n4)|red(n1,n6)|~green(n1,n4),inference(resolution,[status(thm)],[c257, c104])).
% 164.78/165.06 cnf(c821,plain,goal|green(n4,n5)|green(n1,n4)|~green(n1,X170)|~green(X170,n5),inference(resolution,[status(thm)],[c236, c18])).
% 164.78/165.06 cnf(c2688,plain,goal|green(n4,n5)|green(n1,n4)|~green(n1,n3)|green(n3,n4),inference(resolution,[status(thm)],[c821, c711])).
% 164.78/165.06 cnf(c34003,plain,goal|green(n4,n5)|green(n1,n4)|green(n3,n4),inference(resolution,[status(thm)],[c2688, c415])).
% 164.78/165.06 cnf(c34006,plain,green(n4,n5)|green(n1,n4)|green(n3,n4),inference(resolution,[status(thm)],[c34003, c2])).
% 164.78/165.06 cnf(c1604,plain,green(n3,n6)|goal|green(n3,n4)|~green(n4,X297)|~green(X297,n6),inference(resolution,[status(thm)],[c257, c18])).
% 164.78/165.06 cnf(c3210,plain,goal|green(n3,n6)|green(n1,n3)|~green(n1,n4)|green(n3,n4),inference(resolution,[status(thm)],[c1042, c1599])).
% 164.78/165.06 cnf(c60791,plain,goal|green(n3,n6)|green(n1,n3)|green(n3,n4),inference(resolution,[status(thm)],[c3210, c415])).
% 164.78/165.06 cnf(c60799,plain,green(n3,n6)|green(n1,n3)|green(n3,n4),inference(resolution,[status(thm)],[c60791, c2])).
% 164.78/165.06 cnf(c80129,plain,goal|green(n5,n6)|green(n3,n6)|green(n3,n4),inference(resolution,[status(thm)],[c79738, c60799])).
% 164.78/165.06 cnf(c87624,plain,goal|green(n3,n6)|green(n3,n4)|~green(n4,n5),inference(resolution,[status(thm)],[c80129, c1604])).
% 164.78/165.06 cnf(c94377,plain,goal|green(n3,n6)|green(n3,n4)|green(n1,n4),inference(resolution,[status(thm)],[c87624, c34006])).
% 164.78/165.06 cnf(c96423,plain,goal|green(n3,n6)|green(n3,n4)|red(n1,n6),inference(resolution,[status(thm)],[c94377, c1602])).
% 164.78/165.06 cnf(c112126,plain,goal|green(n3,n4)|red(n1,n6)|~green(n1,n3),inference(resolution,[status(thm)],[c96423, c104])).
% 164.78/165.06 cnf(c123195,plain,goal|green(n3,n4)|red(n1,n6)|green(n1,n4),inference(resolution,[status(thm)],[c112126, c415])).
% 164.78/165.06 cnf(c135171,plain,goal|green(n3,n4)|red(n1,n6),inference(resolution,[status(thm)],[c123195, c119821])).
% 164.78/165.06 cnf(c135315,plain,goal|green(n3,n4)|~red(n1,X908)|~red(X908,n6),inference(resolution,[status(thm)],[c135171, c23])).
% 164.78/165.06 cnf(c106,plain,red(n2,n6)|~green(n2,X75)|~green(X75,n6)|goal,inference(resolution,[status(thm)],[c65, c18])).
% 164.78/165.06 cnf(c1596,plain,goal|green(n4,n6)|green(n3,n4)|red(n2,n6)|~green(n2,n3),inference(resolution,[status(thm)],[c257, c106])).
% 164.78/165.06 cnf(c95309,plain,goal|green(n4,n6)|green(n3,n4)|green(n2,n3),inference(resolution,[status(thm)],[c91099, c26345])).
% 164.78/165.06 cnf(c106599,plain,goal|green(n4,n6)|green(n3,n4)|red(n2,n6),inference(resolution,[status(thm)],[c95309, c1596])).
% 164.78/165.06 cnf(c119012,plain,goal|green(n3,n4)|red(n2,n6)|~green(n2,n4),inference(resolution,[status(thm)],[c106599, c106])).
% 164.78/165.06 cnf(c1603,plain,green(n3,n6)|goal|green(n3,n4)|red(n2,n6)|~green(n2,n4),inference(resolution,[status(thm)],[c257, c106])).
% 164.78/165.06 cnf(c599,plain,goal|green(n4,n5)|green(n2,n4)|~green(n2,X134)|~green(X134,n5),inference(resolution,[status(thm)],[c230, c18])).
% 164.78/165.06 cnf(c2312,plain,goal|green(n4,n5)|green(n2,n4)|~green(n2,n3)|green(n3,n4),inference(resolution,[status(thm)],[c599, c711])).
% 164.78/165.06 cnf(c27413,plain,goal|green(n4,n5)|green(n2,n4)|green(n3,n4),inference(resolution,[status(thm)],[c2312, c267])).
% 164.78/165.06 cnf(c27423,plain,green(n4,n5)|green(n2,n4)|green(n3,n4),inference(resolution,[status(thm)],[c27413, c2])).
% 164.78/165.06 cnf(c94387,plain,goal|green(n3,n6)|green(n3,n4)|green(n2,n4),inference(resolution,[status(thm)],[c87624, c27423])).
% 164.78/165.06 cnf(c97783,plain,goal|green(n3,n6)|green(n3,n4)|red(n2,n6),inference(resolution,[status(thm)],[c94387, c1603])).
% 164.78/165.06 cnf(c113206,plain,goal|green(n3,n4)|red(n2,n6)|~green(n2,n3),inference(resolution,[status(thm)],[c97783, c106])).
% 164.78/165.06 cnf(c123979,plain,goal|green(n3,n4)|red(n2,n6)|green(n2,n4),inference(resolution,[status(thm)],[c113206, c267])).
% 164.78/165.06 cnf(c136233,plain,goal|green(n3,n4)|red(n2,n6),inference(resolution,[status(thm)],[c123979, c119012])).
% 164.78/165.06 cnf(c136377,plain,goal|green(n3,n4)|~red(n1,n2),inference(resolution,[status(thm)],[c136233, c135315])).
% 164.78/165.06 cnf(c136488,plain,goal|green(n3,n4)|green(n4,n6),inference(resolution,[status(thm)],[c136377, c107268])).
% 164.78/165.06 cnf(c136570,plain,goal|green(n4,n6)|~green(n2,n3),inference(resolution,[status(thm)],[c136488, c132229])).
% 164.78/165.06 cnf(c137854,plain,goal|green(n4,n6)|red(n2,n3),inference(resolution,[status(thm)],[c136570, c25])).
% 164.78/165.06 cnf(c137857,plain,green(n4,n6)|red(n2,n3),inference(resolution,[status(thm)],[c137854, c2])).
% 164.78/165.06 cnf(c125204,plain,green(n3,n6)|green(n2,n3),inference(resolution,[status(thm)],[c125156, c2])).
% 164.78/165.06 cnf(c137855,plain,goal|green(n4,n6)|green(n3,n6),inference(resolution,[status(thm)],[c136570, c125204])).
% 164.78/165.06 cnf(c138151,plain,goal|green(n4,n6)|~green(n3,X940)|~green(X940,n6),inference(resolution,[status(thm)],[c137855, c18])).
% 164.78/165.06 cnf(c80186,plain,goal|green(n5,n6)|green(n4,n6)|red(n1,n4),inference(resolution,[status(thm)],[c79802, c44])).
% 164.78/165.06 cnf(c90314,plain,green(n5,n6)|green(n4,n6)|red(n1,n4),inference(resolution,[status(thm)],[c80186, c2])).
% 164.78/165.06 cnf(c1306,plain,green(n2,n6)|goal|green(n2,n3)|red(n1,n6)|~green(n1,n3),inference(resolution,[status(thm)],[c249, c104])).
% 164.78/165.06 cnf(c104225,plain,goal|green(n2,n6)|green(n2,n3)|red(n1,n6),inference(resolution,[status(thm)],[c95053, c1306])).
% 164.78/165.06 cnf(c118307,plain,goal|green(n2,n3)|red(n1,n6)|~green(n1,n2),inference(resolution,[status(thm)],[c104225, c104])).
% 164.78/165.06 cnf(c1299,plain,goal|green(n3,n6)|green(n2,n3)|red(n1,n6)|~green(n1,n2),inference(resolution,[status(thm)],[c249, c104])).
% 164.78/165.06 cnf(c100149,plain,goal|green(n3,n6)|green(n2,n3)|red(n1,n6),inference(resolution,[status(thm)],[c94583, c1299])).
% 164.78/165.06 cnf(c115158,plain,goal|green(n2,n3)|red(n1,n6)|~green(n1,n3),inference(resolution,[status(thm)],[c100149, c104])).
% 164.78/165.06 cnf(c125760,plain,goal|green(n2,n3)|red(n1,n6)|green(n1,n2),inference(resolution,[status(thm)],[c115158, c341])).
% 164.78/165.06 cnf(c143285,plain,goal|green(n2,n3)|red(n1,n6),inference(resolution,[status(thm)],[c125760, c118307])).
% 164.78/165.06 cnf(c143327,plain,goal|red(n1,n6)|green(n4,n6),inference(resolution,[status(thm)],[c143285, c136570])).
% 164.78/165.06 cnf(c143478,plain,goal|green(n4,n6)|~red(n1,X951)|~red(X951,n6),inference(resolution,[status(thm)],[c143327, c23])).
% 164.78/165.06 cnf(c144004,plain,goal|green(n4,n6)|~red(n1,n4),inference(resolution,[status(thm)],[c143478, c67])).
% 164.78/165.06 cnf(c144128,plain,goal|green(n4,n6)|green(n5,n6),inference(resolution,[status(thm)],[c144004, c90314])).
% 164.78/165.06 cnf(c144419,plain,goal|green(n4,n6)|~green(n3,n5),inference(resolution,[status(thm)],[c144128, c138151])).
% 164.78/165.06 cnf(c144583,plain,goal|green(n4,n6)|red(n3,n5),inference(resolution,[status(thm)],[c144419, c53])).
% 164.78/165.06 cnf(c144815,plain,green(n4,n6)|red(n3,n5),inference(resolution,[status(thm)],[c144583, c2])).
% 164.78/165.06 cnf(c128232,plain,green(n2,n6)|green(n2,n3),inference(resolution,[status(thm)],[c128224, c2])).
% 164.78/165.06 cnf(c1350,plain,green(n2,n6)|goal|green(n4,n6)|~green(n2,X256)|~green(X256,n4),inference(resolution,[status(thm)],[c250, c18])).
% 164.78/165.06 cnf(c107813,plain,goal|green(n4,n6)|green(n3,n4)|green(n2,n6),inference(resolution,[status(thm)],[c95322, c72355])).
% 164.78/165.06 cnf(c120207,plain,goal|green(n4,n6)|green(n2,n6)|~green(n2,n3),inference(resolution,[status(thm)],[c107813, c1350])).
% 164.78/165.06 cnf(c130043,plain,goal|green(n4,n6)|green(n2,n6),inference(resolution,[status(thm)],[c120207, c128232])).
% 164.78/165.06 cnf(c130164,plain,goal|green(n4,n6)|~green(n2,X900)|~green(X900,n6),inference(resolution,[status(thm)],[c130043, c18])).
% 164.78/165.06 cnf(c144412,plain,goal|green(n4,n6)|~green(n2,n5),inference(resolution,[status(thm)],[c144128, c130164])).
% 164.78/165.06 cnf(c144538,plain,goal|green(n4,n6)|red(n2,n5),inference(resolution,[status(thm)],[c144412, c51])).
% 164.78/165.06 cnf(c144650,plain,goal|green(n4,n6)|~red(n2,X968)|~red(X968,n5),inference(resolution,[status(thm)],[c144538, c23])).
% 164.78/165.06 cnf(c146493,plain,goal|green(n4,n6)|~red(n2,n3),inference(resolution,[status(thm)],[c144650, c144815])).
% 164.78/165.06 cnf(c146532,plain,goal|green(n4,n6),inference(resolution,[status(thm)],[c146493, c137857])).
% 164.78/165.06 cnf(c146581,plain,goal|green(n2,n3)|~green(n2,n4),inference(resolution,[status(thm)],[c146532, c128283])).
% 164.78/165.06 cnf(c146860,plain,goal|green(n2,n3),inference(resolution,[status(thm)],[c146581, c142172])).
% 164.78/165.06 cnf(c146886,plain,green(n2,n3),inference(resolution,[status(thm)],[c146860, c2])).
% 164.78/165.06 cnf(c34080,plain,goal|green(n4,n5)|green(n3,n4)|~green(n1,X479)|~green(X479,n4),inference(resolution,[status(thm)],[c34003, c18])).
% 164.78/165.06 cnf(c34672,plain,goal|green(n4,n5)|green(n3,n4)|~green(n1,n2),inference(resolution,[status(thm)],[c34080, c27423])).
% 164.78/165.06 cnf(c34712,plain,goal|green(n4,n5)|green(n3,n4)|red(n1,n2),inference(resolution,[status(thm)],[c34672, c24])).
% 164.78/165.06 cnf(c34722,plain,green(n4,n5)|green(n3,n4)|red(n1,n2),inference(resolution,[status(thm)],[c34712, c2])).
% 164.78/165.06 cnf(c136512,plain,goal|green(n3,n4)|green(n4,n5),inference(resolution,[status(thm)],[c136377, c34722])).
% 164.78/165.06 cnf(c137295,plain,green(n3,n4)|green(n4,n5),inference(resolution,[status(thm)],[c136512, c2])).
% 164.78/165.06 cnf(c79160,plain,green(n5,n6)|green(n1,n5),inference(resolution,[status(thm)],[c79148, c2])).
% 164.78/165.06 cnf(c146589,plain,goal|~green(n4,X969)|~green(X969,n6),inference(resolution,[status(thm)],[c146532, c18])).
% 164.78/165.06 cnf(c146726,plain,goal|~green(n4,n5)|green(n1,n5),inference(resolution,[status(thm)],[c146589, c79160])).
% 164.78/165.06 cnf(c831,plain,green(n1,n5)|goal|green(n4,n5)|~green(n1,X172)|~green(X172,n4),inference(resolution,[status(thm)],[c236, c18])).
% 164.78/165.06 cnf(c2721,plain,green(n1,n5)|goal|green(n4,n5)|~green(n1,n2)|green(n2,n5),inference(resolution,[status(thm)],[c831, c600])).
% 164.78/165.06 cnf(c35468,plain,green(n1,n5)|goal|green(n4,n5)|green(n2,n5),inference(resolution,[status(thm)],[c2721, c859])).
% 164.78/165.06 cnf(c35608,plain,green(n1,n5)|goal|green(n4,n5)|~green(n2,X498)|~green(X498,n5),inference(resolution,[status(thm)],[c35468, c18])).
% 164.78/165.06 cnf(c2742,plain,green(n1,n5)|goal|green(n4,n5)|~green(n1,n3)|green(n3,n5),inference(resolution,[status(thm)],[c831, c711])).
% 164.78/165.06 cnf(c37548,plain,green(n1,n5)|goal|green(n4,n5)|green(n3,n5),inference(resolution,[status(thm)],[c2742, c785])).
% 164.78/165.06 cnf(c37711,plain,green(n1,n5)|goal|green(n4,n5)|~green(n2,n3),inference(resolution,[status(thm)],[c37548, c35608])).
% 164.78/165.06 cnf(c146907,plain,goal|green(n1,n5)|green(n4,n5),inference(resolution,[status(thm)],[c146860, c37711])).
% 164.78/165.06 cnf(c148392,plain,goal|green(n1,n5),inference(resolution,[status(thm)],[c146907, c146726])).
% 164.78/165.06 cnf(c148446,plain,goal|~green(n1,X973)|~green(X973,n5),inference(resolution,[status(thm)],[c148392, c18])).
% 164.78/165.06 cnf(c148529,plain,goal|~green(n1,n4)|green(n3,n4),inference(resolution,[status(thm)],[c148446, c137295])).
% 164.78/165.06 cnf(c136513,plain,goal|green(n3,n4)|green(n1,n2),inference(resolution,[status(thm)],[c136377, c24])).
% 164.78/165.06 cnf(c137578,plain,green(n3,n4)|green(n1,n2),inference(resolution,[status(thm)],[c136513, c2])).
% 164.78/165.06 cnf(c94,plain,red(n1,n3)|~green(n1,X63)|~green(X63,n3)|goal,inference(resolution,[status(thm)],[c41, c18])).
% 164.78/165.06 cnf(c146891,plain,goal|red(n1,n3)|~green(n1,n2),inference(resolution,[status(thm)],[c146860, c94])).
% 164.78/165.06 cnf(c148089,plain,goal|red(n1,n3)|green(n3,n4),inference(resolution,[status(thm)],[c146891, c137578])).
% 164.78/165.06 cnf(c149508,plain,goal|green(n3,n4)|green(n1,n4),inference(resolution,[status(thm)],[c148089, c151])).
% 164.78/165.06 cnf(c150549,plain,goal|green(n3,n4),inference(resolution,[status(thm)],[c149508, c148529])).
% 164.78/165.06 cnf(c150588,plain,goal|red(n2,n4)|~green(n2,n3),inference(resolution,[status(thm)],[c150549, c90])).
% 164.78/165.06 cnf(c151484,plain,goal|red(n2,n4),inference(resolution,[status(thm)],[c150588, c146886])).
% 164.78/165.06 cnf(c151485,plain,red(n2,n4),inference(resolution,[status(thm)],[c151484, c2])).
% 164.78/165.06 cnf(c100,plain,red(n3,n5)|~green(n3,X69)|~green(X69,n5)|goal,inference(resolution,[status(thm)],[c53, c18])).
% 164.78/165.06 cnf(c170,plain,red(n3,n5)|~green(n3,n4)|goal|red(n4,n5),inference(resolution,[status(thm)],[c100, c27])).
% 164.78/165.06 cnf(c150576,plain,goal|red(n3,n5)|red(n4,n5),inference(resolution,[status(thm)],[c150549, c170])).
% 164.78/165.06 cnf(c151303,plain,red(n3,n5)|red(n4,n5),inference(resolution,[status(thm)],[c150576, c2])).
% 164.78/165.06 cnf(c146674,plain,goal|~green(n4,n5)|red(n5,n6),inference(resolution,[status(thm)],[c146589, c28])).
% 164.78/165.06 cnf(c147003,plain,goal|red(n5,n6)|red(n4,n5),inference(resolution,[status(thm)],[c146674, c27])).
% 164.78/165.06 cnf(c149131,plain,red(n5,n6)|red(n4,n5),inference(resolution,[status(thm)],[c147003, c2])).
% 164.78/165.06 cnf(c111,plain,red(n3,n6)|~green(n3,X79)|~green(X79,n6)|goal,inference(resolution,[status(thm)],[c69, c18])).
% 164.78/165.06 cnf(c146574,plain,goal|red(n3,n6)|~green(n3,n4),inference(resolution,[status(thm)],[c146532, c111])).
% 164.78/165.06 cnf(c150569,plain,goal|red(n3,n6),inference(resolution,[status(thm)],[c150549, c146574])).
% 164.78/165.06 cnf(c150628,plain,goal|~red(n3,X977)|~red(X977,n6),inference(resolution,[status(thm)],[c150569, c23])).
% 164.78/165.06 cnf(c150711,plain,goal|~red(n3,n5)|red(n4,n5),inference(resolution,[status(thm)],[c150628, c149131])).
% 164.78/165.06 cnf(c151610,plain,goal|red(n4,n5),inference(resolution,[status(thm)],[c150711, c151303])).
% 164.78/165.06 cnf(c151616,plain,red(n4,n5),inference(resolution,[status(thm)],[c151610, c2])).
% 164.78/165.06 cnf(c148522,plain,goal|~green(n1,n2)|red(n2,n5),inference(resolution,[status(thm)],[c148446, c51])).
% 164.78/165.06 cnf(c150137,plain,goal|red(n2,n5)|red(n1,n2),inference(resolution,[status(thm)],[c148522, c24])).
% 164.78/165.06 cnf(c150898,plain,red(n2,n5)|red(n1,n2),inference(resolution,[status(thm)],[c150137, c2])).
% 164.78/165.06 cnf(c143539,plain,goal|red(n1,n6)|~green(n1,n4),inference(resolution,[status(thm)],[c143327, c104])).
% 164.78/165.06 cnf(c143633,plain,goal|red(n1,n6)|red(n1,n4),inference(resolution,[status(thm)],[c143539, c44])).
% 164.78/165.06 cnf(c143669,plain,goal|red(n1,n4)|~red(n1,X955)|~red(X955,n6),inference(resolution,[status(thm)],[c143633, c23])).
% 164.78/165.06 cnf(c150625,plain,goal|red(n1,n4)|~red(n1,n3),inference(resolution,[status(thm)],[c150569, c143669])).
% 164.78/165.06 cnf(c96,plain,red(n1,n4)|~green(n1,X65)|~green(X65,n4)|goal,inference(resolution,[status(thm)],[c44, c18])).
% 164.78/165.06 cnf(c150589,plain,goal|red(n1,n4)|~green(n1,n3),inference(resolution,[status(thm)],[c150549, c96])).
% 164.78/165.06 cnf(c151571,plain,goal|red(n1,n4)|red(n1,n3),inference(resolution,[status(thm)],[c150589, c41])).
% 164.78/165.06 cnf(c151961,plain,goal|red(n1,n4),inference(resolution,[status(thm)],[c151571, c150625])).
% 164.78/165.06 cnf(c151975,plain,goal|~red(n1,X983)|~red(X983,n4),inference(resolution,[status(thm)],[c151961, c23])).
% 164.78/165.06 cnf(c151995,plain,goal|~red(n1,n2),inference(resolution,[status(thm)],[c151975, c151485])).
% 164.78/165.06 cnf(c152005,plain,goal|red(n2,n5),inference(resolution,[status(thm)],[c151995, c150898])).
% 164.78/165.06 cnf(c152034,plain,goal|~red(n2,X987)|~red(X987,n5),inference(resolution,[status(thm)],[c152005, c23])).
% 164.78/165.06 cnf(c152131,plain,goal|~red(n2,n4),inference(resolution,[status(thm)],[c152034, c151616])).
% 164.78/165.06 cnf(c152135,plain,goal,inference(resolution,[status(thm)],[c152131, c151485])).
% 164.78/165.06 cnf(c152136,plain,$false,inference(resolution,[status(thm)],[c152135, c2])).
% 164.78/165.06 % SZS output end CNFRefutation
% 164.78/165.06
% 164.78/165.06 % Initial clauses : 10
% 164.78/165.06 % Processed clauses : 2293
% 164.78/165.06 % Factors computed : 7
% 164.78/165.06 % Resolvents computed: 152106
% 164.78/165.06 % Tautologies deleted: 240
% 164.78/165.06 % Forward subsumed : 2821
% 164.78/165.06 % Backward subsumed : 2221
% 164.78/165.06 % -------- CPU Time ---------
% 164.78/165.06 % User time : 164.202 s
% 164.78/165.06 % System time : 0.422 s
% 164.78/165.06 % Total time : 164.624 s
%------------------------------------------------------------------------------