%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO645+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:29 EDT 2024
% Result : Theorem 82.03s 82.23s
% Output : Refutation 82.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO645+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n009.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 07:59:22 EDT 2024
% 0.14/0.34 % CPUTime :
% 82.03/82.23 % Version: 1.5
% 82.03/82.23 % SZS status Theorem
% 82.03/82.23 % SZS output start CNFRefutation
% 82.03/82.23 fof(exemplo6GDDFULLmoreE0091,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(((((((perp(A,C,C,B)&perp(A,D,D,B))&circle(A,C,D,NWPNT1))&coll(E,B,C))&circle(A,B,E,NWPNT2))&coll(F,B,D))&circle(A,B,F,NWPNT3))=>para(C,D,E,F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE0091)).
% 82.03/82.23 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(((((((perp(A,C,C,B)&perp(A,D,D,B))&circle(A,C,D,NWPNT1))&coll(E,B,C))&circle(A,B,E,NWPNT2))&coll(F,B,D))&circle(A,B,F,NWPNT3))=>para(C,D,E,F)))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE0091])).
% 82.03/82.23 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(((((((perp(A,C,C,B)&perp(A,D,D,B))&circle(A,C,D,NWPNT1))&coll(E,B,C))&circle(A,B,E,NWPNT2))&coll(F,B,D))&circle(A,B,F,NWPNT3))&~para(C,D,E,F))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 82.03/82.23 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(((((((perp(A,C,C,B)&perp(A,D,D,B))&(?[NWPNT1]:circle(A,C,D,NWPNT1)))&coll(E,B,C))&(?[NWPNT2]:circle(A,B,E,NWPNT2)))&coll(F,B,D))&(?[NWPNT3]:circle(A,B,F,NWPNT3)))&~para(C,D,E,F)))))))),inference(shift_quantors,[status(thm)],[c12])).
% 82.03/82.23 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((((perp(X2,X4,X4,X3)&perp(X2,X5,X5,X3))&(?[X8]:circle(X2,X4,X5,X8)))&coll(X6,X3,X4))&(?[X9]:circle(X2,X3,X6,X9)))&coll(X7,X3,X5))&(?[X10]:circle(X2,X3,X7,X10)))&~para(X4,X5,X6,X7)))))))),inference(variable_rename,[status(thm)],[c13])).
% 82.03/82.23 fof(c15,negated_conjecture,(((((((perp(skolem0001,skolem0003,skolem0003,skolem0002)&perp(skolem0001,skolem0004,skolem0004,skolem0002))&circle(skolem0001,skolem0003,skolem0004,skolem0007))&coll(skolem0005,skolem0002,skolem0003))&circle(skolem0001,skolem0002,skolem0005,skolem0008))&coll(skolem0006,skolem0002,skolem0004))&circle(skolem0001,skolem0002,skolem0006,skolem0009))&~para(skolem0003,skolem0004,skolem0005,skolem0006)),inference(skolemize,[status(esa)],[c14])).
% 82.03/82.23 cnf(c23,negated_conjecture,~para(skolem0003,skolem0004,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 82.03/82.23 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 82.03/82.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])).
% 82.03/82.23 fof(c401,plain,(![X522]:(![X523]:(![X524]:(![X525]:((~coll(X522,X523,X524)|~coll(X522,X523,X525))|coll(X524,X525,X522)))))),inference(variable_rename,[status(thm)],[c400])).
% 82.03/82.23 cnf(c402,plain,~coll(X735,X736,X734)|~coll(X735,X736,X733)|coll(X734,X733,X735),inference(split_conjunct,[status(thm)],[c401])).
% 82.03/82.23 cnf(c512,plain,~coll(X739,X737,X738)|coll(X738,X738,X739),inference(factor,[status(thm)],[c402])).
% 82.03/82.23 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 82.03/82.23 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 82.03/82.23 fof(c190,plain,(![X165]:(![X166]:(![X167]:(~para(X165,X166,X165,X167)|coll(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c189])).
% 82.03/82.23 cnf(c191,plain,~para(X611,X610,X611,X609)|coll(X611,X610,X609),inference(split_conjunct,[status(thm)],[c190])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 82.03/82.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])).
% 82.03/82.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])).
% 82.03/82.23 fof(c289,plain,(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(![X302]:(~eqangle(X297,X298,X301,X302,X299,X300,X301,X302)|para(X297,X298,X299,X300)))))))),inference(shift_quantors,[status(thm)],[fof(c288,plain,(![X297]:(![X298]:(![X299]:(![X300]:((![X301]:(![X302]:~eqangle(X297,X298,X301,X302,X299,X300,X301,X302)))|para(X297,X298,X299,X300)))))),inference(variable_rename,[status(thm)],[c287])).])).
% 82.03/82.23 cnf(c290,plain,~eqangle(X1079,X1080,X1078,X1075,X1076,X1077,X1078,X1075)|para(X1079,X1080,X1076,X1077),inference(split_conjunct,[status(thm)],[c289])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 82.03/82.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])).
% 82.03/82.23 fof(c351,plain,(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(~eqangle(X443,X444,X445,X446,X447,X448,X449,X450)|eqangle(X445,X446,X443,X444,X449,X450,X447,X448)))))))))),inference(variable_rename,[status(thm)],[c350])).
% 82.03/82.23 cnf(c352,plain,~eqangle(X1213,X1214,X1216,X1217,X1215,X1218,X1219,X1220)|eqangle(X1216,X1217,X1213,X1214,X1219,X1220,X1215,X1218),inference(split_conjunct,[status(thm)],[c351])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 82.03/82.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])).
% 82.03/82.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])).
% 82.03/82.23 fof(c284,plain,(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(![X296]:(~para(X291,X292,X293,X294)|eqangle(X291,X292,X295,X296,X293,X294,X295,X296)))))))),inference(shift_quantors,[status(thm)],[fof(c283,plain,(![X291]:(![X292]:(![X293]:(![X294]:(~para(X291,X292,X293,X294)|(![X295]:(![X296]:eqangle(X291,X292,X295,X296,X293,X294,X295,X296)))))))),inference(variable_rename,[status(thm)],[c282])).])).
% 82.03/82.23 cnf(c285,plain,~para(X1073,X1074,X1071,X1072)|eqangle(X1073,X1074,X1070,X1069,X1071,X1072,X1070,X1069),inference(split_conjunct,[status(thm)],[c284])).
% 82.03/82.23 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 82.03/82.23 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 82.03/82.23 fof(c386,plain,(![X500]:(![X501]:(![X502]:(![X503]:(~perp(X500,X501,X502,X503)|perp(X502,X503,X500,X501)))))),inference(variable_rename,[status(thm)],[c385])).
% 82.03/82.23 cnf(c387,plain,~perp(X650,X649,X651,X648)|perp(X651,X648,X650,X649),inference(split_conjunct,[status(thm)],[c386])).
% 82.03/82.23 cnf(c17,negated_conjecture,perp(skolem0001,skolem0004,skolem0004,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 82.03/82.23 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 82.03/82.23 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 82.03/82.23 fof(c389,plain,(![X504]:(![X505]:(![X506]:(![X507]:(~perp(X504,X505,X506,X507)|perp(X504,X505,X507,X506)))))),inference(variable_rename,[status(thm)],[c388])).
% 82.03/82.23 cnf(c390,plain,~perp(X668,X669,X670,X671)|perp(X668,X669,X671,X670),inference(split_conjunct,[status(thm)],[c389])).
% 82.03/82.23 cnf(c462,plain,perp(skolem0001,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c390, c17])).
% 82.03/82.23 cnf(c473,plain,perp(skolem0002,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c462, c387])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 82.03/82.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])).
% 82.03/82.23 fof(c383,plain,(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:(![X499]:((~perp(X494,X495,X496,X497)|~perp(X496,X497,X498,X499))|para(X494,X495,X498,X499)))))))),inference(variable_rename,[status(thm)],[c382])).
% 82.03/82.23 cnf(c384,plain,~perp(X1272,X1273,X1271,X1274)|~perp(X1271,X1274,X1270,X1269)|para(X1272,X1273,X1270,X1269),inference(split_conjunct,[status(thm)],[c383])).
% 82.03/82.23 cnf(c1470,plain,~perp(X2624,X2623,skolem0001,skolem0004)|para(X2624,X2623,skolem0002,skolem0004),inference(resolution,[status(thm)],[c384, c462])).
% 82.03/82.23 cnf(c7676,plain,para(skolem0002,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c1470, c473])).
% 82.03/82.23 cnf(c7690,plain,eqangle(skolem0002,skolem0004,X2823,X2824,skolem0002,skolem0004,X2823,X2824),inference(resolution,[status(thm)],[c7676, c285])).
% 82.03/82.23 cnf(c11744,plain,eqangle(X3298,X3299,skolem0002,skolem0004,X3298,X3299,skolem0002,skolem0004),inference(resolution,[status(thm)],[c7690, c352])).
% 82.03/82.23 cnf(c18021,plain,para(X3301,X3300,X3301,X3300),inference(resolution,[status(thm)],[c11744, c290])).
% 82.03/82.23 cnf(c18043,plain,coll(X3303,X3302,X3302),inference(resolution,[status(thm)],[c18021, c191])).
% 82.03/82.23 cnf(c18209,plain,coll(X3305,X3305,X3304),inference(resolution,[status(thm)],[c18043, c512])).
% 82.03/82.23 cnf(c18413,plain,~coll(X4000,X4000,X3999)|coll(X3999,X4001,X4000),inference(resolution,[status(thm)],[c18209, c402])).
% 82.03/82.23 cnf(c23729,plain,coll(X4008,X4006,X4007),inference(resolution,[status(thm)],[c18413, c18209])).
% 82.03/82.23 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 82.03/82.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])).
% 82.03/82.23 fof(c187,plain,(![X162]:(![X163]:(![X164]:((~cong(X162,X163,X162,X164)|~coll(X162,X163,X164))|midp(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c186])).
% 82.03/82.23 cnf(c188,plain,~cong(X951,X949,X951,X950)|~coll(X951,X949,X950)|midp(X951,X949,X950),inference(split_conjunct,[status(thm)],[c187])).
% 82.03/82.23 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 82.03/82.23 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 82.03/82.23 fof(c339,plain,(![X411]:(![X412]:(![X413]:(![X414]:(~cong(X411,X412,X413,X414)|cong(X411,X412,X414,X413)))))),inference(variable_rename,[status(thm)],[c338])).
% 82.03/82.23 cnf(c340,plain,~cong(X619,X617,X616,X618)|cong(X619,X617,X618,X616),inference(split_conjunct,[status(thm)],[c339])).
% 82.03/82.23 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 82.03/82.23 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 82.03/82.23 fof(c336,plain,(![X407]:(![X408]:(![X409]:(![X410]:(~cong(X407,X408,X409,X410)|cong(X409,X410,X407,X408)))))),inference(variable_rename,[status(thm)],[c335])).
% 82.03/82.23 cnf(c337,plain,~cong(X614,X612,X615,X613)|cong(X615,X613,X614,X612),inference(split_conjunct,[status(thm)],[c336])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 82.03/82.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])).
% 82.03/82.23 fof(c196,plain,(![X173]:(![X174]:(![X175]:(![X176]:(![X177]:(((~midp(X177,X173,X174)|~para(X173,X175,X174,X176))|~para(X173,X176,X174,X175))|midp(X177,X175,X176))))))),inference(variable_rename,[status(thm)],[c195])).
% 82.03/82.23 cnf(c197,plain,~midp(X958,X960,X959)|~para(X960,X957,X959,X961)|~para(X960,X961,X959,X957)|midp(X958,X957,X961),inference(split_conjunct,[status(thm)],[c196])).
% 82.03/82.23 cnf(c992,plain,~midp(X2019,X2020,X2018)|~para(X2020,X2021,X2018,X2021)|midp(X2019,X2021,X2021),inference(factor,[status(thm)],[c197])).
% 82.03/82.23 cnf(c18054,plain,~midp(X3873,X3874,X3874)|midp(X3873,X3872,X3872),inference(resolution,[status(thm)],[c18021, c992])).
% 82.03/82.23 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 82.03/82.23 fof(c365,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 82.03/82.23 fof(c366,plain,(![X472]:(![X473]:(![X474]:(![X475]:(~cyclic(X472,X473,X474,X475)|cyclic(X472,X473,X475,X474)))))),inference(variable_rename,[status(thm)],[c365])).
% 82.03/82.23 cnf(c367,plain,~cyclic(X646,X644,X647,X645)|cyclic(X646,X644,X645,X647),inference(split_conjunct,[status(thm)],[c366])).
% 82.03/82.23 fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 82.03/82.23 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 82.03/82.23 fof(c363,plain,(![X468]:(![X469]:(![X470]:(![X471]:(~cyclic(X468,X469,X470,X471)|cyclic(X468,X470,X469,X471)))))),inference(variable_rename,[status(thm)],[c362])).
% 82.03/82.23 cnf(c364,plain,~cyclic(X642,X643,X641,X640)|cyclic(X642,X641,X643,X640),inference(split_conjunct,[status(thm)],[c363])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 82.03/82.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])).
% 82.03/82.23 fof(c272,plain,(![X279]:(![X280]:(![X281]:(![X282]:((~eqangle(X281,X279,X281,X280,X282,X279,X282,X280)|~coll(X281,X282,X280))|cyclic(X279,X280,X281,X282)))))),inference(variable_rename,[status(thm)],[c271])).
% 82.03/82.23 cnf(c273,plain,~eqangle(X1058,X1060,X1058,X1059,X1057,X1060,X1057,X1059)|~coll(X1058,X1057,X1059)|cyclic(X1060,X1059,X1058,X1057),inference(split_conjunct,[status(thm)],[c272])).
% 82.03/82.23 cnf(c18044,plain,eqangle(X3867,X3868,X3869,X3866,X3867,X3868,X3869,X3866),inference(resolution,[status(thm)],[c18021, c285])).
% 82.03/82.23 cnf(c23450,plain,~coll(X4293,X4293,X4294)|cyclic(X4292,X4294,X4293,X4293),inference(resolution,[status(thm)],[c18044, c273])).
% 82.03/82.23 cnf(c24389,plain,cyclic(X4295,X4296,X4297,X4297),inference(resolution,[status(thm)],[c23450, c23729])).
% 82.03/82.23 cnf(c24396,plain,cyclic(X4308,X4309,X4310,X4309),inference(resolution,[status(thm)],[c24389, c364])).
% 82.03/82.23 cnf(c24402,plain,cyclic(X4314,X4315,X4315,X4316),inference(resolution,[status(thm)],[c24396, c367])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 82.03/82.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])).
% 82.03/82.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])).
% 82.03/82.23 fof(c269,plain,(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:(![X278]:((((~cyclic(X273,X274,X275,X276)|~cyclic(X273,X274,X275,X277))|~cyclic(X273,X274,X275,X278))|~eqangle(X275,X273,X275,X274,X278,X276,X278,X277))|cong(X273,X274,X276,X277)))))))),inference(shift_quantors,[status(thm)],[fof(c268,plain,(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((![X278]:(((~cyclic(X273,X274,X275,X276)|~cyclic(X273,X274,X275,X277))|~cyclic(X273,X274,X275,X278))|~eqangle(X275,X273,X275,X274,X278,X276,X278,X277)))|cong(X273,X274,X276,X277))))))),inference(variable_rename,[status(thm)],[c267])).])).
% 82.03/82.23 cnf(c270,plain,~cyclic(X1054,X1051,X1056,X1055)|~cyclic(X1054,X1051,X1056,X1053)|~cyclic(X1054,X1051,X1056,X1052)|~eqangle(X1056,X1054,X1056,X1051,X1052,X1055,X1052,X1053)|cong(X1054,X1051,X1055,X1053),inference(split_conjunct,[status(thm)],[c269])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 82.03/82.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])).
% 82.03/82.23 fof(c345,plain,(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(![X434]:(~eqangle(X427,X428,X429,X430,X431,X432,X433,X434)|eqangle(X427,X428,X431,X432,X429,X430,X433,X434)))))))))),inference(variable_rename,[status(thm)],[c344])).
% 82.03/82.23 cnf(c346,plain,~eqangle(X1198,X1202,X1200,X1203,X1201,X1199,X1197,X1204)|eqangle(X1198,X1202,X1201,X1199,X1200,X1203,X1197,X1204),inference(split_conjunct,[status(thm)],[c345])).
% 82.03/82.23 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 82.03/82.23 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 82.03/82.23 fof(c398,plain,(![X518]:(![X519]:(![X520]:(![X521]:(~para(X518,X519,X520,X521)|para(X518,X519,X521,X520)))))),inference(variable_rename,[status(thm)],[c397])).
% 82.03/82.23 cnf(c399,plain,~para(X721,X718,X719,X720)|para(X721,X718,X720,X719),inference(split_conjunct,[status(thm)],[c398])).
% 82.03/82.23 cnf(c18032,plain,para(X3320,X3321,X3321,X3320),inference(resolution,[status(thm)],[c18021, c399])).
% 82.03/82.23 cnf(c18904,plain,eqangle(X4113,X4112,X4114,X4111,X4112,X4113,X4114,X4111),inference(resolution,[status(thm)],[c18032, c285])).
% 82.03/82.23 cnf(c23973,plain,eqangle(X4151,X4153,X4152,X4150,X4151,X4153,X4150,X4152),inference(resolution,[status(thm)],[c18904, c352])).
% 82.03/82.23 cnf(c24068,plain,eqangle(X4196,X4197,X4196,X4197,X4199,X4198,X4198,X4199),inference(resolution,[status(thm)],[c23973, c346])).
% 82.03/82.23 cnf(c24134,plain,~cyclic(X5157,X5157,X5159,X5158)|cong(X5157,X5157,X5158,X5158),inference(resolution,[status(thm)],[c24068, c270])).
% 82.03/82.23 cnf(c25197,plain,cong(X5161,X5161,X5160,X5160),inference(resolution,[status(thm)],[c24134, c24402])).
% 82.03/82.23 cnf(c25223,plain,~coll(X5214,X5214,X5214)|midp(X5214,X5214,X5214),inference(resolution,[status(thm)],[c25197, c188])).
% 82.03/82.23 cnf(c25349,plain,midp(X5215,X5215,X5215),inference(resolution,[status(thm)],[c25223, c23729])).
% 82.03/82.23 cnf(c25409,plain,midp(X5221,X5220,X5220),inference(resolution,[status(thm)],[c25349, c18054])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 82.03/82.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])).
% 82.03/82.23 fof(c239,plain,(![X233]:(![X234]:(![X235]:(![X236]:((~perp(X233,X234,X234,X235)|~midp(X236,X233,X235))|cong(X233,X236,X234,X236)))))),inference(variable_rename,[status(thm)],[c238])).
% 82.03/82.23 cnf(c240,plain,~perp(X1013,X1011,X1011,X1014)|~midp(X1012,X1013,X1014)|cong(X1013,X1012,X1011,X1012),inference(split_conjunct,[status(thm)],[c239])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 82.03/82.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])).
% 82.03/82.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])).
% 82.03/82.23 fof(c162,plain,(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:(![X133]:((~eqangle(X126,X127,X128,X129,X130,X131,X132,X133)|~perp(X130,X131,X132,X133))|perp(X126,X127,X128,X129)))))))))),inference(shift_quantors,[status(thm)],[fof(c161,plain,(![X126]:(![X127]:(![X128]:(![X129]:((![X130]:(![X131]:(![X132]:(![X133]:(~eqangle(X126,X127,X128,X129,X130,X131,X132,X133)|~perp(X130,X131,X132,X133))))))|perp(X126,X127,X128,X129)))))),inference(variable_rename,[status(thm)],[c160])).])).
% 82.03/82.23 cnf(c163,plain,~eqangle(X921,X919,X918,X916,X915,X920,X917,X914)|~perp(X915,X920,X917,X914)|perp(X921,X919,X918,X916),inference(split_conjunct,[status(thm)],[c162])).
% 82.03/82.23 cnf(c23979,plain,eqangle(X4157,X4156,X4156,X4157,X4158,X4159,X4158,X4159),inference(resolution,[status(thm)],[c18904, c346])).
% 82.03/82.23 cnf(c24073,plain,~perp(X5143,X5145,X5143,X5145)|perp(X5144,X5146,X5146,X5144),inference(resolution,[status(thm)],[c23979, c163])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 82.03/82.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])).
% 82.03/82.23 fof(c225,plain,(![X217]:(![X218]:(![X219]:(![X220]:((~cong(X217,X219,X218,X219)|~cong(X217,X220,X218,X220))|perp(X217,X218,X219,X220)))))),inference(variable_rename,[status(thm)],[c224])).
% 82.03/82.23 cnf(c226,plain,~cong(X998,X995,X996,X995)|~cong(X998,X997,X996,X997)|perp(X998,X996,X995,X997),inference(split_conjunct,[status(thm)],[c225])).
% 82.03/82.23 cnf(c1096,plain,~cong(X1246,X1247,X1245,X1247)|perp(X1246,X1245,X1247,X1247),inference(factor,[status(thm)],[c226])).
% 82.03/82.23 cnf(c25206,plain,perp(X5173,X5173,X5173,X5173),inference(resolution,[status(thm)],[c25197, c1096])).
% 82.03/82.23 cnf(c25247,plain,perp(X5184,X5183,X5183,X5184),inference(resolution,[status(thm)],[c25206, c24073])).
% 82.03/82.23 cnf(c25293,plain,~midp(X6103,X6105,X6105)|cong(X6105,X6103,X6104,X6103),inference(resolution,[status(thm)],[c25247, c240])).
% 82.03/82.23 cnf(c27160,plain,cong(X6108,X6106,X6107,X6106),inference(resolution,[status(thm)],[c25293, c25409])).
% 82.03/82.23 cnf(c27171,plain,cong(X6114,X6115,X6115,X6116),inference(resolution,[status(thm)],[c27160, c340])).
% 82.03/82.23 cnf(c27242,plain,cong(X6141,X6140,X6142,X6141),inference(resolution,[status(thm)],[c27171, c337])).
% 82.03/82.23 cnf(c27313,plain,cong(X6158,X6157,X6158,X6159),inference(resolution,[status(thm)],[c27242, c340])).
% 82.03/82.23 cnf(c27358,plain,~coll(X6385,X6386,X6384)|midp(X6385,X6386,X6384),inference(resolution,[status(thm)],[c27313, c188])).
% 82.03/82.23 cnf(c28143,plain,midp(X6392,X6390,X6391),inference(resolution,[status(thm)],[c27358, c23729])).
% 82.03/82.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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 82.03/82.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])).
% 82.03/82.23 fof(c264,plain,(![X268]:(![X269]:(![X270]:(![X271]:(![X272]:((~midp(X271,X268,X269)|~midp(X272,X268,X270))|para(X271,X272,X269,X270))))))),inference(variable_rename,[status(thm)],[c263])).
% 82.03/82.23 cnf(c265,plain,~midp(X1049,X1048,X1046)|~midp(X1047,X1048,X1050)|para(X1049,X1047,X1046,X1050),inference(split_conjunct,[status(thm)],[c264])).
% 82.03/82.23 cnf(c25463,plain,~midp(X9887,X9886,X9885)|para(X9887,X9884,X9885,X9886),inference(resolution,[status(thm)],[c25409, c265])).
% 82.03/82.23 cnf(c30945,plain,para(X9890,X9889,X9891,X9888),inference(resolution,[status(thm)],[c25463, c28143])).
% 82.03/82.23 cnf(c30946,plain,$false,inference(resolution,[status(thm)],[c30945, c23])).
% 82.03/82.23 % SZS output end CNFRefutation
% 82.03/82.23
% 82.03/82.23 % Initial clauses : 135
% 82.03/82.23 % Processed clauses : 3338
% 82.03/82.23 % Factors computed : 144
% 82.03/82.23 % Resolvents computed: 30417
% 82.03/82.23 % Tautologies deleted: 12
% 82.03/82.23 % Forward subsumed : 6712
% 82.03/82.23 % Backward subsumed : 2799
% 82.03/82.23 % -------- CPU Time ---------
% 82.03/82.23 % User time : 81.780 s
% 82.03/82.23 % System time : 0.076 s
% 82.03/82.23 % Total time : 81.856 s
%------------------------------------------------------------------------------