%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO637+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:28 EDT 2024
% Result : Theorem 41.11s 41.32s
% Output : Refutation 41.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO637+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % 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 08:32:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 41.11/41.32 % Version: 1.5
% 41.11/41.32 % SZS status Theorem
% 41.11/41.32 % SZS output start CNFRefutation
% 41.11/41.32 fof(exemplo6GDDFULL81109101,conjecture,(![A]:(![B]:(![C]:(![O]:(![H]:(![D]:(![E]:((((((circle(O,A,B,C)&midp(H,C,B))&coll(D,O,H))&coll(D,A,B))&perp(C,O,C,E))&perp(A,O,A,E))=>cyclic(A,O,E,D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL81109101)).
% 41.11/41.32 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![H]:(![D]:(![E]:((((((circle(O,A,B,C)&midp(H,C,B))&coll(D,O,H))&coll(D,A,B))&perp(C,O,C,E))&perp(A,O,A,E))=>cyclic(A,O,E,D)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL81109101])).
% 41.11/41.32 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[H]:(?[D]:(?[E]:((((((circle(O,A,B,C)&midp(H,C,B))&coll(D,O,H))&coll(D,A,B))&perp(C,O,C,E))&perp(A,O,A,E))&~cyclic(A,O,E,D))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 41.11/41.32 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((circle(X5,X2,X3,X4)&midp(X6,X4,X3))&coll(X7,X5,X6))&coll(X7,X2,X3))&perp(X4,X5,X4,X8))&perp(X2,X5,X2,X8))&~cyclic(X2,X5,X8,X7))))))))),inference(variable_rename,[status(thm)],[c12])).
% 41.11/41.32 fof(c14,negated_conjecture,((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&midp(skolem0005,skolem0003,skolem0002))&coll(skolem0006,skolem0004,skolem0005))&coll(skolem0006,skolem0001,skolem0002))&perp(skolem0003,skolem0004,skolem0003,skolem0007))&perp(skolem0001,skolem0004,skolem0001,skolem0007))&~cyclic(skolem0001,skolem0004,skolem0007,skolem0006)),inference(skolemize,[status(esa)],[c13])).
% 41.11/41.32 cnf(c21,negated_conjecture,~cyclic(skolem0001,skolem0004,skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c357,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 41.11/41.32 fof(c358,plain,(![X462]:(![X463]:(![X464]:(![X465]:(~cyclic(X462,X463,X464,X465)|cyclic(X463,X462,X464,X465)))))),inference(variable_rename,[status(thm)],[c357])).
% 41.11/41.32 cnf(c359,plain,~cyclic(X690,X692,X691,X689)|cyclic(X692,X690,X691,X689),inference(split_conjunct,[status(thm)],[c358])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 41.11/41.32 fof(c364,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X471,X473,X472)))))),inference(variable_rename,[status(thm)],[c363])).
% 41.11/41.32 cnf(c365,plain,~cyclic(X703,X702,X701,X700)|cyclic(X703,X702,X700,X701),inference(split_conjunct,[status(thm)],[c364])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 41.11/41.32 fof(c361,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c360])).
% 41.11/41.32 cnf(c362,plain,~cyclic(X696,X694,X695,X693)|cyclic(X696,X695,X694,X693),inference(split_conjunct,[status(thm)],[c361])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 41.11/41.32 fof(c399,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c398])).
% 41.11/41.32 cnf(c400,plain,~coll(X765,X763,X764)|~coll(X765,X763,X762)|coll(X764,X762,X765),inference(split_conjunct,[status(thm)],[c399])).
% 41.11/41.32 cnf(c572,plain,~coll(X767,X766,X768)|coll(X768,X768,X767),inference(factor,[status(thm)],[c400])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c187,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 41.11/41.32 fof(c188,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c187])).
% 41.11/41.32 cnf(c189,plain,~para(X653,X652,X653,X651)|coll(X653,X652,X651),inference(split_conjunct,[status(thm)],[c188])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c284,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])).
% 41.11/41.32 fof(c285,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)],[c284])).
% 41.11/41.32 fof(c287,plain,(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)|para(X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X295]:(![X296]:(![X297]:(![X298]:((![X299]:(![X300]:~eqangle(X295,X296,X299,X300,X297,X298,X299,X300)))|para(X295,X296,X297,X298)))))),inference(variable_rename,[status(thm)],[c285])).])).
% 41.11/41.32 cnf(c288,plain,~eqangle(X1089,X1088,X1087,X1086,X1085,X1090,X1087,X1086)|para(X1089,X1088,X1085,X1090),inference(split_conjunct,[status(thm)],[c287])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c348,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])).
% 41.11/41.32 fof(c349,plain,(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(~eqangle(X441,X442,X443,X444,X445,X446,X447,X448)|eqangle(X443,X444,X441,X442,X447,X448,X445,X446)))))))))),inference(variable_rename,[status(thm)],[c348])).
% 41.11/41.32 cnf(c350,plain,~eqangle(X1232,X1231,X1226,X1227,X1230,X1225,X1229,X1228)|eqangle(X1226,X1227,X1232,X1231,X1229,X1228,X1230,X1225),inference(split_conjunct,[status(thm)],[c349])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c279,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])).
% 41.11/41.32 fof(c280,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)],[c279])).
% 41.11/41.32 fof(c282,plain,(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(~para(X289,X290,X291,X292)|eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(shift_quantors,[status(thm)],[fof(c281,plain,(![X289]:(![X290]:(![X291]:(![X292]:(~para(X289,X290,X291,X292)|(![X293]:(![X294]:eqangle(X289,X290,X293,X294,X291,X292,X293,X294)))))))),inference(variable_rename,[status(thm)],[c280])).])).
% 41.11/41.32 cnf(c283,plain,~para(X1083,X1080,X1081,X1078)|eqangle(X1083,X1080,X1082,X1079,X1081,X1078,X1082,X1079),inference(split_conjunct,[status(thm)],[c282])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 41.11/41.32 fof(c396,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c395])).
% 41.11/41.32 cnf(c397,plain,~para(X754,X752,X753,X755)|para(X754,X752,X755,X753),inference(split_conjunct,[status(thm)],[c396])).
% 41.11/41.32 cnf(c16,negated_conjecture,midp(skolem0005,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 41.11/41.32 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 41.11/41.32 fof(c374,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 41.11/41.32 fof(c375,plain,(![X483]:(![X484]:(![X485]:(~midp(X485,X484,X483)|midp(X485,X483,X484))))),inference(variable_rename,[status(thm)],[c374])).
% 41.11/41.32 cnf(c376,plain,~midp(X549,X551,X550)|midp(X549,X550,X551),inference(split_conjunct,[status(thm)],[c375])).
% 41.11/41.32 cnf(c414,plain,midp(skolem0005,skolem0002,skolem0003),inference(resolution,[status(thm)],[c376, c16])).
% 41.11/41.32 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 41.11/41.32 fof(c196,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 41.11/41.32 fof(c197,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c196])).
% 41.11/41.32 fof(c199,plain,(![X176]:(![X177]:(![X178]:(![X179]:(![X180]:((~midp(X180,X176,X177)|~midp(X180,X178,X179))|para(X176,X178,X177,X179))))))),inference(shift_quantors,[status(thm)],[fof(c198,plain,(![X176]:(![X177]:(![X178]:(![X179]:((![X180]:(~midp(X180,X176,X177)|~midp(X180,X178,X179)))|para(X176,X178,X177,X179)))))),inference(variable_rename,[status(thm)],[c197])).])).
% 41.11/41.32 cnf(c200,plain,~midp(X946,X947,X949)|~midp(X946,X950,X948)|para(X947,X950,X949,X948),inference(split_conjunct,[status(thm)],[c199])).
% 41.11/41.32 cnf(c1097,plain,~midp(skolem0005,X1643,X1644)|para(X1643,skolem0003,X1644,skolem0002),inference(resolution,[status(thm)],[c200, c16])).
% 41.11/41.32 cnf(c2858,plain,para(skolem0002,skolem0003,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1097, c414])).
% 41.11/41.32 cnf(c2869,plain,para(skolem0002,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c2858, c397])).
% 41.11/41.32 cnf(c2875,plain,eqangle(skolem0002,skolem0003,X2359,X2360,skolem0002,skolem0003,X2359,X2360),inference(resolution,[status(thm)],[c2869, c283])).
% 41.11/41.32 cnf(c4821,plain,eqangle(X2788,X2789,skolem0002,skolem0003,X2788,X2789,skolem0002,skolem0003),inference(resolution,[status(thm)],[c2875, c350])).
% 41.11/41.32 cnf(c7646,plain,para(X2793,X2794,X2793,X2794),inference(resolution,[status(thm)],[c4821, c288])).
% 41.11/41.32 cnf(c7674,plain,coll(X2796,X2795,X2795),inference(resolution,[status(thm)],[c7646, c189])).
% 41.11/41.32 cnf(c7691,plain,coll(X2797,X2797,X2798),inference(resolution,[status(thm)],[c7674, c572])).
% 41.11/41.32 cnf(c7918,plain,~coll(X3807,X3807,X3809)|coll(X3809,X3808,X3807),inference(resolution,[status(thm)],[c7691, c400])).
% 41.11/41.32 cnf(c12386,plain,coll(X3813,X3812,X3814),inference(resolution,[status(thm)],[c7918, c7691])).
% 41.11/41.32 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)).
% 41.11/41.32 fof(c269,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])).
% 41.11/41.32 fof(c270,plain,(![X277]:(![X278]:(![X279]:(![X280]:((~eqangle(X279,X277,X279,X278,X280,X277,X280,X278)|~coll(X279,X280,X278))|cyclic(X277,X278,X279,X280)))))),inference(variable_rename,[status(thm)],[c269])).
% 41.11/41.32 cnf(c271,plain,~eqangle(X1063,X1064,X1063,X1065,X1066,X1064,X1066,X1065)|~coll(X1063,X1066,X1065)|cyclic(X1064,X1065,X1063,X1066),inference(split_conjunct,[status(thm)],[c270])).
% 41.11/41.32 cnf(c7665,plain,eqangle(X3641,X3640,X3639,X3638,X3641,X3640,X3639,X3638),inference(resolution,[status(thm)],[c7646, c283])).
% 41.11/41.32 cnf(c12119,plain,~coll(X4177,X4177,X4176)|cyclic(X4175,X4176,X4177,X4177),inference(resolution,[status(thm)],[c7665, c271])).
% 41.11/41.32 cnf(c13214,plain,cyclic(X4179,X4180,X4178,X4178),inference(resolution,[status(thm)],[c12119, c12386])).
% 41.11/41.32 cnf(c13223,plain,cyclic(X4185,X4186,X4184,X4186),inference(resolution,[status(thm)],[c13214, c362])).
% 41.11/41.32 cnf(c13235,plain,cyclic(X4190,X4191,X4191,X4192),inference(resolution,[status(thm)],[c13223, c365])).
% 41.11/41.32 cnf(c13248,plain,cyclic(X4206,X4207,X4206,X4205),inference(resolution,[status(thm)],[c13235, c359])).
% 41.11/41.32 fof(ruleD17,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:((cyclic(A,B,C,D)&cyclic(A,B,C,E))=>cyclic(B,C,D,E))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD17)).
% 41.11/41.32 fof(c354,plain,(![A]:(![B]:(![C]:(![D]:(![E]:((~cyclic(A,B,C,D)|~cyclic(A,B,C,E))|cyclic(B,C,D,E))))))),inference(fof_nnf,[status(thm)],[ruleD17])).
% 41.11/41.32 fof(c355,plain,(![X457]:(![X458]:(![X459]:(![X460]:(![X461]:((~cyclic(X457,X458,X459,X460)|~cyclic(X457,X458,X459,X461))|cyclic(X458,X459,X460,X461))))))),inference(variable_rename,[status(thm)],[c354])).
% 41.11/41.32 cnf(c356,plain,~cyclic(X1242,X1243,X1241,X1244)|~cyclic(X1242,X1243,X1241,X1245)|cyclic(X1243,X1241,X1244,X1245),inference(split_conjunct,[status(thm)],[c355])).
% 41.11/41.32 cnf(c13266,plain,~cyclic(X12869,X12867,X12869,X12870)|cyclic(X12867,X12869,X12870,X12868),inference(resolution,[status(thm)],[c13248, c356])).
% 41.11/41.32 cnf(c24603,plain,cyclic(X12878,X12877,X12879,X12880),inference(resolution,[status(thm)],[c13266, c13248])).
% 41.11/41.32 cnf(c24607,plain,$false,inference(resolution,[status(thm)],[c24603, c21])).
% 41.11/41.32 % SZS output end CNFRefutation
% 41.11/41.32
% 41.11/41.32 % Initial clauses : 134
% 41.11/41.32 % Processed clauses : 2552
% 41.11/41.32 % Factors computed : 177
% 41.11/41.32 % Resolvents computed: 24035
% 41.11/41.32 % Tautologies deleted: 22
% 41.11/41.32 % Forward subsumed : 8514
% 41.11/41.32 % Backward subsumed : 2143
% 41.11/41.32 % -------- CPU Time ---------
% 41.11/41.32 % User time : 40.937 s
% 41.11/41.32 % System time : 0.046 s
% 41.11/41.32 % Total time : 40.983 s
%------------------------------------------------------------------------------