%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO563+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:17 EDT 2024
% Result : Theorem 111.25s 111.46s
% Output : Refutation 111.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO563+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n004.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:54:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 111.25/111.46 % Version: 1.5
% 111.25/111.46 % SZS status Theorem
% 111.25/111.46 % SZS output start CNFRefutation
% 111.25/111.46 fof(exemplo6GDDFULL214024,conjecture,(![Q]:(![R]:(![P]:(![O1]:(![S]:(![Y]:(![O]:(![X]:(![I]:(![NWPNT1]:(![NWPNT2]:(((((((circle(O1,Q,R,P)&circle(O1,Q,S,NWPNT1))&coll(Y,Q,S))&circle(O,Y,P,Q))&circle(O,Q,X,NWPNT2))&coll(I,R,S))&coll(I,Y,X))=>eqangle(R,I,I,X,R,P,P,X))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL214024)).
% 111.25/111.46 fof(c11,negated_conjecture,(~(![Q]:(![R]:(![P]:(![O1]:(![S]:(![Y]:(![O]:(![X]:(![I]:(![NWPNT1]:(![NWPNT2]:(((((((circle(O1,Q,R,P)&circle(O1,Q,S,NWPNT1))&coll(Y,Q,S))&circle(O,Y,P,Q))&circle(O,Q,X,NWPNT2))&coll(I,R,S))&coll(I,Y,X))=>eqangle(R,I,I,X,R,P,P,X)))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL214024])).
% 111.25/111.46 fof(c12,negated_conjecture,(?[Q]:(?[R]:(?[P]:(?[O1]:(?[S]:(?[Y]:(?[O]:(?[X]:(?[I]:(?[NWPNT1]:(?[NWPNT2]:(((((((circle(O1,Q,R,P)&circle(O1,Q,S,NWPNT1))&coll(Y,Q,S))&circle(O,Y,P,Q))&circle(O,Q,X,NWPNT2))&coll(I,R,S))&coll(I,Y,X))&~eqangle(R,I,I,X,R,P,P,X))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 111.25/111.46 fof(c13,negated_conjecture,(?[Q]:(?[R]:(?[P]:(?[O1]:(?[S]:(?[Y]:(?[O]:(?[X]:(?[I]:(((((((circle(O1,Q,R,P)&(?[NWPNT1]:circle(O1,Q,S,NWPNT1)))&coll(Y,Q,S))&circle(O,Y,P,Q))&(?[NWPNT2]:circle(O,Q,X,NWPNT2)))&coll(I,R,S))&coll(I,Y,X))&~eqangle(R,I,I,X,R,P,P,X))))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 111.25/111.46 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:(((((((circle(X5,X2,X3,X4)&(?[X11]:circle(X5,X2,X6,X11)))&coll(X7,X2,X6))&circle(X8,X7,X4,X2))&(?[X12]:circle(X8,X2,X9,X12)))&coll(X10,X3,X6))&coll(X10,X7,X9))&~eqangle(X3,X10,X10,X9,X3,X4,X4,X9))))))))))),inference(variable_rename,[status(thm)],[c13])).
% 111.25/111.46 fof(c15,negated_conjecture,(((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0010))&coll(skolem0006,skolem0001,skolem0005))&circle(skolem0007,skolem0006,skolem0003,skolem0001))&circle(skolem0007,skolem0001,skolem0008,skolem0011))&coll(skolem0009,skolem0002,skolem0005))&coll(skolem0009,skolem0006,skolem0008))&~eqangle(skolem0002,skolem0009,skolem0009,skolem0008,skolem0002,skolem0003,skolem0003,skolem0008)),inference(skolemize,[status(esa)],[c14])).
% 111.25/111.46 cnf(c23,negated_conjecture,~eqangle(skolem0002,skolem0009,skolem0009,skolem0008,skolem0002,skolem0003,skolem0003,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 111.25/111.46 fof(ruleD18,axiom,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(eqangle(A,B,C,D,P,Q,U,V)=>eqangle(B,A,C,D,P,Q,U,V)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD18)).
% 111.25/111.46 fof(c353,plain,(![A]:(![B]:(![C]:(![D]:(![P]:(![Q]:(![U]:(![V]:(~eqangle(A,B,C,D,P,Q,U,V)|eqangle(B,A,C,D,P,Q,U,V)))))))))),inference(fof_nnf,[status(thm)],[ruleD18])).
% 111.25/111.46 fof(c354,plain,(![X453]:(![X454]:(![X455]:(![X456]:(![X457]:(![X458]:(![X459]:(![X460]:(~eqangle(X453,X454,X455,X456,X457,X458,X459,X460)|eqangle(X454,X453,X455,X456,X457,X458,X459,X460)))))))))),inference(variable_rename,[status(thm)],[c353])).
% 111.25/111.46 cnf(c355,plain,~eqangle(X1242,X1241,X1237,X1238,X1236,X1239,X1243,X1240)|eqangle(X1241,X1242,X1237,X1238,X1236,X1239,X1243,X1240),inference(split_conjunct,[status(thm)],[c354])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c347,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])).
% 111.25/111.46 fof(c348,plain,(![X437]:(![X438]:(![X439]:(![X440]:(![X441]:(![X442]:(![X443]:(![X444]:(~eqangle(X437,X438,X439,X440,X441,X442,X443,X444)|eqangle(X441,X442,X443,X444,X437,X438,X439,X440)))))))))),inference(variable_rename,[status(thm)],[c347])).
% 111.25/111.46 cnf(c349,plain,~eqangle(X1220,X1227,X1224,X1221,X1225,X1226,X1222,X1223)|eqangle(X1225,X1226,X1222,X1223,X1220,X1227,X1224,X1221),inference(split_conjunct,[status(thm)],[c348])).
% 111.25/111.46 fof(ruleD41,axiom,(![A]:(![B]:(![P]:(![Q]:(cyclic(A,B,P,Q)=>eqangle(P,A,P,B,Q,A,Q,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD41)).
% 111.25/111.46 fof(c278,plain,(![A]:(![B]:(![P]:(![Q]:(~cyclic(A,B,P,Q)|eqangle(P,A,P,B,Q,A,Q,B)))))),inference(fof_nnf,[status(thm)],[ruleD41])).
% 111.25/111.46 fof(c279,plain,(![X289]:(![X290]:(![X291]:(![X292]:(~cyclic(X289,X290,X291,X292)|eqangle(X291,X289,X291,X290,X292,X289,X292,X290)))))),inference(variable_rename,[status(thm)],[c278])).
% 111.25/111.46 cnf(c280,plain,~cyclic(X1081,X1082,X1083,X1080)|eqangle(X1083,X1081,X1083,X1082,X1080,X1081,X1080,X1082),inference(split_conjunct,[status(thm)],[c279])).
% 111.25/111.46 fof(ruleD16,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(B,A,C,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD16)).
% 111.25/111.46 fof(c359,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 111.25/111.46 fof(c360,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X467,X466,X468,X469)))))),inference(variable_rename,[status(thm)],[c359])).
% 111.25/111.46 cnf(c361,plain,~cyclic(X668,X666,X669,X667)|cyclic(X666,X668,X669,X667),inference(split_conjunct,[status(thm)],[c360])).
% 111.25/111.46 fof(ruleD14,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,B,D,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD14)).
% 111.25/111.46 fof(c365,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 111.25/111.46 fof(c366,plain,(![X474]:(![X475]:(![X476]:(![X477]:(~cyclic(X474,X475,X476,X477)|cyclic(X474,X475,X477,X476)))))),inference(variable_rename,[status(thm)],[c365])).
% 111.25/111.46 cnf(c367,plain,~cyclic(X677,X675,X676,X674)|cyclic(X677,X675,X674,X676),inference(split_conjunct,[status(thm)],[c366])).
% 111.25/111.46 fof(ruleD15,axiom,(![A]:(![B]:(![C]:(![D]:(cyclic(A,B,C,D)=>cyclic(A,C,B,D)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD15)).
% 111.25/111.46 fof(c362,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 111.25/111.46 fof(c363,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X472,X471,X473)))))),inference(variable_rename,[status(thm)],[c362])).
% 111.25/111.46 cnf(c364,plain,~cyclic(X671,X673,X672,X670)|cyclic(X671,X672,X673,X670),inference(split_conjunct,[status(thm)],[c363])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c400,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 111.25/111.46 fof(c401,plain,(![X524]:(![X525]:(![X526]:(![X527]:((~coll(X524,X525,X526)|~coll(X524,X525,X527))|coll(X526,X527,X524)))))),inference(variable_rename,[status(thm)],[c400])).
% 111.25/111.46 cnf(c402,plain,~coll(X712,X714,X715)|~coll(X712,X714,X713)|coll(X715,X713,X712),inference(split_conjunct,[status(thm)],[c401])).
% 111.25/111.46 cnf(c470,plain,~coll(X717,X716,X718)|coll(X718,X718,X717),inference(factor,[status(thm)],[c402])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c189,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 111.25/111.46 fof(c190,plain,(![X167]:(![X168]:(![X169]:(~para(X167,X168,X167,X169)|coll(X167,X168,X169))))),inference(variable_rename,[status(thm)],[c189])).
% 111.25/111.46 cnf(c191,plain,~para(X645,X644,X645,X643)|coll(X645,X644,X643),inference(split_conjunct,[status(thm)],[c190])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c286,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])).
% 111.25/111.46 fof(c287,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)],[c286])).
% 111.25/111.46 fof(c289,plain,(![X299]:(![X300]:(![X301]:(![X302]:(![X303]:(![X304]:(~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)|para(X299,X300,X301,X302)))))))),inference(shift_quantors,[status(thm)],[fof(c288,plain,(![X299]:(![X300]:(![X301]:(![X302]:((![X303]:(![X304]:~eqangle(X299,X300,X303,X304,X301,X302,X303,X304)))|para(X299,X300,X301,X302)))))),inference(variable_rename,[status(thm)],[c287])).])).
% 111.25/111.46 cnf(c290,plain,~eqangle(X1091,X1095,X1090,X1093,X1094,X1092,X1090,X1093)|para(X1091,X1095,X1094,X1092),inference(split_conjunct,[status(thm)],[c289])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c350,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])).
% 111.25/111.46 fof(c351,plain,(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(![X450]:(![X451]:(![X452]:(~eqangle(X445,X446,X447,X448,X449,X450,X451,X452)|eqangle(X447,X448,X445,X446,X451,X452,X449,X450)))))))))),inference(variable_rename,[status(thm)],[c350])).
% 111.25/111.46 cnf(c352,plain,~eqangle(X1228,X1234,X1232,X1235,X1231,X1230,X1229,X1233)|eqangle(X1232,X1235,X1228,X1234,X1229,X1233,X1231,X1230),inference(split_conjunct,[status(thm)],[c351])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c281,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])).
% 111.25/111.46 fof(c282,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)],[c281])).
% 111.25/111.46 fof(c284,plain,(![X293]:(![X294]:(![X295]:(![X296]:(![X297]:(![X298]:(~para(X293,X294,X295,X296)|eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(shift_quantors,[status(thm)],[fof(c283,plain,(![X293]:(![X294]:(![X295]:(![X296]:(~para(X293,X294,X295,X296)|(![X297]:(![X298]:eqangle(X293,X294,X297,X298,X295,X296,X297,X298)))))))),inference(variable_rename,[status(thm)],[c282])).])).
% 111.25/111.46 cnf(c285,plain,~para(X1085,X1088,X1086,X1089)|eqangle(X1085,X1088,X1087,X1084,X1086,X1089,X1087,X1084),inference(split_conjunct,[status(thm)],[c284])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c382,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])).
% 111.25/111.46 fof(c383,plain,(![X496]:(![X497]:(![X498]:(![X499]:(![X500]:(![X501]:((~perp(X496,X497,X498,X499)|~perp(X498,X499,X500,X501))|para(X496,X497,X500,X501)))))))),inference(variable_rename,[status(thm)],[c382])).
% 111.25/111.46 cnf(c384,plain,~perp(X1264,X1268,X1266,X1265)|~perp(X1266,X1265,X1267,X1269)|para(X1264,X1268,X1267,X1269),inference(split_conjunct,[status(thm)],[c383])).
% 111.25/111.46 cnf(c20,negated_conjecture,circle(skolem0007,skolem0001,skolem0008,skolem0011),inference(split_conjunct,[status(thm)],[c15])).
% 111.25/111.46 fof(ruleX11,axiom,(![A]:(![B]:(![C]:(![O]:(?[P]:(circle(O,A,B,C)=>perp(P,A,A,O))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleX11)).
% 111.25/111.46 fof(c72,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 111.25/111.46 fof(c73,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c72])).
% 111.25/111.46 fof(c74,plain,(![X55]:(![X56]:(![X57]:(![X58]:(~circle(X58,X55,X56,X57)|(?[X59]:perp(X59,X55,X55,X58))))))),inference(variable_rename,[status(thm)],[c73])).
% 111.25/111.46 fof(c75,plain,(![X55]:(![X56]:(![X57]:(![X58]:(~circle(X58,X55,X56,X57)|perp(skolem0020(X55,X56,X57,X58),X55,X55,X58)))))),inference(skolemize,[status(esa)],[c74])).
% 111.25/111.46 cnf(c76,plain,~circle(X787,X788,X786,X785)|perp(skolem0020(X788,X786,X785,X787),X788,X788,X787),inference(split_conjunct,[status(thm)],[c75])).
% 111.25/111.46 cnf(c687,plain,perp(skolem0020(skolem0001,skolem0008,skolem0011,skolem0007),skolem0001,skolem0001,skolem0007),inference(resolution,[status(thm)],[c76, c20])).
% 111.25/111.46 cnf(c2123,plain,~perp(X3948,X3949,skolem0020(skolem0001,skolem0008,skolem0011,skolem0007),skolem0001)|para(X3948,X3949,skolem0001,skolem0007),inference(resolution,[status(thm)],[c687, c384])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c385,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 111.25/111.46 fof(c386,plain,(![X502]:(![X503]:(![X504]:(![X505]:(~perp(X502,X503,X504,X505)|perp(X504,X505,X502,X503)))))),inference(variable_rename,[status(thm)],[c385])).
% 111.25/111.46 cnf(c387,plain,~perp(X679,X678,X680,X681)|perp(X680,X681,X679,X678),inference(split_conjunct,[status(thm)],[c386])).
% 111.25/111.46 cnf(c2127,plain,perp(skolem0001,skolem0007,skolem0020(skolem0001,skolem0008,skolem0011,skolem0007),skolem0001),inference(resolution,[status(thm)],[c687, c387])).
% 111.25/111.46 cnf(c5520,plain,para(skolem0001,skolem0007,skolem0001,skolem0007),inference(resolution,[status(thm)],[c2127, c2123])).
% 111.25/111.46 cnf(c5543,plain,eqangle(skolem0001,skolem0007,X4594,X4595,skolem0001,skolem0007,X4594,X4595),inference(resolution,[status(thm)],[c5520, c285])).
% 111.25/111.46 cnf(c8946,plain,eqangle(X6352,X6353,skolem0001,skolem0007,X6352,X6353,skolem0001,skolem0007),inference(resolution,[status(thm)],[c5543, c352])).
% 111.25/111.46 cnf(c11687,plain,para(X6354,X6355,X6354,X6355),inference(resolution,[status(thm)],[c8946, c290])).
% 111.25/111.46 cnf(c11723,plain,coll(X6359,X6360,X6360),inference(resolution,[status(thm)],[c11687, c191])).
% 111.25/111.46 cnf(c12008,plain,coll(X6366,X6366,X6365),inference(resolution,[status(thm)],[c11723, c470])).
% 111.25/111.46 cnf(c13018,plain,~coll(X8581,X8581,X8582)|coll(X8582,X8583,X8581),inference(resolution,[status(thm)],[c12008, c402])).
% 111.25/111.46 cnf(c19395,plain,coll(X8586,X8584,X8585),inference(resolution,[status(thm)],[c13018, c12008])).
% 111.25/111.46 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)).
% 111.25/111.46 fof(c271,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])).
% 111.25/111.46 fof(c272,plain,(![X281]:(![X282]:(![X283]:(![X284]:((~eqangle(X283,X281,X283,X282,X284,X281,X284,X282)|~coll(X283,X284,X282))|cyclic(X281,X282,X283,X284)))))),inference(variable_rename,[status(thm)],[c271])).
% 111.25/111.46 cnf(c273,plain,~eqangle(X1074,X1072,X1074,X1075,X1073,X1072,X1073,X1075)|~coll(X1074,X1073,X1075)|cyclic(X1072,X1075,X1074,X1073),inference(split_conjunct,[status(thm)],[c272])).
% 111.25/111.46 cnf(c11719,plain,eqangle(X8302,X8299,X8300,X8301,X8302,X8299,X8300,X8301),inference(resolution,[status(thm)],[c11687, c285])).
% 111.25/111.46 cnf(c19195,plain,~coll(X8970,X8970,X8972)|cyclic(X8971,X8972,X8970,X8970),inference(resolution,[status(thm)],[c11719, c273])).
% 111.25/111.46 cnf(c20072,plain,cyclic(X8978,X8976,X8977,X8977),inference(resolution,[status(thm)],[c19195, c19395])).
% 111.25/111.46 cnf(c20076,plain,cyclic(X8982,X8984,X8983,X8984),inference(resolution,[status(thm)],[c20072, c364])).
% 111.25/111.46 cnf(c20081,plain,cyclic(X8988,X8989,X8989,X8990),inference(resolution,[status(thm)],[c20076, c367])).
% 111.25/111.46 cnf(c20093,plain,cyclic(X9006,X9007,X9006,X9008),inference(resolution,[status(thm)],[c20081, c361])).
% 111.25/111.46 fof(ruleD17,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:((cyclic(A,B,C,D)&cyclic(A,B,C,E))=>cyclic(B,C,D,E))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO012+0.ax', ruleD17)).
% 111.25/111.46 fof(c356,plain,(![A]:(![B]:(![C]:(![D]:(![E]:((~cyclic(A,B,C,D)|~cyclic(A,B,C,E))|cyclic(B,C,D,E))))))),inference(fof_nnf,[status(thm)],[ruleD17])).
% 111.25/111.46 fof(c357,plain,(![X461]:(![X462]:(![X463]:(![X464]:(![X465]:((~cyclic(X461,X462,X463,X464)|~cyclic(X461,X462,X463,X465))|cyclic(X462,X463,X464,X465))))))),inference(variable_rename,[status(thm)],[c356])).
% 111.25/111.46 cnf(c358,plain,~cyclic(X1244,X1247,X1245,X1246)|~cyclic(X1244,X1247,X1245,X1248)|cyclic(X1247,X1245,X1246,X1248),inference(split_conjunct,[status(thm)],[c357])).
% 111.25/111.46 cnf(c20107,plain,~cyclic(X15129,X15130,X15129,X15128)|cyclic(X15130,X15129,X15128,X15131),inference(resolution,[status(thm)],[c20093, c358])).
% 111.25/111.46 cnf(c27403,plain,cyclic(X15136,X15137,X15135,X15138),inference(resolution,[status(thm)],[c20107, c20093])).
% 111.25/111.46 cnf(c27409,plain,eqangle(X15157,X15154,X15157,X15155,X15156,X15154,X15156,X15155),inference(resolution,[status(thm)],[c27403, c280])).
% 111.25/111.46 cnf(c27415,plain,eqangle(X15169,X15171,X15171,X15170,X15172,X15169,X15172,X15170),inference(resolution,[status(thm)],[c27409, c355])).
% 111.25/111.46 cnf(c27421,plain,eqangle(X15177,X15178,X15177,X15180,X15178,X15179,X15179,X15180),inference(resolution,[status(thm)],[c27415, c349])).
% 111.25/111.46 cnf(c27442,plain,eqangle(X15224,X15226,X15226,X15225,X15224,X15227,X15227,X15225),inference(resolution,[status(thm)],[c27421, c355])).
% 111.25/111.46 cnf(c27484,plain,$false,inference(resolution,[status(thm)],[c27442, c23])).
% 111.25/111.46 % SZS output end CNFRefutation
% 111.25/111.46
% 111.25/111.46 % Initial clauses : 135
% 111.25/111.46 % Processed clauses : 4022
% 111.25/111.46 % Factors computed : 191
% 111.25/111.46 % Resolvents computed: 26885
% 111.25/111.46 % Tautologies deleted: 13
% 111.25/111.46 % Forward subsumed : 10122
% 111.25/111.46 % Backward subsumed : 3749
% 111.25/111.46 % -------- CPU Time ---------
% 111.25/111.46 % User time : 111.077 s
% 111.25/111.46 % System time : 0.047 s
% 111.25/111.46 % Total time : 111.124 s
%------------------------------------------------------------------------------