PyRes---1.5.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : GEO540+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n027.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:14 EDT 2024

% Result   : Satisfiable 0.72s 0.91s
% Output   : Saturation 0.77s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12  % Problem  : GEO540+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34  % Computer : n027.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Thu May  9 07:54:23 EDT 2024
% 0.12/0.34  % CPUTime  : 
% 0.72/0.91  % Version:  1.5
% 0.72/0.91  % SZS status Satisfiable
% 0.72/0.91  % SZS output start Saturation
% 0.72/0.91  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)).
% 0.72/0.91  fof(c253,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])).
% 0.72/0.91  fof(c254,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)],[c253])).
% 0.72/0.91  fof(c256,plain,(![X264]:(![X265]:(![X266]:(![X267]:(![X268]:(![X269]:((((~cyclic(X264,X265,X266,X267)|~cyclic(X264,X265,X266,X268))|~cyclic(X264,X265,X266,X269))|~eqangle(X266,X264,X266,X265,X269,X267,X269,X268))|cong(X264,X265,X267,X268)))))))),inference(shift_quantors,[status(thm)],[fof(c255,plain,(![X264]:(![X265]:(![X266]:(![X267]:(![X268]:((![X269]:(((~cyclic(X264,X265,X266,X267)|~cyclic(X264,X265,X266,X268))|~cyclic(X264,X265,X266,X269))|~eqangle(X266,X264,X266,X265,X269,X267,X269,X268)))|cong(X264,X265,X267,X268))))))),inference(variable_rename,[status(thm)],[c254])).])).
% 0.72/0.91  cnf(c257,plain,~cyclic(X1351,X1347,X1348,X1349)|~cyclic(X1351,X1347,X1348,X1350)|~cyclic(X1351,X1347,X1348,X1346)|~eqangle(X1348,X1351,X1348,X1347,X1346,X1349,X1346,X1350)|cong(X1351,X1347,X1349,X1350),inference(split_conjunct,[status(thm)],[c256])).
% 0.72/0.91  fof(ruleD58,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(((eqangle(A,B,B,C,P,Q,Q,R)&eqangle(A,C,B,C,P,R,Q,R))&(~coll(A,B,C)))=>simtri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD58)).
% 0.72/0.91  fof(c204,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(((eqangle(A,B,B,C,P,Q,Q,R)&eqangle(A,C,B,C,P,R,Q,R))&~coll(A,B,C))=>simtri(A,B,C,P,Q,R)))))))),inference(fof_simplification,[status(thm)],[ruleD58])).
% 0.72/0.91  fof(c205,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(((~eqangle(A,B,B,C,P,Q,Q,R)|~eqangle(A,C,B,C,P,R,Q,R))|coll(A,B,C))|simtri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[c204])).
% 0.72/0.91  fof(c206,plain,(![X198]:(![X199]:(![X200]:(![X201]:(![X202]:(![X203]:(((~eqangle(X198,X199,X199,X200,X201,X202,X202,X203)|~eqangle(X198,X200,X199,X200,X201,X203,X202,X203))|coll(X198,X199,X200))|simtri(X198,X199,X200,X201,X202,X203)))))))),inference(variable_rename,[status(thm)],[c205])).
% 0.72/0.91  cnf(c207,plain,~eqangle(X1332,X1336,X1336,X1337,X1333,X1334,X1334,X1335)|~eqangle(X1332,X1337,X1336,X1337,X1333,X1335,X1334,X1335)|coll(X1332,X1336,X1337)|simtri(X1332,X1336,X1337,X1333,X1334,X1335),inference(split_conjunct,[status(thm)],[c206])).
% 0.72/0.91  cnf(c433,plain,~eqangle(X1345,X1342,X1342,X1342,X1344,X1343,X1343,X1343)|coll(X1345,X1342,X1342)|simtri(X1345,X1342,X1342,X1344,X1343,X1343),inference(factor,[status(thm)],[c207])).
% 0.72/0.91  fof(ruleD22,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(![E]:(![F]:(![G]:(![H]:((eqangle(A,B,C,D,P,Q,U,V)&eqangle(P,Q,U,V,E,F,G,H))=>eqangle(A,B,C,D,E,F,G,H)))))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD22)).
% 0.72/0.91  fof(c328,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(![E]:(![F]:(![G]:(![H]:((~eqangle(A,B,C,D,P,Q,U,V)|~eqangle(P,Q,U,V,E,F,G,H))|eqangle(A,B,C,D,E,F,G,H)))))))))))))),inference(fof_nnf,[status(thm)],[ruleD22])).
% 0.72/0.91  fof(c329,plain,(![X406]:(![X407]:(![X408]:(![X409]:(![X410]:(![X411]:(![X412]:(![X413]:(![X414]:(![X415]:(![X416]:(![X417]:((~eqangle(X406,X407,X408,X409,X410,X411,X412,X413)|~eqangle(X410,X411,X412,X413,X414,X415,X416,X417))|eqangle(X406,X407,X408,X409,X414,X415,X416,X417)))))))))))))),inference(variable_rename,[status(thm)],[c328])).
% 0.72/0.91  cnf(c330,plain,~eqangle(X1323,X1331,X1322,X1325,X1321,X1320,X1330,X1324)|~eqangle(X1321,X1320,X1330,X1324,X1328,X1326,X1329,X1327)|eqangle(X1323,X1331,X1322,X1325,X1328,X1326,X1329,X1327),inference(split_conjunct,[status(thm)],[c329])).
% 0.72/0.91  fof(ruleD30,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![P]:(![Q]:(![U]:(![V]:((eqratio(A,B,C,D,P,Q,U,V)&eqratio(P,Q,U,V,E,F,G,H))=>eqratio(A,B,C,D,E,F,G,H)))))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD30)).
% 0.72/0.91  fof(c302,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![P]:(![Q]:(![U]:(![V]:((~eqratio(A,B,C,D,P,Q,U,V)|~eqratio(P,Q,U,V,E,F,G,H))|eqratio(A,B,C,D,E,F,G,H)))))))))))))),inference(fof_nnf,[status(thm)],[ruleD30])).
% 0.72/0.91  fof(c303,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:((![P]:(![Q]:(![U]:(![V]:(~eqratio(A,B,C,D,P,Q,U,V)|~eqratio(P,Q,U,V,E,F,G,H))))))|eqratio(A,B,C,D,E,F,G,H)))))))))),inference(shift_quantors,[status(thm)],[c302])).
% 0.72/0.91  fof(c305,plain,(![X348]:(![X349]:(![X350]:(![X351]:(![X352]:(![X353]:(![X354]:(![X355]:(![X356]:(![X357]:(![X358]:(![X359]:((~eqratio(X348,X349,X350,X351,X356,X357,X358,X359)|~eqratio(X356,X357,X358,X359,X352,X353,X354,X355))|eqratio(X348,X349,X350,X351,X352,X353,X354,X355)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c304,plain,(![X348]:(![X349]:(![X350]:(![X351]:(![X352]:(![X353]:(![X354]:(![X355]:((![X356]:(![X357]:(![X358]:(![X359]:(~eqratio(X348,X349,X350,X351,X356,X357,X358,X359)|~eqratio(X356,X357,X358,X359,X352,X353,X354,X355))))))|eqratio(X348,X349,X350,X351,X352,X353,X354,X355)))))))))),inference(variable_rename,[status(thm)],[c303])).])).
% 0.72/0.91  cnf(c306,plain,~eqratio(X1305,X1306,X1313,X1309,X1315,X1312,X1307,X1304)|~eqratio(X1315,X1312,X1307,X1304,X1308,X1310,X1314,X1311)|eqratio(X1305,X1306,X1313,X1309,X1308,X1310,X1314,X1311),inference(split_conjunct,[status(thm)],[c305])).
% 0.72/0.91  fof(ruleX5,axiom,(![A]:(![B]:(![P]:(![X]:(![Y]:(?[Q]:((eqangle(A,P,B,P,A,X,B,Y)&(~coll(A,B,P)))=>(eqangle(A,P,B,P,A,Q,B,Q)&cyclic(X,B,P,Q))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX5)).
% 0.72/0.91  fof(c104,plain,(![A]:(![B]:(![P]:(![X]:(![Y]:(?[Q]:((eqangle(A,P,B,P,A,X,B,Y)&~coll(A,B,P))=>(eqangle(A,P,B,P,A,Q,B,Q)&cyclic(X,B,P,Q))))))))),inference(fof_simplification,[status(thm)],[ruleX5])).
% 0.72/0.91  fof(c105,plain,(![A]:(![B]:(![P]:(![X]:(![Y]:(?[Q]:((~eqangle(A,P,B,P,A,X,B,Y)|coll(A,B,P))|(eqangle(A,P,B,P,A,Q,B,Q)&cyclic(X,B,P,Q))))))))),inference(fof_nnf,[status(thm)],[c104])).
% 0.72/0.91  fof(c106,plain,(![A]:(![B]:(![P]:(![X]:(((![Y]:~eqangle(A,P,B,P,A,X,B,Y))|coll(A,B,P))|(?[Q]:(eqangle(A,P,B,P,A,Q,B,Q)&cyclic(X,B,P,Q)))))))),inference(shift_quantors,[status(thm)],[c105])).
% 0.72/0.91  fof(c107,plain,(![X83]:(![X84]:(![X85]:(![X86]:(((![X87]:~eqangle(X83,X85,X84,X85,X83,X86,X84,X87))|coll(X83,X84,X85))|(?[X88]:(eqangle(X83,X85,X84,X85,X83,X88,X84,X88)&cyclic(X86,X84,X85,X88)))))))),inference(variable_rename,[status(thm)],[c106])).
% 0.72/0.91  fof(c109,plain,(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:((~eqangle(X83,X85,X84,X85,X83,X86,X84,X87)|coll(X83,X84,X85))|(eqangle(X83,X85,X84,X85,X83,skolem0016(X83,X84,X85,X86),X84,skolem0016(X83,X84,X85,X86))&cyclic(X86,X84,X85,skolem0016(X83,X84,X85,X86))))))))),inference(shift_quantors,[status(thm)],[fof(c108,plain,(![X83]:(![X84]:(![X85]:(![X86]:(((![X87]:~eqangle(X83,X85,X84,X85,X83,X86,X84,X87))|coll(X83,X84,X85))|(eqangle(X83,X85,X84,X85,X83,skolem0016(X83,X84,X85,X86),X84,skolem0016(X83,X84,X85,X86))&cyclic(X86,X84,X85,skolem0016(X83,X84,X85,X86)))))))),inference(skolemize,[status(esa)],[c107])).])).
% 0.72/0.91  fof(c110,plain,(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(((~eqangle(X83,X85,X84,X85,X83,X86,X84,X87)|coll(X83,X84,X85))|eqangle(X83,X85,X84,X85,X83,skolem0016(X83,X84,X85,X86),X84,skolem0016(X83,X84,X85,X86)))&((~eqangle(X83,X85,X84,X85,X83,X86,X84,X87)|coll(X83,X84,X85))|cyclic(X86,X84,X85,skolem0016(X83,X84,X85,X86))))))))),inference(distribute,[status(thm)],[c109])).
% 0.72/0.91  cnf(c111,plain,~eqangle(X1294,X1291,X1292,X1291,X1294,X1293,X1292,X1295)|coll(X1294,X1292,X1291)|eqangle(X1294,X1291,X1292,X1291,X1294,skolem0016(X1294,X1292,X1291,X1293),X1292,skolem0016(X1294,X1292,X1291,X1293)),inference(split_conjunct,[status(thm)],[c110])).
% 0.72/0.91  fof(ruleX8,axiom,(![A]:(![B]:(![M]:(![P]:(![Q]:(![R]:(![M]:(?[X]:((((midp(M,A,B)&para(A,P,R,M))&para(A,P,B,Q))&coll(P,Q,R))=>(coll(X,A,Q)&coll(X,M,R))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX8)).
% 0.72/0.91  fof(c82,plain,(![A]:(![B]:(![P]:(![Q]:(![R]:(![M]:(?[X]:((((midp(M,A,B)&para(A,P,R,M))&para(A,P,B,Q))&coll(P,Q,R))=>(coll(X,A,Q)&coll(X,M,R)))))))))),inference(fof_simplification,[status(thm)],[ruleX8])).
% 0.75/0.91  fof(c83,plain,(![A]:(![B]:(![P]:(![Q]:(![R]:(![M]:(?[X]:((((~midp(M,A,B)|~para(A,P,R,M))|~para(A,P,B,Q))|~coll(P,Q,R))|(coll(X,A,Q)&coll(X,M,R)))))))))),inference(fof_nnf,[status(thm)],[c82])).
% 0.75/0.91  fof(c84,plain,(![A]:(![B]:(![P]:(![Q]:(![R]:(![M]:((((~midp(M,A,B)|~para(A,P,R,M))|~para(A,P,B,Q))|~coll(P,Q,R))|(?[X]:(coll(X,A,Q)&coll(X,M,R)))))))))),inference(shift_quantors,[status(thm)],[c83])).
% 0.75/0.91  fof(c85,plain,(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:((((~midp(X66,X61,X62)|~para(X61,X63,X65,X66))|~para(X61,X63,X62,X64))|~coll(X63,X64,X65))|(?[X67]:(coll(X67,X61,X64)&coll(X67,X66,X65)))))))))),inference(variable_rename,[status(thm)],[c84])).
% 0.75/0.91  fof(c86,plain,(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:((((~midp(X66,X61,X62)|~para(X61,X63,X65,X66))|~para(X61,X63,X62,X64))|~coll(X63,X64,X65))|(coll(skolem0013(X61,X62,X63,X64,X65,X66),X61,X64)&coll(skolem0013(X61,X62,X63,X64,X65,X66),X66,X65))))))))),inference(skolemize,[status(esa)],[c85])).
% 0.75/0.91  fof(c87,plain,(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:(((((~midp(X66,X61,X62)|~para(X61,X63,X65,X66))|~para(X61,X63,X62,X64))|~coll(X63,X64,X65))|coll(skolem0013(X61,X62,X63,X64,X65,X66),X61,X64))&((((~midp(X66,X61,X62)|~para(X61,X63,X65,X66))|~para(X61,X63,X62,X64))|~coll(X63,X64,X65))|coll(skolem0013(X61,X62,X63,X64,X65,X66),X66,X65))))))))),inference(distribute,[status(thm)],[c86])).
% 0.75/0.91  cnf(c89,plain,~midp(X1234,X1236,X1238)|~para(X1236,X1239,X1235,X1234)|~para(X1236,X1239,X1238,X1237)|~coll(X1239,X1237,X1235)|coll(skolem0013(X1236,X1238,X1239,X1237,X1235,X1234),X1234,X1235),inference(split_conjunct,[status(thm)],[c87])).
% 0.75/0.91  cnf(c429,plain,~midp(X1290,X1288,X1289)|~para(X1288,X1287,X1289,X1290)|~coll(X1287,X1290,X1289)|coll(skolem0013(X1288,X1289,X1287,X1290,X1289,X1290),X1290,X1289),inference(factor,[status(thm)],[c89])).
% 0.75/0.91  cnf(c88,plain,~midp(X1208,X1210,X1212)|~para(X1210,X1213,X1209,X1208)|~para(X1210,X1213,X1212,X1211)|~coll(X1213,X1211,X1209)|coll(skolem0013(X1210,X1212,X1213,X1211,X1209,X1208),X1210,X1211),inference(split_conjunct,[status(thm)],[c87])).
% 0.75/0.91  cnf(c428,plain,~midp(X1285,X1286,X1284)|~para(X1286,X1283,X1284,X1285)|~coll(X1283,X1285,X1284)|coll(skolem0013(X1286,X1284,X1283,X1285,X1284,X1285),X1286,X1285),inference(factor,[status(thm)],[c88])).
% 0.75/0.91  fof(ruleX7,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:(![Q]:(?[P]:((((midp(M,A,B)&midp(N,C,D))&coll(C,A,B))&coll(D,A,B))=>midp(P,A,Q)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX7)).
% 0.75/0.91  fof(c90,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:(![Q]:(?[P]:((((~midp(M,A,B)|~midp(N,C,D))|~coll(C,A,B))|~coll(D,A,B))|midp(P,A,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleX7])).
% 0.75/0.91  fof(c91,plain,(![A]:((![B]:(![C]:(![D]:((((![M]:~midp(M,A,B))|(![N]:~midp(N,C,D)))|~coll(C,A,B))|~coll(D,A,B)))))|(![Q]:(?[P]:midp(P,A,Q))))),inference(shift_quantors,[status(thm)],[c90])).
% 0.75/0.91  fof(c92,plain,(![X68]:((![X69]:(![X70]:(![X71]:((((![X72]:~midp(X72,X68,X69))|(![X73]:~midp(X73,X70,X71)))|~coll(X70,X68,X69))|~coll(X71,X68,X69)))))|(![X74]:(?[X75]:midp(X75,X68,X74))))),inference(variable_rename,[status(thm)],[c91])).
% 0.75/0.91  fof(c94,plain,(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(![X73]:(![X74]:((((~midp(X72,X68,X69)|~midp(X73,X70,X71))|~coll(X70,X68,X69))|~coll(X71,X68,X69))|midp(skolem0014(X68,X74),X68,X74))))))))),inference(shift_quantors,[status(thm)],[fof(c93,plain,(![X68]:((![X69]:(![X70]:(![X71]:((((![X72]:~midp(X72,X68,X69))|(![X73]:~midp(X73,X70,X71)))|~coll(X70,X68,X69))|~coll(X71,X68,X69)))))|(![X74]:midp(skolem0014(X68,X74),X68,X74)))),inference(skolemize,[status(esa)],[c92])).])).
% 0.75/0.91  cnf(c95,plain,~midp(X1266,X1265,X1262)|~midp(X1268,X1267,X1264)|~coll(X1267,X1265,X1262)|~coll(X1264,X1265,X1262)|midp(skolem0014(X1265,X1263),X1265,X1263),inference(split_conjunct,[status(thm)],[c94])).
% 0.75/0.91  cnf(c430,plain,~midp(X1274,X1269,X1270)|~midp(X1272,X1271,X1271)|~coll(X1271,X1269,X1270)|midp(skolem0014(X1269,X1273),X1269,X1273),inference(factor,[status(thm)],[c95])).
% 0.75/0.91  fof(ruleD51,axiom,(![A]:(![B]:(![C]:(![O]:(![M]:(((circle(O,A,B,C)&coll(M,B,C))&eqangle(A,B,A,C,O,B,O,M))=>midp(M,B,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD51)).
% 0.75/0.91  fof(c228,plain,(![A]:(![B]:(![C]:(![O]:(![M]:(((~circle(O,A,B,C)|~coll(M,B,C))|~eqangle(A,B,A,C,O,B,O,M))|midp(M,B,C))))))),inference(fof_nnf,[status(thm)],[ruleD51])).
% 0.75/0.91  fof(c229,plain,(![X228]:(![X229]:(![X230]:(![X231]:(![X232]:(((~circle(X231,X228,X229,X230)|~coll(X232,X229,X230))|~eqangle(X228,X229,X228,X230,X231,X229,X231,X232))|midp(X232,X229,X230))))))),inference(variable_rename,[status(thm)],[c228])).
% 0.75/0.91  cnf(c230,plain,~circle(X1259,X1261,X1257,X1258)|~coll(X1260,X1257,X1258)|~eqangle(X1261,X1257,X1261,X1258,X1259,X1257,X1259,X1260)|midp(X1260,X1257,X1258),inference(split_conjunct,[status(thm)],[c229])).
% 0.75/0.91  fof(ruleD65,axiom,(![A]:(![B]:(![C]:(![D]:(![O]:(((para(A,B,C,D)&coll(O,A,C))&coll(O,B,D))=>eqratio(O,A,A,C,O,B,B,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD65)).
% 0.75/0.91  fof(c179,plain,(![A]:(![B]:(![C]:(![D]:(![O]:(((~para(A,B,C,D)|~coll(O,A,C))|~coll(O,B,D))|eqratio(O,A,A,C,O,B,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD65])).
% 0.75/0.91  fof(c180,plain,(![X159]:(![X160]:(![X161]:(![X162]:(![X163]:(((~para(X159,X160,X161,X162)|~coll(X163,X159,X161))|~coll(X163,X160,X162))|eqratio(X163,X159,X159,X161,X163,X160,X160,X162))))))),inference(variable_rename,[status(thm)],[c179])).
% 0.75/0.91  cnf(c181,plain,~para(X1252,X1256,X1255,X1253)|~coll(X1254,X1252,X1255)|~coll(X1254,X1256,X1253)|eqratio(X1254,X1252,X1252,X1255,X1254,X1256,X1256,X1253),inference(split_conjunct,[status(thm)],[c180])).
% 0.75/0.91  fof(ruleX1,axiom,(![A]:(![M]:(![O]:(![X]:(?[B]:((perp(O,M,M,A)&eqangle(X,O,M,O,M,O,A,O))=>(coll(B,A,M)&coll(B,O,X)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX1)).
% 0.75/0.91  fof(c134,plain,(![A]:(![M]:(![O]:(![X]:(?[B]:((~perp(O,M,M,A)|~eqangle(X,O,M,O,M,O,A,O))|(coll(B,A,M)&coll(B,O,X)))))))),inference(fof_nnf,[status(thm)],[ruleX1])).
% 0.75/0.91  fof(c135,plain,(![A]:(![M]:(![O]:(![X]:((~perp(O,M,M,A)|~eqangle(X,O,M,O,M,O,A,O))|(?[B]:(coll(B,A,M)&coll(B,O,X)))))))),inference(shift_quantors,[status(thm)],[c134])).
% 0.75/0.91  fof(c136,plain,(![X104]:(![X105]:(![X106]:(![X107]:((~perp(X106,X105,X105,X104)|~eqangle(X107,X106,X105,X106,X105,X106,X104,X106))|(?[X108]:(coll(X108,X104,X105)&coll(X108,X106,X107)))))))),inference(variable_rename,[status(thm)],[c135])).
% 0.75/0.91  fof(c137,plain,(![X104]:(![X105]:(![X106]:(![X107]:((~perp(X106,X105,X105,X104)|~eqangle(X107,X106,X105,X106,X105,X106,X104,X106))|(coll(skolem0020(X104,X105,X106,X107),X104,X105)&coll(skolem0020(X104,X105,X106,X107),X106,X107))))))),inference(skolemize,[status(esa)],[c136])).
% 0.75/0.91  fof(c138,plain,(![X104]:(![X105]:(![X106]:(![X107]:(((~perp(X106,X105,X105,X104)|~eqangle(X107,X106,X105,X106,X105,X106,X104,X106))|coll(skolem0020(X104,X105,X106,X107),X104,X105))&((~perp(X106,X105,X105,X104)|~eqangle(X107,X106,X105,X106,X105,X106,X104,X106))|coll(skolem0020(X104,X105,X106,X107),X106,X107))))))),inference(distribute,[status(thm)],[c137])).
% 0.75/0.91  cnf(c140,plain,~perp(X1248,X1250,X1250,X1251)|~eqangle(X1249,X1248,X1250,X1248,X1250,X1248,X1251,X1248)|coll(skolem0020(X1251,X1250,X1248,X1249),X1248,X1249),inference(split_conjunct,[status(thm)],[c138])).
% 0.75/0.91  cnf(c139,plain,~perp(X1244,X1246,X1246,X1247)|~eqangle(X1245,X1244,X1246,X1244,X1246,X1244,X1247,X1244)|coll(skolem0020(X1247,X1246,X1244,X1245),X1247,X1246),inference(split_conjunct,[status(thm)],[c138])).
% 0.75/0.91  fof(ruleX2,axiom,(![A]:(![B]:(![O]:(![X]:(?[M]:((cong(O,A,O,B)&eqangle(A,O,O,X,O,X,O,B))=>(coll(B,A,M)&coll(M,O,X)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX2)).
% 0.75/0.91  fof(c127,plain,(![A]:(![B]:(![O]:(![X]:(?[M]:((~cong(O,A,O,B)|~eqangle(A,O,O,X,O,X,O,B))|(coll(B,A,M)&coll(M,O,X)))))))),inference(fof_nnf,[status(thm)],[ruleX2])).
% 0.75/0.91  fof(c128,plain,(![A]:(![B]:(![O]:(![X]:((~cong(O,A,O,B)|~eqangle(A,O,O,X,O,X,O,B))|(?[M]:(coll(B,A,M)&coll(M,O,X)))))))),inference(shift_quantors,[status(thm)],[c127])).
% 0.75/0.91  fof(c129,plain,(![X99]:(![X100]:(![X101]:(![X102]:((~cong(X101,X99,X101,X100)|~eqangle(X99,X101,X101,X102,X101,X102,X101,X100))|(?[X103]:(coll(X100,X99,X103)&coll(X103,X101,X102)))))))),inference(variable_rename,[status(thm)],[c128])).
% 0.75/0.91  fof(c130,plain,(![X99]:(![X100]:(![X101]:(![X102]:((~cong(X101,X99,X101,X100)|~eqangle(X99,X101,X101,X102,X101,X102,X101,X100))|(coll(X100,X99,skolem0019(X99,X100,X101,X102))&coll(skolem0019(X99,X100,X101,X102),X101,X102))))))),inference(skolemize,[status(esa)],[c129])).
% 0.75/0.91  fof(c131,plain,(![X99]:(![X100]:(![X101]:(![X102]:(((~cong(X101,X99,X101,X100)|~eqangle(X99,X101,X101,X102,X101,X102,X101,X100))|coll(X100,X99,skolem0019(X99,X100,X101,X102)))&((~cong(X101,X99,X101,X100)|~eqangle(X99,X101,X101,X102,X101,X102,X101,X100))|coll(skolem0019(X99,X100,X101,X102),X101,X102))))))),inference(distribute,[status(thm)],[c130])).
% 0.75/0.91  cnf(c133,plain,~cong(X1243,X1240,X1243,X1242)|~eqangle(X1240,X1243,X1243,X1241,X1243,X1241,X1243,X1242)|coll(skolem0019(X1240,X1242,X1243,X1241),X1243,X1241),inference(split_conjunct,[status(thm)],[c131])).
% 0.75/0.91  cnf(c132,plain,~cong(X1233,X1230,X1233,X1232)|~eqangle(X1230,X1233,X1233,X1231,X1233,X1231,X1233,X1232)|coll(X1232,X1230,skolem0019(X1230,X1232,X1233,X1231)),inference(split_conjunct,[status(thm)],[c131])).
% 0.75/0.91  fof(ruleX3,axiom,(![A]:(![B]:(![O]:(![X]:(?[M]:((perp(O,X,A,B)&eqangle(A,O,O,X,O,X,O,B))=>(coll(B,A,M)&coll(M,O,X)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX3)).
% 0.75/0.91  fof(c120,plain,(![A]:(![B]:(![O]:(![X]:(?[M]:((~perp(O,X,A,B)|~eqangle(A,O,O,X,O,X,O,B))|(coll(B,A,M)&coll(M,O,X)))))))),inference(fof_nnf,[status(thm)],[ruleX3])).
% 0.75/0.91  fof(c121,plain,(![A]:(![B]:(![O]:(![X]:((~perp(O,X,A,B)|~eqangle(A,O,O,X,O,X,O,B))|(?[M]:(coll(B,A,M)&coll(M,O,X)))))))),inference(shift_quantors,[status(thm)],[c120])).
% 0.75/0.91  fof(c122,plain,(![X94]:(![X95]:(![X96]:(![X97]:((~perp(X96,X97,X94,X95)|~eqangle(X94,X96,X96,X97,X96,X97,X96,X95))|(?[X98]:(coll(X95,X94,X98)&coll(X98,X96,X97)))))))),inference(variable_rename,[status(thm)],[c121])).
% 0.75/0.91  fof(c123,plain,(![X94]:(![X95]:(![X96]:(![X97]:((~perp(X96,X97,X94,X95)|~eqangle(X94,X96,X96,X97,X96,X97,X96,X95))|(coll(X95,X94,skolem0018(X94,X95,X96,X97))&coll(skolem0018(X94,X95,X96,X97),X96,X97))))))),inference(skolemize,[status(esa)],[c122])).
% 0.75/0.91  fof(c124,plain,(![X94]:(![X95]:(![X96]:(![X97]:(((~perp(X96,X97,X94,X95)|~eqangle(X94,X96,X96,X97,X96,X97,X96,X95))|coll(X95,X94,skolem0018(X94,X95,X96,X97)))&((~perp(X96,X97,X94,X95)|~eqangle(X94,X96,X96,X97,X96,X97,X96,X95))|coll(skolem0018(X94,X95,X96,X97),X96,X97))))))),inference(distribute,[status(thm)],[c123])).
% 0.75/0.91  cnf(c126,plain,~perp(X1228,X1229,X1227,X1226)|~eqangle(X1227,X1228,X1228,X1229,X1228,X1229,X1228,X1226)|coll(skolem0018(X1227,X1226,X1228,X1229),X1228,X1229),inference(split_conjunct,[status(thm)],[c124])).
% 0.75/0.91  cnf(c125,plain,~perp(X1224,X1225,X1223,X1222)|~eqangle(X1223,X1224,X1224,X1225,X1224,X1225,X1224,X1222)|coll(X1222,X1223,skolem0018(X1223,X1222,X1224,X1225)),inference(split_conjunct,[status(thm)],[c124])).
% 0.75/0.91  cnf(c112,plain,~eqangle(X1220,X1217,X1218,X1217,X1220,X1219,X1218,X1221)|coll(X1220,X1218,X1217)|cyclic(X1219,X1218,X1217,skolem0016(X1220,X1218,X1217,X1219)),inference(split_conjunct,[status(thm)],[c110])).
% 0.75/0.91  fof(ruleD13,axiom,(![A]:(![B]:(![C]:(![D]:(![O]:(((cong(O,A,O,B)&cong(O,A,O,C))&cong(O,A,O,D))=>cyclic(A,B,C,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD13)).
% 0.75/0.91  fof(c355,plain,(![A]:(![B]:(![C]:(![D]:(![O]:(((~cong(O,A,O,B)|~cong(O,A,O,C))|~cong(O,A,O,D))|cyclic(A,B,C,D))))))),inference(fof_nnf,[status(thm)],[ruleD13])).
% 0.75/0.91  fof(c356,plain,(![A]:(![B]:(![C]:(![D]:((![O]:((~cong(O,A,O,B)|~cong(O,A,O,C))|~cong(O,A,O,D)))|cyclic(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c355])).
% 0.75/0.91  fof(c358,plain,(![X467]:(![X468]:(![X469]:(![X470]:(![X471]:(((~cong(X471,X467,X471,X468)|~cong(X471,X467,X471,X469))|~cong(X471,X467,X471,X470))|cyclic(X467,X468,X469,X470))))))),inference(shift_quantors,[status(thm)],[fof(c357,plain,(![X467]:(![X468]:(![X469]:(![X470]:((![X471]:((~cong(X471,X467,X471,X468)|~cong(X471,X467,X471,X469))|~cong(X471,X467,X471,X470)))|cyclic(X467,X468,X469,X470)))))),inference(variable_rename,[status(thm)],[c356])).])).
% 0.75/0.91  cnf(c359,plain,~cong(X1195,X1196,X1195,X1194)|~cong(X1195,X1196,X1195,X1193)|~cong(X1195,X1196,X1195,X1192)|cyclic(X1196,X1194,X1193,X1192),inference(split_conjunct,[status(thm)],[c358])).
% 0.75/0.91  cnf(c425,plain,~cong(X1207,X1206,X1207,X1205)|~cong(X1207,X1206,X1207,X1204)|cyclic(X1206,X1205,X1204,X1204),inference(factor,[status(thm)],[c359])).
% 0.75/0.91  cnf(c424,plain,~cong(X1200,X1199,X1200,X1198)|~cong(X1200,X1199,X1200,X1197)|cyclic(X1199,X1198,X1197,X1198),inference(factor,[status(thm)],[c359])).
% 0.75/0.91  cnf(c426,plain,~cong(X1201,X1202,X1201,X1203)|cyclic(X1202,X1203,X1203,X1203),inference(factor,[status(thm)],[c424])).
% 0.75/0.91  fof(ruleX12,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:(?[P]:(?[Q]:((((circle(M,A,B,C)&cong(M,A,M,D))&cong(N,A,N,B))&M!=N)=>(((coll(P,A,C)&cong(P,N,N,A))&coll(Q,B,D))&cong(Q,N,N,A))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX12)).
% 0.75/0.91  fof(c50,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:(?[P]:(?[Q]:((((~circle(M,A,B,C)|~cong(M,A,M,D))|~cong(N,A,N,B))|M=N)|(((coll(P,A,C)&cong(P,N,N,A))&coll(Q,B,D))&cong(Q,N,N,A))))))))))),inference(fof_nnf,[status(thm)],[ruleX12])).
% 0.75/0.91  fof(c51,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:((((~circle(M,A,B,C)|~cong(M,A,M,D))|~cong(N,A,N,B))|M=N)|(?[P]:(?[Q]:(((coll(P,A,C)&cong(P,N,N,A))&coll(Q,B,D))&cong(Q,N,N,A))))))))))),inference(shift_quantors,[status(thm)],[c50])).
% 0.75/0.91  fof(c52,plain,(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:((((~circle(X40,X36,X37,X38)|~cong(X40,X36,X40,X39))|~cong(X41,X36,X41,X37))|X40=X41)|(?[X42]:(?[X43]:(((coll(X42,X36,X38)&cong(X42,X41,X41,X36))&coll(X43,X37,X39))&cong(X43,X41,X41,X36))))))))))),inference(variable_rename,[status(thm)],[c51])).
% 0.75/0.91  fof(c53,plain,(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:((((~circle(X40,X36,X37,X38)|~cong(X40,X36,X40,X39))|~cong(X41,X36,X41,X37))|X40=X41)|(((coll(skolem0007(X36,X37,X38,X39,X40,X41),X36,X38)&cong(skolem0007(X36,X37,X38,X39,X40,X41),X41,X41,X36))&coll(skolem0008(X36,X37,X38,X39,X40,X41),X37,X39))&cong(skolem0008(X36,X37,X38,X39,X40,X41),X41,X41,X36))))))))),inference(skolemize,[status(esa)],[c52])).
% 0.75/0.91  fof(c54,plain,(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(((((((~circle(X40,X36,X37,X38)|~cong(X40,X36,X40,X39))|~cong(X41,X36,X41,X37))|X40=X41)|coll(skolem0007(X36,X37,X38,X39,X40,X41),X36,X38))&((((~circle(X40,X36,X37,X38)|~cong(X40,X36,X40,X39))|~cong(X41,X36,X41,X37))|X40=X41)|cong(skolem0007(X36,X37,X38,X39,X40,X41),X41,X41,X36)))&((((~circle(X40,X36,X37,X38)|~cong(X40,X36,X40,X39))|~cong(X41,X36,X41,X37))|X40=X41)|coll(skolem0008(X36,X37,X38,X39,X40,X41),X37,X39)))&((((~circle(X40,X36,X37,X38)|~cong(X40,X36,X40,X39))|~cong(X41,X36,X41,X37))|X40=X41)|cong(skolem0008(X36,X37,X38,X39,X40,X41),X41,X41,X36))))))))),inference(distribute,[status(thm)],[c53])).
% 0.75/0.91  cnf(c58,plain,~circle(X1184,X1187,X1186,X1188)|~cong(X1184,X1187,X1184,X1183)|~cong(X1185,X1187,X1185,X1186)|X1184=X1185|cong(skolem0008(X1187,X1186,X1188,X1183,X1184,X1185),X1185,X1185,X1187),inference(split_conjunct,[status(thm)],[c54])).
% 0.75/0.91  fof(ruleD34,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:(![G]:(![P]:(![Q]:(![R]:((simtri(A,B,C,E,F,G)&simtri(E,F,G,P,Q,R))=>simtri(A,B,C,P,Q,R))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD34)).
% 0.75/0.91  fof(c290,plain,(![A]:(![B]:(![C]:(![E]:(![F]:(![G]:(![P]:(![Q]:(![R]:((~simtri(A,B,C,E,F,G)|~simtri(E,F,G,P,Q,R))|simtri(A,B,C,P,Q,R))))))))))),inference(fof_nnf,[status(thm)],[ruleD34])).
% 0.75/0.91  fof(c291,plain,(![X321]:(![X322]:(![X323]:(![X324]:(![X325]:(![X326]:(![X327]:(![X328]:(![X329]:((~simtri(X321,X322,X323,X324,X325,X326)|~simtri(X324,X325,X326,X327,X328,X329))|simtri(X321,X322,X323,X327,X328,X329))))))))))),inference(variable_rename,[status(thm)],[c290])).
% 0.75/0.91  cnf(c292,plain,~simtri(X1177,X1174,X1178,X1175,X1180,X1182)|~simtri(X1175,X1180,X1182,X1176,X1179,X1181)|simtri(X1177,X1174,X1178,X1176,X1179,X1181),inference(split_conjunct,[status(thm)],[c291])).
% 0.75/0.91  fof(ruleD38,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:(![G]:(![P]:(![Q]:(![R]:((contri(A,B,C,E,F,G)&contri(E,F,G,P,Q,R))=>contri(A,B,C,P,Q,R))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD38)).
% 0.75/0.91  fof(c278,plain,(![A]:(![B]:(![C]:(![E]:(![F]:(![G]:(![P]:(![Q]:(![R]:((~contri(A,B,C,E,F,G)|~contri(E,F,G,P,Q,R))|contri(A,B,C,P,Q,R))))))))))),inference(fof_nnf,[status(thm)],[ruleD38])).
% 0.75/0.91  fof(c279,plain,(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(![X302]:((~contri(X294,X295,X296,X297,X298,X299)|~contri(X297,X298,X299,X300,X301,X302))|contri(X294,X295,X296,X300,X301,X302))))))))))),inference(variable_rename,[status(thm)],[c278])).
% 0.75/0.91  cnf(c280,plain,~contri(X1162,X1167,X1163,X1169,X1164,X1166)|~contri(X1169,X1164,X1166,X1165,X1168,X1170)|contri(X1162,X1167,X1163,X1165,X1168,X1170),inference(split_conjunct,[status(thm)],[c279])).
% 0.75/0.91  fof(ruleD57,axiom,(![A]:(![B]:(![P]:(![Q]:(((cong(A,P,B,P)&cong(A,Q,B,Q))&cyclic(A,B,P,Q))=>perp(P,A,A,Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD57)).
% 0.75/0.91  fof(c208,plain,(![A]:(![B]:(![P]:(![Q]:(((~cong(A,P,B,P)|~cong(A,Q,B,Q))|~cyclic(A,B,P,Q))|perp(P,A,A,Q)))))),inference(fof_nnf,[status(thm)],[ruleD57])).
% 0.75/0.91  fof(c209,plain,(![X204]:(![X205]:(![X206]:(![X207]:(((~cong(X204,X206,X205,X206)|~cong(X204,X207,X205,X207))|~cyclic(X204,X205,X206,X207))|perp(X206,X204,X204,X207)))))),inference(variable_rename,[status(thm)],[c208])).
% 0.75/0.91  cnf(c210,plain,~cong(X1161,X1159,X1158,X1159)|~cong(X1161,X1160,X1158,X1160)|~cyclic(X1161,X1158,X1159,X1160)|perp(X1159,X1161,X1161,X1160),inference(split_conjunct,[status(thm)],[c209])).
% 0.75/0.91  fof(ruleX9,axiom,(![A]:(![B]:(![C]:(![D]:(![O]:(?[P]:((cong(O,C,O,D)&perp(A,B,B,O))=>((cong(O,C,O,P)&para(P,C,A,B))&cong(B,C,B,P))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX9)).
% 0.75/0.91  fof(c74,plain,(![A]:(![B]:(![C]:(![D]:(![O]:(?[P]:((~cong(O,C,O,D)|~perp(A,B,B,O))|((cong(O,C,O,P)&para(P,C,A,B))&cong(B,C,B,P))))))))),inference(fof_nnf,[status(thm)],[ruleX9])).
% 0.75/0.91  fof(c75,plain,(![A]:(![B]:(![C]:(![D]:(![O]:((~cong(O,C,O,D)|~perp(A,B,B,O))|(?[P]:((cong(O,C,O,P)&para(P,C,A,B))&cong(B,C,B,P))))))))),inference(shift_quantors,[status(thm)],[c74])).
% 0.75/0.91  fof(c76,plain,(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:((~cong(X59,X57,X59,X58)|~perp(X55,X56,X56,X59))|(?[X60]:((cong(X59,X57,X59,X60)&para(X60,X57,X55,X56))&cong(X56,X57,X56,X60))))))))),inference(variable_rename,[status(thm)],[c75])).
% 0.75/0.91  fof(c77,plain,(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:((~cong(X59,X57,X59,X58)|~perp(X55,X56,X56,X59))|((cong(X59,X57,X59,skolem0012(X55,X56,X57,X58,X59))&para(skolem0012(X55,X56,X57,X58,X59),X57,X55,X56))&cong(X56,X57,X56,skolem0012(X55,X56,X57,X58,X59))))))))),inference(skolemize,[status(esa)],[c76])).
% 0.75/0.91  fof(c78,plain,(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:((((~cong(X59,X57,X59,X58)|~perp(X55,X56,X56,X59))|cong(X59,X57,X59,skolem0012(X55,X56,X57,X58,X59)))&((~cong(X59,X57,X59,X58)|~perp(X55,X56,X56,X59))|para(skolem0012(X55,X56,X57,X58,X59),X57,X55,X56)))&((~cong(X59,X57,X59,X58)|~perp(X55,X56,X56,X59))|cong(X56,X57,X56,skolem0012(X55,X56,X57,X58,X59))))))))),inference(distribute,[status(thm)],[c77])).
% 0.75/0.91  cnf(c81,plain,~cong(X1153,X1157,X1153,X1156)|~perp(X1154,X1155,X1155,X1153)|cong(X1155,X1157,X1155,skolem0012(X1154,X1155,X1157,X1156,X1153)),inference(split_conjunct,[status(thm)],[c78])).
% 0.75/0.91  cnf(c57,plain,~circle(X1148,X1151,X1150,X1152)|~cong(X1148,X1151,X1148,X1147)|~cong(X1149,X1151,X1149,X1150)|X1148=X1149|coll(skolem0008(X1151,X1150,X1152,X1147,X1148,X1149),X1150,X1147),inference(split_conjunct,[status(thm)],[c54])).
% 0.75/0.91  cnf(c80,plain,~cong(X1142,X1146,X1142,X1145)|~perp(X1143,X1144,X1144,X1142)|para(skolem0012(X1143,X1144,X1146,X1145,X1142),X1146,X1143,X1144),inference(split_conjunct,[status(thm)],[c78])).
% 0.75/0.91  cnf(c79,plain,~cong(X1137,X1141,X1137,X1140)|~perp(X1138,X1139,X1139,X1137)|cong(X1137,X1141,X1137,skolem0012(X1138,X1139,X1141,X1140,X1137)),inference(split_conjunct,[status(thm)],[c78])).
% 0.75/0.91  fof(ruleX6,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:(?[P]:((midp(M,A,B)&midp(N,C,D))=>((midp(P,A,D)&para(P,M,B,D))&para(P,N,A,C)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX6)).
% 0.75/0.91  fof(c96,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:(?[P]:((~midp(M,A,B)|~midp(N,C,D))|((midp(P,A,D)&para(P,M,B,D))&para(P,N,A,C)))))))))),inference(fof_nnf,[status(thm)],[ruleX6])).
% 0.75/0.91  fof(c97,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:((~midp(M,A,B)|~midp(N,C,D))|(?[P]:((midp(P,A,D)&para(P,M,B,D))&para(P,N,A,C)))))))))),inference(shift_quantors,[status(thm)],[c96])).
% 0.75/0.91  fof(c98,plain,(![X76]:(![X77]:(![X78]:(![X79]:(![X80]:(![X81]:((~midp(X80,X76,X77)|~midp(X81,X78,X79))|(?[X82]:((midp(X82,X76,X79)&para(X82,X80,X77,X79))&para(X82,X81,X76,X78)))))))))),inference(variable_rename,[status(thm)],[c97])).
% 0.75/0.91  fof(c99,plain,(![X76]:(![X77]:(![X78]:(![X79]:(![X80]:(![X81]:((~midp(X80,X76,X77)|~midp(X81,X78,X79))|((midp(skolem0015(X76,X77,X78,X79,X80,X81),X76,X79)&para(skolem0015(X76,X77,X78,X79,X80,X81),X80,X77,X79))&para(skolem0015(X76,X77,X78,X79,X80,X81),X81,X76,X78))))))))),inference(skolemize,[status(esa)],[c98])).
% 0.75/0.91  fof(c100,plain,(![X76]:(![X77]:(![X78]:(![X79]:(![X80]:(![X81]:((((~midp(X80,X76,X77)|~midp(X81,X78,X79))|midp(skolem0015(X76,X77,X78,X79,X80,X81),X76,X79))&((~midp(X80,X76,X77)|~midp(X81,X78,X79))|para(skolem0015(X76,X77,X78,X79,X80,X81),X80,X77,X79)))&((~midp(X80,X76,X77)|~midp(X81,X78,X79))|para(skolem0015(X76,X77,X78,X79,X80,X81),X81,X76,X78))))))))),inference(distribute,[status(thm)],[c99])).
% 0.75/0.91  cnf(c103,plain,~midp(X1131,X1128,X1130)|~midp(X1132,X1129,X1133)|para(skolem0015(X1128,X1130,X1129,X1133,X1131,X1132),X1132,X1128,X1129),inference(split_conjunct,[status(thm)],[c100])).
% 0.75/0.91  cnf(c419,plain,~midp(X1134,X1136,X1135)|para(skolem0015(X1136,X1135,X1136,X1135,X1134,X1134),X1134,X1136,X1136),inference(factor,[status(thm)],[c103])).
% 0.75/0.91  cnf(c102,plain,~midp(X1116,X1113,X1115)|~midp(X1117,X1114,X1118)|para(skolem0015(X1113,X1115,X1114,X1118,X1116,X1117),X1116,X1115,X1118),inference(split_conjunct,[status(thm)],[c100])).
% 0.75/0.91  cnf(c417,plain,~midp(X1127,X1125,X1126)|para(skolem0015(X1125,X1126,X1125,X1126,X1127,X1127),X1127,X1126,X1126),inference(factor,[status(thm)],[c102])).
% 0.75/0.91  cnf(c56,plain,~circle(X1120,X1123,X1122,X1124)|~cong(X1120,X1123,X1120,X1119)|~cong(X1121,X1123,X1121,X1122)|X1120=X1121|cong(skolem0007(X1123,X1122,X1124,X1119,X1120,X1121),X1121,X1121,X1123),inference(split_conjunct,[status(thm)],[c54])).
% 0.75/0.91  fof(ruleD48,axiom,(![A]:(![B]:(![C]:(![O]:(![X]:((circle(O,A,B,C)&perp(O,A,A,X))=>eqangle(A,X,A,B,C,A,C,B))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD48)).
% 0.75/0.91  fof(c237,plain,(![A]:(![B]:(![C]:(![O]:(![X]:((~circle(O,A,B,C)|~perp(O,A,A,X))|eqangle(A,X,A,B,C,A,C,B))))))),inference(fof_nnf,[status(thm)],[ruleD48])).
% 0.75/0.91  fof(c238,plain,(![X243]:(![X244]:(![X245]:(![X246]:(![X247]:((~circle(X246,X243,X244,X245)|~perp(X246,X243,X243,X247))|eqangle(X243,X247,X243,X244,X245,X243,X245,X244))))))),inference(variable_rename,[status(thm)],[c237])).
% 0.75/0.91  cnf(c239,plain,~circle(X1112,X1108,X1109,X1111)|~perp(X1112,X1108,X1108,X1110)|eqangle(X1108,X1110,X1108,X1109,X1111,X1108,X1111,X1109),inference(split_conjunct,[status(thm)],[c238])).
% 0.75/0.91  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)).
% 0.75/0.91  fof(c234,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])).
% 0.75/0.91  fof(c235,plain,(![X238]:(![X239]:(![X240]:(![X241]:(![X242]:((~circle(X241,X238,X239,X240)|~eqangle(X238,X242,X238,X239,X240,X238,X240,X239))|perp(X241,X238,X238,X242))))))),inference(variable_rename,[status(thm)],[c234])).
% 0.75/0.91  cnf(c236,plain,~circle(X1106,X1107,X1103,X1104)|~eqangle(X1107,X1105,X1107,X1103,X1104,X1107,X1104,X1103)|perp(X1106,X1107,X1107,X1105),inference(split_conjunct,[status(thm)],[c235])).
% 0.75/0.91  fof(ruleD54,axiom,(![A]:(![B]:(![C]:(![D]:((cyclic(A,B,C,D)&para(A,B,C,D))=>eqangle(A,D,C,D,C,D,C,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD54)).
% 0.75/0.91  fof(c217,plain,(![A]:(![B]:(![C]:(![D]:((~cyclic(A,B,C,D)|~para(A,B,C,D))|eqangle(A,D,C,D,C,D,C,B)))))),inference(fof_nnf,[status(thm)],[ruleD54])).
% 0.75/0.91  fof(c218,plain,(![X216]:(![X217]:(![X218]:(![X219]:((~cyclic(X216,X217,X218,X219)|~para(X216,X217,X218,X219))|eqangle(X216,X219,X218,X219,X218,X219,X218,X217)))))),inference(variable_rename,[status(thm)],[c217])).
% 0.75/0.91  cnf(c219,plain,~cyclic(X1102,X1099,X1100,X1101)|~para(X1102,X1099,X1100,X1101)|eqangle(X1102,X1101,X1100,X1101,X1100,X1101,X1100,X1099),inference(split_conjunct,[status(thm)],[c218])).
% 0.75/0.91  fof(ruleD61,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((simtri(A,B,C,P,Q,R)&cong(A,B,P,Q))=>contri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD61)).
% 0.75/0.91  fof(c195,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((~simtri(A,B,C,P,Q,R)|~cong(A,B,P,Q))|contri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD61])).
% 0.75/0.92  fof(c196,plain,(![X180]:(![X181]:(![X182]:(![X183]:(![X184]:(![X185]:((~simtri(X180,X181,X182,X183,X184,X185)|~cong(X180,X181,X183,X184))|contri(X180,X181,X182,X183,X184,X185)))))))),inference(variable_rename,[status(thm)],[c195])).
% 0.75/0.92  cnf(c197,plain,~simtri(X1097,X1098,X1096,X1094,X1093,X1095)|~cong(X1097,X1098,X1094,X1093)|contri(X1097,X1098,X1096,X1094,X1093,X1095),inference(split_conjunct,[status(thm)],[c196])).
% 0.75/0.92  cnf(c55,plain,~circle(X1088,X1091,X1090,X1092)|~cong(X1088,X1091,X1088,X1087)|~cong(X1089,X1091,X1089,X1090)|X1088=X1089|coll(skolem0007(X1091,X1090,X1092,X1087,X1088,X1089),X1091,X1092),inference(split_conjunct,[status(thm)],[c54])).
% 0.75/0.92  fof(ruleD64,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(((midp(M,A,B)&para(A,C,B,D))&para(A,D,B,C))=>midp(M,C,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 0.75/0.92  fof(c182,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])).
% 0.75/0.92  fof(c183,plain,(![X164]:(![X165]:(![X166]:(![X167]:(![X168]:(((~midp(X168,X164,X165)|~para(X164,X166,X165,X167))|~para(X164,X167,X165,X166))|midp(X168,X166,X167))))))),inference(variable_rename,[status(thm)],[c182])).
% 0.75/0.92  cnf(c184,plain,~midp(X1080,X1079,X1078)|~para(X1079,X1081,X1078,X1082)|~para(X1079,X1082,X1078,X1081)|midp(X1080,X1081,X1082),inference(split_conjunct,[status(thm)],[c183])).
% 0.75/0.92  cnf(c415,plain,~midp(X1084,X1083,X1086)|~para(X1083,X1085,X1086,X1085)|midp(X1084,X1085,X1085),inference(factor,[status(thm)],[c184])).
% 0.75/0.92  fof(ruleD72,axiom,(![A]:(![B]:(![C]:(![D]:((eqangle(A,B,C,D,C,D,A,B)&(~perp(A,B,C,D)))=>para(A,B,C,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD72)).
% 0.75/0.92  fof(c156,plain,(![A]:(![B]:(![C]:(![D]:((eqangle(A,B,C,D,C,D,A,B)&~perp(A,B,C,D))=>para(A,B,C,D)))))),inference(fof_simplification,[status(thm)],[ruleD72])).
% 0.75/0.92  fof(c157,plain,(![A]:(![B]:(![C]:(![D]:((~eqangle(A,B,C,D,C,D,A,B)|perp(A,B,C,D))|para(A,B,C,D)))))),inference(fof_nnf,[status(thm)],[c156])).
% 0.75/0.92  fof(c158,plain,(![X133]:(![X134]:(![X135]:(![X136]:((~eqangle(X133,X134,X135,X136,X135,X136,X133,X134)|perp(X133,X134,X135,X136))|para(X133,X134,X135,X136)))))),inference(variable_rename,[status(thm)],[c157])).
% 0.75/0.92  cnf(c159,plain,~eqangle(X1073,X1072,X1070,X1071,X1070,X1071,X1073,X1072)|perp(X1073,X1072,X1070,X1071)|para(X1073,X1072,X1070,X1071),inference(split_conjunct,[status(thm)],[c158])).
% 0.75/0.92  fof(ruleD73,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((eqangle(A,B,C,D,P,Q,U,V)&para(P,Q,U,V))=>para(A,B,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD73)).
% 0.75/0.92  fof(c151,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~para(P,Q,U,V))|para(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD73])).
% 0.75/0.92  fof(c152,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~para(P,Q,U,V))))))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c151])).
% 0.75/0.92  fof(c154,plain,(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:((~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~para(X129,X130,X131,X132))|para(X125,X126,X127,X128)))))))))),inference(shift_quantors,[status(thm)],[fof(c153,plain,(![X125]:(![X126]:(![X127]:(![X128]:((![X129]:(![X130]:(![X131]:(![X132]:(~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~para(X129,X130,X131,X132))))))|para(X125,X126,X127,X128)))))),inference(variable_rename,[status(thm)],[c152])).])).
% 0.75/0.92  cnf(c155,plain,~eqangle(X1067,X1064,X1062,X1066,X1063,X1065,X1068,X1069)|~para(X1063,X1065,X1068,X1069)|para(X1067,X1064,X1062,X1066),inference(split_conjunct,[status(thm)],[c154])).
% 0.75/0.92  fof(ruleX13,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(?[O]:(((cyclic(A,B,C,D)&para(A,B,C,D))&midp(M,A,B))=>circle(O,A,B,C)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX13)).
% 0.75/0.92  fof(c44,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(?[O]:(((~cyclic(A,B,C,D)|~para(A,B,C,D))|~midp(M,A,B))|circle(O,A,B,C)))))))),inference(fof_nnf,[status(thm)],[ruleX13])).
% 0.75/0.92  fof(c45,plain,(![A]:(![B]:(![C]:(((![D]:(~cyclic(A,B,C,D)|~para(A,B,C,D)))|(![M]:~midp(M,A,B)))|(?[O]:circle(O,A,B,C)))))),inference(shift_quantors,[status(thm)],[c44])).
% 0.75/0.92  fof(c46,plain,(![X30]:(![X31]:(![X32]:(((![X33]:(~cyclic(X30,X31,X32,X33)|~para(X30,X31,X32,X33)))|(![X34]:~midp(X34,X30,X31)))|(?[X35]:circle(X35,X30,X31,X32)))))),inference(variable_rename,[status(thm)],[c45])).
% 0.75/0.92  fof(c48,plain,(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(((~cyclic(X30,X31,X32,X33)|~para(X30,X31,X32,X33))|~midp(X34,X30,X31))|circle(skolem0006(X30,X31,X32),X30,X31,X32))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,(![X30]:(![X31]:(![X32]:(((![X33]:(~cyclic(X30,X31,X32,X33)|~para(X30,X31,X32,X33)))|(![X34]:~midp(X34,X30,X31)))|circle(skolem0006(X30,X31,X32),X30,X31,X32))))),inference(skolemize,[status(esa)],[c46])).])).
% 0.75/0.92  cnf(c49,plain,~cyclic(X1058,X1061,X1059,X1057)|~para(X1058,X1061,X1059,X1057)|~midp(X1060,X1058,X1061)|circle(skolem0006(X1058,X1061,X1059),X1058,X1061,X1059),inference(split_conjunct,[status(thm)],[c48])).
% 0.75/0.92  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)).
% 0.75/0.92  fof(c146,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])).
% 0.75/0.92  fof(c147,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)],[c146])).
% 0.75/0.92  fof(c149,plain,(![X117]:(![X118]:(![X119]:(![X120]:(![X121]:(![X122]:(![X123]:(![X124]:((~eqangle(X117,X118,X119,X120,X121,X122,X123,X124)|~perp(X121,X122,X123,X124))|perp(X117,X118,X119,X120)))))))))),inference(shift_quantors,[status(thm)],[fof(c148,plain,(![X117]:(![X118]:(![X119]:(![X120]:((![X121]:(![X122]:(![X123]:(![X124]:(~eqangle(X117,X118,X119,X120,X121,X122,X123,X124)|~perp(X121,X122,X123,X124))))))|perp(X117,X118,X119,X120)))))),inference(variable_rename,[status(thm)],[c147])).])).
% 0.75/0.92  cnf(c150,plain,~eqangle(X1055,X1052,X1050,X1049,X1053,X1056,X1054,X1051)|~perp(X1053,X1056,X1054,X1051)|perp(X1055,X1052,X1050,X1049),inference(split_conjunct,[status(thm)],[c149])).
% 0.75/0.92  fof(ruleD75,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((eqratio(A,B,C,D,P,Q,U,V)&cong(P,Q,U,V))=>cong(A,B,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD75)).
% 0.75/0.92  fof(c141,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqratio(A,B,C,D,P,Q,U,V)|~cong(P,Q,U,V))|cong(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD75])).
% 0.75/0.92  fof(c142,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqratio(A,B,C,D,P,Q,U,V)|~cong(P,Q,U,V))))))|cong(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c141])).
% 0.75/0.92  fof(c144,plain,(![X109]:(![X110]:(![X111]:(![X112]:(![X113]:(![X114]:(![X115]:(![X116]:((~eqratio(X109,X110,X111,X112,X113,X114,X115,X116)|~cong(X113,X114,X115,X116))|cong(X109,X110,X111,X112)))))))))),inference(shift_quantors,[status(thm)],[fof(c143,plain,(![X109]:(![X110]:(![X111]:(![X112]:((![X113]:(![X114]:(![X115]:(![X116]:(~eqratio(X109,X110,X111,X112,X113,X114,X115,X116)|~cong(X113,X114,X115,X116))))))|cong(X109,X110,X111,X112)))))),inference(variable_rename,[status(thm)],[c142])).])).
% 0.75/0.92  cnf(c145,plain,~eqratio(X1047,X1045,X1042,X1048,X1046,X1041,X1044,X1043)|~cong(X1046,X1041,X1044,X1043)|cong(X1047,X1045,X1042,X1048),inference(split_conjunct,[status(thm)],[c144])).
% 0.75/0.92  fof(ruleX4,axiom,(![A]:(![B]:(![O]:(![X]:(?[M]:((perp(O,X,A,B)&cong(O,A,O,B))=>(coll(B,A,M)&coll(M,O,X)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX4)).
% 0.75/0.92  fof(c113,plain,(![A]:(![B]:(![O]:(![X]:(?[M]:((~perp(O,X,A,B)|~cong(O,A,O,B))|(coll(B,A,M)&coll(M,O,X)))))))),inference(fof_nnf,[status(thm)],[ruleX4])).
% 0.75/0.92  fof(c114,plain,(![A]:(![B]:(![O]:(![X]:((~perp(O,X,A,B)|~cong(O,A,O,B))|(?[M]:(coll(B,A,M)&coll(M,O,X)))))))),inference(shift_quantors,[status(thm)],[c113])).
% 0.75/0.92  fof(c115,plain,(![X89]:(![X90]:(![X91]:(![X92]:((~perp(X91,X92,X89,X90)|~cong(X91,X89,X91,X90))|(?[X93]:(coll(X90,X89,X93)&coll(X93,X91,X92)))))))),inference(variable_rename,[status(thm)],[c114])).
% 0.75/0.92  fof(c116,plain,(![X89]:(![X90]:(![X91]:(![X92]:((~perp(X91,X92,X89,X90)|~cong(X91,X89,X91,X90))|(coll(X90,X89,skolem0017(X89,X90,X91,X92))&coll(skolem0017(X89,X90,X91,X92),X91,X92))))))),inference(skolemize,[status(esa)],[c115])).
% 0.75/0.92  fof(c117,plain,(![X89]:(![X90]:(![X91]:(![X92]:(((~perp(X91,X92,X89,X90)|~cong(X91,X89,X91,X90))|coll(X90,X89,skolem0017(X89,X90,X91,X92)))&((~perp(X91,X92,X89,X90)|~cong(X91,X89,X91,X90))|coll(skolem0017(X89,X90,X91,X92),X91,X92))))))),inference(distribute,[status(thm)],[c116])).
% 0.75/0.92  cnf(c119,plain,~perp(X1038,X1040,X1039,X1037)|~cong(X1038,X1039,X1038,X1037)|coll(skolem0017(X1039,X1037,X1038,X1040),X1038,X1040),inference(split_conjunct,[status(thm)],[c117])).
% 0.75/0.92  cnf(c118,plain,~perp(X1034,X1036,X1035,X1033)|~cong(X1034,X1035,X1034,X1033)|coll(X1033,X1035,skolem0017(X1035,X1033,X1034,X1036)),inference(split_conjunct,[status(thm)],[c117])).
% 0.75/0.92  cnf(c101,plain,~midp(X1022,X1019,X1021)|~midp(X1023,X1020,X1024)|midp(skolem0015(X1019,X1021,X1020,X1024,X1022,X1023),X1019,X1024),inference(split_conjunct,[status(thm)],[c100])).
% 0.75/0.92  cnf(c414,plain,~midp(X1031,X1030,X1032)|midp(skolem0015(X1030,X1032,X1030,X1032,X1031,X1031),X1030,X1032),inference(factor,[status(thm)],[c101])).
% 0.75/0.92  fof(ruleX15,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:(?[P]:((perp(A,C,C,B)&coll(B,E,F))=>(coll(P,E,F)&perp(P,A,E,F))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX15)).
% 0.75/0.92  fof(c31,plain,(![A]:(![B]:(![C]:(![E]:(![F]:(?[P]:((~perp(A,C,C,B)|~coll(B,E,F))|(coll(P,E,F)&perp(P,A,E,F))))))))),inference(fof_nnf,[status(thm)],[ruleX15])).
% 0.75/0.92  fof(c32,plain,(![A]:(![B]:(![C]:(![E]:(![F]:((~perp(A,C,C,B)|~coll(B,E,F))|(?[P]:(coll(P,E,F)&perp(P,A,E,F))))))))),inference(shift_quantors,[status(thm)],[c31])).
% 0.75/0.92  fof(c33,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~perp(X19,X21,X21,X20)|~coll(X20,X22,X23))|(?[X24]:(coll(X24,X22,X23)&perp(X24,X19,X22,X23))))))))),inference(variable_rename,[status(thm)],[c32])).
% 0.75/0.92  fof(c34,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~perp(X19,X21,X21,X20)|~coll(X20,X22,X23))|(coll(skolem0004(X19,X20,X21,X22,X23),X22,X23)&perp(skolem0004(X19,X20,X21,X22,X23),X19,X22,X23)))))))),inference(skolemize,[status(esa)],[c33])).
% 0.75/0.92  fof(c35,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((~perp(X19,X21,X21,X20)|~coll(X20,X22,X23))|coll(skolem0004(X19,X20,X21,X22,X23),X22,X23))&((~perp(X19,X21,X21,X20)|~coll(X20,X22,X23))|perp(skolem0004(X19,X20,X21,X22,X23),X19,X22,X23)))))))),inference(distribute,[status(thm)],[c34])).
% 0.75/0.92  cnf(c37,plain,~perp(X1025,X1027,X1027,X1026)|~coll(X1026,X1029,X1028)|perp(skolem0004(X1025,X1026,X1027,X1029,X1028),X1025,X1029,X1028),inference(split_conjunct,[status(thm)],[c35])).
% 0.75/0.92  fof(ruleX10,axiom,(![A]:(![B]:(![C]:(![H]:(?[P]:(?[Q]:((perp(A,H,B,C)&perp(B,H,A,C))=>(((coll(P,C,B)&perp(A,P,C,B))&coll(Q,C,A))&perp(B,Q,C,A))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX10)).
% 0.75/0.92  fof(c64,plain,(![A]:(![B]:(![C]:(![H]:(?[P]:(?[Q]:((~perp(A,H,B,C)|~perp(B,H,A,C))|(((coll(P,C,B)&perp(A,P,C,B))&coll(Q,C,A))&perp(B,Q,C,A))))))))),inference(fof_nnf,[status(thm)],[ruleX10])).
% 0.75/0.92  fof(c65,plain,(![A]:(![B]:(![C]:((![H]:(~perp(A,H,B,C)|~perp(B,H,A,C)))|(?[P]:(?[Q]:(((coll(P,C,B)&perp(A,P,C,B))&coll(Q,C,A))&perp(B,Q,C,A)))))))),inference(shift_quantors,[status(thm)],[c64])).
% 0.75/0.92  fof(c66,plain,(![X49]:(![X50]:(![X51]:((![X52]:(~perp(X49,X52,X50,X51)|~perp(X50,X52,X49,X51)))|(?[X53]:(?[X54]:(((coll(X53,X51,X50)&perp(X49,X53,X51,X50))&coll(X54,X51,X49))&perp(X50,X54,X51,X49)))))))),inference(variable_rename,[status(thm)],[c65])).
% 0.75/0.92  fof(c68,plain,(![X49]:(![X50]:(![X51]:(![X52]:((~perp(X49,X52,X50,X51)|~perp(X50,X52,X49,X51))|(((coll(skolem0010(X49,X50,X51),X51,X50)&perp(X49,skolem0010(X49,X50,X51),X51,X50))&coll(skolem0011(X49,X50,X51),X51,X49))&perp(X50,skolem0011(X49,X50,X51),X51,X49))))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,(![X49]:(![X50]:(![X51]:((![X52]:(~perp(X49,X52,X50,X51)|~perp(X50,X52,X49,X51)))|(((coll(skolem0010(X49,X50,X51),X51,X50)&perp(X49,skolem0010(X49,X50,X51),X51,X50))&coll(skolem0011(X49,X50,X51),X51,X49))&perp(X50,skolem0011(X49,X50,X51),X51,X49)))))),inference(skolemize,[status(esa)],[c66])).])).
% 0.75/0.92  fof(c69,plain,(![X49]:(![X50]:(![X51]:(![X52]:(((((~perp(X49,X52,X50,X51)|~perp(X50,X52,X49,X51))|coll(skolem0010(X49,X50,X51),X51,X50))&((~perp(X49,X52,X50,X51)|~perp(X50,X52,X49,X51))|perp(X49,skolem0010(X49,X50,X51),X51,X50)))&((~perp(X49,X52,X50,X51)|~perp(X50,X52,X49,X51))|coll(skolem0011(X49,X50,X51),X51,X49)))&((~perp(X49,X52,X50,X51)|~perp(X50,X52,X49,X51))|perp(X50,skolem0011(X49,X50,X51),X51,X49))))))),inference(distribute,[status(thm)],[c68])).
% 0.75/0.92  cnf(c73,plain,~perp(X1012,X1013,X1015,X1014)|~perp(X1015,X1013,X1012,X1014)|perp(X1015,skolem0011(X1012,X1015,X1014),X1014,X1012),inference(split_conjunct,[status(thm)],[c69])).
% 0.75/0.92  cnf(c413,plain,~perp(X1016,X1018,X1016,X1017)|perp(X1016,skolem0011(X1016,X1016,X1017),X1017,X1016),inference(factor,[status(thm)],[c73])).
% 0.75/0.92  fof(ruleX16,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(?[P]:(((perp(A,B,A,C)&perp(C,A,C,D))&midp(M,B,D))=>midp(P,A,C)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX16)).
% 0.75/0.92  fof(c25,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(?[P]:(((~perp(A,B,A,C)|~perp(C,A,C,D))|~midp(M,B,D))|midp(P,A,C)))))))),inference(fof_nnf,[status(thm)],[ruleX16])).
% 0.75/0.92  fof(c26,plain,(![A]:(![B]:(![C]:((![D]:((~perp(A,B,A,C)|~perp(C,A,C,D))|(![M]:~midp(M,B,D))))|(?[P]:midp(P,A,C)))))),inference(shift_quantors,[status(thm)],[c25])).
% 0.75/0.92  fof(c27,plain,(![X13]:(![X14]:(![X15]:((![X16]:((~perp(X13,X14,X13,X15)|~perp(X15,X13,X15,X16))|(![X17]:~midp(X17,X14,X16))))|(?[X18]:midp(X18,X13,X15)))))),inference(variable_rename,[status(thm)],[c26])).
% 0.75/0.92  fof(c29,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(((~perp(X13,X14,X13,X15)|~perp(X15,X13,X15,X16))|~midp(X17,X14,X16))|midp(skolem0003(X13,X14,X15),X13,X15))))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,(![X13]:(![X14]:(![X15]:((![X16]:((~perp(X13,X14,X13,X15)|~perp(X15,X13,X15,X16))|(![X17]:~midp(X17,X14,X16))))|midp(skolem0003(X13,X14,X15),X13,X15))))),inference(skolemize,[status(esa)],[c27])).])).
% 0.75/0.92  cnf(c30,plain,~perp(X1006,X1005,X1006,X1002)|~perp(X1002,X1006,X1002,X1003)|~midp(X1004,X1005,X1003)|midp(skolem0003(X1006,X1005,X1002),X1006,X1002),inference(split_conjunct,[status(thm)],[c29])).
% 0.75/0.92  cnf(c412,plain,~perp(X1010,X1010,X1010,X1010)|~midp(X1011,X1010,X1010)|midp(skolem0003(X1010,X1010,X1010),X1010,X1010),inference(factor,[status(thm)],[c30])).
% 0.75/0.92  cnf(c71,plain,~perp(X998,X999,X1001,X1000)|~perp(X1001,X999,X998,X1000)|perp(X998,skolem0010(X998,X1001,X1000),X1000,X1001),inference(split_conjunct,[status(thm)],[c69])).
% 0.75/0.92  cnf(c411,plain,~perp(X1008,X1009,X1008,X1007)|perp(X1008,skolem0010(X1008,X1008,X1007),X1007,X1008),inference(factor,[status(thm)],[c71])).
% 0.75/0.92  fof(ruleX14,axiom,(![A]:(![B]:(![C]:(![D]:(?[O]:((perp(A,C,C,B)&cyclic(A,B,C,D))=>circle(O,A,B,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX14)).
% 0.75/0.92  fof(c38,plain,(![A]:(![B]:(![C]:(![D]:(?[O]:((~perp(A,C,C,B)|~cyclic(A,B,C,D))|circle(O,A,B,C))))))),inference(fof_nnf,[status(thm)],[ruleX14])).
% 0.75/0.92  fof(c39,plain,(![A]:(![B]:(![C]:((~perp(A,C,C,B)|(![D]:~cyclic(A,B,C,D)))|(?[O]:circle(O,A,B,C)))))),inference(shift_quantors,[status(thm)],[c38])).
% 0.75/0.92  fof(c40,plain,(![X25]:(![X26]:(![X27]:((~perp(X25,X27,X27,X26)|(![X28]:~cyclic(X25,X26,X27,X28)))|(?[X29]:circle(X29,X25,X26,X27)))))),inference(variable_rename,[status(thm)],[c39])).
% 0.75/0.92  fof(c42,plain,(![X25]:(![X26]:(![X27]:(![X28]:((~perp(X25,X27,X27,X26)|~cyclic(X25,X26,X27,X28))|circle(skolem0005(X25,X26,X27),X25,X26,X27)))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,(![X25]:(![X26]:(![X27]:((~perp(X25,X27,X27,X26)|(![X28]:~cyclic(X25,X26,X27,X28)))|circle(skolem0005(X25,X26,X27),X25,X26,X27))))),inference(skolemize,[status(esa)],[c40])).])).
% 0.75/0.92  cnf(c43,plain,~perp(X995,X994,X994,X996)|~cyclic(X995,X996,X994,X997)|circle(skolem0005(X995,X996,X994),X995,X996,X994),inference(split_conjunct,[status(thm)],[c42])).
% 0.75/0.92  cnf(c36,plain,~perp(X989,X991,X991,X990)|~coll(X990,X993,X992)|coll(skolem0004(X989,X990,X991,X993,X992),X993,X992),inference(split_conjunct,[status(thm)],[c35])).
% 0.75/0.92  fof(ruleD42a,axiom,(![A]:(![B]:(![P]:(![Q]:((eqangle(P,A,P,B,Q,A,Q,B)&(~coll(P,Q,A)))=>cyclic(A,B,P,Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD42a)).
% 0.75/0.92  fof(c261,plain,(![A]:(![B]:(![P]:(![Q]:((eqangle(P,A,P,B,Q,A,Q,B)&~coll(P,Q,A))=>cyclic(A,B,P,Q)))))),inference(fof_simplification,[status(thm)],[ruleD42a])).
% 0.75/0.92  fof(c262,plain,(![A]:(![B]:(![P]:(![Q]:((~eqangle(P,A,P,B,Q,A,Q,B)|coll(P,Q,A))|cyclic(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[c261])).
% 0.75/0.92  fof(c263,plain,(![X274]:(![X275]:(![X276]:(![X277]:((~eqangle(X276,X274,X276,X275,X277,X274,X277,X275)|coll(X276,X277,X274))|cyclic(X274,X275,X276,X277)))))),inference(variable_rename,[status(thm)],[c262])).
% 0.75/0.92  cnf(c264,plain,~eqangle(X988,X985,X988,X986,X987,X985,X987,X986)|coll(X988,X987,X985)|cyclic(X985,X986,X988,X987),inference(split_conjunct,[status(thm)],[c263])).
% 0.75/0.92  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)).
% 0.75/0.92  fof(c258,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])).
% 0.75/0.92  fof(c259,plain,(![X270]:(![X271]:(![X272]:(![X273]:((~eqangle(X272,X270,X272,X271,X273,X270,X273,X271)|~coll(X272,X273,X271))|cyclic(X270,X271,X272,X273)))))),inference(variable_rename,[status(thm)],[c258])).
% 0.75/0.92  cnf(c260,plain,~eqangle(X983,X981,X983,X984,X982,X981,X982,X984)|~coll(X983,X982,X984)|cyclic(X981,X984,X983,X982),inference(split_conjunct,[status(thm)],[c259])).
% 0.75/0.92  fof(ruleX17,axiom,(![A]:(![B]:(![O]:(?[C]:((cong(O,A,O,B)&perp(A,O,O,B))=>(coll(A,O,C)&cong(O,A,O,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX17)).
% 0.75/0.92  fof(c18,plain,(![A]:(![B]:(![O]:(?[C]:((~cong(O,A,O,B)|~perp(A,O,O,B))|(coll(A,O,C)&cong(O,A,O,C))))))),inference(fof_nnf,[status(thm)],[ruleX17])).
% 0.75/0.92  fof(c19,plain,(![A]:(![B]:(![O]:((~cong(O,A,O,B)|~perp(A,O,O,B))|(?[C]:(coll(A,O,C)&cong(O,A,O,C))))))),inference(shift_quantors,[status(thm)],[c18])).
% 0.75/0.92  fof(c20,plain,(![X9]:(![X10]:(![X11]:((~cong(X11,X9,X11,X10)|~perp(X9,X11,X11,X10))|(?[X12]:(coll(X9,X11,X12)&cong(X11,X9,X11,X12))))))),inference(variable_rename,[status(thm)],[c19])).
% 0.75/0.92  fof(c21,plain,(![X9]:(![X10]:(![X11]:((~cong(X11,X9,X11,X10)|~perp(X9,X11,X11,X10))|(coll(X9,X11,skolem0002(X9,X10,X11))&cong(X11,X9,X11,skolem0002(X9,X10,X11))))))),inference(skolemize,[status(esa)],[c20])).
% 0.75/0.92  fof(c22,plain,(![X9]:(![X10]:(![X11]:(((~cong(X11,X9,X11,X10)|~perp(X9,X11,X11,X10))|coll(X9,X11,skolem0002(X9,X10,X11)))&((~cong(X11,X9,X11,X10)|~perp(X9,X11,X11,X10))|cong(X11,X9,X11,skolem0002(X9,X10,X11))))))),inference(distribute,[status(thm)],[c21])).
% 0.75/0.92  cnf(c24,plain,~cong(X979,X980,X979,X978)|~perp(X980,X979,X979,X978)|cong(X979,X980,X979,skolem0002(X980,X978,X979)),inference(split_conjunct,[status(thm)],[c22])).
% 0.75/0.92  fof(ruleD45,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:(((midp(E,A,B)&para(E,F,B,C))&coll(F,A,C))=>midp(F,A,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD45)).
% 0.75/0.92  fof(c247,plain,(![A]:(![B]:(![C]:(![E]:(![F]:(((~midp(E,A,B)|~para(E,F,B,C))|~coll(F,A,C))|midp(F,A,C))))))),inference(fof_nnf,[status(thm)],[ruleD45])).
% 0.75/0.92  fof(c248,plain,(![X254]:(![X255]:(![X256]:(![X257]:(![X258]:(((~midp(X257,X254,X255)|~para(X257,X258,X255,X256))|~coll(X258,X254,X256))|midp(X258,X254,X256))))))),inference(variable_rename,[status(thm)],[c247])).
% 0.75/0.92  cnf(c249,plain,~midp(X977,X976,X975)|~para(X977,X974,X975,X973)|~coll(X974,X976,X973)|midp(X974,X976,X973),inference(split_conjunct,[status(thm)],[c248])).
% 0.75/0.92  fof(ruleD47,axiom,(![A]:(![B]:(![O]:((eqangle(O,A,A,B,A,B,O,B)&(~coll(O,A,B)))=>cong(O,A,O,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD47)).
% 0.75/0.92  fof(c240,plain,(![A]:(![B]:(![O]:((eqangle(O,A,A,B,A,B,O,B)&~coll(O,A,B))=>cong(O,A,O,B))))),inference(fof_simplification,[status(thm)],[ruleD47])).
% 0.75/0.92  fof(c241,plain,(![A]:(![B]:(![O]:((~eqangle(O,A,A,B,A,B,O,B)|coll(O,A,B))|cong(O,A,O,B))))),inference(fof_nnf,[status(thm)],[c240])).
% 0.75/0.92  fof(c242,plain,(![X248]:(![X249]:(![X250]:((~eqangle(X250,X248,X248,X249,X248,X249,X250,X249)|coll(X250,X248,X249))|cong(X250,X248,X250,X249))))),inference(variable_rename,[status(thm)],[c241])).
% 0.75/0.92  cnf(c243,plain,~eqangle(X970,X972,X972,X971,X972,X971,X970,X971)|coll(X970,X972,X971)|cong(X970,X972,X970,X971),inference(split_conjunct,[status(thm)],[c242])).
% 0.75/0.92  fof(ruleD50,axiom,(![A]:(![B]:(![C]:(![O]:(![M]:((circle(O,A,B,C)&midp(M,B,C))=>eqangle(A,B,A,C,O,B,O,M))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD50)).
% 0.75/0.92  fof(c231,plain,(![A]:(![B]:(![C]:(![O]:(![M]:((~circle(O,A,B,C)|~midp(M,B,C))|eqangle(A,B,A,C,O,B,O,M))))))),inference(fof_nnf,[status(thm)],[ruleD50])).
% 0.75/0.92  fof(c232,plain,(![X233]:(![X234]:(![X235]:(![X236]:(![X237]:((~circle(X236,X233,X234,X235)|~midp(X237,X234,X235))|eqangle(X233,X234,X233,X235,X236,X234,X236,X237))))))),inference(variable_rename,[status(thm)],[c231])).
% 0.75/0.92  cnf(c233,plain,~circle(X968,X969,X965,X967)|~midp(X966,X965,X967)|eqangle(X969,X965,X969,X967,X968,X965,X968,X966),inference(split_conjunct,[status(thm)],[c232])).
% 0.75/0.92  cnf(c72,plain,~perp(X958,X959,X961,X960)|~perp(X961,X959,X958,X960)|coll(skolem0011(X958,X961,X960),X960,X958),inference(split_conjunct,[status(thm)],[c69])).
% 0.75/0.92  cnf(c410,plain,~perp(X962,X963,X962,X964)|coll(skolem0011(X962,X962,X964),X964,X962),inference(factor,[status(thm)],[c72])).
% 0.75/0.92  fof(ruleX18,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(?[R]:((((para(A,B,C,D)&coll(P,A,C))&coll(P,B,D))&coll(Q,A,B))=>(coll(P,Q,R)&coll(R,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX18)).
% 0.75/0.92  fof(c11,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(?[R]:((((~para(A,B,C,D)|~coll(P,A,C))|~coll(P,B,D))|~coll(Q,A,B))|(coll(P,Q,R)&coll(R,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleX18])).
% 0.75/0.92  fof(c12,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:((((~para(A,B,C,D)|~coll(P,A,C))|~coll(P,B,D))|~coll(Q,A,B))|(?[R]:(coll(P,Q,R)&coll(R,C,D)))))))))),inference(shift_quantors,[status(thm)],[c11])).
% 0.75/0.92  fof(c13,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((~para(X2,X3,X4,X5)|~coll(X6,X2,X4))|~coll(X6,X3,X5))|~coll(X7,X2,X3))|(?[X8]:(coll(X6,X7,X8)&coll(X8,X4,X5)))))))))),inference(variable_rename,[status(thm)],[c12])).
% 0.75/0.92  fof(c14,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((~para(X2,X3,X4,X5)|~coll(X6,X2,X4))|~coll(X6,X3,X5))|~coll(X7,X2,X3))|(coll(X6,X7,skolem0001(X2,X3,X4,X5,X6,X7))&coll(skolem0001(X2,X3,X4,X5,X6,X7),X4,X5))))))))),inference(skolemize,[status(esa)],[c13])).
% 0.75/0.92  fof(c15,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(((((~para(X2,X3,X4,X5)|~coll(X6,X2,X4))|~coll(X6,X3,X5))|~coll(X7,X2,X3))|coll(X6,X7,skolem0001(X2,X3,X4,X5,X6,X7)))&((((~para(X2,X3,X4,X5)|~coll(X6,X2,X4))|~coll(X6,X3,X5))|~coll(X7,X2,X3))|coll(skolem0001(X2,X3,X4,X5,X6,X7),X4,X5))))))))),inference(distribute,[status(thm)],[c14])).
% 0.75/0.92  cnf(c17,plain,~para(X957,X953,X954,X956)|~coll(X952,X957,X954)|~coll(X952,X953,X956)|~coll(X955,X957,X953)|coll(skolem0001(X957,X953,X954,X956,X952,X955),X954,X956),inference(split_conjunct,[status(thm)],[c15])).
% 0.75/0.92  cnf(c70,plain,~perp(X945,X946,X948,X947)|~perp(X948,X946,X945,X947)|coll(skolem0010(X945,X948,X947),X947,X948),inference(split_conjunct,[status(thm)],[c69])).
% 0.75/0.92  cnf(c409,plain,~perp(X951,X950,X951,X949)|coll(skolem0010(X951,X951,X949),X949,X951),inference(factor,[status(thm)],[c70])).
% 0.75/0.92  cnf(c23,plain,~cong(X943,X944,X943,X942)|~perp(X944,X943,X943,X942)|coll(X944,X943,skolem0002(X944,X942,X943)),inference(split_conjunct,[status(thm)],[c22])).
% 0.75/0.92  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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD18)).
% 0.75/0.92  fof(c340,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])).
% 0.75/0.92  fof(c341,plain,(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(~eqangle(X442,X443,X444,X445,X446,X447,X448,X449)|eqangle(X443,X442,X444,X445,X446,X447,X448,X449)))))))))),inference(variable_rename,[status(thm)],[c340])).
% 0.75/0.92  cnf(c342,plain,~eqangle(X934,X936,X941,X940,X937,X935,X939,X938)|eqangle(X936,X934,X941,X940,X937,X935,X939,X938),inference(split_conjunct,[status(thm)],[c341])).
% 0.75/0.92  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)).
% 0.75/0.92  fof(c337,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])).
% 0.75/0.92  fof(c338,plain,(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(~eqangle(X434,X435,X436,X437,X438,X439,X440,X441)|eqangle(X436,X437,X434,X435,X440,X441,X438,X439)))))))))),inference(variable_rename,[status(thm)],[c337])).
% 0.75/0.92  cnf(c339,plain,~eqangle(X931,X932,X928,X929,X926,X927,X930,X933)|eqangle(X928,X929,X931,X932,X930,X933,X926,X927),inference(split_conjunct,[status(thm)],[c338])).
% 0.75/0.92  cnf(c16,plain,~para(X925,X921,X922,X924)|~coll(X920,X925,X922)|~coll(X920,X921,X924)|~coll(X923,X925,X921)|coll(X920,X923,skolem0001(X925,X921,X922,X924,X920,X923)),inference(split_conjunct,[status(thm)],[c15])).
% 0.75/0.92  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)).
% 0.75/0.92  fof(c334,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])).
% 0.75/0.92  fof(c335,plain,(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(~eqangle(X426,X427,X428,X429,X430,X431,X432,X433)|eqangle(X430,X431,X432,X433,X426,X427,X428,X429)))))))))),inference(variable_rename,[status(thm)],[c334])).
% 0.75/0.92  cnf(c336,plain,~eqangle(X916,X918,X915,X913,X912,X914,X919,X917)|eqangle(X912,X914,X919,X917,X916,X918,X915,X913),inference(split_conjunct,[status(thm)],[c335])).
% 0.75/0.92  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)).
% 0.75/0.92  fof(c331,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])).
% 0.75/0.92  fof(c332,plain,(![X418]:(![X419]:(![X420]:(![X421]:(![X422]:(![X423]:(![X424]:(![X425]:(~eqangle(X418,X419,X420,X421,X422,X423,X424,X425)|eqangle(X418,X419,X422,X423,X420,X421,X424,X425)))))))))),inference(variable_rename,[status(thm)],[c331])).
% 0.75/0.92  cnf(c333,plain,~eqangle(X905,X906,X910,X908,X911,X904,X907,X909)|eqangle(X905,X906,X911,X904,X910,X908,X907,X909),inference(split_conjunct,[status(thm)],[c332])).
% 0.75/0.92  fof(ruleD26,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqratio(A,B,C,D,P,Q,U,V)=>eqratio(B,A,C,D,P,Q,U,V)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD26)).
% 0.75/0.92  fof(c316,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqratio(A,B,C,D,P,Q,U,V)|eqratio(B,A,C,D,P,Q,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD26])).
% 0.75/0.92  fof(c317,plain,(![X384]:(![X385]:(![X386]:(![X387]:(![X388]:(![X389]:(![X390]:(![X391]:(~eqratio(X384,X385,X386,X387,X388,X389,X390,X391)|eqratio(X385,X384,X386,X387,X388,X389,X390,X391)))))))))),inference(variable_rename,[status(thm)],[c316])).
% 0.75/0.92  cnf(c318,plain,~eqratio(X903,X897,X896,X902,X898,X900,X901,X899)|eqratio(X897,X903,X896,X902,X898,X900,X901,X899),inference(split_conjunct,[status(thm)],[c317])).
% 0.75/0.92  fof(ruleD27,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqratio(A,B,C,D,P,Q,U,V)=>eqratio(C,D,A,B,U,V,P,Q)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD27)).
% 0.75/0.92  fof(c313,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqratio(A,B,C,D,P,Q,U,V)|eqratio(C,D,A,B,U,V,P,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleD27])).
% 0.75/0.92  fof(c314,plain,(![X376]:(![X377]:(![X378]:(![X379]:(![X380]:(![X381]:(![X382]:(![X383]:(~eqratio(X376,X377,X378,X379,X380,X381,X382,X383)|eqratio(X378,X379,X376,X377,X382,X383,X380,X381)))))))))),inference(variable_rename,[status(thm)],[c313])).
% 0.75/0.92  cnf(c315,plain,~eqratio(X894,X889,X888,X895,X890,X892,X893,X891)|eqratio(X888,X895,X894,X889,X893,X891,X890,X892),inference(split_conjunct,[status(thm)],[c314])).
% 0.75/0.92  fof(ruleD28,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqratio(A,B,C,D,P,Q,U,V)=>eqratio(P,Q,U,V,A,B,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD28)).
% 0.75/0.92  fof(c310,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqratio(A,B,C,D,P,Q,U,V)|eqratio(P,Q,U,V,A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD28])).
% 0.75/0.92  fof(c311,plain,(![X368]:(![X369]:(![X370]:(![X371]:(![X372]:(![X373]:(![X374]:(![X375]:(~eqratio(X368,X369,X370,X371,X372,X373,X374,X375)|eqratio(X372,X373,X374,X375,X368,X369,X370,X371)))))))))),inference(variable_rename,[status(thm)],[c310])).
% 0.75/0.92  cnf(c312,plain,~eqratio(X881,X883,X884,X880,X886,X882,X887,X885)|eqratio(X886,X882,X887,X885,X881,X883,X884,X880),inference(split_conjunct,[status(thm)],[c311])).
% 0.75/0.92  cnf(c10,axiom,X873!=X875|X876!=X879|X869!=X872|X870!=X871|X874!=X877|X868!=X878|~contri(X873,X876,X869,X870,X874,X868)|contri(X875,X879,X872,X871,X877,X878),theory(equality)).
% 0.75/0.92  fof(ruleD29,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqratio(A,B,C,D,P,Q,U,V)=>eqratio(A,B,P,Q,C,D,U,V)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD29)).
% 0.75/0.92  fof(c307,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqratio(A,B,C,D,P,Q,U,V)|eqratio(A,B,P,Q,C,D,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD29])).
% 0.75/0.92  fof(c308,plain,(![X360]:(![X361]:(![X362]:(![X363]:(![X364]:(![X365]:(![X366]:(![X367]:(~eqratio(X360,X361,X362,X363,X364,X365,X366,X367)|eqratio(X360,X361,X364,X365,X362,X363,X366,X367)))))))))),inference(variable_rename,[status(thm)],[c307])).
% 0.75/0.92  cnf(c309,plain,~eqratio(X863,X866,X862,X860,X865,X864,X861,X867)|eqratio(X863,X866,X865,X864,X862,X860,X861,X867),inference(split_conjunct,[status(thm)],[c308])).
% 0.75/0.92  fof(ruleD70,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:((midp(M,A,B)&midp(N,C,D))=>eqratio(M,A,A,B,N,C,C,D)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD70)).
% 0.75/0.92  fof(c164,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(![N]:((~midp(M,A,B)|~midp(N,C,D))|eqratio(M,A,A,B,N,C,C,D)))))))),inference(fof_nnf,[status(thm)],[ruleD70])).
% 0.75/0.92  fof(c165,plain,(![X141]:(![X142]:(![X143]:(![X144]:(![X145]:(![X146]:((~midp(X145,X141,X142)|~midp(X146,X143,X144))|eqratio(X145,X141,X141,X142,X146,X143,X143,X144)))))))),inference(variable_rename,[status(thm)],[c164])).
% 0.75/0.92  cnf(c166,plain,~midp(X855,X853,X856)|~midp(X854,X852,X851)|eqratio(X855,X853,X853,X856,X854,X852,X852,X851),inference(split_conjunct,[status(thm)],[c165])).
% 0.75/0.92  cnf(c408,plain,~midp(X857,X859,X858)|eqratio(X857,X859,X859,X858,X857,X859,X859,X858),inference(factor,[status(thm)],[c166])).
% 0.75/0.92  fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)&para(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 0.75/0.92  fof(c378,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])).
% 0.75/0.92  fof(c379,plain,(![X499]:(![X500]:(![X501]:(![X502]:(![X503]:(![X504]:((~para(X499,X500,X501,X502)|~para(X501,X502,X503,X504))|para(X499,X500,X503,X504)))))))),inference(variable_rename,[status(thm)],[c378])).
% 0.75/0.92  cnf(c380,plain,~para(X845,X844,X846,X848)|~para(X846,X848,X847,X843)|para(X845,X844,X847,X843),inference(split_conjunct,[status(thm)],[c379])).
% 0.75/0.92  cnf(c9,axiom,X836!=X838|X839!=X842|X832!=X835|X833!=X834|X837!=X840|X831!=X841|~simtri(X836,X839,X832,X833,X837,X831)|simtri(X838,X842,X835,X834,X840,X841),theory(equality)).
% 0.75/0.92  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)).
% 0.75/0.92  fof(c369,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])).
% 0.75/0.92  fof(c370,plain,(![X485]:(![X486]:(![X487]:(![X488]:(![X489]:(![X490]:((~perp(X485,X486,X487,X488)|~perp(X487,X488,X489,X490))|para(X485,X486,X489,X490)))))))),inference(variable_rename,[status(thm)],[c369])).
% 0.75/0.92  cnf(c371,plain,~perp(X825,X828,X827,X823)|~perp(X827,X823,X824,X826)|para(X825,X828,X824,X826),inference(split_conjunct,[status(thm)],[c370])).
% 0.75/0.92  cnf(c406,plain,~perp(X830,X829,X830,X829)|para(X830,X829,X830,X829),inference(factor,[status(thm)],[c371])).
% 0.75/0.92  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)).
% 0.77/0.92  fof(c366,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])).
% 0.77/0.92  fof(c367,plain,(![X479]:(![X480]:(![X481]:(![X482]:(![X483]:(![X484]:((~para(X479,X480,X481,X482)|~perp(X481,X482,X483,X484))|perp(X479,X480,X483,X484)))))))),inference(variable_rename,[status(thm)],[c366])).
% 0.77/0.92  cnf(c368,plain,~para(X817,X820,X821,X822)|~perp(X821,X822,X818,X819)|perp(X817,X820,X818,X819),inference(split_conjunct,[status(thm)],[c367])).
% 0.77/0.92  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)).
% 0.77/0.92  fof(c360,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])).
% 0.77/0.92  fof(c361,plain,(![X472]:(![X473]:(![X474]:(![X475]:((~cong(X475,X472,X475,X473)|~cong(X475,X472,X475,X474))|circle(X475,X472,X473,X474)))))),inference(variable_rename,[status(thm)],[c360])).
% 0.77/0.92  cnf(c362,plain,~cong(X811,X810,X811,X812)|~cong(X811,X810,X811,X813)|circle(X811,X810,X812,X813),inference(split_conjunct,[status(thm)],[c361])).
% 0.77/0.92  cnf(c405,plain,~cong(X814,X815,X814,X816)|circle(X814,X815,X816,X816),inference(factor,[status(thm)],[c362])).
% 0.77/0.92  cnf(c8,axiom,X801!=X803|X804!=X809|X796!=X800|X797!=X798|X802!=X805|X795!=X808|X799!=X794|X806!=X807|~eqratio(X801,X804,X796,X797,X802,X795,X799,X806)|eqratio(X803,X809,X800,X798,X805,X808,X794,X807),theory(equality)).
% 0.77/0.92  fof(ruleD17,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:((cyclic(A,B,C,D)&cyclic(A,B,C,E))=>cyclic(B,C,D,E))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD17)).
% 0.77/0.92  fof(c343,plain,(![A]:(![B]:(![C]:(![D]:(![E]:((~cyclic(A,B,C,D)|~cyclic(A,B,C,E))|cyclic(B,C,D,E))))))),inference(fof_nnf,[status(thm)],[ruleD17])).
% 0.77/0.92  fof(c344,plain,(![X450]:(![X451]:(![X452]:(![X453]:(![X454]:((~cyclic(X450,X451,X452,X453)|~cyclic(X450,X451,X452,X454))|cyclic(X451,X452,X453,X454))))))),inference(variable_rename,[status(thm)],[c343])).
% 0.77/0.92  cnf(c345,plain,~cyclic(X789,X786,X785,X788)|~cyclic(X789,X786,X785,X787)|cyclic(X786,X785,X788,X787),inference(split_conjunct,[status(thm)],[c344])).
% 0.77/0.92  cnf(c404,plain,~cyclic(X790,X793,X791,X792)|cyclic(X793,X791,X792,X792),inference(factor,[status(thm)],[c345])).
% 0.77/0.92  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)).
% 0.77/0.92  fof(c319,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])).
% 0.77/0.92  fof(c320,plain,(![X392]:(![X393]:(![X394]:(![X395]:(![X396]:(![X397]:((~cong(X392,X393,X394,X395)|~cong(X394,X395,X396,X397))|cong(X392,X393,X396,X397)))))))),inference(variable_rename,[status(thm)],[c319])).
% 0.77/0.92  cnf(c321,plain,~cong(X779,X781,X782,X780)|~cong(X782,X780,X778,X777)|cong(X779,X781,X778,X777),inference(split_conjunct,[status(thm)],[c320])).
% 0.77/0.92  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)).
% 0.77/0.93  fof(c211,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])).
% 0.77/0.93  fof(c212,plain,(![X208]:(![X209]:(![X210]:(![X211]:((~cong(X208,X210,X209,X210)|~cong(X208,X211,X209,X211))|perp(X208,X209,X210,X211)))))),inference(variable_rename,[status(thm)],[c211])).
% 0.77/0.93  cnf(c213,plain,~cong(X755,X754,X756,X754)|~cong(X755,X757,X756,X757)|perp(X755,X756,X754,X757),inference(split_conjunct,[status(thm)],[c212])).
% 0.77/0.93  cnf(c402,plain,~cong(X774,X776,X775,X776)|perp(X774,X775,X776,X776),inference(factor,[status(thm)],[c213])).
% 0.77/0.93  cnf(c7,axiom,X765!=X767|X768!=X773|X760!=X764|X761!=X762|X766!=X769|X759!=X772|X763!=X758|X770!=X771|~eqangle(X765,X768,X760,X761,X766,X759,X763,X770)|eqangle(X767,X773,X764,X762,X769,X772,X758,X771),theory(equality)).
% 0.77/0.93  fof(ruleD59,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(simtri(A,B,C,P,Q,R)=>eqratio(A,B,A,C,P,Q,P,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD59)).
% 0.77/0.93  fof(c201,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~simtri(A,B,C,P,Q,R)|eqratio(A,B,A,C,P,Q,P,R)))))))),inference(fof_nnf,[status(thm)],[ruleD59])).
% 0.77/0.93  fof(c202,plain,(![X192]:(![X193]:(![X194]:(![X195]:(![X196]:(![X197]:(~simtri(X192,X193,X194,X195,X196,X197)|eqratio(X192,X193,X192,X194,X195,X196,X195,X197)))))))),inference(variable_rename,[status(thm)],[c201])).
% 0.77/0.93  cnf(c203,plain,~simtri(X750,X753,X751,X748,X749,X752)|eqratio(X750,X753,X750,X751,X748,X749,X748,X752),inference(split_conjunct,[status(thm)],[c202])).
% 0.77/0.93  fof(ruleD60,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(simtri(A,B,C,P,Q,R)=>eqangle(A,B,B,C,P,Q,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD60)).
% 0.77/0.93  fof(c198,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~simtri(A,B,C,P,Q,R)|eqangle(A,B,B,C,P,Q,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD60])).
% 0.77/0.93  fof(c199,plain,(![X186]:(![X187]:(![X188]:(![X189]:(![X190]:(![X191]:(~simtri(X186,X187,X188,X189,X190,X191)|eqangle(X186,X187,X187,X188,X189,X190,X190,X191)))))))),inference(variable_rename,[status(thm)],[c198])).
% 0.77/0.93  cnf(c200,plain,~simtri(X744,X746,X743,X745,X742,X747)|eqangle(X744,X746,X746,X743,X745,X742,X742,X747),inference(split_conjunct,[status(thm)],[c199])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c225,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])).
% 0.77/0.93  fof(c226,plain,(![X224]:(![X225]:(![X226]:(![X227]:((~perp(X224,X225,X225,X226)|~midp(X227,X224,X226))|cong(X224,X227,X225,X227)))))),inference(variable_rename,[status(thm)],[c225])).
% 0.77/0.93  cnf(c227,plain,~perp(X739,X738,X738,X741)|~midp(X740,X739,X741)|cong(X739,X740,X738,X740),inference(split_conjunct,[status(thm)],[c226])).
% 0.77/0.93  fof(ruleD53,axiom,(![A]:(![B]:(![C]:(![O]:((circle(O,A,B,C)&coll(O,A,C))=>perp(A,B,B,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD53)).
% 0.77/0.93  fof(c220,plain,(![A]:(![B]:(![C]:(![O]:((~circle(O,A,B,C)|~coll(O,A,C))|perp(A,B,B,C)))))),inference(fof_nnf,[status(thm)],[ruleD53])).
% 0.77/0.93  fof(c221,plain,(![A]:(![B]:(![C]:((![O]:(~circle(O,A,B,C)|~coll(O,A,C)))|perp(A,B,B,C))))),inference(shift_quantors,[status(thm)],[c220])).
% 0.77/0.93  fof(c223,plain,(![X220]:(![X221]:(![X222]:(![X223]:((~circle(X223,X220,X221,X222)|~coll(X223,X220,X222))|perp(X220,X221,X221,X222)))))),inference(shift_quantors,[status(thm)],[fof(c222,plain,(![X220]:(![X221]:(![X222]:((![X223]:(~circle(X223,X220,X221,X222)|~coll(X223,X220,X222)))|perp(X220,X221,X221,X222))))),inference(variable_rename,[status(thm)],[c221])).])).
% 0.77/0.93  cnf(c224,plain,~circle(X737,X736,X735,X734)|~coll(X737,X736,X734)|perp(X736,X735,X735,X734),inference(split_conjunct,[status(thm)],[c223])).
% 0.77/0.93  cnf(c6,axiom,X730!=X731|X732!=X733|X726!=X729|X727!=X728|~cyclic(X730,X732,X726,X727)|cyclic(X731,X733,X729,X728),theory(equality)).
% 0.77/0.93  fof(ruleD55,axiom,(![A]:(![B]:(![M]:(![O]:((midp(M,A,B)&perp(O,M,A,B))=>cong(O,A,O,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD55)).
% 0.77/0.93  fof(c214,plain,(![A]:(![B]:(![M]:(![O]:((~midp(M,A,B)|~perp(O,M,A,B))|cong(O,A,O,B)))))),inference(fof_nnf,[status(thm)],[ruleD55])).
% 0.77/0.93  fof(c215,plain,(![X212]:(![X213]:(![X214]:(![X215]:((~midp(X214,X212,X213)|~perp(X215,X214,X212,X213))|cong(X215,X212,X215,X213)))))),inference(variable_rename,[status(thm)],[c214])).
% 0.77/0.93  cnf(c216,plain,~midp(X725,X722,X724)|~perp(X723,X725,X722,X724)|cong(X723,X722,X723,X724),inference(split_conjunct,[status(thm)],[c215])).
% 0.77/0.93  fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 0.77/0.93  fof(c59,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 0.77/0.93  fof(c60,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c59])).
% 0.77/0.93  fof(c61,plain,(![X44]:(![X45]:(![X46]:(![X47]:(~circle(X47,X44,X45,X46)|(?[X48]:perp(X48,X44,X44,X47))))))),inference(variable_rename,[status(thm)],[c60])).
% 0.77/0.93  fof(c62,plain,(![X44]:(![X45]:(![X46]:(![X47]:(~circle(X47,X44,X45,X46)|perp(skolem0009(X44,X45,X46,X47),X44,X44,X47)))))),inference(skolemize,[status(esa)],[c61])).
% 0.77/0.93  cnf(c63,plain,~circle(X720,X721,X719,X718)|perp(skolem0009(X721,X719,X718,X720),X721,X721,X720),inference(split_conjunct,[status(thm)],[c62])).
% 0.77/0.93  fof(ruleD31,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(simtri(A,C,B,P,R,Q)=>simtri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD31)).
% 0.77/0.93  fof(c299,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~simtri(A,C,B,P,R,Q)|simtri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD31])).
% 0.77/0.93  fof(c300,plain,(![X342]:(![X343]:(![X344]:(![X345]:(![X346]:(![X347]:(~simtri(X342,X344,X343,X345,X347,X346)|simtri(X342,X343,X344,X345,X346,X347)))))))),inference(variable_rename,[status(thm)],[c299])).
% 0.77/0.93  cnf(c301,plain,~simtri(X715,X712,X713,X716,X717,X714)|simtri(X715,X713,X712,X716,X714,X717),inference(split_conjunct,[status(thm)],[c300])).
% 0.77/0.93  fof(ruleD32,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(simtri(B,A,C,Q,P,R)=>simtri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD32)).
% 0.77/0.93  fof(c296,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~simtri(B,A,C,Q,P,R)|simtri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD32])).
% 0.77/0.93  fof(c297,plain,(![X336]:(![X337]:(![X338]:(![X339]:(![X340]:(![X341]:(~simtri(X337,X336,X338,X340,X339,X341)|simtri(X336,X337,X338,X339,X340,X341)))))))),inference(variable_rename,[status(thm)],[c296])).
% 0.77/0.93  cnf(c298,plain,~simtri(X707,X708,X710,X711,X706,X709)|simtri(X708,X707,X710,X706,X711,X709),inference(split_conjunct,[status(thm)],[c297])).
% 0.77/0.93  fof(ruleD33,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(simtri(P,Q,R,A,B,C)=>simtri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD33)).
% 0.77/0.93  fof(c293,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~simtri(P,Q,R,A,B,C)|simtri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD33])).
% 0.77/0.93  fof(c294,plain,(![X330]:(![X331]:(![X332]:(![X333]:(![X334]:(![X335]:(~simtri(X333,X334,X335,X330,X331,X332)|simtri(X330,X331,X332,X333,X334,X335)))))))),inference(variable_rename,[status(thm)],[c293])).
% 0.77/0.93  cnf(c295,plain,~simtri(X701,X703,X704,X700,X705,X702)|simtri(X700,X705,X702,X701,X703,X704),inference(split_conjunct,[status(thm)],[c294])).
% 0.77/0.93  cnf(c5,axiom,X696!=X697|X698!=X699|X692!=X695|X693!=X694|~cong(X696,X698,X692,X693)|cong(X697,X699,X695,X694),theory(equality)).
% 0.77/0.93  fof(ruleD35,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(contri(A,C,B,P,R,Q)=>contri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD35)).
% 0.77/0.93  fof(c287,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~contri(A,C,B,P,R,Q)|contri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD35])).
% 0.77/0.93  fof(c288,plain,(![X315]:(![X316]:(![X317]:(![X318]:(![X319]:(![X320]:(~contri(X315,X317,X316,X318,X320,X319)|contri(X315,X316,X317,X318,X319,X320)))))))),inference(variable_rename,[status(thm)],[c287])).
% 0.77/0.93  cnf(c289,plain,~contri(X689,X688,X686,X691,X687,X690)|contri(X689,X686,X688,X691,X690,X687),inference(split_conjunct,[status(thm)],[c288])).
% 0.77/0.93  fof(ruleD36,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(contri(B,A,C,Q,P,R)=>contri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD36)).
% 0.77/0.93  fof(c284,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~contri(B,A,C,Q,P,R)|contri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD36])).
% 0.77/0.93  fof(c285,plain,(![X309]:(![X310]:(![X311]:(![X312]:(![X313]:(![X314]:(~contri(X310,X309,X311,X313,X312,X314)|contri(X309,X310,X311,X312,X313,X314)))))))),inference(variable_rename,[status(thm)],[c284])).
% 0.77/0.93  cnf(c286,plain,~contri(X681,X682,X683,X680,X685,X684)|contri(X682,X681,X683,X685,X680,X684),inference(split_conjunct,[status(thm)],[c285])).
% 0.77/0.93  fof(ruleD37,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(contri(P,Q,R,A,B,C)=>contri(A,B,C,P,Q,R)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD37)).
% 0.77/0.93  fof(c281,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~contri(P,Q,R,A,B,C)|contri(A,B,C,P,Q,R)))))))),inference(fof_nnf,[status(thm)],[ruleD37])).
% 0.77/0.93  fof(c282,plain,(![X303]:(![X304]:(![X305]:(![X306]:(![X307]:(![X308]:(~contri(X306,X307,X308,X303,X304,X305)|contri(X303,X304,X305,X306,X307,X308)))))))),inference(variable_rename,[status(thm)],[c281])).
% 0.77/0.93  cnf(c283,plain,~contri(X674,X679,X676,X677,X675,X678)|contri(X677,X675,X678,X674,X679,X676),inference(split_conjunct,[status(thm)],[c282])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c273,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])).
% 0.77/0.93  fof(c274,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)],[c273])).
% 0.77/0.93  fof(c276,plain,(![X288]:(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(~eqangle(X288,X289,X292,X293,X290,X291,X292,X293)|para(X288,X289,X290,X291)))))))),inference(shift_quantors,[status(thm)],[fof(c275,plain,(![X288]:(![X289]:(![X290]:(![X291]:((![X292]:(![X293]:~eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))|para(X288,X289,X290,X291)))))),inference(variable_rename,[status(thm)],[c274])).])).
% 0.77/0.93  cnf(c277,plain,~eqangle(X670,X669,X673,X668,X671,X672,X673,X668)|para(X670,X669,X671,X672),inference(split_conjunct,[status(thm)],[c276])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c268,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])).
% 0.77/0.93  fof(c269,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)],[c268])).
% 0.77/0.93  fof(c271,plain,(![X282]:(![X283]:(![X284]:(![X285]:(![X286]:(![X287]:(~para(X282,X283,X284,X285)|eqangle(X282,X283,X286,X287,X284,X285,X286,X287)))))))),inference(shift_quantors,[status(thm)],[fof(c270,plain,(![X282]:(![X283]:(![X284]:(![X285]:(~para(X282,X283,X284,X285)|(![X286]:(![X287]:eqangle(X282,X283,X286,X287,X284,X285,X286,X287)))))))),inference(variable_rename,[status(thm)],[c269])).])).
% 0.77/0.93  cnf(c272,plain,~para(X665,X667,X662,X664)|eqangle(X665,X667,X663,X666,X662,X664,X663,X666),inference(split_conjunct,[status(thm)],[c271])).
% 0.77/0.93  cnf(c4,axiom,X658!=X659|X660!=X661|X654!=X657|X655!=X656|~circle(X658,X660,X654,X655)|circle(X659,X661,X657,X656),theory(equality)).
% 0.77/0.93  fof(ruleD41,axiom,(![A]:(![B]:(![P]:(![Q]:(cyclic(A,B,P,Q)=>eqangle(P,A,P,B,Q,A,Q,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD41)).
% 0.77/0.93  fof(c265,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])).
% 0.77/0.93  fof(c266,plain,(![X278]:(![X279]:(![X280]:(![X281]:(~cyclic(X278,X279,X280,X281)|eqangle(X280,X278,X280,X279,X281,X278,X281,X279)))))),inference(variable_rename,[status(thm)],[c265])).
% 0.77/0.93  cnf(c267,plain,~cyclic(X651,X653,X650,X652)|eqangle(X650,X651,X650,X653,X652,X651,X652,X653),inference(split_conjunct,[status(thm)],[c266])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c250,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])).
% 0.77/0.93  fof(c251,plain,(![X259]:(![X260]:(![X261]:(![X262]:(![X263]:((~midp(X262,X259,X260)|~midp(X263,X259,X261))|para(X262,X263,X260,X261))))))),inference(variable_rename,[status(thm)],[c250])).
% 0.77/0.93  cnf(c252,plain,~midp(X645,X646,X644)|~midp(X642,X646,X643)|para(X645,X642,X644,X643),inference(split_conjunct,[status(thm)],[c251])).
% 0.77/0.93  cnf(c401,plain,~midp(X648,X647,X649)|para(X648,X648,X649,X649),inference(factor,[status(thm)],[c252])).
% 0.77/0.93  fof(ruleD46,axiom,(![A]:(![B]:(![O]:(cong(O,A,O,B)=>eqangle(O,A,A,B,A,B,O,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD46)).
% 0.77/0.93  fof(c244,plain,(![A]:(![B]:(![O]:(~cong(O,A,O,B)|eqangle(O,A,A,B,A,B,O,B))))),inference(fof_nnf,[status(thm)],[ruleD46])).
% 0.77/0.93  fof(c245,plain,(![X251]:(![X252]:(![X253]:(~cong(X253,X251,X253,X252)|eqangle(X253,X251,X251,X252,X251,X252,X253,X252))))),inference(variable_rename,[status(thm)],[c244])).
% 0.77/0.93  cnf(c246,plain,~cong(X639,X641,X639,X640)|eqangle(X639,X641,X641,X640,X641,X640,X639,X640),inference(split_conjunct,[status(thm)],[c245])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c185,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])).
% 0.77/0.93  fof(c186,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c185])).
% 0.77/0.93  fof(c188,plain,(![X169]:(![X170]:(![X171]:(![X172]:(![X173]:((~midp(X173,X169,X170)|~midp(X173,X171,X172))|para(X169,X171,X170,X172))))))),inference(shift_quantors,[status(thm)],[fof(c187,plain,(![X169]:(![X170]:(![X171]:(![X172]:((![X173]:(~midp(X173,X169,X170)|~midp(X173,X171,X172)))|para(X169,X171,X170,X172)))))),inference(variable_rename,[status(thm)],[c186])).])).
% 0.77/0.93  cnf(c189,plain,~midp(X628,X629,X626)|~midp(X628,X627,X625)|para(X629,X627,X626,X625),inference(split_conjunct,[status(thm)],[c188])).
% 0.77/0.93  cnf(c400,plain,~midp(X638,X636,X637)|para(X636,X636,X637,X637),inference(factor,[status(thm)],[c189])).
% 0.77/0.93  cnf(c3,axiom,X632!=X633|X634!=X635|X630!=X631|~midp(X632,X634,X630)|midp(X633,X635,X631),theory(equality)).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c173,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 0.77/0.93  fof(c174,plain,(![X153]:(![X154]:(![X155]:((~cong(X153,X154,X153,X155)|~coll(X153,X154,X155))|midp(X153,X154,X155))))),inference(variable_rename,[status(thm)],[c173])).
% 0.77/0.93  cnf(c175,plain,~cong(X624,X623,X624,X622)|~coll(X624,X623,X622)|midp(X624,X623,X622),inference(split_conjunct,[status(thm)],[c174])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c387,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 0.77/0.93  fof(c388,plain,(![X513]:(![X514]:(![X515]:(![X516]:((~coll(X513,X514,X515)|~coll(X513,X514,X516))|coll(X515,X516,X513)))))),inference(variable_rename,[status(thm)],[c387])).
% 0.77/0.93  cnf(c389,plain,~coll(X618,X615,X617)|~coll(X618,X615,X616)|coll(X617,X616,X618),inference(split_conjunct,[status(thm)],[c388])).
% 0.77/0.93  cnf(c399,plain,~coll(X621,X620,X619)|coll(X619,X619,X621),inference(factor,[status(thm)],[c389])).
% 0.77/0.93  fof(ruleD62,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(contri(A,B,C,P,Q,R)=>cong(A,B,P,Q)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD62)).
% 0.77/0.93  fof(c190,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:(~contri(A,B,C,P,Q,R)|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD62])).
% 0.77/0.93  fof(c191,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:((![R]:~contri(A,B,C,P,Q,R))|cong(A,B,P,Q))))))),inference(shift_quantors,[status(thm)],[c190])).
% 0.77/0.93  fof(c193,plain,(![X174]:(![X175]:(![X176]:(![X177]:(![X178]:(![X179]:(~contri(X174,X175,X176,X177,X178,X179)|cong(X174,X175,X177,X178)))))))),inference(shift_quantors,[status(thm)],[fof(c192,plain,(![X174]:(![X175]:(![X176]:(![X177]:(![X178]:((![X179]:~contri(X174,X175,X176,X177,X178,X179))|cong(X174,X175,X177,X178))))))),inference(variable_rename,[status(thm)],[c191])).])).
% 0.77/0.93  cnf(c194,plain,~contri(X614,X609,X610,X612,X613,X611)|cong(X614,X609,X612,X613),inference(split_conjunct,[status(thm)],[c193])).
% 0.77/0.93  cnf(c2,axiom,X605!=X606|X607!=X608|X601!=X604|X602!=X603|~perp(X605,X607,X601,X602)|perp(X606,X608,X604,X603),theory(equality)).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 0.77/0.93  fof(c385,plain,(![X509]:(![X510]:(![X511]:(![X512]:(~para(X509,X510,X511,X512)|para(X509,X510,X512,X511)))))),inference(variable_rename,[status(thm)],[c384])).
% 0.77/0.93  cnf(c386,plain,~para(X600,X597,X598,X599)|para(X600,X597,X599,X598),inference(split_conjunct,[status(thm)],[c385])).
% 0.77/0.93  fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 0.77/0.93  fof(c381,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 0.77/0.93  fof(c382,plain,(![X505]:(![X506]:(![X507]:(![X508]:(~para(X505,X506,X507,X508)|para(X507,X508,X505,X506)))))),inference(variable_rename,[status(thm)],[c381])).
% 0.77/0.93  cnf(c383,plain,~para(X594,X595,X596,X593)|para(X596,X593,X594,X595),inference(split_conjunct,[status(thm)],[c382])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c375,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 0.77/0.93  fof(c376,plain,(![X495]:(![X496]:(![X497]:(![X498]:(~perp(X495,X496,X497,X498)|perp(X495,X496,X498,X497)))))),inference(variable_rename,[status(thm)],[c375])).
% 0.77/0.93  cnf(c377,plain,~perp(X592,X589,X590,X591)|perp(X592,X589,X591,X590),inference(split_conjunct,[status(thm)],[c376])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c372,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 0.77/0.93  fof(c373,plain,(![X491]:(![X492]:(![X493]:(![X494]:(~perp(X491,X492,X493,X494)|perp(X493,X494,X491,X492)))))),inference(variable_rename,[status(thm)],[c372])).
% 0.77/0.93  cnf(c374,plain,~perp(X588,X585,X586,X587)|perp(X586,X587,X588,X585),inference(split_conjunct,[status(thm)],[c373])).
% 0.77/0.93  fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 0.77/0.93  fof(c352,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 0.77/0.93  fof(c353,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X463,X464,X466,X465)))))),inference(variable_rename,[status(thm)],[c352])).
% 0.77/0.93  cnf(c354,plain,~cyclic(X582,X583,X584,X581)|cyclic(X582,X583,X581,X584),inference(split_conjunct,[status(thm)],[c353])).
% 0.77/0.93  cnf(c1,axiom,X577!=X578|X579!=X580|X573!=X576|X574!=X575|~para(X577,X579,X573,X574)|para(X578,X580,X576,X575),theory(equality)).
% 0.77/0.93  fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 0.77/0.93  fof(c349,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 0.77/0.93  fof(c350,plain,(![X459]:(![X460]:(![X461]:(![X462]:(~cyclic(X459,X460,X461,X462)|cyclic(X459,X461,X460,X462)))))),inference(variable_rename,[status(thm)],[c349])).
% 0.77/0.93  cnf(c351,plain,~cyclic(X572,X571,X569,X570)|cyclic(X572,X569,X571,X570),inference(split_conjunct,[status(thm)],[c350])).
% 0.77/0.93  fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 0.77/0.93  fof(c346,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 0.77/0.93  fof(c347,plain,(![X455]:(![X456]:(![X457]:(![X458]:(~cyclic(X455,X456,X457,X458)|cyclic(X456,X455,X457,X458)))))),inference(variable_rename,[status(thm)],[c346])).
% 0.77/0.93  cnf(c348,plain,~cyclic(X568,X567,X566,X565)|cyclic(X567,X568,X566,X565),inference(split_conjunct,[status(thm)],[c347])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c325,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 0.77/0.93  fof(c326,plain,(![X402]:(![X403]:(![X404]:(![X405]:(~cong(X402,X403,X404,X405)|cong(X402,X403,X405,X404)))))),inference(variable_rename,[status(thm)],[c325])).
% 0.77/0.93  cnf(c327,plain,~cong(X564,X562,X563,X561)|cong(X564,X562,X561,X563),inference(split_conjunct,[status(thm)],[c326])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c322,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 0.77/0.93  fof(c323,plain,(![X398]:(![X399]:(![X400]:(![X401]:(~cong(X398,X399,X400,X401)|cong(X400,X401,X398,X399)))))),inference(variable_rename,[status(thm)],[c322])).
% 0.77/0.93  cnf(c324,plain,~cong(X560,X559,X557,X558)|cong(X557,X558,X560,X559),inference(split_conjunct,[status(thm)],[c323])).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c176,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 0.77/0.93  fof(c177,plain,(![X156]:(![X157]:(![X158]:(~para(X156,X157,X156,X158)|coll(X156,X157,X158))))),inference(variable_rename,[status(thm)],[c176])).
% 0.77/0.93  cnf(c178,plain,~para(X555,X554,X555,X556)|coll(X555,X554,X556),inference(split_conjunct,[status(thm)],[c177])).
% 0.77/0.93  cnf(c0,axiom,X550!=X551|X552!=X553|X548!=X549|~coll(X550,X552,X548)|coll(X551,X553,X549),theory(equality)).
% 0.77/0.93  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)).
% 0.77/0.93  fof(c170,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 0.77/0.93  fof(c171,plain,(![X150]:(![X151]:(![X152]:(~midp(X150,X151,X152)|cong(X150,X151,X150,X152))))),inference(variable_rename,[status(thm)],[c170])).
% 0.77/0.93  cnf(c172,plain,~midp(X545,X547,X546)|cong(X545,X547,X545,X546),inference(split_conjunct,[status(thm)],[c171])).
% 0.77/0.93  fof(ruleD1,axiom,(![A]:(![B]:(![C]:(coll(A,B,C)=>coll(A,C,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD1)).
% 0.77/0.93  fof(c393,plain,(![A]:(![B]:(![C]:(~coll(A,B,C)|coll(A,C,B))))),inference(fof_nnf,[status(thm)],[ruleD1])).
% 0.77/0.93  fof(c394,plain,(![X520]:(![X521]:(![X522]:(~coll(X520,X521,X522)|coll(X520,X522,X521))))),inference(variable_rename,[status(thm)],[c393])).
% 0.77/0.93  cnf(c395,plain,~coll(X543,X544,X542)|coll(X543,X542,X544),inference(split_conjunct,[status(thm)],[c394])).
% 0.77/0.93  fof(ruleD2,axiom,(![A]:(![B]:(![C]:(coll(A,B,C)=>coll(B,A,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD2)).
% 0.77/0.93  fof(c390,plain,(![A]:(![B]:(![C]:(~coll(A,B,C)|coll(B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD2])).
% 0.77/0.93  fof(c391,plain,(![X517]:(![X518]:(![X519]:(~coll(X517,X518,X519)|coll(X518,X517,X519))))),inference(variable_rename,[status(thm)],[c390])).
% 0.77/0.93  cnf(c392,plain,~coll(X540,X541,X539)|coll(X541,X540,X539),inference(split_conjunct,[status(thm)],[c391])).
% 0.77/0.93  cnf(transitivity,axiom,X533!=X535|X535!=X534|X533=X534,theory(equality)).
% 0.77/0.93  fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 0.77/0.93  fof(c363,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 0.77/0.93  fof(c364,plain,(![X476]:(![X477]:(![X478]:(~midp(X478,X477,X476)|midp(X478,X476,X477))))),inference(variable_rename,[status(thm)],[c363])).
% 0.77/0.93  cnf(c365,plain,~midp(X532,X530,X531)|midp(X532,X531,X530),inference(split_conjunct,[status(thm)],[c364])).
% 0.77/0.93  fof(ruleD69,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>coll(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD69)).
% 0.77/0.93  fof(c167,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD69])).
% 0.77/0.93  fof(c168,plain,(![X147]:(![X148]:(![X149]:(~midp(X147,X148,X149)|coll(X147,X148,X149))))),inference(variable_rename,[status(thm)],[c167])).
% 0.77/0.93  cnf(c169,plain,~midp(X527,X529,X528)|coll(X527,X529,X528),inference(split_conjunct,[status(thm)],[c168])).
% 0.77/0.93  cnf(symmetry,axiom,X524!=X525|X525=X524,theory(equality)).
% 0.77/0.93  cnf(reflexivity,axiom,X523=X523,theory(equality)).
% 0.77/0.93  % SZS output end Saturation
% 0.77/0.93  
% 0.77/0.93  % Initial clauses    : 127
% 0.77/0.93  % Processed clauses  : 150
% 0.77/0.93  % Factors computed   : 36
% 0.77/0.93  % Resolvents computed: 2
% 0.77/0.93  % Tautologies deleted: 8
% 0.77/0.93  % Forward subsumed   : 7
% 0.77/0.93  % Backward subsumed  : 0
% 0.77/0.93  % -------- CPU Time ---------
% 0.77/0.93  % User time          : 0.571 s
% 0.77/0.93  % System time        : 0.015 s
% 0.77/0.93  % Total time         : 0.586 s
%------------------------------------------------------------------------------