%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP083+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:33:58 EDT 2024
% Result : CounterSatisfiable 2.44s 2.61s
% Output : Saturation 2.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP083+1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n003.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % 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:47:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 2.44/2.61 % Version: 1.5
% 2.44/2.61 % SZS status CounterSatisfiable
% 2.44/2.61 % SZS output start Saturation
% 2.44/2.61 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((((((male(U,V)&male(U,W))&man(U,W))&of(U,X,W))&cannon(U,X))&(![X3]:(member(U,X3,Y)=>(?[X4]:((((((event(U,X4)&agent(U,X4,W))&patient(U,X4,X3))&present(U,X4))&nonreflexive(U,X4))&fire(U,X4))&from_loc(U,X4,X))))))&six(U,Y))&group(U,Y))&(![X5]:(member(U,X5,Y)=>shot(U,X5))))&revenge(U,Z))&cry(U,X1))&event(U,X2))&agent(U,X2,V))&patient(U,X2,X1))&present(U,X2))&nonreflexive(U,X2))&scream(U,X2))&of(U,X2,Z)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 2.44/2.61 fof(c44,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((((((male(U,V)&male(U,W))&man(U,W))&of(U,X,W))&cannon(U,X))&(![X3]:(member(U,X3,Y)=>(?[X4]:((((((event(U,X4)&agent(U,X4,W))&patient(U,X4,X3))&present(U,X4))&nonreflexive(U,X4))&fire(U,X4))&from_loc(U,X4,X))))))&six(U,Y))&group(U,Y))&(![X5]:(member(U,X5,Y)=>shot(U,X5))))&revenge(U,Z))&cry(U,X1))&event(U,X2))&agent(U,X2,V))&patient(U,X2,X1))&present(U,X2))&nonreflexive(U,X2))&scream(U,X2))&of(U,X2,Z))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 2.44/2.61 fof(c45,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((((((male(U,V)&male(U,W))&man(U,W))&of(U,X,W))&cannon(U,X))&(![X3]:(~member(U,X3,Y)|(?[X4]:((((((event(U,X4)&agent(U,X4,W))&patient(U,X4,X3))&present(U,X4))&nonreflexive(U,X4))&fire(U,X4))&from_loc(U,X4,X))))))&six(U,Y))&group(U,Y))&(![X5]:(~member(U,X5,Y)|shot(U,X5))))&revenge(U,Z))&cry(U,X1))&event(U,X2))&agent(U,X2,V))&patient(U,X2,X1))&present(U,X2))&nonreflexive(U,X2))&scream(U,X2))&of(U,X2,Z))))))))))),inference(fof_nnf,[status(thm)],[c44])).
% 2.44/2.61 fof(c46,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((((((((((male(X2,X3)&male(X2,X4))&man(X2,X4))&of(X2,X5,X4))&cannon(X2,X5))&(![X10]:(~member(X2,X10,X6)|(?[X11]:((((((event(X2,X11)&agent(X2,X11,X4))&patient(X2,X11,X10))&present(X2,X11))&nonreflexive(X2,X11))&fire(X2,X11))&from_loc(X2,X11,X5))))))&six(X2,X6))&group(X2,X6))&(![X12]:(~member(X2,X12,X6)|shot(X2,X12))))&revenge(X2,X7))&cry(X2,X8))&event(X2,X9))&agent(X2,X9,X3))&patient(X2,X9,X8))&present(X2,X9))&nonreflexive(X2,X9))&scream(X2,X9))&of(X2,X9,X7))))))))))),inference(variable_rename,[status(thm)],[c45])).
% 2.44/2.61 fof(c48,negated_conjecture,(![X10]:(![X12]:(actual_world(skolem0001)&(((((((((((((((((male(skolem0001,skolem0002)&male(skolem0001,skolem0003))&man(skolem0001,skolem0003))&of(skolem0001,skolem0004,skolem0003))&cannon(skolem0001,skolem0004))&(~member(skolem0001,X10,skolem0005)|((((((event(skolem0001,skolem0009(X10))&agent(skolem0001,skolem0009(X10),skolem0003))&patient(skolem0001,skolem0009(X10),X10))&present(skolem0001,skolem0009(X10)))&nonreflexive(skolem0001,skolem0009(X10)))&fire(skolem0001,skolem0009(X10)))&from_loc(skolem0001,skolem0009(X10),skolem0004))))&six(skolem0001,skolem0005))&group(skolem0001,skolem0005))&(~member(skolem0001,X12,skolem0005)|shot(skolem0001,X12)))&revenge(skolem0001,skolem0006))&cry(skolem0001,skolem0007))&event(skolem0001,skolem0008))&agent(skolem0001,skolem0008,skolem0002))&patient(skolem0001,skolem0008,skolem0007))&present(skolem0001,skolem0008))&nonreflexive(skolem0001,skolem0008))&scream(skolem0001,skolem0008))&of(skolem0001,skolem0008,skolem0006))))),inference(shift_quantors,[status(thm)],[fof(c47,negated_conjecture,(actual_world(skolem0001)&(((((((((((((((((male(skolem0001,skolem0002)&male(skolem0001,skolem0003))&man(skolem0001,skolem0003))&of(skolem0001,skolem0004,skolem0003))&cannon(skolem0001,skolem0004))&(![X10]:(~member(skolem0001,X10,skolem0005)|((((((event(skolem0001,skolem0009(X10))&agent(skolem0001,skolem0009(X10),skolem0003))&patient(skolem0001,skolem0009(X10),X10))&present(skolem0001,skolem0009(X10)))&nonreflexive(skolem0001,skolem0009(X10)))&fire(skolem0001,skolem0009(X10)))&from_loc(skolem0001,skolem0009(X10),skolem0004)))))&six(skolem0001,skolem0005))&group(skolem0001,skolem0005))&(![X12]:(~member(skolem0001,X12,skolem0005)|shot(skolem0001,X12))))&revenge(skolem0001,skolem0006))&cry(skolem0001,skolem0007))&event(skolem0001,skolem0008))&agent(skolem0001,skolem0008,skolem0002))&patient(skolem0001,skolem0008,skolem0007))&present(skolem0001,skolem0008))&nonreflexive(skolem0001,skolem0008))&scream(skolem0001,skolem0008))&of(skolem0001,skolem0008,skolem0006))),inference(skolemize,[status(esa)],[c46])).])).
% 2.44/2.61 fof(c49,negated_conjecture,(![X10]:(![X12]:(actual_world(skolem0001)&(((((((((((((((((male(skolem0001,skolem0002)&male(skolem0001,skolem0003))&man(skolem0001,skolem0003))&of(skolem0001,skolem0004,skolem0003))&cannon(skolem0001,skolem0004))&(((((((~member(skolem0001,X10,skolem0005)|event(skolem0001,skolem0009(X10)))&(~member(skolem0001,X10,skolem0005)|agent(skolem0001,skolem0009(X10),skolem0003)))&(~member(skolem0001,X10,skolem0005)|patient(skolem0001,skolem0009(X10),X10)))&(~member(skolem0001,X10,skolem0005)|present(skolem0001,skolem0009(X10))))&(~member(skolem0001,X10,skolem0005)|nonreflexive(skolem0001,skolem0009(X10))))&(~member(skolem0001,X10,skolem0005)|fire(skolem0001,skolem0009(X10))))&(~member(skolem0001,X10,skolem0005)|from_loc(skolem0001,skolem0009(X10),skolem0004))))&six(skolem0001,skolem0005))&group(skolem0001,skolem0005))&(~member(skolem0001,X12,skolem0005)|shot(skolem0001,X12)))&revenge(skolem0001,skolem0006))&cry(skolem0001,skolem0007))&event(skolem0001,skolem0008))&agent(skolem0001,skolem0008,skolem0002))&patient(skolem0001,skolem0008,skolem0007))&present(skolem0001,skolem0008))&nonreflexive(skolem0001,skolem0008))&scream(skolem0001,skolem0008))&of(skolem0001,skolem0008,skolem0006))))),inference(distribute,[status(thm)],[c48])).
% 2.44/2.61 cnf(c63,negated_conjecture,six(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 fof(ax44,axiom,(![U]:(![V]:(six(U,V)<=>(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(?[Z]:((((member(U,Z,V)&Z!=Y)&Z!=X)&Z!=W)&(?[X1]:(((((member(U,X1,V)&X1!=Z)&X1!=Y)&X1!=X)&X1!=W)&(?[X2]:((((((member(U,X2,V)&X2!=X1)&X2!=Z)&X2!=Y)&X2!=X)&X2!=W)&(![X3]:(member(U,X3,V)=>(((((X3=X2|X3=X1)|X3=Z)|X3=Y)|X3=X)|X3=W)))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax44)).
% 2.44/2.61 fof(c81,plain,(![U]:(![V]:((~six(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(?[Z]:((((member(U,Z,V)&Z!=Y)&Z!=X)&Z!=W)&(?[X1]:(((((member(U,X1,V)&X1!=Z)&X1!=Y)&X1!=X)&X1!=W)&(?[X2]:((((((member(U,X2,V)&X2!=X1)&X2!=Z)&X2!=Y)&X2!=X)&X2!=W)&(![X3]:(~member(U,X3,V)|(((((X3=X2|X3=X1)|X3=Z)|X3=Y)|X3=X)|X3=W))))))))))))))))&((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(![Y]:(((~member(U,Y,V)|Y=X)|Y=W)|(![Z]:((((~member(U,Z,V)|Z=Y)|Z=X)|Z=W)|(![X1]:(((((~member(U,X1,V)|X1=Z)|X1=Y)|X1=X)|X1=W)|(![X2]:((((((~member(U,X2,V)|X2=X1)|X2=Z)|X2=Y)|X2=X)|X2=W)|(?[X3]:(member(U,X3,V)&(((((X3!=X2&X3!=X1)&X3!=Z)&X3!=Y)&X3!=X)&X3!=W)))))))))))))))|six(U,V))))),inference(fof_nnf,[status(thm)],[ax44])).
% 2.44/2.61 fof(c82,plain,((![U]:(![V]:(~six(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(?[Z]:((((member(U,Z,V)&Z!=Y)&Z!=X)&Z!=W)&(?[X1]:(((((member(U,X1,V)&X1!=Z)&X1!=Y)&X1!=X)&X1!=W)&(?[X2]:((((((member(U,X2,V)&X2!=X1)&X2!=Z)&X2!=Y)&X2!=X)&X2!=W)&(![X3]:(~member(U,X3,V)|(((((X3=X2|X3=X1)|X3=Z)|X3=Y)|X3=X)|X3=W))))))))))))))))))&(![U]:(![V]:((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(![Y]:(((~member(U,Y,V)|Y=X)|Y=W)|(![Z]:((((~member(U,Z,V)|Z=Y)|Z=X)|Z=W)|(![X1]:(((((~member(U,X1,V)|X1=Z)|X1=Y)|X1=X)|X1=W)|(![X2]:((((((~member(U,X2,V)|X2=X1)|X2=Z)|X2=Y)|X2=X)|X2=W)|(?[X3]:(member(U,X3,V)&(((((X3!=X2&X3!=X1)&X3!=Z)&X3!=Y)&X3!=X)&X3!=W)))))))))))))))|six(U,V))))),inference(shift_quantors,[status(thm)],[c81])).
% 2.44/2.61 fof(c83,plain,((![X19]:(![X20]:(~six(X19,X20)|(?[X21]:(member(X19,X21,X20)&(?[X22]:((member(X19,X22,X20)&X22!=X21)&(?[X23]:(((member(X19,X23,X20)&X23!=X22)&X23!=X21)&(?[X24]:((((member(X19,X24,X20)&X24!=X23)&X24!=X22)&X24!=X21)&(?[X25]:(((((member(X19,X25,X20)&X25!=X24)&X25!=X23)&X25!=X22)&X25!=X21)&(?[X26]:((((((member(X19,X26,X20)&X26!=X25)&X26!=X24)&X26!=X23)&X26!=X22)&X26!=X21)&(![X27]:(~member(X19,X27,X20)|(((((X27=X26|X27=X25)|X27=X24)|X27=X23)|X27=X22)|X27=X21))))))))))))))))))&(![X28]:(![X29]:((![X30]:(~member(X28,X30,X29)|(![X31]:((~member(X28,X31,X29)|X31=X30)|(![X32]:(((~member(X28,X32,X29)|X32=X31)|X32=X30)|(![X33]:((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(![X34]:(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|(![X35]:((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|(?[X36]:(member(X28,X36,X29)&(((((X36!=X35&X36!=X34)&X36!=X33)&X36!=X32)&X36!=X31)&X36!=X30)))))))))))))))|six(X28,X29))))),inference(variable_rename,[status(thm)],[c82])).
% 2.44/2.61 fof(c85,plain,(![X19]:(![X20]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:((~six(X19,X20)|(member(X19,skolem0010(X19,X20),X20)&((member(X19,skolem0011(X19,X20),X20)&skolem0011(X19,X20)!=skolem0010(X19,X20))&(((member(X19,skolem0012(X19,X20),X20)&skolem0012(X19,X20)!=skolem0011(X19,X20))&skolem0012(X19,X20)!=skolem0010(X19,X20))&((((member(X19,skolem0013(X19,X20),X20)&skolem0013(X19,X20)!=skolem0012(X19,X20))&skolem0013(X19,X20)!=skolem0011(X19,X20))&skolem0013(X19,X20)!=skolem0010(X19,X20))&(((((member(X19,skolem0014(X19,X20),X20)&skolem0014(X19,X20)!=skolem0013(X19,X20))&skolem0014(X19,X20)!=skolem0012(X19,X20))&skolem0014(X19,X20)!=skolem0011(X19,X20))&skolem0014(X19,X20)!=skolem0010(X19,X20))&((((((member(X19,skolem0015(X19,X20),X20)&skolem0015(X19,X20)!=skolem0014(X19,X20))&skolem0015(X19,X20)!=skolem0013(X19,X20))&skolem0015(X19,X20)!=skolem0012(X19,X20))&skolem0015(X19,X20)!=skolem0011(X19,X20))&skolem0015(X19,X20)!=skolem0010(X19,X20))&(~member(X19,X27,X20)|(((((X27=skolem0015(X19,X20)|X27=skolem0014(X19,X20))|X27=skolem0013(X19,X20))|X27=skolem0012(X19,X20))|X27=skolem0011(X19,X20))|X27=skolem0010(X19,X20))))))))))&((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|(member(X28,skolem0016(X28,X29,X30,X31,X32,X33,X34,X35),X29)&(((((skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X35&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X34)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X33)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X32)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X31)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X30))))))))|six(X28,X29)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c84,plain,((![X19]:(![X20]:(~six(X19,X20)|(member(X19,skolem0010(X19,X20),X20)&((member(X19,skolem0011(X19,X20),X20)&skolem0011(X19,X20)!=skolem0010(X19,X20))&(((member(X19,skolem0012(X19,X20),X20)&skolem0012(X19,X20)!=skolem0011(X19,X20))&skolem0012(X19,X20)!=skolem0010(X19,X20))&((((member(X19,skolem0013(X19,X20),X20)&skolem0013(X19,X20)!=skolem0012(X19,X20))&skolem0013(X19,X20)!=skolem0011(X19,X20))&skolem0013(X19,X20)!=skolem0010(X19,X20))&(((((member(X19,skolem0014(X19,X20),X20)&skolem0014(X19,X20)!=skolem0013(X19,X20))&skolem0014(X19,X20)!=skolem0012(X19,X20))&skolem0014(X19,X20)!=skolem0011(X19,X20))&skolem0014(X19,X20)!=skolem0010(X19,X20))&((((((member(X19,skolem0015(X19,X20),X20)&skolem0015(X19,X20)!=skolem0014(X19,X20))&skolem0015(X19,X20)!=skolem0013(X19,X20))&skolem0015(X19,X20)!=skolem0012(X19,X20))&skolem0015(X19,X20)!=skolem0011(X19,X20))&skolem0015(X19,X20)!=skolem0010(X19,X20))&(![X27]:(~member(X19,X27,X20)|(((((X27=skolem0015(X19,X20)|X27=skolem0014(X19,X20))|X27=skolem0013(X19,X20))|X27=skolem0012(X19,X20))|X27=skolem0011(X19,X20))|X27=skolem0010(X19,X20)))))))))))))&(![X28]:(![X29]:((![X30]:(~member(X28,X30,X29)|(![X31]:((~member(X28,X31,X29)|X31=X30)|(![X32]:(((~member(X28,X32,X29)|X32=X31)|X32=X30)|(![X33]:((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(![X34]:(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|(![X35]:((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|(member(X28,skolem0016(X28,X29,X30,X31,X32,X33,X34,X35),X29)&(((((skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X35&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X34)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X33)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X32)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X31)&skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X30))))))))))))))|six(X28,X29))))),inference(skolemize,[status(esa)],[c83])).])).
% 2.44/2.61 fof(c86,plain,(![X19]:(![X20]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(((~six(X19,X20)|member(X19,skolem0010(X19,X20),X20))&(((~six(X19,X20)|member(X19,skolem0011(X19,X20),X20))&(~six(X19,X20)|skolem0011(X19,X20)!=skolem0010(X19,X20)))&((((~six(X19,X20)|member(X19,skolem0012(X19,X20),X20))&(~six(X19,X20)|skolem0012(X19,X20)!=skolem0011(X19,X20)))&(~six(X19,X20)|skolem0012(X19,X20)!=skolem0010(X19,X20)))&(((((~six(X19,X20)|member(X19,skolem0013(X19,X20),X20))&(~six(X19,X20)|skolem0013(X19,X20)!=skolem0012(X19,X20)))&(~six(X19,X20)|skolem0013(X19,X20)!=skolem0011(X19,X20)))&(~six(X19,X20)|skolem0013(X19,X20)!=skolem0010(X19,X20)))&((((((~six(X19,X20)|member(X19,skolem0014(X19,X20),X20))&(~six(X19,X20)|skolem0014(X19,X20)!=skolem0013(X19,X20)))&(~six(X19,X20)|skolem0014(X19,X20)!=skolem0012(X19,X20)))&(~six(X19,X20)|skolem0014(X19,X20)!=skolem0011(X19,X20)))&(~six(X19,X20)|skolem0014(X19,X20)!=skolem0010(X19,X20)))&(((((((~six(X19,X20)|member(X19,skolem0015(X19,X20),X20))&(~six(X19,X20)|skolem0015(X19,X20)!=skolem0014(X19,X20)))&(~six(X19,X20)|skolem0015(X19,X20)!=skolem0013(X19,X20)))&(~six(X19,X20)|skolem0015(X19,X20)!=skolem0012(X19,X20)))&(~six(X19,X20)|skolem0015(X19,X20)!=skolem0011(X19,X20)))&(~six(X19,X20)|skolem0015(X19,X20)!=skolem0010(X19,X20)))&(~six(X19,X20)|(~member(X19,X27,X20)|(((((X27=skolem0015(X19,X20)|X27=skolem0014(X19,X20))|X27=skolem0013(X19,X20))|X27=skolem0012(X19,X20))|X27=skolem0011(X19,X20))|X27=skolem0010(X19,X20))))))))))&(((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|member(X28,skolem0016(X28,X29,X30,X31,X32,X33,X34,X35),X29)))))))|six(X28,X29))&(((((((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X35))))))|six(X28,X29))&((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X34))))))|six(X28,X29)))&((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X33))))))|six(X28,X29)))&((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X32))))))|six(X28,X29)))&((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X31))))))|six(X28,X29)))&((~member(X28,X30,X29)|((~member(X28,X31,X29)|X31=X30)|(((~member(X28,X32,X29)|X32=X31)|X32=X30)|((((~member(X28,X33,X29)|X33=X32)|X33=X31)|X33=X30)|(((((~member(X28,X34,X29)|X34=X33)|X34=X32)|X34=X31)|X34=X30)|((((((~member(X28,X35,X29)|X35=X34)|X35=X33)|X35=X32)|X35=X31)|X35=X30)|skolem0016(X28,X29,X30,X31,X32,X33,X34,X35)!=X30))))))|six(X28,X29)))))))))))))))),inference(distribute,[status(thm)],[c85])).
% 2.44/2.61 cnf(c88,plain,~six(X323,X324)|member(X323,skolem0011(X323,X324),X324),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.61 cnf(c356,plain,member(skolem0001,skolem0011(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c88, c63])).
% 2.44/2.61 cnf(c60,negated_conjecture,~member(skolem0001,X423,skolem0005)|nonreflexive(skolem0001,skolem0009(X423)),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 cnf(c626,plain,nonreflexive(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c60, c356])).
% 2.44/2.61 cnf(c57,negated_conjecture,~member(skolem0001,X420,skolem0005)|agent(skolem0001,skolem0009(X420),skolem0003),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 cnf(c585,plain,agent(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c57, c356])).
% 2.44/2.61 fof(ax46,axiom,(![U]:(![V]:(![W]:(![X]:(((nonreflexive(U,V)&agent(U,V,W))&patient(U,V,X))=>W!=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax46)).
% 2.44/2.61 fof(c75,plain,(![U]:(![V]:(![W]:(![X]:(((~nonreflexive(U,V)|~agent(U,V,W))|~patient(U,V,X))|W!=X))))),inference(fof_nnf,[status(thm)],[ax46])).
% 2.44/2.61 fof(c76,plain,(![X13]:(![X14]:(![X15]:(![X16]:(((~nonreflexive(X13,X14)|~agent(X13,X14,X15))|~patient(X13,X14,X16))|X15!=X16))))),inference(variable_rename,[status(thm)],[c75])).
% 2.44/2.61 cnf(c77,plain,~nonreflexive(X428,X426)|~agent(X428,X426,X429)|~patient(X428,X426,X427)|X429!=X427,inference(split_conjunct,[status(thm)],[c76])).
% 2.44/2.61 cnf(c58,negated_conjecture,~member(skolem0001,X421,skolem0005)|patient(skolem0001,skolem0009(X421),X421),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 cnf(c599,plain,patient(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005)),skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c58, c356])).
% 2.44/2.61 cnf(c961,plain,~nonreflexive(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005)))|~agent(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005)),X1301)|X1301!=skolem0011(skolem0001,skolem0005),inference(resolution,[status(thm)],[c599, c77])).
% 2.44/2.61 cnf(c1167,plain,~nonreflexive(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005)))|skolem0003!=skolem0011(skolem0001,skolem0005),inference(resolution,[status(thm)],[c961, c585])).
% 2.44/2.61 cnf(c1168,plain,skolem0003!=skolem0011(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1167, c626])).
% 2.44/2.61 cnf(c102,plain,~six(X331,X332)|member(X331,skolem0015(X331,X332),X332),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.61 cnf(c360,plain,member(skolem0001,skolem0015(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c102, c63])).
% 2.44/2.61 cnf(c625,plain,nonreflexive(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c60, c360])).
% 2.44/2.61 cnf(c584,plain,agent(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c57, c360])).
% 2.44/2.61 cnf(c598,plain,patient(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005)),skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c58, c360])).
% 2.44/2.61 cnf(c959,plain,~nonreflexive(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005)))|~agent(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005)),X1300)|X1300!=skolem0015(skolem0001,skolem0005),inference(resolution,[status(thm)],[c598, c77])).
% 2.44/2.61 cnf(c1165,plain,~nonreflexive(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005)))|skolem0003!=skolem0015(skolem0001,skolem0005),inference(resolution,[status(thm)],[c959, c584])).
% 2.44/2.61 cnf(c1166,plain,skolem0003!=skolem0015(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1165, c625])).
% 2.44/2.61 cnf(c90,plain,~six(X325,X326)|member(X325,skolem0012(X325,X326),X326),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.61 cnf(c357,plain,member(skolem0001,skolem0012(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c90, c63])).
% 2.44/2.61 cnf(c624,plain,nonreflexive(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c60, c357])).
% 2.44/2.61 cnf(c583,plain,agent(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c57, c357])).
% 2.44/2.61 cnf(c597,plain,patient(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005)),skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c58, c357])).
% 2.44/2.61 cnf(c957,plain,~nonreflexive(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005)))|~agent(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005)),X1299)|X1299!=skolem0012(skolem0001,skolem0005),inference(resolution,[status(thm)],[c597, c77])).
% 2.44/2.61 cnf(c1163,plain,~nonreflexive(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005)))|skolem0003!=skolem0012(skolem0001,skolem0005),inference(resolution,[status(thm)],[c957, c583])).
% 2.44/2.61 cnf(c1164,plain,skolem0003!=skolem0012(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1163, c624])).
% 2.44/2.61 cnf(c87,plain,~six(X317,X318)|member(X317,skolem0010(X317,X318),X318),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.61 cnf(c354,plain,member(skolem0001,skolem0010(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c87, c63])).
% 2.44/2.61 cnf(c623,plain,nonreflexive(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c60, c354])).
% 2.44/2.61 cnf(c582,plain,agent(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c57, c354])).
% 2.44/2.61 cnf(c596,plain,patient(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005)),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c58, c354])).
% 2.44/2.61 cnf(c953,plain,~nonreflexive(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005)))|~agent(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005)),X1298)|X1298!=skolem0010(skolem0001,skolem0005),inference(resolution,[status(thm)],[c596, c77])).
% 2.44/2.61 cnf(c1161,plain,~nonreflexive(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005)))|skolem0003!=skolem0010(skolem0001,skolem0005),inference(resolution,[status(thm)],[c953, c582])).
% 2.44/2.61 cnf(c1162,plain,skolem0003!=skolem0010(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1161, c623])).
% 2.44/2.61 cnf(c97,plain,~six(X329,X330)|member(X329,skolem0014(X329,X330),X330),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.61 cnf(c359,plain,member(skolem0001,skolem0014(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c97, c63])).
% 2.44/2.61 cnf(c622,plain,nonreflexive(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c60, c359])).
% 2.44/2.61 cnf(c581,plain,agent(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c57, c359])).
% 2.44/2.61 cnf(c595,plain,patient(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005)),skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c58, c359])).
% 2.44/2.61 cnf(c951,plain,~nonreflexive(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005)))|~agent(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005)),X1297)|X1297!=skolem0014(skolem0001,skolem0005),inference(resolution,[status(thm)],[c595, c77])).
% 2.44/2.61 cnf(c1159,plain,~nonreflexive(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005)))|skolem0003!=skolem0014(skolem0001,skolem0005),inference(resolution,[status(thm)],[c951, c581])).
% 2.44/2.61 cnf(c1160,plain,skolem0003!=skolem0014(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1159, c622])).
% 2.44/2.61 cnf(reflexivity,axiom,X123=X123,theory(equality)).
% 2.44/2.61 cnf(c37,axiom,X390!=X392|X391!=X388|X387!=X389|~patient(X390,X391,X387)|patient(X392,X388,X389),theory(equality)).
% 2.44/2.61 cnf(c962,plain,skolem0001!=X1291|skolem0009(skolem0011(skolem0001,skolem0005))!=X1293|skolem0011(skolem0001,skolem0005)!=X1292|patient(X1291,X1293,X1292),inference(resolution,[status(thm)],[c599, c37])).
% 2.44/2.61 cnf(c1156,plain,skolem0001!=X1295|skolem0011(skolem0001,skolem0005)!=X1294|patient(X1295,skolem0009(skolem0011(skolem0001,skolem0005)),X1294),inference(resolution,[status(thm)],[c962, reflexivity])).
% 2.44/2.61 cnf(c1157,plain,skolem0001!=X1296|patient(X1296,skolem0009(skolem0011(skolem0001,skolem0005)),skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c1156, reflexivity])).
% 2.44/2.61 cnf(c93,plain,~six(X327,X328)|member(X327,skolem0013(X327,X328),X328),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.61 cnf(c358,plain,member(skolem0001,skolem0013(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c93, c63])).
% 2.44/2.61 cnf(c621,plain,nonreflexive(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c60, c358])).
% 2.44/2.61 cnf(c580,plain,agent(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c57, c358])).
% 2.44/2.61 cnf(c594,plain,patient(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005)),skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c58, c358])).
% 2.44/2.61 cnf(c946,plain,~nonreflexive(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005)))|~agent(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005)),X1290)|X1290!=skolem0013(skolem0001,skolem0005),inference(resolution,[status(thm)],[c594, c77])).
% 2.44/2.61 cnf(c1154,plain,~nonreflexive(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005)))|skolem0003!=skolem0013(skolem0001,skolem0005),inference(resolution,[status(thm)],[c946, c580])).
% 2.44/2.61 cnf(c1155,plain,skolem0003!=skolem0013(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1154, c621])).
% 2.44/2.61 cnf(c960,plain,skolem0001!=X1284|skolem0009(skolem0015(skolem0001,skolem0005))!=X1286|skolem0015(skolem0001,skolem0005)!=X1285|patient(X1284,X1286,X1285),inference(resolution,[status(thm)],[c598, c37])).
% 2.44/2.61 cnf(c1151,plain,skolem0001!=X1287|skolem0015(skolem0001,skolem0005)!=X1288|patient(X1287,skolem0009(skolem0015(skolem0001,skolem0005)),X1288),inference(resolution,[status(thm)],[c960, reflexivity])).
% 2.44/2.61 cnf(c1152,plain,skolem0001!=X1289|patient(X1289,skolem0009(skolem0015(skolem0001,skolem0005)),skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c1151, reflexivity])).
% 2.44/2.61 cnf(c958,plain,skolem0001!=X1273|skolem0009(skolem0012(skolem0001,skolem0005))!=X1275|skolem0012(skolem0001,skolem0005)!=X1274|patient(X1273,X1275,X1274),inference(resolution,[status(thm)],[c597, c37])).
% 2.44/2.61 cnf(c1148,plain,skolem0001!=X1277|skolem0012(skolem0001,skolem0005)!=X1276|patient(X1277,skolem0009(skolem0012(skolem0001,skolem0005)),X1276),inference(resolution,[status(thm)],[c958, reflexivity])).
% 2.44/2.61 cnf(c1149,plain,skolem0001!=X1278|patient(X1278,skolem0009(skolem0012(skolem0001,skolem0005)),skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c1148, reflexivity])).
% 2.44/2.61 cnf(c954,plain,skolem0001!=X1262|skolem0009(skolem0010(skolem0001,skolem0005))!=X1264|skolem0010(skolem0001,skolem0005)!=X1263|patient(X1262,X1264,X1263),inference(resolution,[status(thm)],[c596, c37])).
% 2.44/2.61 cnf(c1145,plain,skolem0001!=X1266|skolem0010(skolem0001,skolem0005)!=X1265|patient(X1266,skolem0009(skolem0010(skolem0001,skolem0005)),X1265),inference(resolution,[status(thm)],[c954, reflexivity])).
% 2.44/2.61 cnf(c1146,plain,skolem0001!=X1272|patient(X1272,skolem0009(skolem0010(skolem0001,skolem0005)),skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c1145, reflexivity])).
% 2.44/2.61 cnf(c952,plain,skolem0001!=X1251|skolem0009(skolem0014(skolem0001,skolem0005))!=X1253|skolem0014(skolem0001,skolem0005)!=X1252|patient(X1251,X1253,X1252),inference(resolution,[status(thm)],[c595, c37])).
% 2.44/2.61 cnf(c1142,plain,skolem0001!=X1259|skolem0014(skolem0001,skolem0005)!=X1260|patient(X1259,skolem0009(skolem0014(skolem0001,skolem0005)),X1260),inference(resolution,[status(thm)],[c952, reflexivity])).
% 2.44/2.61 cnf(c1143,plain,skolem0001!=X1261|patient(X1261,skolem0009(skolem0014(skolem0001,skolem0005)),skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c1142, reflexivity])).
% 2.44/2.61 cnf(c947,plain,skolem0001!=X1245|skolem0009(skolem0013(skolem0001,skolem0005))!=X1247|skolem0013(skolem0001,skolem0005)!=X1246|patient(X1245,X1247,X1246),inference(resolution,[status(thm)],[c594, c37])).
% 2.44/2.61 cnf(c1139,plain,skolem0001!=X1249|skolem0013(skolem0001,skolem0005)!=X1248|patient(X1249,skolem0009(skolem0013(skolem0001,skolem0005)),X1248),inference(resolution,[status(thm)],[c947, reflexivity])).
% 2.44/2.61 cnf(c1140,plain,skolem0001!=X1250|patient(X1250,skolem0009(skolem0013(skolem0001,skolem0005)),skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c1139, reflexivity])).
% 2.44/2.61 cnf(c43,axiom,X417!=X419|X418!=X415|X414!=X416|~from_loc(X417,X418,X414)|from_loc(X419,X415,X416),theory(equality)).
% 2.44/2.61 cnf(c62,negated_conjecture,~member(skolem0001,X425,skolem0005)|from_loc(skolem0001,skolem0009(X425),skolem0004),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 cnf(c643,plain,from_loc(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c62, c356])).
% 2.44/2.61 cnf(c834,plain,skolem0001!=X1235|skolem0009(skolem0011(skolem0001,skolem0005))!=X1236|skolem0004!=X1234|from_loc(X1235,X1236,X1234),inference(resolution,[status(thm)],[c643, c43])).
% 2.44/2.61 cnf(c1136,plain,skolem0001!=X1237|skolem0004!=X1238|from_loc(X1237,skolem0009(skolem0011(skolem0001,skolem0005)),X1238),inference(resolution,[status(thm)],[c834, reflexivity])).
% 2.44/2.61 cnf(c1137,plain,skolem0001!=X1239|from_loc(X1239,skolem0009(skolem0011(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c1136, reflexivity])).
% 2.44/2.61 cnf(c642,plain,from_loc(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c62, c360])).
% 2.44/2.61 cnf(c832,plain,skolem0001!=X1224|skolem0009(skolem0015(skolem0001,skolem0005))!=X1225|skolem0004!=X1223|from_loc(X1224,X1225,X1223),inference(resolution,[status(thm)],[c642, c43])).
% 2.44/2.61 cnf(c1133,plain,skolem0001!=X1227|skolem0004!=X1226|from_loc(X1227,skolem0009(skolem0015(skolem0001,skolem0005)),X1226),inference(resolution,[status(thm)],[c832, reflexivity])).
% 2.44/2.61 cnf(c1134,plain,skolem0001!=X1228|from_loc(X1228,skolem0009(skolem0015(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c1133, reflexivity])).
% 2.44/2.61 cnf(c641,plain,from_loc(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c62, c357])).
% 2.44/2.61 cnf(c831,plain,skolem0001!=X1213|skolem0009(skolem0012(skolem0001,skolem0005))!=X1214|skolem0004!=X1212|from_loc(X1213,X1214,X1212),inference(resolution,[status(thm)],[c641, c43])).
% 2.44/2.61 cnf(c1130,plain,skolem0001!=X1215|skolem0004!=X1216|from_loc(X1215,skolem0009(skolem0012(skolem0001,skolem0005)),X1216),inference(resolution,[status(thm)],[c831, reflexivity])).
% 2.44/2.61 cnf(c1131,plain,skolem0001!=X1222|from_loc(X1222,skolem0009(skolem0012(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c1130, reflexivity])).
% 2.44/2.61 cnf(c640,plain,from_loc(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c62, c354])).
% 2.44/2.61 cnf(c830,plain,skolem0001!=X1200|skolem0009(skolem0010(skolem0001,skolem0005))!=X1201|skolem0004!=X1199|from_loc(X1200,X1201,X1199),inference(resolution,[status(thm)],[c640, c43])).
% 2.44/2.61 cnf(c1127,plain,skolem0001!=X1210|skolem0004!=X1209|from_loc(X1210,skolem0009(skolem0010(skolem0001,skolem0005)),X1209),inference(resolution,[status(thm)],[c830, reflexivity])).
% 2.44/2.61 cnf(c1128,plain,skolem0001!=X1211|from_loc(X1211,skolem0009(skolem0010(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c1127, reflexivity])).
% 2.44/2.61 cnf(c639,plain,from_loc(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c62, c359])).
% 2.44/2.61 cnf(c829,plain,skolem0001!=X1194|skolem0009(skolem0014(skolem0001,skolem0005))!=X1195|skolem0004!=X1193|from_loc(X1194,X1195,X1193),inference(resolution,[status(thm)],[c639, c43])).
% 2.44/2.61 cnf(c1124,plain,skolem0001!=X1196|skolem0004!=X1197|from_loc(X1196,skolem0009(skolem0014(skolem0001,skolem0005)),X1197),inference(resolution,[status(thm)],[c829, reflexivity])).
% 2.44/2.61 cnf(c1125,plain,skolem0001!=X1198|from_loc(X1198,skolem0009(skolem0014(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c1124, reflexivity])).
% 2.44/2.61 cnf(c638,plain,from_loc(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c62, c358])).
% 2.44/2.61 cnf(c828,plain,skolem0001!=X1181|skolem0009(skolem0013(skolem0001,skolem0005))!=X1182|skolem0004!=X1180|from_loc(X1181,X1182,X1180),inference(resolution,[status(thm)],[c638, c43])).
% 2.44/2.61 cnf(c1121,plain,skolem0001!=X1183|skolem0004!=X1184|from_loc(X1183,skolem0009(skolem0013(skolem0001,skolem0005)),X1184),inference(resolution,[status(thm)],[c828, reflexivity])).
% 2.44/2.61 cnf(c1122,plain,skolem0001!=X1185|from_loc(X1185,skolem0009(skolem0013(skolem0001,skolem0005)),skolem0004),inference(resolution,[status(thm)],[c1121, reflexivity])).
% 2.44/2.61 cnf(c39,axiom,X401!=X403|X402!=X399|X398!=X400|~agent(X401,X402,X398)|agent(X403,X399,X400),theory(equality)).
% 2.44/2.61 cnf(c826,plain,skolem0001!=X1169|skolem0009(skolem0011(skolem0001,skolem0005))!=X1167|skolem0003!=X1168|agent(X1169,X1167,X1168),inference(resolution,[status(thm)],[c585, c39])).
% 2.44/2.61 cnf(c1118,plain,skolem0001!=X1170|skolem0003!=X1171|agent(X1170,skolem0009(skolem0011(skolem0001,skolem0005)),X1171),inference(resolution,[status(thm)],[c826, reflexivity])).
% 2.44/2.61 cnf(c1119,plain,skolem0001!=X1172|agent(X1172,skolem0009(skolem0011(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c1118, reflexivity])).
% 2.44/2.61 cnf(c825,plain,skolem0001!=X1156|skolem0009(skolem0015(skolem0001,skolem0005))!=X1154|skolem0003!=X1155|agent(X1156,X1154,X1155),inference(resolution,[status(thm)],[c584, c39])).
% 2.44/2.61 cnf(c1115,plain,skolem0001!=X1158|skolem0003!=X1157|agent(X1158,skolem0009(skolem0015(skolem0001,skolem0005)),X1157),inference(resolution,[status(thm)],[c825, reflexivity])).
% 2.44/2.61 cnf(c1116,plain,skolem0001!=X1166|agent(X1166,skolem0009(skolem0015(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c1115, reflexivity])).
% 2.44/2.61 cnf(c824,plain,skolem0001!=X1143|skolem0009(skolem0012(skolem0001,skolem0005))!=X1141|skolem0003!=X1142|agent(X1143,X1141,X1142),inference(resolution,[status(thm)],[c583, c39])).
% 2.44/2.61 cnf(c1112,plain,skolem0001!=X1151|skolem0003!=X1152|agent(X1151,skolem0009(skolem0012(skolem0001,skolem0005)),X1152),inference(resolution,[status(thm)],[c824, reflexivity])).
% 2.44/2.61 cnf(c1113,plain,skolem0001!=X1153|agent(X1153,skolem0009(skolem0012(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c1112, reflexivity])).
% 2.44/2.61 cnf(c823,plain,skolem0001!=X1137|skolem0009(skolem0010(skolem0001,skolem0005))!=X1135|skolem0003!=X1136|agent(X1137,X1135,X1136),inference(resolution,[status(thm)],[c582, c39])).
% 2.44/2.61 cnf(c1109,plain,skolem0001!=X1138|skolem0003!=X1139|agent(X1138,skolem0009(skolem0010(skolem0001,skolem0005)),X1139),inference(resolution,[status(thm)],[c823, reflexivity])).
% 2.44/2.61 cnf(c1110,plain,skolem0001!=X1140|agent(X1140,skolem0009(skolem0010(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c1109, reflexivity])).
% 2.44/2.61 cnf(c822,plain,skolem0001!=X1131|skolem0009(skolem0014(skolem0001,skolem0005))!=X1129|skolem0003!=X1130|agent(X1131,X1129,X1130),inference(resolution,[status(thm)],[c581, c39])).
% 2.44/2.61 cnf(c1106,plain,skolem0001!=X1133|skolem0003!=X1132|agent(X1133,skolem0009(skolem0014(skolem0001,skolem0005)),X1132),inference(resolution,[status(thm)],[c822, reflexivity])).
% 2.44/2.61 cnf(c1107,plain,skolem0001!=X1134|agent(X1134,skolem0009(skolem0014(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c1106, reflexivity])).
% 2.44/2.61 cnf(c820,plain,skolem0001!=X1125|skolem0009(skolem0013(skolem0001,skolem0005))!=X1123|skolem0003!=X1124|agent(X1125,X1123,X1124),inference(resolution,[status(thm)],[c580, c39])).
% 2.44/2.61 cnf(c1103,plain,skolem0001!=X1126|skolem0003!=X1127|agent(X1126,skolem0009(skolem0013(skolem0001,skolem0005)),X1127),inference(resolution,[status(thm)],[c820, reflexivity])).
% 2.44/2.61 cnf(c1104,plain,skolem0001!=X1128|agent(X1128,skolem0009(skolem0013(skolem0001,skolem0005)),skolem0003),inference(resolution,[status(thm)],[c1103, reflexivity])).
% 2.44/2.61 cnf(c36,axiom,X384!=X386|X385!=X382|X381!=X383|~member(X384,X385,X381)|member(X386,X382,X383),theory(equality)).
% 2.44/2.61 cnf(c491,plain,skolem0001!=X896|skolem0015(skolem0001,skolem0005)!=X894|skolem0005!=X895|member(X896,X894,X895),inference(resolution,[status(thm)],[c360, c36])).
% 2.44/2.61 cnf(c943,plain,skolem0001!=X1120|skolem0005!=X1121|member(X1120,skolem0015(skolem0001,skolem0005),X1121),inference(resolution,[status(thm)],[c491, reflexivity])).
% 2.44/2.61 cnf(c1101,plain,skolem0001!=X1122|member(X1122,skolem0015(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c943, reflexivity])).
% 2.44/2.61 cnf(c489,plain,skolem0001!=X887|skolem0011(skolem0001,skolem0005)!=X885|skolem0005!=X886|member(X887,X885,X886),inference(resolution,[status(thm)],[c36, c356])).
% 2.44/2.61 cnf(c938,plain,skolem0001!=X1117|skolem0005!=X1118|member(X1117,skolem0011(skolem0001,skolem0005),X1118),inference(resolution,[status(thm)],[c489, reflexivity])).
% 2.44/2.61 cnf(c1099,plain,skolem0001!=X1119|member(X1119,skolem0011(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c938, reflexivity])).
% 2.44/2.61 cnf(c488,plain,skolem0001!=X880|skolem0012(skolem0001,skolem0005)!=X878|skolem0005!=X879|member(X880,X878,X879),inference(resolution,[status(thm)],[c36, c357])).
% 2.44/2.61 cnf(c934,plain,skolem0001!=X1114|skolem0005!=X1115|member(X1114,skolem0012(skolem0001,skolem0005),X1115),inference(resolution,[status(thm)],[c488, reflexivity])).
% 2.44/2.61 cnf(c1097,plain,skolem0001!=X1116|member(X1116,skolem0012(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c934, reflexivity])).
% 2.44/2.61 cnf(c487,plain,skolem0001!=X872|skolem0010(skolem0001,skolem0005)!=X870|skolem0005!=X871|member(X872,X870,X871),inference(resolution,[status(thm)],[c36, c354])).
% 2.44/2.61 cnf(c930,plain,skolem0001!=X1112|skolem0005!=X1111|member(X1112,skolem0010(skolem0001,skolem0005),X1111),inference(resolution,[status(thm)],[c487, reflexivity])).
% 2.44/2.61 cnf(c1095,plain,skolem0001!=X1113|member(X1113,skolem0010(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c930, reflexivity])).
% 2.44/2.61 cnf(c486,plain,skolem0001!=X863|skolem0014(skolem0001,skolem0005)!=X861|skolem0005!=X862|member(X863,X861,X862),inference(resolution,[status(thm)],[c36, c359])).
% 2.44/2.61 cnf(c925,plain,skolem0001!=X1108|skolem0005!=X1109|member(X1108,skolem0014(skolem0001,skolem0005),X1109),inference(resolution,[status(thm)],[c486, reflexivity])).
% 2.44/2.61 cnf(c1093,plain,skolem0001!=X1110|member(X1110,skolem0014(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c925, reflexivity])).
% 2.44/2.61 cnf(c485,plain,skolem0001!=X856|skolem0013(skolem0001,skolem0005)!=X854|skolem0005!=X855|member(X856,X854,X855),inference(resolution,[status(thm)],[c36, c358])).
% 2.44/2.61 cnf(c921,plain,skolem0001!=X1105|skolem0005!=X1106|member(X1105,skolem0013(skolem0001,skolem0005),X1106),inference(resolution,[status(thm)],[c485, reflexivity])).
% 2.44/2.61 cnf(c1091,plain,skolem0001!=X1107|member(X1107,skolem0013(skolem0001,skolem0005),skolem0005),inference(resolution,[status(thm)],[c921, reflexivity])).
% 2.44/2.61 cnf(c20,axiom,X291!=X293|X290!=X292|~fire(X291,X290)|fire(X293,X292),theory(equality)).
% 2.44/2.61 cnf(c61,negated_conjecture,~member(skolem0001,X424,skolem0005)|fire(skolem0001,skolem0009(X424)),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 cnf(c634,plain,fire(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c61, c356])).
% 2.44/2.61 cnf(c667,plain,skolem0001!=X1102|skolem0009(skolem0011(skolem0001,skolem0005))!=X1101|fire(X1102,X1101),inference(resolution,[status(thm)],[c634, c20])).
% 2.44/2.61 cnf(c1088,plain,skolem0001!=X1104|fire(X1104,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c667, reflexivity])).
% 2.44/2.61 cnf(c633,plain,fire(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c61, c360])).
% 2.44/2.61 cnf(c665,plain,skolem0001!=X1100|skolem0009(skolem0015(skolem0001,skolem0005))!=X1099|fire(X1100,X1099),inference(resolution,[status(thm)],[c633, c20])).
% 2.44/2.61 cnf(c1087,plain,skolem0001!=X1103|fire(X1103,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c665, reflexivity])).
% 2.44/2.61 cnf(c632,plain,fire(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c61, c357])).
% 2.44/2.61 cnf(c663,plain,skolem0001!=X1096|skolem0009(skolem0012(skolem0001,skolem0005))!=X1095|fire(X1096,X1095),inference(resolution,[status(thm)],[c632, c20])).
% 2.44/2.61 cnf(c1084,plain,skolem0001!=X1098|fire(X1098,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c663, reflexivity])).
% 2.44/2.61 cnf(c631,plain,fire(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c61, c354])).
% 2.44/2.61 cnf(c661,plain,skolem0001!=X1094|skolem0009(skolem0010(skolem0001,skolem0005))!=X1093|fire(X1094,X1093),inference(resolution,[status(thm)],[c631, c20])).
% 2.44/2.61 cnf(c1083,plain,skolem0001!=X1097|fire(X1097,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c661, reflexivity])).
% 2.44/2.61 cnf(c630,plain,fire(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c61, c359])).
% 2.44/2.61 cnf(c659,plain,skolem0001!=X1090|skolem0009(skolem0014(skolem0001,skolem0005))!=X1089|fire(X1090,X1089),inference(resolution,[status(thm)],[c630, c20])).
% 2.44/2.61 cnf(c1080,plain,skolem0001!=X1092|fire(X1092,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c659, reflexivity])).
% 2.44/2.61 cnf(c629,plain,fire(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c61, c358])).
% 2.44/2.61 cnf(c657,plain,skolem0001!=X1088|skolem0009(skolem0013(skolem0001,skolem0005))!=X1087|fire(X1088,X1087),inference(resolution,[status(thm)],[c629, c20])).
% 2.44/2.61 cnf(c1079,plain,skolem0001!=X1091|fire(X1091,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c657, reflexivity])).
% 2.44/2.61 cnf(c38,axiom,X394!=X396|X393!=X395|~nonreflexive(X394,X393)|nonreflexive(X396,X395),theory(equality)).
% 2.44/2.61 cnf(c656,plain,skolem0001!=X1083|skolem0009(skolem0011(skolem0001,skolem0005))!=X1084|nonreflexive(X1083,X1084),inference(resolution,[status(thm)],[c626, c38])).
% 2.44/2.61 cnf(c1076,plain,skolem0001!=X1086|nonreflexive(X1086,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c656, reflexivity])).
% 2.44/2.61 cnf(c655,plain,skolem0001!=X1081|skolem0009(skolem0015(skolem0001,skolem0005))!=X1082|nonreflexive(X1081,X1082),inference(resolution,[status(thm)],[c625, c38])).
% 2.44/2.61 cnf(c1075,plain,skolem0001!=X1085|nonreflexive(X1085,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c655, reflexivity])).
% 2.44/2.61 cnf(c654,plain,skolem0001!=X1077|skolem0009(skolem0012(skolem0001,skolem0005))!=X1078|nonreflexive(X1077,X1078),inference(resolution,[status(thm)],[c624, c38])).
% 2.44/2.61 cnf(c1072,plain,skolem0001!=X1080|nonreflexive(X1080,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c654, reflexivity])).
% 2.44/2.61 cnf(c653,plain,skolem0001!=X1075|skolem0009(skolem0010(skolem0001,skolem0005))!=X1076|nonreflexive(X1075,X1076),inference(resolution,[status(thm)],[c623, c38])).
% 2.44/2.61 cnf(c1071,plain,skolem0001!=X1079|nonreflexive(X1079,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c653, reflexivity])).
% 2.44/2.61 cnf(c652,plain,skolem0001!=X1071|skolem0009(skolem0014(skolem0001,skolem0005))!=X1072|nonreflexive(X1071,X1072),inference(resolution,[status(thm)],[c622, c38])).
% 2.44/2.61 cnf(c1068,plain,skolem0001!=X1074|nonreflexive(X1074,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c652, reflexivity])).
% 2.44/2.61 cnf(c651,plain,skolem0001!=X1069|skolem0009(skolem0013(skolem0001,skolem0005))!=X1070|nonreflexive(X1069,X1070),inference(resolution,[status(thm)],[c621, c38])).
% 2.44/2.61 cnf(c1067,plain,skolem0001!=X1073|nonreflexive(X1073,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c651, reflexivity])).
% 2.44/2.61 cnf(c34,axiom,X374!=X376|X373!=X375|~singleton(X374,X373)|singleton(X376,X375),theory(equality)).
% 2.44/2.61 fof(ax34,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 2.44/2.61 fof(c148,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 2.44/2.61 fof(c149,plain,(![X55]:(![X56]:(~thing(X55,X56)|singleton(X55,X56)))),inference(variable_rename,[status(thm)],[c148])).
% 2.44/2.61 cnf(c150,plain,~thing(X171,X170)|singleton(X171,X170),inference(split_conjunct,[status(thm)],[c149])).
% 2.44/2.61 fof(ax35,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 2.44/2.61 fof(c145,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 2.44/2.61 fof(c146,plain,(![X53]:(![X54]:(~eventuality(X53,X54)|thing(X53,X54)))),inference(variable_rename,[status(thm)],[c145])).
% 2.44/2.61 cnf(c147,plain,~eventuality(X165,X164)|thing(X165,X164),inference(split_conjunct,[status(thm)],[c146])).
% 2.44/2.61 fof(ax36,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 2.44/2.61 fof(c142,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax36])).
% 2.44/2.61 fof(c143,plain,(![X51]:(![X52]:(~event(X51,X52)|eventuality(X51,X52)))),inference(variable_rename,[status(thm)],[c142])).
% 2.44/2.61 cnf(c144,plain,~event(X162,X163)|eventuality(X162,X163),inference(split_conjunct,[status(thm)],[c143])).
% 2.44/2.61 cnf(c56,negated_conjecture,~member(skolem0001,X397,skolem0005)|event(skolem0001,skolem0009(X397)),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 cnf(c519,plain,event(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c56, c356])).
% 2.44/2.61 cnf(c532,plain,eventuality(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c519, c144])).
% 2.44/2.61 cnf(c562,plain,thing(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c532, c147])).
% 2.44/2.61 cnf(c617,plain,singleton(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c562, c150])).
% 2.44/2.61 cnf(c650,plain,skolem0001!=X1066|skolem0009(skolem0011(skolem0001,skolem0005))!=X1065|singleton(X1066,X1065),inference(resolution,[status(thm)],[c617, c34])).
% 2.44/2.61 cnf(c1064,plain,skolem0001!=X1068|singleton(X1068,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c650, reflexivity])).
% 2.44/2.61 cnf(c42,axiom,X411!=X413|X410!=X412|~present(X411,X410)|present(X413,X412),theory(equality)).
% 2.44/2.61 cnf(c59,negated_conjecture,~member(skolem0001,X422,skolem0005)|present(skolem0001,skolem0009(X422)),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.61 cnf(c613,plain,present(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c59, c356])).
% 2.44/2.61 cnf(c648,plain,skolem0001!=X1064|skolem0009(skolem0011(skolem0001,skolem0005))!=X1063|present(X1064,X1063),inference(resolution,[status(thm)],[c613, c42])).
% 2.44/2.61 cnf(c1063,plain,skolem0001!=X1067|present(X1067,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c648, reflexivity])).
% 2.44/2.61 cnf(c612,plain,present(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c59, c360])).
% 2.44/2.61 cnf(c647,plain,skolem0001!=X1060|skolem0009(skolem0015(skolem0001,skolem0005))!=X1059|present(X1060,X1059),inference(resolution,[status(thm)],[c612, c42])).
% 2.44/2.61 cnf(c1060,plain,skolem0001!=X1062|present(X1062,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c647, reflexivity])).
% 2.44/2.61 cnf(c611,plain,present(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c59, c357])).
% 2.44/2.61 cnf(c646,plain,skolem0001!=X1058|skolem0009(skolem0012(skolem0001,skolem0005))!=X1057|present(X1058,X1057),inference(resolution,[status(thm)],[c611, c42])).
% 2.44/2.61 cnf(c1059,plain,skolem0001!=X1061|present(X1061,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c646, reflexivity])).
% 2.44/2.61 cnf(c610,plain,present(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c59, c354])).
% 2.44/2.61 cnf(c645,plain,skolem0001!=X1054|skolem0009(skolem0010(skolem0001,skolem0005))!=X1053|present(X1054,X1053),inference(resolution,[status(thm)],[c610, c42])).
% 2.44/2.61 cnf(c1056,plain,skolem0001!=X1056|present(X1056,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c645, reflexivity])).
% 2.44/2.61 cnf(c609,plain,present(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c59, c359])).
% 2.44/2.61 cnf(c644,plain,skolem0001!=X1052|skolem0009(skolem0014(skolem0001,skolem0005))!=X1051|present(X1052,X1051),inference(resolution,[status(thm)],[c609, c42])).
% 2.44/2.61 cnf(c1055,plain,skolem0001!=X1055|present(X1055,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c644, reflexivity])).
% 2.44/2.61 cnf(c608,plain,present(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c59, c358])).
% 2.44/2.61 cnf(c637,plain,skolem0001!=X1048|skolem0009(skolem0013(skolem0001,skolem0005))!=X1047|present(X1048,X1047),inference(resolution,[status(thm)],[c608, c42])).
% 2.44/2.61 cnf(c1052,plain,skolem0001!=X1050|present(X1050,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c637, reflexivity])).
% 2.44/2.61 cnf(c518,plain,event(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c56, c360])).
% 2.44/2.61 cnf(c530,plain,eventuality(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c518, c144])).
% 2.44/2.61 cnf(c557,plain,thing(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c530, c147])).
% 2.44/2.61 cnf(c605,plain,singleton(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c557, c150])).
% 2.44/2.62 cnf(c636,plain,skolem0001!=X1046|skolem0009(skolem0015(skolem0001,skolem0005))!=X1045|singleton(X1046,X1045),inference(resolution,[status(thm)],[c605, c34])).
% 2.44/2.62 cnf(c1051,plain,skolem0001!=X1049|singleton(X1049,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c636, reflexivity])).
% 2.44/2.62 cnf(c517,plain,event(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c56, c357])).
% 2.44/2.62 cnf(c528,plain,eventuality(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c517, c144])).
% 2.44/2.62 cnf(c552,plain,thing(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c528, c147])).
% 2.44/2.62 cnf(c593,plain,singleton(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c552, c150])).
% 2.44/2.62 cnf(c635,plain,skolem0001!=X1042|skolem0009(skolem0012(skolem0001,skolem0005))!=X1041|singleton(X1042,X1041),inference(resolution,[status(thm)],[c593, c34])).
% 2.44/2.62 cnf(c1048,plain,skolem0001!=X1044|singleton(X1044,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c635, reflexivity])).
% 2.44/2.62 cnf(c516,plain,event(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c56, c354])).
% 2.44/2.62 cnf(c526,plain,eventuality(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c516, c144])).
% 2.44/2.62 cnf(c547,plain,thing(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c526, c147])).
% 2.44/2.62 cnf(c587,plain,singleton(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c547, c150])).
% 2.44/2.62 cnf(c628,plain,skolem0001!=X1040|skolem0009(skolem0010(skolem0001,skolem0005))!=X1039|singleton(X1040,X1039),inference(resolution,[status(thm)],[c587, c34])).
% 2.44/2.62 cnf(c1047,plain,skolem0001!=X1043|singleton(X1043,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c628, reflexivity])).
% 2.44/2.62 cnf(c515,plain,event(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c56, c359])).
% 2.44/2.62 cnf(c523,plain,eventuality(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c515, c144])).
% 2.44/2.62 cnf(c542,plain,thing(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c523, c147])).
% 2.44/2.62 cnf(c575,plain,singleton(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c542, c150])).
% 2.44/2.62 cnf(c627,plain,skolem0001!=X1036|skolem0009(skolem0014(skolem0001,skolem0005))!=X1035|singleton(X1036,X1035),inference(resolution,[status(thm)],[c575, c34])).
% 2.44/2.62 cnf(c1044,plain,skolem0001!=X1038|singleton(X1038,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c627, reflexivity])).
% 2.44/2.62 cnf(c514,plain,event(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c56, c358])).
% 2.44/2.62 cnf(c521,plain,eventuality(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c514, c144])).
% 2.44/2.62 cnf(c535,plain,thing(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c521, c147])).
% 2.44/2.62 cnf(c569,plain,singleton(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c535, c150])).
% 2.44/2.62 cnf(c620,plain,skolem0001!=X1034|skolem0009(skolem0013(skolem0001,skolem0005))!=X1033|singleton(X1034,X1033),inference(resolution,[status(thm)],[c569, c34])).
% 2.44/2.62 cnf(c1043,plain,skolem0001!=X1037|singleton(X1037,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c620, reflexivity])).
% 2.44/2.62 cnf(c33,axiom,X370!=X372|X369!=X371|~nonexistent(X370,X369)|nonexistent(X372,X371),theory(equality)).
% 2.44/2.62 fof(ax32,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 2.44/2.62 fof(c154,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 2.44/2.62 fof(c155,plain,(![X59]:(![X60]:(~eventuality(X59,X60)|nonexistent(X59,X60)))),inference(variable_rename,[status(thm)],[c154])).
% 2.44/2.62 cnf(c156,plain,~eventuality(X175,X174)|nonexistent(X175,X174),inference(split_conjunct,[status(thm)],[c155])).
% 2.44/2.62 cnf(c563,plain,nonexistent(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c532, c156])).
% 2.44/2.62 cnf(c618,plain,skolem0001!=X1030|skolem0009(skolem0011(skolem0001,skolem0005))!=X1029|nonexistent(X1030,X1029),inference(resolution,[status(thm)],[c563, c33])).
% 2.44/2.62 cnf(c1040,plain,skolem0001!=X1032|nonexistent(X1032,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c618, reflexivity])).
% 2.44/2.62 cnf(c14,axiom,X243!=X245|X242!=X244|~thing(X243,X242)|thing(X245,X244),theory(equality)).
% 2.44/2.62 cnf(c616,plain,skolem0001!=X1028|skolem0009(skolem0011(skolem0001,skolem0005))!=X1027|thing(X1028,X1027),inference(resolution,[status(thm)],[c562, c14])).
% 2.44/2.62 cnf(c1039,plain,skolem0001!=X1031|thing(X1031,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c616, reflexivity])).
% 2.44/2.62 cnf(c10,axiom,X209!=X211|X208!=X210|~unisex(X209,X208)|unisex(X211,X210),theory(equality)).
% 2.44/2.62 fof(ax31,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 2.44/2.62 fof(c157,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 2.44/2.62 fof(c158,plain,(![X61]:(![X62]:(~eventuality(X61,X62)|unisex(X61,X62)))),inference(variable_rename,[status(thm)],[c157])).
% 2.44/2.62 cnf(c159,plain,~eventuality(X181,X180)|unisex(X181,X180),inference(split_conjunct,[status(thm)],[c158])).
% 2.44/2.62 cnf(c561,plain,unisex(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c532, c159])).
% 2.44/2.62 cnf(c615,plain,skolem0001!=X1023|skolem0009(skolem0011(skolem0001,skolem0005))!=X1024|unisex(X1023,X1024),inference(resolution,[status(thm)],[c561, c10])).
% 2.44/2.62 cnf(c1036,plain,skolem0001!=X1026|unisex(X1026,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c615, reflexivity])).
% 2.44/2.62 cnf(c13,axiom,X235!=X237|X234!=X236|~specific(X235,X234)|specific(X237,X236),theory(equality)).
% 2.44/2.62 fof(ax33,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 2.44/2.62 fof(c151,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 2.44/2.62 fof(c152,plain,(![X57]:(![X58]:(~eventuality(X57,X58)|specific(X57,X58)))),inference(variable_rename,[status(thm)],[c151])).
% 2.44/2.62 cnf(c153,plain,~eventuality(X173,X172)|specific(X173,X172),inference(split_conjunct,[status(thm)],[c152])).
% 2.44/2.62 cnf(c560,plain,specific(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c532, c153])).
% 2.44/2.62 cnf(c614,plain,skolem0001!=X1022|skolem0009(skolem0011(skolem0001,skolem0005))!=X1021|specific(X1022,X1021),inference(resolution,[status(thm)],[c560, c13])).
% 2.44/2.62 cnf(c1035,plain,skolem0001!=X1025|specific(X1025,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c614, reflexivity])).
% 2.44/2.62 cnf(c558,plain,nonexistent(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c530, c156])).
% 2.44/2.62 cnf(c606,plain,skolem0001!=X1018|skolem0009(skolem0015(skolem0001,skolem0005))!=X1017|nonexistent(X1018,X1017),inference(resolution,[status(thm)],[c558, c33])).
% 2.44/2.62 cnf(c1032,plain,skolem0001!=X1020|nonexistent(X1020,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c606, reflexivity])).
% 2.44/2.62 cnf(c604,plain,skolem0001!=X1016|skolem0009(skolem0015(skolem0001,skolem0005))!=X1015|thing(X1016,X1015),inference(resolution,[status(thm)],[c557, c14])).
% 2.44/2.62 cnf(c1031,plain,skolem0001!=X1019|thing(X1019,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c604, reflexivity])).
% 2.44/2.62 cnf(c556,plain,unisex(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c530, c159])).
% 2.44/2.62 cnf(c603,plain,skolem0001!=X1011|skolem0009(skolem0015(skolem0001,skolem0005))!=X1012|unisex(X1011,X1012),inference(resolution,[status(thm)],[c556, c10])).
% 2.44/2.62 cnf(c1028,plain,skolem0001!=X1014|unisex(X1014,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c603, reflexivity])).
% 2.44/2.62 cnf(c555,plain,specific(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c530, c153])).
% 2.44/2.62 cnf(c602,plain,skolem0001!=X1010|skolem0009(skolem0015(skolem0001,skolem0005))!=X1009|specific(X1010,X1009),inference(resolution,[status(thm)],[c555, c13])).
% 2.44/2.62 cnf(c1027,plain,skolem0001!=X1013|specific(X1013,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c602, reflexivity])).
% 2.44/2.62 cnf(c553,plain,nonexistent(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c528, c156])).
% 2.44/2.62 cnf(c600,plain,skolem0001!=X1006|skolem0009(skolem0012(skolem0001,skolem0005))!=X1005|nonexistent(X1006,X1005),inference(resolution,[status(thm)],[c553, c33])).
% 2.44/2.62 cnf(c1024,plain,skolem0001!=X1008|nonexistent(X1008,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c600, reflexivity])).
% 2.44/2.62 cnf(c592,plain,skolem0001!=X1004|skolem0009(skolem0012(skolem0001,skolem0005))!=X1003|thing(X1004,X1003),inference(resolution,[status(thm)],[c552, c14])).
% 2.44/2.62 cnf(c1023,plain,skolem0001!=X1007|thing(X1007,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c592, reflexivity])).
% 2.44/2.62 cnf(c551,plain,unisex(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c528, c159])).
% 2.44/2.62 cnf(c591,plain,skolem0001!=X999|skolem0009(skolem0012(skolem0001,skolem0005))!=X1000|unisex(X999,X1000),inference(resolution,[status(thm)],[c551, c10])).
% 2.44/2.62 cnf(c1020,plain,skolem0001!=X1002|unisex(X1002,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c591, reflexivity])).
% 2.44/2.62 cnf(c550,plain,specific(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c528, c153])).
% 2.44/2.62 cnf(c590,plain,skolem0001!=X998|skolem0009(skolem0012(skolem0001,skolem0005))!=X997|specific(X998,X997),inference(resolution,[status(thm)],[c550, c13])).
% 2.44/2.62 cnf(c1019,plain,skolem0001!=X1001|specific(X1001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c590, reflexivity])).
% 2.44/2.62 cnf(c548,plain,nonexistent(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c526, c156])).
% 2.44/2.62 cnf(c588,plain,skolem0001!=X994|skolem0009(skolem0010(skolem0001,skolem0005))!=X993|nonexistent(X994,X993),inference(resolution,[status(thm)],[c548, c33])).
% 2.44/2.62 cnf(c1016,plain,skolem0001!=X996|nonexistent(X996,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c588, reflexivity])).
% 2.44/2.62 cnf(c586,plain,skolem0001!=X992|skolem0009(skolem0010(skolem0001,skolem0005))!=X991|thing(X992,X991),inference(resolution,[status(thm)],[c547, c14])).
% 2.44/2.62 cnf(c1015,plain,skolem0001!=X995|thing(X995,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c586, reflexivity])).
% 2.44/2.62 cnf(c546,plain,unisex(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c526, c159])).
% 2.44/2.62 cnf(c579,plain,skolem0001!=X987|skolem0009(skolem0010(skolem0001,skolem0005))!=X988|unisex(X987,X988),inference(resolution,[status(thm)],[c546, c10])).
% 2.44/2.62 cnf(c1012,plain,skolem0001!=X990|unisex(X990,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c579, reflexivity])).
% 2.44/2.62 cnf(c545,plain,specific(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c526, c153])).
% 2.44/2.62 cnf(c578,plain,skolem0001!=X986|skolem0009(skolem0010(skolem0001,skolem0005))!=X985|specific(X986,X985),inference(resolution,[status(thm)],[c545, c13])).
% 2.44/2.62 cnf(c1011,plain,skolem0001!=X989|specific(X989,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c578, reflexivity])).
% 2.44/2.62 cnf(c543,plain,nonexistent(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c523, c156])).
% 2.44/2.62 cnf(c576,plain,skolem0001!=X982|skolem0009(skolem0014(skolem0001,skolem0005))!=X981|nonexistent(X982,X981),inference(resolution,[status(thm)],[c543, c33])).
% 2.44/2.62 cnf(c1008,plain,skolem0001!=X984|nonexistent(X984,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c576, reflexivity])).
% 2.44/2.62 cnf(c574,plain,skolem0001!=X980|skolem0009(skolem0014(skolem0001,skolem0005))!=X979|thing(X980,X979),inference(resolution,[status(thm)],[c542, c14])).
% 2.44/2.62 cnf(c1007,plain,skolem0001!=X983|thing(X983,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c574, reflexivity])).
% 2.44/2.62 cnf(c541,plain,unisex(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c523, c159])).
% 2.44/2.62 cnf(c573,plain,skolem0001!=X975|skolem0009(skolem0014(skolem0001,skolem0005))!=X976|unisex(X975,X976),inference(resolution,[status(thm)],[c541, c10])).
% 2.44/2.62 cnf(c1004,plain,skolem0001!=X978|unisex(X978,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c573, reflexivity])).
% 2.44/2.62 cnf(c540,plain,specific(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c523, c153])).
% 2.44/2.62 cnf(c572,plain,skolem0001!=X974|skolem0009(skolem0014(skolem0001,skolem0005))!=X973|specific(X974,X973),inference(resolution,[status(thm)],[c540, c13])).
% 2.44/2.62 cnf(c1003,plain,skolem0001!=X977|specific(X977,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c572, reflexivity])).
% 2.44/2.62 cnf(c536,plain,nonexistent(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c521, c156])).
% 2.44/2.62 cnf(c570,plain,skolem0001!=X970|skolem0009(skolem0013(skolem0001,skolem0005))!=X969|nonexistent(X970,X969),inference(resolution,[status(thm)],[c536, c33])).
% 2.44/2.62 cnf(c1000,plain,skolem0001!=X972|nonexistent(X972,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c570, reflexivity])).
% 2.44/2.62 cnf(c568,plain,skolem0001!=X968|skolem0009(skolem0013(skolem0001,skolem0005))!=X967|thing(X968,X967),inference(resolution,[status(thm)],[c535, c14])).
% 2.44/2.62 cnf(c999,plain,skolem0001!=X971|thing(X971,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c568, reflexivity])).
% 2.44/2.62 cnf(c534,plain,unisex(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c521, c159])).
% 2.44/2.62 cnf(c567,plain,skolem0001!=X963|skolem0009(skolem0013(skolem0001,skolem0005))!=X964|unisex(X963,X964),inference(resolution,[status(thm)],[c534, c10])).
% 2.44/2.62 cnf(c996,plain,skolem0001!=X966|unisex(X966,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c567, reflexivity])).
% 2.44/2.62 cnf(c533,plain,specific(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c521, c153])).
% 2.44/2.62 cnf(c566,plain,skolem0001!=X962|skolem0009(skolem0013(skolem0001,skolem0005))!=X961|specific(X962,X961),inference(resolution,[status(thm)],[c533, c13])).
% 2.44/2.62 cnf(c995,plain,skolem0001!=X965|specific(X965,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c566, reflexivity])).
% 2.44/2.62 cnf(c32,axiom,X366!=X368|X365!=X367|~eventuality(X366,X365)|eventuality(X368,X367),theory(equality)).
% 2.44/2.62 cnf(c564,plain,skolem0001!=X957|skolem0009(skolem0011(skolem0001,skolem0005))!=X958|eventuality(X957,X958),inference(resolution,[status(thm)],[c532, c32])).
% 2.44/2.62 cnf(c992,plain,skolem0001!=X960|eventuality(X960,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c564, reflexivity])).
% 2.44/2.62 cnf(c559,plain,skolem0001!=X955|skolem0009(skolem0015(skolem0001,skolem0005))!=X956|eventuality(X955,X956),inference(resolution,[status(thm)],[c530, c32])).
% 2.44/2.62 cnf(c991,plain,skolem0001!=X959|eventuality(X959,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c559, reflexivity])).
% 2.44/2.62 cnf(c554,plain,skolem0001!=X951|skolem0009(skolem0012(skolem0001,skolem0005))!=X952|eventuality(X951,X952),inference(resolution,[status(thm)],[c528, c32])).
% 2.44/2.62 cnf(c988,plain,skolem0001!=X954|eventuality(X954,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c554, reflexivity])).
% 2.44/2.62 cnf(c549,plain,skolem0001!=X949|skolem0009(skolem0010(skolem0001,skolem0005))!=X950|eventuality(X949,X950),inference(resolution,[status(thm)],[c526, c32])).
% 2.44/2.62 cnf(c987,plain,skolem0001!=X953|eventuality(X953,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c549, reflexivity])).
% 2.44/2.62 cnf(c544,plain,skolem0001!=X945|skolem0009(skolem0014(skolem0001,skolem0005))!=X946|eventuality(X945,X946),inference(resolution,[status(thm)],[c523, c32])).
% 2.44/2.62 cnf(c984,plain,skolem0001!=X948|eventuality(X948,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c544, reflexivity])).
% 2.44/2.62 cnf(c54,negated_conjecture,of(skolem0001,skolem0004,skolem0003),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c41,axiom,X407!=X409|X408!=X405|X404!=X406|~of(X407,X408,X404)|of(X409,X405,X406),theory(equality)).
% 2.44/2.62 cnf(c539,plain,skolem0001!=X940|skolem0004!=X942|skolem0003!=X941|of(X940,X942,X941),inference(resolution,[status(thm)],[c41, c54])).
% 2.44/2.62 cnf(c982,plain,skolem0001!=X944|skolem0004!=X943|of(X944,X943,skolem0003),inference(resolution,[status(thm)],[c539, reflexivity])).
% 2.44/2.62 cnf(c983,plain,skolem0001!=X947|of(X947,skolem0004,skolem0003),inference(resolution,[status(thm)],[c982, reflexivity])).
% 2.44/2.62 cnf(c74,negated_conjecture,of(skolem0001,skolem0008,skolem0006),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c538,plain,skolem0001!=X934|skolem0008!=X936|skolem0006!=X935|of(X934,X936,X935),inference(resolution,[status(thm)],[c41, c74])).
% 2.44/2.62 cnf(c979,plain,skolem0001!=X938|skolem0008!=X937|of(X938,X937,skolem0006),inference(resolution,[status(thm)],[c538, reflexivity])).
% 2.44/2.62 cnf(c980,plain,skolem0001!=X939|of(X939,skolem0008,skolem0006),inference(resolution,[status(thm)],[c979, reflexivity])).
% 2.44/2.62 cnf(c537,plain,skolem0001!=X931|skolem0009(skolem0013(skolem0001,skolem0005))!=X932|eventuality(X931,X932),inference(resolution,[status(thm)],[c521, c32])).
% 2.44/2.62 cnf(c977,plain,skolem0001!=X933|eventuality(X933,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c537, reflexivity])).
% 2.44/2.62 cnf(c21,axiom,X299!=X301|X298!=X300|~event(X299,X298)|event(X301,X300),theory(equality)).
% 2.44/2.62 cnf(c531,plain,skolem0001!=X929|skolem0009(skolem0011(skolem0001,skolem0005))!=X928|event(X929,X928),inference(resolution,[status(thm)],[c519, c21])).
% 2.44/2.62 cnf(c975,plain,skolem0001!=X930|event(X930,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c531, reflexivity])).
% 2.44/2.62 cnf(c529,plain,skolem0001!=X926|skolem0009(skolem0015(skolem0001,skolem0005))!=X925|event(X926,X925),inference(resolution,[status(thm)],[c518, c21])).
% 2.44/2.62 cnf(c973,plain,skolem0001!=X927|event(X927,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c529, reflexivity])).
% 2.44/2.62 cnf(c527,plain,skolem0001!=X923|skolem0009(skolem0012(skolem0001,skolem0005))!=X922|event(X923,X922),inference(resolution,[status(thm)],[c517, c21])).
% 2.44/2.62 cnf(c971,plain,skolem0001!=X924|event(X924,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c527, reflexivity])).
% 2.44/2.62 cnf(c525,plain,skolem0001!=X917|skolem0009(skolem0010(skolem0001,skolem0005))!=X916|event(X917,X916),inference(resolution,[status(thm)],[c516, c21])).
% 2.44/2.62 cnf(c967,plain,skolem0001!=X921|event(X921,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c525, reflexivity])).
% 2.44/2.62 cnf(c69,negated_conjecture,agent(skolem0001,skolem0008,skolem0002),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c524,plain,skolem0001!=X915|skolem0008!=X913|skolem0002!=X914|agent(X915,X913,X914),inference(resolution,[status(thm)],[c39, c69])).
% 2.44/2.62 cnf(c966,plain,skolem0001!=X918|skolem0008!=X919|agent(X918,X919,skolem0002),inference(resolution,[status(thm)],[c524, reflexivity])).
% 2.44/2.62 cnf(c968,plain,skolem0001!=X920|agent(X920,skolem0008,skolem0002),inference(resolution,[status(thm)],[c966, reflexivity])).
% 2.44/2.62 cnf(c70,negated_conjecture,patient(skolem0001,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c649,plain,~nonreflexive(skolem0001,skolem0008)|~agent(skolem0001,skolem0008,X912)|X912!=skolem0007,inference(resolution,[status(thm)],[c77, c70])).
% 2.44/2.62 cnf(c965,plain,~nonreflexive(skolem0001,skolem0008)|skolem0002!=skolem0007,inference(resolution,[status(thm)],[c649, c69])).
% 2.44/2.62 cnf(c522,plain,skolem0001!=X910|skolem0009(skolem0014(skolem0001,skolem0005))!=X909|event(X910,X909),inference(resolution,[status(thm)],[c515, c21])).
% 2.44/2.62 cnf(c963,plain,skolem0001!=X911|event(X911,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c522, reflexivity])).
% 2.44/2.62 cnf(c520,plain,skolem0001!=X907|skolem0009(skolem0013(skolem0001,skolem0005))!=X906|event(X907,X906),inference(resolution,[status(thm)],[c514, c21])).
% 2.44/2.62 cnf(c955,plain,skolem0001!=X908|event(X908,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c520, reflexivity])).
% 2.44/2.62 cnf(c500,plain,skolem0001!=X900|skolem0008!=X902|skolem0007!=X901|patient(X900,X902,X901),inference(resolution,[status(thm)],[c37, c70])).
% 2.44/2.62 cnf(c948,plain,skolem0001!=X903|skolem0008!=X904|patient(X903,X904,skolem0007),inference(resolution,[status(thm)],[c500, reflexivity])).
% 2.44/2.62 cnf(c949,plain,skolem0001!=X905|patient(X905,skolem0008,skolem0007),inference(resolution,[status(thm)],[c948, reflexivity])).
% 2.44/2.62 fof(ax26,axiom,(![U]:(![V]:(act(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 2.44/2.62 fof(c172,plain,(![U]:(![V]:(~act(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 2.44/2.62 fof(c173,plain,(![X71]:(![X72]:(~act(X71,X72)|event(X71,X72)))),inference(variable_rename,[status(thm)],[c172])).
% 2.44/2.62 cnf(c174,plain,~act(X202,X203)|event(X202,X203),inference(split_conjunct,[status(thm)],[c173])).
% 2.44/2.62 fof(ax27,axiom,(![U]:(![V]:(action(U,V)=>act(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 2.44/2.62 fof(c169,plain,(![U]:(![V]:(~action(U,V)|act(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 2.44/2.62 fof(c170,plain,(![X69]:(![X70]:(~action(X69,X70)|act(X69,X70)))),inference(variable_rename,[status(thm)],[c169])).
% 2.44/2.62 cnf(c171,plain,~action(X200,X201)|act(X200,X201),inference(split_conjunct,[status(thm)],[c170])).
% 2.44/2.62 fof(ax25,axiom,(![U]:(![V]:(shot(U,V)=>action(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 2.44/2.62 fof(c175,plain,(![U]:(![V]:(~shot(U,V)|action(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 2.44/2.62 fof(c176,plain,(![X73]:(![X74]:(~shot(X73,X74)|action(X73,X74)))),inference(variable_rename,[status(thm)],[c175])).
% 2.44/2.62 cnf(c177,plain,~shot(X212,X213)|action(X212,X213),inference(split_conjunct,[status(thm)],[c176])).
% 2.44/2.62 cnf(c65,negated_conjecture,~member(skolem0001,X316,skolem0005)|shot(skolem0001,X316),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c490,plain,shot(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c360, c65])).
% 2.44/2.62 cnf(c492,plain,action(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c490, c177])).
% 2.44/2.62 cnf(c494,plain,act(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c492, c171])).
% 2.44/2.62 cnf(c496,plain,event(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c494, c174])).
% 2.44/2.62 cnf(c499,plain,eventuality(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c496, c144])).
% 2.44/2.62 cnf(c503,plain,thing(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c499, c147])).
% 2.44/2.62 cnf(c509,plain,singleton(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c503, c150])).
% 2.44/2.62 cnf(c513,plain,skolem0001!=X898|skolem0015(skolem0001,skolem0005)!=X897|singleton(X898,X897),inference(resolution,[status(thm)],[c509, c34])).
% 2.44/2.62 cnf(c944,plain,skolem0001!=X899|singleton(X899,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c513, reflexivity])).
% 2.44/2.62 cnf(c504,plain,nonexistent(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c499, c156])).
% 2.44/2.62 cnf(c510,plain,skolem0001!=X892|skolem0015(skolem0001,skolem0005)!=X891|nonexistent(X892,X891),inference(resolution,[status(thm)],[c504, c33])).
% 2.44/2.62 cnf(c941,plain,skolem0001!=X893|nonexistent(X893,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c510, reflexivity])).
% 2.44/2.62 cnf(c508,plain,skolem0001!=X889|skolem0015(skolem0001,skolem0005)!=X888|thing(X889,X888),inference(resolution,[status(thm)],[c503, c14])).
% 2.44/2.62 cnf(c939,plain,skolem0001!=X890|thing(X890,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c508, reflexivity])).
% 2.44/2.62 cnf(c502,plain,unisex(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c499, c159])).
% 2.44/2.62 cnf(c507,plain,skolem0001!=X882|skolem0015(skolem0001,skolem0005)!=X883|unisex(X882,X883),inference(resolution,[status(thm)],[c502, c10])).
% 2.44/2.62 cnf(c936,plain,skolem0001!=X884|unisex(X884,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c507, reflexivity])).
% 2.44/2.62 cnf(c501,plain,specific(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c499, c153])).
% 2.44/2.62 cnf(c506,plain,skolem0001!=X877|skolem0015(skolem0001,skolem0005)!=X876|specific(X877,X876),inference(resolution,[status(thm)],[c501, c13])).
% 2.44/2.62 cnf(c933,plain,skolem0001!=X881|specific(X881,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c506, reflexivity])).
% 2.44/2.62 cnf(c505,plain,skolem0001!=X873|skolem0015(skolem0001,skolem0005)!=X874|eventuality(X873,X874),inference(resolution,[status(thm)],[c499, c32])).
% 2.44/2.62 cnf(c931,plain,skolem0001!=X875|eventuality(X875,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c505, reflexivity])).
% 2.44/2.62 cnf(c498,plain,skolem0001!=X868|skolem0015(skolem0001,skolem0005)!=X867|event(X868,X867),inference(resolution,[status(thm)],[c496, c21])).
% 2.44/2.62 cnf(c928,plain,skolem0001!=X869|event(X869,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c498, reflexivity])).
% 2.44/2.62 cnf(c28,axiom,X350!=X352|X349!=X351|~act(X350,X349)|act(X352,X351),theory(equality)).
% 2.44/2.62 cnf(c497,plain,skolem0001!=X864|skolem0015(skolem0001,skolem0005)!=X865|act(X864,X865),inference(resolution,[status(thm)],[c494, c28])).
% 2.44/2.62 cnf(c926,plain,skolem0001!=X866|act(X866,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c497, reflexivity])).
% 2.44/2.62 cnf(c27,axiom,X346!=X348|X345!=X347|~action(X346,X345)|action(X348,X347),theory(equality)).
% 2.44/2.62 cnf(c495,plain,skolem0001!=X859|skolem0015(skolem0001,skolem0005)!=X858|action(X859,X858),inference(resolution,[status(thm)],[c492, c27])).
% 2.44/2.62 cnf(c923,plain,skolem0001!=X860|action(X860,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c495, reflexivity])).
% 2.44/2.62 cnf(c26,axiom,X342!=X344|X341!=X343|~shot(X342,X341)|shot(X344,X343),theory(equality)).
% 2.44/2.62 cnf(c493,plain,skolem0001!=X853|skolem0015(skolem0001,skolem0005)!=X852|shot(X853,X852),inference(resolution,[status(thm)],[c490, c26])).
% 2.44/2.62 cnf(c920,plain,skolem0001!=X857|shot(X857,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c493, reflexivity])).
% 2.44/2.62 cnf(c454,plain,shot(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c359, c65])).
% 2.44/2.62 cnf(c455,plain,action(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c454, c177])).
% 2.44/2.62 cnf(c466,plain,act(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c455, c171])).
% 2.44/2.62 cnf(c468,plain,event(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c466, c174])).
% 2.44/2.62 cnf(c471,plain,eventuality(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c468, c144])).
% 2.44/2.62 cnf(c474,plain,thing(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c471, c147])).
% 2.44/2.62 cnf(c481,plain,singleton(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c474, c150])).
% 2.44/2.62 cnf(c484,plain,skolem0001!=X849|skolem0014(skolem0001,skolem0005)!=X848|singleton(X849,X848),inference(resolution,[status(thm)],[c481, c34])).
% 2.44/2.62 cnf(c917,plain,skolem0001!=X851|singleton(X851,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c484, reflexivity])).
% 2.44/2.62 cnf(c475,plain,nonexistent(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c471, c156])).
% 2.44/2.62 cnf(c482,plain,skolem0001!=X847|skolem0014(skolem0001,skolem0005)!=X846|nonexistent(X847,X846),inference(resolution,[status(thm)],[c475, c33])).
% 2.44/2.62 cnf(c916,plain,skolem0001!=X850|nonexistent(X850,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c482, reflexivity])).
% 2.44/2.62 cnf(c480,plain,skolem0001!=X843|skolem0014(skolem0001,skolem0005)!=X842|thing(X843,X842),inference(resolution,[status(thm)],[c474, c14])).
% 2.44/2.62 cnf(c913,plain,skolem0001!=X845|thing(X845,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c480, reflexivity])).
% 2.44/2.62 cnf(c473,plain,unisex(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c471, c159])).
% 2.44/2.62 cnf(c479,plain,skolem0001!=X840|skolem0014(skolem0001,skolem0005)!=X841|unisex(X840,X841),inference(resolution,[status(thm)],[c473, c10])).
% 2.44/2.62 cnf(c912,plain,skolem0001!=X844|unisex(X844,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c479, reflexivity])).
% 2.44/2.62 cnf(c472,plain,specific(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c471, c153])).
% 2.44/2.62 cnf(c477,plain,skolem0001!=X837|skolem0014(skolem0001,skolem0005)!=X836|specific(X837,X836),inference(resolution,[status(thm)],[c472, c13])).
% 2.44/2.62 cnf(c909,plain,skolem0001!=X839|specific(X839,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c477, reflexivity])).
% 2.44/2.62 cnf(c476,plain,skolem0001!=X834|skolem0014(skolem0001,skolem0005)!=X835|eventuality(X834,X835),inference(resolution,[status(thm)],[c471, c32])).
% 2.44/2.62 cnf(c908,plain,skolem0001!=X838|eventuality(X838,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c476, reflexivity])).
% 2.44/2.62 cnf(c470,plain,skolem0001!=X831|skolem0014(skolem0001,skolem0005)!=X830|event(X831,X830),inference(resolution,[status(thm)],[c468, c21])).
% 2.44/2.62 cnf(c905,plain,skolem0001!=X833|event(X833,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c470, reflexivity])).
% 2.44/2.62 cnf(c469,plain,skolem0001!=X828|skolem0014(skolem0001,skolem0005)!=X829|act(X828,X829),inference(resolution,[status(thm)],[c466, c28])).
% 2.44/2.62 cnf(c904,plain,skolem0001!=X832|act(X832,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c469, reflexivity])).
% 2.44/2.62 cnf(c467,plain,skolem0001!=X825|skolem0014(skolem0001,skolem0005)!=X824|action(X825,X824),inference(resolution,[status(thm)],[c455, c27])).
% 2.44/2.62 cnf(c901,plain,skolem0001!=X827|action(X827,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c467, reflexivity])).
% 2.44/2.62 cnf(c362,plain,shot(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c354, c65])).
% 2.44/2.62 cnf(c363,plain,action(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c362, c177])).
% 2.44/2.62 cnf(c364,plain,act(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c363, c171])).
% 2.44/2.62 cnf(c365,plain,event(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c364, c174])).
% 2.44/2.62 cnf(c367,plain,eventuality(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c365, c144])).
% 2.44/2.62 cnf(c371,plain,thing(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c367, c147])).
% 2.44/2.62 cnf(c376,plain,singleton(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c371, c150])).
% 2.44/2.62 cnf(c462,plain,skolem0001!=X823|skolem0010(skolem0001,skolem0005)!=X822|singleton(X823,X822),inference(resolution,[status(thm)],[c34, c376])).
% 2.44/2.62 cnf(c900,plain,skolem0001!=X826|singleton(X826,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c462, reflexivity])).
% 2.44/2.62 cnf(c401,plain,shot(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c357, c65])).
% 2.44/2.62 cnf(c403,plain,action(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c401, c177])).
% 2.44/2.62 cnf(c405,plain,act(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c403, c171])).
% 2.44/2.62 cnf(c407,plain,event(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c405, c174])).
% 2.44/2.62 cnf(c410,plain,eventuality(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c407, c144])).
% 2.44/2.62 cnf(c413,plain,thing(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c410, c147])).
% 2.44/2.62 cnf(c419,plain,singleton(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c413, c150])).
% 2.44/2.62 cnf(c461,plain,skolem0001!=X819|skolem0012(skolem0001,skolem0005)!=X818|singleton(X819,X818),inference(resolution,[status(thm)],[c34, c419])).
% 2.44/2.62 cnf(c897,plain,skolem0001!=X821|singleton(X821,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c461, reflexivity])).
% 2.44/2.62 cnf(c379,plain,shot(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c356, c65])).
% 2.44/2.62 cnf(c380,plain,action(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c379, c177])).
% 2.44/2.62 cnf(c382,plain,act(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c380, c171])).
% 2.44/2.62 cnf(c386,plain,event(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c382, c174])).
% 2.44/2.62 cnf(c388,plain,eventuality(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c386, c144])).
% 2.44/2.62 cnf(c391,plain,thing(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c388, c147])).
% 2.44/2.62 cnf(c399,plain,singleton(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c391, c150])).
% 2.44/2.62 cnf(c460,plain,skolem0001!=X817|skolem0011(skolem0001,skolem0005)!=X816|singleton(X817,X816),inference(resolution,[status(thm)],[c34, c399])).
% 2.44/2.62 cnf(c896,plain,skolem0001!=X820|singleton(X820,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c460, reflexivity])).
% 2.44/2.62 cnf(c422,plain,shot(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c358, c65])).
% 2.44/2.62 cnf(c423,plain,action(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c422, c177])).
% 2.44/2.62 cnf(c425,plain,act(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c423, c171])).
% 2.44/2.62 cnf(c427,plain,event(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c425, c174])).
% 2.44/2.62 cnf(c436,plain,eventuality(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c427, c144])).
% 2.44/2.62 cnf(c439,plain,thing(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c436, c147])).
% 2.44/2.62 cnf(c445,plain,singleton(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c439, c150])).
% 2.44/2.62 cnf(c457,plain,skolem0001!=X813|skolem0013(skolem0001,skolem0005)!=X812|singleton(X813,X812),inference(resolution,[status(thm)],[c34, c445])).
% 2.44/2.62 cnf(c893,plain,skolem0001!=X815|singleton(X815,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c457, reflexivity])).
% 2.44/2.62 cnf(c456,plain,skolem0001!=X811|skolem0014(skolem0001,skolem0005)!=X810|shot(X811,X810),inference(resolution,[status(thm)],[c454, c26])).
% 2.44/2.62 cnf(c892,plain,skolem0001!=X814|shot(X814,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c456, reflexivity])).
% 2.44/2.62 cnf(c440,plain,nonexistent(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c436, c156])).
% 2.44/2.62 cnf(c452,plain,skolem0001!=X807|skolem0013(skolem0001,skolem0005)!=X806|nonexistent(X807,X806),inference(resolution,[status(thm)],[c440, c33])).
% 2.44/2.62 cnf(c889,plain,skolem0001!=X809|nonexistent(X809,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c452, reflexivity])).
% 2.44/2.62 cnf(c390,plain,nonexistent(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c388, c156])).
% 2.44/2.62 cnf(c451,plain,skolem0001!=X805|skolem0011(skolem0001,skolem0005)!=X804|nonexistent(X805,X804),inference(resolution,[status(thm)],[c33, c390])).
% 2.44/2.62 cnf(c888,plain,skolem0001!=X808|nonexistent(X808,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c451, reflexivity])).
% 2.44/2.62 cnf(c412,plain,nonexistent(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c410, c156])).
% 2.44/2.62 cnf(c449,plain,skolem0001!=X801|skolem0012(skolem0001,skolem0005)!=X800|nonexistent(X801,X800),inference(resolution,[status(thm)],[c33, c412])).
% 2.44/2.62 cnf(c885,plain,skolem0001!=X803|nonexistent(X803,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c449, reflexivity])).
% 2.44/2.62 cnf(c370,plain,nonexistent(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c367, c156])).
% 2.44/2.62 cnf(c448,plain,skolem0001!=X799|skolem0010(skolem0001,skolem0005)!=X798|nonexistent(X799,X798),inference(resolution,[status(thm)],[c33, c370])).
% 2.44/2.62 cnf(c884,plain,skolem0001!=X802|nonexistent(X802,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c448, reflexivity])).
% 2.44/2.62 cnf(c444,plain,skolem0001!=X795|skolem0013(skolem0001,skolem0005)!=X794|thing(X795,X794),inference(resolution,[status(thm)],[c439, c14])).
% 2.44/2.62 cnf(c881,plain,skolem0001!=X797|thing(X797,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c444, reflexivity])).
% 2.44/2.62 cnf(c438,plain,unisex(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c436, c159])).
% 2.44/2.62 cnf(c443,plain,skolem0001!=X792|skolem0013(skolem0001,skolem0005)!=X793|unisex(X792,X793),inference(resolution,[status(thm)],[c438, c10])).
% 2.44/2.62 cnf(c880,plain,skolem0001!=X796|unisex(X796,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c443, reflexivity])).
% 2.44/2.62 cnf(c437,plain,specific(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c436, c153])).
% 2.44/2.62 cnf(c442,plain,skolem0001!=X789|skolem0013(skolem0001,skolem0005)!=X788|specific(X789,X788),inference(resolution,[status(thm)],[c437, c13])).
% 2.44/2.62 cnf(c877,plain,skolem0001!=X791|specific(X791,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c442, reflexivity])).
% 2.44/2.62 cnf(c441,plain,skolem0001!=X786|skolem0013(skolem0001,skolem0005)!=X787|eventuality(X786,X787),inference(resolution,[status(thm)],[c436, c32])).
% 2.44/2.62 cnf(c876,plain,skolem0001!=X790|eventuality(X790,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c441, reflexivity])).
% 2.44/2.62 cnf(c435,plain,skolem0001!=X783|skolem0013(skolem0001,skolem0005)!=X782|event(X783,X782),inference(resolution,[status(thm)],[c427, c21])).
% 2.44/2.62 cnf(c873,plain,skolem0001!=X785|event(X785,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c435, reflexivity])).
% 2.44/2.62 cnf(c433,plain,skolem0001!=X780|skolem0012(skolem0001,skolem0005)!=X781|eventuality(X780,X781),inference(resolution,[status(thm)],[c32, c410])).
% 2.44/2.62 cnf(c872,plain,skolem0001!=X784|eventuality(X784,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c433, reflexivity])).
% 2.44/2.62 cnf(c432,plain,skolem0001!=X776|skolem0010(skolem0001,skolem0005)!=X777|eventuality(X776,X777),inference(resolution,[status(thm)],[c32, c367])).
% 2.44/2.62 cnf(c869,plain,skolem0001!=X779|eventuality(X779,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c432, reflexivity])).
% 2.44/2.62 cnf(c430,plain,skolem0001!=X774|skolem0011(skolem0001,skolem0005)!=X775|eventuality(X774,X775),inference(resolution,[status(thm)],[c32, c388])).
% 2.44/2.62 cnf(c868,plain,skolem0001!=X778|eventuality(X778,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c430, reflexivity])).
% 2.44/2.62 cnf(c428,plain,skolem0001!=X770|skolem0013(skolem0001,skolem0005)!=X771|act(X770,X771),inference(resolution,[status(thm)],[c425, c28])).
% 2.44/2.62 cnf(c865,plain,skolem0001!=X773|act(X773,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c428, reflexivity])).
% 2.44/2.62 cnf(c426,plain,skolem0001!=X767|skolem0013(skolem0001,skolem0005)!=X766|action(X767,X766),inference(resolution,[status(thm)],[c423, c27])).
% 2.44/2.62 cnf(c862,plain,skolem0001!=X772|action(X772,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c426, reflexivity])).
% 2.44/2.62 cnf(c424,plain,skolem0001!=X762|skolem0013(skolem0001,skolem0005)!=X761|shot(X762,X761),inference(resolution,[status(thm)],[c422, c26])).
% 2.44/2.62 cnf(c858,plain,skolem0001!=X769|shot(X769,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c424, reflexivity])).
% 2.44/2.62 cnf(c414,plain,unisex(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c410, c159])).
% 2.44/2.62 cnf(c420,plain,skolem0001!=X757|skolem0012(skolem0001,skolem0005)!=X758|unisex(X757,X758),inference(resolution,[status(thm)],[c414, c10])).
% 2.44/2.62 cnf(c855,plain,skolem0001!=X768|unisex(X768,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c420, reflexivity])).
% 2.44/2.62 cnf(c418,plain,skolem0001!=X753|skolem0012(skolem0001,skolem0005)!=X752|thing(X753,X752),inference(resolution,[status(thm)],[c413, c14])).
% 2.44/2.62 cnf(c851,plain,skolem0001!=X765|thing(X765,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c418, reflexivity])).
% 2.44/2.62 cnf(c411,plain,specific(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c410, c153])).
% 2.44/2.62 cnf(c416,plain,skolem0001!=X749|skolem0012(skolem0001,skolem0005)!=X748|specific(X749,X748),inference(resolution,[status(thm)],[c411, c13])).
% 2.44/2.62 cnf(c848,plain,skolem0001!=X764|specific(X764,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c416, reflexivity])).
% 2.44/2.62 cnf(c409,plain,skolem0001!=X744|skolem0012(skolem0001,skolem0005)!=X743|event(X744,X743),inference(resolution,[status(thm)],[c407, c21])).
% 2.44/2.62 cnf(c844,plain,skolem0001!=X763|event(X763,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c409, reflexivity])).
% 2.44/2.62 cnf(c408,plain,skolem0001!=X739|skolem0012(skolem0001,skolem0005)!=X740|act(X739,X740),inference(resolution,[status(thm)],[c405, c28])).
% 2.44/2.62 cnf(c841,plain,skolem0001!=X760|act(X760,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c408, reflexivity])).
% 2.44/2.62 cnf(c406,plain,skolem0001!=X735|skolem0012(skolem0001,skolem0005)!=X734|action(X735,X734),inference(resolution,[status(thm)],[c403, c27])).
% 2.44/2.62 cnf(c837,plain,skolem0001!=X759|action(X759,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c406, reflexivity])).
% 2.44/2.62 cnf(c404,plain,skolem0001!=X731|skolem0012(skolem0001,skolem0005)!=X730|shot(X731,X730),inference(resolution,[status(thm)],[c401, c26])).
% 2.44/2.62 cnf(c833,plain,skolem0001!=X756|shot(X756,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c404, reflexivity])).
% 2.44/2.62 cnf(c392,plain,unisex(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c388, c159])).
% 2.44/2.62 cnf(c400,plain,skolem0001!=X728|skolem0011(skolem0001,skolem0005)!=X729|unisex(X728,X729),inference(resolution,[status(thm)],[c392, c10])).
% 2.44/2.62 cnf(c827,plain,skolem0001!=X755|unisex(X755,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c400, reflexivity])).
% 2.44/2.62 cnf(c398,plain,skolem0001!=X727|skolem0011(skolem0001,skolem0005)!=X726|thing(X727,X726),inference(resolution,[status(thm)],[c391, c14])).
% 2.44/2.62 cnf(c821,plain,skolem0001!=X754|thing(X754,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c398, reflexivity])).
% 2.44/2.62 cnf(c396,plain,skolem0001!=X721|skolem0011(skolem0001,skolem0005)!=X722|act(X721,X722),inference(resolution,[status(thm)],[c28, c382])).
% 2.44/2.62 cnf(c817,plain,skolem0001!=X751|act(X751,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c396, reflexivity])).
% 2.44/2.62 cnf(c395,plain,skolem0001!=X713|skolem0010(skolem0001,skolem0005)!=X714|act(X713,X714),inference(resolution,[status(thm)],[c28, c364])).
% 2.44/2.62 cnf(c812,plain,skolem0001!=X750|act(X750,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c395, reflexivity])).
% 2.44/2.62 cnf(c389,plain,specific(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c388, c153])).
% 2.44/2.62 cnf(c393,plain,skolem0001!=X708|skolem0011(skolem0001,skolem0005)!=X707|specific(X708,X707),inference(resolution,[status(thm)],[c389, c13])).
% 2.44/2.62 cnf(c808,plain,skolem0001!=X747|specific(X747,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c393, reflexivity])).
% 2.44/2.62 cnf(c387,plain,skolem0001!=X701|skolem0011(skolem0001,skolem0005)!=X700|event(X701,X700),inference(resolution,[status(thm)],[c386, c21])).
% 2.44/2.62 cnf(c804,plain,skolem0001!=X746|event(X746,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c387, reflexivity])).
% 2.44/2.62 cnf(c384,plain,skolem0001!=X693|skolem0010(skolem0001,skolem0005)!=X692|action(X693,X692),inference(resolution,[status(thm)],[c27, c363])).
% 2.44/2.62 cnf(c799,plain,skolem0001!=X745|action(X745,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c384, reflexivity])).
% 2.44/2.62 cnf(c383,plain,skolem0001!=X687|skolem0011(skolem0001,skolem0005)!=X686|action(X687,X686),inference(resolution,[status(thm)],[c27, c380])).
% 2.44/2.62 cnf(c795,plain,skolem0001!=X742|action(X742,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c383, reflexivity])).
% 2.44/2.62 cnf(c381,plain,skolem0001!=X680|skolem0011(skolem0001,skolem0005)!=X679|shot(X680,X679),inference(resolution,[status(thm)],[c379, c26])).
% 2.44/2.62 cnf(c791,plain,skolem0001!=X741|shot(X741,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c381, reflexivity])).
% 2.44/2.62 cnf(c378,plain,skolem0001!=X672|skolem0010(skolem0001,skolem0005)!=X671|shot(X672,X671),inference(resolution,[status(thm)],[c26, c362])).
% 2.44/2.62 cnf(c786,plain,skolem0001!=X738|shot(X738,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c378, reflexivity])).
% 2.44/2.62 cnf(c372,plain,unisex(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c367, c159])).
% 2.44/2.62 cnf(c377,plain,skolem0001!=X665|skolem0010(skolem0001,skolem0005)!=X666|unisex(X665,X666),inference(resolution,[status(thm)],[c372, c10])).
% 2.44/2.62 cnf(c782,plain,skolem0001!=X737|unisex(X737,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c377, reflexivity])).
% 2.44/2.62 cnf(c375,plain,skolem0001!=X659|skolem0010(skolem0001,skolem0005)!=X658|thing(X659,X658),inference(resolution,[status(thm)],[c371, c14])).
% 2.44/2.62 cnf(c778,plain,skolem0001!=X736|thing(X736,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c375, reflexivity])).
% 2.44/2.62 cnf(c369,plain,specific(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c367, c153])).
% 2.44/2.62 cnf(c373,plain,skolem0001!=X651|skolem0010(skolem0001,skolem0005)!=X650|specific(X651,X650),inference(resolution,[status(thm)],[c369, c13])).
% 2.44/2.62 cnf(c773,plain,skolem0001!=X733|specific(X733,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c373, reflexivity])).
% 2.44/2.62 cnf(c366,plain,skolem0001!=X645|skolem0010(skolem0001,skolem0005)!=X644|event(X645,X644),inference(resolution,[status(thm)],[c365, c21])).
% 2.44/2.62 cnf(c769,plain,skolem0001!=X732|event(X732,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c366, reflexivity])).
% 2.44/2.62 cnf(c71,negated_conjecture,present(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c565,plain,skolem0001!=X724|skolem0008!=X723|present(X724,X723),inference(resolution,[status(thm)],[c42, c71])).
% 2.44/2.62 cnf(c818,plain,skolem0001!=X725|present(X725,skolem0008),inference(resolution,[status(thm)],[c565, reflexivity])).
% 2.44/2.62 cnf(c72,negated_conjecture,nonreflexive(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c512,plain,skolem0001!=X718|skolem0008!=X719|nonreflexive(X718,X719),inference(resolution,[status(thm)],[c38, c72])).
% 2.44/2.62 cnf(c815,plain,skolem0001!=X720|nonreflexive(X720,skolem0008),inference(resolution,[status(thm)],[c512, reflexivity])).
% 2.44/2.62 cnf(c73,negated_conjecture,scream(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 fof(ax38,axiom,(![U]:(![V]:(scream(U,V)=>sound(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 2.44/2.62 fof(c136,plain,(![U]:(![V]:(~scream(U,V)|sound(U,V)))),inference(fof_nnf,[status(thm)],[ax38])).
% 2.44/2.62 fof(c137,plain,(![X47]:(![X48]:(~scream(X47,X48)|sound(X47,X48)))),inference(variable_rename,[status(thm)],[c136])).
% 2.44/2.62 cnf(c138,plain,~scream(X155,X154)|sound(X155,X154),inference(split_conjunct,[status(thm)],[c137])).
% 2.44/2.62 cnf(c258,plain,sound(skolem0001,skolem0008),inference(resolution,[status(thm)],[c138, c73])).
% 2.44/2.62 cnf(c35,axiom,X378!=X380|X377!=X379|~sound(X378,X377)|sound(X380,X379),theory(equality)).
% 2.44/2.62 cnf(c478,plain,skolem0001!=X716|skolem0008!=X715|sound(X716,X715),inference(resolution,[status(thm)],[c35, c258])).
% 2.44/2.62 cnf(c813,plain,skolem0001!=X717|sound(X717,skolem0008),inference(resolution,[status(thm)],[c478, reflexivity])).
% 2.44/2.62 fof(ax14,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 2.44/2.62 fof(c208,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 2.44/2.62 fof(c209,plain,(![X95]:(![X96]:(~entity(X95,X96)|thing(X95,X96)))),inference(variable_rename,[status(thm)],[c208])).
% 2.44/2.62 cnf(c210,plain,~entity(X251,X250)|thing(X251,X250),inference(split_conjunct,[status(thm)],[c209])).
% 2.44/2.62 cnf(c53,negated_conjecture,man(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 fof(ax8,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 2.44/2.62 fof(c226,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 2.44/2.62 fof(c227,plain,(![X107]:(![X108]:(~man(X107,X108)|human_person(X107,X108)))),inference(variable_rename,[status(thm)],[c226])).
% 2.44/2.62 cnf(c228,plain,~man(X275,X274)|human_person(X275,X274),inference(split_conjunct,[status(thm)],[c227])).
% 2.44/2.62 cnf(c324,plain,human_person(skolem0001,skolem0003),inference(resolution,[status(thm)],[c228, c53])).
% 2.44/2.62 fof(ax7,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 2.44/2.62 fof(c229,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 2.44/2.62 fof(c230,plain,(![X109]:(![X110]:(~human_person(X109,X110)|organism(X109,X110)))),inference(variable_rename,[status(thm)],[c229])).
% 2.44/2.62 cnf(c231,plain,~human_person(X281,X280)|organism(X281,X280),inference(split_conjunct,[status(thm)],[c230])).
% 2.44/2.62 cnf(c327,plain,organism(skolem0001,skolem0003),inference(resolution,[status(thm)],[c231, c324])).
% 2.44/2.62 fof(ax6,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 2.44/2.62 fof(c232,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 2.44/2.62 fof(c233,plain,(![X111]:(![X112]:(~organism(X111,X112)|entity(X111,X112)))),inference(variable_rename,[status(thm)],[c232])).
% 2.44/2.62 cnf(c234,plain,~organism(X283,X282)|entity(X283,X282),inference(split_conjunct,[status(thm)],[c233])).
% 2.44/2.62 cnf(c329,plain,entity(skolem0001,skolem0003),inference(resolution,[status(thm)],[c234, c327])).
% 2.44/2.62 cnf(c330,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c329, c210])).
% 2.44/2.62 cnf(c335,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c330, c150])).
% 2.44/2.62 cnf(c465,plain,skolem0001!=X711|skolem0003!=X710|singleton(X711,X710),inference(resolution,[status(thm)],[c34, c335])).
% 2.44/2.62 cnf(c810,plain,skolem0001!=X712|singleton(X712,skolem0003),inference(resolution,[status(thm)],[c465, reflexivity])).
% 2.44/2.62 cnf(c55,negated_conjecture,cannon(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 fof(ax20,axiom,(![U]:(![V]:(cannon(U,V)=>weapon(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 2.44/2.62 fof(c190,plain,(![U]:(![V]:(~cannon(U,V)|weapon(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 2.44/2.62 fof(c191,plain,(![X83]:(![X84]:(~cannon(X83,X84)|weapon(X83,X84)))),inference(variable_rename,[status(thm)],[c190])).
% 2.44/2.62 cnf(c192,plain,~cannon(X230,X231)|weapon(X230,X231),inference(split_conjunct,[status(thm)],[c191])).
% 2.44/2.62 cnf(c293,plain,weapon(skolem0001,skolem0004),inference(resolution,[status(thm)],[c192, c55])).
% 2.44/2.62 fof(ax19,axiom,(![U]:(![V]:(weapon(U,V)=>weaponry(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 2.44/2.62 fof(c193,plain,(![U]:(![V]:(~weapon(U,V)|weaponry(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 2.44/2.62 fof(c194,plain,(![X85]:(![X86]:(~weapon(X85,X86)|weaponry(X85,X86)))),inference(variable_rename,[status(thm)],[c193])).
% 2.44/2.62 cnf(c195,plain,~weapon(X232,X233)|weaponry(X232,X233),inference(split_conjunct,[status(thm)],[c194])).
% 2.44/2.62 cnf(c294,plain,weaponry(skolem0001,skolem0004),inference(resolution,[status(thm)],[c195, c293])).
% 2.44/2.62 fof(ax18,axiom,(![U]:(![V]:(weaponry(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 2.44/2.62 fof(c196,plain,(![U]:(![V]:(~weaponry(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 2.44/2.62 fof(c197,plain,(![X87]:(![X88]:(~weaponry(X87,X88)|instrumentality(X87,X88)))),inference(variable_rename,[status(thm)],[c196])).
% 2.44/2.62 cnf(c198,plain,~weaponry(X238,X239)|instrumentality(X238,X239),inference(split_conjunct,[status(thm)],[c197])).
% 2.44/2.62 cnf(c298,plain,instrumentality(skolem0001,skolem0004),inference(resolution,[status(thm)],[c198, c294])).
% 2.44/2.62 fof(ax17,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 2.44/2.62 fof(c199,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 2.44/2.62 fof(c200,plain,(![X89]:(![X90]:(~instrumentality(X89,X90)|artifact(X89,X90)))),inference(variable_rename,[status(thm)],[c199])).
% 2.44/2.62 cnf(c201,plain,~instrumentality(X240,X241)|artifact(X240,X241),inference(split_conjunct,[status(thm)],[c200])).
% 2.44/2.62 cnf(c299,plain,artifact(skolem0001,skolem0004),inference(resolution,[status(thm)],[c201, c298])).
% 2.44/2.62 fof(ax16,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 2.44/2.62 fof(c202,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 2.44/2.62 fof(c203,plain,(![X91]:(![X92]:(~artifact(X91,X92)|object(X91,X92)))),inference(variable_rename,[status(thm)],[c202])).
% 2.44/2.62 cnf(c204,plain,~artifact(X246,X247)|object(X246,X247),inference(split_conjunct,[status(thm)],[c203])).
% 2.44/2.62 cnf(c303,plain,object(skolem0001,skolem0004),inference(resolution,[status(thm)],[c204, c299])).
% 2.44/2.62 fof(ax15,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 2.44/2.62 fof(c205,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 2.44/2.62 fof(c206,plain,(![X93]:(![X94]:(~object(X93,X94)|entity(X93,X94)))),inference(variable_rename,[status(thm)],[c205])).
% 2.44/2.62 cnf(c207,plain,~object(X249,X248)|entity(X249,X248),inference(split_conjunct,[status(thm)],[c206])).
% 2.44/2.62 cnf(c305,plain,entity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c207, c303])).
% 2.44/2.62 cnf(c307,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c210, c305])).
% 2.44/2.62 cnf(c310,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c307, c150])).
% 2.44/2.62 cnf(c464,plain,skolem0001!=X706|skolem0004!=X705|singleton(X706,X705),inference(resolution,[status(thm)],[c34, c310])).
% 2.44/2.62 cnf(c807,plain,skolem0001!=X709|singleton(X709,skolem0004),inference(resolution,[status(thm)],[c464, reflexivity])).
% 2.44/2.62 cnf(c67,negated_conjecture,cry(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 fof(ax29,axiom,(![U]:(![V]:(cry(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 2.44/2.62 fof(c163,plain,(![U]:(![V]:(~cry(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 2.44/2.62 fof(c164,plain,(![X65]:(![X66]:(~cry(X65,X66)|event(X65,X66)))),inference(variable_rename,[status(thm)],[c163])).
% 2.44/2.62 cnf(c165,plain,~cry(X188,X189)|event(X188,X189),inference(split_conjunct,[status(thm)],[c164])).
% 2.44/2.62 cnf(c268,plain,event(skolem0001,skolem0007),inference(resolution,[status(thm)],[c165, c67])).
% 2.44/2.62 cnf(c269,plain,eventuality(skolem0001,skolem0007),inference(resolution,[status(thm)],[c268, c144])).
% 2.44/2.62 cnf(c272,plain,thing(skolem0001,skolem0007),inference(resolution,[status(thm)],[c269, c147])).
% 2.44/2.62 cnf(c275,plain,singleton(skolem0001,skolem0007),inference(resolution,[status(thm)],[c272, c150])).
% 2.44/2.62 cnf(c463,plain,skolem0001!=X703|skolem0007!=X702|singleton(X703,X702),inference(resolution,[status(thm)],[c34, c275])).
% 2.44/2.62 cnf(c805,plain,skolem0001!=X704|singleton(X704,skolem0007),inference(resolution,[status(thm)],[c463, reflexivity])).
% 2.44/2.62 cnf(c68,negated_conjecture,event(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 cnf(c260,plain,eventuality(skolem0001,skolem0008),inference(resolution,[status(thm)],[c144, c68])).
% 2.44/2.62 cnf(c261,plain,thing(skolem0001,skolem0008),inference(resolution,[status(thm)],[c147, c260])).
% 2.44/2.62 cnf(c262,plain,singleton(skolem0001,skolem0008),inference(resolution,[status(thm)],[c150, c261])).
% 2.44/2.62 cnf(c459,plain,skolem0001!=X698|skolem0008!=X697|singleton(X698,X697),inference(resolution,[status(thm)],[c34, c262])).
% 2.44/2.62 cnf(c802,plain,skolem0001!=X699|singleton(X699,skolem0008),inference(resolution,[status(thm)],[c459, reflexivity])).
% 2.44/2.62 cnf(c66,negated_conjecture,revenge(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.62 fof(ax28,axiom,(![U]:(![V]:(revenge(U,V)=>action(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 2.44/2.62 fof(c166,plain,(![U]:(![V]:(~revenge(U,V)|action(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 2.44/2.62 fof(c167,plain,(![X67]:(![X68]:(~revenge(X67,X68)|action(X67,X68)))),inference(variable_rename,[status(thm)],[c166])).
% 2.44/2.62 cnf(c168,plain,~revenge(X199,X198)|action(X199,X198),inference(split_conjunct,[status(thm)],[c167])).
% 2.44/2.62 cnf(c276,plain,action(skolem0001,skolem0006),inference(resolution,[status(thm)],[c168, c66])).
% 2.44/2.62 cnf(c277,plain,act(skolem0001,skolem0006),inference(resolution,[status(thm)],[c171, c276])).
% 2.44/2.62 cnf(c278,plain,event(skolem0001,skolem0006),inference(resolution,[status(thm)],[c174, c277])).
% 2.44/2.63 cnf(c279,plain,eventuality(skolem0001,skolem0006),inference(resolution,[status(thm)],[c278, c144])).
% 2.44/2.63 cnf(c282,plain,thing(skolem0001,skolem0006),inference(resolution,[status(thm)],[c279, c147])).
% 2.44/2.63 cnf(c285,plain,singleton(skolem0001,skolem0006),inference(resolution,[status(thm)],[c282, c150])).
% 2.44/2.63 cnf(c458,plain,skolem0001!=X695|skolem0006!=X694|singleton(X695,X694),inference(resolution,[status(thm)],[c34, c285])).
% 2.44/2.63 cnf(c800,plain,skolem0001!=X696|singleton(X696,skolem0006),inference(resolution,[status(thm)],[c458, reflexivity])).
% 2.44/2.63 cnf(c271,plain,nonexistent(skolem0001,skolem0007),inference(resolution,[status(thm)],[c269, c156])).
% 2.44/2.63 cnf(c450,plain,skolem0001!=X690|skolem0007!=X689|nonexistent(X690,X689),inference(resolution,[status(thm)],[c33, c271])).
% 2.44/2.63 cnf(c797,plain,skolem0001!=X691|nonexistent(X691,skolem0007),inference(resolution,[status(thm)],[c450, reflexivity])).
% 2.44/2.63 cnf(c281,plain,nonexistent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c279, c156])).
% 2.44/2.63 cnf(c447,plain,skolem0001!=X685|skolem0006!=X684|nonexistent(X685,X684),inference(resolution,[status(thm)],[c33, c281])).
% 2.44/2.63 cnf(c794,plain,skolem0001!=X688|nonexistent(X688,skolem0006),inference(resolution,[status(thm)],[c447, reflexivity])).
% 2.44/2.63 cnf(c264,plain,nonexistent(skolem0001,skolem0008),inference(resolution,[status(thm)],[c156, c260])).
% 2.44/2.63 cnf(c446,plain,skolem0001!=X682|skolem0008!=X681|nonexistent(X682,X681),inference(resolution,[status(thm)],[c33, c264])).
% 2.44/2.63 cnf(c792,plain,skolem0001!=X683|nonexistent(X683,skolem0008),inference(resolution,[status(thm)],[c446, reflexivity])).
% 2.44/2.63 cnf(c434,plain,skolem0001!=X676|skolem0008!=X677|eventuality(X676,X677),inference(resolution,[status(thm)],[c32, c260])).
% 2.44/2.63 cnf(c789,plain,skolem0001!=X678|eventuality(X678,skolem0008),inference(resolution,[status(thm)],[c434, reflexivity])).
% 2.44/2.63 cnf(c431,plain,skolem0001!=X673|skolem0007!=X674|eventuality(X673,X674),inference(resolution,[status(thm)],[c32, c269])).
% 2.44/2.63 cnf(c787,plain,skolem0001!=X675|eventuality(X675,skolem0007),inference(resolution,[status(thm)],[c431, reflexivity])).
% 2.44/2.63 cnf(c429,plain,skolem0001!=X668|skolem0006!=X669|eventuality(X668,X669),inference(resolution,[status(thm)],[c32, c279])).
% 2.44/2.63 cnf(c784,plain,skolem0001!=X670|eventuality(X670,skolem0006),inference(resolution,[status(thm)],[c429, reflexivity])).
% 2.44/2.63 cnf(c31,axiom,X362!=X364|X361!=X363|~scream(X362,X361)|scream(X364,X363),theory(equality)).
% 2.44/2.63 cnf(c421,plain,skolem0001!=X664|skolem0008!=X663|scream(X664,X663),inference(resolution,[status(thm)],[c31, c73])).
% 2.44/2.63 cnf(c781,plain,skolem0001!=X667|scream(X667,skolem0008),inference(resolution,[status(thm)],[c421, reflexivity])).
% 2.44/2.63 cnf(c30,axiom,X358!=X360|X357!=X359|~cry(X358,X357)|cry(X360,X359),theory(equality)).
% 2.44/2.63 cnf(c415,plain,skolem0001!=X661|skolem0007!=X660|cry(X661,X660),inference(resolution,[status(thm)],[c30, c67])).
% 2.44/2.63 cnf(c779,plain,skolem0001!=X662|cry(X662,skolem0007),inference(resolution,[status(thm)],[c415, reflexivity])).
% 2.44/2.63 cnf(c29,axiom,X354!=X356|X353!=X355|~revenge(X354,X353)|revenge(X356,X355),theory(equality)).
% 2.44/2.63 cnf(c402,plain,skolem0001!=X655|skolem0006!=X656|revenge(X655,X656),inference(resolution,[status(thm)],[c29, c66])).
% 2.44/2.63 cnf(c776,plain,skolem0001!=X657|revenge(X657,skolem0006),inference(resolution,[status(thm)],[c402, reflexivity])).
% 2.44/2.63 cnf(c397,plain,skolem0001!=X652|skolem0006!=X653|act(X652,X653),inference(resolution,[status(thm)],[c28, c277])).
% 2.44/2.63 cnf(c774,plain,skolem0001!=X654|act(X654,skolem0006),inference(resolution,[status(thm)],[c397, reflexivity])).
% 2.44/2.63 cnf(c385,plain,skolem0001!=X648|skolem0006!=X647|action(X648,X647),inference(resolution,[status(thm)],[c27, c276])).
% 2.44/2.63 cnf(c771,plain,skolem0001!=X649|action(X649,skolem0006),inference(resolution,[status(thm)],[c385, reflexivity])).
% 2.44/2.63 cnf(c64,negated_conjecture,group(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.63 fof(ax24,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 2.44/2.63 fof(c178,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 2.44/2.63 fof(c179,plain,(![X75]:(![X76]:(~group(X75,X76)|set(X75,X76)))),inference(variable_rename,[status(thm)],[c178])).
% 2.44/2.63 cnf(c180,plain,~group(X214,X215)|set(X214,X215),inference(split_conjunct,[status(thm)],[c179])).
% 2.44/2.63 cnf(c289,plain,set(skolem0001,skolem0005),inference(resolution,[status(thm)],[c180, c64])).
% 2.44/2.63 fof(ax23,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 2.44/2.63 fof(c181,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 2.44/2.63 fof(c182,plain,(![X77]:(![X78]:(~set(X77,X78)|multiple(X77,X78)))),inference(variable_rename,[status(thm)],[c181])).
% 2.44/2.63 cnf(c183,plain,~set(X220,X221)|multiple(X220,X221),inference(split_conjunct,[status(thm)],[c182])).
% 2.44/2.63 cnf(c290,plain,multiple(skolem0001,skolem0005),inference(resolution,[status(thm)],[c183, c289])).
% 2.44/2.63 cnf(c25,axiom,X338!=X340|X337!=X339|~multiple(X338,X337)|multiple(X340,X339),theory(equality)).
% 2.44/2.63 cnf(c368,plain,skolem0001!=X643|skolem0005!=X642|multiple(X643,X642),inference(resolution,[status(thm)],[c25, c290])).
% 2.44/2.63 cnf(c768,plain,skolem0001!=X646|multiple(X646,skolem0005),inference(resolution,[status(thm)],[c368, reflexivity])).
% 2.44/2.63 cnf(c24,axiom,X334!=X336|X333!=X335|~set(X334,X333)|set(X336,X335),theory(equality)).
% 2.44/2.63 cnf(c361,plain,skolem0001!=X639|skolem0005!=X638|set(X639,X638),inference(resolution,[status(thm)],[c24, c289])).
% 2.44/2.63 cnf(c765,plain,skolem0001!=X641|set(X641,skolem0005),inference(resolution,[status(thm)],[c361, reflexivity])).
% 2.44/2.63 cnf(c23,axiom,X320!=X322|X319!=X321|~group(X320,X319)|group(X322,X321),theory(equality)).
% 2.44/2.63 cnf(c355,plain,skolem0001!=X637|skolem0005!=X636|group(X637,X636),inference(resolution,[status(thm)],[c23, c64])).
% 2.44/2.63 cnf(c764,plain,skolem0001!=X640|group(X640,skolem0005),inference(resolution,[status(thm)],[c355, reflexivity])).
% 2.44/2.63 cnf(c22,axiom,X308!=X310|X307!=X309|~six(X308,X307)|six(X310,X309),theory(equality)).
% 2.44/2.63 cnf(c352,plain,skolem0001!=X633|skolem0005!=X632|six(X633,X632),inference(resolution,[status(thm)],[c22, c63])).
% 2.44/2.63 cnf(c761,plain,skolem0001!=X635|six(X635,skolem0005),inference(resolution,[status(thm)],[c352, reflexivity])).
% 2.44/2.63 cnf(c3,axiom,X159!=X161|X158!=X160|~animate(X159,X158)|animate(X161,X160),theory(equality)).
% 2.44/2.63 fof(ax2,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 2.44/2.63 fof(c244,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 2.44/2.63 fof(c245,plain,(![X119]:(![X120]:(~human_person(X119,X120)|animate(X119,X120)))),inference(variable_rename,[status(thm)],[c244])).
% 2.44/2.63 cnf(c246,plain,~human_person(X302,X303)|animate(X302,X303),inference(split_conjunct,[status(thm)],[c245])).
% 2.44/2.63 cnf(c349,plain,animate(skolem0001,skolem0003),inference(resolution,[status(thm)],[c246, c324])).
% 2.44/2.63 cnf(c350,plain,skolem0001!=X630|skolem0003!=X631|animate(X630,X631),inference(resolution,[status(thm)],[c349, c3])).
% 2.44/2.63 cnf(c760,plain,skolem0001!=X634|animate(X634,skolem0003),inference(resolution,[status(thm)],[c350, reflexivity])).
% 2.44/2.63 cnf(c348,plain,skolem0001!=X627|skolem0008!=X626|event(X627,X626),inference(resolution,[status(thm)],[c21, c68])).
% 2.44/2.63 cnf(c757,plain,skolem0001!=X629|event(X629,skolem0008),inference(resolution,[status(thm)],[c348, reflexivity])).
% 2.44/2.63 cnf(c347,plain,skolem0001!=X625|skolem0006!=X624|event(X625,X624),inference(resolution,[status(thm)],[c21, c278])).
% 2.44/2.63 cnf(c756,plain,skolem0001!=X628|event(X628,skolem0006),inference(resolution,[status(thm)],[c347, reflexivity])).
% 2.44/2.63 cnf(c346,plain,skolem0001!=X621|skolem0007!=X620|event(X621,X620),inference(resolution,[status(thm)],[c21, c268])).
% 2.44/2.63 cnf(c753,plain,skolem0001!=X623|event(X623,skolem0007),inference(resolution,[status(thm)],[c346, reflexivity])).
% 2.44/2.63 cnf(c4,axiom,X167!=X169|X166!=X168|~human(X167,X166)|human(X169,X168),theory(equality)).
% 2.44/2.63 fof(ax3,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 2.44/2.63 fof(c241,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 2.44/2.63 fof(c242,plain,(![X117]:(![X118]:(~human_person(X117,X118)|human(X117,X118)))),inference(variable_rename,[status(thm)],[c241])).
% 2.44/2.63 cnf(c243,plain,~human_person(X296,X297)|human(X296,X297),inference(split_conjunct,[status(thm)],[c242])).
% 2.44/2.63 cnf(c344,plain,human(skolem0001,skolem0003),inference(resolution,[status(thm)],[c243, c324])).
% 2.44/2.63 cnf(c345,plain,skolem0001!=X618|skolem0003!=X619|human(X618,X619),inference(resolution,[status(thm)],[c344, c4])).
% 2.44/2.63 cnf(c752,plain,skolem0001!=X622|human(X622,skolem0003),inference(resolution,[status(thm)],[c345, reflexivity])).
% 2.44/2.63 cnf(c6,axiom,X185!=X187|X184!=X186|~living(X185,X184)|living(X187,X186),theory(equality)).
% 2.44/2.63 fof(ax4,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 2.44/2.63 fof(c238,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 2.44/2.63 fof(c239,plain,(![X115]:(![X116]:(~organism(X115,X116)|living(X115,X116)))),inference(variable_rename,[status(thm)],[c238])).
% 2.44/2.63 cnf(c240,plain,~organism(X295,X294)|living(X295,X294),inference(split_conjunct,[status(thm)],[c239])).
% 2.44/2.63 cnf(c341,plain,living(skolem0001,skolem0003),inference(resolution,[status(thm)],[c240, c327])).
% 2.44/2.63 cnf(c342,plain,skolem0001!=X614|skolem0003!=X615|living(X614,X615),inference(resolution,[status(thm)],[c341, c6])).
% 2.44/2.63 cnf(c749,plain,skolem0001!=X617|living(X617,skolem0003),inference(resolution,[status(thm)],[c342, reflexivity])).
% 2.44/2.63 cnf(c7,axiom,X191!=X193|X190!=X192|~impartial(X191,X190)|impartial(X193,X192),theory(equality)).
% 2.44/2.63 fof(ax5,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 2.44/2.63 fof(c235,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 2.44/2.63 fof(c236,plain,(![X113]:(![X114]:(~organism(X113,X114)|impartial(X113,X114)))),inference(variable_rename,[status(thm)],[c235])).
% 2.44/2.63 cnf(c237,plain,~organism(X289,X288)|impartial(X289,X288),inference(split_conjunct,[status(thm)],[c236])).
% 2.44/2.63 cnf(c339,plain,impartial(skolem0001,skolem0003),inference(resolution,[status(thm)],[c237, c327])).
% 2.44/2.63 cnf(c340,plain,skolem0001!=X613|skolem0003!=X612|impartial(X613,X612),inference(resolution,[status(thm)],[c339, c7])).
% 2.44/2.63 cnf(c748,plain,skolem0001!=X616|impartial(X616,skolem0003),inference(resolution,[status(thm)],[c340, reflexivity])).
% 2.44/2.63 fof(ax13,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 2.44/2.63 fof(c211,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 2.44/2.63 fof(c212,plain,(![X97]:(![X98]:(~entity(X97,X98)|specific(X97,X98)))),inference(variable_rename,[status(thm)],[c211])).
% 2.44/2.63 cnf(c213,plain,~entity(X257,X256)|specific(X257,X256),inference(split_conjunct,[status(thm)],[c212])).
% 2.44/2.63 cnf(c332,plain,specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c329, c213])).
% 2.44/2.63 cnf(c338,plain,skolem0001!=X609|skolem0003!=X608|specific(X609,X608),inference(resolution,[status(thm)],[c332, c13])).
% 2.44/2.63 cnf(c745,plain,skolem0001!=X611|specific(X611,skolem0003),inference(resolution,[status(thm)],[c338, reflexivity])).
% 2.44/2.63 cnf(c12,axiom,X225!=X227|X224!=X226|~existent(X225,X224)|existent(X227,X226),theory(equality)).
% 2.44/2.63 fof(ax12,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 2.44/2.63 fof(c214,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 2.44/2.63 fof(c215,plain,(![X99]:(![X100]:(~entity(X99,X100)|existent(X99,X100)))),inference(variable_rename,[status(thm)],[c214])).
% 2.44/2.63 cnf(c216,plain,~entity(X258,X259)|existent(X258,X259),inference(split_conjunct,[status(thm)],[c215])).
% 2.44/2.63 cnf(c331,plain,existent(skolem0001,skolem0003),inference(resolution,[status(thm)],[c329, c216])).
% 2.44/2.63 cnf(c337,plain,skolem0001!=X607|skolem0003!=X606|existent(X607,X606),inference(resolution,[status(thm)],[c331, c12])).
% 2.44/2.63 cnf(c744,plain,skolem0001!=X610|existent(X610,skolem0003),inference(resolution,[status(thm)],[c337, reflexivity])).
% 2.44/2.63 cnf(c19,axiom,X285!=X287|X284!=X286|~cannon(X285,X284)|cannon(X287,X286),theory(equality)).
% 2.44/2.63 cnf(c336,plain,skolem0001!=X603|skolem0004!=X602|cannon(X603,X602),inference(resolution,[status(thm)],[c19, c55])).
% 2.44/2.63 cnf(c741,plain,skolem0001!=X605|cannon(X605,skolem0004),inference(resolution,[status(thm)],[c336, reflexivity])).
% 2.44/2.63 cnf(c334,plain,skolem0001!=X601|skolem0003!=X600|thing(X601,X600),inference(resolution,[status(thm)],[c330, c14])).
% 2.44/2.63 cnf(c740,plain,skolem0001!=X604|thing(X604,skolem0003),inference(resolution,[status(thm)],[c334, reflexivity])).
% 2.44/2.63 cnf(c8,axiom,X195!=X197|X194!=X196|~entity(X195,X194)|entity(X197,X196),theory(equality)).
% 2.44/2.63 cnf(c333,plain,skolem0001!=X597|skolem0003!=X596|entity(X597,X596),inference(resolution,[status(thm)],[c329, c8])).
% 2.44/2.63 cnf(c737,plain,skolem0001!=X599|entity(X599,skolem0003),inference(resolution,[status(thm)],[c333, reflexivity])).
% 2.44/2.63 cnf(c5,axiom,X177!=X179|X176!=X178|~organism(X177,X176)|organism(X179,X178),theory(equality)).
% 2.44/2.63 cnf(c328,plain,skolem0001!=X595|skolem0003!=X594|organism(X595,X594),inference(resolution,[status(thm)],[c327, c5])).
% 2.44/2.63 cnf(c736,plain,skolem0001!=X598|organism(X598,skolem0003),inference(resolution,[status(thm)],[c328, reflexivity])).
% 2.44/2.63 cnf(c18,axiom,X277!=X279|X276!=X278|~weapon(X277,X276)|weapon(X279,X278),theory(equality)).
% 2.44/2.63 cnf(c326,plain,skolem0001!=X590|skolem0004!=X591|weapon(X590,X591),inference(resolution,[status(thm)],[c18, c293])).
% 2.44/2.63 cnf(c733,plain,skolem0001!=X593|weapon(X593,skolem0004),inference(resolution,[status(thm)],[c326, reflexivity])).
% 2.44/2.63 cnf(c2,axiom,X147!=X149|X146!=X148|~human_person(X147,X146)|human_person(X149,X148),theory(equality)).
% 2.44/2.63 cnf(c325,plain,skolem0001!=X588|skolem0003!=X589|human_person(X588,X589),inference(resolution,[status(thm)],[c324, c2])).
% 2.44/2.63 cnf(c732,plain,skolem0001!=X592|human_person(X592,skolem0003),inference(resolution,[status(thm)],[c325, reflexivity])).
% 2.44/2.63 fof(ax9,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 2.44/2.63 fof(c223,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 2.44/2.63 fof(c224,plain,(![X105]:(![X106]:(~object(X105,X106)|unisex(X105,X106)))),inference(variable_rename,[status(thm)],[c223])).
% 2.44/2.63 cnf(c225,plain,~object(X272,X273)|unisex(X272,X273),inference(split_conjunct,[status(thm)],[c224])).
% 2.44/2.63 cnf(c322,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c225, c303])).
% 2.44/2.63 cnf(c323,plain,skolem0001!=X584|skolem0004!=X585|unisex(X584,X585),inference(resolution,[status(thm)],[c322, c10])).
% 2.44/2.63 cnf(c729,plain,skolem0001!=X587|unisex(X587,skolem0004),inference(resolution,[status(thm)],[c323, reflexivity])).
% 2.44/2.63 fof(ax10,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 2.44/2.63 fof(c220,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 2.44/2.63 fof(c221,plain,(![X103]:(![X104]:(~object(X103,X104)|impartial(X103,X104)))),inference(variable_rename,[status(thm)],[c220])).
% 2.44/2.63 cnf(c222,plain,~object(X266,X267)|impartial(X266,X267),inference(split_conjunct,[status(thm)],[c221])).
% 2.44/2.63 cnf(c319,plain,impartial(skolem0001,skolem0004),inference(resolution,[status(thm)],[c222, c303])).
% 2.44/2.63 cnf(c321,plain,skolem0001!=X583|skolem0004!=X582|impartial(X583,X582),inference(resolution,[status(thm)],[c319, c7])).
% 2.44/2.63 cnf(c728,plain,skolem0001!=X586|impartial(X586,skolem0004),inference(resolution,[status(thm)],[c321, reflexivity])).
% 2.44/2.63 cnf(c17,axiom,X269!=X271|X268!=X270|~weaponry(X269,X268)|weaponry(X271,X270),theory(equality)).
% 2.44/2.63 cnf(c320,plain,skolem0001!=X578|skolem0004!=X579|weaponry(X578,X579),inference(resolution,[status(thm)],[c17, c294])).
% 2.44/2.63 cnf(c725,plain,skolem0001!=X581|weaponry(X581,skolem0004),inference(resolution,[status(thm)],[c320, reflexivity])).
% 2.44/2.63 cnf(c11,axiom,X217!=X219|X216!=X218|~nonliving(X217,X216)|nonliving(X219,X218),theory(equality)).
% 2.44/2.63 fof(ax11,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 2.44/2.63 fof(c217,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 2.44/2.63 fof(c218,plain,(![X101]:(![X102]:(~object(X101,X102)|nonliving(X101,X102)))),inference(variable_rename,[status(thm)],[c217])).
% 2.44/2.63 cnf(c219,plain,~object(X264,X265)|nonliving(X264,X265),inference(split_conjunct,[status(thm)],[c218])).
% 2.44/2.63 cnf(c316,plain,nonliving(skolem0001,skolem0004),inference(resolution,[status(thm)],[c219, c303])).
% 2.44/2.63 cnf(c318,plain,skolem0001!=X576|skolem0004!=X577|nonliving(X576,X577),inference(resolution,[status(thm)],[c316, c11])).
% 2.44/2.63 cnf(c724,plain,skolem0001!=X580|nonliving(X580,skolem0004),inference(resolution,[status(thm)],[c318, reflexivity])).
% 2.44/2.63 cnf(c313,plain,existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c216, c305])).
% 2.44/2.63 cnf(c315,plain,skolem0001!=X573|skolem0004!=X572|existent(X573,X572),inference(resolution,[status(thm)],[c313, c12])).
% 2.44/2.63 cnf(c721,plain,skolem0001!=X575|existent(X575,skolem0004),inference(resolution,[status(thm)],[c315, reflexivity])).
% 2.44/2.63 cnf(c16,axiom,X261!=X263|X260!=X262|~instrumentality(X261,X260)|instrumentality(X263,X262),theory(equality)).
% 2.44/2.63 cnf(c314,plain,skolem0001!=X570|skolem0004!=X571|instrumentality(X570,X571),inference(resolution,[status(thm)],[c16, c298])).
% 2.44/2.63 cnf(c720,plain,skolem0001!=X574|instrumentality(X574,skolem0004),inference(resolution,[status(thm)],[c314, reflexivity])).
% 2.44/2.63 cnf(c311,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c213, c305])).
% 2.44/2.63 cnf(c312,plain,skolem0001!=X567|skolem0004!=X566|specific(X567,X566),inference(resolution,[status(thm)],[c311, c13])).
% 2.44/2.63 cnf(c717,plain,skolem0001!=X569|specific(X569,skolem0004),inference(resolution,[status(thm)],[c312, reflexivity])).
% 2.44/2.63 cnf(c309,plain,skolem0001!=X565|skolem0004!=X564|thing(X565,X564),inference(resolution,[status(thm)],[c307, c14])).
% 2.44/2.63 cnf(c716,plain,skolem0001!=X568|thing(X568,skolem0004),inference(resolution,[status(thm)],[c309, reflexivity])).
% 2.44/2.63 cnf(c15,axiom,X253!=X255|X252!=X254|~artifact(X253,X252)|artifact(X255,X254),theory(equality)).
% 2.44/2.63 cnf(c308,plain,skolem0001!=X560|skolem0004!=X561|artifact(X560,X561),inference(resolution,[status(thm)],[c15, c299])).
% 2.44/2.63 cnf(c713,plain,skolem0001!=X563|artifact(X563,skolem0004),inference(resolution,[status(thm)],[c308, reflexivity])).
% 2.44/2.63 cnf(c306,plain,skolem0001!=X559|skolem0004!=X558|entity(X559,X558),inference(resolution,[status(thm)],[c305, c8])).
% 2.44/2.63 cnf(c712,plain,skolem0001!=X562|entity(X562,skolem0004),inference(resolution,[status(thm)],[c306, reflexivity])).
% 2.44/2.63 cnf(c9,axiom,X205!=X207|X204!=X206|~object(X205,X204)|object(X207,X206),theory(equality)).
% 2.44/2.63 cnf(c304,plain,skolem0001!=X556|skolem0004!=X555|object(X556,X555),inference(resolution,[status(thm)],[c303, c9])).
% 2.44/2.63 cnf(c710,plain,skolem0001!=X557|object(X557,skolem0004),inference(resolution,[status(thm)],[c304, reflexivity])).
% 2.44/2.63 cnf(c115,plain,~member(X554,X551,X549)|~member(X554,X553,X549)|X553=X551|~member(X554,X550,X549)|X550=X553|X550=X551|~member(X554,X547,X549)|X547=X550|X547=X553|X547=X551|~member(X554,X552,X549)|X552=X547|X552=X550|X552=X553|X552=X551|~member(X554,X548,X549)|X548=X552|X548=X547|X548=X550|X548=X553|X548=X551|skolem0016(X554,X549,X551,X553,X550,X547,X552,X548)!=X551|six(X554,X549),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c302,plain,skolem0001!=X545|skolem0007!=X544|thing(X545,X544),inference(resolution,[status(thm)],[c14, c272])).
% 2.44/2.63 cnf(c708,plain,skolem0001!=X546|thing(X546,skolem0007),inference(resolution,[status(thm)],[c302, reflexivity])).
% 2.44/2.63 cnf(c301,plain,skolem0001!=X542|skolem0006!=X541|thing(X542,X541),inference(resolution,[status(thm)],[c14, c282])).
% 2.44/2.63 cnf(c706,plain,skolem0001!=X543|thing(X543,skolem0006),inference(resolution,[status(thm)],[c301, reflexivity])).
% 2.44/2.63 cnf(c114,plain,~member(X540,X537,X535)|~member(X540,X539,X535)|X539=X537|~member(X540,X536,X535)|X536=X539|X536=X537|~member(X540,X533,X535)|X533=X536|X533=X539|X533=X537|~member(X540,X538,X535)|X538=X533|X538=X536|X538=X539|X538=X537|~member(X540,X534,X535)|X534=X538|X534=X533|X534=X536|X534=X539|X534=X537|skolem0016(X540,X535,X537,X539,X536,X533,X538,X534)!=X539|six(X540,X535),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c300,plain,skolem0001!=X531|skolem0008!=X530|thing(X531,X530),inference(resolution,[status(thm)],[c14, c261])).
% 2.44/2.63 cnf(c704,plain,skolem0001!=X532|thing(X532,skolem0008),inference(resolution,[status(thm)],[c300, reflexivity])).
% 2.44/2.63 cnf(c280,plain,specific(skolem0001,skolem0006),inference(resolution,[status(thm)],[c279, c153])).
% 2.44/2.63 cnf(c297,plain,skolem0001!=X520|skolem0006!=X519|specific(X520,X519),inference(resolution,[status(thm)],[c13, c280])).
% 2.44/2.63 cnf(c702,plain,skolem0001!=X529|specific(X529,skolem0006),inference(resolution,[status(thm)],[c297, reflexivity])).
% 2.44/2.63 cnf(c113,plain,~member(X528,X525,X523)|~member(X528,X527,X523)|X527=X525|~member(X528,X524,X523)|X524=X527|X524=X525|~member(X528,X521,X523)|X521=X524|X521=X527|X521=X525|~member(X528,X526,X523)|X526=X521|X526=X524|X526=X527|X526=X525|~member(X528,X522,X523)|X522=X526|X522=X521|X522=X524|X522=X527|X522=X525|skolem0016(X528,X523,X525,X527,X524,X521,X526,X522)!=X524|six(X528,X523),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c270,plain,specific(skolem0001,skolem0007),inference(resolution,[status(thm)],[c269, c153])).
% 2.44/2.63 cnf(c296,plain,skolem0001!=X517|skolem0007!=X516|specific(X517,X516),inference(resolution,[status(thm)],[c13, c270])).
% 2.44/2.63 cnf(c700,plain,skolem0001!=X518|specific(X518,skolem0007),inference(resolution,[status(thm)],[c296, reflexivity])).
% 2.44/2.63 cnf(c112,plain,~member(X515,X512,X510)|~member(X515,X514,X510)|X514=X512|~member(X515,X511,X510)|X511=X514|X511=X512|~member(X515,X508,X510)|X508=X511|X508=X514|X508=X512|~member(X515,X513,X510)|X513=X508|X513=X511|X513=X514|X513=X512|~member(X515,X509,X510)|X509=X513|X509=X508|X509=X511|X509=X514|X509=X512|skolem0016(X515,X510,X512,X514,X511,X508,X513,X509)!=X508|six(X515,X510),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c263,plain,specific(skolem0001,skolem0008),inference(resolution,[status(thm)],[c153, c260])).
% 2.44/2.63 cnf(c295,plain,skolem0001!=X506|skolem0008!=X505|specific(X506,X505),inference(resolution,[status(thm)],[c13, c263])).
% 2.44/2.63 cnf(c698,plain,skolem0001!=X507|specific(X507,skolem0008),inference(resolution,[status(thm)],[c295, reflexivity])).
% 2.44/2.63 cnf(c283,plain,unisex(skolem0001,skolem0006),inference(resolution,[status(thm)],[c279, c159])).
% 2.44/2.63 cnf(c288,plain,skolem0001!=X502|skolem0006!=X503|unisex(X502,X503),inference(resolution,[status(thm)],[c283, c10])).
% 2.44/2.63 cnf(c696,plain,skolem0001!=X504|unisex(X504,skolem0006),inference(resolution,[status(thm)],[c288, reflexivity])).
% 2.44/2.63 cnf(c111,plain,~member(X501,X498,X496)|~member(X501,X500,X496)|X500=X498|~member(X501,X497,X496)|X497=X500|X497=X498|~member(X501,X494,X496)|X494=X497|X494=X500|X494=X498|~member(X501,X499,X496)|X499=X494|X499=X497|X499=X500|X499=X498|~member(X501,X495,X496)|X495=X499|X495=X494|X495=X497|X495=X500|X495=X498|skolem0016(X501,X496,X498,X500,X497,X494,X499,X495)!=X499|six(X501,X496),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c273,plain,unisex(skolem0001,skolem0007),inference(resolution,[status(thm)],[c269, c159])).
% 2.44/2.63 cnf(c287,plain,skolem0001!=X491|skolem0007!=X492|unisex(X491,X492),inference(resolution,[status(thm)],[c10, c273])).
% 2.44/2.63 cnf(c694,plain,skolem0001!=X493|unisex(X493,skolem0007),inference(resolution,[status(thm)],[c287, reflexivity])).
% 2.44/2.63 cnf(c266,plain,unisex(skolem0001,skolem0008),inference(resolution,[status(thm)],[c159, c260])).
% 2.44/2.63 cnf(c286,plain,skolem0001!=X480|skolem0008!=X481|unisex(X480,X481),inference(resolution,[status(thm)],[c10, c266])).
% 2.44/2.63 cnf(c692,plain,skolem0001!=X490|unisex(X490,skolem0008),inference(resolution,[status(thm)],[c286, reflexivity])).
% 2.44/2.63 cnf(c110,plain,~member(X489,X486,X484)|~member(X489,X488,X484)|X488=X486|~member(X489,X485,X484)|X485=X488|X485=X486|~member(X489,X482,X484)|X482=X485|X482=X488|X482=X486|~member(X489,X487,X484)|X487=X482|X487=X485|X487=X488|X487=X486|~member(X489,X483,X484)|X483=X487|X483=X482|X483=X485|X483=X488|X483=X486|skolem0016(X489,X484,X486,X488,X485,X482,X487,X483)!=X483|six(X489,X484),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c51,negated_conjecture,male(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.63 cnf(c1,axiom,X137!=X139|X136!=X138|~male(X137,X136)|male(X139,X138),theory(equality)).
% 2.44/2.63 cnf(c255,plain,skolem0001!=X478|skolem0002!=X477|male(X478,X477),inference(resolution,[status(thm)],[c1, c51])).
% 2.44/2.63 cnf(c690,plain,skolem0001!=X479|male(X479,skolem0002),inference(resolution,[status(thm)],[c255, reflexivity])).
% 2.44/2.63 cnf(c109,plain,~member(X476,X473,X471)|~member(X476,X475,X471)|X475=X473|~member(X476,X472,X471)|X472=X475|X472=X473|~member(X476,X469,X471)|X469=X472|X469=X475|X469=X473|~member(X476,X474,X471)|X474=X469|X474=X472|X474=X475|X474=X473|~member(X476,X470,X471)|X470=X474|X470=X469|X470=X472|X470=X475|X470=X473|member(X476,skolem0016(X476,X471,X473,X475,X472,X469,X474,X470),X471)|six(X476,X471),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c52,negated_conjecture,male(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.63 cnf(c254,plain,skolem0001!=X467|skolem0003!=X466|male(X467,X466),inference(resolution,[status(thm)],[c1, c52])).
% 2.44/2.63 cnf(c677,plain,skolem0001!=X468|male(X468,skolem0003),inference(resolution,[status(thm)],[c254, reflexivity])).
% 2.44/2.63 cnf(c0,axiom,X133!=X135|X132!=X134|~man(X133,X132)|man(X135,X134),theory(equality)).
% 2.44/2.63 cnf(c253,plain,skolem0001!=X463|skolem0003!=X464|man(X463,X464),inference(resolution,[status(thm)],[c0, c53])).
% 2.44/2.63 cnf(c675,plain,skolem0001!=X465|man(X465,skolem0003),inference(resolution,[status(thm)],[c253, reflexivity])).
% 2.44/2.63 cnf(c108,plain,~six(X460,X461)|~member(X460,X462,X461)|X462=skolem0015(X460,X461)|X462=skolem0014(X460,X461)|X462=skolem0013(X460,X461)|X462=skolem0012(X460,X461)|X462=skolem0011(X460,X461)|X462=skolem0010(X460,X461),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c107,plain,~six(X458,X459)|skolem0015(X458,X459)!=skolem0010(X458,X459),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c106,plain,~six(X456,X457)|skolem0015(X456,X457)!=skolem0011(X456,X457),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c105,plain,~six(X454,X455)|skolem0015(X454,X455)!=skolem0012(X454,X455),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c104,plain,~six(X452,X453)|skolem0015(X452,X453)!=skolem0013(X452,X453),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c103,plain,~six(X450,X451)|skolem0015(X450,X451)!=skolem0014(X450,X451),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c101,plain,~six(X448,X449)|skolem0014(X448,X449)!=skolem0010(X448,X449),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c100,plain,~six(X446,X447)|skolem0014(X446,X447)!=skolem0011(X446,X447),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c99,plain,~six(X444,X445)|skolem0014(X444,X445)!=skolem0012(X444,X445),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c98,plain,~six(X442,X443)|skolem0014(X442,X443)!=skolem0013(X442,X443),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c96,plain,~six(X440,X441)|skolem0013(X440,X441)!=skolem0010(X440,X441),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c95,plain,~six(X438,X439)|skolem0013(X438,X439)!=skolem0011(X438,X439),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c94,plain,~six(X436,X437)|skolem0013(X436,X437)!=skolem0012(X436,X437),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c92,plain,~six(X434,X435)|skolem0012(X434,X435)!=skolem0010(X434,X435),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c91,plain,~six(X432,X433)|skolem0012(X432,X433)!=skolem0011(X432,X433),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 cnf(c89,plain,~six(X430,X431)|skolem0011(X430,X431)!=skolem0010(X430,X431),inference(split_conjunct,[status(thm)],[c86])).
% 2.44/2.63 fof(ax40,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 2.44/2.63 fof(c128,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax40])).
% 2.44/2.63 fof(c129,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c128])).
% 2.44/2.63 fof(c130,plain,(![X43]:(![X44]:(~existent(X43,X44)|~nonexistent(X43,X44)))),inference(variable_rename,[status(thm)],[c129])).
% 2.44/2.63 cnf(c131,plain,~existent(X150,X151)|~nonexistent(X150,X151),inference(split_conjunct,[status(thm)],[c130])).
% 2.44/2.63 cnf(c619,plain,~existent(skolem0001,skolem0009(skolem0011(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c563, c131])).
% 2.44/2.63 cnf(c607,plain,~existent(skolem0001,skolem0009(skolem0015(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c558, c131])).
% 2.44/2.63 cnf(c601,plain,~existent(skolem0001,skolem0009(skolem0012(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c553, c131])).
% 2.44/2.63 cnf(c589,plain,~existent(skolem0001,skolem0009(skolem0010(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c548, c131])).
% 2.44/2.63 cnf(c577,plain,~existent(skolem0001,skolem0009(skolem0014(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c543, c131])).
% 2.44/2.63 cnf(c571,plain,~existent(skolem0001,skolem0009(skolem0013(skolem0001,skolem0005))),inference(resolution,[status(thm)],[c536, c131])).
% 2.44/2.63 cnf(c511,plain,~existent(skolem0001,skolem0015(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c504, c131])).
% 2.44/2.63 cnf(c483,plain,~existent(skolem0001,skolem0014(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c475, c131])).
% 2.44/2.63 cnf(c453,plain,~existent(skolem0001,skolem0013(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c440, c131])).
% 2.44/2.63 cnf(c417,plain,~existent(skolem0001,skolem0012(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c412, c131])).
% 2.44/2.63 cnf(c394,plain,~existent(skolem0001,skolem0011(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c390, c131])).
% 2.44/2.63 cnf(c374,plain,~existent(skolem0001,skolem0010(skolem0001,skolem0005)),inference(resolution,[status(thm)],[c370, c131])).
% 2.44/2.63 cnf(c40,axiom,X313!=X314|~actual_world(X313)|actual_world(X314),theory(equality)).
% 2.44/2.63 fof(ax1,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 2.44/2.63 fof(c247,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 2.44/2.63 fof(c248,plain,(![X121]:(![X122]:(~man(X121,X122)|male(X121,X122)))),inference(variable_rename,[status(thm)],[c247])).
% 2.44/2.63 cnf(c249,plain,~man(X305,X304)|male(X305,X304),inference(split_conjunct,[status(thm)],[c248])).
% 2.44/2.63 fof(ax41,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 2.44/2.63 fof(c124,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax41])).
% 2.44/2.63 fof(c125,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c124])).
% 2.44/2.63 fof(c126,plain,(![X41]:(![X42]:(~nonliving(X41,X42)|~living(X41,X42)))),inference(variable_rename,[status(thm)],[c125])).
% 2.44/2.63 cnf(c127,plain,~nonliving(X145,X144)|~living(X145,X144),inference(split_conjunct,[status(thm)],[c126])).
% 2.44/2.63 cnf(c343,plain,~nonliving(skolem0001,skolem0003),inference(resolution,[status(thm)],[c341, c127])).
% 2.44/2.63 fof(ax39,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 2.44/2.63 fof(c132,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax39])).
% 2.44/2.63 fof(c133,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c132])).
% 2.44/2.63 fof(c134,plain,(![X45]:(![X46]:(~animate(X45,X46)|~nonliving(X45,X46)))),inference(variable_rename,[status(thm)],[c133])).
% 2.44/2.63 cnf(c135,plain,~animate(X153,X152)|~nonliving(X153,X152),inference(split_conjunct,[status(thm)],[c134])).
% 2.44/2.63 cnf(c317,plain,~animate(skolem0001,skolem0004),inference(resolution,[status(thm)],[c316, c135])).
% 2.44/2.63 fof(ax21,axiom,(![U]:(![V]:(fire(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 2.44/2.63 fof(c187,plain,(![U]:(![V]:(~fire(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 2.44/2.63 fof(c188,plain,(![X81]:(![X82]:(~fire(X81,X82)|event(X81,X82)))),inference(variable_rename,[status(thm)],[c187])).
% 2.44/2.63 cnf(c189,plain,~fire(X228,X229)|event(X228,X229),inference(split_conjunct,[status(thm)],[c188])).
% 2.44/2.63 fof(ax22,axiom,(![U]:(![V]:(six(U,V)=>group(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 2.44/2.63 fof(c184,plain,(![U]:(![V]:(~six(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 2.44/2.63 fof(c185,plain,(![X79]:(![X80]:(~six(X79,X80)|group(X79,X80)))),inference(variable_rename,[status(thm)],[c184])).
% 2.44/2.63 cnf(c186,plain,~six(X223,X222)|group(X223,X222),inference(split_conjunct,[status(thm)],[c185])).
% 2.44/2.63 fof(ax42,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 2.44/2.63 fof(c120,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax42])).
% 2.44/2.63 fof(c121,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c120])).
% 2.44/2.63 fof(c122,plain,(![X39]:(![X40]:(~singleton(X39,X40)|~multiple(X39,X40)))),inference(variable_rename,[status(thm)],[c121])).
% 2.44/2.63 cnf(c123,plain,~singleton(X142,X143)|~multiple(X142,X143),inference(split_conjunct,[status(thm)],[c122])).
% 2.44/2.63 cnf(c291,plain,~singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c290, c123])).
% 2.44/2.63 cnf(c284,plain,~existent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c281, c131])).
% 2.44/2.63 cnf(c274,plain,~existent(skolem0001,skolem0007),inference(resolution,[status(thm)],[c271, c131])).
% 2.44/2.63 fof(ax30,axiom,(![U]:(![V]:(scream(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 2.44/2.63 fof(c160,plain,(![U]:(![V]:(~scream(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 2.44/2.63 fof(c161,plain,(![X63]:(![X64]:(~scream(X63,X64)|event(X63,X64)))),inference(variable_rename,[status(thm)],[c160])).
% 2.44/2.63 cnf(c162,plain,~scream(X183,X182)|event(X183,X182),inference(split_conjunct,[status(thm)],[c161])).
% 2.44/2.63 cnf(c265,plain,~existent(skolem0001,skolem0008),inference(resolution,[status(thm)],[c264, c131])).
% 2.44/2.63 fof(ax37,axiom,(![U]:(![V]:(sound(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 2.44/2.63 fof(c139,plain,(![U]:(![V]:(~sound(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax37])).
% 2.44/2.63 fof(c140,plain,(![X49]:(![X50]:(~sound(X49,X50)|event(X49,X50)))),inference(variable_rename,[status(thm)],[c139])).
% 2.44/2.63 cnf(c141,plain,~sound(X157,X156)|event(X157,X156),inference(split_conjunct,[status(thm)],[c140])).
% 2.44/2.63 fof(ax43,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax43)).
% 2.44/2.63 fof(c116,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax43])).
% 2.44/2.63 fof(c117,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c116])).
% 2.44/2.63 fof(c118,plain,(![X37]:(![X38]:(~unisex(X37,X38)|~male(X37,X38)))),inference(variable_rename,[status(thm)],[c117])).
% 2.44/2.63 cnf(c119,plain,~unisex(X140,X141)|~male(X140,X141),inference(split_conjunct,[status(thm)],[c118])).
% 2.44/2.63 cnf(c257,plain,~unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c119, c51])).
% 2.44/2.63 cnf(c256,plain,~unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c119, c52])).
% 2.44/2.63 cnf(transitivity,axiom,X130!=X131|X131!=X129|X130=X129,theory(equality)).
% 2.44/2.63 cnf(symmetry,axiom,X126!=X127|X127=X126,theory(equality)).
% 2.44/2.63 fof(ax45,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax45)).
% 2.44/2.63 fof(c78,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax45])).
% 2.44/2.63 fof(c79,plain,(![X17]:(![X18]:~member(X17,X18,X18))),inference(variable_rename,[status(thm)],[c78])).
% 2.44/2.63 cnf(c80,plain,~member(X125,X124,X124),inference(split_conjunct,[status(thm)],[c79])).
% 2.44/2.63 cnf(c50,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c49])).
% 2.44/2.63 % SZS output end Saturation
% 2.44/2.63
% 2.44/2.63 % Initial clauses : 146
% 2.44/2.63 % Processed clauses : 825
% 2.44/2.63 % Factors computed : 6
% 2.44/2.63 % Resolvents computed: 913
% 2.44/2.63 % Tautologies deleted: 3
% 2.44/2.63 % Forward subsumed : 237
% 2.44/2.63 % Backward subsumed : 6
% 2.44/2.63 % -------- CPU Time ---------
% 2.44/2.63 % User time : 2.261 s
% 2.44/2.63 % System time : 0.022 s
% 2.44/2.63 % Total time : 2.283 s
%------------------------------------------------------------------------------