%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO595+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:22 EDT 2024
% Result : Theorem 71.03s 71.22s
% Output : Refutation 71.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO595+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.32 % Computer : n017.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu May 9 07:54:38 EDT 2024
% 0.12/0.32 % CPUTime :
% 71.03/71.22 % Version: 1.5
% 71.03/71.22 % SZS status Theorem
% 71.03/71.22 % SZS output start CNFRefutation
% 71.03/71.22 fof(exemplo6GDDFULL416057,conjecture,(![A]:(![B]:(![C]:(![D]:(![O]:(![E]:(![F]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:((((((((perp(D,A,B,C)&coll(D,B,C))&midp(O,A,D))&circle(O,D,NWPNT1,NWPNT2))&coll(E,A,B))&circle(O,D,E,NWPNT3))&coll(F,A,C))&circle(O,D,F,NWPNT4))=>cyclic(B,C,E,F))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL416057)).
% 71.03/71.22 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![O]:(![E]:(![F]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:((((((((perp(D,A,B,C)&coll(D,B,C))&midp(O,A,D))&circle(O,D,NWPNT1,NWPNT2))&coll(E,A,B))&circle(O,D,E,NWPNT3))&coll(F,A,C))&circle(O,D,F,NWPNT4))=>cyclic(B,C,E,F)))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416057])).
% 71.03/71.22 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[O]:(?[E]:(?[F]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:((((((((perp(D,A,B,C)&coll(D,B,C))&midp(O,A,D))&circle(O,D,NWPNT1,NWPNT2))&coll(E,A,B))&circle(O,D,E,NWPNT3))&coll(F,A,C))&circle(O,D,F,NWPNT4))&~cyclic(B,C,E,F))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 71.03/71.22 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[O]:(?[E]:(?[F]:((((((((perp(D,A,B,C)&coll(D,B,C))&midp(O,A,D))&(?[NWPNT1]:(?[NWPNT2]:circle(O,D,NWPNT1,NWPNT2))))&coll(E,A,B))&(?[NWPNT3]:circle(O,D,E,NWPNT3)))&coll(F,A,C))&(?[NWPNT4]:circle(O,D,F,NWPNT4)))&~cyclic(B,C,E,F))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 71.03/71.22 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((((perp(X5,X2,X3,X4)&coll(X5,X3,X4))&midp(X6,X2,X5))&(?[X9]:(?[X10]:circle(X6,X5,X9,X10))))&coll(X7,X2,X3))&(?[X11]:circle(X6,X5,X7,X11)))&coll(X8,X2,X4))&(?[X12]:circle(X6,X5,X8,X12)))&~cyclic(X3,X4,X7,X8))))))))),inference(variable_rename,[status(thm)],[c13])).
% 71.03/71.22 fof(c15,negated_conjecture,((((((((perp(skolem0004,skolem0001,skolem0002,skolem0003)&coll(skolem0004,skolem0002,skolem0003))&midp(skolem0005,skolem0001,skolem0004))&circle(skolem0005,skolem0004,skolem0008,skolem0009))&coll(skolem0006,skolem0001,skolem0002))&circle(skolem0005,skolem0004,skolem0006,skolem0010))&coll(skolem0007,skolem0001,skolem0003))&circle(skolem0005,skolem0004,skolem0007,skolem0011))&~cyclic(skolem0002,skolem0003,skolem0006,skolem0007)),inference(skolemize,[status(esa)],[c14])).
% 71.03/71.22 cnf(c24,negated_conjecture,~cyclic(skolem0002,skolem0003,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 71.03/71.22 fof(c361,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X467,X466,X468,X469)))))),inference(variable_rename,[status(thm)],[c360])).
% 71.03/71.22 cnf(c362,plain,~cyclic(X709,X706,X707,X708)|cyclic(X706,X709,X707,X708),inference(split_conjunct,[status(thm)],[c361])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c366,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 71.03/71.22 fof(c367,plain,(![X474]:(![X475]:(![X476]:(![X477]:(~cyclic(X474,X475,X476,X477)|cyclic(X474,X475,X477,X476)))))),inference(variable_rename,[status(thm)],[c366])).
% 71.03/71.22 cnf(c368,plain,~cyclic(X716,X717,X715,X714)|cyclic(X716,X717,X714,X715),inference(split_conjunct,[status(thm)],[c367])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 71.03/71.22 fof(c364,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X472,X471,X473)))))),inference(variable_rename,[status(thm)],[c363])).
% 71.03/71.22 cnf(c365,plain,~cyclic(X710,X712,X711,X713)|cyclic(X710,X711,X712,X713),inference(split_conjunct,[status(thm)],[c364])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c401,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 71.03/71.22 fof(c402,plain,(![X524]:(![X525]:(![X526]:(![X527]:((~coll(X524,X525,X526)|~coll(X524,X525,X527))|coll(X526,X527,X524)))))),inference(variable_rename,[status(thm)],[c401])).
% 71.03/71.22 cnf(c403,plain,~coll(X767,X766,X768)|~coll(X767,X766,X769)|coll(X768,X769,X767),inference(split_conjunct,[status(thm)],[c402])).
% 71.03/71.22 cnf(c551,plain,~coll(X772,X771,X770)|coll(X770,X770,X772),inference(factor,[status(thm)],[c403])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 71.03/71.22 fof(c191,plain,(![X167]:(![X168]:(![X169]:(~para(X167,X168,X167,X169)|coll(X167,X168,X169))))),inference(variable_rename,[status(thm)],[c190])).
% 71.03/71.22 cnf(c192,plain,~para(X679,X681,X679,X680)|coll(X679,X681,X680),inference(split_conjunct,[status(thm)],[c191])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c287,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])).
% 71.03/71.22 fof(c288,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)],[c287])).
% 71.03/71.22 fof(c290,plain,(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)|para(X299,X300,X301,X302)))))))),inference(shift_quantors,[status(thm)],[fof(c289,plain,(![X299]:(![X300]:(![X301]:(![X302]:((![X303]:(![X304]:~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))|para(X299,X300,X301,X302)))))),inference(variable_rename,[status(thm)],[c288])).])).
% 71.03/71.22 cnf(c291,plain,~eqangle(X1077,X1075,X1079,X1076,X1074,X1078,X1079,X1076)|para(X1077,X1075,X1074,X1078),inference(split_conjunct,[status(thm)],[c290])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c351,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])).
% 71.03/71.22 fof(c352,plain,(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(![X451]:(![X452]:(~eqangle(X445,X446,X447,X448,X449,X450,X451,X452)|eqangle(X447,X448,X445,X446,X451,X452,X449,X450)))))))))),inference(variable_rename,[status(thm)],[c351])).
% 71.03/71.22 cnf(c353,plain,~eqangle(X1243,X1242,X1241,X1238,X1239,X1237,X1240,X1236)|eqangle(X1241,X1238,X1243,X1242,X1240,X1236,X1239,X1237),inference(split_conjunct,[status(thm)],[c352])).
% 71.03/71.22 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)).
% 71.03/71.22 fof(c282,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])).
% 71.03/71.22 fof(c283,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)],[c282])).
% 71.03/71.22 fof(c285,plain,(![X293]:(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(~para(X293,X294,X295,X296)|eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c284,plain,(![X293]:(![X294]:(![X295]:(![X296]:(~para(X293,X294,X295,X296)|(![X297]:(![X298]:eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(variable_rename,[status(thm)],[c283])).])).
% 71.03/71.22 cnf(c286,plain,~para(X1072,X1068,X1070,X1067)|eqangle(X1072,X1068,X1071,X1069,X1070,X1067,X1071,X1069),inference(split_conjunct,[status(thm)],[c285])).
% 71.03/71.22 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)).
% 71.03/71.23 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 71.03/71.23 fof(c399,plain,(![X520]:(![X521]:(![X522]:(![X523]:(~para(X520,X521,X522,X523)|para(X520,X521,X523,X522)))))),inference(variable_rename,[status(thm)],[c398])).
% 71.03/71.23 cnf(c400,plain,~para(X752,X751,X753,X750)|para(X752,X751,X750,X753),inference(split_conjunct,[status(thm)],[c399])).
% 71.03/71.23 cnf(c18,negated_conjecture,midp(skolem0005,skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c15])).
% 71.03/71.23 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 71.03/71.23 fof(c377,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 71.03/71.23 fof(c378,plain,(![X487]:(![X488]:(![X489]:(~midp(X489,X488,X487)|midp(X489,X487,X488))))),inference(variable_rename,[status(thm)],[c377])).
% 71.03/71.23 cnf(c379,plain,~midp(X561,X562,X563)|midp(X561,X563,X562),inference(split_conjunct,[status(thm)],[c378])).
% 71.03/71.23 cnf(c418,plain,midp(skolem0005,skolem0004,skolem0001),inference(resolution,[status(thm)],[c379, c18])).
% 71.03/71.23 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)).
% 71.03/71.23 fof(c199,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])).
% 71.03/71.23 fof(c200,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c199])).
% 71.03/71.23 fof(c202,plain,(![X180]:(![X181]:(![X182]:(![X183]:(![X184]:((~midp(X184,X180,X181)|~midp(X184,X182,X183))|para(X180,X182,X181,X183))))))),inference(shift_quantors,[status(thm)],[fof(c201,plain,(![X180]:(![X181]:(![X182]:(![X183]:((![X184]:(~midp(X184,X180,X181)|~midp(X184,X182,X183)))|para(X180,X182,X181,X183)))))),inference(variable_rename,[status(thm)],[c200])).])).
% 71.03/71.23 cnf(c203,plain,~midp(X952,X951,X950)|~midp(X952,X953,X954)|para(X951,X953,X950,X954),inference(split_conjunct,[status(thm)],[c202])).
% 71.03/71.23 cnf(c1166,plain,~midp(skolem0005,X2044,X2043)|para(X2044,skolem0004,X2043,skolem0001),inference(resolution,[status(thm)],[c203, c418])).
% 71.03/71.23 cnf(c4411,plain,para(skolem0001,skolem0004,skolem0004,skolem0001),inference(resolution,[status(thm)],[c1166, c18])).
% 71.03/71.23 cnf(c4416,plain,para(skolem0001,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c4411, c400])).
% 71.03/71.23 cnf(c4446,plain,eqangle(skolem0001,skolem0004,X3621,X3620,skolem0001,skolem0004,X3621,X3620),inference(resolution,[status(thm)],[c4416, c286])).
% 71.03/71.23 cnf(c9369,plain,eqangle(X4062,X4061,skolem0001,skolem0004,X4062,X4061,skolem0001,skolem0004),inference(resolution,[status(thm)],[c4446, c353])).
% 71.03/71.23 cnf(c10770,plain,para(X4064,X4063,X4064,X4063),inference(resolution,[status(thm)],[c9369, c291])).
% 71.03/71.23 cnf(c10802,plain,coll(X4065,X4066,X4066),inference(resolution,[status(thm)],[c10770, c192])).
% 71.03/71.23 cnf(c10886,plain,coll(X4068,X4068,X4067),inference(resolution,[status(thm)],[c10802, c551])).
% 71.03/71.23 cnf(c11222,plain,~coll(X5769,X5769,X5767)|coll(X5767,X5768,X5769),inference(resolution,[status(thm)],[c10886, c403])).
% 71.03/71.23 cnf(c20075,plain,coll(X5773,X5772,X5774),inference(resolution,[status(thm)],[c11222, c10886])).
% 71.03/71.23 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)).
% 71.03/71.23 fof(c272,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])).
% 71.03/71.23 fof(c273,plain,(![X281]:(![X282]:(![X283]:(![X284]:((~eqangle(X283,X281,X283,X282,X284,X281,X284,X282)|~coll(X283,X284,X282))|cyclic(X281,X282,X283,X284)))))),inference(variable_rename,[status(thm)],[c272])).
% 71.03/71.23 cnf(c274,plain,~eqangle(X1053,X1051,X1053,X1052,X1054,X1051,X1054,X1052)|~coll(X1053,X1054,X1052)|cyclic(X1051,X1052,X1053,X1054),inference(split_conjunct,[status(thm)],[c273])).
% 71.03/71.23 cnf(c10790,plain,eqangle(X5328,X5327,X5329,X5326,X5328,X5327,X5329,X5326),inference(resolution,[status(thm)],[c10770, c286])).
% 71.03/71.23 cnf(c18702,plain,~coll(X6246,X6246,X6245)|cyclic(X6247,X6245,X6246,X6246),inference(resolution,[status(thm)],[c10790, c274])).
% 71.03/71.23 cnf(c20870,plain,cyclic(X6248,X6249,X6250,X6250),inference(resolution,[status(thm)],[c18702, c20075])).
% 71.03/71.23 cnf(c20885,plain,cyclic(X6260,X6261,X6262,X6261),inference(resolution,[status(thm)],[c20870, c365])).
% 71.03/71.23 cnf(c20892,plain,cyclic(X6264,X6263,X6263,X6265),inference(resolution,[status(thm)],[c20885, c368])).
% 71.03/71.23 cnf(c20906,plain,cyclic(X6279,X6280,X6279,X6278),inference(resolution,[status(thm)],[c20892, c362])).
% 71.03/71.23 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)).
% 71.03/71.23 fof(c357,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])).
% 71.03/71.23 fof(c358,plain,(![X461]:(![X462]:(![X463]:(![X464]:(![X465]:((~cyclic(X461,X462,X463,X464)|~cyclic(X461,X462,X463,X465))|cyclic(X462,X463,X464,X465))))))),inference(variable_rename,[status(thm)],[c357])).
% 71.03/71.23 cnf(c359,plain,~cyclic(X1255,X1254,X1253,X1257)|~cyclic(X1255,X1254,X1253,X1256)|cyclic(X1254,X1253,X1257,X1256),inference(split_conjunct,[status(thm)],[c358])).
% 71.03/71.23 cnf(c20921,plain,~cyclic(X14349,X14348,X14349,X14347)|cyclic(X14348,X14349,X14347,X14346),inference(resolution,[status(thm)],[c20906, c359])).
% 71.03/71.23 cnf(c30505,plain,cyclic(X14355,X14358,X14356,X14357),inference(resolution,[status(thm)],[c20921, c20906])).
% 71.03/71.23 cnf(c30514,plain,$false,inference(resolution,[status(thm)],[c30505, c24])).
% 71.03/71.23 % SZS output end CNFRefutation
% 71.03/71.23
% 71.03/71.23 % Initial clauses : 136
% 71.03/71.23 % Processed clauses : 3409
% 71.03/71.23 % Factors computed : 189
% 71.03/71.23 % Resolvents computed: 29922
% 71.03/71.23 % Tautologies deleted: 24
% 71.03/71.23 % Forward subsumed : 9204
% 71.03/71.23 % Backward subsumed : 3060
% 71.03/71.23 % -------- CPU Time ---------
% 71.03/71.23 % User time : 70.842 s
% 71.03/71.23 % System time : 0.057 s
% 71.03/71.23 % Total time : 70.899 s
%------------------------------------------------------------------------------