%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO594+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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 48.28s 48.51s
% Output : Refutation 48.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO594+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n007.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 07:59:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 48.28/48.51 % Version: 1.5
% 48.28/48.51 % SZS status Theorem
% 48.28/48.51 % SZS output start CNFRefutation
% 48.28/48.51 fof(exemplo6GDDFULL416056,conjecture,(![A]:(![B]:(![M]:(![O]:(![D]:(![E]:(((((((cong(M,A,A,B)|cong(M,A,M,B))&circle(O,A,B,M))&coll(D,M,O))&coll(D,A,B))&perp(A,O,A,E))¶(A,O,E,M))=>cong(M,E,M,D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL416056)).
% 48.28/48.51 fof(c11,negated_conjecture,(~(![A]:(![B]:(![M]:(![O]:(![D]:(![E]:(((((((cong(M,A,A,B)|cong(M,A,M,B))&circle(O,A,B,M))&coll(D,M,O))&coll(D,A,B))&perp(A,O,A,E))¶(A,O,E,M))=>cong(M,E,M,D))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416056])).
% 48.28/48.51 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[M]:(?[O]:(?[D]:(?[E]:(((((((cong(M,A,A,B)|cong(M,A,M,B))&circle(O,A,B,M))&coll(D,M,O))&coll(D,A,B))&perp(A,O,A,E))¶(A,O,E,M))&~cong(M,E,M,D)))))))),inference(fof_nnf,[status(thm)],[c11])).
% 48.28/48.51 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((((cong(X4,X2,X2,X3)|cong(X4,X2,X4,X3))&circle(X5,X2,X3,X4))&coll(X6,X4,X5))&coll(X6,X2,X3))&perp(X2,X5,X2,X7))¶(X2,X5,X7,X4))&~cong(X4,X7,X4,X6)))))))),inference(variable_rename,[status(thm)],[c12])).
% 48.28/48.51 fof(c14,negated_conjecture,(((((((cong(skolem0003,skolem0001,skolem0001,skolem0002)|cong(skolem0003,skolem0001,skolem0003,skolem0002))&circle(skolem0004,skolem0001,skolem0002,skolem0003))&coll(skolem0005,skolem0003,skolem0004))&coll(skolem0005,skolem0001,skolem0002))&perp(skolem0001,skolem0004,skolem0001,skolem0006))¶(skolem0001,skolem0004,skolem0006,skolem0003))&~cong(skolem0003,skolem0006,skolem0003,skolem0005)),inference(skolemize,[status(esa)],[c13])).
% 48.28/48.51 cnf(c21,negated_conjecture,~cong(skolem0003,skolem0006,skolem0003,skolem0005),inference(split_conjunct,[status(thm)],[c14])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 48.28/48.51 fof(c337,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X408,X409,X411,X410)))))),inference(variable_rename,[status(thm)],[c336])).
% 48.28/48.51 cnf(c338,plain,~cong(X614,X615,X616,X613)|cong(X614,X615,X613,X616),inference(split_conjunct,[status(thm)],[c337])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c333,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 48.28/48.51 fof(c334,plain,(![X404]:(![X405]:(![X406]:(![X407]:(~cong(X404,X405,X406,X407)|cong(X406,X407,X404,X405)))))),inference(variable_rename,[status(thm)],[c333])).
% 48.28/48.51 cnf(c335,plain,~cong(X610,X609,X611,X612)|cong(X611,X612,X610,X609),inference(split_conjunct,[status(thm)],[c334])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c193,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])).
% 48.28/48.51 fof(c194,plain,(![X170]:(![X171]:(![X172]:(![X173]:(![X174]:(((~midp(X174,X170,X171)|~para(X170,X172,X171,X173))|~para(X170,X173,X171,X172))|midp(X174,X172,X173))))))),inference(variable_rename,[status(thm)],[c193])).
% 48.28/48.51 cnf(c195,plain,~midp(X954,X958,X955)|~para(X958,X956,X955,X957)|~para(X958,X957,X955,X956)|midp(X954,X956,X957),inference(split_conjunct,[status(thm)],[c194])).
% 48.28/48.51 cnf(c1025,plain,~midp(X2327,X2329,X2326)|~para(X2329,X2328,X2326,X2328)|midp(X2327,X2328,X2328),inference(factor,[status(thm)],[c195])).
% 48.28/48.51 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)).
% 48.28/48.51 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])).
% 48.28/48.51 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])).
% 48.28/48.51 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])).])).
% 48.28/48.51 cnf(c288,plain,~eqangle(X1076,X1073,X1072,X1077,X1074,X1075,X1072,X1077)|para(X1076,X1073,X1074,X1075),inference(split_conjunct,[status(thm)],[c287])).
% 48.28/48.51 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)).
% 48.28/48.51 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])).
% 48.28/48.51 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])).
% 48.28/48.51 cnf(c350,plain,~eqangle(X1216,X1213,X1215,X1210,X1214,X1217,X1211,X1212)|eqangle(X1215,X1210,X1216,X1213,X1211,X1212,X1214,X1217),inference(split_conjunct,[status(thm)],[c349])).
% 48.28/48.51 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)).
% 48.28/48.51 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])).
% 48.28/48.51 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])).
% 48.28/48.51 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])).])).
% 48.28/48.51 cnf(c283,plain,~para(X1071,X1066,X1067,X1070)|eqangle(X1071,X1066,X1069,X1068,X1067,X1070,X1069,X1068),inference(split_conjunct,[status(thm)],[c282])).
% 48.28/48.51 cnf(c19,negated_conjecture,perp(skolem0001,skolem0004,skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 48.28/48.51 fof(c387,plain,(![X501]:(![X502]:(![X503]:(![X504]:(~perp(X501,X502,X503,X504)|perp(X501,X502,X504,X503)))))),inference(variable_rename,[status(thm)],[c386])).
% 48.28/48.51 cnf(c388,plain,~perp(X649,X652,X651,X650)|perp(X649,X652,X650,X651),inference(split_conjunct,[status(thm)],[c387])).
% 48.28/48.51 cnf(c452,plain,perp(skolem0001,skolem0004,skolem0006,skolem0001),inference(resolution,[status(thm)],[c388, c19])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c383,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 48.28/48.51 fof(c384,plain,(![X497]:(![X498]:(![X499]:(![X500]:(~perp(X497,X498,X499,X500)|perp(X499,X500,X497,X498)))))),inference(variable_rename,[status(thm)],[c383])).
% 48.28/48.51 cnf(c385,plain,~perp(X648,X646,X645,X647)|perp(X645,X647,X648,X646),inference(split_conjunct,[status(thm)],[c384])).
% 48.28/48.51 cnf(c456,plain,perp(skolem0006,skolem0001,skolem0001,skolem0004),inference(resolution,[status(thm)],[c452, c385])).
% 48.28/48.51 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)).
% 48.28/48.51 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])).
% 48.28/48.51 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])).
% 48.28/48.51 cnf(c382,plain,~perp(X1270,X1269,X1271,X1268)|~perp(X1271,X1268,X1267,X1272)|para(X1270,X1269,X1267,X1272),inference(split_conjunct,[status(thm)],[c381])).
% 48.28/48.51 cnf(c1496,plain,~perp(X3153,X3154,skolem0006,skolem0001)|para(X3153,X3154,skolem0001,skolem0004),inference(resolution,[status(thm)],[c382, c456])).
% 48.28/48.51 cnf(c7417,plain,para(skolem0001,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c1496, c452])).
% 48.28/48.51 cnf(c7457,plain,eqangle(skolem0001,skolem0004,X3437,X3436,skolem0001,skolem0004,X3437,X3436),inference(resolution,[status(thm)],[c7417, c283])).
% 48.28/48.51 cnf(c9752,plain,eqangle(X3663,X3664,skolem0001,skolem0004,X3663,X3664,skolem0001,skolem0004),inference(resolution,[status(thm)],[c7457, c350])).
% 48.28/48.51 cnf(c13810,plain,para(X3665,X3666,X3665,X3666),inference(resolution,[status(thm)],[c9752, c288])).
% 48.28/48.51 cnf(c13847,plain,~midp(X4570,X4569,X4569)|midp(X4570,X4571,X4571),inference(resolution,[status(thm)],[c13810, c1025])).
% 48.28/48.51 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)).
% 48.28/48.51 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])).
% 48.28/48.51 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])).
% 48.28/48.51 cnf(c400,plain,~coll(X725,X722,X724)|~coll(X725,X722,X723)|coll(X724,X723,X725),inference(split_conjunct,[status(thm)],[c399])).
% 48.28/48.51 cnf(c519,plain,~coll(X726,X727,X728)|coll(X728,X728,X726),inference(factor,[status(thm)],[c400])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c187,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 48.28/48.51 fof(c188,plain,(![X162]:(![X163]:(![X164]:(~para(X162,X163,X162,X164)|coll(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c187])).
% 48.28/48.51 cnf(c189,plain,~para(X606,X608,X606,X607)|coll(X606,X608,X607),inference(split_conjunct,[status(thm)],[c188])).
% 48.28/48.51 cnf(c13827,plain,coll(X3669,X3670,X3670),inference(resolution,[status(thm)],[c13810, c189])).
% 48.28/48.51 cnf(c14097,plain,coll(X3675,X3675,X3676),inference(resolution,[status(thm)],[c13827, c519])).
% 48.28/48.51 cnf(c14536,plain,~coll(X4722,X4722,X4721)|coll(X4721,X4723,X4722),inference(resolution,[status(thm)],[c14097, c400])).
% 48.28/48.51 cnf(c19717,plain,coll(X4726,X4727,X4728),inference(resolution,[status(thm)],[c14536, c14097])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c184,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 48.28/48.51 fof(c185,plain,(![X159]:(![X160]:(![X161]:((~cong(X159,X160,X159,X161)|~coll(X159,X160,X161))|midp(X159,X160,X161))))),inference(variable_rename,[status(thm)],[c184])).
% 48.28/48.51 cnf(c186,plain,~cong(X948,X947,X948,X946)|~coll(X948,X947,X946)|midp(X948,X947,X946),inference(split_conjunct,[status(thm)],[c185])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 48.28/48.51 fof(c364,plain,(![X469]:(![X470]:(![X471]:(![X472]:(~cyclic(X469,X470,X471,X472)|cyclic(X469,X470,X472,X471)))))),inference(variable_rename,[status(thm)],[c363])).
% 48.28/48.51 cnf(c365,plain,~cyclic(X641,X644,X643,X642)|cyclic(X641,X644,X642,X643),inference(split_conjunct,[status(thm)],[c364])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 48.28/48.51 fof(c361,plain,(![X465]:(![X466]:(![X467]:(![X468]:(~cyclic(X465,X466,X467,X468)|cyclic(X465,X467,X466,X468)))))),inference(variable_rename,[status(thm)],[c360])).
% 48.28/48.51 cnf(c362,plain,~cyclic(X621,X624,X622,X623)|cyclic(X621,X622,X624,X623),inference(split_conjunct,[status(thm)],[c361])).
% 48.28/48.51 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)).
% 48.28/48.51 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])).
% 48.28/48.51 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])).
% 48.28/48.51 cnf(c271,plain,~eqangle(X1054,X1057,X1054,X1056,X1055,X1057,X1055,X1056)|~coll(X1054,X1055,X1056)|cyclic(X1057,X1056,X1054,X1055),inference(split_conjunct,[status(thm)],[c270])).
% 48.28/48.51 cnf(c13858,plain,eqangle(X4577,X4579,X4578,X4576,X4577,X4579,X4578,X4576),inference(resolution,[status(thm)],[c13810, c283])).
% 48.28/48.51 cnf(c19487,plain,~coll(X5096,X5096,X5095)|cyclic(X5094,X5095,X5096,X5096),inference(resolution,[status(thm)],[c13858, c271])).
% 48.28/48.51 cnf(c20260,plain,cyclic(X5097,X5098,X5099,X5099),inference(resolution,[status(thm)],[c19487, c19717])).
% 48.28/48.51 cnf(c20264,plain,cyclic(X5101,X5100,X5102,X5100),inference(resolution,[status(thm)],[c20260, c362])).
% 48.28/48.51 cnf(c20276,plain,cyclic(X5121,X5119,X5119,X5120),inference(resolution,[status(thm)],[c20264, c365])).
% 48.28/48.51 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)).
% 48.28/48.51 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(fof_nnf,[status(thm)],[ruleD43])).
% 48.28/48.51 fof(c265,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)],[c264])).
% 48.28/48.51 fof(c267,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274))|cong(X270,X271,X273,X274)))))))),inference(shift_quantors,[status(thm)],[fof(c266,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:((![X275]:(((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274)))|cong(X270,X271,X273,X274))))))),inference(variable_rename,[status(thm)],[c265])).])).
% 48.28/48.51 cnf(c268,plain,~cyclic(X1050,X1052,X1051,X1048)|~cyclic(X1050,X1052,X1051,X1049)|~cyclic(X1050,X1052,X1051,X1053)|~eqangle(X1051,X1050,X1051,X1052,X1053,X1048,X1053,X1049)|cong(X1050,X1052,X1048,X1049),inference(split_conjunct,[status(thm)],[c267])).
% 48.28/48.51 fof(ruleD20,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(P,Q,U,V,A,B,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 48.28/48.51 fof(c345,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(P,Q,U,V,A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD20])).
% 48.28/48.51 fof(c346,plain,(![X432]:(![X433]:(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(~eqangle(X432,X433,X434,X435,X436,X437,X438,X439)|eqangle(X436,X437,X438,X439,X432,X433,X434,X435)))))))))),inference(variable_rename,[status(thm)],[c345])).
% 48.28/48.51 cnf(c347,plain,~eqangle(X1209,X1204,X1207,X1202,X1205,X1206,X1203,X1208)|eqangle(X1205,X1206,X1203,X1208,X1209,X1204,X1207,X1202),inference(split_conjunct,[status(thm)],[c346])).
% 48.28/48.51 fof(ruleD18,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(B,A,C,D,P,Q,U,V)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD18)).
% 48.28/48.51 fof(c351,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(B,A,C,D,P,Q,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD18])).
% 48.28/48.51 fof(c352,plain,(![X448]:(![X449]:(![X450]:(![X451]:(![X452]:(![X453]:(![X454]:(![X455]:(~eqangle(X448,X449,X450,X451,X452,X453,X454,X455)|eqangle(X449,X448,X450,X451,X452,X453,X454,X455)))))))))),inference(variable_rename,[status(thm)],[c351])).
% 48.28/48.51 cnf(c353,plain,~eqangle(X1224,X1219,X1221,X1218,X1225,X1220,X1222,X1223)|eqangle(X1219,X1224,X1221,X1218,X1225,X1220,X1222,X1223),inference(split_conjunct,[status(thm)],[c352])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c342,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])).
% 48.28/48.51 fof(c343,plain,(![X424]:(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(~eqangle(X424,X425,X426,X427,X428,X429,X430,X431)|eqangle(X424,X425,X428,X429,X426,X427,X430,X431)))))))))),inference(variable_rename,[status(thm)],[c342])).
% 48.28/48.51 cnf(c344,plain,~eqangle(X1199,X1196,X1201,X1197,X1195,X1194,X1200,X1198)|eqangle(X1199,X1196,X1195,X1194,X1201,X1197,X1200,X1198),inference(split_conjunct,[status(thm)],[c343])).
% 48.28/48.51 cnf(c20,negated_conjecture,para(skolem0001,skolem0004,skolem0006,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c392,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 48.28/48.51 fof(c393,plain,(![X511]:(![X512]:(![X513]:(![X514]:(~para(X511,X512,X513,X514)|para(X513,X514,X511,X512)))))),inference(variable_rename,[status(thm)],[c392])).
% 48.28/48.51 cnf(c394,plain,~para(X695,X693,X696,X694)|para(X696,X694,X695,X693),inference(split_conjunct,[status(thm)],[c393])).
% 48.28/48.51 cnf(c472,plain,para(skolem0006,skolem0003,skolem0001,skolem0004),inference(resolution,[status(thm)],[c394, c20])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 48.28/48.51 fof(c396,plain,(![X515]:(![X516]:(![X517]:(![X518]:(~para(X515,X516,X517,X518)|para(X515,X516,X518,X517)))))),inference(variable_rename,[status(thm)],[c395])).
% 48.28/48.51 cnf(c397,plain,~para(X698,X699,X697,X700)|para(X698,X699,X700,X697),inference(split_conjunct,[status(thm)],[c396])).
% 48.28/48.51 cnf(c481,plain,para(skolem0006,skolem0003,skolem0004,skolem0001),inference(resolution,[status(thm)],[c397, c472])).
% 48.28/48.51 cnf(c1335,plain,eqangle(skolem0006,skolem0003,X1655,X1654,skolem0004,skolem0001,X1655,X1654),inference(resolution,[status(thm)],[c283, c481])).
% 48.28/48.51 cnf(c2235,plain,eqangle(skolem0006,skolem0003,skolem0004,skolem0001,X1712,X1713,X1712,X1713),inference(resolution,[status(thm)],[c1335, c344])).
% 48.28/48.51 cnf(c2442,plain,eqangle(X2037,X2036,X2037,X2036,skolem0006,skolem0003,skolem0004,skolem0001),inference(resolution,[status(thm)],[c2235, c347])).
% 48.28/48.51 cnf(c4039,plain,eqangle(X2659,X2660,X2660,X2659,skolem0006,skolem0003,skolem0004,skolem0001),inference(resolution,[status(thm)],[c2442, c353])).
% 48.28/48.51 fof(ruleD22,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(![E]:(![F]:(![G]:(![H]:((eqangle(A,B,C,D,P,Q,U,V)&eqangle(P,Q,U,V,E,F,G,H))=>eqangle(A,B,C,D,E,F,G,H)))))))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD22)).
% 48.28/48.51 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(![E]:(![F]:(![G]:(![H]:((~eqangle(A,B,C,D,P,Q,U,V)|~eqangle(P,Q,U,V,E,F,G,H))|eqangle(A,B,C,D,E,F,G,H)))))))))))))),inference(fof_nnf,[status(thm)],[ruleD22])).
% 48.28/48.51 fof(c340,plain,(![X412]:(![X413]:(![X414]:(![X415]:(![X416]:(![X417]:(![X418]:(![X419]:(![X420]:(![X421]:(![X422]:(![X423]:((~eqangle(X412,X413,X414,X415,X416,X417,X418,X419)|~eqangle(X416,X417,X418,X419,X420,X421,X422,X423))|eqangle(X412,X413,X414,X415,X420,X421,X422,X423)))))))))))))),inference(variable_rename,[status(thm)],[c339])).
% 48.28/48.51 cnf(c341,plain,~eqangle(X1185,X1189,X1183,X1184,X1190,X1188,X1191,X1193)|~eqangle(X1190,X1188,X1191,X1193,X1192,X1182,X1186,X1187)|eqangle(X1185,X1189,X1183,X1184,X1192,X1182,X1186,X1187),inference(split_conjunct,[status(thm)],[c340])).
% 48.28/48.51 cnf(c2439,plain,~eqangle(X4171,X4169,X4173,X4170,skolem0006,skolem0003,skolem0004,skolem0001)|eqangle(X4171,X4169,X4173,X4170,X4172,X4168,X4172,X4168),inference(resolution,[status(thm)],[c2235, c341])).
% 48.28/48.51 cnf(c18519,plain,eqangle(X4853,X4850,X4850,X4853,X4851,X4852,X4851,X4852),inference(resolution,[status(thm)],[c2439, c4039])).
% 48.28/48.51 cnf(c20061,plain,eqangle(X4984,X4983,X4984,X4983,X4982,X4981,X4981,X4982),inference(resolution,[status(thm)],[c18519, c347])).
% 48.28/48.51 cnf(c20175,plain,~cyclic(X5974,X5974,X5973,X5975)|cong(X5974,X5974,X5975,X5975),inference(resolution,[status(thm)],[c20061, c268])).
% 48.28/48.51 cnf(c21335,plain,cong(X5978,X5978,X5979,X5979),inference(resolution,[status(thm)],[c20175, c20276])).
% 48.28/48.51 cnf(c21362,plain,~coll(X6027,X6027,X6027)|midp(X6027,X6027,X6027),inference(resolution,[status(thm)],[c21335, c186])).
% 48.28/48.51 cnf(c21526,plain,midp(X6028,X6028,X6028),inference(resolution,[status(thm)],[c21362, c19717])).
% 48.28/48.51 cnf(c21537,plain,midp(X6030,X6031,X6031),inference(resolution,[status(thm)],[c21526, c13847])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c236,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])).
% 48.28/48.51 fof(c237,plain,(![X230]:(![X231]:(![X232]:(![X233]:((~perp(X230,X231,X231,X232)|~midp(X233,X230,X232))|cong(X230,X233,X231,X233)))))),inference(variable_rename,[status(thm)],[c236])).
% 48.28/48.51 cnf(c238,plain,~perp(X1009,X1008,X1008,X1010)|~midp(X1011,X1009,X1010)|cong(X1009,X1011,X1008,X1011),inference(split_conjunct,[status(thm)],[c237])).
% 48.28/48.51 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)).
% 48.28/48.51 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(fof_nnf,[status(thm)],[ruleD74])).
% 48.28/48.51 fof(c158,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)],[c157])).
% 48.28/48.51 fof(c160,plain,(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:((~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))|perp(X123,X124,X125,X126)))))))))),inference(shift_quantors,[status(thm)],[fof(c159,plain,(![X123]:(![X124]:(![X125]:(![X126]:((![X127]:(![X128]:(![X129]:(![X130]:(~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))))))|perp(X123,X124,X125,X126)))))),inference(variable_rename,[status(thm)],[c158])).])).
% 48.28/48.51 cnf(c161,plain,~eqangle(X915,X918,X916,X919,X913,X914,X912,X917)|~perp(X913,X914,X912,X917)|perp(X915,X918,X916,X919),inference(split_conjunct,[status(thm)],[c160])).
% 48.28/48.51 cnf(c20045,plain,~perp(X5931,X5928,X5931,X5928)|perp(X5930,X5929,X5929,X5930),inference(resolution,[status(thm)],[c18519, c161])).
% 48.28/48.51 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)).
% 48.28/48.51 fof(c222,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])).
% 48.28/48.51 fof(c223,plain,(![X214]:(![X215]:(![X216]:(![X217]:((~cong(X214,X216,X215,X216)|~cong(X214,X217,X215,X217))|perp(X214,X215,X216,X217)))))),inference(variable_rename,[status(thm)],[c222])).
% 48.28/48.51 cnf(c224,plain,~cong(X995,X992,X993,X992)|~cong(X995,X994,X993,X994)|perp(X995,X993,X992,X994),inference(split_conjunct,[status(thm)],[c223])).
% 48.28/48.51 cnf(c1118,plain,~cong(X1237,X1239,X1238,X1239)|perp(X1237,X1238,X1239,X1239),inference(factor,[status(thm)],[c224])).
% 48.28/48.51 cnf(c21346,plain,perp(X5990,X5990,X5990,X5990),inference(resolution,[status(thm)],[c21335, c1118])).
% 48.28/48.51 cnf(c21394,plain,perp(X6004,X6003,X6003,X6004),inference(resolution,[status(thm)],[c21346, c20045])).
% 48.28/48.51 cnf(c21470,plain,~midp(X6819,X6821,X6821)|cong(X6821,X6819,X6820,X6819),inference(resolution,[status(thm)],[c21394, c238])).
% 48.28/48.51 cnf(c23912,plain,cong(X6824,X6822,X6823,X6822),inference(resolution,[status(thm)],[c21470, c21537])).
% 48.28/48.51 cnf(c23923,plain,cong(X6829,X6828,X6828,X6830),inference(resolution,[status(thm)],[c23912, c338])).
% 48.28/48.51 cnf(c23994,plain,cong(X6849,X6848,X6850,X6849),inference(resolution,[status(thm)],[c23923, c335])).
% 48.28/48.51 cnf(c24055,plain,cong(X6865,X6866,X6865,X6867),inference(resolution,[status(thm)],[c23994, c338])).
% 48.28/48.51 cnf(c24091,plain,$false,inference(resolution,[status(thm)],[c24055, c21])).
% 48.28/48.51 % SZS output end CNFRefutation
% 48.28/48.51
% 48.28/48.51 % Initial clauses : 134
% 48.28/48.51 % Processed clauses : 2532
% 48.28/48.51 % Factors computed : 266
% 48.28/48.51 % Resolvents computed: 23420
% 48.28/48.51 % Tautologies deleted: 12
% 48.28/48.51 % Forward subsumed : 5422
% 48.28/48.51 % Backward subsumed : 1711
% 48.28/48.51 % -------- CPU Time ---------
% 48.28/48.51 % User time : 48.100 s
% 48.28/48.51 % System time : 0.062 s
% 48.28/48.51 % Total time : 48.162 s
%------------------------------------------------------------------------------