%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO632+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:27 EDT 2024
% Result : Theorem 47.14s 47.32s
% Output : Refutation 47.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO632+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 07:59:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 47.14/47.32 % Version: 1.5
% 47.14/47.32 % SZS status Theorem
% 47.14/47.32 % SZS output start CNFRefutation
% 47.14/47.32 fof(exemplo6GDDFULL8110995,conjecture,(![A]:(![B]:(![C]:(![A1]:(![S]:(![F]:(![P]:(![Q]:(![NWPNT1]:(![NWPNT2]:((((((((midp(A1,C,B)&eqangle(S,A,A,B,C,A,A,A1))&coll(S,B,C))&circle(F,A,B,C))&circle(F,A,P,NWPNT1))&coll(P,A,A1))&circle(F,A,Q,NWPNT2))&coll(Q,A,S))=>para(B,C,P,Q)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL8110995)).
% 47.14/47.32 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![A1]:(![S]:(![F]:(![P]:(![Q]:(![NWPNT1]:(![NWPNT2]:((((((((midp(A1,C,B)&eqangle(S,A,A,B,C,A,A,A1))&coll(S,B,C))&circle(F,A,B,C))&circle(F,A,P,NWPNT1))&coll(P,A,A1))&circle(F,A,Q,NWPNT2))&coll(Q,A,S))=>para(B,C,P,Q))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110995])).
% 47.14/47.32 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[A1]:(?[S]:(?[F]:(?[P]:(?[Q]:(?[NWPNT1]:(?[NWPNT2]:((((((((midp(A1,C,B)&eqangle(S,A,A,B,C,A,A,A1))&coll(S,B,C))&circle(F,A,B,C))&circle(F,A,P,NWPNT1))&coll(P,A,A1))&circle(F,A,Q,NWPNT2))&coll(Q,A,S))&~para(B,C,P,Q)))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 47.14/47.32 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[A1]:(?[S]:(?[F]:(?[P]:(?[Q]:((((((((midp(A1,C,B)&eqangle(S,A,A,B,C,A,A,A1))&coll(S,B,C))&circle(F,A,B,C))&(?[NWPNT1]:circle(F,A,P,NWPNT1)))&coll(P,A,A1))&(?[NWPNT2]:circle(F,A,Q,NWPNT2)))&coll(Q,A,S))&~para(B,C,P,Q)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 47.14/47.32 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((midp(X5,X4,X3)&eqangle(X6,X2,X2,X3,X4,X2,X2,X5))&coll(X6,X3,X4))&circle(X7,X2,X3,X4))&(?[X10]:circle(X7,X2,X8,X10)))&coll(X8,X2,X5))&(?[X11]:circle(X7,X2,X9,X11)))&coll(X9,X2,X6))&~para(X3,X4,X8,X9)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 47.14/47.32 fof(c15,negated_conjecture,((((((((midp(skolem0004,skolem0003,skolem0002)&eqangle(skolem0005,skolem0001,skolem0001,skolem0002,skolem0003,skolem0001,skolem0001,skolem0004))&coll(skolem0005,skolem0002,skolem0003))&circle(skolem0006,skolem0001,skolem0002,skolem0003))&circle(skolem0006,skolem0001,skolem0007,skolem0009))&coll(skolem0007,skolem0001,skolem0004))&circle(skolem0006,skolem0001,skolem0008,skolem0010))&coll(skolem0008,skolem0001,skolem0005))&~para(skolem0002,skolem0003,skolem0007,skolem0008)),inference(skolemize,[status(esa)],[c14])).
% 47.14/47.32 cnf(c24,negated_conjecture,~para(skolem0002,skolem0003,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c395,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD5])).
% 47.14/47.32 fof(c396,plain,(![X515]:(![X516]:(![X517]:(![X518]:(~para(X515,X516,X517,X518)|para(X517,X518,X515,X516)))))),inference(variable_rename,[status(thm)],[c395])).
% 47.14/47.32 cnf(c397,plain,~para(X728,X727,X725,X726)|para(X725,X726,X728,X727),inference(split_conjunct,[status(thm)],[c396])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 47.14/47.32 fof(c387,plain,(![X501]:(![X502]:(![X503]:(![X504]:(~perp(X501,X502,X503,X504)|perp(X503,X504,X501,X502)))))),inference(variable_rename,[status(thm)],[c386])).
% 47.14/47.32 cnf(c388,plain,~perp(X715,X713,X714,X712)|perp(X714,X712,X715,X713),inference(split_conjunct,[status(thm)],[c387])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 47.14/47.32 fof(c340,plain,(![X412]:(![X413]:(![X414]:(![X415]:(~cong(X412,X413,X414,X415)|cong(X412,X413,X415,X414)))))),inference(variable_rename,[status(thm)],[c339])).
% 47.14/47.32 cnf(c341,plain,~cong(X685,X687,X688,X686)|cong(X685,X687,X686,X688),inference(split_conjunct,[status(thm)],[c340])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 47.14/47.32 fof(c337,plain,(![X408]:(![X409]:(![X410]:(![X411]:(~cong(X408,X409,X410,X411)|cong(X410,X411,X408,X409)))))),inference(variable_rename,[status(thm)],[c336])).
% 47.14/47.32 cnf(c338,plain,~cong(X677,X675,X678,X676)|cong(X678,X676,X677,X675),inference(split_conjunct,[status(thm)],[c337])).
% 47.14/47.32 cnf(c16,negated_conjecture,midp(skolem0004,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c184,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 47.14/47.32 fof(c185,plain,(![X160]:(![X161]:(![X162]:(~midp(X160,X161,X162)|cong(X160,X161,X160,X162))))),inference(variable_rename,[status(thm)],[c184])).
% 47.14/47.32 cnf(c186,plain,~midp(X665,X663,X664)|cong(X665,X663,X665,X664),inference(split_conjunct,[status(thm)],[c185])).
% 47.14/47.32 cnf(c496,plain,cong(skolem0004,skolem0003,skolem0004,skolem0002),inference(resolution,[status(thm)],[c186, c16])).
% 47.14/47.32 cnf(c502,plain,cong(skolem0004,skolem0003,skolem0002,skolem0004),inference(resolution,[status(thm)],[c341, c496])).
% 47.14/47.32 cnf(c506,plain,cong(skolem0002,skolem0004,skolem0004,skolem0003),inference(resolution,[status(thm)],[c502, c338])).
% 47.14/47.32 cnf(c514,plain,cong(skolem0002,skolem0004,skolem0003,skolem0004),inference(resolution,[status(thm)],[c506, c341])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c225,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])).
% 47.14/47.32 fof(c226,plain,(![X218]:(![X219]:(![X220]:(![X221]:((~cong(X218,X220,X219,X220)|~cong(X218,X221,X219,X221))|perp(X218,X219,X220,X221)))))),inference(variable_rename,[status(thm)],[c225])).
% 47.14/47.32 cnf(c227,plain,~cong(X984,X983,X982,X983)|~cong(X984,X985,X982,X985)|perp(X984,X982,X983,X985),inference(split_conjunct,[status(thm)],[c226])).
% 47.14/47.32 cnf(c1080,plain,~cong(X1005,X1007,X1006,X1007)|perp(X1005,X1006,X1007,X1007),inference(factor,[status(thm)],[c227])).
% 47.14/47.32 cnf(c1111,plain,perp(skolem0002,skolem0003,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1080, c514])).
% 47.14/47.32 cnf(c1124,plain,perp(skolem0004,skolem0004,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1111, c388])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c383,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])).
% 47.14/47.32 fof(c384,plain,(![X495]:(![X496]:(![X497]:(![X498]:(![X499]:(![X500]:((~perp(X495,X496,X497,X498)|~perp(X497,X498,X499,X500))|para(X495,X496,X499,X500)))))))),inference(variable_rename,[status(thm)],[c383])).
% 47.14/47.32 cnf(c385,plain,~perp(X1283,X1278,X1282,X1279)|~perp(X1282,X1279,X1280,X1281)|para(X1283,X1278,X1280,X1281),inference(split_conjunct,[status(thm)],[c384])).
% 47.14/47.32 cnf(c1443,plain,~perp(X2653,X2654,skolem0004,skolem0004)|para(X2653,X2654,skolem0002,skolem0003),inference(resolution,[status(thm)],[c385, c1124])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c196,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])).
% 47.14/47.32 fof(c197,plain,(![X174]:(![X175]:(![X176]:(![X177]:(![X178]:(((~midp(X178,X174,X175)|~para(X174,X176,X175,X177))|~para(X174,X177,X175,X176))|midp(X178,X176,X177))))))),inference(variable_rename,[status(thm)],[c196])).
% 47.14/47.32 cnf(c198,plain,~midp(X944,X946,X947)|~para(X946,X948,X947,X945)|~para(X946,X945,X947,X948)|midp(X944,X948,X945),inference(split_conjunct,[status(thm)],[c197])).
% 47.14/47.32 cnf(c1075,plain,~midp(X2253,X2256,X2254)|~para(X2256,X2255,X2254,X2255)|midp(X2253,X2255,X2255),inference(factor,[status(thm)],[c198])).
% 47.14/47.32 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 47.14/47.32 fof(c377,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 47.14/47.32 fof(c378,plain,(![X486]:(![X487]:(![X488]:(~midp(X488,X487,X486)|midp(X488,X486,X487))))),inference(variable_rename,[status(thm)],[c377])).
% 47.14/47.32 cnf(c379,plain,~midp(X562,X560,X561)|midp(X562,X561,X560),inference(split_conjunct,[status(thm)],[c378])).
% 47.14/47.32 cnf(c418,plain,midp(skolem0004,skolem0002,skolem0003),inference(resolution,[status(thm)],[c379, c16])).
% 47.14/47.32 cnf(c495,plain,cong(skolem0004,skolem0002,skolem0004,skolem0003),inference(resolution,[status(thm)],[c186, c418])).
% 47.14/47.32 cnf(c501,plain,cong(skolem0004,skolem0002,skolem0003,skolem0004),inference(resolution,[status(thm)],[c341, c495])).
% 47.14/47.32 cnf(c503,plain,cong(skolem0003,skolem0004,skolem0004,skolem0002),inference(resolution,[status(thm)],[c501, c338])).
% 47.14/47.32 cnf(c511,plain,cong(skolem0003,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c503, c341])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c333,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])).
% 47.14/47.32 fof(c334,plain,(![X402]:(![X403]:(![X404]:(![X405]:(![X406]:(![X407]:((~cong(X402,X403,X404,X405)|~cong(X404,X405,X406,X407))|cong(X402,X403,X406,X407)))))))),inference(variable_rename,[status(thm)],[c333])).
% 47.14/47.32 cnf(c335,plain,~cong(X1192,X1193,X1191,X1190)|~cong(X1191,X1190,X1194,X1189)|cong(X1192,X1193,X1194,X1189),inference(split_conjunct,[status(thm)],[c334])).
% 47.14/47.32 cnf(c1372,plain,~cong(X2595,X2596,skolem0002,skolem0004)|cong(X2595,X2596,skolem0004,skolem0003),inference(resolution,[status(thm)],[c335, c506])).
% 47.14/47.32 cnf(c5926,plain,cong(skolem0003,skolem0004,skolem0004,skolem0003),inference(resolution,[status(thm)],[c1372, c511])).
% 47.14/47.32 cnf(c5967,plain,cong(skolem0003,skolem0004,skolem0003,skolem0004),inference(resolution,[status(thm)],[c5926, c341])).
% 47.14/47.32 cnf(c6008,plain,perp(skolem0003,skolem0003,skolem0004,skolem0004),inference(resolution,[status(thm)],[c5967, c1080])).
% 47.14/47.32 cnf(c6486,plain,para(skolem0003,skolem0003,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1443, c6008])).
% 47.14/47.32 cnf(c6526,plain,~midp(X3850,skolem0003,skolem0002)|midp(X3850,skolem0003,skolem0003),inference(resolution,[status(thm)],[c6486, c1075])).
% 47.14/47.32 cnf(c9281,plain,midp(skolem0004,skolem0003,skolem0003),inference(resolution,[status(thm)],[c6526, c16])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c287,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])).
% 47.14/47.32 fof(c288,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)],[c287])).
% 47.14/47.32 fof(c290,plain,(![X298]:(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(~eqangle(X298,X299,X302,X303,X300,X301,X302,X303)|para(X298,X299,X300,X301)))))))),inference(shift_quantors,[status(thm)],[fof(c289,plain,(![X298]:(![X299]:(![X300]:(![X301]:((![X302]:(![X303]:~eqangle(X298,X299,X302,X303,X300,X301,X302,X303)))|para(X298,X299,X300,X301)))))),inference(variable_rename,[status(thm)],[c288])).])).
% 47.14/47.32 cnf(c291,plain,~eqangle(X1080,X1079,X1078,X1077,X1075,X1076,X1078,X1077)|para(X1080,X1079,X1075,X1076),inference(split_conjunct,[status(thm)],[c290])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c351,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])).
% 47.14/47.32 fof(c352,plain,(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(![X451]:(~eqangle(X444,X445,X446,X447,X448,X449,X450,X451)|eqangle(X446,X447,X444,X445,X450,X451,X448,X449)))))))))),inference(variable_rename,[status(thm)],[c351])).
% 47.14/47.32 cnf(c353,plain,~eqangle(X1230,X1236,X1233,X1237,X1232,X1234,X1235,X1231)|eqangle(X1233,X1237,X1230,X1236,X1235,X1231,X1232,X1234),inference(split_conjunct,[status(thm)],[c352])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c282,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])).
% 47.14/47.32 fof(c283,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)],[c282])).
% 47.14/47.32 fof(c285,plain,(![X292]:(![X293]:(![X294]:(![X295]:(![X296]:(![X297]:(~para(X292,X293,X294,X295)|eqangle(X292,X293,X296,X297,X294,X295,X296,X297)))))))),inference(shift_quantors,[status(thm)],[fof(c284,plain,(![X292]:(![X293]:(![X294]:(![X295]:(~para(X292,X293,X294,X295)|(![X296]:(![X297]:eqangle(X292,X293,X296,X297,X294,X295,X296,X297)))))))),inference(variable_rename,[status(thm)],[c283])).])).
% 47.14/47.32 cnf(c286,plain,~para(X1070,X1069,X1066,X1067)|eqangle(X1070,X1069,X1071,X1068,X1066,X1067,X1071,X1068),inference(split_conjunct,[status(thm)],[c285])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c398,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 47.14/47.32 fof(c399,plain,(![X519]:(![X520]:(![X521]:(![X522]:(~para(X519,X520,X521,X522)|para(X519,X520,X522,X521)))))),inference(variable_rename,[status(thm)],[c398])).
% 47.14/47.32 cnf(c400,plain,~para(X731,X729,X730,X732)|para(X731,X729,X732,X730),inference(split_conjunct,[status(thm)],[c399])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c199,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])).
% 47.14/47.32 fof(c200,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c199])).
% 47.14/47.32 fof(c202,plain,(![X179]:(![X180]:(![X181]:(![X182]:(![X183]:((~midp(X183,X179,X180)|~midp(X183,X181,X182))|para(X179,X181,X180,X182))))))),inference(shift_quantors,[status(thm)],[fof(c201,plain,(![X179]:(![X180]:(![X181]:(![X182]:((![X183]:(~midp(X183,X179,X180)|~midp(X183,X181,X182)))|para(X179,X181,X180,X182)))))),inference(variable_rename,[status(thm)],[c200])).])).
% 47.14/47.32 cnf(c203,plain,~midp(X949,X950,X952)|~midp(X949,X951,X953)|para(X950,X951,X952,X953),inference(split_conjunct,[status(thm)],[c202])).
% 47.14/47.32 cnf(c1077,plain,~midp(skolem0004,X2100,X2099)|para(X2100,skolem0002,X2099,skolem0003),inference(resolution,[status(thm)],[c203, c418])).
% 47.14/47.32 cnf(c4492,plain,para(skolem0003,skolem0002,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1077, c16])).
% 47.14/47.32 cnf(c4495,plain,para(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c4492, c400])).
% 47.14/47.32 cnf(c4530,plain,eqangle(skolem0003,skolem0002,X3676,X3675,skolem0003,skolem0002,X3676,X3675),inference(resolution,[status(thm)],[c4495, c286])).
% 47.14/47.32 cnf(c8797,plain,eqangle(X3947,X3946,skolem0003,skolem0002,X3947,X3946,skolem0003,skolem0002),inference(resolution,[status(thm)],[c4530, c353])).
% 47.14/47.32 cnf(c9698,plain,para(X3948,X3949,X3948,X3949),inference(resolution,[status(thm)],[c8797, c291])).
% 47.14/47.32 cnf(c9738,plain,~midp(X5208,X5209,X5209)|midp(X5208,X5210,X5210),inference(resolution,[status(thm)],[c9698, c1075])).
% 47.14/47.32 cnf(c17331,plain,midp(skolem0004,X5211,X5211),inference(resolution,[status(thm)],[c9738, c9281])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c239,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])).
% 47.14/47.32 fof(c240,plain,(![X234]:(![X235]:(![X236]:(![X237]:((~perp(X234,X235,X235,X236)|~midp(X237,X234,X236))|cong(X234,X237,X235,X237)))))),inference(variable_rename,[status(thm)],[c239])).
% 47.14/47.32 cnf(c241,plain,~perp(X1001,X1002,X1002,X1003)|~midp(X1004,X1001,X1003)|cong(X1001,X1004,X1002,X1004),inference(split_conjunct,[status(thm)],[c240])).
% 47.14/47.32 fof(ruleD7,axiom,(![A]:(![B]:(![C]:(![D]:(perp(A,B,C,D)=>perp(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD7)).
% 47.14/47.32 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 47.14/47.32 fof(c390,plain,(![X505]:(![X506]:(![X507]:(![X508]:(~perp(X505,X506,X507,X508)|perp(X505,X506,X508,X507)))))),inference(variable_rename,[status(thm)],[c389])).
% 47.14/47.32 cnf(c391,plain,~perp(X724,X721,X722,X723)|perp(X724,X721,X723,X722),inference(split_conjunct,[status(thm)],[c390])).
% 47.14/47.32 cnf(c1110,plain,perp(skolem0003,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1080, c511])).
% 47.14/47.32 cnf(c1116,plain,perp(skolem0004,skolem0004,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1110, c388])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c380,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])).
% 47.14/47.32 fof(c381,plain,(![X489]:(![X490]:(![X491]:(![X492]:(![X493]:(![X494]:((~para(X489,X490,X491,X492)|~perp(X491,X492,X493,X494))|perp(X489,X490,X493,X494)))))))),inference(variable_rename,[status(thm)],[c380])).
% 47.14/47.32 cnf(c382,plain,~para(X1271,X1274,X1272,X1275)|~perp(X1272,X1275,X1273,X1276)|perp(X1271,X1274,X1273,X1276),inference(split_conjunct,[status(thm)],[c381])).
% 47.14/47.32 cnf(c1432,plain,~para(X2643,X2642,skolem0004,skolem0004)|perp(X2643,X2642,skolem0003,skolem0002),inference(resolution,[status(thm)],[c382, c1116])).
% 47.14/47.32 cnf(c1371,plain,~cong(X2593,X2594,skolem0004,skolem0003)|cong(X2593,X2594,skolem0004,skolem0002),inference(resolution,[status(thm)],[c335, c496])).
% 47.14/47.32 cnf(c5882,plain,cong(skolem0002,skolem0004,skolem0004,skolem0002),inference(resolution,[status(thm)],[c1371, c506])).
% 47.14/47.32 cnf(c5886,plain,cong(skolem0002,skolem0004,skolem0002,skolem0004),inference(resolution,[status(thm)],[c5882, c341])).
% 47.14/47.32 cnf(c5915,plain,perp(skolem0002,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c5886, c1080])).
% 47.14/47.32 cnf(c1444,plain,~perp(X2655,X2656,skolem0004,skolem0004)|para(X2655,X2656,skolem0003,skolem0002),inference(resolution,[status(thm)],[c385, c1116])).
% 47.14/47.32 cnf(c6491,plain,para(skolem0002,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1444, c5915])).
% 47.14/47.32 cnf(c6574,plain,para(skolem0003,skolem0002,skolem0002,skolem0002),inference(resolution,[status(thm)],[c6491, c397])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c264,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])).
% 47.14/47.32 fof(c265,plain,(![X269]:(![X270]:(![X271]:(![X272]:(![X273]:((~midp(X272,X269,X270)|~midp(X273,X269,X271))|para(X272,X273,X270,X271))))))),inference(variable_rename,[status(thm)],[c264])).
% 47.14/47.32 cnf(c266,plain,~midp(X1047,X1045,X1043)|~midp(X1044,X1045,X1046)|para(X1047,X1044,X1043,X1046),inference(split_conjunct,[status(thm)],[c265])).
% 47.14/47.32 cnf(c1212,plain,~midp(X1073,X1074,X1072)|para(X1073,X1073,X1072,X1072),inference(factor,[status(thm)],[c266])).
% 47.14/47.32 cnf(c1242,plain,para(skolem0004,skolem0004,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1212, c16])).
% 47.14/47.32 cnf(c1264,plain,para(skolem0002,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1242, c397])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c392,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])).
% 47.14/47.32 fof(c393,plain,(![X509]:(![X510]:(![X511]:(![X512]:(![X513]:(![X514]:((~para(X509,X510,X511,X512)|~para(X511,X512,X513,X514))|para(X509,X510,X513,X514)))))))),inference(variable_rename,[status(thm)],[c392])).
% 47.14/47.32 cnf(c394,plain,~para(X1288,X1287,X1290,X1289)|~para(X1290,X1289,X1291,X1292)|para(X1288,X1287,X1291,X1292),inference(split_conjunct,[status(thm)],[c393])).
% 47.14/47.32 cnf(c1467,plain,~para(X2680,X2679,skolem0002,skolem0002)|para(X2680,X2679,skolem0004,skolem0004),inference(resolution,[status(thm)],[c394, c1264])).
% 47.14/47.32 cnf(c6701,plain,para(skolem0003,skolem0002,skolem0004,skolem0004),inference(resolution,[status(thm)],[c1467, c6574])).
% 47.14/47.32 cnf(c6778,plain,perp(skolem0003,skolem0002,skolem0003,skolem0002),inference(resolution,[status(thm)],[c6701, c1432])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c160,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])).
% 47.14/47.32 fof(c161,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)],[c160])).
% 47.14/47.32 fof(c163,plain,(![X127]:(![X128]:(![X129]:(![X130]:(![X131]:(![X132]:(![X133]:(![X134]:((~eqangle(X127,X128,X129,X130,X131,X132,X133,X134)|~perp(X131,X132,X133,X134))|perp(X127,X128,X129,X130)))))))))),inference(shift_quantors,[status(thm)],[fof(c162,plain,(![X127]:(![X128]:(![X129]:(![X130]:((![X131]:(![X132]:(![X133]:(![X134]:(~eqangle(X127,X128,X129,X130,X131,X132,X133,X134)|~perp(X131,X132,X133,X134))))))|perp(X127,X128,X129,X130)))))),inference(variable_rename,[status(thm)],[c161])).])).
% 47.14/47.32 cnf(c164,plain,~eqangle(X912,X911,X909,X910,X906,X913,X907,X908)|~perp(X906,X913,X907,X908)|perp(X912,X911,X909,X910),inference(split_conjunct,[status(thm)],[c163])).
% 47.14/47.32 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)).
% 47.14/47.32 fof(c345,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])).
% 47.14/47.32 fof(c346,plain,(![X428]:(![X429]:(![X430]:(![X431]:(![X432]:(![X433]:(![X434]:(![X435]:(~eqangle(X428,X429,X430,X431,X432,X433,X434,X435)|eqangle(X428,X429,X432,X433,X430,X431,X434,X435)))))))))),inference(variable_rename,[status(thm)],[c345])).
% 47.14/47.32 cnf(c347,plain,~eqangle(X1214,X1219,X1216,X1213,X1217,X1212,X1215,X1218)|eqangle(X1214,X1219,X1217,X1212,X1216,X1213,X1215,X1218),inference(split_conjunct,[status(thm)],[c346])).
% 47.14/47.32 cnf(c9728,plain,eqangle(X5201,X5200,X5202,X5199,X5201,X5200,X5202,X5199),inference(resolution,[status(thm)],[c9698, c286])).
% 47.14/47.32 cnf(c17307,plain,eqangle(X5754,X5755,X5754,X5755,X5753,X5756,X5753,X5756),inference(resolution,[status(thm)],[c9728, c347])).
% 47.14/47.32 cnf(c18830,plain,~perp(X7321,X7320,X7321,X7320)|perp(X7318,X7319,X7318,X7319),inference(resolution,[status(thm)],[c17307, c164])).
% 47.14/47.32 cnf(c20719,plain,perp(X7323,X7322,X7323,X7322),inference(resolution,[status(thm)],[c18830, c6778])).
% 47.14/47.32 cnf(c20746,plain,perp(X7360,X7359,X7359,X7360),inference(resolution,[status(thm)],[c20719, c391])).
% 47.14/47.32 cnf(c20783,plain,~midp(X7522,X7521,X7521)|cong(X7521,X7522,X7523,X7522),inference(resolution,[status(thm)],[c20746, c241])).
% 47.14/47.32 cnf(c21055,plain,cong(X7524,skolem0004,X7525,skolem0004),inference(resolution,[status(thm)],[c20783, c17331])).
% 47.14/47.32 cnf(c21068,plain,perp(X7527,X7526,skolem0004,skolem0004),inference(resolution,[status(thm)],[c21055, c1080])).
% 47.14/47.32 cnf(c21103,plain,para(X7546,X7547,skolem0002,skolem0003),inference(resolution,[status(thm)],[c21068, c1443])).
% 47.14/47.32 cnf(c21159,plain,para(skolem0002,skolem0003,X7572,X7571),inference(resolution,[status(thm)],[c21103, c397])).
% 47.14/47.32 cnf(c21238,plain,$false,inference(resolution,[status(thm)],[c21159, c24])).
% 47.14/47.32 % SZS output end CNFRefutation
% 47.14/47.32
% 47.14/47.32 % Initial clauses : 136
% 47.14/47.32 % Processed clauses : 2626
% 47.14/47.32 % Factors computed : 181
% 47.14/47.32 % Resolvents computed: 20653
% 47.14/47.32 % Tautologies deleted: 21
% 47.14/47.32 % Forward subsumed : 6210
% 47.14/47.32 % Backward subsumed : 1517
% 47.14/47.32 % -------- CPU Time ---------
% 47.14/47.32 % User time : 46.929 s
% 47.14/47.32 % System time : 0.049 s
% 47.14/47.32 % Total time : 46.978 s
%------------------------------------------------------------------------------