%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO622+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:25 EDT 2024
% Result : Theorem 8.05s 8.23s
% Output : Refutation 8.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO622+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n024.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 08:14:23 EDT 2024
% 0.14/0.34 % CPUTime :
% 8.05/8.23 % Version: 1.5
% 8.05/8.23 % SZS status Theorem
% 8.05/8.23 % SZS output start CNFRefutation
% 8.05/8.23 fof(exemplo6GDDFULL8110985,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![NWPNT1]:((((((circle(D,A,B,C)&eqangle(E,A,A,C,E,A,A,B))&coll(E,B,C))&midpoint(NWPNT1,A,E))&perp(A,E,NWPNT1,F))&coll(F,A,D))=>perp(E,F,B,C))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL8110985)).
% 8.05/8.23 fof(c12,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![NWPNT1]:((((((circle(D,A,B,C)&eqangle(E,A,A,C,E,A,A,B))&coll(E,B,C))&midpoint(NWPNT1,A,E))&perp(A,E,NWPNT1,F))&coll(F,A,D))=>perp(E,F,B,C)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110985])).
% 8.05/8.23 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[NWPNT1]:((((((circle(D,A,B,C)&eqangle(E,A,A,C,E,A,A,B))&coll(E,B,C))&midpoint(NWPNT1,A,E))&perp(A,E,NWPNT1,F))&coll(F,A,D))&~perp(E,F,B,C))))))))),inference(fof_nnf,[status(thm)],[c12])).
% 8.05/8.23 fof(c14,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(((?[NWPNT1]:((((circle(D,A,B,C)&eqangle(E,A,A,C,E,A,A,B))&coll(E,B,C))&midpoint(NWPNT1,A,E))&perp(A,E,NWPNT1,F)))&coll(F,A,D))&~perp(E,F,B,C)))))))),inference(shift_quantors,[status(thm)],[c13])).
% 8.05/8.23 fof(c15,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((?[X8]:((((circle(X5,X2,X3,X4)&eqangle(X6,X2,X2,X4,X6,X2,X2,X3))&coll(X6,X3,X4))&midpoint(X8,X2,X6))&perp(X2,X6,X8,X7)))&coll(X7,X2,X5))&~perp(X6,X7,X3,X4)))))))),inference(variable_rename,[status(thm)],[c14])).
% 8.05/8.23 fof(c16,negated_conjecture,((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&eqangle(skolem0005,skolem0001,skolem0001,skolem0003,skolem0005,skolem0001,skolem0001,skolem0002))&coll(skolem0005,skolem0002,skolem0003))&midpoint(skolem0007,skolem0001,skolem0005))&perp(skolem0001,skolem0005,skolem0007,skolem0006))&coll(skolem0006,skolem0001,skolem0004))&~perp(skolem0005,skolem0006,skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c15])).
% 8.05/8.23 cnf(c23,negated_conjecture,~perp(skolem0005,skolem0006,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c16])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 8.05/8.23 fof(c401,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c400])).
% 8.05/8.23 cnf(c402,plain,~coll(X714,X717,X716)|~coll(X714,X717,X715)|coll(X716,X715,X714),inference(split_conjunct,[status(thm)],[c401])).
% 8.05/8.23 cnf(c474,plain,~coll(X720,X719,X718)|coll(X718,X718,X720),inference(factor,[status(thm)],[c402])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 8.05/8.23 fof(c190,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c189])).
% 8.05/8.23 cnf(c191,plain,~para(X607,X608,X607,X609)|coll(X607,X608,X609),inference(split_conjunct,[status(thm)],[c190])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c286,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])).
% 8.05/8.23 fof(c287,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)],[c286])).
% 8.05/8.23 fof(c289,plain,(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)|para(X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c288,plain,(![X295]:(![X296]:(![X297]:(![X298]:((![X299]:(![X300]:~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)))|para(X295,X296,X297,X298)))))),inference(variable_rename,[status(thm)],[c287])).])).
% 8.05/8.23 cnf(c290,plain,~eqangle(X1130,X1132,X1133,X1128,X1131,X1129,X1133,X1128)|para(X1130,X1132,X1131,X1129),inference(split_conjunct,[status(thm)],[c289])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c350,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])).
% 8.05/8.23 fof(c351,plain,(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(~eqangle(X441,X442,X443,X444,X445,X446,X447,X448)|eqangle(X443,X444,X441,X442,X447,X448,X445,X446)))))))))),inference(variable_rename,[status(thm)],[c350])).
% 8.05/8.23 cnf(c352,plain,~eqangle(X1347,X1349,X1346,X1344,X1350,X1351,X1348,X1345)|eqangle(X1346,X1344,X1347,X1349,X1348,X1345,X1350,X1351),inference(split_conjunct,[status(thm)],[c351])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c281,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])).
% 8.05/8.23 fof(c282,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)],[c281])).
% 8.05/8.23 fof(c284,plain,(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(~para(X289,X290,X291,X292)|eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(shift_quantors,[status(thm)],[fof(c283,plain,(![X289]:(![X290]:(![X291]:(![X292]:(~para(X289,X290,X291,X292)|(![X293]:(![X294]:eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(variable_rename,[status(thm)],[c282])).])).
% 8.05/8.23 cnf(c285,plain,~para(X1122,X1121,X1124,X1123)|eqangle(X1122,X1121,X1125,X1126,X1124,X1123,X1125,X1126),inference(split_conjunct,[status(thm)],[c284])).
% 8.05/8.23 cnf(c21,negated_conjecture,perp(skolem0001,skolem0005,skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c16])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 8.05/8.23 fof(c386,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c385])).
% 8.05/8.23 cnf(c387,plain,~perp(X646,X649,X647,X648)|perp(X647,X648,X646,X649),inference(split_conjunct,[status(thm)],[c386])).
% 8.05/8.23 cnf(c450,plain,perp(skolem0007,skolem0006,skolem0001,skolem0005),inference(resolution,[status(thm)],[c387, c21])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 8.05/8.23 fof(c389,plain,(![X502]:(![X503]:(![X504]:(![X505]:(~perp(X502,X503,X504,X505)|perp(X502,X503,X505,X504)))))),inference(variable_rename,[status(thm)],[c388])).
% 8.05/8.23 cnf(c390,plain,~perp(X650,X652,X653,X651)|perp(X650,X652,X651,X653),inference(split_conjunct,[status(thm)],[c389])).
% 8.05/8.23 cnf(c453,plain,perp(skolem0007,skolem0006,skolem0005,skolem0001),inference(resolution,[status(thm)],[c390, c450])).
% 8.05/8.23 cnf(c457,plain,perp(skolem0005,skolem0001,skolem0007,skolem0006),inference(resolution,[status(thm)],[c453, c387])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c382,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])).
% 8.05/8.23 fof(c383,plain,(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:((~perp(X492,X493,X494,X495)|~perp(X494,X495,X496,X497))|para(X492,X493,X496,X497)))))))),inference(variable_rename,[status(thm)],[c382])).
% 8.05/8.23 cnf(c384,plain,~perp(X1301,X1300,X1302,X1299)|~perp(X1302,X1299,X1298,X1303)|para(X1301,X1300,X1298,X1303),inference(split_conjunct,[status(thm)],[c383])).
% 8.05/8.23 cnf(c1007,plain,~perp(X1306,X1307,skolem0005,skolem0001)|para(X1306,X1307,skolem0007,skolem0006),inference(resolution,[status(thm)],[c384, c457])).
% 8.05/8.23 cnf(c1016,plain,para(skolem0007,skolem0006,skolem0007,skolem0006),inference(resolution,[status(thm)],[c1007, c453])).
% 8.05/8.23 cnf(c1032,plain,eqangle(skolem0007,skolem0006,X1464,X1465,skolem0007,skolem0006,X1464,X1465),inference(resolution,[status(thm)],[c1016, c285])).
% 8.05/8.23 cnf(c1384,plain,eqangle(X1637,X1638,skolem0007,skolem0006,X1637,X1638,skolem0007,skolem0006),inference(resolution,[status(thm)],[c1032, c352])).
% 8.05/8.23 cnf(c1683,plain,para(X1639,X1640,X1639,X1640),inference(resolution,[status(thm)],[c1384, c290])).
% 8.05/8.23 cnf(c1702,plain,coll(X1644,X1645,X1645),inference(resolution,[status(thm)],[c1683, c191])).
% 8.05/8.23 cnf(c1775,plain,coll(X1651,X1651,X1650),inference(resolution,[status(thm)],[c1702, c474])).
% 8.05/8.23 cnf(c1874,plain,~coll(X2073,X2073,X2074)|coll(X2074,X2072,X2073),inference(resolution,[status(thm)],[c1775, c402])).
% 8.05/8.23 cnf(c2805,plain,coll(X2083,X2085,X2084),inference(resolution,[status(thm)],[c1874, c1775])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c186,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 8.05/8.23 fof(c187,plain,(![X160]:(![X161]:(![X162]:((~cong(X160,X161,X160,X162)|~coll(X160,X161,X162))|midp(X160,X161,X162))))),inference(variable_rename,[status(thm)],[c186])).
% 8.05/8.23 cnf(c188,plain,~cong(X960,X961,X960,X962)|~coll(X960,X961,X962)|midp(X960,X961,X962),inference(split_conjunct,[status(thm)],[c187])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 8.05/8.23 fof(c339,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c338])).
% 8.05/8.23 cnf(c340,plain,~cong(X617,X614,X616,X615)|cong(X617,X614,X615,X616),inference(split_conjunct,[status(thm)],[c339])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 8.05/8.23 fof(c336,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c335])).
% 8.05/8.23 cnf(c337,plain,~cong(X610,X611,X612,X613)|cong(X612,X613,X610,X611),inference(split_conjunct,[status(thm)],[c336])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c195,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])).
% 8.05/8.23 fof(c196,plain,(![X171]:(![X172]:(![X173]:(![X174]:(![X175]:(((~midp(X175,X171,X172)|~para(X171,X173,X172,X174))|~para(X171,X174,X172,X173))|midp(X175,X173,X174))))))),inference(variable_rename,[status(thm)],[c195])).
% 8.05/8.23 cnf(c197,plain,~midp(X975,X973,X974)|~para(X973,X972,X974,X971)|~para(X973,X971,X974,X972)|midp(X975,X972,X971),inference(split_conjunct,[status(thm)],[c196])).
% 8.05/8.23 cnf(c887,plain,~midp(X1206,X1204,X1205)|~para(X1204,X1203,X1205,X1203)|midp(X1206,X1203,X1203),inference(factor,[status(thm)],[c197])).
% 8.05/8.23 cnf(c1695,plain,~midp(X1953,X1951,X1951)|midp(X1953,X1952,X1952),inference(resolution,[status(thm)],[c1683, c887])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 8.05/8.23 fof(c363,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c362])).
% 8.05/8.23 cnf(c364,plain,~cyclic(X624,X625,X622,X623)|cyclic(X624,X622,X625,X623),inference(split_conjunct,[status(thm)],[c363])).
% 8.05/8.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)).
% 8.05/8.23 fof(c271,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])).
% 8.05/8.23 fof(c272,plain,(![X277]:(![X278]:(![X279]:(![X280]:((~eqangle(X279,X277,X279,X278,X280,X277,X280,X278)|~coll(X279,X280,X278))|cyclic(X277,X278,X279,X280)))))),inference(variable_rename,[status(thm)],[c271])).
% 8.05/8.23 cnf(c273,plain,~eqangle(X1107,X1105,X1107,X1108,X1106,X1105,X1106,X1108)|~coll(X1107,X1106,X1108)|cyclic(X1105,X1108,X1107,X1106),inference(split_conjunct,[status(thm)],[c272])).
% 8.05/8.23 cnf(c1685,plain,eqangle(X1943,X1944,X1941,X1942,X1943,X1944,X1941,X1942),inference(resolution,[status(thm)],[c1683, c285])).
% 8.05/8.23 cnf(c2597,plain,~coll(X2326,X2326,X2324)|cyclic(X2325,X2324,X2326,X2326),inference(resolution,[status(thm)],[c1685, c273])).
% 8.05/8.23 cnf(c2970,plain,cyclic(X2328,X2329,X2327,X2327),inference(resolution,[status(thm)],[c2597, c2805])).
% 8.05/8.23 cnf(c2971,plain,cyclic(X2331,X2330,X2332,X2330),inference(resolution,[status(thm)],[c2970, c364])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c266,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])).
% 8.05/8.23 fof(c267,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)],[c266])).
% 8.05/8.23 fof(c269,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275))|cong(X271,X272,X274,X275)))))))),inference(shift_quantors,[status(thm)],[fof(c268,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((![X276]:(((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275)))|cong(X271,X272,X274,X275))))))),inference(variable_rename,[status(thm)],[c267])).])).
% 8.05/8.23 cnf(c270,plain,~cyclic(X1100,X1099,X1101,X1098)|~cyclic(X1100,X1099,X1101,X1102)|~cyclic(X1100,X1099,X1101,X1103)|~eqangle(X1101,X1100,X1101,X1099,X1103,X1098,X1103,X1102)|cong(X1100,X1099,X1098,X1102),inference(split_conjunct,[status(thm)],[c269])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c344,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])).
% 8.05/8.23 fof(c345,plain,(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(~eqangle(X425,X426,X427,X428,X429,X430,X431,X432)|eqangle(X425,X426,X429,X430,X427,X428,X431,X432)))))))))),inference(variable_rename,[status(thm)],[c344])).
% 8.05/8.23 cnf(c346,plain,~eqangle(X1333,X1328,X1331,X1329,X1335,X1332,X1330,X1334)|eqangle(X1333,X1328,X1335,X1332,X1331,X1329,X1330,X1334),inference(split_conjunct,[status(thm)],[c345])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 8.05/8.23 fof(c398,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c397])).
% 8.05/8.23 cnf(c399,plain,~para(X705,X704,X706,X707)|para(X705,X704,X707,X706),inference(split_conjunct,[status(thm)],[c398])).
% 8.05/8.23 cnf(c1707,plain,para(X1667,X1666,X1666,X1667),inference(resolution,[status(thm)],[c1683, c399])).
% 8.05/8.23 cnf(c1900,plain,eqangle(X2153,X2152,X2150,X2151,X2152,X2153,X2150,X2151),inference(resolution,[status(thm)],[c1707, c285])).
% 8.05/8.23 cnf(c2871,plain,eqangle(X2188,X2190,X2189,X2191,X2188,X2190,X2191,X2189),inference(resolution,[status(thm)],[c1900, c352])).
% 8.05/8.23 cnf(c2910,plain,eqangle(X2244,X2245,X2244,X2245,X2247,X2246,X2246,X2247),inference(resolution,[status(thm)],[c2871, c346])).
% 8.05/8.23 cnf(c2942,plain,~cyclic(X3196,X3196,X3198,X3197)|cong(X3196,X3196,X3197,X3197),inference(resolution,[status(thm)],[c2910, c270])).
% 8.05/8.23 cnf(c3772,plain,cong(X3199,X3199,X3199,X3199),inference(resolution,[status(thm)],[c2942, c2971])).
% 8.05/8.23 cnf(c3781,plain,~coll(X3269,X3269,X3269)|midp(X3269,X3269,X3269),inference(resolution,[status(thm)],[c3772, c188])).
% 8.05/8.23 cnf(c3894,plain,midp(X3270,X3270,X3270),inference(resolution,[status(thm)],[c3781, c2805])).
% 8.05/8.23 cnf(c3910,plain,midp(X3273,X3272,X3272),inference(resolution,[status(thm)],[c3894, c1695])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c238,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])).
% 8.05/8.23 fof(c239,plain,(![X231]:(![X232]:(![X233]:(![X234]:((~perp(X231,X232,X232,X233)|~midp(X234,X231,X233))|cong(X231,X234,X232,X234)))))),inference(variable_rename,[status(thm)],[c238])).
% 8.05/8.23 cnf(c240,plain,~perp(X1047,X1046,X1046,X1044)|~midp(X1045,X1047,X1044)|cong(X1047,X1045,X1046,X1045),inference(split_conjunct,[status(thm)],[c239])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c159,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])).
% 8.05/8.23 fof(c160,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)],[c159])).
% 8.05/8.23 fof(c162,plain,(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:((~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))|perp(X124,X125,X126,X127)))))))))),inference(shift_quantors,[status(thm)],[fof(c161,plain,(![X124]:(![X125]:(![X126]:(![X127]:((![X128]:(![X129]:(![X130]:(![X131]:(~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))))))|perp(X124,X125,X126,X127)))))),inference(variable_rename,[status(thm)],[c160])).])).
% 8.05/8.23 cnf(c163,plain,~eqangle(X925,X930,X926,X931,X929,X924,X927,X928)|~perp(X929,X924,X927,X928)|perp(X925,X930,X926,X931),inference(split_conjunct,[status(thm)],[c162])).
% 8.05/8.23 cnf(c2879,plain,eqangle(X2206,X2205,X2205,X2206,X2207,X2208,X2207,X2208),inference(resolution,[status(thm)],[c1900, c346])).
% 8.05/8.23 cnf(c2915,plain,~perp(X3143,X3144,X3143,X3144)|perp(X3145,X3142,X3142,X3145),inference(resolution,[status(thm)],[c2879, c163])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c224,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])).
% 8.05/8.23 fof(c225,plain,(![X215]:(![X216]:(![X217]:(![X218]:((~cong(X215,X217,X216,X217)|~cong(X215,X218,X216,X218))|perp(X215,X216,X217,X218)))))),inference(variable_rename,[status(thm)],[c224])).
% 8.05/8.23 cnf(c226,plain,~cong(X1023,X1021,X1022,X1021)|~cong(X1023,X1020,X1022,X1020)|perp(X1023,X1022,X1021,X1020),inference(split_conjunct,[status(thm)],[c225])).
% 8.05/8.23 cnf(c914,plain,~cong(X1025,X1026,X1024,X1026)|perp(X1025,X1024,X1026,X1026),inference(factor,[status(thm)],[c226])).
% 8.05/8.23 cnf(c3789,plain,perp(X3219,X3219,X3219,X3219),inference(resolution,[status(thm)],[c3772, c914])).
% 8.05/8.23 cnf(c3826,plain,perp(X3239,X3240,X3240,X3239),inference(resolution,[status(thm)],[c3789, c2915])).
% 8.05/8.23 cnf(c3866,plain,~midp(X4117,X4118,X4118)|cong(X4118,X4117,X4119,X4117),inference(resolution,[status(thm)],[c3826, c240])).
% 8.05/8.23 cnf(c5125,plain,cong(X4122,X4121,X4120,X4121),inference(resolution,[status(thm)],[c3866, c3910])).
% 8.05/8.23 cnf(c5132,plain,cong(X4127,X4126,X4126,X4128),inference(resolution,[status(thm)],[c5125, c340])).
% 8.05/8.23 cnf(c5143,plain,cong(X4134,X4136,X4135,X4134),inference(resolution,[status(thm)],[c5132, c337])).
% 8.05/8.23 cnf(c5172,plain,cong(X4169,X4170,X4169,X4171),inference(resolution,[status(thm)],[c5143, c340])).
% 8.05/8.23 cnf(c5217,plain,~coll(X4336,X4337,X4335)|midp(X4336,X4337,X4335),inference(resolution,[status(thm)],[c5172, c188])).
% 8.05/8.23 cnf(c5481,plain,midp(X4339,X4338,X4340),inference(resolution,[status(thm)],[c5217, c2805])).
% 8.05/8.23 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)).
% 8.05/8.23 fof(c263,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])).
% 8.05/8.23 fof(c264,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c263])).
% 8.05/8.23 cnf(c265,plain,~midp(X1092,X1093,X1091)|~midp(X1090,X1093,X1089)|para(X1092,X1090,X1091,X1089),inference(split_conjunct,[status(thm)],[c264])).
% 8.05/8.23 cnf(c3915,plain,~midp(X7632,X7633,X7631)|para(X7632,X7634,X7631,X7633),inference(resolution,[status(thm)],[c3910, c265])).
% 8.05/8.23 cnf(c8398,plain,para(X7635,X7638,X7637,X7636),inference(resolution,[status(thm)],[c3915, c5481])).
% 8.05/8.23 fof(ruleD10,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)&perp(C,D,E,F))=>perp(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 8.05/8.23 fof(c379,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~perp(C,D,E,F))|perp(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD10])).
% 8.05/8.23 fof(c380,plain,(![X486]:(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:((~para(X486,X487,X488,X489)|~perp(X488,X489,X490,X491))|perp(X486,X487,X490,X491)))))))),inference(variable_rename,[status(thm)],[c379])).
% 8.05/8.23 cnf(c381,plain,~para(X1263,X1265,X1264,X1261)|~perp(X1264,X1261,X1262,X1260)|perp(X1263,X1265,X1262,X1260),inference(split_conjunct,[status(thm)],[c380])).
% 8.05/8.23 cnf(c2596,plain,eqangle(X2182,X2183,X2182,X2183,X2184,X2185,X2184,X2185),inference(resolution,[status(thm)],[c1685, c346])).
% 8.05/8.23 cnf(c2887,plain,~perp(X3116,X3117,X3116,X3117)|perp(X3115,X3118,X3115,X3118),inference(resolution,[status(thm)],[c2596, c163])).
% 8.05/8.23 cnf(c3821,plain,perp(X3237,X3236,X3237,X3236),inference(resolution,[status(thm)],[c3789, c2887])).
% 8.05/8.23 cnf(c3846,plain,~para(X9706,X9708,X9709,X9707)|perp(X9706,X9708,X9709,X9707),inference(resolution,[status(thm)],[c3821, c381])).
% 8.05/8.23 cnf(c9152,plain,perp(X9712,X9710,X9713,X9711),inference(resolution,[status(thm)],[c3846, c8398])).
% 8.05/8.23 cnf(c9154,plain,$false,inference(resolution,[status(thm)],[c9152, c23])).
% 8.05/8.23 % SZS output end CNFRefutation
% 8.05/8.23
% 8.05/8.23 % Initial clauses : 135
% 8.05/8.23 % Processed clauses : 1159
% 8.05/8.23 % Factors computed : 130
% 8.05/8.23 % Resolvents computed: 8616
% 8.05/8.23 % Tautologies deleted: 27
% 8.05/8.23 % Forward subsumed : 3644
% 8.05/8.23 % Backward subsumed : 988
% 8.05/8.23 % -------- CPU Time ---------
% 8.05/8.23 % User time : 7.857 s
% 8.05/8.23 % System time : 0.029 s
% 8.05/8.23 % Total time : 7.886 s
%------------------------------------------------------------------------------