%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO550+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:15 EDT 2024
% Result : Theorem 126.16s 126.33s
% Output : Refutation 126.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GEO550+1 : TPTP v8.1.2. Released v7.5.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n018.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 08:23:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 126.16/126.33 % Version: 1.5
% 126.16/126.33 % SZS status Theorem
% 126.16/126.33 % SZS output start CNFRefutation
% 126.16/126.33 fof(exemplo6GDDFULL012010,conjecture,(![A]:(![B]:(![C]:(![D]:(![P]:(![E]:(![O1]:(![O]:(![Q]:(![NWPNT1]:(![NWPNT2]:((((((((coll(P,C,D)&coll(P,A,B))&coll(E,B,C))&coll(E,A,D))&circle(O1,C,D,E))&circle(O,E,B,A))&circle(O1,C,Q,NWPNT1))&circle(O,A,Q,NWPNT2))=>cyclic(P,D,Q,A))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL012010)).
% 126.16/126.33 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![P]:(![E]:(![O1]:(![O]:(![Q]:(![NWPNT1]:(![NWPNT2]:((((((((coll(P,C,D)&coll(P,A,B))&coll(E,B,C))&coll(E,A,D))&circle(O1,C,D,E))&circle(O,E,B,A))&circle(O1,C,Q,NWPNT1))&circle(O,A,Q,NWPNT2))=>cyclic(P,D,Q,A)))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL012010])).
% 126.16/126.33 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[P]:(?[E]:(?[O1]:(?[O]:(?[Q]:(?[NWPNT1]:(?[NWPNT2]:((((((((coll(P,C,D)&coll(P,A,B))&coll(E,B,C))&coll(E,A,D))&circle(O1,C,D,E))&circle(O,E,B,A))&circle(O1,C,Q,NWPNT1))&circle(O,A,Q,NWPNT2))&~cyclic(P,D,Q,A))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 126.16/126.33 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[P]:(?[E]:(?[O1]:(?[O]:(?[Q]:((((((((coll(P,C,D)&coll(P,A,B))&coll(E,B,C))&coll(E,A,D))&circle(O1,C,D,E))&circle(O,E,B,A))&(?[NWPNT1]:circle(O1,C,Q,NWPNT1)))&(?[NWPNT2]:circle(O,A,Q,NWPNT2)))&~cyclic(P,D,Q,A))))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 126.16/126.33 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:((((((((coll(X6,X4,X5)&coll(X6,X2,X3))&coll(X7,X3,X4))&coll(X7,X2,X5))&circle(X8,X4,X5,X7))&circle(X9,X7,X3,X2))&(?[X11]:circle(X8,X4,X10,X11)))&(?[X12]:circle(X9,X2,X10,X12)))&~cyclic(X6,X5,X10,X2))))))))))),inference(variable_rename,[status(thm)],[c13])).
% 126.16/126.33 fof(c15,negated_conjecture,((((((((coll(skolem0005,skolem0003,skolem0004)&coll(skolem0005,skolem0001,skolem0002))&coll(skolem0006,skolem0002,skolem0003))&coll(skolem0006,skolem0001,skolem0004))&circle(skolem0007,skolem0003,skolem0004,skolem0006))&circle(skolem0008,skolem0006,skolem0002,skolem0001))&circle(skolem0007,skolem0003,skolem0009,skolem0010))&circle(skolem0008,skolem0001,skolem0009,skolem0011))&~cyclic(skolem0005,skolem0004,skolem0009,skolem0001)),inference(skolemize,[status(esa)],[c14])).
% 126.16/126.33 cnf(c24,negated_conjecture,~cyclic(skolem0005,skolem0004,skolem0009,skolem0001),inference(split_conjunct,[status(thm)],[c15])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 126.16/126.33 fof(c361,plain,(![X466]:(![X467]:(![X468]:(![X469]:(~cyclic(X466,X467,X468,X469)|cyclic(X467,X466,X468,X469)))))),inference(variable_rename,[status(thm)],[c360])).
% 126.16/126.33 cnf(c362,plain,~cyclic(X693,X691,X692,X690)|cyclic(X691,X693,X692,X690),inference(split_conjunct,[status(thm)],[c361])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c366,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 126.16/126.33 fof(c367,plain,(![X474]:(![X475]:(![X476]:(![X477]:(~cyclic(X474,X475,X476,X477)|cyclic(X474,X475,X477,X476)))))),inference(variable_rename,[status(thm)],[c366])).
% 126.16/126.33 cnf(c368,plain,~cyclic(X701,X699,X698,X700)|cyclic(X701,X699,X700,X698),inference(split_conjunct,[status(thm)],[c367])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 126.16/126.33 fof(c364,plain,(![X470]:(![X471]:(![X472]:(![X473]:(~cyclic(X470,X471,X472,X473)|cyclic(X470,X472,X471,X473)))))),inference(variable_rename,[status(thm)],[c363])).
% 126.16/126.33 cnf(c365,plain,~cyclic(X697,X695,X696,X694)|cyclic(X697,X696,X695,X694),inference(split_conjunct,[status(thm)],[c364])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c401,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 126.16/126.33 fof(c402,plain,(![X524]:(![X525]:(![X526]:(![X527]:((~coll(X524,X525,X526)|~coll(X524,X525,X527))|coll(X526,X527,X524)))))),inference(variable_rename,[status(thm)],[c401])).
% 126.16/126.33 cnf(c403,plain,~coll(X728,X730,X729)|~coll(X728,X730,X727)|coll(X729,X727,X728),inference(split_conjunct,[status(thm)],[c402])).
% 126.16/126.33 cnf(c489,plain,~coll(X733,X732,X731)|coll(X731,X731,X733),inference(factor,[status(thm)],[c403])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 126.16/126.33 fof(c191,plain,(![X167]:(![X168]:(![X169]:(~para(X167,X168,X167,X169)|coll(X167,X168,X169))))),inference(variable_rename,[status(thm)],[c190])).
% 126.16/126.33 cnf(c192,plain,~para(X674,X675,X674,X673)|coll(X674,X675,X673),inference(split_conjunct,[status(thm)],[c191])).
% 126.16/126.33 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)).
% 126.16/126.33 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])).
% 126.16/126.33 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])).
% 126.16/126.33 fof(c290,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(c289,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)],[c288])).])).
% 126.16/126.33 cnf(c291,plain,~eqangle(X1094,X1096,X1095,X1093,X1092,X1091,X1095,X1093)|para(X1094,X1096,X1092,X1091),inference(split_conjunct,[status(thm)],[c290])).
% 126.16/126.33 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)).
% 126.16/126.33 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])).
% 126.16/126.33 fof(c352,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)],[c351])).
% 126.16/126.33 cnf(c353,plain,~eqangle(X1236,X1242,X1241,X1235,X1240,X1237,X1238,X1239)|eqangle(X1241,X1235,X1236,X1242,X1238,X1239,X1240,X1237),inference(split_conjunct,[status(thm)],[c352])).
% 126.16/126.33 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)).
% 126.16/126.33 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])).
% 126.16/126.33 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])).
% 126.16/126.33 fof(c285,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(c284,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)],[c283])).])).
% 126.16/126.33 cnf(c286,plain,~para(X1089,X1086,X1088,X1085)|eqangle(X1089,X1086,X1087,X1084,X1088,X1085,X1087,X1084),inference(split_conjunct,[status(thm)],[c285])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 126.16/126.33 fof(c387,plain,(![X502]:(![X503]:(![X504]:(![X505]:(~perp(X502,X503,X504,X505)|perp(X504,X505,X502,X503)))))),inference(variable_rename,[status(thm)],[c386])).
% 126.16/126.33 cnf(c388,plain,~perp(X704,X705,X702,X703)|perp(X702,X703,X704,X705),inference(split_conjunct,[status(thm)],[c387])).
% 126.16/126.33 cnf(c20,negated_conjecture,circle(skolem0007,skolem0003,skolem0004,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c73,plain,(![A]:(![B]:(![C]:(![O]:(?[P]:(~circle(O,A,B,C)|perp(P,A,A,O))))))),inference(fof_nnf,[status(thm)],[ruleX11])).
% 126.16/126.33 fof(c74,plain,(![A]:(![B]:(![C]:(![O]:(~circle(O,A,B,C)|(?[P]:perp(P,A,A,O))))))),inference(shift_quantors,[status(thm)],[c73])).
% 126.16/126.33 fof(c75,plain,(![X55]:(![X56]:(![X57]:(![X58]:(~circle(X58,X55,X56,X57)|(?[X59]:perp(X59,X55,X55,X58))))))),inference(variable_rename,[status(thm)],[c74])).
% 126.16/126.33 fof(c76,plain,(![X55]:(![X56]:(![X57]:(![X58]:(~circle(X58,X55,X56,X57)|perp(skolem0020(X55,X56,X57,X58),X55,X55,X58)))))),inference(skolemize,[status(esa)],[c75])).
% 126.16/126.33 cnf(c77,plain,~circle(X786,X787,X788,X785)|perp(skolem0020(X787,X788,X785,X786),X787,X787,X786),inference(split_conjunct,[status(thm)],[c76])).
% 126.16/126.33 cnf(c708,plain,perp(skolem0020(skolem0003,skolem0004,skolem0006,skolem0007),skolem0003,skolem0003,skolem0007),inference(resolution,[status(thm)],[c77, c20])).
% 126.16/126.33 cnf(c2170,plain,perp(skolem0003,skolem0007,skolem0020(skolem0003,skolem0004,skolem0006,skolem0007),skolem0003),inference(resolution,[status(thm)],[c708, c388])).
% 126.16/126.33 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)).
% 126.16/126.33 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])).
% 126.16/126.33 fof(c384,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)],[c383])).
% 126.16/126.33 cnf(c385,plain,~perp(X1271,X1276,X1274,X1275)|~perp(X1274,X1275,X1273,X1272)|para(X1271,X1276,X1273,X1272),inference(split_conjunct,[status(thm)],[c384])).
% 126.16/126.33 cnf(c2176,plain,~perp(X4051,X4052,skolem0020(skolem0003,skolem0004,skolem0006,skolem0007),skolem0003)|para(X4051,X4052,skolem0003,skolem0007),inference(resolution,[status(thm)],[c708, c385])).
% 126.16/126.33 cnf(c5709,plain,para(skolem0003,skolem0007,skolem0003,skolem0007),inference(resolution,[status(thm)],[c2176, c2170])).
% 126.16/126.33 cnf(c5735,plain,eqangle(skolem0003,skolem0007,X4707,X4708,skolem0003,skolem0007,X4707,X4708),inference(resolution,[status(thm)],[c5709, c286])).
% 126.16/126.33 cnf(c9211,plain,eqangle(X6475,X6476,skolem0003,skolem0007,X6475,X6476,skolem0003,skolem0007),inference(resolution,[status(thm)],[c5735, c353])).
% 126.16/126.33 cnf(c12002,plain,para(X6477,X6478,X6477,X6478),inference(resolution,[status(thm)],[c9211, c291])).
% 126.16/126.33 cnf(c12029,plain,coll(X6483,X6482,X6482),inference(resolution,[status(thm)],[c12002, c192])).
% 126.16/126.33 cnf(c12174,plain,coll(X6487,X6487,X6486),inference(resolution,[status(thm)],[c12029, c489])).
% 126.16/126.33 cnf(c13174,plain,~coll(X8708,X8708,X8709)|coll(X8709,X8707,X8708),inference(resolution,[status(thm)],[c12174, c403])).
% 126.16/126.33 cnf(c19719,plain,coll(X8718,X8717,X8719),inference(resolution,[status(thm)],[c13174, c12174])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c272,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])).
% 126.16/126.33 fof(c273,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)],[c272])).
% 126.16/126.33 cnf(c274,plain,~eqangle(X1070,X1071,X1070,X1068,X1069,X1071,X1069,X1068)|~coll(X1070,X1069,X1068)|cyclic(X1071,X1068,X1070,X1069),inference(split_conjunct,[status(thm)],[c273])).
% 126.16/126.33 cnf(c12031,plain,eqangle(X8428,X8427,X8426,X8425,X8428,X8427,X8426,X8425),inference(resolution,[status(thm)],[c12002, c286])).
% 126.16/126.33 cnf(c19505,plain,~coll(X9089,X9089,X9087)|cyclic(X9088,X9087,X9089,X9089),inference(resolution,[status(thm)],[c12031, c274])).
% 126.16/126.33 cnf(c20293,plain,cyclic(X9092,X9091,X9090,X9090),inference(resolution,[status(thm)],[c19505, c19719])).
% 126.16/126.33 cnf(c20294,plain,cyclic(X9093,X9095,X9094,X9095),inference(resolution,[status(thm)],[c20293, c365])).
% 126.16/126.33 cnf(c20303,plain,cyclic(X9110,X9108,X9108,X9109),inference(resolution,[status(thm)],[c20294, c368])).
% 126.16/126.33 cnf(c20314,plain,cyclic(X9124,X9125,X9124,X9123),inference(resolution,[status(thm)],[c20303, c362])).
% 126.16/126.33 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)).
% 126.16/126.33 fof(c357,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])).
% 126.16/126.33 fof(c358,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)],[c357])).
% 126.16/126.33 cnf(c359,plain,~cyclic(X1253,X1251,X1255,X1254)|~cyclic(X1253,X1251,X1255,X1252)|cyclic(X1251,X1255,X1254,X1252),inference(split_conjunct,[status(thm)],[c358])).
% 126.16/126.33 cnf(c20331,plain,~cyclic(X14900,X14899,X14900,X14901)|cyclic(X14899,X14900,X14901,X14902),inference(resolution,[status(thm)],[c20314, c359])).
% 126.16/126.33 cnf(c27687,plain,cyclic(X14921,X14924,X14923,X14922),inference(resolution,[status(thm)],[c20331, c20314])).
% 126.16/126.33 cnf(c27688,plain,$false,inference(resolution,[status(thm)],[c27687, c24])).
% 126.16/126.33 % SZS output end CNFRefutation
% 126.16/126.33
% 126.16/126.33 % Initial clauses : 136
% 126.16/126.33 % Processed clauses : 4090
% 126.16/126.33 % Factors computed : 191
% 126.16/126.33 % Resolvents computed: 27092
% 126.16/126.33 % Tautologies deleted: 14
% 126.16/126.33 % Forward subsumed : 10039
% 126.16/126.33 % Backward subsumed : 3770
% 126.16/126.33 % -------- CPU Time ---------
% 126.16/126.33 % User time : 125.897 s
% 126.16/126.33 % System time : 0.071 s
% 126.16/126.33 % Total time : 125.968 s
%------------------------------------------------------------------------------