%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO589+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:21 EDT 2024
% Result : Theorem 5.69s 5.85s
% Output : Refutation 5.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO589+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.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:21:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 5.69/5.85 % Version: 1.5
% 5.69/5.85 % SZS status Theorem
% 5.69/5.85 % SZS output start CNFRefutation
% 5.69/5.85 fof(exemplo6GDDFULL416051,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![NWPNT1]:(![NWPNT2]:(((((circle(O,A,B,C)&perp(A,C,B,D))&circle(O,A,D,NWPNT1))&circle(O,D,E,NWPNT2))&coll(E,D,O))=>para(B,E,A,C)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL416051)).
% 5.69/5.85 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![NWPNT1]:(![NWPNT2]:(((((circle(O,A,B,C)&perp(A,C,B,D))&circle(O,A,D,NWPNT1))&circle(O,D,E,NWPNT2))&coll(E,D,O))=>para(B,E,A,C))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416051])).
% 5.69/5.85 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(?[NWPNT1]:(?[NWPNT2]:(((((circle(O,A,B,C)&perp(A,C,B,D))&circle(O,A,D,NWPNT1))&circle(O,D,E,NWPNT2))&coll(E,D,O))&~para(B,E,A,C)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 5.69/5.85 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(((((circle(O,A,B,C)&perp(A,C,B,D))&(?[NWPNT1]:circle(O,A,D,NWPNT1)))&(?[NWPNT2]:circle(O,D,E,NWPNT2)))&coll(E,D,O))&~para(B,E,A,C)))))))),inference(shift_quantors,[status(thm)],[c12])).
% 5.69/5.85 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((circle(X5,X2,X3,X4)&perp(X2,X4,X3,X6))&(?[X8]:circle(X5,X2,X6,X8)))&(?[X9]:circle(X5,X6,X7,X9)))&coll(X7,X6,X5))&~para(X3,X7,X2,X4)))))))),inference(variable_rename,[status(thm)],[c13])).
% 5.69/5.85 fof(c15,negated_conjecture,(((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&perp(skolem0001,skolem0003,skolem0002,skolem0005))&circle(skolem0004,skolem0001,skolem0005,skolem0007))&circle(skolem0004,skolem0005,skolem0006,skolem0008))&coll(skolem0006,skolem0005,skolem0004))&~para(skolem0002,skolem0006,skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c14])).
% 5.69/5.85 cnf(c21,negated_conjecture,~para(skolem0002,skolem0006,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 5.69/5.85 fof(c399,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c398])).
% 5.69/5.85 cnf(c400,plain,~coll(X698,X700,X697)|~coll(X698,X700,X699)|coll(X697,X699,X698),inference(split_conjunct,[status(thm)],[c399])).
% 5.69/5.85 cnf(c455,plain,~coll(X703,X702,X701)|coll(X701,X701,X703),inference(factor,[status(thm)],[c400])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c187,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 5.69/5.85 fof(c188,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c187])).
% 5.69/5.85 cnf(c189,plain,~para(X584,X585,X584,X586)|coll(X584,X585,X586),inference(split_conjunct,[status(thm)],[c188])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c284,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])).
% 5.69/5.85 fof(c285,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)],[c284])).
% 5.69/5.85 fof(c287,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(c286,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)],[c285])).])).
% 5.69/5.85 cnf(c288,plain,~eqangle(X960,X957,X962,X958,X959,X961,X962,X958)|para(X960,X957,X959,X961),inference(split_conjunct,[status(thm)],[c287])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c279,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])).
% 5.69/5.85 fof(c280,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)],[c279])).
% 5.69/5.85 fof(c282,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(c281,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)],[c280])).])).
% 5.69/5.85 cnf(c283,plain,~para(X952,X953,X956,X954)|eqangle(X952,X953,X951,X955,X956,X954,X951,X955),inference(split_conjunct,[status(thm)],[c282])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 5.69/5.85 fof(c396,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c395])).
% 5.69/5.85 cnf(c397,plain,~para(X677,X675,X678,X676)|para(X677,X675,X676,X678),inference(split_conjunct,[status(thm)],[c396])).
% 5.69/5.85 cnf(c17,negated_conjecture,perp(skolem0001,skolem0003,skolem0002,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 5.69/5.85 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 5.69/5.85 fof(c383,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 5.69/5.85 fof(c384,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c383])).
% 5.69/5.85 cnf(c385,plain,~perp(X617,X618,X616,X615)|perp(X616,X615,X617,X618),inference(split_conjunct,[status(thm)],[c384])).
% 5.69/5.85 cnf(c432,plain,perp(skolem0002,skolem0005,skolem0001,skolem0003),inference(resolution,[status(thm)],[c385, c17])).
% 5.69/5.85 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 5.69/5.85 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 5.69/5.85 fof(c387,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c386])).
% 5.69/5.85 cnf(c388,plain,~perp(X630,X627,X629,X628)|perp(X630,X627,X628,X629),inference(split_conjunct,[status(thm)],[c387])).
% 5.69/5.85 cnf(c436,plain,perp(skolem0002,skolem0005,skolem0003,skolem0001),inference(resolution,[status(thm)],[c388, c432])).
% 5.69/5.85 fof(ruleD9,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((perp(A,B,C,D)&perp(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 5.69/5.85 fof(c380,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~perp(A,B,C,D)|~perp(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD9])).
% 5.69/5.85 fof(c381,plain,(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:((~perp(X493,X494,X495,X496)|~perp(X495,X496,X497,X498))|para(X493,X494,X497,X498)))))))),inference(variable_rename,[status(thm)],[c380])).
% 5.69/5.85 cnf(c382,plain,~perp(X1134,X1131,X1132,X1133)|~perp(X1132,X1133,X1135,X1130)|para(X1134,X1131,X1135,X1130),inference(split_conjunct,[status(thm)],[c381])).
% 5.69/5.85 cnf(c758,plain,~perp(X1139,X1138,skolem0002,skolem0005)|para(X1139,X1138,skolem0003,skolem0001),inference(resolution,[status(thm)],[c382, c436])).
% 5.69/5.85 cnf(c767,plain,para(skolem0001,skolem0003,skolem0003,skolem0001),inference(resolution,[status(thm)],[c758, c17])).
% 5.69/5.85 cnf(c839,plain,para(skolem0001,skolem0003,skolem0001,skolem0003),inference(resolution,[status(thm)],[c767, c397])).
% 5.69/5.85 cnf(c873,plain,eqangle(skolem0001,skolem0003,X1227,X1226,skolem0001,skolem0003,X1227,X1226),inference(resolution,[status(thm)],[c839, c283])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c348,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])).
% 5.69/5.85 fof(c349,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)],[c348])).
% 5.69/5.85 cnf(c350,plain,~eqangle(X1322,X1328,X1323,X1326,X1325,X1327,X1324,X1329)|eqangle(X1323,X1326,X1322,X1328,X1324,X1329,X1325,X1327),inference(split_conjunct,[status(thm)],[c349])).
% 5.69/5.85 cnf(c1135,plain,eqangle(X1535,X1536,skolem0001,skolem0003,X1535,X1536,skolem0001,skolem0003),inference(resolution,[status(thm)],[c350, c873])).
% 5.69/5.85 cnf(c1575,plain,para(X1538,X1537,X1538,X1537),inference(resolution,[status(thm)],[c1135, c288])).
% 5.69/5.85 cnf(c1583,plain,coll(X1539,X1540,X1540),inference(resolution,[status(thm)],[c1575, c189])).
% 5.69/5.85 cnf(c1670,plain,coll(X1546,X1546,X1545),inference(resolution,[status(thm)],[c1583, c455])).
% 5.69/5.85 cnf(c1723,plain,~coll(X1832,X1832,X1833)|coll(X1833,X1831,X1832),inference(resolution,[status(thm)],[c1670, c400])).
% 5.69/5.85 cnf(c2362,plain,coll(X1842,X1840,X1841),inference(resolution,[status(thm)],[c1723, c1670])).
% 5.69/5.85 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 5.69/5.85 fof(c184,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 5.69/5.85 fof(c185,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c184])).
% 5.69/5.85 cnf(c186,plain,~cong(X923,X922,X923,X921)|~coll(X923,X922,X921)|midp(X923,X922,X921),inference(split_conjunct,[status(thm)],[c185])).
% 5.69/5.85 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 5.69/5.85 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 5.69/5.85 fof(c337,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c336])).
% 5.69/5.85 cnf(c338,plain,~cong(X602,X599,X600,X601)|cong(X602,X599,X601,X600),inference(split_conjunct,[status(thm)],[c337])).
% 5.69/5.85 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 5.69/5.85 fof(c333,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 5.69/5.85 fof(c334,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c333])).
% 5.69/5.85 cnf(c335,plain,~cong(X587,X589,X588,X590)|cong(X588,X590,X587,X589),inference(split_conjunct,[status(thm)],[c334])).
% 5.69/5.85 fof(ruleD64,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(((midp(M,A,B)¶(A,C,B,D))¶(A,D,B,C))=>midp(M,C,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 5.69/5.85 fof(c193,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C))|midp(M,C,D))))))),inference(fof_nnf,[status(thm)],[ruleD64])).
% 5.69/5.85 fof(c194,plain,(![X172]:(![X173]:(![X174]:(![X175]:(![X176]:(((~midp(X176,X172,X173)|~para(X172,X174,X173,X175))|~para(X172,X175,X173,X174))|midp(X176,X174,X175))))))),inference(variable_rename,[status(thm)],[c193])).
% 5.69/5.85 cnf(c195,plain,~midp(X1146,X1149,X1148)|~para(X1149,X1145,X1148,X1147)|~para(X1149,X1147,X1148,X1145)|midp(X1146,X1145,X1147),inference(split_conjunct,[status(thm)],[c194])).
% 5.69/5.85 cnf(c799,plain,~midp(X2163,X2162,X2165)|~para(X2162,X2164,X2165,X2164)|midp(X2163,X2164,X2164),inference(factor,[status(thm)],[c195])).
% 5.69/5.85 cnf(c2898,plain,~midp(X2246,X2245,X2245)|midp(X2246,X2244,X2244),inference(resolution,[status(thm)],[c799, c1575])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 5.69/5.85 fof(c364,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c363])).
% 5.69/5.85 cnf(c365,plain,~cyclic(X612,X613,X614,X611)|cyclic(X612,X613,X611,X614),inference(split_conjunct,[status(thm)],[c364])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c357,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 5.69/5.85 fof(c358,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X464,X463,X465,X466)))))),inference(variable_rename,[status(thm)],[c357])).
% 5.69/5.85 cnf(c359,plain,~cyclic(X605,X604,X603,X606)|cyclic(X604,X605,X603,X606),inference(split_conjunct,[status(thm)],[c358])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 5.69/5.85 fof(c361,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c360])).
% 5.69/5.85 cnf(c362,plain,~cyclic(X610,X607,X609,X608)|cyclic(X610,X609,X607,X608),inference(split_conjunct,[status(thm)],[c361])).
% 5.69/5.85 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)).
% 5.69/5.85 fof(c269,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])).
% 5.69/5.85 fof(c270,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)],[c269])).
% 5.69/5.85 cnf(c271,plain,~eqangle(X1214,X1213,X1214,X1215,X1216,X1213,X1216,X1215)|~coll(X1214,X1216,X1215)|cyclic(X1213,X1215,X1214,X1216),inference(split_conjunct,[status(thm)],[c270])).
% 5.69/5.85 cnf(c1599,plain,eqangle(X1731,X1733,X1734,X1732,X1731,X1733,X1734,X1732),inference(resolution,[status(thm)],[c1575, c283])).
% 5.69/5.85 cnf(c2204,plain,~coll(X2066,X2066,X2067)|cyclic(X2065,X2067,X2066,X2066),inference(resolution,[status(thm)],[c1599, c271])).
% 5.69/5.85 cnf(c2789,plain,cyclic(X2069,X2068,X2070,X2070),inference(resolution,[status(thm)],[c2204, c2362])).
% 5.69/5.85 cnf(c2792,plain,cyclic(X2073,X2072,X2071,X2072),inference(resolution,[status(thm)],[c2789, c362])).
% 5.69/5.85 cnf(c2802,plain,cyclic(X2087,X2088,X2086,X2087),inference(resolution,[status(thm)],[c2792, c359])).
% 5.69/5.85 cnf(c2814,plain,cyclic(X2102,X2104,X2102,X2103),inference(resolution,[status(thm)],[c2802, c365])).
% 5.69/5.85 fof(ruleD43,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((cyclic(A,B,C,P)&cyclic(A,B,C,Q))&cyclic(A,B,C,R))&eqangle(C,A,C,B,R,P,R,Q))=>cong(A,B,P,Q)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 5.69/5.85 fof(c264,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q))|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD43])).
% 5.69/5.85 fof(c265,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:((![R]:(((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q)))|cong(A,B,P,Q))))))),inference(shift_quantors,[status(thm)],[c264])).
% 5.69/5.85 fof(c267,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276))|cong(X272,X273,X275,X276)))))))),inference(shift_quantors,[status(thm)],[fof(c266,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((![X277]:(((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276)))|cong(X272,X273,X275,X276))))))),inference(variable_rename,[status(thm)],[c265])).])).
% 5.69/5.85 cnf(c268,plain,~cyclic(X1206,X1207,X1208,X1205)|~cyclic(X1206,X1207,X1208,X1210)|~cyclic(X1206,X1207,X1208,X1209)|~eqangle(X1208,X1206,X1208,X1207,X1209,X1205,X1209,X1210)|cong(X1206,X1207,X1205,X1210),inference(split_conjunct,[status(thm)],[c267])).
% 5.69/5.85 fof(ruleD21,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(A,B,P,Q,C,D,U,V)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 5.69/5.85 fof(c342,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(A,B,P,Q,C,D,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD21])).
% 5.69/5.85 fof(c343,plain,(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(~eqangle(X426,X427,X428,X429,X430,X431,X432,X433)|eqangle(X426,X427,X430,X431,X428,X429,X432,X433)))))))))),inference(variable_rename,[status(thm)],[c342])).
% 5.69/5.85 cnf(c344,plain,~eqangle(X1313,X1311,X1309,X1307,X1306,X1312,X1308,X1310)|eqangle(X1313,X1311,X1306,X1312,X1309,X1307,X1308,X1310),inference(split_conjunct,[status(thm)],[c343])).
% 5.69/5.85 cnf(c1593,plain,para(X1557,X1556,X1556,X1557),inference(resolution,[status(thm)],[c1575, c397])).
% 5.69/5.85 cnf(c1752,plain,eqangle(X1889,X1887,X1890,X1888,X1887,X1889,X1890,X1888),inference(resolution,[status(thm)],[c1593, c283])).
% 5.69/5.85 cnf(c2423,plain,eqangle(X1911,X1913,X1914,X1912,X1911,X1913,X1912,X1914),inference(resolution,[status(thm)],[c1752, c350])).
% 5.69/5.85 cnf(c2452,plain,eqangle(X1954,X1951,X1954,X1951,X1953,X1952,X1952,X1953),inference(resolution,[status(thm)],[c2423, c344])).
% 5.69/5.85 cnf(c2483,plain,~cyclic(X2877,X2877,X2876,X2878)|cong(X2877,X2877,X2878,X2878),inference(resolution,[status(thm)],[c2452, c268])).
% 5.69/5.85 cnf(c3358,plain,cong(X2879,X2879,X2880,X2880),inference(resolution,[status(thm)],[c2483, c2814])).
% 5.69/5.85 cnf(c3369,plain,~coll(X2924,X2924,X2924)|midp(X2924,X2924,X2924),inference(resolution,[status(thm)],[c3358, c186])).
% 5.69/5.85 cnf(c3470,plain,midp(X2925,X2925,X2925),inference(resolution,[status(thm)],[c3369, c2362])).
% 5.69/5.85 cnf(c3480,plain,midp(X2927,X2928,X2928),inference(resolution,[status(thm)],[c3470, c2898])).
% 5.69/5.85 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 5.69/5.85 fof(c236,plain,(![A]:(![B]:(![C]:(![M]:((~perp(A,B,B,C)|~midp(M,A,C))|cong(A,M,B,M)))))),inference(fof_nnf,[status(thm)],[ruleD52])).
% 5.69/5.85 fof(c237,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c236])).
% 5.69/5.85 cnf(c238,plain,~perp(X1036,X1033,X1033,X1035)|~midp(X1034,X1036,X1035)|cong(X1036,X1034,X1033,X1034),inference(split_conjunct,[status(thm)],[c237])).
% 5.69/5.85 fof(ruleD74,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((eqangle(A,B,C,D,P,Q,U,V)&perp(P,Q,U,V))=>perp(A,B,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 5.69/5.85 fof(c157,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 5.69/5.85 fof(c158,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))))))|perp(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c157])).
% 5.69/5.85 fof(c160,plain,(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:((~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))|perp(X125,X126,X127,X128)))))))))),inference(shift_quantors,[status(thm)],[fof(c159,plain,(![X125]:(![X126]:(![X127]:(![X128]:((![X129]:(![X130]:(![X131]:(![X132]:(~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))))))|perp(X125,X126,X127,X128)))))),inference(variable_rename,[status(thm)],[c158])).])).
% 5.69/5.85 cnf(c161,plain,~eqangle(X1028,X1027,X1025,X1026,X1029,X1031,X1030,X1032)|~perp(X1029,X1031,X1030,X1032)|perp(X1028,X1027,X1025,X1026),inference(split_conjunct,[status(thm)],[c160])).
% 5.69/5.85 cnf(c2424,plain,eqangle(X1920,X1919,X1919,X1920,X1918,X1917,X1918,X1917),inference(resolution,[status(thm)],[c1752, c344])).
% 5.69/5.85 cnf(c2472,plain,~perp(X2866,X2864,X2866,X2864)|perp(X2867,X2865,X2865,X2867),inference(resolution,[status(thm)],[c2424, c161])).
% 5.69/5.85 fof(ruleD56,axiom,(![A]:(![B]:(![P]:(![Q]:((cong(A,P,B,P)&cong(A,Q,B,Q))=>perp(A,B,P,Q)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 5.69/5.85 fof(c222,plain,(![A]:(![B]:(![P]:(![Q]:((~cong(A,P,B,P)|~cong(A,Q,B,Q))|perp(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD56])).
% 5.69/5.85 fof(c223,plain,(![X216]:(![X217]:(![X218]:(![X219]:((~cong(X216,X218,X217,X218)|~cong(X216,X219,X217,X219))|perp(X216,X217,X218,X219)))))),inference(variable_rename,[status(thm)],[c222])).
% 5.69/5.85 cnf(c224,plain,~cong(X1054,X1053,X1055,X1053)|~cong(X1054,X1052,X1055,X1052)|perp(X1054,X1055,X1053,X1052),inference(split_conjunct,[status(thm)],[c223])).
% 5.69/5.85 cnf(c744,plain,~cong(X1064,X1066,X1065,X1066)|perp(X1064,X1065,X1066,X1066),inference(factor,[status(thm)],[c224])).
% 5.69/5.85 cnf(c3370,plain,perp(X2891,X2891,X2891,X2891),inference(resolution,[status(thm)],[c3358, c744])).
% 5.69/5.85 cnf(c3389,plain,perp(X2904,X2903,X2903,X2904),inference(resolution,[status(thm)],[c3370, c2472])).
% 5.69/5.85 cnf(c3412,plain,~midp(X3700,X3701,X3701)|cong(X3701,X3700,X3699,X3700),inference(resolution,[status(thm)],[c3389, c238])).
% 5.69/5.85 cnf(c4695,plain,cong(X3703,X3704,X3702,X3704),inference(resolution,[status(thm)],[c3412, c3480])).
% 5.69/5.85 cnf(c4707,plain,cong(X3718,X3719,X3719,X3717),inference(resolution,[status(thm)],[c4695, c338])).
% 5.69/5.85 cnf(c4734,plain,cong(X3734,X3736,X3735,X3734),inference(resolution,[status(thm)],[c4707, c335])).
% 5.69/5.85 cnf(c4775,plain,cong(X3760,X3759,X3760,X3758),inference(resolution,[status(thm)],[c4734, c338])).
% 5.69/5.85 cnf(c4786,plain,~coll(X3902,X3904,X3903)|midp(X3902,X3904,X3903),inference(resolution,[status(thm)],[c4775, c186])).
% 5.69/5.85 cnf(c5037,plain,midp(X3907,X3906,X3905),inference(resolution,[status(thm)],[c4786, c2362])).
% 5.69/5.85 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 5.69/5.85 fof(c261,plain,(![A]:(![B]:(![C]:(![E]:(![F]:((~midp(E,A,B)|~midp(F,A,C))|para(E,F,B,C))))))),inference(fof_nnf,[status(thm)],[ruleD44])).
% 5.69/5.85 fof(c262,plain,(![X267]:(![X268]:(![X269]:(![X270]:(![X271]:((~midp(X270,X267,X268)|~midp(X271,X267,X269))|para(X270,X271,X268,X269))))))),inference(variable_rename,[status(thm)],[c261])).
% 5.69/5.85 cnf(c263,plain,~midp(X941,X942,X943)|~midp(X940,X942,X939)|para(X941,X940,X943,X939),inference(split_conjunct,[status(thm)],[c262])).
% 5.69/5.85 cnf(c3497,plain,~midp(X6991,X6990,X6992)|para(X6991,X6989,X6992,X6990),inference(resolution,[status(thm)],[c3480, c263])).
% 5.69/5.85 cnf(c7498,plain,para(X6995,X6996,X6993,X6994),inference(resolution,[status(thm)],[c3497, c5037])).
% 5.69/5.85 cnf(c7505,plain,$false,inference(resolution,[status(thm)],[c7498, c21])).
% 5.69/5.85 % SZS output end CNFRefutation
% 5.69/5.85
% 5.69/5.85 % Initial clauses : 133
% 5.69/5.85 % Processed clauses : 947
% 5.69/5.85 % Factors computed : 110
% 5.69/5.85 % Resolvents computed: 6995
% 5.69/5.85 % Tautologies deleted: 29
% 5.69/5.85 % Forward subsumed : 2470
% 5.69/5.85 % Backward subsumed : 582
% 5.69/5.85 % -------- CPU Time ---------
% 5.69/5.85 % User time : 5.484 s
% 5.69/5.85 % System time : 0.021 s
% 5.69/5.85 % Total time : 5.505 s
%------------------------------------------------------------------------------