%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ128+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:37:49 EDT 2024
% Result : Theorem 4.63s 4.81s
% Output : Refutation 4.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : PUZ128+2 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:38:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 4.63/4.81 % Version: 1.5
% 4.63/4.81 % SZS status Theorem
% 4.63/4.81 % SZS output start CNFRefutation
% 4.63/4.81 fof(background,axiom,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:((((((((((((((parent(A)&relation(A,of,'Oedipus'))&'Iokaste'=A)&parent(B))&relation(B,of,'Polyneikes'))&'Iokaste'=B)&parent(C))&relation(C,of,'Polyneikes'))&'Oedipus'=C)&parent(D))&relation(D,of,'Thersandros'))&'Polyneikes'=D)&patricide(E))&'Oedipus'=E)&(~(?[F]:(patricide(F)&'Thersandros'=F))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', background)).
% 4.63/4.81 fof(c13,plain,(?[A]:(?[B]:(?[C]:(?[D]:(?[E]:((((((((((((((parent(A)&relation(A,of,'Oedipus'))&'Iokaste'=A)&parent(B))&relation(B,of,'Polyneikes'))&'Iokaste'=B)&parent(C))&relation(C,of,'Polyneikes'))&'Oedipus'=C)&parent(D))&relation(D,of,'Thersandros'))&'Polyneikes'=D)&patricide(E))&'Oedipus'=E)&(![F]:(~patricide(F)|'Thersandros'!=F)))))))),inference(fof_nnf,[status(thm)],[background])).
% 4.63/4.81 fof(c14,plain,((?[A]:(?[B]:(?[C]:(?[D]:(?[E]:(((((((((((((parent(A)&relation(A,of,'Oedipus'))&'Iokaste'=A)&parent(B))&relation(B,of,'Polyneikes'))&'Iokaste'=B)&parent(C))&relation(C,of,'Polyneikes'))&'Oedipus'=C)&parent(D))&relation(D,of,'Thersandros'))&'Polyneikes'=D)&patricide(E))&'Oedipus'=E))))))&(![F]:(~patricide(F)|'Thersandros'!=F))),inference(shift_quantors,[status(thm)],[c13])).
% 4.63/4.81 fof(c15,plain,((?[X7]:(?[X8]:(?[X9]:(?[X10]:(?[X11]:(((((((((((((parent(X7)&relation(X7,of,'Oedipus'))&'Iokaste'=X7)&parent(X8))&relation(X8,of,'Polyneikes'))&'Iokaste'=X8)&parent(X9))&relation(X9,of,'Polyneikes'))&'Oedipus'=X9)&parent(X10))&relation(X10,of,'Thersandros'))&'Polyneikes'=X10)&patricide(X11))&'Oedipus'=X11))))))&(![X12]:(~patricide(X12)|'Thersandros'!=X12))),inference(variable_rename,[status(thm)],[c14])).
% 4.63/4.81 fof(c17,plain,(![X12]:((((((((((((((parent(skolem0002)&relation(skolem0002,of,'Oedipus'))&'Iokaste'=skolem0002)&parent(skolem0003))&relation(skolem0003,of,'Polyneikes'))&'Iokaste'=skolem0003)&parent(skolem0004))&relation(skolem0004,of,'Polyneikes'))&'Oedipus'=skolem0004)&parent(skolem0005))&relation(skolem0005,of,'Thersandros'))&'Polyneikes'=skolem0005)&patricide(skolem0006))&'Oedipus'=skolem0006)&(~patricide(X12)|'Thersandros'!=X12))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((((((((((((((parent(skolem0002)&relation(skolem0002,of,'Oedipus'))&'Iokaste'=skolem0002)&parent(skolem0003))&relation(skolem0003,of,'Polyneikes'))&'Iokaste'=skolem0003)&parent(skolem0004))&relation(skolem0004,of,'Polyneikes'))&'Oedipus'=skolem0004)&parent(skolem0005))&relation(skolem0005,of,'Thersandros'))&'Polyneikes'=skolem0005)&patricide(skolem0006))&'Oedipus'=skolem0006)&(![X12]:(~patricide(X12)|'Thersandros'!=X12))),inference(skolemize,[status(esa)],[c15])).])).
% 4.63/4.81 cnf(c21,plain,parent(skolem0003),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c27,plain,parent(skolem0005),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(symmetry,axiom,X15!=X14|X14=X15,theory(equality)).
% 4.63/4.81 cnf(c29,plain,'Polyneikes'=skolem0005,inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c42,plain,skolem0005='Polyneikes',inference(resolution,[status(thm)],[c29, symmetry])).
% 4.63/4.81 cnf(c2,axiom,X30!=X29|~parent(X30)|parent(X29),theory(equality)).
% 4.63/4.81 cnf(c78,plain,~parent(skolem0005)|parent('Polyneikes'),inference(resolution,[status(thm)],[c2, c42])).
% 4.63/4.81 cnf(c139,plain,parent('Polyneikes'),inference(resolution,[status(thm)],[c78, c27])).
% 4.63/4.81 cnf(reflexivity,axiom,X13=X13,theory(equality)).
% 4.63/4.81 cnf(c23,plain,'Iokaste'=skolem0003,inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c22,plain,relation(skolem0003,of,'Polyneikes'),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 fof(prove,conjecture,(?[A]:(?[B]:(?[C]:(?[D]:((((((((parent(A)&patricide(B))&parent(C))&$true)&(~(?[E]:(patricide(E)&D=E))))&relation(C,of,D))&B=C)&relation(A,of,B))&'Iokaste'=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove)).
% 4.63/4.81 fof(c3,negated_conjecture,(~(?[A]:(?[B]:(?[C]:(?[D]:((((((((parent(A)&patricide(B))&parent(C))&$true)&(~(?[E]:(patricide(E)&D=E))))&relation(C,of,D))&B=C)&relation(A,of,B))&'Iokaste'=A)))))),inference(assume_negation,[status(cth)],[prove])).
% 4.63/4.81 fof(c4,negated_conjecture,(~(?[A]:(?[B]:(?[C]:(?[D]:(((((((parent(A)&patricide(B))&parent(C))&(~(?[E]:(patricide(E)&D=E))))&relation(C,of,D))&B=C)&relation(A,of,B))&'Iokaste'=A)))))),inference(fof_simplification,[status(thm)],[c3])).
% 4.63/4.81 fof(c5,negated_conjecture,(![A]:(![B]:(![C]:(![D]:(((((((~parent(A)|~patricide(B))|~parent(C))|(?[E]:(patricide(E)&D=E)))|~relation(C,of,D))|B!=C)|~relation(A,of,B))|'Iokaste'!=A))))),inference(fof_nnf,[status(thm)],[c4])).
% 4.63/4.81 fof(c6,negated_conjecture,(![A]:((![B]:((![C]:((![D]:((((~parent(A)|~patricide(B))|~parent(C))|(?[E]:(patricide(E)&D=E)))|~relation(C,of,D)))|B!=C))|~relation(A,of,B)))|'Iokaste'!=A)),inference(shift_quantors,[status(thm)],[c5])).
% 4.63/4.81 fof(c7,negated_conjecture,(![X2]:((![X3]:((![X4]:((![X5]:((((~parent(X2)|~patricide(X3))|~parent(X4))|(?[X6]:(patricide(X6)&X5=X6)))|~relation(X4,of,X5)))|X3!=X4))|~relation(X2,of,X3)))|'Iokaste'!=X2)),inference(variable_rename,[status(thm)],[c6])).
% 4.63/4.81 fof(c9,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(((((((~parent(X2)|~patricide(X3))|~parent(X4))|(patricide(skolem0001(X2,X3,X4,X5))&X5=skolem0001(X2,X3,X4,X5)))|~relation(X4,of,X5))|X3!=X4)|~relation(X2,of,X3))|'Iokaste'!=X2))))),inference(shift_quantors,[status(thm)],[fof(c8,negated_conjecture,(![X2]:((![X3]:((![X4]:((![X5]:((((~parent(X2)|~patricide(X3))|~parent(X4))|(patricide(skolem0001(X2,X3,X4,X5))&X5=skolem0001(X2,X3,X4,X5)))|~relation(X4,of,X5)))|X3!=X4))|~relation(X2,of,X3)))|'Iokaste'!=X2)),inference(skolemize,[status(esa)],[c7])).])).
% 4.63/4.81 fof(c10,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:((((((((~parent(X2)|~patricide(X3))|~parent(X4))|patricide(skolem0001(X2,X3,X4,X5)))|~relation(X4,of,X5))|X3!=X4)|~relation(X2,of,X3))|'Iokaste'!=X2)&(((((((~parent(X2)|~patricide(X3))|~parent(X4))|X5=skolem0001(X2,X3,X4,X5))|~relation(X4,of,X5))|X3!=X4)|~relation(X2,of,X3))|'Iokaste'!=X2)))))),inference(distribute,[status(thm)],[c9])).
% 4.63/4.81 cnf(c11,negated_conjecture,~parent(X36)|~patricide(X33)|~parent(X35)|patricide(skolem0001(X36,X33,X35,X34))|~relation(X35,of,X34)|X33!=X35|~relation(X36,of,X33)|'Iokaste'!=X36,inference(split_conjunct,[status(thm)],[c10])).
% 4.63/4.81 cnf(c84,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent(X74)|patricide(skolem0001(skolem0003,'Polyneikes',X74,X75))|~relation(X74,of,X75)|'Polyneikes'!=X74|'Iokaste'!=skolem0003,inference(resolution,[status(thm)],[c11, c22])).
% 4.63/4.81 cnf(c1,axiom,X26!=X24|X27!=X22|X23!=X25|~relation(X26,X27,X23)|relation(X24,X22,X25),theory(equality)).
% 4.63/4.81 cnf(c28,plain,relation(skolem0005,of,'Thersandros'),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c81,plain,skolem0005!=X67|of!=X66|'Thersandros'!=X65|relation(X67,X66,X65),inference(resolution,[status(thm)],[c28, c1])).
% 4.63/4.81 cnf(c156,plain,skolem0005!=X108|of!=X107|relation(X108,X107,'Thersandros'),inference(resolution,[status(thm)],[c81, reflexivity])).
% 4.63/4.81 cnf(c377,plain,skolem0005!=X111|relation(X111,of,'Thersandros'),inference(resolution,[status(thm)],[c156, reflexivity])).
% 4.63/4.81 cnf(c401,plain,relation('Polyneikes',of,'Thersandros'),inference(resolution,[status(thm)],[c377, c42])).
% 4.63/4.81 cnf(c402,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent('Polyneikes')|patricide(skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros'))|'Polyneikes'!='Polyneikes'|'Iokaste'!=skolem0003,inference(resolution,[status(thm)],[c401, c84])).
% 4.63/4.81 cnf(c1573,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent('Polyneikes')|patricide(skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros'))|'Polyneikes'!='Polyneikes',inference(resolution,[status(thm)],[c402, c23])).
% 4.63/4.81 cnf(c1574,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent('Polyneikes')|patricide(skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros')),inference(resolution,[status(thm)],[c1573, reflexivity])).
% 4.63/4.81 cnf(c1575,plain,~parent(skolem0003)|~patricide('Polyneikes')|patricide(skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros')),inference(resolution,[status(thm)],[c1574, c139])).
% 4.63/4.81 cnf(c0,axiom,X21!=X20|~patricide(X21)|patricide(X20),theory(equality)).
% 4.63/4.81 cnf(c63,plain,~patricide(skolem0005)|patricide('Polyneikes'),inference(resolution,[status(thm)],[c42, c0])).
% 4.63/4.81 cnf(c18,plain,parent(skolem0002),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c30,plain,patricide(skolem0006),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c31,plain,'Oedipus'=skolem0006,inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c44,plain,skolem0006='Oedipus',inference(resolution,[status(thm)],[c31, symmetry])).
% 4.63/4.81 cnf(c66,plain,~patricide(skolem0006)|patricide('Oedipus'),inference(resolution,[status(thm)],[c44, c0])).
% 4.63/4.81 cnf(c118,plain,patricide('Oedipus'),inference(resolution,[status(thm)],[c66, c30])).
% 4.63/4.81 cnf(c24,plain,parent(skolem0004),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c26,plain,'Oedipus'=skolem0004,inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c20,plain,'Iokaste'=skolem0002,inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c19,plain,relation(skolem0002,of,'Oedipus'),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c87,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(X89)|patricide(skolem0001(skolem0002,'Oedipus',X89,X90))|~relation(X89,of,X90)|'Oedipus'!=X89|'Iokaste'!=skolem0002,inference(resolution,[status(thm)],[c11, c19])).
% 4.63/4.81 cnf(c25,plain,relation(skolem0004,of,'Polyneikes'),inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.81 cnf(c80,plain,skolem0004!=X63|of!=X62|'Polyneikes'!=X61|relation(X63,X62,X61),inference(resolution,[status(thm)],[c25, c1])).
% 4.63/4.81 cnf(c151,plain,skolem0004!=X98|of!=X97|relation(X98,X97,skolem0005),inference(resolution,[status(thm)],[c80, c29])).
% 4.63/4.81 cnf(c307,plain,skolem0004!=X101|relation(X101,of,skolem0005),inference(resolution,[status(thm)],[c151, reflexivity])).
% 4.63/4.81 cnf(c325,plain,relation(skolem0004,of,skolem0005),inference(resolution,[status(thm)],[c307, reflexivity])).
% 4.63/4.81 cnf(c329,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(skolem0004)|patricide(skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005))|'Oedipus'!=skolem0004|'Iokaste'!=skolem0002,inference(resolution,[status(thm)],[c325, c87])).
% 4.63/4.81 cnf(c1313,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(skolem0004)|patricide(skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005))|'Oedipus'!=skolem0004,inference(resolution,[status(thm)],[c329, c20])).
% 4.63/4.81 cnf(c1314,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(skolem0004)|patricide(skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1313, c26])).
% 4.63/4.82 cnf(c1315,plain,~parent(skolem0002)|~patricide('Oedipus')|patricide(skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1314, c24])).
% 4.63/4.82 cnf(c1316,plain,~parent(skolem0002)|patricide(skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1315, c118])).
% 4.63/4.82 cnf(c1317,plain,patricide(skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005)),inference(resolution,[status(thm)],[c1316, c18])).
% 4.63/4.82 cnf(c12,negated_conjecture,~parent(X43)|~patricide(X40)|~parent(X42)|X41=skolem0001(X43,X40,X42,X41)|~relation(X42,of,X41)|X40!=X42|~relation(X43,of,X40)|'Iokaste'!=X43,inference(split_conjunct,[status(thm)],[c10])).
% 4.63/4.82 cnf(c92,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(X118)|X117=skolem0001(skolem0002,'Oedipus',X118,X117)|~relation(X118,of,X117)|'Oedipus'!=X118|'Iokaste'!=skolem0002,inference(resolution,[status(thm)],[c12, c19])).
% 4.63/4.82 cnf(c416,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(skolem0004)|skolem0005=skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005)|'Oedipus'!=skolem0004|'Iokaste'!=skolem0002,inference(resolution,[status(thm)],[c92, c325])).
% 4.63/4.82 cnf(c1684,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(skolem0004)|skolem0005=skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005)|'Oedipus'!=skolem0004,inference(resolution,[status(thm)],[c416, c20])).
% 4.63/4.82 cnf(c1688,plain,~parent(skolem0002)|~patricide('Oedipus')|~parent(skolem0004)|skolem0005=skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005),inference(resolution,[status(thm)],[c1684, c26])).
% 4.63/4.82 cnf(c1690,plain,~parent(skolem0002)|~patricide('Oedipus')|skolem0005=skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005),inference(resolution,[status(thm)],[c1688, c24])).
% 4.63/4.82 cnf(c1691,plain,~parent(skolem0002)|skolem0005=skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005),inference(resolution,[status(thm)],[c1690, c118])).
% 4.63/4.82 cnf(c1692,plain,skolem0005=skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005),inference(resolution,[status(thm)],[c1691, c18])).
% 4.63/4.82 cnf(c1701,plain,skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005)=skolem0005,inference(resolution,[status(thm)],[c1692, symmetry])).
% 4.63/4.82 cnf(c1708,plain,~patricide(skolem0001(skolem0002,'Oedipus',skolem0004,skolem0005))|patricide(skolem0005),inference(resolution,[status(thm)],[c1701, c0])).
% 4.63/4.82 cnf(c1776,plain,patricide(skolem0005),inference(resolution,[status(thm)],[c1708, c1317])).
% 4.63/4.82 cnf(c1777,plain,patricide('Polyneikes'),inference(resolution,[status(thm)],[c1776, c63])).
% 4.63/4.82 cnf(c1781,plain,~parent(skolem0003)|patricide(skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros')),inference(resolution,[status(thm)],[c1777, c1575])).
% 4.63/4.82 cnf(c1785,plain,patricide(skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros')),inference(resolution,[status(thm)],[c1781, c21])).
% 4.63/4.82 cnf(c32,plain,~patricide(X32)|'Thersandros'!=X32,inference(split_conjunct,[status(thm)],[c17])).
% 4.63/4.82 cnf(c89,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent(X100)|X99=skolem0001(skolem0003,'Polyneikes',X100,X99)|~relation(X100,of,X99)|'Polyneikes'!=X100|'Iokaste'!=skolem0003,inference(resolution,[status(thm)],[c12, c22])).
% 4.63/4.82 cnf(c405,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent('Polyneikes')|'Thersandros'=skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros')|'Polyneikes'!='Polyneikes'|'Iokaste'!=skolem0003,inference(resolution,[status(thm)],[c401, c89])).
% 4.63/4.82 cnf(c1670,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent('Polyneikes')|'Thersandros'=skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros')|'Polyneikes'!='Polyneikes',inference(resolution,[status(thm)],[c405, c23])).
% 4.63/4.82 cnf(c1671,plain,~parent(skolem0003)|~patricide('Polyneikes')|~parent('Polyneikes')|'Thersandros'=skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros'),inference(resolution,[status(thm)],[c1670, reflexivity])).
% 4.63/4.82 cnf(c1672,plain,~parent(skolem0003)|~patricide('Polyneikes')|'Thersandros'=skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros'),inference(resolution,[status(thm)],[c1671, c139])).
% 4.63/4.82 cnf(c1778,plain,~parent(skolem0003)|'Thersandros'=skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros'),inference(resolution,[status(thm)],[c1777, c1672])).
% 4.63/4.82 cnf(c1801,plain,'Thersandros'=skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros'),inference(resolution,[status(thm)],[c1778, c21])).
% 4.63/4.82 cnf(c1805,plain,~patricide(skolem0001(skolem0003,'Polyneikes','Polyneikes','Thersandros')),inference(resolution,[status(thm)],[c1801, c32])).
% 4.63/4.82 cnf(c1809,plain,$false,inference(resolution,[status(thm)],[c1805, c1785])).
% 4.63/4.82 % SZS output end CNFRefutation
% 4.63/4.82
% 4.63/4.82 % Initial clauses : 23
% 4.63/4.82 % Processed clauses : 862
% 4.63/4.82 % Factors computed : 3
% 4.63/4.82 % Resolvents computed: 1774
% 4.63/4.82 % Tautologies deleted: 4
% 4.63/4.82 % Forward subsumed : 206
% 4.63/4.82 % Backward subsumed : 343
% 4.63/4.82 % -------- CPU Time ---------
% 4.63/4.82 % User time : 4.448 s
% 4.63/4.82 % System time : 0.024 s
% 4.63/4.82 % Total time : 4.472 s
%------------------------------------------------------------------------------