%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO573+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:18 EDT 2024
% Result : Theorem 49.60s 49.76s
% Output : Refutation 49.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GEO573+1 : TPTP v8.1.2. Released v7.5.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n013.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:11:38 EDT 2024
% 0.14/0.37 % CPUTime :
% 49.60/49.76 % Version: 1.5
% 49.60/49.76 % SZS status Theorem
% 49.60/49.76 % SZS output start CNFRefutation
% 49.60/49.76 fof(exemplo6GDDFULL214035,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![K]:(![H]:(![NWPNT1]:(((((((((circle(O,A,B,C)&perp(D,C,A,B))&coll(D,A,B))&perp(E,B,A,C))&coll(E,A,C))&circle(O,C,K,NWPNT1))&coll(K,C,D))&coll(H,C,D))&coll(H,B,E))=>cong(A,K,A,H))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214035)).
% 49.60/49.76 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![K]:(![H]:(![NWPNT1]:(((((((((circle(O,A,B,C)&perp(D,C,A,B))&coll(D,A,B))&perp(E,B,A,C))&coll(E,A,C))&circle(O,C,K,NWPNT1))&coll(K,C,D))&coll(H,C,D))&coll(H,B,E))=>cong(A,K,A,H)))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214035])).
% 49.60/49.76 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(?[K]:(?[H]:(?[NWPNT1]:(((((((((circle(O,A,B,C)&perp(D,C,A,B))&coll(D,A,B))&perp(E,B,A,C))&coll(E,A,C))&circle(O,C,K,NWPNT1))&coll(K,C,D))&coll(H,C,D))&coll(H,B,E))&~cong(A,K,A,H))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 49.60/49.76 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(?[K]:(?[H]:(((((((((circle(O,A,B,C)&perp(D,C,A,B))&coll(D,A,B))&perp(E,B,A,C))&coll(E,A,C))&(?[NWPNT1]:circle(O,C,K,NWPNT1)))&coll(K,C,D))&coll(H,C,D))&coll(H,B,E))&~cong(A,K,A,H)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 49.60/49.76 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((circle(X5,X2,X3,X4)&perp(X6,X4,X2,X3))&coll(X6,X2,X3))&perp(X7,X3,X2,X4))&coll(X7,X2,X4))&(?[X10]:circle(X5,X4,X8,X10)))&coll(X8,X4,X6))&coll(X9,X4,X6))&coll(X9,X3,X7))&~cong(X2,X8,X2,X9)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 49.60/49.76 fof(c15,negated_conjecture,(((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&perp(skolem0005,skolem0003,skolem0001,skolem0002))&coll(skolem0005,skolem0001,skolem0002))&perp(skolem0006,skolem0002,skolem0001,skolem0003))&coll(skolem0006,skolem0001,skolem0003))&circle(skolem0004,skolem0003,skolem0007,skolem0009))&coll(skolem0007,skolem0003,skolem0005))&coll(skolem0008,skolem0003,skolem0005))&coll(skolem0008,skolem0002,skolem0006))&~cong(skolem0001,skolem0007,skolem0001,skolem0008)),inference(skolemize,[status(esa)],[c14])).
% 49.60/49.76 cnf(c25,negated_conjecture,~cong(skolem0001,skolem0007,skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c340,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 49.60/49.76 fof(c341,plain,(![X411]:(![X412]:(![X413]:(![X414]:(~cong(X411,X412,X413,X414)|cong(X411,X412,X414,X413)))))),inference(variable_rename,[status(thm)],[c340])).
% 49.60/49.76 cnf(c342,plain,~cong(X692,X690,X691,X693)|cong(X692,X690,X693,X691),inference(split_conjunct,[status(thm)],[c341])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 49.60/49.76 fof(c338,plain,(![X407]:(![X408]:(![X409]:(![X410]:(~cong(X407,X408,X409,X410)|cong(X409,X410,X407,X408)))))),inference(variable_rename,[status(thm)],[c337])).
% 49.60/49.76 cnf(c339,plain,~cong(X686,X688,X687,X689)|cong(X687,X689,X686,X688),inference(split_conjunct,[status(thm)],[c338])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c197,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])).
% 49.60/49.76 fof(c198,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)],[c197])).
% 49.60/49.76 cnf(c199,plain,~midp(X947,X946,X943)|~para(X946,X945,X943,X944)|~para(X946,X944,X943,X945)|midp(X947,X945,X944),inference(split_conjunct,[status(thm)],[c198])).
% 49.60/49.76 cnf(c1207,plain,~midp(X2328,X2326,X2325)|~para(X2326,X2327,X2325,X2327)|midp(X2328,X2327,X2327),inference(factor,[status(thm)],[c199])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c288,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])).
% 49.60/49.76 fof(c289,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)],[c288])).
% 49.60/49.76 fof(c291,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(c290,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)],[c289])).])).
% 49.60/49.76 cnf(c292,plain,~eqangle(X1066,X1065,X1063,X1062,X1061,X1064,X1063,X1062)|para(X1066,X1065,X1061,X1064),inference(split_conjunct,[status(thm)],[c291])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c352,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])).
% 49.60/49.76 fof(c353,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)],[c352])).
% 49.60/49.76 cnf(c354,plain,~eqangle(X1218,X1223,X1224,X1219,X1220,X1217,X1222,X1221)|eqangle(X1224,X1219,X1218,X1223,X1222,X1221,X1220,X1217),inference(split_conjunct,[status(thm)],[c353])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c283,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])).
% 49.60/49.76 fof(c284,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)],[c283])).
% 49.60/49.76 fof(c286,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(c285,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)],[c284])).])).
% 49.60/49.76 cnf(c287,plain,~para(X1058,X1059,X1060,X1056)|eqangle(X1058,X1059,X1055,X1057,X1060,X1056,X1055,X1057),inference(split_conjunct,[status(thm)],[c286])).
% 49.60/49.76 cnf(c19,negated_conjecture,perp(skolem0006,skolem0002,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c15])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 49.60/49.76 fof(c388,plain,(![X500]:(![X501]:(![X502]:(![X503]:(~perp(X500,X501,X502,X503)|perp(X502,X503,X500,X501)))))),inference(variable_rename,[status(thm)],[c387])).
% 49.60/49.76 cnf(c389,plain,~perp(X712,X713,X714,X711)|perp(X714,X711,X712,X713),inference(split_conjunct,[status(thm)],[c388])).
% 49.60/49.76 cnf(c510,plain,perp(skolem0001,skolem0003,skolem0006,skolem0002),inference(resolution,[status(thm)],[c389, c19])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c384,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])).
% 49.60/49.76 fof(c385,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)],[c384])).
% 49.60/49.76 cnf(c386,plain,~perp(X1269,X1274,X1273,X1270)|~perp(X1273,X1270,X1271,X1272)|para(X1269,X1274,X1271,X1272),inference(split_conjunct,[status(thm)],[c385])).
% 49.60/49.76 cnf(c1448,plain,~perp(X2612,X2613,skolem0006,skolem0002)|para(X2612,X2613,skolem0001,skolem0003),inference(resolution,[status(thm)],[c386, c19])).
% 49.60/49.76 cnf(c5711,plain,para(skolem0001,skolem0003,skolem0001,skolem0003),inference(resolution,[status(thm)],[c1448, c510])).
% 49.60/49.76 cnf(c5745,plain,eqangle(skolem0001,skolem0003,X3547,X3548,skolem0001,skolem0003,X3547,X3548),inference(resolution,[status(thm)],[c5711, c287])).
% 49.60/49.76 cnf(c7776,plain,eqangle(X3628,X3627,skolem0001,skolem0003,X3628,X3627,skolem0001,skolem0003),inference(resolution,[status(thm)],[c5745, c354])).
% 49.60/49.76 cnf(c8086,plain,para(X3632,X3633,X3632,X3633),inference(resolution,[status(thm)],[c7776, c292])).
% 49.60/49.76 cnf(c8123,plain,~midp(X5020,X5018,X5018)|midp(X5020,X5019,X5019),inference(resolution,[status(thm)],[c8086, c1207])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c402,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 49.60/49.76 fof(c403,plain,(![X522]:(![X523]:(![X524]:(![X525]:((~coll(X522,X523,X524)|~coll(X522,X523,X525))|coll(X524,X525,X522)))))),inference(variable_rename,[status(thm)],[c402])).
% 49.60/49.76 cnf(c404,plain,~coll(X773,X772,X771)|~coll(X773,X772,X770)|coll(X771,X770,X773),inference(split_conjunct,[status(thm)],[c403])).
% 49.60/49.76 cnf(c558,plain,~coll(X775,X774,X776)|coll(X776,X776,X775),inference(factor,[status(thm)],[c404])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c191,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 49.60/49.76 fof(c192,plain,(![X165]:(![X166]:(![X167]:(~para(X165,X166,X165,X167)|coll(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c191])).
% 49.60/49.76 cnf(c193,plain,~para(X685,X683,X685,X684)|coll(X685,X683,X684),inference(split_conjunct,[status(thm)],[c192])).
% 49.60/49.76 cnf(c8112,plain,coll(X3634,X3635,X3635),inference(resolution,[status(thm)],[c8086, c193])).
% 49.60/49.76 cnf(c8345,plain,coll(X3638,X3638,X3639),inference(resolution,[status(thm)],[c8112, c558])).
% 49.60/49.76 cnf(c9230,plain,~coll(X5240,X5240,X5241)|coll(X5241,X5242,X5240),inference(resolution,[status(thm)],[c8345, c404])).
% 49.60/49.76 cnf(c16077,plain,coll(X5250,X5249,X5248),inference(resolution,[status(thm)],[c9230, c8345])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c188,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 49.60/49.76 fof(c189,plain,(![X162]:(![X163]:(![X164]:((~cong(X162,X163,X162,X164)|~coll(X162,X163,X164))|midp(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c188])).
% 49.60/49.76 cnf(c190,plain,~cong(X937,X936,X937,X935)|~coll(X937,X936,X935)|midp(X937,X936,X935),inference(split_conjunct,[status(thm)],[c189])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 49.60/49.76 fof(c362,plain,(![X464]:(![X465]:(![X466]:(![X467]:(~cyclic(X464,X465,X466,X467)|cyclic(X465,X464,X466,X467)))))),inference(variable_rename,[status(thm)],[c361])).
% 49.60/49.76 cnf(c363,plain,~cyclic(X695,X696,X694,X697)|cyclic(X696,X695,X694,X697),inference(split_conjunct,[status(thm)],[c362])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 49.60/49.76 fof(c365,plain,(![X468]:(![X469]:(![X470]:(![X471]:(~cyclic(X468,X469,X470,X471)|cyclic(X468,X470,X469,X471)))))),inference(variable_rename,[status(thm)],[c364])).
% 49.60/49.76 cnf(c366,plain,~cyclic(X701,X700,X698,X699)|cyclic(X701,X698,X700,X699),inference(split_conjunct,[status(thm)],[c365])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c273,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])).
% 49.60/49.76 fof(c274,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)],[c273])).
% 49.60/49.76 cnf(c275,plain,~eqangle(X1043,X1044,X1043,X1046,X1045,X1044,X1045,X1046)|~coll(X1043,X1045,X1046)|cyclic(X1044,X1046,X1043,X1045),inference(split_conjunct,[status(thm)],[c274])).
% 49.60/49.76 cnf(c8115,plain,eqangle(X5011,X5009,X5010,X5012,X5011,X5009,X5010,X5012),inference(resolution,[status(thm)],[c8086, c287])).
% 49.60/49.76 cnf(c15914,plain,~coll(X5653,X5653,X5651)|cyclic(X5652,X5651,X5653,X5653),inference(resolution,[status(thm)],[c8115, c275])).
% 49.60/49.76 cnf(c16861,plain,cyclic(X5655,X5656,X5654,X5654),inference(resolution,[status(thm)],[c15914, c16077])).
% 49.60/49.76 cnf(c16862,plain,cyclic(X5658,X5657,X5659,X5657),inference(resolution,[status(thm)],[c16861, c366])).
% 49.60/49.76 cnf(c16877,plain,cyclic(X5675,X5676,X5677,X5675),inference(resolution,[status(thm)],[c16862, c363])).
% 49.60/49.76 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)).
% 49.60/49.76 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(fof_nnf,[status(thm)],[ruleD43])).
% 49.60/49.76 fof(c269,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)],[c268])).
% 49.60/49.76 fof(c271,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(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(variable_rename,[status(thm)],[c269])).])).
% 49.60/49.76 cnf(c272,plain,~cyclic(X1037,X1042,X1041,X1038)|~cyclic(X1037,X1042,X1041,X1040)|~cyclic(X1037,X1042,X1041,X1039)|~eqangle(X1041,X1037,X1041,X1042,X1039,X1038,X1039,X1040)|cong(X1037,X1042,X1038,X1040),inference(split_conjunct,[status(thm)],[c271])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c346,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])).
% 49.60/49.76 fof(c347,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)],[c346])).
% 49.60/49.76 cnf(c348,plain,~eqangle(X1208,X1207,X1202,X1204,X1206,X1205,X1201,X1203)|eqangle(X1208,X1207,X1206,X1205,X1202,X1204,X1201,X1203),inference(split_conjunct,[status(thm)],[c347])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 49.60/49.76 fof(c400,plain,(![X518]:(![X519]:(![X520]:(![X521]:(~para(X518,X519,X520,X521)|para(X518,X519,X521,X520)))))),inference(variable_rename,[status(thm)],[c399])).
% 49.60/49.76 cnf(c401,plain,~para(X761,X760,X763,X762)|para(X761,X760,X762,X763),inference(split_conjunct,[status(thm)],[c400])).
% 49.60/49.76 cnf(c8120,plain,para(X3660,X3661,X3661,X3660),inference(resolution,[status(thm)],[c8086, c401])).
% 49.60/49.76 cnf(c9299,plain,eqangle(X5394,X5396,X5395,X5397,X5396,X5394,X5395,X5397),inference(resolution,[status(thm)],[c8120, c287])).
% 49.60/49.76 cnf(c16503,plain,eqangle(X5439,X5436,X5437,X5438,X5439,X5436,X5438,X5437),inference(resolution,[status(thm)],[c9299, c354])).
% 49.60/49.76 cnf(c16566,plain,eqangle(X5493,X5494,X5493,X5494,X5492,X5491,X5491,X5492),inference(resolution,[status(thm)],[c16503, c348])).
% 49.60/49.76 cnf(c16634,plain,~cyclic(X6688,X6688,X6687,X6686)|cong(X6688,X6688,X6686,X6686),inference(resolution,[status(thm)],[c16566, c272])).
% 49.60/49.76 cnf(c17454,plain,cong(X6689,X6689,X6689,X6689),inference(resolution,[status(thm)],[c16634, c16877])).
% 49.60/49.76 cnf(c17471,plain,~coll(X6755,X6755,X6755)|midp(X6755,X6755,X6755),inference(resolution,[status(thm)],[c17454, c190])).
% 49.60/49.76 cnf(c17607,plain,midp(X6756,X6756,X6756),inference(resolution,[status(thm)],[c17471, c16077])).
% 49.60/49.76 cnf(c17721,plain,midp(X6761,X6762,X6762),inference(resolution,[status(thm)],[c17607, c8123])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c240,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])).
% 49.60/49.76 fof(c241,plain,(![X233]:(![X234]:(![X235]:(![X236]:((~perp(X233,X234,X234,X235)|~midp(X236,X233,X235))|cong(X233,X236,X234,X236)))))),inference(variable_rename,[status(thm)],[c240])).
% 49.60/49.76 cnf(c242,plain,~perp(X997,X999,X999,X1000)|~midp(X998,X997,X1000)|cong(X997,X998,X999,X998),inference(split_conjunct,[status(thm)],[c241])).
% 49.60/49.76 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)).
% 49.60/49.76 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(fof_nnf,[status(thm)],[ruleD74])).
% 49.60/49.76 fof(c162,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)],[c161])).
% 49.60/49.76 fof(c164,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(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(variable_rename,[status(thm)],[c162])).])).
% 49.60/49.76 cnf(c165,plain,~eqangle(X910,X909,X908,X912,X907,X905,X911,X906)|~perp(X907,X905,X911,X906)|perp(X910,X909,X908,X912),inference(split_conjunct,[status(thm)],[c164])).
% 49.60/49.76 cnf(c16508,plain,eqangle(X5449,X5448,X5448,X5449,X5446,X5447,X5446,X5447),inference(resolution,[status(thm)],[c9299, c348])).
% 49.60/49.76 cnf(c16573,plain,~perp(X6630,X6631,X6630,X6631)|perp(X6629,X6628,X6628,X6629),inference(resolution,[status(thm)],[c16508, c165])).
% 49.60/49.76 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)).
% 49.60/49.76 fof(c226,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])).
% 49.60/49.76 fof(c227,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)],[c226])).
% 49.60/49.76 cnf(c228,plain,~cong(X981,X984,X983,X984)|~cong(X981,X982,X983,X982)|perp(X981,X983,X984,X982),inference(split_conjunct,[status(thm)],[c227])).
% 49.60/49.76 cnf(c1276,plain,~cong(X1094,X1096,X1095,X1096)|perp(X1094,X1095,X1096,X1096),inference(factor,[status(thm)],[c228])).
% 49.60/49.76 cnf(c17466,plain,perp(X6703,X6703,X6703,X6703),inference(resolution,[status(thm)],[c17454, c1276])).
% 49.60/49.76 cnf(c17505,plain,perp(X6720,X6721,X6721,X6720),inference(resolution,[status(thm)],[c17466, c16573])).
% 49.60/49.76 cnf(c17544,plain,~midp(X7745,X7746,X7746)|cong(X7746,X7745,X7744,X7745),inference(resolution,[status(thm)],[c17505, c242])).
% 49.60/49.76 cnf(c19839,plain,cong(X7748,X7749,X7747,X7749),inference(resolution,[status(thm)],[c17544, c17721])).
% 49.60/49.76 cnf(c19853,plain,cong(X7762,X7761,X7761,X7763),inference(resolution,[status(thm)],[c19839, c342])).
% 49.60/49.76 cnf(c19880,plain,cong(X7781,X7782,X7783,X7781),inference(resolution,[status(thm)],[c19853, c339])).
% 49.60/49.76 cnf(c19945,plain,cong(X7810,X7811,X7810,X7812),inference(resolution,[status(thm)],[c19880, c342])).
% 49.60/49.76 cnf(c19958,plain,$false,inference(resolution,[status(thm)],[c19945, c25])).
% 49.60/49.76 % SZS output end CNFRefutation
% 49.60/49.76
% 49.60/49.76 % Initial clauses : 137
% 49.60/49.76 % Processed clauses : 2562
% 49.60/49.76 % Factors computed : 169
% 49.60/49.76 % Resolvents computed: 19390
% 49.60/49.76 % Tautologies deleted: 12
% 49.60/49.76 % Forward subsumed : 6175
% 49.60/49.76 % Backward subsumed : 1445
% 49.60/49.76 % -------- CPU Time ---------
% 49.60/49.76 % User time : 49.359 s
% 49.60/49.76 % System time : 0.041 s
% 49.60/49.76 % Total time : 49.400 s
%------------------------------------------------------------------------------