%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ001+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:32 EDT 2024
% Result : Theorem 3.68s 3.89s
% Output : Refutation 3.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ001+2 : TPTP v8.1.2. Released v4.0.0.
% 0.13/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n006.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:41:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 3.68/3.89 % Version: 1.5
% 3.68/3.89 % SZS status Theorem
% 3.68/3.89 % SZS output start CNFRefutation
% 3.68/3.89 fof(background,axiom,(?[A]:(?[B]:(?[C]:((((((((((((($true&predicate1(B,live,A))&modifier_pp(B,in,'DreadburyMansion'))&predicate2(C,kill,A,'AuntAgatha'))&(![D]:(![E]:((($true&predicate1(E,live,D))&modifier_pp(E,in,'DreadburyMansion'))=>((D='AuntAgatha'|D='Butler')|D='Charles')))))&(![F]:($true=>(![G]:(![H]:(($true&predicate2(H,kill,F,G))=>(?[I]:predicate2(I,hate,F,G))))))))&(![J]:($true=>(~(?[K]:(?[L]:(?[M]:((($true&predicate2(L,kill,J,K))&property2(M,rich,comp_than,K))&J=M))))))))&(![N]:(![O]:(($true&predicate2(O,hate,'AuntAgatha',N))=>(~(?[P]:predicate2(P,hate,'Charles',N)))))))&(~(?[Q]:predicate2(Q,hate,'AuntAgatha','Butler'))))&(![R]:(($true&R!='Butler')=>(?[S]:predicate2(S,hate,'AuntAgatha',R)))))&(![T]:(($true&(~(?[U]:(property2(U,rich,comp_than,'AuntAgatha')&T=U))))=>(?[V]:predicate2(V,hate,'Butler',T)))))&(![W]:(![X]:(($true&predicate2(X,hate,'AuntAgatha',W))=>(?[Y]:predicate2(Y,hate,'Butler',W))))))&(![Z]:($true=>(~(![A1]:($true=>(?[B1]:predicate2(B1,hate,Z,A1))))))))&'AuntAgatha'!='Butler')))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', background)).
% 3.68/3.89 fof(c8,plain,(?[A]:(?[B]:(?[C]:((((((((((((predicate1(B,live,A)&modifier_pp(B,in,'DreadburyMansion'))&predicate2(C,kill,A,'AuntAgatha'))&(![D]:(![E]:((predicate1(E,live,D)&modifier_pp(E,in,'DreadburyMansion'))=>((D='AuntAgatha'|D='Butler')|D='Charles')))))&(![F]:(![G]:(![H]:(predicate2(H,kill,F,G)=>(?[I]:predicate2(I,hate,F,G)))))))&(![J]:(~(?[K]:(?[L]:(?[M]:((predicate2(L,kill,J,K)&property2(M,rich,comp_than,K))&J=M)))))))&(![N]:(![O]:(predicate2(O,hate,'AuntAgatha',N)=>(~(?[P]:predicate2(P,hate,'Charles',N)))))))&(~(?[Q]:predicate2(Q,hate,'AuntAgatha','Butler'))))&(![R]:(R!='Butler'=>(?[S]:predicate2(S,hate,'AuntAgatha',R)))))&(![T]:((~(?[U]:(property2(U,rich,comp_than,'AuntAgatha')&T=U)))=>(?[V]:predicate2(V,hate,'Butler',T)))))&(![W]:(![X]:(predicate2(X,hate,'AuntAgatha',W)=>(?[Y]:predicate2(Y,hate,'Butler',W))))))&(![Z]:(~(![A1]:(?[B1]:predicate2(B1,hate,Z,A1))))))&'AuntAgatha'!='Butler')))),inference(fof_simplification,[status(thm)],[background])).
% 3.68/3.89 fof(c9,plain,(?[A]:(?[B]:(?[C]:((((((((((((predicate1(B,live,A)&modifier_pp(B,in,'DreadburyMansion'))&predicate2(C,kill,A,'AuntAgatha'))&(![D]:(![E]:((~predicate1(E,live,D)|~modifier_pp(E,in,'DreadburyMansion'))|((D='AuntAgatha'|D='Butler')|D='Charles')))))&(![F]:(![G]:(![H]:(~predicate2(H,kill,F,G)|(?[I]:predicate2(I,hate,F,G)))))))&(![J]:(![K]:(![L]:(![M]:((~predicate2(L,kill,J,K)|~property2(M,rich,comp_than,K))|J!=M))))))&(![N]:(![O]:(~predicate2(O,hate,'AuntAgatha',N)|(![P]:~predicate2(P,hate,'Charles',N))))))&(![Q]:~predicate2(Q,hate,'AuntAgatha','Butler')))&(![R]:(R='Butler'|(?[S]:predicate2(S,hate,'AuntAgatha',R)))))&(![T]:((?[U]:(property2(U,rich,comp_than,'AuntAgatha')&T=U))|(?[V]:predicate2(V,hate,'Butler',T)))))&(![W]:(![X]:(~predicate2(X,hate,'AuntAgatha',W)|(?[Y]:predicate2(Y,hate,'Butler',W))))))&(![Z]:(?[A1]:(![B1]:~predicate2(B1,hate,Z,A1)))))&'AuntAgatha'!='Butler')))),inference(fof_nnf,[status(thm)],[c8])).
% 3.68/3.89 fof(c10,plain,(((((((((((?[A]:((?[B]:(predicate1(B,live,A)&modifier_pp(B,in,'DreadburyMansion')))&(?[C]:predicate2(C,kill,A,'AuntAgatha'))))&(![D]:((![E]:(~predicate1(E,live,D)|~modifier_pp(E,in,'DreadburyMansion')))|((D='AuntAgatha'|D='Butler')|D='Charles'))))&(![F]:(![G]:((![H]:~predicate2(H,kill,F,G))|(?[I]:predicate2(I,hate,F,G))))))&(![J]:(![K]:(![L]:(![M]:((~predicate2(L,kill,J,K)|~property2(M,rich,comp_than,K))|J!=M))))))&(![N]:((![O]:~predicate2(O,hate,'AuntAgatha',N))|(![P]:~predicate2(P,hate,'Charles',N)))))&(![Q]:~predicate2(Q,hate,'AuntAgatha','Butler')))&(![R]:(R='Butler'|(?[S]:predicate2(S,hate,'AuntAgatha',R)))))&(![T]:((?[U]:(property2(U,rich,comp_than,'AuntAgatha')&T=U))|(?[V]:predicate2(V,hate,'Butler',T)))))&(![W]:((![X]:~predicate2(X,hate,'AuntAgatha',W))|(?[Y]:predicate2(Y,hate,'Butler',W)))))&(![Z]:(?[A1]:(![B1]:~predicate2(B1,hate,Z,A1)))))&'AuntAgatha'!='Butler'),inference(shift_quantors,[status(thm)],[c9])).
% 3.68/3.89 fof(c11,plain,(((((((((((?[X3]:((?[X4]:(predicate1(X4,live,X3)&modifier_pp(X4,in,'DreadburyMansion')))&(?[X5]:predicate2(X5,kill,X3,'AuntAgatha'))))&(![X6]:((![X7]:(~predicate1(X7,live,X6)|~modifier_pp(X7,in,'DreadburyMansion')))|((X6='AuntAgatha'|X6='Butler')|X6='Charles'))))&(![X8]:(![X9]:((![X10]:~predicate2(X10,kill,X8,X9))|(?[X11]:predicate2(X11,hate,X8,X9))))))&(![X12]:(![X13]:(![X14]:(![X15]:((~predicate2(X14,kill,X12,X13)|~property2(X15,rich,comp_than,X13))|X12!=X15))))))&(![X16]:((![X17]:~predicate2(X17,hate,'AuntAgatha',X16))|(![X18]:~predicate2(X18,hate,'Charles',X16)))))&(![X19]:~predicate2(X19,hate,'AuntAgatha','Butler')))&(![X20]:(X20='Butler'|(?[X21]:predicate2(X21,hate,'AuntAgatha',X20)))))&(![X22]:((?[X23]:(property2(X23,rich,comp_than,'AuntAgatha')&X22=X23))|(?[X24]:predicate2(X24,hate,'Butler',X22)))))&(![X25]:((![X26]:~predicate2(X26,hate,'AuntAgatha',X25))|(?[X27]:predicate2(X27,hate,'Butler',X25)))))&(![X28]:(?[X29]:(![X30]:~predicate2(X30,hate,X28,X29)))))&'AuntAgatha'!='Butler'),inference(variable_rename,[status(thm)],[c10])).
% 3.68/3.89 fof(c13,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X22]:(![X25]:(![X26]:(![X28]:(![X30]:((((((((((((predicate1(skolem0002,live,skolem0001)&modifier_pp(skolem0002,in,'DreadburyMansion'))&predicate2(skolem0003,kill,skolem0001,'AuntAgatha'))&((~predicate1(X7,live,X6)|~modifier_pp(X7,in,'DreadburyMansion'))|((X6='AuntAgatha'|X6='Butler')|X6='Charles')))&(~predicate2(X10,kill,X8,X9)|predicate2(skolem0004(X8,X9),hate,X8,X9)))&((~predicate2(X14,kill,X12,X13)|~property2(X15,rich,comp_than,X13))|X12!=X15))&(~predicate2(X17,hate,'AuntAgatha',X16)|~predicate2(X18,hate,'Charles',X16)))&~predicate2(X19,hate,'AuntAgatha','Butler'))&(X20='Butler'|predicate2(skolem0005(X20),hate,'AuntAgatha',X20)))&((property2(skolem0006(X22),rich,comp_than,'AuntAgatha')&X22=skolem0006(X22))|predicate2(skolem0007(X22),hate,'Butler',X22)))&(~predicate2(X26,hate,'AuntAgatha',X25)|predicate2(skolem0008(X25),hate,'Butler',X25)))&~predicate2(X30,hate,X28,skolem0009(X28)))&'AuntAgatha'!='Butler')))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,((((((((((((predicate1(skolem0002,live,skolem0001)&modifier_pp(skolem0002,in,'DreadburyMansion'))&predicate2(skolem0003,kill,skolem0001,'AuntAgatha'))&(![X6]:((![X7]:(~predicate1(X7,live,X6)|~modifier_pp(X7,in,'DreadburyMansion')))|((X6='AuntAgatha'|X6='Butler')|X6='Charles'))))&(![X8]:(![X9]:((![X10]:~predicate2(X10,kill,X8,X9))|predicate2(skolem0004(X8,X9),hate,X8,X9)))))&(![X12]:(![X13]:(![X14]:(![X15]:((~predicate2(X14,kill,X12,X13)|~property2(X15,rich,comp_than,X13))|X12!=X15))))))&(![X16]:((![X17]:~predicate2(X17,hate,'AuntAgatha',X16))|(![X18]:~predicate2(X18,hate,'Charles',X16)))))&(![X19]:~predicate2(X19,hate,'AuntAgatha','Butler')))&(![X20]:(X20='Butler'|predicate2(skolem0005(X20),hate,'AuntAgatha',X20))))&(![X22]:((property2(skolem0006(X22),rich,comp_than,'AuntAgatha')&X22=skolem0006(X22))|predicate2(skolem0007(X22),hate,'Butler',X22))))&(![X25]:((![X26]:~predicate2(X26,hate,'AuntAgatha',X25))|predicate2(skolem0008(X25),hate,'Butler',X25))))&(![X28]:(![X30]:~predicate2(X30,hate,X28,skolem0009(X28)))))&'AuntAgatha'!='Butler'),inference(skolemize,[status(esa)],[c11])).])).
% 3.68/3.89 fof(c14,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X22]:(![X25]:(![X26]:(![X28]:(![X30]:((((((((((((predicate1(skolem0002,live,skolem0001)&modifier_pp(skolem0002,in,'DreadburyMansion'))&predicate2(skolem0003,kill,skolem0001,'AuntAgatha'))&((~predicate1(X7,live,X6)|~modifier_pp(X7,in,'DreadburyMansion'))|((X6='AuntAgatha'|X6='Butler')|X6='Charles')))&(~predicate2(X10,kill,X8,X9)|predicate2(skolem0004(X8,X9),hate,X8,X9)))&((~predicate2(X14,kill,X12,X13)|~property2(X15,rich,comp_than,X13))|X12!=X15))&(~predicate2(X17,hate,'AuntAgatha',X16)|~predicate2(X18,hate,'Charles',X16)))&~predicate2(X19,hate,'AuntAgatha','Butler'))&(X20='Butler'|predicate2(skolem0005(X20),hate,'AuntAgatha',X20)))&((property2(skolem0006(X22),rich,comp_than,'AuntAgatha')|predicate2(skolem0007(X22),hate,'Butler',X22))&(X22=skolem0006(X22)|predicate2(skolem0007(X22),hate,'Butler',X22))))&(~predicate2(X26,hate,'AuntAgatha',X25)|predicate2(skolem0008(X25),hate,'Butler',X25)))&~predicate2(X30,hate,X28,skolem0009(X28)))&'AuntAgatha'!='Butler')))))))))))))))))))),inference(distribute,[status(thm)],[c13])).
% 3.68/3.89 cnf(c28,plain,'AuntAgatha'!='Butler',inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c23,plain,X53='Butler'|predicate2(skolem0005(X53),hate,'AuntAgatha',X53),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c34,plain,predicate2(skolem0005('AuntAgatha'),hate,'AuntAgatha','AuntAgatha'),inference(resolution,[status(thm)],[c23, c28])).
% 3.68/3.89 cnf(c21,plain,~predicate2(X79,hate,'AuntAgatha',X80)|~predicate2(X78,hate,'Charles',X80),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c19,plain,~predicate2(X86,kill,X85,X87)|predicate2(skolem0004(X85,X87),hate,X85,X87),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(reflexivity,axiom,X31=X31,theory(equality)).
% 3.68/3.89 cnf(c0,axiom,X49!=X43|X45!=X46|X48!=X47|X44!=X50|~predicate2(X49,X45,X48,X44)|predicate2(X43,X46,X47,X50),theory(equality)).
% 3.68/3.89 cnf(c17,plain,predicate2(skolem0003,kill,skolem0001,'AuntAgatha'),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c32,plain,skolem0003!=X103|kill!=X102|skolem0001!=X105|'AuntAgatha'!=X104|predicate2(X103,X102,X105,X104),inference(resolution,[status(thm)],[c17, c0])).
% 3.68/3.89 cnf(c127,plain,skolem0003!=X295|kill!=X294|skolem0001!=X296|predicate2(X295,X294,X296,'AuntAgatha'),inference(resolution,[status(thm)],[c32, reflexivity])).
% 3.68/3.89 fof(prove,conjecture,(?[A]:predicate2(A,kill,'AuntAgatha','AuntAgatha')),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove)).
% 3.68/3.89 fof(c4,negated_conjecture,(~(?[A]:predicate2(A,kill,'AuntAgatha','AuntAgatha'))),inference(assume_negation,[status(cth)],[prove])).
% 3.68/3.89 fof(c5,negated_conjecture,(![A]:~predicate2(A,kill,'AuntAgatha','AuntAgatha')),inference(fof_nnf,[status(thm)],[c4])).
% 3.68/3.89 fof(c6,negated_conjecture,(![X2]:~predicate2(X2,kill,'AuntAgatha','AuntAgatha')),inference(variable_rename,[status(thm)],[c5])).
% 3.68/3.89 cnf(c7,negated_conjecture,~predicate2(X41,kill,'AuntAgatha','AuntAgatha'),inference(split_conjunct,[status(thm)],[c6])).
% 3.68/3.89 cnf(c20,plain,~predicate2(X90,kill,X92,X91)|~property2(X93,rich,comp_than,X91)|X92!=X93,inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c27,plain,~predicate2(X52,hate,X51,skolem0009(X51)),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c24,plain,property2(skolem0006(X96),rich,comp_than,'AuntAgatha')|predicate2(skolem0007(X96),hate,'Butler',X96),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c93,plain,property2(skolem0006(skolem0009('Butler')),rich,comp_than,'AuntAgatha'),inference(resolution,[status(thm)],[c24, c27])).
% 3.68/3.89 cnf(c94,plain,~predicate2(X168,kill,X169,'AuntAgatha')|X169!=skolem0006(skolem0009('Butler')),inference(resolution,[status(thm)],[c93, c20])).
% 3.68/3.89 cnf(transitivity,axiom,X36!=X35|X35!=X37|X36=X37,theory(equality)).
% 3.68/3.89 cnf(c25,plain,X81=skolem0006(X81)|predicate2(skolem0007(X81),hate,'Butler',X81),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c61,plain,skolem0009('Butler')=skolem0006(skolem0009('Butler')),inference(resolution,[status(thm)],[c25, c27])).
% 3.68/3.89 cnf(c63,plain,X88!=skolem0009('Butler')|X88=skolem0006(skolem0009('Butler')),inference(resolution,[status(thm)],[c61, transitivity])).
% 3.68/3.89 cnf(symmetry,axiom,X33!=X32|X32=X33,theory(equality)).
% 3.68/3.89 cnf(c35,plain,predicate2(skolem0005(X70),hate,'AuntAgatha',X70)|'Butler'=X70,inference(resolution,[status(thm)],[c23, symmetry])).
% 3.68/3.89 cnf(c26,plain,~predicate2(X100,hate,'AuntAgatha',X99)|predicate2(skolem0008(X99),hate,'Butler',X99),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c105,plain,predicate2(skolem0008(X101),hate,'Butler',X101)|'Butler'=X101,inference(resolution,[status(thm)],[c26, c35])).
% 3.68/3.89 cnf(c112,plain,'Butler'=skolem0009('Butler'),inference(resolution,[status(thm)],[c105, c27])).
% 3.68/3.89 cnf(c119,plain,'Butler'=skolem0006(skolem0009('Butler')),inference(resolution,[status(thm)],[c112, c63])).
% 3.68/3.89 cnf(c129,plain,X127!='Butler'|X127=skolem0006(skolem0009('Butler')),inference(resolution,[status(thm)],[c119, transitivity])).
% 3.68/3.89 cnf(c15,plain,predicate1(skolem0002,live,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c16,plain,modifier_pp(skolem0002,in,'DreadburyMansion'),inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c18,plain,~predicate1(X83,live,X82)|~modifier_pp(X83,in,'DreadburyMansion')|X82='AuntAgatha'|X82='Butler'|X82='Charles',inference(split_conjunct,[status(thm)],[c14])).
% 3.68/3.89 cnf(c62,plain,~predicate1(skolem0002,live,X153)|X153='AuntAgatha'|X153='Butler'|X153='Charles',inference(resolution,[status(thm)],[c18, c16])).
% 3.68/3.89 cnf(c309,plain,skolem0001='AuntAgatha'|skolem0001='Butler'|skolem0001='Charles',inference(resolution,[status(thm)],[c62, c15])).
% 3.68/3.89 cnf(c525,plain,skolem0001='AuntAgatha'|skolem0001='Charles'|skolem0001=skolem0006(skolem0009('Butler')),inference(resolution,[status(thm)],[c309, c129])).
% 3.68/3.89 cnf(c2705,plain,skolem0001='AuntAgatha'|skolem0001='Charles'|~predicate2(X384,kill,skolem0001,'AuntAgatha'),inference(resolution,[status(thm)],[c525, c94])).
% 3.68/3.89 cnf(c2728,plain,skolem0001='AuntAgatha'|skolem0001='Charles',inference(resolution,[status(thm)],[c2705, c17])).
% 3.68/3.89 cnf(c2729,plain,skolem0001='Charles'|skolem0003!=X728|kill!=X727|predicate2(X728,X727,'AuntAgatha','AuntAgatha'),inference(resolution,[status(thm)],[c2728, c127])).
% 3.68/3.89 cnf(c7523,plain,skolem0001='Charles'|skolem0003!=X729|predicate2(X729,kill,'AuntAgatha','AuntAgatha'),inference(resolution,[status(thm)],[c2729, reflexivity])).
% 3.68/3.89 cnf(c7542,plain,skolem0001='Charles'|predicate2(skolem0003,kill,'AuntAgatha','AuntAgatha'),inference(resolution,[status(thm)],[c7523, reflexivity])).
% 3.68/3.89 cnf(c7590,plain,skolem0001='Charles',inference(resolution,[status(thm)],[c7542, c7])).
% 3.68/3.89 cnf(c7604,plain,skolem0003!=X743|kill!=X742|predicate2(X743,X742,'Charles','AuntAgatha'),inference(resolution,[status(thm)],[c7590, c127])).
% 3.68/3.89 cnf(c8003,plain,skolem0003!=X748|predicate2(X748,kill,'Charles','AuntAgatha'),inference(resolution,[status(thm)],[c7604, reflexivity])).
% 3.68/3.89 cnf(c8097,plain,predicate2(skolem0003,kill,'Charles','AuntAgatha'),inference(resolution,[status(thm)],[c8003, reflexivity])).
% 3.68/3.89 cnf(c8111,plain,predicate2(skolem0004('Charles','AuntAgatha'),hate,'Charles','AuntAgatha'),inference(resolution,[status(thm)],[c8097, c19])).
% 3.68/3.89 cnf(c8264,plain,~predicate2(X753,hate,'AuntAgatha','AuntAgatha'),inference(resolution,[status(thm)],[c8111, c21])).
% 3.68/3.89 cnf(c8294,plain,$false,inference(resolution,[status(thm)],[c8264, c34])).
% 3.68/3.89 % SZS output end CNFRefutation
% 3.68/3.89
% 3.68/3.89 % Initial clauses : 22
% 3.68/3.89 % Processed clauses : 385
% 3.68/3.89 % Factors computed : 50
% 3.68/3.89 % Resolvents computed: 8226
% 3.68/3.89 % Tautologies deleted: 2
% 3.68/3.89 % Forward subsumed : 724
% 3.68/3.89 % Backward subsumed : 85
% 3.68/3.89 % -------- CPU Time ---------
% 3.68/3.89 % User time : 3.516 s
% 3.68/3.89 % System time : 0.034 s
% 3.68/3.89 % Total time : 3.550 s
%------------------------------------------------------------------------------