%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO626+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 252.82s 253.08s
% Output : Refutation 252.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO626+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n020.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Thu May 9 08:18:38 EDT 2024
% 0.13/0.36 % CPUTime :
% 252.82/253.08 % Version: 1.5
% 252.82/253.08 % SZS status Theorem
% 252.82/253.08 % SZS output start CNFRefutation
% 252.82/253.08 fof(exemplo6GDDFULL8110990,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![G]:(![F]:(![C1]:(![B1]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:((((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(G,D,A,B))&coll(G,A,B))&perp(F,D,A,C))&coll(F,A,C))&circle(O,D,C1,NWPNT2))&coll(C1,D,G))&circle(O,D,B1,NWPNT3))&coll(B1,D,F))=>para(C1,C,B1,B)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL8110990)).
% 252.82/253.08 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![G]:(![F]:(![C1]:(![B1]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:((((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(G,D,A,B))&coll(G,A,B))&perp(F,D,A,C))&coll(F,A,C))&circle(O,D,C1,NWPNT2))&coll(C1,D,G))&circle(O,D,B1,NWPNT3))&coll(B1,D,F))=>para(C1,C,B1,B))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110990])).
% 252.82/253.08 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[G]:(?[F]:(?[C1]:(?[B1]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:((((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(G,D,A,B))&coll(G,A,B))&perp(F,D,A,C))&coll(F,A,C))&circle(O,D,C1,NWPNT2))&coll(C1,D,G))&circle(O,D,B1,NWPNT3))&coll(B1,D,F))&~para(C1,C,B1,B)))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 252.82/253.08 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[G]:(?[F]:(?[C1]:(?[B1]:((((((((((circle(O,A,B,C)&(?[NWPNT1]:circle(O,A,D,NWPNT1)))&perp(G,D,A,B))&coll(G,A,B))&perp(F,D,A,C))&coll(F,A,C))&(?[NWPNT2]:circle(O,D,C1,NWPNT2)))&coll(C1,D,G))&(?[NWPNT3]:circle(O,D,B1,NWPNT3)))&coll(B1,D,F))&~para(C1,C,B1,B))))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 252.82/253.08 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:((((((((((circle(X5,X2,X3,X4)&(?[X11]:circle(X5,X2,X6,X11)))&perp(X7,X6,X2,X3))&coll(X7,X2,X3))&perp(X8,X6,X2,X4))&coll(X8,X2,X4))&(?[X12]:circle(X5,X6,X9,X12)))&coll(X9,X6,X7))&(?[X13]:circle(X5,X6,X10,X13)))&coll(X10,X6,X8))&~para(X9,X4,X10,X3))))))))))),inference(variable_rename,[status(thm)],[c13])).
% 252.82/253.08 fof(c15,negated_conjecture,((((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0010))&perp(skolem0006,skolem0005,skolem0001,skolem0002))&coll(skolem0006,skolem0001,skolem0002))&perp(skolem0007,skolem0005,skolem0001,skolem0003))&coll(skolem0007,skolem0001,skolem0003))&circle(skolem0004,skolem0005,skolem0008,skolem0011))&coll(skolem0008,skolem0005,skolem0006))&circle(skolem0004,skolem0005,skolem0009,skolem0012))&coll(skolem0009,skolem0005,skolem0007))&~para(skolem0008,skolem0003,skolem0009,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 252.82/253.08 cnf(c26,negated_conjecture,~para(skolem0008,skolem0003,skolem0009,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 252.82/253.08 fof(ruleD3,axiom,(![A]:(![B]:(![C]:(![D]:((coll(A,B,C)&coll(A,B,D))=>coll(C,D,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD3)).
% 252.82/253.08 fof(c403,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 252.82/253.08 fof(c404,plain,(![X525]:(![X526]:(![X527]:(![X528]:((~coll(X525,X526,X527)|~coll(X525,X526,X528))|coll(X527,X528,X525)))))),inference(variable_rename,[status(thm)],[c403])).
% 252.82/253.08 cnf(c405,plain,~coll(X761,X764,X762)|~coll(X761,X764,X763)|coll(X762,X763,X761),inference(split_conjunct,[status(thm)],[c404])).
% 252.82/253.08 cnf(c541,plain,~coll(X766,X767,X765)|coll(X765,X765,X766),inference(factor,[status(thm)],[c405])).
% 252.82/253.08 fof(ruleD66,axiom,(![A]:(![B]:(![C]:(para(A,B,A,C)=>coll(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD66)).
% 252.82/253.08 fof(c192,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 252.82/253.08 fof(c193,plain,(![X168]:(![X169]:(![X170]:(~para(X168,X169,X168,X170)|coll(X168,X169,X170))))),inference(variable_rename,[status(thm)],[c192])).
% 252.82/253.08 cnf(c194,plain,~para(X675,X676,X675,X674)|coll(X675,X676,X674),inference(split_conjunct,[status(thm)],[c193])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c289,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])).
% 252.82/253.08 fof(c290,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)],[c289])).
% 252.82/253.08 fof(c292,plain,(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(![X305]:(~eqangle(X300,X301,X304,X305,X302,X303,X304,X305)|para(X300,X301,X302,X303)))))))),inference(shift_quantors,[status(thm)],[fof(c291,plain,(![X300]:(![X301]:(![X302]:(![X303]:((![X304]:(![X305]:~eqangle(X300,X301,X304,X305,X302,X303,X304,X305)))|para(X300,X301,X302,X303)))))),inference(variable_rename,[status(thm)],[c290])).])).
% 252.82/253.08 cnf(c293,plain,~eqangle(X1087,X1084,X1086,X1083,X1085,X1082,X1086,X1083)|para(X1087,X1084,X1085,X1082),inference(split_conjunct,[status(thm)],[c292])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c353,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])).
% 252.82/253.08 fof(c354,plain,(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(![X451]:(![X452]:(![X453]:(~eqangle(X446,X447,X448,X449,X450,X451,X452,X453)|eqangle(X448,X449,X446,X447,X452,X453,X450,X451)))))))))),inference(variable_rename,[status(thm)],[c353])).
% 252.82/253.08 cnf(c355,plain,~eqangle(X1238,X1240,X1241,X1237,X1239,X1243,X1242,X1236)|eqangle(X1241,X1237,X1238,X1240,X1242,X1236,X1239,X1243),inference(split_conjunct,[status(thm)],[c354])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c284,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])).
% 252.82/253.08 fof(c285,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)],[c284])).
% 252.82/253.08 fof(c287,plain,(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(![X299]:(~para(X294,X295,X296,X297)|eqangle(X294,X295,X298,X299,X296,X297,X298,X299)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X294]:(![X295]:(![X296]:(![X297]:(~para(X294,X295,X296,X297)|(![X298]:(![X299]:eqangle(X294,X295,X298,X299,X296,X297,X298,X299)))))))),inference(variable_rename,[status(thm)],[c285])).])).
% 252.82/253.08 cnf(c288,plain,~para(X1078,X1079,X1080,X1075)|eqangle(X1078,X1079,X1076,X1077,X1080,X1075,X1076,X1077),inference(split_conjunct,[status(thm)],[c287])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 252.82/253.08 fof(c392,plain,(![X507]:(![X508]:(![X509]:(![X510]:(~perp(X507,X508,X509,X510)|perp(X507,X508,X510,X509)))))),inference(variable_rename,[status(thm)],[c391])).
% 252.82/253.08 cnf(c393,plain,~perp(X713,X714,X716,X715)|perp(X713,X714,X715,X716),inference(split_conjunct,[status(thm)],[c392])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 252.82/253.08 fof(c389,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X505,X506,X503,X504)))))),inference(variable_rename,[status(thm)],[c388])).
% 252.82/253.08 cnf(c390,plain,~perp(X707,X706,X708,X709)|perp(X708,X709,X707,X706),inference(split_conjunct,[status(thm)],[c389])).
% 252.82/253.08 cnf(c18,negated_conjecture,perp(skolem0006,skolem0005,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 252.82/253.08 cnf(c500,plain,perp(skolem0006,skolem0005,skolem0002,skolem0001),inference(resolution,[status(thm)],[c393, c18])).
% 252.82/253.08 cnf(c507,plain,perp(skolem0002,skolem0001,skolem0006,skolem0005),inference(resolution,[status(thm)],[c500, c390])).
% 252.82/253.08 cnf(c519,plain,perp(skolem0002,skolem0001,skolem0005,skolem0006),inference(resolution,[status(thm)],[c507, c393])).
% 252.82/253.08 cnf(c493,plain,perp(skolem0001,skolem0002,skolem0006,skolem0005),inference(resolution,[status(thm)],[c390, c18])).
% 252.82/253.08 cnf(c502,plain,perp(skolem0001,skolem0002,skolem0005,skolem0006),inference(resolution,[status(thm)],[c393, c493])).
% 252.82/253.08 cnf(c513,plain,perp(skolem0005,skolem0006,skolem0001,skolem0002),inference(resolution,[status(thm)],[c502, c390])).
% 252.82/253.08 cnf(c525,plain,perp(skolem0005,skolem0006,skolem0002,skolem0001),inference(resolution,[status(thm)],[c513, c393])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c385,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])).
% 252.82/253.08 fof(c386,plain,(![X497]:(![X498]:(![X499]:(![X500]:(![X501]:(![X502]:((~perp(X497,X498,X499,X500)|~perp(X499,X500,X501,X502))|para(X497,X498,X501,X502)))))))),inference(variable_rename,[status(thm)],[c385])).
% 252.82/253.08 cnf(c387,plain,~perp(X1276,X1273,X1274,X1277)|~perp(X1274,X1277,X1272,X1275)|para(X1276,X1273,X1272,X1275),inference(split_conjunct,[status(thm)],[c386])).
% 252.82/253.08 cnf(c1478,plain,~perp(X2552,X2553,skolem0005,skolem0006)|para(X2552,X2553,skolem0002,skolem0001),inference(resolution,[status(thm)],[c387, c525])).
% 252.82/253.08 cnf(c6666,plain,para(skolem0002,skolem0001,skolem0002,skolem0001),inference(resolution,[status(thm)],[c1478, c519])).
% 252.82/253.08 cnf(c6697,plain,eqangle(skolem0002,skolem0001,X5740,X5741,skolem0002,skolem0001,X5740,X5741),inference(resolution,[status(thm)],[c6666, c288])).
% 252.82/253.08 cnf(c16137,plain,eqangle(X7545,X7544,skolem0002,skolem0001,X7545,X7544,skolem0002,skolem0001),inference(resolution,[status(thm)],[c6697, c355])).
% 252.82/253.08 cnf(c19027,plain,para(X7546,X7547,X7546,X7547),inference(resolution,[status(thm)],[c16137, c293])).
% 252.82/253.08 cnf(c19083,plain,coll(X7548,X7549,X7549),inference(resolution,[status(thm)],[c19027, c194])).
% 252.82/253.08 cnf(c19693,plain,coll(X7555,X7555,X7556),inference(resolution,[status(thm)],[c19083, c541])).
% 252.82/253.08 cnf(c21157,plain,~coll(X11050,X11050,X11049)|coll(X11049,X11051,X11050),inference(resolution,[status(thm)],[c19693, c405])).
% 252.82/253.08 cnf(c34819,plain,coll(X11059,X11061,X11060),inference(resolution,[status(thm)],[c21157, c19693])).
% 252.82/253.08 fof(ruleD67,axiom,(![A]:(![B]:(![C]:((cong(A,B,A,C)&coll(A,B,C))=>midp(A,B,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD67)).
% 252.82/253.08 fof(c189,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 252.82/253.08 fof(c190,plain,(![X165]:(![X166]:(![X167]:((~cong(X165,X166,X165,X167)|~coll(X165,X166,X167))|midp(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c189])).
% 252.82/253.08 cnf(c191,plain,~cong(X938,X939,X938,X940)|~coll(X938,X939,X940)|midp(X938,X939,X940),inference(split_conjunct,[status(thm)],[c190])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c341,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 252.82/253.08 fof(c342,plain,(![X414]:(![X415]:(![X416]:(![X417]:(~cong(X414,X415,X416,X417)|cong(X414,X415,X417,X416)))))),inference(variable_rename,[status(thm)],[c341])).
% 252.82/253.08 cnf(c343,plain,~cong(X690,X687,X688,X689)|cong(X690,X687,X689,X688),inference(split_conjunct,[status(thm)],[c342])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 252.82/253.08 fof(c339,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X412,X413,X410,X411)))))),inference(variable_rename,[status(thm)],[c338])).
% 252.82/253.08 cnf(c340,plain,~cong(X685,X684,X683,X686)|cong(X683,X686,X685,X684),inference(split_conjunct,[status(thm)],[c339])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c198,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])).
% 252.82/253.08 fof(c199,plain,(![X176]:(![X177]:(![X178]:(![X179]:(![X180]:(((~midp(X180,X176,X177)|~para(X176,X178,X177,X179))|~para(X176,X179,X177,X178))|midp(X180,X178,X179))))))),inference(variable_rename,[status(thm)],[c198])).
% 252.82/253.08 cnf(c200,plain,~midp(X948,X950,X946)|~para(X950,X947,X946,X949)|~para(X950,X949,X946,X947)|midp(X948,X947,X949),inference(split_conjunct,[status(thm)],[c199])).
% 252.82/253.08 cnf(c1176,plain,~midp(X2245,X2246,X2244)|~para(X2246,X2247,X2244,X2247)|midp(X2245,X2247,X2247),inference(factor,[status(thm)],[c200])).
% 252.82/253.08 cnf(c19066,plain,~midp(X10659,X10660,X10660)|midp(X10659,X10661,X10661),inference(resolution,[status(thm)],[c19027, c1176])).
% 252.82/253.08 fof(ruleD42b,axiom,(![A]:(![B]:(![P]:(![Q]:((eqangle(P,A,P,B,Q,A,Q,B)&coll(P,Q,B))=>cyclic(A,B,P,Q)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD42b)).
% 252.82/253.08 fof(c274,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])).
% 252.82/253.08 fof(c275,plain,(![X282]:(![X283]:(![X284]:(![X285]:((~eqangle(X284,X282,X284,X283,X285,X282,X285,X283)|~coll(X284,X285,X283))|cyclic(X282,X283,X284,X285)))))),inference(variable_rename,[status(thm)],[c274])).
% 252.82/253.08 cnf(c276,plain,~eqangle(X1062,X1060,X1062,X1061,X1059,X1060,X1059,X1061)|~coll(X1062,X1059,X1061)|cyclic(X1060,X1061,X1062,X1059),inference(split_conjunct,[status(thm)],[c275])).
% 252.82/253.08 cnf(c19068,plain,eqangle(X10663,X10664,X10662,X10665,X10663,X10664,X10662,X10665),inference(resolution,[status(thm)],[c19027, c288])).
% 252.82/253.08 cnf(c34195,plain,~coll(X11521,X11521,X11520)|cyclic(X11519,X11520,X11521,X11521),inference(resolution,[status(thm)],[c19068, c276])).
% 252.82/253.08 cnf(c35726,plain,cyclic(X11522,X11524,X11523,X11523),inference(resolution,[status(thm)],[c34195, c34819])).
% 252.82/253.08 fof(ruleD43,axiom,(![A]:(![B]:(![C]:(![P]:(![Q]:(![R]:((((cyclic(A,B,C,P)&cyclic(A,B,C,Q))&cyclic(A,B,C,R))&eqangle(C,A,C,B,R,P,R,Q))=>cong(A,B,P,Q)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD43)).
% 252.82/253.08 fof(c269,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])).
% 252.82/253.08 fof(c270,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)],[c269])).
% 252.82/253.08 fof(c272,plain,(![X276]:(![X277]:(![X278]:(![X279]:(![X280]:(![X281]:((((~cyclic(X276,X277,X278,X279)|~cyclic(X276,X277,X278,X280))|~cyclic(X276,X277,X278,X281))|~eqangle(X278,X276,X278,X277,X281,X279,X281,X280))|cong(X276,X277,X279,X280)))))))),inference(shift_quantors,[status(thm)],[fof(c271,plain,(![X276]:(![X277]:(![X278]:(![X279]:(![X280]:((![X281]:(((~cyclic(X276,X277,X278,X279)|~cyclic(X276,X277,X278,X280))|~cyclic(X276,X277,X278,X281))|~eqangle(X278,X276,X278,X277,X281,X279,X281,X280)))|cong(X276,X277,X279,X280))))))),inference(variable_rename,[status(thm)],[c270])).])).
% 252.82/253.08 cnf(c273,plain,~cyclic(X1055,X1053,X1052,X1054)|~cyclic(X1055,X1053,X1052,X1057)|~cyclic(X1055,X1053,X1052,X1056)|~eqangle(X1052,X1055,X1052,X1053,X1056,X1054,X1056,X1057)|cong(X1055,X1053,X1054,X1057),inference(split_conjunct,[status(thm)],[c272])).
% 252.82/253.08 fof(ruleD20,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(P,Q,U,V,A,B,C,D)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 252.82/253.08 fof(c350,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(P,Q,U,V,A,B,C,D)))))))))),inference(fof_nnf,[status(thm)],[ruleD20])).
% 252.82/253.08 fof(c351,plain,(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(![X445]:(~eqangle(X438,X439,X440,X441,X442,X443,X444,X445)|eqangle(X442,X443,X444,X445,X438,X439,X440,X441)))))))))),inference(variable_rename,[status(thm)],[c350])).
% 252.82/253.08 cnf(c352,plain,~eqangle(X1228,X1233,X1232,X1234,X1230,X1229,X1231,X1235)|eqangle(X1230,X1229,X1231,X1235,X1228,X1233,X1232,X1234),inference(split_conjunct,[status(thm)],[c351])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c347,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])).
% 252.82/253.08 fof(c348,plain,(![X430]:(![X431]:(![X432]:(![X433]:(![X434]:(![X435]:(![X436]:(![X437]:(~eqangle(X430,X431,X432,X433,X434,X435,X436,X437)|eqangle(X430,X431,X434,X435,X432,X433,X436,X437)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 252.82/253.08 cnf(c349,plain,~eqangle(X1227,X1225,X1220,X1226,X1221,X1223,X1224,X1222)|eqangle(X1227,X1225,X1221,X1223,X1220,X1226,X1224,X1222),inference(split_conjunct,[status(thm)],[c348])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 252.82/253.08 fof(c401,plain,(![X521]:(![X522]:(![X523]:(![X524]:(~para(X521,X522,X523,X524)|para(X521,X522,X524,X523)))))),inference(variable_rename,[status(thm)],[c400])).
% 252.82/253.08 cnf(c402,plain,~para(X751,X752,X753,X754)|para(X751,X752,X754,X753),inference(split_conjunct,[status(thm)],[c401])).
% 252.82/253.08 cnf(c19060,plain,para(X7571,X7572,X7572,X7571),inference(resolution,[status(thm)],[c19027, c402])).
% 252.82/253.08 cnf(c21429,plain,eqangle(X11300,X11299,X11298,X11301,X11299,X11300,X11298,X11301),inference(resolution,[status(thm)],[c19060, c288])).
% 252.82/253.08 cnf(c35380,plain,eqangle(X11335,X11334,X11334,X11335,X11337,X11336,X11337,X11336),inference(resolution,[status(thm)],[c21429, c349])).
% 252.82/253.08 cnf(c35462,plain,eqangle(X11393,X11395,X11393,X11395,X11396,X11394,X11394,X11396),inference(resolution,[status(thm)],[c35380, c352])).
% 252.82/253.08 cnf(c35532,plain,~cyclic(X12599,X12599,X12597,X12598)|cong(X12599,X12599,X12598,X12598),inference(resolution,[status(thm)],[c35462, c273])).
% 252.82/253.08 cnf(c36293,plain,cong(X12600,X12600,X12601,X12601),inference(resolution,[status(thm)],[c35532, c35726])).
% 252.82/253.08 cnf(c36318,plain,~coll(X12655,X12655,X12655)|midp(X12655,X12655,X12655),inference(resolution,[status(thm)],[c36293, c191])).
% 252.82/253.08 cnf(c36433,plain,midp(X12659,X12659,X12659),inference(resolution,[status(thm)],[c36318, c34819])).
% 252.82/253.08 cnf(c36725,plain,midp(X12662,X12661,X12661),inference(resolution,[status(thm)],[c36433, c19066])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c241,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])).
% 252.82/253.08 fof(c242,plain,(![X236]:(![X237]:(![X238]:(![X239]:((~perp(X236,X237,X237,X238)|~midp(X239,X236,X238))|cong(X236,X239,X237,X239)))))),inference(variable_rename,[status(thm)],[c241])).
% 252.82/253.08 cnf(c243,plain,~perp(X1000,X1003,X1003,X1002)|~midp(X1001,X1000,X1002)|cong(X1000,X1001,X1003,X1001),inference(split_conjunct,[status(thm)],[c242])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c162,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])).
% 252.82/253.08 fof(c163,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)],[c162])).
% 252.82/253.08 fof(c165,plain,(![X129]:(![X130]:(![X131]:(![X132]:(![X133]:(![X134]:(![X135]:(![X136]:((~eqangle(X129,X130,X131,X132,X133,X134,X135,X136)|~perp(X133,X134,X135,X136))|perp(X129,X130,X131,X132)))))))))),inference(shift_quantors,[status(thm)],[fof(c164,plain,(![X129]:(![X130]:(![X131]:(![X132]:((![X133]:(![X134]:(![X135]:(![X136]:(~eqangle(X129,X130,X131,X132,X133,X134,X135,X136)|~perp(X133,X134,X135,X136))))))|perp(X129,X130,X131,X132)))))),inference(variable_rename,[status(thm)],[c163])).])).
% 252.82/253.08 cnf(c166,plain,~eqangle(X911,X908,X909,X913,X910,X914,X912,X915)|~perp(X910,X914,X912,X915)|perp(X911,X908,X909,X913),inference(split_conjunct,[status(thm)],[c165])).
% 252.82/253.08 cnf(c35458,plain,~perp(X12578,X12576,X12578,X12576)|perp(X12577,X12575,X12575,X12577),inference(resolution,[status(thm)],[c35380, c166])).
% 252.82/253.08 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)).
% 252.82/253.08 fof(c227,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])).
% 252.82/253.08 fof(c228,plain,(![X220]:(![X221]:(![X222]:(![X223]:((~cong(X220,X222,X221,X222)|~cong(X220,X223,X221,X223))|perp(X220,X221,X222,X223)))))),inference(variable_rename,[status(thm)],[c227])).
% 252.82/253.08 cnf(c229,plain,~cong(X987,X985,X986,X985)|~cong(X987,X984,X986,X984)|perp(X987,X986,X985,X984),inference(split_conjunct,[status(thm)],[c228])).
% 252.82/253.08 cnf(c1179,plain,~cong(X1035,X1033,X1034,X1033)|perp(X1035,X1034,X1033,X1033),inference(factor,[status(thm)],[c229])).
% 252.82/253.08 cnf(c36321,plain,perp(X12621,X12621,X12621,X12621),inference(resolution,[status(thm)],[c36293, c1179])).
% 252.82/253.08 cnf(c36338,plain,perp(X12630,X12629,X12629,X12630),inference(resolution,[status(thm)],[c36321, c35458])).
% 252.82/253.08 cnf(c36373,plain,~midp(X13543,X13544,X13544)|cong(X13544,X13543,X13545,X13543),inference(resolution,[status(thm)],[c36338, c243])).
% 252.82/253.08 cnf(c39054,plain,cong(X13550,X13548,X13549,X13548),inference(resolution,[status(thm)],[c36373, c36725])).
% 252.82/253.08 cnf(c39076,plain,cong(X13556,X13557,X13557,X13558),inference(resolution,[status(thm)],[c39054, c343])).
% 252.82/253.08 cnf(c39081,plain,cong(X13567,X13566,X13565,X13567),inference(resolution,[status(thm)],[c39076, c340])).
% 252.82/253.08 cnf(c39138,plain,cong(X13593,X13592,X13593,X13594),inference(resolution,[status(thm)],[c39081, c343])).
% 252.82/253.08 cnf(c39208,plain,~coll(X13821,X13823,X13822)|midp(X13821,X13823,X13822),inference(resolution,[status(thm)],[c39138, c191])).
% 252.82/253.08 cnf(c42404,plain,midp(X13827,X13826,X13828),inference(resolution,[status(thm)],[c39208, c34819])).
% 252.82/253.08 fof(ruleD44,axiom,(![A]:(![B]:(![C]:(![E]:(![F]:((midp(E,A,B)&midp(F,A,C))=>para(E,F,B,C))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD44)).
% 252.82/253.08 fof(c266,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])).
% 252.82/253.08 fof(c267,plain,(![X271]:(![X272]:(![X273]:(![X274]:(![X275]:((~midp(X274,X271,X272)|~midp(X275,X271,X273))|para(X274,X275,X272,X273))))))),inference(variable_rename,[status(thm)],[c266])).
% 252.82/253.08 cnf(c268,plain,~midp(X1046,X1045,X1044)|~midp(X1047,X1045,X1043)|para(X1046,X1047,X1044,X1043),inference(split_conjunct,[status(thm)],[c267])).
% 252.82/253.08 cnf(c37262,plain,~midp(X17150,X17147,X17148)|para(X17150,X17149,X17148,X17147),inference(resolution,[status(thm)],[c36725, c268])).
% 252.82/253.08 cnf(c45569,plain,para(X17157,X17156,X17155,X17154),inference(resolution,[status(thm)],[c37262, c42404])).
% 252.82/253.08 cnf(c45575,plain,$false,inference(resolution,[status(thm)],[c45569, c26])).
% 252.82/253.08 % SZS output end CNFRefutation
% 252.82/253.08
% 252.82/253.08 % Initial clauses : 138
% 252.82/253.08 % Processed clauses : 5309
% 252.82/253.08 % Factors computed : 246
% 252.82/253.08 % Resolvents computed: 44937
% 252.82/253.08 % Tautologies deleted: 28
% 252.82/253.08 % Forward subsumed : 15568
% 252.82/253.08 % Backward subsumed : 4822
% 252.82/253.08 % -------- CPU Time ---------
% 252.82/253.08 % User time : 252.599 s
% 252.82/253.08 % System time : 0.093 s
% 252.82/253.08 % Total time : 252.692 s
%------------------------------------------------------------------------------