%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO623+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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:26 EDT 2024
% Result : Theorem 207.78s 207.96s
% Output : Refutation 207.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO623+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 : n002.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:01:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 207.78/207.96 % Version: 1.5
% 207.78/207.96 % SZS status Theorem
% 207.78/207.96 % SZS output start CNFRefutation
% 207.78/207.96 fof(exemplo6GDDFULL8110986,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(((((((midp(D,C,A)&midp(E,B,C))&midp(F,A,B))&eqangle(G,B,B,C,G,B,B,A))&coll(G,D,F))&coll(H,B,G))&coll(H,D,E))=>cong(D,G,D,H)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL8110986)).
% 207.78/207.96 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(((((((midp(D,C,A)&midp(E,B,C))&midp(F,A,B))&eqangle(G,B,B,C,G,B,B,A))&coll(G,D,F))&coll(H,B,G))&coll(H,D,E))=>cong(D,G,D,H))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110986])).
% 207.78/207.96 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(((((((midp(D,C,A)&midp(E,B,C))&midp(F,A,B))&eqangle(G,B,B,C,G,B,B,A))&coll(G,D,F))&coll(H,B,G))&coll(H,D,E))&~cong(D,G,D,H)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 207.78/207.96 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((midp(X5,X4,X2)&midp(X6,X3,X4))&midp(X7,X2,X3))&eqangle(X8,X3,X3,X4,X8,X3,X3,X2))&coll(X8,X5,X7))&coll(X9,X3,X8))&coll(X9,X5,X6))&~cong(X5,X8,X5,X9)))))))))),inference(variable_rename,[status(thm)],[c12])).
% 207.78/207.96 fof(c14,negated_conjecture,(((((((midp(skolem0004,skolem0003,skolem0001)&midp(skolem0005,skolem0002,skolem0003))&midp(skolem0006,skolem0001,skolem0002))&eqangle(skolem0007,skolem0002,skolem0002,skolem0003,skolem0007,skolem0002,skolem0002,skolem0001))&coll(skolem0007,skolem0004,skolem0006))&coll(skolem0008,skolem0002,skolem0007))&coll(skolem0008,skolem0004,skolem0005))&~cong(skolem0004,skolem0007,skolem0004,skolem0008)),inference(skolemize,[status(esa)],[c13])).
% 207.78/207.96 cnf(c22,negated_conjecture,~cong(skolem0004,skolem0007,skolem0004,skolem0008),inference(split_conjunct,[status(thm)],[c14])).
% 207.78/207.96 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)).
% 207.78/207.96 fof(c337,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 207.78/207.96 fof(c338,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X410,X411,X413,X412)))))),inference(variable_rename,[status(thm)],[c337])).
% 207.78/207.96 cnf(c339,plain,~cong(X719,X721,X722,X720)|cong(X719,X721,X720,X722),inference(split_conjunct,[status(thm)],[c338])).
% 207.78/207.96 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)).
% 207.78/207.96 fof(c334,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 207.78/207.96 fof(c335,plain,(![X406]:(![X407]:(![X408]:(![X409]:(~cong(X406,X407,X408,X409)|cong(X408,X409,X406,X407)))))),inference(variable_rename,[status(thm)],[c334])).
% 207.78/207.96 cnf(c336,plain,~cong(X706,X704,X705,X707)|cong(X705,X707,X706,X704),inference(split_conjunct,[status(thm)],[c335])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 cnf(c196,plain,~midp(X946,X945,X942)|~para(X945,X944,X942,X943)|~para(X945,X943,X942,X944)|midp(X946,X944,X943),inference(split_conjunct,[status(thm)],[c195])).
% 207.78/207.96 cnf(c1205,plain,~midp(X2421,X2420,X2419)|~para(X2420,X2418,X2419,X2418)|midp(X2421,X2418,X2418),inference(factor,[status(thm)],[c196])).
% 207.78/207.96 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)).
% 207.78/207.96 fof(c396,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 207.78/207.96 fof(c397,plain,(![X517]:(![X518]:(![X519]:(![X520]:(~para(X517,X518,X519,X520)|para(X517,X518,X520,X519)))))),inference(variable_rename,[status(thm)],[c396])).
% 207.78/207.96 cnf(c398,plain,~para(X792,X793,X791,X790)|para(X792,X793,X790,X791),inference(split_conjunct,[status(thm)],[c397])).
% 207.78/207.96 cnf(c17,negated_conjecture,midp(skolem0006,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 207.78/207.96 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 207.78/207.96 fof(c375,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 207.78/207.96 fof(c376,plain,(![X484]:(![X485]:(![X486]:(~midp(X486,X485,X484)|midp(X486,X484,X485))))),inference(variable_rename,[status(thm)],[c375])).
% 207.78/207.96 cnf(c377,plain,~midp(X559,X558,X560)|midp(X559,X560,X558),inference(split_conjunct,[status(thm)],[c376])).
% 207.78/207.96 cnf(c422,plain,midp(skolem0006,skolem0002,skolem0001),inference(resolution,[status(thm)],[c377, c17])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 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])).])).
% 207.78/207.96 cnf(c201,plain,~midp(X951,X947,X948)|~midp(X951,X949,X950)|para(X947,X949,X948,X950),inference(split_conjunct,[status(thm)],[c200])).
% 207.78/207.96 cnf(c1221,plain,~midp(skolem0006,X2442,X2443)|para(X2442,skolem0001,X2443,skolem0002),inference(resolution,[status(thm)],[c201, c17])).
% 207.78/207.96 cnf(c6706,plain,para(skolem0002,skolem0001,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1221, c422])).
% 207.78/207.96 cnf(c6811,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c6706, c398])).
% 207.78/207.96 cnf(c6950,plain,~midp(X5582,skolem0002,skolem0002)|midp(X5582,skolem0001,skolem0001),inference(resolution,[status(thm)],[c6811, c1205])).
% 207.78/207.96 cnf(c15,negated_conjecture,midp(skolem0004,skolem0003,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 207.78/207.96 cnf(c421,plain,midp(skolem0004,skolem0001,skolem0003),inference(resolution,[status(thm)],[c377, c15])).
% 207.78/207.96 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)).
% 207.78/207.96 fof(c393,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 207.78/207.96 fof(c394,plain,(![X513]:(![X514]:(![X515]:(![X516]:(~para(X513,X514,X515,X516)|para(X515,X516,X513,X514)))))),inference(variable_rename,[status(thm)],[c393])).
% 207.78/207.96 cnf(c395,plain,~para(X789,X788,X787,X786)|para(X787,X786,X789,X788),inference(split_conjunct,[status(thm)],[c394])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 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])).])).
% 207.78/207.96 cnf(c289,plain,~eqangle(X1060,X1064,X1062,X1061,X1065,X1063,X1062,X1061)|para(X1060,X1064,X1065,X1063),inference(split_conjunct,[status(thm)],[c288])).
% 207.78/207.96 cnf(c18,negated_conjecture,eqangle(skolem0007,skolem0002,skolem0002,skolem0003,skolem0007,skolem0002,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 cnf(c351,plain,~eqangle(X1201,X1202,X1200,X1198,X1205,X1204,X1199,X1203)|eqangle(X1200,X1198,X1201,X1202,X1199,X1203,X1205,X1204),inference(split_conjunct,[status(thm)],[c350])).
% 207.78/207.96 cnf(c1566,plain,eqangle(skolem0002,skolem0003,skolem0007,skolem0002,skolem0002,skolem0001,skolem0007,skolem0002),inference(resolution,[status(thm)],[c351, c18])).
% 207.78/207.96 cnf(c8949,plain,para(skolem0002,skolem0003,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1566, c289])).
% 207.78/207.96 cnf(c9072,plain,para(skolem0002,skolem0003,skolem0001,skolem0002),inference(resolution,[status(thm)],[c8949, c398])).
% 207.78/207.96 cnf(c9097,plain,para(skolem0001,skolem0002,skolem0002,skolem0003),inference(resolution,[status(thm)],[c9072, c395])).
% 207.78/207.96 cnf(c9138,plain,para(skolem0001,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c9097, c398])).
% 207.78/207.96 cnf(c9182,plain,~midp(X5892,skolem0001,skolem0003)|midp(X5892,skolem0002,skolem0002),inference(resolution,[status(thm)],[c9138, c1205])).
% 207.78/207.96 cnf(c20060,plain,midp(skolem0004,skolem0002,skolem0002),inference(resolution,[status(thm)],[c9182, c421])).
% 207.78/207.96 cnf(c20100,plain,midp(skolem0004,skolem0001,skolem0001),inference(resolution,[status(thm)],[c20060, c6950])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 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])).])).
% 207.78/207.96 cnf(c284,plain,~para(X1057,X1054,X1058,X1059)|eqangle(X1057,X1054,X1056,X1055,X1058,X1059,X1056,X1055),inference(split_conjunct,[status(thm)],[c283])).
% 207.78/207.96 cnf(c16,negated_conjecture,midp(skolem0005,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 207.78/207.96 cnf(c420,plain,midp(skolem0005,skolem0003,skolem0002),inference(resolution,[status(thm)],[c377, c16])).
% 207.78/207.96 cnf(c1219,plain,~midp(skolem0005,X2438,X2439)|para(X2438,skolem0002,X2439,skolem0003),inference(resolution,[status(thm)],[c201, c16])).
% 207.78/207.96 cnf(c6702,plain,para(skolem0003,skolem0002,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1219, c420])).
% 207.78/207.96 cnf(c6761,plain,para(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c6702, c398])).
% 207.78/207.96 cnf(c6906,plain,eqangle(skolem0003,skolem0002,X5575,X5574,skolem0003,skolem0002,X5575,X5574),inference(resolution,[status(thm)],[c6761, c284])).
% 207.78/207.96 cnf(c19374,plain,eqangle(X6667,X6668,skolem0003,skolem0002,X6667,X6668,skolem0003,skolem0002),inference(resolution,[status(thm)],[c6906, c351])).
% 207.78/207.96 cnf(c24134,plain,para(X6669,X6670,X6669,X6670),inference(resolution,[status(thm)],[c19374, c289])).
% 207.78/207.96 cnf(c24169,plain,~midp(X8860,X8861,X8861)|midp(X8860,X8862,X8862),inference(resolution,[status(thm)],[c24134, c1205])).
% 207.78/207.96 cnf(c35120,plain,midp(skolem0004,X8869,X8869),inference(resolution,[status(thm)],[c24169, c20100])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 cnf(c239,plain,~perp(X998,X999,X999,X997)|~midp(X996,X998,X997)|cong(X998,X996,X999,X996),inference(split_conjunct,[status(thm)],[c238])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 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])).])).
% 207.78/207.96 cnf(c162,plain,~eqangle(X906,X909,X911,X910,X904,X907,X908,X905)|~perp(X904,X907,X908,X905)|perp(X906,X909,X911,X910),inference(split_conjunct,[status(thm)],[c161])).
% 207.78/207.96 cnf(c24204,plain,para(X6695,X6696,X6696,X6695),inference(resolution,[status(thm)],[c24134, c398])).
% 207.78/207.96 cnf(c26030,plain,eqangle(X9812,X9813,X9814,X9815,X9813,X9812,X9814,X9815),inference(resolution,[status(thm)],[c24204, c284])).
% 207.78/207.96 cnf(c39957,plain,~perp(X11971,X11973,X11972,X11974)|perp(X11973,X11971,X11972,X11974),inference(resolution,[status(thm)],[c26030, c162])).
% 207.78/207.96 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 207.78/207.96 fof(c387,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 207.78/207.96 fof(c388,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c387])).
% 207.78/207.96 cnf(c389,plain,~perp(X785,X784,X783,X782)|perp(X785,X784,X782,X783),inference(split_conjunct,[status(thm)],[c388])).
% 207.78/207.96 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)).
% 207.78/207.96 fof(c384,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 207.78/207.96 fof(c385,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c384])).
% 207.78/207.96 cnf(c386,plain,~perp(X780,X781,X778,X779)|perp(X778,X779,X780,X781),inference(split_conjunct,[status(thm)],[c385])).
% 207.78/207.96 fof(ruleD12,axiom,(![A]:(![B]:(![C]:(![O]:((cong(O,A,O,B)&cong(O,A,O,C))=>circle(O,A,B,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD12)).
% 207.78/207.96 fof(c372,plain,(![A]:(![B]:(![C]:(![O]:((~cong(O,A,O,B)|~cong(O,A,O,C))|circle(O,A,B,C)))))),inference(fof_nnf,[status(thm)],[ruleD12])).
% 207.78/207.96 fof(c373,plain,(![X480]:(![X481]:(![X482]:(![X483]:((~cong(X483,X480,X483,X481)|~cong(X483,X480,X483,X482))|circle(X483,X480,X481,X482)))))),inference(variable_rename,[status(thm)],[c372])).
% 207.78/207.96 cnf(c374,plain,~cong(X1227,X1224,X1227,X1226)|~cong(X1227,X1224,X1227,X1225)|circle(X1227,X1224,X1226,X1225),inference(split_conjunct,[status(thm)],[c373])).
% 207.78/207.96 cnf(c1577,plain,~cong(X1317,X1315,X1317,X1316)|circle(X1317,X1315,X1316,X1316),inference(factor,[status(thm)],[c374])).
% 207.78/207.96 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)).
% 207.78/207.96 fof(c182,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 207.78/207.96 fof(c183,plain,(![X158]:(![X159]:(![X160]:(~midp(X158,X159,X160)|cong(X158,X159,X158,X160))))),inference(variable_rename,[status(thm)],[c182])).
% 207.78/207.96 cnf(c184,plain,~midp(X695,X696,X694)|cong(X695,X696,X695,X694),inference(split_conjunct,[status(thm)],[c183])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 cnf(c225,plain,~cong(X982,X981,X983,X981)|~cong(X982,X980,X983,X980)|perp(X982,X983,X981,X980),inference(split_conjunct,[status(thm)],[c224])).
% 207.78/207.96 cnf(c1310,plain,~cong(X1285,X1287,X1286,X1287)|perp(X1285,X1286,X1287,X1287),inference(factor,[status(thm)],[c225])).
% 207.78/207.96 cnf(c541,plain,cong(skolem0006,skolem0001,skolem0006,skolem0002),inference(resolution,[status(thm)],[c184, c17])).
% 207.78/207.96 cnf(c568,plain,cong(skolem0006,skolem0001,skolem0002,skolem0006),inference(resolution,[status(thm)],[c339, c541])).
% 207.78/207.96 cnf(c590,plain,cong(skolem0002,skolem0006,skolem0006,skolem0001),inference(resolution,[status(thm)],[c568, c336])).
% 207.78/207.96 cnf(c623,plain,cong(skolem0002,skolem0006,skolem0001,skolem0006),inference(resolution,[status(thm)],[c590, c339])).
% 207.78/207.96 cnf(c543,plain,cong(skolem0006,skolem0002,skolem0006,skolem0001),inference(resolution,[status(thm)],[c184, c422])).
% 207.78/207.96 cnf(c564,plain,cong(skolem0006,skolem0002,skolem0001,skolem0006),inference(resolution,[status(thm)],[c339, c543])).
% 207.78/207.96 cnf(c571,plain,cong(skolem0001,skolem0006,skolem0006,skolem0002),inference(resolution,[status(thm)],[c564, c336])).
% 207.78/207.96 cnf(c597,plain,cong(skolem0001,skolem0006,skolem0002,skolem0006),inference(resolution,[status(thm)],[c571, c339])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 cnf(c333,plain,~cong(X1164,X1168,X1166,X1169)|~cong(X1166,X1169,X1165,X1167)|cong(X1164,X1168,X1165,X1167),inference(split_conjunct,[status(thm)],[c332])).
% 207.78/207.96 cnf(c1541,plain,~cong(X2909,X2910,skolem0001,skolem0006)|cong(X2909,X2910,skolem0002,skolem0006),inference(resolution,[status(thm)],[c333, c597])).
% 207.78/207.96 cnf(c8519,plain,cong(skolem0002,skolem0006,skolem0002,skolem0006),inference(resolution,[status(thm)],[c1541, c623])).
% 207.78/207.96 cnf(c8616,plain,perp(skolem0002,skolem0002,skolem0006,skolem0006),inference(resolution,[status(thm)],[c8519, c1310])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 cnf(c383,plain,~perp(X1237,X1236,X1239,X1234)|~perp(X1239,X1234,X1235,X1238)|para(X1237,X1236,X1235,X1238),inference(split_conjunct,[status(thm)],[c382])).
% 207.78/207.96 cnf(c1861,plain,perp(skolem0001,skolem0002,skolem0006,skolem0006),inference(resolution,[status(thm)],[c1310, c597])).
% 207.78/207.96 cnf(c1869,plain,perp(skolem0006,skolem0006,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1861, c386])).
% 207.78/207.96 cnf(c1934,plain,~perp(X3491,X3490,skolem0006,skolem0006)|para(X3491,X3490,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1869, c383])).
% 207.78/207.96 cnf(c11898,plain,para(skolem0002,skolem0002,skolem0001,skolem0002),inference(resolution,[status(thm)],[c1934, c8616])).
% 207.78/207.96 cnf(c12021,plain,~midp(X6121,skolem0002,skolem0001)|midp(X6121,skolem0002,skolem0002),inference(resolution,[status(thm)],[c11898, c1205])).
% 207.78/207.96 cnf(c21176,plain,midp(skolem0006,skolem0002,skolem0002),inference(resolution,[status(thm)],[c12021, c422])).
% 207.78/207.96 cnf(c21226,plain,midp(skolem0006,skolem0001,skolem0001),inference(resolution,[status(thm)],[c21176, c6950])).
% 207.78/207.96 cnf(c35118,plain,midp(skolem0006,X8864,X8864),inference(resolution,[status(thm)],[c24169, c21226])).
% 207.78/207.96 cnf(c35598,plain,cong(skolem0006,X8917,skolem0006,X8917),inference(resolution,[status(thm)],[c35118, c184])).
% 207.78/207.96 cnf(c36605,plain,cong(skolem0006,X8958,X8958,skolem0006),inference(resolution,[status(thm)],[c35598, c339])).
% 207.78/207.96 cnf(c37091,plain,cong(X9014,skolem0006,skolem0006,X9014),inference(resolution,[status(thm)],[c36605, c336])).
% 207.78/207.96 cnf(c37661,plain,cong(X9109,skolem0006,X9109,skolem0006),inference(resolution,[status(thm)],[c37091, c339])).
% 207.78/207.96 cnf(c38352,plain,circle(X9298,skolem0006,skolem0006,skolem0006),inference(resolution,[status(thm)],[c37661, c1577])).
% 207.78/207.96 fof(ruleD49,axiom,(![A]:(![B]:(![C]:(![O]:(![X]:((circle(O,A,B,C)&eqangle(A,X,A,B,C,A,C,B))=>perp(O,A,A,X))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD49)).
% 207.78/207.96 fof(c246,plain,(![A]:(![B]:(![C]:(![O]:(![X]:((~circle(O,A,B,C)|~eqangle(A,X,A,B,C,A,C,B))|perp(O,A,A,X))))))),inference(fof_nnf,[status(thm)],[ruleD49])).
% 207.78/207.96 fof(c247,plain,(![X246]:(![X247]:(![X248]:(![X249]:(![X250]:((~circle(X249,X246,X247,X248)|~eqangle(X246,X250,X246,X247,X248,X246,X248,X247))|perp(X249,X246,X246,X250))))))),inference(variable_rename,[status(thm)],[c246])).
% 207.78/207.96 cnf(c248,plain,~circle(X1012,X1014,X1011,X1013)|~eqangle(X1014,X1010,X1014,X1011,X1013,X1014,X1013,X1011)|perp(X1012,X1014,X1014,X1010),inference(split_conjunct,[status(thm)],[c247])).
% 207.78/207.96 cnf(c24173,plain,eqangle(X9301,X9300,X9302,X9303,X9301,X9300,X9302,X9303),inference(resolution,[status(thm)],[c24134, c284])).
% 207.78/207.96 cnf(c39143,plain,~circle(X11666,X11664,X11665,X11664)|perp(X11666,X11664,X11664,X11664),inference(resolution,[status(thm)],[c24173, c248])).
% 207.78/207.96 cnf(c45494,plain,perp(X11715,skolem0006,skolem0006,skolem0006),inference(resolution,[status(thm)],[c39143, c38352])).
% 207.78/207.96 cnf(c45826,plain,perp(skolem0006,skolem0006,X11735,skolem0006),inference(resolution,[status(thm)],[c45494, c386])).
% 207.78/207.96 cnf(c45966,plain,perp(skolem0006,skolem0006,skolem0006,X11775),inference(resolution,[status(thm)],[c45826, c389])).
% 207.78/207.96 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)).
% 207.78/207.96 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])).
% 207.78/207.96 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])).
% 207.78/207.96 cnf(c345,plain,~eqangle(X1186,X1189,X1185,X1188,X1184,X1183,X1187,X1182)|eqangle(X1186,X1189,X1184,X1183,X1185,X1188,X1187,X1182),inference(split_conjunct,[status(thm)],[c344])).
% 207.78/207.96 cnf(c39158,plain,eqangle(X10074,X10073,X10074,X10073,X10075,X10076,X10075,X10076),inference(resolution,[status(thm)],[c24173, c345])).
% 207.78/207.96 cnf(c42402,plain,~perp(X12267,X12269,X12267,X12269)|perp(X12266,X12268,X12266,X12268),inference(resolution,[status(thm)],[c39158, c162])).
% 207.78/207.96 cnf(c46894,plain,perp(X12271,X12270,X12271,X12270),inference(resolution,[status(thm)],[c42402, c45966])).
% 207.78/207.96 cnf(c46944,plain,perp(X12357,X12356,X12356,X12357),inference(resolution,[status(thm)],[c46894, c39957])).
% 207.78/207.96 cnf(c47028,plain,~midp(X12476,X12475,X12475)|cong(X12475,X12476,X12477,X12476),inference(resolution,[status(thm)],[c46944, c239])).
% 207.78/207.96 cnf(c47487,plain,cong(X12483,skolem0004,X12482,skolem0004),inference(resolution,[status(thm)],[c47028, c35120])).
% 207.78/207.96 cnf(c47544,plain,cong(X12496,skolem0004,skolem0004,X12497),inference(resolution,[status(thm)],[c47487, c339])).
% 207.78/207.96 cnf(c47663,plain,cong(skolem0004,X12539,X12538,skolem0004),inference(resolution,[status(thm)],[c47544, c336])).
% 207.78/207.96 cnf(c47858,plain,cong(skolem0004,X12625,skolem0004,X12624),inference(resolution,[status(thm)],[c47663, c339])).
% 207.78/207.96 cnf(c48143,plain,$false,inference(resolution,[status(thm)],[c47858, c22])).
% 207.78/207.96 % SZS output end CNFRefutation
% 207.78/207.96
% 207.78/207.96 % Initial clauses : 135
% 207.78/207.96 % Processed clauses : 5072
% 207.78/207.96 % Factors computed : 228
% 207.78/207.96 % Resolvents computed: 47524
% 207.78/207.96 % Tautologies deleted: 36
% 207.78/207.96 % Forward subsumed : 12397
% 207.78/207.96 % Backward subsumed : 2782
% 207.78/207.96 % -------- CPU Time ---------
% 207.78/207.96 % User time : 207.483 s
% 207.78/207.96 % System time : 0.122 s
% 207.78/207.96 % Total time : 207.605 s
%------------------------------------------------------------------------------