%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO576+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:22:19 EDT 2024
% Result : Theorem 49.51s 49.70s
% Output : Refutation 49.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GEO576+1 : TPTP v8.1.2. Released v7.5.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n003.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 07:48:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 49.51/49.70 % Version: 1.5
% 49.51/49.70 % SZS status Theorem
% 49.51/49.70 % SZS output start CNFRefutation
% 49.51/49.70 fof(exemplo6GDDFULL214038,conjecture,(![A]:(![B]:(![C]:(![D]:(![O]:(![D1]:(![P]:(![NWPNT1]:(((((((perp(D,A,B,C)&coll(D,B,C))&circle(O,A,B,C))&circle(O,A,D1,NWPNT1))&coll(D1,A,D))&perp(A,C,D1,P))&coll(P,B,C))=>eqangle(O,A,A,D,C,A,A,P)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214038)).
% 49.51/49.70 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![O]:(![D1]:(![P]:(![NWPNT1]:(((((((perp(D,A,B,C)&coll(D,B,C))&circle(O,A,B,C))&circle(O,A,D1,NWPNT1))&coll(D1,A,D))&perp(A,C,D1,P))&coll(P,B,C))=>eqangle(O,A,A,D,C,A,A,P))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214038])).
% 49.51/49.70 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[O]:(?[D1]:(?[P]:(?[NWPNT1]:(((((((perp(D,A,B,C)&coll(D,B,C))&circle(O,A,B,C))&circle(O,A,D1,NWPNT1))&coll(D1,A,D))&perp(A,C,D1,P))&coll(P,B,C))&~eqangle(O,A,A,D,C,A,A,P)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 49.51/49.70 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[O]:(?[D1]:(?[P]:(((((((perp(D,A,B,C)&coll(D,B,C))&circle(O,A,B,C))&(?[NWPNT1]:circle(O,A,D1,NWPNT1)))&coll(D1,A,D))&perp(A,C,D1,P))&coll(P,B,C))&~eqangle(O,A,A,D,C,A,A,P))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 49.51/49.70 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((perp(X5,X2,X3,X4)&coll(X5,X3,X4))&circle(X6,X2,X3,X4))&(?[X9]:circle(X6,X2,X7,X9)))&coll(X7,X2,X5))&perp(X2,X4,X7,X8))&coll(X8,X3,X4))&~eqangle(X6,X2,X2,X5,X4,X2,X2,X8))))))))),inference(variable_rename,[status(thm)],[c13])).
% 49.51/49.70 fof(c15,negated_conjecture,(((((((perp(skolem0004,skolem0001,skolem0002,skolem0003)&coll(skolem0004,skolem0002,skolem0003))&circle(skolem0005,skolem0001,skolem0002,skolem0003))&circle(skolem0005,skolem0001,skolem0006,skolem0008))&coll(skolem0006,skolem0001,skolem0004))&perp(skolem0001,skolem0003,skolem0006,skolem0007))&coll(skolem0007,skolem0002,skolem0003))&~eqangle(skolem0005,skolem0001,skolem0001,skolem0004,skolem0003,skolem0001,skolem0001,skolem0007)),inference(skolemize,[status(esa)],[c14])).
% 49.51/49.70 cnf(c23,negated_conjecture,~eqangle(skolem0005,skolem0001,skolem0001,skolem0004,skolem0003,skolem0001,skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 49.51/49.70 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.51/49.70 fof(c344,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.51/49.70 fof(c345,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)],[c344])).
% 49.51/49.70 cnf(c346,plain,~eqangle(X1213,X1217,X1218,X1215,X1212,X1216,X1211,X1214)|eqangle(X1213,X1217,X1212,X1216,X1218,X1215,X1211,X1214),inference(split_conjunct,[status(thm)],[c345])).
% 49.51/49.70 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)).
% 49.51/49.70 fof(c341,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])).
% 49.51/49.70 fof(c342,plain,(![X414]:(![X415]:(![X416]:(![X417]:(![X418]:(![X419]:(![X420]:(![X421]:(![X422]:(![X423]:(![X424]:(![X425]:((~eqangle(X414,X415,X416,X417,X418,X419,X420,X421)|~eqangle(X418,X419,X420,X421,X422,X423,X424,X425))|eqangle(X414,X415,X416,X417,X422,X423,X424,X425)))))))))))))),inference(variable_rename,[status(thm)],[c341])).
% 49.51/49.70 cnf(c343,plain,~eqangle(X1200,X1199,X1205,X1203,X1210,X1201,X1207,X1204)|~eqangle(X1210,X1201,X1207,X1204,X1209,X1202,X1206,X1208)|eqangle(X1200,X1199,X1205,X1203,X1209,X1202,X1206,X1208),inference(split_conjunct,[status(thm)],[c342])).
% 49.51/49.70 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)).
% 49.51/49.70 fof(c278,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])).
% 49.51/49.70 fof(c279,plain,(![X286]:(![X287]:(![X288]:(![X289]:(~cyclic(X286,X287,X288,X289)|eqangle(X288,X286,X288,X287,X289,X286,X289,X287)))))),inference(variable_rename,[status(thm)],[c278])).
% 49.51/49.70 cnf(c280,plain,~cyclic(X1079,X1078,X1077,X1076)|eqangle(X1077,X1079,X1077,X1078,X1076,X1079,X1076,X1078),inference(split_conjunct,[status(thm)],[c279])).
% 49.51/49.70 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)).
% 49.51/49.70 fof(c365,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 49.51/49.70 fof(c366,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c365])).
% 49.51/49.70 cnf(c367,plain,~cyclic(X674,X672,X671,X673)|cyclic(X674,X672,X673,X671),inference(split_conjunct,[status(thm)],[c366])).
% 49.51/49.70 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.51/49.70 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 49.51/49.70 fof(c363,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c362])).
% 49.51/49.70 cnf(c364,plain,~cyclic(X668,X669,X670,X667)|cyclic(X668,X670,X669,X667),inference(split_conjunct,[status(thm)],[c363])).
% 49.51/49.70 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.51/49.70 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 49.51/49.70 fof(c401,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c400])).
% 49.51/49.70 cnf(c402,plain,~coll(X739,X737,X740)|~coll(X739,X737,X738)|coll(X740,X738,X739),inference(split_conjunct,[status(thm)],[c401])).
% 49.51/49.70 cnf(c517,plain,~coll(X741,X742,X743)|coll(X743,X743,X741),inference(factor,[status(thm)],[c402])).
% 49.51/49.70 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.51/49.70 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 49.51/49.70 fof(c190,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c189])).
% 49.51/49.70 cnf(c191,plain,~para(X641,X640,X641,X642)|coll(X641,X640,X642),inference(split_conjunct,[status(thm)],[c190])).
% 49.51/49.70 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.51/49.70 fof(c286,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.51/49.70 fof(c287,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)],[c286])).
% 49.51/49.70 fof(c289,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(c288,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)],[c287])).])).
% 49.51/49.70 cnf(c290,plain,~eqangle(X1088,X1093,X1089,X1092,X1091,X1090,X1089,X1092)|para(X1088,X1093,X1091,X1090),inference(split_conjunct,[status(thm)],[c289])).
% 49.51/49.70 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.51/49.70 fof(c350,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.51/49.70 fof(c351,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)],[c350])).
% 49.51/49.70 cnf(c352,plain,~eqangle(X1228,X1227,X1230,X1229,X1233,X1234,X1232,X1231)|eqangle(X1230,X1229,X1228,X1227,X1232,X1231,X1233,X1234),inference(split_conjunct,[status(thm)],[c351])).
% 49.51/49.70 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.51/49.70 fof(c281,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.51/49.70 fof(c282,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)],[c281])).
% 49.51/49.70 fof(c284,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(c283,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)],[c282])).])).
% 49.51/49.70 cnf(c285,plain,~para(X1082,X1086,X1084,X1085)|eqangle(X1082,X1086,X1083,X1081,X1084,X1085,X1083,X1081),inference(split_conjunct,[status(thm)],[c284])).
% 49.51/49.70 cnf(c21,negated_conjecture,perp(skolem0001,skolem0003,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 49.51/49.70 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.51/49.70 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 49.51/49.70 fof(c386,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c385])).
% 49.51/49.70 cnf(c387,plain,~perp(X676,X675,X678,X677)|perp(X678,X677,X676,X675),inference(split_conjunct,[status(thm)],[c386])).
% 49.51/49.70 cnf(c471,plain,perp(skolem0006,skolem0007,skolem0001,skolem0003),inference(resolution,[status(thm)],[c387, c21])).
% 49.51/49.70 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)).
% 49.51/49.70 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 49.51/49.70 fof(c389,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c388])).
% 49.51/49.70 cnf(c390,plain,~perp(X694,X692,X693,X691)|perp(X694,X692,X691,X693),inference(split_conjunct,[status(thm)],[c389])).
% 49.51/49.70 cnf(c477,plain,perp(skolem0006,skolem0007,skolem0003,skolem0001),inference(resolution,[status(thm)],[c390, c471])).
% 49.51/49.70 cnf(c483,plain,perp(skolem0003,skolem0001,skolem0006,skolem0007),inference(resolution,[status(thm)],[c477, c387])).
% 49.51/49.70 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.51/49.70 fof(c382,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.51/49.70 fof(c383,plain,(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:((~perp(X493,X494,X495,X496)|~perp(X495,X496,X497,X498))|para(X493,X494,X497,X498)))))))),inference(variable_rename,[status(thm)],[c382])).
% 49.51/49.70 cnf(c384,plain,~perp(X1266,X1267,X1263,X1265)|~perp(X1263,X1265,X1268,X1264)|para(X1266,X1267,X1268,X1264),inference(split_conjunct,[status(thm)],[c383])).
% 49.51/49.70 cnf(c1484,plain,~perp(X2607,X2606,skolem0003,skolem0001)|para(X2607,X2606,skolem0006,skolem0007),inference(resolution,[status(thm)],[c384, c483])).
% 49.51/49.70 cnf(c4424,plain,para(skolem0006,skolem0007,skolem0006,skolem0007),inference(resolution,[status(thm)],[c1484, c477])).
% 49.51/49.70 cnf(c4462,plain,eqangle(skolem0006,skolem0007,X2629,X2630,skolem0006,skolem0007,X2629,X2630),inference(resolution,[status(thm)],[c4424, c285])).
% 49.51/49.70 cnf(c4549,plain,eqangle(X2659,X2658,skolem0006,skolem0007,X2659,X2658,skolem0006,skolem0007),inference(resolution,[status(thm)],[c4462, c352])).
% 49.51/49.70 cnf(c4631,plain,para(X2660,X2661,X2660,X2661),inference(resolution,[status(thm)],[c4549, c290])).
% 49.51/49.70 cnf(c4647,plain,coll(X2662,X2663,X2663),inference(resolution,[status(thm)],[c4631, c191])).
% 49.51/49.70 cnf(c4802,plain,coll(X2671,X2671,X2670),inference(resolution,[status(thm)],[c4647, c517])).
% 49.51/49.70 cnf(c5276,plain,~coll(X3736,X3736,X3737)|coll(X3737,X3738,X3736),inference(resolution,[status(thm)],[c4802, c402])).
% 49.51/49.70 cnf(c8991,plain,coll(X3741,X3740,X3739),inference(resolution,[status(thm)],[c5276, c4802])).
% 49.51/49.70 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.51/49.70 fof(c271,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.51/49.70 fof(c272,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)],[c271])).
% 49.51/49.70 cnf(c273,plain,~eqangle(X1067,X1069,X1067,X1068,X1066,X1069,X1066,X1068)|~coll(X1067,X1066,X1068)|cyclic(X1069,X1068,X1067,X1066),inference(split_conjunct,[status(thm)],[c272])).
% 49.51/49.70 cnf(c4660,plain,eqangle(X3567,X3565,X3564,X3566,X3567,X3565,X3564,X3566),inference(resolution,[status(thm)],[c4631, c285])).
% 49.51/49.70 cnf(c8751,plain,~coll(X4097,X4097,X4099)|cyclic(X4098,X4099,X4097,X4097),inference(resolution,[status(thm)],[c4660, c273])).
% 49.51/49.70 cnf(c9624,plain,cyclic(X4100,X4101,X4102,X4102),inference(resolution,[status(thm)],[c8751, c8991])).
% 49.51/49.70 cnf(c9631,plain,cyclic(X4109,X4110,X4108,X4110),inference(resolution,[status(thm)],[c9624, c364])).
% 49.51/49.70 cnf(c9637,plain,cyclic(X4116,X4114,X4114,X4115),inference(resolution,[status(thm)],[c9631, c367])).
% 49.51/49.70 cnf(c9646,plain,eqangle(X4179,X4178,X4179,X4179,X4180,X4178,X4180,X4179),inference(resolution,[status(thm)],[c9637, c280])).
% 49.51/49.70 cnf(c9691,plain,~eqangle(X39034,X39036,X39033,X39039,X39038,X39037,X39038,X39038)|eqangle(X39034,X39036,X39033,X39039,X39035,X39037,X39035,X39038),inference(resolution,[status(thm)],[c9646, c343])).
% 49.51/49.70 cnf(c9638,plain,eqangle(X4172,X4171,X4172,X4173,X4173,X4171,X4173,X4173),inference(resolution,[status(thm)],[c9631, c280])).
% 49.51/49.70 cnf(c9677,plain,~eqangle(X32638,X32640,X32637,X32643,X32639,X32641,X32639,X32642)|eqangle(X32638,X32640,X32637,X32643,X32642,X32641,X32642,X32642),inference(resolution,[status(thm)],[c9638, c343])).
% 49.51/49.70 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.51/49.70 fof(c186,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 49.51/49.70 fof(c187,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c186])).
% 49.51/49.70 cnf(c188,plain,~cong(X936,X938,X936,X937)|~coll(X936,X938,X937)|midp(X936,X938,X937),inference(split_conjunct,[status(thm)],[c187])).
% 49.51/49.70 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.51/49.70 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 49.51/49.70 fof(c339,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c338])).
% 49.51/49.70 cnf(c340,plain,~cong(X661,X660,X659,X662)|cong(X661,X660,X662,X659),inference(split_conjunct,[status(thm)],[c339])).
% 49.51/49.70 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.51/49.70 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 49.51/49.70 fof(c336,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c335])).
% 49.51/49.70 cnf(c337,plain,~cong(X644,X646,X643,X645)|cong(X643,X645,X644,X646),inference(split_conjunct,[status(thm)],[c336])).
% 49.51/49.70 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.51/49.70 fof(c195,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.51/49.70 fof(c196,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)],[c195])).
% 49.51/49.70 cnf(c197,plain,~midp(X944,X945,X947)|~para(X945,X948,X947,X946)|~para(X945,X946,X947,X948)|midp(X944,X948,X946),inference(split_conjunct,[status(thm)],[c196])).
% 49.51/49.70 cnf(c1021,plain,~midp(X2122,X2120,X2121)|~para(X2120,X2119,X2121,X2119)|midp(X2122,X2119,X2119),inference(factor,[status(thm)],[c197])).
% 49.51/49.70 cnf(c4649,plain,~midp(X3561,X3560,X3560)|midp(X3561,X3559,X3559),inference(resolution,[status(thm)],[c4631, c1021])).
% 49.51/49.70 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.51/49.70 fof(c266,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.51/49.70 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(shift_quantors,[status(thm)],[c266])).
% 49.51/49.70 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(shift_quantors,[status(thm)],[fof(c268,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)],[c267])).])).
% 49.51/49.70 cnf(c270,plain,~cyclic(X1062,X1059,X1063,X1058)|~cyclic(X1062,X1059,X1063,X1061)|~cyclic(X1062,X1059,X1063,X1060)|~eqangle(X1063,X1062,X1063,X1059,X1060,X1058,X1060,X1061)|cong(X1062,X1059,X1058,X1061),inference(split_conjunct,[status(thm)],[c269])).
% 49.51/49.70 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.51/49.70 fof(c397,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 49.51/49.70 fof(c398,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c397])).
% 49.51/49.70 cnf(c399,plain,~para(X722,X725,X724,X723)|para(X722,X725,X723,X724),inference(split_conjunct,[status(thm)],[c398])).
% 49.51/49.70 cnf(c4651,plain,para(X2687,X2686,X2686,X2687),inference(resolution,[status(thm)],[c4631, c399])).
% 49.51/49.70 cnf(c5367,plain,eqangle(X3856,X3858,X3855,X3857,X3858,X3856,X3855,X3857),inference(resolution,[status(thm)],[c4651, c285])).
% 49.51/49.70 cnf(c9260,plain,eqangle(X3916,X3915,X3914,X3917,X3916,X3915,X3917,X3914),inference(resolution,[status(thm)],[c5367, c352])).
% 49.51/49.70 cnf(c9325,plain,eqangle(X3971,X3972,X3971,X3972,X3970,X3973,X3973,X3970),inference(resolution,[status(thm)],[c9260, c346])).
% 49.51/49.70 cnf(c9416,plain,~cyclic(X5001,X5001,X5002,X5003)|cong(X5001,X5001,X5003,X5003),inference(resolution,[status(thm)],[c9325, c270])).
% 49.51/49.70 cnf(c10260,plain,cong(X5004,X5004,X5005,X5005),inference(resolution,[status(thm)],[c9416, c9637])).
% 49.51/49.70 cnf(c10268,plain,~coll(X5066,X5066,X5066)|midp(X5066,X5066,X5066),inference(resolution,[status(thm)],[c10260, c188])).
% 49.51/49.70 cnf(c10394,plain,midp(X5067,X5067,X5067),inference(resolution,[status(thm)],[c10268, c8991])).
% 49.51/49.70 cnf(c10420,plain,midp(X5070,X5069,X5069),inference(resolution,[status(thm)],[c10394, c4649])).
% 49.51/49.70 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.51/49.70 fof(c238,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.51/49.70 fof(c239,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c238])).
% 49.51/49.70 cnf(c240,plain,~perp(X1006,X1007,X1007,X1008)|~midp(X1009,X1006,X1008)|cong(X1006,X1009,X1007,X1009),inference(split_conjunct,[status(thm)],[c239])).
% 49.51/49.70 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.51/49.70 fof(c159,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.51/49.70 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(shift_quantors,[status(thm)],[c159])).
% 49.51/49.70 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(shift_quantors,[status(thm)],[fof(c161,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)],[c160])).])).
% 49.51/49.70 cnf(c163,plain,~eqangle(X904,X910,X907,X909,X906,X908,X911,X905)|~perp(X906,X908,X911,X905)|perp(X904,X910,X907,X909),inference(split_conjunct,[status(thm)],[c162])).
% 49.51/49.70 cnf(c9262,plain,eqangle(X3925,X3924,X3924,X3925,X3926,X3923,X3926,X3923),inference(resolution,[status(thm)],[c5367, c346])).
% 49.51/49.70 cnf(c9338,plain,~perp(X4955,X4956,X4955,X4956)|perp(X4957,X4954,X4954,X4957),inference(resolution,[status(thm)],[c9262, c163])).
% 49.51/49.70 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.51/49.70 fof(c224,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.51/49.70 fof(c225,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)],[c224])).
% 49.51/49.70 cnf(c226,plain,~cong(X989,X987,X986,X987)|~cong(X989,X988,X986,X988)|perp(X989,X986,X987,X988),inference(split_conjunct,[status(thm)],[c225])).
% 49.51/49.70 cnf(c1070,plain,~cong(X1003,X1004,X1002,X1004)|perp(X1003,X1002,X1004,X1004),inference(factor,[status(thm)],[c226])).
% 49.51/49.70 cnf(c10271,plain,perp(X5017,X5017,X5017,X5017),inference(resolution,[status(thm)],[c10260, c1070])).
% 49.51/49.70 cnf(c10288,plain,perp(X5028,X5027,X5027,X5028),inference(resolution,[status(thm)],[c10271, c9338])).
% 49.51/49.70 cnf(c10315,plain,~midp(X6036,X6035,X6035)|cong(X6035,X6036,X6037,X6036),inference(resolution,[status(thm)],[c10288, c240])).
% 49.51/49.70 cnf(c12188,plain,cong(X6042,X6041,X6043,X6041),inference(resolution,[status(thm)],[c10315, c10420])).
% 49.51/49.70 cnf(c12203,plain,cong(X6050,X6052,X6052,X6051),inference(resolution,[status(thm)],[c12188, c340])).
% 49.51/49.70 cnf(c12235,plain,cong(X6071,X6072,X6070,X6071),inference(resolution,[status(thm)],[c12203, c337])).
% 49.51/49.70 cnf(c12292,plain,cong(X6100,X6101,X6100,X6099),inference(resolution,[status(thm)],[c12235, c340])).
% 49.51/49.70 cnf(c12305,plain,~coll(X6367,X6369,X6368)|midp(X6367,X6369,X6368),inference(resolution,[status(thm)],[c12292, c188])).
% 49.51/49.70 cnf(c13109,plain,midp(X6371,X6372,X6370),inference(resolution,[status(thm)],[c12305, c8991])).
% 49.51/49.70 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)).
% 49.51/49.70 fof(c263,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])).
% 49.51/49.70 fof(c264,plain,(![X267]:(![X268]:(![X269]:(![X270]:(![X271]:((~midp(X270,X267,X268)|~midp(X271,X267,X269))|para(X270,X271,X268,X269))))))),inference(variable_rename,[status(thm)],[c263])).
% 49.51/49.70 cnf(c265,plain,~midp(X1054,X1050,X1051)|~midp(X1053,X1050,X1052)|para(X1054,X1053,X1051,X1052),inference(split_conjunct,[status(thm)],[c264])).
% 49.51/49.70 cnf(c10432,plain,~midp(X10112,X10114,X10111)|para(X10112,X10113,X10111,X10114),inference(resolution,[status(thm)],[c10420, c265])).
% 49.51/49.70 cnf(c16235,plain,para(X10118,X10116,X10115,X10117),inference(resolution,[status(thm)],[c10432, c13109])).
% 49.51/49.70 cnf(c16251,plain,eqangle(X10379,X10380,X10375,X10378,X10376,X10377,X10375,X10378),inference(resolution,[status(thm)],[c16235, c285])).
% 49.51/49.70 cnf(c16468,plain,eqangle(X10395,X10398,X10394,X10393,X10395,X10398,X10396,X10397),inference(resolution,[status(thm)],[c16251, c352])).
% 49.51/49.70 cnf(c21096,plain,eqangle(X32947,X32949,X32951,X32948,X32950,X32949,X32950,X32950),inference(resolution,[status(thm)],[c9677, c16468])).
% 49.51/49.70 cnf(c22777,plain,eqangle(X39261,X39264,X39259,X39262,X39260,X39264,X39260,X39263),inference(resolution,[status(thm)],[c9691, c21096])).
% 49.51/49.70 cnf(c22948,plain,eqangle(X40102,X40104,X40101,X40104,X40099,X40103,X40101,X40100),inference(resolution,[status(thm)],[c22777, c346])).
% 49.51/49.70 cnf(c23182,plain,eqangle(X41226,X41223,X41224,X41223,X41225,X41227,X41225,X41225),inference(resolution,[status(thm)],[c22948, c9677])).
% 49.51/49.70 cnf(c23770,plain,eqangle(X43879,X43875,X43880,X43875,X43876,X43877,X43876,X43878),inference(resolution,[status(thm)],[c23182, c9691])).
% 49.51/49.70 cnf(c24389,plain,eqangle(X46516,X46518,X46515,X46517,X46513,X46518,X46515,X46514),inference(resolution,[status(thm)],[c23770, c346])).
% 49.51/49.70 cnf(c25062,plain,$false,inference(resolution,[status(thm)],[c24389, c23])).
% 49.51/49.70 % SZS output end CNFRefutation
% 49.51/49.70
% 49.51/49.70 % Initial clauses : 135
% 49.51/49.70 % Processed clauses : 3054
% 49.51/49.70 % Factors computed : 178
% 49.51/49.70 % Resolvents computed: 24486
% 49.51/49.70 % Tautologies deleted: 40
% 49.51/49.70 % Forward subsumed : 15638
% 49.51/49.70 % Backward subsumed : 2883
% 49.51/49.70 % -------- CPU Time ---------
% 49.51/49.70 % User time : 49.332 s
% 49.51/49.70 % System time : 0.028 s
% 49.51/49.70 % Total time : 49.360 s
%------------------------------------------------------------------------------