%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO635+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:27 EDT 2024
% Result : Theorem 30.53s 30.73s
% Output : Refutation 30.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : GEO635+1 : TPTP v8.1.2. Released v7.5.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n022.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 07:49:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 30.53/30.73 % Version: 1.5
% 30.53/30.73 % SZS status Theorem
% 30.53/30.73 % SZS output start CNFRefutation
% 30.53/30.73 fof(exemplo6GDDFULL8110998,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![NWPNT1]:(![NWPNT2]:((((((circle(D,A,B,C)&coll(E,A,B))&circle(D,A,F,NWPNT1))&eqangle(A,C,C,E,F,C,C,B))&circle(D,C,G,NWPNT2))&coll(G,C,E))=>para(A,B,G,F))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL8110998)).
% 30.53/30.73 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![NWPNT1]:(![NWPNT2]:((((((circle(D,A,B,C)&coll(E,A,B))&circle(D,A,F,NWPNT1))&eqangle(A,C,C,E,F,C,C,B))&circle(D,C,G,NWPNT2))&coll(G,C,E))=>para(A,B,G,F)))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110998])).
% 30.53/30.73 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[NWPNT1]:(?[NWPNT2]:((((((circle(D,A,B,C)&coll(E,A,B))&circle(D,A,F,NWPNT1))&eqangle(A,C,C,E,F,C,C,B))&circle(D,C,G,NWPNT2))&coll(G,C,E))&~para(A,B,G,F))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 30.53/30.73 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:((((((circle(D,A,B,C)&coll(E,A,B))&(?[NWPNT1]:circle(D,A,F,NWPNT1)))&eqangle(A,C,C,E,F,C,C,B))&(?[NWPNT2]:circle(D,C,G,NWPNT2)))&coll(G,C,E))&~para(A,B,G,F))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 30.53/30.73 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((circle(X5,X2,X3,X4)&coll(X6,X2,X3))&(?[X9]:circle(X5,X2,X7,X9)))&eqangle(X2,X4,X4,X6,X7,X4,X4,X3))&(?[X10]:circle(X5,X4,X8,X10)))&coll(X8,X4,X6))&~para(X2,X3,X8,X7))))))))),inference(variable_rename,[status(thm)],[c13])).
% 30.53/30.73 fof(c15,negated_conjecture,((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&coll(skolem0005,skolem0001,skolem0002))&circle(skolem0004,skolem0001,skolem0006,skolem0008))&eqangle(skolem0001,skolem0003,skolem0003,skolem0005,skolem0006,skolem0003,skolem0003,skolem0002))&circle(skolem0004,skolem0003,skolem0007,skolem0009))&coll(skolem0007,skolem0003,skolem0005))&~para(skolem0001,skolem0002,skolem0007,skolem0006)),inference(skolemize,[status(esa)],[c14])).
% 30.53/30.73 cnf(c22,negated_conjecture,~para(skolem0001,skolem0002,skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c400,plain,(![X522]:(![X523]:(![X524]:(![X525]:((~coll(X522,X523,X524)|~coll(X522,X523,X525))|coll(X524,X525,X522)))))),inference(variable_rename,[status(thm)],[c399])).
% 30.53/30.73 cnf(c401,plain,~coll(X689,X686,X687)|~coll(X689,X686,X688)|coll(X687,X688,X689),inference(split_conjunct,[status(thm)],[c400])).
% 30.53/30.73 cnf(c450,plain,~coll(X690,X691,X692)|coll(X692,X692,X690),inference(factor,[status(thm)],[c401])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c188,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 30.53/30.73 fof(c189,plain,(![X165]:(![X166]:(![X167]:(~para(X165,X166,X165,X167)|coll(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c188])).
% 30.53/30.73 cnf(c190,plain,~para(X610,X609,X610,X611)|coll(X610,X609,X611),inference(split_conjunct,[status(thm)],[c189])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c288,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(c287,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)],[c286])).])).
% 30.53/30.73 cnf(c289,plain,~eqangle(X1074,X1075,X1078,X1077,X1079,X1076,X1078,X1077)|para(X1074,X1075,X1079,X1076),inference(split_conjunct,[status(thm)],[c288])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c350,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)],[c349])).
% 30.53/30.73 cnf(c351,plain,~eqangle(X1234,X1233,X1229,X1230,X1231,X1227,X1228,X1232)|eqangle(X1229,X1230,X1234,X1233,X1228,X1232,X1231,X1227),inference(split_conjunct,[status(thm)],[c350])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c283,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(c282,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)],[c281])).])).
% 30.53/30.73 cnf(c284,plain,~para(X1069,X1070,X1073,X1071)|eqangle(X1069,X1070,X1072,X1068,X1073,X1071,X1072,X1068),inference(split_conjunct,[status(thm)],[c283])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 30.53/30.73 fof(c385,plain,(![X500]:(![X501]:(![X502]:(![X503]:(~perp(X500,X501,X502,X503)|perp(X502,X503,X500,X501)))))),inference(variable_rename,[status(thm)],[c384])).
% 30.53/30.73 cnf(c386,plain,~perp(X649,X650,X648,X651)|perp(X648,X651,X649,X650),inference(split_conjunct,[status(thm)],[c385])).
% 30.53/30.73 cnf(c16,negated_conjecture,circle(skolem0004,skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 30.53/30.73 fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 30.53/30.73 fof(c71,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 30.53/30.73 fof(c72,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c71])).
% 30.53/30.73 fof(c73,plain,(![X53]:(![X54]:(![X55]:(![X56]:(~circle(X56,X53,X54,X55)|(?[X57]:perp(X57,X53,X53,X56))))))),inference(variable_rename,[status(thm)],[c72])).
% 30.53/30.73 fof(c74,plain,(![X53]:(![X54]:(![X55]:(![X56]:(~circle(X56,X53,X54,X55)|perp(skolem0018(X53,X54,X55,X56),X53,X53,X56)))))),inference(skolemize,[status(esa)],[c73])).
% 30.53/30.73 cnf(c75,plain,~circle(X785,X783,X784,X786)|perp(skolem0018(X783,X784,X786,X785),X783,X783,X785),inference(split_conjunct,[status(thm)],[c74])).
% 30.53/30.73 cnf(c686,plain,perp(skolem0018(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001,skolem0001,skolem0004),inference(resolution,[status(thm)],[c75, c16])).
% 30.53/30.73 cnf(c1681,plain,perp(skolem0001,skolem0004,skolem0018(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001),inference(resolution,[status(thm)],[c686, c386])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c382,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)],[c381])).
% 30.53/30.73 cnf(c383,plain,~perp(X1276,X1278,X1280,X1275)|~perp(X1280,X1275,X1277,X1279)|para(X1276,X1278,X1277,X1279),inference(split_conjunct,[status(thm)],[c382])).
% 30.53/30.73 cnf(c1697,plain,~perp(X2891,X2890,skolem0018(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001)|para(X2891,X2890,skolem0001,skolem0004),inference(resolution,[status(thm)],[c686, c383])).
% 30.53/30.73 cnf(c4504,plain,para(skolem0001,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c1697, c1681])).
% 30.53/30.73 cnf(c4627,plain,eqangle(skolem0001,skolem0004,X3381,X3380,skolem0001,skolem0004,X3381,X3380),inference(resolution,[status(thm)],[c4504, c284])).
% 30.53/30.73 cnf(c5543,plain,eqangle(X3448,X3447,skolem0001,skolem0004,X3448,X3447,skolem0001,skolem0004),inference(resolution,[status(thm)],[c4627, c351])).
% 30.53/30.73 cnf(c5991,plain,para(X3450,X3449,X3450,X3449),inference(resolution,[status(thm)],[c5543, c289])).
% 30.53/30.73 cnf(c6005,plain,coll(X3452,X3451,X3451),inference(resolution,[status(thm)],[c5991, c190])).
% 30.53/30.73 cnf(c6126,plain,coll(X3456,X3456,X3457),inference(resolution,[status(thm)],[c6005, c450])).
% 30.53/30.73 cnf(c6311,plain,~coll(X4463,X4463,X4465)|coll(X4465,X4464,X4463),inference(resolution,[status(thm)],[c6126, c401])).
% 30.53/30.73 cnf(c9473,plain,coll(X4473,X4471,X4472),inference(resolution,[status(thm)],[c6311, c6126])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c186,plain,(![X162]:(![X163]:(![X164]:((~cong(X162,X163,X162,X164)|~coll(X162,X163,X164))|midp(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c185])).
% 30.53/30.73 cnf(c187,plain,~cong(X950,X949,X950,X948)|~coll(X950,X949,X948)|midp(X950,X949,X948),inference(split_conjunct,[status(thm)],[c186])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 30.53/30.73 fof(c338,plain,(![X411]:(![X412]:(![X413]:(![X414]:(~cong(X411,X412,X413,X414)|cong(X411,X412,X414,X413)))))),inference(variable_rename,[status(thm)],[c337])).
% 30.53/30.73 cnf(c339,plain,~cong(X617,X618,X616,X619)|cong(X617,X618,X619,X616),inference(split_conjunct,[status(thm)],[c338])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 30.53/30.73 fof(c335,plain,(![X407]:(![X408]:(![X409]:(![X410]:(~cong(X407,X408,X409,X410)|cong(X409,X410,X407,X408)))))),inference(variable_rename,[status(thm)],[c334])).
% 30.53/30.73 cnf(c336,plain,~cong(X614,X613,X612,X615)|cong(X612,X615,X614,X613),inference(split_conjunct,[status(thm)],[c335])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c195,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)],[c194])).
% 30.53/30.73 cnf(c196,plain,~midp(X958,X956,X959)|~para(X956,X957,X959,X960)|~para(X956,X960,X959,X957)|midp(X958,X957,X960),inference(split_conjunct,[status(thm)],[c195])).
% 30.53/30.73 cnf(c966,plain,~midp(X2021,X2020,X2022)|~para(X2020,X2023,X2022,X2023)|midp(X2021,X2023,X2023),inference(factor,[status(thm)],[c196])).
% 30.53/30.73 cnf(c6015,plain,~midp(X4306,X4305,X4305)|midp(X4306,X4304,X4304),inference(resolution,[status(thm)],[c5991, c966])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c358,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 30.53/30.73 fof(c359,plain,(![X464]:(![X465]:(![X466]:(![X467]:(~cyclic(X464,X465,X466,X467)|cyclic(X465,X464,X466,X467)))))),inference(variable_rename,[status(thm)],[c358])).
% 30.53/30.73 cnf(c360,plain,~cyclic(X620,X621,X623,X622)|cyclic(X621,X620,X623,X622),inference(split_conjunct,[status(thm)],[c359])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 30.53/30.73 fof(c365,plain,(![X472]:(![X473]:(![X474]:(![X475]:(~cyclic(X472,X473,X474,X475)|cyclic(X472,X473,X475,X474)))))),inference(variable_rename,[status(thm)],[c364])).
% 30.53/30.73 cnf(c366,plain,~cyclic(X646,X645,X644,X647)|cyclic(X646,X645,X647,X644),inference(split_conjunct,[status(thm)],[c365])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 30.53/30.73 fof(c362,plain,(![X468]:(![X469]:(![X470]:(![X471]:(~cyclic(X468,X469,X470,X471)|cyclic(X468,X470,X469,X471)))))),inference(variable_rename,[status(thm)],[c361])).
% 30.53/30.73 cnf(c363,plain,~cyclic(X625,X627,X626,X624)|cyclic(X625,X626,X627,X624),inference(split_conjunct,[status(thm)],[c362])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c271,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)],[c270])).
% 30.53/30.73 cnf(c272,plain,~eqangle(X1056,X1059,X1056,X1057,X1058,X1059,X1058,X1057)|~coll(X1056,X1058,X1057)|cyclic(X1059,X1057,X1056,X1058),inference(split_conjunct,[status(thm)],[c271])).
% 30.53/30.73 cnf(c6013,plain,eqangle(X4301,X4298,X4300,X4299,X4301,X4298,X4300,X4299),inference(resolution,[status(thm)],[c5991, c284])).
% 30.53/30.73 cnf(c9323,plain,~coll(X4772,X4772,X4773)|cyclic(X4771,X4773,X4772,X4772),inference(resolution,[status(thm)],[c6013, c272])).
% 30.53/30.73 cnf(c9906,plain,cyclic(X4776,X4774,X4775,X4775),inference(resolution,[status(thm)],[c9323, c9473])).
% 30.53/30.73 cnf(c9908,plain,cyclic(X4781,X4782,X4780,X4782),inference(resolution,[status(thm)],[c9906, c363])).
% 30.53/30.73 cnf(c9915,plain,cyclic(X4790,X4789,X4789,X4791),inference(resolution,[status(thm)],[c9908, c366])).
% 30.53/30.73 cnf(c9927,plain,cyclic(X4807,X4809,X4807,X4808),inference(resolution,[status(thm)],[c9915, c360])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 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])).
% 30.53/30.73 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(shift_quantors,[status(thm)],[fof(c267,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)],[c266])).])).
% 30.53/30.73 cnf(c269,plain,~cyclic(X1050,X1054,X1055,X1051)|~cyclic(X1050,X1054,X1055,X1053)|~cyclic(X1050,X1054,X1055,X1052)|~eqangle(X1055,X1050,X1055,X1054,X1052,X1051,X1052,X1053)|cong(X1050,X1054,X1051,X1053),inference(split_conjunct,[status(thm)],[c268])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c344,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)],[c343])).
% 30.53/30.73 cnf(c345,plain,~eqangle(X1217,X1212,X1210,X1214,X1211,X1215,X1216,X1213)|eqangle(X1217,X1212,X1211,X1215,X1210,X1214,X1216,X1213),inference(split_conjunct,[status(thm)],[c344])).
% 30.53/30.73 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)).
% 30.53/30.73 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 30.53/30.73 fof(c397,plain,(![X518]:(![X519]:(![X520]:(![X521]:(~para(X518,X519,X520,X521)|para(X518,X519,X521,X520)))))),inference(variable_rename,[status(thm)],[c396])).
% 30.53/30.73 cnf(c398,plain,~para(X663,X661,X660,X662)|para(X663,X661,X662,X660),inference(split_conjunct,[status(thm)],[c397])).
% 30.53/30.73 cnf(c6002,plain,para(X3473,X3474,X3474,X3473),inference(resolution,[status(thm)],[c5991, c398])).
% 30.53/30.73 cnf(c6736,plain,eqangle(X4575,X4578,X4577,X4576,X4578,X4575,X4577,X4576),inference(resolution,[status(thm)],[c6002, c284])).
% 30.53/30.73 cnf(c9641,plain,eqangle(X4616,X4615,X4614,X4617,X4616,X4615,X4617,X4614),inference(resolution,[status(thm)],[c6736, c351])).
% 30.53/30.73 cnf(c9709,plain,eqangle(X4672,X4670,X4672,X4670,X4669,X4671,X4671,X4669),inference(resolution,[status(thm)],[c9641, c345])).
% 30.53/30.73 cnf(c9782,plain,~cyclic(X5715,X5715,X5714,X5716)|cong(X5715,X5715,X5716,X5716),inference(resolution,[status(thm)],[c9709, c269])).
% 30.53/30.73 cnf(c10491,plain,cong(X5717,X5717,X5718,X5718),inference(resolution,[status(thm)],[c9782, c9927])).
% 30.53/30.73 cnf(c10518,plain,~coll(X5784,X5784,X5784)|midp(X5784,X5784,X5784),inference(resolution,[status(thm)],[c10491, c187])).
% 30.53/30.73 cnf(c10599,plain,midp(X5785,X5785,X5785),inference(resolution,[status(thm)],[c10518, c9473])).
% 30.53/30.73 cnf(c10736,plain,midp(X5788,X5787,X5787),inference(resolution,[status(thm)],[c10599, c6015])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c238,plain,(![X233]:(![X234]:(![X235]:(![X236]:((~perp(X233,X234,X234,X235)|~midp(X236,X233,X235))|cong(X233,X236,X234,X236)))))),inference(variable_rename,[status(thm)],[c237])).
% 30.53/30.73 cnf(c239,plain,~perp(X1011,X1010,X1010,X1013)|~midp(X1012,X1011,X1013)|cong(X1011,X1012,X1010,X1012),inference(split_conjunct,[status(thm)],[c238])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 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])).
% 30.53/30.73 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(shift_quantors,[status(thm)],[fof(c160,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)],[c159])).])).
% 30.53/30.73 cnf(c162,plain,~eqangle(X920,X923,X921,X925,X922,X919,X924,X918)|~perp(X922,X919,X924,X918)|perp(X920,X923,X921,X925),inference(split_conjunct,[status(thm)],[c161])).
% 30.53/30.73 cnf(c9650,plain,eqangle(X4629,X4630,X4630,X4629,X4627,X4628,X4627,X4628),inference(resolution,[status(thm)],[c6736, c345])).
% 30.53/30.73 cnf(c9716,plain,~perp(X5652,X5654,X5652,X5654)|perp(X5653,X5655,X5655,X5653),inference(resolution,[status(thm)],[c9650, c162])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c224,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)],[c223])).
% 30.53/30.73 cnf(c225,plain,~cong(X994,X995,X996,X995)|~cong(X994,X997,X996,X997)|perp(X994,X996,X995,X997),inference(split_conjunct,[status(thm)],[c224])).
% 30.53/30.73 cnf(c1050,plain,~cong(X1178,X1176,X1177,X1176)|perp(X1178,X1177,X1176,X1176),inference(factor,[status(thm)],[c225])).
% 30.53/30.73 cnf(c10510,plain,perp(X5731,X5731,X5731,X5731),inference(resolution,[status(thm)],[c10491, c1050])).
% 30.53/30.73 cnf(c10526,plain,perp(X5742,X5741,X5741,X5742),inference(resolution,[status(thm)],[c10510, c9716])).
% 30.53/30.73 cnf(c10563,plain,~midp(X6572,X6573,X6573)|cong(X6573,X6572,X6574,X6572),inference(resolution,[status(thm)],[c10526, c239])).
% 30.53/30.73 cnf(c11742,plain,cong(X6575,X6576,X6577,X6576),inference(resolution,[status(thm)],[c10563, c10736])).
% 30.53/30.73 cnf(c11760,plain,cong(X6589,X6590,X6590,X6591),inference(resolution,[status(thm)],[c11742, c339])).
% 30.53/30.73 cnf(c11794,plain,cong(X6609,X6610,X6611,X6609),inference(resolution,[status(thm)],[c11760, c336])).
% 30.53/30.73 cnf(c11845,plain,cong(X6638,X6639,X6638,X6640),inference(resolution,[status(thm)],[c11794, c339])).
% 30.53/30.73 cnf(c11869,plain,~coll(X6783,X6782,X6784)|midp(X6783,X6782,X6784),inference(resolution,[status(thm)],[c11845, c187])).
% 30.53/30.73 cnf(c12957,plain,midp(X6785,X6787,X6786),inference(resolution,[status(thm)],[c11869, c9473])).
% 30.53/30.73 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)).
% 30.53/30.73 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])).
% 30.53/30.73 fof(c263,plain,(![X268]:(![X269]:(![X270]:(![X271]:(![X272]:((~midp(X271,X268,X269)|~midp(X272,X268,X270))|para(X271,X272,X269,X270))))))),inference(variable_rename,[status(thm)],[c262])).
% 30.53/30.73 cnf(c264,plain,~midp(X1046,X1045,X1049)|~midp(X1047,X1045,X1048)|para(X1046,X1047,X1049,X1048),inference(split_conjunct,[status(thm)],[c263])).
% 30.53/30.73 cnf(c10756,plain,~midp(X9691,X9690,X9692)|para(X9691,X9693,X9692,X9690),inference(resolution,[status(thm)],[c10736, c264])).
% 30.53/30.73 cnf(c15506,plain,para(X9694,X9695,X9696,X9697),inference(resolution,[status(thm)],[c10756, c12957])).
% 30.53/30.73 cnf(c15520,plain,$false,inference(resolution,[status(thm)],[c15506, c22])).
% 30.53/30.73 % SZS output end CNFRefutation
% 30.53/30.73
% 30.53/30.73 % Initial clauses : 134
% 30.53/30.73 % Processed clauses : 2248
% 30.53/30.73 % Factors computed : 155
% 30.53/30.73 % Resolvents computed: 14958
% 30.53/30.73 % Tautologies deleted: 12
% 30.53/30.73 % Forward subsumed : 4648
% 30.53/30.73 % Backward subsumed : 1855
% 30.53/30.73 % -------- CPU Time ---------
% 30.53/30.73 % User time : 30.317 s
% 30.53/30.73 % System time : 0.045 s
% 30.53/30.73 % Total time : 30.362 s
%------------------------------------------------------------------------------