%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO633+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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 155.67s 155.87s
% Output : Refutation 155.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO633+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n017.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:04:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 155.67/155.87 % Version: 1.5
% 155.67/155.87 % SZS status Theorem
% 155.67/155.87 % SZS output start CNFRefutation
% 155.67/155.87 fof(exemplo6GDDFULL8110996,conjecture,(![A]:(![B]:(![C]:(![A1]:(![S]:(![N]:(![G]:(![H]:((((((((midp(A1,C,B)&eqangle(S,A,A,B,C,A,A,A1))&coll(S,B,C))&coll(N,A,A1))&perp(G,N,A,B))&coll(G,A,B))&perp(H,N,A,C))&coll(H,A,C))=>perp(G,H,A,S)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL8110996)).
% 155.67/155.87 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![A1]:(![S]:(![N]:(![G]:(![H]:((((((((midp(A1,C,B)&eqangle(S,A,A,B,C,A,A,A1))&coll(S,B,C))&coll(N,A,A1))&perp(G,N,A,B))&coll(G,A,B))&perp(H,N,A,C))&coll(H,A,C))=>perp(G,H,A,S))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110996])).
% 155.67/155.87 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[A1]:(?[S]:(?[N]:(?[G]:(?[H]:((((((((midp(A1,C,B)&eqangle(S,A,A,B,C,A,A,A1))&coll(S,B,C))&coll(N,A,A1))&perp(G,N,A,B))&coll(G,A,B))&perp(H,N,A,C))&coll(H,A,C))&~perp(G,H,A,S)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 155.67/155.87 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((midp(X5,X4,X3)&eqangle(X6,X2,X2,X3,X4,X2,X2,X5))&coll(X6,X3,X4))&coll(X7,X2,X5))&perp(X8,X7,X2,X3))&coll(X8,X2,X3))&perp(X9,X7,X2,X4))&coll(X9,X2,X4))&~perp(X8,X9,X2,X6)))))))))),inference(variable_rename,[status(thm)],[c12])).
% 155.67/155.87 fof(c14,negated_conjecture,((((((((midp(skolem0004,skolem0003,skolem0002)&eqangle(skolem0005,skolem0001,skolem0001,skolem0002,skolem0003,skolem0001,skolem0001,skolem0004))&coll(skolem0005,skolem0002,skolem0003))&coll(skolem0006,skolem0001,skolem0004))&perp(skolem0007,skolem0006,skolem0001,skolem0002))&coll(skolem0007,skolem0001,skolem0002))&perp(skolem0008,skolem0006,skolem0001,skolem0003))&coll(skolem0008,skolem0001,skolem0003))&~perp(skolem0007,skolem0008,skolem0001,skolem0005)),inference(skolemize,[status(esa)],[c13])).
% 155.67/155.87 cnf(c23,negated_conjecture,~perp(skolem0007,skolem0008,skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c402,plain,~coll(X784,X785,X786)|~coll(X784,X785,X783)|coll(X786,X783,X784),inference(split_conjunct,[status(thm)],[c401])).
% 155.67/155.87 cnf(c613,plain,~coll(X788,X789,X787)|coll(X787,X787,X788),inference(factor,[status(thm)],[c402])).
% 155.67/155.87 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)).
% 155.67/155.87 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 155.67/155.87 fof(c190,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c189])).
% 155.67/155.87 cnf(c191,plain,~para(X679,X681,X679,X680)|coll(X679,X681,X680),inference(split_conjunct,[status(thm)],[c190])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 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])).])).
% 155.67/155.87 cnf(c290,plain,~eqangle(X1063,X1062,X1065,X1064,X1060,X1061,X1065,X1064)|para(X1063,X1062,X1060,X1061),inference(split_conjunct,[status(thm)],[c289])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c352,plain,~eqangle(X1215,X1218,X1213,X1219,X1216,X1220,X1214,X1217)|eqangle(X1213,X1219,X1215,X1218,X1214,X1217,X1216,X1220),inference(split_conjunct,[status(thm)],[c351])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 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])).])).
% 155.67/155.87 cnf(c285,plain,~para(X1058,X1056,X1059,X1055)|eqangle(X1058,X1056,X1054,X1057,X1059,X1055,X1054,X1057),inference(split_conjunct,[status(thm)],[c284])).
% 155.67/155.87 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)).
% 155.67/155.87 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 155.67/155.87 fof(c398,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c397])).
% 155.67/155.87 cnf(c399,plain,~para(X776,X774,X775,X773)|para(X776,X774,X773,X775),inference(split_conjunct,[status(thm)],[c398])).
% 155.67/155.87 cnf(c15,negated_conjecture,midp(skolem0004,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 155.67/155.87 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 155.67/155.87 fof(c376,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 155.67/155.87 fof(c377,plain,(![X484]:(![X485]:(![X486]:(~midp(X486,X485,X484)|midp(X486,X484,X485))))),inference(variable_rename,[status(thm)],[c376])).
% 155.67/155.87 cnf(c378,plain,~midp(X559,X560,X558)|midp(X559,X558,X560),inference(split_conjunct,[status(thm)],[c377])).
% 155.67/155.87 cnf(c418,plain,midp(skolem0004,skolem0002,skolem0003),inference(resolution,[status(thm)],[c378, c15])).
% 155.67/155.87 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 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])).])).
% 155.67/155.87 cnf(c202,plain,~midp(X951,X948,X949)|~midp(X951,X947,X950)|para(X948,X947,X949,X950),inference(split_conjunct,[status(thm)],[c201])).
% 155.67/155.87 cnf(c1242,plain,~midp(skolem0004,X2297,X2298)|para(X2297,skolem0003,X2298,skolem0002),inference(resolution,[status(thm)],[c202, c15])).
% 155.67/155.87 cnf(c5924,plain,para(skolem0002,skolem0003,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1242, c418])).
% 155.67/155.87 cnf(c5938,plain,para(skolem0002,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c5924, c399])).
% 155.67/155.87 cnf(c5947,plain,eqangle(skolem0002,skolem0003,X4957,X4958,skolem0002,skolem0003,X4957,X4958),inference(resolution,[status(thm)],[c5938, c285])).
% 155.67/155.87 cnf(c13316,plain,eqangle(X5740,X5741,skolem0002,skolem0003,X5740,X5741,skolem0002,skolem0003),inference(resolution,[status(thm)],[c5947, c352])).
% 155.67/155.87 cnf(c16009,plain,para(X5742,X5743,X5742,X5743),inference(resolution,[status(thm)],[c13316, c290])).
% 155.67/155.87 cnf(c16027,plain,coll(X5744,X5745,X5745),inference(resolution,[status(thm)],[c16009, c191])).
% 155.67/155.87 cnf(c16376,plain,coll(X5754,X5754,X5753),inference(resolution,[status(thm)],[c16027, c613])).
% 155.67/155.87 cnf(c17894,plain,~coll(X8355,X8355,X8354)|coll(X8354,X8353,X8355),inference(resolution,[status(thm)],[c16376, c402])).
% 155.67/155.87 cnf(c28516,plain,coll(X8365,X8363,X8364),inference(resolution,[status(thm)],[c17894, c16376])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c188,plain,~cong(X936,X934,X936,X935)|~coll(X936,X934,X935)|midp(X936,X934,X935),inference(split_conjunct,[status(thm)],[c187])).
% 155.67/155.87 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)).
% 155.67/155.87 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 155.67/155.87 fof(c339,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c338])).
% 155.67/155.87 cnf(c340,plain,~cong(X690,X692,X689,X691)|cong(X690,X692,X691,X689),inference(split_conjunct,[status(thm)],[c339])).
% 155.67/155.87 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)).
% 155.67/155.87 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 155.67/155.87 fof(c336,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c335])).
% 155.67/155.87 cnf(c337,plain,~cong(X686,X688,X687,X685)|cong(X687,X685,X686,X688),inference(split_conjunct,[status(thm)],[c336])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c240,plain,~perp(X998,X999,X999,X996)|~midp(X997,X998,X996)|cong(X998,X997,X999,X997),inference(split_conjunct,[status(thm)],[c239])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 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])).])).
% 155.67/155.87 cnf(c163,plain,~eqangle(X905,X904,X907,X908,X909,X910,X911,X906)|~perp(X909,X910,X911,X906)|perp(X905,X904,X907,X908),inference(split_conjunct,[status(thm)],[c162])).
% 155.67/155.87 cnf(c16063,plain,para(X5768,X5767,X5767,X5768),inference(resolution,[status(thm)],[c16009, c399])).
% 155.67/155.87 cnf(c17931,plain,eqangle(X8552,X8553,X8551,X8554,X8553,X8552,X8551,X8554),inference(resolution,[status(thm)],[c16063, c285])).
% 155.67/155.87 cnf(c28983,plain,~perp(X9967,X9965,X9964,X9966)|perp(X9965,X9967,X9964,X9966),inference(resolution,[status(thm)],[c17931, c163])).
% 155.67/155.87 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)).
% 155.67/155.87 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 155.67/155.87 fof(c386,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c385])).
% 155.67/155.87 cnf(c387,plain,~perp(X725,X727,X726,X724)|perp(X726,X724,X725,X727),inference(split_conjunct,[status(thm)],[c386])).
% 155.67/155.87 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 155.67/155.87 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 155.67/155.87 fof(c389,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c388])).
% 155.67/155.87 cnf(c390,plain,~perp(X736,X733,X734,X735)|perp(X736,X733,X735,X734),inference(split_conjunct,[status(thm)],[c389])).
% 155.67/155.87 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD12)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c375,plain,~cong(X1242,X1241,X1242,X1239)|~cong(X1242,X1241,X1242,X1240)|circle(X1242,X1241,X1239,X1240),inference(split_conjunct,[status(thm)],[c374])).
% 155.67/155.87 cnf(c1596,plain,~cong(X1269,X1268,X1269,X1270)|circle(X1269,X1268,X1270,X1270),inference(factor,[status(thm)],[c375])).
% 155.67/155.87 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 155.67/155.87 fof(c183,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 155.67/155.87 fof(c184,plain,(![X158]:(![X159]:(![X160]:(~midp(X158,X159,X160)|cong(X158,X159,X158,X160))))),inference(variable_rename,[status(thm)],[c183])).
% 155.67/155.87 cnf(c185,plain,~midp(X677,X678,X676)|cong(X677,X678,X677,X676),inference(split_conjunct,[status(thm)],[c184])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c197,plain,~midp(X942,X944,X943)|~para(X944,X945,X943,X946)|~para(X944,X946,X943,X945)|midp(X942,X945,X946),inference(split_conjunct,[status(thm)],[c196])).
% 155.67/155.87 cnf(c1228,plain,~midp(X2338,X2339,X2337)|~para(X2339,X2336,X2337,X2336)|midp(X2338,X2336,X2336),inference(factor,[status(thm)],[c197])).
% 155.67/155.87 cnf(c6070,plain,~midp(X4972,skolem0002,skolem0002)|midp(X4972,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1228, c5938])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c226,plain,~cong(X981,X982,X983,X982)|~cong(X981,X980,X983,X980)|perp(X981,X983,X982,X980),inference(split_conjunct,[status(thm)],[c225])).
% 155.67/155.87 cnf(c1311,plain,~cong(X1138,X1140,X1139,X1140)|perp(X1138,X1139,X1140,X1140),inference(factor,[status(thm)],[c226])).
% 155.67/155.87 cnf(c511,plain,cong(skolem0004,skolem0003,skolem0004,skolem0002),inference(resolution,[status(thm)],[c185, c15])).
% 155.67/155.87 cnf(c517,plain,cong(skolem0004,skolem0003,skolem0002,skolem0004),inference(resolution,[status(thm)],[c340, c511])).
% 155.67/155.87 cnf(c519,plain,cong(skolem0002,skolem0004,skolem0004,skolem0003),inference(resolution,[status(thm)],[c517, c337])).
% 155.67/155.87 cnf(c527,plain,cong(skolem0002,skolem0004,skolem0003,skolem0004),inference(resolution,[status(thm)],[c519, c340])).
% 155.67/155.87 cnf(c512,plain,cong(skolem0004,skolem0002,skolem0004,skolem0003),inference(resolution,[status(thm)],[c185, c418])).
% 155.67/155.87 cnf(c518,plain,cong(skolem0004,skolem0002,skolem0003,skolem0004),inference(resolution,[status(thm)],[c340, c512])).
% 155.67/155.87 cnf(c523,plain,cong(skolem0003,skolem0004,skolem0004,skolem0002),inference(resolution,[status(thm)],[c518, c337])).
% 155.67/155.87 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c334,plain,~cong(X1176,X1181,X1178,X1179)|~cong(X1178,X1179,X1177,X1180)|cong(X1176,X1181,X1177,X1180),inference(split_conjunct,[status(thm)],[c333])).
% 155.67/155.87 cnf(c1488,plain,~cong(X2672,X2671,skolem0003,skolem0004)|cong(X2672,X2671,skolem0004,skolem0002),inference(resolution,[status(thm)],[c334, c523])).
% 155.67/155.87 cnf(c7257,plain,cong(skolem0002,skolem0004,skolem0004,skolem0002),inference(resolution,[status(thm)],[c1488, c527])).
% 155.67/155.87 cnf(c7263,plain,cong(skolem0002,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c7257, c340])).
% 155.67/155.87 cnf(c7318,plain,perp(skolem0002,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c7263, c1311])).
% 155.67/155.87 cnf(c530,plain,cong(skolem0003,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c523, c340])).
% 155.67/155.87 cnf(c1445,plain,perp(skolem0003,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1311, c530])).
% 155.67/155.87 cnf(c1455,plain,perp(skolem0004,skolem0004,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1445, c387])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c384,plain,~perp(X1254,X1250,X1249,X1253)|~perp(X1249,X1253,X1251,X1252)|para(X1254,X1250,X1251,X1252),inference(split_conjunct,[status(thm)],[c383])).
% 155.67/155.87 cnf(c1660,plain,~perp(X2934,X2935,skolem0004,skolem0004)|para(X2934,X2935,skolem0003,skolem0002),inference(resolution,[status(thm)],[c384, c1455])).
% 155.67/155.87 cnf(c8512,plain,para(skolem0002,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1660, c7318])).
% 155.67/155.87 cnf(c8594,plain,~midp(X5419,skolem0002,skolem0003)|midp(X5419,skolem0002,skolem0002),inference(resolution,[status(thm)],[c8512, c1228])).
% 155.67/155.87 cnf(c14614,plain,midp(skolem0004,skolem0002,skolem0002),inference(resolution,[status(thm)],[c8594, c418])).
% 155.67/155.87 cnf(c14638,plain,midp(skolem0004,skolem0003,skolem0003),inference(resolution,[status(thm)],[c14614, c6070])).
% 155.67/155.87 cnf(c16041,plain,~midp(X7903,X7902,X7902)|midp(X7903,X7901,X7901),inference(resolution,[status(thm)],[c16009, c1228])).
% 155.67/155.87 cnf(c27021,plain,midp(skolem0004,X7904,X7904),inference(resolution,[status(thm)],[c16041, c14638])).
% 155.67/155.87 cnf(c27109,plain,cong(skolem0004,X7920,skolem0004,X7920),inference(resolution,[status(thm)],[c27021, c185])).
% 155.67/155.87 cnf(c27524,plain,cong(skolem0004,X7939,X7939,skolem0004),inference(resolution,[status(thm)],[c27109, c340])).
% 155.67/155.87 cnf(c27672,plain,cong(X7959,skolem0004,skolem0004,X7959),inference(resolution,[status(thm)],[c27524, c337])).
% 155.67/155.87 cnf(c27799,plain,cong(X7986,skolem0004,X7986,skolem0004),inference(resolution,[status(thm)],[c27672, c340])).
% 155.67/155.87 cnf(c28017,plain,circle(X8060,skolem0004,skolem0004,skolem0004),inference(resolution,[status(thm)],[c27799, c1596])).
% 155.67/155.87 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD49)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c249,plain,~circle(X1010,X1014,X1011,X1012)|~eqangle(X1014,X1013,X1014,X1011,X1012,X1014,X1012,X1011)|perp(X1010,X1014,X1014,X1013),inference(split_conjunct,[status(thm)],[c248])).
% 155.67/155.87 cnf(c16028,plain,eqangle(X7891,X7890,X7889,X7892,X7891,X7890,X7889,X7892),inference(resolution,[status(thm)],[c16009, c285])).
% 155.67/155.87 cnf(c27017,plain,~circle(X9690,X9689,X9688,X9689)|perp(X9690,X9689,X9689,X9689),inference(resolution,[status(thm)],[c16028, c249])).
% 155.67/155.87 cnf(c29621,plain,perp(X9706,skolem0004,skolem0004,skolem0004),inference(resolution,[status(thm)],[c27017, c28017])).
% 155.67/155.87 cnf(c29719,plain,perp(skolem0004,skolem0004,X9708,skolem0004),inference(resolution,[status(thm)],[c29621, c387])).
% 155.67/155.87 cnf(c29757,plain,perp(skolem0004,skolem0004,skolem0004,X9721),inference(resolution,[status(thm)],[c29719, c390])).
% 155.67/155.87 cnf(c29797,plain,perp(skolem0004,X9730,skolem0004,skolem0004),inference(resolution,[status(thm)],[c29757, c387])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c346,plain,~eqangle(X1198,X1204,X1199,X1202,X1197,X1200,X1203,X1201)|eqangle(X1198,X1204,X1197,X1200,X1199,X1202,X1203,X1201),inference(split_conjunct,[status(thm)],[c345])).
% 155.67/155.87 cnf(c26996,plain,eqangle(X8572,X8574,X8572,X8574,X8575,X8573,X8575,X8573),inference(resolution,[status(thm)],[c16028, c346])).
% 155.67/155.87 cnf(c29000,plain,~perp(X10087,X10089,X10087,X10089)|perp(X10090,X10088,X10090,X10088),inference(resolution,[status(thm)],[c26996, c163])).
% 155.67/155.87 cnf(c30376,plain,perp(X10095,X10094,X10095,X10094),inference(resolution,[status(thm)],[c29000, c29797])).
% 155.67/155.87 cnf(c30399,plain,perp(X10126,X10127,X10127,X10126),inference(resolution,[status(thm)],[c30376, c28983])).
% 155.67/155.87 cnf(c30461,plain,~midp(X10362,X10363,X10363)|cong(X10363,X10362,X10364,X10362),inference(resolution,[status(thm)],[c30399, c240])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c273,plain,~eqangle(X1045,X1042,X1045,X1044,X1043,X1042,X1043,X1044)|~coll(X1045,X1043,X1044)|cyclic(X1042,X1044,X1045,X1043),inference(split_conjunct,[status(thm)],[c272])).
% 155.67/155.87 cnf(c27020,plain,~coll(X8814,X8814,X8813)|cyclic(X8812,X8813,X8814,X8814),inference(resolution,[status(thm)],[c16028, c273])).
% 155.67/155.87 cnf(c29086,plain,cyclic(X8817,X8815,X8816,X8816),inference(resolution,[status(thm)],[c27020, c28516])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 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])).])).
% 155.67/155.87 cnf(c270,plain,~cyclic(X1038,X1040,X1036,X1041)|~cyclic(X1038,X1040,X1036,X1037)|~cyclic(X1038,X1040,X1036,X1039)|~eqangle(X1036,X1038,X1036,X1040,X1039,X1041,X1039,X1037)|cong(X1038,X1040,X1041,X1037),inference(split_conjunct,[status(thm)],[c269])).
% 155.67/155.87 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)).
% 155.67/155.87 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])).
% 155.67/155.87 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])).
% 155.67/155.87 cnf(c349,plain,~eqangle(X1212,X1210,X1207,X1208,X1211,X1206,X1209,X1205)|eqangle(X1211,X1206,X1209,X1205,X1212,X1210,X1207,X1208),inference(split_conjunct,[status(thm)],[c348])).
% 155.67/155.87 cnf(c28978,plain,eqangle(X8666,X8664,X8664,X8666,X8667,X8665,X8667,X8665),inference(resolution,[status(thm)],[c17931, c346])).
% 155.67/155.87 cnf(c29013,plain,eqangle(X8713,X8710,X8713,X8710,X8712,X8711,X8711,X8712),inference(resolution,[status(thm)],[c28978, c349])).
% 155.67/155.87 cnf(c29047,plain,~cyclic(X10908,X10908,X10906,X10907)|cong(X10908,X10908,X10907,X10907),inference(resolution,[status(thm)],[c29013, c270])).
% 155.67/155.87 cnf(c32707,plain,cong(X10910,X10910,X10909,X10909),inference(resolution,[status(thm)],[c29047, c29086])).
% 155.67/155.87 cnf(c32724,plain,~coll(X10935,X10935,X10935)|midp(X10935,X10935,X10935),inference(resolution,[status(thm)],[c32707, c188])).
% 155.67/155.87 cnf(c32733,plain,midp(X10938,X10938,X10938),inference(resolution,[status(thm)],[c32724, c28516])).
% 155.67/155.87 cnf(c32832,plain,midp(X10940,X10939,X10939),inference(resolution,[status(thm)],[c32733, c16041])).
% 155.67/155.87 cnf(c33568,plain,cong(X10962,X10961,X10960,X10961),inference(resolution,[status(thm)],[c32832, c30461])).
% 155.67/155.87 cnf(c33803,plain,cong(X11002,X11001,X11001,X11003),inference(resolution,[status(thm)],[c33568, c340])).
% 155.67/155.87 cnf(c33958,plain,cong(X11058,X11057,X11059,X11058),inference(resolution,[status(thm)],[c33803, c337])).
% 155.67/155.87 cnf(c34063,plain,cong(X11089,X11091,X11089,X11090),inference(resolution,[status(thm)],[c33958, c340])).
% 155.67/155.87 cnf(c34096,plain,~coll(X12043,X12041,X12042)|midp(X12043,X12041,X12042),inference(resolution,[status(thm)],[c34063, c188])).
% 155.67/155.87 cnf(c37721,plain,midp(X12046,X12047,X12048),inference(resolution,[status(thm)],[c34096, c28516])).
% 155.67/155.87 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)).
% 155.67/155.87 fof(c263,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])).
% 155.67/155.87 fof(c264,plain,(![X267]:(![X268]:(![X269]:(![X270]:(![X271]:((~midp(X270,X267,X268)|~midp(X271,X267,X269))|para(X270,X271,X268,X269))))))),inference(variable_rename,[status(thm)],[c263])).
% 155.67/155.87 cnf(c265,plain,~midp(X1034,X1035,X1031)|~midp(X1033,X1035,X1032)|para(X1034,X1033,X1031,X1032),inference(split_conjunct,[status(thm)],[c264])).
% 155.67/155.87 cnf(c33550,plain,~midp(X16655,X16654,X16656)|para(X16655,X16657,X16656,X16654),inference(resolution,[status(thm)],[c32832, c265])).
% 155.67/155.87 cnf(c41672,plain,para(X16663,X16662,X16661,X16660),inference(resolution,[status(thm)],[c33550, c37721])).
% 155.67/155.87 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)).
% 155.67/155.87 fof(c379,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])).
% 155.67/155.87 fof(c380,plain,(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:(![X492]:((~para(X487,X488,X489,X490)|~perp(X489,X490,X491,X492))|perp(X487,X488,X491,X492)))))))),inference(variable_rename,[status(thm)],[c379])).
% 155.67/155.87 cnf(c381,plain,~para(X1243,X1246,X1244,X1248)|~perp(X1244,X1248,X1247,X1245)|perp(X1243,X1246,X1247,X1245),inference(split_conjunct,[status(thm)],[c380])).
% 155.67/155.87 cnf(c30417,plain,~para(X19073,X19074,X19075,X19076)|perp(X19073,X19074,X19075,X19076),inference(resolution,[status(thm)],[c30376, c381])).
% 155.67/155.87 cnf(c42780,plain,perp(X19079,X19078,X19077,X19080),inference(resolution,[status(thm)],[c30417, c41672])).
% 155.67/155.87 cnf(c42782,plain,$false,inference(resolution,[status(thm)],[c42780, c23])).
% 155.67/155.87 % SZS output end CNFRefutation
% 155.67/155.87
% 155.67/155.87 % Initial clauses : 136
% 155.67/155.87 % Processed clauses : 4768
% 155.67/155.87 % Factors computed : 269
% 155.67/155.87 % Resolvents computed: 42105
% 155.67/155.87 % Tautologies deleted: 25
% 155.67/155.87 % Forward subsumed : 13987
% 155.67/155.87 % Backward subsumed : 4544
% 155.67/155.87 % -------- CPU Time ---------
% 155.67/155.87 % User time : 155.424 s
% 155.67/155.87 % System time : 0.082 s
% 155.67/155.87 % Total time : 155.506 s
%------------------------------------------------------------------------------