%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP208+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:37 EDT 2024
% Result : Theorem 0.69s 0.92s
% Output : Refutation 0.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP208+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n022.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 13:41:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.69/0.92 % Version: 1.5
% 0.69/0.92 % SZS status Theorem
% 0.69/0.92 % SZS output start CNFRefutation
% 0.69/0.92 fof(ax60,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax60)).
% 0.69/0.92 fof(c170,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax60])).
% 0.69/0.92 fof(c171,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c170])).
% 0.69/0.92 fof(c172,plain,(![X59]:(![X60]:(~nonliving(X59,X60)|~living(X59,X60)))),inference(variable_rename,[status(thm)],[c171])).
% 0.69/0.92 cnf(c173,plain,~nonliving(X219,X218)|~living(X219,X218),inference(split_conjunct,[status(thm)],[c172])).
% 0.69/0.92 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,Z))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&of(U,Y,Z))&city(U,Z))&hollywood_placename(U,Y))&placename(U,Y))&street(U,Z))&lonely(U,Z))&event(U,X1))&agent(U,X1,X))&present(U,X1))&barrel(U,X1))&down(U,X1,Z))&in(U,X1,Z))&(![X6]:(member(U,X6,X2)=>(?[X7]:(?[X8]:((state(U,X7)&be(U,X7,X6,X8))&in(U,X8,Z)))))))&two(U,X2))&group(U,X2))&(![X9]:(member(U,X9,X2)=>(fellow(U,X9)&young(U,X9)))))&(![X10]:(member(U,X10,X3)=>(![X11]:(member(U,X11,X2)=>(?[X12]:(((((event(U,X12)&agent(U,X12,X11))&patient(U,X12,X10))&present(U,X12))&nonreflexive(U,X12))&wear(U,X12))))))))&group(U,X3))&(![X13]:(member(U,X13,X3)=>((coat(U,X13)&black(U,X13))&cheap(U,X13)))))&wheel(U,X5))&state(U,X4))&be(U,X4,V,X5))&behind(U,X5,X5))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.69/0.92 fof(c71,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,Z))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&of(U,Y,Z))&city(U,Z))&hollywood_placename(U,Y))&placename(U,Y))&street(U,Z))&lonely(U,Z))&event(U,X1))&agent(U,X1,X))&present(U,X1))&barrel(U,X1))&down(U,X1,Z))&in(U,X1,Z))&(![X6]:(member(U,X6,X2)=>(?[X7]:(?[X8]:((state(U,X7)&be(U,X7,X6,X8))&in(U,X8,Z)))))))&two(U,X2))&group(U,X2))&(![X9]:(member(U,X9,X2)=>(fellow(U,X9)&young(U,X9)))))&(![X10]:(member(U,X10,X3)=>(![X11]:(member(U,X11,X2)=>(?[X12]:(((((event(U,X12)&agent(U,X12,X11))&patient(U,X12,X10))&present(U,X12))&nonreflexive(U,X12))&wear(U,X12))))))))&group(U,X3))&(![X13]:(member(U,X13,X3)=>((coat(U,X13)&black(U,X13))&cheap(U,X13)))))&wheel(U,X5))&state(U,X4))&be(U,X4,V,X5))&behind(U,X5,X5)))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.69/0.92 fof(c72,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((((((((((((((((((of(U,W,V)&man(U,V))&jules_forename(U,W))&forename(U,W))&frontseat(U,Z))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&of(U,Y,Z))&city(U,Z))&hollywood_placename(U,Y))&placename(U,Y))&street(U,Z))&lonely(U,Z))&event(U,X1))&agent(U,X1,X))&present(U,X1))&barrel(U,X1))&down(U,X1,Z))&in(U,X1,Z))&(![X6]:(~member(U,X6,X2)|(?[X7]:(?[X8]:((state(U,X7)&be(U,X7,X6,X8))&in(U,X8,Z)))))))&two(U,X2))&group(U,X2))&(![X9]:(~member(U,X9,X2)|(fellow(U,X9)&young(U,X9)))))&(![X10]:(~member(U,X10,X3)|(![X11]:(~member(U,X11,X2)|(?[X12]:(((((event(U,X12)&agent(U,X12,X11))&patient(U,X12,X10))&present(U,X12))&nonreflexive(U,X12))&wear(U,X12))))))))&group(U,X3))&(![X13]:(~member(U,X13,X3)|((coat(U,X13)&black(U,X13))&cheap(U,X13)))))&wheel(U,X5))&state(U,X4))&be(U,X4,V,X5))&behind(U,X5,X5)))))))))))))),inference(fof_nnf,[status(thm)],[c71])).
% 0.69/0.92 fof(c73,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(?[X10]:(?[X11]:(?[X12]:(((((((((((((((((((((((((((((((of(X2,X4,X3)&man(X2,X3))&jules_forename(X2,X4))&forename(X2,X4))&frontseat(X2,X7))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&of(X2,X6,X7))&city(X2,X7))&hollywood_placename(X2,X6))&placename(X2,X6))&street(X2,X7))&lonely(X2,X7))&event(X2,X8))&agent(X2,X8,X5))&present(X2,X8))&barrel(X2,X8))&down(X2,X8,X7))&in(X2,X8,X7))&(![X13]:(~member(X2,X13,X9)|(?[X14]:(?[X15]:((state(X2,X14)&be(X2,X14,X13,X15))&in(X2,X15,X7)))))))&two(X2,X9))&group(X2,X9))&(![X16]:(~member(X2,X16,X9)|(fellow(X2,X16)&young(X2,X16)))))&(![X17]:(~member(X2,X17,X10)|(![X18]:(~member(X2,X18,X9)|(?[X19]:(((((event(X2,X19)&agent(X2,X19,X18))&patient(X2,X19,X17))&present(X2,X19))&nonreflexive(X2,X19))&wear(X2,X19))))))))&group(X2,X10))&(![X20]:(~member(X2,X20,X10)|((coat(X2,X20)&black(X2,X20))&cheap(X2,X20)))))&wheel(X2,X12))&state(X2,X11))&be(X2,X11,X3,X12))&behind(X2,X12,X12)))))))))))))),inference(variable_rename,[status(thm)],[c72])).
% 0.69/0.92 fof(c75,negated_conjecture,(![X13]:(![X16]:(![X17]:(![X18]:(![X20]:(actual_world(skolem0001)&(((((((((((((((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&frontseat(skolem0001,skolem0006))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&of(skolem0001,skolem0005,skolem0006))&city(skolem0001,skolem0006))&hollywood_placename(skolem0001,skolem0005))&placename(skolem0001,skolem0005))&street(skolem0001,skolem0006))&lonely(skolem0001,skolem0006))&event(skolem0001,skolem0007))&agent(skolem0001,skolem0007,skolem0004))&present(skolem0001,skolem0007))&barrel(skolem0001,skolem0007))&down(skolem0001,skolem0007,skolem0006))&in(skolem0001,skolem0007,skolem0006))&(~member(skolem0001,X13,skolem0008)|((state(skolem0001,skolem0012(X13))&be(skolem0001,skolem0012(X13),X13,skolem0013(X13)))&in(skolem0001,skolem0013(X13),skolem0006))))&two(skolem0001,skolem0008))&group(skolem0001,skolem0008))&(~member(skolem0001,X16,skolem0008)|(fellow(skolem0001,X16)&young(skolem0001,X16))))&(~member(skolem0001,X17,skolem0009)|(~member(skolem0001,X18,skolem0008)|(((((event(skolem0001,skolem0014(X17,X18))&agent(skolem0001,skolem0014(X17,X18),X18))&patient(skolem0001,skolem0014(X17,X18),X17))&present(skolem0001,skolem0014(X17,X18)))&nonreflexive(skolem0001,skolem0014(X17,X18)))&wear(skolem0001,skolem0014(X17,X18))))))&group(skolem0001,skolem0009))&(~member(skolem0001,X20,skolem0009)|((coat(skolem0001,X20)&black(skolem0001,X20))&cheap(skolem0001,X20))))&wheel(skolem0001,skolem0011))&state(skolem0001,skolem0010))&be(skolem0001,skolem0010,skolem0002,skolem0011))&behind(skolem0001,skolem0011,skolem0011)))))))),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,skolem0006))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&of(skolem0001,skolem0005,skolem0006))&city(skolem0001,skolem0006))&hollywood_placename(skolem0001,skolem0005))&placename(skolem0001,skolem0005))&street(skolem0001,skolem0006))&lonely(skolem0001,skolem0006))&event(skolem0001,skolem0007))&agent(skolem0001,skolem0007,skolem0004))&present(skolem0001,skolem0007))&barrel(skolem0001,skolem0007))&down(skolem0001,skolem0007,skolem0006))&in(skolem0001,skolem0007,skolem0006))&(![X13]:(~member(skolem0001,X13,skolem0008)|((state(skolem0001,skolem0012(X13))&be(skolem0001,skolem0012(X13),X13,skolem0013(X13)))&in(skolem0001,skolem0013(X13),skolem0006)))))&two(skolem0001,skolem0008))&group(skolem0001,skolem0008))&(![X16]:(~member(skolem0001,X16,skolem0008)|(fellow(skolem0001,X16)&young(skolem0001,X16)))))&(![X17]:(~member(skolem0001,X17,skolem0009)|(![X18]:(~member(skolem0001,X18,skolem0008)|(((((event(skolem0001,skolem0014(X17,X18))&agent(skolem0001,skolem0014(X17,X18),X18))&patient(skolem0001,skolem0014(X17,X18),X17))&present(skolem0001,skolem0014(X17,X18)))&nonreflexive(skolem0001,skolem0014(X17,X18)))&wear(skolem0001,skolem0014(X17,X18))))))))&group(skolem0001,skolem0009))&(![X20]:(~member(skolem0001,X20,skolem0009)|((coat(skolem0001,X20)&black(skolem0001,X20))&cheap(skolem0001,X20)))))&wheel(skolem0001,skolem0011))&state(skolem0001,skolem0010))&be(skolem0001,skolem0010,skolem0002,skolem0011))&behind(skolem0001,skolem0011,skolem0011))),inference(skolemize,[status(esa)],[c73])).])).
% 0.69/0.92 fof(c76,negated_conjecture,(![X13]:(![X16]:(![X17]:(![X18]:(![X20]:(actual_world(skolem0001)&(((((((((((((((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&jules_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&frontseat(skolem0001,skolem0006))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&of(skolem0001,skolem0005,skolem0006))&city(skolem0001,skolem0006))&hollywood_placename(skolem0001,skolem0005))&placename(skolem0001,skolem0005))&street(skolem0001,skolem0006))&lonely(skolem0001,skolem0006))&event(skolem0001,skolem0007))&agent(skolem0001,skolem0007,skolem0004))&present(skolem0001,skolem0007))&barrel(skolem0001,skolem0007))&down(skolem0001,skolem0007,skolem0006))&in(skolem0001,skolem0007,skolem0006))&(((~member(skolem0001,X13,skolem0008)|state(skolem0001,skolem0012(X13)))&(~member(skolem0001,X13,skolem0008)|be(skolem0001,skolem0012(X13),X13,skolem0013(X13))))&(~member(skolem0001,X13,skolem0008)|in(skolem0001,skolem0013(X13),skolem0006))))&two(skolem0001,skolem0008))&group(skolem0001,skolem0008))&((~member(skolem0001,X16,skolem0008)|fellow(skolem0001,X16))&(~member(skolem0001,X16,skolem0008)|young(skolem0001,X16))))&((((((~member(skolem0001,X17,skolem0009)|(~member(skolem0001,X18,skolem0008)|event(skolem0001,skolem0014(X17,X18))))&(~member(skolem0001,X17,skolem0009)|(~member(skolem0001,X18,skolem0008)|agent(skolem0001,skolem0014(X17,X18),X18))))&(~member(skolem0001,X17,skolem0009)|(~member(skolem0001,X18,skolem0008)|patient(skolem0001,skolem0014(X17,X18),X17))))&(~member(skolem0001,X17,skolem0009)|(~member(skolem0001,X18,skolem0008)|present(skolem0001,skolem0014(X17,X18)))))&(~member(skolem0001,X17,skolem0009)|(~member(skolem0001,X18,skolem0008)|nonreflexive(skolem0001,skolem0014(X17,X18)))))&(~member(skolem0001,X17,skolem0009)|(~member(skolem0001,X18,skolem0008)|wear(skolem0001,skolem0014(X17,X18))))))&group(skolem0001,skolem0009))&(((~member(skolem0001,X20,skolem0009)|coat(skolem0001,X20))&(~member(skolem0001,X20,skolem0009)|black(skolem0001,X20)))&(~member(skolem0001,X20,skolem0009)|cheap(skolem0001,X20))))&wheel(skolem0001,skolem0011))&state(skolem0001,skolem0010))&be(skolem0001,skolem0010,skolem0002,skolem0011))&behind(skolem0001,skolem0011,skolem0011)))))))),inference(distribute,[status(thm)],[c75])).
% 0.69/0.92 cnf(c79,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c76])).
% 0.69/0.92 fof(ax31,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 0.69/0.92 fof(c261,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.69/0.92 fof(c262,plain,(![X117]:(![X118]:(~man(X117,X118)|human_person(X117,X118)))),inference(variable_rename,[status(thm)],[c261])).
% 0.69/0.92 cnf(c263,plain,~man(X329,X328)|human_person(X329,X328),inference(split_conjunct,[status(thm)],[c262])).
% 0.69/0.92 cnf(c407,plain,human_person(skolem0001,skolem0002),inference(resolution,[status(thm)],[c263, c79])).
% 0.69/0.92 fof(ax30,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax30)).
% 0.69/0.92 fof(c264,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.69/0.92 fof(c265,plain,(![X119]:(![X120]:(~human_person(X119,X120)|organism(X119,X120)))),inference(variable_rename,[status(thm)],[c264])).
% 0.69/0.92 cnf(c266,plain,~human_person(X331,X330)|organism(X331,X330),inference(split_conjunct,[status(thm)],[c265])).
% 0.69/0.92 cnf(c408,plain,organism(skolem0001,skolem0002),inference(resolution,[status(thm)],[c266, c407])).
% 0.69/0.92 fof(ax27,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax27)).
% 0.69/0.92 fof(c273,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.69/0.92 fof(c274,plain,(![X125]:(![X126]:(~organism(X125,X126)|living(X125,X126)))),inference(variable_rename,[status(thm)],[c273])).
% 0.69/0.92 cnf(c275,plain,~organism(X344,X345)|living(X344,X345),inference(split_conjunct,[status(thm)],[c274])).
% 0.69/0.92 cnf(c416,plain,living(skolem0001,skolem0002),inference(resolution,[status(thm)],[c275, c408])).
% 0.69/0.92 cnf(c417,plain,~nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c416, c173])).
% 0.69/0.92 fof(ax40,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax40)).
% 0.69/0.92 fof(c234,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax40])).
% 0.69/0.92 fof(c235,plain,(![X99]:(![X100]:(~object(X99,X100)|nonliving(X99,X100)))),inference(variable_rename,[status(thm)],[c234])).
% 0.69/0.92 cnf(c236,plain,~object(X294,X295)|nonliving(X294,X295),inference(split_conjunct,[status(thm)],[c235])).
% 0.69/0.92 fof(ax45,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax45)).
% 0.69/0.92 fof(c219,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax45])).
% 0.69/0.92 fof(c220,plain,(![X89]:(![X90]:(~artifact(X89,X90)|object(X89,X90)))),inference(variable_rename,[status(thm)],[c219])).
% 0.69/0.92 cnf(c221,plain,~artifact(X276,X277)|object(X276,X277),inference(split_conjunct,[status(thm)],[c220])).
% 0.69/0.92 fof(ax46,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax46)).
% 0.69/0.92 fof(c216,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax46])).
% 0.69/0.92 fof(c217,plain,(![X87]:(![X88]:(~instrumentality(X87,X88)|artifact(X87,X88)))),inference(variable_rename,[status(thm)],[c216])).
% 0.69/0.92 cnf(c218,plain,~instrumentality(X270,X271)|artifact(X270,X271),inference(split_conjunct,[status(thm)],[c217])).
% 0.69/0.92 cnf(reflexivity,axiom,X179=X179,theory(equality)).
% 0.69/0.92 cnf(symmetry,axiom,X182!=X183|X183=X182,theory(equality)).
% 0.69/0.92 cnf(c118,negated_conjecture,be(skolem0001,skolem0010,skolem0002,skolem0011),inference(split_conjunct,[status(thm)],[c76])).
% 0.69/0.92 fof(ax71,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax71)).
% 0.69/0.92 fof(c120,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax71])).
% 0.69/0.92 fof(c121,plain,(![X21]:(![X22]:(![X23]:(![X24]:(~be(X21,X22,X23,X24)|X23=X24))))),inference(variable_rename,[status(thm)],[c120])).
% 0.69/0.92 cnf(c122,plain,~be(X481,X483,X480,X482)|X480=X482,inference(split_conjunct,[status(thm)],[c121])).
% 0.69/0.92 cnf(c534,plain,skolem0002=skolem0011,inference(resolution,[status(thm)],[c122, c118])).
% 0.69/0.92 cnf(c536,plain,skolem0011=skolem0002,inference(resolution,[status(thm)],[c534, symmetry])).
% 0.69/0.92 cnf(c4,axiom,X213!=X212|X211!=X210|~instrumentality(X213,X211)|instrumentality(X212,X210),theory(equality)).
% 0.69/0.92 cnf(c116,negated_conjecture,wheel(skolem0001,skolem0011),inference(split_conjunct,[status(thm)],[c76])).
% 0.69/0.92 fof(ax48,axiom,(![U]:(![V]:(wheel(U,V)=>device(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 0.69/0.92 fof(c210,plain,(![U]:(![V]:(~wheel(U,V)|device(U,V)))),inference(fof_nnf,[status(thm)],[ax48])).
% 0.69/0.92 fof(c211,plain,(![X83]:(![X84]:(~wheel(X83,X84)|device(X83,X84)))),inference(variable_rename,[status(thm)],[c210])).
% 0.69/0.92 cnf(c212,plain,~wheel(X266,X267)|device(X266,X267),inference(split_conjunct,[status(thm)],[c211])).
% 0.69/0.92 cnf(c379,plain,device(skolem0001,skolem0011),inference(resolution,[status(thm)],[c212, c116])).
% 0.69/0.92 fof(ax47,axiom,(![U]:(![V]:(device(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax47)).
% 0.69/0.92 fof(c213,plain,(![U]:(![V]:(~device(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax47])).
% 0.69/0.92 fof(c214,plain,(![X85]:(![X86]:(~device(X85,X86)|instrumentality(X85,X86)))),inference(variable_rename,[status(thm)],[c213])).
% 0.69/0.92 cnf(c215,plain,~device(X268,X269)|instrumentality(X268,X269),inference(split_conjunct,[status(thm)],[c214])).
% 0.69/0.92 cnf(c380,plain,instrumentality(skolem0001,skolem0011),inference(resolution,[status(thm)],[c215, c379])).
% 0.69/0.92 cnf(c381,plain,skolem0001!=X592|skolem0011!=X591|instrumentality(X592,X591),inference(resolution,[status(thm)],[c380, c4])).
% 0.69/0.92 cnf(c695,plain,skolem0001!=X593|instrumentality(X593,skolem0002),inference(resolution,[status(thm)],[c381, c536])).
% 0.69/0.92 cnf(c697,plain,instrumentality(skolem0001,skolem0002),inference(resolution,[status(thm)],[c695, reflexivity])).
% 0.69/0.92 cnf(c698,plain,artifact(skolem0001,skolem0002),inference(resolution,[status(thm)],[c697, c218])).
% 0.69/0.92 cnf(c701,plain,object(skolem0001,skolem0002),inference(resolution,[status(thm)],[c698, c221])).
% 0.69/0.92 cnf(c706,plain,nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c701, c236])).
% 0.69/0.92 cnf(c709,plain,$false,inference(resolution,[status(thm)],[c706, c417])).
% 0.69/0.92 % SZS output end CNFRefutation
% 0.69/0.92
% 0.69/0.92 % Initial clauses : 194
% 0.69/0.92 % Processed clauses : 345
% 0.69/0.92 % Factors computed : 1
% 0.69/0.92 % Resolvents computed: 357
% 0.69/0.92 % Tautologies deleted: 3
% 0.69/0.92 % Forward subsumed : 21
% 0.69/0.92 % Backward subsumed : 0
% 0.69/0.92 % -------- CPU Time ---------
% 0.69/0.92 % User time : 0.559 s
% 0.69/0.92 % System time : 0.011 s
% 0.69/0.92 % Total time : 0.570 s
%------------------------------------------------------------------------------