%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO638+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:28 EDT 2024
% Result : Theorem 49.47s 49.63s
% Output : Refutation 49.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO638+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n013.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:05:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 49.47/49.63 % Version: 1.5
% 49.47/49.63 % SZS status Theorem
% 49.47/49.63 % SZS output start CNFRefutation
% 49.47/49.63 fof(exemplo6GDDFULL81109104,conjecture,(![A]:(![B]:(![E]:(![G]:(![D]:(![C]:(![F]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(((((((((midp(E,A,B)&circle(E,A,NWPNT1,NWPNT2))&circle(E,A,G,NWPNT3))&perp(E,G,G,D))¶(A,D,C,B))&coll(C,G,D))&midp(F,C,D))&perp(H,F,A,B))&coll(H,A,B))=>perp(C,H,D,H))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL81109104)).
% 49.47/49.63 fof(c11,negated_conjecture,(~(![A]:(![B]:(![E]:(![G]:(![D]:(![C]:(![F]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(((((((((midp(E,A,B)&circle(E,A,NWPNT1,NWPNT2))&circle(E,A,G,NWPNT3))&perp(E,G,G,D))¶(A,D,C,B))&coll(C,G,D))&midp(F,C,D))&perp(H,F,A,B))&coll(H,A,B))=>perp(C,H,D,H)))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL81109104])).
% 49.47/49.63 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[E]:(?[G]:(?[D]:(?[C]:(?[F]:(?[H]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(((((((((midp(E,A,B)&circle(E,A,NWPNT1,NWPNT2))&circle(E,A,G,NWPNT3))&perp(E,G,G,D))¶(A,D,C,B))&coll(C,G,D))&midp(F,C,D))&perp(H,F,A,B))&coll(H,A,B))&~perp(C,H,D,H))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 49.47/49.63 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[E]:(?[G]:(?[D]:(?[C]:(?[F]:(?[H]:(((((((((midp(E,A,B)&(?[NWPNT1]:(?[NWPNT2]:circle(E,A,NWPNT1,NWPNT2))))&(?[NWPNT3]:circle(E,A,G,NWPNT3)))&perp(E,G,G,D))¶(A,D,C,B))&coll(C,G,D))&midp(F,C,D))&perp(H,F,A,B))&coll(H,A,B))&~perp(C,H,D,H)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 49.47/49.63 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((midp(X4,X2,X3)&(?[X10]:(?[X11]:circle(X4,X2,X10,X11))))&(?[X12]:circle(X4,X2,X5,X12)))&perp(X4,X5,X5,X6))¶(X2,X6,X7,X3))&coll(X7,X5,X6))&midp(X8,X7,X6))&perp(X9,X8,X2,X3))&coll(X9,X2,X3))&~perp(X7,X9,X6,X9)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 49.47/49.63 fof(c15,negated_conjecture,(((((((((midp(skolem0003,skolem0001,skolem0002)&circle(skolem0003,skolem0001,skolem0009,skolem0010))&circle(skolem0003,skolem0001,skolem0004,skolem0011))&perp(skolem0003,skolem0004,skolem0004,skolem0005))¶(skolem0001,skolem0005,skolem0006,skolem0002))&coll(skolem0006,skolem0004,skolem0005))&midp(skolem0007,skolem0006,skolem0005))&perp(skolem0008,skolem0007,skolem0001,skolem0002))&coll(skolem0008,skolem0001,skolem0002))&~perp(skolem0006,skolem0008,skolem0005,skolem0008)),inference(skolemize,[status(esa)],[c14])).
% 49.47/49.63 cnf(c25,negated_conjecture,~perp(skolem0006,skolem0008,skolem0005,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c161,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])).
% 49.47/49.63 fof(c162,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)],[c161])).
% 49.47/49.63 fof(c164,plain,(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:(![X133]:(![X134]:(![X135]:((~eqangle(X128,X129,X130,X131,X132,X133,X134,X135)|~perp(X132,X133,X134,X135))|perp(X128,X129,X130,X131)))))))))),inference(shift_quantors,[status(thm)],[fof(c163,plain,(![X128]:(![X129]:(![X130]:(![X131]:((![X132]:(![X133]:(![X134]:(![X135]:(~eqangle(X128,X129,X130,X131,X132,X133,X134,X135)|~perp(X132,X133,X134,X135))))))|perp(X128,X129,X130,X131)))))),inference(variable_rename,[status(thm)],[c162])).])).
% 49.47/49.63 cnf(c165,plain,~eqangle(X910,X912,X913,X907,X914,X908,X911,X909)|~perp(X914,X908,X911,X909)|perp(X910,X912,X913,X907),inference(split_conjunct,[status(thm)],[c164])).
% 49.47/49.63 fof(ruleD18,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(B,A,C,D,P,Q,U,V)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD18)).
% 49.47/49.63 fof(c355,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(B,A,C,D,P,Q,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD18])).
% 49.47/49.63 fof(c356,plain,(![X453]:(![X454]:(![X455]:(![X456]:(![X457]:(![X458]:(![X459]:(![X460]:(~eqangle(X453,X454,X455,X456,X457,X458,X459,X460)|eqangle(X454,X453,X455,X456,X457,X458,X459,X460)))))))))),inference(variable_rename,[status(thm)],[c355])).
% 49.47/49.63 cnf(c357,plain,~eqangle(X1229,X1228,X1225,X1230,X1231,X1226,X1227,X1224)|eqangle(X1228,X1229,X1225,X1230,X1231,X1226,X1227,X1224),inference(split_conjunct,[status(thm)],[c356])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c352,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])).
% 49.47/49.63 fof(c353,plain,(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(![X451]:(![X452]:(~eqangle(X445,X446,X447,X448,X449,X450,X451,X452)|eqangle(X447,X448,X445,X446,X451,X452,X449,X450)))))))))),inference(variable_rename,[status(thm)],[c352])).
% 49.47/49.63 cnf(c354,plain,~eqangle(X1220,X1218,X1221,X1215,X1214,X1219,X1216,X1217)|eqangle(X1221,X1215,X1220,X1218,X1216,X1217,X1214,X1219),inference(split_conjunct,[status(thm)],[c353])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c283,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])).
% 49.47/49.63 fof(c284,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)],[c283])).
% 49.47/49.63 fof(c286,plain,(![X293]:(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(~para(X293,X294,X295,X296)|eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c285,plain,(![X293]:(![X294]:(![X295]:(![X296]:(~para(X293,X294,X295,X296)|(![X297]:(![X298]:eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(variable_rename,[status(thm)],[c284])).])).
% 49.47/49.63 cnf(c287,plain,~para(X1065,X1062,X1060,X1064)|eqangle(X1065,X1062,X1063,X1061,X1060,X1064,X1063,X1061),inference(split_conjunct,[status(thm)],[c286])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 49.47/49.63 fof(c400,plain,(![X520]:(![X521]:(![X522]:(![X523]:(~para(X520,X521,X522,X523)|para(X520,X521,X523,X522)))))),inference(variable_rename,[status(thm)],[c399])).
% 49.47/49.63 cnf(c401,plain,~para(X794,X795,X796,X793)|para(X794,X795,X793,X796),inference(split_conjunct,[status(thm)],[c400])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c288,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])).
% 49.47/49.63 fof(c289,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)],[c288])).
% 49.47/49.63 fof(c291,plain,(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)|para(X299,X300,X301,X302)))))))),inference(shift_quantors,[status(thm)],[fof(c290,plain,(![X299]:(![X300]:(![X301]:(![X302]:((![X303]:(![X304]:~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))|para(X299,X300,X301,X302)))))),inference(variable_rename,[status(thm)],[c289])).])).
% 49.47/49.63 cnf(c292,plain,~eqangle(X1070,X1071,X1072,X1074,X1069,X1073,X1072,X1074)|para(X1070,X1071,X1069,X1073),inference(split_conjunct,[status(thm)],[c291])).
% 49.47/49.63 cnf(c22,negated_conjecture,midp(skolem0007,skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 49.47/49.63 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 49.47/49.63 fof(c378,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 49.47/49.63 fof(c379,plain,(![X487]:(![X488]:(![X489]:(~midp(X489,X488,X487)|midp(X489,X487,X488))))),inference(variable_rename,[status(thm)],[c378])).
% 49.47/49.63 cnf(c380,plain,~midp(X561,X563,X562)|midp(X561,X562,X563),inference(split_conjunct,[status(thm)],[c379])).
% 49.47/49.63 cnf(c421,plain,midp(skolem0007,skolem0005,skolem0006),inference(resolution,[status(thm)],[c380, c22])).
% 49.47/49.63 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 49.47/49.63 fof(c200,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 49.47/49.63 fof(c201,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c200])).
% 49.47/49.63 fof(c203,plain,(![X180]:(![X181]:(![X182]:(![X183]:(![X184]:((~midp(X184,X180,X181)|~midp(X184,X182,X183))|para(X180,X182,X181,X183))))))),inference(shift_quantors,[status(thm)],[fof(c202,plain,(![X180]:(![X181]:(![X182]:(![X183]:((![X184]:(~midp(X184,X180,X181)|~midp(X184,X182,X183)))|para(X180,X182,X181,X183)))))),inference(variable_rename,[status(thm)],[c201])).])).
% 49.47/49.63 cnf(c204,plain,~midp(X950,X951,X952)|~midp(X950,X954,X953)|para(X951,X954,X952,X953),inference(split_conjunct,[status(thm)],[c203])).
% 49.47/49.63 cnf(c1251,plain,~midp(skolem0007,X1633,X1634)|para(X1633,skolem0006,X1634,skolem0005),inference(resolution,[status(thm)],[c204, c22])).
% 49.47/49.63 cnf(c2430,plain,para(skolem0005,skolem0006,skolem0006,skolem0005),inference(resolution,[status(thm)],[c1251, c421])).
% 49.47/49.63 cnf(c2440,plain,para(skolem0005,skolem0006,skolem0005,skolem0006),inference(resolution,[status(thm)],[c2430, c401])).
% 49.47/49.63 cnf(c2466,plain,eqangle(skolem0005,skolem0006,X1779,X1778,skolem0005,skolem0006,X1779,X1778),inference(resolution,[status(thm)],[c2440, c287])).
% 49.47/49.63 cnf(c3004,plain,eqangle(X1998,X1999,skolem0005,skolem0006,X1998,X1999,skolem0005,skolem0006),inference(resolution,[status(thm)],[c2466, c354])).
% 49.47/49.63 cnf(c3568,plain,para(X2000,X2001,X2000,X2001),inference(resolution,[status(thm)],[c3004, c292])).
% 49.47/49.63 cnf(c3582,plain,para(X2025,X2024,X2024,X2025),inference(resolution,[status(thm)],[c3568, c401])).
% 49.47/49.63 cnf(c3854,plain,eqangle(X2745,X2746,X2748,X2747,X2746,X2745,X2748,X2747),inference(resolution,[status(thm)],[c3582, c287])).
% 49.47/49.63 cnf(c5445,plain,eqangle(X2791,X2793,X2790,X2792,X2791,X2793,X2792,X2790),inference(resolution,[status(thm)],[c3854, c354])).
% 49.47/49.63 cnf(c5487,plain,eqangle(X2845,X2844,X2843,X2842,X2844,X2845,X2842,X2843),inference(resolution,[status(thm)],[c5445, c357])).
% 49.47/49.63 cnf(c5520,plain,~perp(X14029,X14028,X14027,X14030)|perp(X14028,X14029,X14030,X14027),inference(resolution,[status(thm)],[c5487, c165])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c226,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])).
% 49.47/49.63 fof(c227,plain,(![X219]:(![X220]:(![X221]:(![X222]:((~cong(X219,X221,X220,X221)|~cong(X219,X222,X220,X222))|perp(X219,X220,X221,X222)))))),inference(variable_rename,[status(thm)],[c226])).
% 49.47/49.63 cnf(c228,plain,~cong(X984,X986,X983,X986)|~cong(X984,X985,X983,X985)|perp(X984,X983,X986,X985),inference(split_conjunct,[status(thm)],[c227])).
% 49.47/49.63 cnf(c1310,plain,~cong(X1102,X1103,X1104,X1103)|perp(X1102,X1104,X1103,X1103),inference(factor,[status(thm)],[c228])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c402,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 49.47/49.63 fof(c403,plain,(![X524]:(![X525]:(![X526]:(![X527]:((~coll(X524,X525,X526)|~coll(X524,X525,X527))|coll(X526,X527,X524)))))),inference(variable_rename,[status(thm)],[c402])).
% 49.47/49.63 cnf(c404,plain,~coll(X822,X819,X820)|~coll(X822,X819,X821)|coll(X820,X821,X822),inference(split_conjunct,[status(thm)],[c403])).
% 49.47/49.63 cnf(c764,plain,~coll(X825,X824,X823)|coll(X823,X823,X825),inference(factor,[status(thm)],[c404])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c191,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 49.47/49.63 fof(c192,plain,(![X167]:(![X168]:(![X169]:(~para(X167,X168,X167,X169)|coll(X167,X168,X169))))),inference(variable_rename,[status(thm)],[c191])).
% 49.47/49.63 cnf(c193,plain,~para(X686,X687,X686,X685)|coll(X686,X687,X685),inference(split_conjunct,[status(thm)],[c192])).
% 49.47/49.63 cnf(c3588,plain,coll(X2002,X2003,X2003),inference(resolution,[status(thm)],[c3568, c193])).
% 49.47/49.63 cnf(c3641,plain,coll(X2010,X2010,X2011),inference(resolution,[status(thm)],[c3588, c764])).
% 49.47/49.63 cnf(c3815,plain,~coll(X2650,X2650,X2648)|coll(X2648,X2649,X2650),inference(resolution,[status(thm)],[c3641, c404])).
% 49.47/49.63 cnf(c5365,plain,coll(X2658,X2659,X2657),inference(resolution,[status(thm)],[c3815, c3641])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c188,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 49.47/49.63 fof(c189,plain,(![X164]:(![X165]:(![X166]:((~cong(X164,X165,X164,X166)|~coll(X164,X165,X166))|midp(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c188])).
% 49.47/49.63 cnf(c190,plain,~cong(X939,X938,X939,X937)|~coll(X939,X938,X937)|midp(X939,X938,X937),inference(split_conjunct,[status(thm)],[c189])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 49.47/49.63 fof(c365,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X472,X471,X473)))))),inference(variable_rename,[status(thm)],[c364])).
% 49.47/49.63 cnf(c366,plain,~cyclic(X738,X736,X737,X739)|cyclic(X738,X737,X736,X739),inference(split_conjunct,[status(thm)],[c365])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 49.47/49.63 fof(c362,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X467,X466,X468,X469)))))),inference(variable_rename,[status(thm)],[c361])).
% 49.47/49.63 cnf(c363,plain,~cyclic(X735,X734,X733,X732)|cyclic(X734,X735,X733,X732),inference(split_conjunct,[status(thm)],[c362])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c367,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 49.47/49.63 fof(c368,plain,(![X474]:(![X475]:(![X476]:(![X477]:(~cyclic(X474,X475,X476,X477)|cyclic(X474,X475,X477,X476)))))),inference(variable_rename,[status(thm)],[c367])).
% 49.47/49.63 cnf(c369,plain,~cyclic(X741,X743,X740,X742)|cyclic(X741,X743,X742,X740),inference(split_conjunct,[status(thm)],[c368])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c273,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])).
% 49.47/49.63 fof(c274,plain,(![X281]:(![X282]:(![X283]:(![X284]:((~eqangle(X283,X281,X283,X282,X284,X281,X284,X282)|~coll(X283,X284,X282))|cyclic(X281,X282,X283,X284)))))),inference(variable_rename,[status(thm)],[c273])).
% 49.47/49.63 cnf(c275,plain,~eqangle(X1045,X1048,X1045,X1047,X1046,X1048,X1046,X1047)|~coll(X1045,X1046,X1047)|cyclic(X1048,X1047,X1045,X1046),inference(split_conjunct,[status(thm)],[c274])).
% 49.47/49.63 cnf(c3580,plain,eqangle(X2508,X2507,X2510,X2509,X2508,X2507,X2510,X2509),inference(resolution,[status(thm)],[c3568, c287])).
% 49.47/49.63 cnf(c5154,plain,~coll(X2909,X2909,X2910)|cyclic(X2911,X2910,X2909,X2909),inference(resolution,[status(thm)],[c3580, c275])).
% 49.47/49.63 cnf(c5540,plain,cyclic(X2912,X2913,X2914,X2914),inference(resolution,[status(thm)],[c5154, c5365])).
% 49.47/49.63 cnf(c5544,plain,cyclic(X2918,X2919,X2920,X2919),inference(resolution,[status(thm)],[c5540, c366])).
% 49.47/49.63 cnf(c5551,plain,cyclic(X2927,X2929,X2929,X2928),inference(resolution,[status(thm)],[c5544, c369])).
% 49.47/49.63 cnf(c5562,plain,cyclic(X2943,X2944,X2943,X2945),inference(resolution,[status(thm)],[c5551, c363])).
% 49.47/49.63 cnf(c5576,plain,cyclic(X2961,X2961,X2960,X2959),inference(resolution,[status(thm)],[c5562, c366])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c268,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])).
% 49.47/49.63 fof(c269,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)],[c268])).
% 49.47/49.63 fof(c271,plain,(![X275]:(![X276]:(![X277]:(![X278]:(![X279]:(![X280]:((((~cyclic(X275,X276,X277,X278)|~cyclic(X275,X276,X277,X279))|~cyclic(X275,X276,X277,X280))|~eqangle(X277,X275,X277,X276,X280,X278,X280,X279))|cong(X275,X276,X278,X279)))))))),inference(shift_quantors,[status(thm)],[fof(c270,plain,(![X275]:(![X276]:(![X277]:(![X278]:(![X279]:((![X280]:(((~cyclic(X275,X276,X277,X278)|~cyclic(X275,X276,X277,X279))|~cyclic(X275,X276,X277,X280))|~eqangle(X277,X275,X277,X276,X280,X278,X280,X279)))|cong(X275,X276,X278,X279))))))),inference(variable_rename,[status(thm)],[c269])).])).
% 49.47/49.63 cnf(c272,plain,~cyclic(X1042,X1040,X1039,X1043)|~cyclic(X1042,X1040,X1039,X1044)|~cyclic(X1042,X1040,X1039,X1041)|~eqangle(X1039,X1042,X1039,X1040,X1041,X1043,X1041,X1044)|cong(X1042,X1040,X1043,X1044),inference(split_conjunct,[status(thm)],[c271])).
% 49.47/49.63 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 49.47/49.63 fof(c349,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])).
% 49.47/49.63 fof(c350,plain,(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(~eqangle(X437,X438,X439,X440,X441,X442,X443,X444)|eqangle(X441,X442,X443,X444,X437,X438,X439,X440)))))))))),inference(variable_rename,[status(thm)],[c349])).
% 49.47/49.63 cnf(c351,plain,~eqangle(X1206,X1208,X1211,X1207,X1209,X1213,X1212,X1210)|eqangle(X1209,X1213,X1212,X1210,X1206,X1208,X1211,X1207),inference(split_conjunct,[status(thm)],[c350])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c346,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])).
% 49.47/49.63 fof(c347,plain,(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(![X434]:(![X435]:(![X436]:(~eqangle(X429,X430,X431,X432,X433,X434,X435,X436)|eqangle(X429,X430,X433,X434,X431,X432,X435,X436)))))))))),inference(variable_rename,[status(thm)],[c346])).
% 49.47/49.63 cnf(c348,plain,~eqangle(X1198,X1200,X1203,X1205,X1202,X1204,X1201,X1199)|eqangle(X1198,X1200,X1202,X1204,X1203,X1205,X1201,X1199),inference(split_conjunct,[status(thm)],[c347])).
% 49.47/49.63 cnf(c5441,plain,eqangle(X2774,X2775,X2775,X2774,X2773,X2772,X2773,X2772),inference(resolution,[status(thm)],[c3854, c348])).
% 49.47/49.63 cnf(c5470,plain,eqangle(X2819,X2821,X2819,X2821,X2820,X2822,X2822,X2820),inference(resolution,[status(thm)],[c5441, c351])).
% 49.47/49.63 cnf(c5503,plain,~cyclic(X3819,X3819,X3817,X3818)|cong(X3819,X3819,X3818,X3818),inference(resolution,[status(thm)],[c5470, c272])).
% 49.47/49.63 cnf(c6132,plain,cong(X3824,X3824,X3823,X3823),inference(resolution,[status(thm)],[c5503, c5576])).
% 49.47/49.63 cnf(c6145,plain,~coll(X3862,X3862,X3862)|midp(X3862,X3862,X3862),inference(resolution,[status(thm)],[c6132, c190])).
% 49.47/49.63 cnf(c6236,plain,midp(X3867,X3867,X3867),inference(resolution,[status(thm)],[c6145, c5365])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c197,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])).
% 49.47/49.63 fof(c198,plain,(![X175]:(![X176]:(![X177]:(![X178]:(![X179]:(((~midp(X179,X175,X176)|~para(X175,X177,X176,X178))|~para(X175,X178,X176,X177))|midp(X179,X177,X178))))))),inference(variable_rename,[status(thm)],[c197])).
% 49.47/49.63 cnf(c199,plain,~midp(X948,X949,X945)|~para(X949,X946,X945,X947)|~para(X949,X947,X945,X946)|midp(X948,X946,X947),inference(split_conjunct,[status(thm)],[c198])).
% 49.47/49.63 cnf(c1235,plain,~midp(X3985,X3987,X3984)|~para(X3987,X3986,X3984,X3986)|midp(X3985,X3986,X3986),inference(factor,[status(thm)],[c199])).
% 49.47/49.63 cnf(c6890,plain,~midp(X4078,X4077,X4077)|midp(X4078,X4076,X4076),inference(resolution,[status(thm)],[c1235, c3568])).
% 49.47/49.63 cnf(c7116,plain,midp(X4080,X4079,X4079),inference(resolution,[status(thm)],[c6890, c6236])).
% 49.47/49.63 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)).
% 49.47/49.63 fof(c240,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])).
% 49.47/49.63 fof(c241,plain,(![X235]:(![X236]:(![X237]:(![X238]:((~perp(X235,X236,X236,X237)|~midp(X238,X235,X237))|cong(X235,X238,X236,X238)))))),inference(variable_rename,[status(thm)],[c240])).
% 49.47/49.63 cnf(c242,plain,~perp(X1001,X999,X999,X1002)|~midp(X1000,X1001,X1002)|cong(X1001,X1000,X999,X1000),inference(split_conjunct,[status(thm)],[c241])).
% 49.47/49.63 cnf(c5477,plain,~perp(X3791,X3794,X3791,X3794)|perp(X3792,X3793,X3793,X3792),inference(resolution,[status(thm)],[c5441, c165])).
% 49.47/49.63 cnf(c6163,plain,perp(X3838,X3838,X3838,X3838),inference(resolution,[status(thm)],[c6132, c1310])).
% 49.47/49.63 cnf(c6192,plain,perp(X3846,X3847,X3847,X3846),inference(resolution,[status(thm)],[c6163, c5477])).
% 49.47/49.63 cnf(c6231,plain,~midp(X4731,X4732,X4732)|cong(X4732,X4731,X4733,X4731),inference(resolution,[status(thm)],[c6192, c242])).
% 49.47/49.63 cnf(c8243,plain,cong(X4735,X4736,X4734,X4736),inference(resolution,[status(thm)],[c6231, c7116])).
% 49.47/49.63 cnf(c8272,plain,perp(X4748,X4747,X4746,X4746),inference(resolution,[status(thm)],[c8243, c1310])).
% 49.47/49.63 fof(ruleD41,axiom,(![A]:(![B]:(![P]:(![Q]:(cyclic(A,B,P,Q)=>eqangle(P,A,P,B,Q,A,Q,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD41)).
% 49.47/49.63 fof(c280,plain,(![A]:(![B]:(![P]:(![Q]:(~cyclic(A,B,P,Q)|eqangle(P,A,P,B,Q,A,Q,B)))))),inference(fof_nnf,[status(thm)],[ruleD41])).
% 49.47/49.63 fof(c281,plain,(![X289]:(![X290]:(![X291]:(![X292]:(~cyclic(X289,X290,X291,X292)|eqangle(X291,X289,X291,X290,X292,X289,X292,X290)))))),inference(variable_rename,[status(thm)],[c280])).
% 49.47/49.63 cnf(c282,plain,~cyclic(X1058,X1057,X1056,X1059)|eqangle(X1056,X1058,X1056,X1057,X1059,X1058,X1059,X1057),inference(split_conjunct,[status(thm)],[c281])).
% 49.47/49.63 cnf(c5553,plain,eqangle(X2980,X2978,X2980,X2979,X2979,X2978,X2979,X2979),inference(resolution,[status(thm)],[c5544, c282])).
% 49.47/49.63 cnf(c5598,plain,~perp(X14578,X14577,X14578,X14578)|perp(X14576,X14577,X14576,X14578),inference(resolution,[status(thm)],[c5553, c165])).
% 49.47/49.63 cnf(c29474,plain,perp(X14583,X14585,X14583,X14584),inference(resolution,[status(thm)],[c5598, c8272])).
% 49.47/49.63 cnf(c29485,plain,perp(X14590,X14591,X14589,X14591),inference(resolution,[status(thm)],[c29474, c5520])).
% 49.47/49.63 cnf(c29523,plain,$false,inference(resolution,[status(thm)],[c29485, c25])).
% 49.47/49.63 % SZS output end CNFRefutation
% 49.47/49.63
% 49.47/49.63 % Initial clauses : 137
% 49.47/49.63 % Processed clauses : 2482
% 49.47/49.63 % Factors computed : 549
% 49.47/49.63 % Resolvents computed: 28575
% 49.47/49.63 % Tautologies deleted: 44
% 49.47/49.63 % Forward subsumed : 8570
% 49.47/49.63 % Backward subsumed : 1901
% 49.47/49.63 % -------- CPU Time ---------
% 49.47/49.63 % User time : 49.244 s
% 49.47/49.63 % System time : 0.052 s
% 49.47/49.63 % Total time : 49.296 s
%------------------------------------------------------------------------------