%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO647+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:29 EDT 2024
% Result : Theorem 56.23s 56.44s
% Output : Refutation 56.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO647+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n011.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 08:26:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 56.23/56.44 % Version: 1.5
% 56.23/56.44 % SZS status Theorem
% 56.23/56.44 % SZS output start CNFRefutation
% 56.23/56.44 fof(exemplo6GDDFULLmoreE0156,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((midp(D,A,C)&midp(E,B,A))&midp(F,C,B))¶(A,F,G,D))¶(A,C,G,F))=>para(C,E,G,B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE0156)).
% 56.23/56.44 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(((((midp(D,A,C)&midp(E,B,A))&midp(F,C,B))¶(A,F,G,D))¶(A,C,G,F))=>para(C,E,G,B)))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE0156])).
% 56.23/56.44 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(((((midp(D,A,C)&midp(E,B,A))&midp(F,C,B))¶(A,F,G,D))¶(A,C,G,F))&~para(C,E,G,B))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 56.23/56.44 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((midp(X5,X2,X4)&midp(X6,X3,X2))&midp(X7,X4,X3))¶(X2,X7,X8,X5))¶(X2,X4,X8,X7))&~para(X4,X6,X8,X3))))))))),inference(variable_rename,[status(thm)],[c12])).
% 56.23/56.44 fof(c14,negated_conjecture,(((((midp(skolem0004,skolem0001,skolem0003)&midp(skolem0005,skolem0002,skolem0001))&midp(skolem0006,skolem0003,skolem0002))¶(skolem0001,skolem0006,skolem0007,skolem0004))¶(skolem0001,skolem0003,skolem0007,skolem0006))&~para(skolem0003,skolem0005,skolem0007,skolem0002)),inference(skolemize,[status(esa)],[c13])).
% 56.23/56.44 cnf(c20,negated_conjecture,~para(skolem0003,skolem0005,skolem0007,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 56.23/56.44 cnf(c16,negated_conjecture,midp(skolem0005,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 56.23/56.44 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 56.23/56.44 fof(c373,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 56.23/56.44 fof(c374,plain,(![X483]:(![X484]:(![X485]:(~midp(X485,X484,X483)|midp(X485,X483,X484))))),inference(variable_rename,[status(thm)],[c373])).
% 56.23/56.44 cnf(c375,plain,~midp(X557,X558,X559)|midp(X557,X559,X558),inference(split_conjunct,[status(thm)],[c374])).
% 56.23/56.44 cnf(c418,plain,midp(skolem0005,skolem0001,skolem0002),inference(resolution,[status(thm)],[c375, c16])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c262,plain,~midp(X1037,X1038,X1036)|~midp(X1039,X1038,X1040)|para(X1037,X1039,X1036,X1040),inference(split_conjunct,[status(thm)],[c261])).
% 56.23/56.44 cnf(c1391,plain,~midp(X1891,skolem0001,X1890)|para(X1891,skolem0005,X1890,skolem0002),inference(resolution,[status(thm)],[c262, c418])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c399,plain,~coll(X807,X805,X804)|~coll(X807,X805,X806)|coll(X804,X806,X807),inference(split_conjunct,[status(thm)],[c398])).
% 56.23/56.44 cnf(c688,plain,~coll(X808,X809,X810)|coll(X810,X810,X808),inference(factor,[status(thm)],[c399])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c186,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 56.23/56.44 fof(c187,plain,(![X163]:(![X164]:(![X165]:(~para(X163,X164,X163,X165)|coll(X163,X164,X165))))),inference(variable_rename,[status(thm)],[c186])).
% 56.23/56.44 cnf(c188,plain,~para(X677,X676,X677,X675)|coll(X677,X676,X675),inference(split_conjunct,[status(thm)],[c187])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 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])).])).
% 56.23/56.44 cnf(c287,plain,~eqangle(X1068,X1073,X1070,X1072,X1069,X1071,X1070,X1072)|para(X1068,X1073,X1069,X1071),inference(split_conjunct,[status(thm)],[c286])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c349,plain,~eqangle(X1230,X1227,X1224,X1226,X1231,X1229,X1225,X1228)|eqangle(X1224,X1226,X1230,X1227,X1225,X1228,X1231,X1229),inference(split_conjunct,[status(thm)],[c348])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 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])).])).
% 56.23/56.44 cnf(c282,plain,~para(X1064,X1060,X1061,X1059)|eqangle(X1064,X1060,X1062,X1063,X1061,X1059,X1062,X1063),inference(split_conjunct,[status(thm)],[c281])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c394,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 56.23/56.44 fof(c395,plain,(![X516]:(![X517]:(![X518]:(![X519]:(~para(X516,X517,X518,X519)|para(X516,X517,X519,X518)))))),inference(variable_rename,[status(thm)],[c394])).
% 56.23/56.44 cnf(c396,plain,~para(X771,X769,X770,X768)|para(X771,X769,X768,X770),inference(split_conjunct,[status(thm)],[c395])).
% 56.23/56.44 cnf(c15,negated_conjecture,midp(skolem0004,skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 56.23/56.44 cnf(c417,plain,midp(skolem0004,skolem0003,skolem0001),inference(resolution,[status(thm)],[c375, c15])).
% 56.23/56.44 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 56.23/56.44 fof(c195,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])).
% 56.23/56.44 fof(c196,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c195])).
% 56.23/56.44 fof(c198,plain,(![X176]:(![X177]:(![X178]:(![X179]:(![X180]:((~midp(X180,X176,X177)|~midp(X180,X178,X179))|para(X176,X178,X177,X179))))))),inference(shift_quantors,[status(thm)],[fof(c197,plain,(![X176]:(![X177]:(![X178]:(![X179]:((![X180]:(~midp(X180,X176,X177)|~midp(X180,X178,X179)))|para(X176,X178,X177,X179)))))),inference(variable_rename,[status(thm)],[c196])).])).
% 56.23/56.44 cnf(c199,plain,~midp(X950,X947,X948)|~midp(X950,X946,X949)|para(X947,X946,X948,X949),inference(split_conjunct,[status(thm)],[c198])).
% 56.23/56.44 cnf(c1218,plain,~midp(skolem0004,X1823,X1822)|para(X1823,skolem0003,X1822,skolem0001),inference(resolution,[status(thm)],[c199, c417])).
% 56.23/56.44 cnf(c3332,plain,para(skolem0001,skolem0003,skolem0003,skolem0001),inference(resolution,[status(thm)],[c1218, c15])).
% 56.23/56.44 cnf(c3337,plain,para(skolem0001,skolem0003,skolem0001,skolem0003),inference(resolution,[status(thm)],[c3332, c396])).
% 56.23/56.44 cnf(c3364,plain,eqangle(skolem0001,skolem0003,X2686,X2687,skolem0001,skolem0003,X2686,X2687),inference(resolution,[status(thm)],[c3337, c282])).
% 56.23/56.44 cnf(c6200,plain,eqangle(X3120,X3119,skolem0001,skolem0003,X3120,X3119,skolem0001,skolem0003),inference(resolution,[status(thm)],[c3364, c349])).
% 56.23/56.44 cnf(c7356,plain,para(X3121,X3122,X3121,X3122),inference(resolution,[status(thm)],[c6200, c287])).
% 56.23/56.44 cnf(c7374,plain,coll(X3124,X3123,X3123),inference(resolution,[status(thm)],[c7356, c188])).
% 56.23/56.44 cnf(c7517,plain,coll(X3132,X3132,X3131),inference(resolution,[status(thm)],[c7374, c688])).
% 56.23/56.44 cnf(c8041,plain,~coll(X3741,X3741,X3740)|coll(X3740,X3742,X3741),inference(resolution,[status(thm)],[c7517, c399])).
% 56.23/56.44 cnf(c11218,plain,coll(X3745,X3746,X3744),inference(resolution,[status(thm)],[c8041, c7517])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c185,plain,~cong(X933,X934,X933,X935)|~coll(X933,X934,X935)|midp(X933,X934,X935),inference(split_conjunct,[status(thm)],[c184])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c335,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 56.23/56.44 fof(c336,plain,(![X409]:(![X410]:(![X411]:(![X412]:(~cong(X409,X410,X411,X412)|cong(X409,X410,X412,X411)))))),inference(variable_rename,[status(thm)],[c335])).
% 56.23/56.44 cnf(c337,plain,~cong(X685,X686,X688,X687)|cong(X685,X686,X687,X688),inference(split_conjunct,[status(thm)],[c336])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c332,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 56.23/56.44 fof(c333,plain,(![X405]:(![X406]:(![X407]:(![X408]:(~cong(X405,X406,X407,X408)|cong(X407,X408,X405,X406)))))),inference(variable_rename,[status(thm)],[c332])).
% 56.23/56.44 cnf(c334,plain,~cong(X678,X680,X679,X681)|cong(X679,X681,X678,X680),inference(split_conjunct,[status(thm)],[c333])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c237,plain,~perp(X997,X995,X995,X996)|~midp(X998,X997,X996)|cong(X997,X998,X995,X998),inference(split_conjunct,[status(thm)],[c236])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 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])).])).
% 56.23/56.44 cnf(c160,plain,~eqangle(X904,X910,X906,X909,X907,X908,X905,X903)|~perp(X907,X908,X905,X903)|perp(X904,X910,X906,X909),inference(split_conjunct,[status(thm)],[c159])).
% 56.23/56.44 cnf(c7387,plain,para(X3145,X3144,X3144,X3145),inference(resolution,[status(thm)],[c7356, c396])).
% 56.23/56.44 cnf(c8190,plain,eqangle(X3835,X3837,X3836,X3838,X3837,X3835,X3836,X3838),inference(resolution,[status(thm)],[c7387, c282])).
% 56.23/56.44 cnf(c11417,plain,~perp(X6024,X6026,X6023,X6025)|perp(X6026,X6024,X6023,X6025),inference(resolution,[status(thm)],[c8190, c160])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c382,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 56.23/56.44 fof(c383,plain,(![X498]:(![X499]:(![X500]:(![X501]:(~perp(X498,X499,X500,X501)|perp(X500,X501,X498,X499)))))),inference(variable_rename,[status(thm)],[c382])).
% 56.23/56.44 cnf(c384,plain,~perp(X748,X746,X749,X747)|perp(X749,X747,X748,X746),inference(split_conjunct,[status(thm)],[c383])).
% 56.23/56.44 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 56.23/56.44 fof(c180,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 56.23/56.44 fof(c181,plain,(![X157]:(![X158]:(![X159]:(~midp(X157,X158,X159)|cong(X157,X158,X157,X159))))),inference(variable_rename,[status(thm)],[c180])).
% 56.23/56.44 cnf(c182,plain,~midp(X662,X661,X660)|cong(X662,X661,X662,X660),inference(split_conjunct,[status(thm)],[c181])).
% 56.23/56.44 cnf(c488,plain,cong(skolem0005,skolem0002,skolem0005,skolem0001),inference(resolution,[status(thm)],[c182, c16])).
% 56.23/56.44 cnf(c510,plain,cong(skolem0005,skolem0002,skolem0001,skolem0005),inference(resolution,[status(thm)],[c337, c488])).
% 56.23/56.44 cnf(c526,plain,cong(skolem0001,skolem0005,skolem0005,skolem0002),inference(resolution,[status(thm)],[c510, c334])).
% 56.23/56.44 cnf(c546,plain,cong(skolem0001,skolem0005,skolem0002,skolem0005),inference(resolution,[status(thm)],[c526, c337])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c223,plain,~cong(X981,X979,X980,X979)|~cong(X981,X982,X980,X982)|perp(X981,X980,X979,X982),inference(split_conjunct,[status(thm)],[c222])).
% 56.23/56.44 cnf(c1225,plain,~cong(X1035,X1033,X1034,X1033)|perp(X1035,X1034,X1033,X1033),inference(factor,[status(thm)],[c223])).
% 56.23/56.44 cnf(c1351,plain,perp(skolem0001,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c1225, c546])).
% 56.23/56.44 cnf(c1380,plain,perp(skolem0005,skolem0005,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1351, c384])).
% 56.23/56.44 fof(ruleD10,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((para(A,B,C,D)&perp(C,D,E,F))=>perp(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD10)).
% 56.23/56.44 fof(c376,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])).
% 56.23/56.44 fof(c377,plain,(![X486]:(![X487]:(![X488]:(![X489]:(![X490]:(![X491]:((~para(X486,X487,X488,X489)|~perp(X488,X489,X490,X491))|perp(X486,X487,X490,X491)))))))),inference(variable_rename,[status(thm)],[c376])).
% 56.23/56.44 cnf(c378,plain,~para(X1262,X1266,X1265,X1263)|~perp(X1265,X1263,X1267,X1264)|perp(X1262,X1266,X1267,X1264),inference(split_conjunct,[status(thm)],[c377])).
% 56.23/56.44 cnf(c1782,plain,~para(X4194,X4193,skolem0005,skolem0005)|perp(X4194,X4193,skolem0001,skolem0002),inference(resolution,[status(thm)],[c378, c1380])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 56.23/56.44 fof(c392,plain,(![X512]:(![X513]:(![X514]:(![X515]:(~para(X512,X513,X514,X515)|para(X514,X515,X512,X513)))))),inference(variable_rename,[status(thm)],[c391])).
% 56.23/56.44 cnf(c393,plain,~para(X763,X760,X762,X761)|para(X762,X761,X763,X760),inference(split_conjunct,[status(thm)],[c392])).
% 56.23/56.44 cnf(c1386,plain,~midp(X1065,X1067,X1066)|para(X1065,X1065,X1066,X1066),inference(factor,[status(thm)],[c262])).
% 56.23/56.44 cnf(c1483,plain,para(skolem0005,skolem0005,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1386, c418])).
% 56.23/56.44 cnf(c1547,plain,para(skolem0002,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c1483, c393])).
% 56.23/56.44 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD6)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c390,plain,~para(X1276,X1278,X1279,X1274)|~para(X1279,X1274,X1277,X1275)|para(X1276,X1278,X1277,X1275),inference(split_conjunct,[status(thm)],[c389])).
% 56.23/56.44 cnf(c1877,plain,~para(X4755,X4754,skolem0002,skolem0002)|para(X4755,X4754,skolem0005,skolem0005),inference(resolution,[status(thm)],[c390, c1547])).
% 56.23/56.44 cnf(c487,plain,cong(skolem0005,skolem0001,skolem0005,skolem0002),inference(resolution,[status(thm)],[c182, c418])).
% 56.23/56.44 cnf(c506,plain,cong(skolem0005,skolem0001,skolem0002,skolem0005),inference(resolution,[status(thm)],[c337, c487])).
% 56.23/56.44 cnf(c514,plain,cong(skolem0002,skolem0005,skolem0005,skolem0001),inference(resolution,[status(thm)],[c506, c334])).
% 56.23/56.44 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/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 56.23/56.44 fof(c329,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])).
% 56.23/56.44 fof(c330,plain,(![X399]:(![X400]:(![X401]:(![X402]:(![X403]:(![X404]:((~cong(X399,X400,X401,X402)|~cong(X401,X402,X403,X404))|cong(X399,X400,X403,X404)))))))),inference(variable_rename,[status(thm)],[c329])).
% 56.23/56.44 cnf(c331,plain,~cong(X1187,X1185,X1188,X1184)|~cong(X1188,X1184,X1186,X1183)|cong(X1187,X1185,X1186,X1183),inference(split_conjunct,[status(thm)],[c330])).
% 56.23/56.44 cnf(c1690,plain,~cong(X4014,X4015,skolem0005,skolem0001)|cong(X4014,X4015,skolem0002,skolem0005),inference(resolution,[status(thm)],[c331, c506])).
% 56.23/56.44 cnf(c11757,plain,cong(skolem0002,skolem0005,skolem0002,skolem0005),inference(resolution,[status(thm)],[c1690, c514])).
% 56.23/56.44 cnf(c11885,plain,perp(skolem0002,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c11757, c1225])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c379,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])).
% 56.23/56.44 fof(c380,plain,(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:((~perp(X492,X493,X494,X495)|~perp(X494,X495,X496,X497))|para(X492,X493,X496,X497)))))))),inference(variable_rename,[status(thm)],[c379])).
% 56.23/56.44 cnf(c381,plain,~perp(X1271,X1272,X1269,X1273)|~perp(X1269,X1273,X1268,X1270)|para(X1271,X1272,X1268,X1270),inference(split_conjunct,[status(thm)],[c380])).
% 56.23/56.44 cnf(c1814,plain,~perp(X4393,X4392,skolem0005,skolem0005)|para(X4393,X4392,skolem0001,skolem0002),inference(resolution,[status(thm)],[c381, c1380])).
% 56.23/56.44 cnf(c12735,plain,para(skolem0002,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1814, c11885])).
% 56.23/56.44 cnf(c13196,plain,para(skolem0001,skolem0002,skolem0002,skolem0002),inference(resolution,[status(thm)],[c12735, c393])).
% 56.23/56.44 cnf(c13603,plain,para(skolem0001,skolem0002,skolem0005,skolem0005),inference(resolution,[status(thm)],[c13196, c1877])).
% 56.23/56.44 cnf(c14077,plain,perp(skolem0001,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c13603, c1782])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c343,plain,~eqangle(X1211,X1209,X1207,X1205,X1208,X1206,X1210,X1212)|eqangle(X1211,X1209,X1208,X1206,X1207,X1205,X1210,X1212),inference(split_conjunct,[status(thm)],[c342])).
% 56.23/56.44 cnf(c7420,plain,eqangle(X3603,X3601,X3602,X3604,X3603,X3601,X3602,X3604),inference(resolution,[status(thm)],[c7356, c282])).
% 56.23/56.44 cnf(c11044,plain,eqangle(X3852,X3851,X3852,X3851,X3850,X3853,X3850,X3853),inference(resolution,[status(thm)],[c7420, c343])).
% 56.23/56.44 cnf(c11431,plain,~perp(X6102,X6105,X6102,X6105)|perp(X6104,X6103,X6104,X6103),inference(resolution,[status(thm)],[c11044, c160])).
% 56.23/56.44 cnf(c18784,plain,perp(X6107,X6108,X6107,X6108),inference(resolution,[status(thm)],[c11431, c14077])).
% 56.23/56.44 cnf(c18817,plain,perp(X6126,X6127,X6127,X6126),inference(resolution,[status(thm)],[c18784, c11417])).
% 56.23/56.44 cnf(c18834,plain,~midp(X6273,X6272,X6272)|cong(X6272,X6273,X6271,X6273),inference(resolution,[status(thm)],[c18817, c237])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c194,plain,~midp(X941,X942,X945)|~para(X942,X943,X945,X944)|~para(X942,X944,X945,X943)|midp(X941,X943,X944),inference(split_conjunct,[status(thm)],[c193])).
% 56.23/56.44 cnf(c1200,plain,~midp(X2657,X2658,X2656)|~para(X2658,X2655,X2656,X2655)|midp(X2657,X2655,X2655),inference(factor,[status(thm)],[c194])).
% 56.23/56.44 cnf(c7410,plain,~midp(X3599,X3600,X3600)|midp(X3599,X3598,X3598),inference(resolution,[status(thm)],[c7356, c1200])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c356,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 56.23/56.44 fof(c357,plain,(![X462]:(![X463]:(![X464]:(![X465]:(~cyclic(X462,X463,X464,X465)|cyclic(X463,X462,X464,X465)))))),inference(variable_rename,[status(thm)],[c356])).
% 56.23/56.44 cnf(c358,plain,~cyclic(X734,X735,X736,X737)|cyclic(X735,X734,X736,X737),inference(split_conjunct,[status(thm)],[c357])).
% 56.23/56.44 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)).
% 56.23/56.44 fof(c359,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 56.23/56.44 fof(c360,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X466,X468,X467,X469)))))),inference(variable_rename,[status(thm)],[c359])).
% 56.23/56.44 cnf(c361,plain,~cyclic(X738,X739,X740,X741)|cyclic(X738,X740,X739,X741),inference(split_conjunct,[status(thm)],[c360])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 cnf(c270,plain,~eqangle(X1050,X1047,X1050,X1049,X1048,X1047,X1048,X1049)|~coll(X1050,X1048,X1049)|cyclic(X1047,X1049,X1050,X1048),inference(split_conjunct,[status(thm)],[c269])).
% 56.23/56.44 cnf(c11035,plain,~coll(X4089,X4089,X4087)|cyclic(X4088,X4087,X4089,X4089),inference(resolution,[status(thm)],[c7420, c270])).
% 56.23/56.44 cnf(c12072,plain,cyclic(X4095,X4094,X4093,X4093),inference(resolution,[status(thm)],[c11035, c11218])).
% 56.23/56.44 cnf(c12088,plain,cyclic(X4096,X4097,X4098,X4097),inference(resolution,[status(thm)],[c12072, c361])).
% 56.23/56.44 cnf(c12122,plain,cyclic(X4112,X4114,X4113,X4112),inference(resolution,[status(thm)],[c12088, c358])).
% 56.23/56.44 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)).
% 56.23/56.44 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])).
% 56.23/56.44 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])).
% 56.23/56.44 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])).])).
% 56.23/56.44 cnf(c267,plain,~cyclic(X1043,X1044,X1042,X1046)|~cyclic(X1043,X1044,X1042,X1041)|~cyclic(X1043,X1044,X1042,X1045)|~eqangle(X1042,X1043,X1042,X1044,X1045,X1046,X1045,X1041)|cong(X1043,X1044,X1046,X1041),inference(split_conjunct,[status(thm)],[c266])).
% 56.23/56.44 cnf(c11412,plain,eqangle(X3864,X3861,X3862,X3863,X3864,X3861,X3863,X3862),inference(resolution,[status(thm)],[c8190, c349])).
% 56.23/56.44 cnf(c11450,plain,eqangle(X3912,X3911,X3912,X3911,X3913,X3910,X3910,X3913),inference(resolution,[status(thm)],[c11412, c343])).
% 56.23/56.44 cnf(c11488,plain,~cyclic(X6418,X6418,X6419,X6417)|cong(X6418,X6418,X6417,X6417),inference(resolution,[status(thm)],[c11450, c267])).
% 56.23/56.44 cnf(c19690,plain,cong(X6420,X6420,X6420,X6420),inference(resolution,[status(thm)],[c11488, c12122])).
% 56.23/56.44 cnf(c19720,plain,~coll(X6448,X6448,X6448)|midp(X6448,X6448,X6448),inference(resolution,[status(thm)],[c19690, c185])).
% 56.23/56.44 cnf(c19753,plain,midp(X6451,X6451,X6451),inference(resolution,[status(thm)],[c19720, c11218])).
% 56.23/56.44 cnf(c19812,plain,midp(X6453,X6454,X6454),inference(resolution,[status(thm)],[c19753, c7410])).
% 56.23/56.44 cnf(c19842,plain,cong(X6475,X6473,X6474,X6473),inference(resolution,[status(thm)],[c19812, c18834])).
% 56.23/56.44 cnf(c20021,plain,cong(X6505,X6503,X6503,X6504),inference(resolution,[status(thm)],[c19842, c337])).
% 56.23/56.44 cnf(c20288,plain,cong(X6574,X6575,X6573,X6574),inference(resolution,[status(thm)],[c20021, c334])).
% 56.23/56.44 cnf(c20415,plain,cong(X6605,X6606,X6605,X6607),inference(resolution,[status(thm)],[c20288, c337])).
% 56.23/56.44 cnf(c20495,plain,~coll(X9946,X9947,X9948)|midp(X9946,X9947,X9948),inference(resolution,[status(thm)],[c20415, c185])).
% 56.23/56.44 cnf(c28649,plain,midp(X9951,X9952,X9953),inference(resolution,[status(thm)],[c20495, c11218])).
% 56.23/56.44 cnf(c28693,plain,para(X9982,skolem0005,X9983,skolem0002),inference(resolution,[status(thm)],[c28649, c1391])).
% 56.23/56.44 cnf(c28857,plain,$false,inference(resolution,[status(thm)],[c28693, c20])).
% 56.23/56.44 % SZS output end CNFRefutation
% 56.23/56.44
% 56.23/56.44 % Initial clauses : 133
% 56.23/56.44 % Processed clauses : 3137
% 56.23/56.44 % Factors computed : 156
% 56.23/56.44 % Resolvents computed: 28310
% 56.23/56.44 % Tautologies deleted: 42
% 56.23/56.44 % Forward subsumed : 9094
% 56.23/56.44 % Backward subsumed : 1982
% 56.23/56.44 % -------- CPU Time ---------
% 56.23/56.44 % User time : 56.003 s
% 56.23/56.44 % System time : 0.066 s
% 56.23/56.44 % Total time : 56.069 s
%------------------------------------------------------------------------------