PyRes---1.5.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : NLP087+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n026.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:59 EDT 2024

% Result   : CounterSatisfiable 2.24s 2.48s
% Output   : Saturation 2.35s
% Verified : 
% SZS Type : -

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