%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO644+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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 146.64s 146.88s
% Output : Refutation 146.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO644+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n008.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:22:38 EDT 2024
% 0.12/0.33 % CPUTime :
% 146.64/146.88 % Version: 1.5
% 146.64/146.88 % SZS status Theorem
% 146.64/146.88 % SZS output start CNFRefutation
% 146.64/146.88 fof(exemplo6GDDFULLmoreE0061,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:((((((((para(B,C,A,D)¶(A,B,C,D))&midp(E,C,D))&midp(F,B,A))&coll(G,A,C))&coll(G,D,F))&coll(H,B,E))&coll(H,A,C))=>cong(A,G,G,H)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE0061)).
% 146.64/146.88 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:((((((((para(B,C,A,D)¶(A,B,C,D))&midp(E,C,D))&midp(F,B,A))&coll(G,A,C))&coll(G,D,F))&coll(H,B,E))&coll(H,A,C))=>cong(A,G,G,H))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE0061])).
% 146.64/146.88 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:((((((((para(B,C,A,D)¶(A,B,C,D))&midp(E,C,D))&midp(F,B,A))&coll(G,A,C))&coll(G,D,F))&coll(H,B,E))&coll(H,A,C))&~cong(A,G,G,H)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 146.64/146.88 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((para(X3,X4,X2,X5)¶(X2,X3,X4,X5))&midp(X6,X4,X5))&midp(X7,X3,X2))&coll(X8,X2,X4))&coll(X8,X5,X7))&coll(X9,X3,X6))&coll(X9,X2,X4))&~cong(X2,X8,X8,X9)))))))))),inference(variable_rename,[status(thm)],[c12])).
% 146.64/146.88 fof(c14,negated_conjecture,((((((((para(skolem0002,skolem0003,skolem0001,skolem0004)¶(skolem0001,skolem0002,skolem0003,skolem0004))&midp(skolem0005,skolem0003,skolem0004))&midp(skolem0006,skolem0002,skolem0001))&coll(skolem0007,skolem0001,skolem0003))&coll(skolem0007,skolem0004,skolem0006))&coll(skolem0008,skolem0002,skolem0005))&coll(skolem0008,skolem0001,skolem0003))&~cong(skolem0001,skolem0007,skolem0007,skolem0008)),inference(skolemize,[status(esa)],[c13])).
% 146.64/146.88 cnf(c23,negated_conjecture,~cong(skolem0001,skolem0007,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c14])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 146.64/146.88 fof(c339,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c338])).
% 146.64/146.88 cnf(c340,plain,~cong(X714,X713,X715,X716)|cong(X714,X713,X716,X715),inference(split_conjunct,[status(thm)],[c339])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c238,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])).
% 146.64/146.88 fof(c239,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c238])).
% 146.64/146.88 cnf(c240,plain,~perp(X997,X998,X998,X996)|~midp(X999,X997,X996)|cong(X997,X999,X998,X999),inference(split_conjunct,[status(thm)],[c239])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c159,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 146.64/146.88 fof(c160,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)],[c159])).
% 146.64/146.88 fof(c162,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(c161,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)],[c160])).])).
% 146.64/146.88 cnf(c163,plain,~eqangle(X906,X911,X909,X907,X905,X910,X908,X904)|~perp(X905,X910,X908,X904)|perp(X906,X911,X909,X907),inference(split_conjunct,[status(thm)],[c162])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c281,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])).
% 146.64/146.88 fof(c282,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)],[c281])).
% 146.64/146.88 fof(c284,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(c283,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)],[c282])).])).
% 146.64/146.88 cnf(c285,plain,~para(X1059,X1056,X1054,X1055)|eqangle(X1059,X1056,X1058,X1057,X1054,X1055,X1058,X1057),inference(split_conjunct,[status(thm)],[c284])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 146.64/146.88 fof(c398,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c397])).
% 146.64/146.88 cnf(c399,plain,~para(X783,X782,X784,X781)|para(X783,X782,X781,X784),inference(split_conjunct,[status(thm)],[c398])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c286,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])).
% 146.64/146.88 fof(c287,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)],[c286])).
% 146.64/146.88 fof(c289,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(c288,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)],[c287])).])).
% 146.64/146.88 cnf(c290,plain,~eqangle(X1061,X1062,X1063,X1065,X1064,X1060,X1063,X1065)|para(X1061,X1062,X1064,X1060),inference(split_conjunct,[status(thm)],[c289])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c350,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])).
% 146.64/146.88 fof(c351,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)],[c350])).
% 146.64/146.88 cnf(c352,plain,~eqangle(X1199,X1203,X1204,X1202,X1205,X1200,X1201,X1198)|eqangle(X1204,X1202,X1199,X1203,X1201,X1198,X1205,X1200),inference(split_conjunct,[status(thm)],[c351])).
% 146.64/146.88 cnf(c17,negated_conjecture,midp(skolem0005,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c14])).
% 146.64/146.88 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 146.64/146.88 fof(c376,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 146.64/146.88 fof(c377,plain,(![X484]:(![X485]:(![X486]:(~midp(X486,X485,X484)|midp(X486,X484,X485))))),inference(variable_rename,[status(thm)],[c376])).
% 146.64/146.88 cnf(c378,plain,~midp(X560,X558,X559)|midp(X560,X559,X558),inference(split_conjunct,[status(thm)],[c377])).
% 146.64/146.88 cnf(c422,plain,midp(skolem0005,skolem0004,skolem0003),inference(resolution,[status(thm)],[c378, c17])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c198,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])).
% 146.64/146.88 fof(c199,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c198])).
% 146.64/146.88 fof(c201,plain,(![X177]:(![X178]:(![X179]:(![X180]:(![X181]:((~midp(X181,X177,X178)|~midp(X181,X179,X180))|para(X177,X179,X178,X180))))))),inference(shift_quantors,[status(thm)],[fof(c200,plain,(![X177]:(![X178]:(![X179]:(![X180]:((![X181]:(~midp(X181,X177,X178)|~midp(X181,X179,X180)))|para(X177,X179,X178,X180)))))),inference(variable_rename,[status(thm)],[c199])).])).
% 146.64/146.88 cnf(c202,plain,~midp(X949,X948,X950)|~midp(X949,X947,X951)|para(X948,X947,X950,X951),inference(split_conjunct,[status(thm)],[c201])).
% 146.64/146.88 cnf(c1275,plain,~midp(skolem0005,X2445,X2446)|para(X2445,skolem0003,X2446,skolem0004),inference(resolution,[status(thm)],[c202, c17])).
% 146.64/146.88 cnf(c6814,plain,para(skolem0004,skolem0003,skolem0003,skolem0004),inference(resolution,[status(thm)],[c1275, c422])).
% 146.64/146.88 cnf(c6827,plain,para(skolem0004,skolem0003,skolem0004,skolem0003),inference(resolution,[status(thm)],[c6814, c399])).
% 146.64/146.88 cnf(c6872,plain,eqangle(skolem0004,skolem0003,X5288,X5287,skolem0004,skolem0003,X5288,X5287),inference(resolution,[status(thm)],[c6827, c285])).
% 146.64/146.88 cnf(c18204,plain,eqangle(X5967,X5968,skolem0004,skolem0003,X5967,X5968,skolem0004,skolem0003),inference(resolution,[status(thm)],[c6872, c352])).
% 146.64/146.88 cnf(c22580,plain,para(X5971,X5970,X5971,X5970),inference(resolution,[status(thm)],[c18204, c290])).
% 146.64/146.88 cnf(c22706,plain,para(X5997,X5996,X5996,X5997),inference(resolution,[status(thm)],[c22580, c399])).
% 146.64/146.88 cnf(c25067,plain,eqangle(X8685,X8683,X8686,X8684,X8683,X8685,X8686,X8684),inference(resolution,[status(thm)],[c22706, c285])).
% 146.64/146.88 cnf(c40156,plain,~perp(X10828,X10827,X10826,X10829)|perp(X10827,X10828,X10826,X10829),inference(resolution,[status(thm)],[c25067, c163])).
% 146.64/146.88 fof(ruleD12,axiom,(![A]:(![B]:(![C]:(![O]:((cong(O,A,O,B)&cong(O,A,O,C))=>circle(O,A,B,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD12)).
% 146.64/146.88 fof(c373,plain,(![A]:(![B]:(![C]:(![O]:((~cong(O,A,O,B)|~cong(O,A,O,C))|circle(O,A,B,C)))))),inference(fof_nnf,[status(thm)],[ruleD12])).
% 146.64/146.88 fof(c374,plain,(![X480]:(![X481]:(![X482]:(![X483]:((~cong(X483,X480,X483,X481)|~cong(X483,X480,X483,X482))|circle(X483,X480,X481,X482)))))),inference(variable_rename,[status(thm)],[c373])).
% 146.64/146.88 cnf(c375,plain,~cong(X1224,X1227,X1224,X1226)|~cong(X1224,X1227,X1224,X1225)|circle(X1224,X1227,X1226,X1225),inference(split_conjunct,[status(thm)],[c374])).
% 146.64/146.88 cnf(c1670,plain,~cong(X1299,X1301,X1299,X1300)|circle(X1299,X1301,X1300,X1300),inference(factor,[status(thm)],[c375])).
% 146.64/146.88 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 146.64/146.88 fof(c183,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 146.64/146.88 fof(c184,plain,(![X158]:(![X159]:(![X160]:(~midp(X158,X159,X160)|cong(X158,X159,X158,X160))))),inference(variable_rename,[status(thm)],[c183])).
% 146.64/146.88 cnf(c185,plain,~midp(X695,X694,X696)|cong(X695,X694,X695,X696),inference(split_conjunct,[status(thm)],[c184])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c195,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])).
% 146.64/146.88 fof(c196,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)],[c195])).
% 146.64/146.88 cnf(c197,plain,~midp(X944,X943,X942)|~para(X943,X945,X942,X946)|~para(X943,X946,X942,X945)|midp(X944,X945,X946),inference(split_conjunct,[status(thm)],[c196])).
% 146.64/146.88 cnf(c1245,plain,~midp(X2500,X2502,X2503)|~para(X2502,X2501,X2503,X2501)|midp(X2500,X2501,X2501),inference(factor,[status(thm)],[c197])).
% 146.64/146.88 cnf(c15,negated_conjecture,para(skolem0002,skolem0003,skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c14])).
% 146.64/146.88 cnf(c629,plain,para(skolem0002,skolem0003,skolem0004,skolem0001),inference(resolution,[status(thm)],[c399, c15])).
% 146.64/146.88 fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 146.64/146.88 fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 146.64/146.88 fof(c395,plain,(![X513]:(![X514]:(![X515]:(![X516]:(~para(X513,X514,X515,X516)|para(X515,X516,X513,X514)))))),inference(variable_rename,[status(thm)],[c394])).
% 146.64/146.88 cnf(c396,plain,~para(X776,X774,X773,X775)|para(X773,X775,X776,X774),inference(split_conjunct,[status(thm)],[c395])).
% 146.64/146.88 cnf(c642,plain,para(skolem0004,skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c629, c396])).
% 146.64/146.88 fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)¶(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 146.64/146.88 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~para(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD6])).
% 146.64/146.88 fof(c392,plain,(![X507]:(![X508]:(![X509]:(![X510]:(![X511]:(![X512]:((~para(X507,X508,X509,X510)|~para(X509,X510,X511,X512))|para(X507,X508,X511,X512)))))))),inference(variable_rename,[status(thm)],[c391])).
% 146.64/146.88 cnf(c393,plain,~para(X1244,X1240,X1243,X1242)|~para(X1243,X1242,X1245,X1241)|para(X1244,X1240,X1245,X1241),inference(split_conjunct,[status(thm)],[c392])).
% 146.64/146.88 cnf(c1679,plain,~para(X3127,X3126,skolem0004,skolem0001)|para(X3127,X3126,skolem0002,skolem0003),inference(resolution,[status(thm)],[c393, c642])).
% 146.64/146.88 cnf(c9329,plain,para(skolem0002,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1679, c629])).
% 146.64/146.88 cnf(c9389,plain,~midp(X5614,skolem0002,skolem0002)|midp(X5614,skolem0003,skolem0003),inference(resolution,[status(thm)],[c9329, c1245])).
% 146.64/146.88 cnf(c18,negated_conjecture,midp(skolem0006,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c224,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])).
% 146.64/146.88 fof(c225,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)],[c224])).
% 146.64/146.88 cnf(c226,plain,~cong(X982,X980,X981,X980)|~cong(X982,X983,X981,X983)|perp(X982,X981,X980,X983),inference(split_conjunct,[status(thm)],[c225])).
% 146.64/146.88 cnf(c1358,plain,~cong(X1278,X1280,X1279,X1280)|perp(X1278,X1279,X1280,X1280),inference(factor,[status(thm)],[c226])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 146.64/146.88 fof(c336,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c335])).
% 146.64/146.88 cnf(c337,plain,~cong(X707,X706,X704,X705)|cong(X704,X705,X707,X706),inference(split_conjunct,[status(thm)],[c336])).
% 146.64/146.88 cnf(c423,plain,midp(skolem0006,skolem0001,skolem0002),inference(resolution,[status(thm)],[c378, c18])).
% 146.64/146.88 cnf(c540,plain,cong(skolem0006,skolem0001,skolem0006,skolem0002),inference(resolution,[status(thm)],[c185, c423])).
% 146.64/146.88 cnf(c556,plain,cong(skolem0006,skolem0001,skolem0002,skolem0006),inference(resolution,[status(thm)],[c340, c540])).
% 146.64/146.88 cnf(c573,plain,cong(skolem0002,skolem0006,skolem0006,skolem0001),inference(resolution,[status(thm)],[c556, c337])).
% 146.64/146.88 fof(ruleD25,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((cong(A,B,C,D)&cong(C,D,E,F))=>cong(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 146.64/146.88 fof(c332,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~cong(A,B,C,D)|~cong(C,D,E,F))|cong(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD25])).
% 146.64/146.88 fof(c333,plain,(![X400]:(![X401]:(![X402]:(![X403]:(![X404]:(![X405]:((~cong(X400,X401,X402,X403)|~cong(X402,X403,X404,X405))|cong(X400,X401,X404,X405)))))))),inference(variable_rename,[status(thm)],[c332])).
% 146.64/146.88 cnf(c334,plain,~cong(X1169,X1168,X1164,X1165)|~cong(X1164,X1165,X1167,X1166)|cong(X1169,X1168,X1167,X1166),inference(split_conjunct,[status(thm)],[c333])).
% 146.64/146.88 cnf(c1649,plain,~cong(X3073,X3072,skolem0006,skolem0001)|cong(X3073,X3072,skolem0002,skolem0006),inference(resolution,[status(thm)],[c334, c556])).
% 146.64/146.88 cnf(c8948,plain,cong(skolem0002,skolem0006,skolem0002,skolem0006),inference(resolution,[status(thm)],[c1649, c573])).
% 146.64/146.88 cnf(c9056,plain,perp(skolem0002,skolem0002,skolem0006,skolem0006),inference(resolution,[status(thm)],[c8948, c1358])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c382,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])).
% 146.64/146.88 fof(c383,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)],[c382])).
% 146.64/146.88 cnf(c384,plain,~perp(X1236,X1237,X1234,X1239)|~perp(X1234,X1239,X1235,X1238)|para(X1236,X1237,X1235,X1238),inference(split_conjunct,[status(thm)],[c383])).
% 146.64/146.88 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)).
% 146.64/146.88 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 146.64/146.88 fof(c386,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c385])).
% 146.64/146.89 cnf(c387,plain,~perp(X765,X766,X767,X768)|perp(X767,X768,X765,X766),inference(split_conjunct,[status(thm)],[c386])).
% 146.64/146.89 cnf(c542,plain,cong(skolem0006,skolem0002,skolem0006,skolem0001),inference(resolution,[status(thm)],[c185, c18])).
% 146.64/146.89 cnf(c553,plain,cong(skolem0006,skolem0002,skolem0001,skolem0006),inference(resolution,[status(thm)],[c340, c542])).
% 146.64/146.89 cnf(c564,plain,cong(skolem0001,skolem0006,skolem0006,skolem0002),inference(resolution,[status(thm)],[c553, c337])).
% 146.64/146.89 cnf(c580,plain,cong(skolem0001,skolem0006,skolem0002,skolem0006),inference(resolution,[status(thm)],[c564, c340])).
% 146.64/146.89 cnf(c1878,plain,perp(skolem0001,skolem0002,skolem0006,skolem0006),inference(resolution,[status(thm)],[c1358, c580])).
% 146.64/146.89 cnf(c1894,plain,perp(skolem0006,skolem0006,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1878, c387])).
% 146.64/146.89 cnf(c1937,plain,~perp(X3509,X3508,skolem0006,skolem0006)|para(X3509,X3508,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1894, c384])).
% 146.64/146.89 cnf(c11762,plain,para(skolem0002,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1937, c9056])).
% 146.64/146.89 cnf(c12102,plain,~midp(X5837,skolem0002,skolem0001)|midp(X5837,skolem0002,skolem0002),inference(resolution,[status(thm)],[c11762, c1245])).
% 146.64/146.89 cnf(c21529,plain,midp(skolem0006,skolem0002,skolem0002),inference(resolution,[status(thm)],[c12102, c18])).
% 146.64/146.89 cnf(c21552,plain,midp(skolem0006,skolem0003,skolem0003),inference(resolution,[status(thm)],[c21529, c9389])).
% 146.64/146.89 cnf(c22619,plain,~midp(X7841,X7840,X7840)|midp(X7841,X7842,X7842),inference(resolution,[status(thm)],[c22580, c1245])).
% 146.64/146.89 cnf(c36518,plain,midp(skolem0006,X7847,X7847),inference(resolution,[status(thm)],[c22619, c21552])).
% 146.64/146.89 cnf(c37314,plain,cong(skolem0006,X7896,skolem0006,X7896),inference(resolution,[status(thm)],[c36518, c185])).
% 146.64/146.89 cnf(c37610,plain,circle(skolem0006,X7898,X7898,X7898),inference(resolution,[status(thm)],[c37314, c1670])).
% 146.64/146.89 fof(ruleD49,axiom,(![A]:(![B]:(![C]:(![O]:(![X]:((circle(O,A,B,C)&eqangle(A,X,A,B,C,A,C,B))=>perp(O,A,A,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD49)).
% 146.64/146.89 fof(c247,plain,(![A]:(![B]:(![C]:(![O]:(![X]:((~circle(O,A,B,C)|~eqangle(A,X,A,B,C,A,C,B))|perp(O,A,A,X))))))),inference(fof_nnf,[status(thm)],[ruleD49])).
% 146.64/146.89 fof(c248,plain,(![X246]:(![X247]:(![X248]:(![X249]:(![X250]:((~circle(X249,X246,X247,X248)|~eqangle(X246,X250,X246,X247,X248,X246,X248,X247))|perp(X249,X246,X246,X250))))))),inference(variable_rename,[status(thm)],[c247])).
% 146.64/146.89 cnf(c249,plain,~circle(X1013,X1011,X1012,X1010)|~eqangle(X1011,X1014,X1011,X1012,X1010,X1011,X1010,X1012)|perp(X1013,X1011,X1011,X1014),inference(split_conjunct,[status(thm)],[c248])).
% 146.64/146.89 cnf(c22686,plain,eqangle(X8184,X8186,X8187,X8185,X8184,X8186,X8187,X8185),inference(resolution,[status(thm)],[c22580, c285])).
% 146.64/146.89 cnf(c39219,plain,~circle(X10308,X10306,X10307,X10306)|perp(X10308,X10306,X10306,X10306),inference(resolution,[status(thm)],[c22686, c249])).
% 146.64/146.89 cnf(c41699,plain,perp(skolem0006,X10309,X10309,X10309),inference(resolution,[status(thm)],[c39219, c37610])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c344,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])).
% 146.64/146.89 fof(c345,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)],[c344])).
% 146.64/146.89 cnf(c346,plain,~eqangle(X1189,X1188,X1183,X1182,X1186,X1185,X1187,X1184)|eqangle(X1189,X1188,X1186,X1185,X1183,X1182,X1187,X1184),inference(split_conjunct,[status(thm)],[c345])).
% 146.64/146.89 cnf(c39214,plain,eqangle(X8896,X8897,X8896,X8897,X8895,X8894,X8895,X8894),inference(resolution,[status(thm)],[c22686, c346])).
% 146.64/146.89 cnf(c40198,plain,~perp(X10945,X10947,X10945,X10947)|perp(X10948,X10946,X10948,X10946),inference(resolution,[status(thm)],[c39214, c163])).
% 146.64/146.89 cnf(c42831,plain,perp(X10950,X10949,X10950,X10949),inference(resolution,[status(thm)],[c40198, c41699])).
% 146.64/146.89 cnf(c42867,plain,perp(X11017,X11016,X11016,X11017),inference(resolution,[status(thm)],[c42831, c40156])).
% 146.64/146.89 cnf(c42885,plain,~midp(X11176,X11177,X11177)|cong(X11177,X11176,X11178,X11176),inference(resolution,[status(thm)],[c42867, c240])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 146.64/146.89 fof(c401,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c400])).
% 146.64/146.89 cnf(c402,plain,~coll(X824,X823,X822)|~coll(X824,X823,X825)|coll(X822,X825,X824),inference(split_conjunct,[status(thm)],[c401])).
% 146.64/146.89 cnf(c739,plain,~coll(X827,X826,X828)|coll(X828,X828,X827),inference(factor,[status(thm)],[c402])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 146.64/146.89 fof(c190,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c189])).
% 146.64/146.89 cnf(c191,plain,~para(X703,X702,X703,X701)|coll(X703,X702,X701),inference(split_conjunct,[status(thm)],[c190])).
% 146.64/146.89 cnf(c22709,plain,coll(X5972,X5973,X5973),inference(resolution,[status(thm)],[c22580, c191])).
% 146.64/146.89 cnf(c22798,plain,coll(X5976,X5976,X5977),inference(resolution,[status(thm)],[c22709, c739])).
% 146.64/146.89 cnf(c24657,plain,~coll(X8477,X8477,X8478)|coll(X8478,X8479,X8477),inference(resolution,[status(thm)],[c22798, c402])).
% 146.64/146.89 cnf(c39680,plain,coll(X8488,X8489,X8487),inference(resolution,[status(thm)],[c24657, c22798])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c186,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 146.64/146.89 fof(c187,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c186])).
% 146.64/146.89 cnf(c188,plain,~cong(X935,X934,X935,X936)|~coll(X935,X934,X936)|midp(X935,X934,X936),inference(split_conjunct,[status(thm)],[c187])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c359,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 146.64/146.89 fof(c360,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X464,X463,X465,X466)))))),inference(variable_rename,[status(thm)],[c359])).
% 146.64/146.89 cnf(c361,plain,~cyclic(X751,X752,X750,X749)|cyclic(X752,X751,X750,X749),inference(split_conjunct,[status(thm)],[c360])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c365,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 146.64/146.89 fof(c366,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c365])).
% 146.64/146.89 cnf(c367,plain,~cyclic(X764,X763,X761,X762)|cyclic(X764,X763,X762,X761),inference(split_conjunct,[status(thm)],[c366])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 146.64/146.89 fof(c363,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c362])).
% 146.64/146.89 cnf(c364,plain,~cyclic(X753,X755,X756,X754)|cyclic(X753,X756,X755,X754),inference(split_conjunct,[status(thm)],[c363])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c271,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])).
% 146.64/146.89 fof(c272,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)],[c271])).
% 146.64/146.89 cnf(c273,plain,~eqangle(X1044,X1043,X1044,X1042,X1045,X1043,X1045,X1042)|~coll(X1044,X1045,X1042)|cyclic(X1043,X1042,X1044,X1045),inference(split_conjunct,[status(thm)],[c272])).
% 146.64/146.89 cnf(c39229,plain,~coll(X9061,X9061,X9059)|cyclic(X9060,X9059,X9061,X9061),inference(resolution,[status(thm)],[c22686, c273])).
% 146.64/146.89 cnf(c40271,plain,cyclic(X9064,X9062,X9063,X9063),inference(resolution,[status(thm)],[c39229, c39680])).
% 146.64/146.89 cnf(c40274,plain,cyclic(X9067,X9066,X9065,X9066),inference(resolution,[status(thm)],[c40271, c364])).
% 146.64/146.89 cnf(c40307,plain,cyclic(X9080,X9081,X9081,X9082),inference(resolution,[status(thm)],[c40274, c367])).
% 146.64/146.89 cnf(c40319,plain,cyclic(X9095,X9097,X9095,X9096),inference(resolution,[status(thm)],[c40307, c361])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c266,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q))|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD43])).
% 146.64/146.89 fof(c267,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)],[c266])).
% 146.64/146.89 fof(c269,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(c268,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)],[c267])).])).
% 146.64/146.89 cnf(c270,plain,~cyclic(X1041,X1039,X1040,X1036)|~cyclic(X1041,X1039,X1040,X1037)|~cyclic(X1041,X1039,X1040,X1038)|~eqangle(X1040,X1041,X1040,X1039,X1038,X1036,X1038,X1037)|cong(X1041,X1039,X1036,X1037),inference(split_conjunct,[status(thm)],[c269])).
% 146.64/146.89 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)).
% 146.64/146.89 fof(c347,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])).
% 146.64/146.89 fof(c348,plain,(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(~eqangle(X434,X435,X436,X437,X438,X439,X440,X441)|eqangle(X438,X439,X440,X441,X434,X435,X436,X437)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 146.64/146.89 cnf(c349,plain,~eqangle(X1190,X1196,X1197,X1191,X1192,X1193,X1195,X1194)|eqangle(X1192,X1193,X1195,X1194,X1190,X1196,X1197,X1191),inference(split_conjunct,[status(thm)],[c348])).
% 146.64/146.89 cnf(c40144,plain,eqangle(X8918,X8917,X8917,X8918,X8916,X8915,X8916,X8915),inference(resolution,[status(thm)],[c25067, c346])).
% 146.64/146.89 cnf(c40209,plain,eqangle(X8962,X8964,X8962,X8964,X8961,X8963,X8963,X8961),inference(resolution,[status(thm)],[c40144, c349])).
% 146.64/146.89 cnf(c40229,plain,~cyclic(X11545,X11545,X11544,X11543)|cong(X11545,X11545,X11543,X11543),inference(resolution,[status(thm)],[c40209, c270])).
% 146.64/146.89 cnf(c43699,plain,cong(X11546,X11546,X11547,X11547),inference(resolution,[status(thm)],[c40229, c40319])).
% 146.64/146.89 cnf(c43713,plain,~coll(X11570,X11570,X11570)|midp(X11570,X11570,X11570),inference(resolution,[status(thm)],[c43699, c188])).
% 146.64/146.89 cnf(c43726,plain,midp(X11571,X11571,X11571),inference(resolution,[status(thm)],[c43713, c39680])).
% 146.64/146.89 cnf(c44027,plain,midp(X11573,X11572,X11572),inference(resolution,[status(thm)],[c43726, c22619])).
% 146.64/146.89 cnf(c44269,plain,cong(X11591,X11589,X11590,X11589),inference(resolution,[status(thm)],[c44027, c42885])).
% 146.64/146.89 cnf(c44748,plain,cong(X11618,X11620,X11620,X11619),inference(resolution,[status(thm)],[c44269, c340])).
% 146.64/146.89 cnf(c44859,plain,$false,inference(resolution,[status(thm)],[c44748, c23])).
% 146.64/146.89 % SZS output end CNFRefutation
% 146.64/146.89
% 146.64/146.89 % Initial clauses : 136
% 146.64/146.89 % Processed clauses : 4527
% 146.64/146.89 % Factors computed : 201
% 146.64/146.89 % Resolvents computed: 44257
% 146.64/146.89 % Tautologies deleted: 30
% 146.64/146.89 % Forward subsumed : 11500
% 146.64/146.89 % Backward subsumed : 2740
% 146.64/146.89 % -------- CPU Time ---------
% 146.64/146.89 % User time : 146.446 s
% 146.64/146.89 % System time : 0.102 s
% 146.64/146.89 % Total time : 146.548 s
%------------------------------------------------------------------------------