%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO656+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:30 EDT 2024
% Result : Theorem 6.34s 6.56s
% Output : Refutation 6.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO656+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 07:59:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 6.34/6.56 % Version: 1.5
% 6.34/6.56 % SZS status Theorem
% 6.34/6.56 % SZS output start CNFRefutation
% 6.34/6.56 fof(exemplo6GDDFULLmoreE02314,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(((midp(D,B,A)&eqangle(E,D,D,A,E,D,D,C))&eqangle(F,D,D,B,F,D,D,C))=>para(E,F,A,B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE02314)).
% 6.34/6.56 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(((midp(D,B,A)&eqangle(E,D,D,A,E,D,D,C))&eqangle(F,D,D,B,F,D,D,C))=>para(E,F,A,B))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE02314])).
% 6.34/6.56 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(((midp(D,B,A)&eqangle(E,D,D,A,E,D,D,C))&eqangle(F,D,D,B,F,D,D,C))&~para(E,F,A,B)))))))),inference(fof_nnf,[status(thm)],[c11])).
% 6.34/6.56 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((midp(X5,X3,X2)&eqangle(X6,X5,X5,X2,X6,X5,X5,X4))&eqangle(X7,X5,X5,X3,X7,X5,X5,X4))&~para(X6,X7,X2,X3)))))))),inference(variable_rename,[status(thm)],[c12])).
% 6.34/6.56 fof(c14,negated_conjecture,(((midp(skolem0004,skolem0002,skolem0001)&eqangle(skolem0005,skolem0004,skolem0004,skolem0001,skolem0005,skolem0004,skolem0004,skolem0003))&eqangle(skolem0006,skolem0004,skolem0004,skolem0002,skolem0006,skolem0004,skolem0004,skolem0003))&~para(skolem0005,skolem0006,skolem0001,skolem0002)),inference(skolemize,[status(esa)],[c13])).
% 6.34/6.56 cnf(c18,negated_conjecture,~para(skolem0005,skolem0006,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 6.34/6.56 fof(c396,plain,(![X519]:(![X520]:(![X521]:(![X522]:((~coll(X519,X520,X521)|~coll(X519,X520,X522))|coll(X521,X522,X519)))))),inference(variable_rename,[status(thm)],[c395])).
% 6.34/6.56 cnf(c397,plain,~coll(X696,X695,X698)|~coll(X696,X695,X697)|coll(X698,X697,X696),inference(split_conjunct,[status(thm)],[c396])).
% 6.34/6.56 cnf(c457,plain,~coll(X699,X700,X701)|coll(X701,X701,X699),inference(factor,[status(thm)],[c397])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c184,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 6.34/6.56 fof(c185,plain,(![X162]:(![X163]:(![X164]:(~para(X162,X163,X162,X164)|coll(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c184])).
% 6.34/6.56 cnf(c186,plain,~para(X591,X592,X591,X590)|coll(X591,X592,X590),inference(split_conjunct,[status(thm)],[c185])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c281,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])).
% 6.34/6.56 fof(c282,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)],[c281])).
% 6.34/6.56 fof(c284,plain,(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)|para(X294,X295,X296,X297)))))))),inference(shift_quantors,[status(thm)],[fof(c283,plain,(![X294]:(![X295]:(![X296]:(![X297]:((![X298]:(![X299]:~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)))|para(X294,X295,X296,X297)))))),inference(variable_rename,[status(thm)],[c282])).])).
% 6.34/6.56 cnf(c285,plain,~eqangle(X1034,X1038,X1035,X1037,X1033,X1036,X1035,X1037)|para(X1034,X1038,X1033,X1036),inference(split_conjunct,[status(thm)],[c284])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c392,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 6.34/6.56 fof(c393,plain,(![X515]:(![X516]:(![X517]:(![X518]:(~para(X515,X516,X517,X518)|para(X515,X516,X518,X517)))))),inference(variable_rename,[status(thm)],[c392])).
% 6.34/6.56 cnf(c394,plain,~para(X687,X688,X686,X685)|para(X687,X688,X685,X686),inference(split_conjunct,[status(thm)],[c393])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 6.34/6.56 fof(c390,plain,(![X511]:(![X512]:(![X513]:(![X514]:(~para(X511,X512,X513,X514)|para(X513,X514,X511,X512)))))),inference(variable_rename,[status(thm)],[c389])).
% 6.34/6.56 cnf(c391,plain,~para(X670,X672,X669,X671)|para(X669,X671,X670,X672),inference(split_conjunct,[status(thm)],[c390])).
% 6.34/6.56 cnf(c15,negated_conjecture,midp(skolem0004,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 6.34/6.56 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 6.34/6.56 fof(c371,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 6.34/6.56 fof(c372,plain,(![X482]:(![X483]:(![X484]:(~midp(X484,X483,X482)|midp(X484,X482,X483))))),inference(variable_rename,[status(thm)],[c371])).
% 6.34/6.56 cnf(c373,plain,~midp(X542,X544,X543)|midp(X542,X543,X544),inference(split_conjunct,[status(thm)],[c372])).
% 6.34/6.56 cnf(c408,plain,midp(skolem0004,skolem0001,skolem0002),inference(resolution,[status(thm)],[c373, c15])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c193,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])).
% 6.34/6.56 fof(c194,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c193])).
% 6.34/6.56 fof(c196,plain,(![X175]:(![X176]:(![X177]:(![X178]:(![X179]:((~midp(X179,X175,X176)|~midp(X179,X177,X178))|para(X175,X177,X176,X178))))))),inference(shift_quantors,[status(thm)],[fof(c195,plain,(![X175]:(![X176]:(![X177]:(![X178]:((![X179]:(~midp(X179,X175,X176)|~midp(X179,X177,X178)))|para(X175,X177,X176,X178)))))),inference(variable_rename,[status(thm)],[c194])).])).
% 6.34/6.56 cnf(c197,plain,~midp(X917,X915,X914)|~midp(X917,X916,X918)|para(X915,X916,X914,X918),inference(split_conjunct,[status(thm)],[c196])).
% 6.34/6.56 cnf(c721,plain,~midp(skolem0004,X931,X930)|para(X931,skolem0001,X930,skolem0002),inference(resolution,[status(thm)],[c197, c408])).
% 6.34/6.56 cnf(c742,plain,para(skolem0002,skolem0001,skolem0001,skolem0002),inference(resolution,[status(thm)],[c721, c15])).
% 6.34/6.56 cnf(c745,plain,para(skolem0001,skolem0002,skolem0002,skolem0001),inference(resolution,[status(thm)],[c742, c391])).
% 6.34/6.56 cnf(c757,plain,para(skolem0001,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c745, c394])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c276,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])).
% 6.34/6.56 fof(c277,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)],[c276])).
% 6.34/6.56 fof(c279,plain,(![X288]:(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(~para(X288,X289,X290,X291)|eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(shift_quantors,[status(thm)],[fof(c278,plain,(![X288]:(![X289]:(![X290]:(![X291]:(~para(X288,X289,X290,X291)|(![X292]:(![X293]:eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(variable_rename,[status(thm)],[c277])).])).
% 6.34/6.56 cnf(c280,plain,~para(X998,X996,X993,X995)|eqangle(X998,X996,X997,X994,X993,X995,X997,X994),inference(split_conjunct,[status(thm)],[c279])).
% 6.34/6.56 cnf(c832,plain,eqangle(skolem0001,skolem0002,X1027,X1026,skolem0001,skolem0002,X1027,X1026),inference(resolution,[status(thm)],[c280, c757])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c345,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])).
% 6.34/6.56 fof(c346,plain,(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(~eqangle(X440,X441,X442,X443,X444,X445,X446,X447)|eqangle(X442,X443,X440,X441,X446,X447,X444,X445)))))))))),inference(variable_rename,[status(thm)],[c345])).
% 6.34/6.56 cnf(c347,plain,~eqangle(X1291,X1294,X1289,X1292,X1287,X1293,X1288,X1290)|eqangle(X1289,X1292,X1291,X1294,X1288,X1290,X1287,X1293),inference(split_conjunct,[status(thm)],[c346])).
% 6.34/6.56 cnf(c1455,plain,eqangle(X1443,X1442,skolem0001,skolem0002,X1443,X1442,skolem0001,skolem0002),inference(resolution,[status(thm)],[c347, c832])).
% 6.34/6.56 cnf(c1861,plain,para(X1449,X1448,X1449,X1448),inference(resolution,[status(thm)],[c1455, c285])).
% 6.34/6.56 cnf(c1882,plain,coll(X1451,X1450,X1450),inference(resolution,[status(thm)],[c1861, c186])).
% 6.34/6.56 cnf(c1894,plain,coll(X1452,X1452,X1453),inference(resolution,[status(thm)],[c1882, c457])).
% 6.34/6.56 cnf(c1919,plain,~coll(X1640,X1640,X1639)|coll(X1639,X1641,X1640),inference(resolution,[status(thm)],[c1894, c397])).
% 6.34/6.56 cnf(c2164,plain,coll(X1648,X1649,X1650),inference(resolution,[status(thm)],[c1919, c1894])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c181,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 6.34/6.56 fof(c182,plain,(![X159]:(![X160]:(![X161]:((~cong(X159,X160,X159,X161)|~coll(X159,X160,X161))|midp(X159,X160,X161))))),inference(variable_rename,[status(thm)],[c181])).
% 6.34/6.56 cnf(c183,plain,~cong(X912,X913,X912,X911)|~coll(X912,X913,X911)|midp(X912,X913,X911),inference(split_conjunct,[status(thm)],[c182])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c333,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 6.34/6.56 fof(c334,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X408,X409,X411,X410)))))),inference(variable_rename,[status(thm)],[c333])).
% 6.34/6.56 cnf(c335,plain,~cong(X599,X597,X598,X600)|cong(X599,X597,X600,X598),inference(split_conjunct,[status(thm)],[c334])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c330,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 6.34/6.56 fof(c331,plain,(![X404]:(![X405]:(![X406]:(![X407]:(~cong(X404,X405,X406,X407)|cong(X406,X407,X404,X405)))))),inference(variable_rename,[status(thm)],[c330])).
% 6.34/6.56 cnf(c332,plain,~cong(X596,X593,X594,X595)|cong(X594,X595,X596,X593),inference(split_conjunct,[status(thm)],[c331])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c233,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])).
% 6.34/6.56 fof(c234,plain,(![X230]:(![X231]:(![X232]:(![X233]:((~perp(X230,X231,X231,X232)|~midp(X233,X230,X232))|cong(X230,X233,X231,X233)))))),inference(variable_rename,[status(thm)],[c233])).
% 6.34/6.56 cnf(c235,plain,~perp(X1143,X1141,X1141,X1144)|~midp(X1142,X1143,X1144)|cong(X1143,X1142,X1141,X1142),inference(split_conjunct,[status(thm)],[c234])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c154,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])).
% 6.34/6.56 fof(c155,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)],[c154])).
% 6.34/6.56 fof(c157,plain,(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:((~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))|perp(X123,X124,X125,X126)))))))))),inference(shift_quantors,[status(thm)],[fof(c156,plain,(![X123]:(![X124]:(![X125]:(![X126]:((![X127]:(![X128]:(![X129]:(![X130]:(~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))))))|perp(X123,X124,X125,X126)))))),inference(variable_rename,[status(thm)],[c155])).])).
% 6.34/6.56 cnf(c158,plain,~eqangle(X965,X961,X959,X963,X964,X962,X958,X960)|~perp(X964,X962,X958,X960)|perp(X965,X961,X959,X963),inference(split_conjunct,[status(thm)],[c157])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c339,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])).
% 6.34/6.56 fof(c340,plain,(![X424]:(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(~eqangle(X424,X425,X426,X427,X428,X429,X430,X431)|eqangle(X424,X425,X428,X429,X426,X427,X430,X431)))))))))),inference(variable_rename,[status(thm)],[c339])).
% 6.34/6.56 cnf(c341,plain,~eqangle(X1276,X1274,X1275,X1272,X1278,X1273,X1271,X1277)|eqangle(X1276,X1274,X1278,X1273,X1275,X1272,X1271,X1277),inference(split_conjunct,[status(thm)],[c340])).
% 6.34/6.56 cnf(c1887,plain,para(X1476,X1477,X1477,X1476),inference(resolution,[status(thm)],[c1861, c394])).
% 6.34/6.56 cnf(c1958,plain,eqangle(X1679,X1680,X1681,X1678,X1680,X1679,X1681,X1678),inference(resolution,[status(thm)],[c1887, c280])).
% 6.34/6.56 cnf(c2185,plain,eqangle(X1718,X1717,X1717,X1718,X1716,X1719,X1716,X1719),inference(resolution,[status(thm)],[c1958, c341])).
% 6.34/6.56 cnf(c2217,plain,~perp(X2671,X2673,X2671,X2673)|perp(X2674,X2672,X2672,X2674),inference(resolution,[status(thm)],[c2185, c158])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c219,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])).
% 6.34/6.56 fof(c220,plain,(![X214]:(![X215]:(![X216]:(![X217]:((~cong(X214,X216,X215,X216)|~cong(X214,X217,X215,X217))|perp(X214,X215,X216,X217)))))),inference(variable_rename,[status(thm)],[c219])).
% 6.34/6.56 cnf(c221,plain,~cong(X1125,X1122,X1124,X1122)|~cong(X1125,X1123,X1124,X1123)|perp(X1125,X1124,X1122,X1123),inference(split_conjunct,[status(thm)],[c220])).
% 6.34/6.56 cnf(c952,plain,~cong(X1130,X1132,X1131,X1132)|perp(X1130,X1131,X1132,X1132),inference(factor,[status(thm)],[c221])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 6.34/6.56 fof(c361,plain,(![X469]:(![X470]:(![X471]:(![X472]:(~cyclic(X469,X470,X471,X472)|cyclic(X469,X470,X472,X471)))))),inference(variable_rename,[status(thm)],[c360])).
% 6.34/6.56 cnf(c362,plain,~cyclic(X657,X659,X660,X658)|cyclic(X657,X659,X658,X660),inference(split_conjunct,[status(thm)],[c361])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c357,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 6.34/6.56 fof(c358,plain,(![X465]:(![X466]:(![X467]:(![X468]:(~cyclic(X465,X466,X467,X468)|cyclic(X465,X467,X466,X468)))))),inference(variable_rename,[status(thm)],[c357])).
% 6.34/6.56 cnf(c359,plain,~cyclic(X653,X654,X656,X655)|cyclic(X653,X656,X654,X655),inference(split_conjunct,[status(thm)],[c358])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c266,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])).
% 6.34/6.56 fof(c267,plain,(![X276]:(![X277]:(![X278]:(![X279]:((~eqangle(X278,X276,X278,X277,X279,X276,X279,X277)|~coll(X278,X279,X277))|cyclic(X276,X277,X278,X279)))))),inference(variable_rename,[status(thm)],[c266])).
% 6.34/6.56 cnf(c268,plain,~eqangle(X1184,X1183,X1184,X1181,X1182,X1183,X1182,X1181)|~coll(X1184,X1182,X1181)|cyclic(X1183,X1181,X1184,X1182),inference(split_conjunct,[status(thm)],[c267])).
% 6.34/6.56 cnf(c1879,plain,eqangle(X1594,X1593,X1595,X1592,X1594,X1593,X1595,X1592),inference(resolution,[status(thm)],[c1861, c280])).
% 6.34/6.56 cnf(c2131,plain,~coll(X1855,X1855,X1856)|cyclic(X1854,X1856,X1855,X1855),inference(resolution,[status(thm)],[c1879, c268])).
% 6.34/6.56 cnf(c2280,plain,cyclic(X1861,X1862,X1863,X1863),inference(resolution,[status(thm)],[c2131, c2164])).
% 6.34/6.56 cnf(c2285,plain,cyclic(X1868,X1867,X1869,X1867),inference(resolution,[status(thm)],[c2280, c359])).
% 6.34/6.56 cnf(c2290,plain,cyclic(X1874,X1875,X1875,X1873),inference(resolution,[status(thm)],[c2285, c362])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c261,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])).
% 6.34/6.56 fof(c262,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)],[c261])).
% 6.34/6.56 fof(c264,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274))|cong(X270,X271,X273,X274)))))))),inference(shift_quantors,[status(thm)],[fof(c263,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:((![X275]:(((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274)))|cong(X270,X271,X273,X274))))))),inference(variable_rename,[status(thm)],[c262])).])).
% 6.34/6.56 cnf(c265,plain,~cyclic(X1177,X1179,X1175,X1178)|~cyclic(X1177,X1179,X1175,X1176)|~cyclic(X1177,X1179,X1175,X1180)|~eqangle(X1175,X1177,X1175,X1179,X1180,X1178,X1180,X1176)|cong(X1177,X1179,X1178,X1176),inference(split_conjunct,[status(thm)],[c264])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c342,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])).
% 6.34/6.56 fof(c343,plain,(![X432]:(![X433]:(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(~eqangle(X432,X433,X434,X435,X436,X437,X438,X439)|eqangle(X436,X437,X438,X439,X432,X433,X434,X435)))))))))),inference(variable_rename,[status(thm)],[c342])).
% 6.34/6.56 cnf(c344,plain,~eqangle(X1280,X1284,X1279,X1283,X1281,X1285,X1286,X1282)|eqangle(X1281,X1285,X1286,X1282,X1280,X1284,X1279,X1283),inference(split_conjunct,[status(thm)],[c343])).
% 6.34/6.56 cnf(c2210,plain,eqangle(X1755,X1756,X1755,X1756,X1757,X1758,X1758,X1757),inference(resolution,[status(thm)],[c2185, c344])).
% 6.34/6.56 cnf(c2242,plain,~cyclic(X2695,X2695,X2696,X2697)|cong(X2695,X2695,X2697,X2697),inference(resolution,[status(thm)],[c2210, c265])).
% 6.34/6.56 cnf(c2847,plain,cong(X2701,X2701,X2700,X2700),inference(resolution,[status(thm)],[c2242, c2290])).
% 6.34/6.56 cnf(c2865,plain,perp(X2716,X2716,X2716,X2716),inference(resolution,[status(thm)],[c2847, c952])).
% 6.34/6.56 cnf(c2881,plain,perp(X2723,X2722,X2722,X2723),inference(resolution,[status(thm)],[c2865, c2217])).
% 6.34/6.56 cnf(c2913,plain,~midp(X2976,X2975,X2975)|cong(X2975,X2976,X2977,X2976),inference(resolution,[status(thm)],[c2881, c235])).
% 6.34/6.56 cnf(c2869,plain,~coll(X2751,X2751,X2751)|midp(X2751,X2751,X2751),inference(resolution,[status(thm)],[c2847, c183])).
% 6.34/6.56 cnf(c2946,plain,midp(X2752,X2752,X2752),inference(resolution,[status(thm)],[c2869, c2164])).
% 6.34/6.56 cnf(c3645,plain,cong(X2978,X2978,X2979,X2978),inference(resolution,[status(thm)],[c2913, c2946])).
% 6.34/6.56 cnf(c3650,plain,cong(X2980,X2980,X2980,X2981),inference(resolution,[status(thm)],[c3645, c335])).
% 6.34/6.56 cnf(c3679,plain,~coll(X3407,X3407,X3406)|midp(X3407,X3407,X3406),inference(resolution,[status(thm)],[c3650, c183])).
% 6.34/6.56 cnf(c4676,plain,midp(X3410,X3410,X3409),inference(resolution,[status(thm)],[c3679, c2164])).
% 6.34/6.56 fof(ruleD73,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((eqangle(A,B,C,D,P,Q,U,V)¶(P,Q,U,V))=>para(A,B,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD73)).
% 6.34/6.56 fof(c159,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~para(P,Q,U,V))|para(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD73])).
% 6.34/6.56 fof(c160,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~para(P,Q,U,V))))))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c159])).
% 6.34/6.56 fof(c162,plain,(![X131]:(![X132]:(![X133]:(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:((~eqangle(X131,X132,X133,X134,X135,X136,X137,X138)|~para(X135,X136,X137,X138))|para(X131,X132,X133,X134)))))))))),inference(shift_quantors,[status(thm)],[fof(c161,plain,(![X131]:(![X132]:(![X133]:(![X134]:((![X135]:(![X136]:(![X137]:(![X138]:(~eqangle(X131,X132,X133,X134,X135,X136,X137,X138)|~para(X135,X136,X137,X138))))))|para(X131,X132,X133,X134)))))),inference(variable_rename,[status(thm)],[c160])).])).
% 6.34/6.56 cnf(c163,plain,~eqangle(X976,X975,X974,X969,X970,X973,X971,X972)|~para(X970,X973,X971,X972)|para(X976,X975,X974,X969),inference(split_conjunct,[status(thm)],[c162])).
% 6.34/6.56 cnf(c2178,plain,~para(X2627,X2629,X2628,X2626)|para(X2629,X2627,X2628,X2626),inference(resolution,[status(thm)],[c1958, c163])).
% 6.34/6.56 fof(ruleD46,axiom,(![A]:(![B]:(![O]:(cong(O,A,O,B)=>eqangle(O,A,A,B,A,B,O,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD46)).
% 6.34/6.56 fof(c252,plain,(![A]:(![B]:(![O]:(~cong(O,A,O,B)|eqangle(O,A,A,B,A,B,O,B))))),inference(fof_nnf,[status(thm)],[ruleD46])).
% 6.34/6.56 fof(c253,plain,(![X257]:(![X258]:(![X259]:(~cong(X259,X257,X259,X258)|eqangle(X259,X257,X257,X258,X257,X258,X259,X258))))),inference(variable_rename,[status(thm)],[c252])).
% 6.34/6.56 cnf(c254,plain,~cong(X950,X951,X950,X952)|eqangle(X950,X951,X951,X952,X951,X952,X950,X952),inference(split_conjunct,[status(thm)],[c253])).
% 6.34/6.56 cnf(c3674,plain,eqangle(X3070,X3070,X3070,X3069,X3070,X3069,X3070,X3069),inference(resolution,[status(thm)],[c3650, c254])).
% 6.34/6.56 cnf(c3864,plain,para(X3072,X3072,X3072,X3071),inference(resolution,[status(thm)],[c3674, c285])).
% 6.34/6.56 cnf(c3876,plain,para(X3073,X3074,X3073,X3073),inference(resolution,[status(thm)],[c3864, c391])).
% 6.34/6.56 cnf(c3894,plain,para(X3083,X3082,X3082,X3082),inference(resolution,[status(thm)],[c3876, c2178])).
% 6.34/6.56 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)).
% 6.34/6.56 fof(c190,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])).
% 6.34/6.56 fof(c191,plain,(![X170]:(![X171]:(![X172]:(![X173]:(![X174]:(((~midp(X174,X170,X171)|~para(X170,X172,X171,X173))|~para(X170,X173,X171,X172))|midp(X174,X172,X173))))))),inference(variable_rename,[status(thm)],[c190])).
% 6.34/6.56 cnf(c192,plain,~midp(X1041,X1040,X1043)|~para(X1040,X1042,X1043,X1039)|~para(X1040,X1039,X1043,X1042)|midp(X1041,X1042,X1039),inference(split_conjunct,[status(thm)],[c191])).
% 6.34/6.56 cnf(c907,plain,~midp(X3564,X3567,X3565)|~para(X3567,X3566,X3565,X3566)|midp(X3564,X3566,X3566),inference(factor,[status(thm)],[c192])).
% 6.34/6.56 cnf(c5219,plain,~midp(X3706,X3704,X3705)|midp(X3706,X3705,X3705),inference(resolution,[status(thm)],[c907, c3894])).
% 6.34/6.56 cnf(c5418,plain,midp(X3709,X3708,X3708),inference(resolution,[status(thm)],[c5219, c4676])).
% 6.34/6.56 cnf(c5437,plain,cong(X3712,X3713,X3714,X3713),inference(resolution,[status(thm)],[c5418, c2913])).
% 6.34/6.56 cnf(c5448,plain,cong(X3721,X3719,X3719,X3720),inference(resolution,[status(thm)],[c5437, c335])).
% 6.34/6.56 cnf(c5473,plain,cong(X3736,X3738,X3737,X3736),inference(resolution,[status(thm)],[c5448, c332])).
% 6.34/6.56 cnf(c5505,plain,cong(X3752,X3754,X3752,X3753),inference(resolution,[status(thm)],[c5473, c335])).
% 6.34/6.56 cnf(c5534,plain,~coll(X4057,X4056,X4055)|midp(X4057,X4056,X4055),inference(resolution,[status(thm)],[c5505, c183])).
% 6.34/6.56 cnf(c6105,plain,midp(X4059,X4060,X4058),inference(resolution,[status(thm)],[c5534, c2164])).
% 6.34/6.56 cnf(c4692,plain,~midp(X7230,X7232,X7231)|para(X7232,X7230,X7231,X7229),inference(resolution,[status(thm)],[c4676, c197])).
% 6.34/6.56 cnf(c8150,plain,para(X7235,X7233,X7236,X7234),inference(resolution,[status(thm)],[c4692, c6105])).
% 6.34/6.56 cnf(c8154,plain,$false,inference(resolution,[status(thm)],[c8150, c18])).
% 6.34/6.56 % SZS output end CNFRefutation
% 6.34/6.56
% 6.34/6.56 % Initial clauses : 131
% 6.34/6.56 % Processed clauses : 986
% 6.34/6.56 % Factors computed : 164
% 6.34/6.56 % Resolvents computed: 7588
% 6.34/6.56 % Tautologies deleted: 34
% 6.34/6.56 % Forward subsumed : 2547
% 6.34/6.56 % Backward subsumed : 683
% 6.34/6.56 % -------- CPU Time ---------
% 6.34/6.56 % User time : 6.203 s
% 6.34/6.56 % System time : 0.022 s
% 6.34/6.56 % Total time : 6.225 s
%------------------------------------------------------------------------------