%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO552+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:16 EDT 2024
% Result : Theorem 27.61s 27.77s
% Output : Refutation 27.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO552+1 : TPTP v8.1.2. Released v7.5.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n025.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:22:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 27.61/27.77 % Version: 1.5
% 27.61/27.77 % SZS status Theorem
% 27.61/27.77 % SZS output start CNFRefutation
% 27.61/27.77 fof(exemplo6GDDFULL012012,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![F]:(![NWPNT1]:((((((circle(O,A,B,C)&perp(A,C,B,D))&circle(O,A,D,NWPNT1))&coll(E,A,C))&coll(E,B,D))&midp(F,B,A))=>perp(F,E,C,D)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL012012)).
% 27.61/27.77 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![E]:(![F]:(![NWPNT1]:((((((circle(O,A,B,C)&perp(A,C,B,D))&circle(O,A,D,NWPNT1))&coll(E,A,C))&coll(E,B,D))&midp(F,B,A))=>perp(F,E,C,D))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL012012])).
% 27.61/27.77 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(?[F]:(?[NWPNT1]:((((((circle(O,A,B,C)&perp(A,C,B,D))&circle(O,A,D,NWPNT1))&coll(E,A,C))&coll(E,B,D))&midp(F,B,A))&~perp(F,E,C,D)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 27.61/27.77 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[E]:(?[F]:((((((circle(O,A,B,C)&perp(A,C,B,D))&(?[NWPNT1]:circle(O,A,D,NWPNT1)))&coll(E,A,C))&coll(E,B,D))&midp(F,B,A))&~perp(F,E,C,D))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 27.61/27.77 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((circle(X5,X2,X3,X4)&perp(X2,X4,X3,X6))&(?[X9]:circle(X5,X2,X6,X9)))&coll(X7,X2,X4))&coll(X7,X3,X6))&midp(X8,X3,X2))&~perp(X8,X7,X4,X6))))))))),inference(variable_rename,[status(thm)],[c13])).
% 27.61/27.77 fof(c15,negated_conjecture,((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&perp(skolem0001,skolem0003,skolem0002,skolem0005))&circle(skolem0004,skolem0001,skolem0005,skolem0008))&coll(skolem0006,skolem0001,skolem0003))&coll(skolem0006,skolem0002,skolem0005))&midp(skolem0007,skolem0002,skolem0001))&~perp(skolem0007,skolem0006,skolem0003,skolem0005)),inference(skolemize,[status(esa)],[c14])).
% 27.61/27.77 cnf(c22,negated_conjecture,~perp(skolem0007,skolem0006,skolem0003,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c401,plain,~coll(X748,X746,X749)|~coll(X748,X746,X747)|coll(X749,X747,X748),inference(split_conjunct,[status(thm)],[c400])).
% 27.61/27.77 cnf(c524,plain,~coll(X752,X750,X751)|coll(X751,X751,X752),inference(factor,[status(thm)],[c401])).
% 27.61/27.77 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)).
% 27.61/27.77 fof(c188,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 27.61/27.77 fof(c189,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c188])).
% 27.61/27.77 cnf(c190,plain,~para(X654,X652,X654,X653)|coll(X654,X652,X653),inference(split_conjunct,[status(thm)],[c189])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 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])).])).
% 27.61/27.77 cnf(c289,plain,~eqangle(X1090,X1088,X1091,X1093,X1092,X1089,X1091,X1093)|para(X1090,X1088,X1092,X1089),inference(split_conjunct,[status(thm)],[c288])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c351,plain,~eqangle(X1233,X1228,X1227,X1226,X1229,X1232,X1230,X1231)|eqangle(X1227,X1226,X1233,X1228,X1230,X1231,X1229,X1232),inference(split_conjunct,[status(thm)],[c350])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 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])).])).
% 27.61/27.77 cnf(c284,plain,~para(X1084,X1082,X1085,X1087)|eqangle(X1084,X1082,X1086,X1083,X1085,X1087,X1086,X1083),inference(split_conjunct,[status(thm)],[c283])).
% 27.61/27.77 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)).
% 27.61/27.77 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 27.61/27.77 fof(c397,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c396])).
% 27.61/27.77 cnf(c398,plain,~para(X738,X736,X737,X739)|para(X738,X736,X739,X737),inference(split_conjunct,[status(thm)],[c397])).
% 27.61/27.77 cnf(c21,negated_conjecture,midp(skolem0007,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c15])).
% 27.61/27.77 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 27.61/27.77 fof(c375,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 27.61/27.77 fof(c376,plain,(![X484]:(![X485]:(![X486]:(~midp(X486,X485,X484)|midp(X486,X484,X485))))),inference(variable_rename,[status(thm)],[c375])).
% 27.61/27.77 cnf(c377,plain,~midp(X551,X550,X552)|midp(X551,X552,X550),inference(split_conjunct,[status(thm)],[c376])).
% 27.61/27.77 cnf(c415,plain,midp(skolem0007,skolem0001,skolem0002),inference(resolution,[status(thm)],[c377, c21])).
% 27.61/27.77 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 27.61/27.77 fof(c197,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 27.61/27.77 fof(c198,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c197])).
% 27.61/27.77 fof(c200,plain,(![X177]:(![X178]:(![X179]:(![X180]:(![X181]:((~midp(X181,X177,X178)|~midp(X181,X179,X180))|para(X177,X179,X178,X180))))))),inference(shift_quantors,[status(thm)],[fof(c199,plain,(![X177]:(![X178]:(![X179]:(![X180]:((![X181]:(~midp(X181,X177,X178)|~midp(X181,X179,X180)))|para(X177,X179,X178,X180)))))),inference(variable_rename,[status(thm)],[c198])).])).
% 27.61/27.77 cnf(c201,plain,~midp(X947,X948,X949)|~midp(X947,X951,X950)|para(X948,X951,X949,X950),inference(split_conjunct,[status(thm)],[c200])).
% 27.61/27.77 cnf(c1012,plain,~midp(skolem0007,X1645,X1646)|para(X1645,skolem0001,X1646,skolem0002),inference(resolution,[status(thm)],[c201, c415])).
% 27.61/27.77 cnf(c2627,plain,para(skolem0002,skolem0001,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1012, c21])).
% 27.61/27.77 cnf(c2639,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c2627, c398])).
% 27.61/27.77 cnf(c2665,plain,eqangle(skolem0002,skolem0001,X2316,X2317,skolem0002,skolem0001,X2316,X2317),inference(resolution,[status(thm)],[c2639, c284])).
% 27.61/27.77 cnf(c4491,plain,eqangle(X2421,X2420,skolem0002,skolem0001,X2421,X2420,skolem0002,skolem0001),inference(resolution,[status(thm)],[c2665, c351])).
% 27.61/27.77 cnf(c4770,plain,para(X2422,X2423,X2422,X2423),inference(resolution,[status(thm)],[c4491, c289])).
% 27.61/27.77 cnf(c4790,plain,coll(X2424,X2425,X2425),inference(resolution,[status(thm)],[c4770, c190])).
% 27.61/27.77 cnf(c4996,plain,coll(X2434,X2434,X2435),inference(resolution,[status(thm)],[c4790, c524])).
% 27.61/27.77 cnf(c5365,plain,~coll(X3455,X3455,X3456)|coll(X3456,X3457,X3455),inference(resolution,[status(thm)],[c4996, c401])).
% 27.61/27.77 cnf(c8725,plain,coll(X3459,X3458,X3460),inference(resolution,[status(thm)],[c5365, c4996])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c187,plain,~cong(X934,X935,X934,X936)|~coll(X934,X935,X936)|midp(X934,X935,X936),inference(split_conjunct,[status(thm)],[c186])).
% 27.61/27.77 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)).
% 27.61/27.77 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 27.61/27.77 fof(c338,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c337])).
% 27.61/27.77 cnf(c339,plain,~cong(X672,X674,X671,X673)|cong(X672,X674,X673,X671),inference(split_conjunct,[status(thm)],[c338])).
% 27.61/27.77 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)).
% 27.61/27.77 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 27.61/27.77 fof(c335,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c334])).
% 27.61/27.77 cnf(c336,plain,~cong(X667,X668,X670,X669)|cong(X670,X669,X667,X668),inference(split_conjunct,[status(thm)],[c335])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c239,plain,~perp(X1010,X1012,X1012,X1011)|~midp(X1009,X1010,X1011)|cong(X1010,X1009,X1012,X1009),inference(split_conjunct,[status(thm)],[c238])).
% 27.61/27.77 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)).
% 27.61/27.77 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 27.61/27.77 fof(c388,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c387])).
% 27.61/27.77 cnf(c389,plain,~perp(X709,X712,X711,X710)|perp(X709,X712,X710,X711),inference(split_conjunct,[status(thm)],[c388])).
% 27.61/27.77 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)).
% 27.61/27.77 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 27.61/27.77 fof(c385,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c384])).
% 27.61/27.77 cnf(c386,plain,~perp(X707,X705,X708,X706)|perp(X708,X706,X707,X705),inference(split_conjunct,[status(thm)],[c385])).
% 27.61/27.77 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 27.61/27.77 fof(c182,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 27.61/27.77 fof(c183,plain,(![X158]:(![X159]:(![X160]:(~midp(X158,X159,X160)|cong(X158,X159,X158,X160))))),inference(variable_rename,[status(thm)],[c182])).
% 27.61/27.77 cnf(c184,plain,~midp(X649,X650,X651)|cong(X649,X650,X649,X651),inference(split_conjunct,[status(thm)],[c183])).
% 27.61/27.77 cnf(c474,plain,cong(skolem0007,skolem0001,skolem0007,skolem0002),inference(resolution,[status(thm)],[c184, c415])).
% 27.61/27.77 cnf(c480,plain,cong(skolem0007,skolem0001,skolem0002,skolem0007),inference(resolution,[status(thm)],[c339, c474])).
% 27.61/27.77 cnf(c484,plain,cong(skolem0002,skolem0007,skolem0007,skolem0001),inference(resolution,[status(thm)],[c480, c336])).
% 27.61/27.77 cnf(c488,plain,cong(skolem0002,skolem0007,skolem0001,skolem0007),inference(resolution,[status(thm)],[c484, c339])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c225,plain,~cong(X989,X987,X990,X987)|~cong(X989,X988,X990,X988)|perp(X989,X990,X987,X988),inference(split_conjunct,[status(thm)],[c224])).
% 27.61/27.77 cnf(c1049,plain,~cong(X991,X993,X992,X993)|perp(X991,X992,X993,X993),inference(factor,[status(thm)],[c225])).
% 27.61/27.77 cnf(c1053,plain,perp(skolem0002,skolem0001,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1049, c488])).
% 27.61/27.77 cnf(c1061,plain,perp(skolem0007,skolem0007,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1053, c386])).
% 27.61/27.77 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 27.61/27.77 fof(c378,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])).
% 27.61/27.77 fof(c379,plain,(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:(![X492]:((~para(X487,X488,X489,X490)|~perp(X489,X490,X491,X492))|perp(X487,X488,X491,X492)))))))),inference(variable_rename,[status(thm)],[c378])).
% 27.61/27.77 cnf(c380,plain,~para(X1258,X1261,X1259,X1257)|~perp(X1259,X1257,X1256,X1260)|perp(X1258,X1261,X1256,X1260),inference(split_conjunct,[status(thm)],[c379])).
% 27.61/27.77 cnf(c1563,plain,~para(X3088,X3089,skolem0007,skolem0007)|perp(X3088,X3089,skolem0002,skolem0001),inference(resolution,[status(thm)],[c380, c1061])).
% 27.61/27.77 fof(ruleD5,axiom,(![A]:(![B]:(![C]:(![D]:(para(A,B,C,D)=>para(C,D,A,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD5)).
% 27.61/27.77 fof(c393,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 27.61/27.77 fof(c394,plain,(![X513]:(![X514]:(![X515]:(![X516]:(~para(X513,X514,X515,X516)|para(X515,X516,X513,X514)))))),inference(variable_rename,[status(thm)],[c393])).
% 27.61/27.77 cnf(c395,plain,~para(X731,X730,X729,X728)|para(X729,X728,X731,X730),inference(split_conjunct,[status(thm)],[c394])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c264,plain,~midp(X1054,X1057,X1058)|~midp(X1056,X1057,X1055)|para(X1054,X1056,X1058,X1055),inference(split_conjunct,[status(thm)],[c263])).
% 27.61/27.77 cnf(c1143,plain,~midp(X1061,X1059,X1060)|para(X1061,X1061,X1060,X1060),inference(factor,[status(thm)],[c264])).
% 27.61/27.77 cnf(c1146,plain,para(skolem0007,skolem0007,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1143, c415])).
% 27.61/27.77 cnf(c1149,plain,para(skolem0002,skolem0002,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1146, c395])).
% 27.61/27.77 fof(ruleD6,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)¶(C,D,E,F))=>para(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 27.61/27.77 fof(c390,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])).
% 27.61/27.77 fof(c391,plain,(![X507]:(![X508]:(![X509]:(![X510]:(![X511]:(![X512]:((~para(X507,X508,X509,X510)|~para(X509,X510,X511,X512))|para(X507,X508,X511,X512)))))))),inference(variable_rename,[status(thm)],[c390])).
% 27.61/27.77 cnf(c392,plain,~para(X1270,X1273,X1269,X1272)|~para(X1269,X1272,X1268,X1271)|para(X1270,X1273,X1268,X1271),inference(split_conjunct,[status(thm)],[c391])).
% 27.61/27.77 cnf(c1603,plain,~para(X3151,X3150,skolem0002,skolem0002)|para(X3151,X3150,skolem0007,skolem0007),inference(resolution,[status(thm)],[c392, c1149])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c383,plain,~perp(X1267,X1265,X1266,X1264)|~perp(X1266,X1264,X1262,X1263)|para(X1267,X1265,X1262,X1263),inference(split_conjunct,[status(thm)],[c382])).
% 27.61/27.77 cnf(c1576,plain,~perp(X3112,X3113,skolem0007,skolem0007)|para(X3112,X3113,skolem0002,skolem0001),inference(resolution,[status(thm)],[c383, c1061])).
% 27.61/27.77 cnf(c475,plain,cong(skolem0007,skolem0002,skolem0007,skolem0001),inference(resolution,[status(thm)],[c184, c21])).
% 27.61/27.77 cnf(c481,plain,cong(skolem0007,skolem0002,skolem0001,skolem0007),inference(resolution,[status(thm)],[c339, c475])).
% 27.61/27.77 cnf(c487,plain,cong(skolem0001,skolem0007,skolem0007,skolem0002),inference(resolution,[status(thm)],[c481, c336])).
% 27.61/27.77 cnf(c491,plain,cong(skolem0001,skolem0007,skolem0002,skolem0007),inference(resolution,[status(thm)],[c487, c339])).
% 27.61/27.77 fof(ruleD25,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((cong(A,B,C,D)&cong(C,D,E,F))=>cong(A,B,E,F)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 27.61/27.77 fof(c331,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~cong(A,B,C,D)|~cong(C,D,E,F))|cong(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD25])).
% 27.61/27.77 fof(c332,plain,(![X400]:(![X401]:(![X402]:(![X403]:(![X404]:(![X405]:((~cong(X400,X401,X402,X403)|~cong(X402,X403,X404,X405))|cong(X400,X401,X404,X405)))))))),inference(variable_rename,[status(thm)],[c331])).
% 27.61/27.77 cnf(c333,plain,~cong(X1197,X1193,X1192,X1196)|~cong(X1192,X1196,X1195,X1194)|cong(X1197,X1193,X1195,X1194),inference(split_conjunct,[status(thm)],[c332])).
% 27.61/27.77 cnf(c1437,plain,~cong(X2934,X2933,skolem0001,skolem0007)|cong(X2934,X2933,skolem0002,skolem0007),inference(resolution,[status(thm)],[c333, c491])).
% 27.61/27.77 cnf(c7896,plain,cong(skolem0002,skolem0007,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1437, c488])).
% 27.61/27.77 cnf(c9018,plain,perp(skolem0002,skolem0002,skolem0007,skolem0007),inference(resolution,[status(thm)],[c7896, c1049])).
% 27.61/27.77 cnf(c9249,plain,para(skolem0002,skolem0002,skolem0002,skolem0001),inference(resolution,[status(thm)],[c9018, c1576])).
% 27.61/27.77 cnf(c9437,plain,para(skolem0002,skolem0001,skolem0002,skolem0002),inference(resolution,[status(thm)],[c9249, c395])).
% 27.61/27.77 cnf(c9598,plain,para(skolem0002,skolem0001,skolem0007,skolem0007),inference(resolution,[status(thm)],[c9437, c1603])).
% 27.61/27.77 cnf(c9746,plain,perp(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c9598, c1563])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 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])).])).
% 27.61/27.77 cnf(c162,plain,~eqangle(X908,X909,X905,X906,X904,X910,X911,X907)|~perp(X904,X910,X911,X907)|perp(X908,X909,X905,X906),inference(split_conjunct,[status(thm)],[c161])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c345,plain,~eqangle(X1211,X1216,X1212,X1213,X1210,X1217,X1214,X1215)|eqangle(X1211,X1216,X1210,X1217,X1212,X1213,X1214,X1215),inference(split_conjunct,[status(thm)],[c344])).
% 27.61/27.77 cnf(c4802,plain,eqangle(X3285,X3286,X3287,X3288,X3285,X3286,X3287,X3288),inference(resolution,[status(thm)],[c4770, c284])).
% 27.61/27.77 cnf(c8503,plain,eqangle(X3636,X3635,X3636,X3635,X3638,X3637,X3638,X3637),inference(resolution,[status(thm)],[c4802, c345])).
% 27.61/27.77 cnf(c9154,plain,~perp(X4899,X4902,X4899,X4902)|perp(X4901,X4900,X4901,X4900),inference(resolution,[status(thm)],[c8503, c162])).
% 27.61/27.77 cnf(c11003,plain,perp(X4903,X4904,X4903,X4904),inference(resolution,[status(thm)],[c9154, c9746])).
% 27.61/27.77 cnf(c11020,plain,perp(X4916,X4915,X4915,X4916),inference(resolution,[status(thm)],[c11003, c389])).
% 27.61/27.77 cnf(c11063,plain,~midp(X5064,X5063,X5063)|cong(X5063,X5064,X5065,X5064),inference(resolution,[status(thm)],[c11020, c239])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.77 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])).
% 27.61/27.77 cnf(c196,plain,~midp(X946,X942,X944)|~para(X942,X943,X944,X945)|~para(X942,X945,X944,X943)|midp(X946,X943,X945),inference(split_conjunct,[status(thm)],[c195])).
% 27.61/27.77 cnf(c1010,plain,~midp(X2180,X2182,X2181)|~para(X2182,X2179,X2181,X2179)|midp(X2180,X2179,X2179),inference(factor,[status(thm)],[c196])).
% 27.61/27.77 cnf(c4795,plain,~midp(X3283,X3282,X3282)|midp(X3283,X3284,X3284),inference(resolution,[status(thm)],[c4770, c1010])).
% 27.61/27.77 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)).
% 27.61/27.77 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])).
% 27.61/27.78 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])).
% 27.61/27.78 cnf(c272,plain,~eqangle(X1070,X1071,X1070,X1068,X1069,X1071,X1069,X1068)|~coll(X1070,X1069,X1068)|cyclic(X1071,X1068,X1070,X1069),inference(split_conjunct,[status(thm)],[c271])).
% 27.61/27.78 cnf(c8498,plain,~coll(X3941,X3941,X3940)|cyclic(X3939,X3940,X3941,X3941),inference(resolution,[status(thm)],[c4802, c272])).
% 27.61/27.78 cnf(c9894,plain,cyclic(X3942,X3944,X3943,X3943),inference(resolution,[status(thm)],[c8498, c8725])).
% 27.61/27.78 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)).
% 27.61/27.78 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])).
% 27.61/27.78 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])).
% 27.61/27.78 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])).])).
% 27.61/27.78 cnf(c269,plain,~cyclic(X1062,X1067,X1066,X1065)|~cyclic(X1062,X1067,X1066,X1064)|~cyclic(X1062,X1067,X1066,X1063)|~eqangle(X1066,X1062,X1066,X1067,X1063,X1065,X1063,X1064)|cong(X1062,X1067,X1065,X1064),inference(split_conjunct,[status(thm)],[c268])).
% 27.61/27.78 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 27.61/27.78 fof(c346,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])).
% 27.61/27.78 fof(c347,plain,(![X434]:(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(~eqangle(X434,X435,X436,X437,X438,X439,X440,X441)|eqangle(X438,X439,X440,X441,X434,X435,X436,X437)))))))))),inference(variable_rename,[status(thm)],[c346])).
% 27.61/27.78 cnf(c348,plain,~eqangle(X1224,X1220,X1221,X1218,X1223,X1225,X1219,X1222)|eqangle(X1223,X1225,X1219,X1222,X1224,X1220,X1221,X1218),inference(split_conjunct,[status(thm)],[c347])).
% 27.61/27.78 cnf(c4805,plain,para(X2450,X2449,X2449,X2450),inference(resolution,[status(thm)],[c4770, c398])).
% 27.61/27.78 cnf(c5450,plain,eqangle(X3571,X3570,X3572,X3573,X3570,X3571,X3572,X3573),inference(resolution,[status(thm)],[c4805, c284])).
% 27.61/27.78 cnf(c8956,plain,eqangle(X3655,X3656,X3656,X3655,X3658,X3657,X3658,X3657),inference(resolution,[status(thm)],[c5450, c345])).
% 27.61/27.78 cnf(c9188,plain,eqangle(X3752,X3750,X3752,X3750,X3749,X3751,X3751,X3749),inference(resolution,[status(thm)],[c8956, c348])).
% 27.61/27.78 cnf(c9366,plain,~cyclic(X5106,X5106,X5105,X5107)|cong(X5106,X5106,X5107,X5107),inference(resolution,[status(thm)],[c9188, c269])).
% 27.61/27.78 cnf(c11534,plain,cong(X5108,X5108,X5109,X5109),inference(resolution,[status(thm)],[c9366, c9894])).
% 27.61/27.78 cnf(c11540,plain,~coll(X5128,X5128,X5128)|midp(X5128,X5128,X5128),inference(resolution,[status(thm)],[c11534, c187])).
% 27.61/27.78 cnf(c11568,plain,midp(X5129,X5129,X5129),inference(resolution,[status(thm)],[c11540, c8725])).
% 27.61/27.78 cnf(c11587,plain,midp(X5130,X5131,X5131),inference(resolution,[status(thm)],[c11568, c4795])).
% 27.61/27.78 cnf(c11623,plain,cong(X5148,X5147,X5149,X5147),inference(resolution,[status(thm)],[c11587, c11063])).
% 27.61/27.78 cnf(c11695,plain,cong(X5171,X5172,X5172,X5173),inference(resolution,[status(thm)],[c11623, c339])).
% 27.61/27.78 cnf(c11799,plain,cong(X5216,X5215,X5214,X5216),inference(resolution,[status(thm)],[c11695, c336])).
% 27.61/27.78 cnf(c11939,plain,cong(X5252,X5253,X5252,X5254),inference(resolution,[status(thm)],[c11799, c339])).
% 27.61/27.78 cnf(c11949,plain,~coll(X6077,X6076,X6075)|midp(X6077,X6076,X6075),inference(resolution,[status(thm)],[c11939, c187])).
% 27.61/27.78 cnf(c13991,plain,midp(X6083,X6081,X6082),inference(resolution,[status(thm)],[c11949, c8725])).
% 27.61/27.78 cnf(c11632,plain,~midp(X10898,X10899,X10897)|para(X10898,X10900,X10897,X10899),inference(resolution,[status(thm)],[c11587, c264])).
% 27.61/27.78 cnf(c18616,plain,para(X10901,X10902,X10903,X10904),inference(resolution,[status(thm)],[c11632, c13991])).
% 27.61/27.78 cnf(c11032,plain,~para(X12878,X12880,X12877,X12879)|perp(X12878,X12880,X12877,X12879),inference(resolution,[status(thm)],[c11003, c380])).
% 27.61/27.78 cnf(c19475,plain,perp(X12882,X12881,X12883,X12884),inference(resolution,[status(thm)],[c11032, c18616])).
% 27.61/27.78 cnf(c19477,plain,$false,inference(resolution,[status(thm)],[c19475, c22])).
% 27.61/27.78 % SZS output end CNFRefutation
% 27.61/27.78
% 27.61/27.78 % Initial clauses : 134
% 27.61/27.78 % Processed clauses : 2167
% 27.61/27.78 % Factors computed : 162
% 27.61/27.78 % Resolvents computed: 18908
% 27.61/27.78 % Tautologies deleted: 22
% 27.61/27.78 % Forward subsumed : 7313
% 27.61/27.78 % Backward subsumed : 1943
% 27.61/27.78 % -------- CPU Time ---------
% 27.61/27.78 % User time : 27.375 s
% 27.61/27.78 % System time : 0.041 s
% 27.61/27.78 % Total time : 27.416 s
%------------------------------------------------------------------------------