%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO604+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:23 EDT 2024
% Result : Theorem 150.92s 151.13s
% Output : Refutation 150.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO604+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/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:00:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 150.92/151.13 % Version: 1.5
% 150.92/151.13 % SZS status Theorem
% 150.92/151.13 % SZS output start CNFRefutation
% 150.92/151.13 fof(exemplo6GDDFULL618066,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:((((((perp(D,C,A,B)&coll(D,A,B))&perp(B,C,A,E))&coll(E,C,D))&midp(F,A,E))&midp(G,C,B))=>perp(D,G,D,F))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL618066)).
% 150.92/151.13 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:((((((perp(D,C,A,B)&coll(D,A,B))&perp(B,C,A,E))&coll(E,C,D))&midp(F,A,E))&midp(G,C,B))=>perp(D,G,D,F)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618066])).
% 150.92/151.13 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:((((((perp(D,C,A,B)&coll(D,A,B))&perp(B,C,A,E))&coll(E,C,D))&midp(F,A,E))&midp(G,C,B))&~perp(D,G,D,F))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 150.92/151.13 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((perp(X5,X4,X2,X3)&coll(X5,X2,X3))&perp(X3,X4,X2,X6))&coll(X6,X4,X5))&midp(X7,X2,X6))&midp(X8,X4,X3))&~perp(X5,X8,X5,X7))))))))),inference(variable_rename,[status(thm)],[c12])).
% 150.92/151.13 fof(c14,negated_conjecture,((((((perp(skolem0004,skolem0003,skolem0001,skolem0002)&coll(skolem0004,skolem0001,skolem0002))&perp(skolem0002,skolem0003,skolem0001,skolem0005))&coll(skolem0005,skolem0003,skolem0004))&midp(skolem0006,skolem0001,skolem0005))&midp(skolem0007,skolem0003,skolem0002))&~perp(skolem0004,skolem0007,skolem0004,skolem0006)),inference(skolemize,[status(esa)],[c13])).
% 150.92/151.13 cnf(c21,negated_conjecture,~perp(skolem0004,skolem0007,skolem0004,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 150.92/151.13 fof(ruleD56,axiom,(![A]:(![B]:(![P]:(![Q]:((cong(A,P,B,P)&cong(A,Q,B,Q))=>perp(A,B,P,Q)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 150.92/151.13 fof(c222,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])).
% 150.92/151.13 fof(c223,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)],[c222])).
% 150.92/151.13 cnf(c224,plain,~cong(X982,X981,X980,X981)|~cong(X982,X979,X980,X979)|perp(X982,X980,X981,X979),inference(split_conjunct,[status(thm)],[c223])).
% 150.92/151.13 cnf(c1272,plain,~cong(X1114,X1115,X1113,X1115)|perp(X1114,X1113,X1115,X1115),inference(factor,[status(thm)],[c224])).
% 150.92/151.13 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 150.92/151.13 fof(c236,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])).
% 150.92/151.13 fof(c237,plain,(![X231]:(![X232]:(![X233]:(![X234]:((~perp(X231,X232,X232,X233)|~midp(X234,X231,X233))|cong(X231,X234,X232,X234)))))),inference(variable_rename,[status(thm)],[c236])).
% 150.92/151.13 cnf(c238,plain,~perp(X998,X997,X997,X996)|~midp(X995,X998,X996)|cong(X998,X995,X997,X995),inference(split_conjunct,[status(thm)],[c237])).
% 150.92/151.13 fof(ruleD74,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((eqangle(A,B,C,D,P,Q,U,V)&perp(P,Q,U,V))=>perp(A,B,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 150.92/151.13 fof(c157,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])).
% 150.92/151.13 fof(c158,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)],[c157])).
% 150.92/151.13 fof(c160,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(c159,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)],[c158])).])).
% 150.92/151.13 cnf(c161,plain,~eqangle(X908,X906,X905,X904,X907,X909,X903,X910)|~perp(X907,X909,X903,X910)|perp(X908,X906,X905,X904),inference(split_conjunct,[status(thm)],[c160])).
% 150.92/151.13 fof(ruleD40,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(para(A,B,C,D)=>eqangle(A,B,P,Q,C,D,P,Q)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 150.92/151.13 fof(c279,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])).
% 150.92/151.13 fof(c280,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)],[c279])).
% 150.92/151.13 fof(c282,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(c281,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)],[c280])).])).
% 150.92/151.13 cnf(c283,plain,~para(X1058,X1053,X1055,X1056)|eqangle(X1058,X1053,X1057,X1054,X1055,X1056,X1057,X1054),inference(split_conjunct,[status(thm)],[c282])).
% 150.92/151.13 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 150.92/151.13 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 150.92/151.13 fof(c396,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c395])).
% 150.92/151.13 cnf(c397,plain,~para(X786,X787,X785,X784)|para(X786,X787,X784,X785),inference(split_conjunct,[status(thm)],[c396])).
% 150.92/151.13 fof(ruleD39,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(eqangle(A,B,P,Q,C,D,P,Q)=>para(A,B,C,D)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 150.92/151.13 fof(c284,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])).
% 150.92/151.13 fof(c285,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)],[c284])).
% 150.92/151.13 fof(c287,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(c286,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)],[c285])).])).
% 150.92/151.13 cnf(c288,plain,~eqangle(X1061,X1062,X1063,X1059,X1064,X1060,X1063,X1059)|para(X1061,X1062,X1064,X1060),inference(split_conjunct,[status(thm)],[c287])).
% 150.92/151.13 fof(ruleD19,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(C,D,A,B,U,V,P,Q)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 150.92/151.13 fof(c348,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])).
% 150.92/151.13 fof(c349,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)],[c348])).
% 150.92/151.13 cnf(c350,plain,~eqangle(X1224,X1218,X1219,X1220,X1223,X1217,X1221,X1222)|eqangle(X1219,X1220,X1224,X1218,X1221,X1222,X1223,X1217),inference(split_conjunct,[status(thm)],[c349])).
% 150.92/151.13 cnf(c20,negated_conjecture,midp(skolem0007,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 150.92/151.13 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 150.92/151.13 fof(c374,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 150.92/151.13 fof(c375,plain,(![X483]:(![X484]:(![X485]:(~midp(X485,X484,X483)|midp(X485,X483,X484))))),inference(variable_rename,[status(thm)],[c374])).
% 150.92/151.13 cnf(c376,plain,~midp(X558,X559,X557)|midp(X558,X557,X559),inference(split_conjunct,[status(thm)],[c375])).
% 150.92/151.13 cnf(c416,plain,midp(skolem0007,skolem0002,skolem0003),inference(resolution,[status(thm)],[c376, c20])).
% 150.92/151.13 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 150.92/151.13 fof(c196,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])).
% 150.92/151.13 fof(c197,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c196])).
% 150.92/151.13 fof(c199,plain,(![X176]:(![X177]:(![X178]:(![X179]:(![X180]:((~midp(X180,X176,X177)|~midp(X180,X178,X179))|para(X176,X178,X177,X179))))))),inference(shift_quantors,[status(thm)],[fof(c198,plain,(![X176]:(![X177]:(![X178]:(![X179]:((![X180]:(~midp(X180,X176,X177)|~midp(X180,X178,X179)))|para(X176,X178,X177,X179)))))),inference(variable_rename,[status(thm)],[c197])).])).
% 150.92/151.13 cnf(c200,plain,~midp(X947,X948,X950)|~midp(X947,X949,X946)|para(X948,X949,X950,X946),inference(split_conjunct,[status(thm)],[c199])).
% 150.92/151.13 cnf(c1213,plain,~midp(skolem0007,X2031,X2030)|para(X2031,skolem0002,X2030,skolem0003),inference(resolution,[status(thm)],[c200, c416])).
% 150.92/151.13 cnf(c4649,plain,para(skolem0003,skolem0002,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1213, c20])).
% 150.92/151.13 cnf(c4661,plain,para(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c4649, c397])).
% 150.92/151.13 cnf(c4692,plain,eqangle(skolem0003,skolem0002,X3872,X3871,skolem0003,skolem0002,X3872,X3871),inference(resolution,[status(thm)],[c4661, c283])).
% 150.92/151.13 cnf(c12035,plain,eqangle(X4914,X4913,skolem0003,skolem0002,X4914,X4913,skolem0003,skolem0002),inference(resolution,[status(thm)],[c4692, c350])).
% 150.92/151.13 cnf(c18081,plain,para(X4916,X4915,X4916,X4915),inference(resolution,[status(thm)],[c12035, c288])).
% 150.92/151.13 cnf(c18103,plain,para(X4940,X4941,X4941,X4940),inference(resolution,[status(thm)],[c18081, c397])).
% 150.92/151.13 cnf(c19535,plain,eqangle(X6997,X6998,X6996,X6995,X6998,X6997,X6996,X6995),inference(resolution,[status(thm)],[c18103, c283])).
% 150.92/151.13 cnf(c29297,plain,~perp(X9113,X9116,X9115,X9114)|perp(X9116,X9113,X9115,X9114),inference(resolution,[status(thm)],[c19535, c161])).
% 150.92/151.13 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 150.92/151.13 fof(c383,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 150.92/151.13 fof(c384,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c383])).
% 150.92/151.13 cnf(c385,plain,~perp(X742,X743,X740,X741)|perp(X740,X741,X742,X743),inference(split_conjunct,[status(thm)],[c384])).
% 150.92/151.13 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 150.92/151.13 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 150.92/151.13 fof(c337,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c336])).
% 150.92/151.13 cnf(c338,plain,~cong(X691,X688,X690,X689)|cong(X691,X688,X689,X690),inference(split_conjunct,[status(thm)],[c337])).
% 150.92/151.13 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 150.92/151.13 fof(c333,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 150.92/151.13 fof(c334,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c333])).
% 150.92/151.13 cnf(c335,plain,~cong(X682,X681,X684,X683)|cong(X684,X683,X682,X681),inference(split_conjunct,[status(thm)],[c334])).
% 150.92/151.13 cnf(c19,negated_conjecture,midp(skolem0006,skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 150.92/151.13 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 150.92/151.13 fof(c181,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 150.92/151.13 fof(c182,plain,(![X157]:(![X158]:(![X159]:(~midp(X157,X158,X159)|cong(X157,X158,X157,X159))))),inference(variable_rename,[status(thm)],[c181])).
% 150.92/151.13 cnf(c183,plain,~midp(X673,X672,X674)|cong(X673,X672,X673,X674),inference(split_conjunct,[status(thm)],[c182])).
% 150.92/151.13 cnf(c499,plain,cong(skolem0006,skolem0001,skolem0006,skolem0005),inference(resolution,[status(thm)],[c183, c19])).
% 150.92/151.13 cnf(c510,plain,cong(skolem0006,skolem0001,skolem0005,skolem0006),inference(resolution,[status(thm)],[c338, c499])).
% 150.92/151.13 cnf(c521,plain,cong(skolem0005,skolem0006,skolem0006,skolem0001),inference(resolution,[status(thm)],[c510, c335])).
% 150.92/151.13 cnf(c531,plain,cong(skolem0005,skolem0006,skolem0001,skolem0006),inference(resolution,[status(thm)],[c521, c338])).
% 150.92/151.13 cnf(c1470,plain,perp(skolem0005,skolem0001,skolem0006,skolem0006),inference(resolution,[status(thm)],[c1272, c531])).
% 150.92/151.13 cnf(c1490,plain,perp(skolem0006,skolem0006,skolem0005,skolem0001),inference(resolution,[status(thm)],[c1470, c385])).
% 150.92/151.13 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 150.92/151.13 fof(c377,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])).
% 150.92/151.13 fof(c378,plain,(![X486]:(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:((~para(X486,X487,X488,X489)|~perp(X488,X489,X490,X491))|perp(X486,X487,X490,X491)))))))),inference(variable_rename,[status(thm)],[c377])).
% 150.92/151.13 cnf(c379,plain,~para(X1264,X1261,X1262,X1263)|~perp(X1262,X1263,X1260,X1259)|perp(X1264,X1261,X1260,X1259),inference(split_conjunct,[status(thm)],[c378])).
% 150.92/151.13 cnf(c1624,plain,~para(X2929,X2928,skolem0006,skolem0006)|perp(X2929,X2928,skolem0005,skolem0001),inference(resolution,[status(thm)],[c379, c1490])).
% 150.92/151.13 fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 150.92/151.13 fof(c392,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 150.92/151.13 fof(c393,plain,(![X512]:(![X513]:(![X514]:(![X515]:(~para(X512,X513,X514,X515)|para(X514,X515,X512,X513)))))),inference(variable_rename,[status(thm)],[c392])).
% 150.92/151.13 cnf(c394,plain,~para(X778,X779,X777,X776)|para(X777,X776,X778,X779),inference(split_conjunct,[status(thm)],[c393])).
% 150.92/151.13 cnf(c417,plain,midp(skolem0006,skolem0005,skolem0001),inference(resolution,[status(thm)],[c376, c19])).
% 150.92/151.13 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 150.92/151.13 fof(c261,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])).
% 150.92/151.13 fof(c262,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c261])).
% 150.92/151.13 cnf(c263,plain,~midp(X1031,X1034,X1030)|~midp(X1032,X1034,X1033)|para(X1031,X1032,X1030,X1033),inference(split_conjunct,[status(thm)],[c262])).
% 150.92/151.13 cnf(c1297,plain,~midp(X1085,X1084,X1083)|para(X1085,X1085,X1083,X1083),inference(factor,[status(thm)],[c263])).
% 150.92/151.13 cnf(c1361,plain,para(skolem0006,skolem0006,skolem0001,skolem0001),inference(resolution,[status(thm)],[c1297, c417])).
% 150.92/151.13 cnf(c1389,plain,para(skolem0001,skolem0001,skolem0006,skolem0006),inference(resolution,[status(thm)],[c1361, c394])).
% 150.92/151.13 fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)¶(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 150.92/151.13 fof(c389,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])).
% 150.92/151.13 fof(c390,plain,(![X506]:(![X507]:(![X508]:(![X509]:(![X510]:(![X511]:((~para(X506,X507,X508,X509)|~para(X508,X509,X510,X511))|para(X506,X507,X510,X511)))))))),inference(variable_rename,[status(thm)],[c389])).
% 150.92/151.13 cnf(c391,plain,~para(X1278,X1280,X1276,X1275)|~para(X1276,X1275,X1279,X1277)|para(X1278,X1280,X1279,X1277),inference(split_conjunct,[status(thm)],[c390])).
% 150.92/151.13 cnf(c1693,plain,~para(X3042,X3041,skolem0001,skolem0001)|para(X3042,X3041,skolem0006,skolem0006),inference(resolution,[status(thm)],[c391, c1389])).
% 150.92/151.13 cnf(c498,plain,cong(skolem0006,skolem0005,skolem0006,skolem0001),inference(resolution,[status(thm)],[c183, c417])).
% 150.92/151.13 fof(ruleD25,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((cong(A,B,C,D)&cong(C,D,E,F))=>cong(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 150.92/151.13 fof(c330,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])).
% 150.92/151.13 fof(c331,plain,(![X399]:(![X400]:(![X401]:(![X402]:(![X403]:(![X404]:((~cong(X399,X400,X401,X402)|~cong(X401,X402,X403,X404))|cong(X399,X400,X403,X404)))))))),inference(variable_rename,[status(thm)],[c330])).
% 150.92/151.13 cnf(c332,plain,~cong(X1181,X1180,X1176,X1177)|~cong(X1176,X1177,X1178,X1179)|cong(X1181,X1180,X1178,X1179),inference(split_conjunct,[status(thm)],[c331])).
% 150.92/151.13 cnf(c1550,plain,~cong(X2851,X2850,skolem0006,skolem0005)|cong(X2851,X2850,skolem0006,skolem0001),inference(resolution,[status(thm)],[c332, c498])).
% 150.92/151.13 cnf(c7054,plain,cong(skolem0006,skolem0001,skolem0006,skolem0001),inference(resolution,[status(thm)],[c1550, c499])).
% 150.92/151.13 cnf(c7069,plain,perp(skolem0006,skolem0006,skolem0001,skolem0001),inference(resolution,[status(thm)],[c7054, c1272])).
% 150.92/151.13 cnf(c7089,plain,perp(skolem0001,skolem0001,skolem0006,skolem0006),inference(resolution,[status(thm)],[c7069, c385])).
% 150.92/151.13 fof(ruleD9,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((perp(A,B,C,D)&perp(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 150.92/151.13 fof(c380,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])).
% 150.92/151.13 fof(c381,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)],[c380])).
% 150.92/151.13 cnf(c382,plain,~perp(X1270,X1269,X1271,X1268)|~perp(X1271,X1268,X1266,X1267)|para(X1270,X1269,X1266,X1267),inference(split_conjunct,[status(thm)],[c381])).
% 150.92/151.13 cnf(c1664,plain,~perp(X2991,X2992,skolem0006,skolem0006)|para(X2991,X2992,skolem0005,skolem0001),inference(resolution,[status(thm)],[c382, c1490])).
% 150.92/151.13 cnf(c8445,plain,para(skolem0001,skolem0001,skolem0005,skolem0001),inference(resolution,[status(thm)],[c1664, c7089])).
% 150.92/151.13 cnf(c8837,plain,para(skolem0005,skolem0001,skolem0001,skolem0001),inference(resolution,[status(thm)],[c8445, c394])).
% 150.92/151.13 cnf(c9381,plain,para(skolem0005,skolem0001,skolem0006,skolem0006),inference(resolution,[status(thm)],[c8837, c1693])).
% 150.92/151.13 cnf(c9951,plain,perp(skolem0005,skolem0001,skolem0005,skolem0001),inference(resolution,[status(thm)],[c9381, c1624])).
% 150.92/151.13 fof(ruleD21,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(A,B,P,Q,C,D,U,V)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 150.92/151.13 fof(c342,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])).
% 150.92/151.13 fof(c343,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)],[c342])).
% 150.92/151.13 cnf(c344,plain,~eqangle(X1201,X1203,X1200,X1205,X1202,X1204,X1198,X1199)|eqangle(X1201,X1203,X1202,X1204,X1200,X1205,X1198,X1199),inference(split_conjunct,[status(thm)],[c343])).
% 150.92/151.13 cnf(c18132,plain,eqangle(X6605,X6604,X6603,X6602,X6605,X6604,X6603,X6602),inference(resolution,[status(thm)],[c18081, c283])).
% 150.92/151.13 cnf(c28622,plain,eqangle(X7234,X7235,X7234,X7235,X7236,X7237,X7236,X7237),inference(resolution,[status(thm)],[c18132, c344])).
% 150.92/151.13 cnf(c29404,plain,~perp(X9381,X9379,X9381,X9379)|perp(X9380,X9382,X9380,X9382),inference(resolution,[status(thm)],[c28622, c161])).
% 150.92/151.13 cnf(c32099,plain,perp(X9383,X9384,X9383,X9384),inference(resolution,[status(thm)],[c29404, c9951])).
% 150.92/151.13 cnf(c32131,plain,perp(X9453,X9454,X9454,X9453),inference(resolution,[status(thm)],[c32099, c29297])).
% 150.92/151.13 cnf(c32183,plain,~midp(X9662,X9663,X9663)|cong(X9663,X9662,X9664,X9662),inference(resolution,[status(thm)],[c32131, c238])).
% 150.92/151.13 fof(ruleD64,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(((midp(M,A,B)¶(A,C,B,D))¶(A,D,B,C))=>midp(M,C,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 150.92/151.13 fof(c193,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])).
% 150.92/151.13 fof(c194,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)],[c193])).
% 150.92/151.13 cnf(c195,plain,~midp(X941,X945,X944)|~para(X945,X942,X944,X943)|~para(X945,X943,X944,X942)|midp(X941,X942,X943),inference(split_conjunct,[status(thm)],[c194])).
% 150.92/151.13 cnf(c1199,plain,~midp(X2392,X2394,X2391)|~para(X2394,X2393,X2391,X2393)|midp(X2392,X2393,X2393),inference(factor,[status(thm)],[c195])).
% 150.92/151.13 cnf(c18117,plain,~midp(X6260,X6259,X6259)|midp(X6260,X6258,X6258),inference(resolution,[status(thm)],[c18081, c1199])).
% 150.92/151.13 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 150.92/151.13 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 150.92/151.13 fof(c399,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c398])).
% 150.92/151.13 cnf(c400,plain,~coll(X797,X794,X796)|~coll(X797,X794,X795)|coll(X796,X795,X797),inference(split_conjunct,[status(thm)],[c399])).
% 150.92/151.13 cnf(c683,plain,~coll(X799,X800,X798)|coll(X798,X798,X799),inference(factor,[status(thm)],[c400])).
% 150.92/151.13 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 150.92/151.13 fof(c187,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 150.92/151.13 fof(c188,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c187])).
% 150.92/151.13 cnf(c189,plain,~para(X679,X680,X679,X678)|coll(X679,X680,X678),inference(split_conjunct,[status(thm)],[c188])).
% 150.92/151.13 cnf(c18083,plain,coll(X4917,X4918,X4918),inference(resolution,[status(thm)],[c18081, c189])).
% 150.92/151.13 cnf(c18453,plain,coll(X4926,X4926,X4925),inference(resolution,[status(thm)],[c18083, c683])).
% 150.92/151.13 cnf(c18869,plain,~coll(X6832,X6832,X6831)|coll(X6831,X6830,X6832),inference(resolution,[status(thm)],[c18453, c400])).
% 150.92/151.13 cnf(c28898,plain,coll(X6839,X6837,X6838),inference(resolution,[status(thm)],[c18869, c18453])).
% 150.92/151.13 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 150.92/151.13 fof(c184,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 150.92/151.13 fof(c185,plain,(![X160]:(![X161]:(![X162]:((~cong(X160,X161,X160,X162)|~coll(X160,X161,X162))|midp(X160,X161,X162))))),inference(variable_rename,[status(thm)],[c184])).
% 150.92/151.13 cnf(c186,plain,~cong(X935,X933,X935,X934)|~coll(X935,X933,X934)|midp(X935,X933,X934),inference(split_conjunct,[status(thm)],[c185])).
% 150.92/151.13 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 150.92/151.13 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 150.92/151.13 fof(c364,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X471,X473,X472)))))),inference(variable_rename,[status(thm)],[c363])).
% 150.92/151.13 cnf(c365,plain,~cyclic(X732,X733,X730,X731)|cyclic(X732,X733,X731,X730),inference(split_conjunct,[status(thm)],[c364])).
% 150.92/151.13 fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 150.92/151.13 fof(c357,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 150.92/151.13 fof(c358,plain,(![X462]:(![X463]:(![X464]:(![X465]:(~cyclic(X462,X463,X464,X465)|cyclic(X463,X462,X464,X465)))))),inference(variable_rename,[status(thm)],[c357])).
% 150.92/151.13 cnf(c359,plain,~cyclic(X722,X725,X724,X723)|cyclic(X725,X722,X724,X723),inference(split_conjunct,[status(thm)],[c358])).
% 150.92/151.13 fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 150.92/151.13 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 150.92/151.13 fof(c361,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c360])).
% 150.92/151.13 cnf(c362,plain,~cyclic(X728,X729,X726,X727)|cyclic(X728,X726,X729,X727),inference(split_conjunct,[status(thm)],[c361])).
% 150.92/151.13 fof(ruleD42b,axiom,(![A]:(![B]:(![P]:(![Q]:((eqangle(P,A,P,B,Q,A,Q,B)&coll(P,Q,B))=>cyclic(A,B,P,Q)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 150.92/151.13 fof(c269,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])).
% 150.92/151.13 fof(c270,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)],[c269])).
% 150.92/151.13 cnf(c271,plain,~eqangle(X1042,X1043,X1042,X1041,X1044,X1043,X1044,X1041)|~coll(X1042,X1044,X1041)|cyclic(X1043,X1041,X1042,X1044),inference(split_conjunct,[status(thm)],[c270])).
% 150.92/151.13 cnf(c28615,plain,~coll(X7429,X7429,X7431)|cyclic(X7430,X7431,X7429,X7429),inference(resolution,[status(thm)],[c18132, c271])).
% 150.92/151.13 cnf(c29486,plain,cyclic(X7434,X7433,X7432,X7432),inference(resolution,[status(thm)],[c28615, c28898])).
% 150.92/151.13 cnf(c29506,plain,cyclic(X7436,X7435,X7437,X7435),inference(resolution,[status(thm)],[c29486, c362])).
% 150.92/151.13 cnf(c29525,plain,cyclic(X7451,X7450,X7452,X7451),inference(resolution,[status(thm)],[c29506, c359])).
% 150.92/151.13 cnf(c29534,plain,cyclic(X7466,X7467,X7466,X7465),inference(resolution,[status(thm)],[c29525, c365])).
% 150.92/151.13 fof(ruleD43,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((cyclic(A,B,C,P)&cyclic(A,B,C,Q))&cyclic(A,B,C,R))&eqangle(C,A,C,B,R,P,R,Q))=>cong(A,B,P,Q)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 150.92/151.13 fof(c264,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])).
% 150.92/151.13 fof(c265,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)],[c264])).
% 150.92/151.13 fof(c267,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(c266,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)],[c265])).])).
% 150.92/151.13 cnf(c268,plain,~cyclic(X1039,X1035,X1036,X1040)|~cyclic(X1039,X1035,X1036,X1038)|~cyclic(X1039,X1035,X1036,X1037)|~eqangle(X1036,X1039,X1036,X1035,X1037,X1040,X1037,X1038)|cong(X1039,X1035,X1040,X1038),inference(split_conjunct,[status(thm)],[c267])).
% 150.92/151.13 cnf(c29296,plain,eqangle(X7249,X7248,X7250,X7247,X7249,X7248,X7247,X7250),inference(resolution,[status(thm)],[c19535, c350])).
% 150.92/151.13 cnf(c29426,plain,eqangle(X7302,X7303,X7302,X7303,X7305,X7304,X7304,X7305),inference(resolution,[status(thm)],[c29296, c344])).
% 150.92/151.13 cnf(c29458,plain,~cyclic(X10476,X10476,X10474,X10475)|cong(X10476,X10476,X10475,X10475),inference(resolution,[status(thm)],[c29426, c268])).
% 150.92/151.13 cnf(c35140,plain,cong(X10477,X10477,X10478,X10478),inference(resolution,[status(thm)],[c29458, c29534])).
% 150.92/151.13 cnf(c35148,plain,~coll(X10495,X10495,X10495)|midp(X10495,X10495,X10495),inference(resolution,[status(thm)],[c35140, c186])).
% 150.92/151.13 cnf(c35179,plain,midp(X10496,X10496,X10496),inference(resolution,[status(thm)],[c35148, c28898])).
% 150.92/151.13 cnf(c35512,plain,midp(X10498,X10499,X10499),inference(resolution,[status(thm)],[c35179, c18117])).
% 150.92/151.13 cnf(c35733,plain,cong(X10513,X10511,X10512,X10511),inference(resolution,[status(thm)],[c35512, c32183])).
% 150.92/151.13 cnf(c36031,plain,perp(X10536,X10537,X10535,X10535),inference(resolution,[status(thm)],[c35733, c1272])).
% 150.92/151.13 fof(ruleD41,axiom,(![A]:(![B]:(![P]:(![Q]:(cyclic(A,B,P,Q)=>eqangle(P,A,P,B,Q,A,Q,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD41)).
% 150.92/151.13 fof(c276,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])).
% 150.92/151.13 fof(c277,plain,(![X285]:(![X286]:(![X287]:(![X288]:(~cyclic(X285,X286,X287,X288)|eqangle(X287,X285,X287,X286,X288,X285,X288,X286)))))),inference(variable_rename,[status(thm)],[c276])).
% 150.92/151.13 cnf(c278,plain,~cyclic(X1051,X1052,X1050,X1049)|eqangle(X1050,X1051,X1050,X1052,X1049,X1051,X1049,X1052),inference(split_conjunct,[status(thm)],[c277])).
% 150.92/151.13 cnf(c29523,plain,eqangle(X7505,X7506,X7505,X7504,X7504,X7506,X7504,X7504),inference(resolution,[status(thm)],[c29506, c278])).
% 150.92/151.13 cnf(c29587,plain,~perp(X17556,X17558,X17556,X17556)|perp(X17557,X17558,X17557,X17556),inference(resolution,[status(thm)],[c29523, c161])).
% 150.92/151.13 cnf(c46007,plain,perp(X17563,X17562,X17563,X17564),inference(resolution,[status(thm)],[c29587, c36031])).
% 150.92/151.13 cnf(c46029,plain,$false,inference(resolution,[status(thm)],[c46007, c21])).
% 150.92/151.13 % SZS output end CNFRefutation
% 150.92/151.13
% 150.92/151.13 % Initial clauses : 134
% 150.92/151.13 % Processed clauses : 4476
% 150.92/151.13 % Factors computed : 307
% 150.92/151.13 % Resolvents computed: 45316
% 150.92/151.13 % Tautologies deleted: 38
% 150.92/151.13 % Forward subsumed : 11891
% 150.92/151.13 % Backward subsumed : 4072
% 150.92/151.13 % -------- CPU Time ---------
% 150.92/151.13 % User time : 150.659 s
% 150.92/151.13 % System time : 0.107 s
% 150.92/151.13 % Total time : 150.766 s
%------------------------------------------------------------------------------