%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP204+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:34:36 EDT 2024
% Result : Theorem 0.69s 0.86s
% Output : Refutation 0.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : NLP204+1 : TPTP v8.1.2. Released v2.4.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 13:42:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.69/0.86 % Version: 1.5
% 0.69/0.86 % SZS status Theorem
% 0.69/0.86 % SZS output start CNFRefutation
% 0.69/0.86 fof(ax63,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax63)).
% 0.69/0.86 fof(c158,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax63])).
% 0.69/0.86 fof(c159,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c158])).
% 0.69/0.86 fof(c160,plain,(![X54]:(![X55]:(~unisex(X54,X55)|~male(X54,X55)))),inference(variable_rename,[status(thm)],[c159])).
% 0.69/0.86 cnf(c161,plain,~unisex(X210,X209)|~male(X210,X209),inference(split_conjunct,[status(thm)],[c160])).
% 0.69/0.86 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,X))&chevy(U,Y))&white(U,Y))&dirty(U,Y))&old(U,Y))&of(U,Z,X1))&city(U,X1))&hollywood_placename(U,Z))&placename(U,Z))&street(U,X1))&lonely(U,X1))&event(U,X2))&agent(U,X2,Y))&present(U,X2))&barrel(U,X2))&down(U,X2,X1))&in(U,X2,X1))&(![X7]:(member(U,X7,X3)=>(?[X8]:(?[X9]:((state(U,X8)&be(U,X8,X7,X9))&in(U,X9,X)))))))&two(U,X3))&group(U,X3))&(![X10]:(member(U,X10,X3)=>(fellow(U,X10)&young(U,X10)))))&(![X11]:(member(U,X11,X4)=>(![X12]:(member(U,X12,X3)=>(?[X13]:(((((event(U,X13)&agent(U,X13,X12))&patient(U,X13,X11))&present(U,X13))&nonreflexive(U,X13))&wear(U,X13))))))))&group(U,X4))&(![X14]:(member(U,X14,X4)=>((coat(U,X14)&black(U,X14))&cheap(U,X14)))))&wheel(U,X6))&state(U,X5))&be(U,X5,V,X6))&behind(U,X6,X6)))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.69/0.86 fof(c71,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,X))&chevy(U,Y))&white(U,Y))&dirty(U,Y))&old(U,Y))&of(U,Z,X1))&city(U,X1))&hollywood_placename(U,Z))&placename(U,Z))&street(U,X1))&lonely(U,X1))&event(U,X2))&agent(U,X2,Y))&present(U,X2))&barrel(U,X2))&down(U,X2,X1))&in(U,X2,X1))&(![X7]:(member(U,X7,X3)=>(?[X8]:(?[X9]:((state(U,X8)&be(U,X8,X7,X9))&in(U,X9,X)))))))&two(U,X3))&group(U,X3))&(![X10]:(member(U,X10,X3)=>(fellow(U,X10)&young(U,X10)))))&(![X11]:(member(U,X11,X4)=>(![X12]:(member(U,X12,X3)=>(?[X13]:(((((event(U,X13)&agent(U,X13,X12))&patient(U,X13,X11))&present(U,X13))&nonreflexive(U,X13))&wear(U,X13))))))))&group(U,X4))&(![X14]:(member(U,X14,X4)=>((coat(U,X14)&black(U,X14))&cheap(U,X14)))))&wheel(U,X6))&state(U,X5))&be(U,X5,V,X6))&behind(U,X6,X6))))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.69/0.86 fof(c72,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,X))&chevy(U,Y))&white(U,Y))&dirty(U,Y))&old(U,Y))&of(U,Z,X1))&city(U,X1))&hollywood_placename(U,Z))&placename(U,Z))&street(U,X1))&lonely(U,X1))&event(U,X2))&agent(U,X2,Y))&present(U,X2))&barrel(U,X2))&down(U,X2,X1))&in(U,X2,X1))&(![X7]:(~member(U,X7,X3)|(?[X8]:(?[X9]:((state(U,X8)&be(U,X8,X7,X9))&in(U,X9,X)))))))&two(U,X3))&group(U,X3))&(![X10]:(~member(U,X10,X3)|(fellow(U,X10)&young(U,X10)))))&(![X11]:(~member(U,X11,X4)|(![X12]:(~member(U,X12,X3)|(?[X13]:(((((event(U,X13)&agent(U,X13,X12))&patient(U,X13,X11))&present(U,X13))&nonreflexive(U,X13))&wear(U,X13))))))))&group(U,X4))&(![X14]:(~member(U,X14,X4)|((coat(U,X14)&black(U,X14))&cheap(U,X14)))))&wheel(U,X6))&state(U,X5))&be(U,X5,V,X6))&behind(U,X6,X6))))))))))))))),inference(fof_nnf,[status(thm)],[c71])).
% 0.69/0.86 fof(c73,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:(?[X11]:(?[X12]:(?[X13]:(((((((((((((((((((((((((((((((of(X2,X4,X3)&man(X2,X3))&jules_forename(X2,X4))&forename(X2,X4))&frontseat(X2,X5))&chevy(X2,X6))&white(X2,X6))&dirty(X2,X6))&old(X2,X6))&of(X2,X7,X8))&city(X2,X8))&hollywood_placename(X2,X7))&placename(X2,X7))&street(X2,X8))&lonely(X2,X8))&event(X2,X9))&agent(X2,X9,X6))&present(X2,X9))&barrel(X2,X9))&down(X2,X9,X8))&in(X2,X9,X8))&(![X14]:(~member(X2,X14,X10)|(?[X15]:(?[X16]:((state(X2,X15)&be(X2,X15,X14,X16))&in(X2,X16,X5)))))))&two(X2,X10))&group(X2,X10))&(![X17]:(~member(X2,X17,X10)|(fellow(X2,X17)&young(X2,X17)))))&(![X18]:(~member(X2,X18,X11)|(![X19]:(~member(X2,X19,X10)|(?[X20]:(((((event(X2,X20)&agent(X2,X20,X19))&patient(X2,X20,X18))&present(X2,X20))&nonreflexive(X2,X20))&wear(X2,X20))))))))&group(X2,X11))&(![X21]:(~member(X2,X21,X11)|((coat(X2,X21)&black(X2,X21))&cheap(X2,X21)))))&wheel(X2,X13))&state(X2,X12))&be(X2,X12,X3,X13))&behind(X2,X13,X13))))))))))))))),inference(variable_rename,[status(thm)],[c72])).
% 0.69/0.86 fof(c75,negated_conjecture,(![X14]:(![X17]:(![X18]:(![X19]:(![X21]:(actual_world(skolem0001)&(((((((((((((((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&frontseat(skolem0001,skolem0004))&chevy(skolem0001,skolem0005))&white(skolem0001,skolem0005))&dirty(skolem0001,skolem0005))&old(skolem0001,skolem0005))&of(skolem0001,skolem0006,skolem0007))&city(skolem0001,skolem0007))&hollywood_placename(skolem0001,skolem0006))&placename(skolem0001,skolem0006))&street(skolem0001,skolem0007))&lonely(skolem0001,skolem0007))&event(skolem0001,skolem0008))&agent(skolem0001,skolem0008,skolem0005))&present(skolem0001,skolem0008))&barrel(skolem0001,skolem0008))&down(skolem0001,skolem0008,skolem0007))&in(skolem0001,skolem0008,skolem0007))&(~member(skolem0001,X14,skolem0009)|((state(skolem0001,skolem0013(X14))&be(skolem0001,skolem0013(X14),X14,skolem0014(X14)))&in(skolem0001,skolem0014(X14),skolem0004))))&two(skolem0001,skolem0009))&group(skolem0001,skolem0009))&(~member(skolem0001,X17,skolem0009)|(fellow(skolem0001,X17)&young(skolem0001,X17))))&(~member(skolem0001,X18,skolem0010)|(~member(skolem0001,X19,skolem0009)|(((((event(skolem0001,skolem0015(X18,X19))&agent(skolem0001,skolem0015(X18,X19),X19))&patient(skolem0001,skolem0015(X18,X19),X18))&present(skolem0001,skolem0015(X18,X19)))&nonreflexive(skolem0001,skolem0015(X18,X19)))&wear(skolem0001,skolem0015(X18,X19))))))&group(skolem0001,skolem0010))&(~member(skolem0001,X21,skolem0010)|((coat(skolem0001,X21)&black(skolem0001,X21))&cheap(skolem0001,X21))))&wheel(skolem0001,skolem0012))&state(skolem0001,skolem0011))&be(skolem0001,skolem0011,skolem0002,skolem0012))&behind(skolem0001,skolem0012,skolem0012)))))))),inference(shift_quantors,[status(thm)],[fof(c74,negated_conjecture,(actual_world(skolem0001)&(((((((((((((((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&frontseat(skolem0001,skolem0004))&chevy(skolem0001,skolem0005))&white(skolem0001,skolem0005))&dirty(skolem0001,skolem0005))&old(skolem0001,skolem0005))&of(skolem0001,skolem0006,skolem0007))&city(skolem0001,skolem0007))&hollywood_placename(skolem0001,skolem0006))&placename(skolem0001,skolem0006))&street(skolem0001,skolem0007))&lonely(skolem0001,skolem0007))&event(skolem0001,skolem0008))&agent(skolem0001,skolem0008,skolem0005))&present(skolem0001,skolem0008))&barrel(skolem0001,skolem0008))&down(skolem0001,skolem0008,skolem0007))&in(skolem0001,skolem0008,skolem0007))&(![X14]:(~member(skolem0001,X14,skolem0009)|((state(skolem0001,skolem0013(X14))&be(skolem0001,skolem0013(X14),X14,skolem0014(X14)))&in(skolem0001,skolem0014(X14),skolem0004)))))&two(skolem0001,skolem0009))&group(skolem0001,skolem0009))&(![X17]:(~member(skolem0001,X17,skolem0009)|(fellow(skolem0001,X17)&young(skolem0001,X17)))))&(![X18]:(~member(skolem0001,X18,skolem0010)|(![X19]:(~member(skolem0001,X19,skolem0009)|(((((event(skolem0001,skolem0015(X18,X19))&agent(skolem0001,skolem0015(X18,X19),X19))&patient(skolem0001,skolem0015(X18,X19),X18))&present(skolem0001,skolem0015(X18,X19)))&nonreflexive(skolem0001,skolem0015(X18,X19)))&wear(skolem0001,skolem0015(X18,X19))))))))&group(skolem0001,skolem0010))&(![X21]:(~member(skolem0001,X21,skolem0010)|((coat(skolem0001,X21)&black(skolem0001,X21))&cheap(skolem0001,X21)))))&wheel(skolem0001,skolem0012))&state(skolem0001,skolem0011))&be(skolem0001,skolem0011,skolem0002,skolem0012))&behind(skolem0001,skolem0012,skolem0012))),inference(skolemize,[status(esa)],[c73])).])).
% 0.69/0.86 fof(c76,negated_conjecture,(![X14]:(![X17]:(![X18]:(![X19]:(![X21]:(actual_world(skolem0001)&(((((((((((((((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&frontseat(skolem0001,skolem0004))&chevy(skolem0001,skolem0005))&white(skolem0001,skolem0005))&dirty(skolem0001,skolem0005))&old(skolem0001,skolem0005))&of(skolem0001,skolem0006,skolem0007))&city(skolem0001,skolem0007))&hollywood_placename(skolem0001,skolem0006))&placename(skolem0001,skolem0006))&street(skolem0001,skolem0007))&lonely(skolem0001,skolem0007))&event(skolem0001,skolem0008))&agent(skolem0001,skolem0008,skolem0005))&present(skolem0001,skolem0008))&barrel(skolem0001,skolem0008))&down(skolem0001,skolem0008,skolem0007))&in(skolem0001,skolem0008,skolem0007))&(((~member(skolem0001,X14,skolem0009)|state(skolem0001,skolem0013(X14)))&(~member(skolem0001,X14,skolem0009)|be(skolem0001,skolem0013(X14),X14,skolem0014(X14))))&(~member(skolem0001,X14,skolem0009)|in(skolem0001,skolem0014(X14),skolem0004))))&two(skolem0001,skolem0009))&group(skolem0001,skolem0009))&((~member(skolem0001,X17,skolem0009)|fellow(skolem0001,X17))&(~member(skolem0001,X17,skolem0009)|young(skolem0001,X17))))&((((((~member(skolem0001,X18,skolem0010)|(~member(skolem0001,X19,skolem0009)|event(skolem0001,skolem0015(X18,X19))))&(~member(skolem0001,X18,skolem0010)|(~member(skolem0001,X19,skolem0009)|agent(skolem0001,skolem0015(X18,X19),X19))))&(~member(skolem0001,X18,skolem0010)|(~member(skolem0001,X19,skolem0009)|patient(skolem0001,skolem0015(X18,X19),X18))))&(~member(skolem0001,X18,skolem0010)|(~member(skolem0001,X19,skolem0009)|present(skolem0001,skolem0015(X18,X19)))))&(~member(skolem0001,X18,skolem0010)|(~member(skolem0001,X19,skolem0009)|nonreflexive(skolem0001,skolem0015(X18,X19)))))&(~member(skolem0001,X18,skolem0010)|(~member(skolem0001,X19,skolem0009)|wear(skolem0001,skolem0015(X18,X19))))))&group(skolem0001,skolem0010))&(((~member(skolem0001,X21,skolem0010)|coat(skolem0001,X21))&(~member(skolem0001,X21,skolem0010)|black(skolem0001,X21)))&(~member(skolem0001,X21,skolem0010)|cheap(skolem0001,X21))))&wheel(skolem0001,skolem0012))&state(skolem0001,skolem0011))&be(skolem0001,skolem0011,skolem0002,skolem0012))&behind(skolem0001,skolem0012,skolem0012)))))))),inference(distribute,[status(thm)],[c75])).
% 0.69/0.86 cnf(c79,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c76])).
% 0.69/0.86 fof(ax24,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.69/0.86 fof(c282,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.69/0.86 fof(c283,plain,(![X132]:(![X133]:(~man(X132,X133)|male(X132,X133)))),inference(variable_rename,[status(thm)],[c282])).
% 0.69/0.86 cnf(c284,plain,~man(X359,X360)|male(X359,X360),inference(split_conjunct,[status(thm)],[c283])).
% 0.69/0.86 cnf(c422,plain,male(skolem0001,skolem0002),inference(resolution,[status(thm)],[c284, c79])).
% 0.69/0.86 cnf(c423,plain,~unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c422, c161])).
% 0.69/0.86 fof(ax38,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 0.69/0.86 fof(c240,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax38])).
% 0.69/0.86 fof(c241,plain,(![X104]:(![X105]:(~object(X104,X105)|unisex(X104,X105)))),inference(variable_rename,[status(thm)],[c240])).
% 0.69/0.86 cnf(c242,plain,~object(X303,X304)|unisex(X303,X304),inference(split_conjunct,[status(thm)],[c241])).
% 0.69/0.86 fof(ax45,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax45)).
% 0.69/0.86 fof(c219,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax45])).
% 0.69/0.86 fof(c220,plain,(![X90]:(![X91]:(~artifact(X90,X91)|object(X90,X91)))),inference(variable_rename,[status(thm)],[c219])).
% 0.69/0.86 cnf(c221,plain,~artifact(X278,X277)|object(X278,X277),inference(split_conjunct,[status(thm)],[c220])).
% 0.69/0.86 fof(ax46,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax46)).
% 0.69/0.86 fof(c216,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax46])).
% 0.69/0.86 fof(c217,plain,(![X88]:(![X89]:(~instrumentality(X88,X89)|artifact(X88,X89)))),inference(variable_rename,[status(thm)],[c216])).
% 0.69/0.86 cnf(c218,plain,~instrumentality(X271,X272)|artifact(X271,X272),inference(split_conjunct,[status(thm)],[c217])).
% 0.69/0.86 cnf(reflexivity,axiom,X180=X180,theory(equality)).
% 0.69/0.86 cnf(symmetry,axiom,X184!=X183|X183=X184,theory(equality)).
% 0.69/0.86 cnf(c118,negated_conjecture,be(skolem0001,skolem0011,skolem0002,skolem0012),inference(split_conjunct,[status(thm)],[c76])).
% 0.69/0.86 fof(ax71,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax71)).
% 0.69/0.86 fof(c120,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax71])).
% 0.69/0.86 fof(c121,plain,(![X22]:(![X23]:(![X24]:(![X25]:(~be(X22,X23,X24,X25)|X24=X25))))),inference(variable_rename,[status(thm)],[c120])).
% 0.69/0.86 cnf(c122,plain,~be(X492,X489,X491,X490)|X491=X490,inference(split_conjunct,[status(thm)],[c121])).
% 0.69/0.86 cnf(c552,plain,skolem0002=skolem0012,inference(resolution,[status(thm)],[c122, c118])).
% 0.69/0.86 cnf(c553,plain,skolem0012=skolem0002,inference(resolution,[status(thm)],[c552, symmetry])).
% 0.69/0.86 cnf(c4,axiom,X212!=X213|X211!=X214|~instrumentality(X212,X211)|instrumentality(X213,X214),theory(equality)).
% 0.69/0.86 cnf(c116,negated_conjecture,wheel(skolem0001,skolem0012),inference(split_conjunct,[status(thm)],[c76])).
% 0.69/0.86 fof(ax48,axiom,(![U]:(![V]:(wheel(U,V)=>device(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax48)).
% 0.69/0.86 fof(c210,plain,(![U]:(![V]:(~wheel(U,V)|device(U,V)))),inference(fof_nnf,[status(thm)],[ax48])).
% 0.69/0.86 fof(c211,plain,(![X84]:(![X85]:(~wheel(X84,X85)|device(X84,X85)))),inference(variable_rename,[status(thm)],[c210])).
% 0.69/0.86 cnf(c212,plain,~wheel(X267,X268)|device(X267,X268),inference(split_conjunct,[status(thm)],[c211])).
% 0.69/0.86 cnf(c379,plain,device(skolem0001,skolem0012),inference(resolution,[status(thm)],[c212, c116])).
% 0.69/0.86 fof(ax47,axiom,(![U]:(![V]:(device(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax47)).
% 0.69/0.86 fof(c213,plain,(![U]:(![V]:(~device(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax47])).
% 0.69/0.86 fof(c214,plain,(![X86]:(![X87]:(~device(X86,X87)|instrumentality(X86,X87)))),inference(variable_rename,[status(thm)],[c213])).
% 0.69/0.86 cnf(c215,plain,~device(X269,X270)|instrumentality(X269,X270),inference(split_conjunct,[status(thm)],[c214])).
% 0.69/0.86 cnf(c380,plain,instrumentality(skolem0001,skolem0012),inference(resolution,[status(thm)],[c215, c379])).
% 0.69/0.86 cnf(c381,plain,skolem0001!=X604|skolem0012!=X605|instrumentality(X604,X605),inference(resolution,[status(thm)],[c380, c4])).
% 0.69/0.86 cnf(c718,plain,skolem0001!=X607|instrumentality(X607,skolem0002),inference(resolution,[status(thm)],[c381, c553])).
% 0.69/0.86 cnf(c720,plain,instrumentality(skolem0001,skolem0002),inference(resolution,[status(thm)],[c718, reflexivity])).
% 0.69/0.86 cnf(c721,plain,artifact(skolem0001,skolem0002),inference(resolution,[status(thm)],[c720, c218])).
% 0.69/0.86 cnf(c723,plain,object(skolem0001,skolem0002),inference(resolution,[status(thm)],[c721, c221])).
% 0.69/0.86 cnf(c726,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c723, c242])).
% 0.69/0.86 cnf(c731,plain,$false,inference(resolution,[status(thm)],[c726, c423])).
% 0.69/0.86 % SZS output end CNFRefutation
% 0.69/0.86
% 0.69/0.86 % Initial clauses : 194
% 0.69/0.86 % Processed clauses : 360
% 0.69/0.86 % Factors computed : 1
% 0.69/0.86 % Resolvents computed: 378
% 0.69/0.86 % Tautologies deleted: 3
% 0.69/0.86 % Forward subsumed : 21
% 0.69/0.86 % Backward subsumed : 0
% 0.69/0.86 % -------- CPU Time ---------
% 0.69/0.86 % User time : 0.486 s
% 0.69/0.86 % System time : 0.018 s
% 0.69/0.86 % Total time : 0.504 s
%------------------------------------------------------------------------------