%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO582+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:20 EDT 2024
% Result : Theorem 50.34s 50.58s
% Output : Refutation 50.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO582+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n023.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 08:04:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 50.34/50.58 % Version: 1.5
% 50.34/50.58 % SZS status Theorem
% 50.34/50.58 % SZS output start CNFRefutation
% 50.34/50.58 fof(exemplo6GDDFULL416044,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![A1]:(![C1]:(![NWPNT1]:((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,A,A1))&coll(A1,C,D))&perp(C,D,C,C1))&coll(C1,A,B))=>para(D,B,A1,C1)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL416044)).
% 50.34/50.58 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![A1]:(![C1]:(![NWPNT1]:((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,A,A1))&coll(A1,C,D))&perp(C,D,C,C1))&coll(C1,A,B))=>para(D,B,A1,C1))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416044])).
% 50.34/50.58 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[A1]:(?[C1]:(?[NWPNT1]:((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,A,A1))&coll(A1,C,D))&perp(C,D,C,C1))&coll(C1,A,B))&~para(D,B,A1,C1)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 50.34/50.58 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[A1]:(?[C1]:((((((circle(O,A,B,C)&(?[NWPNT1]:circle(O,A,D,NWPNT1)))&perp(A,B,A,A1))&coll(A1,C,D))&perp(C,D,C,C1))&coll(C1,A,B))&~para(D,B,A1,C1))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 50.34/50.58 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((circle(X5,X2,X3,X4)&(?[X9]:circle(X5,X2,X6,X9)))&perp(X2,X3,X2,X7))&coll(X7,X4,X6))&perp(X4,X6,X4,X8))&coll(X8,X2,X3))&~para(X6,X3,X7,X8))))))))),inference(variable_rename,[status(thm)],[c13])).
% 50.34/50.58 fof(c15,negated_conjecture,((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0008))&perp(skolem0001,skolem0002,skolem0001,skolem0006))&coll(skolem0006,skolem0003,skolem0005))&perp(skolem0003,skolem0005,skolem0003,skolem0007))&coll(skolem0007,skolem0001,skolem0002))&~para(skolem0005,skolem0002,skolem0006,skolem0007)),inference(skolemize,[status(esa)],[c14])).
% 50.34/50.58 cnf(c22,negated_conjecture,~para(skolem0005,skolem0002,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c399,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 50.34/50.58 fof(c400,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c399])).
% 50.34/50.58 cnf(c401,plain,~coll(X727,X729,X728)|~coll(X727,X729,X730)|coll(X728,X730,X727),inference(split_conjunct,[status(thm)],[c400])).
% 50.34/50.58 cnf(c505,plain,~coll(X738,X737,X736)|coll(X736,X736,X738),inference(factor,[status(thm)],[c401])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c188,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 50.34/50.58 fof(c189,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c188])).
% 50.34/50.58 cnf(c190,plain,~para(X608,X609,X608,X610)|coll(X608,X609,X610),inference(split_conjunct,[status(thm)],[c189])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c285,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])).
% 50.34/50.58 fof(c286,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)],[c285])).
% 50.34/50.58 fof(c288,plain,(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)|para(X296,X297,X298,X299)))))))),inference(shift_quantors,[status(thm)],[fof(c287,plain,(![X296]:(![X297]:(![X298]:(![X299]:((![X300]:(![X301]:~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))|para(X296,X297,X298,X299)))))),inference(variable_rename,[status(thm)],[c286])).])).
% 50.34/50.58 cnf(c289,plain,~eqangle(X1117,X1118,X1119,X1121,X1120,X1116,X1119,X1121)|para(X1117,X1118,X1120,X1116),inference(split_conjunct,[status(thm)],[c288])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c349,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])).
% 50.34/50.58 fof(c350,plain,(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(~eqangle(X442,X443,X444,X445,X446,X447,X448,X449)|eqangle(X444,X445,X442,X443,X448,X449,X446,X447)))))))))),inference(variable_rename,[status(thm)],[c349])).
% 50.34/50.58 cnf(c351,plain,~eqangle(X1270,X1264,X1271,X1265,X1266,X1268,X1267,X1269)|eqangle(X1271,X1265,X1270,X1264,X1267,X1269,X1266,X1268),inference(split_conjunct,[status(thm)],[c350])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c280,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])).
% 50.34/50.58 fof(c281,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)],[c280])).
% 50.34/50.58 fof(c283,plain,(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(~para(X290,X291,X292,X293)|eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(shift_quantors,[status(thm)],[fof(c282,plain,(![X290]:(![X291]:(![X292]:(![X293]:(~para(X290,X291,X292,X293)|(![X294]:(![X295]:eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(variable_rename,[status(thm)],[c281])).])).
% 50.34/50.58 cnf(c284,plain,~para(X1110,X1111,X1109,X1113)|eqangle(X1110,X1111,X1112,X1114,X1109,X1113,X1112,X1114),inference(split_conjunct,[status(thm)],[c283])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 50.34/50.58 fof(c385,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c384])).
% 50.34/50.58 cnf(c386,plain,~perp(X647,X649,X648,X650)|perp(X648,X650,X647,X649),inference(split_conjunct,[status(thm)],[c385])).
% 50.34/50.58 cnf(c20,negated_conjecture,perp(skolem0003,skolem0005,skolem0003,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 50.34/50.58 cnf(c451,plain,perp(skolem0003,skolem0007,skolem0003,skolem0005),inference(resolution,[status(thm)],[c386, c20])).
% 50.34/50.58 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 50.34/50.58 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 50.34/50.58 fof(c388,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c387])).
% 50.34/50.58 cnf(c389,plain,~perp(X667,X668,X669,X670)|perp(X667,X668,X670,X669),inference(split_conjunct,[status(thm)],[c388])).
% 50.34/50.58 cnf(c457,plain,perp(skolem0003,skolem0007,skolem0005,skolem0003),inference(resolution,[status(thm)],[c389, c451])).
% 50.34/50.58 cnf(c462,plain,perp(skolem0005,skolem0003,skolem0003,skolem0007),inference(resolution,[status(thm)],[c457, c386])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c381,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])).
% 50.34/50.58 fof(c382,plain,(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:((~perp(X493,X494,X495,X496)|~perp(X495,X496,X497,X498))|para(X493,X494,X497,X498)))))))),inference(variable_rename,[status(thm)],[c381])).
% 50.34/50.58 cnf(c383,plain,~perp(X1302,X1305,X1303,X1300)|~perp(X1303,X1300,X1301,X1304)|para(X1302,X1305,X1301,X1304),inference(split_conjunct,[status(thm)],[c382])).
% 50.34/50.58 cnf(c1458,plain,~perp(X2467,X2468,skolem0003,skolem0007)|para(X2467,X2468,skolem0005,skolem0003),inference(resolution,[status(thm)],[c383, c457])).
% 50.34/50.58 cnf(c5987,plain,para(skolem0005,skolem0003,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1458, c462])).
% 50.34/50.58 cnf(c6001,plain,eqangle(skolem0005,skolem0003,X2747,X2746,skolem0005,skolem0003,X2747,X2746),inference(resolution,[status(thm)],[c5987, c284])).
% 50.34/50.58 cnf(c8082,plain,eqangle(X3187,X3188,skolem0005,skolem0003,X3187,X3188,skolem0005,skolem0003),inference(resolution,[status(thm)],[c6001, c351])).
% 50.34/50.58 cnf(c11914,plain,para(X3190,X3189,X3190,X3189),inference(resolution,[status(thm)],[c8082, c289])).
% 50.34/50.58 cnf(c11938,plain,coll(X3192,X3191,X3191),inference(resolution,[status(thm)],[c11914, c190])).
% 50.34/50.58 cnf(c12034,plain,coll(X3197,X3197,X3198),inference(resolution,[status(thm)],[c11938, c505])).
% 50.34/50.58 cnf(c12717,plain,~coll(X3662,X3662,X3661)|coll(X3661,X3660,X3662),inference(resolution,[status(thm)],[c12034, c401])).
% 50.34/50.58 cnf(c17455,plain,coll(X3669,X3668,X3667),inference(resolution,[status(thm)],[c12717, c12034])).
% 50.34/50.58 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 50.34/50.58 fof(c185,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 50.34/50.58 fof(c186,plain,(![X161]:(![X162]:(![X163]:((~cong(X161,X162,X161,X163)|~coll(X161,X162,X163))|midp(X161,X162,X163))))),inference(variable_rename,[status(thm)],[c185])).
% 50.34/50.58 cnf(c187,plain,~cong(X950,X948,X950,X949)|~coll(X950,X948,X949)|midp(X950,X948,X949),inference(split_conjunct,[status(thm)],[c186])).
% 50.34/50.58 fof(ruleD23,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD23)).
% 50.34/50.58 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 50.34/50.58 fof(c338,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c337])).
% 50.34/50.58 cnf(c339,plain,~cong(X617,X616,X618,X615)|cong(X617,X616,X615,X618),inference(split_conjunct,[status(thm)],[c338])).
% 50.34/50.58 fof(ruleD24,axiom,(![A]:(![B]:(![C]:(![D]:(cong(A,B,C,D)=>cong(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD24)).
% 50.34/50.58 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 50.34/50.58 fof(c335,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c334])).
% 50.34/50.58 cnf(c336,plain,~cong(X613,X614,X611,X612)|cong(X611,X612,X613,X614),inference(split_conjunct,[status(thm)],[c335])).
% 50.34/50.58 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD64)).
% 50.34/50.58 fof(c194,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])).
% 50.34/50.58 fof(c195,plain,(![X172]:(![X173]:(![X174]:(![X175]:(![X176]:(((~midp(X176,X172,X173)|~para(X172,X174,X173,X175))|~para(X172,X175,X173,X174))|midp(X176,X174,X175))))))),inference(variable_rename,[status(thm)],[c194])).
% 50.34/50.58 cnf(c196,plain,~midp(X959,X961,X963)|~para(X961,X960,X963,X962)|~para(X961,X962,X963,X960)|midp(X959,X960,X962),inference(split_conjunct,[status(thm)],[c195])).
% 50.34/50.58 cnf(c951,plain,~midp(X1964,X1965,X1962)|~para(X1965,X1963,X1962,X1963)|midp(X1964,X1963,X1963),inference(factor,[status(thm)],[c196])).
% 50.34/50.58 cnf(c11953,plain,~midp(X3541,X3542,X3542)|midp(X3541,X3543,X3543),inference(resolution,[status(thm)],[c11914, c951])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c364,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 50.34/50.58 fof(c365,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c364])).
% 50.34/50.58 cnf(c366,plain,~cyclic(X643,X646,X645,X644)|cyclic(X643,X646,X644,X645),inference(split_conjunct,[status(thm)],[c365])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c361,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 50.34/50.58 fof(c362,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c361])).
% 50.34/50.58 cnf(c363,plain,~cyclic(X639,X642,X641,X640)|cyclic(X639,X641,X642,X640),inference(split_conjunct,[status(thm)],[c362])).
% 50.34/50.58 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)).
% 50.34/50.58 fof(c270,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])).
% 50.34/50.58 fof(c271,plain,(![X278]:(![X279]:(![X280]:(![X281]:((~eqangle(X280,X278,X280,X279,X281,X278,X281,X279)|~coll(X280,X281,X279))|cyclic(X278,X279,X280,X281)))))),inference(variable_rename,[status(thm)],[c270])).
% 50.34/50.58 cnf(c272,plain,~eqangle(X1094,X1095,X1094,X1093,X1096,X1095,X1096,X1093)|~coll(X1094,X1096,X1093)|cyclic(X1095,X1093,X1094,X1096),inference(split_conjunct,[status(thm)],[c271])).
% 50.34/50.58 cnf(c11950,plain,eqangle(X3537,X3536,X3538,X3535,X3537,X3536,X3538,X3535),inference(resolution,[status(thm)],[c11914, c284])).
% 50.34/50.58 cnf(c17120,plain,~coll(X3894,X3894,X3896)|cyclic(X3895,X3896,X3894,X3894),inference(resolution,[status(thm)],[c11950, c272])).
% 50.34/50.58 cnf(c18394,plain,cyclic(X3898,X3899,X3897,X3897),inference(resolution,[status(thm)],[c17120, c17455])).
% 50.34/50.58 cnf(c18411,plain,cyclic(X3900,X3902,X3901,X3902),inference(resolution,[status(thm)],[c18394, c363])).
% 50.34/50.58 cnf(c18425,plain,cyclic(X3919,X3920,X3920,X3921),inference(resolution,[status(thm)],[c18411, c366])).
% 50.34/50.58 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 50.34/50.58 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(fof_nnf,[status(thm)],[ruleD43])).
% 50.34/50.58 fof(c266,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)],[c265])).
% 50.34/50.58 fof(c268,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:(![X277]:((((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276))|cong(X272,X273,X275,X276)))))))),inference(shift_quantors,[status(thm)],[fof(c267,plain,(![X272]:(![X273]:(![X274]:(![X275]:(![X276]:((![X277]:(((~cyclic(X272,X273,X274,X275)|~cyclic(X272,X273,X274,X276))|~cyclic(X272,X273,X274,X277))|~eqangle(X274,X272,X274,X273,X277,X275,X277,X276)))|cong(X272,X273,X275,X276))))))),inference(variable_rename,[status(thm)],[c266])).])).
% 50.34/50.58 cnf(c269,plain,~cyclic(X1091,X1087,X1088,X1089)|~cyclic(X1091,X1087,X1088,X1086)|~cyclic(X1091,X1087,X1088,X1090)|~eqangle(X1088,X1091,X1088,X1087,X1090,X1089,X1090,X1086)|cong(X1091,X1087,X1089,X1086),inference(split_conjunct,[status(thm)],[c268])).
% 50.34/50.58 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD21)).
% 50.34/50.58 fof(c343,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])).
% 50.34/50.58 fof(c344,plain,(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(~eqangle(X426,X427,X428,X429,X430,X431,X432,X433)|eqangle(X426,X427,X430,X431,X428,X429,X432,X433)))))))))),inference(variable_rename,[status(thm)],[c343])).
% 50.34/50.58 cnf(c345,plain,~eqangle(X1249,X1250,X1248,X1251,X1255,X1254,X1253,X1252)|eqangle(X1249,X1250,X1255,X1254,X1248,X1251,X1253,X1252),inference(split_conjunct,[status(thm)],[c344])).
% 50.34/50.58 fof(ruleD4,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD4)).
% 50.34/50.58 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 50.34/50.58 fof(c397,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c396])).
% 50.34/50.58 cnf(c398,plain,~para(X719,X718,X720,X717)|para(X719,X718,X717,X720),inference(split_conjunct,[status(thm)],[c397])).
% 50.34/50.58 cnf(c11939,plain,para(X3208,X3209,X3209,X3208),inference(resolution,[status(thm)],[c11914, c398])).
% 50.34/50.58 cnf(c12837,plain,eqangle(X3731,X3732,X3733,X3730,X3732,X3731,X3733,X3730),inference(resolution,[status(thm)],[c11939, c284])).
% 50.34/50.58 cnf(c17826,plain,eqangle(X3756,X3758,X3759,X3757,X3756,X3758,X3757,X3759),inference(resolution,[status(thm)],[c12837, c351])).
% 50.34/50.58 cnf(c17950,plain,eqangle(X3809,X3808,X3809,X3808,X3807,X3806,X3806,X3807),inference(resolution,[status(thm)],[c17826, c345])).
% 50.34/50.58 cnf(c18044,plain,~cyclic(X4789,X4789,X4788,X4790)|cong(X4789,X4789,X4790,X4790),inference(resolution,[status(thm)],[c17950, c269])).
% 50.34/50.58 cnf(c19359,plain,cong(X4793,X4793,X4794,X4794),inference(resolution,[status(thm)],[c18044, c18425])).
% 50.34/50.58 cnf(c19386,plain,~coll(X4847,X4847,X4847)|midp(X4847,X4847,X4847),inference(resolution,[status(thm)],[c19359, c187])).
% 50.34/50.58 cnf(c19509,plain,midp(X4848,X4848,X4848),inference(resolution,[status(thm)],[c19386, c17455])).
% 50.34/50.58 cnf(c19525,plain,midp(X4853,X4854,X4854),inference(resolution,[status(thm)],[c19509, c11953])).
% 50.34/50.58 fof(ruleD52,axiom,(![A]:(![B]:(![C]:(![M]:((perp(A,B,B,C)&midp(M,A,C))=>cong(A,M,B,M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD52)).
% 50.34/50.58 fof(c237,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])).
% 50.34/50.58 fof(c238,plain,(![X232]:(![X233]:(![X234]:(![X235]:((~perp(X232,X233,X233,X234)|~midp(X235,X232,X234))|cong(X232,X235,X233,X235)))))),inference(variable_rename,[status(thm)],[c237])).
% 50.34/50.58 cnf(c239,plain,~perp(X1032,X1035,X1035,X1033)|~midp(X1034,X1032,X1033)|cong(X1032,X1034,X1035,X1034),inference(split_conjunct,[status(thm)],[c238])).
% 50.34/50.58 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD74)).
% 50.34/50.58 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(fof_nnf,[status(thm)],[ruleD74])).
% 50.34/50.58 fof(c159,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)],[c158])).
% 50.34/50.58 fof(c161,plain,(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:((~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))|perp(X125,X126,X127,X128)))))))))),inference(shift_quantors,[status(thm)],[fof(c160,plain,(![X125]:(![X126]:(![X127]:(![X128]:((![X129]:(![X130]:(![X131]:(![X132]:(~eqangle(X125,X126,X127,X128,X129,X130,X131,X132)|~perp(X129,X130,X131,X132))))))|perp(X125,X126,X127,X128)))))),inference(variable_rename,[status(thm)],[c159])).])).
% 50.34/50.58 cnf(c162,plain,~eqangle(X915,X919,X913,X916,X917,X918,X914,X912)|~perp(X917,X918,X914,X912)|perp(X915,X919,X913,X916),inference(split_conjunct,[status(thm)],[c161])).
% 50.34/50.58 cnf(c17834,plain,eqangle(X3772,X3773,X3773,X3772,X3770,X3771,X3770,X3771),inference(resolution,[status(thm)],[c12837, c345])).
% 50.34/50.58 cnf(c17957,plain,~perp(X4744,X4743,X4744,X4743)|perp(X4746,X4745,X4745,X4746),inference(resolution,[status(thm)],[c17834, c162])).
% 50.34/50.58 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD56)).
% 50.34/50.58 fof(c223,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])).
% 50.34/50.58 fof(c224,plain,(![X216]:(![X217]:(![X218]:(![X219]:((~cong(X216,X218,X217,X218)|~cong(X216,X219,X217,X219))|perp(X216,X217,X218,X219)))))),inference(variable_rename,[status(thm)],[c223])).
% 50.34/50.58 cnf(c225,plain,~cong(X1010,X1009,X1011,X1009)|~cong(X1010,X1008,X1011,X1008)|perp(X1010,X1011,X1009,X1008),inference(split_conjunct,[status(thm)],[c224])).
% 50.34/50.58 cnf(c978,plain,~cong(X1013,X1012,X1014,X1012)|perp(X1013,X1014,X1012,X1012),inference(factor,[status(thm)],[c225])).
% 50.34/50.58 cnf(c19378,plain,perp(X4805,X4805,X4805,X4805),inference(resolution,[status(thm)],[c19359, c978])).
% 50.34/50.58 cnf(c19396,plain,perp(X4816,X4817,X4817,X4816),inference(resolution,[status(thm)],[c19378, c17957])).
% 50.34/50.58 cnf(c19427,plain,~midp(X5645,X5644,X5644)|cong(X5644,X5645,X5643,X5645),inference(resolution,[status(thm)],[c19396, c239])).
% 50.34/50.58 cnf(c21479,plain,cong(X5647,X5646,X5648,X5646),inference(resolution,[status(thm)],[c19427, c19525])).
% 50.34/50.58 cnf(c21503,plain,cong(X5659,X5657,X5657,X5658),inference(resolution,[status(thm)],[c21479, c339])).
% 50.34/50.58 cnf(c21557,plain,cong(X5687,X5685,X5686,X5687),inference(resolution,[status(thm)],[c21503, c336])).
% 50.34/50.58 cnf(c21636,plain,cong(X5705,X5707,X5705,X5706),inference(resolution,[status(thm)],[c21557, c339])).
% 50.34/50.58 cnf(c21666,plain,~coll(X5945,X5947,X5946)|midp(X5945,X5947,X5946),inference(resolution,[status(thm)],[c21636, c187])).
% 50.34/50.58 cnf(c22146,plain,midp(X5952,X5954,X5953),inference(resolution,[status(thm)],[c21666, c17455])).
% 50.34/50.58 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 50.34/50.58 fof(c262,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])).
% 50.34/50.58 fof(c263,plain,(![X267]:(![X268]:(![X269]:(![X270]:(![X271]:((~midp(X270,X267,X268)|~midp(X271,X267,X269))|para(X270,X271,X268,X269))))))),inference(variable_rename,[status(thm)],[c262])).
% 50.34/50.58 cnf(c264,plain,~midp(X1077,X1080,X1081)|~midp(X1079,X1080,X1078)|para(X1077,X1079,X1081,X1078),inference(split_conjunct,[status(thm)],[c263])).
% 50.34/50.58 cnf(c19546,plain,~midp(X9492,X9495,X9493)|para(X9492,X9494,X9493,X9495),inference(resolution,[status(thm)],[c19525, c264])).
% 50.34/50.58 cnf(c24987,plain,para(X9496,X9499,X9498,X9497),inference(resolution,[status(thm)],[c19546, c22146])).
% 50.34/50.58 cnf(c25007,plain,$false,inference(resolution,[status(thm)],[c24987, c22])).
% 50.34/50.58 % SZS output end CNFRefutation
% 50.34/50.58
% 50.34/50.58 % Initial clauses : 134
% 50.34/50.58 % Processed clauses : 2612
% 50.34/50.58 % Factors computed : 123
% 50.34/50.58 % Resolvents computed: 24480
% 50.34/50.58 % Tautologies deleted: 12
% 50.34/50.58 % Forward subsumed : 6408
% 50.34/50.58 % Backward subsumed : 2075
% 50.34/50.58 % -------- CPU Time ---------
% 50.34/50.58 % User time : 50.175 s
% 50.34/50.58 % System time : 0.070 s
% 50.34/50.58 % Total time : 50.245 s
%------------------------------------------------------------------------------