↑ Up

PyRes---1.5.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : GEO657+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n032.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:30 EDT 2024

% Result   : Theorem 54.53s 54.75s
% Output   : Refutation 54.53s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11  % Problem  : GEO657+1 : TPTP v8.1.2. Released v7.5.0.
% 0.12/0.12  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.31  % Computer : n032.cluster.edu
% 0.12/0.31  % Model    : x86_64 x86_64
% 0.12/0.31  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31  % Memory   : 8042.1875MB
% 0.12/0.31  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31  % CPULimit : 300
% 0.12/0.31  % WCLimit  : 300
% 0.12/0.31  % DateTime : Thu May  9 08:02:37 EDT 2024
% 0.16/0.31  % CPUTime  : 
% 54.53/54.75  % Version:  1.5
% 54.53/54.75  % SZS status Theorem
% 54.53/54.75  % SZS output start CNFRefutation
% 54.53/54.75  fof(exemplo6GDDFULLmoreE02315,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((coll(E,A,C)&para(A,B,G,E))&para(A,D,F,E))&coll(F,C,D))&coll(G,B,C))=>para(B,D,G,F))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE02315)).
% 54.53/54.75  fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((coll(E,A,C)&para(A,B,G,E))&para(A,D,F,E))&coll(F,C,D))&coll(G,B,C))=>para(B,D,G,F)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE02315])).
% 54.53/54.75  fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(((((coll(E,A,C)&para(A,B,G,E))&para(A,D,F,E))&coll(F,C,D))&coll(G,B,C))&~para(B,D,G,F))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 54.53/54.75  fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((coll(X6,X2,X4)&para(X2,X3,X8,X6))&para(X2,X5,X7,X6))&coll(X7,X4,X5))&coll(X8,X3,X4))&~para(X3,X5,X8,X7))))))))),inference(variable_rename,[status(thm)],[c12])).
% 54.53/54.75  fof(c14,negated_conjecture,(((((coll(skolem0005,skolem0001,skolem0003)&para(skolem0001,skolem0002,skolem0007,skolem0005))&para(skolem0001,skolem0004,skolem0006,skolem0005))&coll(skolem0006,skolem0003,skolem0004))&coll(skolem0007,skolem0002,skolem0003))&~para(skolem0002,skolem0004,skolem0007,skolem0006)),inference(skolemize,[status(esa)],[c13])).
% 54.53/54.75  cnf(c20,negated_conjecture,~para(skolem0002,skolem0004,skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 54.53/54.75  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)).
% 54.53/54.75  fof(c397,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 54.53/54.75  fof(c398,plain,(![X520]:(![X521]:(![X522]:(![X523]:((~coll(X520,X521,X522)|~coll(X520,X521,X523))|coll(X522,X523,X520)))))),inference(variable_rename,[status(thm)],[c397])).
% 54.53/54.75  cnf(c399,plain,~coll(X742,X744,X741)|~coll(X742,X744,X743)|coll(X741,X743,X742),inference(split_conjunct,[status(thm)],[c398])).
% 54.53/54.75  cnf(c544,plain,~coll(X745,X746,X747)|coll(X747,X747,X745),inference(factor,[status(thm)],[c399])).
% 54.53/54.75  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)).
% 54.53/54.75  fof(c186,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 54.53/54.75  fof(c187,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c186])).
% 54.53/54.75  cnf(c188,plain,~para(X639,X640,X639,X641)|coll(X639,X640,X641),inference(split_conjunct,[status(thm)],[c187])).
% 54.53/54.75  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)).
% 54.53/54.75  fof(c283,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])).
% 54.53/54.75  fof(c284,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)],[c283])).
% 54.53/54.75  fof(c286,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(c285,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)],[c284])).])).
% 54.53/54.75  cnf(c287,plain,~eqangle(X1091,X1094,X1096,X1092,X1095,X1093,X1096,X1092)|para(X1091,X1094,X1095,X1093),inference(split_conjunct,[status(thm)],[c286])).
% 54.53/54.75  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)).
% 54.53/54.75  fof(c347,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])).
% 54.53/54.75  fof(c348,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)],[c347])).
% 54.53/54.75  cnf(c349,plain,~eqangle(X1232,X1233,X1236,X1231,X1230,X1235,X1234,X1229)|eqangle(X1236,X1231,X1232,X1233,X1234,X1229,X1230,X1235),inference(split_conjunct,[status(thm)],[c348])).
% 54.53/54.75  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)).
% 54.53/54.75  fof(c278,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])).
% 54.53/54.75  fof(c279,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)],[c278])).
% 54.53/54.75  fof(c281,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(c280,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)],[c279])).])).
% 54.53/54.75  cnf(c282,plain,~para(X1090,X1087,X1086,X1085)|eqangle(X1090,X1087,X1088,X1089,X1086,X1085,X1088,X1089),inference(split_conjunct,[status(thm)],[c281])).
% 54.53/54.75  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)).
% 54.53/54.75  fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 54.53/54.75  fof(c395,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c394])).
% 54.53/54.75  cnf(c396,plain,~para(X704,X705,X706,X707)|para(X704,X705,X707,X706),inference(split_conjunct,[status(thm)],[c395])).
% 54.53/54.75  fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 54.53/54.75  fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 54.53/54.75  fof(c392,plain,(![X512]:(![X513]:(![X514]:(![X515]:(~para(X512,X513,X514,X515)|para(X514,X515,X512,X513)))))),inference(variable_rename,[status(thm)],[c391])).
% 54.53/54.75  cnf(c393,plain,~para(X694,X697,X695,X696)|para(X695,X696,X694,X697),inference(split_conjunct,[status(thm)],[c392])).
% 54.53/54.75  cnf(c16,negated_conjecture,para(skolem0001,skolem0002,skolem0007,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 54.53/54.75  cnf(c465,plain,para(skolem0007,skolem0005,skolem0001,skolem0002),inference(resolution,[status(thm)],[c393, c16])).
% 54.53/54.75  cnf(c478,plain,para(skolem0007,skolem0005,skolem0002,skolem0001),inference(resolution,[status(thm)],[c396, c465])).
% 54.53/54.75  cnf(c493,plain,para(skolem0002,skolem0001,skolem0007,skolem0005),inference(resolution,[status(thm)],[c478, c393])).
% 54.53/54.75  cnf(c522,plain,para(skolem0002,skolem0001,skolem0005,skolem0007),inference(resolution,[status(thm)],[c493, c396])).
% 54.53/54.75  cnf(c476,plain,para(skolem0001,skolem0002,skolem0005,skolem0007),inference(resolution,[status(thm)],[c396, c16])).
% 54.53/54.75  cnf(c485,plain,para(skolem0005,skolem0007,skolem0001,skolem0002),inference(resolution,[status(thm)],[c476, c393])).
% 54.53/54.75  cnf(c512,plain,para(skolem0005,skolem0007,skolem0002,skolem0001),inference(resolution,[status(thm)],[c485, c396])).
% 54.53/54.75  fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)&para(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 54.53/54.75  fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~para(A,B,C,D)|~para(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD6])).
% 54.53/54.75  fof(c389,plain,(![X506]:(![X507]:(![X508]:(![X509]:(![X510]:(![X511]:((~para(X506,X507,X508,X509)|~para(X508,X509,X510,X511))|para(X506,X507,X510,X511)))))))),inference(variable_rename,[status(thm)],[c388])).
% 54.53/54.75  cnf(c390,plain,~para(X1274,X1275,X1276,X1273)|~para(X1276,X1273,X1272,X1271)|para(X1274,X1275,X1272,X1271),inference(split_conjunct,[status(thm)],[c389])).
% 54.53/54.76  cnf(c1608,plain,~para(X2901,X2900,skolem0005,skolem0007)|para(X2901,X2900,skolem0002,skolem0001),inference(resolution,[status(thm)],[c390, c512])).
% 54.53/54.76  cnf(c6700,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1608, c522])).
% 54.53/54.76  cnf(c6711,plain,eqangle(skolem0002,skolem0001,X3715,X3714,skolem0002,skolem0001,X3715,X3714),inference(resolution,[status(thm)],[c6700, c282])).
% 54.53/54.76  cnf(c8874,plain,eqangle(X4084,X4083,skolem0002,skolem0001,X4084,X4083,skolem0002,skolem0001),inference(resolution,[status(thm)],[c6711, c349])).
% 54.53/54.76  cnf(c9643,plain,para(X4085,X4086,X4085,X4086),inference(resolution,[status(thm)],[c8874, c287])).
% 54.53/54.76  cnf(c9696,plain,coll(X4088,X4087,X4087),inference(resolution,[status(thm)],[c9643, c188])).
% 54.53/54.76  cnf(c9830,plain,coll(X4093,X4093,X4092),inference(resolution,[status(thm)],[c9696, c544])).
% 54.53/54.76  cnf(c10413,plain,~coll(X5364,X5364,X5366)|coll(X5366,X5365,X5364),inference(resolution,[status(thm)],[c9830, c399])).
% 54.53/54.76  cnf(c18924,plain,coll(X5375,X5373,X5374),inference(resolution,[status(thm)],[c10413, c9830])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c183,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 54.53/54.76  fof(c184,plain,(![X160]:(![X161]:(![X162]:((~cong(X160,X161,X160,X162)|~coll(X160,X161,X162))|midp(X160,X161,X162))))),inference(variable_rename,[status(thm)],[c183])).
% 54.53/54.76  cnf(c185,plain,~cong(X934,X933,X934,X935)|~coll(X934,X933,X935)|midp(X934,X933,X935),inference(split_conjunct,[status(thm)],[c184])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 54.53/54.76  fof(c336,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c335])).
% 54.53/54.76  cnf(c337,plain,~cong(X646,X647,X648,X649)|cong(X646,X647,X649,X648),inference(split_conjunct,[status(thm)],[c336])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c332,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 54.53/54.76  fof(c333,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c332])).
% 54.53/54.76  cnf(c334,plain,~cong(X642,X643,X644,X645)|cong(X644,X645,X642,X643),inference(split_conjunct,[status(thm)],[c333])).
% 54.53/54.76  fof(ruleD64,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:(((midp(M,A,B)&para(A,C,B,D))&para(A,D,B,C))=>midp(M,C,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 54.53/54.76  fof(c192,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])).
% 54.53/54.76  fof(c193,plain,(![X171]:(![X172]:(![X173]:(![X174]:(![X175]:(((~midp(X175,X171,X172)|~para(X171,X173,X172,X174))|~para(X171,X174,X172,X173))|midp(X175,X173,X174))))))),inference(variable_rename,[status(thm)],[c192])).
% 54.53/54.76  cnf(c194,plain,~midp(X942,X941,X945)|~para(X941,X943,X945,X944)|~para(X941,X944,X945,X943)|midp(X942,X943,X944),inference(split_conjunct,[status(thm)],[c193])).
% 54.53/54.76  cnf(c1044,plain,~midp(X2267,X2269,X2268)|~para(X2269,X2266,X2268,X2266)|midp(X2267,X2266,X2266),inference(factor,[status(thm)],[c194])).
% 54.53/54.76  cnf(c9698,plain,~midp(X5217,X5218,X5218)|midp(X5217,X5216,X5216),inference(resolution,[status(thm)],[c9643, c1044])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c356,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 54.53/54.76  fof(c357,plain,(![X462]:(![X463]:(![X464]:(![X465]:(~cyclic(X462,X463,X464,X465)|cyclic(X463,X462,X464,X465)))))),inference(variable_rename,[status(thm)],[c356])).
% 54.53/54.76  cnf(c358,plain,~cyclic(X665,X662,X664,X663)|cyclic(X662,X665,X664,X663),inference(split_conjunct,[status(thm)],[c357])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c359,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 54.53/54.76  fof(c360,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c359])).
% 54.53/54.76  cnf(c361,plain,~cyclic(X668,X666,X669,X667)|cyclic(X668,X669,X666,X667),inference(split_conjunct,[status(thm)],[c360])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c268,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])).
% 54.53/54.76  fof(c269,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)],[c268])).
% 54.53/54.76  cnf(c270,plain,~eqangle(X1073,X1076,X1073,X1074,X1075,X1076,X1075,X1074)|~coll(X1073,X1075,X1074)|cyclic(X1076,X1074,X1073,X1075),inference(split_conjunct,[status(thm)],[c269])).
% 54.53/54.76  cnf(c9674,plain,eqangle(X5213,X5210,X5212,X5211,X5213,X5210,X5212,X5211),inference(resolution,[status(thm)],[c9643, c282])).
% 54.53/54.76  cnf(c18700,plain,~coll(X5635,X5635,X5636)|cyclic(X5634,X5636,X5635,X5635),inference(resolution,[status(thm)],[c9674, c270])).
% 54.53/54.76  cnf(c19363,plain,cyclic(X5637,X5639,X5638,X5638),inference(resolution,[status(thm)],[c18700, c18924])).
% 54.53/54.76  cnf(c19369,plain,cyclic(X5643,X5644,X5645,X5644),inference(resolution,[status(thm)],[c19363, c361])).
% 54.53/54.76  cnf(c19378,plain,cyclic(X5656,X5657,X5655,X5656),inference(resolution,[status(thm)],[c19369, c358])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c263,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])).
% 54.53/54.76  fof(c264,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)],[c263])).
% 54.53/54.76  fof(c266,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275))|cong(X271,X272,X274,X275)))))))),inference(shift_quantors,[status(thm)],[fof(c265,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((![X276]:(((~cyclic(X271,X272,X273,X274)|~cyclic(X271,X272,X273,X275))|~cyclic(X271,X272,X273,X276))|~eqangle(X273,X271,X273,X272,X276,X274,X276,X275)))|cong(X271,X272,X274,X275))))))),inference(variable_rename,[status(thm)],[c264])).])).
% 54.53/54.76  cnf(c267,plain,~cyclic(X1070,X1068,X1072,X1069)|~cyclic(X1070,X1068,X1072,X1067)|~cyclic(X1070,X1068,X1072,X1071)|~eqangle(X1072,X1070,X1072,X1068,X1071,X1069,X1071,X1067)|cong(X1070,X1068,X1069,X1067),inference(split_conjunct,[status(thm)],[c266])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c341,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])).
% 54.53/54.76  fof(c342,plain,(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(~eqangle(X425,X426,X427,X428,X429,X430,X431,X432)|eqangle(X425,X426,X429,X430,X427,X428,X431,X432)))))))))),inference(variable_rename,[status(thm)],[c341])).
% 54.53/54.76  cnf(c343,plain,~eqangle(X1219,X1216,X1215,X1220,X1214,X1217,X1213,X1218)|eqangle(X1219,X1216,X1214,X1217,X1215,X1220,X1213,X1218),inference(split_conjunct,[status(thm)],[c342])).
% 54.53/54.76  cnf(c9723,plain,para(X4110,X4111,X4111,X4110),inference(resolution,[status(thm)],[c9643, c396])).
% 54.53/54.76  cnf(c11109,plain,eqangle(X5467,X5470,X5469,X5468,X5470,X5467,X5469,X5468),inference(resolution,[status(thm)],[c9723, c282])).
% 54.53/54.76  cnf(c19276,plain,eqangle(X5499,X5498,X5500,X5497,X5499,X5498,X5497,X5500),inference(resolution,[status(thm)],[c11109, c349])).
% 54.53/54.76  cnf(c19305,plain,eqangle(X5542,X5540,X5542,X5540,X5539,X5541,X5541,X5539),inference(resolution,[status(thm)],[c19276, c343])).
% 54.53/54.76  cnf(c19344,plain,~cyclic(X6595,X6595,X6594,X6593)|cong(X6595,X6595,X6593,X6593),inference(resolution,[status(thm)],[c19305, c267])).
% 54.53/54.76  cnf(c19900,plain,cong(X6596,X6596,X6596,X6596),inference(resolution,[status(thm)],[c19344, c19378])).
% 54.53/54.76  cnf(c19909,plain,~coll(X6662,X6662,X6662)|midp(X6662,X6662,X6662),inference(resolution,[status(thm)],[c19900, c185])).
% 54.53/54.76  cnf(c20004,plain,midp(X6663,X6663,X6663),inference(resolution,[status(thm)],[c19909, c18924])).
% 54.53/54.76  cnf(c20007,plain,midp(X6667,X6668,X6668),inference(resolution,[status(thm)],[c20004, c9698])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c235,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])).
% 54.53/54.76  fof(c236,plain,(![X231]:(![X232]:(![X233]:(![X234]:((~perp(X231,X232,X232,X233)|~midp(X234,X231,X233))|cong(X231,X234,X232,X234)))))),inference(variable_rename,[status(thm)],[c235])).
% 54.53/54.76  cnf(c237,plain,~perp(X1016,X1013,X1013,X1015)|~midp(X1014,X1016,X1015)|cong(X1016,X1014,X1013,X1014),inference(split_conjunct,[status(thm)],[c236])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c156,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])).
% 54.53/54.76  fof(c157,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)],[c156])).
% 54.53/54.76  fof(c159,plain,(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:((~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))|perp(X124,X125,X126,X127)))))))))),inference(shift_quantors,[status(thm)],[fof(c158,plain,(![X124]:(![X125]:(![X126]:(![X127]:((![X128]:(![X129]:(![X130]:(![X131]:(~eqangle(X124,X125,X126,X127,X128,X129,X130,X131)|~perp(X128,X129,X130,X131))))))|perp(X124,X125,X126,X127)))))),inference(variable_rename,[status(thm)],[c157])).])).
% 54.53/54.76  cnf(c160,plain,~eqangle(X910,X905,X909,X906,X907,X904,X908,X903)|~perp(X907,X904,X908,X903)|perp(X910,X905,X909,X906),inference(split_conjunct,[status(thm)],[c159])).
% 54.53/54.76  cnf(c19277,plain,eqangle(X5506,X5503,X5503,X5506,X5505,X5504,X5505,X5504),inference(resolution,[status(thm)],[c11109, c343])).
% 54.53/54.76  cnf(c19317,plain,~perp(X6553,X6554,X6553,X6554)|perp(X6552,X6551,X6551,X6552),inference(resolution,[status(thm)],[c19277, c160])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c221,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])).
% 54.53/54.76  fof(c222,plain,(![X215]:(![X216]:(![X217]:(![X218]:((~cong(X215,X217,X216,X217)|~cong(X215,X218,X216,X218))|perp(X215,X216,X217,X218)))))),inference(variable_rename,[status(thm)],[c221])).
% 54.53/54.76  cnf(c223,plain,~cong(X991,X989,X992,X989)|~cong(X991,X990,X992,X990)|perp(X991,X992,X989,X990),inference(split_conjunct,[status(thm)],[c222])).
% 54.53/54.76  cnf(c1084,plain,~cong(X993,X994,X995,X994)|perp(X993,X995,X994,X994),inference(factor,[status(thm)],[c223])).
% 54.53/54.76  cnf(c19910,plain,perp(X6610,X6610,X6610,X6610),inference(resolution,[status(thm)],[c19900, c1084])).
% 54.53/54.76  cnf(c19933,plain,perp(X6626,X6627,X6627,X6626),inference(resolution,[status(thm)],[c19910, c19317])).
% 54.53/54.76  cnf(c19981,plain,~midp(X7439,X7440,X7440)|cong(X7440,X7439,X7438,X7439),inference(resolution,[status(thm)],[c19933, c237])).
% 54.53/54.76  cnf(c20916,plain,cong(X7442,X7441,X7443,X7441),inference(resolution,[status(thm)],[c19981, c20007])).
% 54.53/54.76  cnf(c20919,plain,cong(X7449,X7447,X7447,X7448),inference(resolution,[status(thm)],[c20916, c337])).
% 54.53/54.76  cnf(c20940,plain,cong(X7470,X7469,X7468,X7470),inference(resolution,[status(thm)],[c20919, c334])).
% 54.53/54.76  cnf(c20966,plain,cong(X7486,X7488,X7486,X7487),inference(resolution,[status(thm)],[c20940, c337])).
% 54.53/54.76  cnf(c20995,plain,~coll(X7591,X7589,X7590)|midp(X7591,X7589,X7590),inference(resolution,[status(thm)],[c20966, c185])).
% 54.53/54.76  cnf(c21392,plain,midp(X7597,X7595,X7596),inference(resolution,[status(thm)],[c20995, c18924])).
% 54.53/54.76  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)).
% 54.53/54.76  fof(c260,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])).
% 54.53/54.76  fof(c261,plain,(![X266]:(![X267]:(![X268]:(![X269]:(![X270]:((~midp(X269,X266,X267)|~midp(X270,X266,X268))|para(X269,X270,X267,X268))))))),inference(variable_rename,[status(thm)],[c260])).
% 54.53/54.76  cnf(c262,plain,~midp(X1060,X1062,X1061)|~midp(X1058,X1062,X1059)|para(X1060,X1058,X1061,X1059),inference(split_conjunct,[status(thm)],[c261])).
% 54.53/54.76  cnf(c20099,plain,~midp(X11239,X11241,X11238)|para(X11239,X11240,X11238,X11241),inference(resolution,[status(thm)],[c20007, c262])).
% 54.53/54.76  cnf(c24345,plain,para(X11245,X11246,X11247,X11248),inference(resolution,[status(thm)],[c20099, c21392])).
% 54.53/54.76  cnf(c24350,plain,$false,inference(resolution,[status(thm)],[c24345, c20])).
% 54.53/54.76  % SZS output end CNFRefutation
% 54.53/54.76  
% 54.53/54.76  % Initial clauses    : 133
% 54.53/54.76  % Processed clauses  : 2593
% 54.53/54.76  % Factors computed   : 159
% 54.53/54.76  % Resolvents computed: 23786
% 54.53/54.76  % Tautologies deleted: 12
% 54.53/54.76  % Forward subsumed   : 7578
% 54.53/54.76  % Backward subsumed  : 2225
% 54.53/54.76  % -------- CPU Time ---------
% 54.53/54.76  % User time          : 54.400 s
% 54.53/54.76  % System time        : 0.039 s
% 54.53/54.76  % Total time         : 54.439 s
%------------------------------------------------------------------------------