%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO575+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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 234.17s 234.35s
% Output : Refutation 234.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO575+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n007.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:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 234.17/234.35 % Version: 1.5
% 234.17/234.35 % SZS status Theorem
% 234.17/234.35 % SZS output start CNFRefutation
% 234.17/234.35 fof(exemplo6GDDFULL214037,conjecture,(![A]:(![B]:(![C]:(![O]:(![H]:(![C1]:(![A1]:(![NWPNT1]:(![NWPNT2]:((((((((circle(O,A,B,C)&perp(A,B,C,H))&perp(A,C,B,H))&perp(B,C,A,H))&circle(O,C,C1,NWPNT1))&coll(C1,C,H))&circle(O,A,A1,NWPNT2))&coll(A1,A,H))=>cong(B,A1,B,C1))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214037)).
% 234.17/234.35 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![H]:(![C1]:(![A1]:(![NWPNT1]:(![NWPNT2]:((((((((circle(O,A,B,C)&perp(A,B,C,H))&perp(A,C,B,H))&perp(B,C,A,H))&circle(O,C,C1,NWPNT1))&coll(C1,C,H))&circle(O,A,A1,NWPNT2))&coll(A1,A,H))=>cong(B,A1,B,C1)))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214037])).
% 234.17/234.35 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[H]:(?[C1]:(?[A1]:(?[NWPNT1]:(?[NWPNT2]:((((((((circle(O,A,B,C)&perp(A,B,C,H))&perp(A,C,B,H))&perp(B,C,A,H))&circle(O,C,C1,NWPNT1))&coll(C1,C,H))&circle(O,A,A1,NWPNT2))&coll(A1,A,H))&~cong(B,A1,B,C1))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 234.17/234.35 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[H]:(?[C1]:(?[A1]:((((((((circle(O,A,B,C)&perp(A,B,C,H))&perp(A,C,B,H))&perp(B,C,A,H))&(?[NWPNT1]:circle(O,C,C1,NWPNT1)))&coll(C1,C,H))&(?[NWPNT2]:circle(O,A,A1,NWPNT2)))&coll(A1,A,H))&~cong(B,A1,B,C1))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 234.17/234.35 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((((circle(X5,X2,X3,X4)&perp(X2,X3,X4,X6))&perp(X2,X4,X3,X6))&perp(X3,X4,X2,X6))&(?[X9]:circle(X5,X4,X7,X9)))&coll(X7,X4,X6))&(?[X10]:circle(X5,X2,X8,X10)))&coll(X8,X2,X6))&~cong(X3,X8,X3,X7))))))))),inference(variable_rename,[status(thm)],[c13])).
% 234.17/234.35 fof(c15,negated_conjecture,((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&perp(skolem0001,skolem0002,skolem0003,skolem0005))&perp(skolem0001,skolem0003,skolem0002,skolem0005))&perp(skolem0002,skolem0003,skolem0001,skolem0005))&circle(skolem0004,skolem0003,skolem0006,skolem0008))&coll(skolem0006,skolem0003,skolem0005))&circle(skolem0004,skolem0001,skolem0007,skolem0009))&coll(skolem0007,skolem0001,skolem0005))&~cong(skolem0002,skolem0007,skolem0002,skolem0006)),inference(skolemize,[status(esa)],[c14])).
% 234.17/234.35 cnf(c24,negated_conjecture,~cong(skolem0002,skolem0007,skolem0002,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 234.17/234.35 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)).
% 234.17/234.35 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 234.17/234.35 fof(c340,plain,(![X411]:(![X412]:(![X413]:(![X414]:(~cong(X411,X412,X413,X414)|cong(X411,X412,X414,X413)))))),inference(variable_rename,[status(thm)],[c339])).
% 234.17/234.35 cnf(c341,plain,~cong(X633,X635,X632,X634)|cong(X633,X635,X634,X632),inference(split_conjunct,[status(thm)],[c340])).
% 234.17/234.35 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)).
% 234.17/234.35 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 234.17/234.35 fof(c337,plain,(![X407]:(![X408]:(![X409]:(![X410]:(~cong(X407,X408,X409,X410)|cong(X409,X410,X407,X408)))))),inference(variable_rename,[status(thm)],[c336])).
% 234.17/234.35 cnf(c338,plain,~cong(X614,X613,X612,X615)|cong(X612,X615,X614,X613),inference(split_conjunct,[status(thm)],[c337])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c198,plain,~midp(X956,X957,X960)|~para(X957,X959,X960,X958)|~para(X957,X958,X960,X959)|midp(X956,X959,X958),inference(split_conjunct,[status(thm)],[c197])).
% 234.17/234.35 cnf(c963,plain,~midp(X1930,X1929,X1931)|~para(X1929,X1932,X1931,X1932)|midp(X1930,X1932,X1932),inference(factor,[status(thm)],[c198])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 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])).])).
% 234.17/234.35 cnf(c291,plain,~eqangle(X1079,X1077,X1076,X1074,X1078,X1075,X1076,X1074)|para(X1079,X1077,X1078,X1075),inference(split_conjunct,[status(thm)],[c290])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c353,plain,~eqangle(X1213,X1217,X1214,X1219,X1216,X1212,X1215,X1218)|eqangle(X1214,X1219,X1213,X1217,X1215,X1218,X1216,X1212),inference(split_conjunct,[status(thm)],[c352])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 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])).])).
% 234.17/234.35 cnf(c286,plain,~para(X1071,X1073,X1069,X1068)|eqangle(X1071,X1073,X1072,X1070,X1069,X1068,X1072,X1070),inference(split_conjunct,[status(thm)],[c285])).
% 234.17/234.35 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 234.17/234.35 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 234.17/234.35 fof(c390,plain,(![X504]:(![X505]:(![X506]:(![X507]:(~perp(X504,X505,X506,X507)|perp(X504,X505,X507,X506)))))),inference(variable_rename,[status(thm)],[c389])).
% 234.17/234.35 cnf(c391,plain,~perp(X682,X681,X680,X683)|perp(X682,X681,X683,X680),inference(split_conjunct,[status(thm)],[c390])).
% 234.17/234.35 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 234.17/234.35 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 234.17/234.35 fof(c387,plain,(![X500]:(![X501]:(![X502]:(![X503]:(~perp(X500,X501,X502,X503)|perp(X502,X503,X500,X501)))))),inference(variable_rename,[status(thm)],[c386])).
% 234.17/234.35 cnf(c388,plain,~perp(X650,X651,X649,X648)|perp(X649,X648,X650,X651),inference(split_conjunct,[status(thm)],[c387])).
% 234.17/234.35 cnf(c19,negated_conjecture,perp(skolem0002,skolem0003,skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 234.17/234.35 cnf(c457,plain,perp(skolem0001,skolem0005,skolem0002,skolem0003),inference(resolution,[status(thm)],[c388, c19])).
% 234.17/234.35 cnf(c466,plain,perp(skolem0001,skolem0005,skolem0003,skolem0002),inference(resolution,[status(thm)],[c391, c457])).
% 234.17/234.35 cnf(c478,plain,perp(skolem0003,skolem0002,skolem0001,skolem0005),inference(resolution,[status(thm)],[c466, c388])).
% 234.17/234.35 cnf(c494,plain,perp(skolem0003,skolem0002,skolem0005,skolem0001),inference(resolution,[status(thm)],[c478, c391])).
% 234.17/234.35 cnf(c467,plain,perp(skolem0002,skolem0003,skolem0005,skolem0001),inference(resolution,[status(thm)],[c391, c19])).
% 234.17/234.35 cnf(c481,plain,perp(skolem0005,skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c467, c388])).
% 234.17/234.35 cnf(c497,plain,perp(skolem0005,skolem0001,skolem0003,skolem0002),inference(resolution,[status(thm)],[c481, c391])).
% 234.17/234.35 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c385,plain,~perp(X1257,X1256,X1259,X1255)|~perp(X1259,X1255,X1254,X1258)|para(X1257,X1256,X1254,X1258),inference(split_conjunct,[status(thm)],[c384])).
% 234.17/234.35 cnf(c1488,plain,~perp(X2612,X2611,skolem0005,skolem0001)|para(X2612,X2611,skolem0003,skolem0002),inference(resolution,[status(thm)],[c385, c497])).
% 234.17/234.35 cnf(c8516,plain,para(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1488, c494])).
% 234.17/234.35 cnf(c8519,plain,eqangle(skolem0003,skolem0002,X3749,X3748,skolem0003,skolem0002,X3749,X3748),inference(resolution,[status(thm)],[c8516, c286])).
% 234.17/234.35 cnf(c18736,plain,eqangle(X6015,X6016,skolem0003,skolem0002,X6015,X6016,skolem0003,skolem0002),inference(resolution,[status(thm)],[c8519, c353])).
% 234.17/234.35 cnf(c30494,plain,para(X6017,X6018,X6017,X6018),inference(resolution,[status(thm)],[c18736, c291])).
% 234.17/234.35 cnf(c30538,plain,~midp(X7302,X7301,X7301)|midp(X7302,X7303,X7303),inference(resolution,[status(thm)],[c30494, c963])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c403,plain,~coll(X748,X747,X749)|~coll(X748,X747,X750)|coll(X749,X750,X748),inference(split_conjunct,[status(thm)],[c402])).
% 234.17/234.35 cnf(c525,plain,~coll(X753,X751,X752)|coll(X752,X752,X753),inference(factor,[status(thm)],[c403])).
% 234.17/234.35 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)).
% 234.17/234.35 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 234.17/234.35 fof(c191,plain,(![X165]:(![X166]:(![X167]:(~para(X165,X166,X165,X167)|coll(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c190])).
% 234.17/234.35 cnf(c192,plain,~para(X610,X609,X610,X611)|coll(X610,X609,X611),inference(split_conjunct,[status(thm)],[c191])).
% 234.17/234.35 cnf(c30513,plain,coll(X6019,X6020,X6020),inference(resolution,[status(thm)],[c30494, c192])).
% 234.17/234.35 cnf(c30666,plain,coll(X6021,X6021,X6022),inference(resolution,[status(thm)],[c30513, c525])).
% 234.17/234.35 cnf(c31169,plain,~coll(X7512,X7512,X7514)|coll(X7514,X7513,X7512),inference(resolution,[status(thm)],[c30666, c403])).
% 234.17/234.35 cnf(c38061,plain,coll(X7517,X7519,X7518),inference(resolution,[status(thm)],[c31169, c30666])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c189,plain,~cong(X946,X948,X946,X947)|~coll(X946,X948,X947)|midp(X946,X948,X947),inference(split_conjunct,[status(thm)],[c188])).
% 234.17/234.35 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)).
% 234.17/234.35 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 234.17/234.35 fof(c364,plain,(![X468]:(![X469]:(![X470]:(![X471]:(~cyclic(X468,X469,X470,X471)|cyclic(X468,X470,X469,X471)))))),inference(variable_rename,[status(thm)],[c363])).
% 234.17/234.35 cnf(c365,plain,~cyclic(X640,X643,X642,X641)|cyclic(X640,X642,X643,X641),inference(split_conjunct,[status(thm)],[c364])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c274,plain,~eqangle(X1056,X1058,X1056,X1057,X1059,X1058,X1059,X1057)|~coll(X1056,X1059,X1057)|cyclic(X1058,X1057,X1056,X1059),inference(split_conjunct,[status(thm)],[c273])).
% 234.17/234.35 cnf(c30496,plain,eqangle(X7283,X7282,X7284,X7285,X7283,X7282,X7284,X7285),inference(resolution,[status(thm)],[c30494, c286])).
% 234.17/234.35 cnf(c37765,plain,~coll(X7858,X7858,X7857)|cyclic(X7856,X7857,X7858,X7858),inference(resolution,[status(thm)],[c30496, c274])).
% 234.17/234.35 cnf(c38619,plain,cyclic(X7860,X7861,X7859,X7859),inference(resolution,[status(thm)],[c37765, c38061])).
% 234.17/234.35 cnf(c38624,plain,cyclic(X7872,X7874,X7873,X7874),inference(resolution,[status(thm)],[c38619, c365])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 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])).])).
% 234.17/234.35 cnf(c271,plain,~cyclic(X1050,X1053,X1051,X1054)|~cyclic(X1050,X1053,X1051,X1052)|~cyclic(X1050,X1053,X1051,X1055)|~eqangle(X1051,X1050,X1051,X1053,X1055,X1054,X1055,X1052)|cong(X1050,X1053,X1054,X1052),inference(split_conjunct,[status(thm)],[c270])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c347,plain,~eqangle(X1197,X1198,X1200,X1201,X1199,X1203,X1196,X1202)|eqangle(X1197,X1198,X1199,X1203,X1200,X1201,X1196,X1202),inference(split_conjunct,[status(thm)],[c346])).
% 234.17/234.35 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)).
% 234.17/234.35 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 234.17/234.35 fof(c399,plain,(![X518]:(![X519]:(![X520]:(![X521]:(~para(X518,X519,X520,X521)|para(X518,X519,X521,X520)))))),inference(variable_rename,[status(thm)],[c398])).
% 234.17/234.35 cnf(c400,plain,~para(X737,X738,X740,X739)|para(X737,X738,X739,X740),inference(split_conjunct,[status(thm)],[c399])).
% 234.17/234.35 cnf(c30510,plain,para(X6038,X6039,X6039,X6038),inference(resolution,[status(thm)],[c30494, c400])).
% 234.17/234.35 cnf(c31818,plain,eqangle(X7654,X7655,X7653,X7656,X7655,X7654,X7653,X7656),inference(resolution,[status(thm)],[c30510, c286])).
% 234.17/234.35 cnf(c38351,plain,eqangle(X7698,X7699,X7700,X7697,X7698,X7699,X7697,X7700),inference(resolution,[status(thm)],[c31818, c353])).
% 234.17/234.35 cnf(c38416,plain,eqangle(X7748,X7745,X7748,X7745,X7746,X7747,X7747,X7746),inference(resolution,[status(thm)],[c38351, c347])).
% 234.17/234.35 cnf(c38475,plain,~cyclic(X8788,X8788,X8787,X8789)|cong(X8788,X8788,X8789,X8789),inference(resolution,[status(thm)],[c38416, c271])).
% 234.17/234.35 cnf(c39257,plain,cong(X8790,X8790,X8790,X8790),inference(resolution,[status(thm)],[c38475, c38624])).
% 234.17/234.35 cnf(c39278,plain,~coll(X8850,X8850,X8850)|midp(X8850,X8850,X8850),inference(resolution,[status(thm)],[c39257, c189])).
% 234.17/234.35 cnf(c39430,plain,midp(X8851,X8851,X8851),inference(resolution,[status(thm)],[c39278, c38061])).
% 234.17/234.35 cnf(c39775,plain,midp(X8853,X8854,X8854),inference(resolution,[status(thm)],[c39430, c30538])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c241,plain,~perp(X1013,X1010,X1010,X1011)|~midp(X1012,X1013,X1011)|cong(X1013,X1012,X1010,X1012),inference(split_conjunct,[status(thm)],[c240])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 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])).])).
% 234.17/234.35 cnf(c164,plain,~eqangle(X916,X909,X910,X914,X911,X912,X915,X913)|~perp(X911,X912,X915,X913)|perp(X916,X909,X910,X914),inference(split_conjunct,[status(thm)],[c163])).
% 234.17/234.35 cnf(c38357,plain,eqangle(X7706,X7705,X7705,X7706,X7703,X7704,X7703,X7704),inference(resolution,[status(thm)],[c31818, c347])).
% 234.17/234.35 cnf(c38436,plain,~perp(X8778,X8776,X8778,X8776)|perp(X8779,X8777,X8777,X8779),inference(resolution,[status(thm)],[c38357, c164])).
% 234.17/234.35 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)).
% 234.17/234.35 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])).
% 234.17/234.35 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])).
% 234.17/234.35 cnf(c227,plain,~cong(X997,X996,X995,X996)|~cong(X997,X994,X995,X994)|perp(X997,X995,X996,X994),inference(split_conjunct,[status(thm)],[c226])).
% 234.17/234.35 cnf(c1081,plain,~cong(X1262,X1260,X1261,X1260)|perp(X1262,X1261,X1260,X1260),inference(factor,[status(thm)],[c227])).
% 234.17/234.35 cnf(c39283,plain,perp(X8807,X8807,X8807,X8807),inference(resolution,[status(thm)],[c39257, c1081])).
% 234.17/234.35 cnf(c39329,plain,perp(X8827,X8828,X8828,X8827),inference(resolution,[status(thm)],[c39283, c38436])).
% 234.17/234.35 cnf(c39428,plain,~midp(X9791,X9790,X9790)|cong(X9790,X9791,X9792,X9791),inference(resolution,[status(thm)],[c39329, c241])).
% 234.17/234.35 cnf(c42186,plain,cong(X9793,X9794,X9795,X9794),inference(resolution,[status(thm)],[c39428, c39775])).
% 234.17/234.35 cnf(c42198,plain,cong(X9797,X9798,X9798,X9796),inference(resolution,[status(thm)],[c42186, c341])).
% 234.17/234.35 cnf(c42221,plain,cong(X9815,X9816,X9817,X9815),inference(resolution,[status(thm)],[c42198, c338])).
% 234.17/234.35 cnf(c42259,plain,cong(X9833,X9831,X9833,X9832),inference(resolution,[status(thm)],[c42221, c341])).
% 234.17/234.35 cnf(c42329,plain,$false,inference(resolution,[status(thm)],[c42259, c24])).
% 234.17/234.35 % SZS output end CNFRefutation
% 234.17/234.35
% 234.17/234.35 % Initial clauses : 136
% 234.17/234.35 % Processed clauses : 5135
% 234.17/234.35 % Factors computed : 153
% 234.17/234.35 % Resolvents computed: 41768
% 234.17/234.35 % Tautologies deleted: 12
% 234.17/234.35 % Forward subsumed : 8879
% 234.17/234.35 % Backward subsumed : 3443
% 234.17/234.35 % -------- CPU Time ---------
% 234.17/234.35 % User time : 233.908 s
% 234.17/234.35 % System time : 0.103 s
% 234.17/234.35 % Total time : 234.011 s
%------------------------------------------------------------------------------