%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO596+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:22 EDT 2024
% Result : Theorem 138.66s 138.86s
% Output : Refutation 138.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO596+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 08:26:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 138.66/138.86 % Version: 1.5
% 138.66/138.86 % SZS status Theorem
% 138.66/138.86 % SZS output start CNFRefutation
% 138.66/138.86 fof(exemplo6GDDFULL416058,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![NWPNT1]:((((((circle(D,A,B,C)&circle(D,A,E,NWPNT1))&coll(F,A,B))&coll(F,C,E))¶(A,E,G,F))&coll(G,B,C))=>eqangle(G,F,F,B,F,C,C,B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL416058)).
% 138.66/138.86 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![NWPNT1]:((((((circle(D,A,B,C)&circle(D,A,E,NWPNT1))&coll(F,A,B))&coll(F,C,E))¶(A,E,G,F))&coll(G,B,C))=>eqangle(G,F,F,B,F,C,C,B))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416058])).
% 138.66/138.86 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[NWPNT1]:((((((circle(D,A,B,C)&circle(D,A,E,NWPNT1))&coll(F,A,B))&coll(F,C,E))¶(A,E,G,F))&coll(G,B,C))&~eqangle(G,F,F,B,F,C,C,B)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 138.66/138.86 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:((((((circle(D,A,B,C)&(?[NWPNT1]:circle(D,A,E,NWPNT1)))&coll(F,A,B))&coll(F,C,E))¶(A,E,G,F))&coll(G,B,C))&~eqangle(G,F,F,B,F,C,C,B))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 138.66/138.86 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((circle(X5,X2,X3,X4)&(?[X9]:circle(X5,X2,X6,X9)))&coll(X7,X2,X3))&coll(X7,X4,X6))¶(X2,X6,X8,X7))&coll(X8,X3,X4))&~eqangle(X8,X7,X7,X3,X7,X4,X4,X3))))))))),inference(variable_rename,[status(thm)],[c13])).
% 138.66/138.86 fof(c15,negated_conjecture,((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0008))&coll(skolem0006,skolem0001,skolem0002))&coll(skolem0006,skolem0003,skolem0005))¶(skolem0001,skolem0005,skolem0007,skolem0006))&coll(skolem0007,skolem0002,skolem0003))&~eqangle(skolem0007,skolem0006,skolem0006,skolem0002,skolem0006,skolem0003,skolem0003,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 138.66/138.86 cnf(c22,negated_conjecture,~eqangle(skolem0007,skolem0006,skolem0006,skolem0002,skolem0006,skolem0003,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 138.66/138.86 fof(ruleD18,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(B,A,C,D,P,Q,U,V)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD18)).
% 138.66/138.86 fof(c352,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(B,A,C,D,P,Q,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD18])).
% 138.66/138.86 fof(c353,plain,(![X450]:(![X451]:(![X452]:(![X453]:(![X454]:(![X455]:(![X456]:(![X457]:(~eqangle(X450,X451,X452,X453,X454,X455,X456,X457)|eqangle(X451,X450,X452,X453,X454,X455,X456,X457)))))))))),inference(variable_rename,[status(thm)],[c352])).
% 138.66/138.86 cnf(c354,plain,~eqangle(X1234,X1232,X1231,X1238,X1235,X1236,X1233,X1237)|eqangle(X1232,X1234,X1231,X1238,X1235,X1236,X1233,X1237),inference(split_conjunct,[status(thm)],[c353])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 138.66/138.86 fof(c346,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])).
% 138.66/138.86 fof(c347,plain,(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(~eqangle(X434,X435,X436,X437,X438,X439,X440,X441)|eqangle(X438,X439,X440,X441,X434,X435,X436,X437)))))))))),inference(variable_rename,[status(thm)],[c346])).
% 138.66/138.86 cnf(c348,plain,~eqangle(X1221,X1219,X1216,X1222,X1215,X1220,X1217,X1218)|eqangle(X1215,X1220,X1217,X1218,X1221,X1219,X1216,X1222),inference(split_conjunct,[status(thm)],[c347])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 138.66/138.86 fof(c349,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])).
% 138.66/138.86 fof(c350,plain,(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(~eqangle(X442,X443,X444,X445,X446,X447,X448,X449)|eqangle(X444,X445,X442,X443,X448,X449,X446,X447)))))))))),inference(variable_rename,[status(thm)],[c349])).
% 138.66/138.86 cnf(c351,plain,~eqangle(X1229,X1230,X1224,X1223,X1227,X1228,X1225,X1226)|eqangle(X1224,X1223,X1229,X1230,X1225,X1226,X1227,X1228),inference(split_conjunct,[status(thm)],[c350])).
% 138.66/138.86 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 138.66/138.86 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 138.66/138.86 fof(c400,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c399])).
% 138.66/138.86 cnf(c401,plain,~coll(X723,X722,X724)|~coll(X723,X722,X721)|coll(X724,X721,X723),inference(split_conjunct,[status(thm)],[c400])).
% 138.66/138.86 cnf(c507,plain,~coll(X730,X729,X728)|coll(X728,X728,X730),inference(factor,[status(thm)],[c401])).
% 138.66/138.86 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 138.66/138.86 fof(c188,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 138.66/138.86 fof(c189,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c188])).
% 138.66/138.86 cnf(c190,plain,~para(X641,X640,X641,X642)|coll(X641,X640,X642),inference(split_conjunct,[status(thm)],[c189])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 138.66/138.86 fof(c285,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])).
% 138.66/138.86 fof(c286,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)],[c285])).
% 138.66/138.86 fof(c288,plain,(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)|para(X296,X297,X298,X299)))))))),inference(shift_quantors,[status(thm)],[fof(c287,plain,(![X296]:(![X297]:(![X298]:(![X299]:((![X300]:(![X301]:~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))|para(X296,X297,X298,X299)))))),inference(variable_rename,[status(thm)],[c286])).])).
% 138.66/138.86 cnf(c289,plain,~eqangle(X1090,X1086,X1089,X1088,X1085,X1087,X1089,X1088)|para(X1090,X1086,X1085,X1087),inference(split_conjunct,[status(thm)],[c288])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 138.66/138.86 fof(c280,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])).
% 138.66/138.86 fof(c281,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)],[c280])).
% 138.66/138.86 fof(c283,plain,(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(~para(X290,X291,X292,X293)|eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(shift_quantors,[status(thm)],[fof(c282,plain,(![X290]:(![X291]:(![X292]:(![X293]:(~para(X290,X291,X292,X293)|(![X294]:(![X295]:eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(variable_rename,[status(thm)],[c281])).])).
% 138.66/138.86 cnf(c284,plain,~para(X1081,X1084,X1083,X1079)|eqangle(X1081,X1084,X1080,X1082,X1083,X1079,X1080,X1082),inference(split_conjunct,[status(thm)],[c283])).
% 138.66/138.86 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 138.66/138.86 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 138.66/138.86 fof(c397,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c396])).
% 138.66/138.86 cnf(c398,plain,~para(X701,X700,X699,X702)|para(X701,X700,X702,X699),inference(split_conjunct,[status(thm)],[c397])).
% 138.66/138.86 fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 138.66/138.86 fof(c393,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 138.66/138.86 fof(c394,plain,(![X513]:(![X514]:(![X515]:(![X516]:(~para(X513,X514,X515,X516)|para(X515,X516,X513,X514)))))),inference(variable_rename,[status(thm)],[c393])).
% 138.66/138.86 cnf(c395,plain,~para(X697,X695,X698,X696)|para(X698,X696,X697,X695),inference(split_conjunct,[status(thm)],[c394])).
% 138.66/138.86 cnf(c20,negated_conjecture,para(skolem0001,skolem0005,skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 138.66/138.86 cnf(c468,plain,para(skolem0007,skolem0006,skolem0001,skolem0005),inference(resolution,[status(thm)],[c395, c20])).
% 138.66/138.86 cnf(c471,plain,para(skolem0007,skolem0006,skolem0005,skolem0001),inference(resolution,[status(thm)],[c398, c468])).
% 138.66/138.86 cnf(c474,plain,para(skolem0005,skolem0001,skolem0007,skolem0006),inference(resolution,[status(thm)],[c471, c395])).
% 138.66/138.86 cnf(c479,plain,para(skolem0005,skolem0001,skolem0006,skolem0007),inference(resolution,[status(thm)],[c474, c398])).
% 138.66/138.86 cnf(c472,plain,para(skolem0001,skolem0005,skolem0006,skolem0007),inference(resolution,[status(thm)],[c398, c20])).
% 138.66/138.86 cnf(c477,plain,para(skolem0006,skolem0007,skolem0001,skolem0005),inference(resolution,[status(thm)],[c472, c395])).
% 138.66/138.86 cnf(c482,plain,para(skolem0006,skolem0007,skolem0005,skolem0001),inference(resolution,[status(thm)],[c477, c398])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 138.66/138.86 fof(c390,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])).
% 138.66/138.86 fof(c391,plain,(![X507]:(![X508]:(![X509]:(![X510]:(![X511]:(![X512]:((~para(X507,X508,X509,X510)|~para(X509,X510,X511,X512))|para(X507,X508,X511,X512)))))))),inference(variable_rename,[status(thm)],[c390])).
% 138.66/138.86 cnf(c392,plain,~para(X1266,X1269,X1265,X1267)|~para(X1265,X1267,X1270,X1268)|para(X1266,X1269,X1270,X1268),inference(split_conjunct,[status(thm)],[c391])).
% 138.66/138.86 cnf(c1596,plain,~para(X3487,X3486,skolem0006,skolem0007)|para(X3487,X3486,skolem0005,skolem0001),inference(resolution,[status(thm)],[c392, c482])).
% 138.66/138.86 cnf(c5503,plain,para(skolem0005,skolem0001,skolem0005,skolem0001),inference(resolution,[status(thm)],[c1596, c479])).
% 138.66/138.86 cnf(c5529,plain,eqangle(skolem0005,skolem0001,X3502,X3501,skolem0005,skolem0001,X3502,X3501),inference(resolution,[status(thm)],[c5503, c284])).
% 138.66/138.86 cnf(c5616,plain,eqangle(X3530,X3529,skolem0005,skolem0001,X3530,X3529,skolem0005,skolem0001),inference(resolution,[status(thm)],[c5529, c351])).
% 138.66/138.86 cnf(c5701,plain,para(X3532,X3531,X3532,X3531),inference(resolution,[status(thm)],[c5616, c289])).
% 138.66/138.86 cnf(c5741,plain,coll(X3534,X3533,X3533),inference(resolution,[status(thm)],[c5701, c190])).
% 138.66/138.86 cnf(c5826,plain,coll(X3542,X3542,X3541),inference(resolution,[status(thm)],[c5741, c507])).
% 138.66/138.86 cnf(c6406,plain,~coll(X4408,X4408,X4409)|coll(X4409,X4407,X4408),inference(resolution,[status(thm)],[c5826, c401])).
% 138.66/138.86 cnf(c11038,plain,coll(X4416,X4414,X4415),inference(resolution,[status(thm)],[c6406, c5826])).
% 138.66/138.86 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 138.66/138.86 fof(c185,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 138.66/138.86 fof(c186,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c185])).
% 138.66/138.86 cnf(c187,plain,~cong(X936,X937,X936,X938)|~coll(X936,X937,X938)|midp(X936,X937,X938),inference(split_conjunct,[status(thm)],[c186])).
% 138.66/138.86 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 138.66/138.86 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 138.66/138.86 fof(c338,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c337])).
% 138.66/138.86 cnf(c339,plain,~cong(X648,X649,X647,X650)|cong(X648,X649,X650,X647),inference(split_conjunct,[status(thm)],[c338])).
% 138.66/138.86 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 138.66/138.86 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 138.66/138.86 fof(c335,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c334])).
% 138.66/138.86 cnf(c336,plain,~cong(X643,X646,X644,X645)|cong(X644,X645,X643,X646),inference(split_conjunct,[status(thm)],[c335])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 138.66/138.86 fof(c194,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])).
% 138.66/138.86 fof(c195,plain,(![X172]:(![X173]:(![X174]:(![X175]:(![X176]:(((~midp(X176,X172,X173)|~para(X172,X174,X173,X175))|~para(X172,X175,X173,X174))|midp(X176,X174,X175))))))),inference(variable_rename,[status(thm)],[c194])).
% 138.66/138.86 cnf(c196,plain,~midp(X947,X950,X948)|~para(X950,X946,X948,X949)|~para(X950,X949,X948,X946)|midp(X947,X946,X949),inference(split_conjunct,[status(thm)],[c195])).
% 138.66/138.86 cnf(c984,plain,~midp(X2162,X2160,X2159)|~para(X2160,X2161,X2159,X2161)|midp(X2162,X2161,X2161),inference(factor,[status(thm)],[c196])).
% 138.66/138.86 cnf(c5737,plain,~midp(X4274,X4273,X4273)|midp(X4274,X4272,X4272),inference(resolution,[status(thm)],[c5701, c984])).
% 138.66/138.86 fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 138.66/138.86 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 138.66/138.86 fof(c362,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c361])).
% 138.66/138.86 cnf(c363,plain,~cyclic(X668,X669,X667,X670)|cyclic(X668,X667,X669,X670),inference(split_conjunct,[status(thm)],[c362])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 138.66/138.86 fof(c270,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])).
% 138.66/138.86 fof(c271,plain,(![X278]:(![X279]:(![X280]:(![X281]:((~eqangle(X280,X278,X280,X279,X281,X278,X281,X279)|~coll(X280,X281,X279))|cyclic(X278,X279,X280,X281)))))),inference(variable_rename,[status(thm)],[c270])).
% 138.66/138.86 cnf(c272,plain,~eqangle(X1068,X1069,X1068,X1067,X1070,X1069,X1070,X1067)|~coll(X1068,X1070,X1067)|cyclic(X1069,X1067,X1068,X1070),inference(split_conjunct,[status(thm)],[c271])).
% 138.66/138.86 cnf(c5725,plain,eqangle(X4266,X4267,X4269,X4268,X4266,X4267,X4269,X4268),inference(resolution,[status(thm)],[c5701, c284])).
% 138.66/138.86 cnf(c10860,plain,~coll(X4701,X4701,X4702)|cyclic(X4703,X4702,X4701,X4701),inference(resolution,[status(thm)],[c5725, c272])).
% 138.66/138.86 cnf(c11575,plain,cyclic(X4705,X4704,X4706,X4706),inference(resolution,[status(thm)],[c10860, c11038])).
% 138.66/138.86 cnf(c11581,plain,cyclic(X4716,X4717,X4715,X4717),inference(resolution,[status(thm)],[c11575, c363])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 138.66/138.86 fof(c265,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q))|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD43])).
% 138.66/138.86 fof(c266,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:((![R]:(((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q)))|cong(A,B,P,Q))))))),inference(shift_quantors,[status(thm)],[c265])).
% 138.66/138.86 fof(c268,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276))|cong(X272,X273,X275,X276)))))))),inference(shift_quantors,[status(thm)],[fof(c267,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((![X277]:(((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276)))|cong(X272,X273,X275,X276))))))),inference(variable_rename,[status(thm)],[c266])).])).
% 138.66/138.86 cnf(c269,plain,~cyclic(X1064,X1063,X1061,X1065)|~cyclic(X1064,X1063,X1061,X1062)|~cyclic(X1064,X1063,X1061,X1066)|~eqangle(X1061,X1064,X1061,X1063,X1066,X1065,X1066,X1062)|cong(X1064,X1063,X1065,X1062),inference(split_conjunct,[status(thm)],[c268])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 138.66/138.86 fof(c343,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])).
% 138.66/138.86 fof(c344,plain,(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(~eqangle(X426,X427,X428,X429,X430,X431,X432,X433)|eqangle(X426,X427,X430,X431,X428,X429,X432,X433)))))))))),inference(variable_rename,[status(thm)],[c343])).
% 138.66/138.86 cnf(c345,plain,~eqangle(X1208,X1210,X1214,X1213,X1209,X1211,X1207,X1212)|eqangle(X1208,X1210,X1209,X1211,X1214,X1213,X1207,X1212),inference(split_conjunct,[status(thm)],[c344])).
% 138.66/138.86 cnf(c5733,plain,para(X3560,X3559,X3559,X3560),inference(resolution,[status(thm)],[c5701, c398])).
% 138.66/138.86 cnf(c6579,plain,eqangle(X4511,X4510,X4513,X4512,X4510,X4511,X4513,X4512),inference(resolution,[status(thm)],[c5733, c284])).
% 138.66/138.86 cnf(c11311,plain,eqangle(X4559,X4556,X4557,X4558,X4559,X4556,X4558,X4557),inference(resolution,[status(thm)],[c6579, c351])).
% 138.66/138.86 cnf(c11375,plain,eqangle(X4602,X4603,X4602,X4603,X4605,X4604,X4604,X4605),inference(resolution,[status(thm)],[c11311, c345])).
% 138.66/138.86 cnf(c11432,plain,~cyclic(X5516,X5516,X5515,X5517)|cong(X5516,X5516,X5517,X5517),inference(resolution,[status(thm)],[c11375, c269])).
% 138.66/138.86 cnf(c12146,plain,cong(X5518,X5518,X5518,X5518),inference(resolution,[status(thm)],[c11432, c11581])).
% 138.66/138.86 cnf(c12154,plain,~coll(X5561,X5561,X5561)|midp(X5561,X5561,X5561),inference(resolution,[status(thm)],[c12146, c187])).
% 138.66/138.86 cnf(c12263,plain,midp(X5562,X5562,X5562),inference(resolution,[status(thm)],[c12154, c11038])).
% 138.66/138.86 cnf(c12273,plain,midp(X5565,X5564,X5564),inference(resolution,[status(thm)],[c12263, c5737])).
% 138.66/138.86 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 138.66/138.86 fof(c237,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])).
% 138.66/138.86 fof(c238,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c237])).
% 138.66/138.86 cnf(c239,plain,~perp(X1020,X1022,X1022,X1023)|~midp(X1021,X1020,X1023)|cong(X1020,X1021,X1022,X1021),inference(split_conjunct,[status(thm)],[c238])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 138.66/138.86 fof(c158,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 138.66/138.86 fof(c159,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))))))|perp(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c158])).
% 138.66/138.86 fof(c161,plain,(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:((~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))|perp(X125,X126,X127,X128)))))))))),inference(shift_quantors,[status(thm)],[fof(c160,plain,(![X125]:(![X126]:(![X127]:(![X128]:((![X129]:(![X130]:(![X131]:(![X132]:(~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))))))|perp(X125,X126,X127,X128)))))),inference(variable_rename,[status(thm)],[c159])).])).
% 138.66/138.86 cnf(c162,plain,~eqangle(X911,X907,X906,X909,X905,X908,X910,X904)|~perp(X905,X908,X910,X904)|perp(X911,X907,X906,X909),inference(split_conjunct,[status(thm)],[c161])).
% 138.66/138.86 cnf(c11317,plain,eqangle(X4562,X4565,X4565,X4562,X4563,X4564,X4563,X4564),inference(resolution,[status(thm)],[c6579, c345])).
% 138.66/138.86 cnf(c11393,plain,~perp(X5510,X5511,X5510,X5511)|perp(X5508,X5509,X5509,X5508),inference(resolution,[status(thm)],[c11317, c162])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 138.66/138.86 fof(c223,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])).
% 138.66/138.86 fof(c224,plain,(![X216]:(![X217]:(![X218]:(![X219]:((~cong(X216,X218,X217,X218)|~cong(X216,X219,X217,X219))|perp(X216,X217,X218,X219)))))),inference(variable_rename,[status(thm)],[c223])).
% 138.66/138.86 cnf(c225,plain,~cong(X999,X998,X996,X998)|~cong(X999,X997,X996,X997)|perp(X999,X996,X998,X997),inference(split_conjunct,[status(thm)],[c224])).
% 138.66/138.86 cnf(c1022,plain,~cong(X1000,X1001,X1002,X1001)|perp(X1000,X1002,X1001,X1001),inference(factor,[status(thm)],[c225])).
% 138.66/138.86 cnf(c12164,plain,perp(X5529,X5529,X5529,X5529),inference(resolution,[status(thm)],[c12146, c1022])).
% 138.66/138.86 cnf(c12202,plain,perp(X5541,X5540,X5540,X5541),inference(resolution,[status(thm)],[c12164, c11393])).
% 138.66/138.86 cnf(c12218,plain,~midp(X6174,X6175,X6175)|cong(X6175,X6174,X6173,X6174),inference(resolution,[status(thm)],[c12202, c239])).
% 138.66/138.86 cnf(c13078,plain,cong(X6178,X6176,X6177,X6176),inference(resolution,[status(thm)],[c12218, c12273])).
% 138.66/138.86 cnf(c13090,plain,cong(X6181,X6180,X6180,X6179),inference(resolution,[status(thm)],[c13078, c339])).
% 138.66/138.86 cnf(c13110,plain,cong(X6199,X6198,X6200,X6199),inference(resolution,[status(thm)],[c13090, c336])).
% 138.66/138.86 cnf(c13142,plain,cong(X6217,X6215,X6217,X6216),inference(resolution,[status(thm)],[c13110, c339])).
% 138.66/138.86 cnf(c13175,plain,~coll(X6332,X6331,X6330)|midp(X6332,X6331,X6330),inference(resolution,[status(thm)],[c13142, c187])).
% 138.66/138.86 cnf(c13428,plain,midp(X6333,X6335,X6334),inference(resolution,[status(thm)],[c13175, c11038])).
% 138.66/138.86 fof(ruleD50,axiom,(![A]:(![B]:(![C]:(![O]:(![M]:((circle(O,A,B,C)&midp(M,B,C))=>eqangle(A,B,A,C,O,B,O,M))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD50)).
% 138.66/138.86 fof(c243,plain,(![A]:(![B]:(![C]:(![O]:(![M]:((~circle(O,A,B,C)|~midp(M,B,C))|eqangle(A,B,A,C,O,B,O,M))))))),inference(fof_nnf,[status(thm)],[ruleD50])).
% 138.66/138.86 fof(c244,plain,(![X241]:(![X242]:(![X243]:(![X244]:(![X245]:((~circle(X244,X241,X242,X243)|~midp(X245,X242,X243))|eqangle(X241,X242,X241,X243,X244,X242,X244,X245))))))),inference(variable_rename,[status(thm)],[c243])).
% 138.66/138.86 cnf(c245,plain,~circle(X1034,X1032,X1030,X1031)|~midp(X1033,X1030,X1031)|eqangle(X1032,X1030,X1032,X1031,X1034,X1030,X1034,X1033),inference(split_conjunct,[status(thm)],[c244])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 138.66/138.86 fof(c331,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])).
% 138.66/138.86 fof(c332,plain,(![X400]:(![X401]:(![X402]:(![X403]:(![X404]:(![X405]:((~cong(X400,X401,X402,X403)|~cong(X402,X403,X404,X405))|cong(X400,X401,X404,X405)))))))),inference(variable_rename,[status(thm)],[c331])).
% 138.66/138.86 cnf(c333,plain,~cong(X1190,X1193,X1191,X1189)|~cong(X1191,X1189,X1194,X1192)|cong(X1190,X1193,X1194,X1192),inference(split_conjunct,[status(thm)],[c332])).
% 138.66/138.86 cnf(c12147,plain,cong(X5519,X5519,X5520,X5520),inference(resolution,[status(thm)],[c11432, c11575])).
% 138.66/138.86 cnf(c12181,plain,~cong(X11453,X11455,X11454,X11454)|cong(X11453,X11455,X11456,X11456),inference(resolution,[status(thm)],[c12147, c333])).
% 138.66/138.86 cnf(c16463,plain,cong(X11460,X11462,X11461,X11461),inference(resolution,[status(thm)],[c12181, c13090])).
% 138.66/138.86 cnf(c13089,plain,~cong(X11881,X11878,X11882,X11879)|cong(X11881,X11878,X11880,X11879),inference(resolution,[status(thm)],[c13078, c333])).
% 138.66/138.86 cnf(c16560,plain,cong(X11884,X11885,X11886,X11883),inference(resolution,[status(thm)],[c13089, c16463])).
% 138.66/138.86 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD12)).
% 138.66/138.86 fof(c372,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])).
% 138.66/138.86 fof(c373,plain,(![X480]:(![X481]:(![X482]:(![X483]:((~cong(X483,X480,X483,X481)|~cong(X483,X480,X483,X482))|circle(X483,X480,X481,X482)))))),inference(variable_rename,[status(thm)],[c372])).
% 138.66/138.86 cnf(c374,plain,~cong(X1249,X1252,X1249,X1250)|~cong(X1249,X1252,X1249,X1251)|circle(X1249,X1252,X1250,X1251),inference(split_conjunct,[status(thm)],[c373])).
% 138.66/138.86 cnf(c13137,plain,~cong(X11949,X11950,X11949,X11951)|circle(X11949,X11950,X11951,X11949),inference(resolution,[status(thm)],[c13110, c374])).
% 138.66/138.86 cnf(c16634,plain,circle(X11952,X11953,X11954,X11952),inference(resolution,[status(thm)],[c13137, c16560])).
% 138.66/138.86 cnf(c16637,plain,~midp(X39635,X39633,X39634)|eqangle(X39632,X39633,X39632,X39634,X39634,X39633,X39634,X39635),inference(resolution,[status(thm)],[c16634, c245])).
% 138.66/138.86 cnf(c38826,plain,eqangle(X39639,X39637,X39639,X39636,X39636,X39637,X39636,X39638),inference(resolution,[status(thm)],[c16637, c13428])).
% 138.66/138.86 cnf(c38833,plain,eqangle(X39650,X39651,X39650,X39648,X39651,X39649,X39651,X39648),inference(resolution,[status(thm)],[c38826, c351])).
% 138.66/138.86 cnf(c38940,plain,eqangle(X39690,X39691,X39691,X39693,X39690,X39692,X39690,X39693),inference(resolution,[status(thm)],[c38833, c354])).
% 138.66/138.86 cnf(c39198,plain,eqangle(X39790,X39793,X39790,X39791,X39790,X39792,X39792,X39791),inference(resolution,[status(thm)],[c38940, c348])).
% 138.66/138.86 cnf(c39637,plain,eqangle(X39981,X39982,X39982,X39983,X39982,X39980,X39980,X39983),inference(resolution,[status(thm)],[c39198, c354])).
% 138.66/138.86 cnf(c40319,plain,$false,inference(resolution,[status(thm)],[c39637, c22])).
% 138.66/138.86 % SZS output end CNFRefutation
% 138.66/138.86
% 138.66/138.86 % Initial clauses : 134
% 138.66/138.86 % Processed clauses : 3357
% 138.66/138.86 % Factors computed : 515
% 138.66/138.86 % Resolvents computed: 39422
% 138.66/138.86 % Tautologies deleted: 40
% 138.66/138.86 % Forward subsumed : 15627
% 138.66/138.86 % Backward subsumed : 2164
% 138.66/138.86 % -------- CPU Time ---------
% 138.66/138.86 % User time : 138.439 s
% 138.66/138.86 % System time : 0.078 s
% 138.66/138.86 % Total time : 138.517 s
%------------------------------------------------------------------------------