%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO654+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:30 EDT 2024
% Result : Theorem 136.74s 136.90s
% Output : Refutation 136.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO654+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 : n018.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:43:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 136.74/136.90 % Version: 1.5
% 136.74/136.90 % SZS status Theorem
% 136.74/136.90 % SZS output start CNFRefutation
% 136.74/136.90 fof(exemplo6GDDFULLmoreE0228,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:((((((((((circle(A,B,NWPNT1,NWPNT2)&circle(C,B,NWPNT3,NWPNT4))&circle(A,B,D,NWPNT5))&circle(C,B,D,NWPNT6))&circle(C,B,E,NWPNT7))&coll(D,E,F))&circle(A,D,F,NWPNT8))&coll(B,E,G))&circle(A,B,G,NWPNT9))&perp(C,E,E,H))=>para(H,E,G,F))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULLmoreE0228)).
% 136.74/136.90 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(![NWPNT5]:(![NWPNT6]:(![NWPNT7]:(![NWPNT8]:(![NWPNT9]:((((((((((circle(A,B,NWPNT1,NWPNT2)&circle(C,B,NWPNT3,NWPNT4))&circle(A,B,D,NWPNT5))&circle(C,B,D,NWPNT6))&circle(C,B,E,NWPNT7))&coll(D,E,F))&circle(A,D,F,NWPNT8))&coll(B,E,G))&circle(A,B,G,NWPNT9))&perp(C,E,E,H))=>para(H,E,G,F)))))))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE0228])).
% 136.74/136.90 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(?[NWPNT5]:(?[NWPNT6]:(?[NWPNT7]:(?[NWPNT8]:(?[NWPNT9]:((((((((((circle(A,B,NWPNT1,NWPNT2)&circle(C,B,NWPNT3,NWPNT4))&circle(A,B,D,NWPNT5))&circle(C,B,D,NWPNT6))&circle(C,B,E,NWPNT7))&coll(D,E,F))&circle(A,D,F,NWPNT8))&coll(B,E,G))&circle(A,B,G,NWPNT9))&perp(C,E,E,H))&~para(H,E,G,F))))))))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 136.74/136.90 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(((((((((((?[NWPNT1]:(?[NWPNT2]:circle(A,B,NWPNT1,NWPNT2)))&(?[NWPNT3]:(?[NWPNT4]:circle(C,B,NWPNT3,NWPNT4))))&(?[NWPNT5]:circle(A,B,D,NWPNT5)))&(?[NWPNT6]:circle(C,B,D,NWPNT6)))&(?[NWPNT7]:circle(C,B,E,NWPNT7)))&coll(D,E,F))&(?[NWPNT8]:circle(A,D,F,NWPNT8)))&coll(B,E,G))&(?[NWPNT9]:circle(A,B,G,NWPNT9)))&perp(C,E,E,H))&~para(H,E,G,F)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 136.74/136.90 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((((?[X10]:(?[X11]:circle(X2,X3,X10,X11)))&(?[X12]:(?[X13]:circle(X4,X3,X12,X13))))&(?[X14]:circle(X2,X3,X5,X14)))&(?[X15]:circle(X4,X3,X5,X15)))&(?[X16]:circle(X4,X3,X6,X16)))&coll(X5,X6,X7))&(?[X17]:circle(X2,X5,X7,X17)))&coll(X3,X6,X8))&(?[X18]:circle(X2,X3,X8,X18)))&perp(X4,X6,X6,X9))&~para(X9,X6,X8,X7)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 136.74/136.90 fof(c15,negated_conjecture,((((((((((circle(skolem0001,skolem0002,skolem0009,skolem0010)&circle(skolem0003,skolem0002,skolem0011,skolem0012))&circle(skolem0001,skolem0002,skolem0004,skolem0013))&circle(skolem0003,skolem0002,skolem0004,skolem0014))&circle(skolem0003,skolem0002,skolem0005,skolem0015))&coll(skolem0004,skolem0005,skolem0006))&circle(skolem0001,skolem0004,skolem0006,skolem0016))&coll(skolem0002,skolem0005,skolem0007))&circle(skolem0001,skolem0002,skolem0007,skolem0017))&perp(skolem0003,skolem0005,skolem0005,skolem0008))&~para(skolem0008,skolem0005,skolem0007,skolem0006)),inference(skolemize,[status(esa)],[c14])).
% 136.74/136.90 cnf(c26,negated_conjecture,~para(skolem0008,skolem0005,skolem0007,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c404,plain,(![X530]:(![X531]:(![X532]:(![X533]:((~coll(X530,X531,X532)|~coll(X530,X531,X533))|coll(X532,X533,X530)))))),inference(variable_rename,[status(thm)],[c403])).
% 136.74/136.90 cnf(c405,plain,~coll(X730,X731,X732)|~coll(X730,X731,X733)|coll(X732,X733,X730),inference(split_conjunct,[status(thm)],[c404])).
% 136.74/136.90 cnf(c482,plain,~coll(X734,X736,X735)|coll(X735,X735,X734),inference(factor,[status(thm)],[c405])).
% 136.74/136.90 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)).
% 136.74/136.90 fof(c192,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 136.74/136.90 fof(c193,plain,(![X173]:(![X174]:(![X175]:(~para(X173,X174,X173,X175)|coll(X173,X174,X175))))),inference(variable_rename,[status(thm)],[c192])).
% 136.74/136.90 cnf(c194,plain,~para(X634,X633,X634,X635)|coll(X634,X633,X635),inference(split_conjunct,[status(thm)],[c193])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c292,plain,(![X305]:(![X306]:(![X307]:(![X308]:(![X309]:(![X310]:(~eqangle(X305,X306,X309,X310,X307,X308,X309,X310)|para(X305,X306,X307,X308)))))))),inference(shift_quantors,[status(thm)],[fof(c291,plain,(![X305]:(![X306]:(![X307]:(![X308]:((![X309]:(![X310]:~eqangle(X305,X306,X309,X310,X307,X308,X309,X310)))|para(X305,X306,X307,X308)))))),inference(variable_rename,[status(thm)],[c290])).])).
% 136.74/136.90 cnf(c293,plain,~eqangle(X1085,X1090,X1089,X1087,X1088,X1086,X1089,X1087)|para(X1085,X1090,X1088,X1086),inference(split_conjunct,[status(thm)],[c292])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c354,plain,(![X451]:(![X452]:(![X453]:(![X454]:(![X455]:(![X456]:(![X457]:(![X458]:(~eqangle(X451,X452,X453,X454,X455,X456,X457,X458)|eqangle(X453,X454,X451,X452,X457,X458,X455,X456)))))))))),inference(variable_rename,[status(thm)],[c353])).
% 136.74/136.90 cnf(c355,plain,~eqangle(X1225,X1224,X1229,X1227,X1230,X1228,X1223,X1226)|eqangle(X1229,X1227,X1225,X1224,X1223,X1226,X1230,X1228),inference(split_conjunct,[status(thm)],[c354])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c287,plain,(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(~para(X299,X300,X301,X302)|eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,(![X299]:(![X300]:(![X301]:(![X302]:(~para(X299,X300,X301,X302)|(![X303]:(![X304]:eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))))))),inference(variable_rename,[status(thm)],[c285])).])).
% 136.74/136.90 cnf(c288,plain,~para(X1079,X1080,X1082,X1081)|eqangle(X1079,X1080,X1084,X1083,X1082,X1081,X1084,X1083),inference(split_conjunct,[status(thm)],[c287])).
% 136.74/136.90 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)).
% 136.74/136.90 fof(c391,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 136.74/136.90 fof(c392,plain,(![X512]:(![X513]:(![X514]:(![X515]:(~perp(X512,X513,X514,X515)|perp(X512,X513,X515,X514)))))),inference(variable_rename,[status(thm)],[c391])).
% 136.74/136.90 cnf(c393,plain,~perp(X677,X676,X678,X679)|perp(X677,X676,X679,X678),inference(split_conjunct,[status(thm)],[c392])).
% 136.74/136.90 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)).
% 136.74/136.90 fof(c388,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 136.74/136.90 fof(c389,plain,(![X508]:(![X509]:(![X510]:(![X511]:(~perp(X508,X509,X510,X511)|perp(X510,X511,X508,X509)))))),inference(variable_rename,[status(thm)],[c388])).
% 136.74/136.90 cnf(c390,plain,~perp(X672,X674,X673,X675)|perp(X673,X675,X672,X674),inference(split_conjunct,[status(thm)],[c389])).
% 136.74/136.90 cnf(c25,negated_conjecture,perp(skolem0003,skolem0005,skolem0005,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 136.74/136.90 cnf(c463,plain,perp(skolem0003,skolem0005,skolem0008,skolem0005),inference(resolution,[status(thm)],[c393, c25])).
% 136.74/136.90 cnf(c468,plain,perp(skolem0008,skolem0005,skolem0003,skolem0005),inference(resolution,[status(thm)],[c463, c390])).
% 136.74/136.90 cnf(c473,plain,perp(skolem0008,skolem0005,skolem0005,skolem0003),inference(resolution,[status(thm)],[c468, c393])).
% 136.74/136.90 cnf(c459,plain,perp(skolem0005,skolem0008,skolem0003,skolem0005),inference(resolution,[status(thm)],[c390, c25])).
% 136.74/136.90 cnf(c462,plain,perp(skolem0005,skolem0008,skolem0005,skolem0003),inference(resolution,[status(thm)],[c393, c459])).
% 136.74/136.90 cnf(c465,plain,perp(skolem0005,skolem0003,skolem0005,skolem0008),inference(resolution,[status(thm)],[c462, c390])).
% 136.74/136.90 cnf(c470,plain,perp(skolem0005,skolem0003,skolem0008,skolem0005),inference(resolution,[status(thm)],[c465, c393])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c386,plain,(![X502]:(![X503]:(![X504]:(![X505]:(![X506]:(![X507]:((~perp(X502,X503,X504,X505)|~perp(X504,X505,X506,X507))|para(X502,X503,X506,X507)))))))),inference(variable_rename,[status(thm)],[c385])).
% 136.74/136.90 cnf(c387,plain,~perp(X1282,X1284,X1280,X1281)|~perp(X1280,X1281,X1279,X1283)|para(X1282,X1284,X1279,X1283),inference(split_conjunct,[status(thm)],[c386])).
% 136.74/136.90 cnf(c1407,plain,~perp(X2520,X2519,skolem0005,skolem0003)|para(X2520,X2519,skolem0008,skolem0005),inference(resolution,[status(thm)],[c387, c470])).
% 136.74/136.90 cnf(c5899,plain,para(skolem0008,skolem0005,skolem0008,skolem0005),inference(resolution,[status(thm)],[c1407, c473])).
% 136.74/136.90 cnf(c5920,plain,eqangle(skolem0008,skolem0005,X4022,X4023,skolem0008,skolem0005,X4022,X4023),inference(resolution,[status(thm)],[c5899, c288])).
% 136.74/136.90 cnf(c12088,plain,eqangle(X5314,X5313,skolem0008,skolem0005,X5314,X5313,skolem0008,skolem0005),inference(resolution,[status(thm)],[c5920, c355])).
% 136.74/136.90 cnf(c16289,plain,para(X5316,X5315,X5316,X5315),inference(resolution,[status(thm)],[c12088, c293])).
% 136.74/136.90 cnf(c16307,plain,coll(X5318,X5317,X5317),inference(resolution,[status(thm)],[c16289, c194])).
% 136.74/136.90 cnf(c16363,plain,coll(X5320,X5320,X5319),inference(resolution,[status(thm)],[c16307, c482])).
% 136.74/136.90 cnf(c17095,plain,~coll(X7599,X7599,X7598)|coll(X7598,X7597,X7599),inference(resolution,[status(thm)],[c16363, c405])).
% 136.74/136.90 cnf(c26653,plain,coll(X7607,X7609,X7608),inference(resolution,[status(thm)],[c17095, c16363])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c190,plain,(![X170]:(![X171]:(![X172]:((~cong(X170,X171,X170,X172)|~coll(X170,X171,X172))|midp(X170,X171,X172))))),inference(variable_rename,[status(thm)],[c189])).
% 136.74/136.90 cnf(c191,plain,~cong(X960,X959,X960,X961)|~coll(X960,X959,X961)|midp(X960,X959,X961),inference(split_conjunct,[status(thm)],[c190])).
% 136.74/136.90 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)).
% 136.74/136.90 fof(c341,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 136.74/136.90 fof(c342,plain,(![X419]:(![X420]:(![X421]:(![X422]:(~cong(X419,X420,X421,X422)|cong(X419,X420,X422,X421)))))),inference(variable_rename,[status(thm)],[c341])).
% 136.74/136.90 cnf(c343,plain,~cong(X643,X640,X641,X642)|cong(X643,X640,X642,X641),inference(split_conjunct,[status(thm)],[c342])).
% 136.74/136.90 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)).
% 136.74/136.90 fof(c338,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 136.74/136.90 fof(c339,plain,(![X415]:(![X416]:(![X417]:(![X418]:(~cong(X415,X416,X417,X418)|cong(X417,X418,X415,X416)))))),inference(variable_rename,[status(thm)],[c338])).
% 136.74/136.90 cnf(c340,plain,~cong(X636,X639,X638,X637)|cong(X638,X637,X636,X639),inference(split_conjunct,[status(thm)],[c339])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c199,plain,(![X181]:(![X182]:(![X183]:(![X184]:(![X185]:(((~midp(X185,X181,X182)|~para(X181,X183,X182,X184))|~para(X181,X184,X182,X183))|midp(X185,X183,X184))))))),inference(variable_rename,[status(thm)],[c198])).
% 136.74/136.90 cnf(c200,plain,~midp(X968,X970,X971)|~para(X970,X969,X971,X967)|~para(X970,X967,X971,X969)|midp(X968,X969,X967),inference(split_conjunct,[status(thm)],[c199])).
% 136.74/136.90 cnf(c956,plain,~midp(X1993,X1991,X1990)|~para(X1991,X1992,X1990,X1992)|midp(X1993,X1992,X1992),inference(factor,[status(thm)],[c200])).
% 136.74/136.90 cnf(c16319,plain,~midp(X7324,X7323,X7323)|midp(X7324,X7325,X7325),inference(resolution,[status(thm)],[c16289, c956])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c275,plain,(![X287]:(![X288]:(![X289]:(![X290]:((~eqangle(X289,X287,X289,X288,X290,X287,X290,X288)|~coll(X289,X290,X288))|cyclic(X287,X288,X289,X290)))))),inference(variable_rename,[status(thm)],[c274])).
% 136.74/136.90 cnf(c276,plain,~eqangle(X1068,X1069,X1068,X1067,X1070,X1069,X1070,X1067)|~coll(X1068,X1070,X1067)|cyclic(X1069,X1067,X1068,X1070),inference(split_conjunct,[status(thm)],[c275])).
% 136.74/136.90 cnf(c16292,plain,eqangle(X7316,X7317,X7315,X7314,X7316,X7317,X7315,X7314),inference(resolution,[status(thm)],[c16289, c288])).
% 136.74/136.90 cnf(c26306,plain,~coll(X8032,X8032,X8033)|cyclic(X8034,X8033,X8032,X8032),inference(resolution,[status(thm)],[c16292, c276])).
% 136.74/136.90 cnf(c27723,plain,cyclic(X8039,X8040,X8038,X8038),inference(resolution,[status(thm)],[c26306, c26653])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c272,plain,(![X281]:(![X282]:(![X283]:(![X284]:(![X285]:(![X286]:((((~cyclic(X281,X282,X283,X284)|~cyclic(X281,X282,X283,X285))|~cyclic(X281,X282,X283,X286))|~eqangle(X283,X281,X283,X282,X286,X284,X286,X285))|cong(X281,X282,X284,X285)))))))),inference(shift_quantors,[status(thm)],[fof(c271,plain,(![X281]:(![X282]:(![X283]:(![X284]:(![X285]:((![X286]:(((~cyclic(X281,X282,X283,X284)|~cyclic(X281,X282,X283,X285))|~cyclic(X281,X282,X283,X286))|~eqangle(X283,X281,X283,X282,X286,X284,X286,X285)))|cong(X281,X282,X284,X285))))))),inference(variable_rename,[status(thm)],[c270])).])).
% 136.74/136.90 cnf(c273,plain,~cyclic(X1065,X1064,X1061,X1063)|~cyclic(X1065,X1064,X1061,X1066)|~cyclic(X1065,X1064,X1061,X1062)|~eqangle(X1061,X1065,X1061,X1064,X1062,X1063,X1062,X1066)|cong(X1065,X1064,X1063,X1066),inference(split_conjunct,[status(thm)],[c272])).
% 136.74/136.90 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/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD20)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c351,plain,(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(~eqangle(X443,X444,X445,X446,X447,X448,X449,X450)|eqangle(X447,X448,X449,X450,X443,X444,X445,X446)))))))))),inference(variable_rename,[status(thm)],[c350])).
% 136.74/136.90 cnf(c352,plain,~eqangle(X1221,X1222,X1215,X1218,X1216,X1220,X1219,X1217)|eqangle(X1216,X1220,X1219,X1217,X1221,X1222,X1215,X1218),inference(split_conjunct,[status(thm)],[c351])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c348,plain,(![X435]:(![X436]:(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(~eqangle(X435,X436,X437,X438,X439,X440,X441,X442)|eqangle(X435,X436,X439,X440,X437,X438,X441,X442)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 136.74/136.90 cnf(c349,plain,~eqangle(X1211,X1208,X1212,X1207,X1209,X1210,X1214,X1213)|eqangle(X1211,X1208,X1209,X1210,X1212,X1207,X1214,X1213),inference(split_conjunct,[status(thm)],[c348])).
% 136.74/136.90 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)).
% 136.74/136.90 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 136.74/136.90 fof(c401,plain,(![X526]:(![X527]:(![X528]:(![X529]:(~para(X526,X527,X528,X529)|para(X526,X527,X529,X528)))))),inference(variable_rename,[status(thm)],[c400])).
% 136.74/136.90 cnf(c402,plain,~para(X721,X723,X722,X720)|para(X721,X723,X720,X722),inference(split_conjunct,[status(thm)],[c401])).
% 136.74/136.90 cnf(c16314,plain,para(X5342,X5341,X5341,X5342),inference(resolution,[status(thm)],[c16289, c402])).
% 136.74/136.90 cnf(c17801,plain,eqangle(X7787,X7786,X7785,X7784,X7786,X7787,X7785,X7784),inference(resolution,[status(thm)],[c16314, c288])).
% 136.74/136.90 cnf(c27016,plain,eqangle(X7830,X7829,X7829,X7830,X7828,X7827,X7828,X7827),inference(resolution,[status(thm)],[c17801, c349])).
% 136.74/136.90 cnf(c27159,plain,eqangle(X7883,X7881,X7883,X7881,X7880,X7882,X7882,X7880),inference(resolution,[status(thm)],[c27016, c352])).
% 136.74/136.90 cnf(c27301,plain,~cyclic(X9042,X9042,X9041,X9040)|cong(X9042,X9042,X9040,X9040),inference(resolution,[status(thm)],[c27159, c273])).
% 136.74/136.90 cnf(c28427,plain,cong(X9043,X9043,X9044,X9044),inference(resolution,[status(thm)],[c27301, c27723])).
% 136.74/136.90 cnf(c28462,plain,~coll(X9097,X9097,X9097)|midp(X9097,X9097,X9097),inference(resolution,[status(thm)],[c28427, c191])).
% 136.74/136.90 cnf(c28574,plain,midp(X9098,X9098,X9098),inference(resolution,[status(thm)],[c28462, c26653])).
% 136.74/136.90 cnf(c28626,plain,midp(X9099,X9100,X9100),inference(resolution,[status(thm)],[c28574, c16319])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c242,plain,(![X241]:(![X242]:(![X243]:(![X244]:((~perp(X241,X242,X242,X243)|~midp(X244,X241,X243))|cong(X241,X244,X242,X244)))))),inference(variable_rename,[status(thm)],[c241])).
% 136.74/136.90 cnf(c243,plain,~perp(X1023,X1021,X1021,X1022)|~midp(X1024,X1023,X1022)|cong(X1023,X1024,X1021,X1024),inference(split_conjunct,[status(thm)],[c242])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c165,plain,(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:(![X139]:(![X140]:(![X141]:((~eqangle(X134,X135,X136,X137,X138,X139,X140,X141)|~perp(X138,X139,X140,X141))|perp(X134,X135,X136,X137)))))))))),inference(shift_quantors,[status(thm)],[fof(c164,plain,(![X134]:(![X135]:(![X136]:(![X137]:((![X138]:(![X139]:(![X140]:(![X141]:(~eqangle(X134,X135,X136,X137,X138,X139,X140,X141)|~perp(X138,X139,X140,X141))))))|perp(X134,X135,X136,X137)))))),inference(variable_rename,[status(thm)],[c163])).])).
% 136.74/136.90 cnf(c166,plain,~eqangle(X929,X932,X926,X931,X927,X925,X928,X930)|~perp(X927,X925,X928,X930)|perp(X929,X932,X926,X931),inference(split_conjunct,[status(thm)],[c165])).
% 136.74/136.90 cnf(c27162,plain,~perp(X9024,X9023,X9024,X9023)|perp(X9022,X9025,X9025,X9022),inference(resolution,[status(thm)],[c27016, c166])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c228,plain,(![X225]:(![X226]:(![X227]:(![X228]:((~cong(X225,X227,X226,X227)|~cong(X225,X228,X226,X228))|perp(X225,X226,X227,X228)))))),inference(variable_rename,[status(thm)],[c227])).
% 136.74/136.90 cnf(c229,plain,~cong(X1005,X1006,X1007,X1006)|~cong(X1005,X1008,X1007,X1008)|perp(X1005,X1007,X1006,X1008),inference(split_conjunct,[status(thm)],[c228])).
% 136.74/136.90 cnf(c1043,plain,~cong(X1257,X1255,X1256,X1255)|perp(X1257,X1256,X1255,X1255),inference(factor,[status(thm)],[c229])).
% 136.74/136.90 cnf(c28442,plain,perp(X9056,X9056,X9056,X9056),inference(resolution,[status(thm)],[c28427, c1043])).
% 136.74/136.90 cnf(c28494,plain,perp(X9074,X9073,X9073,X9074),inference(resolution,[status(thm)],[c28442, c27162])).
% 136.74/136.90 cnf(c28550,plain,~midp(X9933,X9934,X9934)|cong(X9934,X9933,X9932,X9933),inference(resolution,[status(thm)],[c28494, c243])).
% 136.74/136.90 cnf(c30600,plain,cong(X9936,X9937,X9935,X9937),inference(resolution,[status(thm)],[c28550, c28626])).
% 136.74/136.90 cnf(c30614,plain,cong(X9941,X9943,X9943,X9942),inference(resolution,[status(thm)],[c30600, c343])).
% 136.74/136.90 cnf(c30682,plain,cong(X9968,X9967,X9969,X9968),inference(resolution,[status(thm)],[c30614, c340])).
% 136.74/136.90 cnf(c30759,plain,cong(X9986,X9984,X9986,X9985),inference(resolution,[status(thm)],[c30682, c343])).
% 136.74/136.90 cnf(c30803,plain,~coll(X10192,X10194,X10193)|midp(X10192,X10194,X10193),inference(resolution,[status(thm)],[c30759, c191])).
% 136.74/136.90 cnf(c32870,plain,midp(X10197,X10195,X10196),inference(resolution,[status(thm)],[c30803, c26653])).
% 136.74/136.90 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)).
% 136.74/136.90 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])).
% 136.74/136.90 fof(c267,plain,(![X276]:(![X277]:(![X278]:(![X279]:(![X280]:((~midp(X279,X276,X277)|~midp(X280,X276,X278))|para(X279,X280,X277,X278))))))),inference(variable_rename,[status(thm)],[c266])).
% 136.74/136.90 cnf(c268,plain,~midp(X1058,X1060,X1056)|~midp(X1057,X1060,X1059)|para(X1058,X1057,X1056,X1059),inference(split_conjunct,[status(thm)],[c267])).
% 136.74/136.90 cnf(c29213,plain,~midp(X13378,X13379,X13381)|para(X13378,X13380,X13381,X13379),inference(resolution,[status(thm)],[c28626, c268])).
% 136.74/136.90 cnf(c35443,plain,para(X13385,X13382,X13383,X13384),inference(resolution,[status(thm)],[c29213, c32870])).
% 136.74/136.90 cnf(c35454,plain,$false,inference(resolution,[status(thm)],[c35443, c26])).
% 136.74/136.90 % SZS output end CNFRefutation
% 136.74/136.90
% 136.74/136.90 % Initial clauses : 138
% 136.74/136.90 % Processed clauses : 4158
% 136.74/136.90 % Factors computed : 183
% 136.74/136.90 % Resolvents computed: 34869
% 136.74/136.90 % Tautologies deleted: 12
% 136.74/136.90 % Forward subsumed : 10814
% 136.74/136.90 % Backward subsumed : 3633
% 136.74/136.90 % -------- CPU Time ---------
% 136.74/136.90 % User time : 136.481 s
% 136.74/136.90 % System time : 0.068 s
% 136.74/136.90 % Total time : 136.549 s
%------------------------------------------------------------------------------