%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO585+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:20 EDT 2024
% Result : Theorem 45.38s 45.64s
% Output : Refutation 45.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO585+1 : TPTP v8.1.2. Released v7.5.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n024.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:53:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 45.38/45.64 % Version: 1.5
% 45.38/45.64 % SZS status Theorem
% 45.38/45.64 % SZS output start CNFRefutation
% 45.38/45.64 fof(exemplo6GDDFULL416047,conjecture,(![A]:(![B]:(![C]:(![O]:(![D]:(![U]:(![V]:(![NWPNT1]:((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))=>cyclic(A,U,D,V)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', exemplo6GDDFULL416047)).
% 45.38/45.64 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(![O]:(![D]:(![U]:(![V]:(![NWPNT1]:((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))=>cyclic(A,U,D,V))))))))))),inference(assume_negation,[status(cth)],[exemplo6GDDFULL416047])).
% 45.38/45.64 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[U]:(?[V]:(?[NWPNT1]:((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))&~cyclic(A,U,D,V)))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 45.38/45.64 fof(c13,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[O]:(?[D]:(?[U]:(?[V]:((((((((circle(O,A,B,C)&(?[NWPNT1]:circle(O,A,D,NWPNT1)))&perp(A,B,D,U))&perp(A,D,B,U))&perp(B,D,A,U))&perp(A,C,D,V))&perp(A,D,C,V))&perp(C,D,A,V))&~cyclic(A,U,D,V))))))))),inference(shift_quantors,[status(thm)],[c12])).
% 45.38/45.64 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((((((((circle(X5,X2,X3,X4)&(?[X9]:circle(X5,X2,X6,X9)))&perp(X2,X3,X6,X7))&perp(X2,X6,X3,X7))&perp(X3,X6,X2,X7))&perp(X2,X4,X6,X8))&perp(X2,X6,X4,X8))&perp(X4,X6,X2,X8))&~cyclic(X2,X7,X6,X8))))))))),inference(variable_rename,[status(thm)],[c13])).
% 45.38/45.64 fof(c15,negated_conjecture,((((((((circle(skolem0004,skolem0001,skolem0002,skolem0003)&circle(skolem0004,skolem0001,skolem0005,skolem0008))&perp(skolem0001,skolem0002,skolem0005,skolem0006))&perp(skolem0001,skolem0005,skolem0002,skolem0006))&perp(skolem0002,skolem0005,skolem0001,skolem0006))&perp(skolem0001,skolem0003,skolem0005,skolem0007))&perp(skolem0001,skolem0005,skolem0003,skolem0007))&perp(skolem0003,skolem0005,skolem0001,skolem0007))&~cyclic(skolem0001,skolem0006,skolem0005,skolem0007)),inference(skolemize,[status(esa)],[c14])).
% 45.38/45.64 cnf(c24,negated_conjecture,~cyclic(skolem0001,skolem0006,skolem0005,skolem0007),inference(split_conjunct,[status(thm)],[c15])).
% 45.38/45.64 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)).
% 45.38/45.64 fof(c366,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD14])).
% 45.38/45.64 fof(c367,plain,(![X471]:(![X472]:(![X473]:(![X474]:(~cyclic(X471,X472,X473,X474)|cyclic(X471,X472,X474,X473)))))),inference(variable_rename,[status(thm)],[c366])).
% 45.38/45.64 cnf(c368,plain,~cyclic(X597,X599,X598,X600)|cyclic(X597,X599,X600,X598),inference(split_conjunct,[status(thm)],[c367])).
% 45.38/45.64 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)).
% 45.38/45.64 fof(c360,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(B,A,C,D)))))),inference(fof_nnf,[status(thm)],[ruleD16])).
% 45.38/45.64 fof(c361,plain,(![X463]:(![X464]:(![X465]:(![X466]:(~cyclic(X463,X464,X465,X466)|cyclic(X464,X463,X465,X466)))))),inference(variable_rename,[status(thm)],[c360])).
% 45.38/45.64 cnf(c362,plain,~cyclic(X592,X591,X589,X590)|cyclic(X591,X592,X589,X590),inference(split_conjunct,[status(thm)],[c361])).
% 45.38/45.64 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)).
% 45.38/45.64 fof(c363,plain,(![A]:(![B]:(![C]:(![D]:(~cyclic(A,B,C,D)|cyclic(A,C,B,D)))))),inference(fof_nnf,[status(thm)],[ruleD15])).
% 45.38/45.64 fof(c364,plain,(![X467]:(![X468]:(![X469]:(![X470]:(~cyclic(X467,X468,X469,X470)|cyclic(X467,X469,X468,X470)))))),inference(variable_rename,[status(thm)],[c363])).
% 45.38/45.64 cnf(c365,plain,~cyclic(X594,X595,X593,X596)|cyclic(X594,X593,X595,X596),inference(split_conjunct,[status(thm)],[c364])).
% 45.38/45.64 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)).
% 45.38/45.64 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])).
% 45.38/45.64 fof(c402,plain,(![X521]:(![X522]:(![X523]:(![X524]:((~coll(X521,X522,X523)|~coll(X521,X522,X524))|coll(X523,X524,X521)))))),inference(variable_rename,[status(thm)],[c401])).
% 45.38/45.64 cnf(c403,plain,~coll(X777,X775,X776)|~coll(X777,X775,X778)|coll(X776,X778,X777),inference(split_conjunct,[status(thm)],[c402])).
% 45.38/45.64 cnf(c564,plain,~coll(X780,X781,X779)|coll(X779,X779,X780),inference(factor,[status(thm)],[c403])).
% 45.38/45.64 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)).
% 45.38/45.64 fof(c190,plain,(![A]:(![B]:(![C]:(~para(A,B,A,C)|coll(A,B,C))))),inference(fof_nnf,[status(thm)],[ruleD66])).
% 45.38/45.64 fof(c191,plain,(![X164]:(![X165]:(![X166]:(~para(X164,X165,X164,X166)|coll(X164,X165,X166))))),inference(variable_rename,[status(thm)],[c190])).
% 45.38/45.64 cnf(c192,plain,~para(X571,X572,X571,X570)|coll(X571,X572,X570),inference(split_conjunct,[status(thm)],[c191])).
% 45.38/45.64 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)).
% 45.38/45.64 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])).
% 45.38/45.64 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])).
% 45.38/45.64 fof(c290,plain,(![X296]:(![X297]:(![X298]:(![X299]:(![X300]:(![X301]:(~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)|para(X296,X297,X298,X299)))))))),inference(shift_quantors,[status(thm)],[fof(c289,plain,(![X296]:(![X297]:(![X298]:(![X299]:((![X300]:(![X301]:~eqangle(X296,X297,X300,X301,X298,X299,X300,X301)))|para(X296,X297,X298,X299)))))),inference(variable_rename,[status(thm)],[c288])).])).
% 45.38/45.64 cnf(c291,plain,~eqangle(X828,X830,X829,X826,X825,X827,X829,X826)|para(X828,X830,X825,X827),inference(split_conjunct,[status(thm)],[c290])).
% 45.38/45.64 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)).
% 45.38/45.64 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])).
% 45.38/45.64 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])).
% 45.38/45.64 fof(c285,plain,(![X290]:(![X291]:(![X292]:(![X293]:(![X294]:(![X295]:(~para(X290,X291,X292,X293)|eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(shift_quantors,[status(thm)],[fof(c284,plain,(![X290]:(![X291]:(![X292]:(![X293]:(~para(X290,X291,X292,X293)|(![X294]:(![X295]:eqangle(X290,X291,X294,X295,X292,X293,X294,X295)))))))),inference(variable_rename,[status(thm)],[c283])).])).
% 45.38/45.64 cnf(c286,plain,~para(X819,X824,X821,X820)|eqangle(X819,X824,X823,X822,X821,X820,X823,X822),inference(split_conjunct,[status(thm)],[c285])).
% 45.38/45.64 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)).
% 45.38/45.64 fof(c386,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(C,D,A,B)))))),inference(fof_nnf,[status(thm)],[ruleD8])).
% 45.38/45.64 fof(c387,plain,(![X499]:(![X500]:(![X501]:(![X502]:(~perp(X499,X500,X501,X502)|perp(X501,X502,X499,X500)))))),inference(variable_rename,[status(thm)],[c386])).
% 45.38/45.64 cnf(c388,plain,~perp(X610,X608,X607,X609)|perp(X607,X609,X610,X608),inference(split_conjunct,[status(thm)],[c387])).
% 45.38/45.64 cnf(c19,negated_conjecture,perp(skolem0001,skolem0005,skolem0002,skolem0006),inference(split_conjunct,[status(thm)],[c15])).
% 45.38/45.64 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)).
% 45.38/45.64 fof(c389,plain,(![A]:(![B]:(![C]:(![D]:(~perp(A,B,C,D)|perp(A,B,D,C)))))),inference(fof_nnf,[status(thm)],[ruleD7])).
% 45.38/45.64 fof(c390,plain,(![X503]:(![X504]:(![X505]:(![X506]:(~perp(X503,X504,X505,X506)|perp(X503,X504,X506,X505)))))),inference(variable_rename,[status(thm)],[c389])).
% 45.38/45.64 cnf(c391,plain,~perp(X629,X630,X627,X628)|perp(X629,X630,X628,X627),inference(split_conjunct,[status(thm)],[c390])).
% 45.38/45.64 cnf(c447,plain,perp(skolem0001,skolem0005,skolem0006,skolem0002),inference(resolution,[status(thm)],[c391, c19])).
% 45.38/45.64 cnf(c477,plain,perp(skolem0006,skolem0002,skolem0001,skolem0005),inference(resolution,[status(thm)],[c447, c388])).
% 45.38/45.64 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)).
% 45.38/45.64 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])).
% 45.38/45.64 fof(c384,plain,(![X493]:(![X494]:(![X495]:(![X496]:(![X497]:(![X498]:((~perp(X493,X494,X495,X496)|~perp(X495,X496,X497,X498))|para(X493,X494,X497,X498)))))))),inference(variable_rename,[status(thm)],[c383])).
% 45.38/45.64 cnf(c385,plain,~perp(X1117,X1116,X1119,X1118)|~perp(X1119,X1118,X1114,X1115)|para(X1117,X1116,X1114,X1115),inference(split_conjunct,[status(thm)],[c384])).
% 45.38/45.64 cnf(c874,plain,~perp(X1122,X1123,skolem0001,skolem0005)|para(X1122,X1123,skolem0006,skolem0002),inference(resolution,[status(thm)],[c385, c447])).
% 45.38/45.64 cnf(c923,plain,para(skolem0006,skolem0002,skolem0006,skolem0002),inference(resolution,[status(thm)],[c874, c477])).
% 45.38/45.64 cnf(c946,plain,eqangle(skolem0006,skolem0002,X1208,X1209,skolem0006,skolem0002,X1208,X1209),inference(resolution,[status(thm)],[c923, c286])).
% 45.38/45.64 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)).
% 45.38/45.64 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])).
% 45.38/45.64 fof(c352,plain,(![X442]:(![X443]:(![X444]:(![X445]:(![X446]:(![X447]:(![X448]:(![X449]:(~eqangle(X442,X443,X444,X445,X446,X447,X448,X449)|eqangle(X444,X445,X442,X443,X448,X449,X446,X447)))))))))),inference(variable_rename,[status(thm)],[c351])).
% 45.38/45.64 cnf(c353,plain,~eqangle(X1389,X1390,X1395,X1392,X1393,X1396,X1391,X1394)|eqangle(X1395,X1392,X1389,X1390,X1391,X1394,X1393,X1396),inference(split_conjunct,[status(thm)],[c352])).
% 45.38/45.64 cnf(c1457,plain,eqangle(X1612,X1611,skolem0006,skolem0002,X1612,X1611,skolem0006,skolem0002),inference(resolution,[status(thm)],[c353, c946])).
% 45.38/45.64 cnf(c1859,plain,para(X1613,X1614,X1613,X1614),inference(resolution,[status(thm)],[c1457, c291])).
% 45.38/45.64 cnf(c1871,plain,coll(X1615,X1616,X1616),inference(resolution,[status(thm)],[c1859, c192])).
% 45.38/45.64 cnf(c1932,plain,coll(X1621,X1621,X1622),inference(resolution,[status(thm)],[c1871, c564])).
% 45.38/45.64 cnf(c1963,plain,~coll(X1830,X1830,X1831)|coll(X1831,X1829,X1830),inference(resolution,[status(thm)],[c1932, c403])).
% 45.38/45.64 cnf(c2277,plain,coll(X1837,X1838,X1836),inference(resolution,[status(thm)],[c1963, c1932])).
% 45.38/45.64 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)).
% 45.38/45.64 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])).
% 45.38/45.65 fof(c273,plain,(![X278]:(![X279]:(![X280]:(![X281]:((~eqangle(X280,X278,X280,X279,X281,X278,X281,X279)|~coll(X280,X281,X279))|cyclic(X278,X279,X280,X281)))))),inference(variable_rename,[status(thm)],[c272])).
% 45.38/45.65 cnf(c274,plain,~eqangle(X1293,X1292,X1293,X1291,X1294,X1292,X1294,X1291)|~coll(X1293,X1294,X1291)|cyclic(X1292,X1291,X1293,X1294),inference(split_conjunct,[status(thm)],[c273])).
% 45.38/45.65 cnf(c1910,plain,eqangle(X1796,X1799,X1798,X1797,X1796,X1799,X1798,X1797),inference(resolution,[status(thm)],[c1859, c286])).
% 45.38/45.65 cnf(c2184,plain,~coll(X2001,X2001,X2003)|cyclic(X2002,X2003,X2001,X2001),inference(resolution,[status(thm)],[c1910, c274])).
% 45.38/45.65 cnf(c2380,plain,cyclic(X2005,X2006,X2004,X2004),inference(resolution,[status(thm)],[c2184, c2277])).
% 45.38/45.65 cnf(c2388,plain,cyclic(X2015,X2014,X2013,X2014),inference(resolution,[status(thm)],[c2380, c365])).
% 45.38/45.65 cnf(c2392,plain,cyclic(X2017,X2016,X2018,X2017),inference(resolution,[status(thm)],[c2388, c362])).
% 45.38/45.65 cnf(c2402,plain,cyclic(X2028,X2030,X2028,X2029),inference(resolution,[status(thm)],[c2392, c368])).
% 45.38/45.65 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)).
% 45.38/45.65 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])).
% 45.38/45.65 fof(c358,plain,(![X458]:(![X459]:(![X460]:(![X461]:(![X462]:((~cyclic(X458,X459,X460,X461)|~cyclic(X458,X459,X460,X462))|cyclic(X459,X460,X461,X462))))))),inference(variable_rename,[status(thm)],[c357])).
% 45.38/45.65 cnf(c359,plain,~cyclic(X936,X933,X934,X932)|~cyclic(X936,X933,X934,X935)|cyclic(X933,X934,X932,X935),inference(split_conjunct,[status(thm)],[c358])).
% 45.38/45.65 cnf(c2413,plain,~cyclic(X9452,X9450,X9452,X9453)|cyclic(X9450,X9452,X9453,X9451),inference(resolution,[status(thm)],[c2402, c359])).
% 45.38/45.65 cnf(c20536,plain,cyclic(X9456,X9455,X9457,X9454),inference(resolution,[status(thm)],[c2413, c2402])).
% 45.38/45.65 cnf(c20560,plain,$false,inference(resolution,[status(thm)],[c20536, c24])).
% 45.38/45.65 % SZS output end CNFRefutation
% 45.38/45.65
% 45.38/45.65 % Initial clauses : 136
% 45.38/45.65 % Processed clauses : 1822
% 45.38/45.65 % Factors computed : 346
% 45.38/45.65 % Resolvents computed: 19806
% 45.38/45.65 % Tautologies deleted: 37
% 45.38/45.65 % Forward subsumed : 5612
% 45.38/45.65 % Backward subsumed : 801
% 45.38/45.65 % -------- CPU Time ---------
% 45.38/45.65 % User time : 45.219 s
% 45.38/45.65 % System time : 0.048 s
% 45.38/45.65 % Total time : 45.267 s
%------------------------------------------------------------------------------