%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO580+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:20 EDT 2024
% Result : Theorem 23.25s 23.41s
% Output : Refutation 23.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO580+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n016.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 9 07:48:53 EDT 2024
% 0.19/0.33 % CPUTime :
% 23.25/23.41 % Version: 1.5
% 23.25/23.41 % SZS status Theorem
% 23.25/23.41 % SZS output start CNFRefutation
% 23.25/23.41 fof(exemplo6GDDFULL416042,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:((((((((((eqangle(D,A,A,B,D,A,A,C)&eqangle(D,B,B,C,D,B,B,A))&eqangle(D,C,C,A,D,C,C,B))&perp(E,A,B,C))&coll(E,B,C))&perp(F,B,A,D))&coll(F,A,D))&perp(G,C,A,D))&coll(G,A,D))&midp(H,C,B))=>cyclic(E,F,G,H)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL416042)).
% 23.25/23.41 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:((((((((((eqangle(D,A,A,B,D,A,A,C)&eqangle(D,B,B,C,D,B,B,A))&eqangle(D,C,C,A,D,C,C,B))&perp(E,A,B,C))&coll(E,B,C))&perp(F,B,A,D))&coll(F,A,D))&perp(G,C,A,D))&coll(G,A,D))&midp(H,C,B))=>cyclic(E,F,G,H))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416042])).
% 23.25/23.41 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:((((((((((eqangle(D,A,A,B,D,A,A,C)&eqangle(D,B,B,C,D,B,B,A))&eqangle(D,C,C,A,D,C,C,B))&perp(E,A,B,C))&coll(E,B,C))&perp(F,B,A,D))&coll(F,A,D))&perp(G,C,A,D))&coll(G,A,D))&midp(H,C,B))&~cyclic(E,F,G,H)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 23.25/23.41 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((((eqangle(X5,X2,X2,X3,X5,X2,X2,X4)&eqangle(X5,X3,X3,X4,X5,X3,X3,X2))&eqangle(X5,X4,X4,X2,X5,X4,X4,X3))&perp(X6,X2,X3,X4))&coll(X6,X3,X4))&perp(X7,X3,X2,X5))&coll(X7,X2,X5))&perp(X8,X4,X2,X5))&coll(X8,X2,X5))&midp(X9,X4,X3))&~cyclic(X6,X7,X8,X9)))))))))),inference(variable_rename,[status(thm)],[c12])).
% 23.25/23.41 fof(c14,negated_conjecture,((((((((((eqangle(skolem0004,skolem0001,skolem0001,skolem0002,skolem0004,skolem0001,skolem0001,skolem0003)&eqangle(skolem0004,skolem0002,skolem0002,skolem0003,skolem0004,skolem0002,skolem0002,skolem0001))&eqangle(skolem0004,skolem0003,skolem0003,skolem0001,skolem0004,skolem0003,skolem0003,skolem0002))&perp(skolem0005,skolem0001,skolem0002,skolem0003))&coll(skolem0005,skolem0002,skolem0003))&perp(skolem0006,skolem0002,skolem0001,skolem0004))&coll(skolem0006,skolem0001,skolem0004))&perp(skolem0007,skolem0003,skolem0001,skolem0004))&coll(skolem0007,skolem0001,skolem0004))&midp(skolem0008,skolem0003,skolem0002))&~cyclic(skolem0005,skolem0006,skolem0007,skolem0008)),inference(skolemize,[status(esa)],[c13])).
% 23.25/23.41 cnf(c25,negated_conjecture,~cyclic(skolem0005,skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c14])).
% 23.25/23.41 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 23.25/23.41 fof(c367,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 23.25/23.41 fof(c368,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c367])).
% 23.25/23.41 cnf(c369,plain,~cyclic(X701,X700,X698,X699)|cyclic(X701,X700,X699,X698),inference(split_conjunct,[status(thm)],[c368])).
% 23.25/23.41 fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 23.25/23.41 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 23.25/23.41 fof(c362,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X464,X463,X465,X466)))))),inference(variable_rename,[status(thm)],[c361])).
% 23.25/23.41 cnf(c363,plain,~cyclic(X692,X691,X693,X690)|cyclic(X691,X692,X693,X690),inference(split_conjunct,[status(thm)],[c362])).
% 23.25/23.41 fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 23.25/23.41 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 23.25/23.41 fof(c365,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c364])).
% 23.25/23.41 cnf(c366,plain,~cyclic(X696,X694,X697,X695)|cyclic(X696,X697,X694,X695),inference(split_conjunct,[status(thm)],[c365])).
% 23.25/23.41 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 23.25/23.41 fof(c402,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 23.25/23.41 fof(c403,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c402])).
% 23.25/23.41 cnf(c404,plain,~coll(X779,X781,X782)|~coll(X779,X781,X780)|coll(X782,X780,X779),inference(split_conjunct,[status(thm)],[c403])).
% 23.25/23.41 cnf(c606,plain,~coll(X783,X785,X784)|coll(X784,X784,X783),inference(factor,[status(thm)],[c404])).
% 23.25/23.41 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 23.25/23.41 fof(c191,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 23.25/23.41 fof(c192,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c191])).
% 23.25/23.41 cnf(c193,plain,~para(X664,X666,X664,X665)|coll(X664,X666,X665),inference(split_conjunct,[status(thm)],[c192])).
% 23.25/23.41 fof(ruleD39,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(eqangle(A,B,P,Q,C,D,P,Q)=>para(A,B,C,D)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 23.25/23.41 fof(c288,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~eqangle(A,B,P,Q,C,D,P,Q)|para(A,B,C,D)))))))),inference(fof_nnf,[status(thm)],[ruleD39])).
% 23.25/23.41 fof(c289,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:~eqangle(A,B,P,Q,C,D,P,Q)))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c288])).
% 23.25/23.41 fof(c291,plain,(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)|para(X296,X297,X298,X299)))))))),inference(shift_quantors,[status(thm)],[fof(c290,plain,(![X296]:(![X297]:(![X298]:(![X299]:((![X300]:(![X301]:~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))|para(X296,X297,X298,X299)))))),inference(variable_rename,[status(thm)],[c289])).])).
% 23.25/23.41 cnf(c292,plain,~eqangle(X1068,X1071,X1072,X1069,X1070,X1067,X1072,X1069)|para(X1068,X1071,X1070,X1067),inference(split_conjunct,[status(thm)],[c291])).
% 23.25/23.41 fof(ruleD19,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(C,D,A,B,U,V,P,Q)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 23.25/23.41 fof(c352,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(C,D,A,B,U,V,P,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleD19])).
% 23.25/23.41 fof(c353,plain,(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(~eqangle(X442,X443,X444,X445,X446,X447,X448,X449)|eqangle(X444,X445,X442,X443,X448,X449,X446,X447)))))))))),inference(variable_rename,[status(thm)],[c352])).
% 23.25/23.41 cnf(c354,plain,~eqangle(X1216,X1219,X1221,X1218,X1217,X1222,X1223,X1220)|eqangle(X1221,X1218,X1216,X1219,X1223,X1220,X1217,X1222),inference(split_conjunct,[status(thm)],[c353])).
% 23.25/23.41 fof(ruleD40,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(para(A,B,C,D)=>eqangle(A,B,P,Q,C,D,P,Q)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 23.25/23.41 fof(c283,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~para(A,B,C,D)|eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD40])).
% 23.25/23.41 fof(c284,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|(![P]:(![Q]:eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(shift_quantors,[status(thm)],[c283])).
% 23.25/23.41 fof(c286,plain,(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(~para(X290,X291,X292,X293)|eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(shift_quantors,[status(thm)],[fof(c285,plain,(![X290]:(![X291]:(![X292]:(![X293]:(~para(X290,X291,X292,X293)|(![X294]:(![X295]:eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(variable_rename,[status(thm)],[c284])).])).
% 23.25/23.41 cnf(c287,plain,~para(X1063,X1065,X1066,X1064)|eqangle(X1063,X1065,X1061,X1062,X1066,X1064,X1061,X1062),inference(split_conjunct,[status(thm)],[c286])).
% 23.25/23.41 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 23.25/23.41 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 23.25/23.41 fof(c400,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c399])).
% 23.25/23.41 cnf(c401,plain,~para(X772,X769,X771,X770)|para(X772,X769,X770,X771),inference(split_conjunct,[status(thm)],[c400])).
% 23.25/23.41 cnf(c24,negated_conjecture,midp(skolem0008,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 23.25/23.41 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 23.25/23.41 fof(c378,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 23.25/23.41 fof(c379,plain,(![X484]:(![X485]:(![X486]:(~midp(X486,X485,X484)|midp(X486,X484,X485))))),inference(variable_rename,[status(thm)],[c378])).
% 23.25/23.41 cnf(c380,plain,~midp(X560,X559,X558)|midp(X560,X558,X559),inference(split_conjunct,[status(thm)],[c379])).
% 23.25/23.41 cnf(c419,plain,midp(skolem0008,skolem0002,skolem0003),inference(resolution,[status(thm)],[c380, c24])).
% 23.25/23.41 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 23.25/23.41 fof(c200,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 23.25/23.41 fof(c201,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c200])).
% 23.25/23.41 fof(c203,plain,(![X177]:(![X178]:(![X179]:(![X180]:(![X181]:((~midp(X181,X177,X178)|~midp(X181,X179,X180))|para(X177,X179,X178,X180))))))),inference(shift_quantors,[status(thm)],[fof(c202,plain,(![X177]:(![X178]:(![X179]:(![X180]:((![X181]:(~midp(X181,X177,X178)|~midp(X181,X179,X180)))|para(X177,X179,X178,X180)))))),inference(variable_rename,[status(thm)],[c201])).])).
% 23.25/23.41 cnf(c204,plain,~midp(X950,X949,X947)|~midp(X950,X948,X951)|para(X949,X948,X947,X951),inference(split_conjunct,[status(thm)],[c203])).
% 23.25/23.41 cnf(c1216,plain,~midp(skolem0008,X1639,X1638)|para(X1639,skolem0003,X1638,skolem0002),inference(resolution,[status(thm)],[c204, c24])).
% 23.25/23.41 cnf(c2136,plain,para(skolem0002,skolem0003,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1216, c419])).
% 23.25/23.41 cnf(c2148,plain,para(skolem0002,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c2136, c401])).
% 23.25/23.41 cnf(c2159,plain,eqangle(skolem0002,skolem0003,X1715,X1714,skolem0002,skolem0003,X1715,X1714),inference(resolution,[status(thm)],[c2148, c287])).
% 23.25/23.41 cnf(c2425,plain,eqangle(X1796,X1797,skolem0002,skolem0003,X1796,X1797,skolem0002,skolem0003),inference(resolution,[status(thm)],[c2159, c354])).
% 23.25/23.41 cnf(c2600,plain,para(X1798,X1799,X1798,X1799),inference(resolution,[status(thm)],[c2425, c292])).
% 23.25/23.41 cnf(c2623,plain,coll(X1800,X1801,X1801),inference(resolution,[status(thm)],[c2600, c193])).
% 23.25/23.41 cnf(c2712,plain,coll(X1806,X1806,X1807),inference(resolution,[status(thm)],[c2623, c606])).
% 23.25/23.41 cnf(c2846,plain,~coll(X2347,X2347,X2346)|coll(X2346,X2345,X2347),inference(resolution,[status(thm)],[c2712, c404])).
% 23.25/23.41 cnf(c4057,plain,coll(X2357,X2356,X2358),inference(resolution,[status(thm)],[c2846, c2712])).
% 23.25/23.41 fof(ruleD42b,axiom,(![A]:(![B]:(![P]:(![Q]:((eqangle(P,A,P,B,Q,A,Q,B)&coll(P,Q,B))=>cyclic(A,B,P,Q)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 23.25/23.41 fof(c273,plain,(![A]:(![B]:(![P]:(![Q]:((~eqangle(P,A,P,B,Q,A,Q,B)|~coll(P,Q,B))|cyclic(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD42b])).
% 23.25/23.41 fof(c274,plain,(![X278]:(![X279]:(![X280]:(![X281]:((~eqangle(X280,X278,X280,X279,X281,X278,X281,X279)|~coll(X280,X281,X279))|cyclic(X278,X279,X280,X281)))))),inference(variable_rename,[status(thm)],[c273])).
% 23.25/23.41 cnf(c275,plain,~eqangle(X1049,X1050,X1049,X1052,X1051,X1050,X1051,X1052)|~coll(X1049,X1051,X1052)|cyclic(X1050,X1052,X1049,X1051),inference(split_conjunct,[status(thm)],[c274])).
% 23.25/23.41 cnf(c2622,plain,eqangle(X2196,X2198,X2197,X2195,X2196,X2198,X2197,X2195),inference(resolution,[status(thm)],[c2600, c287])).
% 23.25/23.41 cnf(c3807,plain,~coll(X2616,X2616,X2617)|cyclic(X2618,X2617,X2616,X2616),inference(resolution,[status(thm)],[c2622, c275])).
% 23.25/23.41 cnf(c4254,plain,cyclic(X2621,X2619,X2620,X2620),inference(resolution,[status(thm)],[c3807, c4057])).
% 23.25/23.41 cnf(c4258,plain,cyclic(X2630,X2629,X2628,X2629),inference(resolution,[status(thm)],[c4254, c366])).
% 23.25/23.41 cnf(c4267,plain,cyclic(X2635,X2636,X2634,X2635),inference(resolution,[status(thm)],[c4258, c363])).
% 23.25/23.41 cnf(c4279,plain,cyclic(X2652,X2654,X2652,X2653),inference(resolution,[status(thm)],[c4267, c369])).
% 23.25/23.41 fof(ruleD17,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:((cyclic(A,B,C,D)&cyclic(A,B,C,E))=>cyclic(B,C,D,E))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD17)).
% 23.25/23.41 fof(c358,plain,(![A]:(![B]:(![C]:(![D]:(![E]:((~cyclic(A,B,C,D)|~cyclic(A,B,C,E))|cyclic(B,C,D,E))))))),inference(fof_nnf,[status(thm)],[ruleD17])).
% 23.25/23.41 fof(c359,plain,(![X458]:(![X459]:(![X460]:(![X461]:(![X462]:((~cyclic(X458,X459,X460,X461)|~cyclic(X458,X459,X460,X462))|cyclic(X459,X460,X461,X462))))))),inference(variable_rename,[status(thm)],[c358])).
% 23.25/23.41 cnf(c360,plain,~cyclic(X1235,X1233,X1234,X1236)|~cyclic(X1235,X1233,X1234,X1232)|cyclic(X1233,X1234,X1236,X1232),inference(split_conjunct,[status(thm)],[c359])).
% 23.25/23.41 cnf(c4291,plain,~cyclic(X12768,X12771,X12768,X12770)|cyclic(X12771,X12768,X12770,X12769),inference(resolution,[status(thm)],[c4279, c360])).
% 23.25/23.41 cnf(c17626,plain,cyclic(X12791,X12792,X12794,X12793),inference(resolution,[status(thm)],[c4291, c4279])).
% 23.25/23.41 cnf(c17636,plain,$false,inference(resolution,[status(thm)],[c17626, c25])).
% 23.25/23.41 % SZS output end CNFRefutation
% 23.25/23.41
% 23.25/23.41 % Initial clauses : 138
% 23.25/23.41 % Processed clauses : 1882
% 23.25/23.41 % Factors computed : 241
% 23.25/23.41 % Resolvents computed: 16986
% 23.25/23.41 % Tautologies deleted: 32
% 23.25/23.41 % Forward subsumed : 6686
% 23.25/23.41 % Backward subsumed : 1467
% 23.25/23.41 % -------- CPU Time ---------
% 23.25/23.41 % User time : 23.040 s
% 23.25/23.41 % System time : 0.039 s
% 23.25/23.41 % Total time : 23.079 s
%------------------------------------------------------------------------------