%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO612+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:24 EDT 2024
% Result : Theorem 61.28s 61.47s
% Output : Refutation 61.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO612+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n022.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 07:48:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 61.28/61.47 % Version: 1.5
% 61.28/61.47 % SZS status Theorem
% 61.28/61.47 % SZS output start CNFRefutation
% 61.28/61.47 fof(exemplo6GDDFULL618074,conjecture,(![A]:(![B]:(![C]:(![O]:(![G]:(![D]:(![E]:(![F]:(![NWPNT1]:(((((((((circle(O,A,B,C)&perp(G,C,A,B))&coll(G,A,B))&circle(O,C,D,NWPNT1))&coll(D,C,G))&perp(E,D,A,C))&coll(E,A,C))&perp(F,D,B,C))&coll(F,B,C))=>cyclic(A,E,F,B))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL618074)).
% 61.28/61.47 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![G]:(![D]:(![E]:(![F]:(![NWPNT1]:(((((((((circle(O,A,B,C)&perp(G,C,A,B))&coll(G,A,B))&circle(O,C,D,NWPNT1))&coll(D,C,G))&perp(E,D,A,C))&coll(E,A,C))&perp(F,D,B,C))&coll(F,B,C))=>cyclic(A,E,F,B)))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618074])).
% 61.28/61.47 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[G]:(?[D]:(?[E]:(?[F]:(?[NWPNT1]:(((((((((circle(O,A,B,C)&perp(G,C,A,B))&coll(G,A,B))&circle(O,C,D,NWPNT1))&coll(D,C,G))&perp(E,D,A,C))&coll(E,A,C))&perp(F,D,B,C))&coll(F,B,C))&~cyclic(A,E,F,B))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 61.28/61.47 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[G]:(?[D]:(?[E]:(?[F]:(((((((((circle(O,A,B,C)&perp(G,C,A,B))&coll(G,A,B))&(?[NWPNT1]:circle(O,C,D,NWPNT1)))&coll(D,C,G))&perp(E,D,A,C))&coll(E,A,C))&perp(F,D,B,C))&coll(F,B,C))&~cyclic(A,E,F,B)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 61.28/61.47 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((circle(X5,X2,X3,X4)&perp(X6,X4,X2,X3))&coll(X6,X2,X3))&(?[X10]:circle(X5,X4,X7,X10)))&coll(X7,X4,X6))&perp(X8,X7,X2,X4))&coll(X8,X2,X4))&perp(X9,X7,X3,X4))&coll(X9,X3,X4))&~cyclic(X2,X8,X9,X3)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 61.28/61.47 fof(c15,negated_conjecture,(((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&perp(skolem0005,skolem0003,skolem0001,skolem0002))&coll(skolem0005,skolem0001,skolem0002))&circle(skolem0004,skolem0003,skolem0006,skolem0009))&coll(skolem0006,skolem0003,skolem0005))&perp(skolem0007,skolem0006,skolem0001,skolem0003))&coll(skolem0007,skolem0001,skolem0003))&perp(skolem0008,skolem0006,skolem0002,skolem0003))&coll(skolem0008,skolem0002,skolem0003))&~cyclic(skolem0001,skolem0007,skolem0008,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 61.28/61.47 cnf(c25,negated_conjecture,~cyclic(skolem0001,skolem0007,skolem0008,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c367,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 61.28/61.47 fof(c368,plain,(![X472]:(![X473]:(![X474]:(![X475]:(~cyclic(X472,X473,X474,X475)|cyclic(X472,X473,X475,X474)))))),inference(variable_rename,[status(thm)],[c367])).
% 61.28/61.47 cnf(c369,plain,~cyclic(X698,X697,X699,X696)|cyclic(X698,X697,X696,X699),inference(split_conjunct,[status(thm)],[c368])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 61.28/61.47 fof(c362,plain,(![X464]:(![X465]:(![X466]:(![X467]:(~cyclic(X464,X465,X466,X467)|cyclic(X465,X464,X466,X467)))))),inference(variable_rename,[status(thm)],[c361])).
% 61.28/61.47 cnf(c363,plain,~cyclic(X691,X688,X690,X689)|cyclic(X688,X691,X690,X689),inference(split_conjunct,[status(thm)],[c362])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 61.28/61.47 fof(c365,plain,(![X468]:(![X469]:(![X470]:(![X471]:(~cyclic(X468,X469,X470,X471)|cyclic(X468,X470,X469,X471)))))),inference(variable_rename,[status(thm)],[c364])).
% 61.28/61.47 cnf(c366,plain,~cyclic(X692,X695,X694,X693)|cyclic(X692,X694,X695,X693),inference(split_conjunct,[status(thm)],[c365])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c402,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 61.28/61.47 fof(c403,plain,(![X522]:(![X523]:(![X524]:(![X525]:((~coll(X522,X523,X524)|~coll(X522,X523,X525))|coll(X524,X525,X522)))))),inference(variable_rename,[status(thm)],[c402])).
% 61.28/61.47 cnf(c404,plain,~coll(X778,X776,X777)|~coll(X778,X776,X779)|coll(X777,X779,X778),inference(split_conjunct,[status(thm)],[c403])).
% 61.28/61.47 cnf(c565,plain,~coll(X781,X780,X782)|coll(X782,X782,X781),inference(factor,[status(thm)],[c404])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c191,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 61.28/61.47 fof(c192,plain,(![X165]:(![X166]:(![X167]:(~para(X165,X166,X165,X167)|coll(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c191])).
% 61.28/61.47 cnf(c193,plain,~para(X671,X672,X671,X673)|coll(X671,X672,X673),inference(split_conjunct,[status(thm)],[c192])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c288,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])).
% 61.28/61.47 fof(c289,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)],[c288])).
% 61.28/61.47 fof(c291,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(c290,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)],[c289])).])).
% 61.28/61.47 cnf(c292,plain,~eqangle(X1076,X1079,X1077,X1080,X1078,X1081,X1077,X1080)|para(X1076,X1079,X1078,X1081),inference(split_conjunct,[status(thm)],[c291])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c352,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])).
% 61.28/61.47 fof(c353,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)],[c352])).
% 61.28/61.47 cnf(c354,plain,~eqangle(X1235,X1236,X1241,X1237,X1239,X1238,X1240,X1242)|eqangle(X1241,X1237,X1235,X1236,X1240,X1242,X1239,X1238),inference(split_conjunct,[status(thm)],[c353])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c283,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])).
% 61.28/61.47 fof(c284,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)],[c283])).
% 61.28/61.47 fof(c286,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(c285,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)],[c284])).])).
% 61.28/61.47 cnf(c287,plain,~para(X1069,X1072,X1074,X1071)|eqangle(X1069,X1072,X1070,X1073,X1074,X1071,X1070,X1073),inference(split_conjunct,[status(thm)],[c286])).
% 61.28/61.47 cnf(c17,negated_conjecture,perp(skolem0005,skolem0003,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 61.28/61.47 fof(c388,plain,(![X500]:(![X501]:(![X502]:(![X503]:(~perp(X500,X501,X502,X503)|perp(X502,X503,X500,X501)))))),inference(variable_rename,[status(thm)],[c387])).
% 61.28/61.47 cnf(c389,plain,~perp(X700,X702,X701,X703)|perp(X701,X703,X700,X702),inference(split_conjunct,[status(thm)],[c388])).
% 61.28/61.47 cnf(c492,plain,perp(skolem0001,skolem0002,skolem0005,skolem0003),inference(resolution,[status(thm)],[c389, c17])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c384,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])).
% 61.28/61.47 fof(c385,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)],[c384])).
% 61.28/61.47 cnf(c386,plain,~perp(X1276,X1273,X1274,X1271)|~perp(X1274,X1271,X1272,X1275)|para(X1276,X1273,X1272,X1275),inference(split_conjunct,[status(thm)],[c385])).
% 61.28/61.47 cnf(c1534,plain,~perp(X2645,X2644,skolem0005,skolem0003)|para(X2645,X2644,skolem0001,skolem0002),inference(resolution,[status(thm)],[c386, c17])).
% 61.28/61.47 cnf(c5839,plain,para(skolem0001,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1534, c492])).
% 61.28/61.47 cnf(c5869,plain,eqangle(skolem0001,skolem0002,X3510,X3511,skolem0001,skolem0002,X3510,X3511),inference(resolution,[status(thm)],[c5839, c287])).
% 61.28/61.47 cnf(c7924,plain,eqangle(X3627,X3626,skolem0001,skolem0002,X3627,X3626,skolem0001,skolem0002),inference(resolution,[status(thm)],[c5869, c354])).
% 61.28/61.47 cnf(c8380,plain,para(X3629,X3628,X3629,X3628),inference(resolution,[status(thm)],[c7924, c292])).
% 61.28/61.47 cnf(c8405,plain,coll(X3630,X3631,X3631),inference(resolution,[status(thm)],[c8380, c193])).
% 61.28/61.47 cnf(c8513,plain,coll(X3636,X3636,X3635),inference(resolution,[status(thm)],[c8405, c565])).
% 61.28/61.47 cnf(c8862,plain,~coll(X5233,X5233,X5232)|coll(X5232,X5234,X5233),inference(resolution,[status(thm)],[c8513, c404])).
% 61.28/61.47 cnf(c16143,plain,coll(X5237,X5239,X5238),inference(resolution,[status(thm)],[c8862, c8513])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c273,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])).
% 61.28/61.47 fof(c274,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)],[c273])).
% 61.28/61.47 cnf(c275,plain,~eqangle(X1054,X1055,X1054,X1053,X1056,X1055,X1056,X1053)|~coll(X1054,X1056,X1053)|cyclic(X1055,X1053,X1054,X1056),inference(split_conjunct,[status(thm)],[c274])).
% 61.28/61.47 cnf(c8420,plain,eqangle(X5005,X5004,X5006,X5007,X5005,X5004,X5006,X5007),inference(resolution,[status(thm)],[c8380, c287])).
% 61.28/61.47 cnf(c15964,plain,~coll(X5703,X5703,X5705)|cyclic(X5704,X5705,X5703,X5703),inference(resolution,[status(thm)],[c8420, c275])).
% 61.28/61.47 cnf(c17076,plain,cyclic(X5708,X5706,X5707,X5707),inference(resolution,[status(thm)],[c15964, c16143])).
% 61.28/61.47 cnf(c17080,plain,cyclic(X5712,X5713,X5714,X5713),inference(resolution,[status(thm)],[c17076, c366])).
% 61.28/61.47 cnf(c17086,plain,cyclic(X5722,X5723,X5721,X5722),inference(resolution,[status(thm)],[c17080, c363])).
% 61.28/61.47 cnf(c17097,plain,cyclic(X5739,X5740,X5739,X5741),inference(resolution,[status(thm)],[c17086, c369])).
% 61.28/61.47 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)).
% 61.28/61.47 fof(c358,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])).
% 61.28/61.47 fof(c359,plain,(![X459]:(![X460]:(![X461]:(![X462]:(![X463]:((~cyclic(X459,X460,X461,X462)|~cyclic(X459,X460,X461,X463))|cyclic(X460,X461,X462,X463))))))),inference(variable_rename,[status(thm)],[c358])).
% 61.28/61.47 cnf(c360,plain,~cyclic(X1254,X1253,X1252,X1251)|~cyclic(X1254,X1253,X1252,X1255)|cyclic(X1253,X1252,X1251,X1255),inference(split_conjunct,[status(thm)],[c359])).
% 61.28/61.47 cnf(c17114,plain,~cyclic(X13543,X13542,X13543,X13544)|cyclic(X13542,X13543,X13544,X13541),inference(resolution,[status(thm)],[c17097, c360])).
% 61.28/61.47 cnf(c26424,plain,cyclic(X13551,X13553,X13554,X13552),inference(resolution,[status(thm)],[c17114, c17097])).
% 61.28/61.47 cnf(c26430,plain,$false,inference(resolution,[status(thm)],[c26424, c25])).
% 61.28/61.47 % SZS output end CNFRefutation
% 61.28/61.47
% 61.28/61.47 % Initial clauses : 137
% 61.28/61.47 % Processed clauses : 3145
% 61.28/61.47 % Factors computed : 166
% 61.28/61.47 % Resolvents computed: 25855
% 61.28/61.47 % Tautologies deleted: 12
% 61.28/61.47 % Forward subsumed : 8853
% 61.28/61.47 % Backward subsumed : 2818
% 61.28/61.47 % -------- CPU Time ---------
% 61.28/61.47 % User time : 61.052 s
% 61.28/61.47 % System time : 0.055 s
% 61.28/61.47 % Total time : 61.107 s
%------------------------------------------------------------------------------