%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO560+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:22:17 EDT 2024
% Result : Theorem 95.50s 95.72s
% Output : Refutation 95.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO560+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 08:31:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 95.50/95.72 % Version: 1.5
% 95.50/95.72 % SZS status Theorem
% 95.50/95.72 % SZS output start CNFRefutation
% 95.50/95.72 fof(exemplo6GDDFULL012020,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![H]:(![G]:((((((((perp(D,A,B,C)&coll(D,B,C))&perp(E,B,A,C))&coll(E,A,C))&coll(H,A,D))&coll(H,B,E))&perp(G,H,A,B))&coll(G,A,B))=>eqangle(E,G,G,H,H,G,G,D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL012020)).
% 95.50/95.72 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![H]:(![G]:((((((((perp(D,A,B,C)&coll(D,B,C))&perp(E,B,A,C))&coll(E,A,C))&coll(H,A,D))&coll(H,B,E))&perp(G,H,A,B))&coll(G,A,B))=>eqangle(E,G,G,H,H,G,G,D)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL012020])).
% 95.50/95.72 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[H]:(?[G]:((((((((perp(D,A,B,C)&coll(D,B,C))&perp(E,B,A,C))&coll(E,A,C))&coll(H,A,D))&coll(H,B,E))&perp(G,H,A,B))&coll(G,A,B))&~eqangle(E,G,G,H,H,G,G,D))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 95.50/95.72 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((((perp(X5,X2,X3,X4)&coll(X5,X3,X4))&perp(X6,X3,X2,X4))&coll(X6,X2,X4))&coll(X7,X2,X5))&coll(X7,X3,X6))&perp(X8,X7,X2,X3))&coll(X8,X2,X3))&~eqangle(X6,X8,X8,X7,X7,X8,X8,X5))))))))),inference(variable_rename,[status(thm)],[c12])).
% 95.50/95.72 fof(c14,negated_conjecture,((((((((perp(skolem0004,skolem0001,skolem0002,skolem0003)&coll(skolem0004,skolem0002,skolem0003))&perp(skolem0005,skolem0002,skolem0001,skolem0003))&coll(skolem0005,skolem0001,skolem0003))&coll(skolem0006,skolem0001,skolem0004))&coll(skolem0006,skolem0002,skolem0005))&perp(skolem0007,skolem0006,skolem0001,skolem0002))&coll(skolem0007,skolem0001,skolem0002))&~eqangle(skolem0005,skolem0007,skolem0007,skolem0006,skolem0006,skolem0007,skolem0007,skolem0004)),inference(skolemize,[status(esa)],[c13])).
% 95.50/95.72 cnf(c23,negated_conjecture,~eqangle(skolem0005,skolem0007,skolem0007,skolem0006,skolem0006,skolem0007,skolem0007,skolem0004),inference(split_conjunct,[status(thm)],[c14])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c344,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(A,B,P,Q,C,D,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD21])).
% 95.50/95.72 fof(c345,plain,(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(~eqangle(X425,X426,X427,X428,X429,X430,X431,X432)|eqangle(X425,X426,X429,X430,X427,X428,X431,X432)))))))))),inference(variable_rename,[status(thm)],[c344])).
% 95.50/95.72 cnf(c346,plain,~eqangle(X1206,X1205,X1207,X1202,X1204,X1201,X1208,X1203)|eqangle(X1206,X1205,X1204,X1201,X1207,X1202,X1208,X1203),inference(split_conjunct,[status(thm)],[c345])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c341,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])).
% 95.50/95.72 fof(c342,plain,(![X413]:(![X414]:(![X415]:(![X416]:(![X417]:(![X418]:(![X419]:(![X420]:(![X421]:(![X422]:(![X423]:(![X424]:((~eqangle(X413,X414,X415,X416,X417,X418,X419,X420)|~eqangle(X417,X418,X419,X420,X421,X422,X423,X424))|eqangle(X413,X414,X415,X416,X421,X422,X423,X424)))))))))))))),inference(variable_rename,[status(thm)],[c341])).
% 95.50/95.72 cnf(c343,plain,~eqangle(X1199,X1189,X1191,X1190,X1197,X1194,X1188,X1192)|~eqangle(X1197,X1194,X1188,X1192,X1196,X1198,X1195,X1193)|eqangle(X1199,X1189,X1191,X1190,X1196,X1198,X1195,X1193),inference(split_conjunct,[status(thm)],[c342])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c278,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])).
% 95.50/95.72 fof(c279,plain,(![X285]:(![X286]:(![X287]:(![X288]:(~cyclic(X285,X286,X287,X288)|eqangle(X287,X285,X287,X286,X288,X285,X288,X286)))))),inference(variable_rename,[status(thm)],[c278])).
% 95.50/95.72 cnf(c280,plain,~cyclic(X1049,X1051,X1052,X1050)|eqangle(X1052,X1049,X1052,X1051,X1050,X1049,X1050,X1051),inference(split_conjunct,[status(thm)],[c279])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c365,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 95.50/95.72 fof(c366,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X471,X473,X472)))))),inference(variable_rename,[status(thm)],[c365])).
% 95.50/95.72 cnf(c367,plain,~cyclic(X700,X699,X697,X698)|cyclic(X700,X699,X698,X697),inference(split_conjunct,[status(thm)],[c366])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 95.50/95.72 fof(c363,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c362])).
% 95.50/95.72 cnf(c364,plain,~cyclic(X694,X696,X695,X693)|cyclic(X694,X695,X696,X693),inference(split_conjunct,[status(thm)],[c363])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 95.50/95.72 fof(c401,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c400])).
% 95.50/95.72 cnf(c402,plain,~coll(X780,X779,X778)|~coll(X780,X779,X781)|coll(X778,X781,X780),inference(split_conjunct,[status(thm)],[c401])).
% 95.50/95.72 cnf(c579,plain,~coll(X784,X783,X782)|coll(X782,X782,X784),inference(factor,[status(thm)],[c402])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 95.50/95.72 fof(c190,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c189])).
% 95.50/95.72 cnf(c191,plain,~para(X676,X675,X676,X677)|coll(X676,X675,X677),inference(split_conjunct,[status(thm)],[c190])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c286,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~eqangle(A,B,P,Q,C,D,P,Q)|para(A,B,C,D)))))))),inference(fof_nnf,[status(thm)],[ruleD39])).
% 95.50/95.72 fof(c287,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:~eqangle(A,B,P,Q,C,D,P,Q)))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c286])).
% 95.50/95.72 fof(c289,plain,(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)|para(X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c288,plain,(![X295]:(![X296]:(![X297]:(![X298]:((![X299]:(![X300]:~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)))|para(X295,X296,X297,X298)))))),inference(variable_rename,[status(thm)],[c287])).])).
% 95.50/95.72 cnf(c290,plain,~eqangle(X1061,X1063,X1062,X1059,X1060,X1064,X1062,X1059)|para(X1061,X1063,X1060,X1064),inference(split_conjunct,[status(thm)],[c289])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c350,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(C,D,A,B,U,V,P,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleD19])).
% 95.50/95.72 fof(c351,plain,(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(~eqangle(X441,X442,X443,X444,X445,X446,X447,X448)|eqangle(X443,X444,X441,X442,X447,X448,X445,X446)))))))))),inference(variable_rename,[status(thm)],[c350])).
% 95.50/95.72 cnf(c352,plain,~eqangle(X1223,X1220,X1221,X1227,X1225,X1226,X1222,X1224)|eqangle(X1221,X1227,X1223,X1220,X1222,X1224,X1225,X1226),inference(split_conjunct,[status(thm)],[c351])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c281,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~para(A,B,C,D)|eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD40])).
% 95.50/95.72 fof(c282,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|(![P]:(![Q]:eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(shift_quantors,[status(thm)],[c281])).
% 95.50/95.72 fof(c284,plain,(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(~para(X289,X290,X291,X292)|eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(shift_quantors,[status(thm)],[fof(c283,plain,(![X289]:(![X290]:(![X291]:(![X292]:(~para(X289,X290,X291,X292)|(![X293]:(![X294]:eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(variable_rename,[status(thm)],[c282])).])).
% 95.50/95.72 cnf(c285,plain,~para(X1056,X1058,X1054,X1055)|eqangle(X1056,X1058,X1057,X1053,X1054,X1055,X1057,X1053),inference(split_conjunct,[status(thm)],[c284])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 95.50/95.72 fof(c386,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c385])).
% 95.50/95.72 cnf(c387,plain,~perp(X704,X701,X702,X703)|perp(X702,X703,X704,X701),inference(split_conjunct,[status(thm)],[c386])).
% 95.50/95.72 cnf(c21,negated_conjecture,perp(skolem0007,skolem0006,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 95.50/95.72 fof(c389,plain,(![X502]:(![X503]:(![X504]:(![X505]:(~perp(X502,X503,X504,X505)|perp(X502,X503,X505,X504)))))),inference(variable_rename,[status(thm)],[c388])).
% 95.50/95.72 cnf(c390,plain,~perp(X714,X716,X713,X715)|perp(X714,X716,X715,X713),inference(split_conjunct,[status(thm)],[c389])).
% 95.50/95.72 cnf(c520,plain,perp(skolem0007,skolem0006,skolem0002,skolem0001),inference(resolution,[status(thm)],[c390, c21])).
% 95.50/95.72 cnf(c537,plain,perp(skolem0002,skolem0001,skolem0007,skolem0006),inference(resolution,[status(thm)],[c520, c387])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c382,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~perp(A,B,C,D)|~perp(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD9])).
% 95.50/95.72 fof(c383,plain,(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:((~perp(X492,X493,X494,X495)|~perp(X494,X495,X496,X497))|para(X492,X493,X496,X497)))))))),inference(variable_rename,[status(thm)],[c382])).
% 95.50/95.72 cnf(c384,plain,~perp(X1274,X1270,X1272,X1275)|~perp(X1272,X1275,X1271,X1273)|para(X1274,X1270,X1271,X1273),inference(split_conjunct,[status(thm)],[c383])).
% 95.50/95.72 cnf(c1479,plain,~perp(X2612,X2611,skolem0007,skolem0006)|para(X2612,X2611,skolem0002,skolem0001),inference(resolution,[status(thm)],[c384, c520])).
% 95.50/95.72 cnf(c5735,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1479, c537])).
% 95.50/95.72 cnf(c5756,plain,eqangle(skolem0002,skolem0001,X3525,X3524,skolem0002,skolem0001,X3525,X3524),inference(resolution,[status(thm)],[c5735, c285])).
% 95.50/95.72 cnf(c7879,plain,eqangle(X3625,X3624,skolem0002,skolem0001,X3625,X3624,skolem0002,skolem0001),inference(resolution,[status(thm)],[c5756, c352])).
% 95.50/95.72 cnf(c8319,plain,para(X3627,X3626,X3627,X3626),inference(resolution,[status(thm)],[c7879, c290])).
% 95.50/95.72 cnf(c8348,plain,coll(X3631,X3632,X3632),inference(resolution,[status(thm)],[c8319, c191])).
% 95.50/95.72 cnf(c8502,plain,coll(X3634,X3634,X3633),inference(resolution,[status(thm)],[c8348, c579])).
% 95.50/95.72 cnf(c8848,plain,~coll(X5312,X5312,X5311)|coll(X5311,X5313,X5312),inference(resolution,[status(thm)],[c8502, c402])).
% 95.50/95.72 cnf(c16021,plain,coll(X5319,X5320,X5321),inference(resolution,[status(thm)],[c8848, c8502])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c271,plain,(![A]:(![B]:(![P]:(![Q]:((~eqangle(P,A,P,B,Q,A,Q,B)|~coll(P,Q,B))|cyclic(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD42b])).
% 95.50/95.72 fof(c272,plain,(![X277]:(![X278]:(![X279]:(![X280]:((~eqangle(X279,X277,X279,X278,X280,X277,X280,X278)|~coll(X279,X280,X278))|cyclic(X277,X278,X279,X280)))))),inference(variable_rename,[status(thm)],[c271])).
% 95.50/95.72 cnf(c273,plain,~eqangle(X1043,X1044,X1043,X1042,X1041,X1044,X1041,X1042)|~coll(X1043,X1041,X1042)|cyclic(X1044,X1042,X1043,X1041),inference(split_conjunct,[status(thm)],[c272])).
% 95.50/95.72 cnf(c8375,plain,eqangle(X5091,X5090,X5092,X5089,X5091,X5090,X5092,X5089),inference(resolution,[status(thm)],[c8319, c285])).
% 95.50/95.72 cnf(c15881,plain,~coll(X5703,X5703,X5702)|cyclic(X5701,X5702,X5703,X5703),inference(resolution,[status(thm)],[c8375, c273])).
% 95.50/95.72 cnf(c16534,plain,cyclic(X5707,X5708,X5709,X5709),inference(resolution,[status(thm)],[c15881, c16021])).
% 95.50/95.72 cnf(c16539,plain,cyclic(X5717,X5718,X5716,X5718),inference(resolution,[status(thm)],[c16534, c364])).
% 95.50/95.72 cnf(c16543,plain,cyclic(X5721,X5720,X5720,X5719),inference(resolution,[status(thm)],[c16539, c367])).
% 95.50/95.72 cnf(c16554,plain,eqangle(X5784,X5785,X5784,X5784,X5786,X5785,X5786,X5784),inference(resolution,[status(thm)],[c16543, c280])).
% 95.50/95.72 cnf(c16602,plain,~eqangle(X42130,X42132,X42131,X42128,X42133,X42134,X42133,X42133)|eqangle(X42130,X42132,X42131,X42128,X42129,X42134,X42129,X42133),inference(resolution,[status(thm)],[c16554, c343])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c347,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(P,Q,U,V,A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD20])).
% 95.50/95.72 fof(c348,plain,(![X433]:(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(~eqangle(X433,X434,X435,X436,X437,X438,X439,X440)|eqangle(X437,X438,X439,X440,X433,X434,X435,X436)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 95.50/95.72 cnf(c349,plain,~eqangle(X1218,X1217,X1216,X1215,X1214,X1212,X1213,X1211)|eqangle(X1214,X1212,X1213,X1211,X1218,X1217,X1216,X1215),inference(split_conjunct,[status(thm)],[c348])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c353,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])).
% 95.50/95.72 fof(c354,plain,(![X449]:(![X450]:(![X451]:(![X452]:(![X453]:(![X454]:(![X455]:(![X456]:(~eqangle(X449,X450,X451,X452,X453,X454,X455,X456)|eqangle(X450,X449,X451,X452,X453,X454,X455,X456)))))))))),inference(variable_rename,[status(thm)],[c353])).
% 95.50/95.72 cnf(c355,plain,~eqangle(X1230,X1229,X1234,X1233,X1231,X1236,X1235,X1232)|eqangle(X1229,X1230,X1234,X1233,X1231,X1236,X1235,X1232),inference(split_conjunct,[status(thm)],[c354])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 95.50/95.72 fof(c398,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c397])).
% 95.50/95.72 cnf(c399,plain,~para(X769,X768,X771,X770)|para(X769,X768,X770,X771),inference(split_conjunct,[status(thm)],[c398])).
% 95.50/95.72 cnf(c8363,plain,para(X3650,X3651,X3651,X3650),inference(resolution,[status(thm)],[c8319, c399])).
% 95.50/95.72 cnf(c9544,plain,eqangle(X5480,X5481,X5482,X5479,X5481,X5480,X5482,X5479),inference(resolution,[status(thm)],[c8363, c285])).
% 95.50/95.72 cnf(c16437,plain,eqangle(X5508,X5507,X5509,X5506,X5508,X5507,X5506,X5509),inference(resolution,[status(thm)],[c9544, c352])).
% 95.50/95.72 cnf(c16471,plain,eqangle(X5562,X5561,X5564,X5563,X5561,X5562,X5563,X5564),inference(resolution,[status(thm)],[c16437, c355])).
% 95.50/95.72 cnf(c16511,plain,~eqangle(X34174,X34175,X34178,X34172,X34179,X34176,X34177,X34173)|eqangle(X34174,X34175,X34178,X34172,X34176,X34179,X34173,X34177),inference(resolution,[status(thm)],[c16471, c343])).
% 95.50/95.72 cnf(c16546,plain,eqangle(X5779,X5780,X5779,X5781,X5781,X5780,X5781,X5781),inference(resolution,[status(thm)],[c16539, c280])).
% 95.50/95.72 cnf(c16588,plain,~eqangle(X34748,X34749,X34751,X34747,X34752,X34753,X34752,X34750)|eqangle(X34748,X34749,X34751,X34747,X34750,X34753,X34750,X34750),inference(resolution,[status(thm)],[c16546, c343])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c359,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 95.50/95.72 fof(c360,plain,(![X462]:(![X463]:(![X464]:(![X465]:(~cyclic(X462,X463,X464,X465)|cyclic(X463,X462,X464,X465)))))),inference(variable_rename,[status(thm)],[c359])).
% 95.50/95.72 cnf(c361,plain,~cyclic(X692,X690,X691,X689)|cyclic(X690,X692,X691,X689),inference(split_conjunct,[status(thm)],[c360])).
% 95.50/95.72 cnf(c16553,plain,cyclic(X5736,X5734,X5736,X5735),inference(resolution,[status(thm)],[c16543, c361])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c356,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])).
% 95.50/95.72 fof(c357,plain,(![X457]:(![X458]:(![X459]:(![X460]:(![X461]:((~cyclic(X457,X458,X459,X460)|~cyclic(X457,X458,X459,X461))|cyclic(X458,X459,X460,X461))))))),inference(variable_rename,[status(thm)],[c356])).
% 95.50/95.72 cnf(c358,plain,~cyclic(X1239,X1241,X1240,X1238)|~cyclic(X1239,X1241,X1240,X1242)|cyclic(X1241,X1240,X1238,X1242),inference(split_conjunct,[status(thm)],[c357])).
% 95.50/95.72 cnf(c16574,plain,~cyclic(X13207,X13206,X13207,X13208)|cyclic(X13206,X13207,X13208,X13209),inference(resolution,[status(thm)],[c16553, c358])).
% 95.50/95.72 cnf(c24995,plain,cyclic(X13231,X13234,X13233,X13232),inference(resolution,[status(thm)],[c16574, c16553])).
% 95.50/95.72 fof(ruleD54,axiom,(![A]:(![B]:(![C]:(![D]:((cyclic(A,B,C,D)¶(A,B,C,D))=>eqangle(A,D,C,D,C,D,C,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD54)).
% 95.50/95.72 fof(c230,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])).
% 95.50/95.72 fof(c231,plain,(![X223]:(![X224]:(![X225]:(![X226]:((~cyclic(X223,X224,X225,X226)|~para(X223,X224,X225,X226))|eqangle(X223,X226,X225,X226,X225,X226,X225,X224)))))),inference(variable_rename,[status(thm)],[c230])).
% 95.50/95.72 cnf(c232,plain,~cyclic(X987,X989,X990,X988)|~para(X987,X989,X990,X988)|eqangle(X987,X988,X990,X988,X990,X988,X990,X989),inference(split_conjunct,[status(thm)],[c231])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c186,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 95.50/95.72 fof(c187,plain,(![X160]:(![X161]:(![X162]:((~cong(X160,X161,X160,X162)|~coll(X160,X161,X162))|midp(X160,X161,X162))))),inference(variable_rename,[status(thm)],[c186])).
% 95.50/95.72 cnf(c188,plain,~cong(X934,X935,X934,X933)|~coll(X934,X935,X933)|midp(X934,X935,X933),inference(split_conjunct,[status(thm)],[c187])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 95.50/95.72 fof(c339,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c338])).
% 95.50/95.72 cnf(c340,plain,~cong(X687,X686,X685,X688)|cong(X687,X686,X688,X685),inference(split_conjunct,[status(thm)],[c339])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 95.50/95.72 fof(c336,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c335])).
% 95.50/95.72 cnf(c337,plain,~cong(X679,X680,X681,X678)|cong(X681,X678,X679,X680),inference(split_conjunct,[status(thm)],[c336])).
% 95.50/95.72 fof(ruleD64,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(((midp(M,A,B)¶(A,C,B,D))¶(A,D,B,C))=>midp(M,C,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 95.50/95.72 fof(c195,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C))|midp(M,C,D))))))),inference(fof_nnf,[status(thm)],[ruleD64])).
% 95.50/95.72 fof(c196,plain,(![X171]:(![X172]:(![X173]:(![X174]:(![X175]:(((~midp(X175,X171,X172)|~para(X171,X173,X172,X174))|~para(X171,X174,X172,X173))|midp(X175,X173,X174))))))),inference(variable_rename,[status(thm)],[c195])).
% 95.50/95.72 cnf(c197,plain,~midp(X945,X943,X944)|~para(X943,X942,X944,X941)|~para(X943,X941,X944,X942)|midp(X945,X942,X941),inference(split_conjunct,[status(thm)],[c196])).
% 95.50/95.72 cnf(c1251,plain,~midp(X2344,X2345,X2347)|~para(X2345,X2346,X2347,X2346)|midp(X2344,X2346,X2346),inference(factor,[status(thm)],[c197])).
% 95.50/95.72 cnf(c8338,plain,~midp(X5075,X5074,X5074)|midp(X5075,X5076,X5076),inference(resolution,[status(thm)],[c8319, c1251])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c266,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q))|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD43])).
% 95.50/95.72 fof(c267,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:((![R]:(((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q)))|cong(A,B,P,Q))))))),inference(shift_quantors,[status(thm)],[c266])).
% 95.50/95.72 fof(c269,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275))|cong(X271,X272,X274,X275)))))))),inference(shift_quantors,[status(thm)],[fof(c268,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((![X276]:(((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275)))|cong(X271,X272,X274,X275))))))),inference(variable_rename,[status(thm)],[c267])).])).
% 95.50/95.72 cnf(c270,plain,~cyclic(X1036,X1035,X1037,X1039)|~cyclic(X1036,X1035,X1037,X1038)|~cyclic(X1036,X1035,X1037,X1040)|~eqangle(X1037,X1036,X1037,X1035,X1040,X1039,X1040,X1038)|cong(X1036,X1035,X1039,X1038),inference(split_conjunct,[status(thm)],[c269])).
% 95.50/95.72 cnf(c16466,plain,eqangle(X5556,X5558,X5556,X5558,X5555,X5557,X5557,X5555),inference(resolution,[status(thm)],[c16437, c346])).
% 95.50/95.72 cnf(c16496,plain,~cyclic(X6688,X6688,X6686,X6687)|cong(X6688,X6688,X6687,X6687),inference(resolution,[status(thm)],[c16466, c270])).
% 95.50/95.72 cnf(c17059,plain,cong(X6689,X6689,X6690,X6690),inference(resolution,[status(thm)],[c16496, c16534])).
% 95.50/95.72 cnf(c17077,plain,~coll(X6744,X6744,X6744)|midp(X6744,X6744,X6744),inference(resolution,[status(thm)],[c17059, c188])).
% 95.50/95.72 cnf(c17195,plain,midp(X6745,X6745,X6745),inference(resolution,[status(thm)],[c17077, c16021])).
% 95.50/95.72 cnf(c17411,plain,midp(X6750,X6751,X6751),inference(resolution,[status(thm)],[c17195, c8338])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c238,plain,(![A]:(![B]:(![C]:(![M]:((~perp(A,B,B,C)|~midp(M,A,C))|cong(A,M,B,M)))))),inference(fof_nnf,[status(thm)],[ruleD52])).
% 95.50/95.72 fof(c239,plain,(![X231]:(![X232]:(![X233]:(![X234]:((~perp(X231,X232,X232,X233)|~midp(X234,X231,X233))|cong(X231,X234,X232,X234)))))),inference(variable_rename,[status(thm)],[c238])).
% 95.50/95.72 cnf(c240,plain,~perp(X995,X998,X998,X997)|~midp(X996,X995,X997)|cong(X995,X996,X998,X996),inference(split_conjunct,[status(thm)],[c239])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c159,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 95.50/95.72 fof(c160,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))))))|perp(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c159])).
% 95.50/95.72 fof(c162,plain,(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:((~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))|perp(X124,X125,X126,X127)))))))))),inference(shift_quantors,[status(thm)],[fof(c161,plain,(![X124]:(![X125]:(![X126]:(![X127]:((![X128]:(![X129]:(![X130]:(![X131]:(~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))))))|perp(X124,X125,X126,X127)))))),inference(variable_rename,[status(thm)],[c160])).])).
% 95.50/95.72 cnf(c163,plain,~eqangle(X904,X908,X909,X907,X903,X905,X910,X906)|~perp(X903,X905,X910,X906)|perp(X904,X908,X909,X907),inference(split_conjunct,[status(thm)],[c162])).
% 95.50/95.72 cnf(c16438,plain,eqangle(X5518,X5516,X5516,X5518,X5517,X5515,X5517,X5515),inference(resolution,[status(thm)],[c9544, c346])).
% 95.50/95.72 cnf(c16486,plain,~perp(X6671,X6674,X6671,X6674)|perp(X6673,X6672,X6672,X6673),inference(resolution,[status(thm)],[c16438, c163])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c224,plain,(![A]:(![B]:(![P]:(![Q]:((~cong(A,P,B,P)|~cong(A,Q,B,Q))|perp(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD56])).
% 95.50/95.72 fof(c225,plain,(![X215]:(![X216]:(![X217]:(![X218]:((~cong(X215,X217,X216,X217)|~cong(X215,X218,X216,X218))|perp(X215,X216,X217,X218)))))),inference(variable_rename,[status(thm)],[c224])).
% 95.50/95.72 cnf(c226,plain,~cong(X979,X981,X982,X981)|~cong(X979,X980,X982,X980)|perp(X979,X982,X981,X980),inference(split_conjunct,[status(thm)],[c225])).
% 95.50/95.72 cnf(c1320,plain,~cong(X1127,X1125,X1126,X1125)|perp(X1127,X1126,X1125,X1125),inference(factor,[status(thm)],[c226])).
% 95.50/95.72 cnf(c17071,plain,perp(X6709,X6709,X6709,X6709),inference(resolution,[status(thm)],[c17059, c1320])).
% 95.50/95.72 cnf(c17087,plain,perp(X6713,X6712,X6712,X6713),inference(resolution,[status(thm)],[c17071, c16486])).
% 95.50/95.72 cnf(c17125,plain,~midp(X7704,X7706,X7706)|cong(X7706,X7704,X7705,X7704),inference(resolution,[status(thm)],[c17087, c240])).
% 95.50/95.72 cnf(c19602,plain,cong(X7709,X7707,X7708,X7707),inference(resolution,[status(thm)],[c17125, c17411])).
% 95.50/95.72 cnf(c19604,plain,cong(X7712,X7711,X7711,X7710),inference(resolution,[status(thm)],[c19602, c340])).
% 95.50/95.72 cnf(c19620,plain,cong(X7729,X7728,X7727,X7729),inference(resolution,[status(thm)],[c19604, c337])).
% 95.50/95.72 cnf(c19644,plain,cong(X7747,X7746,X7747,X7748),inference(resolution,[status(thm)],[c19620, c340])).
% 95.50/95.72 cnf(c19706,plain,~coll(X8035,X8037,X8036)|midp(X8035,X8037,X8036),inference(resolution,[status(thm)],[c19644, c188])).
% 95.50/95.72 cnf(c20923,plain,midp(X8038,X8040,X8039),inference(resolution,[status(thm)],[c19706, c16021])).
% 95.50/95.72 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)).
% 95.50/95.72 fof(c263,plain,(![A]:(![B]:(![C]:(![E]:(![F]:((~midp(E,A,B)|~midp(F,A,C))|para(E,F,B,C))))))),inference(fof_nnf,[status(thm)],[ruleD44])).
% 95.50/95.72 fof(c264,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c263])).
% 95.50/95.72 cnf(c265,plain,~midp(X1031,X1033,X1034)|~midp(X1032,X1033,X1030)|para(X1031,X1032,X1034,X1030),inference(split_conjunct,[status(thm)],[c264])).
% 95.50/95.72 cnf(c17443,plain,~midp(X11931,X11929,X11930)|para(X11931,X11932,X11930,X11929),inference(resolution,[status(thm)],[c17411, c265])).
% 95.50/95.72 cnf(c24403,plain,para(X11934,X11933,X11935,X11936),inference(resolution,[status(thm)],[c17443, c20923])).
% 95.50/95.72 cnf(c24407,plain,~cyclic(X27403,X27402,X27404,X27405)|eqangle(X27403,X27405,X27404,X27405,X27404,X27405,X27404,X27402),inference(resolution,[status(thm)],[c24403, c232])).
% 95.50/95.72 cnf(c27473,plain,eqangle(X27407,X27408,X27406,X27408,X27406,X27408,X27406,X27409),inference(resolution,[status(thm)],[c24407, c24995])).
% 95.50/95.72 cnf(c27474,plain,eqangle(X27411,X27413,X27412,X27413,X27411,X27410,X27411,X27413),inference(resolution,[status(thm)],[c27473, c352])).
% 95.50/95.72 cnf(c27483,plain,eqangle(X27436,X27435,X27437,X27436,X27435,X27434,X27435,X27436),inference(resolution,[status(thm)],[c27474, c355])).
% 95.50/95.72 cnf(c27498,plain,eqangle(X27480,X27481,X27481,X27482,X27482,X27481,X27482,X27483),inference(resolution,[status(thm)],[c27483, c352])).
% 95.50/95.72 cnf(c27531,plain,eqangle(X27573,X27572,X27573,X27574,X27574,X27573,X27574,X27575),inference(resolution,[status(thm)],[c27498, c355])).
% 95.50/95.72 cnf(c28030,plain,eqangle(X34975,X34977,X34975,X34976,X34978,X34975,X34978,X34978),inference(resolution,[status(thm)],[c16588, c27531])).
% 95.50/95.72 cnf(c28140,plain,eqangle(X35419,X35418,X35419,X35419,X35418,X35421,X35418,X35420),inference(resolution,[status(thm)],[c28030, c349])).
% 95.50/95.72 cnf(c28416,plain,eqangle(X36420,X36421,X36420,X36420,X36418,X36419,X36418,X36418),inference(resolution,[status(thm)],[c28140, c16588])).
% 95.50/95.72 cnf(c30081,plain,eqangle(X42150,X42149,X42150,X42150,X42152,X42148,X42152,X42151),inference(resolution,[status(thm)],[c16602, c28416])).
% 95.50/95.72 cnf(c30262,plain,eqangle(X42995,X42994,X42995,X42995,X42997,X42996,X42993,X42996),inference(resolution,[status(thm)],[c30081, c16511])).
% 95.50/95.72 cnf(c30424,plain,eqangle(X43600,X43603,X43604,X43603,X43601,X43602,X43601,X43601),inference(resolution,[status(thm)],[c30262, c349])).
% 95.50/95.72 cnf(c31037,plain,eqangle(X46323,X46322,X46324,X46322,X46325,X46327,X46325,X46326),inference(resolution,[status(thm)],[c30424, c16602])).
% 95.50/95.72 cnf(c31654,plain,eqangle(X48909,X48911,X48907,X48910,X48912,X48911,X48907,X48908),inference(resolution,[status(thm)],[c31037, c346])).
% 95.50/95.72 cnf(c31913,plain,$false,inference(resolution,[status(thm)],[c31654, c23])).
% 95.50/95.72 % SZS output end CNFRefutation
% 95.50/95.72
% 95.50/95.72 % Initial clauses : 136
% 95.50/95.72 % Processed clauses : 3809
% 95.50/95.72 % Factors computed : 346
% 95.50/95.72 % Resolvents computed: 31161
% 95.50/95.72 % Tautologies deleted: 90
% 95.50/95.72 % Forward subsumed : 18364
% 95.50/95.72 % Backward subsumed : 3631
% 95.50/95.72 % -------- CPU Time ---------
% 95.50/95.72 % User time : 95.301 s
% 95.50/95.72 % System time : 0.062 s
% 95.50/95.72 % Total time : 95.363 s
%------------------------------------------------------------------------------