%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO567+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 26.70s 26.88s
% Output : Refutation 26.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GEO567+1 : TPTP v8.1.2. Released v7.5.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 08:04:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 26.70/26.88 % Version: 1.5
% 26.70/26.88 % SZS status Theorem
% 26.70/26.88 % SZS output start CNFRefutation
% 26.70/26.88 fof(exemplo6GDDFULL214029,conjecture,(![A]:(![B]:(![C]:(![D]:(![Q]:(![P]:((((((perp(D,A,B,C)&coll(D,B,C))&perp(Q,D,A,B))&coll(Q,A,B))&perp(P,D,A,C))&coll(P,A,C))=>cyclic(B,Q,P,C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214029)).
% 26.70/26.88 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![Q]:(![P]:((((((perp(D,A,B,C)&coll(D,B,C))&perp(Q,D,A,B))&coll(Q,A,B))&perp(P,D,A,C))&coll(P,A,C))=>cyclic(B,Q,P,C))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214029])).
% 26.70/26.88 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[Q]:(?[P]:((((((perp(D,A,B,C)&coll(D,B,C))&perp(Q,D,A,B))&coll(Q,A,B))&perp(P,D,A,C))&coll(P,A,C))&~cyclic(B,Q,P,C)))))))),inference(fof_nnf,[status(thm)],[c11])).
% 26.70/26.88 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:((((((perp(X5,X2,X3,X4)&coll(X5,X3,X4))&perp(X6,X5,X2,X3))&coll(X6,X2,X3))&perp(X7,X5,X2,X4))&coll(X7,X2,X4))&~cyclic(X3,X6,X7,X4)))))))),inference(variable_rename,[status(thm)],[c12])).
% 26.70/26.88 fof(c14,negated_conjecture,((((((perp(skolem0004,skolem0001,skolem0002,skolem0003)&coll(skolem0004,skolem0002,skolem0003))&perp(skolem0005,skolem0004,skolem0001,skolem0002))&coll(skolem0005,skolem0001,skolem0002))&perp(skolem0006,skolem0004,skolem0001,skolem0003))&coll(skolem0006,skolem0001,skolem0003))&~cyclic(skolem0002,skolem0005,skolem0006,skolem0003)),inference(skolemize,[status(esa)],[c13])).
% 26.70/26.88 cnf(c21,negated_conjecture,~cyclic(skolem0002,skolem0005,skolem0006,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 26.70/26.88 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)).
% 26.70/26.88 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 26.70/26.88 fof(c364,plain,(![X469]:(![X470]:(![X471]:(![X472]:(~cyclic(X469,X470,X471,X472)|cyclic(X469,X470,X472,X471)))))),inference(variable_rename,[status(thm)],[c363])).
% 26.70/26.88 cnf(c365,plain,~cyclic(X671,X672,X670,X669)|cyclic(X671,X672,X669,X670),inference(split_conjunct,[status(thm)],[c364])).
% 26.70/26.88 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)).
% 26.70/26.88 fof(c357,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 26.70/26.88 fof(c358,plain,(![X461]:(![X462]:(![X463]:(![X464]:(~cyclic(X461,X462,X463,X464)|cyclic(X462,X461,X463,X464)))))),inference(variable_rename,[status(thm)],[c357])).
% 26.70/26.88 cnf(c359,plain,~cyclic(X661,X663,X662,X664)|cyclic(X663,X661,X662,X664),inference(split_conjunct,[status(thm)],[c358])).
% 26.70/26.88 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)).
% 26.70/26.88 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 26.70/26.88 fof(c361,plain,(![X465]:(![X466]:(![X467]:(![X468]:(~cyclic(X465,X466,X467,X468)|cyclic(X465,X467,X466,X468)))))),inference(variable_rename,[status(thm)],[c360])).
% 26.70/26.88 cnf(c362,plain,~cyclic(X667,X666,X668,X665)|cyclic(X667,X668,X666,X665),inference(split_conjunct,[status(thm)],[c361])).
% 26.70/26.88 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)).
% 26.70/26.88 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])).
% 26.70/26.88 fof(c399,plain,(![X519]:(![X520]:(![X521]:(![X522]:((~coll(X519,X520,X521)|~coll(X519,X520,X522))|coll(X521,X522,X519)))))),inference(variable_rename,[status(thm)],[c398])).
% 26.70/26.88 cnf(c400,plain,~coll(X756,X755,X758)|~coll(X756,X755,X757)|coll(X758,X757,X756),inference(split_conjunct,[status(thm)],[c399])).
% 26.70/26.88 cnf(c538,plain,~coll(X759,X761,X760)|coll(X760,X760,X759),inference(factor,[status(thm)],[c400])).
% 26.70/26.88 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)).
% 26.70/26.88 fof(c187,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 26.70/26.88 fof(c188,plain,(![X162]:(![X163]:(![X164]:(~para(X162,X163,X162,X164)|coll(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c187])).
% 26.70/26.88 cnf(c189,plain,~para(X639,X638,X639,X640)|coll(X639,X638,X640),inference(split_conjunct,[status(thm)],[c188])).
% 26.70/26.88 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)).
% 26.70/26.88 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])).
% 26.70/26.88 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])).
% 26.70/26.88 fof(c287,plain,(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)|para(X294,X295,X296,X297)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X294]:(![X295]:(![X296]:(![X297]:((![X298]:(![X299]:~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)))|para(X294,X295,X296,X297)))))),inference(variable_rename,[status(thm)],[c285])).])).
% 26.70/26.88 cnf(c288,plain,~eqangle(X1088,X1090,X1086,X1091,X1087,X1089,X1086,X1091)|para(X1088,X1090,X1087,X1089),inference(split_conjunct,[status(thm)],[c287])).
% 26.70/26.88 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)).
% 26.70/26.88 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])).
% 26.70/26.88 fof(c349,plain,(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(~eqangle(X440,X441,X442,X443,X444,X445,X446,X447)|eqangle(X442,X443,X440,X441,X446,X447,X444,X445)))))))))),inference(variable_rename,[status(thm)],[c348])).
% 26.70/26.88 cnf(c350,plain,~eqangle(X1224,X1227,X1230,X1229,X1225,X1231,X1226,X1228)|eqangle(X1230,X1229,X1224,X1227,X1226,X1228,X1225,X1231),inference(split_conjunct,[status(thm)],[c349])).
% 26.70/26.88 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)).
% 26.70/26.88 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])).
% 26.70/26.88 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])).
% 26.70/26.88 fof(c282,plain,(![X288]:(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(~para(X288,X289,X290,X291)|eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(shift_quantors,[status(thm)],[fof(c281,plain,(![X288]:(![X289]:(![X290]:(![X291]:(~para(X288,X289,X290,X291)|(![X292]:(![X293]:eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(variable_rename,[status(thm)],[c280])).])).
% 26.70/26.88 cnf(c283,plain,~para(X1082,X1081,X1080,X1084)|eqangle(X1082,X1081,X1085,X1083,X1080,X1084,X1085,X1083),inference(split_conjunct,[status(thm)],[c282])).
% 26.70/26.88 cnf(c19,negated_conjecture,perp(skolem0006,skolem0004,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 26.70/26.88 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)).
% 26.70/26.88 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 26.70/26.88 fof(c387,plain,(![X501]:(![X502]:(![X503]:(![X504]:(~perp(X501,X502,X503,X504)|perp(X501,X502,X504,X503)))))),inference(variable_rename,[status(thm)],[c386])).
% 26.70/26.88 cnf(c388,plain,~perp(X698,X696,X695,X697)|perp(X698,X696,X697,X695),inference(split_conjunct,[status(thm)],[c387])).
% 26.70/26.88 cnf(c481,plain,perp(skolem0006,skolem0004,skolem0003,skolem0001),inference(resolution,[status(thm)],[c388, c19])).
% 26.70/26.88 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)).
% 26.70/26.88 fof(c383,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 26.70/26.88 fof(c384,plain,(![X497]:(![X498]:(![X499]:(![X500]:(~perp(X497,X498,X499,X500)|perp(X499,X500,X497,X498)))))),inference(variable_rename,[status(thm)],[c383])).
% 26.70/26.88 cnf(c385,plain,~perp(X674,X673,X675,X676)|perp(X675,X676,X674,X673),inference(split_conjunct,[status(thm)],[c384])).
% 26.70/26.88 cnf(c497,plain,perp(skolem0003,skolem0001,skolem0006,skolem0004),inference(resolution,[status(thm)],[c481, c385])).
% 26.70/26.88 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)).
% 26.70/26.88 fof(c380,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])).
% 26.70/26.88 fof(c381,plain,(![X491]:(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:((~perp(X491,X492,X493,X494)|~perp(X493,X494,X495,X496))|para(X491,X492,X495,X496)))))))),inference(variable_rename,[status(thm)],[c380])).
% 26.70/26.88 cnf(c382,plain,~perp(X1260,X1263,X1261,X1262)|~perp(X1261,X1262,X1264,X1265)|para(X1260,X1263,X1264,X1265),inference(split_conjunct,[status(thm)],[c381])).
% 26.70/26.88 cnf(c1595,plain,~perp(X2536,X2535,skolem0003,skolem0001)|para(X2536,X2535,skolem0006,skolem0004),inference(resolution,[status(thm)],[c382, c497])).
% 26.70/26.88 cnf(c4362,plain,para(skolem0006,skolem0004,skolem0006,skolem0004),inference(resolution,[status(thm)],[c1595, c481])).
% 26.70/26.88 cnf(c4370,plain,eqangle(skolem0006,skolem0004,X2551,X2552,skolem0006,skolem0004,X2551,X2552),inference(resolution,[status(thm)],[c4362, c283])).
% 26.70/26.88 cnf(c4457,plain,eqangle(X2569,X2568,skolem0006,skolem0004,X2569,X2568,skolem0006,skolem0004),inference(resolution,[status(thm)],[c4370, c350])).
% 26.70/26.88 cnf(c4539,plain,para(X2570,X2571,X2570,X2571),inference(resolution,[status(thm)],[c4457, c288])).
% 26.70/26.88 cnf(c4580,plain,coll(X2573,X2572,X2572),inference(resolution,[status(thm)],[c4539, c189])).
% 26.70/26.88 cnf(c4634,plain,coll(X2578,X2578,X2577),inference(resolution,[status(thm)],[c4580, c538])).
% 26.70/26.88 cnf(c4853,plain,~coll(X3650,X3650,X3649)|coll(X3649,X3648,X3650),inference(resolution,[status(thm)],[c4634, c400])).
% 26.70/26.88 cnf(c8806,plain,coll(X3660,X3659,X3658),inference(resolution,[status(thm)],[c4853, c4634])).
% 26.70/26.88 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)).
% 26.70/26.88 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])).
% 26.70/26.88 fof(c270,plain,(![X276]:(![X277]:(![X278]:(![X279]:((~eqangle(X278,X276,X278,X277,X279,X276,X279,X277)|~coll(X278,X279,X277))|cyclic(X276,X277,X278,X279)))))),inference(variable_rename,[status(thm)],[c269])).
% 26.70/26.88 cnf(c271,plain,~eqangle(X1068,X1070,X1068,X1069,X1071,X1070,X1071,X1069)|~coll(X1068,X1071,X1069)|cyclic(X1070,X1069,X1068,X1071),inference(split_conjunct,[status(thm)],[c270])).
% 26.70/26.88 cnf(c4560,plain,eqangle(X3468,X3466,X3467,X3469,X3468,X3466,X3467,X3469),inference(resolution,[status(thm)],[c4539, c283])).
% 26.70/26.88 cnf(c8517,plain,~coll(X3988,X3988,X3987)|cyclic(X3986,X3987,X3988,X3988),inference(resolution,[status(thm)],[c4560, c271])).
% 26.70/26.88 cnf(c9125,plain,cyclic(X3994,X3992,X3993,X3993),inference(resolution,[status(thm)],[c8517, c8806])).
% 26.70/26.88 cnf(c9127,plain,cyclic(X3997,X3995,X3996,X3995),inference(resolution,[status(thm)],[c9125, c362])).
% 26.70/26.88 cnf(c9141,plain,cyclic(X4011,X4013,X4012,X4011),inference(resolution,[status(thm)],[c9127, c359])).
% 26.70/26.88 cnf(c9151,plain,cyclic(X4024,X4023,X4024,X4025),inference(resolution,[status(thm)],[c9141, c365])).
% 26.70/26.88 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)).
% 26.70/26.88 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])).
% 26.70/26.88 fof(c355,plain,(![X456]:(![X457]:(![X458]:(![X459]:(![X460]:((~cyclic(X456,X457,X458,X459)|~cyclic(X456,X457,X458,X460))|cyclic(X457,X458,X459,X460))))))),inference(variable_rename,[status(thm)],[c354])).
% 26.70/26.88 cnf(c356,plain,~cyclic(X1244,X1240,X1243,X1242)|~cyclic(X1244,X1240,X1243,X1241)|cyclic(X1240,X1243,X1242,X1241),inference(split_conjunct,[status(thm)],[c355])).
% 26.70/26.88 cnf(c9165,plain,~cyclic(X11379,X11377,X11379,X11378)|cyclic(X11377,X11379,X11378,X11376),inference(resolution,[status(thm)],[c9151, c356])).
% 26.70/26.88 cnf(c16574,plain,cyclic(X11387,X11386,X11389,X11388),inference(resolution,[status(thm)],[c9165, c9151])).
% 26.70/26.88 cnf(c16581,plain,$false,inference(resolution,[status(thm)],[c16574, c21])).
% 26.70/26.88 % SZS output end CNFRefutation
% 26.70/26.88
% 26.70/26.88 % Initial clauses : 134
% 26.70/26.88 % Processed clauses : 2192
% 26.70/26.88 % Factors computed : 115
% 26.70/26.88 % Resolvents computed: 16060
% 26.70/26.88 % Tautologies deleted: 12
% 26.70/26.88 % Forward subsumed : 6166
% 26.70/26.88 % Backward subsumed : 1901
% 26.70/26.88 % -------- CPU Time ---------
% 26.70/26.88 % User time : 26.480 s
% 26.70/26.88 % System time : 0.038 s
% 26.70/26.88 % Total time : 26.518 s
%------------------------------------------------------------------------------