%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO607+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:22:23 EDT 2024
% Result : Theorem 12.26s 12.52s
% Output : Refutation 12.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : GEO607+1 : TPTP v8.1.2. Released v7.5.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n029.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 08:04:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 12.26/12.52 % Version: 1.5
% 12.26/12.52 % SZS status Theorem
% 12.26/12.52 % SZS output start CNFRefutation
% 12.26/12.52 fof(exemplo6GDDFULL618069,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((((midp(C,B,A)&perp(D,A,D,B))&circle(E,A,C,D))&circle(F,B,D,C))=>perp(E,D,D,F)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL618069)).
% 12.26/12.52 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((((midp(C,B,A)&perp(D,A,D,B))&circle(E,A,C,D))&circle(F,B,D,C))=>perp(E,D,D,F))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618069])).
% 12.26/12.52 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:((((midp(C,B,A)&perp(D,A,D,B))&circle(E,A,C,D))&circle(F,B,D,C))&~perp(E,D,D,F)))))))),inference(fof_nnf,[status(thm)],[c11])).
% 12.26/12.52 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:((((midp(X4,X3,X2)&perp(X5,X2,X5,X3))&circle(X6,X2,X4,X5))&circle(X7,X3,X5,X4))&~perp(X6,X5,X5,X7)))))))),inference(variable_rename,[status(thm)],[c12])).
% 12.26/12.52 fof(c14,negated_conjecture,((((midp(skolem0003,skolem0002,skolem0001)&perp(skolem0004,skolem0001,skolem0004,skolem0002))&circle(skolem0005,skolem0001,skolem0003,skolem0004))&circle(skolem0006,skolem0002,skolem0004,skolem0003))&~perp(skolem0005,skolem0004,skolem0004,skolem0006)),inference(skolemize,[status(esa)],[c13])).
% 12.26/12.52 cnf(c19,negated_conjecture,~perp(skolem0005,skolem0004,skolem0004,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 12.26/12.52 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)).
% 12.26/12.52 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(fof_nnf,[status(thm)],[ruleD74])).
% 12.26/12.52 fof(c156,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)],[c155])).
% 12.26/12.52 fof(c158,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(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(variable_rename,[status(thm)],[c156])).])).
% 12.26/12.52 cnf(c159,plain,~eqangle(X932,X933,X929,X931,X930,X934,X936,X935)|~perp(X930,X934,X936,X935)|perp(X932,X933,X929,X931),inference(split_conjunct,[status(thm)],[c158])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c277,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])).
% 12.26/12.52 fof(c278,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)],[c277])).
% 12.26/12.52 fof(c280,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(c279,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)],[c278])).])).
% 12.26/12.52 cnf(c281,plain,~para(X1089,X1091,X1092,X1088)|eqangle(X1089,X1091,X1093,X1090,X1092,X1088,X1093,X1090),inference(split_conjunct,[status(thm)],[c280])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c393,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 12.26/12.52 fof(c394,plain,(![X515]:(![X516]:(![X517]:(![X518]:(~para(X515,X516,X517,X518)|para(X515,X516,X518,X517)))))),inference(variable_rename,[status(thm)],[c393])).
% 12.26/12.52 cnf(c395,plain,~para(X711,X709,X710,X712)|para(X711,X709,X712,X710),inference(split_conjunct,[status(thm)],[c394])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c282,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])).
% 12.26/12.52 fof(c283,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)],[c282])).
% 12.26/12.52 fof(c285,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(c284,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)],[c283])).])).
% 12.26/12.52 cnf(c286,plain,~eqangle(X1098,X1096,X1099,X1097,X1094,X1095,X1099,X1097)|para(X1098,X1096,X1094,X1095),inference(split_conjunct,[status(thm)],[c285])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c346,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])).
% 12.26/12.52 fof(c347,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)],[c346])).
% 12.26/12.52 cnf(c348,plain,~eqangle(X1250,X1255,X1254,X1256,X1251,X1253,X1257,X1252)|eqangle(X1254,X1256,X1250,X1255,X1257,X1252,X1251,X1253),inference(split_conjunct,[status(thm)],[c347])).
% 12.26/12.52 cnf(c15,negated_conjecture,midp(skolem0003,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 12.26/12.52 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 12.26/12.52 fof(c372,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 12.26/12.52 fof(c373,plain,(![X482]:(![X483]:(![X484]:(~midp(X484,X483,X482)|midp(X484,X482,X483))))),inference(variable_rename,[status(thm)],[c372])).
% 12.26/12.52 cnf(c374,plain,~midp(X549,X550,X548)|midp(X549,X548,X550),inference(split_conjunct,[status(thm)],[c373])).
% 12.26/12.52 cnf(c410,plain,midp(skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c374, c15])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c194,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])).
% 12.26/12.52 fof(c195,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c194])).
% 12.26/12.52 fof(c197,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(c196,plain,(![X175]:(![X176]:(![X177]:(![X178]:((![X179]:(~midp(X179,X175,X176)|~midp(X179,X177,X178)))|para(X175,X177,X176,X178)))))),inference(variable_rename,[status(thm)],[c195])).])).
% 12.26/12.52 cnf(c198,plain,~midp(X976,X977,X979)|~midp(X976,X978,X975)|para(X977,X978,X979,X975),inference(split_conjunct,[status(thm)],[c197])).
% 12.26/12.52 cnf(c928,plain,~midp(skolem0003,X1278,X1277)|para(X1278,skolem0001,X1277,skolem0002),inference(resolution,[status(thm)],[c198, c410])).
% 12.26/12.52 cnf(c1352,plain,para(skolem0002,skolem0001,skolem0001,skolem0002),inference(resolution,[status(thm)],[c928, c15])).
% 12.26/12.52 cnf(c1358,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1352, c395])).
% 12.26/12.52 cnf(c1378,plain,eqangle(skolem0002,skolem0001,X1458,X1457,skolem0002,skolem0001,X1458,X1457),inference(resolution,[status(thm)],[c1358, c281])).
% 12.26/12.52 cnf(c1755,plain,eqangle(X1570,X1571,skolem0002,skolem0001,X1570,X1571,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1378, c348])).
% 12.26/12.52 cnf(c2136,plain,para(X1572,X1573,X1572,X1573),inference(resolution,[status(thm)],[c1755, c286])).
% 12.26/12.52 cnf(c2149,plain,para(X1597,X1596,X1596,X1597),inference(resolution,[status(thm)],[c2136, c395])).
% 12.26/12.52 cnf(c2313,plain,eqangle(X1873,X1870,X1871,X1872,X1870,X1873,X1871,X1872),inference(resolution,[status(thm)],[c2149, c281])).
% 12.26/12.52 cnf(c2812,plain,~perp(X2841,X2840,X2839,X2838)|perp(X2840,X2841,X2839,X2838),inference(resolution,[status(thm)],[c2313, c159])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c220,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])).
% 12.26/12.52 fof(c221,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)],[c220])).
% 12.26/12.52 cnf(c222,plain,~cong(X1011,X1009,X1008,X1009)|~cong(X1011,X1010,X1008,X1010)|perp(X1011,X1008,X1009,X1010),inference(split_conjunct,[status(thm)],[c221])).
% 12.26/12.52 cnf(c1021,plain,~cong(X1102,X1101,X1100,X1101)|perp(X1102,X1100,X1101,X1101),inference(factor,[status(thm)],[c222])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 12.26/12.52 fof(c397,plain,(![X519]:(![X520]:(![X521]:(![X522]:((~coll(X519,X520,X521)|~coll(X519,X520,X522))|coll(X521,X522,X519)))))),inference(variable_rename,[status(thm)],[c396])).
% 12.26/12.52 cnf(c398,plain,~coll(X722,X724,X725)|~coll(X722,X724,X723)|coll(X725,X723,X722),inference(split_conjunct,[status(thm)],[c397])).
% 12.26/12.52 cnf(c486,plain,~coll(X728,X727,X726)|coll(X726,X726,X728),inference(factor,[status(thm)],[c398])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c185,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 12.26/12.52 fof(c186,plain,(![X162]:(![X163]:(![X164]:(~para(X162,X163,X162,X164)|coll(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c185])).
% 12.26/12.52 cnf(c187,plain,~para(X591,X590,X591,X592)|coll(X591,X590,X592),inference(split_conjunct,[status(thm)],[c186])).
% 12.26/12.52 cnf(c2158,plain,coll(X1574,X1575,X1575),inference(resolution,[status(thm)],[c2136, c187])).
% 12.26/12.52 cnf(c2163,plain,coll(X1579,X1579,X1580),inference(resolution,[status(thm)],[c2158, c486])).
% 12.26/12.52 cnf(c2228,plain,~coll(X1816,X1816,X1815)|coll(X1815,X1817,X1816),inference(resolution,[status(thm)],[c2163, c398])).
% 12.26/12.52 cnf(c2770,plain,coll(X1819,X1820,X1818),inference(resolution,[status(thm)],[c2228, c2163])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c182,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 12.26/12.52 fof(c183,plain,(![X159]:(![X160]:(![X161]:((~cong(X159,X160,X159,X161)|~coll(X159,X160,X161))|midp(X159,X160,X161))))),inference(variable_rename,[status(thm)],[c182])).
% 12.26/12.52 cnf(c184,plain,~cong(X964,X962,X964,X963)|~coll(X964,X962,X963)|midp(X964,X962,X963),inference(split_conjunct,[status(thm)],[c183])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 12.26/12.52 fof(c362,plain,(![X469]:(![X470]:(![X471]:(![X472]:(~cyclic(X469,X470,X471,X472)|cyclic(X469,X470,X472,X471)))))),inference(variable_rename,[status(thm)],[c361])).
% 12.26/12.52 cnf(c363,plain,~cyclic(X660,X657,X659,X658)|cyclic(X660,X657,X658,X659),inference(split_conjunct,[status(thm)],[c362])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c355,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 12.26/12.52 fof(c356,plain,(![X461]:(![X462]:(![X463]:(![X464]:(~cyclic(X461,X462,X463,X464)|cyclic(X462,X461,X463,X464)))))),inference(variable_rename,[status(thm)],[c355])).
% 12.26/12.52 cnf(c357,plain,~cyclic(X651,X652,X650,X649)|cyclic(X652,X651,X650,X649),inference(split_conjunct,[status(thm)],[c356])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c358,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 12.26/12.52 fof(c359,plain,(![X465]:(![X466]:(![X467]:(![X468]:(~cyclic(X465,X466,X467,X468)|cyclic(X465,X467,X466,X468)))))),inference(variable_rename,[status(thm)],[c358])).
% 12.26/12.52 cnf(c360,plain,~cyclic(X654,X655,X656,X653)|cyclic(X654,X656,X655,X653),inference(split_conjunct,[status(thm)],[c359])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c267,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])).
% 12.26/12.52 fof(c268,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)],[c267])).
% 12.26/12.52 cnf(c269,plain,~eqangle(X1072,X1071,X1072,X1073,X1070,X1071,X1070,X1073)|~coll(X1072,X1070,X1073)|cyclic(X1071,X1073,X1072,X1070),inference(split_conjunct,[status(thm)],[c268])).
% 12.26/12.52 cnf(c2157,plain,eqangle(X1756,X1759,X1757,X1758,X1756,X1759,X1757,X1758),inference(resolution,[status(thm)],[c2136, c281])).
% 12.26/12.52 cnf(c2713,plain,~coll(X2055,X2055,X2056)|cyclic(X2057,X2056,X2055,X2055),inference(resolution,[status(thm)],[c2157, c269])).
% 12.26/12.52 cnf(c2908,plain,cyclic(X2059,X2060,X2058,X2058),inference(resolution,[status(thm)],[c2713, c2770])).
% 12.26/12.52 cnf(c2915,plain,cyclic(X2064,X2066,X2065,X2066),inference(resolution,[status(thm)],[c2908, c360])).
% 12.26/12.52 cnf(c2918,plain,cyclic(X2076,X2075,X2074,X2076),inference(resolution,[status(thm)],[c2915, c357])).
% 12.26/12.52 cnf(c2933,plain,cyclic(X2095,X2093,X2095,X2094),inference(resolution,[status(thm)],[c2918, c363])).
% 12.26/12.52 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)).
% 12.26/12.52 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(fof_nnf,[status(thm)],[ruleD43])).
% 12.26/12.52 fof(c263,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)],[c262])).
% 12.26/12.52 fof(c265,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(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(variable_rename,[status(thm)],[c263])).])).
% 12.26/12.52 cnf(c266,plain,~cyclic(X1067,X1064,X1069,X1068)|~cyclic(X1067,X1064,X1069,X1066)|~cyclic(X1067,X1064,X1069,X1065)|~eqangle(X1069,X1067,X1069,X1064,X1065,X1068,X1065,X1066)|cong(X1067,X1064,X1068,X1066),inference(split_conjunct,[status(thm)],[c265])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c343,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])).
% 12.26/12.52 fof(c344,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)],[c343])).
% 12.26/12.52 cnf(c345,plain,~eqangle(X1248,X1244,X1242,X1245,X1247,X1246,X1241,X1243)|eqangle(X1247,X1246,X1241,X1243,X1248,X1244,X1242,X1245),inference(split_conjunct,[status(thm)],[c344])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c340,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])).
% 12.26/12.52 fof(c341,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)],[c340])).
% 12.26/12.52 cnf(c342,plain,~eqangle(X1232,X1237,X1239,X1238,X1233,X1234,X1235,X1236)|eqangle(X1232,X1237,X1233,X1234,X1239,X1238,X1235,X1236),inference(split_conjunct,[status(thm)],[c341])).
% 12.26/12.52 cnf(c2804,plain,eqangle(X1902,X1904,X1904,X1902,X1903,X1905,X1903,X1905),inference(resolution,[status(thm)],[c2313, c342])).
% 12.26/12.52 cnf(c2837,plain,eqangle(X1951,X1952,X1951,X1952,X1950,X1953,X1953,X1950),inference(resolution,[status(thm)],[c2804, c345])).
% 12.26/12.52 cnf(c2862,plain,~cyclic(X2907,X2907,X2908,X2906)|cong(X2907,X2907,X2906,X2906),inference(resolution,[status(thm)],[c2837, c266])).
% 12.26/12.52 cnf(c3469,plain,cong(X2909,X2909,X2910,X2910),inference(resolution,[status(thm)],[c2862, c2933])).
% 12.26/12.52 cnf(c3495,plain,~coll(X2967,X2967,X2967)|midp(X2967,X2967,X2967),inference(resolution,[status(thm)],[c3469, c184])).
% 12.26/12.52 cnf(c3572,plain,midp(X2968,X2968,X2968),inference(resolution,[status(thm)],[c3495, c2770])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c191,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])).
% 12.26/12.52 fof(c192,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)],[c191])).
% 12.26/12.52 cnf(c193,plain,~midp(X970,X971,X973)|~para(X971,X974,X973,X972)|~para(X971,X972,X973,X974)|midp(X970,X974,X972),inference(split_conjunct,[status(thm)],[c192])).
% 12.26/12.52 cnf(c911,plain,~midp(X3107,X3105,X3106)|~para(X3105,X3104,X3106,X3104)|midp(X3107,X3104,X3104),inference(factor,[status(thm)],[c193])).
% 12.26/12.52 cnf(c4126,plain,~midp(X3195,X3196,X3196)|midp(X3195,X3194,X3194),inference(resolution,[status(thm)],[c911, c2136])).
% 12.26/12.52 cnf(c4208,plain,midp(X3201,X3202,X3202),inference(resolution,[status(thm)],[c4126, c3572])).
% 12.26/12.52 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)).
% 12.26/12.52 fof(c234,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])).
% 12.26/12.52 fof(c235,plain,(![X230]:(![X231]:(![X232]:(![X233]:((~perp(X230,X231,X231,X232)|~midp(X233,X230,X232))|cong(X230,X233,X231,X233)))))),inference(variable_rename,[status(thm)],[c234])).
% 12.26/12.52 cnf(c236,plain,~perp(X1026,X1025,X1025,X1027)|~midp(X1024,X1026,X1027)|cong(X1026,X1024,X1025,X1024),inference(split_conjunct,[status(thm)],[c235])).
% 12.26/12.52 cnf(c2842,plain,~perp(X2879,X2878,X2879,X2878)|perp(X2880,X2877,X2877,X2880),inference(resolution,[status(thm)],[c2804, c159])).
% 12.26/12.52 cnf(c3483,plain,perp(X2925,X2925,X2925,X2925),inference(resolution,[status(thm)],[c3469, c1021])).
% 12.26/12.52 cnf(c3508,plain,perp(X2933,X2934,X2934,X2933),inference(resolution,[status(thm)],[c3483, c2842])).
% 12.26/12.52 cnf(c3530,plain,~midp(X3864,X3865,X3865)|cong(X3865,X3864,X3863,X3864),inference(resolution,[status(thm)],[c3508, c236])).
% 12.26/12.52 cnf(c5323,plain,cong(X3866,X3868,X3867,X3868),inference(resolution,[status(thm)],[c3530, c4208])).
% 12.26/12.52 cnf(c5332,plain,perp(X3872,X3873,X3874,X3874),inference(resolution,[status(thm)],[c5323, c1021])).
% 12.26/12.52 fof(ruleD41,axiom,(![A]:(![B]:(![P]:(![Q]:(cyclic(A,B,P,Q)=>eqangle(P,A,P,B,Q,A,Q,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD41)).
% 12.26/12.52 fof(c274,plain,(![A]:(![B]:(![P]:(![Q]:(~cyclic(A,B,P,Q)|eqangle(P,A,P,B,Q,A,Q,B)))))),inference(fof_nnf,[status(thm)],[ruleD41])).
% 12.26/12.52 fof(c275,plain,(![X284]:(![X285]:(![X286]:(![X287]:(~cyclic(X284,X285,X286,X287)|eqangle(X286,X284,X286,X285,X287,X284,X287,X285)))))),inference(variable_rename,[status(thm)],[c274])).
% 12.26/12.52 cnf(c276,plain,~cyclic(X1084,X1082,X1081,X1083)|eqangle(X1081,X1084,X1081,X1082,X1083,X1084,X1083,X1082),inference(split_conjunct,[status(thm)],[c275])).
% 12.26/12.52 cnf(c2920,plain,eqangle(X2136,X2134,X2136,X2135,X2135,X2134,X2135,X2135),inference(resolution,[status(thm)],[c2915, c276])).
% 12.26/12.52 cnf(c2972,plain,~perp(X9804,X9806,X9804,X9804)|perp(X9805,X9806,X9805,X9804),inference(resolution,[status(thm)],[c2920, c159])).
% 12.26/12.52 cnf(c13005,plain,perp(X9811,X9810,X9811,X9809),inference(resolution,[status(thm)],[c2972, c5332])).
% 12.26/12.52 cnf(c13014,plain,perp(X9817,X9818,X9818,X9816),inference(resolution,[status(thm)],[c13005, c2812])).
% 12.26/12.52 cnf(c13030,plain,$false,inference(resolution,[status(thm)],[c13014, c19])).
% 12.26/12.52 % SZS output end CNFRefutation
% 12.26/12.52
% 12.26/12.52 % Initial clauses : 132
% 12.26/12.52 % Processed clauses : 1387
% 12.26/12.52 % Factors computed : 226
% 12.26/12.52 % Resolvents computed: 12404
% 12.26/12.52 % Tautologies deleted: 28
% 12.26/12.52 % Forward subsumed : 4087
% 12.26/12.52 % Backward subsumed : 1069
% 12.26/12.52 % -------- CPU Time ---------
% 12.26/12.52 % User time : 12.135 s
% 12.26/12.52 % System time : 0.025 s
% 12.26/12.52 % Total time : 12.160 s
%------------------------------------------------------------------------------