%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO619+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:25 EDT 2024
% Result : Theorem 157.03s 157.22s
% Output : Refutation 157.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO619+1 : TPTP v8.1.2. Released v7.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n005.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 08:37:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 157.03/157.22 % Version: 1.5
% 157.03/157.22 % SZS status Theorem
% 157.03/157.22 % SZS output start CNFRefutation
% 157.03/157.22 fof(exemplo6GDDFULL8110981,conjecture,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(((((((((((perp(C,A,C,B)&cong(A,C,B,C))&coll(D,A,B))&eqangle(E,C,C,A,A,C,C,D))&coll(E,A,B))&midp(F,D,E))&circle(F,E,NWPNT1,NWPNT2))&coll(G,C,E))&circle(F,E,G,NWPNT3))&coll(H,C,D))&circle(F,E,H,NWPNT4))=>cong(D,G,D,H)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exemplo6GDDFULL8110981)).
% 157.03/157.22 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:(![G]:(![H]:(![NWPNT1]:(![NWPNT2]:(![NWPNT3]:(![NWPNT4]:(((((((((((perp(C,A,C,B)&cong(A,C,B,C))&coll(D,A,B))&eqangle(E,C,C,A,A,C,C,D))&coll(E,A,B))&midp(F,D,E))&circle(F,E,NWPNT1,NWPNT2))&coll(G,C,E))&circle(F,E,G,NWPNT3))&coll(H,C,D))&circle(F,E,H,NWPNT4))=>cong(D,G,D,H))))))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL8110981])).
% 157.03/157.22 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(?[NWPNT1]:(?[NWPNT2]:(?[NWPNT3]:(?[NWPNT4]:(((((((((((perp(C,A,C,B)&cong(A,C,B,C))&coll(D,A,B))&eqangle(E,C,C,A,A,C,C,D))&coll(E,A,B))&midp(F,D,E))&circle(F,E,NWPNT1,NWPNT2))&coll(G,C,E))&circle(F,E,G,NWPNT3))&coll(H,C,D))&circle(F,E,H,NWPNT4))&~cong(D,G,D,H)))))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 157.03/157.23 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(?[F]:(?[G]:(?[H]:(((((((((((perp(C,A,C,B)&cong(A,C,B,C))&coll(D,A,B))&eqangle(E,C,C,A,A,C,C,D))&coll(E,A,B))&midp(F,D,E))&(?[NWPNT1]:(?[NWPNT2]:circle(F,E,NWPNT1,NWPNT2))))&coll(G,C,E))&(?[NWPNT3]:circle(F,E,G,NWPNT3)))&coll(H,C,D))&(?[NWPNT4]:circle(F,E,H,NWPNT4)))&~cong(D,G,D,H)))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 157.03/157.23 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((((perp(X4,X2,X4,X3)&cong(X2,X4,X3,X4))&coll(X5,X2,X3))&eqangle(X6,X4,X4,X2,X2,X4,X4,X5))&coll(X6,X2,X3))&midp(X7,X5,X6))&(?[X10]:(?[X11]:circle(X7,X6,X10,X11))))&coll(X8,X4,X6))&(?[X12]:circle(X7,X6,X8,X12)))&coll(X9,X4,X5))&(?[X13]:circle(X7,X6,X9,X13)))&~cong(X5,X8,X5,X9)))))))))),inference(variable_rename,[status(thm)],[c13])).
% 157.03/157.23 fof(c15,negated_conjecture,(((((((((((perp(skolem0003,skolem0001,skolem0003,skolem0002)&cong(skolem0001,skolem0003,skolem0002,skolem0003))&coll(skolem0004,skolem0001,skolem0002))&eqangle(skolem0005,skolem0003,skolem0003,skolem0001,skolem0001,skolem0003,skolem0003,skolem0004))&coll(skolem0005,skolem0001,skolem0002))&midp(skolem0006,skolem0004,skolem0005))&circle(skolem0006,skolem0005,skolem0009,skolem0010))&coll(skolem0007,skolem0003,skolem0005))&circle(skolem0006,skolem0005,skolem0007,skolem0011))&coll(skolem0008,skolem0003,skolem0004))&circle(skolem0006,skolem0005,skolem0008,skolem0012))&~cong(skolem0004,skolem0007,skolem0004,skolem0008)),inference(skolemize,[status(esa)],[c14])).
% 157.03/157.23 cnf(c27,negated_conjecture,~cong(skolem0004,skolem0007,skolem0004,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c342,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD23])).
% 157.03/157.23 fof(c343,plain,(![X414]:(![X415]:(![X416]:(![X417]:(~cong(X414,X415,X416,X417)|cong(X414,X415,X417,X416)))))),inference(variable_rename,[status(thm)],[c342])).
% 157.03/157.23 cnf(c344,plain,~cong(X698,X701,X699,X700)|cong(X698,X701,X700,X699),inference(split_conjunct,[status(thm)],[c343])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c339,plain,(![A]:(![B]:(![C]:(![D]:(~cong(A,B,C,D)|cong(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD24])).
% 157.03/157.23 fof(c340,plain,(![X410]:(![X411]:(![X412]:(![X413]:(~cong(X410,X411,X412,X413)|cong(X412,X413,X410,X411)))))),inference(variable_rename,[status(thm)],[c339])).
% 157.03/157.23 cnf(c341,plain,~cong(X691,X690,X689,X692)|cong(X689,X692,X691,X690),inference(split_conjunct,[status(thm)],[c340])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c242,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])).
% 157.03/157.23 fof(c243,plain,(![X236]:(![X237]:(![X238]:(![X239]:((~perp(X236,X237,X237,X238)|~midp(X239,X236,X238))|cong(X236,X239,X237,X239)))))),inference(variable_rename,[status(thm)],[c242])).
% 157.03/157.23 cnf(c244,plain,~perp(X1001,X1002,X1002,X1003)|~midp(X1000,X1001,X1003)|cong(X1001,X1000,X1002,X1000),inference(split_conjunct,[status(thm)],[c243])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c392,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 157.03/157.23 fof(c393,plain,(![X507]:(![X508]:(![X509]:(![X510]:(~perp(X507,X508,X509,X510)|perp(X507,X508,X510,X509)))))),inference(variable_rename,[status(thm)],[c392])).
% 157.03/157.23 cnf(c394,plain,~perp(X756,X758,X755,X757)|perp(X756,X758,X757,X755),inference(split_conjunct,[status(thm)],[c393])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 157.03/157.23 fof(c390,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X505,X506,X503,X504)))))),inference(variable_rename,[status(thm)],[c389])).
% 157.03/157.23 cnf(c391,plain,~perp(X753,X754,X752,X751)|perp(X752,X751,X753,X754),inference(split_conjunct,[status(thm)],[c390])).
% 157.03/157.23 fof(ruleD12,axiom,(![A]:(![B]:(![C]:(![O]:((cong(O,A,O,B)&cong(O,A,O,C))=>circle(O,A,B,C)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD12)).
% 157.03/157.23 fof(c377,plain,(![A]:(![B]:(![C]:(![O]:((~cong(O,A,O,B)|~cong(O,A,O,C))|circle(O,A,B,C)))))),inference(fof_nnf,[status(thm)],[ruleD12])).
% 157.03/157.23 fof(c378,plain,(![X484]:(![X485]:(![X486]:(![X487]:((~cong(X487,X484,X487,X485)|~cong(X487,X484,X487,X486))|circle(X487,X484,X485,X486)))))),inference(variable_rename,[status(thm)],[c377])).
% 157.03/157.23 cnf(c379,plain,~cong(X1241,X1244,X1241,X1242)|~cong(X1241,X1244,X1241,X1243)|circle(X1241,X1244,X1242,X1243),inference(split_conjunct,[status(thm)],[c378])).
% 157.03/157.23 cnf(c1636,plain,~cong(X1275,X1273,X1275,X1274)|circle(X1275,X1273,X1274,X1274),inference(factor,[status(thm)],[c379])).
% 157.03/157.23 fof(ruleD68,axiom,(![A]:(![B]:(![C]:(midp(A,B,C)=>cong(A,B,A,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD68)).
% 157.03/157.23 fof(c187,plain,(![A]:(![B]:(![C]:(~midp(A,B,C)|cong(A,B,A,C))))),inference(fof_nnf,[status(thm)],[ruleD68])).
% 157.03/157.23 fof(c188,plain,(![X162]:(![X163]:(![X164]:(~midp(X162,X163,X164)|cong(X162,X163,X162,X164))))),inference(variable_rename,[status(thm)],[c187])).
% 157.03/157.23 cnf(c189,plain,~midp(X681,X680,X682)|cong(X681,X680,X681,X682),inference(split_conjunct,[status(thm)],[c188])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c401,plain,(![A]:(![B]:(![C]:(![D]:(~para(A,B,C,D)|para(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD4])).
% 157.03/157.23 fof(c402,plain,(![X521]:(![X522]:(![X523]:(![X524]:(~para(X521,X522,X523,X524)|para(X521,X522,X524,X523)))))),inference(variable_rename,[status(thm)],[c401])).
% 157.03/157.23 cnf(c403,plain,~para(X779,X778,X777,X780)|para(X779,X778,X780,X777),inference(split_conjunct,[status(thm)],[c402])).
% 157.03/157.23 cnf(c21,negated_conjecture,midp(skolem0006,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c15])).
% 157.03/157.23 fof(ruleD11,axiom,(![A]:(![B]:(![M]:(midp(M,B,A)=>midp(M,A,B))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD11)).
% 157.03/157.23 fof(c380,plain,(![A]:(![B]:(![M]:(~midp(M,B,A)|midp(M,A,B))))),inference(fof_nnf,[status(thm)],[ruleD11])).
% 157.03/157.23 fof(c381,plain,(![X488]:(![X489]:(![X490]:(~midp(X490,X489,X488)|midp(X490,X488,X489))))),inference(variable_rename,[status(thm)],[c380])).
% 157.03/157.23 cnf(c382,plain,~midp(X563,X562,X564)|midp(X563,X564,X562),inference(split_conjunct,[status(thm)],[c381])).
% 157.03/157.23 cnf(c422,plain,midp(skolem0006,skolem0005,skolem0004),inference(resolution,[status(thm)],[c382, c21])).
% 157.03/157.23 fof(ruleD63,axiom,(![A]:(![B]:(![C]:(![D]:(![M]:((midp(M,A,B)&midp(M,C,D))=>para(A,C,B,D))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD63)).
% 157.03/157.23 fof(c202,plain,(![A]:(![B]:(![C]:(![D]:(![M]:((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))))))),inference(fof_nnf,[status(thm)],[ruleD63])).
% 157.03/157.23 fof(c203,plain,(![A]:(![B]:(![C]:(![D]:((![M]:(~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D)))))),inference(shift_quantors,[status(thm)],[c202])).
% 157.03/157.23 fof(c205,plain,(![X181]:(![X182]:(![X183]:(![X184]:(![X185]:((~midp(X185,X181,X182)|~midp(X185,X183,X184))|para(X181,X183,X182,X184))))))),inference(shift_quantors,[status(thm)],[fof(c204,plain,(![X181]:(![X182]:(![X183]:(![X184]:((![X185]:(~midp(X185,X181,X182)|~midp(X185,X183,X184)))|para(X181,X183,X182,X184)))))),inference(variable_rename,[status(thm)],[c203])).])).
% 157.03/157.23 cnf(c206,plain,~midp(X953,X951,X952)|~midp(X953,X954,X955)|para(X951,X954,X952,X955),inference(split_conjunct,[status(thm)],[c205])).
% 157.03/157.23 cnf(c1238,plain,~midp(skolem0006,X2362,X2363)|para(X2362,skolem0005,X2363,skolem0004),inference(resolution,[status(thm)],[c206, c422])).
% 157.03/157.23 cnf(c6450,plain,para(skolem0004,skolem0005,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1238, c21])).
% 157.03/157.23 cnf(c6460,plain,para(skolem0004,skolem0005,skolem0004,skolem0005),inference(resolution,[status(thm)],[c6450, c403])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c199,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])).
% 157.03/157.23 fof(c200,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)],[c199])).
% 157.03/157.23 cnf(c201,plain,~midp(X950,X946,X949)|~para(X946,X947,X949,X948)|~para(X946,X948,X949,X947)|midp(X950,X947,X948),inference(split_conjunct,[status(thm)],[c200])).
% 157.03/157.23 cnf(c1224,plain,~midp(X2386,X2387,X2389)|~para(X2387,X2388,X2389,X2388)|midp(X2386,X2388,X2388),inference(factor,[status(thm)],[c201])).
% 157.03/157.23 cnf(c6564,plain,~midp(X4539,skolem0004,skolem0004)|midp(X4539,skolem0005,skolem0005),inference(resolution,[status(thm)],[c1224, c6460])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c228,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])).
% 157.03/157.23 fof(c229,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)],[c228])).
% 157.03/157.23 cnf(c230,plain,~cong(X985,X987,X984,X987)|~cong(X985,X986,X984,X986)|perp(X985,X984,X987,X986),inference(split_conjunct,[status(thm)],[c229])).
% 157.03/157.23 cnf(c1313,plain,~cong(X1152,X1150,X1151,X1150)|perp(X1152,X1151,X1150,X1150),inference(factor,[status(thm)],[c230])).
% 157.03/157.23 cnf(c518,plain,cong(skolem0006,skolem0005,skolem0006,skolem0004),inference(resolution,[status(thm)],[c189, c422])).
% 157.03/157.23 cnf(c530,plain,cong(skolem0006,skolem0005,skolem0004,skolem0006),inference(resolution,[status(thm)],[c344, c518])).
% 157.03/157.23 cnf(c538,plain,cong(skolem0004,skolem0006,skolem0006,skolem0005),inference(resolution,[status(thm)],[c530, c341])).
% 157.03/157.23 cnf(c548,plain,cong(skolem0004,skolem0006,skolem0005,skolem0006),inference(resolution,[status(thm)],[c538, c344])).
% 157.03/157.23 cnf(c519,plain,cong(skolem0006,skolem0004,skolem0006,skolem0005),inference(resolution,[status(thm)],[c189, c21])).
% 157.03/157.23 cnf(c529,plain,cong(skolem0006,skolem0004,skolem0005,skolem0006),inference(resolution,[status(thm)],[c344, c519])).
% 157.03/157.23 cnf(c535,plain,cong(skolem0005,skolem0006,skolem0006,skolem0004),inference(resolution,[status(thm)],[c529, c341])).
% 157.03/157.23 cnf(c545,plain,cong(skolem0005,skolem0006,skolem0004,skolem0006),inference(resolution,[status(thm)],[c535, c344])).
% 157.03/157.23 fof(ruleD25,axiom,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((cong(A,B,C,D)&cong(C,D,E,F))=>cong(A,B,E,F)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD25)).
% 157.03/157.23 fof(c336,plain,(![A]:(![B]:(![C]:(![D]:(![E]:(![F]:((~cong(A,B,C,D)|~cong(C,D,E,F))|cong(A,B,E,F)))))))),inference(fof_nnf,[status(thm)],[ruleD25])).
% 157.03/157.23 fof(c337,plain,(![X404]:(![X405]:(![X406]:(![X407]:(![X408]:(![X409]:((~cong(X404,X405,X406,X407)|~cong(X406,X407,X408,X409))|cong(X404,X405,X408,X409)))))))),inference(variable_rename,[status(thm)],[c336])).
% 157.03/157.23 cnf(c338,plain,~cong(X1180,X1179,X1178,X1182)|~cong(X1178,X1182,X1181,X1177)|cong(X1180,X1179,X1181,X1177),inference(split_conjunct,[status(thm)],[c337])).
% 157.03/157.23 cnf(c1527,plain,~cong(X2772,X2771,skolem0005,skolem0006)|cong(X2772,X2771,skolem0004,skolem0006),inference(resolution,[status(thm)],[c338, c545])).
% 157.03/157.23 cnf(c8245,plain,cong(skolem0004,skolem0006,skolem0004,skolem0006),inference(resolution,[status(thm)],[c1527, c548])).
% 157.03/157.23 cnf(c8248,plain,perp(skolem0004,skolem0004,skolem0006,skolem0006),inference(resolution,[status(thm)],[c8245, c1313])).
% 157.03/157.23 cnf(c1458,plain,perp(skolem0005,skolem0004,skolem0006,skolem0006),inference(resolution,[status(thm)],[c1313, c545])).
% 157.03/157.23 cnf(c1469,plain,perp(skolem0006,skolem0006,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1458, c391])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c386,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])).
% 157.03/157.23 fof(c387,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)],[c386])).
% 157.03/157.23 cnf(c388,plain,~perp(X1256,X1252,X1251,X1253)|~perp(X1251,X1253,X1255,X1254)|para(X1256,X1252,X1255,X1254),inference(split_conjunct,[status(thm)],[c387])).
% 157.03/157.23 cnf(c1677,plain,~perp(X2984,X2983,skolem0006,skolem0006)|para(X2984,X2983,skolem0005,skolem0004),inference(resolution,[status(thm)],[c388, c1469])).
% 157.03/157.23 cnf(c9457,plain,para(skolem0004,skolem0004,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1677, c8248])).
% 157.03/157.23 cnf(c9762,plain,~midp(X4868,skolem0004,skolem0005)|midp(X4868,skolem0004,skolem0004),inference(resolution,[status(thm)],[c9457, c1224])).
% 157.03/157.23 cnf(c19610,plain,midp(skolem0006,skolem0004,skolem0004),inference(resolution,[status(thm)],[c9762, c21])).
% 157.03/157.23 cnf(c19628,plain,midp(skolem0006,skolem0005,skolem0005),inference(resolution,[status(thm)],[c19610, c6564])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c290,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])).
% 157.03/157.23 fof(c291,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)],[c290])).
% 157.03/157.23 fof(c293,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(c292,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)],[c291])).])).
% 157.03/157.23 cnf(c294,plain,~eqangle(X1065,X1067,X1069,X1066,X1068,X1064,X1069,X1066)|para(X1065,X1067,X1068,X1064),inference(split_conjunct,[status(thm)],[c293])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c354,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])).
% 157.03/157.23 fof(c355,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)],[c354])).
% 157.03/157.23 cnf(c356,plain,~eqangle(X1218,X1219,X1217,X1220,X1222,X1216,X1215,X1221)|eqangle(X1217,X1220,X1218,X1219,X1215,X1221,X1222,X1216),inference(split_conjunct,[status(thm)],[c355])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c285,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])).
% 157.03/157.23 fof(c286,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)],[c285])).
% 157.03/157.23 fof(c288,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(c287,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)],[c286])).])).
% 157.03/157.23 cnf(c289,plain,~para(X1061,X1062,X1058,X1060)|eqangle(X1061,X1062,X1063,X1059,X1058,X1060,X1063,X1059),inference(split_conjunct,[status(thm)],[c288])).
% 157.03/157.23 cnf(c6498,plain,eqangle(skolem0004,skolem0005,X4531,X4532,skolem0004,skolem0005,X4531,X4532),inference(resolution,[status(thm)],[c6460, c289])).
% 157.03/157.23 cnf(c18077,plain,eqangle(X5460,X5459,skolem0004,skolem0005,X5460,X5459,skolem0004,skolem0005),inference(resolution,[status(thm)],[c6498, c356])).
% 157.03/157.23 cnf(c23448,plain,para(X5462,X5461,X5462,X5461),inference(resolution,[status(thm)],[c18077, c294])).
% 157.03/157.23 cnf(c23497,plain,~midp(X7584,X7586,X7586)|midp(X7584,X7585,X7585),inference(resolution,[status(thm)],[c23448, c1224])).
% 157.03/157.23 cnf(c34983,plain,midp(skolem0006,X7589,X7589),inference(resolution,[status(thm)],[c23497, c19628])).
% 157.03/157.23 cnf(c35558,plain,cong(skolem0006,X7629,skolem0006,X7629),inference(resolution,[status(thm)],[c34983, c189])).
% 157.03/157.23 cnf(c35997,plain,circle(skolem0006,X7634,X7634,X7634),inference(resolution,[status(thm)],[c35558, c1636])).
% 157.03/157.23 fof(ruleD49,axiom,(![A]:(![B]:(![C]:(![O]:(![X]:((circle(O,A,B,C)&eqangle(A,X,A,B,C,A,C,B))=>perp(O,A,A,X))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO012+0.ax', ruleD49)).
% 157.03/157.23 fof(c251,plain,(![A]:(![B]:(![C]:(![O]:(![X]:((~circle(O,A,B,C)|~eqangle(A,X,A,B,C,A,C,B))|perp(O,A,A,X))))))),inference(fof_nnf,[status(thm)],[ruleD49])).
% 157.03/157.23 fof(c252,plain,(![X250]:(![X251]:(![X252]:(![X253]:(![X254]:((~circle(X253,X250,X251,X252)|~eqangle(X250,X254,X250,X251,X252,X250,X252,X251))|perp(X253,X250,X250,X254))))))),inference(variable_rename,[status(thm)],[c251])).
% 157.03/157.23 cnf(c253,plain,~circle(X1018,X1014,X1017,X1016)|~eqangle(X1014,X1015,X1014,X1017,X1016,X1014,X1016,X1017)|perp(X1018,X1014,X1014,X1015),inference(split_conjunct,[status(thm)],[c252])).
% 157.03/157.23 cnf(c23470,plain,eqangle(X7572,X7570,X7569,X7571,X7572,X7570,X7569,X7571),inference(resolution,[status(thm)],[c23448, c289])).
% 157.03/157.23 cnf(c34969,plain,~circle(X9702,X9701,X9703,X9701)|perp(X9702,X9701,X9701,X9701),inference(resolution,[status(thm)],[c23470, c253])).
% 157.03/157.23 cnf(c39486,plain,perp(skolem0006,X9705,X9705,X9705),inference(resolution,[status(thm)],[c34969, c35997])).
% 157.03/157.23 cnf(c39515,plain,perp(X9712,X9712,skolem0006,X9712),inference(resolution,[status(thm)],[c39486, c391])).
% 157.03/157.23 cnf(c39559,plain,perp(X9715,X9715,X9715,skolem0006),inference(resolution,[status(thm)],[c39515, c394])).
% 157.03/157.23 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)).
% 157.03/157.23 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(fof_nnf,[status(thm)],[ruleD74])).
% 157.03/157.23 fof(c164,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)],[c163])).
% 157.03/157.23 fof(c166,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(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(variable_rename,[status(thm)],[c164])).])).
% 157.03/157.23 cnf(c167,plain,~eqangle(X914,X909,X910,X913,X915,X908,X912,X911)|~perp(X915,X908,X912,X911)|perp(X914,X909,X910,X913),inference(split_conjunct,[status(thm)],[c166])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c348,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])).
% 157.03/157.23 fof(c349,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)],[c348])).
% 157.03/157.23 cnf(c350,plain,~eqangle(X1203,X1200,X1204,X1202,X1205,X1201,X1206,X1199)|eqangle(X1203,X1200,X1205,X1201,X1204,X1202,X1206,X1199),inference(split_conjunct,[status(thm)],[c349])).
% 157.03/157.23 cnf(c34978,plain,eqangle(X8392,X8393,X8392,X8393,X8390,X8391,X8390,X8391),inference(resolution,[status(thm)],[c23470, c350])).
% 157.03/157.23 cnf(c38189,plain,~perp(X10509,X10510,X10509,X10510)|perp(X10507,X10508,X10507,X10508),inference(resolution,[status(thm)],[c34978, c167])).
% 157.03/157.23 cnf(c41323,plain,perp(X10514,X10515,X10514,X10515),inference(resolution,[status(thm)],[c38189, c39559])).
% 157.03/157.23 cnf(c41354,plain,perp(X10587,X10588,X10588,X10587),inference(resolution,[status(thm)],[c41323, c394])).
% 157.03/157.23 cnf(c41430,plain,~midp(X10773,X10772,X10772)|cong(X10772,X10773,X10771,X10773),inference(resolution,[status(thm)],[c41354, c244])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c404,plain,(![A]:(![B]:(![C]:(![D]:((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A)))))),inference(fof_nnf,[status(thm)],[ruleD3])).
% 157.03/157.23 fof(c405,plain,(![X525]:(![X526]:(![X527]:(![X528]:((~coll(X525,X526,X527)|~coll(X525,X526,X528))|coll(X527,X528,X525)))))),inference(variable_rename,[status(thm)],[c404])).
% 157.03/157.23 cnf(c406,plain,~coll(X792,X791,X793)|~coll(X792,X791,X794)|coll(X793,X794,X792),inference(split_conjunct,[status(thm)],[c405])).
% 157.03/157.23 cnf(c642,plain,~coll(X797,X795,X796)|coll(X796,X796,X797),inference(factor,[status(thm)],[c406])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c193,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 157.03/157.23 fof(c194,plain,(![X168]:(![X169]:(![X170]:(~para(X168,X169,X168,X170)|coll(X168,X169,X170))))),inference(variable_rename,[status(thm)],[c193])).
% 157.03/157.23 cnf(c195,plain,~para(X688,X686,X688,X687)|coll(X688,X686,X687),inference(split_conjunct,[status(thm)],[c194])).
% 157.03/157.23 cnf(c23480,plain,coll(X5463,X5464,X5464),inference(resolution,[status(thm)],[c23448, c195])).
% 157.03/157.23 cnf(c23536,plain,coll(X5466,X5466,X5465),inference(resolution,[status(thm)],[c23480, c642])).
% 157.03/157.23 cnf(c24311,plain,~coll(X8160,X8160,X8162)|coll(X8162,X8161,X8160),inference(resolution,[status(thm)],[c23536, c406])).
% 157.03/157.23 cnf(c37611,plain,coll(X8167,X8166,X8165),inference(resolution,[status(thm)],[c24311, c23536])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c190,plain,(![A]:(![B]:(![C]:((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD67])).
% 157.03/157.23 fof(c191,plain,(![X165]:(![X166]:(![X167]:((~cong(X165,X166,X165,X167)|~coll(X165,X166,X167))|midp(X165,X166,X167))))),inference(variable_rename,[status(thm)],[c190])).
% 157.03/157.23 cnf(c192,plain,~cong(X939,X938,X939,X940)|~coll(X939,X938,X940)|midp(X939,X938,X940),inference(split_conjunct,[status(thm)],[c191])).
% 157.03/157.23 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)).
% 157.03/157.23 fof(c275,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])).
% 157.03/157.23 fof(c276,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)],[c275])).
% 157.03/157.23 cnf(c277,plain,~eqangle(X1049,X1046,X1049,X1047,X1048,X1046,X1048,X1047)|~coll(X1049,X1048,X1047)|cyclic(X1046,X1047,X1049,X1048),inference(split_conjunct,[status(thm)],[c276])).
% 157.03/157.23 cnf(c34977,plain,~coll(X8803,X8803,X8802)|cyclic(X8804,X8802,X8803,X8803),inference(resolution,[status(thm)],[c23470, c277])).
% 157.03/157.23 cnf(c38943,plain,cyclic(X8805,X8806,X8807,X8807),inference(resolution,[status(thm)],[c34977, c37611])).
% 157.03/157.23 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)).
% 157.03/157.23 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(fof_nnf,[status(thm)],[ruleD43])).
% 157.03/157.23 fof(c271,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)],[c270])).
% 157.03/157.23 fof(c273,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(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(variable_rename,[status(thm)],[c271])).])).
% 157.03/157.23 cnf(c274,plain,~cyclic(X1043,X1044,X1042,X1040)|~cyclic(X1043,X1044,X1042,X1041)|~cyclic(X1043,X1044,X1042,X1045)|~eqangle(X1042,X1043,X1042,X1044,X1045,X1040,X1045,X1041)|cong(X1043,X1044,X1040,X1041),inference(split_conjunct,[status(thm)],[c273])).
% 157.03/157.23 cnf(c23486,plain,para(X5488,X5489,X5489,X5488),inference(resolution,[status(thm)],[c23448, c403])).
% 157.03/157.23 cnf(c25302,plain,eqangle(X8359,X8361,X8358,X8360,X8361,X8359,X8358,X8360),inference(resolution,[status(thm)],[c23486, c289])).
% 157.03/157.23 cnf(c38117,plain,eqangle(X8539,X8537,X8540,X8538,X8539,X8537,X8538,X8540),inference(resolution,[status(thm)],[c25302, c356])).
% 157.03/157.23 cnf(c38424,plain,eqangle(X8628,X8629,X8628,X8629,X8627,X8626,X8626,X8627),inference(resolution,[status(thm)],[c38117, c350])).
% 157.03/157.23 cnf(c38574,plain,~cyclic(X11380,X11380,X11381,X11382)|cong(X11380,X11380,X11382,X11382),inference(resolution,[status(thm)],[c38424, c274])).
% 157.03/157.23 cnf(c43434,plain,cong(X11383,X11383,X11384,X11384),inference(resolution,[status(thm)],[c38574, c38943])).
% 157.03/157.23 cnf(c43457,plain,~coll(X11407,X11407,X11407)|midp(X11407,X11407,X11407),inference(resolution,[status(thm)],[c43434, c192])).
% 157.03/157.23 cnf(c43469,plain,midp(X11411,X11411,X11411),inference(resolution,[status(thm)],[c43457, c37611])).
% 157.03/157.23 cnf(c43860,plain,midp(X11413,X11414,X11414),inference(resolution,[status(thm)],[c43469, c23497])).
% 157.03/157.23 cnf(c44412,plain,cong(X11445,X11447,X11446,X11447),inference(resolution,[status(thm)],[c43860, c41430])).
% 157.03/157.23 cnf(c44557,plain,cong(X11483,X11485,X11485,X11484),inference(resolution,[status(thm)],[c44412, c344])).
% 157.03/157.23 cnf(c44749,plain,cong(X11544,X11545,X11546,X11544),inference(resolution,[status(thm)],[c44557, c341])).
% 157.03/157.23 cnf(c44879,plain,cong(X11582,X11580,X11582,X11581),inference(resolution,[status(thm)],[c44749, c344])).
% 157.03/157.23 cnf(c44922,plain,$false,inference(resolution,[status(thm)],[c44879, c27])).
% 157.03/157.23 % SZS output end CNFRefutation
% 157.03/157.23
% 157.03/157.23 % Initial clauses : 139
% 157.03/157.23 % Processed clauses : 4803
% 157.03/157.23 % Factors computed : 230
% 157.03/157.23 % Resolvents computed: 44301
% 157.03/157.23 % Tautologies deleted: 22
% 157.03/157.23 % Forward subsumed : 11406
% 157.03/157.23 % Backward subsumed : 2722
% 157.03/157.23 % -------- CPU Time ---------
% 157.03/157.23 % User time : 156.761 s
% 157.03/157.23 % System time : 0.093 s
% 157.03/157.23 % Total time : 156.854 s
%------------------------------------------------------------------------------