%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO590+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:21 EDT 2024
% Result : Theorem 23.43s 23.65s
% Output : Refutation 23.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO590+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 07:43:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 23.43/23.65 % Version: 1.5
% 23.43/23.65 % SZS status Theorem
% 23.43/23.65 % SZS output start CNFRefutation
% 23.43/23.65 fof(exemplo6GDDFULL416052,conjecture,(![C]:(![D]:(![E]:(![O]:(![A]:(![F]:((((((perp(E,C,E,D)&midp(O,D,C))&perp(C,D,C,A))&perp(E,O,E,A))&coll(F,C,A))&coll(F,D,E))=>cong(A,E,A,F)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL416052)).
% 23.43/23.65 fof(c11,negated_conjecture,(~(![C]:(![D]:(![E]:(![O]:(![A]:(![F]:((((((perp(E,C,E,D)&midp(O,D,C))&perp(C,D,C,A))&perp(E,O,E,A))&coll(F,C,A))&coll(F,D,E))=>cong(A,E,A,F))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416052])).
% 23.43/23.65 fof(c12,negated_conjecture,(?[C]:(?[D]:(?[E]:(?[O]:(?[A]:(?[F]:((((((perp(E,C,E,D)&midp(O,D,C))&perp(C,D,C,A))&perp(E,O,E,A))&coll(F,C,A))&coll(F,D,E))&~cong(A,E,A,F)))))))),inference(fof_nnf,[status(thm)],[c11])).
% 23.43/23.65 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:((((((perp(X4,X2,X4,X3)&midp(X5,X3,X2))&perp(X2,X3,X2,X6))&perp(X4,X5,X4,X6))&coll(X7,X2,X6))&coll(X7,X3,X4))&~cong(X6,X4,X6,X7)))))))),inference(variable_rename,[status(thm)],[c12])).
% 23.43/23.65 fof(c14,negated_conjecture,((((((perp(skolem0003,skolem0001,skolem0003,skolem0002)&midp(skolem0004,skolem0002,skolem0001))&perp(skolem0001,skolem0002,skolem0001,skolem0005))&perp(skolem0003,skolem0004,skolem0003,skolem0005))&coll(skolem0006,skolem0001,skolem0005))&coll(skolem0006,skolem0002,skolem0003))&~cong(skolem0005,skolem0003,skolem0005,skolem0006)),inference(skolemize,[status(esa)],[c13])).
% 23.43/23.65 cnf(c21,negated_conjecture,~cong(skolem0005,skolem0003,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c14])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 23.43/23.65 fof(c337,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X408,X409,X411,X410)))))),inference(variable_rename,[status(thm)],[c336])).
% 23.43/23.65 cnf(c338,plain,~cong(X670,X671,X672,X669)|cong(X670,X671,X669,X672),inference(split_conjunct,[status(thm)],[c337])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c333,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 23.43/23.65 fof(c334,plain,(![X404]:(![X405]:(![X406]:(![X407]:(~cong(X404,X405,X406,X407)|cong(X406,X407,X404,X405)))))),inference(variable_rename,[status(thm)],[c333])).
% 23.43/23.65 cnf(c335,plain,~cong(X665,X667,X668,X666)|cong(X668,X666,X665,X667),inference(split_conjunct,[status(thm)],[c334])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c236,plain,(![A]:(![B]:(![C]:(![M]:((~perp(A,B,B,C)|~midp(M,A,C))|cong(A,M,B,M)))))),inference(fof_nnf,[status(thm)],[ruleD52])).
% 23.43/23.65 fof(c237,plain,(![X230]:(![X231]:(![X232]:(![X233]:((~perp(X230,X231,X231,X232)|~midp(X233,X230,X232))|cong(X230,X233,X231,X233)))))),inference(variable_rename,[status(thm)],[c236])).
% 23.43/23.65 cnf(c238,plain,~perp(X1001,X1003,X1003,X1000)|~midp(X1002,X1001,X1000)|cong(X1001,X1002,X1003,X1002),inference(split_conjunct,[status(thm)],[c237])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c157,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:((~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))|perp(A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD74])).
% 23.43/23.65 fof(c158,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|~perp(P,Q,U,V))))))|perp(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c157])).
% 23.43/23.65 fof(c160,plain,(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(![X129]:(![X130]:((~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))|perp(X123,X124,X125,X126)))))))))),inference(shift_quantors,[status(thm)],[fof(c159,plain,(![X123]:(![X124]:(![X125]:(![X126]:((![X127]:(![X128]:(![X129]:(![X130]:(~eqangle(X123,X124,X125,X126,X127,X128,X129,X130)|~perp(X127,X128,X129,X130))))))|perp(X123,X124,X125,X126)))))),inference(variable_rename,[status(thm)],[c158])).])).
% 23.43/23.65 cnf(c161,plain,~eqangle(X902,X906,X907,X909,X904,X908,X903,X905)|~perp(X904,X908,X903,X905)|perp(X902,X906,X907,X909),inference(split_conjunct,[status(thm)],[c160])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c279,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~para(A,B,C,D)|eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD40])).
% 23.43/23.65 fof(c280,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|(![P]:(![Q]:eqangle(A,B,P,Q,C,D,P,Q)))))))),inference(shift_quantors,[status(thm)],[c279])).
% 23.43/23.65 fof(c282,plain,(![X288]:(![X289]:(![X290]:(![X291]:(![X292]:(![X293]:(~para(X288,X289,X290,X291)|eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(shift_quantors,[status(thm)],[fof(c281,plain,(![X288]:(![X289]:(![X290]:(![X291]:(~para(X288,X289,X290,X291)|(![X292]:(![X293]:eqangle(X288,X289,X292,X293,X290,X291,X292,X293)))))))),inference(variable_rename,[status(thm)],[c280])).])).
% 23.43/23.65 cnf(c283,plain,~para(X1077,X1078,X1073,X1074)|eqangle(X1077,X1078,X1075,X1076,X1073,X1074,X1075,X1076),inference(split_conjunct,[status(thm)],[c282])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 23.43/23.65 fof(c396,plain,(![X515]:(![X516]:(![X517]:(![X518]:(~para(X515,X516,X517,X518)|para(X515,X516,X518,X517)))))),inference(variable_rename,[status(thm)],[c395])).
% 23.43/23.65 cnf(c397,plain,~para(X768,X770,X767,X769)|para(X768,X770,X769,X767),inference(split_conjunct,[status(thm)],[c396])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c284,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(~eqangle(A,B,P,Q,C,D,P,Q)|para(A,B,C,D)))))))),inference(fof_nnf,[status(thm)],[ruleD39])).
% 23.43/23.65 fof(c285,plain,(![A]:(![B]:(![C]:(![D]:((![P]:(![Q]:~eqangle(A,B,P,Q,C,D,P,Q)))|para(A,B,C,D)))))),inference(shift_quantors,[status(thm)],[c284])).
% 23.43/23.65 fof(c287,plain,(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)|para(X294,X295,X296,X297)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X294]:(![X295]:(![X296]:(![X297]:((![X298]:(![X299]:~eqangle(X294,X295,X298,X299,X296,X297,X298,X299)))|para(X294,X295,X296,X297)))))),inference(variable_rename,[status(thm)],[c285])).])).
% 23.43/23.65 cnf(c288,plain,~eqangle(X1084,X1082,X1081,X1080,X1085,X1083,X1081,X1080)|para(X1084,X1082,X1085,X1083),inference(split_conjunct,[status(thm)],[c287])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c348,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(C,D,A,B,U,V,P,Q)))))))))),inference(fof_nnf,[status(thm)],[ruleD19])).
% 23.43/23.65 fof(c349,plain,(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(~eqangle(X440,X441,X442,X443,X444,X445,X446,X447)|eqangle(X442,X443,X440,X441,X446,X447,X444,X445)))))))))),inference(variable_rename,[status(thm)],[c348])).
% 23.43/23.65 cnf(c350,plain,~eqangle(X1228,X1229,X1234,X1231,X1233,X1227,X1232,X1230)|eqangle(X1234,X1231,X1228,X1229,X1232,X1230,X1233,X1227),inference(split_conjunct,[status(thm)],[c349])).
% 23.43/23.65 cnf(c16,negated_conjecture,midp(skolem0004,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 23.43/23.65 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 23.43/23.65 fof(c374,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 23.43/23.65 fof(c375,plain,(![X482]:(![X483]:(![X484]:(~midp(X484,X483,X482)|midp(X484,X482,X483))))),inference(variable_rename,[status(thm)],[c374])).
% 23.43/23.65 cnf(c376,plain,~midp(X549,X550,X548)|midp(X549,X548,X550),inference(split_conjunct,[status(thm)],[c375])).
% 23.43/23.65 cnf(c414,plain,midp(skolem0004,skolem0001,skolem0002),inference(resolution,[status(thm)],[c376, c16])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c196,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])).
% 23.43/23.65 fof(c197,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c196])).
% 23.43/23.65 fof(c199,plain,(![X175]:(![X176]:(![X177]:(![X178]:(![X179]:((~midp(X179,X175,X176)|~midp(X179,X177,X178))|para(X175,X177,X176,X178))))))),inference(shift_quantors,[status(thm)],[fof(c198,plain,(![X175]:(![X176]:(![X177]:(![X178]:((![X179]:(~midp(X179,X175,X176)|~midp(X179,X177,X178)))|para(X175,X177,X176,X178)))))),inference(variable_rename,[status(thm)],[c197])).])).
% 23.43/23.65 cnf(c200,plain,~midp(X947,X946,X945)|~midp(X947,X949,X948)|para(X946,X949,X945,X948),inference(split_conjunct,[status(thm)],[c199])).
% 23.43/23.65 cnf(c1167,plain,~midp(skolem0004,X1644,X1643)|para(X1644,skolem0001,X1643,skolem0002),inference(resolution,[status(thm)],[c200, c414])).
% 23.43/23.65 cnf(c3215,plain,para(skolem0002,skolem0001,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1167, c16])).
% 23.43/23.65 cnf(c3221,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c3215, c397])).
% 23.43/23.65 cnf(c3249,plain,eqangle(skolem0002,skolem0001,X2301,X2300,skolem0002,skolem0001,X2301,X2300),inference(resolution,[status(thm)],[c3221, c283])).
% 23.43/23.65 cnf(c5144,plain,eqangle(X2437,X2436,skolem0002,skolem0001,X2437,X2436,skolem0002,skolem0001),inference(resolution,[status(thm)],[c3249, c350])).
% 23.43/23.65 cnf(c6063,plain,para(X2439,X2438,X2439,X2438),inference(resolution,[status(thm)],[c5144, c288])).
% 23.43/23.65 cnf(c6078,plain,para(X2457,X2456,X2456,X2457),inference(resolution,[status(thm)],[c6063, c397])).
% 23.43/23.65 cnf(c6730,plain,eqangle(X3365,X3366,X3367,X3364,X3366,X3365,X3367,X3364),inference(resolution,[status(thm)],[c6078, c283])).
% 23.43/23.65 cnf(c10202,plain,~perp(X4952,X4953,X4955,X4954)|perp(X4953,X4952,X4955,X4954),inference(resolution,[status(thm)],[c6730, c161])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c383,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 23.43/23.65 fof(c384,plain,(![X497]:(![X498]:(![X499]:(![X500]:(~perp(X497,X498,X499,X500)|perp(X499,X500,X497,X498)))))),inference(variable_rename,[status(thm)],[c383])).
% 23.43/23.65 cnf(c385,plain,~perp(X704,X705,X706,X703)|perp(X706,X703,X704,X705),inference(split_conjunct,[status(thm)],[c384])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c181,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 23.43/23.65 fof(c182,plain,(![X156]:(![X157]:(![X158]:(~midp(X156,X157,X158)|cong(X156,X157,X156,X158))))),inference(variable_rename,[status(thm)],[c181])).
% 23.43/23.65 cnf(c183,plain,~midp(X648,X647,X649)|cong(X648,X647,X648,X649),inference(split_conjunct,[status(thm)],[c182])).
% 23.43/23.65 cnf(c473,plain,cong(skolem0004,skolem0001,skolem0004,skolem0002),inference(resolution,[status(thm)],[c183, c414])).
% 23.43/23.65 cnf(c480,plain,cong(skolem0004,skolem0001,skolem0002,skolem0004),inference(resolution,[status(thm)],[c338, c473])).
% 23.43/23.65 cnf(c484,plain,cong(skolem0002,skolem0004,skolem0004,skolem0001),inference(resolution,[status(thm)],[c480, c335])).
% 23.43/23.65 cnf(c491,plain,cong(skolem0002,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c484, c338])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c222,plain,(![A]:(![B]:(![P]:(![Q]:((~cong(A,P,B,P)|~cong(A,Q,B,Q))|perp(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD56])).
% 23.43/23.65 fof(c223,plain,(![X214]:(![X215]:(![X216]:(![X217]:((~cong(X214,X216,X215,X216)|~cong(X214,X217,X215,X217))|perp(X214,X215,X216,X217)))))),inference(variable_rename,[status(thm)],[c222])).
% 23.43/23.65 cnf(c224,plain,~cong(X981,X978,X979,X978)|~cong(X981,X980,X979,X980)|perp(X981,X979,X978,X980),inference(split_conjunct,[status(thm)],[c223])).
% 23.43/23.65 cnf(c1170,plain,~cong(X998,X997,X999,X997)|perp(X998,X999,X997,X997),inference(factor,[status(thm)],[c224])).
% 23.43/23.65 cnf(c1222,plain,perp(skolem0002,skolem0001,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1170, c491])).
% 23.43/23.65 cnf(c1235,plain,perp(skolem0004,skolem0004,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1222, c385])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c377,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])).
% 23.43/23.65 fof(c378,plain,(![X485]:(![X486]:(![X487]:(![X488]:(![X489]:(![X490]:((~para(X485,X486,X487,X488)|~perp(X487,X488,X489,X490))|perp(X485,X486,X489,X490)))))))),inference(variable_rename,[status(thm)],[c377])).
% 23.43/23.65 cnf(c379,plain,~para(X1257,X1258,X1262,X1259)|~perp(X1262,X1259,X1261,X1260)|perp(X1257,X1258,X1261,X1260),inference(split_conjunct,[status(thm)],[c378])).
% 23.43/23.65 cnf(c1704,plain,~para(X3372,X3373,skolem0004,skolem0004)|perp(X3372,X3373,skolem0002,skolem0001),inference(resolution,[status(thm)],[c379, c1235])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c392,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 23.43/23.65 fof(c393,plain,(![X511]:(![X512]:(![X513]:(![X514]:(~para(X511,X512,X513,X514)|para(X513,X514,X511,X512)))))),inference(variable_rename,[status(thm)],[c392])).
% 23.43/23.65 cnf(c394,plain,~para(X765,X763,X766,X764)|para(X766,X764,X765,X763),inference(split_conjunct,[status(thm)],[c393])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c261,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])).
% 23.43/23.65 fof(c262,plain,(![X265]:(![X266]:(![X267]:(![X268]:(![X269]:((~midp(X268,X265,X266)|~midp(X269,X265,X267))|para(X268,X269,X266,X267))))))),inference(variable_rename,[status(thm)],[c261])).
% 23.43/23.65 cnf(c263,plain,~midp(X1044,X1046,X1047)|~midp(X1048,X1046,X1045)|para(X1044,X1048,X1047,X1045),inference(split_conjunct,[status(thm)],[c262])).
% 23.43/23.65 cnf(c1298,plain,~midp(X1049,X1050,X1051)|para(X1049,X1049,X1051,X1051),inference(factor,[status(thm)],[c263])).
% 23.43/23.65 cnf(c1302,plain,para(skolem0004,skolem0004,skolem0001,skolem0001),inference(resolution,[status(thm)],[c1298, c16])).
% 23.43/23.65 cnf(c1323,plain,para(skolem0001,skolem0001,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1302, c394])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c389,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])).
% 23.43/23.65 fof(c390,plain,(![X505]:(![X506]:(![X507]:(![X508]:(![X509]:(![X510]:((~para(X505,X506,X507,X508)|~para(X507,X508,X509,X510))|para(X505,X506,X509,X510)))))))),inference(variable_rename,[status(thm)],[c389])).
% 23.43/23.65 cnf(c391,plain,~para(X1273,X1274,X1272,X1270)|~para(X1272,X1270,X1271,X1269)|para(X1273,X1274,X1271,X1269),inference(split_conjunct,[status(thm)],[c390])).
% 23.43/23.65 cnf(c1761,plain,~para(X3550,X3551,skolem0001,skolem0001)|para(X3550,X3551,skolem0004,skolem0004),inference(resolution,[status(thm)],[c391, c1323])).
% 23.43/23.65 cnf(c474,plain,cong(skolem0004,skolem0002,skolem0004,skolem0001),inference(resolution,[status(thm)],[c183, c16])).
% 23.43/23.65 cnf(c479,plain,cong(skolem0004,skolem0002,skolem0001,skolem0004),inference(resolution,[status(thm)],[c338, c474])).
% 23.43/23.65 cnf(c481,plain,cong(skolem0001,skolem0004,skolem0004,skolem0002),inference(resolution,[status(thm)],[c479, c335])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c330,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])).
% 23.43/23.65 fof(c331,plain,(![X398]:(![X399]:(![X400]:(![X401]:(![X402]:(![X403]:((~cong(X398,X399,X400,X401)|~cong(X400,X401,X402,X403))|cong(X398,X399,X402,X403)))))))),inference(variable_rename,[status(thm)],[c330])).
% 23.43/23.65 cnf(c332,plain,~cong(X1194,X1197,X1198,X1196)|~cong(X1198,X1196,X1193,X1195)|cong(X1194,X1197,X1193,X1195),inference(split_conjunct,[status(thm)],[c331])).
% 23.43/23.65 cnf(c1536,plain,~cong(X2962,X2961,skolem0004,skolem0002)|cong(X2962,X2961,skolem0001,skolem0004),inference(resolution,[status(thm)],[c332, c479])).
% 23.43/23.65 cnf(c9526,plain,cong(skolem0001,skolem0004,skolem0001,skolem0004),inference(resolution,[status(thm)],[c1536, c481])).
% 23.43/23.65 cnf(c10300,plain,perp(skolem0001,skolem0001,skolem0004,skolem0004),inference(resolution,[status(thm)],[c9526, c1170])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c380,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~perp(A,B,C,D)|~perp(C,D,E,F))|para(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD9])).
% 23.43/23.65 fof(c381,plain,(![X491]:(![X492]:(![X493]:(![X494]:(![X495]:(![X496]:((~perp(X491,X492,X493,X494)|~perp(X493,X494,X495,X496))|para(X491,X492,X495,X496)))))))),inference(variable_rename,[status(thm)],[c380])).
% 23.43/23.65 cnf(c382,plain,~perp(X1268,X1265,X1267,X1263)|~perp(X1267,X1263,X1266,X1264)|para(X1268,X1265,X1266,X1264),inference(split_conjunct,[status(thm)],[c381])).
% 23.43/23.65 cnf(c1739,plain,~perp(X3489,X3490,skolem0004,skolem0004)|para(X3489,X3490,skolem0002,skolem0001),inference(resolution,[status(thm)],[c382, c1235])).
% 23.43/23.65 cnf(c10624,plain,para(skolem0001,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1739, c10300])).
% 23.43/23.65 cnf(c10963,plain,para(skolem0002,skolem0001,skolem0001,skolem0001),inference(resolution,[status(thm)],[c10624, c394])).
% 23.43/23.65 cnf(c11406,plain,para(skolem0002,skolem0001,skolem0004,skolem0004),inference(resolution,[status(thm)],[c10963, c1761])).
% 23.43/23.65 cnf(c11838,plain,perp(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c11406, c1704])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c342,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(A,B,P,Q,C,D,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD21])).
% 23.43/23.65 fof(c343,plain,(![X424]:(![X425]:(![X426]:(![X427]:(![X428]:(![X429]:(![X430]:(![X431]:(~eqangle(X424,X425,X426,X427,X428,X429,X430,X431)|eqangle(X424,X425,X428,X429,X426,X427,X430,X431)))))))))),inference(variable_rename,[status(thm)],[c342])).
% 23.43/23.65 cnf(c344,plain,~eqangle(X1215,X1212,X1218,X1213,X1211,X1216,X1217,X1214)|eqangle(X1215,X1212,X1211,X1216,X1218,X1213,X1217,X1214),inference(split_conjunct,[status(thm)],[c343])).
% 23.43/23.65 cnf(c6087,plain,eqangle(X3113,X3112,X3114,X3111,X3113,X3112,X3114,X3111),inference(resolution,[status(thm)],[c6063, c283])).
% 23.43/23.65 cnf(c9804,plain,eqangle(X3394,X3391,X3394,X3391,X3392,X3393,X3392,X3393),inference(resolution,[status(thm)],[c6087, c344])).
% 23.43/23.65 cnf(c10352,plain,~perp(X4979,X4980,X4979,X4980)|perp(X4981,X4982,X4981,X4982),inference(resolution,[status(thm)],[c9804, c161])).
% 23.43/23.65 cnf(c15021,plain,perp(X4984,X4983,X4984,X4983),inference(resolution,[status(thm)],[c10352, c11838])).
% 23.43/23.65 cnf(c15028,plain,perp(X4994,X4993,X4993,X4994),inference(resolution,[status(thm)],[c15021, c10202])).
% 23.43/23.65 cnf(c15132,plain,~midp(X5122,X5123,X5123)|cong(X5123,X5122,X5121,X5122),inference(resolution,[status(thm)],[c15028, c238])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c193,plain,(![A]:(![B]:(![C]:(![D]:(![M]:(((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C))|midp(M,C,D))))))),inference(fof_nnf,[status(thm)],[ruleD64])).
% 23.43/23.65 fof(c194,plain,(![X170]:(![X171]:(![X172]:(![X173]:(![X174]:(((~midp(X174,X170,X171)|~para(X170,X172,X171,X173))|~para(X170,X173,X171,X172))|midp(X174,X172,X173))))))),inference(variable_rename,[status(thm)],[c193])).
% 23.43/23.65 cnf(c195,plain,~midp(X940,X943,X944)|~para(X943,X942,X944,X941)|~para(X943,X941,X944,X942)|midp(X940,X942,X941),inference(split_conjunct,[status(thm)],[c194])).
% 23.43/23.65 cnf(c1165,plain,~midp(X2418,X2419,X2421)|~para(X2419,X2420,X2421,X2420)|midp(X2418,X2420,X2420),inference(factor,[status(thm)],[c195])).
% 23.43/23.65 cnf(c6076,plain,~midp(X3105,X3107,X3107)|midp(X3105,X3106,X3106),inference(resolution,[status(thm)],[c6063, c1165])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 23.43/23.65 fof(c399,plain,(![X519]:(![X520]:(![X521]:(![X522]:((~coll(X519,X520,X521)|~coll(X519,X520,X522))|coll(X521,X522,X519)))))),inference(variable_rename,[status(thm)],[c398])).
% 23.43/23.65 cnf(c400,plain,~coll(X779,X777,X780)|~coll(X779,X777,X778)|coll(X780,X778,X779),inference(split_conjunct,[status(thm)],[c399])).
% 23.43/23.65 cnf(c611,plain,~coll(X787,X786,X785)|coll(X785,X785,X787),inference(factor,[status(thm)],[c400])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c187,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 23.43/23.65 fof(c188,plain,(![X162]:(![X163]:(![X164]:(~para(X162,X163,X162,X164)|coll(X162,X163,X164))))),inference(variable_rename,[status(thm)],[c187])).
% 23.43/23.65 cnf(c189,plain,~para(X650,X651,X650,X652)|coll(X650,X651,X652),inference(split_conjunct,[status(thm)],[c188])).
% 23.43/23.65 cnf(c6072,plain,coll(X2440,X2441,X2441),inference(resolution,[status(thm)],[c6063, c189])).
% 23.43/23.65 cnf(c6198,plain,coll(X2444,X2444,X2445),inference(resolution,[status(thm)],[c6072, c611])).
% 23.43/23.65 cnf(c6417,plain,~coll(X3264,X3264,X3265)|coll(X3265,X3263,X3264),inference(resolution,[status(thm)],[c6198, c400])).
% 23.43/23.65 cnf(c9987,plain,coll(X3268,X3269,X3270),inference(resolution,[status(thm)],[c6417, c6198])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c184,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 23.43/23.65 fof(c185,plain,(![X159]:(![X160]:(![X161]:((~cong(X159,X160,X159,X161)|~coll(X159,X160,X161))|midp(X159,X160,X161))))),inference(variable_rename,[status(thm)],[c184])).
% 23.43/23.65 cnf(c186,plain,~cong(X932,X934,X932,X933)|~coll(X932,X934,X933)|midp(X932,X934,X933),inference(split_conjunct,[status(thm)],[c185])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 23.43/23.65 fof(c361,plain,(![X465]:(![X466]:(![X467]:(![X468]:(~cyclic(X465,X466,X467,X468)|cyclic(X465,X467,X466,X468)))))),inference(variable_rename,[status(thm)],[c360])).
% 23.43/23.65 cnf(c362,plain,~cyclic(X693,X695,X694,X692)|cyclic(X693,X694,X695,X692),inference(split_conjunct,[status(thm)],[c361])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 23.43/23.65 fof(c364,plain,(![X469]:(![X470]:(![X471]:(![X472]:(~cyclic(X469,X470,X471,X472)|cyclic(X469,X470,X472,X471)))))),inference(variable_rename,[status(thm)],[c363])).
% 23.43/23.65 cnf(c365,plain,~cyclic(X699,X701,X700,X702)|cyclic(X699,X701,X702,X700),inference(split_conjunct,[status(thm)],[c364])).
% 23.43/23.65 fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 23.43/23.65 fof(c357,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 23.43/23.65 fof(c358,plain,(![X461]:(![X462]:(![X463]:(![X464]:(~cyclic(X461,X462,X463,X464)|cyclic(X462,X461,X463,X464)))))),inference(variable_rename,[status(thm)],[c357])).
% 23.43/23.65 cnf(c359,plain,~cyclic(X688,X690,X689,X691)|cyclic(X690,X688,X689,X691),inference(split_conjunct,[status(thm)],[c358])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c269,plain,(![A]:(![B]:(![P]:(![Q]:((~eqangle(P,A,P,B,Q,A,Q,B)|~coll(P,Q,B))|cyclic(A,B,P,Q)))))),inference(fof_nnf,[status(thm)],[ruleD42b])).
% 23.43/23.65 fof(c270,plain,(![X276]:(![X277]:(![X278]:(![X279]:((~eqangle(X278,X276,X278,X277,X279,X276,X279,X277)|~coll(X278,X279,X277))|cyclic(X276,X277,X278,X279)))))),inference(variable_rename,[status(thm)],[c269])).
% 23.43/23.65 cnf(c271,plain,~eqangle(X1060,X1061,X1060,X1058,X1059,X1061,X1059,X1058)|~coll(X1060,X1059,X1058)|cyclic(X1061,X1058,X1060,X1059),inference(split_conjunct,[status(thm)],[c270])).
% 23.43/23.65 cnf(c9803,plain,~coll(X4142,X4142,X4143)|cyclic(X4144,X4143,X4142,X4142),inference(resolution,[status(thm)],[c6087, c271])).
% 23.43/23.65 cnf(c12989,plain,cyclic(X4145,X4146,X4147,X4147),inference(resolution,[status(thm)],[c9803, c9987])).
% 23.43/23.65 cnf(c12990,plain,cyclic(X4149,X4150,X4148,X4150),inference(resolution,[status(thm)],[c12989, c362])).
% 23.43/23.65 cnf(c13011,plain,cyclic(X4164,X4166,X4165,X4164),inference(resolution,[status(thm)],[c12990, c359])).
% 23.43/23.65 cnf(c13021,plain,cyclic(X4179,X4180,X4179,X4181),inference(resolution,[status(thm)],[c13011, c365])).
% 23.43/23.65 cnf(c13035,plain,cyclic(X4195,X4195,X4197,X4196),inference(resolution,[status(thm)],[c13021, c362])).
% 23.43/23.65 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)).
% 23.43/23.65 fof(c264,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q))|cong(A,B,P,Q)))))))),inference(fof_nnf,[status(thm)],[ruleD43])).
% 23.43/23.65 fof(c265,plain,(![A]:(![B]:(![C]:(![P]:(![Q]:((![R]:(((~cyclic(A,B,C,P)|~cyclic(A,B,C,Q))|~cyclic(A,B,C,R))|~eqangle(C,A,C,B,R,P,R,Q)))|cong(A,B,P,Q))))))),inference(shift_quantors,[status(thm)],[c264])).
% 23.43/23.65 fof(c267,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274))|cong(X270,X271,X273,X274)))))))),inference(shift_quantors,[status(thm)],[fof(c266,plain,(![X270]:(![X271]:(![X272]:(![X273]:(![X274]:((![X275]:(((~cyclic(X270,X271,X272,X273)|~cyclic(X270,X271,X272,X274))|~cyclic(X270,X271,X272,X275))|~eqangle(X272,X270,X272,X271,X275,X273,X275,X274)))|cong(X270,X271,X273,X274))))))),inference(variable_rename,[status(thm)],[c265])).])).
% 23.43/23.65 cnf(c268,plain,~cyclic(X1057,X1056,X1054,X1055)|~cyclic(X1057,X1056,X1054,X1052)|~cyclic(X1057,X1056,X1054,X1053)|~eqangle(X1054,X1057,X1054,X1056,X1053,X1055,X1053,X1052)|cong(X1057,X1056,X1055,X1052),inference(split_conjunct,[status(thm)],[c267])).
% 23.43/23.65 cnf(c10201,plain,eqangle(X3425,X3424,X3423,X3426,X3425,X3424,X3426,X3423),inference(resolution,[status(thm)],[c6730, c350])).
% 23.43/23.65 cnf(c10425,plain,eqangle(X3522,X3519,X3522,X3519,X3521,X3520,X3520,X3521),inference(resolution,[status(thm)],[c10201, c344])).
% 23.43/23.65 cnf(c10736,plain,~cyclic(X5239,X5239,X5238,X5237)|cong(X5239,X5239,X5237,X5237),inference(resolution,[status(thm)],[c10425, c268])).
% 23.43/23.65 cnf(c16641,plain,cong(X5240,X5240,X5241,X5241),inference(resolution,[status(thm)],[c10736, c13035])).
% 23.43/23.65 cnf(c16659,plain,~coll(X5258,X5258,X5258)|midp(X5258,X5258,X5258),inference(resolution,[status(thm)],[c16641, c186])).
% 23.43/23.65 cnf(c16688,plain,midp(X5259,X5259,X5259),inference(resolution,[status(thm)],[c16659, c9987])).
% 23.43/23.65 cnf(c16700,plain,midp(X5261,X5260,X5260),inference(resolution,[status(thm)],[c16688, c6076])).
% 23.43/23.65 cnf(c16723,plain,cong(X5272,X5273,X5274,X5273),inference(resolution,[status(thm)],[c16700, c15132])).
% 23.43/23.65 cnf(c16820,plain,cong(X5292,X5293,X5293,X5294),inference(resolution,[status(thm)],[c16723, c338])).
% 23.43/23.65 cnf(c16988,plain,cong(X5340,X5341,X5342,X5340),inference(resolution,[status(thm)],[c16820, c335])).
% 23.43/23.65 cnf(c17172,plain,cong(X5369,X5370,X5369,X5371),inference(resolution,[status(thm)],[c16988, c338])).
% 23.43/23.65 cnf(c17212,plain,$false,inference(resolution,[status(thm)],[c17172, c21])).
% 23.43/23.65 % SZS output end CNFRefutation
% 23.43/23.65
% 23.43/23.65 % Initial clauses : 134
% 23.43/23.65 % Processed clauses : 2009
% 23.43/23.65 % Factors computed : 125
% 23.43/23.65 % Resolvents computed: 16698
% 23.43/23.65 % Tautologies deleted: 18
% 23.43/23.65 % Forward subsumed : 5102
% 23.43/23.65 % Backward subsumed : 1077
% 23.43/23.65 % -------- CPU Time ---------
% 23.43/23.65 % User time : 23.275 s
% 23.43/23.65 % System time : 0.036 s
% 23.43/23.65 % Total time : 23.311 s
%------------------------------------------------------------------------------