%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO642+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:28 EDT 2024
% Result : Theorem 245.56s 245.79s
% Output : Refutation 245.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO642+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n018.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 08:37:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 245.56/245.79 % Version: 1.5
% 245.56/245.79 % SZS status Theorem
% 245.56/245.79 % SZS output start CNFRefutation
% 245.56/245.79 fof(exemplo6GDDFULL81109108,conjecture,(![A]:(![B]:(![O]:(![C]:(![P]:(![D]:(![G]:(![E]:(![F]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(((((((((((((midp(O,B,A)&circle(O,A,NWPNT1,NWPNT2))&circle(O,A,C,NWPNT3))&circle(O,A,P,NWPNT4))&circle(C,B,NWPNT5,NWPNT6))&circle(O,A,D,NWPNT7))&circle(C,B,D,NWPNT8))&coll(G,B,P))&coll(G,A,D))&coll(E,A,C))&coll(E,B,P))&coll(F,A,D))&coll(F,C,P))=>perp(E,F,A,D))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL81109108)).
% 245.56/245.79 fof(c11,negated_conjecture,(~(![A]:(![B]:(![O]:(![C]:(![P]:(![D]:(![G]:(![E]:(![F]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(((((((((((((midp(O,B,A)&circle(O,A,NWPNT1,NWPNT2))&circle(O,A,C,NWPNT3))&circle(O,A,P,NWPNT4))&circle(C,B,NWPNT5,NWPNT6))&circle(O,A,D,NWPNT7))&circle(C,B,D,NWPNT8))&coll(G,B,P))&coll(G,A,D))&coll(E,A,C))&coll(E,B,P))&coll(F,A,D))&coll(F,C,P))=>perp(E,F,A,D)))))))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL81109108])).
% 245.56/245.79 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[O]:(?[C]:(?[P]:(?[D]:(?[G]:(?[E]:(?[F]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(?[NWPNT5]:(?[NWPNT6]:(?[NWPNT7]:(?[NWPNT8]:(((((((((((((midp(O,B,A)&circle(O,A,NWPNT1,NWPNT2))&circle(O,A,C,NWPNT3))&circle(O,A,P,NWPNT4))&circle(C,B,NWPNT5,NWPNT6))&circle(O,A,D,NWPNT7))&circle(C,B,D,NWPNT8))&coll(G,B,P))&coll(G,A,D))&coll(E,A,C))&coll(E,B,P))&coll(F,A,D))&coll(F,C,P))&~perp(E,F,A,D))))))))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 245.56/245.79 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[O]:(?[C]:(?[P]:(?[D]:(?[G]:(?[E]:(?[F]:(((((((((((((midp(O,B,A)&(?[NWPNT1]:(?[NWPNT2]:circle(O,A,NWPNT1,NWPNT2))))&(?[NWPNT3]:circle(O,A,C,NWPNT3)))&(?[NWPNT4]:circle(O,A,P,NWPNT4)))&(?[NWPNT5]:(?[NWPNT6]:circle(C,B,NWPNT5,NWPNT6))))&(?[NWPNT7]:circle(O,A,D,NWPNT7)))&(?[NWPNT8]:circle(C,B,D,NWPNT8)))&coll(G,B,P))&coll(G,A,D))&coll(E,A,C))&coll(E,B,P))&coll(F,A,D))&coll(F,C,P))&~perp(E,F,A,D))))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 245.56/245.79 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:(((((((((((((midp(X4,X3,X2)&(?[X11]:(?[X12]:circle(X4,X2,X11,X12))))&(?[X13]:circle(X4,X2,X5,X13)))&(?[X14]:circle(X4,X2,X6,X14)))&(?[X15]:(?[X16]:circle(X5,X3,X15,X16))))&(?[X17]:circle(X4,X2,X7,X17)))&(?[X18]:circle(X5,X3,X7,X18)))&coll(X8,X3,X6))&coll(X8,X2,X7))&coll(X9,X2,X5))&coll(X9,X3,X6))&coll(X10,X2,X7))&coll(X10,X5,X6))&~perp(X9,X10,X2,X7))))))))))),inference(variable_rename,[status(thm)],[c13])).
% 245.56/245.79 fof(c15,negated_conjecture,(((((((((((((midp(skolem0003,skolem0002,skolem0001)&circle(skolem0003,skolem0001,skolem0010,skolem0011))&circle(skolem0003,skolem0001,skolem0004,skolem0012))&circle(skolem0003,skolem0001,skolem0005,skolem0013))&circle(skolem0004,skolem0002,skolem0014,skolem0015))&circle(skolem0003,skolem0001,skolem0006,skolem0016))&circle(skolem0004,skolem0002,skolem0006,skolem0017))&coll(skolem0007,skolem0002,skolem0005))&coll(skolem0007,skolem0001,skolem0006))&coll(skolem0008,skolem0001,skolem0004))&coll(skolem0008,skolem0002,skolem0005))&coll(skolem0009,skolem0001,skolem0006))&coll(skolem0009,skolem0004,skolem0005))&~perp(skolem0008,skolem0009,skolem0001,skolem0006)),inference(skolemize,[status(esa)],[c14])).
% 245.56/245.79 cnf(c29,negated_conjecture,~perp(skolem0008,skolem0009,skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 245.56/245.79 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)).
% 245.56/245.79 fof(c406,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 245.56/245.79 fof(c407,plain,(![X530]:(![X531]:(![X532]:(![X533]:((~coll(X530,X531,X532)|~coll(X530,X531,X533))|coll(X532,X533,X530)))))),inference(variable_rename,[status(thm)],[c406])).
% 245.56/245.79 cnf(c408,plain,~coll(X798,X799,X796)|~coll(X798,X799,X797)|coll(X796,X797,X798),inference(split_conjunct,[status(thm)],[c407])).
% 245.56/245.79 cnf(c603,plain,~coll(X800,X801,X802)|coll(X802,X802,X800),inference(factor,[status(thm)],[c408])).
% 245.56/245.79 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)).
% 245.56/245.79 fof(c195,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 245.56/245.79 fof(c196,plain,(![X173]:(![X174]:(![X175]:(~para(X173,X174,X173,X175)|coll(X173,X174,X175))))),inference(variable_rename,[status(thm)],[c195])).
% 245.56/245.79 cnf(c197,plain,~para(X721,X722,X721,X723)|coll(X721,X722,X723),inference(split_conjunct,[status(thm)],[c196])).
% 245.56/245.79 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)).
% 245.56/245.79 fof(c292,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])).
% 245.56/245.79 fof(c293,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)],[c292])).
% 245.56/245.79 fof(c295,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(c294,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)],[c293])).])).
% 245.56/245.79 cnf(c296,plain,~eqangle(X1073,X1074,X1071,X1072,X1070,X1069,X1071,X1072)|para(X1073,X1074,X1070,X1069),inference(split_conjunct,[status(thm)],[c295])).
% 245.56/245.79 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)).
% 245.56/245.79 fof(c356,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])).
% 245.56/245.79 fof(c357,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)],[c356])).
% 245.56/245.79 cnf(c358,plain,~eqangle(X1207,X1213,X1214,X1210,X1212,X1211,X1208,X1209)|eqangle(X1214,X1210,X1207,X1213,X1208,X1209,X1212,X1211),inference(split_conjunct,[status(thm)],[c357])).
% 245.56/245.79 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)).
% 245.56/245.79 fof(c287,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])).
% 245.56/245.79 fof(c288,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)],[c287])).
% 245.56/245.79 fof(c290,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(c289,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)],[c288])).])).
% 245.56/245.79 cnf(c291,plain,~para(X1064,X1068,X1065,X1066)|eqangle(X1064,X1068,X1067,X1063,X1065,X1066,X1067,X1063),inference(split_conjunct,[status(thm)],[c290])).
% 245.56/245.79 cnf(c16,negated_conjecture,midp(skolem0003,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c15])).
% 245.56/245.79 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)).
% 245.56/245.79 fof(c204,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])).
% 245.56/245.79 fof(c205,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c204])).
% 245.56/245.79 fof(c207,plain,(![X186]:(![X187]:(![X188]:(![X189]:(![X190]:((~midp(X190,X186,X187)|~midp(X190,X188,X189))|para(X186,X188,X187,X189))))))),inference(shift_quantors,[status(thm)],[fof(c206,plain,(![X186]:(![X187]:(![X188]:(![X189]:((![X190]:(~midp(X190,X186,X187)|~midp(X190,X188,X189)))|para(X186,X188,X187,X189)))))),inference(variable_rename,[status(thm)],[c205])).])).
% 245.56/245.80 cnf(c208,plain,~midp(X959,X960,X958)|~midp(X959,X956,X957)|para(X960,X956,X958,X957),inference(split_conjunct,[status(thm)],[c207])).
% 245.56/245.80 cnf(c1204,plain,~midp(X1262,X1261,X1263)|para(X1261,X1261,X1263,X1263),inference(factor,[status(thm)],[c208])).
% 245.56/245.80 cnf(c1542,plain,para(skolem0002,skolem0002,skolem0001,skolem0001),inference(resolution,[status(thm)],[c1204, c16])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c397,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])).
% 245.56/245.80 fof(c398,plain,(![X516]:(![X517]:(![X518]:(![X519]:(![X520]:(![X521]:((~para(X516,X517,X518,X519)|~para(X518,X519,X520,X521))|para(X516,X517,X520,X521)))))))),inference(variable_rename,[status(thm)],[c397])).
% 245.56/245.80 cnf(c399,plain,~para(X1252,X1254,X1251,X1253)|~para(X1251,X1253,X1249,X1250)|para(X1252,X1254,X1249,X1250),inference(split_conjunct,[status(thm)],[c398])).
% 245.56/245.80 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 245.56/245.80 fof(c382,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 245.56/245.80 fof(c383,plain,(![X493]:(![X494]:(![X495]:(~midp(X495,X494,X493)|midp(X495,X493,X494))))),inference(variable_rename,[status(thm)],[c382])).
% 245.56/245.80 cnf(c384,plain,~midp(X575,X577,X576)|midp(X575,X576,X577),inference(split_conjunct,[status(thm)],[c383])).
% 245.56/245.80 cnf(c426,plain,midp(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c384, c16])).
% 245.56/245.80 cnf(c1541,plain,para(skolem0001,skolem0001,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1204, c426])).
% 245.56/245.80 cnf(c1549,plain,~para(X2850,X2851,skolem0001,skolem0001)|para(X2850,X2851,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1541, c399])).
% 245.56/245.80 cnf(c8865,plain,para(skolem0002,skolem0002,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1549, c1542])).
% 245.56/245.80 cnf(c9304,plain,eqangle(skolem0002,skolem0002,X6888,X6889,skolem0002,skolem0002,X6888,X6889),inference(resolution,[status(thm)],[c8865, c291])).
% 245.56/245.80 cnf(c18942,plain,eqangle(X7636,X7635,skolem0002,skolem0002,X7636,X7635,skolem0002,skolem0002),inference(resolution,[status(thm)],[c9304, c358])).
% 245.56/245.80 cnf(c21333,plain,para(X7638,X7637,X7638,X7637),inference(resolution,[status(thm)],[c18942, c296])).
% 245.56/245.80 cnf(c21383,plain,coll(X7640,X7639,X7639),inference(resolution,[status(thm)],[c21333, c197])).
% 245.56/245.80 cnf(c21568,plain,coll(X7647,X7647,X7646),inference(resolution,[status(thm)],[c21383, c603])).
% 245.56/245.80 cnf(c22312,plain,~coll(X11375,X11375,X11377)|coll(X11377,X11376,X11375),inference(resolution,[status(thm)],[c21568, c408])).
% 245.56/245.80 cnf(c40102,plain,coll(X11381,X11382,X11380),inference(resolution,[status(thm)],[c22312, c21568])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c192,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 245.56/245.80 fof(c193,plain,(![X170]:(![X171]:(![X172]:((~cong(X170,X171,X170,X172)|~coll(X170,X171,X172))|midp(X170,X171,X172))))),inference(variable_rename,[status(thm)],[c192])).
% 245.56/245.80 cnf(c194,plain,~cong(X943,X944,X943,X945)|~coll(X943,X944,X945)|midp(X943,X944,X945),inference(split_conjunct,[status(thm)],[c193])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c344,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 245.56/245.80 fof(c345,plain,(![X419]:(![X420]:(![X421]:(![X422]:(~cong(X419,X420,X421,X422)|cong(X419,X420,X422,X421)))))),inference(variable_rename,[status(thm)],[c344])).
% 245.56/245.80 cnf(c346,plain,~cong(X737,X734,X735,X736)|cong(X737,X734,X736,X735),inference(split_conjunct,[status(thm)],[c345])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c341,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 245.56/245.80 fof(c342,plain,(![X415]:(![X416]:(![X417]:(![X418]:(~cong(X415,X416,X417,X418)|cong(X417,X418,X415,X416)))))),inference(variable_rename,[status(thm)],[c341])).
% 245.56/245.80 cnf(c343,plain,~cong(X730,X732,X733,X731)|cong(X733,X731,X730,X732),inference(split_conjunct,[status(thm)],[c342])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c244,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])).
% 245.56/245.80 fof(c245,plain,(![X241]:(![X242]:(![X243]:(![X244]:((~perp(X241,X242,X242,X243)|~midp(X244,X241,X243))|cong(X241,X244,X242,X244)))))),inference(variable_rename,[status(thm)],[c244])).
% 245.56/245.80 cnf(c246,plain,~perp(X1005,X1007,X1007,X1006)|~midp(X1008,X1005,X1006)|cong(X1005,X1008,X1007,X1008),inference(split_conjunct,[status(thm)],[c245])).
% 245.56/245.80 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 245.56/245.80 fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 245.56/245.80 fof(c395,plain,(![X512]:(![X513]:(![X514]:(![X515]:(~perp(X512,X513,X514,X515)|perp(X512,X513,X515,X514)))))),inference(variable_rename,[status(thm)],[c394])).
% 245.56/245.80 cnf(c396,plain,~perp(X777,X776,X774,X775)|perp(X777,X776,X775,X774),inference(split_conjunct,[status(thm)],[c395])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 245.56/245.80 fof(c392,plain,(![X508]:(![X509]:(![X510]:(![X511]:(~perp(X508,X509,X510,X511)|perp(X510,X511,X508,X509)))))),inference(variable_rename,[status(thm)],[c391])).
% 245.56/245.80 cnf(c393,plain,~perp(X770,X772,X771,X773)|perp(X771,X773,X770,X772),inference(split_conjunct,[status(thm)],[c392])).
% 245.56/245.80 fof(ruleD12,axiom,(![A]:(![B]:(![C]:(![O]:((cong(O,A,O,B)&cong(O,A,O,C))=>circle(O,A,B,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD12)).
% 245.56/245.80 fof(c379,plain,(![A]:(![B]:(![C]:(![O]:((~cong(O,A,O,B)|~cong(O,A,O,C))|circle(O,A,B,C)))))),inference(fof_nnf,[status(thm)],[ruleD12])).
% 245.56/245.80 fof(c380,plain,(![X489]:(![X490]:(![X491]:(![X492]:((~cong(X492,X489,X492,X490)|~cong(X492,X489,X492,X491))|circle(X492,X489,X490,X491)))))),inference(variable_rename,[status(thm)],[c379])).
% 245.56/245.80 cnf(c381,plain,~cong(X1235,X1234,X1235,X1233)|~cong(X1235,X1234,X1235,X1236)|circle(X1235,X1234,X1233,X1236),inference(split_conjunct,[status(thm)],[c380])).
% 245.56/245.80 cnf(c1534,plain,~cong(X1298,X1297,X1298,X1299)|circle(X1298,X1297,X1299,X1299),inference(factor,[status(thm)],[c381])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c189,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 245.56/245.80 fof(c190,plain,(![X167]:(![X168]:(![X169]:(~midp(X167,X168,X169)|cong(X167,X168,X167,X169))))),inference(variable_rename,[status(thm)],[c189])).
% 245.56/245.80 cnf(c191,plain,~midp(X718,X720,X719)|cong(X718,X720,X718,X719),inference(split_conjunct,[status(thm)],[c190])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c201,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])).
% 245.56/245.80 fof(c202,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)],[c201])).
% 245.56/245.80 cnf(c203,plain,~midp(X951,X952,X953)|~para(X952,X955,X953,X954)|~para(X952,X954,X953,X955)|midp(X951,X955,X954),inference(split_conjunct,[status(thm)],[c202])).
% 245.56/245.80 cnf(c1191,plain,~midp(X2368,X2369,X2367)|~para(X2369,X2370,X2367,X2370)|midp(X2368,X2370,X2370),inference(factor,[status(thm)],[c203])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c403,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 245.56/245.80 fof(c404,plain,(![X526]:(![X527]:(![X528]:(![X529]:(~para(X526,X527,X528,X529)|para(X526,X527,X529,X528)))))),inference(variable_rename,[status(thm)],[c403])).
% 245.56/245.80 cnf(c405,plain,~para(X783,X784,X782,X785)|para(X783,X784,X785,X782),inference(split_conjunct,[status(thm)],[c404])).
% 245.56/245.80 cnf(c1206,plain,~midp(skolem0003,X2389,X2390)|para(X2389,skolem0002,X2390,skolem0001),inference(resolution,[status(thm)],[c208, c16])).
% 245.56/245.80 cnf(c7348,plain,para(skolem0001,skolem0002,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1206, c426])).
% 245.56/245.80 cnf(c9150,plain,para(skolem0001,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c7348, c405])).
% 245.56/245.80 cnf(c9397,plain,~midp(X6905,skolem0001,skolem0001)|midp(X6905,skolem0002,skolem0002),inference(resolution,[status(thm)],[c9150, c1191])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c230,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])).
% 245.56/245.80 fof(c231,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)],[c230])).
% 245.56/245.80 cnf(c232,plain,~cong(X992,X990,X989,X990)|~cong(X992,X991,X989,X991)|perp(X992,X989,X990,X991),inference(split_conjunct,[status(thm)],[c231])).
% 245.56/245.80 cnf(c1298,plain,~cong(X1279,X1281,X1280,X1281)|perp(X1279,X1280,X1281,X1281),inference(factor,[status(thm)],[c232])).
% 245.56/245.80 cnf(c559,plain,cong(skolem0003,skolem0002,skolem0003,skolem0001),inference(resolution,[status(thm)],[c191, c16])).
% 245.56/245.80 cnf(c570,plain,cong(skolem0003,skolem0002,skolem0001,skolem0003),inference(resolution,[status(thm)],[c346, c559])).
% 245.56/245.80 cnf(c578,plain,cong(skolem0001,skolem0003,skolem0003,skolem0002),inference(resolution,[status(thm)],[c570, c343])).
% 245.56/245.80 cnf(c585,plain,cong(skolem0001,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c578, c346])).
% 245.56/245.80 cnf(c558,plain,cong(skolem0003,skolem0001,skolem0003,skolem0002),inference(resolution,[status(thm)],[c191, c426])).
% 245.56/245.80 cnf(c569,plain,cong(skolem0003,skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c346, c558])).
% 245.56/245.80 cnf(c572,plain,cong(skolem0002,skolem0003,skolem0003,skolem0001),inference(resolution,[status(thm)],[c569, c343])).
% 245.56/245.80 cnf(c582,plain,cong(skolem0002,skolem0003,skolem0001,skolem0003),inference(resolution,[status(thm)],[c572, c346])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c338,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])).
% 245.56/245.80 fof(c339,plain,(![X409]:(![X410]:(![X411]:(![X412]:(![X413]:(![X414]:((~cong(X409,X410,X411,X412)|~cong(X411,X412,X413,X414))|cong(X409,X410,X413,X414)))))))),inference(variable_rename,[status(thm)],[c338])).
% 245.56/245.80 cnf(c340,plain,~cong(X1176,X1175,X1178,X1173)|~cong(X1178,X1173,X1177,X1174)|cong(X1176,X1175,X1177,X1174),inference(split_conjunct,[status(thm)],[c339])).
% 245.56/245.80 cnf(c1522,plain,~cong(X2805,X2806,skolem0002,skolem0003)|cong(X2805,X2806,skolem0001,skolem0003),inference(resolution,[status(thm)],[c340, c582])).
% 245.56/245.80 cnf(c8798,plain,cong(skolem0001,skolem0003,skolem0001,skolem0003),inference(resolution,[status(thm)],[c1522, c585])).
% 245.56/245.80 cnf(c9201,plain,perp(skolem0001,skolem0001,skolem0003,skolem0003),inference(resolution,[status(thm)],[c8798, c1298])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c388,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])).
% 245.56/245.80 fof(c389,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)],[c388])).
% 245.56/245.80 cnf(c390,plain,~perp(X1244,X1247,X1246,X1245)|~perp(X1246,X1245,X1243,X1248)|para(X1244,X1247,X1243,X1248),inference(split_conjunct,[status(thm)],[c389])).
% 245.56/245.80 cnf(c1633,plain,perp(skolem0002,skolem0001,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1298, c582])).
% 245.56/245.80 cnf(c1642,plain,perp(skolem0003,skolem0003,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1633, c393])).
% 245.56/245.80 cnf(c1665,plain,~perp(X2995,X2994,skolem0003,skolem0003)|para(X2995,X2994,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1642, c390])).
% 245.56/245.80 cnf(c9621,plain,para(skolem0001,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1665, c9201])).
% 245.56/245.80 cnf(c9724,plain,~midp(X6914,skolem0001,skolem0002)|midp(X6914,skolem0001,skolem0001),inference(resolution,[status(thm)],[c9621, c1191])).
% 245.56/245.80 cnf(c19157,plain,midp(skolem0003,skolem0001,skolem0001),inference(resolution,[status(thm)],[c9724, c426])).
% 245.56/245.80 cnf(c19159,plain,midp(skolem0003,skolem0002,skolem0002),inference(resolution,[status(thm)],[c19157, c9397])).
% 245.56/245.80 cnf(c20,negated_conjecture,circle(skolem0004,skolem0002,skolem0014,skolem0015),inference(split_conjunct,[status(thm)],[c15])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c78,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 245.56/245.80 fof(c79,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c78])).
% 245.56/245.80 fof(c80,plain,(![X61]:(![X62]:(![X63]:(![X64]:(~circle(X64,X61,X62,X63)|(?[X65]:perp(X65,X61,X61,X64))))))),inference(variable_rename,[status(thm)],[c79])).
% 245.56/245.80 fof(c81,plain,(![X61]:(![X62]:(![X63]:(![X64]:(~circle(X64,X61,X62,X63)|perp(skolem0026(X61,X62,X63,X64),X61,X61,X64)))))),inference(skolemize,[status(esa)],[c80])).
% 245.56/245.80 cnf(c82,plain,~circle(X752,X750,X753,X751)|perp(skolem0026(X750,X753,X751,X752),X750,X750,X752),inference(split_conjunct,[status(thm)],[c81])).
% 245.56/245.80 cnf(c595,plain,perp(skolem0026(skolem0002,skolem0014,skolem0015,skolem0004),skolem0002,skolem0002,skolem0004),inference(resolution,[status(thm)],[c82, c20])).
% 245.56/245.80 cnf(c2167,plain,perp(skolem0002,skolem0004,skolem0026(skolem0002,skolem0014,skolem0015,skolem0004),skolem0002),inference(resolution,[status(thm)],[c595, c393])).
% 245.56/245.80 cnf(c2170,plain,~perp(X3565,X3564,skolem0026(skolem0002,skolem0014,skolem0015,skolem0004),skolem0002)|para(X3565,X3564,skolem0002,skolem0004),inference(resolution,[status(thm)],[c595, c390])).
% 245.56/245.80 cnf(c11732,plain,para(skolem0002,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c2170, c2167])).
% 245.56/245.80 cnf(c11739,plain,~midp(X7284,skolem0002,skolem0002)|midp(X7284,skolem0004,skolem0004),inference(resolution,[status(thm)],[c11732, c1191])).
% 245.56/245.80 cnf(c20048,plain,midp(skolem0003,skolem0004,skolem0004),inference(resolution,[status(thm)],[c11739, c19159])).
% 245.56/245.80 cnf(c21368,plain,~midp(X10841,X10842,X10842)|midp(X10841,X10843,X10843),inference(resolution,[status(thm)],[c21333, c1191])).
% 245.56/245.80 cnf(c38246,plain,midp(skolem0003,X10844,X10844),inference(resolution,[status(thm)],[c21368, c20048])).
% 245.56/245.80 cnf(c38622,plain,cong(skolem0003,X10859,skolem0003,X10859),inference(resolution,[status(thm)],[c38246, c191])).
% 245.56/245.80 cnf(c38826,plain,cong(skolem0003,X10878,X10878,skolem0003),inference(resolution,[status(thm)],[c38622, c346])).
% 245.56/245.80 cnf(c38982,plain,cong(X10901,skolem0003,skolem0003,X10901),inference(resolution,[status(thm)],[c38826, c343])).
% 245.56/245.80 cnf(c39177,plain,cong(X10938,skolem0003,X10938,skolem0003),inference(resolution,[status(thm)],[c38982, c346])).
% 245.56/245.80 cnf(c39429,plain,circle(X11000,skolem0003,skolem0003,skolem0003),inference(resolution,[status(thm)],[c39177, c1534])).
% 245.56/245.80 fof(ruleD49,axiom,(![A]:(![B]:(![C]:(![O]:(![X]:((circle(O,A,B,C)&eqangle(A,X,A,B,C,A,C,B))=>perp(O,A,A,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD49)).
% 245.56/245.80 fof(c253,plain,(![A]:(![B]:(![C]:(![O]:(![X]:((~circle(O,A,B,C)|~eqangle(A,X,A,B,C,A,C,B))|perp(O,A,A,X))))))),inference(fof_nnf,[status(thm)],[ruleD49])).
% 245.56/245.80 fof(c254,plain,(![X255]:(![X256]:(![X257]:(![X258]:(![X259]:((~circle(X258,X255,X256,X257)|~eqangle(X255,X259,X255,X256,X257,X255,X257,X256))|perp(X258,X255,X255,X259))))))),inference(variable_rename,[status(thm)],[c253])).
% 245.56/245.80 cnf(c255,plain,~circle(X1023,X1021,X1019,X1022)|~eqangle(X1021,X1020,X1021,X1019,X1022,X1021,X1022,X1019)|perp(X1023,X1021,X1021,X1020),inference(split_conjunct,[status(thm)],[c254])).
% 245.56/245.80 cnf(c21375,plain,eqangle(X11004,X11002,X11001,X11003,X11004,X11002,X11001,X11003),inference(resolution,[status(thm)],[c21333, c291])).
% 245.56/245.80 cnf(c39650,plain,~circle(X13040,X13039,X13038,X13039)|perp(X13040,X13039,X13039,X13039),inference(resolution,[status(thm)],[c21375, c255])).
% 245.56/245.80 cnf(c42302,plain,perp(X13056,skolem0003,skolem0003,skolem0003),inference(resolution,[status(thm)],[c39650, c39429])).
% 245.56/245.80 cnf(c42404,plain,perp(skolem0003,skolem0003,X13060,skolem0003),inference(resolution,[status(thm)],[c42302, c393])).
% 245.56/245.80 cnf(c42438,plain,perp(skolem0003,skolem0003,skolem0003,X13072),inference(resolution,[status(thm)],[c42404, c396])).
% 245.56/245.80 cnf(c42496,plain,perp(skolem0003,X13081,skolem0003,skolem0003),inference(resolution,[status(thm)],[c42438, c393])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c165,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])).
% 245.56/245.80 fof(c166,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)],[c165])).
% 245.56/245.80 fof(c168,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(c167,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)],[c166])).])).
% 245.56/245.80 cnf(c169,plain,~eqangle(X917,X919,X916,X913,X920,X918,X914,X915)|~perp(X920,X918,X914,X915)|perp(X917,X919,X916,X913),inference(split_conjunct,[status(thm)],[c168])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c350,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])).
% 245.56/245.80 fof(c351,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)],[c350])).
% 245.56/245.80 cnf(c352,plain,~eqangle(X1191,X1194,X1196,X1192,X1193,X1198,X1197,X1195)|eqangle(X1191,X1194,X1193,X1198,X1196,X1192,X1197,X1195),inference(split_conjunct,[status(thm)],[c351])).
% 245.56/245.80 cnf(c39664,plain,eqangle(X11709,X11708,X11709,X11708,X11706,X11707,X11706,X11707),inference(resolution,[status(thm)],[c21375, c352])).
% 245.56/245.80 cnf(c40864,plain,~perp(X13278,X13276,X13278,X13276)|perp(X13275,X13277,X13275,X13277),inference(resolution,[status(thm)],[c39664, c169])).
% 245.56/245.80 cnf(c42717,plain,perp(X13282,X13283,X13282,X13283),inference(resolution,[status(thm)],[c40864, c42496])).
% 245.56/245.80 cnf(c42740,plain,perp(X13314,X13315,X13315,X13314),inference(resolution,[status(thm)],[c42717, c396])).
% 245.56/245.80 cnf(c42778,plain,~midp(X13484,X13485,X13485)|cong(X13485,X13484,X13486,X13484),inference(resolution,[status(thm)],[c42740, c246])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c368,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 245.56/245.80 fof(c369,plain,(![X476]:(![X477]:(![X478]:(![X479]:(~cyclic(X476,X477,X478,X479)|cyclic(X476,X478,X477,X479)))))),inference(variable_rename,[status(thm)],[c368])).
% 245.56/245.80 cnf(c370,plain,~cyclic(X758,X759,X760,X761)|cyclic(X758,X760,X759,X761),inference(split_conjunct,[status(thm)],[c369])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c371,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 245.56/245.80 fof(c372,plain,(![X480]:(![X481]:(![X482]:(![X483]:(~cyclic(X480,X481,X482,X483)|cyclic(X480,X481,X483,X482)))))),inference(variable_rename,[status(thm)],[c371])).
% 245.56/245.80 cnf(c373,plain,~cyclic(X769,X767,X768,X766)|cyclic(X769,X767,X766,X768),inference(split_conjunct,[status(thm)],[c372])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c365,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 245.56/245.80 fof(c366,plain,(![X472]:(![X473]:(![X474]:(![X475]:(~cyclic(X472,X473,X474,X475)|cyclic(X473,X472,X474,X475)))))),inference(variable_rename,[status(thm)],[c365])).
% 245.56/245.80 cnf(c367,plain,~cyclic(X754,X755,X757,X756)|cyclic(X755,X754,X757,X756),inference(split_conjunct,[status(thm)],[c366])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c277,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])).
% 245.56/245.80 fof(c278,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)],[c277])).
% 245.56/245.80 cnf(c279,plain,~eqangle(X1052,X1053,X1052,X1054,X1051,X1053,X1051,X1054)|~coll(X1052,X1051,X1054)|cyclic(X1053,X1054,X1052,X1051),inference(split_conjunct,[status(thm)],[c278])).
% 245.56/245.80 cnf(c39656,plain,~coll(X11935,X11935,X11936)|cyclic(X11937,X11936,X11935,X11935),inference(resolution,[status(thm)],[c21375, c279])).
% 245.56/245.80 cnf(c41364,plain,cyclic(X11940,X11938,X11939,X11939),inference(resolution,[status(thm)],[c39656, c40102])).
% 245.56/245.80 cnf(c41381,plain,cyclic(X11952,X11950,X11951,X11950),inference(resolution,[status(thm)],[c41364, c370])).
% 245.56/245.80 cnf(c41385,plain,cyclic(X11955,X11954,X11953,X11955),inference(resolution,[status(thm)],[c41381, c367])).
% 245.56/245.80 cnf(c41394,plain,cyclic(X11970,X11968,X11970,X11969),inference(resolution,[status(thm)],[c41385, c373])).
% 245.56/245.80 cnf(c41416,plain,cyclic(X11992,X11992,X11993,X11994),inference(resolution,[status(thm)],[c41394, c370])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c272,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])).
% 245.56/245.80 fof(c273,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)],[c272])).
% 245.56/245.80 fof(c275,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(c274,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)],[c273])).])).
% 245.56/245.80 cnf(c276,plain,~cyclic(X1048,X1045,X1049,X1047)|~cyclic(X1048,X1045,X1049,X1050)|~cyclic(X1048,X1045,X1049,X1046)|~eqangle(X1049,X1048,X1049,X1045,X1046,X1047,X1046,X1050)|cong(X1048,X1045,X1047,X1050),inference(split_conjunct,[status(thm)],[c275])).
% 245.56/245.80 cnf(c21398,plain,para(X7664,X7663,X7663,X7664),inference(resolution,[status(thm)],[c21333, c405])).
% 245.56/245.80 cnf(c23724,plain,eqangle(X11633,X11631,X11630,X11632,X11631,X11633,X11630,X11632),inference(resolution,[status(thm)],[c21398, c291])).
% 245.56/245.80 cnf(c40746,plain,eqangle(X11729,X11728,X11730,X11727,X11729,X11728,X11727,X11730),inference(resolution,[status(thm)],[c23724, c358])).
% 245.56/245.80 cnf(c40882,plain,eqangle(X11786,X11785,X11786,X11785,X11784,X11783,X11783,X11784),inference(resolution,[status(thm)],[c40746, c352])).
% 245.56/245.80 cnf(c41006,plain,~cyclic(X13777,X13777,X13778,X13776)|cong(X13777,X13777,X13776,X13776),inference(resolution,[status(thm)],[c40882, c276])).
% 245.56/245.80 cnf(c43874,plain,cong(X13782,X13782,X13783,X13783),inference(resolution,[status(thm)],[c41006, c41416])).
% 245.56/245.80 cnf(c43897,plain,~coll(X13806,X13806,X13806)|midp(X13806,X13806,X13806),inference(resolution,[status(thm)],[c43874, c194])).
% 245.56/245.80 cnf(c43913,plain,midp(X13807,X13807,X13807),inference(resolution,[status(thm)],[c43897, c40102])).
% 245.56/245.80 cnf(c44338,plain,midp(X13808,X13809,X13809),inference(resolution,[status(thm)],[c43913, c21368])).
% 245.56/245.80 cnf(c44703,plain,cong(X13831,X13832,X13833,X13832),inference(resolution,[status(thm)],[c44338, c42778])).
% 245.56/245.80 cnf(c45168,plain,cong(X13861,X13860,X13860,X13859),inference(resolution,[status(thm)],[c44703, c346])).
% 245.56/245.80 cnf(c45273,plain,cong(X13902,X13901,X13900,X13902),inference(resolution,[status(thm)],[c45168, c343])).
% 245.56/245.80 cnf(c45378,plain,cong(X13936,X13934,X13936,X13935),inference(resolution,[status(thm)],[c45273, c346])).
% 245.56/245.80 cnf(c45466,plain,~coll(X14813,X14812,X14811)|midp(X14813,X14812,X14811),inference(resolution,[status(thm)],[c45378, c194])).
% 245.56/245.80 cnf(c49712,plain,midp(X14814,X14816,X14815),inference(resolution,[status(thm)],[c45466, c40102])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c269,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])).
% 245.56/245.80 fof(c270,plain,(![X276]:(![X277]:(![X278]:(![X279]:(![X280]:((~midp(X279,X276,X277)|~midp(X280,X276,X278))|para(X279,X280,X277,X278))))))),inference(variable_rename,[status(thm)],[c269])).
% 245.56/245.80 cnf(c271,plain,~midp(X1044,X1040,X1041)|~midp(X1042,X1040,X1043)|para(X1044,X1042,X1041,X1043),inference(split_conjunct,[status(thm)],[c270])).
% 245.56/245.80 cnf(c44769,plain,~midp(X18800,X18801,X18798)|para(X18800,X18799,X18798,X18801),inference(resolution,[status(thm)],[c44338, c271])).
% 245.56/245.80 cnf(c52559,plain,para(X18802,X18803,X18805,X18804),inference(resolution,[status(thm)],[c44769, c49712])).
% 245.56/245.80 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)).
% 245.56/245.80 fof(c385,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])).
% 245.56/245.80 fof(c386,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)],[c385])).
% 245.56/245.80 cnf(c387,plain,~para(X1237,X1239,X1241,X1242)|~perp(X1241,X1242,X1238,X1240)|perp(X1237,X1239,X1238,X1240),inference(split_conjunct,[status(thm)],[c386])).
% 245.56/245.80 cnf(c42744,plain,~para(X21083,X21084,X21082,X21085)|perp(X21083,X21084,X21082,X21085),inference(resolution,[status(thm)],[c42717, c387])).
% 245.56/245.80 cnf(c53226,plain,perp(X21089,X21088,X21087,X21086),inference(resolution,[status(thm)],[c42744, c52559])).
% 245.56/245.80 cnf(c53228,plain,$false,inference(resolution,[status(thm)],[c53226, c29])).
% 245.56/245.80 % SZS output end CNFRefutation
% 245.56/245.80
% 245.56/245.80 % Initial clauses : 141
% 245.56/245.80 % Processed clauses : 5749
% 245.56/245.80 % Factors computed : 252
% 245.56/245.80 % Resolvents computed: 52562
% 245.56/245.80 % Tautologies deleted: 21
% 245.56/245.80 % Forward subsumed : 17180
% 245.56/245.80 % Backward subsumed : 5521
% 245.56/245.80 % -------- CPU Time ---------
% 245.56/245.80 % User time : 245.328 s
% 245.56/245.80 % System time : 0.094 s
% 245.56/245.80 % Total time : 245.422 s
%------------------------------------------------------------------------------