%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO577+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:19 EDT 2024
% Result : Theorem 108.41s 108.59s
% Output : Refutation 108.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO577+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n003.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:38:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 108.41/108.59 % Version: 1.5
% 108.41/108.59 % SZS status Theorem
% 108.41/108.59 % SZS output start CNFRefutation
% 108.41/108.59 fof(exemplo6GDDFULL214039,conjecture,(![A]:(![B]:(![C]:(![I]:(![O]:(![M]:(![L1]:(![NWPNT1]:(![NWPNT2]:((((((((eqangle(I,A,A,B,I,A,A,C)&eqangle(I,B,B,C,I,B,B,A))&eqangle(I,C,C,A,I,C,C,B))&circle(O,A,B,C))&circle(O,C,M,NWPNT1))&coll(M,C,I))&perp(B,I,B,L1))&circle(O,A,L1,NWPNT2))=>para(M,L1,A,I))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL214039)).
% 108.41/108.59 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![I]:(![O]:(![M]:(![L1]:(![NWPNT1]:(![NWPNT2]:((((((((eqangle(I,A,A,B,I,A,A,C)&eqangle(I,B,B,C,I,B,B,A))&eqangle(I,C,C,A,I,C,C,B))&circle(O,A,B,C))&circle(O,C,M,NWPNT1))&coll(M,C,I))&perp(B,I,B,L1))&circle(O,A,L1,NWPNT2))=>para(M,L1,A,I)))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214039])).
% 108.41/108.59 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[I]:(?[O]:(?[M]:(?[L1]:(?[NWPNT1]:(?[NWPNT2]:((((((((eqangle(I,A,A,B,I,A,A,C)&eqangle(I,B,B,C,I,B,B,A))&eqangle(I,C,C,A,I,C,C,B))&circle(O,A,B,C))&circle(O,C,M,NWPNT1))&coll(M,C,I))&perp(B,I,B,L1))&circle(O,A,L1,NWPNT2))&~para(M,L1,A,I))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 108.41/108.59 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[I]:(?[O]:(?[M]:(?[L1]:((((((((eqangle(I,A,A,B,I,A,A,C)&eqangle(I,B,B,C,I,B,B,A))&eqangle(I,C,C,A,I,C,C,B))&circle(O,A,B,C))&(?[NWPNT1]:circle(O,C,M,NWPNT1)))&coll(M,C,I))&perp(B,I,B,L1))&(?[NWPNT2]:circle(O,A,L1,NWPNT2)))&~para(M,L1,A,I))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 108.41/108.59 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((((eqangle(X5,X2,X2,X3,X5,X2,X2,X4)&eqangle(X5,X3,X3,X4,X5,X3,X3,X2))&eqangle(X5,X4,X4,X2,X5,X4,X4,X3))&circle(X6,X2,X3,X4))&(?[X9]:circle(X6,X4,X7,X9)))&coll(X7,X4,X5))&perp(X3,X5,X3,X8))&(?[X10]:circle(X6,X2,X8,X10)))&~para(X7,X8,X2,X5))))))))),inference(variable_rename,[status(thm)],[c13])).
% 108.41/108.59 fof(c15,negated_conjecture,((((((((eqangle(skolem0004,skolem0001,skolem0001,skolem0002,skolem0004,skolem0001,skolem0001,skolem0003)&eqangle(skolem0004,skolem0002,skolem0002,skolem0003,skolem0004,skolem0002,skolem0002,skolem0001))&eqangle(skolem0004,skolem0003,skolem0003,skolem0001,skolem0004,skolem0003,skolem0003,skolem0002))&circle(skolem0005,skolem0001,skolem0002,skolem0003))&circle(skolem0005,skolem0003,skolem0006,skolem0008))&coll(skolem0006,skolem0003,skolem0004))&perp(skolem0002,skolem0004,skolem0002,skolem0007))&circle(skolem0005,skolem0001,skolem0007,skolem0009))&~para(skolem0006,skolem0007,skolem0001,skolem0004)),inference(skolemize,[status(esa)],[c14])).
% 108.41/108.59 cnf(c24,negated_conjecture,~para(skolem0006,skolem0007,skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c15])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c401,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 108.41/108.59 fof(c402,plain,(![X522]:(![X523]:(![X524]:(![X525]:((~coll(X522,X523,X524)|~coll(X522,X523,X525))|coll(X524,X525,X522)))))),inference(variable_rename,[status(thm)],[c401])).
% 108.41/108.59 cnf(c403,plain,~coll(X698,X699,X701)|~coll(X698,X699,X700)|coll(X701,X700,X698),inference(split_conjunct,[status(thm)],[c402])).
% 108.41/108.59 cnf(c458,plain,~coll(X704,X702,X703)|coll(X703,X703,X704),inference(factor,[status(thm)],[c403])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 108.41/108.59 fof(c191,plain,(![X165]:(![X166]:(![X167]:(~para(X165,X166,X165,X167)|coll(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c190])).
% 108.41/108.59 cnf(c192,plain,~para(X585,X586,X585,X587)|coll(X585,X586,X587),inference(split_conjunct,[status(thm)],[c191])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c287,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])).
% 108.41/108.59 fof(c288,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)],[c287])).
% 108.41/108.59 fof(c290,plain,(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(![X302]:(~eqangle(X297,X298,X301,X302,X299,X300,X301,X302)|para(X297,X298,X299,X300)))))))),inference(shift_quantors,[status(thm)],[fof(c289,plain,(![X297]:(![X298]:(![X299]:(![X300]:((![X301]:(![X302]:~eqangle(X297,X298,X301,X302,X299,X300,X301,X302)))|para(X297,X298,X299,X300)))))),inference(variable_rename,[status(thm)],[c288])).])).
% 108.41/108.59 cnf(c291,plain,~eqangle(X1104,X1106,X1105,X1103,X1101,X1102,X1105,X1103)|para(X1104,X1106,X1101,X1102),inference(split_conjunct,[status(thm)],[c290])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c351,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])).
% 108.41/108.59 fof(c352,plain,(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(~eqangle(X443,X444,X445,X446,X447,X448,X449,X450)|eqangle(X445,X446,X443,X444,X449,X450,X447,X448)))))))))),inference(variable_rename,[status(thm)],[c351])).
% 108.41/108.59 cnf(c353,plain,~eqangle(X1241,X1239,X1244,X1242,X1246,X1243,X1240,X1245)|eqangle(X1244,X1242,X1241,X1239,X1240,X1245,X1246,X1243),inference(split_conjunct,[status(thm)],[c352])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c282,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])).
% 108.41/108.59 fof(c283,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)],[c282])).
% 108.41/108.59 fof(c285,plain,(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(![X296]:(~para(X291,X292,X293,X294)|eqangle(X291,X292,X295,X296,X293,X294,X295,X296)))))))),inference(shift_quantors,[status(thm)],[fof(c284,plain,(![X291]:(![X292]:(![X293]:(![X294]:(~para(X291,X292,X293,X294)|(![X295]:(![X296]:eqangle(X291,X292,X295,X296,X293,X294,X295,X296)))))))),inference(variable_rename,[status(thm)],[c283])).])).
% 108.41/108.59 cnf(c286,plain,~para(X1099,X1096,X1097,X1098)|eqangle(X1099,X1096,X1095,X1100,X1097,X1098,X1095,X1100),inference(split_conjunct,[status(thm)],[c285])).
% 108.41/108.59 cnf(c22,negated_conjecture,perp(skolem0002,skolem0004,skolem0002,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 108.41/108.59 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 108.41/108.59 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 108.41/108.59 fof(c387,plain,(![X500]:(![X501]:(![X502]:(![X503]:(~perp(X500,X501,X502,X503)|perp(X502,X503,X500,X501)))))),inference(variable_rename,[status(thm)],[c386])).
% 108.41/108.59 cnf(c388,plain,~perp(X619,X618,X616,X617)|perp(X616,X617,X619,X618),inference(split_conjunct,[status(thm)],[c387])).
% 108.41/108.59 cnf(c435,plain,perp(skolem0002,skolem0007,skolem0002,skolem0004),inference(resolution,[status(thm)],[c388, c22])).
% 108.41/108.59 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 108.41/108.59 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 108.41/108.59 fof(c390,plain,(![X504]:(![X505]:(![X506]:(![X507]:(~perp(X504,X505,X506,X507)|perp(X504,X505,X507,X506)))))),inference(variable_rename,[status(thm)],[c389])).
% 108.41/108.59 cnf(c391,plain,~perp(X628,X630,X629,X631)|perp(X628,X630,X631,X629),inference(split_conjunct,[status(thm)],[c390])).
% 108.41/108.59 cnf(c438,plain,perp(skolem0002,skolem0007,skolem0004,skolem0002),inference(resolution,[status(thm)],[c391, c435])).
% 108.41/108.59 cnf(c442,plain,perp(skolem0004,skolem0002,skolem0002,skolem0007),inference(resolution,[status(thm)],[c438, c388])).
% 108.41/108.59 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 108.41/108.59 fof(c383,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])).
% 108.41/108.59 fof(c384,plain,(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:(![X499]:((~perp(X494,X495,X496,X497)|~perp(X496,X497,X498,X499))|para(X494,X495,X498,X499)))))))),inference(variable_rename,[status(thm)],[c383])).
% 108.41/108.59 cnf(c385,plain,~perp(X1279,X1277,X1280,X1275)|~perp(X1280,X1275,X1278,X1276)|para(X1279,X1277,X1278,X1276),inference(split_conjunct,[status(thm)],[c384])).
% 108.41/108.59 cnf(c1467,plain,~perp(X2514,X2515,skolem0004,skolem0002)|para(X2514,X2515,skolem0002,skolem0007),inference(resolution,[status(thm)],[c385, c442])).
% 108.41/108.59 cnf(c8243,plain,para(skolem0002,skolem0007,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1467, c438])).
% 108.41/108.59 cnf(c8956,plain,eqangle(skolem0002,skolem0007,X3577,X3576,skolem0002,skolem0007,X3577,X3576),inference(resolution,[status(thm)],[c8243, c286])).
% 108.41/108.59 cnf(c14896,plain,eqangle(X4875,X4876,skolem0002,skolem0007,X4875,X4876,skolem0002,skolem0007),inference(resolution,[status(thm)],[c8956, c353])).
% 108.41/108.59 cnf(c18028,plain,para(X4877,X4878,X4877,X4878),inference(resolution,[status(thm)],[c14896, c291])).
% 108.41/108.59 cnf(c18054,plain,coll(X4879,X4880,X4880),inference(resolution,[status(thm)],[c18028, c192])).
% 108.41/108.59 cnf(c18074,plain,coll(X4884,X4884,X4885),inference(resolution,[status(thm)],[c18054, c458])).
% 108.41/108.59 cnf(c18502,plain,~coll(X6227,X6227,X6229)|coll(X6229,X6228,X6227),inference(resolution,[status(thm)],[c18074, c403])).
% 108.41/108.59 cnf(c24945,plain,coll(X6233,X6234,X6232),inference(resolution,[status(thm)],[c18502, c18074])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c187,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 108.41/108.59 fof(c188,plain,(![X162]:(![X163]:(![X164]:((~cong(X162,X163,X162,X164)|~coll(X162,X163,X164))|midp(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c187])).
% 108.41/108.59 cnf(c189,plain,~cong(X967,X966,X967,X965)|~coll(X967,X966,X965)|midp(X967,X966,X965),inference(split_conjunct,[status(thm)],[c188])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 108.41/108.59 fof(c340,plain,(![X411]:(![X412]:(![X413]:(![X414]:(~cong(X411,X412,X413,X414)|cong(X411,X412,X414,X413)))))),inference(variable_rename,[status(thm)],[c339])).
% 108.41/108.59 cnf(c341,plain,~cong(X603,X602,X600,X601)|cong(X603,X602,X601,X600),inference(split_conjunct,[status(thm)],[c340])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 108.41/108.59 fof(c337,plain,(![X407]:(![X408]:(![X409]:(![X410]:(~cong(X407,X408,X409,X410)|cong(X409,X410,X407,X408)))))),inference(variable_rename,[status(thm)],[c336])).
% 108.41/108.59 cnf(c338,plain,~cong(X588,X591,X590,X589)|cong(X590,X589,X588,X591),inference(split_conjunct,[status(thm)],[c337])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c196,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])).
% 108.41/108.59 fof(c197,plain,(![X173]:(![X174]:(![X175]:(![X176]:(![X177]:(((~midp(X177,X173,X174)|~para(X173,X175,X174,X176))|~para(X173,X176,X174,X175))|midp(X177,X175,X176))))))),inference(variable_rename,[status(thm)],[c196])).
% 108.41/108.59 cnf(c198,plain,~midp(X975,X976,X977)|~para(X976,X974,X977,X973)|~para(X976,X973,X977,X974)|midp(X975,X974,X973),inference(split_conjunct,[status(thm)],[c197])).
% 108.41/108.59 cnf(c969,plain,~midp(X1963,X1964,X1962)|~para(X1964,X1961,X1962,X1961)|midp(X1963,X1961,X1961),inference(factor,[status(thm)],[c198])).
% 108.41/108.59 cnf(c18053,plain,~midp(X6020,X6022,X6022)|midp(X6020,X6021,X6021),inference(resolution,[status(thm)],[c18028, c969])).
% 108.41/108.59 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 108.41/108.59 fof(c366,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 108.41/108.59 fof(c367,plain,(![X472]:(![X473]:(![X474]:(![X475]:(~cyclic(X472,X473,X474,X475)|cyclic(X472,X473,X475,X474)))))),inference(variable_rename,[status(thm)],[c366])).
% 108.41/108.59 cnf(c368,plain,~cyclic(X612,X614,X615,X613)|cyclic(X612,X614,X613,X615),inference(split_conjunct,[status(thm)],[c367])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 108.41/108.59 fof(c364,plain,(![X468]:(![X469]:(![X470]:(![X471]:(~cyclic(X468,X469,X470,X471)|cyclic(X468,X470,X469,X471)))))),inference(variable_rename,[status(thm)],[c363])).
% 108.41/108.59 cnf(c365,plain,~cyclic(X609,X611,X608,X610)|cyclic(X609,X608,X611,X610),inference(split_conjunct,[status(thm)],[c364])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c272,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])).
% 108.41/108.59 fof(c273,plain,(![X279]:(![X280]:(![X281]:(![X282]:((~eqangle(X281,X279,X281,X280,X282,X279,X282,X280)|~coll(X281,X282,X280))|cyclic(X279,X280,X281,X282)))))),inference(variable_rename,[status(thm)],[c272])).
% 108.41/108.59 cnf(c274,plain,~eqangle(X1085,X1084,X1085,X1086,X1083,X1084,X1083,X1086)|~coll(X1085,X1083,X1086)|cyclic(X1084,X1086,X1085,X1083),inference(split_conjunct,[status(thm)],[c273])).
% 108.41/108.59 cnf(c18060,plain,eqangle(X6023,X6026,X6025,X6024,X6023,X6026,X6025,X6024),inference(resolution,[status(thm)],[c18028, c286])).
% 108.41/108.59 cnf(c24710,plain,~coll(X6574,X6574,X6572)|cyclic(X6573,X6572,X6574,X6574),inference(resolution,[status(thm)],[c18060, c274])).
% 108.41/108.59 cnf(c25507,plain,cyclic(X6578,X6580,X6579,X6579),inference(resolution,[status(thm)],[c24710, c24945])).
% 108.41/108.59 cnf(c25508,plain,cyclic(X6581,X6583,X6582,X6583),inference(resolution,[status(thm)],[c25507, c365])).
% 108.41/108.59 cnf(c25520,plain,cyclic(X6601,X6599,X6599,X6600),inference(resolution,[status(thm)],[c25508, c368])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c267,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])).
% 108.41/108.59 fof(c268,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)],[c267])).
% 108.41/108.59 fof(c270,plain,(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:(![X278]:((((~cyclic(X273,X274,X275,X276)|~cyclic(X273,X274,X275,X277))|~cyclic(X273,X274,X275,X278))|~eqangle(X275,X273,X275,X274,X278,X276,X278,X277))|cong(X273,X274,X276,X277)))))))),inference(shift_quantors,[status(thm)],[fof(c269,plain,(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((![X278]:(((~cyclic(X273,X274,X275,X276)|~cyclic(X273,X274,X275,X277))|~cyclic(X273,X274,X275,X278))|~eqangle(X275,X273,X275,X274,X278,X276,X278,X277)))|cong(X273,X274,X276,X277))))))),inference(variable_rename,[status(thm)],[c268])).])).
% 108.41/108.59 cnf(c271,plain,~cyclic(X1080,X1077,X1078,X1079)|~cyclic(X1080,X1077,X1078,X1081)|~cyclic(X1080,X1077,X1078,X1076)|~eqangle(X1078,X1080,X1078,X1077,X1076,X1079,X1076,X1081)|cong(X1080,X1077,X1079,X1081),inference(split_conjunct,[status(thm)],[c270])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c345,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])).
% 108.41/108.59 fof(c346,plain,(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(![X434]:(~eqangle(X427,X428,X429,X430,X431,X432,X433,X434)|eqangle(X427,X428,X431,X432,X429,X430,X433,X434)))))))))),inference(variable_rename,[status(thm)],[c345])).
% 108.41/108.59 cnf(c347,plain,~eqangle(X1229,X1226,X1230,X1223,X1225,X1228,X1227,X1224)|eqangle(X1229,X1226,X1225,X1228,X1230,X1223,X1227,X1224),inference(split_conjunct,[status(thm)],[c346])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 108.41/108.59 fof(c399,plain,(![X518]:(![X519]:(![X520]:(![X521]:(~para(X518,X519,X520,X521)|para(X518,X519,X521,X520)))))),inference(variable_rename,[status(thm)],[c398])).
% 108.41/108.59 cnf(c400,plain,~para(X678,X676,X677,X679)|para(X678,X676,X679,X677),inference(split_conjunct,[status(thm)],[c399])).
% 108.41/108.59 cnf(c18073,plain,para(X4903,X4904,X4904,X4903),inference(resolution,[status(thm)],[c18028, c400])).
% 108.41/108.59 cnf(c19218,plain,eqangle(X6376,X6373,X6375,X6374,X6373,X6376,X6375,X6374),inference(resolution,[status(thm)],[c18073, c286])).
% 108.41/108.59 cnf(c25241,plain,eqangle(X6411,X6412,X6410,X6413,X6411,X6412,X6413,X6410),inference(resolution,[status(thm)],[c19218, c353])).
% 108.41/108.59 cnf(c25304,plain,eqangle(X6465,X6467,X6465,X6467,X6466,X6464,X6464,X6466),inference(resolution,[status(thm)],[c25241, c347])).
% 108.41/108.59 cnf(c25373,plain,~cyclic(X7513,X7513,X7514,X7512)|cong(X7513,X7513,X7512,X7512),inference(resolution,[status(thm)],[c25304, c271])).
% 108.41/108.59 cnf(c26397,plain,cong(X7515,X7515,X7516,X7516),inference(resolution,[status(thm)],[c25373, c25520])).
% 108.41/108.59 cnf(c26416,plain,~coll(X7575,X7575,X7575)|midp(X7575,X7575,X7575),inference(resolution,[status(thm)],[c26397, c189])).
% 108.41/108.59 cnf(c26527,plain,midp(X7576,X7576,X7576),inference(resolution,[status(thm)],[c26416, c24945])).
% 108.41/108.59 cnf(c26650,plain,midp(X7577,X7578,X7578),inference(resolution,[status(thm)],[c26527, c18053])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c239,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])).
% 108.41/108.59 fof(c240,plain,(![X233]:(![X234]:(![X235]:(![X236]:((~perp(X233,X234,X234,X235)|~midp(X236,X233,X235))|cong(X233,X236,X234,X236)))))),inference(variable_rename,[status(thm)],[c239])).
% 108.41/108.59 cnf(c241,plain,~perp(X1030,X1029,X1029,X1028)|~midp(X1027,X1030,X1028)|cong(X1030,X1027,X1029,X1027),inference(split_conjunct,[status(thm)],[c240])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c160,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])).
% 108.41/108.59 fof(c161,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)],[c160])).
% 108.41/108.59 fof(c163,plain,(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:(![X133]:((~eqangle(X126,X127,X128,X129,X130,X131,X132,X133)|~perp(X130,X131,X132,X133))|perp(X126,X127,X128,X129)))))))))),inference(shift_quantors,[status(thm)],[fof(c162,plain,(![X126]:(![X127]:(![X128]:(![X129]:((![X130]:(![X131]:(![X132]:(![X133]:(~eqangle(X126,X127,X128,X129,X130,X131,X132,X133)|~perp(X130,X131,X132,X133))))))|perp(X126,X127,X128,X129)))))),inference(variable_rename,[status(thm)],[c161])).])).
% 108.41/108.59 cnf(c164,plain,~eqangle(X935,X939,X936,X941,X938,X942,X937,X940)|~perp(X938,X942,X937,X940)|perp(X935,X939,X936,X941),inference(split_conjunct,[status(thm)],[c163])).
% 108.41/108.59 cnf(c25243,plain,eqangle(X6423,X6420,X6420,X6423,X6421,X6422,X6421,X6422),inference(resolution,[status(thm)],[c19218, c347])).
% 108.41/108.59 cnf(c25320,plain,~perp(X7466,X7464,X7466,X7464)|perp(X7463,X7465,X7465,X7463),inference(resolution,[status(thm)],[c25243, c164])).
% 108.41/108.59 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)).
% 108.41/108.59 fof(c225,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])).
% 108.41/108.59 fof(c226,plain,(![X217]:(![X218]:(![X219]:(![X220]:((~cong(X217,X219,X218,X219)|~cong(X217,X220,X218,X220))|perp(X217,X218,X219,X220)))))),inference(variable_rename,[status(thm)],[c225])).
% 108.41/108.59 cnf(c227,plain,~cong(X1011,X1013,X1014,X1013)|~cong(X1011,X1012,X1014,X1012)|perp(X1011,X1014,X1013,X1012),inference(split_conjunct,[status(thm)],[c226])).
% 108.41/108.59 cnf(c1038,plain,~cong(X1073,X1075,X1074,X1075)|perp(X1073,X1074,X1075,X1075),inference(factor,[status(thm)],[c227])).
% 108.41/108.59 cnf(c26412,plain,perp(X7532,X7532,X7532,X7532),inference(resolution,[status(thm)],[c26397, c1038])).
% 108.41/108.59 cnf(c26453,plain,perp(X7550,X7551,X7551,X7550),inference(resolution,[status(thm)],[c26412, c25320])).
% 108.41/108.59 cnf(c26522,plain,~midp(X8422,X8423,X8423)|cong(X8423,X8422,X8421,X8422),inference(resolution,[status(thm)],[c26453, c241])).
% 108.41/108.59 cnf(c28396,plain,cong(X8425,X8426,X8424,X8426),inference(resolution,[status(thm)],[c26522, c26650])).
% 108.41/108.59 cnf(c28404,plain,cong(X8431,X8432,X8432,X8430),inference(resolution,[status(thm)],[c28396, c341])).
% 108.41/108.59 cnf(c28447,plain,cong(X8451,X8450,X8449,X8451),inference(resolution,[status(thm)],[c28404, c338])).
% 108.41/108.59 cnf(c28481,plain,cong(X8470,X8469,X8470,X8468),inference(resolution,[status(thm)],[c28447, c341])).
% 108.41/108.59 cnf(c28557,plain,~coll(X8699,X8700,X8701)|midp(X8699,X8700,X8701),inference(resolution,[status(thm)],[c28481, c189])).
% 108.41/108.59 cnf(c30198,plain,midp(X8704,X8702,X8703),inference(resolution,[status(thm)],[c28557, c24945])).
% 108.41/108.59 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 108.41/108.59 fof(c264,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])).
% 108.41/108.59 fof(c265,plain,(![X268]:(![X269]:(![X270]:(![X271]:(![X272]:((~midp(X271,X268,X269)|~midp(X272,X268,X270))|para(X271,X272,X269,X270))))))),inference(variable_rename,[status(thm)],[c264])).
% 108.41/108.59 cnf(c266,plain,~midp(X1062,X1063,X1066)|~midp(X1064,X1063,X1065)|para(X1062,X1064,X1066,X1065),inference(split_conjunct,[status(thm)],[c265])).
% 108.41/108.59 cnf(c26907,plain,~midp(X11918,X11917,X11915)|para(X11918,X11916,X11915,X11917),inference(resolution,[status(thm)],[c26650, c266])).
% 108.41/108.59 cnf(c32745,plain,para(X11919,X11921,X11922,X11920),inference(resolution,[status(thm)],[c26907, c30198])).
% 108.41/108.59 cnf(c32761,plain,$false,inference(resolution,[status(thm)],[c32745, c24])).
% 108.41/108.59 % SZS output end CNFRefutation
% 108.41/108.59
% 108.41/108.59 % Initial clauses : 136
% 108.41/108.59 % Processed clauses : 3846
% 108.41/108.59 % Factors computed : 143
% 108.41/108.59 % Resolvents computed: 32209
% 108.41/108.59 % Tautologies deleted: 12
% 108.41/108.59 % Forward subsumed : 9376
% 108.41/108.59 % Backward subsumed : 3377
% 108.41/108.59 % -------- CPU Time ---------
% 108.41/108.59 % User time : 108.143 s
% 108.41/108.59 % System time : 0.072 s
% 108.41/108.59 % Total time : 108.215 s
%------------------------------------------------------------------------------