%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO602+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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 121.93s 122.11s
% Output : Refutation 121.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO602+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 : n010.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 07:53:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 121.93/122.11 % Version: 1.5
% 121.93/122.11 % SZS status Theorem
% 121.93/122.11 % SZS output start CNFRefutation
% 121.93/122.11 fof(exemplo6GDDFULL618064,conjecture,(![A]:(![B]:(![E]:(![F]:(![D]:(![M]:(![E1]:(![F1]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:(((((((((((circle(B,E,NWPNT1,NWPNT2)&circle(A,E,NWPNT3,NWPNT4))&circle(B,E,F,NWPNT5))&circle(A,E,F,NWPNT6))&coll(D,A,B))&coll(D,E,F))&circle(B,E,M,NWPNT7))&circle(A,E,E1,NWPNT8))&coll(E1,E,M))&coll(F1,F,M))&circle(A,E,F1,NWPNT9))=>perp(E1,F1,M,B))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL618064)).
% 121.93/122.11 fof(c11,negated_conjecture,(~(![A]:(![B]:(![E]:(![F]:(![D]:(![M]:(![E1]:(![F1]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:(((((((((((circle(B,E,NWPNT1,NWPNT2)&circle(A,E,NWPNT3,NWPNT4))&circle(B,E,F,NWPNT5))&circle(A,E,F,NWPNT6))&coll(D,A,B))&coll(D,E,F))&circle(B,E,M,NWPNT7))&circle(A,E,E1,NWPNT8))&coll(E1,E,M))&coll(F1,F,M))&circle(A,E,F1,NWPNT9))=>perp(E1,F1,M,B)))))))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618064])).
% 121.93/122.11 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[E]:(?[F]:(?[D]:(?[M]:(?[E1]:(?[F1]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(?[NWPNT5]:(?[NWPNT6]:(?[NWPNT7]:(?[NWPNT8]:(?[NWPNT9]:(((((((((((circle(B,E,NWPNT1,NWPNT2)&circle(A,E,NWPNT3,NWPNT4))&circle(B,E,F,NWPNT5))&circle(A,E,F,NWPNT6))&coll(D,A,B))&coll(D,E,F))&circle(B,E,M,NWPNT7))&circle(A,E,E1,NWPNT8))&coll(E1,E,M))&coll(F1,F,M))&circle(A,E,F1,NWPNT9))&~perp(E1,F1,M,B))))))))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 121.93/122.11 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[E]:(?[F]:(?[D]:(?[M]:(?[E1]:(?[F1]:((((((((((((?[NWPNT1]:(?[NWPNT2]:circle(B,E,NWPNT1,NWPNT2)))&(?[NWPNT3]:(?[NWPNT4]:circle(A,E,NWPNT3,NWPNT4))))&(?[NWPNT5]:circle(B,E,F,NWPNT5)))&(?[NWPNT6]:circle(A,E,F,NWPNT6)))&coll(D,A,B))&coll(D,E,F))&(?[NWPNT7]:circle(B,E,M,NWPNT7)))&(?[NWPNT8]:circle(A,E,E1,NWPNT8)))&coll(E1,E,M))&coll(F1,F,M))&(?[NWPNT9]:circle(A,E,F1,NWPNT9)))&~perp(E1,F1,M,B)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 121.93/122.11 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((((((?[X10]:(?[X11]:circle(X3,X4,X10,X11)))&(?[X12]:(?[X13]:circle(X2,X4,X12,X13))))&(?[X14]:circle(X3,X4,X5,X14)))&(?[X15]:circle(X2,X4,X5,X15)))&coll(X6,X2,X3))&coll(X6,X4,X5))&(?[X16]:circle(X3,X4,X7,X16)))&(?[X17]:circle(X2,X4,X8,X17)))&coll(X8,X4,X7))&coll(X9,X5,X7))&(?[X18]:circle(X2,X4,X9,X18)))&~perp(X8,X9,X7,X3)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 121.93/122.11 fof(c15,negated_conjecture,(((((((((((circle(skolem0002,skolem0003,skolem0009,skolem0010)&circle(skolem0001,skolem0003,skolem0011,skolem0012))&circle(skolem0002,skolem0003,skolem0004,skolem0013))&circle(skolem0001,skolem0003,skolem0004,skolem0014))&coll(skolem0005,skolem0001,skolem0002))&coll(skolem0005,skolem0003,skolem0004))&circle(skolem0002,skolem0003,skolem0006,skolem0015))&circle(skolem0001,skolem0003,skolem0007,skolem0016))&coll(skolem0007,skolem0003,skolem0006))&coll(skolem0008,skolem0004,skolem0006))&circle(skolem0001,skolem0003,skolem0008,skolem0017))&~perp(skolem0007,skolem0008,skolem0006,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 121.93/122.11 cnf(c27,negated_conjecture,~perp(skolem0007,skolem0008,skolem0006,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c404,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 121.93/122.11 fof(c405,plain,(![X530]:(![X531]:(![X532]:(![X533]:((~coll(X530,X531,X532)|~coll(X530,X531,X533))|coll(X532,X533,X530)))))),inference(variable_rename,[status(thm)],[c404])).
% 121.93/122.11 cnf(c406,plain,~coll(X736,X737,X738)|~coll(X736,X737,X739)|coll(X738,X739,X736),inference(split_conjunct,[status(thm)],[c405])).
% 121.93/122.11 cnf(c495,plain,~coll(X742,X741,X740)|coll(X740,X740,X742),inference(factor,[status(thm)],[c406])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c193,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 121.93/122.11 fof(c194,plain,(![X173]:(![X174]:(![X175]:(~para(X173,X174,X173,X175)|coll(X173,X174,X175))))),inference(variable_rename,[status(thm)],[c193])).
% 121.93/122.11 cnf(c195,plain,~para(X685,X687,X685,X686)|coll(X685,X687,X686),inference(split_conjunct,[status(thm)],[c194])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c290,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])).
% 121.93/122.11 fof(c291,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)],[c290])).
% 121.93/122.11 fof(c293,plain,(![X305]:(![X306]:(![X307]:(![X308]:(![X309]:(![X310]:(~eqangle(X305,X306,X309,X310,X307,X308,X309,X310)|para(X305,X306,X307,X308)))))))),inference(shift_quantors,[status(thm)],[fof(c292,plain,(![X305]:(![X306]:(![X307]:(![X308]:((![X309]:(![X310]:~eqangle(X305,X306,X309,X310,X307,X308,X309,X310)))|para(X305,X306,X307,X308)))))),inference(variable_rename,[status(thm)],[c291])).])).
% 121.93/122.11 cnf(c294,plain,~eqangle(X1099,X1100,X1098,X1095,X1097,X1096,X1098,X1095)|para(X1099,X1100,X1097,X1096),inference(split_conjunct,[status(thm)],[c293])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c354,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])).
% 121.93/122.11 fof(c355,plain,(![X451]:(![X452]:(![X453]:(![X454]:(![X455]:(![X456]:(![X457]:(![X458]:(~eqangle(X451,X452,X453,X454,X455,X456,X457,X458)|eqangle(X453,X454,X451,X452,X457,X458,X455,X456)))))))))),inference(variable_rename,[status(thm)],[c354])).
% 121.93/122.11 cnf(c356,plain,~eqangle(X1248,X1247,X1244,X1241,X1245,X1246,X1243,X1242)|eqangle(X1244,X1241,X1248,X1247,X1243,X1242,X1245,X1246),inference(split_conjunct,[status(thm)],[c355])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c285,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])).
% 121.93/122.11 fof(c286,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)],[c285])).
% 121.93/122.11 fof(c288,plain,(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(~para(X299,X300,X301,X302)|eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))))))),inference(shift_quantors,[status(thm)],[fof(c287,plain,(![X299]:(![X300]:(![X301]:(![X302]:(~para(X299,X300,X301,X302)|(![X303]:(![X304]:eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))))))),inference(variable_rename,[status(thm)],[c286])).])).
% 121.93/122.11 cnf(c289,plain,~para(X1087,X1089,X1092,X1088)|eqangle(X1087,X1089,X1091,X1090,X1092,X1088,X1091,X1090),inference(split_conjunct,[status(thm)],[c288])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c386,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])).
% 121.93/122.11 fof(c387,plain,(![X502]:(![X503]:(![X504]:(![X505]:(![X506]:(![X507]:((~perp(X502,X503,X504,X505)|~perp(X504,X505,X506,X507))|para(X502,X503,X506,X507)))))))),inference(variable_rename,[status(thm)],[c386])).
% 121.93/122.11 cnf(c388,plain,~perp(X1277,X1279,X1282,X1280)|~perp(X1282,X1280,X1278,X1281)|para(X1277,X1279,X1278,X1281),inference(split_conjunct,[status(thm)],[c387])).
% 121.93/122.11 cnf(c18,negated_conjecture,circle(skolem0002,skolem0003,skolem0004,skolem0013),inference(split_conjunct,[status(thm)],[c15])).
% 121.93/122.11 fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 121.93/122.11 fof(c76,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 121.93/122.11 fof(c77,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c76])).
% 121.93/122.11 fof(c78,plain,(![X61]:(![X62]:(![X63]:(![X64]:(~circle(X64,X61,X62,X63)|(?[X65]:perp(X65,X61,X61,X64))))))),inference(variable_rename,[status(thm)],[c77])).
% 121.93/122.11 fof(c79,plain,(![X61]:(![X62]:(![X63]:(![X64]:(~circle(X64,X61,X62,X63)|perp(skolem0026(X61,X62,X63,X64),X61,X61,X64)))))),inference(skolemize,[status(esa)],[c78])).
% 121.93/122.11 cnf(c80,plain,~circle(X792,X793,X794,X791)|perp(skolem0026(X793,X794,X791,X792),X793,X793,X792),inference(split_conjunct,[status(thm)],[c79])).
% 121.93/122.11 cnf(c709,plain,perp(skolem0026(skolem0003,skolem0004,skolem0013,skolem0002),skolem0003,skolem0003,skolem0002),inference(resolution,[status(thm)],[c80, c18])).
% 121.93/122.11 cnf(c2478,plain,~perp(X3837,X3838,skolem0026(skolem0003,skolem0004,skolem0013,skolem0002),skolem0003)|para(X3837,X3838,skolem0003,skolem0002),inference(resolution,[status(thm)],[c709, c388])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 121.93/122.11 fof(c390,plain,(![X508]:(![X509]:(![X510]:(![X511]:(~perp(X508,X509,X510,X511)|perp(X510,X511,X508,X509)))))),inference(variable_rename,[status(thm)],[c389])).
% 121.93/122.11 cnf(c391,plain,~perp(X711,X714,X712,X713)|perp(X712,X713,X711,X714),inference(split_conjunct,[status(thm)],[c390])).
% 121.93/122.11 cnf(c2490,plain,perp(skolem0003,skolem0002,skolem0026(skolem0003,skolem0004,skolem0013,skolem0002),skolem0003),inference(resolution,[status(thm)],[c709, c391])).
% 121.93/122.11 cnf(c9518,plain,para(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c2490, c2478])).
% 121.93/122.11 cnf(c9594,plain,eqangle(skolem0003,skolem0002,X5065,X5066,skolem0003,skolem0002,X5065,X5066),inference(resolution,[status(thm)],[c9518, c289])).
% 121.93/122.11 cnf(c12869,plain,eqangle(X5102,X5101,skolem0003,skolem0002,X5102,X5101,skolem0003,skolem0002),inference(resolution,[status(thm)],[c9594, c356])).
% 121.93/122.11 cnf(c13010,plain,para(X5106,X5107,X5106,X5107),inference(resolution,[status(thm)],[c12869, c294])).
% 121.93/122.11 cnf(c13026,plain,coll(X5108,X5109,X5109),inference(resolution,[status(thm)],[c13010, c195])).
% 121.93/122.11 cnf(c13052,plain,coll(X5110,X5110,X5111),inference(resolution,[status(thm)],[c13026, c495])).
% 121.93/122.11 cnf(c13786,plain,~coll(X7565,X7565,X7564)|coll(X7564,X7563,X7565),inference(resolution,[status(thm)],[c13052, c406])).
% 121.93/122.11 cnf(c24391,plain,coll(X7566,X7568,X7567),inference(resolution,[status(thm)],[c13786, c13052])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c190,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 121.93/122.11 fof(c191,plain,(![X170]:(![X171]:(![X172]:((~cong(X170,X171,X170,X172)|~coll(X170,X171,X172))|midp(X170,X171,X172))))),inference(variable_rename,[status(thm)],[c190])).
% 121.93/122.11 cnf(c192,plain,~cong(X943,X945,X943,X944)|~coll(X943,X945,X944)|midp(X943,X945,X944),inference(split_conjunct,[status(thm)],[c191])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c342,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 121.93/122.11 fof(c343,plain,(![X419]:(![X420]:(![X421]:(![X422]:(~cong(X419,X420,X421,X422)|cong(X419,X420,X422,X421)))))),inference(variable_rename,[status(thm)],[c342])).
% 121.93/122.11 cnf(c344,plain,~cong(X692,X693,X694,X695)|cong(X692,X693,X695,X694),inference(split_conjunct,[status(thm)],[c343])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 121.93/122.11 fof(c340,plain,(![X415]:(![X416]:(![X417]:(![X418]:(~cong(X415,X416,X417,X418)|cong(X417,X418,X415,X416)))))),inference(variable_rename,[status(thm)],[c339])).
% 121.93/122.11 cnf(c341,plain,~cong(X691,X688,X689,X690)|cong(X689,X690,X691,X688),inference(split_conjunct,[status(thm)],[c340])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c199,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])).
% 121.93/122.11 fof(c200,plain,(![X181]:(![X182]:(![X183]:(![X184]:(![X185]:(((~midp(X185,X181,X182)|~para(X181,X183,X182,X184))|~para(X181,X184,X182,X183))|midp(X185,X183,X184))))))),inference(variable_rename,[status(thm)],[c199])).
% 121.93/122.11 cnf(c201,plain,~midp(X955,X953,X952)|~para(X953,X951,X952,X954)|~para(X953,X954,X952,X951)|midp(X955,X951,X954),inference(split_conjunct,[status(thm)],[c200])).
% 121.93/122.11 cnf(c1071,plain,~midp(X2180,X2183,X2182)|~para(X2183,X2181,X2182,X2181)|midp(X2180,X2181,X2181),inference(factor,[status(thm)],[c201])).
% 121.93/122.11 cnf(c13035,plain,~midp(X7267,X7268,X7268)|midp(X7267,X7269,X7269),inference(resolution,[status(thm)],[c13010, c1071])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c275,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])).
% 121.93/122.11 fof(c276,plain,(![X287]:(![X288]:(![X289]:(![X290]:((~eqangle(X289,X287,X289,X288,X290,X287,X290,X288)|~coll(X289,X290,X288))|cyclic(X287,X288,X289,X290)))))),inference(variable_rename,[status(thm)],[c275])).
% 121.93/122.11 cnf(c277,plain,~eqangle(X1075,X1073,X1075,X1074,X1072,X1073,X1072,X1074)|~coll(X1075,X1072,X1074)|cyclic(X1073,X1074,X1075,X1072),inference(split_conjunct,[status(thm)],[c276])).
% 121.93/122.11 cnf(c13046,plain,eqangle(X7272,X7271,X7270,X7273,X7272,X7271,X7270,X7273),inference(resolution,[status(thm)],[c13010, c289])).
% 121.93/122.11 cnf(c24046,plain,~coll(X8011,X8011,X8012)|cyclic(X8013,X8012,X8011,X8011),inference(resolution,[status(thm)],[c13046, c277])).
% 121.93/122.11 cnf(c25528,plain,cyclic(X8014,X8016,X8015,X8015),inference(resolution,[status(thm)],[c24046, c24391])).
% 121.93/122.11 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)).
% 121.93/122.11 fof(c270,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])).
% 121.93/122.11 fof(c271,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)],[c270])).
% 121.93/122.11 fof(c273,plain,(![X281]:(![X282]:(![X283]:(![X284]:(![X285]:(![X286]:((((~cyclic(X281,X282,X283,X284)|~cyclic(X281,X282,X283,X285))|~cyclic(X281,X282,X283,X286))|~eqangle(X283,X281,X283,X282,X286,X284,X286,X285))|cong(X281,X282,X284,X285)))))))),inference(shift_quantors,[status(thm)],[fof(c272,plain,(![X281]:(![X282]:(![X283]:(![X284]:(![X285]:((![X286]:(((~cyclic(X281,X282,X283,X284)|~cyclic(X281,X282,X283,X285))|~cyclic(X281,X282,X283,X286))|~eqangle(X283,X281,X283,X282,X286,X284,X286,X285)))|cong(X281,X282,X284,X285))))))),inference(variable_rename,[status(thm)],[c271])).])).
% 121.93/122.11 cnf(c274,plain,~cyclic(X1067,X1069,X1064,X1065)|~cyclic(X1067,X1069,X1064,X1068)|~cyclic(X1067,X1069,X1064,X1066)|~eqangle(X1064,X1067,X1064,X1069,X1066,X1065,X1066,X1068)|cong(X1067,X1069,X1065,X1068),inference(split_conjunct,[status(thm)],[c273])).
% 121.93/122.11 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)).
% 121.93/122.12 fof(c351,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])).
% 121.93/122.12 fof(c352,plain,(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(~eqangle(X443,X444,X445,X446,X447,X448,X449,X450)|eqangle(X447,X448,X449,X450,X443,X444,X445,X446)))))))))),inference(variable_rename,[status(thm)],[c351])).
% 121.93/122.12 cnf(c353,plain,~eqangle(X1233,X1237,X1236,X1234,X1238,X1240,X1239,X1235)|eqangle(X1238,X1240,X1239,X1235,X1233,X1237,X1236,X1234),inference(split_conjunct,[status(thm)],[c352])).
% 121.93/122.12 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)).
% 121.93/122.12 fof(c348,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])).
% 121.93/122.12 fof(c349,plain,(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(~eqangle(X435,X436,X437,X438,X439,X440,X441,X442)|eqangle(X435,X436,X439,X440,X437,X438,X441,X442)))))))))),inference(variable_rename,[status(thm)],[c348])).
% 121.93/122.12 cnf(c350,plain,~eqangle(X1232,X1228,X1225,X1231,X1230,X1227,X1226,X1229)|eqangle(X1232,X1228,X1230,X1227,X1225,X1231,X1226,X1229),inference(split_conjunct,[status(thm)],[c349])).
% 121.93/122.12 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)).
% 121.93/122.12 fof(c401,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 121.93/122.12 fof(c402,plain,(![X526]:(![X527]:(![X528]:(![X529]:(~para(X526,X527,X528,X529)|para(X526,X527,X529,X528)))))),inference(variable_rename,[status(thm)],[c401])).
% 121.93/122.12 cnf(c403,plain,~para(X726,X723,X725,X724)|para(X726,X723,X724,X725),inference(split_conjunct,[status(thm)],[c402])).
% 121.93/122.12 cnf(c13037,plain,para(X5127,X5128,X5128,X5127),inference(resolution,[status(thm)],[c13010, c403])).
% 121.93/122.12 cnf(c14801,plain,eqangle(X7764,X7765,X7763,X7766,X7765,X7764,X7763,X7766),inference(resolution,[status(thm)],[c13037, c289])).
% 121.93/122.12 cnf(c24843,plain,eqangle(X7801,X7802,X7802,X7801,X7803,X7800,X7803,X7800),inference(resolution,[status(thm)],[c14801, c350])).
% 121.93/122.12 cnf(c24981,plain,eqangle(X7857,X7855,X7857,X7855,X7856,X7858,X7858,X7856),inference(resolution,[status(thm)],[c24843, c353])).
% 121.93/122.12 cnf(c25115,plain,~cyclic(X8995,X8995,X8996,X8997)|cong(X8995,X8995,X8997,X8997),inference(resolution,[status(thm)],[c24981, c274])).
% 121.93/122.12 cnf(c26110,plain,cong(X9001,X9001,X9002,X9002),inference(resolution,[status(thm)],[c25115, c25528])).
% 121.93/122.12 cnf(c26127,plain,~coll(X9052,X9052,X9052)|midp(X9052,X9052,X9052),inference(resolution,[status(thm)],[c26110, c192])).
% 121.93/122.12 cnf(c26233,plain,midp(X9056,X9056,X9056),inference(resolution,[status(thm)],[c26127, c24391])).
% 121.93/122.12 cnf(c26518,plain,midp(X9058,X9059,X9059),inference(resolution,[status(thm)],[c26233, c13035])).
% 121.93/122.12 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)).
% 121.93/122.12 fof(c242,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])).
% 121.93/122.12 fof(c243,plain,(![X241]:(![X242]:(![X243]:(![X244]:((~perp(X241,X242,X242,X243)|~midp(X244,X241,X243))|cong(X241,X244,X242,X244)))))),inference(variable_rename,[status(thm)],[c242])).
% 121.93/122.12 cnf(c244,plain,~perp(X1007,X1008,X1008,X1005)|~midp(X1006,X1007,X1005)|cong(X1007,X1006,X1008,X1006),inference(split_conjunct,[status(thm)],[c243])).
% 121.93/122.12 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)).
% 121.93/122.12 fof(c163,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])).
% 121.93/122.12 fof(c164,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)],[c163])).
% 121.93/122.12 fof(c166,plain,(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:(![X139]:(![X140]:(![X141]:((~eqangle(X134,X135,X136,X137,X138,X139,X140,X141)|~perp(X138,X139,X140,X141))|perp(X134,X135,X136,X137)))))))))),inference(shift_quantors,[status(thm)],[fof(c165,plain,(![X134]:(![X135]:(![X136]:(![X137]:((![X138]:(![X139]:(![X140]:(![X141]:(~eqangle(X134,X135,X136,X137,X138,X139,X140,X141)|~perp(X138,X139,X140,X141))))))|perp(X134,X135,X136,X137)))))),inference(variable_rename,[status(thm)],[c164])).])).
% 121.93/122.12 cnf(c167,plain,~eqangle(X913,X915,X918,X914,X916,X917,X920,X919)|~perp(X916,X917,X920,X919)|perp(X913,X915,X918,X914),inference(split_conjunct,[status(thm)],[c166])).
% 121.93/122.12 cnf(c24984,plain,~perp(X8979,X8976,X8979,X8976)|perp(X8977,X8978,X8978,X8977),inference(resolution,[status(thm)],[c24843, c167])).
% 121.93/122.12 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)).
% 121.93/122.12 fof(c228,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])).
% 121.93/122.12 fof(c229,plain,(![X225]:(![X226]:(![X227]:(![X228]:((~cong(X225,X227,X226,X227)|~cong(X225,X228,X226,X228))|perp(X225,X226,X227,X228)))))),inference(variable_rename,[status(thm)],[c228])).
% 121.93/122.12 cnf(c230,plain,~cong(X990,X991,X989,X991)|~cong(X990,X992,X989,X992)|perp(X990,X989,X991,X992),inference(split_conjunct,[status(thm)],[c229])).
% 121.93/122.12 cnf(c1074,plain,~cong(X1013,X1012,X1014,X1012)|perp(X1013,X1014,X1012,X1012),inference(factor,[status(thm)],[c230])).
% 121.93/122.12 cnf(c26149,plain,perp(X9019,X9019,X9019,X9019),inference(resolution,[status(thm)],[c26110, c1074])).
% 121.93/122.12 cnf(c26157,plain,perp(X9025,X9026,X9026,X9025),inference(resolution,[status(thm)],[c26149, c24984])).
% 121.93/122.12 cnf(c26195,plain,~midp(X9796,X9794,X9794)|cong(X9794,X9796,X9795,X9796),inference(resolution,[status(thm)],[c26157, c244])).
% 121.93/122.12 cnf(c27948,plain,cong(X9798,X9799,X9797,X9799),inference(resolution,[status(thm)],[c26195, c26518])).
% 121.93/122.12 cnf(c27954,plain,cong(X9808,X9809,X9809,X9810),inference(resolution,[status(thm)],[c27948, c344])).
% 121.93/122.12 cnf(c27987,plain,cong(X9818,X9817,X9816,X9818),inference(resolution,[status(thm)],[c27954, c341])).
% 121.93/122.12 cnf(c28040,plain,cong(X9846,X9844,X9846,X9845),inference(resolution,[status(thm)],[c27987, c344])).
% 121.93/122.12 cnf(c28121,plain,~coll(X9978,X9977,X9979)|midp(X9978,X9977,X9979),inference(resolution,[status(thm)],[c28040, c192])).
% 121.93/122.12 cnf(c29854,plain,midp(X9981,X9980,X9982),inference(resolution,[status(thm)],[c28121, c24391])).
% 121.93/122.12 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)).
% 121.93/122.12 fof(c267,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])).
% 121.93/122.12 fof(c268,plain,(![X276]:(![X277]:(![X278]:(![X279]:(![X280]:((~midp(X279,X276,X277)|~midp(X280,X276,X278))|para(X279,X280,X277,X278))))))),inference(variable_rename,[status(thm)],[c267])).
% 121.93/122.12 cnf(c269,plain,~midp(X1057,X1059,X1056)|~midp(X1055,X1059,X1058)|para(X1057,X1055,X1056,X1058),inference(split_conjunct,[status(thm)],[c268])).
% 121.93/122.12 cnf(c26836,plain,~midp(X12970,X12969,X12972)|para(X12970,X12971,X12972,X12969),inference(resolution,[status(thm)],[c26518, c269])).
% 121.93/122.12 cnf(c31811,plain,para(X12976,X12978,X12979,X12977),inference(resolution,[status(thm)],[c26836, c29854])).
% 121.93/122.12 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)).
% 121.93/122.12 fof(c383,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])).
% 121.93/122.12 fof(c384,plain,(![X496]:(![X497]:(![X498]:(![X499]:(![X500]:(![X501]:((~para(X496,X497,X498,X499)|~perp(X498,X499,X500,X501))|perp(X496,X497,X500,X501)))))))),inference(variable_rename,[status(thm)],[c383])).
% 121.93/122.12 cnf(c385,plain,~para(X1273,X1276,X1275,X1271)|~perp(X1275,X1271,X1274,X1272)|perp(X1273,X1276,X1274,X1272),inference(split_conjunct,[status(thm)],[c384])).
% 121.93/122.12 cnf(c26183,plain,~para(X14977,X14980,X14978,X14979)|perp(X14977,X14980,X14979,X14978),inference(resolution,[status(thm)],[c26157, c385])).
% 121.93/122.12 cnf(c32496,plain,perp(X14982,X14984,X14981,X14983),inference(resolution,[status(thm)],[c26183, c31811])).
% 121.93/122.12 cnf(c32497,plain,$false,inference(resolution,[status(thm)],[c32496, c27])).
% 121.93/122.12 % SZS output end CNFRefutation
% 121.93/122.12
% 121.93/122.12 % Initial clauses : 139
% 121.93/122.12 % Processed clauses : 3748
% 121.93/122.12 % Factors computed : 205
% 121.93/122.12 % Resolvents computed: 31881
% 121.93/122.12 % Tautologies deleted: 12
% 121.93/122.12 % Forward subsumed : 10602
% 121.93/122.12 % Backward subsumed : 3567
% 121.93/122.12 % -------- CPU Time ---------
% 121.93/122.12 % User time : 121.684 s
% 121.93/122.12 % System time : 0.075 s
% 121.93/122.12 % Total time : 121.759 s
%------------------------------------------------------------------------------