%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO608+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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 25.11s 25.33s
% Output : Refutation 25.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO608+1 : TPTP v8.1.2. Released v7.5.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n016.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 08:07:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 25.11/25.33 % Version: 1.5
% 25.11/25.33 % SZS status Theorem
% 25.11/25.33 % SZS output start CNFRefutation
% 25.11/25.33 fof(exemplo6GDDFULL618070,conjecture,(![P]:(![A]:(![B]:(![O]:(![A1]:(![B1]:(![O1]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(((((((midp(O,B,A)&circle(O,A,NWPNT1,NWPNT2))&coll(A1,P,A))&circle(O,A,A1,NWPNT3))&coll(B1,P,B))&circle(O,A,B1,NWPNT4))&circle(O1,P,A1,B1))=>perp(O,A1,A1,O1))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL618070)).
% 25.11/25.33 fof(c11,negated_conjecture,(~(![P]:(![A]:(![B]:(![O]:(![A1]:(![B1]:(![O1]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(((((((midp(O,B,A)&circle(O,A,NWPNT1,NWPNT2))&coll(A1,P,A))&circle(O,A,A1,NWPNT3))&coll(B1,P,B))&circle(O,A,B1,NWPNT4))&circle(O1,P,A1,B1))=>perp(O,A1,A1,O1)))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618070])).
% 25.11/25.33 fof(c12,negated_conjecture,(?[P]:(?[A]:(?[B]:(?[O]:(?[A1]:(?[B1]:(?[O1]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(((((((midp(O,B,A)&circle(O,A,NWPNT1,NWPNT2))&coll(A1,P,A))&circle(O,A,A1,NWPNT3))&coll(B1,P,B))&circle(O,A,B1,NWPNT4))&circle(O1,P,A1,B1))&~perp(O,A1,A1,O1))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 25.11/25.33 fof(c13,negated_conjecture,(?[P]:(?[A]:(?[B]:(?[O]:(?[A1]:(?[B1]:(?[O1]:(((((((midp(O,B,A)&(?[NWPNT1]:(?[NWPNT2]:circle(O,A,NWPNT1,NWPNT2))))&coll(A1,P,A))&(?[NWPNT3]:circle(O,A,A1,NWPNT3)))&coll(B1,P,B))&(?[NWPNT4]:circle(O,A,B1,NWPNT4)))&circle(O1,P,A1,B1))&~perp(O,A1,A1,O1))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 25.11/25.33 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((midp(X5,X4,X3)&(?[X9]:(?[X10]:circle(X5,X3,X9,X10))))&coll(X6,X2,X3))&(?[X11]:circle(X5,X3,X6,X11)))&coll(X7,X2,X4))&(?[X12]:circle(X5,X3,X7,X12)))&circle(X8,X2,X6,X7))&~perp(X5,X6,X6,X8))))))))),inference(variable_rename,[status(thm)],[c13])).
% 25.11/25.33 fof(c15,negated_conjecture,(((((((midp(skolem0004,skolem0003,skolem0002)&circle(skolem0004,skolem0002,skolem0008,skolem0009))&coll(skolem0005,skolem0001,skolem0002))&circle(skolem0004,skolem0002,skolem0005,skolem0010))&coll(skolem0006,skolem0001,skolem0003))&circle(skolem0004,skolem0002,skolem0006,skolem0011))&circle(skolem0007,skolem0001,skolem0005,skolem0006))&~perp(skolem0004,skolem0005,skolem0005,skolem0007)),inference(skolemize,[status(esa)],[c14])).
% 25.11/25.33 cnf(c23,negated_conjecture,~perp(skolem0004,skolem0005,skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 25.11/25.33 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)).
% 25.11/25.33 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])).
% 25.11/25.33 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])).
% 25.11/25.33 fof(c162,plain,(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:(![X133]:(![X134]:(![X135]:((~eqangle(X128,X129,X130,X131,X132,X133,X134,X135)|~perp(X132,X133,X134,X135))|perp(X128,X129,X130,X131)))))))))),inference(shift_quantors,[status(thm)],[fof(c161,plain,(![X128]:(![X129]:(![X130]:(![X131]:((![X132]:(![X133]:(![X134]:(![X135]:(~eqangle(X128,X129,X130,X131,X132,X133,X134,X135)|~perp(X132,X133,X134,X135))))))|perp(X128,X129,X130,X131)))))),inference(variable_rename,[status(thm)],[c160])).])).
% 25.11/25.33 cnf(c163,plain,~eqangle(X911,X907,X914,X909,X913,X912,X908,X910)|~perp(X913,X912,X908,X910)|perp(X911,X907,X914,X909),inference(split_conjunct,[status(thm)],[c162])).
% 25.11/25.33 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)).
% 25.11/25.33 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])).
% 25.11/25.33 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])).
% 25.11/25.33 fof(c284,plain,(![X293]:(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(~para(X293,X294,X295,X296)|eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c283,plain,(![X293]:(![X294]:(![X295]:(![X296]:(~para(X293,X294,X295,X296)|(![X297]:(![X298]:eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(variable_rename,[status(thm)],[c282])).])).
% 25.11/25.33 cnf(c285,plain,~para(X1083,X1086,X1087,X1082)|eqangle(X1083,X1086,X1085,X1084,X1087,X1082,X1085,X1084),inference(split_conjunct,[status(thm)],[c284])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 25.11/25.33 fof(c398,plain,(![X520]:(![X521]:(![X522]:(![X523]:(~para(X520,X521,X522,X523)|para(X520,X521,X523,X522)))))),inference(variable_rename,[status(thm)],[c397])).
% 25.11/25.33 cnf(c399,plain,~para(X727,X726,X725,X728)|para(X727,X726,X728,X725),inference(split_conjunct,[status(thm)],[c398])).
% 25.11/25.33 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)).
% 25.11/25.33 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])).
% 25.11/25.33 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])).
% 25.11/25.33 fof(c289,plain,(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)|para(X299,X300,X301,X302)))))))),inference(shift_quantors,[status(thm)],[fof(c288,plain,(![X299]:(![X300]:(![X301]:(![X302]:((![X303]:(![X304]:~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))|para(X299,X300,X301,X302)))))),inference(variable_rename,[status(thm)],[c287])).])).
% 25.11/25.33 cnf(c290,plain,~eqangle(X1091,X1089,X1093,X1088,X1090,X1092,X1093,X1088)|para(X1091,X1089,X1090,X1092),inference(split_conjunct,[status(thm)],[c289])).
% 25.11/25.33 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)).
% 25.11/25.33 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])).
% 25.11/25.33 fof(c351,plain,(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(![X451]:(![X452]:(~eqangle(X445,X446,X447,X448,X449,X450,X451,X452)|eqangle(X447,X448,X445,X446,X451,X452,X449,X450)))))))))),inference(variable_rename,[status(thm)],[c350])).
% 25.11/25.33 cnf(c352,plain,~eqangle(X1231,X1228,X1227,X1230,X1233,X1226,X1232,X1229)|eqangle(X1227,X1230,X1231,X1228,X1232,X1229,X1233,X1226),inference(split_conjunct,[status(thm)],[c351])).
% 25.11/25.33 cnf(c16,negated_conjecture,midp(skolem0004,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 25.11/25.33 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 25.11/25.33 fof(c376,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 25.11/25.33 fof(c377,plain,(![X487]:(![X488]:(![X489]:(~midp(X489,X488,X487)|midp(X489,X487,X488))))),inference(variable_rename,[status(thm)],[c376])).
% 25.11/25.33 cnf(c378,plain,~midp(X562,X561,X563)|midp(X562,X563,X561),inference(split_conjunct,[status(thm)],[c377])).
% 25.11/25.33 cnf(c416,plain,midp(skolem0004,skolem0002,skolem0003),inference(resolution,[status(thm)],[c378, c16])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c198,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 25.11/25.33 fof(c199,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c198])).
% 25.11/25.33 fof(c201,plain,(![X180]:(![X181]:(![X182]:(![X183]:(![X184]:((~midp(X184,X180,X181)|~midp(X184,X182,X183))|para(X180,X182,X181,X183))))))),inference(shift_quantors,[status(thm)],[fof(c200,plain,(![X180]:(![X181]:(![X182]:(![X183]:((![X184]:(~midp(X184,X180,X181)|~midp(X184,X182,X183)))|para(X180,X182,X181,X183)))))),inference(variable_rename,[status(thm)],[c199])).])).
% 25.11/25.33 cnf(c202,plain,~midp(X956,X953,X952)|~midp(X956,X954,X955)|para(X953,X954,X952,X955),inference(split_conjunct,[status(thm)],[c201])).
% 25.11/25.33 cnf(c967,plain,~midp(skolem0004,X1727,X1726)|para(X1727,skolem0003,X1726,skolem0002),inference(resolution,[status(thm)],[c202, c16])).
% 25.11/25.33 cnf(c2917,plain,para(skolem0002,skolem0003,skolem0003,skolem0002),inference(resolution,[status(thm)],[c967, c416])).
% 25.11/25.33 cnf(c2933,plain,para(skolem0002,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c2917, c399])).
% 25.11/25.33 cnf(c2943,plain,eqangle(skolem0002,skolem0003,X2427,X2428,skolem0002,skolem0003,X2427,X2428),inference(resolution,[status(thm)],[c2933, c285])).
% 25.11/25.33 cnf(c4560,plain,eqangle(X2559,X2558,skolem0002,skolem0003,X2559,X2558,skolem0002,skolem0003),inference(resolution,[status(thm)],[c2943, c352])).
% 25.11/25.33 cnf(c4859,plain,para(X2561,X2560,X2561,X2560),inference(resolution,[status(thm)],[c4560, c290])).
% 25.11/25.33 cnf(c4861,plain,para(X2587,X2586,X2586,X2587),inference(resolution,[status(thm)],[c4859, c399])).
% 25.11/25.33 cnf(c5568,plain,eqangle(X3736,X3735,X3734,X3737,X3735,X3736,X3734,X3737),inference(resolution,[status(thm)],[c4861, c285])).
% 25.11/25.33 cnf(c9413,plain,~perp(X4869,X4871,X4872,X4870)|perp(X4871,X4869,X4872,X4870),inference(resolution,[status(thm)],[c5568, c163])).
% 25.11/25.33 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)).
% 25.11/25.33 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])).
% 25.11/25.33 fof(c225,plain,(![X219]:(![X220]:(![X221]:(![X222]:((~cong(X219,X221,X220,X221)|~cong(X219,X222,X220,X222))|perp(X219,X220,X221,X222)))))),inference(variable_rename,[status(thm)],[c224])).
% 25.11/25.33 cnf(c226,plain,~cong(X994,X996,X997,X996)|~cong(X994,X995,X997,X995)|perp(X994,X997,X996,X995),inference(split_conjunct,[status(thm)],[c225])).
% 25.11/25.33 cnf(c1010,plain,~cong(X998,X1000,X999,X1000)|perp(X998,X999,X1000,X1000),inference(factor,[status(thm)],[c226])).
% 25.11/25.33 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)).
% 25.11/25.33 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])).
% 25.11/25.33 fof(c239,plain,(![X235]:(![X236]:(![X237]:(![X238]:((~perp(X235,X236,X236,X237)|~midp(X238,X235,X237))|cong(X235,X238,X236,X238)))))),inference(variable_rename,[status(thm)],[c238])).
% 25.11/25.33 cnf(c240,plain,~perp(X1015,X1016,X1016,X1017)|~midp(X1018,X1015,X1017)|cong(X1015,X1018,X1016,X1018),inference(split_conjunct,[status(thm)],[c239])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 25.11/25.33 fof(c386,plain,(![X502]:(![X503]:(![X504]:(![X505]:(~perp(X502,X503,X504,X505)|perp(X504,X505,X502,X503)))))),inference(variable_rename,[status(thm)],[c385])).
% 25.11/25.33 cnf(c387,plain,~perp(X708,X710,X711,X709)|perp(X711,X709,X708,X710),inference(split_conjunct,[status(thm)],[c386])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 25.11/25.33 fof(c339,plain,(![X413]:(![X414]:(![X415]:(![X416]:(~cong(X413,X414,X415,X416)|cong(X413,X414,X416,X415)))))),inference(variable_rename,[status(thm)],[c338])).
% 25.11/25.33 cnf(c340,plain,~cong(X675,X677,X676,X674)|cong(X675,X677,X674,X676),inference(split_conjunct,[status(thm)],[c339])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 25.11/25.33 fof(c336,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X411,X412,X409,X410)))))),inference(variable_rename,[status(thm)],[c335])).
% 25.11/25.33 cnf(c337,plain,~cong(X670,X673,X671,X672)|cong(X671,X672,X670,X673),inference(split_conjunct,[status(thm)],[c336])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c183,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 25.11/25.33 fof(c184,plain,(![X161]:(![X162]:(![X163]:(~midp(X161,X162,X163)|cong(X161,X162,X161,X163))))),inference(variable_rename,[status(thm)],[c183])).
% 25.11/25.33 cnf(c185,plain,~midp(X652,X654,X653)|cong(X652,X654,X652,X653),inference(split_conjunct,[status(thm)],[c184])).
% 25.11/25.33 cnf(c477,plain,cong(skolem0004,skolem0002,skolem0004,skolem0003),inference(resolution,[status(thm)],[c185, c416])).
% 25.11/25.33 cnf(c483,plain,cong(skolem0004,skolem0002,skolem0003,skolem0004),inference(resolution,[status(thm)],[c340, c477])).
% 25.11/25.33 cnf(c489,plain,cong(skolem0003,skolem0004,skolem0004,skolem0002),inference(resolution,[status(thm)],[c483, c337])).
% 25.11/25.33 cnf(c493,plain,cong(skolem0003,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c489, c340])).
% 25.11/25.33 cnf(c1014,plain,perp(skolem0003,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1010, c493])).
% 25.11/25.33 cnf(c1028,plain,perp(skolem0004,skolem0004,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1014, c387])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c379,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~perp(C,D,E,F))|perp(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD10])).
% 25.11/25.33 fof(c380,plain,(![X490]:(![X491]:(![X492]:(![X493]:(![X494]:(![X495]:((~para(X490,X491,X492,X493)|~perp(X492,X493,X494,X495))|perp(X490,X491,X494,X495)))))))),inference(variable_rename,[status(thm)],[c379])).
% 25.11/25.33 cnf(c381,plain,~para(X1256,X1260,X1258,X1257)|~perp(X1258,X1257,X1261,X1259)|perp(X1256,X1260,X1261,X1259),inference(split_conjunct,[status(thm)],[c380])).
% 25.11/25.33 cnf(c1533,plain,~para(X3077,X3078,skolem0004,skolem0004)|perp(X3077,X3078,skolem0003,skolem0002),inference(resolution,[status(thm)],[c381, c1028])).
% 25.11/25.33 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)).
% 25.11/25.33 fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 25.11/25.33 fof(c395,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X518,X519,X516,X517)))))),inference(variable_rename,[status(thm)],[c394])).
% 25.11/25.33 cnf(c396,plain,~para(X716,X719,X717,X718)|para(X717,X718,X716,X719),inference(split_conjunct,[status(thm)],[c395])).
% 25.11/25.33 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)).
% 25.11/25.33 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])).
% 25.11/25.33 fof(c383,plain,(![X496]:(![X497]:(![X498]:(![X499]:(![X500]:(![X501]:((~perp(X496,X497,X498,X499)|~perp(X498,X499,X500,X501))|para(X496,X497,X500,X501)))))))),inference(variable_rename,[status(thm)],[c382])).
% 25.11/25.33 cnf(c384,plain,~perp(X1262,X1266,X1265,X1263)|~perp(X1265,X1263,X1264,X1267)|para(X1262,X1266,X1264,X1267),inference(split_conjunct,[status(thm)],[c383])).
% 25.11/25.33 cnf(c1557,plain,~perp(X3107,X3106,skolem0004,skolem0004)|para(X3107,X3106,skolem0003,skolem0002),inference(resolution,[status(thm)],[c384, c1028])).
% 25.11/25.33 cnf(c476,plain,cong(skolem0004,skolem0003,skolem0004,skolem0002),inference(resolution,[status(thm)],[c185, c16])).
% 25.11/25.33 cnf(c482,plain,cong(skolem0004,skolem0003,skolem0002,skolem0004),inference(resolution,[status(thm)],[c340, c476])).
% 25.11/25.33 cnf(c486,plain,cong(skolem0002,skolem0004,skolem0004,skolem0003),inference(resolution,[status(thm)],[c482, c337])).
% 25.11/25.33 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)).
% 25.11/25.34 fof(c332,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~cong(A,B,C,D)|~cong(C,D,E,F))|cong(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD25])).
% 25.11/25.34 fof(c333,plain,(![X403]:(![X404]:(![X405]:(![X406]:(![X407]:(![X408]:((~cong(X403,X404,X405,X406)|~cong(X405,X406,X407,X408))|cong(X403,X404,X407,X408)))))))),inference(variable_rename,[status(thm)],[c332])).
% 25.11/25.34 cnf(c334,plain,~cong(X1192,X1197,X1194,X1195)|~cong(X1194,X1195,X1193,X1196)|cong(X1192,X1197,X1193,X1196),inference(split_conjunct,[status(thm)],[c333])).
% 25.11/25.34 cnf(c1429,plain,~cong(X2951,X2952,skolem0004,skolem0003)|cong(X2951,X2952,skolem0002,skolem0004),inference(resolution,[status(thm)],[c334, c482])).
% 25.11/25.34 cnf(c8051,plain,cong(skolem0002,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c1429, c486])).
% 25.11/25.34 cnf(c9538,plain,perp(skolem0002,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c8051, c1010])).
% 25.11/25.34 cnf(c9781,plain,para(skolem0002,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c9538, c1557])).
% 25.11/25.34 cnf(c9996,plain,para(skolem0003,skolem0002,skolem0002,skolem0002),inference(resolution,[status(thm)],[c9781, c396])).
% 25.11/25.34 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)).
% 25.11/25.34 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~para(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD6])).
% 25.11/25.34 fof(c392,plain,(![X510]:(![X511]:(![X512]:(![X513]:(![X514]:(![X515]:((~para(X510,X511,X512,X513)|~para(X512,X513,X514,X515))|para(X510,X511,X514,X515)))))))),inference(variable_rename,[status(thm)],[c391])).
% 25.11/25.34 cnf(c393,plain,~para(X1269,X1273,X1272,X1268)|~para(X1272,X1268,X1271,X1270)|para(X1269,X1273,X1271,X1270),inference(split_conjunct,[status(thm)],[c392])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c264,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:((~midp(X273,X270,X271)|~midp(X274,X270,X272))|para(X273,X274,X271,X272))))))),inference(variable_rename,[status(thm)],[c263])).
% 25.11/25.34 cnf(c265,plain,~midp(X1060,X1061,X1062)|~midp(X1059,X1061,X1063)|para(X1060,X1059,X1062,X1063),inference(split_conjunct,[status(thm)],[c264])).
% 25.11/25.34 cnf(c1115,plain,~midp(X1499,X1500,X1501)|para(X1499,X1499,X1501,X1501),inference(factor,[status(thm)],[c265])).
% 25.11/25.34 cnf(c2181,plain,para(skolem0004,skolem0004,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1115, c16])).
% 25.11/25.34 cnf(c2191,plain,para(skolem0002,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c2181, c396])).
% 25.11/25.34 cnf(c2224,plain,~para(X4660,X4659,skolem0002,skolem0002)|para(X4660,X4659,skolem0004,skolem0004),inference(resolution,[status(thm)],[c2191, c393])).
% 25.11/25.34 cnf(c10744,plain,para(skolem0003,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c2224, c9996])).
% 25.11/25.34 cnf(c10757,plain,perp(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c10744, c1533])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c345,plain,(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(![X434]:(![X435]:(![X436]:(~eqangle(X429,X430,X431,X432,X433,X434,X435,X436)|eqangle(X429,X430,X433,X434,X431,X432,X435,X436)))))))))),inference(variable_rename,[status(thm)],[c344])).
% 25.11/25.34 cnf(c346,plain,~eqangle(X1213,X1212,X1216,X1217,X1215,X1210,X1211,X1214)|eqangle(X1213,X1212,X1215,X1210,X1216,X1217,X1211,X1214),inference(split_conjunct,[status(thm)],[c345])).
% 25.11/25.34 cnf(c4879,plain,eqangle(X3447,X3448,X3446,X3449,X3447,X3448,X3446,X3449),inference(resolution,[status(thm)],[c4859, c285])).
% 25.11/25.34 cnf(c8924,plain,eqangle(X3777,X3776,X3777,X3776,X3778,X3775,X3778,X3775),inference(resolution,[status(thm)],[c4879, c346])).
% 25.11/25.34 cnf(c9647,plain,~perp(X4903,X4901,X4903,X4901)|perp(X4900,X4902,X4900,X4902),inference(resolution,[status(thm)],[c8924, c163])).
% 25.11/25.34 cnf(c11494,plain,perp(X4904,X4905,X4904,X4905),inference(resolution,[status(thm)],[c9647, c10757])).
% 25.11/25.34 cnf(c11513,plain,perp(X4910,X4911,X4911,X4910),inference(resolution,[status(thm)],[c11494, c9413])).
% 25.11/25.34 cnf(c11548,plain,~midp(X5053,X5052,X5052)|cong(X5052,X5053,X5054,X5053),inference(resolution,[status(thm)],[c11513, c240])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c196,plain,(![X175]:(![X176]:(![X177]:(![X178]:(![X179]:(((~midp(X179,X175,X176)|~para(X175,X177,X176,X178))|~para(X175,X178,X176,X177))|midp(X179,X177,X178))))))),inference(variable_rename,[status(thm)],[c195])).
% 25.11/25.34 cnf(c197,plain,~midp(X946,X949,X950)|~para(X949,X947,X950,X948)|~para(X949,X948,X950,X947)|midp(X946,X947,X948),inference(split_conjunct,[status(thm)],[c196])).
% 25.11/25.34 cnf(c962,plain,~midp(X2134,X2132,X2133)|~para(X2132,X2131,X2133,X2131)|midp(X2134,X2131,X2131),inference(factor,[status(thm)],[c197])).
% 25.11/25.34 cnf(c4880,plain,~midp(X3456,X3458,X3458)|midp(X3456,X3457,X3457),inference(resolution,[status(thm)],[c4859, c962])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c401,plain,(![X524]:(![X525]:(![X526]:(![X527]:((~coll(X524,X525,X526)|~coll(X524,X525,X527))|coll(X526,X527,X524)))))),inference(variable_rename,[status(thm)],[c400])).
% 25.11/25.34 cnf(c402,plain,~coll(X735,X738,X737)|~coll(X735,X738,X736)|coll(X737,X736,X735),inference(split_conjunct,[status(thm)],[c401])).
% 25.11/25.34 cnf(c503,plain,~coll(X741,X739,X740)|coll(X740,X740,X741),inference(factor,[status(thm)],[c402])).
% 25.11/25.34 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)).
% 25.11/25.34 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 25.11/25.34 fof(c190,plain,(![X167]:(![X168]:(![X169]:(~para(X167,X168,X167,X169)|coll(X167,X168,X169))))),inference(variable_rename,[status(thm)],[c189])).
% 25.11/25.34 cnf(c191,plain,~para(X668,X669,X668,X667)|coll(X668,X669,X667),inference(split_conjunct,[status(thm)],[c190])).
% 25.11/25.34 cnf(c4862,plain,coll(X2565,X2566,X2566),inference(resolution,[status(thm)],[c4859, c191])).
% 25.11/25.34 cnf(c5041,plain,coll(X2571,X2571,X2572),inference(resolution,[status(thm)],[c4862, c503])).
% 25.11/25.34 cnf(c5508,plain,~coll(X3622,X3622,X3624)|coll(X3624,X3623,X3622),inference(resolution,[status(thm)],[c5041, c402])).
% 25.11/25.34 cnf(c9178,plain,coll(X3635,X3633,X3634),inference(resolution,[status(thm)],[c5508, c5041])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c187,plain,(![X164]:(![X165]:(![X166]:((~cong(X164,X165,X164,X166)|~coll(X164,X165,X166))|midp(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c186])).
% 25.11/25.34 cnf(c188,plain,~cong(X939,X937,X939,X938)|~coll(X939,X937,X938)|midp(X939,X937,X938),inference(split_conjunct,[status(thm)],[c187])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c272,plain,(![X281]:(![X282]:(![X283]:(![X284]:((~eqangle(X283,X281,X283,X282,X284,X281,X284,X282)|~coll(X283,X284,X282))|cyclic(X281,X282,X283,X284)))))),inference(variable_rename,[status(thm)],[c271])).
% 25.11/25.34 cnf(c273,plain,~eqangle(X1071,X1073,X1071,X1072,X1070,X1073,X1070,X1072)|~coll(X1071,X1070,X1072)|cyclic(X1073,X1072,X1071,X1070),inference(split_conjunct,[status(thm)],[c272])).
% 25.11/25.34 cnf(c8925,plain,~coll(X4034,X4034,X4033)|cyclic(X4032,X4033,X4034,X4034),inference(resolution,[status(thm)],[c4879, c273])).
% 25.11/25.34 cnf(c10211,plain,cyclic(X4036,X4037,X4035,X4035),inference(resolution,[status(thm)],[c8925, c9178])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c269,plain,(![X275]:(![X276]:(![X277]:(![X278]:(![X279]:(![X280]:((((~cyclic(X275,X276,X277,X278)|~cyclic(X275,X276,X277,X279))|~cyclic(X275,X276,X277,X280))|~eqangle(X277,X275,X277,X276,X280,X278,X280,X279))|cong(X275,X276,X278,X279)))))))),inference(shift_quantors,[status(thm)],[fof(c268,plain,(![X275]:(![X276]:(![X277]:(![X278]:(![X279]:((![X280]:(((~cyclic(X275,X276,X277,X278)|~cyclic(X275,X276,X277,X279))|~cyclic(X275,X276,X277,X280))|~eqangle(X277,X275,X277,X276,X280,X278,X280,X279)))|cong(X275,X276,X278,X279))))))),inference(variable_rename,[status(thm)],[c267])).])).
% 25.11/25.34 cnf(c270,plain,~cyclic(X1067,X1064,X1068,X1065)|~cyclic(X1067,X1064,X1068,X1066)|~cyclic(X1067,X1064,X1068,X1069)|~eqangle(X1068,X1067,X1068,X1064,X1069,X1065,X1069,X1066)|cong(X1067,X1064,X1065,X1066),inference(split_conjunct,[status(thm)],[c269])).
% 25.11/25.34 fof(ruleD20,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(P,Q,U,V,A,B,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c348,plain,(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(~eqangle(X437,X438,X439,X440,X441,X442,X443,X444)|eqangle(X441,X442,X443,X444,X437,X438,X439,X440)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 25.11/25.34 cnf(c349,plain,~eqangle(X1218,X1219,X1224,X1221,X1225,X1222,X1220,X1223)|eqangle(X1225,X1222,X1220,X1223,X1218,X1219,X1224,X1221),inference(split_conjunct,[status(thm)],[c348])).
% 25.11/25.34 cnf(c9405,plain,eqangle(X3800,X3801,X3801,X3800,X3802,X3799,X3802,X3799),inference(resolution,[status(thm)],[c5568, c346])).
% 25.11/25.34 cnf(c9657,plain,eqangle(X3891,X3890,X3891,X3890,X3892,X3889,X3889,X3892),inference(resolution,[status(thm)],[c9405, c349])).
% 25.11/25.34 cnf(c9861,plain,~cyclic(X5081,X5081,X5079,X5080)|cong(X5081,X5081,X5080,X5080),inference(resolution,[status(thm)],[c9657, c270])).
% 25.11/25.34 cnf(c11832,plain,cong(X5082,X5082,X5083,X5083),inference(resolution,[status(thm)],[c9861, c10211])).
% 25.11/25.34 cnf(c11860,plain,~coll(X5101,X5101,X5101)|midp(X5101,X5101,X5101),inference(resolution,[status(thm)],[c11832, c188])).
% 25.11/25.34 cnf(c11889,plain,midp(X5102,X5102,X5102),inference(resolution,[status(thm)],[c11860, c9178])).
% 25.11/25.34 cnf(c11890,plain,midp(X5103,X5104,X5104),inference(resolution,[status(thm)],[c11889, c4880])).
% 25.11/25.34 cnf(c11945,plain,cong(X5125,X5126,X5124,X5126),inference(resolution,[status(thm)],[c11890, c11548])).
% 25.11/25.34 cnf(c12069,plain,perp(X5155,X5157,X5156,X5156),inference(resolution,[status(thm)],[c11945, c1010])).
% 25.11/25.34 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)).
% 25.11/25.34 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])).
% 25.11/25.34 fof(c279,plain,(![X289]:(![X290]:(![X291]:(![X292]:(~cyclic(X289,X290,X291,X292)|eqangle(X291,X289,X291,X290,X292,X289,X292,X290)))))),inference(variable_rename,[status(thm)],[c278])).
% 25.11/25.34 cnf(c280,plain,~cyclic(X1081,X1078,X1080,X1079)|eqangle(X1080,X1081,X1080,X1078,X1079,X1081,X1079,X1078),inference(split_conjunct,[status(thm)],[c279])).
% 25.11/25.34 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)).
% 25.11/25.34 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 25.11/25.34 fof(c363,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X472,X471,X473)))))),inference(variable_rename,[status(thm)],[c362])).
% 25.11/25.34 cnf(c364,plain,~cyclic(X701,X703,X700,X702)|cyclic(X701,X700,X703,X702),inference(split_conjunct,[status(thm)],[c363])).
% 25.11/25.34 cnf(c10212,plain,cyclic(X4040,X4039,X4038,X4039),inference(resolution,[status(thm)],[c10211, c364])).
% 25.11/25.34 cnf(c10226,plain,eqangle(X4103,X4102,X4103,X4104,X4104,X4102,X4104,X4104),inference(resolution,[status(thm)],[c10212, c280])).
% 25.11/25.34 cnf(c10280,plain,~perp(X11492,X11491,X11492,X11492)|perp(X11490,X11491,X11490,X11492),inference(resolution,[status(thm)],[c10226, c163])).
% 25.11/25.34 cnf(c17907,plain,perp(X11498,X11500,X11498,X11499),inference(resolution,[status(thm)],[c10280, c12069])).
% 25.11/25.34 cnf(c17923,plain,perp(X11512,X11513,X11513,X11511),inference(resolution,[status(thm)],[c17907, c9413])).
% 25.11/25.34 cnf(c17939,plain,$false,inference(resolution,[status(thm)],[c17923, c23])).
% 25.11/25.34 % SZS output end CNFRefutation
% 25.11/25.34
% 25.11/25.34 % Initial clauses : 135
% 25.11/25.34 % Processed clauses : 2102
% 25.11/25.34 % Factors computed : 125
% 25.11/25.34 % Resolvents computed: 17416
% 25.11/25.34 % Tautologies deleted: 22
% 25.11/25.34 % Forward subsumed : 6295
% 25.11/25.34 % Backward subsumed : 1822
% 25.11/25.34 % -------- CPU Time ---------
% 25.11/25.34 % User time : 24.963 s
% 25.11/25.34 % System time : 0.037 s
% 25.11/25.34 % Total time : 25.000 s
%------------------------------------------------------------------------------