%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO569+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:18 EDT 2024
% Result : Theorem 202.36s 202.57s
% Output : Refutation 202.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO569+1 : TPTP v8.1.2. Released v7.5.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 08:35:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 202.36/202.57 % Version: 1.5
% 202.36/202.57 % SZS status Theorem
% 202.36/202.57 % SZS output start CNFRefutation
% 202.36/202.57 fof(exemplo6GDDFULL214031,conjecture,(![A]:(![B]:(![C]:(![O]:(![C1]:(![B1]:(![P]:(![Q]:(((((((circle(O,A,B,C)&midp(C1,B,A))&midp(B1,C,A))&coll(P,O,C1))&coll(P,A,C))&coll(Q,O,B1))&coll(Q,A,B))=>cyclic(Q,B,C,P)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214031)).
% 202.36/202.57 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![C1]:(![B1]:(![P]:(![Q]:(((((((circle(O,A,B,C)&midp(C1,B,A))&midp(B1,C,A))&coll(P,O,C1))&coll(P,A,C))&coll(Q,O,B1))&coll(Q,A,B))=>cyclic(Q,B,C,P))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214031])).
% 202.36/202.57 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[C1]:(?[B1]:(?[P]:(?[Q]:(((((((circle(O,A,B,C)&midp(C1,B,A))&midp(B1,C,A))&coll(P,O,C1))&coll(P,A,C))&coll(Q,O,B1))&coll(Q,A,B))&~cyclic(Q,B,C,P)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 202.36/202.57 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((circle(X5,X2,X3,X4)&midp(X6,X3,X2))&midp(X7,X4,X2))&coll(X8,X5,X6))&coll(X8,X2,X4))&coll(X9,X5,X7))&coll(X9,X2,X3))&~cyclic(X9,X3,X4,X8)))))))))),inference(variable_rename,[status(thm)],[c12])).
% 202.36/202.57 fof(c14,negated_conjecture,(((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&midp(skolem0005,skolem0002,skolem0001))&midp(skolem0006,skolem0003,skolem0001))&coll(skolem0007,skolem0004,skolem0005))&coll(skolem0007,skolem0001,skolem0003))&coll(skolem0008,skolem0004,skolem0006))&coll(skolem0008,skolem0001,skolem0002))&~cyclic(skolem0008,skolem0002,skolem0003,skolem0007)),inference(skolemize,[status(esa)],[c13])).
% 202.36/202.57 cnf(c22,negated_conjecture,~cyclic(skolem0008,skolem0002,skolem0003,skolem0007),inference(split_conjunct,[status(thm)],[c14])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 202.36/202.57 fof(c365,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c364])).
% 202.36/202.57 cnf(c366,plain,~cyclic(X759,X758,X757,X760)|cyclic(X759,X758,X760,X757),inference(split_conjunct,[status(thm)],[c365])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c358,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 202.36/202.57 fof(c359,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X464,X463,X465,X466)))))),inference(variable_rename,[status(thm)],[c358])).
% 202.36/202.57 cnf(c360,plain,~cyclic(X751,X749,X752,X750)|cyclic(X749,X751,X752,X750),inference(split_conjunct,[status(thm)],[c359])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 202.36/202.57 fof(c362,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c361])).
% 202.36/202.57 cnf(c363,plain,~cyclic(X755,X754,X753,X756)|cyclic(X755,X753,X754,X756),inference(split_conjunct,[status(thm)],[c362])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 202.36/202.57 fof(c400,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c399])).
% 202.36/202.57 cnf(c401,plain,~coll(X792,X791,X794)|~coll(X792,X791,X793)|coll(X794,X793,X792),inference(split_conjunct,[status(thm)],[c400])).
% 202.36/202.57 cnf(c609,plain,~coll(X796,X795,X797)|coll(X797,X797,X796),inference(factor,[status(thm)],[c401])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c188,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 202.36/202.57 fof(c189,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c188])).
% 202.36/202.57 cnf(c190,plain,~para(X703,X702,X703,X701)|coll(X703,X702,X701),inference(split_conjunct,[status(thm)],[c189])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c285,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])).
% 202.36/202.57 fof(c286,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)],[c285])).
% 202.36/202.57 fof(c288,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(c287,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)],[c286])).])).
% 202.36/202.57 cnf(c289,plain,~eqangle(X1065,X1063,X1061,X1062,X1064,X1060,X1061,X1062)|para(X1065,X1063,X1064,X1060),inference(split_conjunct,[status(thm)],[c288])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c349,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])).
% 202.36/202.57 fof(c350,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)],[c349])).
% 202.36/202.57 cnf(c351,plain,~eqangle(X1201,X1205,X1204,X1207,X1208,X1202,X1203,X1206)|eqangle(X1204,X1207,X1201,X1205,X1203,X1206,X1208,X1202),inference(split_conjunct,[status(thm)],[c350])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c280,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])).
% 202.36/202.57 fof(c281,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)],[c280])).
% 202.36/202.57 fof(c283,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(c282,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)],[c281])).])).
% 202.36/202.57 cnf(c284,plain,~para(X1058,X1056,X1057,X1055)|eqangle(X1058,X1056,X1059,X1054,X1057,X1055,X1059,X1054),inference(split_conjunct,[status(thm)],[c283])).
% 202.36/202.57 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)).
% 202.36/202.57 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 202.36/202.57 fof(c397,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c396])).
% 202.36/202.57 cnf(c398,plain,~para(X780,X777,X779,X778)|para(X780,X777,X778,X779),inference(split_conjunct,[status(thm)],[c397])).
% 202.36/202.57 cnf(c17,negated_conjecture,midp(skolem0006,skolem0003,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 202.36/202.57 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 202.36/202.58 fof(c375,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 202.36/202.58 fof(c376,plain,(![X484]:(![X485]:(![X486]:(~midp(X486,X485,X484)|midp(X486,X484,X485))))),inference(variable_rename,[status(thm)],[c375])).
% 202.36/202.58 cnf(c377,plain,~midp(X559,X560,X558)|midp(X559,X558,X560),inference(split_conjunct,[status(thm)],[c376])).
% 202.36/202.58 cnf(c419,plain,midp(skolem0006,skolem0001,skolem0003),inference(resolution,[status(thm)],[c377, c17])).
% 202.36/202.58 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)).
% 202.36/202.58 fof(c197,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])).
% 202.36/202.58 fof(c198,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c197])).
% 202.36/202.58 fof(c200,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(c199,plain,(![X177]:(![X178]:(![X179]:(![X180]:((![X181]:(~midp(X181,X177,X178)|~midp(X181,X179,X180)))|para(X177,X179,X178,X180)))))),inference(variable_rename,[status(thm)],[c198])).])).
% 202.36/202.58 cnf(c201,plain,~midp(X950,X948,X947)|~midp(X950,X949,X951)|para(X948,X949,X947,X951),inference(split_conjunct,[status(thm)],[c200])).
% 202.36/202.58 cnf(c1200,plain,~midp(skolem0006,X2392,X2393)|para(X2392,skolem0001,X2393,skolem0003),inference(resolution,[status(thm)],[c201, c419])).
% 202.36/202.58 cnf(c6425,plain,para(skolem0003,skolem0001,skolem0001,skolem0003),inference(resolution,[status(thm)],[c1200, c17])).
% 202.36/202.58 cnf(c6685,plain,para(skolem0003,skolem0001,skolem0003,skolem0001),inference(resolution,[status(thm)],[c6425, c398])).
% 202.36/202.58 cnf(c6765,plain,eqangle(skolem0003,skolem0001,X5361,X5362,skolem0003,skolem0001,X5361,X5362),inference(resolution,[status(thm)],[c6685, c284])).
% 202.36/202.58 cnf(c16612,plain,eqangle(X6267,X6266,skolem0003,skolem0001,X6267,X6266,skolem0003,skolem0001),inference(resolution,[status(thm)],[c6765, c351])).
% 202.36/202.58 cnf(c20969,plain,para(X6271,X6272,X6271,X6272),inference(resolution,[status(thm)],[c16612, c289])).
% 202.36/202.58 cnf(c21023,plain,coll(X6273,X6274,X6274),inference(resolution,[status(thm)],[c20969, c190])).
% 202.36/202.58 cnf(c21451,plain,coll(X6277,X6277,X6278),inference(resolution,[status(thm)],[c21023, c609])).
% 202.36/202.58 cnf(c21795,plain,~coll(X9066,X9066,X9065)|coll(X9065,X9067,X9066),inference(resolution,[status(thm)],[c21451, c401])).
% 202.36/202.58 cnf(c34786,plain,coll(X9072,X9073,X9074),inference(resolution,[status(thm)],[c21795, c21451])).
% 202.36/202.58 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)).
% 202.36/202.58 fof(c270,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])).
% 202.36/202.58 fof(c271,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)],[c270])).
% 202.36/202.58 cnf(c272,plain,~eqangle(X1044,X1042,X1044,X1045,X1043,X1042,X1043,X1045)|~coll(X1044,X1043,X1045)|cyclic(X1042,X1045,X1044,X1043),inference(split_conjunct,[status(thm)],[c271])).
% 202.36/202.58 cnf(c20993,plain,eqangle(X8457,X8455,X8456,X8458,X8457,X8455,X8456,X8458),inference(resolution,[status(thm)],[c20969, c284])).
% 202.36/202.58 cnf(c31864,plain,~coll(X9644,X9644,X9642)|cyclic(X9643,X9642,X9644,X9644),inference(resolution,[status(thm)],[c20993, c272])).
% 202.36/202.58 cnf(c35337,plain,cyclic(X9645,X9646,X9647,X9647),inference(resolution,[status(thm)],[c31864, c34786])).
% 202.36/202.58 cnf(c35349,plain,cyclic(X9652,X9651,X9653,X9651),inference(resolution,[status(thm)],[c35337, c363])).
% 202.36/202.58 cnf(c35370,plain,cyclic(X9660,X9662,X9661,X9660),inference(resolution,[status(thm)],[c35349, c360])).
% 202.36/202.58 cnf(c35380,plain,cyclic(X9678,X9680,X9678,X9679),inference(resolution,[status(thm)],[c35370, c366])).
% 202.36/202.58 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)).
% 202.36/202.58 fof(c355,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])).
% 202.36/202.58 fof(c356,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)],[c355])).
% 202.36/202.58 cnf(c357,plain,~cyclic(X1223,X1224,X1221,X1220)|~cyclic(X1223,X1224,X1221,X1222)|cyclic(X1224,X1221,X1220,X1222),inference(split_conjunct,[status(thm)],[c356])).
% 202.36/202.58 cnf(c35401,plain,~cyclic(X19411,X19412,X19411,X19409)|cyclic(X19412,X19411,X19409,X19410),inference(resolution,[status(thm)],[c35380, c357])).
% 202.36/202.58 cnf(c50454,plain,cyclic(X19432,X19431,X19433,X19434),inference(resolution,[status(thm)],[c35401, c35380])).
% 202.36/202.58 cnf(c50455,plain,$false,inference(resolution,[status(thm)],[c50454, c22])).
% 202.36/202.58 % SZS output end CNFRefutation
% 202.36/202.58
% 202.36/202.58 % Initial clauses : 135
% 202.36/202.58 % Processed clauses : 5314
% 202.36/202.58 % Factors computed : 236
% 202.36/202.58 % Resolvents computed: 49827
% 202.36/202.58 % Tautologies deleted: 29
% 202.36/202.58 % Forward subsumed : 14633
% 202.36/202.58 % Backward subsumed : 4951
% 202.36/202.58 % -------- CPU Time ---------
% 202.36/202.58 % User time : 202.145 s
% 202.36/202.58 % System time : 0.083 s
% 202.36/202.58 % Total time : 202.228 s
%------------------------------------------------------------------------------