%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO636+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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 11.52s 11.70s
% Output : Refutation 11.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO636+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.36 % Computer : n013.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Thu May 9 08:04:22 EDT 2024
% 0.13/0.36 % CPUTime :
% 11.52/11.70 % Version: 1.5
% 11.52/11.70 % SZS status Theorem
% 11.52/11.70 % SZS output start CNFRefutation
% 11.52/11.70 fof(exemplo6GDDFULL8110999,conjecture,(![A]:(![B]:(![C]:(![M]:(![N]:(![Q]:(![P]:(((((eqangle(C,A,A,N,M,A,A,B)&perp(Q,M,A,B))&coll(Q,A,B))&perp(P,M,A,C))&coll(P,A,C))=>perp(A,N,P,Q))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL8110999)).
% 11.52/11.70 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![M]:(![N]:(![Q]:(![P]:(((((eqangle(C,A,A,N,M,A,A,B)&perp(Q,M,A,B))&coll(Q,A,B))&perp(P,M,A,C))&coll(P,A,C))=>perp(A,N,P,Q)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110999])).
% 11.52/11.70 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[M]:(?[N]:(?[Q]:(?[P]:(((((eqangle(C,A,A,N,M,A,A,B)&perp(Q,M,A,B))&coll(Q,A,B))&perp(P,M,A,C))&coll(P,A,C))&~perp(A,N,P,Q))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 11.52/11.70 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((eqangle(X4,X2,X2,X6,X5,X2,X2,X3)&perp(X7,X5,X2,X3))&coll(X7,X2,X3))&perp(X8,X5,X2,X4))&coll(X8,X2,X4))&~perp(X2,X6,X8,X7))))))))),inference(variable_rename,[status(thm)],[c12])).
% 11.52/11.70 fof(c14,negated_conjecture,(((((eqangle(skolem0003,skolem0001,skolem0001,skolem0005,skolem0004,skolem0001,skolem0001,skolem0002)&perp(skolem0006,skolem0004,skolem0001,skolem0002))&coll(skolem0006,skolem0001,skolem0002))&perp(skolem0007,skolem0004,skolem0001,skolem0003))&coll(skolem0007,skolem0001,skolem0003))&~perp(skolem0001,skolem0005,skolem0007,skolem0006)),inference(skolemize,[status(esa)],[c13])).
% 11.52/11.70 cnf(c20,negated_conjecture,~perp(skolem0001,skolem0005,skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 11.52/11.70 fof(c398,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c397])).
% 11.52/11.70 cnf(c399,plain,~coll(X725,X724,X723)|~coll(X725,X724,X726)|coll(X723,X726,X725),inference(split_conjunct,[status(thm)],[c398])).
% 11.52/11.70 cnf(c494,plain,~coll(X729,X728,X727)|coll(X727,X727,X729),inference(factor,[status(thm)],[c399])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c186,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 11.52/11.70 fof(c187,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c186])).
% 11.52/11.70 cnf(c188,plain,~para(X599,X600,X599,X601)|coll(X599,X600,X601),inference(split_conjunct,[status(thm)],[c187])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c283,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])).
% 11.52/11.70 fof(c284,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)],[c283])).
% 11.52/11.70 fof(c286,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(c285,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)],[c284])).])).
% 11.52/11.70 cnf(c287,plain,~eqangle(X1076,X1078,X1075,X1074,X1077,X1079,X1075,X1074)|para(X1076,X1078,X1077,X1079),inference(split_conjunct,[status(thm)],[c286])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c347,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])).
% 11.52/11.70 fof(c348,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)],[c347])).
% 11.52/11.70 cnf(c349,plain,~eqangle(X1214,X1217,X1213,X1218,X1215,X1216,X1219,X1212)|eqangle(X1213,X1218,X1214,X1217,X1219,X1212,X1215,X1216),inference(split_conjunct,[status(thm)],[c348])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c278,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])).
% 11.52/11.70 fof(c279,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)],[c278])).
% 11.52/11.70 fof(c281,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(c280,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)],[c279])).])).
% 11.52/11.70 cnf(c282,plain,~para(X1068,X1070,X1073,X1069)|eqangle(X1068,X1070,X1072,X1071,X1073,X1069,X1072,X1071),inference(split_conjunct,[status(thm)],[c281])).
% 11.52/11.70 cnf(c16,negated_conjecture,perp(skolem0006,skolem0004,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c382,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 11.52/11.70 fof(c383,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c382])).
% 11.52/11.70 cnf(c384,plain,~perp(X646,X648,X649,X647)|perp(X649,X647,X646,X648),inference(split_conjunct,[status(thm)],[c383])).
% 11.52/11.70 cnf(c447,plain,perp(skolem0001,skolem0002,skolem0006,skolem0004),inference(resolution,[status(thm)],[c384, c16])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c379,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])).
% 11.52/11.70 fof(c380,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)],[c379])).
% 11.52/11.70 cnf(c381,plain,~perp(X1272,X1269,X1271,X1268)|~perp(X1271,X1268,X1270,X1273)|para(X1272,X1269,X1270,X1273),inference(split_conjunct,[status(thm)],[c380])).
% 11.52/11.70 cnf(c1428,plain,~perp(X1869,X1868,skolem0006,skolem0004)|para(X1869,X1868,skolem0001,skolem0002),inference(resolution,[status(thm)],[c381, c16])).
% 11.52/11.70 cnf(c2352,plain,para(skolem0001,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1428, c447])).
% 11.52/11.70 cnf(c2362,plain,eqangle(skolem0001,skolem0002,X1886,X1887,skolem0001,skolem0002,X1886,X1887),inference(resolution,[status(thm)],[c2352, c282])).
% 11.52/11.70 cnf(c2455,plain,eqangle(X1906,X1907,skolem0001,skolem0002,X1906,X1907,skolem0001,skolem0002),inference(resolution,[status(thm)],[c2362, c349])).
% 11.52/11.70 cnf(c2560,plain,para(X1908,X1909,X1908,X1909),inference(resolution,[status(thm)],[c2455, c287])).
% 11.52/11.70 cnf(c2566,plain,coll(X1914,X1915,X1915),inference(resolution,[status(thm)],[c2560, c188])).
% 11.52/11.70 cnf(c2706,plain,coll(X1921,X1921,X1920),inference(resolution,[status(thm)],[c2566, c494])).
% 11.52/11.70 cnf(c2882,plain,~coll(X2554,X2554,X2552)|coll(X2552,X2553,X2554),inference(resolution,[status(thm)],[c2706, c399])).
% 11.52/11.70 cnf(c4537,plain,coll(X2562,X2560,X2561),inference(resolution,[status(thm)],[c2882, c2706])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c183,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 11.52/11.70 fof(c184,plain,(![X160]:(![X161]:(![X162]:((~cong(X160,X161,X160,X162)|~coll(X160,X161,X162))|midp(X160,X161,X162))))),inference(variable_rename,[status(thm)],[c183])).
% 11.52/11.70 cnf(c185,plain,~cong(X948,X949,X948,X950)|~coll(X948,X949,X950)|midp(X948,X949,X950),inference(split_conjunct,[status(thm)],[c184])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 11.52/11.70 fof(c336,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c335])).
% 11.52/11.70 cnf(c337,plain,~cong(X617,X616,X614,X615)|cong(X617,X616,X615,X614),inference(split_conjunct,[status(thm)],[c336])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c332,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 11.52/11.70 fof(c333,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c332])).
% 11.52/11.70 cnf(c334,plain,~cong(X611,X613,X612,X610)|cong(X612,X610,X611,X613),inference(split_conjunct,[status(thm)],[c333])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c192,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])).
% 11.52/11.70 fof(c193,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)],[c192])).
% 11.52/11.70 cnf(c194,plain,~midp(X956,X960,X958)|~para(X960,X957,X958,X959)|~para(X960,X959,X958,X957)|midp(X956,X957,X959),inference(split_conjunct,[status(thm)],[c193])).
% 11.52/11.70 cnf(c970,plain,~midp(X1811,X1813,X1810)|~para(X1813,X1812,X1810,X1812)|midp(X1811,X1812,X1812),inference(factor,[status(thm)],[c194])).
% 11.52/11.70 cnf(c2578,plain,~midp(X2424,X2425,X2425)|midp(X2424,X2426,X2426),inference(resolution,[status(thm)],[c2560, c970])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 11.52/11.70 fof(c363,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X471,X473,X472)))))),inference(variable_rename,[status(thm)],[c362])).
% 11.52/11.70 cnf(c364,plain,~cyclic(X629,X628,X627,X626)|cyclic(X629,X628,X626,X627),inference(split_conjunct,[status(thm)],[c363])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c359,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 11.52/11.70 fof(c360,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c359])).
% 11.52/11.70 cnf(c361,plain,~cyclic(X623,X624,X625,X622)|cyclic(X623,X625,X624,X622),inference(split_conjunct,[status(thm)],[c360])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c268,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])).
% 11.52/11.70 fof(c269,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)],[c268])).
% 11.52/11.70 cnf(c270,plain,~eqangle(X1058,X1059,X1058,X1057,X1056,X1059,X1056,X1057)|~coll(X1058,X1056,X1057)|cyclic(X1059,X1057,X1058,X1056),inference(split_conjunct,[status(thm)],[c269])).
% 11.52/11.70 cnf(c2577,plain,eqangle(X2421,X2420,X2419,X2418,X2421,X2420,X2419,X2418),inference(resolution,[status(thm)],[c2560, c282])).
% 11.52/11.70 cnf(c4347,plain,~coll(X2820,X2820,X2822)|cyclic(X2821,X2822,X2820,X2820),inference(resolution,[status(thm)],[c2577, c270])).
% 11.52/11.70 cnf(c4760,plain,cyclic(X2826,X2827,X2828,X2828),inference(resolution,[status(thm)],[c4347, c4537])).
% 11.52/11.70 cnf(c4763,plain,cyclic(X2829,X2830,X2831,X2830),inference(resolution,[status(thm)],[c4760, c361])).
% 11.52/11.70 cnf(c4776,plain,cyclic(X2848,X2849,X2849,X2850),inference(resolution,[status(thm)],[c4763, c364])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c263,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])).
% 11.52/11.70 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(shift_quantors,[status(thm)],[c263])).
% 11.52/11.70 fof(c266,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(c265,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)],[c264])).])).
% 11.52/11.70 cnf(c267,plain,~cyclic(X1052,X1053,X1054,X1050)|~cyclic(X1052,X1053,X1054,X1051)|~cyclic(X1052,X1053,X1054,X1055)|~eqangle(X1054,X1052,X1054,X1053,X1055,X1050,X1055,X1051)|cong(X1052,X1053,X1050,X1051),inference(split_conjunct,[status(thm)],[c266])).
% 11.52/11.70 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 11.52/11.70 fof(c344,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])).
% 11.52/11.70 fof(c345,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)],[c344])).
% 11.52/11.70 cnf(c346,plain,~eqangle(X1210,X1206,X1205,X1211,X1207,X1208,X1204,X1209)|eqangle(X1207,X1208,X1204,X1209,X1210,X1206,X1205,X1211),inference(split_conjunct,[status(thm)],[c345])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c341,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])).
% 11.52/11.70 fof(c342,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)],[c341])).
% 11.52/11.70 cnf(c343,plain,~eqangle(X1203,X1199,X1197,X1201,X1198,X1196,X1200,X1202)|eqangle(X1203,X1199,X1198,X1196,X1197,X1201,X1200,X1202),inference(split_conjunct,[status(thm)],[c342])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 11.52/11.70 fof(c395,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c394])).
% 11.52/11.70 cnf(c396,plain,~para(X714,X716,X715,X713)|para(X714,X716,X713,X715),inference(split_conjunct,[status(thm)],[c395])).
% 11.52/11.70 cnf(c2590,plain,para(X1935,X1936,X1936,X1935),inference(resolution,[status(thm)],[c2560, c396])).
% 11.52/11.70 cnf(c2906,plain,eqangle(X2640,X2639,X2638,X2637,X2639,X2640,X2638,X2637),inference(resolution,[status(thm)],[c2590, c282])).
% 11.52/11.70 cnf(c4658,plain,eqangle(X2678,X2680,X2680,X2678,X2677,X2679,X2677,X2679),inference(resolution,[status(thm)],[c2906, c343])).
% 11.52/11.70 cnf(c4697,plain,eqangle(X2735,X2732,X2735,X2732,X2733,X2734,X2734,X2733),inference(resolution,[status(thm)],[c4658, c346])).
% 11.52/11.70 cnf(c4718,plain,~cyclic(X3715,X3715,X3717,X3716)|cong(X3715,X3715,X3716,X3716),inference(resolution,[status(thm)],[c4697, c267])).
% 11.52/11.70 cnf(c5318,plain,cong(X3719,X3719,X3718,X3718),inference(resolution,[status(thm)],[c4718, c4776])).
% 11.52/11.70 cnf(c5330,plain,~coll(X3764,X3764,X3764)|midp(X3764,X3764,X3764),inference(resolution,[status(thm)],[c5318, c185])).
% 11.52/11.70 cnf(c5434,plain,midp(X3765,X3765,X3765),inference(resolution,[status(thm)],[c5330, c4537])).
% 11.52/11.70 cnf(c5442,plain,midp(X3766,X3767,X3767),inference(resolution,[status(thm)],[c5434, c2578])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c235,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])).
% 11.52/11.70 fof(c236,plain,(![X231]:(![X232]:(![X233]:(![X234]:((~perp(X231,X232,X232,X233)|~midp(X234,X231,X233))|cong(X231,X234,X232,X234)))))),inference(variable_rename,[status(thm)],[c235])).
% 11.52/11.70 cnf(c237,plain,~perp(X1013,X1012,X1012,X1010)|~midp(X1011,X1013,X1010)|cong(X1013,X1011,X1012,X1011),inference(split_conjunct,[status(thm)],[c236])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c156,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])).
% 11.52/11.70 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(shift_quantors,[status(thm)],[c156])).
% 11.52/11.70 fof(c159,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(c158,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)],[c157])).])).
% 11.52/11.70 cnf(c160,plain,~eqangle(X916,X920,X914,X919,X918,X915,X921,X917)|~perp(X918,X915,X921,X917)|perp(X916,X920,X914,X919),inference(split_conjunct,[status(thm)],[c159])).
% 11.52/11.70 cnf(c4696,plain,~perp(X3687,X3688,X3687,X3688)|perp(X3686,X3689,X3689,X3686),inference(resolution,[status(thm)],[c4658, c160])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c221,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])).
% 11.52/11.70 fof(c222,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)],[c221])).
% 11.52/11.70 cnf(c223,plain,~cong(X997,X996,X995,X996)|~cong(X997,X994,X995,X994)|perp(X997,X995,X996,X994),inference(split_conjunct,[status(thm)],[c222])).
% 11.52/11.70 cnf(c1062,plain,~cong(X1246,X1245,X1244,X1245)|perp(X1246,X1244,X1245,X1245),inference(factor,[status(thm)],[c223])).
% 11.52/11.70 cnf(c5326,plain,perp(X3733,X3733,X3733,X3733),inference(resolution,[status(thm)],[c5318, c1062])).
% 11.52/11.70 cnf(c5352,plain,perp(X3739,X3738,X3738,X3739),inference(resolution,[status(thm)],[c5326, c4696])).
% 11.52/11.70 cnf(c5384,plain,~midp(X4600,X4602,X4602)|cong(X4602,X4600,X4601,X4600),inference(resolution,[status(thm)],[c5352, c237])).
% 11.52/11.70 cnf(c7016,plain,cong(X4605,X4604,X4603,X4604),inference(resolution,[status(thm)],[c5384, c5442])).
% 11.52/11.70 cnf(c7025,plain,cong(X4614,X4613,X4613,X4612),inference(resolution,[status(thm)],[c7016, c337])).
% 11.52/11.70 cnf(c7046,plain,cong(X4631,X4630,X4629,X4631),inference(resolution,[status(thm)],[c7025, c334])).
% 11.52/11.70 cnf(c7094,plain,cong(X4656,X4657,X4656,X4655),inference(resolution,[status(thm)],[c7046, c337])).
% 11.52/11.70 cnf(c7108,plain,~coll(X4859,X4858,X4857)|midp(X4859,X4858,X4857),inference(resolution,[status(thm)],[c7094, c185])).
% 11.52/11.70 cnf(c7569,plain,midp(X4863,X4864,X4865),inference(resolution,[status(thm)],[c7108, c4537])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c260,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])).
% 11.52/11.70 fof(c261,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c260])).
% 11.52/11.70 cnf(c262,plain,~midp(X1045,X1049,X1048)|~midp(X1047,X1049,X1046)|para(X1045,X1047,X1048,X1046),inference(split_conjunct,[status(thm)],[c261])).
% 11.52/11.70 cnf(c5464,plain,~midp(X8219,X8217,X8218)|para(X8219,X8220,X8218,X8217),inference(resolution,[status(thm)],[c5442, c262])).
% 11.52/11.70 cnf(c10562,plain,para(X8222,X8223,X8221,X8224),inference(resolution,[status(thm)],[c5464, c7569])).
% 11.52/11.70 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)).
% 11.52/11.70 fof(c376,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])).
% 11.52/11.70 fof(c377,plain,(![X486]:(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:((~para(X486,X487,X488,X489)|~perp(X488,X489,X490,X491))|perp(X486,X487,X490,X491)))))))),inference(variable_rename,[status(thm)],[c376])).
% 11.52/11.70 cnf(c378,plain,~para(X1265,X1263,X1262,X1261)|~perp(X1262,X1261,X1264,X1266)|perp(X1265,X1263,X1264,X1266),inference(split_conjunct,[status(thm)],[c377])).
% 11.52/11.70 cnf(c5394,plain,~para(X10284,X10281,X10282,X10283)|perp(X10284,X10281,X10283,X10282),inference(resolution,[status(thm)],[c5352, c378])).
% 11.52/11.70 cnf(c11373,plain,perp(X10289,X10292,X10290,X10291),inference(resolution,[status(thm)],[c5394, c10562])).
% 11.52/11.70 cnf(c11374,plain,$false,inference(resolution,[status(thm)],[c11373, c20])).
% 11.52/11.70 % SZS output end CNFRefutation
% 11.52/11.70
% 11.52/11.70 % Initial clauses : 133
% 11.52/11.70 % Processed clauses : 1527
% 11.52/11.70 % Factors computed : 133
% 11.52/11.70 % Resolvents computed: 10837
% 11.52/11.70 % Tautologies deleted: 25
% 11.52/11.70 % Forward subsumed : 4473
% 11.52/11.70 % Backward subsumed : 1361
% 11.52/11.70 % -------- CPU Time ---------
% 11.52/11.70 % User time : 11.305 s
% 11.52/11.70 % System time : 0.024 s
% 11.52/11.70 % Total time : 11.329 s
%------------------------------------------------------------------------------