%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP143+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:21 EDT 2024
% Result : Theorem 0.92s 1.12s
% Output : Refutation 0.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP143+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n005.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 13:29:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.92/1.12 % Version: 1.5
% 0.92/1.12 % SZS status Theorem
% 0.92/1.12 % SZS output start CNFRefutation
% 0.92/1.12 fof(ax18,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.92/1.12 fof(c238,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.92/1.12 fof(c239,plain,(![X110]:(![X111]:(~object(X110,X111)|nonliving(X110,X111)))),inference(variable_rename,[status(thm)],[c238])).
% 0.92/1.12 cnf(c240,plain,~object(X293,X294)|nonliving(X293,X294),inference(split_conjunct,[status(thm)],[c239])).
% 0.92/1.12 fof(ax20,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.92/1.12 fof(c232,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.92/1.12 fof(c233,plain,(![X106]:(![X107]:(~artifact(X106,X107)|object(X106,X107)))),inference(variable_rename,[status(thm)],[c232])).
% 0.92/1.12 cnf(c234,plain,~artifact(X282,X281)|object(X282,X281),inference(split_conjunct,[status(thm)],[c233])).
% 0.92/1.12 fof(ax21,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.92/1.12 fof(c229,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.92/1.12 fof(c230,plain,(![X104]:(![X105]:(~instrumentality(X104,X105)|artifact(X104,X105)))),inference(variable_rename,[status(thm)],[c229])).
% 0.92/1.12 cnf(c231,plain,~instrumentality(X279,X280)|artifact(X279,X280),inference(split_conjunct,[status(thm)],[c230])).
% 0.92/1.12 fof(ax1,axiom,(![U]:(![V]:(furniture(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.92/1.12 fof(c289,plain,(![U]:(![V]:(~furniture(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.92/1.12 fof(c290,plain,(![X144]:(![X145]:(~furniture(X144,X145)|instrumentality(X144,X145)))),inference(variable_rename,[status(thm)],[c289])).
% 0.92/1.12 cnf(c291,plain,~furniture(X363,X364)|instrumentality(X363,X364),inference(split_conjunct,[status(thm)],[c290])).
% 0.92/1.12 fof(ax2,axiom,(![U]:(![V]:(seat(U,V)=>furniture(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.92/1.12 fof(c286,plain,(![U]:(![V]:(~seat(U,V)|furniture(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.92/1.12 fof(c287,plain,(![X142]:(![X143]:(~seat(X142,X143)|furniture(X142,X143)))),inference(variable_rename,[status(thm)],[c286])).
% 0.92/1.12 cnf(c288,plain,~seat(X358,X357)|furniture(X358,X357),inference(split_conjunct,[status(thm)],[c287])).
% 0.92/1.12 fof(ax3,axiom,(![U]:(![V]:(frontseat(U,V)=>seat(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.92/1.12 fof(c283,plain,(![U]:(![V]:(~frontseat(U,V)|seat(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.92/1.12 fof(c284,plain,(![X140]:(![X141]:(~frontseat(X140,X141)|seat(X140,X141)))),inference(variable_rename,[status(thm)],[c283])).
% 0.92/1.12 cnf(c285,plain,~frontseat(X355,X356)|seat(X355,X356),inference(split_conjunct,[status(thm)],[c284])).
% 0.92/1.12 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))&(![X1]:(member(U,X1,Z)=>(?[X2]:(?[X3]:(((frontseat(U,X3)&state(U,X2))&be(U,X2,X1,X3))&in(U,X3,X3)))))))&two(U,Z))&group(U,Z))&(![X4]:(member(U,X4,Z)=>(fellow(U,X4)&young(U,X4))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.92/1.12 fof(c59,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))&(![X1]:(member(U,X1,Z)=>(?[X2]:(?[X3]:(((frontseat(U,X3)&state(U,X2))&be(U,X2,X1,X3))&in(U,X3,X3)))))))&two(U,Z))&group(U,Z))&(![X4]:(member(U,X4,Z)=>(fellow(U,X4)&young(U,X4)))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.92/1.12 fof(c60,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))&(![X1]:(~member(U,X1,Z)|(?[X2]:(?[X3]:(((frontseat(U,X3)&state(U,X2))&be(U,X2,X1,X3))&in(U,X3,X3)))))))&two(U,Z))&group(U,Z))&(![X4]:(~member(U,X4,Z)|(fellow(U,X4)&young(U,X4)))))))))))),inference(fof_nnf,[status(thm)],[c59])).
% 0.92/1.12 fof(c61,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((((((((((((((((of(X2,X3,X4)&city(X2,X4))&hollywood_placename(X2,X3))&placename(X2,X3))&chevy(X2,X4))&white(X2,X4))&dirty(X2,X4))&old(X2,X4))&street(X2,X5))&lonely(X2,X5))&event(X2,X6))&agent(X2,X6,X4))&present(X2,X6))&barrel(X2,X6))&down(X2,X6,X5))&in(X2,X6,X4))&(![X8]:(~member(X2,X8,X7)|(?[X9]:(?[X10]:(((frontseat(X2,X10)&state(X2,X9))&be(X2,X9,X8,X10))&in(X2,X10,X10)))))))&two(X2,X7))&group(X2,X7))&(![X11]:(~member(X2,X11,X7)|(fellow(X2,X11)&young(X2,X11)))))))))))),inference(variable_rename,[status(thm)],[c60])).
% 0.92/1.12 fof(c63,negated_conjecture,(![X8]:(![X11]:(actual_world(skolem0001)&(((((((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003))&(~member(skolem0001,X8,skolem0006)|(((frontseat(skolem0001,skolem0008(X8))&state(skolem0001,skolem0007(X8)))&be(skolem0001,skolem0007(X8),X8,skolem0008(X8)))&in(skolem0001,skolem0008(X8),skolem0008(X8)))))&two(skolem0001,skolem0006))&group(skolem0001,skolem0006))&(~member(skolem0001,X11,skolem0006)|(fellow(skolem0001,X11)&young(skolem0001,X11))))))),inference(shift_quantors,[status(thm)],[fof(c62,negated_conjecture,(actual_world(skolem0001)&(((((((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003))&(![X8]:(~member(skolem0001,X8,skolem0006)|(((frontseat(skolem0001,skolem0008(X8))&state(skolem0001,skolem0007(X8)))&be(skolem0001,skolem0007(X8),X8,skolem0008(X8)))&in(skolem0001,skolem0008(X8),skolem0008(X8))))))&two(skolem0001,skolem0006))&group(skolem0001,skolem0006))&(![X11]:(~member(skolem0001,X11,skolem0006)|(fellow(skolem0001,X11)&young(skolem0001,X11)))))),inference(skolemize,[status(esa)],[c61])).])).
% 0.92/1.12 fof(c64,negated_conjecture,(![X8]:(![X11]:(actual_world(skolem0001)&(((((((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003))&((((~member(skolem0001,X8,skolem0006)|frontseat(skolem0001,skolem0008(X8)))&(~member(skolem0001,X8,skolem0006)|state(skolem0001,skolem0007(X8))))&(~member(skolem0001,X8,skolem0006)|be(skolem0001,skolem0007(X8),X8,skolem0008(X8))))&(~member(skolem0001,X8,skolem0006)|in(skolem0001,skolem0008(X8),skolem0008(X8)))))&two(skolem0001,skolem0006))&group(skolem0001,skolem0006))&((~member(skolem0001,X11,skolem0006)|fellow(skolem0001,X11))&(~member(skolem0001,X11,skolem0006)|young(skolem0001,X11))))))),inference(distribute,[status(thm)],[c63])).
% 0.92/1.12 cnf(c86,negated_conjecture,two(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c64])).
% 0.92/1.12 fof(ax60,axiom,(![U]:(![V]:(two(U,V)<=>(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(member(U,Y,V)=>(Y=X|Y=W)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax60)).
% 0.92/1.12 fof(c93,plain,(![U]:(![V]:((~two(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(~member(U,Y,V)|(Y=X|Y=W))))))))&((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(?[Y]:(member(U,Y,V)&(Y!=X&Y!=W)))))))|two(U,V))))),inference(fof_nnf,[status(thm)],[ax60])).
% 0.92/1.12 fof(c94,plain,((![U]:(![V]:(~two(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(~member(U,Y,V)|(Y=X|Y=W))))))))))&(![U]:(![V]:((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(?[Y]:(member(U,Y,V)&(Y!=X&Y!=W)))))))|two(U,V))))),inference(shift_quantors,[status(thm)],[c93])).
% 0.92/1.12 fof(c95,plain,((![X14]:(![X15]:(~two(X14,X15)|(?[X16]:(member(X14,X16,X15)&(?[X17]:((member(X14,X17,X15)&X17!=X16)&(![X18]:(~member(X14,X18,X15)|(X18=X17|X18=X16))))))))))&(![X19]:(![X20]:((![X21]:(~member(X19,X21,X20)|(![X22]:((~member(X19,X22,X20)|X22=X21)|(?[X23]:(member(X19,X23,X20)&(X23!=X22&X23!=X21)))))))|two(X19,X20))))),inference(variable_rename,[status(thm)],[c94])).
% 0.92/1.12 fof(c97,plain,(![X14]:(![X15]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:((~two(X14,X15)|(member(X14,skolem0009(X14,X15),X15)&((member(X14,skolem0010(X14,X15),X15)&skolem0010(X14,X15)!=skolem0009(X14,X15))&(~member(X14,X18,X15)|(X18=skolem0010(X14,X15)|X18=skolem0009(X14,X15))))))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(member(X19,skolem0011(X19,X20,X21,X22),X20)&(skolem0011(X19,X20,X21,X22)!=X22&skolem0011(X19,X20,X21,X22)!=X21))))|two(X19,X20)))))))))),inference(shift_quantors,[status(thm)],[fof(c96,plain,((![X14]:(![X15]:(~two(X14,X15)|(member(X14,skolem0009(X14,X15),X15)&((member(X14,skolem0010(X14,X15),X15)&skolem0010(X14,X15)!=skolem0009(X14,X15))&(![X18]:(~member(X14,X18,X15)|(X18=skolem0010(X14,X15)|X18=skolem0009(X14,X15)))))))))&(![X19]:(![X20]:((![X21]:(~member(X19,X21,X20)|(![X22]:((~member(X19,X22,X20)|X22=X21)|(member(X19,skolem0011(X19,X20,X21,X22),X20)&(skolem0011(X19,X20,X21,X22)!=X22&skolem0011(X19,X20,X21,X22)!=X21))))))|two(X19,X20))))),inference(skolemize,[status(esa)],[c95])).])).
% 0.92/1.12 fof(c98,plain,(![X14]:(![X15]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(((~two(X14,X15)|member(X14,skolem0009(X14,X15),X15))&(((~two(X14,X15)|member(X14,skolem0010(X14,X15),X15))&(~two(X14,X15)|skolem0010(X14,X15)!=skolem0009(X14,X15)))&(~two(X14,X15)|(~member(X14,X18,X15)|(X18=skolem0010(X14,X15)|X18=skolem0009(X14,X15))))))&(((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|member(X19,skolem0011(X19,X20,X21,X22),X20)))|two(X19,X20))&(((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|skolem0011(X19,X20,X21,X22)!=X22))|two(X19,X20))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|skolem0011(X19,X20,X21,X22)!=X21))|two(X19,X20)))))))))))),inference(distribute,[status(thm)],[c97])).
% 0.92/1.12 cnf(c100,plain,~two(X384,X383)|member(X384,skolem0010(X384,X383),X383),inference(split_conjunct,[status(thm)],[c98])).
% 0.92/1.12 cnf(c382,plain,member(skolem0001,skolem0010(skolem0001,skolem0006),skolem0006),inference(resolution,[status(thm)],[c100, c86])).
% 0.92/1.12 cnf(c82,negated_conjecture,~member(skolem0001,X417,skolem0006)|frontseat(skolem0001,skolem0008(X417)),inference(split_conjunct,[status(thm)],[c64])).
% 0.92/1.12 cnf(c436,plain,frontseat(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c82, c382])).
% 0.92/1.12 cnf(c438,plain,seat(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c436, c285])).
% 0.92/1.12 cnf(c443,plain,furniture(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c438, c288])).
% 0.92/1.12 cnf(c448,plain,instrumentality(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c443, c291])).
% 0.92/1.12 cnf(c452,plain,artifact(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c448, c231])).
% 0.92/1.12 cnf(c456,plain,object(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c452, c234])).
% 0.92/1.12 cnf(c462,plain,nonliving(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c456, c240])).
% 0.92/1.12 fof(ax53,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax53)).
% 0.92/1.12 fof(c129,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax53])).
% 0.92/1.12 fof(c130,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c129])).
% 0.92/1.12 fof(c131,plain,(![X40]:(![X41]:(~nonliving(X40,X41)|~living(X40,X41)))),inference(variable_rename,[status(thm)],[c130])).
% 0.92/1.12 cnf(c132,plain,~nonliving(X175,X176)|~living(X175,X176),inference(split_conjunct,[status(thm)],[c131])).
% 0.92/1.12 fof(ax40,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 0.92/1.12 fof(c172,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax40])).
% 0.92/1.12 fof(c173,plain,(![X66]:(![X67]:(~organism(X66,X67)|living(X66,X67)))),inference(variable_rename,[status(thm)],[c172])).
% 0.92/1.12 cnf(c174,plain,~organism(X214,X213)|living(X214,X213),inference(split_conjunct,[status(thm)],[c173])).
% 0.92/1.12 cnf(reflexivity,axiom,X146=X146,theory(equality)).
% 0.92/1.12 fof(ax47,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax47)).
% 0.92/1.12 fof(c151,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax47])).
% 0.92/1.12 fof(c152,plain,(![X52]:(![X53]:(~human_person(X52,X53)|organism(X52,X53)))),inference(variable_rename,[status(thm)],[c151])).
% 0.92/1.12 cnf(c153,plain,~human_person(X191,X192)|organism(X191,X192),inference(split_conjunct,[status(thm)],[c152])).
% 0.92/1.12 fof(ax48,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax48)).
% 0.92/1.12 fof(c148,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax48])).
% 0.92/1.12 fof(c149,plain,(![X50]:(![X51]:(~man(X50,X51)|human_person(X50,X51)))),inference(variable_rename,[status(thm)],[c148])).
% 0.92/1.12 cnf(c150,plain,~man(X190,X189)|human_person(X190,X189),inference(split_conjunct,[status(thm)],[c149])).
% 0.92/1.12 fof(ax49,axiom,(![U]:(![V]:(fellow(U,V)=>man(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax49)).
% 0.92/1.12 fof(c145,plain,(![U]:(![V]:(~fellow(U,V)|man(U,V)))),inference(fof_nnf,[status(thm)],[ax49])).
% 0.92/1.12 fof(c146,plain,(![X48]:(![X49]:(~fellow(X48,X49)|man(X48,X49)))),inference(variable_rename,[status(thm)],[c145])).
% 0.92/1.12 cnf(c147,plain,~fellow(X187,X188)|man(X187,X188),inference(split_conjunct,[status(thm)],[c146])).
% 0.92/1.12 cnf(c88,negated_conjecture,~member(skolem0001,X379,skolem0006)|fellow(skolem0001,X379),inference(split_conjunct,[status(thm)],[c64])).
% 0.92/1.12 cnf(c409,plain,fellow(skolem0001,skolem0010(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c382, c88])).
% 0.92/1.12 cnf(c410,plain,man(skolem0001,skolem0010(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c409, c147])).
% 0.92/1.12 cnf(c412,plain,human_person(skolem0001,skolem0010(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c410, c150])).
% 0.92/1.12 cnf(c415,plain,organism(skolem0001,skolem0010(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c412, c153])).
% 0.92/1.12 cnf(c41,axiom,X451!=X454|X452!=X453|~organism(X451,X452)|organism(X454,X453),theory(equality)).
% 0.92/1.12 cnf(c531,plain,skolem0001!=X856|skolem0010(skolem0001,skolem0006)!=X857|organism(X856,X857),inference(resolution,[status(thm)],[c41, c415])).
% 0.92/1.12 fof(ax59,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax59)).
% 0.92/1.12 fof(c106,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax59])).
% 0.92/1.12 fof(c107,plain,(![X24]:(![X25]:(![X26]:(![X27]:(~be(X24,X25,X26,X27)|X26=X27))))),inference(variable_rename,[status(thm)],[c106])).
% 0.92/1.12 cnf(c108,plain,~be(X378,X377,X376,X375)|X376=X375,inference(split_conjunct,[status(thm)],[c107])).
% 0.92/1.12 cnf(c84,negated_conjecture,~member(skolem0001,X610,skolem0006)|be(skolem0001,skolem0007(X610),X610,skolem0008(X610)),inference(split_conjunct,[status(thm)],[c64])).
% 0.92/1.12 cnf(c622,plain,be(skolem0001,skolem0007(skolem0010(skolem0001,skolem0006)),skolem0010(skolem0001,skolem0006),skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c84, c382])).
% 0.92/1.12 cnf(c857,plain,skolem0010(skolem0001,skolem0006)=skolem0008(skolem0010(skolem0001,skolem0006)),inference(resolution,[status(thm)],[c622, c108])).
% 0.92/1.12 cnf(c861,plain,skolem0001!=X981|organism(X981,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c857, c531])).
% 0.92/1.12 cnf(c878,plain,organism(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c861, reflexivity])).
% 0.92/1.12 cnf(c882,plain,living(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c878, c174])).
% 0.92/1.12 cnf(c886,plain,~nonliving(skolem0001,skolem0008(skolem0010(skolem0001,skolem0006))),inference(resolution,[status(thm)],[c882, c132])).
% 0.92/1.12 cnf(c887,plain,$false,inference(resolution,[status(thm)],[c886, c462])).
% 0.92/1.12 % SZS output end CNFRefutation
% 0.92/1.12
% 0.92/1.12 % Initial clauses : 154
% 0.92/1.12 % Processed clauses : 569
% 0.92/1.12 % Factors computed : 3
% 0.92/1.12 % Resolvents computed: 593
% 0.92/1.12 % Tautologies deleted: 3
% 0.92/1.12 % Forward subsumed : 146
% 0.92/1.12 % Backward subsumed : 0
% 0.92/1.12 % -------- CPU Time ---------
% 0.92/1.12 % User time : 0.763 s
% 0.92/1.12 % System time : 0.012 s
% 0.92/1.12 % Total time : 0.775 s
%------------------------------------------------------------------------------