%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO601+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:22 EDT 2024
% Result : Theorem 45.35s 45.52s
% Output : Refutation 45.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO601+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.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 07:43:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 45.35/45.52 % Version: 1.5
% 45.35/45.52 % SZS status Theorem
% 45.35/45.52 % SZS output start CNFRefutation
% 45.35/45.52 fof(exemplo6GDDFULL618063f,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:((((coll(D,B,C)&circle(E,A,D,C))&circle(F,A,D,B))&circle(G,B,A,C))=>cyclic(A,F,G,E))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL618063f)).
% 45.35/45.52 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:((((coll(D,B,C)&circle(E,A,D,C))&circle(F,A,D,B))&circle(G,B,A,C))=>cyclic(A,F,G,E)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618063f])).
% 45.35/45.52 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:((((coll(D,B,C)&circle(E,A,D,C))&circle(F,A,D,B))&circle(G,B,A,C))&~cyclic(A,F,G,E))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 45.35/45.52 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((coll(X5,X3,X4)&circle(X6,X2,X5,X4))&circle(X7,X2,X5,X3))&circle(X8,X3,X2,X4))&~cyclic(X2,X7,X8,X6))))))))),inference(variable_rename,[status(thm)],[c12])).
% 45.35/45.52 fof(c14,negated_conjecture,((((coll(skolem0004,skolem0002,skolem0003)&circle(skolem0005,skolem0001,skolem0004,skolem0003))&circle(skolem0006,skolem0001,skolem0004,skolem0002))&circle(skolem0007,skolem0002,skolem0001,skolem0003))&~cyclic(skolem0001,skolem0006,skolem0007,skolem0005)),inference(skolemize,[status(esa)],[c13])).
% 45.35/45.52 cnf(c19,negated_conjecture,~cyclic(skolem0001,skolem0006,skolem0007,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 45.35/45.52 fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 45.35/45.52 fof(c355,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 45.35/45.52 fof(c356,plain,(![X462]:(![X463]:(![X464]:(![X465]:(~cyclic(X462,X463,X464,X465)|cyclic(X463,X462,X464,X465)))))),inference(variable_rename,[status(thm)],[c355])).
% 45.35/45.52 cnf(c357,plain,~cyclic(X603,X605,X602,X604)|cyclic(X605,X603,X602,X604),inference(split_conjunct,[status(thm)],[c356])).
% 45.35/45.52 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 45.35/45.52 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 45.35/45.52 fof(c362,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X471,X473,X472)))))),inference(variable_rename,[status(thm)],[c361])).
% 45.35/45.52 cnf(c363,plain,~cyclic(X610,X611,X613,X612)|cyclic(X610,X611,X612,X613),inference(split_conjunct,[status(thm)],[c362])).
% 45.35/45.52 fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 45.35/45.52 fof(c358,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 45.35/45.52 fof(c359,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c358])).
% 45.35/45.52 cnf(c360,plain,~cyclic(X606,X607,X609,X608)|cyclic(X606,X609,X607,X608),inference(split_conjunct,[status(thm)],[c359])).
% 45.35/45.52 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 45.35/45.52 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 45.35/45.52 fof(c397,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c396])).
% 45.35/45.52 cnf(c398,plain,~coll(X647,X645,X644)|~coll(X647,X645,X646)|coll(X644,X646,X647),inference(split_conjunct,[status(thm)],[c397])).
% 45.35/45.52 cnf(c429,plain,~coll(X648,X650,X649)|coll(X649,X649,X648),inference(factor,[status(thm)],[c398])).
% 45.35/45.52 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 45.35/45.52 fof(c185,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 45.35/45.52 fof(c186,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c185])).
% 45.35/45.52 cnf(c187,plain,~para(X585,X583,X585,X584)|coll(X585,X583,X584),inference(split_conjunct,[status(thm)],[c186])).
% 45.35/45.52 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD39)).
% 45.35/45.52 fof(c282,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])).
% 45.35/45.52 fof(c283,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)],[c282])).
% 45.35/45.52 fof(c285,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(c284,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)],[c283])).])).
% 45.35/45.52 cnf(c286,plain,~eqangle(X947,X946,X944,X945,X948,X949,X944,X945)|para(X947,X946,X948,X949),inference(split_conjunct,[status(thm)],[c285])).
% 45.35/45.52 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD19)).
% 45.35/45.52 fof(c346,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])).
% 45.35/45.52 fof(c347,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)],[c346])).
% 45.35/45.52 cnf(c348,plain,~eqangle(X1304,X1303,X1306,X1308,X1302,X1305,X1307,X1301)|eqangle(X1306,X1308,X1304,X1303,X1307,X1301,X1302,X1305),inference(split_conjunct,[status(thm)],[c347])).
% 45.35/45.52 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD40)).
% 45.35/45.52 fof(c277,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])).
% 45.35/45.52 fof(c278,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)],[c277])).
% 45.35/45.52 fof(c280,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(c279,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)],[c278])).])).
% 45.35/45.52 cnf(c281,plain,~para(X942,X940,X941,X943)|eqangle(X942,X940,X938,X939,X941,X943,X938,X939),inference(split_conjunct,[status(thm)],[c280])).
% 45.35/45.52 fof(ruleD8,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD8)).
% 45.35/45.52 fof(c381,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 45.35/45.52 fof(c382,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c381])).
% 45.35/45.52 cnf(c383,plain,~perp(X617,X615,X616,X614)|perp(X616,X614,X617,X615),inference(split_conjunct,[status(thm)],[c382])).
% 45.35/45.52 cnf(c18,negated_conjecture,circle(skolem0007,skolem0002,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 45.35/45.52 fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 45.35/45.52 fof(c68,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 45.35/45.52 fof(c69,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c68])).
% 45.35/45.52 fof(c70,plain,(![X51]:(![X52]:(![X53]:(![X54]:(~circle(X54,X51,X52,X53)|(?[X55]:perp(X55,X51,X51,X54))))))),inference(variable_rename,[status(thm)],[c69])).
% 45.35/45.52 fof(c71,plain,(![X51]:(![X52]:(![X53]:(![X54]:(~circle(X54,X51,X52,X53)|perp(skolem0016(X51,X52,X53,X54),X51,X51,X54)))))),inference(skolemize,[status(esa)],[c70])).
% 45.35/45.52 cnf(c72,plain,~circle(X787,X788,X790,X789)|perp(skolem0016(X788,X790,X789,X787),X788,X788,X787),inference(split_conjunct,[status(thm)],[c71])).
% 45.35/45.52 cnf(c570,plain,perp(skolem0016(skolem0002,skolem0001,skolem0003,skolem0007),skolem0002,skolem0002,skolem0007),inference(resolution,[status(thm)],[c72, c18])).
% 45.35/45.52 cnf(c694,plain,perp(skolem0002,skolem0007,skolem0016(skolem0002,skolem0001,skolem0003,skolem0007),skolem0002),inference(resolution,[status(thm)],[c570, c383])).
% 45.35/45.52 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD9)).
% 45.35/45.52 fof(c378,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])).
% 45.35/45.52 fof(c379,plain,(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:((~perp(X492,X493,X494,X495)|~perp(X494,X495,X496,X497))|para(X492,X493,X496,X497)))))))),inference(variable_rename,[status(thm)],[c378])).
% 45.35/45.52 cnf(c380,plain,~perp(X1083,X1082,X1085,X1081)|~perp(X1085,X1081,X1080,X1084)|para(X1083,X1082,X1080,X1084),inference(split_conjunct,[status(thm)],[c379])).
% 45.35/45.52 cnf(c685,plain,~perp(X1593,X1592,skolem0016(skolem0002,skolem0001,skolem0003,skolem0007),skolem0002)|para(X1593,X1592,skolem0002,skolem0007),inference(resolution,[status(thm)],[c570, c380])).
% 45.35/45.52 cnf(c2222,plain,para(skolem0002,skolem0007,skolem0002,skolem0007),inference(resolution,[status(thm)],[c685, c694])).
% 45.35/45.52 cnf(c2550,plain,eqangle(skolem0002,skolem0007,X2194,X2193,skolem0002,skolem0007,X2194,X2193),inference(resolution,[status(thm)],[c2222, c281])).
% 45.35/45.52 cnf(c6124,plain,eqangle(X3398,X3399,skolem0002,skolem0007,X3398,X3399,skolem0002,skolem0007),inference(resolution,[status(thm)],[c2550, c348])).
% 45.35/45.52 cnf(c9531,plain,para(X3404,X3403,X3404,X3403),inference(resolution,[status(thm)],[c6124, c286])).
% 45.35/45.52 cnf(c9550,plain,coll(X3406,X3405,X3405),inference(resolution,[status(thm)],[c9531, c187])).
% 45.35/45.52 cnf(c9708,plain,coll(X3409,X3409,X3410),inference(resolution,[status(thm)],[c9550, c429])).
% 45.35/45.52 cnf(c9946,plain,~coll(X4729,X4729,X4730)|coll(X4730,X4728,X4729),inference(resolution,[status(thm)],[c9708, c398])).
% 45.35/45.52 cnf(c15203,plain,coll(X4732,X4731,X4733),inference(resolution,[status(thm)],[c9946, c9708])).
% 45.35/45.52 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 45.35/45.52 fof(c267,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])).
% 45.35/45.52 fof(c268,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)],[c267])).
% 45.35/45.52 cnf(c269,plain,~eqangle(X1203,X1205,X1203,X1206,X1204,X1205,X1204,X1206)|~coll(X1203,X1204,X1206)|cyclic(X1205,X1206,X1203,X1204),inference(split_conjunct,[status(thm)],[c268])).
% 45.35/45.52 cnf(c9562,plain,eqangle(X4524,X4526,X4525,X4523,X4524,X4526,X4525,X4523),inference(resolution,[status(thm)],[c9531, c281])).
% 45.35/45.52 cnf(c14843,plain,~coll(X5025,X5025,X5023)|cyclic(X5024,X5023,X5025,X5025),inference(resolution,[status(thm)],[c9562, c269])).
% 45.35/45.52 cnf(c15486,plain,cyclic(X5030,X5028,X5029,X5029),inference(resolution,[status(thm)],[c14843, c15203])).
% 45.35/45.52 cnf(c15490,plain,cyclic(X5035,X5034,X5036,X5034),inference(resolution,[status(thm)],[c15486, c360])).
% 45.35/45.52 cnf(c15496,plain,cyclic(X5042,X5040,X5040,X5041),inference(resolution,[status(thm)],[c15490, c363])).
% 45.35/45.52 cnf(c15510,plain,cyclic(X5057,X5055,X5057,X5056),inference(resolution,[status(thm)],[c15496, c357])).
% 45.35/45.52 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD17)).
% 45.35/45.52 fof(c352,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])).
% 45.35/45.52 fof(c353,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)],[c352])).
% 45.35/45.52 cnf(c354,plain,~cyclic(X1051,X1050,X1053,X1052)|~cyclic(X1051,X1050,X1053,X1054)|cyclic(X1050,X1053,X1052,X1054),inference(split_conjunct,[status(thm)],[c353])).
% 45.35/45.52 cnf(c15526,plain,~cyclic(X11238,X11235,X11238,X11237)|cyclic(X11235,X11238,X11237,X11236),inference(resolution,[status(thm)],[c15510, c354])).
% 45.35/45.52 cnf(c22947,plain,cyclic(X11244,X11245,X11243,X11242),inference(resolution,[status(thm)],[c15526, c15510])).
% 45.35/45.52 cnf(c22954,plain,$false,inference(resolution,[status(thm)],[c22947, c19])).
% 45.35/45.52 % SZS output end CNFRefutation
% 45.35/45.52
% 45.35/45.52 % Initial clauses : 132
% 45.35/45.52 % Processed clauses : 2790
% 45.35/45.52 % Factors computed : 135
% 45.35/45.52 % Resolvents computed: 22423
% 45.35/45.52 % Tautologies deleted: 24
% 45.35/45.52 % Forward subsumed : 7471
% 45.35/45.52 % Backward subsumed : 2420
% 45.35/45.52 % -------- CPU Time ---------
% 45.35/45.52 % User time : 45.122 s
% 45.35/45.52 % System time : 0.048 s
% 45.35/45.52 % Total time : 45.170 s
%------------------------------------------------------------------------------