%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO606+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:23 EDT 2024
% Result : Theorem 116.18s 116.42s
% Output : Refutation 116.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO606+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 : n017.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 08:07:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 116.18/116.42 % Version: 1.5
% 116.18/116.42 % SZS status Theorem
% 116.18/116.42 % SZS output start CNFRefutation
% 116.18/116.42 fof(exemplo6GDDFULL618068,conjecture,(![A]:(![B]:(![P]:(![D]:(![E]:(![I]:(![F]:(![G]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:(![NWPNT01]:((((((((((((perp(P,A,P,B)&circle(A,P,NWPNT1,NWPNT2))&circle(B,P,NWPNT3,NWPNT4))&circle(A,P,D,NWPNT5))&circle(A,D,E,NWPNT6))&coll(E,D,A))&circle(A,P,I,NWPNT7))&circle(B,P,I,NWPNT8))&coll(F,D,I))&circle(B,P,F,NWPNT9))&circle(B,F,G,NWPNT01))&coll(G,F,B))=>perp(G,F,D,E)))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL618068)).
% 116.18/116.42 fof(c11,negated_conjecture,(~(![A]:(![B]:(![P]:(![D]:(![E]:(![I]:(![F]:(![G]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:(![NWPNT01]:((((((((((((perp(P,A,P,B)&circle(A,P,NWPNT1,NWPNT2))&circle(B,P,NWPNT3,NWPNT4))&circle(A,P,D,NWPNT5))&circle(A,D,E,NWPNT6))&coll(E,D,A))&circle(A,P,I,NWPNT7))&circle(B,P,I,NWPNT8))&coll(F,D,I))&circle(B,P,F,NWPNT9))&circle(B,F,G,NWPNT01))&coll(G,F,B))=>perp(G,F,D,E))))))))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL618068])).
% 116.18/116.42 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[P]:(?[D]:(?[E]:(?[I]:(?[F]:(?[G]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(?[NWPNT5]:(?[NWPNT6]:(?[NWPNT7]:(?[NWPNT8]:(?[NWPNT9]:(?[NWPNT01]:((((((((((((perp(P,A,P,B)&circle(A,P,NWPNT1,NWPNT2))&circle(B,P,NWPNT3,NWPNT4))&circle(A,P,D,NWPNT5))&circle(A,D,E,NWPNT6))&coll(E,D,A))&circle(A,P,I,NWPNT7))&circle(B,P,I,NWPNT8))&coll(F,D,I))&circle(B,P,F,NWPNT9))&circle(B,F,G,NWPNT01))&coll(G,F,B))&~perp(G,F,D,E)))))))))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 116.18/116.42 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[P]:(?[D]:(?[E]:(?[I]:(?[F]:(?[G]:((((((((((((perp(P,A,P,B)&(?[NWPNT1]:(?[NWPNT2]:circle(A,P,NWPNT1,NWPNT2))))&(?[NWPNT3]:(?[NWPNT4]:circle(B,P,NWPNT3,NWPNT4))))&(?[NWPNT5]:circle(A,P,D,NWPNT5)))&(?[NWPNT6]:circle(A,D,E,NWPNT6)))&coll(E,D,A))&(?[NWPNT7]:circle(A,P,I,NWPNT7)))&(?[NWPNT8]:circle(B,P,I,NWPNT8)))&coll(F,D,I))&(?[NWPNT9]:circle(B,P,F,NWPNT9)))&(?[NWPNT01]:circle(B,F,G,NWPNT01)))&coll(G,F,B))&~perp(G,F,D,E)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 116.18/116.42 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((((((perp(X4,X2,X4,X3)&(?[X10]:(?[X11]:circle(X2,X4,X10,X11))))&(?[X12]:(?[X13]:circle(X3,X4,X12,X13))))&(?[X14]:circle(X2,X4,X5,X14)))&(?[X15]:circle(X2,X5,X6,X15)))&coll(X6,X5,X2))&(?[X16]:circle(X2,X4,X7,X16)))&(?[X17]:circle(X3,X4,X7,X17)))&coll(X8,X5,X7))&(?[X18]:circle(X3,X4,X8,X18)))&(?[X19]:circle(X3,X8,X9,X19)))&coll(X9,X8,X3))&~perp(X9,X8,X5,X6)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 116.18/116.42 fof(c15,negated_conjecture,((((((((((((perp(skolem0003,skolem0001,skolem0003,skolem0002)&circle(skolem0001,skolem0003,skolem0009,skolem0010))&circle(skolem0002,skolem0003,skolem0011,skolem0012))&circle(skolem0001,skolem0003,skolem0004,skolem0013))&circle(skolem0001,skolem0004,skolem0005,skolem0014))&coll(skolem0005,skolem0004,skolem0001))&circle(skolem0001,skolem0003,skolem0006,skolem0015))&circle(skolem0002,skolem0003,skolem0006,skolem0016))&coll(skolem0007,skolem0004,skolem0006))&circle(skolem0002,skolem0003,skolem0007,skolem0017))&circle(skolem0002,skolem0007,skolem0008,skolem0018))&coll(skolem0008,skolem0007,skolem0002))&~perp(skolem0008,skolem0007,skolem0004,skolem0005)),inference(skolemize,[status(esa)],[c14])).
% 116.18/116.42 cnf(c28,negated_conjecture,~perp(skolem0008,skolem0007,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c405,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 116.18/116.42 fof(c406,plain,(![X531]:(![X532]:(![X533]:(![X534]:((~coll(X531,X532,X533)|~coll(X531,X532,X534))|coll(X533,X534,X531)))))),inference(variable_rename,[status(thm)],[c405])).
% 116.18/116.42 cnf(c407,plain,~coll(X743,X744,X742)|~coll(X743,X744,X745)|coll(X742,X745,X743),inference(split_conjunct,[status(thm)],[c406])).
% 116.18/116.42 cnf(c510,plain,~coll(X746,X748,X747)|coll(X747,X747,X746),inference(factor,[status(thm)],[c407])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c194,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 116.18/116.42 fof(c195,plain,(![X174]:(![X175]:(![X176]:(~para(X174,X175,X174,X176)|coll(X174,X175,X176))))),inference(variable_rename,[status(thm)],[c194])).
% 116.18/116.42 cnf(c196,plain,~para(X664,X662,X664,X663)|coll(X664,X662,X663),inference(split_conjunct,[status(thm)],[c195])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c291,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])).
% 116.18/116.42 fof(c292,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)],[c291])).
% 116.18/116.42 fof(c294,plain,(![X306]:(![X307]:(![X308]:(![X309]:(![X310]:(![X311]:(~eqangle(X306,X307,X310,X311,X308,X309,X310,X311)|para(X306,X307,X308,X309)))))))),inference(shift_quantors,[status(thm)],[fof(c293,plain,(![X306]:(![X307]:(![X308]:(![X309]:((![X310]:(![X311]:~eqangle(X306,X307,X310,X311,X308,X309,X310,X311)))|para(X306,X307,X308,X309)))))),inference(variable_rename,[status(thm)],[c292])).])).
% 116.18/116.42 cnf(c295,plain,~eqangle(X1103,X1102,X1100,X1101,X1099,X1098,X1100,X1101)|para(X1103,X1102,X1099,X1098),inference(split_conjunct,[status(thm)],[c294])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c355,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])).
% 116.18/116.42 fof(c356,plain,(![X452]:(![X453]:(![X454]:(![X455]:(![X456]:(![X457]:(![X458]:(![X459]:(~eqangle(X452,X453,X454,X455,X456,X457,X458,X459)|eqangle(X454,X455,X452,X453,X458,X459,X456,X457)))))))))),inference(variable_rename,[status(thm)],[c355])).
% 116.18/116.42 cnf(c357,plain,~eqangle(X1238,X1236,X1241,X1242,X1240,X1237,X1243,X1239)|eqangle(X1241,X1242,X1238,X1236,X1243,X1239,X1240,X1237),inference(split_conjunct,[status(thm)],[c356])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c286,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])).
% 116.18/116.42 fof(c287,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)],[c286])).
% 116.18/116.42 fof(c289,plain,(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(![X305]:(~para(X300,X301,X302,X303)|eqangle(X300,X301,X304,X305,X302,X303,X304,X305)))))))),inference(shift_quantors,[status(thm)],[fof(c288,plain,(![X300]:(![X301]:(![X302]:(![X303]:(~para(X300,X301,X302,X303)|(![X304]:(![X305]:eqangle(X300,X301,X304,X305,X302,X303,X304,X305)))))))),inference(variable_rename,[status(thm)],[c287])).])).
% 116.18/116.42 cnf(c290,plain,~para(X1092,X1093,X1097,X1094)|eqangle(X1092,X1093,X1095,X1096,X1097,X1094,X1095,X1096),inference(split_conjunct,[status(thm)],[c289])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c390,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 116.18/116.42 fof(c391,plain,(![X509]:(![X510]:(![X511]:(![X512]:(~perp(X509,X510,X511,X512)|perp(X511,X512,X509,X510)))))),inference(variable_rename,[status(thm)],[c390])).
% 116.18/116.42 cnf(c392,plain,~perp(X706,X705,X703,X704)|perp(X703,X704,X706,X705),inference(split_conjunct,[status(thm)],[c391])).
% 116.18/116.42 cnf(c16,negated_conjecture,perp(skolem0003,skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 116.18/116.42 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 116.18/116.42 fof(c393,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 116.18/116.42 fof(c394,plain,(![X513]:(![X514]:(![X515]:(![X516]:(~perp(X513,X514,X515,X516)|perp(X513,X514,X516,X515)))))),inference(variable_rename,[status(thm)],[c393])).
% 116.18/116.42 cnf(c395,plain,~perp(X707,X708,X709,X710)|perp(X707,X708,X710,X709),inference(split_conjunct,[status(thm)],[c394])).
% 116.18/116.42 cnf(c484,plain,perp(skolem0003,skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c395, c16])).
% 116.18/116.42 cnf(c489,plain,perp(skolem0002,skolem0003,skolem0003,skolem0001),inference(resolution,[status(thm)],[c484, c392])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c387,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])).
% 116.18/116.42 fof(c388,plain,(![X503]:(![X504]:(![X505]:(![X506]:(![X507]:(![X508]:((~perp(X503,X504,X505,X506)|~perp(X505,X506,X507,X508))|para(X503,X504,X507,X508)))))))),inference(variable_rename,[status(thm)],[c387])).
% 116.18/116.42 cnf(c389,plain,~perp(X1277,X1276,X1273,X1275)|~perp(X1273,X1275,X1274,X1272)|para(X1277,X1276,X1274,X1272),inference(split_conjunct,[status(thm)],[c388])).
% 116.18/116.42 cnf(c1491,plain,~perp(X2670,X2671,skolem0003,skolem0001)|para(X2670,X2671,skolem0002,skolem0003),inference(resolution,[status(thm)],[c389, c484])).
% 116.18/116.42 cnf(c6054,plain,para(skolem0002,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1491, c489])).
% 116.18/116.42 cnf(c6087,plain,eqangle(skolem0002,skolem0003,X3803,X3804,skolem0002,skolem0003,X3803,X3804),inference(resolution,[status(thm)],[c6054, c290])).
% 116.18/116.42 cnf(c11458,plain,eqangle(X4605,X4606,skolem0002,skolem0003,X4605,X4606,skolem0002,skolem0003),inference(resolution,[status(thm)],[c6087, c357])).
% 116.18/116.42 cnf(c15803,plain,para(X4607,X4608,X4607,X4608),inference(resolution,[status(thm)],[c11458, c295])).
% 116.18/116.42 cnf(c15809,plain,coll(X4610,X4609,X4609),inference(resolution,[status(thm)],[c15803, c196])).
% 116.18/116.42 cnf(c16008,plain,coll(X4618,X4618,X4617),inference(resolution,[status(thm)],[c15809, c510])).
% 116.18/116.42 cnf(c17389,plain,~coll(X6949,X6949,X6947)|coll(X6947,X6948,X6949),inference(resolution,[status(thm)],[c16008, c407])).
% 116.18/116.42 cnf(c26790,plain,coll(X6951,X6952,X6950),inference(resolution,[status(thm)],[c17389, c16008])).
% 116.18/116.42 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 116.18/116.42 fof(c191,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 116.18/116.42 fof(c192,plain,(![X171]:(![X172]:(![X173]:((~cong(X171,X172,X171,X173)|~coll(X171,X172,X173))|midp(X171,X172,X173))))),inference(variable_rename,[status(thm)],[c191])).
% 116.18/116.42 cnf(c193,plain,~cong(X945,X946,X945,X944)|~coll(X945,X946,X944)|midp(X945,X946,X944),inference(split_conjunct,[status(thm)],[c192])).
% 116.18/116.42 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 116.18/116.42 fof(c343,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 116.18/116.42 fof(c344,plain,(![X420]:(![X421]:(![X422]:(![X423]:(~cong(X420,X421,X422,X423)|cong(X420,X421,X423,X422)))))),inference(variable_rename,[status(thm)],[c343])).
% 116.18/116.42 cnf(c345,plain,~cong(X681,X682,X683,X684)|cong(X681,X682,X684,X683),inference(split_conjunct,[status(thm)],[c344])).
% 116.18/116.42 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 116.18/116.42 fof(c340,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 116.18/116.42 fof(c341,plain,(![X416]:(![X417]:(![X418]:(![X419]:(~cong(X416,X417,X418,X419)|cong(X418,X419,X416,X417)))))),inference(variable_rename,[status(thm)],[c340])).
% 116.18/116.42 cnf(c342,plain,~cong(X680,X678,X677,X679)|cong(X677,X679,X680,X678),inference(split_conjunct,[status(thm)],[c341])).
% 116.18/116.42 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 116.18/116.42 fof(c200,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])).
% 116.18/116.42 fof(c201,plain,(![X182]:(![X183]:(![X184]:(![X185]:(![X186]:(((~midp(X186,X182,X183)|~para(X182,X184,X183,X185))|~para(X182,X185,X183,X184))|midp(X186,X184,X185))))))),inference(variable_rename,[status(thm)],[c200])).
% 116.18/116.42 cnf(c202,plain,~midp(X956,X953,X955)|~para(X953,X954,X955,X957)|~para(X953,X957,X955,X954)|midp(X956,X954,X957),inference(split_conjunct,[status(thm)],[c201])).
% 116.18/116.42 cnf(c999,plain,~midp(X2090,X2091,X2093)|~para(X2091,X2092,X2093,X2092)|midp(X2090,X2092,X2092),inference(factor,[status(thm)],[c202])).
% 116.18/116.42 cnf(c15837,plain,~midp(X6659,X6660,X6660)|midp(X6659,X6661,X6661),inference(resolution,[status(thm)],[c15803, c999])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 116.18/116.42 fof(c365,plain,(![X473]:(![X474]:(![X475]:(![X476]:(~cyclic(X473,X474,X475,X476)|cyclic(X474,X473,X475,X476)))))),inference(variable_rename,[status(thm)],[c364])).
% 116.18/116.42 cnf(c366,plain,~cyclic(X685,X686,X687,X688)|cyclic(X686,X685,X687,X688),inference(split_conjunct,[status(thm)],[c365])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c367,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 116.18/116.42 fof(c368,plain,(![X477]:(![X478]:(![X479]:(![X480]:(~cyclic(X477,X478,X479,X480)|cyclic(X477,X479,X478,X480)))))),inference(variable_rename,[status(thm)],[c367])).
% 116.18/116.42 cnf(c369,plain,~cyclic(X692,X689,X691,X690)|cyclic(X692,X691,X689,X690),inference(split_conjunct,[status(thm)],[c368])).
% 116.18/116.42 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)).
% 116.18/116.42 fof(c276,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])).
% 116.18/116.42 fof(c277,plain,(![X288]:(![X289]:(![X290]:(![X291]:((~eqangle(X290,X288,X290,X289,X291,X288,X291,X289)|~coll(X290,X291,X289))|cyclic(X288,X289,X290,X291)))))),inference(variable_rename,[status(thm)],[c276])).
% 116.18/116.42 cnf(c278,plain,~eqangle(X1082,X1083,X1082,X1081,X1080,X1083,X1080,X1081)|~coll(X1082,X1080,X1081)|cyclic(X1083,X1081,X1082,X1080),inference(split_conjunct,[status(thm)],[c277])).
% 116.18/116.42 cnf(c15830,plain,eqangle(X6653,X6651,X6650,X6652,X6653,X6651,X6650,X6652),inference(resolution,[status(thm)],[c15803, c290])).
% 116.18/116.42 cnf(c26582,plain,~coll(X7409,X7409,X7411)|cyclic(X7410,X7411,X7409,X7409),inference(resolution,[status(thm)],[c15830, c278])).
% 116.18/116.42 cnf(c28003,plain,cyclic(X7412,X7414,X7413,X7413),inference(resolution,[status(thm)],[c26582, c26790])).
% 116.18/116.42 cnf(c28006,plain,cyclic(X7415,X7416,X7417,X7416),inference(resolution,[status(thm)],[c28003, c369])).
% 116.18/116.42 cnf(c28018,plain,cyclic(X7430,X7431,X7432,X7430),inference(resolution,[status(thm)],[c28006, c366])).
% 116.18/116.42 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 116.18/116.42 fof(c271,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])).
% 116.18/116.42 fof(c272,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)],[c271])).
% 116.18/116.42 fof(c274,plain,(![X282]:(![X283]:(![X284]:(![X285]:(![X286]:(![X287]:((((~cyclic(X282,X283,X284,X285)|~cyclic(X282,X283,X284,X286))|~cyclic(X282,X283,X284,X287))|~eqangle(X284,X282,X284,X283,X287,X285,X287,X286))|cong(X282,X283,X285,X286)))))))),inference(shift_quantors,[status(thm)],[fof(c273,plain,(![X282]:(![X283]:(![X284]:(![X285]:(![X286]:((![X287]:(((~cyclic(X282,X283,X284,X285)|~cyclic(X282,X283,X284,X286))|~cyclic(X282,X283,X284,X287))|~eqangle(X284,X282,X284,X283,X287,X285,X287,X286)))|cong(X282,X283,X285,X286))))))),inference(variable_rename,[status(thm)],[c272])).])).
% 116.18/116.42 cnf(c275,plain,~cyclic(X1074,X1077,X1075,X1078)|~cyclic(X1074,X1077,X1075,X1079)|~cyclic(X1074,X1077,X1075,X1076)|~eqangle(X1075,X1074,X1075,X1077,X1076,X1078,X1076,X1079)|cong(X1074,X1077,X1078,X1079),inference(split_conjunct,[status(thm)],[c274])).
% 116.18/116.42 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 116.18/116.42 fof(c349,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])).
% 116.18/116.42 fof(c350,plain,(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(![X443]:(~eqangle(X436,X437,X438,X439,X440,X441,X442,X443)|eqangle(X436,X437,X440,X441,X438,X439,X442,X443)))))))))),inference(variable_rename,[status(thm)],[c349])).
% 116.18/116.42 cnf(c351,plain,~eqangle(X1224,X1220,X1223,X1226,X1227,X1222,X1221,X1225)|eqangle(X1224,X1220,X1227,X1222,X1223,X1226,X1221,X1225),inference(split_conjunct,[status(thm)],[c350])).
% 116.18/116.42 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 116.18/116.42 fof(c402,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 116.18/116.42 fof(c403,plain,(![X527]:(![X528]:(![X529]:(![X530]:(~para(X527,X528,X529,X530)|para(X527,X528,X530,X529)))))),inference(variable_rename,[status(thm)],[c402])).
% 116.18/116.42 cnf(c404,plain,~para(X727,X728,X730,X729)|para(X727,X728,X729,X730),inference(split_conjunct,[status(thm)],[c403])).
% 116.18/116.42 cnf(c15820,plain,para(X4636,X4635,X4635,X4636),inference(resolution,[status(thm)],[c15803, c404])).
% 116.18/116.42 cnf(c17562,plain,eqangle(X7140,X7142,X7139,X7141,X7142,X7140,X7139,X7141),inference(resolution,[status(thm)],[c15820, c290])).
% 116.18/116.42 cnf(c27216,plain,eqangle(X7182,X7184,X7185,X7183,X7182,X7184,X7183,X7185),inference(resolution,[status(thm)],[c17562, c357])).
% 116.18/116.42 cnf(c27375,plain,eqangle(X7245,X7242,X7245,X7242,X7243,X7244,X7244,X7243),inference(resolution,[status(thm)],[c27216, c351])).
% 116.18/116.42 cnf(c27548,plain,~cyclic(X8505,X8505,X8504,X8503)|cong(X8505,X8505,X8503,X8503),inference(resolution,[status(thm)],[c27375, c275])).
% 116.18/116.42 cnf(c28904,plain,cong(X8506,X8506,X8506,X8506),inference(resolution,[status(thm)],[c27548, c28018])).
% 116.18/116.42 cnf(c28940,plain,~coll(X8580,X8580,X8580)|midp(X8580,X8580,X8580),inference(resolution,[status(thm)],[c28904, c193])).
% 116.18/116.42 cnf(c29104,plain,midp(X8581,X8581,X8581),inference(resolution,[status(thm)],[c28940, c26790])).
% 116.18/116.42 cnf(c29395,plain,midp(X8582,X8583,X8583),inference(resolution,[status(thm)],[c29104, c15837])).
% 116.18/116.42 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 116.18/116.42 fof(c243,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])).
% 116.18/116.42 fof(c244,plain,(![X242]:(![X243]:(![X244]:(![X245]:((~perp(X242,X243,X243,X244)|~midp(X245,X242,X244))|cong(X242,X245,X243,X245)))))),inference(variable_rename,[status(thm)],[c243])).
% 116.18/116.42 cnf(c245,plain,~perp(X1029,X1027,X1027,X1026)|~midp(X1028,X1029,X1026)|cong(X1029,X1028,X1027,X1028),inference(split_conjunct,[status(thm)],[c244])).
% 116.18/116.42 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 116.18/116.42 fof(c164,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])).
% 116.18/116.42 fof(c165,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)],[c164])).
% 116.18/116.42 fof(c167,plain,(![X135]:(![X136]:(![X137]:(![X138]:(![X139]:(![X140]:(![X141]:(![X142]:((~eqangle(X135,X136,X137,X138,X139,X140,X141,X142)|~perp(X139,X140,X141,X142))|perp(X135,X136,X137,X138)))))))))),inference(shift_quantors,[status(thm)],[fof(c166,plain,(![X135]:(![X136]:(![X137]:(![X138]:((![X139]:(![X140]:(![X141]:(![X142]:(~eqangle(X135,X136,X137,X138,X139,X140,X141,X142)|~perp(X139,X140,X141,X142))))))|perp(X135,X136,X137,X138)))))),inference(variable_rename,[status(thm)],[c165])).])).
% 116.18/116.42 cnf(c168,plain,~eqangle(X919,X920,X917,X916,X921,X915,X914,X918)|~perp(X921,X915,X914,X918)|perp(X919,X920,X917,X916),inference(split_conjunct,[status(thm)],[c167])).
% 116.18/116.42 cnf(c27218,plain,eqangle(X7191,X7194,X7194,X7191,X7193,X7192,X7193,X7192),inference(resolution,[status(thm)],[c17562, c351])).
% 116.18/116.42 cnf(c27384,plain,~perp(X8416,X8415,X8416,X8415)|perp(X8414,X8413,X8413,X8414),inference(resolution,[status(thm)],[c27218, c168])).
% 116.18/116.42 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 116.18/116.42 fof(c229,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])).
% 116.18/116.42 fof(c230,plain,(![X226]:(![X227]:(![X228]:(![X229]:((~cong(X226,X228,X227,X228)|~cong(X226,X229,X227,X229))|perp(X226,X227,X228,X229)))))),inference(variable_rename,[status(thm)],[c229])).
% 116.18/116.42 cnf(c231,plain,~cong(X1002,X1005,X1004,X1005)|~cong(X1002,X1003,X1004,X1003)|perp(X1002,X1004,X1005,X1003),inference(split_conjunct,[status(thm)],[c230])).
% 116.18/116.42 cnf(c1026,plain,~cong(X1008,X1006,X1007,X1006)|perp(X1008,X1007,X1006,X1006),inference(factor,[status(thm)],[c231])).
% 116.18/116.42 cnf(c28951,plain,perp(X8525,X8525,X8525,X8525),inference(resolution,[status(thm)],[c28904, c1026])).
% 116.18/116.42 cnf(c29014,plain,perp(X8542,X8543,X8543,X8542),inference(resolution,[status(thm)],[c28951, c27384])).
% 116.18/116.42 cnf(c29043,plain,~midp(X9469,X9470,X9470)|cong(X9470,X9469,X9471,X9469),inference(resolution,[status(thm)],[c29014, c245])).
% 116.18/116.42 cnf(c31163,plain,cong(X9474,X9472,X9473,X9472),inference(resolution,[status(thm)],[c29043, c29395])).
% 116.18/116.42 cnf(c31198,plain,cong(X9483,X9485,X9485,X9484),inference(resolution,[status(thm)],[c31163, c345])).
% 116.18/116.42 cnf(c31234,plain,cong(X9494,X9495,X9496,X9494),inference(resolution,[status(thm)],[c31198, c342])).
% 116.18/116.42 cnf(c31303,plain,cong(X9524,X9522,X9524,X9523),inference(resolution,[status(thm)],[c31234, c345])).
% 116.18/116.42 cnf(c31397,plain,~coll(X9767,X9768,X9769)|midp(X9767,X9768,X9769),inference(resolution,[status(thm)],[c31303, c193])).
% 116.18/116.42 cnf(c33173,plain,midp(X9774,X9775,X9773),inference(resolution,[status(thm)],[c31397, c26790])).
% 116.18/116.42 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 116.18/116.42 fof(c268,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])).
% 116.18/116.42 fof(c269,plain,(![X277]:(![X278]:(![X279]:(![X280]:(![X281]:((~midp(X280,X277,X278)|~midp(X281,X277,X279))|para(X280,X281,X278,X279))))))),inference(variable_rename,[status(thm)],[c268])).
% 116.18/116.42 cnf(c270,plain,~midp(X1069,X1070,X1072)|~midp(X1071,X1070,X1073)|para(X1069,X1071,X1072,X1073),inference(split_conjunct,[status(thm)],[c269])).
% 116.18/116.42 cnf(c29493,plain,~midp(X13055,X13053,X13056)|para(X13055,X13054,X13056,X13053),inference(resolution,[status(thm)],[c29395, c270])).
% 116.18/116.42 cnf(c35724,plain,para(X13058,X13057,X13060,X13059),inference(resolution,[status(thm)],[c29493, c33173])).
% 116.18/116.42 fof(ruleD10,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)&perp(C,D,E,F))=>perp(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 116.18/116.42 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~perp(C,D,E,F))|perp(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD10])).
% 116.18/116.42 fof(c385,plain,(![X497]:(![X498]:(![X499]:(![X500]:(![X501]:(![X502]:((~para(X497,X498,X499,X500)|~perp(X499,X500,X501,X502))|perp(X497,X498,X501,X502)))))))),inference(variable_rename,[status(thm)],[c384])).
% 116.18/116.42 cnf(c386,plain,~para(X1268,X1270,X1267,X1271)|~perp(X1267,X1271,X1266,X1269)|perp(X1268,X1270,X1266,X1269),inference(split_conjunct,[status(thm)],[c385])).
% 116.18/116.42 cnf(c29030,plain,~para(X15087,X15088,X15089,X15086)|perp(X15087,X15088,X15086,X15089),inference(resolution,[status(thm)],[c29014, c386])).
% 116.18/116.42 cnf(c36442,plain,perp(X15093,X15092,X15090,X15091),inference(resolution,[status(thm)],[c29030, c35724])).
% 116.18/116.42 cnf(c36444,plain,$false,inference(resolution,[status(thm)],[c36442, c28])).
% 116.18/116.42 % SZS output end CNFRefutation
% 116.18/116.42
% 116.18/116.42 % Initial clauses : 140
% 116.18/116.42 % Processed clauses : 3955
% 116.18/116.42 % Factors computed : 190
% 116.18/116.42 % Resolvents computed: 35841
% 116.18/116.42 % Tautologies deleted: 13
% 116.18/116.42 % Forward subsumed : 11312
% 116.18/116.42 % Backward subsumed : 3761
% 116.18/116.42 % -------- CPU Time ---------
% 116.18/116.42 % User time : 115.973 s
% 116.18/116.42 % System time : 0.079 s
% 116.18/116.42 % Total time : 116.052 s
%------------------------------------------------------------------------------