%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP145+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:22 EDT 2024
% Result : Theorem 1.00s 1.21s
% Output : Refutation 1.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP145+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n011.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 13:26:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 1.00/1.21 % Version: 1.5
% 1.00/1.21 % SZS status Theorem
% 1.00/1.21 % SZS output start CNFRefutation
% 1.00/1.21 fof(ax50,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax50)).
% 1.00/1.21 fof(c141,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax50])).
% 1.00/1.21 fof(c142,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c141])).
% 1.00/1.21 fof(c143,plain,(![X47]:(![X48]:(~animate(X47,X48)|~nonliving(X47,X48)))),inference(variable_rename,[status(thm)],[c142])).
% 1.00/1.21 cnf(c144,plain,~animate(X186,X187)|~nonliving(X186,X187),inference(split_conjunct,[status(thm)],[c143])).
% 1.00/1.21 fof(ax18,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 1.00/1.21 fof(c238,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 1.00/1.21 fof(c239,plain,(![X111]:(![X112]:(~object(X111,X112)|nonliving(X111,X112)))),inference(variable_rename,[status(thm)],[c238])).
% 1.00/1.21 cnf(c240,plain,~object(X295,X294)|nonliving(X295,X294),inference(split_conjunct,[status(thm)],[c239])).
% 1.00/1.21 fof(ax20,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 1.00/1.21 fof(c232,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 1.00/1.21 fof(c233,plain,(![X107]:(![X108]:(~artifact(X107,X108)|object(X107,X108)))),inference(variable_rename,[status(thm)],[c232])).
% 1.00/1.21 cnf(c234,plain,~artifact(X283,X282)|object(X283,X282),inference(split_conjunct,[status(thm)],[c233])).
% 1.00/1.21 fof(ax21,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 1.00/1.21 fof(c229,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 1.00/1.21 fof(c230,plain,(![X105]:(![X106]:(~instrumentality(X105,X106)|artifact(X105,X106)))),inference(variable_rename,[status(thm)],[c229])).
% 1.00/1.21 cnf(c231,plain,~instrumentality(X281,X280)|artifact(X281,X280),inference(split_conjunct,[status(thm)],[c230])).
% 1.00/1.21 fof(ax1,axiom,(![U]:(![V]:(furniture(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 1.00/1.21 fof(c289,plain,(![U]:(![V]:(~furniture(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 1.00/1.21 fof(c290,plain,(![X145]:(![X146]:(~furniture(X145,X146)|instrumentality(X145,X146)))),inference(variable_rename,[status(thm)],[c289])).
% 1.00/1.21 cnf(c291,plain,~furniture(X368,X369)|instrumentality(X368,X369),inference(split_conjunct,[status(thm)],[c290])).
% 1.00/1.21 fof(ax2,axiom,(![U]:(![V]:(seat(U,V)=>furniture(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 1.00/1.21 fof(c286,plain,(![U]:(![V]:(~seat(U,V)|furniture(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 1.00/1.21 fof(c287,plain,(![X143]:(![X144]:(~seat(X143,X144)|furniture(X143,X144)))),inference(variable_rename,[status(thm)],[c286])).
% 1.00/1.21 cnf(c288,plain,~seat(X366,X367)|furniture(X366,X367),inference(split_conjunct,[status(thm)],[c287])).
% 1.00/1.21 fof(ax3,axiom,(![U]:(![V]:(frontseat(U,V)=>seat(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 1.00/1.21 fof(c283,plain,(![U]:(![V]:(~frontseat(U,V)|seat(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 1.00/1.21 fof(c284,plain,(![X141]:(![X142]:(~frontseat(X141,X142)|seat(X141,X142)))),inference(variable_rename,[status(thm)],[c283])).
% 1.00/1.21 cnf(c285,plain,~frontseat(X365,X364)|seat(X365,X364),inference(split_conjunct,[status(thm)],[c284])).
% 1.00/1.21 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V))&(![X2]:(member(U,X2,X1)=>(?[X3]:(?[X4]:(((frontseat(U,X4)&state(U,X3))&be(U,X3,X2,X4))&in(U,X4,X4)))))))&two(U,X1))&group(U,X1))&(![X5]:(member(U,X5,X1)=>(fellow(U,X5)&young(U,X5)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 1.00/1.21 fof(c59,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V))&(![X2]:(member(U,X2,X1)=>(?[X3]:(?[X4]:(((frontseat(U,X4)&state(U,X3))&be(U,X3,X2,X4))&in(U,X4,X4)))))))&two(U,X1))&group(U,X1))&(![X5]:(member(U,X5,X1)=>(fellow(U,X5)&young(U,X5))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 1.00/1.21 fof(c60,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V))&(![X2]:(~member(U,X2,X1)|(?[X3]:(?[X4]:(((frontseat(U,X4)&state(U,X3))&be(U,X3,X2,X4))&in(U,X4,X4)))))))&two(U,X1))&group(U,X1))&(![X5]:(~member(U,X5,X1)|(fellow(U,X5)&young(U,X5))))))))))))),inference(fof_nnf,[status(thm)],[c59])).
% 1.00/1.21 fof(c61,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((((((((((((((of(X2,X4,X3)&city(X2,X3))&hollywood_placename(X2,X4))&placename(X2,X4))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&street(X2,X6))&lonely(X2,X6))&event(X2,X7))&agent(X2,X7,X5))&present(X2,X7))&barrel(X2,X7))&down(X2,X7,X6))&in(X2,X7,X3))&(![X9]:(~member(X2,X9,X8)|(?[X10]:(?[X11]:(((frontseat(X2,X11)&state(X2,X10))&be(X2,X10,X9,X11))&in(X2,X11,X11)))))))&two(X2,X8))&group(X2,X8))&(![X12]:(~member(X2,X12,X8)|(fellow(X2,X12)&young(X2,X12))))))))))))),inference(variable_rename,[status(thm)],[c60])).
% 1.00/1.21 fof(c63,negated_conjecture,(![X9]:(![X12]:(actual_world(skolem0001)&(((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002))&(~member(skolem0001,X9,skolem0007)|(((frontseat(skolem0001,skolem0009(X9))&state(skolem0001,skolem0008(X9)))&be(skolem0001,skolem0008(X9),X9,skolem0009(X9)))&in(skolem0001,skolem0009(X9),skolem0009(X9)))))&two(skolem0001,skolem0007))&group(skolem0001,skolem0007))&(~member(skolem0001,X12,skolem0007)|(fellow(skolem0001,X12)&young(skolem0001,X12))))))),inference(shift_quantors,[status(thm)],[fof(c62,negated_conjecture,(actual_world(skolem0001)&(((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002))&(![X9]:(~member(skolem0001,X9,skolem0007)|(((frontseat(skolem0001,skolem0009(X9))&state(skolem0001,skolem0008(X9)))&be(skolem0001,skolem0008(X9),X9,skolem0009(X9)))&in(skolem0001,skolem0009(X9),skolem0009(X9))))))&two(skolem0001,skolem0007))&group(skolem0001,skolem0007))&(![X12]:(~member(skolem0001,X12,skolem0007)|(fellow(skolem0001,X12)&young(skolem0001,X12)))))),inference(skolemize,[status(esa)],[c61])).])).
% 1.00/1.21 fof(c64,negated_conjecture,(![X9]:(![X12]:(actual_world(skolem0001)&(((((((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002))&((((~member(skolem0001,X9,skolem0007)|frontseat(skolem0001,skolem0009(X9)))&(~member(skolem0001,X9,skolem0007)|state(skolem0001,skolem0008(X9))))&(~member(skolem0001,X9,skolem0007)|be(skolem0001,skolem0008(X9),X9,skolem0009(X9))))&(~member(skolem0001,X9,skolem0007)|in(skolem0001,skolem0009(X9),skolem0009(X9)))))&two(skolem0001,skolem0007))&group(skolem0001,skolem0007))&((~member(skolem0001,X12,skolem0007)|fellow(skolem0001,X12))&(~member(skolem0001,X12,skolem0007)|young(skolem0001,X12))))))),inference(distribute,[status(thm)],[c63])).
% 1.00/1.21 cnf(c86,negated_conjecture,two(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c64])).
% 1.00/1.21 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/sandbox/benchmark/theBenchmark.p', ax60)).
% 1.00/1.21 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])).
% 1.00/1.21 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])).
% 1.00/1.21 fof(c95,plain,((![X15]:(![X16]:(~two(X15,X16)|(?[X17]:(member(X15,X17,X16)&(?[X18]:((member(X15,X18,X16)&X18!=X17)&(![X19]:(~member(X15,X19,X16)|(X19=X18|X19=X17))))))))))&(![X20]:(![X21]:((![X22]:(~member(X20,X22,X21)|(![X23]:((~member(X20,X23,X21)|X23=X22)|(?[X24]:(member(X20,X24,X21)&(X24!=X23&X24!=X22)))))))|two(X20,X21))))),inference(variable_rename,[status(thm)],[c94])).
% 1.00/1.21 fof(c97,plain,(![X15]:(![X16]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~two(X15,X16)|(member(X15,skolem0010(X15,X16),X16)&((member(X15,skolem0011(X15,X16),X16)&skolem0011(X15,X16)!=skolem0010(X15,X16))&(~member(X15,X19,X16)|(X19=skolem0011(X15,X16)|X19=skolem0010(X15,X16))))))&((~member(X20,X22,X21)|((~member(X20,X23,X21)|X23=X22)|(member(X20,skolem0012(X20,X21,X22,X23),X21)&(skolem0012(X20,X21,X22,X23)!=X23&skolem0012(X20,X21,X22,X23)!=X22))))|two(X20,X21)))))))))),inference(shift_quantors,[status(thm)],[fof(c96,plain,((![X15]:(![X16]:(~two(X15,X16)|(member(X15,skolem0010(X15,X16),X16)&((member(X15,skolem0011(X15,X16),X16)&skolem0011(X15,X16)!=skolem0010(X15,X16))&(![X19]:(~member(X15,X19,X16)|(X19=skolem0011(X15,X16)|X19=skolem0010(X15,X16)))))))))&(![X20]:(![X21]:((![X22]:(~member(X20,X22,X21)|(![X23]:((~member(X20,X23,X21)|X23=X22)|(member(X20,skolem0012(X20,X21,X22,X23),X21)&(skolem0012(X20,X21,X22,X23)!=X23&skolem0012(X20,X21,X22,X23)!=X22))))))|two(X20,X21))))),inference(skolemize,[status(esa)],[c95])).])).
% 1.00/1.21 fof(c98,plain,(![X15]:(![X16]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((~two(X15,X16)|member(X15,skolem0010(X15,X16),X16))&(((~two(X15,X16)|member(X15,skolem0011(X15,X16),X16))&(~two(X15,X16)|skolem0011(X15,X16)!=skolem0010(X15,X16)))&(~two(X15,X16)|(~member(X15,X19,X16)|(X19=skolem0011(X15,X16)|X19=skolem0010(X15,X16))))))&(((~member(X20,X22,X21)|((~member(X20,X23,X21)|X23=X22)|member(X20,skolem0012(X20,X21,X22,X23),X21)))|two(X20,X21))&(((~member(X20,X22,X21)|((~member(X20,X23,X21)|X23=X22)|skolem0012(X20,X21,X22,X23)!=X23))|two(X20,X21))&((~member(X20,X22,X21)|((~member(X20,X23,X21)|X23=X22)|skolem0012(X20,X21,X22,X23)!=X22))|two(X20,X21)))))))))))),inference(distribute,[status(thm)],[c97])).
% 1.00/1.21 cnf(c100,plain,~two(X393,X392)|member(X393,skolem0011(X393,X392),X392),inference(split_conjunct,[status(thm)],[c98])).
% 1.00/1.21 cnf(c399,plain,member(skolem0001,skolem0011(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c100, c86])).
% 1.00/1.21 cnf(c82,negated_conjecture,~member(skolem0001,X426,skolem0007)|frontseat(skolem0001,skolem0009(X426)),inference(split_conjunct,[status(thm)],[c64])).
% 1.00/1.21 cnf(c454,plain,frontseat(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c82, c399])).
% 1.00/1.21 cnf(c456,plain,seat(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c454, c285])).
% 1.00/1.21 cnf(c461,plain,furniture(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c456, c288])).
% 1.00/1.21 cnf(c465,plain,instrumentality(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c461, c291])).
% 1.00/1.21 cnf(c469,plain,artifact(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c465, c231])).
% 1.00/1.21 cnf(c475,plain,object(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c469, c234])).
% 1.00/1.21 cnf(c480,plain,nonliving(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c475, c240])).
% 1.00/1.21 cnf(c495,plain,~animate(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c480, c144])).
% 1.00/1.21 fof(ax38,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax38)).
% 1.00/1.21 fof(c178,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax38])).
% 1.00/1.21 fof(c179,plain,(![X71]:(![X72]:(~human_person(X71,X72)|animate(X71,X72)))),inference(variable_rename,[status(thm)],[c178])).
% 1.00/1.21 cnf(c180,plain,~human_person(X218,X219)|animate(X218,X219),inference(split_conjunct,[status(thm)],[c179])).
% 1.00/1.21 fof(ax48,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 1.00/1.21 fof(c148,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax48])).
% 1.00/1.21 fof(c149,plain,(![X51]:(![X52]:(~man(X51,X52)|human_person(X51,X52)))),inference(variable_rename,[status(thm)],[c148])).
% 1.00/1.21 cnf(c150,plain,~man(X190,X191)|human_person(X190,X191),inference(split_conjunct,[status(thm)],[c149])).
% 1.00/1.21 fof(ax49,axiom,(![U]:(![V]:(fellow(U,V)=>man(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 1.00/1.21 fof(c145,plain,(![U]:(![V]:(~fellow(U,V)|man(U,V)))),inference(fof_nnf,[status(thm)],[ax49])).
% 1.00/1.21 fof(c146,plain,(![X49]:(![X50]:(~fellow(X49,X50)|man(X49,X50)))),inference(variable_rename,[status(thm)],[c145])).
% 1.00/1.21 cnf(c147,plain,~fellow(X189,X188)|man(X189,X188),inference(split_conjunct,[status(thm)],[c146])).
% 1.00/1.21 cnf(reflexivity,axiom,X147=X147,theory(equality)).
% 1.00/1.21 cnf(c88,negated_conjecture,~member(skolem0001,X388,skolem0007)|fellow(skolem0001,X388),inference(split_conjunct,[status(thm)],[c64])).
% 1.00/1.21 cnf(c424,plain,fellow(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c399, c88])).
% 1.00/1.21 cnf(c45,axiom,X472!=X471|X470!=X473|~fellow(X472,X470)|fellow(X471,X473),theory(equality)).
% 1.00/1.21 cnf(c576,plain,skolem0001!=X920|skolem0011(skolem0001,skolem0007)!=X921|fellow(X920,X921),inference(resolution,[status(thm)],[c45, c424])).
% 1.00/1.21 fof(ax59,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax59)).
% 1.00/1.21 fof(c106,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax59])).
% 1.00/1.21 fof(c107,plain,(![X25]:(![X26]:(![X27]:(![X28]:(~be(X25,X26,X27,X28)|X27=X28))))),inference(variable_rename,[status(thm)],[c106])).
% 1.00/1.21 cnf(c108,plain,~be(X381,X380,X382,X383)|X382=X383,inference(split_conjunct,[status(thm)],[c107])).
% 1.00/1.21 cnf(c84,negated_conjecture,~member(skolem0001,X602,skolem0007)|be(skolem0001,skolem0008(X602),X602,skolem0009(X602)),inference(split_conjunct,[status(thm)],[c64])).
% 1.00/1.21 cnf(c634,plain,be(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007)),skolem0011(skolem0001,skolem0007),skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c84, c399])).
% 1.00/1.21 cnf(c894,plain,skolem0011(skolem0001,skolem0007)=skolem0009(skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c634, c108])).
% 1.00/1.21 cnf(c896,plain,skolem0001!=X1008|fellow(X1008,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c894, c576])).
% 1.00/1.21 cnf(c914,plain,fellow(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c896, reflexivity])).
% 1.00/1.21 cnf(c915,plain,man(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c914, c147])).
% 1.00/1.21 cnf(c917,plain,human_person(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c915, c150])).
% 1.00/1.21 cnf(c924,plain,animate(skolem0001,skolem0009(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c917, c180])).
% 1.00/1.21 cnf(c934,plain,$false,inference(resolution,[status(thm)],[c924, c495])).
% 1.00/1.21 % SZS output end CNFRefutation
% 1.00/1.21
% 1.00/1.21 % Initial clauses : 154
% 1.00/1.21 % Processed clauses : 602
% 1.00/1.21 % Factors computed : 3
% 1.00/1.21 % Resolvents computed: 642
% 1.00/1.21 % Tautologies deleted: 3
% 1.00/1.21 % Forward subsumed : 151
% 1.00/1.21 % Backward subsumed : 0
% 1.00/1.21 % -------- CPU Time ---------
% 1.00/1.21 % User time : 0.832 s
% 1.00/1.21 % System time : 0.021 s
% 1.00/1.21 % Total time : 0.853 s
%------------------------------------------------------------------------------