%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO653+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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 145.23s 145.41s
% Output : Refutation 145.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO653+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n021.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:48:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 145.23/145.41 % Version: 1.5
% 145.23/145.41 % SZS status Theorem
% 145.23/145.41 % SZS output start CNFRefutation
% 145.23/145.41 fof(exemplo6GDDFULLmoreE0227,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(((((((((para(A,B,C,D)¶(A,C,B,D))&coll(E,C,D))¶(A,D,F,E))&coll(F,A,B))&coll(G,D,F))&coll(G,A,E))&coll(H,B,E))&coll(H,C,F))=>para(G,H,A,B)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE0227)).
% 145.23/145.41 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(((((((((para(A,B,C,D)¶(A,C,B,D))&coll(E,C,D))¶(A,D,F,E))&coll(F,A,B))&coll(G,D,F))&coll(G,A,E))&coll(H,B,E))&coll(H,C,F))=>para(G,H,A,B))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE0227])).
% 145.23/145.41 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(((((((((para(A,B,C,D)¶(A,C,B,D))&coll(E,C,D))¶(A,D,F,E))&coll(F,A,B))&coll(G,D,F))&coll(G,A,E))&coll(H,B,E))&coll(H,C,F))&~para(G,H,A,B)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 145.23/145.41 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((para(X2,X3,X4,X5)¶(X2,X4,X3,X5))&coll(X6,X4,X5))¶(X2,X5,X7,X6))&coll(X7,X2,X3))&coll(X8,X5,X7))&coll(X8,X2,X6))&coll(X9,X3,X6))&coll(X9,X4,X7))&~para(X8,X9,X2,X3)))))))))),inference(variable_rename,[status(thm)],[c12])).
% 145.23/145.41 fof(c14,negated_conjecture,(((((((((para(skolem0001,skolem0002,skolem0003,skolem0004)¶(skolem0001,skolem0003,skolem0002,skolem0004))&coll(skolem0005,skolem0003,skolem0004))¶(skolem0001,skolem0004,skolem0006,skolem0005))&coll(skolem0006,skolem0001,skolem0002))&coll(skolem0007,skolem0004,skolem0006))&coll(skolem0007,skolem0001,skolem0005))&coll(skolem0008,skolem0002,skolem0005))&coll(skolem0008,skolem0003,skolem0006))&~para(skolem0007,skolem0008,skolem0001,skolem0002)),inference(skolemize,[status(esa)],[c13])).
% 145.23/145.41 cnf(c24,negated_conjecture,~para(skolem0007,skolem0008,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c402,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c401])).
% 145.23/145.41 cnf(c403,plain,~coll(X796,X795,X798)|~coll(X796,X795,X797)|coll(X798,X797,X796),inference(split_conjunct,[status(thm)],[c402])).
% 145.23/145.41 cnf(c674,plain,~coll(X800,X799,X801)|coll(X801,X801,X800),inference(factor,[status(thm)],[c403])).
% 145.23/145.41 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)).
% 145.23/145.41 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 145.23/145.41 fof(c191,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c190])).
% 145.23/145.41 cnf(c192,plain,~para(X693,X694,X693,X692)|coll(X693,X694,X692),inference(split_conjunct,[status(thm)],[c191])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c290,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(c289,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)],[c288])).])).
% 145.23/145.41 cnf(c291,plain,~eqangle(X1062,X1064,X1063,X1060,X1061,X1065,X1063,X1060)|para(X1062,X1064,X1061,X1065),inference(split_conjunct,[status(thm)],[c290])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c352,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)],[c351])).
% 145.23/145.41 cnf(c353,plain,~eqangle(X1200,X1204,X1203,X1205,X1201,X1199,X1202,X1198)|eqangle(X1203,X1205,X1200,X1204,X1202,X1198,X1201,X1199),inference(split_conjunct,[status(thm)],[c352])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c285,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(c284,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)],[c283])).])).
% 145.23/145.41 cnf(c286,plain,~para(X1058,X1059,X1054,X1057)|eqangle(X1058,X1059,X1055,X1056,X1054,X1057,X1055,X1056),inference(split_conjunct,[status(thm)],[c285])).
% 145.23/145.41 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)).
% 145.23/145.41 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 145.23/145.41 fof(c399,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c398])).
% 145.23/145.41 cnf(c400,plain,~para(X741,X744,X743,X742)|para(X741,X744,X742,X743),inference(split_conjunct,[status(thm)],[c399])).
% 145.23/145.41 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)).
% 145.23/145.41 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 145.23/145.41 fof(c396,plain,(![X513]:(![X514]:(![X515]:(![X516]:(~para(X513,X514,X515,X516)|para(X515,X516,X513,X514)))))),inference(variable_rename,[status(thm)],[c395])).
% 145.23/145.41 cnf(c397,plain,~para(X735,X732,X733,X734)|para(X733,X734,X735,X732),inference(split_conjunct,[status(thm)],[c396])).
% 145.23/145.41 cnf(c18,negated_conjecture,para(skolem0001,skolem0004,skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 145.23/145.41 cnf(c552,plain,para(skolem0001,skolem0004,skolem0005,skolem0006),inference(resolution,[status(thm)],[c400, c18])).
% 145.23/145.41 cnf(c558,plain,para(skolem0005,skolem0006,skolem0001,skolem0004),inference(resolution,[status(thm)],[c552, c397])).
% 145.23/145.41 cnf(c598,plain,para(skolem0005,skolem0006,skolem0004,skolem0001),inference(resolution,[status(thm)],[c558, c400])).
% 145.23/145.41 cnf(c531,plain,para(skolem0006,skolem0005,skolem0001,skolem0004),inference(resolution,[status(thm)],[c397, c18])).
% 145.23/145.41 cnf(c556,plain,para(skolem0006,skolem0005,skolem0004,skolem0001),inference(resolution,[status(thm)],[c400, c531])).
% 145.23/145.41 cnf(c583,plain,para(skolem0004,skolem0001,skolem0006,skolem0005),inference(resolution,[status(thm)],[c556, c397])).
% 145.23/145.41 cnf(c624,plain,para(skolem0004,skolem0001,skolem0005,skolem0006),inference(resolution,[status(thm)],[c583, c400])).
% 145.23/145.41 fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)¶(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 145.23/145.41 fof(c392,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])).
% 145.23/145.41 fof(c393,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)],[c392])).
% 145.23/145.41 cnf(c394,plain,~para(X1252,X1254,X1250,X1253)|~para(X1250,X1253,X1249,X1251)|para(X1252,X1254,X1249,X1251),inference(split_conjunct,[status(thm)],[c393])).
% 145.23/145.41 cnf(c1670,plain,~para(X3069,X3068,skolem0004,skolem0001)|para(X3069,X3068,skolem0005,skolem0006),inference(resolution,[status(thm)],[c394, c624])).
% 145.23/145.41 cnf(c8681,plain,para(skolem0005,skolem0006,skolem0005,skolem0006),inference(resolution,[status(thm)],[c1670, c598])).
% 145.23/145.41 cnf(c8711,plain,eqangle(skolem0005,skolem0006,X5228,X5229,skolem0005,skolem0006,X5228,X5229),inference(resolution,[status(thm)],[c8681, c286])).
% 145.23/145.41 cnf(c15207,plain,eqangle(X5806,X5805,skolem0005,skolem0006,X5806,X5805,skolem0005,skolem0006),inference(resolution,[status(thm)],[c8711, c353])).
% 145.23/145.41 cnf(c16409,plain,para(X5812,X5811,X5812,X5811),inference(resolution,[status(thm)],[c15207, c291])).
% 145.23/145.41 cnf(c16469,plain,coll(X5813,X5814,X5814),inference(resolution,[status(thm)],[c16409, c192])).
% 145.23/145.41 cnf(c16777,plain,coll(X5817,X5817,X5818),inference(resolution,[status(thm)],[c16469, c674])).
% 145.23/145.41 cnf(c17047,plain,~coll(X7661,X7661,X7662)|coll(X7662,X7663,X7661),inference(resolution,[status(thm)],[c16777, c403])).
% 145.23/145.41 cnf(c32667,plain,coll(X7665,X7666,X7664),inference(resolution,[status(thm)],[c17047, c16777])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c188,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c187])).
% 145.23/145.41 cnf(c189,plain,~cong(X935,X936,X935,X934)|~coll(X935,X936,X934)|midp(X935,X936,X934),inference(split_conjunct,[status(thm)],[c188])).
% 145.23/145.41 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)).
% 145.23/145.41 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 145.23/145.41 fof(c340,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c339])).
% 145.23/145.41 cnf(c341,plain,~cong(X699,X701,X700,X702)|cong(X699,X701,X702,X700),inference(split_conjunct,[status(thm)],[c340])).
% 145.23/145.41 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)).
% 145.23/145.41 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 145.23/145.41 fof(c337,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c336])).
% 145.23/145.41 cnf(c338,plain,~cong(X696,X695,X697,X698)|cong(X697,X698,X696,X695),inference(split_conjunct,[status(thm)],[c337])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c197,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)],[c196])).
% 145.23/145.41 cnf(c198,plain,~midp(X944,X946,X943)|~para(X946,X942,X943,X945)|~para(X946,X945,X943,X942)|midp(X944,X942,X945),inference(split_conjunct,[status(thm)],[c197])).
% 145.23/145.41 cnf(c1276,plain,~midp(X2523,X2522,X2521)|~para(X2522,X2520,X2521,X2520)|midp(X2523,X2520,X2520),inference(factor,[status(thm)],[c198])).
% 145.23/145.41 cnf(c16461,plain,~midp(X7359,X7358,X7358)|midp(X7359,X7360,X7360),inference(resolution,[status(thm)],[c16409, c1276])).
% 145.23/145.41 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)).
% 145.23/145.41 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 145.23/145.41 fof(c361,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X464,X463,X465,X466)))))),inference(variable_rename,[status(thm)],[c360])).
% 145.23/145.41 cnf(c362,plain,~cyclic(X711,X710,X708,X709)|cyclic(X710,X711,X708,X709),inference(split_conjunct,[status(thm)],[c361])).
% 145.23/145.41 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)).
% 145.23/145.41 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 145.23/145.41 fof(c364,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c363])).
% 145.23/145.41 cnf(c365,plain,~cyclic(X714,X713,X712,X715)|cyclic(X714,X712,X713,X715),inference(split_conjunct,[status(thm)],[c364])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c273,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)],[c272])).
% 145.23/145.41 cnf(c274,plain,~eqangle(X1045,X1043,X1045,X1044,X1042,X1043,X1042,X1044)|~coll(X1045,X1042,X1044)|cyclic(X1043,X1044,X1045,X1042),inference(split_conjunct,[status(thm)],[c273])).
% 145.23/145.41 cnf(c16465,plain,eqangle(X7364,X7366,X7365,X7367,X7364,X7366,X7365,X7367),inference(resolution,[status(thm)],[c16409, c286])).
% 145.23/145.41 cnf(c32468,plain,~coll(X8092,X8092,X8093)|cyclic(X8091,X8093,X8092,X8092),inference(resolution,[status(thm)],[c16465, c274])).
% 145.23/145.41 cnf(c33376,plain,cyclic(X8094,X8095,X8096,X8096),inference(resolution,[status(thm)],[c32468, c32667])).
% 145.23/145.41 cnf(c33381,plain,cyclic(X8104,X8105,X8103,X8105),inference(resolution,[status(thm)],[c33376, c365])).
% 145.23/145.41 cnf(c33391,plain,cyclic(X8115,X8116,X8117,X8115),inference(resolution,[status(thm)],[c33381, c362])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c270,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(c269,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)],[c268])).])).
% 145.23/145.41 cnf(c271,plain,~cyclic(X1038,X1036,X1040,X1039)|~cyclic(X1038,X1036,X1040,X1037)|~cyclic(X1038,X1036,X1040,X1041)|~eqangle(X1040,X1038,X1040,X1036,X1041,X1039,X1041,X1037)|cong(X1038,X1036,X1039,X1037),inference(split_conjunct,[status(thm)],[c270])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c346,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)],[c345])).
% 145.23/145.41 cnf(c347,plain,~eqangle(X1187,X1182,X1183,X1184,X1185,X1188,X1186,X1189)|eqangle(X1187,X1182,X1185,X1188,X1183,X1184,X1186,X1189),inference(split_conjunct,[status(thm)],[c346])).
% 145.23/145.41 cnf(c16500,plain,para(X5838,X5839,X5839,X5838),inference(resolution,[status(thm)],[c16409, c400])).
% 145.23/145.41 cnf(c18866,plain,eqangle(X7865,X7863,X7864,X7866,X7863,X7865,X7864,X7866),inference(resolution,[status(thm)],[c16500, c286])).
% 145.23/145.41 cnf(c33280,plain,eqangle(X7909,X7906,X7908,X7907,X7909,X7906,X7907,X7908),inference(resolution,[status(thm)],[c18866, c353])).
% 145.23/145.41 cnf(c33312,plain,eqangle(X7954,X7955,X7954,X7955,X7957,X7956,X7956,X7957),inference(resolution,[status(thm)],[c33280, c347])).
% 145.23/145.41 cnf(c33361,plain,~cyclic(X9139,X9139,X9141,X9140)|cong(X9139,X9139,X9140,X9140),inference(resolution,[status(thm)],[c33312, c271])).
% 145.23/145.41 cnf(c33926,plain,cong(X9142,X9142,X9142,X9142),inference(resolution,[status(thm)],[c33361, c33391])).
% 145.23/145.41 cnf(c33937,plain,~coll(X9213,X9213,X9213)|midp(X9213,X9213,X9213),inference(resolution,[status(thm)],[c33926, c189])).
% 145.23/145.41 cnf(c34031,plain,midp(X9214,X9214,X9214),inference(resolution,[status(thm)],[c33937, c32667])).
% 145.23/145.41 cnf(c34207,plain,midp(X9217,X9216,X9216),inference(resolution,[status(thm)],[c34031, c16461])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c240,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c239])).
% 145.23/145.41 cnf(c241,plain,~perp(X998,X999,X999,X997)|~midp(X996,X998,X997)|cong(X998,X996,X999,X996),inference(split_conjunct,[status(thm)],[c240])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c163,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(c162,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)],[c161])).])).
% 145.23/145.41 cnf(c164,plain,~eqangle(X907,X904,X911,X905,X906,X910,X908,X909)|~perp(X906,X910,X908,X909)|perp(X907,X904,X911,X905),inference(split_conjunct,[status(thm)],[c163])).
% 145.23/145.41 cnf(c33284,plain,eqangle(X7913,X7912,X7912,X7913,X7914,X7915,X7914,X7915),inference(resolution,[status(thm)],[c18866, c347])).
% 145.23/145.41 cnf(c33325,plain,~perp(X9080,X9081,X9080,X9081)|perp(X9083,X9082,X9082,X9083),inference(resolution,[status(thm)],[c33284, c164])).
% 145.23/145.41 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)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c226,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)],[c225])).
% 145.23/145.41 cnf(c227,plain,~cong(X983,X982,X980,X982)|~cong(X983,X981,X980,X981)|perp(X983,X980,X982,X981),inference(split_conjunct,[status(thm)],[c226])).
% 145.23/145.41 cnf(c1423,plain,~cong(X1247,X1248,X1246,X1248)|perp(X1247,X1246,X1248,X1248),inference(factor,[status(thm)],[c227])).
% 145.23/145.41 cnf(c33943,plain,perp(X9161,X9161,X9161,X9161),inference(resolution,[status(thm)],[c33926, c1423])).
% 145.23/145.41 cnf(c33982,plain,perp(X9180,X9181,X9181,X9180),inference(resolution,[status(thm)],[c33943, c33325])).
% 145.23/145.41 cnf(c34019,plain,~midp(X9991,X9992,X9992)|cong(X9992,X9991,X9993,X9991),inference(resolution,[status(thm)],[c33982, c241])).
% 145.23/145.41 cnf(c35250,plain,cong(X9994,X9996,X9995,X9996),inference(resolution,[status(thm)],[c34019, c34207])).
% 145.23/145.41 cnf(c35259,plain,cong(X10000,X9999,X9999,X10001),inference(resolution,[status(thm)],[c35250, c341])).
% 145.23/145.41 cnf(c35273,plain,cong(X10018,X10017,X10016,X10018),inference(resolution,[status(thm)],[c35259, c338])).
% 145.23/145.41 cnf(c35305,plain,cong(X10041,X10042,X10041,X10043),inference(resolution,[status(thm)],[c35273, c341])).
% 145.23/145.41 cnf(c35335,plain,~coll(X10167,X10166,X10168)|midp(X10167,X10166,X10168),inference(resolution,[status(thm)],[c35305, c189])).
% 145.23/145.41 cnf(c36204,plain,midp(X10169,X10171,X10170),inference(resolution,[status(thm)],[c35335, c32667])).
% 145.23/145.41 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 145.23/145.41 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])).
% 145.23/145.41 fof(c265,plain,(![X267]:(![X268]:(![X269]:(![X270]:(![X271]:((~midp(X270,X267,X268)|~midp(X271,X267,X269))|para(X270,X271,X268,X269))))))),inference(variable_rename,[status(thm)],[c264])).
% 145.23/145.41 cnf(c266,plain,~midp(X1031,X1034,X1033)|~midp(X1032,X1034,X1035)|para(X1031,X1032,X1033,X1035),inference(split_conjunct,[status(thm)],[c265])).
% 145.23/145.41 cnf(c34288,plain,~midp(X14250,X14247,X14248)|para(X14250,X14249,X14248,X14247),inference(resolution,[status(thm)],[c34207, c266])).
% 145.23/145.41 cnf(c39842,plain,para(X14253,X14254,X14251,X14252),inference(resolution,[status(thm)],[c34288, c36204])).
% 145.23/145.41 cnf(c39843,plain,$false,inference(resolution,[status(thm)],[c39842, c24])).
% 145.23/145.41 % SZS output end CNFRefutation
% 145.23/145.41
% 145.23/145.41 % Initial clauses : 137
% 145.23/145.41 % Processed clauses : 3882
% 145.23/145.41 % Factors computed : 190
% 145.23/145.41 % Resolvents computed: 39248
% 145.23/145.41 % Tautologies deleted: 12
% 145.23/145.41 % Forward subsumed : 11440
% 145.23/145.41 % Backward subsumed : 3450
% 145.23/145.41 % -------- CPU Time ---------
% 145.23/145.41 % User time : 144.963 s
% 145.23/145.41 % System time : 0.090 s
% 145.23/145.41 % Total time : 145.053 s
%------------------------------------------------------------------------------