%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO586+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:20 EDT 2024
% Result : Theorem 51.11s 51.32s
% Output : Refutation 51.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO586+1 : TPTP v8.1.2. Released v7.5.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n016.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:23:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 51.11/51.32 % Version: 1.5
% 51.11/51.32 % SZS status Theorem
% 51.11/51.32 % SZS output start CNFRefutation
% 51.11/51.32 fof(exemplo6GDDFULL416048,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![I]:(![NWPNT1]:(((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&coll(E,A,C))&coll(E,B,D))&circle(I,A,B,E))=>perp(I,E,C,D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL416048)).
% 51.11/51.32 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![I]:(![NWPNT1]:(((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&coll(E,A,C))&coll(E,B,D))&circle(I,A,B,E))=>perp(I,E,C,D))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416048])).
% 51.11/51.32 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(?[I]:(?[NWPNT1]:(((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&coll(E,A,C))&coll(E,B,D))&circle(I,A,B,E))&~perp(I,E,C,D)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 51.11/51.32 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(?[I]:(((((circle(O,A,B,C)&(?[NWPNT1]:circle(O,A,D,NWPNT1)))&coll(E,A,C))&coll(E,B,D))&circle(I,A,B,E))&~perp(I,E,C,D))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 51.11/51.32 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((circle(X5,X2,X3,X4)&(?[X9]:circle(X5,X2,X6,X9)))&coll(X7,X2,X4))&coll(X7,X3,X6))&circle(X8,X2,X3,X7))&~perp(X8,X7,X4,X6))))))))),inference(variable_rename,[status(thm)],[c13])).
% 51.11/51.32 fof(c15,negated_conjecture,(((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0008))&coll(skolem0006,skolem0001,skolem0003))&coll(skolem0006,skolem0002,skolem0005))&circle(skolem0007,skolem0001,skolem0002,skolem0006))&~perp(skolem0007,skolem0006,skolem0003,skolem0005)),inference(skolemize,[status(esa)],[c14])).
% 51.11/51.32 cnf(c21,negated_conjecture,~perp(skolem0007,skolem0006,skolem0003,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 51.11/51.32 fof(c399,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c398])).
% 51.11/51.32 cnf(c400,plain,~coll(X687,X685,X688)|~coll(X687,X685,X686)|coll(X688,X686,X687),inference(split_conjunct,[status(thm)],[c399])).
% 51.11/51.32 cnf(c449,plain,~coll(X690,X689,X691)|coll(X691,X691,X690),inference(factor,[status(thm)],[c400])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c187,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 51.11/51.32 fof(c188,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c187])).
% 51.11/51.32 cnf(c189,plain,~para(X608,X609,X608,X610)|coll(X608,X609,X610),inference(split_conjunct,[status(thm)],[c188])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c284,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~eqangle(A,B,P,Q,C,D,P,Q)|para(A,B,C,D)))))))),inference(fof_nnf,[status(thm)],[ruleD39])).
% 51.11/51.32 fof(c285,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:~eqangle(A,B,P,Q,C,D,P,Q)))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c284])).
% 51.11/51.32 fof(c287,plain,(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)|para(X296,X297,X298,X299)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X296]:(![X297]:(![X298]:(![X299]:((![X300]:(![X301]:~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))|para(X296,X297,X298,X299)))))),inference(variable_rename,[status(thm)],[c285])).])).
% 51.11/51.32 cnf(c288,plain,~eqangle(X1078,X1079,X1077,X1076,X1074,X1075,X1077,X1076)|para(X1078,X1079,X1074,X1075),inference(split_conjunct,[status(thm)],[c287])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c348,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(C,D,A,B,U,V,P,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleD19])).
% 51.11/51.32 fof(c349,plain,(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(~eqangle(X442,X443,X444,X445,X446,X447,X448,X449)|eqangle(X444,X445,X442,X443,X448,X449,X446,X447)))))))))),inference(variable_rename,[status(thm)],[c348])).
% 51.11/51.32 cnf(c350,plain,~eqangle(X1226,X1229,X1228,X1233,X1232,X1227,X1231,X1230)|eqangle(X1228,X1233,X1226,X1229,X1231,X1230,X1232,X1227),inference(split_conjunct,[status(thm)],[c349])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c279,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~para(A,B,C,D)|eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD40])).
% 51.11/51.32 fof(c280,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|(![P]:(![Q]:eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(shift_quantors,[status(thm)],[c279])).
% 51.11/51.32 fof(c282,plain,(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(~para(X290,X291,X292,X293)|eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(shift_quantors,[status(thm)],[fof(c281,plain,(![X290]:(![X291]:(![X292]:(![X293]:(~para(X290,X291,X292,X293)|(![X294]:(![X295]:eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(variable_rename,[status(thm)],[c280])).])).
% 51.11/51.32 cnf(c283,plain,~para(X1070,X1071,X1069,X1073)|eqangle(X1070,X1071,X1068,X1072,X1069,X1073,X1068,X1072),inference(split_conjunct,[status(thm)],[c282])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c383,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 51.11/51.32 fof(c384,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c383])).
% 51.11/51.32 cnf(c385,plain,~perp(X649,X647,X650,X648)|perp(X650,X648,X649,X647),inference(split_conjunct,[status(thm)],[c384])).
% 51.11/51.32 cnf(c16,negated_conjecture,circle(skolem0004,skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 51.11/51.32 fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 51.11/51.32 fof(c70,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 51.11/51.32 fof(c71,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c70])).
% 51.11/51.32 fof(c72,plain,(![X52]:(![X53]:(![X54]:(![X55]:(~circle(X55,X52,X53,X54)|(?[X56]:perp(X56,X52,X52,X55))))))),inference(variable_rename,[status(thm)],[c71])).
% 51.11/51.32 fof(c73,plain,(![X52]:(![X53]:(![X54]:(![X55]:(~circle(X55,X52,X53,X54)|perp(skolem0017(X52,X53,X54,X55),X52,X52,X55)))))),inference(skolemize,[status(esa)],[c72])).
% 51.11/51.32 cnf(c74,plain,~circle(X783,X785,X782,X784)|perp(skolem0017(X785,X782,X784,X783),X785,X785,X783),inference(split_conjunct,[status(thm)],[c73])).
% 51.11/51.32 cnf(c674,plain,perp(skolem0017(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001,skolem0001,skolem0004),inference(resolution,[status(thm)],[c74, c16])).
% 51.11/51.32 cnf(c1667,plain,perp(skolem0001,skolem0004,skolem0017(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001),inference(resolution,[status(thm)],[c674, c385])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c380,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~perp(A,B,C,D)|~perp(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD9])).
% 51.11/51.32 fof(c381,plain,(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:((~perp(X493,X494,X495,X496)|~perp(X495,X496,X497,X498))|para(X493,X494,X497,X498)))))))),inference(variable_rename,[status(thm)],[c380])).
% 51.11/51.32 cnf(c382,plain,~perp(X1274,X1276,X1273,X1277)|~perp(X1273,X1277,X1278,X1275)|para(X1274,X1276,X1278,X1275),inference(split_conjunct,[status(thm)],[c381])).
% 51.11/51.32 cnf(c1669,plain,~perp(X2858,X2859,skolem0017(skolem0001,skolem0002,skolem0003,skolem0004),skolem0001)|para(X2858,X2859,skolem0001,skolem0004),inference(resolution,[status(thm)],[c674, c382])).
% 51.11/51.32 cnf(c4305,plain,para(skolem0001,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c1669, c1667])).
% 51.11/51.32 cnf(c4376,plain,eqangle(skolem0001,skolem0004,X3691,X3690,skolem0001,skolem0004,X3691,X3690),inference(resolution,[status(thm)],[c4305, c283])).
% 51.11/51.32 cnf(c6802,plain,eqangle(X4490,X4491,skolem0001,skolem0004,X4490,X4491,skolem0001,skolem0004),inference(resolution,[status(thm)],[c4376, c350])).
% 51.11/51.32 cnf(c8174,plain,para(X4496,X4495,X4496,X4495),inference(resolution,[status(thm)],[c6802, c288])).
% 51.11/51.32 cnf(c8198,plain,coll(X4497,X4498,X4498),inference(resolution,[status(thm)],[c8174, c189])).
% 51.11/51.32 cnf(c8373,plain,coll(X4501,X4501,X4502),inference(resolution,[status(thm)],[c8198, c449])).
% 51.11/51.32 cnf(c8539,plain,~coll(X5775,X5775,X5776)|coll(X5776,X5774,X5775),inference(resolution,[status(thm)],[c8373, c400])).
% 51.11/51.32 cnf(c13479,plain,coll(X5780,X5779,X5781),inference(resolution,[status(thm)],[c8539, c8373])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c184,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 51.11/51.32 fof(c185,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c184])).
% 51.11/51.32 cnf(c186,plain,~cong(X950,X949,X950,X948)|~coll(X950,X949,X948)|midp(X950,X949,X948),inference(split_conjunct,[status(thm)],[c185])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 51.11/51.32 fof(c337,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c336])).
% 51.11/51.32 cnf(c338,plain,~cong(X618,X615,X617,X616)|cong(X618,X615,X616,X617),inference(split_conjunct,[status(thm)],[c337])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c333,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 51.11/51.32 fof(c334,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c333])).
% 51.11/51.32 cnf(c335,plain,~cong(X612,X611,X614,X613)|cong(X614,X613,X612,X611),inference(split_conjunct,[status(thm)],[c334])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c193,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C))|midp(M,C,D))))))),inference(fof_nnf,[status(thm)],[ruleD64])).
% 51.11/51.32 fof(c194,plain,(![X172]:(![X173]:(![X174]:(![X175]:(![X176]:(((~midp(X176,X172,X173)|~para(X172,X174,X173,X175))|~para(X172,X175,X173,X174))|midp(X176,X174,X175))))))),inference(variable_rename,[status(thm)],[c193])).
% 51.11/51.32 cnf(c195,plain,~midp(X959,X957,X958)|~para(X957,X960,X958,X956)|~para(X957,X956,X958,X960)|midp(X959,X960,X956),inference(split_conjunct,[status(thm)],[c194])).
% 51.11/51.32 cnf(c948,plain,~midp(X2019,X2021,X2018)|~para(X2021,X2020,X2018,X2020)|midp(X2019,X2020,X2020),inference(factor,[status(thm)],[c195])).
% 51.11/51.32 cnf(c8187,plain,~midp(X5547,X5546,X5546)|midp(X5547,X5545,X5545),inference(resolution,[status(thm)],[c8174, c948])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 51.11/51.32 fof(c361,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c360])).
% 51.11/51.32 cnf(c362,plain,~cyclic(X626,X623,X625,X624)|cyclic(X626,X625,X623,X624),inference(split_conjunct,[status(thm)],[c361])).
% 51.11/51.32 fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 51.11/51.32 fof(c357,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 51.11/51.32 fof(c358,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X464,X463,X465,X466)))))),inference(variable_rename,[status(thm)],[c357])).
% 51.11/51.32 cnf(c359,plain,~cyclic(X622,X619,X621,X620)|cyclic(X619,X622,X621,X620),inference(split_conjunct,[status(thm)],[c358])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 51.11/51.32 fof(c364,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c363])).
% 51.11/51.32 cnf(c365,plain,~cyclic(X644,X645,X643,X646)|cyclic(X644,X645,X646,X643),inference(split_conjunct,[status(thm)],[c364])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c269,plain,(![A]:(![B]:(![P]:(![Q]:((~eqangle(P,A,P,B,Q,A,Q,B)|~coll(P,Q,B))|cyclic(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD42b])).
% 51.11/51.32 fof(c270,plain,(![X278]:(![X279]:(![X280]:(![X281]:((~eqangle(X280,X278,X280,X279,X281,X278,X281,X279)|~coll(X280,X281,X279))|cyclic(X278,X279,X280,X281)))))),inference(variable_rename,[status(thm)],[c269])).
% 51.11/51.32 cnf(c271,plain,~eqangle(X1057,X1058,X1057,X1056,X1059,X1058,X1059,X1056)|~coll(X1057,X1059,X1056)|cyclic(X1058,X1056,X1057,X1059),inference(split_conjunct,[status(thm)],[c270])).
% 51.11/51.32 cnf(c8200,plain,eqangle(X5551,X5548,X5550,X5549,X5551,X5548,X5550,X5549),inference(resolution,[status(thm)],[c8174, c283])).
% 51.11/51.32 cnf(c13218,plain,~coll(X6121,X6121,X6122)|cyclic(X6120,X6122,X6121,X6121),inference(resolution,[status(thm)],[c8200, c271])).
% 51.11/51.32 cnf(c13854,plain,cyclic(X6123,X6124,X6125,X6125),inference(resolution,[status(thm)],[c13218, c13479])).
% 51.11/51.32 cnf(c13857,plain,cyclic(X6130,X6129,X6131,X6129),inference(resolution,[status(thm)],[c13854, c362])).
% 51.11/51.32 cnf(c13866,plain,cyclic(X6143,X6141,X6141,X6142),inference(resolution,[status(thm)],[c13857, c365])).
% 51.11/51.32 cnf(c13877,plain,cyclic(X6156,X6157,X6156,X6158),inference(resolution,[status(thm)],[c13866, c359])).
% 51.11/51.32 cnf(c13889,plain,cyclic(X6172,X6172,X6173,X6171),inference(resolution,[status(thm)],[c13877, c362])).
% 51.11/51.32 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)).
% 51.11/51.32 fof(c264,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q))|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD43])).
% 51.11/51.32 fof(c265,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:((![R]:(((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q)))|cong(A,B,P,Q))))))),inference(shift_quantors,[status(thm)],[c264])).
% 51.11/51.32 fof(c267,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276))|cong(X272,X273,X275,X276)))))))),inference(shift_quantors,[status(thm)],[fof(c266,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((![X277]:(((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276)))|cong(X272,X273,X275,X276))))))),inference(variable_rename,[status(thm)],[c265])).])).
% 51.11/51.33 cnf(c268,plain,~cyclic(X1052,X1055,X1051,X1050)|~cyclic(X1052,X1055,X1051,X1054)|~cyclic(X1052,X1055,X1051,X1053)|~eqangle(X1051,X1052,X1051,X1055,X1053,X1050,X1053,X1054)|cong(X1052,X1055,X1050,X1054),inference(split_conjunct,[status(thm)],[c267])).
% 51.11/51.33 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)).
% 51.11/51.33 fof(c342,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(A,B,P,Q,C,D,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD21])).
% 51.11/51.33 fof(c343,plain,(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(~eqangle(X426,X427,X428,X429,X430,X431,X432,X433)|eqangle(X426,X427,X430,X431,X428,X429,X432,X433)))))))))),inference(variable_rename,[status(thm)],[c342])).
% 51.11/51.33 cnf(c344,plain,~eqangle(X1212,X1210,X1211,X1209,X1213,X1208,X1214,X1215)|eqangle(X1212,X1210,X1213,X1208,X1211,X1209,X1214,X1215),inference(split_conjunct,[status(thm)],[c343])).
% 51.11/51.33 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)).
% 51.11/51.33 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 51.11/51.33 fof(c396,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c395])).
% 51.11/51.33 cnf(c397,plain,~para(X659,X660,X661,X662)|para(X659,X660,X662,X661),inference(split_conjunct,[status(thm)],[c396])).
% 51.11/51.33 cnf(c8182,plain,para(X4517,X4516,X4516,X4517),inference(resolution,[status(thm)],[c8174, c397])).
% 51.11/51.33 cnf(c9163,plain,eqangle(X5930,X5933,X5932,X5931,X5933,X5930,X5932,X5931),inference(resolution,[status(thm)],[c8182, c283])).
% 51.11/51.33 cnf(c13670,plain,eqangle(X5964,X5965,X5963,X5966,X5964,X5965,X5966,X5963),inference(resolution,[status(thm)],[c9163, c350])).
% 51.11/51.33 cnf(c13716,plain,eqangle(X6016,X6015,X6016,X6015,X6014,X6013,X6013,X6014),inference(resolution,[status(thm)],[c13670, c344])).
% 51.11/51.33 cnf(c13766,plain,~cyclic(X7062,X7062,X7060,X7061)|cong(X7062,X7062,X7061,X7061),inference(resolution,[status(thm)],[c13716, c268])).
% 51.11/51.33 cnf(c14419,plain,cong(X7064,X7064,X7063,X7063),inference(resolution,[status(thm)],[c13766, c13889])).
% 51.11/51.33 cnf(c14425,plain,~coll(X7120,X7120,X7120)|midp(X7120,X7120,X7120),inference(resolution,[status(thm)],[c14419, c186])).
% 51.11/51.33 cnf(c14556,plain,midp(X7121,X7121,X7121),inference(resolution,[status(thm)],[c14425, c13479])).
% 51.11/51.33 cnf(c14595,plain,midp(X7123,X7122,X7122),inference(resolution,[status(thm)],[c14556, c8187])).
% 51.11/51.33 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)).
% 51.11/51.33 fof(c236,plain,(![A]:(![B]:(![C]:(![M]:((~perp(A,B,B,C)|~midp(M,A,C))|cong(A,M,B,M)))))),inference(fof_nnf,[status(thm)],[ruleD52])).
% 51.11/51.33 fof(c237,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c236])).
% 51.11/51.33 cnf(c238,plain,~perp(X1011,X1012,X1012,X1010)|~midp(X1013,X1011,X1010)|cong(X1011,X1013,X1012,X1013),inference(split_conjunct,[status(thm)],[c237])).
% 51.11/51.33 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)).
% 51.11/51.33 fof(c157,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 51.11/51.33 fof(c158,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))))))|perp(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c157])).
% 51.11/51.33 fof(c160,plain,(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:((~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))|perp(X125,X126,X127,X128)))))))))),inference(shift_quantors,[status(thm)],[fof(c159,plain,(![X125]:(![X126]:(![X127]:(![X128]:((![X129]:(![X130]:(![X131]:(![X132]:(~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))))))|perp(X125,X126,X127,X128)))))),inference(variable_rename,[status(thm)],[c158])).])).
% 51.11/51.33 cnf(c161,plain,~eqangle(X922,X924,X918,X923,X920,X925,X919,X921)|~perp(X920,X925,X919,X921)|perp(X922,X924,X918,X923),inference(split_conjunct,[status(thm)],[c160])).
% 51.11/51.33 cnf(c13673,plain,eqangle(X5971,X5972,X5972,X5971,X5970,X5969,X5970,X5969),inference(resolution,[status(thm)],[c9163, c344])).
% 51.11/51.33 cnf(c13731,plain,~perp(X7043,X7042,X7043,X7042)|perp(X7044,X7041,X7041,X7044),inference(resolution,[status(thm)],[c13673, c161])).
% 51.11/51.33 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)).
% 51.11/51.33 fof(c222,plain,(![A]:(![B]:(![P]:(![Q]:((~cong(A,P,B,P)|~cong(A,Q,B,Q))|perp(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD56])).
% 51.11/51.33 fof(c223,plain,(![X216]:(![X217]:(![X218]:(![X219]:((~cong(X216,X218,X217,X218)|~cong(X216,X219,X217,X219))|perp(X216,X217,X218,X219)))))),inference(variable_rename,[status(thm)],[c222])).
% 51.11/51.33 cnf(c224,plain,~cong(X995,X996,X994,X996)|~cong(X995,X997,X994,X997)|perp(X995,X994,X996,X997),inference(split_conjunct,[status(thm)],[c223])).
% 51.11/51.33 cnf(c1019,plain,~cong(X1202,X1203,X1204,X1203)|perp(X1202,X1204,X1203,X1203),inference(factor,[status(thm)],[c224])).
% 51.11/51.33 cnf(c14436,plain,perp(X7076,X7076,X7076,X7076),inference(resolution,[status(thm)],[c14419, c1019])).
% 51.11/51.33 cnf(c14467,plain,perp(X7094,X7093,X7093,X7094),inference(resolution,[status(thm)],[c14436, c13731])).
% 51.11/51.33 cnf(c14525,plain,~midp(X7872,X7870,X7870)|cong(X7870,X7872,X7871,X7872),inference(resolution,[status(thm)],[c14467, c238])).
% 51.11/51.33 cnf(c15914,plain,cong(X7873,X7875,X7874,X7875),inference(resolution,[status(thm)],[c14525, c14595])).
% 51.11/51.33 cnf(c15938,plain,cong(X7888,X7889,X7889,X7887),inference(resolution,[status(thm)],[c15914, c338])).
% 51.11/51.33 cnf(c15975,plain,cong(X7903,X7904,X7902,X7903),inference(resolution,[status(thm)],[c15938, c335])).
% 51.11/51.33 cnf(c16044,plain,cong(X7929,X7928,X7929,X7927),inference(resolution,[status(thm)],[c15975, c338])).
% 51.11/51.33 cnf(c16058,plain,~coll(X8054,X8052,X8053)|midp(X8054,X8052,X8053),inference(resolution,[status(thm)],[c16044, c186])).
% 51.11/51.33 cnf(c17559,plain,midp(X8057,X8055,X8056),inference(resolution,[status(thm)],[c16058, c13479])).
% 51.11/51.33 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)).
% 51.11/51.33 fof(c261,plain,(![A]:(![B]:(![C]:(![E]:(![F]:((~midp(E,A,B)|~midp(F,A,C))|para(E,F,B,C))))))),inference(fof_nnf,[status(thm)],[ruleD44])).
% 51.11/51.33 fof(c262,plain,(![X267]:(![X268]:(![X269]:(![X270]:(![X271]:((~midp(X270,X267,X268)|~midp(X271,X267,X269))|para(X270,X271,X268,X269))))))),inference(variable_rename,[status(thm)],[c261])).
% 51.11/51.33 cnf(c263,plain,~midp(X1047,X1046,X1048)|~midp(X1049,X1046,X1045)|para(X1047,X1049,X1048,X1045),inference(split_conjunct,[status(thm)],[c262])).
% 51.11/51.33 cnf(c14771,plain,~midp(X11042,X11043,X11044)|para(X11042,X11045,X11044,X11043),inference(resolution,[status(thm)],[c14595, c263])).
% 51.11/51.33 cnf(c19624,plain,para(X11048,X11046,X11047,X11049),inference(resolution,[status(thm)],[c14771, c17559])).
% 51.11/51.33 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 51.11/51.33 fof(c377,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])).
% 51.11/51.33 fof(c378,plain,(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:(![X492]:((~para(X487,X488,X489,X490)|~perp(X489,X490,X491,X492))|perp(X487,X488,X491,X492)))))))),inference(variable_rename,[status(thm)],[c377])).
% 51.11/51.33 cnf(c379,plain,~para(X1270,X1267,X1266,X1271)|~perp(X1266,X1271,X1269,X1268)|perp(X1270,X1267,X1269,X1268),inference(split_conjunct,[status(thm)],[c378])).
% 51.11/51.33 cnf(c13224,plain,eqangle(X5949,X5948,X5949,X5948,X5947,X5946,X5947,X5946),inference(resolution,[status(thm)],[c8200, c344])).
% 51.11/51.33 cnf(c13703,plain,~perp(X7013,X7012,X7013,X7012)|perp(X7011,X7014,X7011,X7014),inference(resolution,[status(thm)],[c13224, c161])).
% 51.11/51.33 cnf(c14463,plain,perp(X7087,X7086,X7087,X7086),inference(resolution,[status(thm)],[c14436, c13703])).
% 51.11/51.33 cnf(c14502,plain,~para(X13019,X13020,X13018,X13021)|perp(X13019,X13020,X13018,X13021),inference(resolution,[status(thm)],[c14463, c379])).
% 51.11/51.33 cnf(c20300,plain,perp(X13024,X13022,X13023,X13025),inference(resolution,[status(thm)],[c14502, c19624])).
% 51.11/51.33 cnf(c20302,plain,$false,inference(resolution,[status(thm)],[c20300, c21])).
% 51.11/51.33 % SZS output end CNFRefutation
% 51.11/51.33
% 51.11/51.33 % Initial clauses : 133
% 51.11/51.33 % Processed clauses : 2876
% 51.11/51.33 % Factors computed : 142
% 51.11/51.33 % Resolvents computed: 19754
% 51.11/51.33 % Tautologies deleted: 12
% 51.11/51.33 % Forward subsumed : 7562
% 51.11/51.33 % Backward subsumed : 2714
% 51.11/51.33 % -------- CPU Time ---------
% 51.11/51.33 % User time : 50.893 s
% 51.11/51.33 % System time : 0.055 s
% 51.11/51.33 % Total time : 50.948 s
%------------------------------------------------------------------------------