%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO572+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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 12.38s 12.58s
% Output : Refutation 12.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO572+1 : TPTP v8.1.2. Released v7.5.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n025.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:43:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 12.38/12.58 % Version: 1.5
% 12.38/12.58 % SZS status Theorem
% 12.38/12.58 % SZS output start CNFRefutation
% 12.38/12.58 fof(exemplo6GDDFULL214034,conjecture,(![A]:(![B]:(![C]:(![H]:(![O]:(![P]:(![NWPNT1]:((((((perp(A,B,C,H)&perp(A,C,B,H))&perp(B,C,A,H))&perp(C,H,H,P))&circle(O,H,B,C))&circle(O,B,P,NWPNT1))=>para(A,H,B,P))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214034)).
% 12.38/12.58 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![H]:(![O]:(![P]:(![NWPNT1]:((((((perp(A,B,C,H)&perp(A,C,B,H))&perp(B,C,A,H))&perp(C,H,H,P))&circle(O,H,B,C))&circle(O,B,P,NWPNT1))=>para(A,H,B,P)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214034])).
% 12.38/12.58 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[H]:(?[O]:(?[P]:(?[NWPNT1]:((((((perp(A,B,C,H)&perp(A,C,B,H))&perp(B,C,A,H))&perp(C,H,H,P))&circle(O,H,B,C))&circle(O,B,P,NWPNT1))&~para(A,H,B,P))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 12.38/12.58 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[H]:(?[O]:(?[P]:((((((perp(A,B,C,H)&perp(A,C,B,H))&perp(B,C,A,H))&perp(C,H,H,P))&circle(O,H,B,C))&(?[NWPNT1]:circle(O,B,P,NWPNT1)))&~para(A,H,B,P)))))))),inference(shift_quantors,[status(thm)],[c12])).
% 12.38/12.58 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:((((((perp(X2,X3,X4,X5)&perp(X2,X4,X3,X5))&perp(X3,X4,X2,X5))&perp(X4,X5,X5,X7))&circle(X6,X5,X3,X4))&(?[X8]:circle(X6,X3,X7,X8)))&~para(X2,X5,X3,X7)))))))),inference(variable_rename,[status(thm)],[c13])).
% 12.38/12.58 fof(c15,negated_conjecture,((((((perp(skolem0001,skolem0002,skolem0003,skolem0004)&perp(skolem0001,skolem0003,skolem0002,skolem0004))&perp(skolem0002,skolem0003,skolem0001,skolem0004))&perp(skolem0003,skolem0004,skolem0004,skolem0006))&circle(skolem0005,skolem0004,skolem0002,skolem0003))&circle(skolem0005,skolem0002,skolem0006,skolem0007))&~para(skolem0001,skolem0004,skolem0002,skolem0006)),inference(skolemize,[status(esa)],[c14])).
% 12.38/12.58 cnf(c22,negated_conjecture,~para(skolem0001,skolem0004,skolem0002,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 12.38/12.58 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)).
% 12.38/12.58 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])).
% 12.38/12.58 fof(c400,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c399])).
% 12.38/12.58 cnf(c401,plain,~coll(X737,X736,X739)|~coll(X737,X736,X738)|coll(X739,X738,X737),inference(split_conjunct,[status(thm)],[c400])).
% 12.38/12.58 cnf(c518,plain,~coll(X740,X741,X742)|coll(X742,X742,X740),inference(factor,[status(thm)],[c401])).
% 12.38/12.58 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)).
% 12.38/12.58 fof(c188,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 12.38/12.58 fof(c189,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c188])).
% 12.38/12.58 cnf(c190,plain,~para(X571,X569,X571,X570)|coll(X571,X569,X570),inference(split_conjunct,[status(thm)],[c189])).
% 12.38/12.58 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)).
% 12.38/12.58 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])).
% 12.38/12.58 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])).
% 12.38/12.58 fof(c288,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(c287,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)],[c286])).])).
% 12.38/12.58 cnf(c289,plain,~eqangle(X784,X785,X789,X788,X786,X787,X789,X788)|para(X784,X785,X786,X787),inference(split_conjunct,[status(thm)],[c288])).
% 12.38/12.58 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)).
% 12.38/12.58 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])).
% 12.38/12.58 fof(c350,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)],[c349])).
% 12.38/12.58 cnf(c351,plain,~eqangle(X1270,X1273,X1274,X1271,X1275,X1272,X1276,X1277)|eqangle(X1274,X1271,X1270,X1273,X1276,X1277,X1275,X1272),inference(split_conjunct,[status(thm)],[c350])).
% 12.38/12.58 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)).
% 12.38/12.58 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])).
% 12.38/12.58 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])).
% 12.38/12.58 fof(c283,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(c282,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)],[c281])).])).
% 12.38/12.58 cnf(c284,plain,~para(X781,X779,X783,X778)|eqangle(X781,X779,X780,X782,X783,X778,X780,X782),inference(split_conjunct,[status(thm)],[c283])).
% 12.38/12.58 cnf(c19,negated_conjecture,perp(skolem0003,skolem0004,skolem0004,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 12.38/12.58 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)).
% 12.38/12.58 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 12.38/12.58 fof(c388,plain,(![X502]:(![X503]:(![X504]:(![X505]:(~perp(X502,X503,X504,X505)|perp(X502,X503,X505,X504)))))),inference(variable_rename,[status(thm)],[c387])).
% 12.38/12.58 cnf(c389,plain,~perp(X620,X618,X619,X621)|perp(X620,X618,X621,X619),inference(split_conjunct,[status(thm)],[c388])).
% 12.38/12.58 cnf(c434,plain,perp(skolem0003,skolem0004,skolem0006,skolem0004),inference(resolution,[status(thm)],[c389, c19])).
% 12.38/12.58 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)).
% 12.38/12.58 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 12.38/12.58 fof(c385,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c384])).
% 12.38/12.58 cnf(c386,plain,~perp(X603,X601,X600,X602)|perp(X600,X602,X603,X601),inference(split_conjunct,[status(thm)],[c385])).
% 12.38/12.58 cnf(c452,plain,perp(skolem0006,skolem0004,skolem0003,skolem0004),inference(resolution,[status(thm)],[c434, c386])).
% 12.38/12.58 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)).
% 12.38/12.58 fof(c381,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])).
% 12.38/12.58 fof(c382,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)],[c381])).
% 12.38/12.58 cnf(c383,plain,~perp(X1294,X1292,X1293,X1291)|~perp(X1293,X1291,X1295,X1296)|para(X1294,X1292,X1295,X1296),inference(split_conjunct,[status(thm)],[c382])).
% 12.38/12.58 cnf(c1220,plain,~perp(X1540,X1539,skolem0006,skolem0004)|para(X1540,X1539,skolem0003,skolem0004),inference(resolution,[status(thm)],[c383, c452])).
% 12.38/12.59 cnf(c2008,plain,para(skolem0003,skolem0004,skolem0003,skolem0004),inference(resolution,[status(thm)],[c1220, c434])).
% 12.38/12.59 cnf(c2041,plain,eqangle(skolem0003,skolem0004,X1544,X1545,skolem0003,skolem0004,X1544,X1545),inference(resolution,[status(thm)],[c2008, c284])).
% 12.38/12.59 cnf(c2115,plain,eqangle(X1565,X1566,skolem0003,skolem0004,X1565,X1566,skolem0003,skolem0004),inference(resolution,[status(thm)],[c2041, c351])).
% 12.38/12.59 cnf(c2208,plain,para(X1567,X1568,X1567,X1568),inference(resolution,[status(thm)],[c2115, c289])).
% 12.38/12.59 cnf(c2227,plain,coll(X1570,X1569,X1569),inference(resolution,[status(thm)],[c2208, c190])).
% 12.38/12.59 cnf(c2270,plain,coll(X1575,X1575,X1576),inference(resolution,[status(thm)],[c2227, c518])).
% 12.38/12.59 cnf(c2320,plain,~coll(X1688,X1688,X1690)|coll(X1690,X1689,X1688),inference(resolution,[status(thm)],[c2270, c401])).
% 12.38/12.59 cnf(c2585,plain,coll(X1693,X1691,X1692),inference(resolution,[status(thm)],[c2320, c2270])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c185,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 12.38/12.59 fof(c186,plain,(![X160]:(![X161]:(![X162]:((~cong(X160,X161,X160,X162)|~coll(X160,X161,X162))|midp(X160,X161,X162))))),inference(variable_rename,[status(thm)],[c185])).
% 12.38/12.59 cnf(c187,plain,~cong(X743,X744,X743,X745)|~coll(X743,X744,X745)|midp(X743,X744,X745),inference(split_conjunct,[status(thm)],[c186])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 12.38/12.59 fof(c338,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c337])).
% 12.38/12.59 cnf(c339,plain,~cong(X576,X578,X579,X577)|cong(X576,X578,X577,X579),inference(split_conjunct,[status(thm)],[c338])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 12.38/12.59 fof(c335,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c334])).
% 12.38/12.59 cnf(c336,plain,~cong(X572,X573,X574,X575)|cong(X574,X575,X572,X573),inference(split_conjunct,[status(thm)],[c335])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c194,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])).
% 12.38/12.59 fof(c195,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)],[c194])).
% 12.38/12.59 cnf(c196,plain,~midp(X1101,X1099,X1100)|~para(X1099,X1102,X1100,X1098)|~para(X1099,X1098,X1100,X1102)|midp(X1101,X1102,X1098),inference(split_conjunct,[status(thm)],[c195])).
% 12.38/12.59 cnf(c1035,plain,~midp(X1529,X1530,X1531)|~para(X1530,X1532,X1531,X1532)|midp(X1529,X1532,X1532),inference(factor,[status(thm)],[c196])).
% 12.38/12.59 cnf(c2233,plain,~midp(X1649,X1650,X1650)|midp(X1649,X1651,X1651),inference(resolution,[status(thm)],[c2208, c1035])).
% 12.38/12.59 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)).
% 12.38/12.59 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])).
% 12.38/12.59 fof(c271,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)],[c270])).
% 12.38/12.59 cnf(c272,plain,~eqangle(X1169,X1171,X1169,X1170,X1172,X1171,X1172,X1170)|~coll(X1169,X1172,X1170)|cyclic(X1171,X1170,X1169,X1172),inference(split_conjunct,[status(thm)],[c271])).
% 12.38/12.59 cnf(c2246,plain,eqangle(X1653,X1654,X1652,X1655,X1653,X1654,X1652,X1655),inference(resolution,[status(thm)],[c2208, c284])).
% 12.38/12.59 cnf(c2542,plain,~coll(X1877,X1877,X1876)|cyclic(X1878,X1876,X1877,X1877),inference(resolution,[status(thm)],[c2246, c272])).
% 12.38/12.59 cnf(c2878,plain,cyclic(X1881,X1880,X1879,X1879),inference(resolution,[status(thm)],[c2542, c2585])).
% 12.38/12.59 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)).
% 12.38/12.59 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(fof_nnf,[status(thm)],[ruleD43])).
% 12.38/12.59 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(shift_quantors,[status(thm)],[c265])).
% 12.38/12.59 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(shift_quantors,[status(thm)],[fof(c267,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)],[c266])).])).
% 12.38/12.59 cnf(c269,plain,~cyclic(X1165,X1164,X1162,X1167)|~cyclic(X1165,X1164,X1162,X1163)|~cyclic(X1165,X1164,X1162,X1166)|~eqangle(X1162,X1165,X1162,X1164,X1166,X1167,X1166,X1163)|cong(X1165,X1164,X1167,X1163),inference(split_conjunct,[status(thm)],[c268])).
% 12.38/12.59 fof(ruleD20,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(P,Q,U,V,A,B,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 12.38/12.59 fof(c346,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(P,Q,U,V,A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD20])).
% 12.38/12.59 fof(c347,plain,(![X433]:(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(~eqangle(X433,X434,X435,X436,X437,X438,X439,X440)|eqangle(X437,X438,X439,X440,X433,X434,X435,X436)))))))))),inference(variable_rename,[status(thm)],[c346])).
% 12.38/12.59 cnf(c348,plain,~eqangle(X1269,X1266,X1264,X1262,X1267,X1265,X1268,X1263)|eqangle(X1267,X1265,X1268,X1263,X1269,X1266,X1264,X1262),inference(split_conjunct,[status(thm)],[c347])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c343,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])).
% 12.38/12.59 fof(c344,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)],[c343])).
% 12.38/12.59 cnf(c345,plain,~eqangle(X1257,X1256,X1254,X1259,X1260,X1261,X1255,X1258)|eqangle(X1257,X1256,X1260,X1261,X1254,X1259,X1255,X1258),inference(split_conjunct,[status(thm)],[c344])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 12.38/12.59 fof(c397,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c396])).
% 12.38/12.59 cnf(c398,plain,~para(X726,X728,X727,X729)|para(X726,X728,X729,X727),inference(split_conjunct,[status(thm)],[c397])).
% 12.38/12.59 cnf(c2219,plain,para(X1589,X1588,X1588,X1589),inference(resolution,[status(thm)],[c2208, c398])).
% 12.38/12.59 cnf(c2365,plain,eqangle(X1718,X1717,X1716,X1719,X1717,X1718,X1716,X1719),inference(resolution,[status(thm)],[c2219, c284])).
% 12.38/12.59 cnf(c2614,plain,eqangle(X1753,X1754,X1754,X1753,X1755,X1756,X1755,X1756),inference(resolution,[status(thm)],[c2365, c345])).
% 12.38/12.59 cnf(c2668,plain,eqangle(X1791,X1793,X1791,X1793,X1792,X1794,X1794,X1792),inference(resolution,[status(thm)],[c2614, c348])).
% 12.38/12.59 cnf(c2723,plain,~cyclic(X2553,X2553,X2552,X2554)|cong(X2553,X2553,X2554,X2554),inference(resolution,[status(thm)],[c2668, c269])).
% 12.38/12.59 cnf(c3448,plain,cong(X2556,X2556,X2555,X2555),inference(resolution,[status(thm)],[c2723, c2878])).
% 12.38/12.59 cnf(c3465,plain,~coll(X2595,X2595,X2595)|midp(X2595,X2595,X2595),inference(resolution,[status(thm)],[c3448, c187])).
% 12.38/12.59 cnf(c3543,plain,midp(X2596,X2596,X2596),inference(resolution,[status(thm)],[c3465, c2585])).
% 12.38/12.59 cnf(c3555,plain,midp(X2599,X2598,X2598),inference(resolution,[status(thm)],[c3543, c2233])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c237,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])).
% 12.38/12.59 fof(c238,plain,(![X231]:(![X232]:(![X233]:(![X234]:((~perp(X231,X232,X232,X233)|~midp(X234,X231,X233))|cong(X231,X234,X232,X234)))))),inference(variable_rename,[status(thm)],[c237])).
% 12.38/12.59 cnf(c239,plain,~perp(X850,X852,X852,X851)|~midp(X849,X850,X851)|cong(X850,X849,X852,X849),inference(split_conjunct,[status(thm)],[c238])).
% 12.38/12.59 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)).
% 12.38/12.59 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(fof_nnf,[status(thm)],[ruleD74])).
% 12.38/12.59 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(shift_quantors,[status(thm)],[c158])).
% 12.38/12.59 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(shift_quantors,[status(thm)],[fof(c160,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)],[c159])).])).
% 12.38/12.59 cnf(c162,plain,~eqangle(X1058,X1063,X1065,X1061,X1060,X1064,X1059,X1062)|~perp(X1060,X1064,X1059,X1062)|perp(X1058,X1063,X1065,X1061),inference(split_conjunct,[status(thm)],[c161])).
% 12.38/12.59 cnf(c2663,plain,~perp(X2532,X2529,X2532,X2529)|perp(X2531,X2530,X2530,X2531),inference(resolution,[status(thm)],[c2614, c162])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c223,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])).
% 12.38/12.59 fof(c224,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)],[c223])).
% 12.38/12.59 cnf(c225,plain,~cong(X874,X873,X876,X873)|~cong(X874,X875,X876,X875)|perp(X874,X876,X873,X875),inference(split_conjunct,[status(thm)],[c224])).
% 12.38/12.59 cnf(c563,plain,~cong(X879,X878,X877,X878)|perp(X879,X877,X878,X878),inference(factor,[status(thm)],[c225])).
% 12.38/12.59 cnf(c3463,plain,perp(X2570,X2570,X2570,X2570),inference(resolution,[status(thm)],[c3448, c563])).
% 12.38/12.59 cnf(c3476,plain,perp(X2573,X2574,X2574,X2573),inference(resolution,[status(thm)],[c3463, c2663])).
% 12.38/12.59 cnf(c3510,plain,~midp(X3359,X3357,X3357)|cong(X3357,X3359,X3358,X3359),inference(resolution,[status(thm)],[c3476, c239])).
% 12.38/12.59 cnf(c4820,plain,cong(X3361,X3360,X3362,X3360),inference(resolution,[status(thm)],[c3510, c3555])).
% 12.38/12.59 cnf(c4826,plain,cong(X3370,X3369,X3369,X3368),inference(resolution,[status(thm)],[c4820, c339])).
% 12.38/12.59 cnf(c4848,plain,cong(X3388,X3386,X3387,X3388),inference(resolution,[status(thm)],[c4826, c336])).
% 12.38/12.59 cnf(c4885,plain,cong(X3405,X3406,X3405,X3407),inference(resolution,[status(thm)],[c4848, c339])).
% 12.38/12.59 cnf(c4933,plain,~coll(X3539,X3540,X3541)|midp(X3539,X3540,X3541),inference(resolution,[status(thm)],[c4885, c187])).
% 12.38/12.59 cnf(c5180,plain,midp(X3542,X3544,X3543),inference(resolution,[status(thm)],[c4933, c2585])).
% 12.38/12.59 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)).
% 12.38/12.59 fof(c262,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])).
% 12.38/12.59 fof(c263,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c262])).
% 12.38/12.59 cnf(c264,plain,~midp(X762,X764,X763)|~midp(X766,X764,X765)|para(X762,X766,X763,X765),inference(split_conjunct,[status(thm)],[c263])).
% 12.38/12.59 cnf(c3565,plain,~midp(X8054,X8052,X8053)|para(X8054,X8051,X8053,X8052),inference(resolution,[status(thm)],[c3555, c264])).
% 12.38/12.59 cnf(c12010,plain,para(X8057,X8055,X8056,X8058),inference(resolution,[status(thm)],[c3565, c5180])).
% 12.38/12.59 cnf(c12016,plain,$false,inference(resolution,[status(thm)],[c12010, c22])).
% 12.38/12.59 % SZS output end CNFRefutation
% 12.38/12.59
% 12.38/12.59 % Initial clauses : 134
% 12.38/12.59 % Processed clauses : 1426
% 12.38/12.59 % Factors computed : 45
% 12.38/12.59 % Resolvents computed: 11597
% 12.38/12.59 % Tautologies deleted: 15
% 12.38/12.59 % Forward subsumed : 4598
% 12.38/12.59 % Backward subsumed : 842
% 12.38/12.59 % -------- CPU Time ---------
% 12.38/12.59 % User time : 12.207 s
% 12.38/12.59 % System time : 0.028 s
% 12.38/12.59 % Total time : 12.235 s
%------------------------------------------------------------------------------