%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO618+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:25 EDT 2024
% Result : Theorem 19.93s 20.11s
% Output : Refutation 19.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO618+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 08:14:52 EDT 2024
% 0.12/0.33 % CPUTime :
% 19.93/20.11 % Version: 1.5
% 19.93/20.11 % SZS status Theorem
% 19.93/20.11 % SZS output start CNFRefutation
% 19.93/20.11 fof(exemplo6GDDFULL618080,conjecture,(![A]:(![B]:(![C]:(![U]:(![O]:(![T]:(((((eqangle(U,A,A,C,U,A,A,B)&coll(U,B,C))&circle(O,A,B,C))&perp(A,O,A,T))&coll(T,B,C))=>cong(T,A,T,U)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL618080)).
% 19.93/20.11 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![U]:(![O]:(![T]:(((((eqangle(U,A,A,C,U,A,A,B)&coll(U,B,C))&circle(O,A,B,C))&perp(A,O,A,T))&coll(T,B,C))=>cong(T,A,T,U))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618080])).
% 19.93/20.11 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[U]:(?[O]:(?[T]:(((((eqangle(U,A,A,C,U,A,A,B)&coll(U,B,C))&circle(O,A,B,C))&perp(A,O,A,T))&coll(T,B,C))&~cong(T,A,T,U)))))))),inference(fof_nnf,[status(thm)],[c11])).
% 19.93/20.11 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((eqangle(X5,X2,X2,X4,X5,X2,X2,X3)&coll(X5,X3,X4))&circle(X6,X2,X3,X4))&perp(X2,X6,X2,X7))&coll(X7,X3,X4))&~cong(X7,X2,X7,X5)))))))),inference(variable_rename,[status(thm)],[c12])).
% 19.93/20.11 fof(c14,negated_conjecture,(((((eqangle(skolem0004,skolem0001,skolem0001,skolem0003,skolem0004,skolem0001,skolem0001,skolem0002)&coll(skolem0004,skolem0002,skolem0003))&circle(skolem0005,skolem0001,skolem0002,skolem0003))&perp(skolem0001,skolem0005,skolem0001,skolem0006))&coll(skolem0006,skolem0002,skolem0003))&~cong(skolem0006,skolem0001,skolem0006,skolem0004)),inference(skolemize,[status(esa)],[c13])).
% 19.93/20.11 cnf(c20,negated_conjecture,~cong(skolem0006,skolem0001,skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c14])).
% 19.93/20.11 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)).
% 19.93/20.11 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 19.93/20.11 fof(c336,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X408,X409,X411,X410)))))),inference(variable_rename,[status(thm)],[c335])).
% 19.93/20.11 cnf(c337,plain,~cong(X615,X616,X614,X613)|cong(X615,X616,X613,X614),inference(split_conjunct,[status(thm)],[c336])).
% 19.93/20.11 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)).
% 19.93/20.11 fof(c332,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 19.93/20.11 fof(c333,plain,(![X404]:(![X405]:(![X406]:(![X407]:(~cong(X404,X405,X406,X407)|cong(X406,X407,X404,X405)))))),inference(variable_rename,[status(thm)],[c332])).
% 19.93/20.11 cnf(c334,plain,~cong(X609,X611,X610,X612)|cong(X610,X612,X609,X611),inference(split_conjunct,[status(thm)],[c333])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c193,plain,(![X170]:(![X171]:(![X172]:(![X173]:(![X174]:(((~midp(X174,X170,X171)|~para(X170,X172,X171,X173))|~para(X170,X173,X171,X172))|midp(X174,X172,X173))))))),inference(variable_rename,[status(thm)],[c192])).
% 19.93/20.11 cnf(c194,plain,~midp(X955,X954,X953)|~para(X954,X956,X953,X952)|~para(X954,X952,X953,X956)|midp(X955,X956,X952),inference(split_conjunct,[status(thm)],[c193])).
% 19.93/20.11 cnf(c935,plain,~midp(X1962,X1960,X1961)|~para(X1960,X1963,X1961,X1963)|midp(X1962,X1963,X1963),inference(factor,[status(thm)],[c194])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c286,plain,(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)|para(X294,X295,X296,X297)))))))),inference(shift_quantors,[status(thm)],[fof(c285,plain,(![X294]:(![X295]:(![X296]:(![X297]:((![X298]:(![X299]:~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)))|para(X294,X295,X296,X297)))))),inference(variable_rename,[status(thm)],[c284])).])).
% 19.93/20.11 cnf(c287,plain,~eqangle(X1108,X1106,X1109,X1107,X1105,X1104,X1109,X1107)|para(X1108,X1106,X1105,X1104),inference(split_conjunct,[status(thm)],[c286])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c348,plain,(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(~eqangle(X440,X441,X442,X443,X444,X445,X446,X447)|eqangle(X442,X443,X440,X441,X446,X447,X444,X445)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 19.93/20.11 cnf(c349,plain,~eqangle(X1264,X1266,X1267,X1268,X1261,X1265,X1262,X1263)|eqangle(X1267,X1268,X1264,X1266,X1262,X1263,X1261,X1265),inference(split_conjunct,[status(thm)],[c348])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c281,plain,(![X288]:(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(~para(X288,X289,X290,X291)|eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(shift_quantors,[status(thm)],[fof(c280,plain,(![X288]:(![X289]:(![X290]:(![X291]:(~para(X288,X289,X290,X291)|(![X292]:(![X293]:eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(variable_rename,[status(thm)],[c279])).])).
% 19.93/20.11 cnf(c282,plain,~para(X1101,X1098,X1097,X1100)|eqangle(X1101,X1098,X1099,X1102,X1097,X1100,X1099,X1102),inference(split_conjunct,[status(thm)],[c281])).
% 19.93/20.11 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)).
% 19.93/20.11 fof(c382,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 19.93/20.11 fof(c383,plain,(![X497]:(![X498]:(![X499]:(![X500]:(~perp(X497,X498,X499,X500)|perp(X499,X500,X497,X498)))))),inference(variable_rename,[status(thm)],[c382])).
% 19.93/20.11 cnf(c384,plain,~perp(X648,X647,X645,X646)|perp(X645,X646,X648,X647),inference(split_conjunct,[status(thm)],[c383])).
% 19.93/20.11 cnf(c18,negated_conjecture,perp(skolem0001,skolem0005,skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 19.93/20.11 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 19.93/20.11 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 19.93/20.11 fof(c386,plain,(![X501]:(![X502]:(![X503]:(![X504]:(~perp(X501,X502,X503,X504)|perp(X501,X502,X504,X503)))))),inference(variable_rename,[status(thm)],[c385])).
% 19.93/20.11 cnf(c387,plain,~perp(X651,X652,X649,X650)|perp(X651,X652,X650,X649),inference(split_conjunct,[status(thm)],[c386])).
% 19.93/20.11 cnf(c451,plain,perp(skolem0001,skolem0005,skolem0006,skolem0001),inference(resolution,[status(thm)],[c387, c18])).
% 19.93/20.11 cnf(c457,plain,perp(skolem0006,skolem0001,skolem0001,skolem0005),inference(resolution,[status(thm)],[c451, c384])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c380,plain,(![X491]:(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:((~perp(X491,X492,X493,X494)|~perp(X493,X494,X495,X496))|para(X491,X492,X495,X496)))))))),inference(variable_rename,[status(thm)],[c379])).
% 19.93/20.11 cnf(c381,plain,~perp(X1315,X1311,X1312,X1314)|~perp(X1312,X1314,X1313,X1310)|para(X1315,X1311,X1313,X1310),inference(split_conjunct,[status(thm)],[c380])).
% 19.93/20.11 cnf(c1169,plain,~perp(X2041,X2042,skolem0001,skolem0005)|para(X2041,X2042,skolem0006,skolem0001),inference(resolution,[status(thm)],[c381, c451])).
% 19.93/20.11 cnf(c4024,plain,para(skolem0006,skolem0001,skolem0006,skolem0001),inference(resolution,[status(thm)],[c1169, c457])).
% 19.93/20.11 cnf(c4032,plain,eqangle(skolem0006,skolem0001,X2591,X2590,skolem0006,skolem0001,X2591,X2590),inference(resolution,[status(thm)],[c4024, c282])).
% 19.93/20.11 cnf(c5480,plain,eqangle(X2846,X2845,skolem0006,skolem0001,X2846,X2845,skolem0006,skolem0001),inference(resolution,[status(thm)],[c4032, c349])).
% 19.93/20.11 cnf(c6560,plain,para(X2850,X2849,X2850,X2849),inference(resolution,[status(thm)],[c5480, c287])).
% 19.93/20.11 cnf(c6604,plain,~midp(X3423,X3424,X3424)|midp(X3423,X3425,X3425),inference(resolution,[status(thm)],[c6560, c935])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c398,plain,(![X519]:(![X520]:(![X521]:(![X522]:((~coll(X519,X520,X521)|~coll(X519,X520,X522))|coll(X521,X522,X519)))))),inference(variable_rename,[status(thm)],[c397])).
% 19.93/20.11 cnf(c399,plain,~coll(X710,X708,X707)|~coll(X710,X708,X709)|coll(X707,X709,X710),inference(split_conjunct,[status(thm)],[c398])).
% 19.93/20.11 cnf(c471,plain,~coll(X713,X712,X711)|coll(X711,X711,X713),inference(factor,[status(thm)],[c399])).
% 19.93/20.11 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)).
% 19.93/20.11 fof(c186,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 19.93/20.11 fof(c187,plain,(![X162]:(![X163]:(![X164]:(~para(X162,X163,X162,X164)|coll(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c186])).
% 19.93/20.11 cnf(c188,plain,~para(X599,X598,X599,X600)|coll(X599,X598,X600),inference(split_conjunct,[status(thm)],[c187])).
% 19.93/20.11 cnf(c6587,plain,coll(X2852,X2851,X2851),inference(resolution,[status(thm)],[c6560, c188])).
% 19.93/20.11 cnf(c6729,plain,coll(X2857,X2857,X2858),inference(resolution,[status(thm)],[c6587, c471])).
% 19.93/20.11 cnf(c7258,plain,~coll(X3558,X3558,X3556)|coll(X3556,X3557,X3558),inference(resolution,[status(thm)],[c6729, c399])).
% 19.93/20.11 cnf(c11166,plain,coll(X3565,X3567,X3566),inference(resolution,[status(thm)],[c7258, c6729])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c184,plain,(![X159]:(![X160]:(![X161]:((~cong(X159,X160,X159,X161)|~coll(X159,X160,X161))|midp(X159,X160,X161))))),inference(variable_rename,[status(thm)],[c183])).
% 19.93/20.11 cnf(c185,plain,~cong(X942,X944,X942,X943)|~coll(X942,X944,X943)|midp(X942,X944,X943),inference(split_conjunct,[status(thm)],[c184])).
% 19.93/20.11 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)).
% 19.93/20.11 fof(c359,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 19.93/20.11 fof(c360,plain,(![X465]:(![X466]:(![X467]:(![X468]:(~cyclic(X465,X466,X467,X468)|cyclic(X465,X467,X466,X468)))))),inference(variable_rename,[status(thm)],[c359])).
% 19.93/20.11 cnf(c361,plain,~cyclic(X622,X624,X621,X623)|cyclic(X622,X621,X624,X623),inference(split_conjunct,[status(thm)],[c360])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c269,plain,(![X276]:(![X277]:(![X278]:(![X279]:((~eqangle(X278,X276,X278,X277,X279,X276,X279,X277)|~coll(X278,X279,X277))|cyclic(X276,X277,X278,X279)))))),inference(variable_rename,[status(thm)],[c268])).
% 19.93/20.11 cnf(c270,plain,~eqangle(X1085,X1084,X1085,X1082,X1083,X1084,X1083,X1082)|~coll(X1085,X1083,X1082)|cyclic(X1084,X1082,X1085,X1083),inference(split_conjunct,[status(thm)],[c269])).
% 19.93/20.11 cnf(c6585,plain,eqangle(X3413,X3411,X3412,X3410,X3413,X3411,X3412,X3410),inference(resolution,[status(thm)],[c6560, c282])).
% 19.93/20.11 cnf(c10923,plain,~coll(X3835,X3835,X3834)|cyclic(X3833,X3834,X3835,X3835),inference(resolution,[status(thm)],[c6585, c270])).
% 19.93/20.11 cnf(c11529,plain,cyclic(X3837,X3838,X3836,X3836),inference(resolution,[status(thm)],[c10923, c11166])).
% 19.93/20.11 cnf(c11534,plain,cyclic(X3846,X3845,X3847,X3845),inference(resolution,[status(thm)],[c11529, c361])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c266,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274))|cong(X270,X271,X273,X274)))))))),inference(shift_quantors,[status(thm)],[fof(c265,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:((![X275]:(((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274)))|cong(X270,X271,X273,X274))))))),inference(variable_rename,[status(thm)],[c264])).])).
% 19.93/20.11 cnf(c267,plain,~cyclic(X1076,X1077,X1078,X1080)|~cyclic(X1076,X1077,X1078,X1075)|~cyclic(X1076,X1077,X1078,X1079)|~eqangle(X1078,X1076,X1078,X1077,X1079,X1080,X1079,X1075)|cong(X1076,X1077,X1080,X1075),inference(split_conjunct,[status(thm)],[c266])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c342,plain,(![X424]:(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(~eqangle(X424,X425,X426,X427,X428,X429,X430,X431)|eqangle(X424,X425,X428,X429,X426,X427,X430,X431)))))))))),inference(variable_rename,[status(thm)],[c341])).
% 19.93/20.11 cnf(c343,plain,~eqangle(X1249,X1246,X1245,X1247,X1250,X1248,X1244,X1243)|eqangle(X1249,X1246,X1250,X1248,X1245,X1247,X1244,X1243),inference(split_conjunct,[status(thm)],[c342])).
% 19.93/20.11 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)).
% 19.93/20.11 fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 19.93/20.11 fof(c395,plain,(![X515]:(![X516]:(![X517]:(![X518]:(~para(X515,X516,X517,X518)|para(X515,X516,X518,X517)))))),inference(variable_rename,[status(thm)],[c394])).
% 19.93/20.11 cnf(c396,plain,~para(X698,X699,X697,X700)|para(X698,X699,X700,X697),inference(split_conjunct,[status(thm)],[c395])).
% 19.93/20.11 cnf(c6592,plain,para(X2877,X2878,X2878,X2877),inference(resolution,[status(thm)],[c6560, c396])).
% 19.93/20.11 cnf(c7332,plain,eqangle(X3656,X3658,X3657,X3655,X3658,X3656,X3657,X3655),inference(resolution,[status(thm)],[c6592, c282])).
% 19.93/20.11 cnf(c11419,plain,eqangle(X3689,X3688,X3687,X3690,X3689,X3688,X3690,X3687),inference(resolution,[status(thm)],[c7332, c349])).
% 19.93/20.11 cnf(c11452,plain,eqangle(X3730,X3732,X3730,X3732,X3731,X3729,X3729,X3731),inference(resolution,[status(thm)],[c11419, c343])).
% 19.93/20.11 cnf(c11486,plain,~cyclic(X4689,X4689,X4690,X4688)|cong(X4689,X4689,X4688,X4688),inference(resolution,[status(thm)],[c11452, c267])).
% 19.93/20.11 cnf(c12292,plain,cong(X4695,X4695,X4695,X4695),inference(resolution,[status(thm)],[c11486, c11534])).
% 19.93/20.11 cnf(c12316,plain,~coll(X4746,X4746,X4746)|midp(X4746,X4746,X4746),inference(resolution,[status(thm)],[c12292, c185])).
% 19.93/20.11 cnf(c12458,plain,midp(X4747,X4747,X4747),inference(resolution,[status(thm)],[c12316, c11166])).
% 19.93/20.11 cnf(c12461,plain,midp(X4748,X4749,X4749),inference(resolution,[status(thm)],[c12458, c6604])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c236,plain,(![X230]:(![X231]:(![X232]:(![X233]:((~perp(X230,X231,X231,X232)|~midp(X233,X230,X232))|cong(X230,X233,X231,X233)))))),inference(variable_rename,[status(thm)],[c235])).
% 19.93/20.11 cnf(c237,plain,~perp(X1026,X1024,X1024,X1023)|~midp(X1025,X1026,X1023)|cong(X1026,X1025,X1024,X1025),inference(split_conjunct,[status(thm)],[c236])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c159,plain,(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:((~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))|perp(X123,X124,X125,X126)))))))))),inference(shift_quantors,[status(thm)],[fof(c158,plain,(![X123]:(![X124]:(![X125]:(![X126]:((![X127]:(![X128]:(![X129]:(![X130]:(~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))))))|perp(X123,X124,X125,X126)))))),inference(variable_rename,[status(thm)],[c157])).])).
% 19.93/20.11 cnf(c160,plain,~eqangle(X913,X907,X908,X910,X914,X912,X909,X911)|~perp(X914,X912,X909,X911)|perp(X913,X907,X908,X910),inference(split_conjunct,[status(thm)],[c159])).
% 19.93/20.11 cnf(c11423,plain,eqangle(X3698,X3696,X3696,X3698,X3695,X3697,X3695,X3697),inference(resolution,[status(thm)],[c7332, c343])).
% 19.93/20.11 cnf(c11468,plain,~perp(X4681,X4683,X4681,X4683)|perp(X4684,X4682,X4682,X4684),inference(resolution,[status(thm)],[c11423, c160])).
% 19.93/20.11 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)).
% 19.93/20.11 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])).
% 19.93/20.11 fof(c222,plain,(![X214]:(![X215]:(![X216]:(![X217]:((~cong(X214,X216,X215,X216)|~cong(X214,X217,X215,X217))|perp(X214,X215,X216,X217)))))),inference(variable_rename,[status(thm)],[c221])).
% 19.93/20.11 cnf(c223,plain,~cong(X1002,X1000,X1001,X1000)|~cong(X1002,X1003,X1001,X1003)|perp(X1002,X1001,X1000,X1003),inference(split_conjunct,[status(thm)],[c222])).
% 19.93/20.11 cnf(c966,plain,~cong(X1005,X1004,X1006,X1004)|perp(X1005,X1006,X1004,X1004),inference(factor,[status(thm)],[c223])).
% 19.93/20.11 cnf(c12301,plain,perp(X4706,X4706,X4706,X4706),inference(resolution,[status(thm)],[c12292, c966])).
% 19.93/20.11 cnf(c12359,plain,perp(X4722,X4721,X4721,X4722),inference(resolution,[status(thm)],[c12301, c11468])).
% 19.93/20.11 cnf(c12389,plain,~midp(X5485,X5487,X5487)|cong(X5487,X5485,X5486,X5485),inference(resolution,[status(thm)],[c12359, c237])).
% 19.93/20.11 cnf(c13778,plain,cong(X5488,X5489,X5490,X5489),inference(resolution,[status(thm)],[c12389, c12461])).
% 19.93/20.11 cnf(c13797,plain,cong(X5501,X5502,X5502,X5503),inference(resolution,[status(thm)],[c13778, c337])).
% 19.93/20.11 cnf(c13820,plain,cong(X5518,X5519,X5520,X5518),inference(resolution,[status(thm)],[c13797, c334])).
% 19.93/20.11 cnf(c13887,plain,cong(X5543,X5542,X5543,X5544),inference(resolution,[status(thm)],[c13820, c337])).
% 19.93/20.11 cnf(c13899,plain,$false,inference(resolution,[status(thm)],[c13887, c20])).
% 19.93/20.11 % SZS output end CNFRefutation
% 19.93/20.11
% 19.93/20.11 % Initial clauses : 133
% 19.93/20.11 % Processed clauses : 1702
% 19.93/20.11 % Factors computed : 117
% 19.93/20.11 % Resolvents computed: 13387
% 19.93/20.11 % Tautologies deleted: 12
% 19.93/20.11 % Forward subsumed : 3941
% 19.93/20.11 % Backward subsumed : 1064
% 19.93/20.11 % -------- CPU Time ---------
% 19.93/20.11 % User time : 19.733 s
% 19.93/20.11 % System time : 0.040 s
% 19.93/20.11 % Total time : 19.773 s
%------------------------------------------------------------------------------