%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO570+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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 92.92s 93.19s
% Output : Refutation 92.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO570+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 : n006.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 08:20:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 92.92/93.19 % Version: 1.5
% 92.92/93.19 % SZS status Theorem
% 92.92/93.19 % SZS output start CNFRefutation
% 92.92/93.19 fof(exemplo6GDDFULL214032,conjecture,(![B]:(![C]:(![R]:(![O]:(![S]:(![A]:(![M]:(![N]:(![NWPNT1]:((((((((circle(O,B,C,R)&circle(O,B,S,NWPNT1))&coll(A,B,R))&coll(A,C,S))&perp(M,A,R,S))&coll(M,R,S))&perp(N,A,B,C))&coll(N,B,C))=>eqangle(B,A,A,M,N,A,A,C))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214032)).
% 92.92/93.19 fof(c11,negated_conjecture,(~(![B]:(![C]:(![R]:(![O]:(![S]:(![A]:(![M]:(![N]:(![NWPNT1]:((((((((circle(O,B,C,R)&circle(O,B,S,NWPNT1))&coll(A,B,R))&coll(A,C,S))&perp(M,A,R,S))&coll(M,R,S))&perp(N,A,B,C))&coll(N,B,C))=>eqangle(B,A,A,M,N,A,A,C)))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214032])).
% 92.92/93.19 fof(c12,negated_conjecture,(?[B]:(?[C]:(?[R]:(?[O]:(?[S]:(?[A]:(?[M]:(?[N]:(?[NWPNT1]:((((((((circle(O,B,C,R)&circle(O,B,S,NWPNT1))&coll(A,B,R))&coll(A,C,S))&perp(M,A,R,S))&coll(M,R,S))&perp(N,A,B,C))&coll(N,B,C))&~eqangle(B,A,A,M,N,A,A,C))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 92.92/93.19 fof(c13,negated_conjecture,(?[B]:(?[C]:(?[R]:(?[O]:(?[S]:(?[A]:(?[M]:(?[N]:((((((((circle(O,B,C,R)&(?[NWPNT1]:circle(O,B,S,NWPNT1)))&coll(A,B,R))&coll(A,C,S))&perp(M,A,R,S))&coll(M,R,S))&perp(N,A,B,C))&coll(N,B,C))&~eqangle(B,A,A,M,N,A,A,C)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 92.92/93.19 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((circle(X5,X2,X3,X4)&(?[X10]:circle(X5,X2,X6,X10)))&coll(X7,X2,X4))&coll(X7,X3,X6))&perp(X8,X7,X4,X6))&coll(X8,X4,X6))&perp(X9,X7,X2,X3))&coll(X9,X2,X3))&~eqangle(X2,X7,X7,X8,X9,X7,X7,X3)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 92.92/93.19 fof(c15,negated_conjecture,((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0009))&coll(skolem0006,skolem0001,skolem0003))&coll(skolem0006,skolem0002,skolem0005))&perp(skolem0007,skolem0006,skolem0003,skolem0005))&coll(skolem0007,skolem0003,skolem0005))&perp(skolem0008,skolem0006,skolem0001,skolem0002))&coll(skolem0008,skolem0001,skolem0002))&~eqangle(skolem0001,skolem0006,skolem0006,skolem0007,skolem0008,skolem0006,skolem0006,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 92.92/93.19 cnf(c24,negated_conjecture,~eqangle(skolem0001,skolem0006,skolem0006,skolem0007,skolem0008,skolem0006,skolem0006,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c347,plain,~eqangle(X1219,X1218,X1217,X1224,X1221,X1220,X1223,X1222)|eqangle(X1219,X1218,X1221,X1220,X1217,X1224,X1223,X1222),inference(split_conjunct,[status(thm)],[c346])).
% 92.92/93.19 fof(ruleD22,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(![E]:(![F]:(![G]:(![H]:((eqangle(A,B,C,D,P,Q,U,V)&eqangle(P,Q,U,V,E,F,G,H))=>eqangle(A,B,C,D,E,F,G,H)))))))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD22)).
% 92.92/93.19 fof(c342,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(![E]:(![F]:(![G]:(![H]:((~eqangle(A,B,C,D,P,Q,U,V)|~eqangle(P,Q,U,V,E,F,G,H))|eqangle(A,B,C,D,E,F,G,H)))))))))))))),inference(fof_nnf,[status(thm)],[ruleD22])).
% 92.92/93.19 fof(c343,plain,(![X415]:(![X416]:(![X417]:(![X418]:(![X419]:(![X420]:(![X421]:(![X422]:(![X423]:(![X424]:(![X425]:(![X426]:((~eqangle(X415,X416,X417,X418,X419,X420,X421,X422)|~eqangle(X419,X420,X421,X422,X423,X424,X425,X426))|eqangle(X415,X416,X417,X418,X423,X424,X425,X426)))))))))))))),inference(variable_rename,[status(thm)],[c342])).
% 92.92/93.19 cnf(c344,plain,~eqangle(X1212,X1206,X1211,X1208,X1216,X1207,X1215,X1210)|~eqangle(X1216,X1207,X1215,X1210,X1205,X1213,X1214,X1209)|eqangle(X1212,X1206,X1211,X1208,X1205,X1213,X1214,X1209),inference(split_conjunct,[status(thm)],[c343])).
% 92.92/93.19 fof(ruleD41,axiom,(![A]:(![B]:(![P]:(![Q]:(cyclic(A,B,P,Q)=>eqangle(P,A,P,B,Q,A,Q,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD41)).
% 92.92/93.19 fof(c279,plain,(![A]:(![B]:(![P]:(![Q]:(~cyclic(A,B,P,Q)|eqangle(P,A,P,B,Q,A,Q,B)))))),inference(fof_nnf,[status(thm)],[ruleD41])).
% 92.92/93.19 fof(c280,plain,(![X287]:(![X288]:(![X289]:(![X290]:(~cyclic(X287,X288,X289,X290)|eqangle(X289,X287,X289,X288,X290,X287,X290,X288)))))),inference(variable_rename,[status(thm)],[c279])).
% 92.92/93.19 cnf(c281,plain,~cyclic(X1070,X1069,X1071,X1072)|eqangle(X1071,X1070,X1071,X1069,X1072,X1070,X1072,X1069),inference(split_conjunct,[status(thm)],[c280])).
% 92.92/93.19 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 92.92/93.19 fof(c366,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 92.92/93.19 fof(c367,plain,(![X472]:(![X473]:(![X474]:(![X475]:(~cyclic(X472,X473,X474,X475)|cyclic(X472,X473,X475,X474)))))),inference(variable_rename,[status(thm)],[c366])).
% 92.92/93.19 cnf(c368,plain,~cyclic(X693,X690,X691,X692)|cyclic(X693,X690,X692,X691),inference(split_conjunct,[status(thm)],[c367])).
% 92.92/93.19 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)).
% 92.92/93.19 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 92.92/93.19 fof(c364,plain,(![X468]:(![X469]:(![X470]:(![X471]:(~cyclic(X468,X469,X470,X471)|cyclic(X468,X470,X469,X471)))))),inference(variable_rename,[status(thm)],[c363])).
% 92.92/93.19 cnf(c365,plain,~cyclic(X688,X687,X689,X686)|cyclic(X688,X689,X687,X686),inference(split_conjunct,[status(thm)],[c364])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c403,plain,~coll(X749,X750,X747)|~coll(X749,X750,X748)|coll(X747,X748,X749),inference(split_conjunct,[status(thm)],[c402])).
% 92.92/93.19 cnf(c536,plain,~coll(X756,X757,X758)|coll(X758,X758,X756),inference(factor,[status(thm)],[c403])).
% 92.92/93.19 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)).
% 92.92/93.19 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 92.92/93.19 fof(c191,plain,(![X165]:(![X166]:(![X167]:(~para(X165,X166,X165,X167)|coll(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c190])).
% 92.92/93.19 cnf(c192,plain,~para(X667,X666,X667,X665)|coll(X667,X666,X665),inference(split_conjunct,[status(thm)],[c191])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 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])).])).
% 92.92/93.19 cnf(c291,plain,~eqangle(X1083,X1084,X1087,X1082,X1086,X1085,X1087,X1082)|para(X1083,X1084,X1086,X1085),inference(split_conjunct,[status(thm)],[c290])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c353,plain,~eqangle(X1234,X1239,X1238,X1233,X1240,X1236,X1237,X1235)|eqangle(X1238,X1233,X1234,X1239,X1237,X1235,X1240,X1236),inference(split_conjunct,[status(thm)],[c352])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 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])).])).
% 92.92/93.19 cnf(c286,plain,~para(X1079,X1078,X1074,X1077)|eqangle(X1079,X1078,X1076,X1075,X1074,X1077,X1076,X1075),inference(split_conjunct,[status(thm)],[c285])).
% 92.92/93.19 cnf(c22,negated_conjecture,perp(skolem0008,skolem0006,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 92.92/93.19 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)).
% 92.92/93.19 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 92.92/93.19 fof(c387,plain,(![X500]:(![X501]:(![X502]:(![X503]:(~perp(X500,X501,X502,X503)|perp(X502,X503,X500,X501)))))),inference(variable_rename,[status(thm)],[c386])).
% 92.92/93.19 cnf(c388,plain,~perp(X695,X696,X697,X694)|perp(X697,X694,X695,X696),inference(split_conjunct,[status(thm)],[c387])).
% 92.92/93.19 cnf(c490,plain,perp(skolem0001,skolem0002,skolem0008,skolem0006),inference(resolution,[status(thm)],[c388, c22])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c385,plain,~perp(X1274,X1272,X1271,X1269)|~perp(X1271,X1269,X1273,X1270)|para(X1274,X1272,X1273,X1270),inference(split_conjunct,[status(thm)],[c384])).
% 92.92/93.19 cnf(c1508,plain,~perp(X2641,X2640,skolem0001,skolem0002)|para(X2641,X2640,skolem0008,skolem0006),inference(resolution,[status(thm)],[c385, c490])).
% 92.92/93.19 cnf(c5772,plain,para(skolem0008,skolem0006,skolem0008,skolem0006),inference(resolution,[status(thm)],[c1508, c22])).
% 92.92/93.19 cnf(c5804,plain,eqangle(skolem0008,skolem0006,X3515,X3516,skolem0008,skolem0006,X3515,X3516),inference(resolution,[status(thm)],[c5772, c286])).
% 92.92/93.19 cnf(c7739,plain,eqangle(X3589,X3590,skolem0008,skolem0006,X3589,X3590,skolem0008,skolem0006),inference(resolution,[status(thm)],[c5804, c353])).
% 92.92/93.19 cnf(c8038,plain,para(X3596,X3595,X3596,X3595),inference(resolution,[status(thm)],[c7739, c291])).
% 92.92/93.19 cnf(c8080,plain,coll(X3597,X3598,X3598),inference(resolution,[status(thm)],[c8038, c192])).
% 92.92/93.19 cnf(c8421,plain,coll(X3604,X3604,X3603),inference(resolution,[status(thm)],[c8080, c536])).
% 92.92/93.19 cnf(c9000,plain,~coll(X5190,X5190,X5189)|coll(X5189,X5191,X5190),inference(resolution,[status(thm)],[c8421, c403])).
% 92.92/93.19 cnf(c16124,plain,coll(X5199,X5200,X5201),inference(resolution,[status(thm)],[c9000, c8421])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c274,plain,~eqangle(X1059,X1060,X1059,X1061,X1062,X1060,X1062,X1061)|~coll(X1059,X1062,X1061)|cyclic(X1060,X1061,X1059,X1062),inference(split_conjunct,[status(thm)],[c273])).
% 92.92/93.19 cnf(c8076,plain,eqangle(X4963,X4961,X4962,X4964,X4963,X4961,X4962,X4964),inference(resolution,[status(thm)],[c8038, c286])).
% 92.92/93.19 cnf(c15908,plain,~coll(X5605,X5605,X5603)|cyclic(X5604,X5603,X5605,X5605),inference(resolution,[status(thm)],[c8076, c274])).
% 92.92/93.19 cnf(c16833,plain,cyclic(X5608,X5607,X5606,X5606),inference(resolution,[status(thm)],[c15908, c16124])).
% 92.92/93.19 cnf(c16841,plain,cyclic(X5618,X5619,X5620,X5619),inference(resolution,[status(thm)],[c16833, c365])).
% 92.92/93.19 cnf(c16844,plain,cyclic(X5625,X5626,X5626,X5624),inference(resolution,[status(thm)],[c16841, c368])).
% 92.92/93.19 cnf(c16863,plain,eqangle(X5690,X5691,X5690,X5690,X5692,X5691,X5692,X5690),inference(resolution,[status(thm)],[c16844, c281])).
% 92.92/93.19 cnf(c16912,plain,~eqangle(X41622,X41623,X41625,X41624,X41621,X41626,X41621,X41621)|eqangle(X41622,X41623,X41625,X41624,X41627,X41626,X41627,X41621),inference(resolution,[status(thm)],[c16863, c344])).
% 92.92/93.19 cnf(c16847,plain,eqangle(X5678,X5679,X5678,X5680,X5680,X5679,X5680,X5680),inference(resolution,[status(thm)],[c16841, c281])).
% 92.92/93.19 cnf(c16884,plain,~eqangle(X34785,X34786,X34788,X34787,X34790,X34789,X34790,X34784)|eqangle(X34785,X34786,X34788,X34787,X34784,X34789,X34784,X34784),inference(resolution,[status(thm)],[c16847, c344])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c189,plain,~cong(X935,X936,X935,X937)|~coll(X935,X936,X937)|midp(X935,X936,X937),inference(split_conjunct,[status(thm)],[c188])).
% 92.92/93.19 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)).
% 92.92/93.19 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 92.92/93.19 fof(c340,plain,(![X411]:(![X412]:(![X413]:(![X414]:(~cong(X411,X412,X413,X414)|cong(X411,X412,X414,X413)))))),inference(variable_rename,[status(thm)],[c339])).
% 92.92/93.19 cnf(c341,plain,~cong(X673,X672,X675,X674)|cong(X673,X672,X674,X675),inference(split_conjunct,[status(thm)],[c340])).
% 92.92/93.19 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)).
% 92.92/93.19 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 92.92/93.19 fof(c337,plain,(![X407]:(![X408]:(![X409]:(![X410]:(~cong(X407,X408,X409,X410)|cong(X409,X410,X407,X408)))))),inference(variable_rename,[status(thm)],[c336])).
% 92.92/93.19 cnf(c338,plain,~cong(X669,X668,X671,X670)|cong(X671,X670,X669,X668),inference(split_conjunct,[status(thm)],[c337])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c198,plain,~midp(X946,X943,X945)|~para(X943,X944,X945,X947)|~para(X943,X947,X945,X944)|midp(X946,X944,X947),inference(split_conjunct,[status(thm)],[c197])).
% 92.92/93.19 cnf(c1164,plain,~midp(X2273,X2272,X2271)|~para(X2272,X2274,X2271,X2274)|midp(X2273,X2274,X2274),inference(factor,[status(thm)],[c198])).
% 92.92/93.19 cnf(c8070,plain,~midp(X4960,X4958,X4958)|midp(X4960,X4959,X4959),inference(resolution,[status(thm)],[c8038, c1164])).
% 92.92/93.19 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)).
% 92.92/93.19 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 92.92/93.19 fof(c361,plain,(![X464]:(![X465]:(![X466]:(![X467]:(~cyclic(X464,X465,X466,X467)|cyclic(X465,X464,X466,X467)))))),inference(variable_rename,[status(thm)],[c360])).
% 92.92/93.19 cnf(c362,plain,~cyclic(X677,X676,X678,X679)|cyclic(X676,X677,X678,X679),inference(split_conjunct,[status(thm)],[c361])).
% 92.92/93.19 cnf(c16842,plain,cyclic(X5623,X5622,X5621,X5623),inference(resolution,[status(thm)],[c16841, c362])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 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])).])).
% 92.92/93.19 cnf(c271,plain,~cyclic(X1056,X1052,X1053,X1054)|~cyclic(X1056,X1052,X1053,X1051)|~cyclic(X1056,X1052,X1053,X1055)|~eqangle(X1053,X1056,X1053,X1052,X1055,X1054,X1055,X1051)|cong(X1056,X1052,X1054,X1051),inference(split_conjunct,[status(thm)],[c270])).
% 92.92/93.19 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)).
% 92.92/93.19 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 92.92/93.19 fof(c399,plain,(![X518]:(![X519]:(![X520]:(![X521]:(~para(X518,X519,X520,X521)|para(X518,X519,X521,X520)))))),inference(variable_rename,[status(thm)],[c398])).
% 92.92/93.19 cnf(c400,plain,~para(X738,X740,X737,X739)|para(X738,X740,X739,X737),inference(split_conjunct,[status(thm)],[c399])).
% 92.92/93.19 cnf(c8068,plain,para(X3622,X3621,X3621,X3622),inference(resolution,[status(thm)],[c8038, c400])).
% 92.92/93.19 cnf(c9253,plain,eqangle(X5345,X5347,X5346,X5348,X5347,X5345,X5346,X5348),inference(resolution,[status(thm)],[c8068, c286])).
% 92.92/93.19 cnf(c16477,plain,eqangle(X5385,X5386,X5387,X5388,X5385,X5386,X5388,X5387),inference(resolution,[status(thm)],[c9253, c353])).
% 92.92/93.19 cnf(c16536,plain,eqangle(X5438,X5436,X5438,X5436,X5437,X5439,X5439,X5437),inference(resolution,[status(thm)],[c16477, c347])).
% 92.92/93.19 cnf(c16606,plain,~cyclic(X6649,X6649,X6650,X6648)|cong(X6649,X6649,X6648,X6648),inference(resolution,[status(thm)],[c16536, c271])).
% 92.92/93.19 cnf(c17426,plain,cong(X6651,X6651,X6651,X6651),inference(resolution,[status(thm)],[c16606, c16842])).
% 92.92/93.19 cnf(c17438,plain,~coll(X6724,X6724,X6724)|midp(X6724,X6724,X6724),inference(resolution,[status(thm)],[c17426, c189])).
% 92.92/93.19 cnf(c17581,plain,midp(X6725,X6725,X6725),inference(resolution,[status(thm)],[c17438, c16124])).
% 92.92/93.19 cnf(c17752,plain,midp(X6728,X6727,X6727),inference(resolution,[status(thm)],[c17581, c8070])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c241,plain,~perp(X997,X1000,X1000,X998)|~midp(X999,X997,X998)|cong(X997,X999,X1000,X999),inference(split_conjunct,[status(thm)],[c240])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 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])).])).
% 92.92/93.19 cnf(c164,plain,~eqangle(X909,X906,X907,X912,X910,X908,X905,X911)|~perp(X910,X908,X905,X911)|perp(X909,X906,X907,X912),inference(split_conjunct,[status(thm)],[c163])).
% 92.92/93.19 cnf(c16478,plain,eqangle(X5394,X5392,X5392,X5394,X5391,X5393,X5391,X5393),inference(resolution,[status(thm)],[c9253, c347])).
% 92.92/93.19 cnf(c16543,plain,~perp(X6587,X6589,X6587,X6589)|perp(X6586,X6588,X6588,X6586),inference(resolution,[status(thm)],[c16478, c164])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c227,plain,~cong(X984,X981,X982,X981)|~cong(X984,X983,X982,X983)|perp(X984,X982,X981,X983),inference(split_conjunct,[status(thm)],[c226])).
% 92.92/93.19 cnf(c1167,plain,~cong(X1026,X1025,X1024,X1025)|perp(X1026,X1024,X1025,X1025),inference(factor,[status(thm)],[c227])).
% 92.92/93.19 cnf(c17441,plain,perp(X6668,X6668,X6668,X6668),inference(resolution,[status(thm)],[c17426, c1167])).
% 92.92/93.19 cnf(c17470,plain,perp(X6681,X6680,X6680,X6681),inference(resolution,[status(thm)],[c17441, c16543])).
% 92.92/93.19 cnf(c17517,plain,~midp(X7701,X7702,X7702)|cong(X7702,X7701,X7703,X7701),inference(resolution,[status(thm)],[c17470, c241])).
% 92.92/93.19 cnf(c19737,plain,cong(X7708,X7707,X7709,X7707),inference(resolution,[status(thm)],[c17517, c17752])).
% 92.92/93.19 cnf(c19755,plain,cong(X7720,X7718,X7718,X7719),inference(resolution,[status(thm)],[c19737, c341])).
% 92.92/93.19 cnf(c19782,plain,cong(X7736,X7737,X7738,X7736),inference(resolution,[status(thm)],[c19755, c338])).
% 92.92/93.19 cnf(c19844,plain,cong(X7767,X7769,X7767,X7768),inference(resolution,[status(thm)],[c19782, c341])).
% 92.92/93.19 cnf(c19863,plain,~coll(X8034,X8035,X8033)|midp(X8034,X8035,X8033),inference(resolution,[status(thm)],[c19844, c189])).
% 92.92/93.19 cnf(c20993,plain,midp(X8038,X8036,X8037),inference(resolution,[status(thm)],[c19863, c16124])).
% 92.92/93.19 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)).
% 92.92/93.19 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])).
% 92.92/93.19 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])).
% 92.92/93.19 cnf(c266,plain,~midp(X1046,X1044,X1043)|~midp(X1042,X1044,X1045)|para(X1046,X1042,X1043,X1045),inference(split_conjunct,[status(thm)],[c265])).
% 92.92/93.19 cnf(c17998,plain,~midp(X11713,X11712,X11710)|para(X11713,X11711,X11710,X11712),inference(resolution,[status(thm)],[c17752, c266])).
% 92.92/93.19 cnf(c23907,plain,para(X11714,X11717,X11716,X11715),inference(resolution,[status(thm)],[c17998, c20993])).
% 92.92/93.19 cnf(c23921,plain,eqangle(X11974,X11975,X11979,X11978,X11977,X11976,X11979,X11978),inference(resolution,[status(thm)],[c23907, c286])).
% 92.92/93.19 cnf(c24134,plain,eqangle(X11987,X11988,X11986,X11991,X11987,X11988,X11990,X11989),inference(resolution,[status(thm)],[c23921, c353])).
% 92.92/93.19 cnf(c28048,plain,eqangle(X34998,X35000,X35001,X35002,X34999,X35000,X34999,X34999),inference(resolution,[status(thm)],[c16884, c24134])).
% 92.92/93.19 cnf(c29927,plain,eqangle(X41688,X41685,X41686,X41690,X41687,X41685,X41687,X41689),inference(resolution,[status(thm)],[c16912, c28048])).
% 92.92/93.19 cnf(c30103,plain,eqangle(X42532,X42529,X42527,X42529,X42531,X42528,X42527,X42530),inference(resolution,[status(thm)],[c29927, c347])).
% 92.92/93.19 cnf(c30285,plain,eqangle(X43201,X43202,X43203,X43202,X43199,X43200,X43199,X43199),inference(resolution,[status(thm)],[c30103, c16884])).
% 92.92/93.19 cnf(c31020,plain,eqangle(X46437,X46435,X46434,X46435,X46433,X46432,X46433,X46436),inference(resolution,[status(thm)],[c30285, c16912])).
% 92.92/93.19 cnf(c31651,plain,eqangle(X49128,X49124,X49123,X49125,X49127,X49124,X49123,X49126),inference(resolution,[status(thm)],[c31020, c347])).
% 92.92/93.19 cnf(c31996,plain,$false,inference(resolution,[status(thm)],[c31651, c24])).
% 92.92/93.19 % SZS output end CNFRefutation
% 92.92/93.19
% 92.92/93.19 % Initial clauses : 136
% 92.92/93.19 % Processed clauses : 3760
% 92.92/93.19 % Factors computed : 295
% 92.92/93.19 % Resolvents computed: 31301
% 92.92/93.19 % Tautologies deleted: 71
% 92.92/93.19 % Forward subsumed : 18239
% 92.92/93.19 % Backward subsumed : 3585
% 92.92/93.19 % -------- CPU Time ---------
% 92.92/93.19 % User time : 92.727 s
% 92.92/93.19 % System time : 0.077 s
% 92.92/93.19 % Total time : 92.804 s
%------------------------------------------------------------------------------