PyRes---1.5.CSA-Sat.s

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

% Computer : n024.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:48 EDT 2024

% Result   : CounterSatisfiable 1.29s 1.53s
% Output   : Saturation 1.32s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.18  % Problem  : NLP049+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.18  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.40  % Computer : n024.cluster.edu
% 0.13/0.40  % Model    : x86_64 x86_64
% 0.13/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40  % Memory   : 8042.1875MB
% 0.13/0.40  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.40  % CPULimit : 300
% 0.13/0.40  % WCLimit  : 300
% 0.13/0.40  % DateTime : Wed May  8 13:28:08 EDT 2024
% 0.13/0.40  % CPUTime  : 
% 1.29/1.53  % Version:  1.5
% 1.29/1.53  % SZS status CounterSatisfiable
% 1.29/1.53  % SZS output start Saturation
% 1.29/1.53  fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((((nonhuman(U,V)&of(U,X,W))&woman(U,W))&mia_forename(U,X))&forename(U,X))&shake_beverage(U,Y))&event(U,Z))&agent(U,Z,W))&patient(U,Z,Y))&past(U,Z))&nonreflexive(U,Z))&order(U,Z))&(![X2]:(member(U,X2,X1)=>(?[X3]:(((((event(U,X3)&agent(U,X3,V))&patient(U,X3,X2))&present(U,X3))&nonreflexive(U,X3))&cost(U,X3))))))&five(U,X1))&group(U,X1))&(![X4]:(member(U,X4,X1)=>dollar(U,X4))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 1.29/1.53  fof(c49,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((((nonhuman(U,V)&of(U,X,W))&woman(U,W))&mia_forename(U,X))&forename(U,X))&shake_beverage(U,Y))&event(U,Z))&agent(U,Z,W))&patient(U,Z,Y))&past(U,Z))&nonreflexive(U,Z))&order(U,Z))&(![X2]:(member(U,X2,X1)=>(?[X3]:(((((event(U,X3)&agent(U,X3,V))&patient(U,X3,X2))&present(U,X3))&nonreflexive(U,X3))&cost(U,X3))))))&five(U,X1))&group(U,X1))&(![X4]:(member(U,X4,X1)=>dollar(U,X4)))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 1.29/1.53  fof(c50,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((((nonhuman(U,V)&of(U,X,W))&woman(U,W))&mia_forename(U,X))&forename(U,X))&shake_beverage(U,Y))&event(U,Z))&agent(U,Z,W))&patient(U,Z,Y))&past(U,Z))&nonreflexive(U,Z))&order(U,Z))&(![X2]:(~member(U,X2,X1)|(?[X3]:(((((event(U,X3)&agent(U,X3,V))&patient(U,X3,X2))&present(U,X3))&nonreflexive(U,X3))&cost(U,X3))))))&five(U,X1))&group(U,X1))&(![X4]:(~member(U,X4,X1)|dollar(U,X4)))))))))))),inference(fof_nnf,[status(thm)],[c49])).
% 1.29/1.53  fof(c51,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((((((((((nonhuman(X2,X3)&of(X2,X5,X4))&woman(X2,X4))&mia_forename(X2,X5))&forename(X2,X5))&shake_beverage(X2,X6))&event(X2,X7))&agent(X2,X7,X4))&patient(X2,X7,X6))&past(X2,X7))&nonreflexive(X2,X7))&order(X2,X7))&(![X9]:(~member(X2,X9,X8)|(?[X10]:(((((event(X2,X10)&agent(X2,X10,X3))&patient(X2,X10,X9))&present(X2,X10))&nonreflexive(X2,X10))&cost(X2,X10))))))&five(X2,X8))&group(X2,X8))&(![X11]:(~member(X2,X11,X8)|dollar(X2,X11)))))))))))),inference(variable_rename,[status(thm)],[c50])).
% 1.29/1.53  fof(c53,negated_conjecture,(![X9]:(![X11]:(actual_world(skolem0001)&(((((((((((((((nonhuman(skolem0001,skolem0002)&of(skolem0001,skolem0004,skolem0003))&woman(skolem0001,skolem0003))&mia_forename(skolem0001,skolem0004))&forename(skolem0001,skolem0004))&shake_beverage(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0003))&patient(skolem0001,skolem0006,skolem0005))&past(skolem0001,skolem0006))&nonreflexive(skolem0001,skolem0006))&order(skolem0001,skolem0006))&(~member(skolem0001,X9,skolem0007)|(((((event(skolem0001,skolem0008(X9))&agent(skolem0001,skolem0008(X9),skolem0002))&patient(skolem0001,skolem0008(X9),X9))&present(skolem0001,skolem0008(X9)))&nonreflexive(skolem0001,skolem0008(X9)))&cost(skolem0001,skolem0008(X9)))))&five(skolem0001,skolem0007))&group(skolem0001,skolem0007))&(~member(skolem0001,X11,skolem0007)|dollar(skolem0001,X11)))))),inference(shift_quantors,[status(thm)],[fof(c52,negated_conjecture,(actual_world(skolem0001)&(((((((((((((((nonhuman(skolem0001,skolem0002)&of(skolem0001,skolem0004,skolem0003))&woman(skolem0001,skolem0003))&mia_forename(skolem0001,skolem0004))&forename(skolem0001,skolem0004))&shake_beverage(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0003))&patient(skolem0001,skolem0006,skolem0005))&past(skolem0001,skolem0006))&nonreflexive(skolem0001,skolem0006))&order(skolem0001,skolem0006))&(![X9]:(~member(skolem0001,X9,skolem0007)|(((((event(skolem0001,skolem0008(X9))&agent(skolem0001,skolem0008(X9),skolem0002))&patient(skolem0001,skolem0008(X9),X9))&present(skolem0001,skolem0008(X9)))&nonreflexive(skolem0001,skolem0008(X9)))&cost(skolem0001,skolem0008(X9))))))&five(skolem0001,skolem0007))&group(skolem0001,skolem0007))&(![X11]:(~member(skolem0001,X11,skolem0007)|dollar(skolem0001,X11))))),inference(skolemize,[status(esa)],[c51])).])).
% 1.29/1.53  fof(c54,negated_conjecture,(![X9]:(![X11]:(actual_world(skolem0001)&(((((((((((((((nonhuman(skolem0001,skolem0002)&of(skolem0001,skolem0004,skolem0003))&woman(skolem0001,skolem0003))&mia_forename(skolem0001,skolem0004))&forename(skolem0001,skolem0004))&shake_beverage(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0003))&patient(skolem0001,skolem0006,skolem0005))&past(skolem0001,skolem0006))&nonreflexive(skolem0001,skolem0006))&order(skolem0001,skolem0006))&((((((~member(skolem0001,X9,skolem0007)|event(skolem0001,skolem0008(X9)))&(~member(skolem0001,X9,skolem0007)|agent(skolem0001,skolem0008(X9),skolem0002)))&(~member(skolem0001,X9,skolem0007)|patient(skolem0001,skolem0008(X9),X9)))&(~member(skolem0001,X9,skolem0007)|present(skolem0001,skolem0008(X9))))&(~member(skolem0001,X9,skolem0007)|nonreflexive(skolem0001,skolem0008(X9))))&(~member(skolem0001,X9,skolem0007)|cost(skolem0001,skolem0008(X9)))))&five(skolem0001,skolem0007))&group(skolem0001,skolem0007))&(~member(skolem0001,X11,skolem0007)|dollar(skolem0001,X11)))))),inference(distribute,[status(thm)],[c53])).
% 1.29/1.53  cnf(c74,negated_conjecture,five(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c54])).
% 1.29/1.53  fof(ax55,axiom,(![U]:(![V]:(five(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)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax55)).
% 1.29/1.53  fof(c80,plain,(![U]:(![V]:((~five(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))))))))))))))&((![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)))))))))))))|five(U,V))))),inference(fof_nnf,[status(thm)],[ax55])).
% 1.29/1.53  fof(c81,plain,((![U]:(![V]:(~five(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))))))))))))))))&(![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)))))))))))))|five(U,V))))),inference(shift_quantors,[status(thm)],[c80])).
% 1.29/1.53  fof(c82,plain,((![X14]:(![X15]:(~five(X14,X15)|(?[X16]:(member(X14,X16,X15)&(?[X17]:((member(X14,X17,X15)&X17!=X16)&(?[X18]:(((member(X14,X18,X15)&X18!=X17)&X18!=X16)&(?[X19]:((((member(X14,X19,X15)&X19!=X18)&X19!=X17)&X19!=X16)&(?[X20]:(((((member(X14,X20,X15)&X20!=X19)&X20!=X18)&X20!=X17)&X20!=X16)&(![X21]:(~member(X14,X21,X15)|((((X21=X20|X21=X19)|X21=X18)|X21=X17)|X21=X16))))))))))))))))&(![X22]:(![X23]:((![X24]:(~member(X22,X24,X23)|(![X25]:((~member(X22,X25,X23)|X25=X24)|(![X26]:(((~member(X22,X26,X23)|X26=X25)|X26=X24)|(![X27]:((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(![X28]:(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|(?[X29]:(member(X22,X29,X23)&((((X29!=X28&X29!=X27)&X29!=X26)&X29!=X25)&X29!=X24)))))))))))))|five(X22,X23))))),inference(variable_rename,[status(thm)],[c81])).
% 1.29/1.53  fof(c84,plain,(![X14]:(![X15]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:((~five(X14,X15)|(member(X14,skolem0009(X14,X15),X15)&((member(X14,skolem0010(X14,X15),X15)&skolem0010(X14,X15)!=skolem0009(X14,X15))&(((member(X14,skolem0011(X14,X15),X15)&skolem0011(X14,X15)!=skolem0010(X14,X15))&skolem0011(X14,X15)!=skolem0009(X14,X15))&((((member(X14,skolem0012(X14,X15),X15)&skolem0012(X14,X15)!=skolem0011(X14,X15))&skolem0012(X14,X15)!=skolem0010(X14,X15))&skolem0012(X14,X15)!=skolem0009(X14,X15))&(((((member(X14,skolem0013(X14,X15),X15)&skolem0013(X14,X15)!=skolem0012(X14,X15))&skolem0013(X14,X15)!=skolem0011(X14,X15))&skolem0013(X14,X15)!=skolem0010(X14,X15))&skolem0013(X14,X15)!=skolem0009(X14,X15))&(~member(X14,X21,X15)|((((X21=skolem0013(X14,X15)|X21=skolem0012(X14,X15))|X21=skolem0011(X14,X15))|X21=skolem0010(X14,X15))|X21=skolem0009(X14,X15)))))))))&((~member(X22,X24,X23)|((~member(X22,X25,X23)|X25=X24)|(((~member(X22,X26,X23)|X26=X25)|X26=X24)|((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|(member(X22,skolem0014(X22,X23,X24,X25,X26,X27,X28),X23)&((((skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X28&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X27)&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X26)&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X25)&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X24)))))))|five(X22,X23))))))))))))),inference(shift_quantors,[status(thm)],[fof(c83,plain,((![X14]:(![X15]:(~five(X14,X15)|(member(X14,skolem0009(X14,X15),X15)&((member(X14,skolem0010(X14,X15),X15)&skolem0010(X14,X15)!=skolem0009(X14,X15))&(((member(X14,skolem0011(X14,X15),X15)&skolem0011(X14,X15)!=skolem0010(X14,X15))&skolem0011(X14,X15)!=skolem0009(X14,X15))&((((member(X14,skolem0012(X14,X15),X15)&skolem0012(X14,X15)!=skolem0011(X14,X15))&skolem0012(X14,X15)!=skolem0010(X14,X15))&skolem0012(X14,X15)!=skolem0009(X14,X15))&(((((member(X14,skolem0013(X14,X15),X15)&skolem0013(X14,X15)!=skolem0012(X14,X15))&skolem0013(X14,X15)!=skolem0011(X14,X15))&skolem0013(X14,X15)!=skolem0010(X14,X15))&skolem0013(X14,X15)!=skolem0009(X14,X15))&(![X21]:(~member(X14,X21,X15)|((((X21=skolem0013(X14,X15)|X21=skolem0012(X14,X15))|X21=skolem0011(X14,X15))|X21=skolem0010(X14,X15))|X21=skolem0009(X14,X15))))))))))))&(![X22]:(![X23]:((![X24]:(~member(X22,X24,X23)|(![X25]:((~member(X22,X25,X23)|X25=X24)|(![X26]:(((~member(X22,X26,X23)|X26=X25)|X26=X24)|(![X27]:((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(![X28]:(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|(member(X22,skolem0014(X22,X23,X24,X25,X26,X27,X28),X23)&((((skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X28&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X27)&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X26)&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X25)&skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X24))))))))))))|five(X22,X23))))),inference(skolemize,[status(esa)],[c82])).])).
% 1.32/1.53  fof(c85,plain,(![X14]:(![X15]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(((~five(X14,X15)|member(X14,skolem0009(X14,X15),X15))&(((~five(X14,X15)|member(X14,skolem0010(X14,X15),X15))&(~five(X14,X15)|skolem0010(X14,X15)!=skolem0009(X14,X15)))&((((~five(X14,X15)|member(X14,skolem0011(X14,X15),X15))&(~five(X14,X15)|skolem0011(X14,X15)!=skolem0010(X14,X15)))&(~five(X14,X15)|skolem0011(X14,X15)!=skolem0009(X14,X15)))&(((((~five(X14,X15)|member(X14,skolem0012(X14,X15),X15))&(~five(X14,X15)|skolem0012(X14,X15)!=skolem0011(X14,X15)))&(~five(X14,X15)|skolem0012(X14,X15)!=skolem0010(X14,X15)))&(~five(X14,X15)|skolem0012(X14,X15)!=skolem0009(X14,X15)))&((((((~five(X14,X15)|member(X14,skolem0013(X14,X15),X15))&(~five(X14,X15)|skolem0013(X14,X15)!=skolem0012(X14,X15)))&(~five(X14,X15)|skolem0013(X14,X15)!=skolem0011(X14,X15)))&(~five(X14,X15)|skolem0013(X14,X15)!=skolem0010(X14,X15)))&(~five(X14,X15)|skolem0013(X14,X15)!=skolem0009(X14,X15)))&(~five(X14,X15)|(~member(X14,X21,X15)|((((X21=skolem0013(X14,X15)|X21=skolem0012(X14,X15))|X21=skolem0011(X14,X15))|X21=skolem0010(X14,X15))|X21=skolem0009(X14,X15)))))))))&(((~member(X22,X24,X23)|((~member(X22,X25,X23)|X25=X24)|(((~member(X22,X26,X23)|X26=X25)|X26=X24)|((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|member(X22,skolem0014(X22,X23,X24,X25,X26,X27,X28),X23))))))|five(X22,X23))&((((((~member(X22,X24,X23)|((~member(X22,X25,X23)|X25=X24)|(((~member(X22,X26,X23)|X26=X25)|X26=X24)|((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X28)))))|five(X22,X23))&((~member(X22,X24,X23)|((~member(X22,X25,X23)|X25=X24)|(((~member(X22,X26,X23)|X26=X25)|X26=X24)|((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X27)))))|five(X22,X23)))&((~member(X22,X24,X23)|((~member(X22,X25,X23)|X25=X24)|(((~member(X22,X26,X23)|X26=X25)|X26=X24)|((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X26)))))|five(X22,X23)))&((~member(X22,X24,X23)|((~member(X22,X25,X23)|X25=X24)|(((~member(X22,X26,X23)|X26=X25)|X26=X24)|((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X25)))))|five(X22,X23)))&((~member(X22,X24,X23)|((~member(X22,X25,X23)|X25=X24)|(((~member(X22,X26,X23)|X26=X25)|X26=X24)|((((~member(X22,X27,X23)|X27=X26)|X27=X25)|X27=X24)|(((((~member(X22,X28,X23)|X28=X27)|X28=X26)|X28=X25)|X28=X24)|skolem0014(X22,X23,X24,X25,X26,X27,X28)!=X24)))))|five(X22,X23))))))))))))))),inference(distribute,[status(thm)],[c84])).
% 1.32/1.53  cnf(c86,plain,~five(X354,X355)|member(X354,skolem0009(X354,X355),X355),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.53  cnf(c369,plain,member(skolem0001,skolem0009(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c86, c74])).
% 1.32/1.53  cnf(c72,negated_conjecture,~member(skolem0001,X462,skolem0007)|nonreflexive(skolem0001,skolem0008(X462)),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.53  cnf(c589,plain,nonreflexive(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c72, c369])).
% 1.32/1.53  cnf(c69,negated_conjecture,~member(skolem0001,X476,skolem0007)|agent(skolem0001,skolem0008(X476),skolem0002),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.53  cnf(c620,plain,agent(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c69, c369])).
% 1.32/1.53  fof(ax54,axiom,(![U]:(![V]:(![W]:(![X]:(((nonreflexive(U,V)&agent(U,V,W))&patient(U,V,X))=>W!=X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax54)).
% 1.32/1.53  fof(c108,plain,(![U]:(![V]:(![W]:(![X]:(((~nonreflexive(U,V)|~agent(U,V,W))|~patient(U,V,X))|W!=X))))),inference(fof_nnf,[status(thm)],[ax54])).
% 1.32/1.53  fof(c109,plain,(![X30]:(![X31]:(![X32]:(![X33]:(((~nonreflexive(X30,X31)|~agent(X30,X31,X32))|~patient(X30,X31,X33))|X32!=X33))))),inference(variable_rename,[status(thm)],[c108])).
% 1.32/1.53  cnf(c110,plain,~nonreflexive(X584,X583)|~agent(X584,X583,X582)|~patient(X584,X583,X585)|X582!=X585,inference(split_conjunct,[status(thm)],[c109])).
% 1.32/1.53  cnf(c70,negated_conjecture,~member(skolem0001,X483,skolem0007)|patient(skolem0001,skolem0008(X483),X483),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.53  cnf(c625,plain,patient(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007)),skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c70, c369])).
% 1.32/1.53  cnf(c909,plain,~nonreflexive(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007)))|~agent(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007)),X1160)|X1160!=skolem0009(skolem0001,skolem0007),inference(resolution,[status(thm)],[c625, c110])).
% 1.32/1.53  cnf(c1026,plain,~nonreflexive(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007)))|skolem0002!=skolem0009(skolem0001,skolem0007),inference(resolution,[status(thm)],[c909, c620])).
% 1.32/1.53  cnf(c1027,plain,skolem0002!=skolem0009(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1026, c589])).
% 1.32/1.53  cnf(c96,plain,~five(X366,X367)|member(X366,skolem0013(X366,X367),X367),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.53  cnf(c374,plain,member(skolem0001,skolem0013(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c96, c74])).
% 1.32/1.53  cnf(c588,plain,nonreflexive(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c72, c374])).
% 1.32/1.53  cnf(c619,plain,agent(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c69, c374])).
% 1.32/1.53  cnf(c624,plain,patient(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007)),skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c70, c374])).
% 1.32/1.53  cnf(c905,plain,~nonreflexive(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007)))|~agent(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007)),X1155)|X1155!=skolem0013(skolem0001,skolem0007),inference(resolution,[status(thm)],[c624, c110])).
% 1.32/1.53  cnf(c1024,plain,~nonreflexive(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007)))|skolem0002!=skolem0013(skolem0001,skolem0007),inference(resolution,[status(thm)],[c905, c619])).
% 1.32/1.53  cnf(c1025,plain,skolem0002!=skolem0013(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1024, c588])).
% 1.32/1.53  cnf(c89,plain,~five(X362,X363)|member(X362,skolem0011(X362,X363),X363),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.53  cnf(c372,plain,member(skolem0001,skolem0011(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c89, c74])).
% 1.32/1.53  cnf(c587,plain,nonreflexive(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c72, c372])).
% 1.32/1.53  cnf(c618,plain,agent(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c69, c372])).
% 1.32/1.53  cnf(c623,plain,patient(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007)),skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c70, c372])).
% 1.32/1.53  cnf(c903,plain,~nonreflexive(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007)))|~agent(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007)),X1154)|X1154!=skolem0011(skolem0001,skolem0007),inference(resolution,[status(thm)],[c623, c110])).
% 1.32/1.53  cnf(c1022,plain,~nonreflexive(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007)))|skolem0002!=skolem0011(skolem0001,skolem0007),inference(resolution,[status(thm)],[c903, c618])).
% 1.32/1.53  cnf(c1023,plain,skolem0002!=skolem0011(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1022, c587])).
% 1.32/1.53  cnf(c92,plain,~five(X364,X365)|member(X364,skolem0012(X364,X365),X365),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.53  cnf(c373,plain,member(skolem0001,skolem0012(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c92, c74])).
% 1.32/1.53  cnf(c586,plain,nonreflexive(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c72, c373])).
% 1.32/1.53  cnf(c617,plain,agent(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c69, c373])).
% 1.32/1.53  cnf(c622,plain,patient(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007)),skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c70, c373])).
% 1.32/1.53  cnf(c901,plain,~nonreflexive(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007)))|~agent(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007)),X1149)|X1149!=skolem0012(skolem0001,skolem0007),inference(resolution,[status(thm)],[c622, c110])).
% 1.32/1.53  cnf(c1020,plain,~nonreflexive(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007)))|skolem0002!=skolem0012(skolem0001,skolem0007),inference(resolution,[status(thm)],[c901, c617])).
% 1.32/1.53  cnf(c1021,plain,skolem0002!=skolem0012(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1020, c586])).
% 1.32/1.53  cnf(c87,plain,~five(X356,X357)|member(X356,skolem0010(X356,X357),X357),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.53  cnf(c370,plain,member(skolem0001,skolem0010(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c87, c74])).
% 1.32/1.53  cnf(c585,plain,nonreflexive(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c72, c370])).
% 1.32/1.53  cnf(c616,plain,agent(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c69, c370])).
% 1.32/1.53  cnf(c621,plain,patient(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007)),skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c70, c370])).
% 1.32/1.53  cnf(c897,plain,~nonreflexive(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007)))|~agent(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007)),X1144)|X1144!=skolem0010(skolem0001,skolem0007),inference(resolution,[status(thm)],[c621, c110])).
% 1.32/1.53  cnf(c1018,plain,~nonreflexive(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007)))|skolem0002!=skolem0010(skolem0001,skolem0007),inference(resolution,[status(thm)],[c897, c616])).
% 1.32/1.53  cnf(c1019,plain,skolem0002!=skolem0010(skolem0001,skolem0007),inference(resolution,[status(thm)],[c1018, c585])).
% 1.32/1.53  cnf(reflexivity,axiom,X142=X142,theory(equality)).
% 1.32/1.53  cnf(c44,axiom,X456!=X455|X453!=X454|X452!=X457|~patient(X456,X453,X452)|patient(X455,X454,X457),theory(equality)).
% 1.32/1.53  cnf(c908,plain,skolem0001!=X1140|skolem0008(skolem0009(skolem0001,skolem0007))!=X1138|skolem0009(skolem0001,skolem0007)!=X1139|patient(X1140,X1138,X1139),inference(resolution,[status(thm)],[c625, c44])).
% 1.32/1.53  cnf(c1015,plain,skolem0001!=X1142|skolem0009(skolem0001,skolem0007)!=X1141|patient(X1142,skolem0008(skolem0009(skolem0001,skolem0007)),X1141),inference(resolution,[status(thm)],[c908, reflexivity])).
% 1.32/1.53  cnf(c1016,plain,skolem0001!=X1143|patient(X1143,skolem0008(skolem0009(skolem0001,skolem0007)),skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c1015, reflexivity])).
% 1.32/1.53  cnf(c904,plain,skolem0001!=X1128|skolem0008(skolem0013(skolem0001,skolem0007))!=X1126|skolem0013(skolem0001,skolem0007)!=X1127|patient(X1128,X1126,X1127),inference(resolution,[status(thm)],[c624, c44])).
% 1.32/1.53  cnf(c1012,plain,skolem0001!=X1129|skolem0013(skolem0001,skolem0007)!=X1130|patient(X1129,skolem0008(skolem0013(skolem0001,skolem0007)),X1130),inference(resolution,[status(thm)],[c904, reflexivity])).
% 1.32/1.53  cnf(c1013,plain,skolem0001!=X1131|patient(X1131,skolem0008(skolem0013(skolem0001,skolem0007)),skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c1012, reflexivity])).
% 1.32/1.53  cnf(c902,plain,skolem0001!=X1116|skolem0008(skolem0011(skolem0001,skolem0007))!=X1114|skolem0011(skolem0001,skolem0007)!=X1115|patient(X1116,X1114,X1115),inference(resolution,[status(thm)],[c623, c44])).
% 1.32/1.53  cnf(c1009,plain,skolem0001!=X1117|skolem0011(skolem0001,skolem0007)!=X1118|patient(X1117,skolem0008(skolem0011(skolem0001,skolem0007)),X1118),inference(resolution,[status(thm)],[c902, reflexivity])).
% 1.32/1.53  cnf(c1010,plain,skolem0001!=X1119|patient(X1119,skolem0008(skolem0011(skolem0001,skolem0007)),skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c1009, reflexivity])).
% 1.32/1.53  cnf(c900,plain,skolem0001!=X1104|skolem0008(skolem0012(skolem0001,skolem0007))!=X1102|skolem0012(skolem0001,skolem0007)!=X1103|patient(X1104,X1102,X1103),inference(resolution,[status(thm)],[c622, c44])).
% 1.32/1.53  cnf(c1006,plain,skolem0001!=X1105|skolem0012(skolem0001,skolem0007)!=X1106|patient(X1105,skolem0008(skolem0012(skolem0001,skolem0007)),X1106),inference(resolution,[status(thm)],[c900, reflexivity])).
% 1.32/1.53  cnf(c1007,plain,skolem0001!=X1113|patient(X1113,skolem0008(skolem0012(skolem0001,skolem0007)),skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c1006, reflexivity])).
% 1.32/1.53  cnf(c896,plain,skolem0001!=X1092|skolem0008(skolem0010(skolem0001,skolem0007))!=X1090|skolem0010(skolem0001,skolem0007)!=X1091|patient(X1092,X1090,X1091),inference(resolution,[status(thm)],[c621, c44])).
% 1.32/1.53  cnf(c1003,plain,skolem0001!=X1100|skolem0010(skolem0001,skolem0007)!=X1099|patient(X1100,skolem0008(skolem0010(skolem0001,skolem0007)),X1099),inference(resolution,[status(thm)],[c896, reflexivity])).
% 1.32/1.53  cnf(c1004,plain,skolem0001!=X1101|patient(X1101,skolem0008(skolem0010(skolem0001,skolem0007)),skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c1003, reflexivity])).
% 1.32/1.53  cnf(c57,negated_conjecture,of(skolem0001,skolem0004,skolem0003),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.53  fof(ax53,axiom,(![U]:(![V]:(![W]:(((entity(U,V)&forename(U,W))&of(U,W,V))=>(~(?[X]:((forename(U,X)&X!=W)&of(U,X,V)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax53)).
% 1.32/1.53  fof(c111,plain,(![U]:(![V]:(![W]:(((~entity(U,V)|~forename(U,W))|~of(U,W,V))|(![X]:((~forename(U,X)|X=W)|~of(U,X,V))))))),inference(fof_nnf,[status(thm)],[ax53])).
% 1.32/1.53  fof(c113,plain,(![X34]:(![X35]:(![X36]:(![X37]:(((~entity(X34,X35)|~forename(X34,X36))|~of(X34,X36,X35))|((~forename(X34,X37)|X37=X36)|~of(X34,X37,X35))))))),inference(shift_quantors,[status(thm)],[fof(c112,plain,(![X34]:(![X35]:(![X36]:(((~entity(X34,X35)|~forename(X34,X36))|~of(X34,X36,X35))|(![X37]:((~forename(X34,X37)|X37=X36)|~of(X34,X37,X35))))))),inference(variable_rename,[status(thm)],[c111])).])).
% 1.32/1.53  cnf(c114,plain,~entity(X595,X594)|~forename(X595,X593)|~of(X595,X593,X594)|~forename(X595,X592)|X592=X593|~of(X595,X592,X594),inference(split_conjunct,[status(thm)],[c113])).
% 1.32/1.53  cnf(c672,plain,~entity(skolem0001,skolem0003)|~forename(skolem0001,X1089)|~of(skolem0001,X1089,skolem0003)|~forename(skolem0001,skolem0004)|skolem0004=X1089,inference(resolution,[status(thm)],[c114, c57])).
% 1.32/1.53  cnf(c46,axiom,X467!=X466|X464!=X465|X463!=X468|~agent(X467,X464,X463)|agent(X466,X465,X468),theory(equality)).
% 1.32/1.53  cnf(c763,plain,skolem0001!=X1084|skolem0008(skolem0009(skolem0001,skolem0007))!=X1083|skolem0002!=X1085|agent(X1084,X1083,X1085),inference(resolution,[status(thm)],[c620, c46])).
% 1.32/1.53  cnf(c999,plain,skolem0001!=X1087|skolem0002!=X1086|agent(X1087,skolem0008(skolem0009(skolem0001,skolem0007)),X1086),inference(resolution,[status(thm)],[c763, reflexivity])).
% 1.32/1.53  cnf(c1000,plain,skolem0001!=X1088|agent(X1088,skolem0008(skolem0009(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c999, reflexivity])).
% 1.32/1.53  cnf(c762,plain,skolem0001!=X1078|skolem0008(skolem0013(skolem0001,skolem0007))!=X1077|skolem0002!=X1079|agent(X1078,X1077,X1079),inference(resolution,[status(thm)],[c619, c46])).
% 1.32/1.53  cnf(c996,plain,skolem0001!=X1080|skolem0002!=X1081|agent(X1080,skolem0008(skolem0013(skolem0001,skolem0007)),X1081),inference(resolution,[status(thm)],[c762, reflexivity])).
% 1.32/1.53  cnf(c997,plain,skolem0001!=X1082|agent(X1082,skolem0008(skolem0013(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c996, reflexivity])).
% 1.32/1.53  cnf(c761,plain,skolem0001!=X1072|skolem0008(skolem0011(skolem0001,skolem0007))!=X1071|skolem0002!=X1073|agent(X1072,X1071,X1073),inference(resolution,[status(thm)],[c618, c46])).
% 1.32/1.53  cnf(c993,plain,skolem0001!=X1075|skolem0002!=X1074|agent(X1075,skolem0008(skolem0011(skolem0001,skolem0007)),X1074),inference(resolution,[status(thm)],[c761, reflexivity])).
% 1.32/1.53  cnf(c994,plain,skolem0001!=X1076|agent(X1076,skolem0008(skolem0011(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c993, reflexivity])).
% 1.32/1.53  cnf(c759,plain,skolem0001!=X1066|skolem0008(skolem0012(skolem0001,skolem0007))!=X1065|skolem0002!=X1067|agent(X1066,X1065,X1067),inference(resolution,[status(thm)],[c617, c46])).
% 1.32/1.53  cnf(c990,plain,skolem0001!=X1069|skolem0002!=X1068|agent(X1069,skolem0008(skolem0012(skolem0001,skolem0007)),X1068),inference(resolution,[status(thm)],[c759, reflexivity])).
% 1.32/1.54  cnf(c991,plain,skolem0001!=X1070|agent(X1070,skolem0008(skolem0012(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c990, reflexivity])).
% 1.32/1.54  cnf(c758,plain,skolem0001!=X1060|skolem0008(skolem0010(skolem0001,skolem0007))!=X1059|skolem0002!=X1061|agent(X1060,X1059,X1061),inference(resolution,[status(thm)],[c616, c46])).
% 1.32/1.54  cnf(c987,plain,skolem0001!=X1063|skolem0002!=X1062|agent(X1063,skolem0008(skolem0010(skolem0001,skolem0007)),X1062),inference(resolution,[status(thm)],[c758, reflexivity])).
% 1.32/1.54  cnf(c988,plain,skolem0001!=X1064|agent(X1064,skolem0008(skolem0010(skolem0001,skolem0007)),skolem0002),inference(resolution,[status(thm)],[c987, reflexivity])).
% 1.32/1.54  cnf(c47,axiom,X474!=X473|X471!=X472|X470!=X475|~member(X474,X471,X470)|member(X473,X472,X475),theory(equality)).
% 1.32/1.54  cnf(c611,plain,skolem0001!=X1054|skolem0009(skolem0001,skolem0007)!=X1053|skolem0007!=X1055|member(X1054,X1053,X1055),inference(resolution,[status(thm)],[c47, c369])).
% 1.32/1.54  cnf(c984,plain,skolem0001!=X1057|skolem0007!=X1056|member(X1057,skolem0009(skolem0001,skolem0007),X1056),inference(resolution,[status(thm)],[c611, reflexivity])).
% 1.32/1.54  cnf(c985,plain,skolem0001!=X1058|member(X1058,skolem0009(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c984, reflexivity])).
% 1.32/1.54  cnf(c610,plain,skolem0001!=X1048|skolem0013(skolem0001,skolem0007)!=X1047|skolem0007!=X1049|member(X1048,X1047,X1049),inference(resolution,[status(thm)],[c47, c374])).
% 1.32/1.54  cnf(c981,plain,skolem0001!=X1051|skolem0007!=X1050|member(X1051,skolem0013(skolem0001,skolem0007),X1050),inference(resolution,[status(thm)],[c610, reflexivity])).
% 1.32/1.54  cnf(c982,plain,skolem0001!=X1052|member(X1052,skolem0013(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c981, reflexivity])).
% 1.32/1.54  cnf(c609,plain,skolem0001!=X1041|skolem0011(skolem0001,skolem0007)!=X1040|skolem0007!=X1042|member(X1041,X1040,X1042),inference(resolution,[status(thm)],[c47, c372])).
% 1.32/1.54  cnf(c977,plain,skolem0001!=X1045|skolem0007!=X1044|member(X1045,skolem0011(skolem0001,skolem0007),X1044),inference(resolution,[status(thm)],[c609, reflexivity])).
% 1.32/1.54  cnf(c979,plain,skolem0001!=X1046|member(X1046,skolem0011(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c977, reflexivity])).
% 1.32/1.54  cnf(c608,plain,skolem0001!=X1033|skolem0012(skolem0001,skolem0007)!=X1032|skolem0007!=X1034|member(X1033,X1032,X1034),inference(resolution,[status(thm)],[c47, c373])).
% 1.32/1.54  cnf(c973,plain,skolem0001!=X1039|skolem0007!=X1038|member(X1039,skolem0012(skolem0001,skolem0007),X1038),inference(resolution,[status(thm)],[c608, reflexivity])).
% 1.32/1.54  cnf(c976,plain,skolem0001!=X1043|member(X1043,skolem0012(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c973, reflexivity])).
% 1.32/1.54  cnf(c607,plain,skolem0001!=X1024|skolem0010(skolem0001,skolem0007)!=X1023|skolem0007!=X1025|member(X1024,X1023,X1025),inference(resolution,[status(thm)],[c47, c370])).
% 1.32/1.54  cnf(c968,plain,skolem0001!=X1036|skolem0007!=X1035|member(X1036,skolem0010(skolem0001,skolem0007),X1035),inference(resolution,[status(thm)],[c607, reflexivity])).
% 1.32/1.54  cnf(c974,plain,skolem0001!=X1037|member(X1037,skolem0010(skolem0001,skolem0007),skolem0007),inference(resolution,[status(thm)],[c968, reflexivity])).
% 1.32/1.54  cnf(c29,axiom,X389!=X390|X391!=X388|~cost(X389,X391)|cost(X390,X388),theory(equality)).
% 1.32/1.54  cnf(c73,negated_conjecture,~member(skolem0001,X469,skolem0007)|cost(skolem0001,skolem0008(X469)),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c600,plain,cost(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c73, c369])).
% 1.32/1.54  cnf(c614,plain,skolem0001!=X1029|skolem0008(skolem0009(skolem0001,skolem0007))!=X1030|cost(X1029,X1030),inference(resolution,[status(thm)],[c600, c29])).
% 1.32/1.54  cnf(c971,plain,skolem0001!=X1031|cost(X1031,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c614, reflexivity])).
% 1.32/1.54  cnf(c599,plain,cost(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c73, c374])).
% 1.32/1.54  cnf(c612,plain,skolem0001!=X1026|skolem0008(skolem0013(skolem0001,skolem0007))!=X1027|cost(X1026,X1027),inference(resolution,[status(thm)],[c599, c29])).
% 1.32/1.54  cnf(c969,plain,skolem0001!=X1028|cost(X1028,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c612, reflexivity])).
% 1.32/1.54  cnf(c598,plain,cost(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c73, c372])).
% 1.32/1.54  cnf(c605,plain,skolem0001!=X1020|skolem0008(skolem0011(skolem0001,skolem0007))!=X1021|cost(X1020,X1021),inference(resolution,[status(thm)],[c598, c29])).
% 1.32/1.54  cnf(c966,plain,skolem0001!=X1022|cost(X1022,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c605, reflexivity])).
% 1.32/1.54  cnf(c597,plain,cost(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c73, c373])).
% 1.32/1.54  cnf(c603,plain,skolem0001!=X1017|skolem0008(skolem0012(skolem0001,skolem0007))!=X1018|cost(X1017,X1018),inference(resolution,[status(thm)],[c597, c29])).
% 1.32/1.54  cnf(c964,plain,skolem0001!=X1019|cost(X1019,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c603, reflexivity])).
% 1.32/1.54  cnf(c596,plain,cost(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c73, c370])).
% 1.32/1.54  cnf(c601,plain,skolem0001!=X1014|skolem0008(skolem0010(skolem0001,skolem0007))!=X1015|cost(X1014,X1015),inference(resolution,[status(thm)],[c596, c29])).
% 1.32/1.54  cnf(c962,plain,skolem0001!=X1016|cost(X1016,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c601, reflexivity])).
% 1.32/1.54  cnf(c45,axiom,X459!=X460|X461!=X458|~nonreflexive(X459,X461)|nonreflexive(X460,X458),theory(equality)).
% 1.32/1.54  cnf(c595,plain,skolem0001!=X1011|skolem0008(skolem0009(skolem0001,skolem0007))!=X1012|nonreflexive(X1011,X1012),inference(resolution,[status(thm)],[c589, c45])).
% 1.32/1.54  cnf(c960,plain,skolem0001!=X1013|nonreflexive(X1013,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c595, reflexivity])).
% 1.32/1.54  cnf(c63,negated_conjecture,agent(skolem0001,skolem0006,skolem0003),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c594,plain,skolem0001!=X1005|skolem0006!=X1004|skolem0003!=X1006|agent(X1005,X1004,X1006),inference(resolution,[status(thm)],[c46, c63])).
% 1.32/1.54  cnf(c956,plain,skolem0001!=X1009|skolem0006!=X1008|agent(X1009,X1008,skolem0003),inference(resolution,[status(thm)],[c594, reflexivity])).
% 1.32/1.54  cnf(c958,plain,skolem0001!=X1010|agent(X1010,skolem0006,skolem0003),inference(resolution,[status(thm)],[c956, reflexivity])).
% 1.32/1.54  cnf(c593,plain,skolem0001!=X1002|skolem0008(skolem0013(skolem0001,skolem0007))!=X1003|nonreflexive(X1002,X1003),inference(resolution,[status(thm)],[c588, c45])).
% 1.32/1.54  cnf(c955,plain,skolem0001!=X1007|nonreflexive(X1007,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c593, reflexivity])).
% 1.32/1.54  cnf(c592,plain,skolem0001!=X998|skolem0008(skolem0011(skolem0001,skolem0007))!=X999|nonreflexive(X998,X999),inference(resolution,[status(thm)],[c587, c45])).
% 1.32/1.54  cnf(c952,plain,skolem0001!=X1001|nonreflexive(X1001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c592, reflexivity])).
% 1.32/1.54  cnf(c591,plain,skolem0001!=X996|skolem0008(skolem0012(skolem0001,skolem0007))!=X997|nonreflexive(X996,X997),inference(resolution,[status(thm)],[c586, c45])).
% 1.32/1.54  cnf(c951,plain,skolem0001!=X1000|nonreflexive(X1000,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c591, reflexivity])).
% 1.32/1.54  cnf(c590,plain,skolem0001!=X992|skolem0008(skolem0010(skolem0001,skolem0007))!=X993|nonreflexive(X992,X993),inference(resolution,[status(thm)],[c585, c45])).
% 1.32/1.54  cnf(c948,plain,skolem0001!=X995|nonreflexive(X995,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c590, reflexivity])).
% 1.32/1.54  cnf(c41,axiom,X438!=X439|X440!=X437|~present(X438,X440)|present(X439,X437),theory(equality)).
% 1.32/1.54  cnf(c71,negated_conjecture,~member(skolem0001,X451,skolem0007)|present(skolem0001,skolem0008(X451)),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c577,plain,present(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c71, c369])).
% 1.32/1.54  cnf(c583,plain,skolem0001!=X991|skolem0008(skolem0009(skolem0001,skolem0007))!=X990|present(X991,X990),inference(resolution,[status(thm)],[c577, c41])).
% 1.32/1.54  cnf(c947,plain,skolem0001!=X994|present(X994,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c583, reflexivity])).
% 1.32/1.54  cnf(c576,plain,present(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c71, c374])).
% 1.32/1.54  cnf(c582,plain,skolem0001!=X987|skolem0008(skolem0013(skolem0001,skolem0007))!=X986|present(X987,X986),inference(resolution,[status(thm)],[c576, c41])).
% 1.32/1.54  cnf(c944,plain,skolem0001!=X989|present(X989,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c582, reflexivity])).
% 1.32/1.54  cnf(c575,plain,present(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c71, c372])).
% 1.32/1.54  cnf(c581,plain,skolem0001!=X985|skolem0008(skolem0011(skolem0001,skolem0007))!=X984|present(X985,X984),inference(resolution,[status(thm)],[c575, c41])).
% 1.32/1.54  cnf(c943,plain,skolem0001!=X988|present(X988,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c581, reflexivity])).
% 1.32/1.54  cnf(c574,plain,present(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c71, c373])).
% 1.32/1.54  cnf(c580,plain,skolem0001!=X981|skolem0008(skolem0012(skolem0001,skolem0007))!=X980|present(X981,X980),inference(resolution,[status(thm)],[c574, c41])).
% 1.32/1.54  cnf(c940,plain,skolem0001!=X983|present(X983,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c580, reflexivity])).
% 1.32/1.54  cnf(c573,plain,present(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c71, c370])).
% 1.32/1.54  cnf(c579,plain,skolem0001!=X979|skolem0008(skolem0010(skolem0001,skolem0007))!=X978|present(X979,X978),inference(resolution,[status(thm)],[c573, c41])).
% 1.32/1.54  cnf(c939,plain,skolem0001!=X982|present(X982,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c579, reflexivity])).
% 1.32/1.54  cnf(c64,negated_conjecture,patient(skolem0001,skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c578,plain,skolem0001!=X974|skolem0006!=X972|skolem0005!=X973|patient(X974,X972,X973),inference(resolution,[status(thm)],[c44, c64])).
% 1.32/1.54  cnf(c936,plain,skolem0001!=X976|skolem0006!=X975|patient(X976,X975,skolem0005),inference(resolution,[status(thm)],[c578, reflexivity])).
% 1.32/1.54  cnf(c937,plain,skolem0001!=X977|patient(X977,skolem0006,skolem0005),inference(resolution,[status(thm)],[c936, reflexivity])).
% 1.32/1.54  cnf(c36,axiom,X418!=X419|X420!=X417|~singleton(X418,X420)|singleton(X419,X417),theory(equality)).
% 1.32/1.54  fof(ax39,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax39)).
% 1.32/1.54  fof(c162,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax39])).
% 1.32/1.54  fof(c163,plain,(![X64]:(![X65]:(~thing(X64,X65)|singleton(X64,X65)))),inference(variable_rename,[status(thm)],[c162])).
% 1.32/1.54  cnf(c164,plain,~thing(X193,X194)|singleton(X193,X194),inference(split_conjunct,[status(thm)],[c163])).
% 1.32/1.54  fof(ax30,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax30)).
% 1.32/1.54  fof(c189,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 1.32/1.54  fof(c190,plain,(![X82]:(![X83]:(~eventuality(X82,X83)|thing(X82,X83)))),inference(variable_rename,[status(thm)],[c189])).
% 1.32/1.54  cnf(c191,plain,~eventuality(X223,X224)|thing(X223,X224),inference(split_conjunct,[status(thm)],[c190])).
% 1.32/1.54  fof(ax31,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 1.32/1.54  fof(c186,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 1.32/1.54  fof(c187,plain,(![X80]:(![X81]:(~event(X80,X81)|eventuality(X80,X81)))),inference(variable_rename,[status(thm)],[c186])).
% 1.32/1.54  cnf(c188,plain,~event(X218,X217)|eventuality(X218,X217),inference(split_conjunct,[status(thm)],[c187])).
% 1.32/1.54  cnf(c68,negated_conjecture,~member(skolem0001,X416,skolem0007)|event(skolem0001,skolem0008(X416)),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c471,plain,event(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c68, c369])).
% 1.32/1.54  cnf(c490,plain,eventuality(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c471, c188])).
% 1.32/1.54  cnf(c520,plain,thing(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c490, c191])).
% 1.32/1.54  cnf(c565,plain,singleton(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c520, c164])).
% 1.32/1.54  cnf(c572,plain,skolem0001!=X970|skolem0008(skolem0009(skolem0001,skolem0007))!=X969|singleton(X970,X969),inference(resolution,[status(thm)],[c565, c36])).
% 1.32/1.54  cnf(c934,plain,skolem0001!=X971|singleton(X971,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c572, reflexivity])).
% 1.32/1.54  cnf(c470,plain,event(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c68, c374])).
% 1.32/1.54  cnf(c488,plain,eventuality(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c470, c188])).
% 1.32/1.54  cnf(c515,plain,thing(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c488, c191])).
% 1.32/1.54  cnf(c559,plain,singleton(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c515, c164])).
% 1.32/1.54  cnf(c571,plain,skolem0001!=X967|skolem0008(skolem0013(skolem0001,skolem0007))!=X966|singleton(X967,X966),inference(resolution,[status(thm)],[c559, c36])).
% 1.32/1.54  cnf(c932,plain,skolem0001!=X968|singleton(X968,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c571, reflexivity])).
% 1.32/1.54  cnf(c43,axiom,X449!=X448|X446!=X447|X445!=X450|~of(X449,X446,X445)|of(X448,X447,X450),theory(equality)).
% 1.32/1.54  cnf(c570,plain,skolem0001!=X960|skolem0004!=X962|skolem0003!=X961|of(X960,X962,X961),inference(resolution,[status(thm)],[c43, c57])).
% 1.32/1.54  cnf(c929,plain,skolem0001!=X963|skolem0004!=X964|of(X963,X964,skolem0003),inference(resolution,[status(thm)],[c570, reflexivity])).
% 1.32/1.54  cnf(c930,plain,skolem0001!=X965|of(X965,skolem0004,skolem0003),inference(resolution,[status(thm)],[c929, reflexivity])).
% 1.32/1.54  cnf(c469,plain,event(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c68, c372])).
% 1.32/1.54  cnf(c486,plain,eventuality(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c469, c188])).
% 1.32/1.54  cnf(c510,plain,thing(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c486, c191])).
% 1.32/1.54  cnf(c553,plain,singleton(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c510, c164])).
% 1.32/1.54  cnf(c569,plain,skolem0001!=X958|skolem0008(skolem0011(skolem0001,skolem0007))!=X957|singleton(X958,X957),inference(resolution,[status(thm)],[c553, c36])).
% 1.32/1.54  cnf(c927,plain,skolem0001!=X959|singleton(X959,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c569, reflexivity])).
% 1.32/1.54  cnf(c468,plain,event(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c68, c373])).
% 1.32/1.54  cnf(c484,plain,eventuality(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c468, c188])).
% 1.32/1.54  cnf(c505,plain,thing(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c484, c191])).
% 1.32/1.54  cnf(c542,plain,singleton(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c505, c164])).
% 1.32/1.54  cnf(c568,plain,skolem0001!=X955|skolem0008(skolem0012(skolem0001,skolem0007))!=X954|singleton(X955,X954),inference(resolution,[status(thm)],[c542, c36])).
% 1.32/1.54  cnf(c925,plain,skolem0001!=X956|singleton(X956,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c568, reflexivity])).
% 1.32/1.54  cnf(c467,plain,event(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c68, c370])).
% 1.32/1.54  cnf(c473,plain,eventuality(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c467, c188])).
% 1.32/1.54  cnf(c495,plain,thing(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c473, c191])).
% 1.32/1.54  cnf(c531,plain,singleton(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c495, c164])).
% 1.32/1.54  cnf(c567,plain,skolem0001!=X952|skolem0008(skolem0010(skolem0001,skolem0007))!=X951|singleton(X952,X951),inference(resolution,[status(thm)],[c531, c36])).
% 1.32/1.54  cnf(c923,plain,skolem0001!=X953|singleton(X953,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c567, reflexivity])).
% 1.32/1.54  cnf(c19,axiom,X322!=X323|X324!=X321|~thing(X322,X324)|thing(X323,X321),theory(equality)).
% 1.32/1.54  cnf(c564,plain,skolem0001!=X948|skolem0008(skolem0009(skolem0001,skolem0007))!=X949|thing(X948,X949),inference(resolution,[status(thm)],[c520, c19])).
% 1.32/1.54  cnf(c921,plain,skolem0001!=X950|thing(X950,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c564, reflexivity])).
% 1.32/1.54  cnf(c15,axiom,X296!=X297|X298!=X295|~unisex(X296,X298)|unisex(X297,X295),theory(equality)).
% 1.32/1.54  fof(ax27,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax27)).
% 1.32/1.54  fof(c198,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 1.32/1.54  fof(c199,plain,(![X88]:(![X89]:(~eventuality(X88,X89)|unisex(X88,X89)))),inference(variable_rename,[status(thm)],[c198])).
% 1.32/1.54  cnf(c200,plain,~eventuality(X233,X234)|unisex(X233,X234),inference(split_conjunct,[status(thm)],[c199])).
% 1.32/1.54  cnf(c518,plain,unisex(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c490, c200])).
% 1.32/1.54  cnf(c563,plain,skolem0001!=X945|skolem0008(skolem0009(skolem0001,skolem0007))!=X946|unisex(X945,X946),inference(resolution,[status(thm)],[c518, c15])).
% 1.32/1.54  cnf(c919,plain,skolem0001!=X947|unisex(X947,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c563, reflexivity])).
% 1.32/1.54  cnf(c18,axiom,X318!=X319|X320!=X317|~specific(X318,X320)|specific(X319,X317),theory(equality)).
% 1.32/1.54  fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax29)).
% 1.32/1.54  fof(c192,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 1.32/1.54  fof(c193,plain,(![X84]:(![X85]:(~eventuality(X84,X85)|specific(X84,X85)))),inference(variable_rename,[status(thm)],[c192])).
% 1.32/1.54  cnf(c194,plain,~eventuality(X226,X225)|specific(X226,X225),inference(split_conjunct,[status(thm)],[c193])).
% 1.32/1.54  cnf(c517,plain,specific(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c490, c194])).
% 1.32/1.54  cnf(c562,plain,skolem0001!=X942|skolem0008(skolem0009(skolem0001,skolem0007))!=X943|specific(X942,X943),inference(resolution,[status(thm)],[c517, c18])).
% 1.32/1.54  cnf(c917,plain,skolem0001!=X944|specific(X944,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c562, reflexivity])).
% 1.32/1.54  cnf(c28,axiom,X385!=X386|X387!=X384|~nonexistent(X385,X387)|nonexistent(X386,X384),theory(equality)).
% 1.32/1.54  fof(ax28,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax28)).
% 1.32/1.54  fof(c195,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 1.32/1.54  fof(c196,plain,(![X86]:(![X87]:(~eventuality(X86,X87)|nonexistent(X86,X87)))),inference(variable_rename,[status(thm)],[c195])).
% 1.32/1.54  cnf(c197,plain,~eventuality(X232,X231)|nonexistent(X232,X231),inference(split_conjunct,[status(thm)],[c196])).
% 1.32/1.54  cnf(c516,plain,nonexistent(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c490, c197])).
% 1.32/1.54  cnf(c560,plain,skolem0001!=X939|skolem0008(skolem0009(skolem0001,skolem0007))!=X940|nonexistent(X939,X940),inference(resolution,[status(thm)],[c516, c28])).
% 1.32/1.54  cnf(c915,plain,skolem0001!=X941|nonexistent(X941,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c560, reflexivity])).
% 1.32/1.54  cnf(c558,plain,skolem0001!=X936|skolem0008(skolem0013(skolem0001,skolem0007))!=X937|thing(X936,X937),inference(resolution,[status(thm)],[c515, c19])).
% 1.32/1.54  cnf(c913,plain,skolem0001!=X938|thing(X938,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c558, reflexivity])).
% 1.32/1.54  cnf(c513,plain,unisex(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c488, c200])).
% 1.32/1.54  cnf(c557,plain,skolem0001!=X933|skolem0008(skolem0013(skolem0001,skolem0007))!=X934|unisex(X933,X934),inference(resolution,[status(thm)],[c513, c15])).
% 1.32/1.54  cnf(c911,plain,skolem0001!=X935|unisex(X935,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c557, reflexivity])).
% 1.32/1.54  cnf(c666,plain,~nonreflexive(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X932)|X932!=skolem0005,inference(resolution,[status(thm)],[c110, c64])).
% 1.32/1.54  cnf(c910,plain,~nonreflexive(skolem0001,skolem0006)|skolem0003!=skolem0005,inference(resolution,[status(thm)],[c666, c63])).
% 1.32/1.54  cnf(c512,plain,specific(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c488, c194])).
% 1.32/1.54  cnf(c556,plain,skolem0001!=X929|skolem0008(skolem0013(skolem0001,skolem0007))!=X930|specific(X929,X930),inference(resolution,[status(thm)],[c512, c18])).
% 1.32/1.54  cnf(c906,plain,skolem0001!=X931|specific(X931,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c556, reflexivity])).
% 1.32/1.54  cnf(c511,plain,nonexistent(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c488, c197])).
% 1.32/1.54  cnf(c554,plain,skolem0001!=X926|skolem0008(skolem0013(skolem0001,skolem0007))!=X927|nonexistent(X926,X927),inference(resolution,[status(thm)],[c511, c28])).
% 1.32/1.54  cnf(c898,plain,skolem0001!=X928|nonexistent(X928,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c554, reflexivity])).
% 1.32/1.54  cnf(c552,plain,skolem0001!=X922|skolem0008(skolem0011(skolem0001,skolem0007))!=X923|thing(X922,X923),inference(resolution,[status(thm)],[c510, c19])).
% 1.32/1.54  cnf(c893,plain,skolem0001!=X925|thing(X925,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c552, reflexivity])).
% 1.32/1.54  cnf(c76,negated_conjecture,~member(skolem0001,X353,skolem0007)|dollar(skolem0001,X353),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c392,plain,dollar(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c370, c76])).
% 1.32/1.54  cnf(c40,axiom,X434!=X435|X436!=X433|~dollar(X434,X436)|dollar(X435,X433),theory(equality)).
% 1.32/1.54  cnf(c551,plain,skolem0001!=X921|skolem0010(skolem0001,skolem0007)!=X920|dollar(X921,X920),inference(resolution,[status(thm)],[c40, c392])).
% 1.32/1.54  cnf(c892,plain,skolem0001!=X924|dollar(X924,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c551, reflexivity])).
% 1.32/1.54  cnf(c508,plain,unisex(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c486, c200])).
% 1.32/1.54  cnf(c546,plain,skolem0001!=X916|skolem0008(skolem0011(skolem0001,skolem0007))!=X917|unisex(X916,X917),inference(resolution,[status(thm)],[c508, c15])).
% 1.32/1.54  cnf(c889,plain,skolem0001!=X919|unisex(X919,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c546, reflexivity])).
% 1.32/1.54  cnf(c375,plain,dollar(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c369, c76])).
% 1.32/1.54  cnf(c550,plain,skolem0001!=X915|skolem0009(skolem0001,skolem0007)!=X914|dollar(X915,X914),inference(resolution,[status(thm)],[c40, c375])).
% 1.32/1.54  cnf(c888,plain,skolem0001!=X918|dollar(X918,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c550, reflexivity])).
% 1.32/1.54  cnf(c507,plain,specific(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c486, c194])).
% 1.32/1.54  cnf(c545,plain,skolem0001!=X910|skolem0008(skolem0011(skolem0001,skolem0007))!=X911|specific(X910,X911),inference(resolution,[status(thm)],[c507, c18])).
% 1.32/1.54  cnf(c885,plain,skolem0001!=X913|specific(X913,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c545, reflexivity])).
% 1.32/1.54  cnf(c423,plain,dollar(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c373, c76])).
% 1.32/1.54  cnf(c549,plain,skolem0001!=X909|skolem0012(skolem0001,skolem0007)!=X908|dollar(X909,X908),inference(resolution,[status(thm)],[c40, c423])).
% 1.32/1.54  cnf(c884,plain,skolem0001!=X912|dollar(X912,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c549, reflexivity])).
% 1.32/1.54  cnf(c506,plain,nonexistent(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c486, c197])).
% 1.32/1.54  cnf(c543,plain,skolem0001!=X904|skolem0008(skolem0011(skolem0001,skolem0007))!=X905|nonexistent(X904,X905),inference(resolution,[status(thm)],[c506, c28])).
% 1.32/1.54  cnf(c881,plain,skolem0001!=X907|nonexistent(X907,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c543, reflexivity])).
% 1.32/1.54  cnf(c440,plain,dollar(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c374, c76])).
% 1.32/1.54  cnf(c548,plain,skolem0001!=X903|skolem0013(skolem0001,skolem0007)!=X902|dollar(X903,X902),inference(resolution,[status(thm)],[c40, c440])).
% 1.32/1.54  cnf(c880,plain,skolem0001!=X906|dollar(X906,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c548, reflexivity])).
% 1.32/1.54  cnf(c541,plain,skolem0001!=X898|skolem0008(skolem0012(skolem0001,skolem0007))!=X899|thing(X898,X899),inference(resolution,[status(thm)],[c505, c19])).
% 1.32/1.54  cnf(c877,plain,skolem0001!=X901|thing(X901,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c541, reflexivity])).
% 1.32/1.54  cnf(c408,plain,dollar(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c372, c76])).
% 1.32/1.54  cnf(c547,plain,skolem0001!=X897|skolem0011(skolem0001,skolem0007)!=X896|dollar(X897,X896),inference(resolution,[status(thm)],[c40, c408])).
% 1.32/1.54  cnf(c876,plain,skolem0001!=X900|dollar(X900,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c547, reflexivity])).
% 1.32/1.54  cnf(c503,plain,unisex(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c484, c200])).
% 1.32/1.54  cnf(c540,plain,skolem0001!=X892|skolem0008(skolem0012(skolem0001,skolem0007))!=X893|unisex(X892,X893),inference(resolution,[status(thm)],[c503, c15])).
% 1.32/1.54  cnf(c873,plain,skolem0001!=X895|unisex(X895,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c540, reflexivity])).
% 1.32/1.54  fof(ax44,axiom,(![U]:(![V]:(dollar(U,V)=>cash(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax44)).
% 1.32/1.54  fof(c147,plain,(![U]:(![V]:(~dollar(U,V)|cash(U,V)))),inference(fof_nnf,[status(thm)],[ax44])).
% 1.32/1.54  fof(c148,plain,(![X54]:(![X55]:(~dollar(X54,X55)|cash(X54,X55)))),inference(variable_rename,[status(thm)],[c147])).
% 1.32/1.54  cnf(c149,plain,~dollar(X179,X180)|cash(X179,X180),inference(split_conjunct,[status(thm)],[c148])).
% 1.32/1.54  cnf(c409,plain,cash(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c408, c149])).
% 1.32/1.54  cnf(c39,axiom,X430!=X431|X432!=X429|~cash(X430,X432)|cash(X431,X429),theory(equality)).
% 1.32/1.54  cnf(c539,plain,skolem0001!=X891|skolem0011(skolem0001,skolem0007)!=X890|cash(X891,X890),inference(resolution,[status(thm)],[c39, c409])).
% 1.32/1.54  cnf(c872,plain,skolem0001!=X894|cash(X894,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c539, reflexivity])).
% 1.32/1.54  cnf(c502,plain,specific(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c484, c194])).
% 1.32/1.54  cnf(c534,plain,skolem0001!=X886|skolem0008(skolem0012(skolem0001,skolem0007))!=X887|specific(X886,X887),inference(resolution,[status(thm)],[c502, c18])).
% 1.32/1.54  cnf(c869,plain,skolem0001!=X889|specific(X889,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c534, reflexivity])).
% 1.32/1.54  cnf(c441,plain,cash(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c440, c149])).
% 1.32/1.54  cnf(c538,plain,skolem0001!=X885|skolem0013(skolem0001,skolem0007)!=X884|cash(X885,X884),inference(resolution,[status(thm)],[c39, c441])).
% 1.32/1.54  cnf(c868,plain,skolem0001!=X888|cash(X888,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c538, reflexivity])).
% 1.32/1.54  cnf(c501,plain,nonexistent(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c484, c197])).
% 1.32/1.54  cnf(c532,plain,skolem0001!=X880|skolem0008(skolem0012(skolem0001,skolem0007))!=X881|nonexistent(X880,X881),inference(resolution,[status(thm)],[c501, c28])).
% 1.32/1.54  cnf(c865,plain,skolem0001!=X883|nonexistent(X883,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c532, reflexivity])).
% 1.32/1.54  cnf(c425,plain,cash(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c423, c149])).
% 1.32/1.54  cnf(c537,plain,skolem0001!=X879|skolem0012(skolem0001,skolem0007)!=X878|cash(X879,X878),inference(resolution,[status(thm)],[c39, c425])).
% 1.32/1.54  cnf(c864,plain,skolem0001!=X882|cash(X882,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c537, reflexivity])).
% 1.32/1.54  cnf(c530,plain,skolem0001!=X874|skolem0008(skolem0010(skolem0001,skolem0007))!=X875|thing(X874,X875),inference(resolution,[status(thm)],[c495, c19])).
% 1.32/1.54  cnf(c861,plain,skolem0001!=X877|thing(X877,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c530, reflexivity])).
% 1.32/1.54  cnf(c376,plain,cash(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c375, c149])).
% 1.32/1.54  cnf(c536,plain,skolem0001!=X873|skolem0009(skolem0001,skolem0007)!=X872|cash(X873,X872),inference(resolution,[status(thm)],[c39, c376])).
% 1.32/1.54  cnf(c860,plain,skolem0001!=X876|cash(X876,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c536, reflexivity])).
% 1.32/1.54  cnf(c493,plain,unisex(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c473, c200])).
% 1.32/1.54  cnf(c529,plain,skolem0001!=X868|skolem0008(skolem0010(skolem0001,skolem0007))!=X869|unisex(X868,X869),inference(resolution,[status(thm)],[c493, c15])).
% 1.32/1.54  cnf(c857,plain,skolem0001!=X871|unisex(X871,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c529, reflexivity])).
% 1.32/1.54  cnf(c393,plain,cash(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c392, c149])).
% 1.32/1.54  cnf(c535,plain,skolem0001!=X867|skolem0010(skolem0001,skolem0007)!=X866|cash(X867,X866),inference(resolution,[status(thm)],[c39, c393])).
% 1.32/1.54  cnf(c856,plain,skolem0001!=X870|cash(X870,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c535, reflexivity])).
% 1.32/1.54  cnf(c492,plain,specific(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c473, c194])).
% 1.32/1.54  cnf(c528,plain,skolem0001!=X862|skolem0008(skolem0010(skolem0001,skolem0007))!=X863|specific(X862,X863),inference(resolution,[status(thm)],[c492, c18])).
% 1.32/1.54  cnf(c853,plain,skolem0001!=X865|specific(X865,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c528, reflexivity])).
% 1.32/1.54  fof(ax43,axiom,(![U]:(![V]:(cash(U,V)=>currency(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax43)).
% 1.32/1.54  fof(c150,plain,(![U]:(![V]:(~cash(U,V)|currency(U,V)))),inference(fof_nnf,[status(thm)],[ax43])).
% 1.32/1.54  fof(c151,plain,(![X56]:(![X57]:(~cash(X56,X57)|currency(X56,X57)))),inference(variable_rename,[status(thm)],[c150])).
% 1.32/1.54  cnf(c152,plain,~cash(X182,X181)|currency(X182,X181),inference(split_conjunct,[status(thm)],[c151])).
% 1.32/1.54  cnf(c394,plain,currency(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c393, c152])).
% 1.32/1.54  cnf(c38,axiom,X426!=X427|X428!=X425|~currency(X426,X428)|currency(X427,X425),theory(equality)).
% 1.32/1.54  cnf(c527,plain,skolem0001!=X861|skolem0010(skolem0001,skolem0007)!=X860|currency(X861,X860),inference(resolution,[status(thm)],[c38, c394])).
% 1.32/1.54  cnf(c852,plain,skolem0001!=X864|currency(X864,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c527, reflexivity])).
% 1.32/1.54  cnf(c491,plain,nonexistent(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c473, c197])).
% 1.32/1.54  cnf(c521,plain,skolem0001!=X856|skolem0008(skolem0010(skolem0001,skolem0007))!=X857|nonexistent(X856,X857),inference(resolution,[status(thm)],[c491, c28])).
% 1.32/1.54  cnf(c849,plain,skolem0001!=X859|nonexistent(X859,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c521, reflexivity])).
% 1.32/1.54  cnf(c378,plain,currency(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c376, c152])).
% 1.32/1.54  cnf(c526,plain,skolem0001!=X855|skolem0009(skolem0001,skolem0007)!=X854|currency(X855,X854),inference(resolution,[status(thm)],[c38, c378])).
% 1.32/1.54  cnf(c848,plain,skolem0001!=X858|currency(X858,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c526, reflexivity])).
% 1.32/1.54  cnf(c27,axiom,X381!=X382|X383!=X380|~eventuality(X381,X383)|eventuality(X382,X380),theory(equality)).
% 1.32/1.54  cnf(c519,plain,skolem0001!=X851|skolem0008(skolem0009(skolem0001,skolem0007))!=X850|eventuality(X851,X850),inference(resolution,[status(thm)],[c490, c27])).
% 1.32/1.54  cnf(c845,plain,skolem0001!=X853|eventuality(X853,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c519, reflexivity])).
% 1.32/1.54  cnf(c426,plain,currency(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c425, c152])).
% 1.32/1.54  cnf(c525,plain,skolem0001!=X849|skolem0012(skolem0001,skolem0007)!=X848|currency(X849,X848),inference(resolution,[status(thm)],[c38, c426])).
% 1.32/1.54  cnf(c844,plain,skolem0001!=X852|currency(X852,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c525, reflexivity])).
% 1.32/1.54  cnf(c514,plain,skolem0001!=X845|skolem0008(skolem0013(skolem0001,skolem0007))!=X844|eventuality(X845,X844),inference(resolution,[status(thm)],[c488, c27])).
% 1.32/1.54  cnf(c841,plain,skolem0001!=X847|eventuality(X847,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c514, reflexivity])).
% 1.32/1.54  cnf(c410,plain,currency(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c409, c152])).
% 1.32/1.54  cnf(c524,plain,skolem0001!=X843|skolem0011(skolem0001,skolem0007)!=X842|currency(X843,X842),inference(resolution,[status(thm)],[c38, c410])).
% 1.32/1.54  cnf(c840,plain,skolem0001!=X846|currency(X846,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c524, reflexivity])).
% 1.32/1.54  cnf(c509,plain,skolem0001!=X839|skolem0008(skolem0011(skolem0001,skolem0007))!=X838|eventuality(X839,X838),inference(resolution,[status(thm)],[c486, c27])).
% 1.32/1.54  cnf(c837,plain,skolem0001!=X841|eventuality(X841,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c509, reflexivity])).
% 1.32/1.54  cnf(c442,plain,currency(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c441, c152])).
% 1.32/1.54  cnf(c523,plain,skolem0001!=X837|skolem0013(skolem0001,skolem0007)!=X836|currency(X837,X836),inference(resolution,[status(thm)],[c38, c442])).
% 1.32/1.54  cnf(c836,plain,skolem0001!=X840|currency(X840,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c523, reflexivity])).
% 1.32/1.54  cnf(c504,plain,skolem0001!=X833|skolem0008(skolem0012(skolem0001,skolem0007))!=X832|eventuality(X833,X832),inference(resolution,[status(thm)],[c484, c27])).
% 1.32/1.54  cnf(c833,plain,skolem0001!=X835|eventuality(X835,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c504, reflexivity])).
% 1.32/1.54  fof(ax42,axiom,(![U]:(![V]:(currency(U,V)=>possession(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax42)).
% 1.32/1.54  fof(c153,plain,(![U]:(![V]:(~currency(U,V)|possession(U,V)))),inference(fof_nnf,[status(thm)],[ax42])).
% 1.32/1.54  fof(c154,plain,(![X58]:(![X59]:(~currency(X58,X59)|possession(X58,X59)))),inference(variable_rename,[status(thm)],[c153])).
% 1.32/1.54  cnf(c155,plain,~currency(X183,X184)|possession(X183,X184),inference(split_conjunct,[status(thm)],[c154])).
% 1.32/1.54  cnf(c443,plain,possession(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c442, c155])).
% 1.32/1.54  cnf(c37,axiom,X422!=X423|X424!=X421|~possession(X422,X424)|possession(X423,X421),theory(equality)).
% 1.32/1.54  cnf(c500,plain,skolem0001!=X831|skolem0013(skolem0001,skolem0007)!=X830|possession(X831,X830),inference(resolution,[status(thm)],[c37, c443])).
% 1.32/1.54  cnf(c832,plain,skolem0001!=X834|possession(X834,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c500, reflexivity])).
% 1.32/1.54  cnf(c494,plain,skolem0001!=X827|skolem0008(skolem0010(skolem0001,skolem0007))!=X826|eventuality(X827,X826),inference(resolution,[status(thm)],[c473, c27])).
% 1.32/1.54  cnf(c829,plain,skolem0001!=X829|eventuality(X829,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c494, reflexivity])).
% 1.32/1.54  cnf(c395,plain,possession(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c394, c155])).
% 1.32/1.54  cnf(c499,plain,skolem0001!=X825|skolem0010(skolem0001,skolem0007)!=X824|possession(X825,X824),inference(resolution,[status(thm)],[c37, c395])).
% 1.32/1.54  cnf(c828,plain,skolem0001!=X828|possession(X828,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c499, reflexivity])).
% 1.32/1.54  cnf(c25,axiom,X373!=X374|X375!=X372|~event(X373,X375)|event(X374,X372),theory(equality)).
% 1.32/1.54  cnf(c489,plain,skolem0001!=X821|skolem0008(skolem0009(skolem0001,skolem0007))!=X820|event(X821,X820),inference(resolution,[status(thm)],[c471, c25])).
% 1.32/1.54  cnf(c825,plain,skolem0001!=X823|event(X823,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c489, reflexivity])).
% 1.32/1.54  cnf(c379,plain,possession(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c378, c155])).
% 1.32/1.54  cnf(c498,plain,skolem0001!=X819|skolem0009(skolem0001,skolem0007)!=X818|possession(X819,X818),inference(resolution,[status(thm)],[c37, c379])).
% 1.32/1.54  cnf(c824,plain,skolem0001!=X822|possession(X822,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c498, reflexivity])).
% 1.32/1.54  cnf(c487,plain,skolem0001!=X815|skolem0008(skolem0013(skolem0001,skolem0007))!=X814|event(X815,X814),inference(resolution,[status(thm)],[c470, c25])).
% 1.32/1.54  cnf(c821,plain,skolem0001!=X817|event(X817,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c487, reflexivity])).
% 1.32/1.54  cnf(c411,plain,possession(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c410, c155])).
% 1.32/1.54  cnf(c497,plain,skolem0001!=X813|skolem0011(skolem0001,skolem0007)!=X812|possession(X813,X812),inference(resolution,[status(thm)],[c37, c411])).
% 1.32/1.54  cnf(c820,plain,skolem0001!=X816|possession(X816,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c497, reflexivity])).
% 1.32/1.54  cnf(c485,plain,skolem0001!=X809|skolem0008(skolem0011(skolem0001,skolem0007))!=X808|event(X809,X808),inference(resolution,[status(thm)],[c469, c25])).
% 1.32/1.54  cnf(c817,plain,skolem0001!=X811|event(X811,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c485, reflexivity])).
% 1.32/1.54  cnf(c427,plain,possession(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c426, c155])).
% 1.32/1.54  cnf(c496,plain,skolem0001!=X807|skolem0012(skolem0001,skolem0007)!=X806|possession(X807,X806),inference(resolution,[status(thm)],[c37, c427])).
% 1.32/1.54  cnf(c816,plain,skolem0001!=X810|possession(X810,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c496, reflexivity])).
% 1.32/1.54  cnf(c483,plain,skolem0001!=X803|skolem0008(skolem0012(skolem0001,skolem0007))!=X802|event(X803,X802),inference(resolution,[status(thm)],[c468, c25])).
% 1.32/1.54  cnf(c813,plain,skolem0001!=X805|event(X805,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c483, reflexivity])).
% 1.32/1.54  fof(ax40,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax40)).
% 1.32/1.54  fof(c159,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax40])).
% 1.32/1.54  fof(c160,plain,(![X62]:(![X63]:(~abstraction(X62,X63)|thing(X62,X63)))),inference(variable_rename,[status(thm)],[c159])).
% 1.32/1.54  cnf(c161,plain,~abstraction(X191,X192)|thing(X191,X192),inference(split_conjunct,[status(thm)],[c160])).
% 1.32/1.54  fof(ax41,axiom,(![U]:(![V]:(possession(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax41)).
% 1.32/1.54  fof(c156,plain,(![U]:(![V]:(~possession(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax41])).
% 1.32/1.54  fof(c157,plain,(![X60]:(![X61]:(~possession(X60,X61)|abstraction(X60,X61)))),inference(variable_rename,[status(thm)],[c156])).
% 1.32/1.54  cnf(c158,plain,~possession(X189,X190)|abstraction(X189,X190),inference(split_conjunct,[status(thm)],[c157])).
% 1.32/1.54  cnf(c396,plain,abstraction(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c395, c158])).
% 1.32/1.54  cnf(c400,plain,thing(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c396, c161])).
% 1.32/1.54  cnf(c405,plain,singleton(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c400, c164])).
% 1.32/1.54  cnf(c481,plain,skolem0001!=X801|skolem0010(skolem0001,skolem0007)!=X800|singleton(X801,X800),inference(resolution,[status(thm)],[c36, c405])).
% 1.32/1.54  cnf(c812,plain,skolem0001!=X804|singleton(X804,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c481, reflexivity])).
% 1.32/1.54  cnf(c428,plain,abstraction(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c427, c158])).
% 1.32/1.54  cnf(c431,plain,thing(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c428, c161])).
% 1.32/1.54  cnf(c437,plain,singleton(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c431, c164])).
% 1.32/1.54  cnf(c477,plain,skolem0001!=X797|skolem0012(skolem0001,skolem0007)!=X796|singleton(X797,X796),inference(resolution,[status(thm)],[c36, c437])).
% 1.32/1.54  cnf(c809,plain,skolem0001!=X799|singleton(X799,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c477, reflexivity])).
% 1.32/1.54  cnf(c449,plain,abstraction(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c443, c158])).
% 1.32/1.54  cnf(c452,plain,thing(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c449, c161])).
% 1.32/1.54  cnf(c458,plain,singleton(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c452, c164])).
% 1.32/1.54  cnf(c476,plain,skolem0001!=X795|skolem0013(skolem0001,skolem0007)!=X794|singleton(X795,X794),inference(resolution,[status(thm)],[c36, c458])).
% 1.32/1.54  cnf(c808,plain,skolem0001!=X798|singleton(X798,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c476, reflexivity])).
% 1.32/1.54  cnf(c412,plain,abstraction(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c411, c158])).
% 1.32/1.54  cnf(c415,plain,thing(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c412, c161])).
% 1.32/1.54  cnf(c421,plain,singleton(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c415, c164])).
% 1.32/1.54  cnf(c475,plain,skolem0001!=X791|skolem0011(skolem0001,skolem0007)!=X790|singleton(X791,X790),inference(resolution,[status(thm)],[c36, c421])).
% 1.32/1.54  cnf(c805,plain,skolem0001!=X793|singleton(X793,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c475, reflexivity])).
% 1.32/1.54  cnf(c380,plain,abstraction(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c379, c158])).
% 1.32/1.54  cnf(c383,plain,thing(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c380, c161])).
% 1.32/1.54  cnf(c389,plain,singleton(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c383, c164])).
% 1.32/1.54  cnf(c474,plain,skolem0001!=X789|skolem0009(skolem0001,skolem0007)!=X788|singleton(X789,X788),inference(resolution,[status(thm)],[c36, c389])).
% 1.32/1.54  cnf(c804,plain,skolem0001!=X792|singleton(X792,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c474, reflexivity])).
% 1.32/1.54  cnf(c472,plain,skolem0001!=X785|skolem0008(skolem0010(skolem0001,skolem0007))!=X784|event(X785,X784),inference(resolution,[status(thm)],[c467, c25])).
% 1.32/1.54  cnf(c801,plain,skolem0001!=X787|event(X787,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c472, reflexivity])).
% 1.32/1.54  fof(ax36,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax36)).
% 1.32/1.54  fof(c171,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax36])).
% 1.32/1.54  fof(c172,plain,(![X70]:(![X71]:(~abstraction(X70,X71)|unisex(X70,X71)))),inference(variable_rename,[status(thm)],[c171])).
% 1.32/1.54  cnf(c173,plain,~abstraction(X204,X203)|unisex(X204,X203),inference(split_conjunct,[status(thm)],[c172])).
% 1.32/1.54  cnf(c453,plain,unisex(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c449, c173])).
% 1.32/1.54  cnf(c466,plain,skolem0001!=X782|skolem0013(skolem0001,skolem0007)!=X783|unisex(X782,X783),inference(resolution,[status(thm)],[c453, c15])).
% 1.32/1.54  cnf(c800,plain,skolem0001!=X786|unisex(X786,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c466, reflexivity])).
% 1.32/1.54  fof(ax38,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax38)).
% 1.32/1.54  fof(c165,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax38])).
% 1.32/1.54  fof(c166,plain,(![X66]:(![X67]:(~abstraction(X66,X67)|nonhuman(X66,X67)))),inference(variable_rename,[status(thm)],[c165])).
% 1.32/1.54  cnf(c167,plain,~abstraction(X196,X195)|nonhuman(X196,X195),inference(split_conjunct,[status(thm)],[c166])).
% 1.32/1.54  cnf(c413,plain,nonhuman(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c412, c167])).
% 1.32/1.54  cnf(c35,axiom,X413!=X414|X415!=X412|~nonhuman(X413,X415)|nonhuman(X414,X412),theory(equality)).
% 1.32/1.54  cnf(c465,plain,skolem0001!=X778|skolem0011(skolem0001,skolem0007)!=X779|nonhuman(X778,X779),inference(resolution,[status(thm)],[c35, c413])).
% 1.32/1.54  cnf(c797,plain,skolem0001!=X781|nonhuman(X781,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c465, reflexivity])).
% 1.32/1.54  cnf(c450,plain,nonhuman(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c449, c167])).
% 1.32/1.54  cnf(c464,plain,skolem0001!=X776|skolem0013(skolem0001,skolem0007)!=X777|nonhuman(X776,X777),inference(resolution,[status(thm)],[c35, c450])).
% 1.32/1.54  cnf(c796,plain,skolem0001!=X780|nonhuman(X780,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c464, reflexivity])).
% 1.32/1.54  cnf(c398,plain,nonhuman(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c396, c167])).
% 1.32/1.54  cnf(c462,plain,skolem0001!=X772|skolem0010(skolem0001,skolem0007)!=X773|nonhuman(X772,X773),inference(resolution,[status(thm)],[c35, c398])).
% 1.32/1.54  cnf(c793,plain,skolem0001!=X775|nonhuman(X775,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c462, reflexivity])).
% 1.32/1.54  cnf(c381,plain,nonhuman(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c380, c167])).
% 1.32/1.54  cnf(c461,plain,skolem0001!=X770|skolem0009(skolem0001,skolem0007)!=X771|nonhuman(X770,X771),inference(resolution,[status(thm)],[c35, c381])).
% 1.32/1.54  cnf(c792,plain,skolem0001!=X774|nonhuman(X774,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c461, reflexivity])).
% 1.32/1.54  cnf(c429,plain,nonhuman(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c428, c167])).
% 1.32/1.54  cnf(c460,plain,skolem0001!=X764|skolem0012(skolem0001,skolem0007)!=X765|nonhuman(X764,X765),inference(resolution,[status(thm)],[c35, c429])).
% 1.32/1.54  cnf(c790,plain,skolem0001!=X766|nonhuman(X766,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c460, reflexivity])).
% 1.32/1.54  cnf(c457,plain,skolem0001!=X759|skolem0013(skolem0001,skolem0007)!=X760|thing(X759,X760),inference(resolution,[status(thm)],[c452, c19])).
% 1.32/1.54  cnf(c786,plain,skolem0001!=X763|thing(X763,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c457, reflexivity])).
% 1.32/1.54  cnf(c34,axiom,X409!=X410|X411!=X408|~general(X409,X411)|general(X410,X408),theory(equality)).
% 1.32/1.54  fof(ax37,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax37)).
% 1.32/1.54  fof(c168,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax37])).
% 1.32/1.54  fof(c169,plain,(![X68]:(![X69]:(~abstraction(X68,X69)|general(X68,X69)))),inference(variable_rename,[status(thm)],[c168])).
% 1.32/1.54  cnf(c170,plain,~abstraction(X197,X198)|general(X197,X198),inference(split_conjunct,[status(thm)],[c169])).
% 1.32/1.54  cnf(c451,plain,general(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c449, c170])).
% 1.32/1.54  cnf(c455,plain,skolem0001!=X755|skolem0013(skolem0001,skolem0007)!=X756|general(X755,X756),inference(resolution,[status(thm)],[c451, c34])).
% 1.32/1.54  cnf(c783,plain,skolem0001!=X762|general(X762,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c455, reflexivity])).
% 1.32/1.54  cnf(c12,axiom,X270!=X271|X272!=X269|~abstraction(X270,X272)|abstraction(X271,X269),theory(equality)).
% 1.32/1.54  cnf(c454,plain,skolem0001!=X751|skolem0013(skolem0001,skolem0007)!=X750|abstraction(X751,X750),inference(resolution,[status(thm)],[c449, c12])).
% 1.32/1.54  cnf(c779,plain,skolem0001!=X761|abstraction(X761,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c454, reflexivity])).
% 1.32/1.54  cnf(c414,plain,general(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c412, c170])).
% 1.32/1.54  cnf(c448,plain,skolem0001!=X746|skolem0011(skolem0001,skolem0007)!=X747|general(X746,X747),inference(resolution,[status(thm)],[c34, c414])).
% 1.32/1.54  cnf(c776,plain,skolem0001!=X758|general(X758,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c448, reflexivity])).
% 1.32/1.54  cnf(c399,plain,general(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c396, c170])).
% 1.32/1.54  cnf(c447,plain,skolem0001!=X741|skolem0010(skolem0001,skolem0007)!=X742|general(X741,X742),inference(resolution,[status(thm)],[c34, c399])).
% 1.32/1.54  cnf(c772,plain,skolem0001!=X757|general(X757,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c447, reflexivity])).
% 1.32/1.54  cnf(c430,plain,general(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c428, c170])).
% 1.32/1.54  cnf(c446,plain,skolem0001!=X737|skolem0012(skolem0001,skolem0007)!=X738|general(X737,X738),inference(resolution,[status(thm)],[c34, c430])).
% 1.32/1.54  cnf(c769,plain,skolem0001!=X754|general(X754,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c446, reflexivity])).
% 1.32/1.54  cnf(c382,plain,general(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c380, c170])).
% 1.32/1.54  cnf(c444,plain,skolem0001!=X732|skolem0009(skolem0001,skolem0007)!=X733|general(X732,X733),inference(resolution,[status(thm)],[c34, c382])).
% 1.32/1.54  cnf(c765,plain,skolem0001!=X753|general(X753,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c444, reflexivity])).
% 1.32/1.54  cnf(c432,plain,unisex(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c428, c173])).
% 1.32/1.54  cnf(c438,plain,skolem0001!=X729|skolem0012(skolem0001,skolem0007)!=X730|unisex(X729,X730),inference(resolution,[status(thm)],[c432, c15])).
% 1.32/1.54  cnf(c760,plain,skolem0001!=X752|unisex(X752,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c438, reflexivity])).
% 1.32/1.54  cnf(c436,plain,skolem0001!=X724|skolem0012(skolem0001,skolem0007)!=X725|thing(X724,X725),inference(resolution,[status(thm)],[c431, c19])).
% 1.32/1.54  cnf(c755,plain,skolem0001!=X749|thing(X749,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c436, reflexivity])).
% 1.32/1.54  cnf(c433,plain,skolem0001!=X719|skolem0012(skolem0001,skolem0007)!=X718|abstraction(X719,X718),inference(resolution,[status(thm)],[c428, c12])).
% 1.32/1.54  cnf(c751,plain,skolem0001!=X748|abstraction(X748,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c433, reflexivity])).
% 1.32/1.54  cnf(c416,plain,unisex(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c412, c173])).
% 1.32/1.54  cnf(c422,plain,skolem0001!=X711|skolem0011(skolem0001,skolem0007)!=X712|unisex(X711,X712),inference(resolution,[status(thm)],[c416, c15])).
% 1.32/1.54  cnf(c747,plain,skolem0001!=X745|unisex(X745,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c422, reflexivity])).
% 1.32/1.54  cnf(c420,plain,skolem0001!=X703|skolem0011(skolem0001,skolem0007)!=X704|thing(X703,X704),inference(resolution,[status(thm)],[c415, c19])).
% 1.32/1.54  cnf(c742,plain,skolem0001!=X744|thing(X744,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c420, reflexivity])).
% 1.32/1.54  cnf(c417,plain,skolem0001!=X698|skolem0011(skolem0001,skolem0007)!=X697|abstraction(X698,X697),inference(resolution,[status(thm)],[c412, c12])).
% 1.32/1.54  cnf(c738,plain,skolem0001!=X743|abstraction(X743,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c417, reflexivity])).
% 1.32/1.54  cnf(c401,plain,unisex(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c396, c173])).
% 1.32/1.54  cnf(c406,plain,skolem0001!=X690|skolem0010(skolem0001,skolem0007)!=X691|unisex(X690,X691),inference(resolution,[status(thm)],[c401, c15])).
% 1.32/1.54  cnf(c734,plain,skolem0001!=X740|unisex(X740,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c406, reflexivity])).
% 1.32/1.54  cnf(c404,plain,skolem0001!=X682|skolem0010(skolem0001,skolem0007)!=X683|thing(X682,X683),inference(resolution,[status(thm)],[c400, c19])).
% 1.32/1.54  cnf(c729,plain,skolem0001!=X739|thing(X739,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c404, reflexivity])).
% 1.32/1.54  cnf(c402,plain,skolem0001!=X677|skolem0010(skolem0001,skolem0007)!=X676|abstraction(X677,X676),inference(resolution,[status(thm)],[c396, c12])).
% 1.32/1.54  cnf(c725,plain,skolem0001!=X736|abstraction(X736,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c402, reflexivity])).
% 1.32/1.54  cnf(c384,plain,unisex(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c380, c173])).
% 1.32/1.54  cnf(c390,plain,skolem0001!=X669|skolem0009(skolem0001,skolem0007)!=X670|unisex(X669,X670),inference(resolution,[status(thm)],[c384, c15])).
% 1.32/1.54  cnf(c721,plain,skolem0001!=X735|unisex(X735,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c390, reflexivity])).
% 1.32/1.54  cnf(c388,plain,skolem0001!=X661|skolem0009(skolem0001,skolem0007)!=X662|thing(X661,X662),inference(resolution,[status(thm)],[c383, c19])).
% 1.32/1.54  cnf(c716,plain,skolem0001!=X734|thing(X734,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c388, reflexivity])).
% 1.32/1.54  cnf(c385,plain,skolem0001!=X656|skolem0009(skolem0001,skolem0007)!=X655|abstraction(X656,X655),inference(resolution,[status(thm)],[c380, c12])).
% 1.32/1.54  cnf(c712,plain,skolem0001!=X731|abstraction(X731,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c385, reflexivity])).
% 1.32/1.54  cnf(c66,negated_conjecture,nonreflexive(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c584,plain,skolem0001!=X726|skolem0006!=X727|nonreflexive(X726,X727),inference(resolution,[status(thm)],[c45, c66])).
% 1.32/1.54  cnf(c756,plain,skolem0001!=X728|nonreflexive(X728,skolem0006),inference(resolution,[status(thm)],[c584, reflexivity])).
% 1.32/1.54  cnf(c65,negated_conjecture,past(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  cnf(c42,axiom,X442!=X443|X444!=X441|~past(X442,X444)|past(X443,X441),theory(equality)).
% 1.32/1.54  cnf(c566,plain,skolem0001!=X721|skolem0006!=X722|past(X721,X722),inference(resolution,[status(thm)],[c42, c65])).
% 1.32/1.54  cnf(c753,plain,skolem0001!=X723|past(X723,skolem0006),inference(resolution,[status(thm)],[c566, reflexivity])).
% 1.32/1.54  cnf(c61,negated_conjecture,shake_beverage(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.54  fof(ax23,axiom,(![U]:(![V]:(shake_beverage(U,V)=>beverage(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax23)).
% 1.32/1.54  fof(c210,plain,(![U]:(![V]:(~shake_beverage(U,V)|beverage(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 1.32/1.54  fof(c211,plain,(![X96]:(![X97]:(~shake_beverage(X96,X97)|beverage(X96,X97)))),inference(variable_rename,[status(thm)],[c210])).
% 1.32/1.54  cnf(c212,plain,~shake_beverage(X250,X249)|beverage(X250,X249),inference(split_conjunct,[status(thm)],[c211])).
% 1.32/1.54  cnf(c299,plain,beverage(skolem0001,skolem0005),inference(resolution,[status(thm)],[c212, c61])).
% 1.32/1.54  fof(ax22,axiom,(![U]:(![V]:(beverage(U,V)=>food(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax22)).
% 1.32/1.54  fof(c213,plain,(![U]:(![V]:(~beverage(U,V)|food(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 1.32/1.54  fof(c214,plain,(![X98]:(![X99]:(~beverage(X98,X99)|food(X98,X99)))),inference(variable_rename,[status(thm)],[c213])).
% 1.32/1.54  cnf(c215,plain,~beverage(X251,X252)|food(X251,X252),inference(split_conjunct,[status(thm)],[c214])).
% 1.32/1.54  cnf(c300,plain,food(skolem0001,skolem0005),inference(resolution,[status(thm)],[c215, c299])).
% 1.32/1.54  fof(ax21,axiom,(![U]:(![V]:(food(U,V)=>substance_matter(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 1.32/1.54  fof(c216,plain,(![U]:(![V]:(~food(U,V)|substance_matter(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 1.32/1.54  fof(c217,plain,(![X100]:(![X101]:(~food(X100,X101)|substance_matter(X100,X101)))),inference(variable_rename,[status(thm)],[c216])).
% 1.32/1.54  cnf(c218,plain,~food(X258,X257)|substance_matter(X258,X257),inference(split_conjunct,[status(thm)],[c217])).
% 1.32/1.54  cnf(c302,plain,substance_matter(skolem0001,skolem0005),inference(resolution,[status(thm)],[c218, c300])).
% 1.32/1.54  fof(ax20,axiom,(![U]:(![V]:(substance_matter(U,V)=>object(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 1.32/1.54  fof(c219,plain,(![U]:(![V]:(~substance_matter(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 1.32/1.54  fof(c220,plain,(![X102]:(![X103]:(~substance_matter(X102,X103)|object(X102,X103)))),inference(variable_rename,[status(thm)],[c219])).
% 1.32/1.54  cnf(c221,plain,~substance_matter(X259,X260)|object(X259,X260),inference(split_conjunct,[status(thm)],[c220])).
% 1.32/1.55  cnf(c303,plain,object(skolem0001,skolem0005),inference(resolution,[status(thm)],[c221, c302])).
% 1.32/1.55  fof(ax19,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax19)).
% 1.32/1.55  fof(c222,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 1.32/1.55  fof(c223,plain,(![X104]:(![X105]:(~object(X104,X105)|entity(X104,X105)))),inference(variable_rename,[status(thm)],[c222])).
% 1.32/1.55  cnf(c224,plain,~object(X265,X266)|entity(X265,X266),inference(split_conjunct,[status(thm)],[c223])).
% 1.32/1.55  cnf(c304,plain,entity(skolem0001,skolem0005),inference(resolution,[status(thm)],[c224, c303])).
% 1.32/1.55  fof(ax18,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 1.32/1.55  fof(c225,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 1.32/1.55  fof(c226,plain,(![X106]:(![X107]:(~entity(X106,X107)|thing(X106,X107)))),inference(variable_rename,[status(thm)],[c225])).
% 1.32/1.55  cnf(c227,plain,~entity(X268,X267)|thing(X268,X267),inference(split_conjunct,[status(thm)],[c226])).
% 1.32/1.55  cnf(c306,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c227, c304])).
% 1.32/1.55  cnf(c307,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c306, c164])).
% 1.32/1.55  cnf(c482,plain,skolem0001!=X717|skolem0005!=X716|singleton(X717,X716),inference(resolution,[status(thm)],[c36, c307])).
% 1.32/1.55  cnf(c750,plain,skolem0001!=X720|singleton(X720,skolem0005),inference(resolution,[status(thm)],[c482, reflexivity])).
% 1.32/1.55  cnf(c60,negated_conjecture,forename(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  fof(ax12,axiom,(![U]:(![V]:(forename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax12)).
% 1.32/1.55  fof(c243,plain,(![U]:(![V]:(~forename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 1.32/1.55  fof(c244,plain,(![X118]:(![X119]:(~forename(X118,X119)|relname(X118,X119)))),inference(variable_rename,[status(thm)],[c243])).
% 1.32/1.55  cnf(c245,plain,~forename(X292,X291)|relname(X292,X291),inference(split_conjunct,[status(thm)],[c244])).
% 1.32/1.55  cnf(c316,plain,relname(skolem0001,skolem0004),inference(resolution,[status(thm)],[c245, c60])).
% 1.32/1.55  fof(ax11,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax11)).
% 1.32/1.55  fof(c246,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 1.32/1.55  fof(c247,plain,(![X120]:(![X121]:(~relname(X120,X121)|relation(X120,X121)))),inference(variable_rename,[status(thm)],[c246])).
% 1.32/1.55  cnf(c248,plain,~relname(X294,X293)|relation(X294,X293),inference(split_conjunct,[status(thm)],[c247])).
% 1.32/1.55  cnf(c318,plain,relation(skolem0001,skolem0004),inference(resolution,[status(thm)],[c248, c316])).
% 1.32/1.55  fof(ax10,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax10)).
% 1.32/1.55  fof(c249,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 1.32/1.55  fof(c250,plain,(![X122]:(![X123]:(~relation(X122,X123)|abstraction(X122,X123)))),inference(variable_rename,[status(thm)],[c249])).
% 1.32/1.55  cnf(c251,plain,~relation(X299,X300)|abstraction(X299,X300),inference(split_conjunct,[status(thm)],[c250])).
% 1.32/1.55  cnf(c322,plain,abstraction(skolem0001,skolem0004),inference(resolution,[status(thm)],[c251, c318])).
% 1.32/1.55  cnf(c325,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c322, c161])).
% 1.32/1.55  cnf(c329,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c325, c164])).
% 1.32/1.55  cnf(c480,plain,skolem0001!=X714|skolem0004!=X713|singleton(X714,X713),inference(resolution,[status(thm)],[c36, c329])).
% 1.32/1.55  cnf(c748,plain,skolem0001!=X715|singleton(X715,skolem0004),inference(resolution,[status(thm)],[c480, reflexivity])).
% 1.32/1.55  cnf(c58,negated_conjecture,woman(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  fof(ax8,axiom,(![U]:(![V]:(woman(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax8)).
% 1.32/1.55  fof(c255,plain,(![U]:(![V]:(~woman(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 1.32/1.55  fof(c256,plain,(![X126]:(![X127]:(~woman(X126,X127)|human_person(X126,X127)))),inference(variable_rename,[status(thm)],[c255])).
% 1.32/1.55  cnf(c257,plain,~woman(X312,X311)|human_person(X312,X311),inference(split_conjunct,[status(thm)],[c256])).
% 1.32/1.55  cnf(c334,plain,human_person(skolem0001,skolem0003),inference(resolution,[status(thm)],[c257, c58])).
% 1.32/1.55  fof(ax7,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax7)).
% 1.32/1.55  fof(c258,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 1.32/1.55  fof(c259,plain,(![X128]:(![X129]:(~human_person(X128,X129)|organism(X128,X129)))),inference(variable_rename,[status(thm)],[c258])).
% 1.32/1.55  cnf(c260,plain,~human_person(X314,X313)|organism(X314,X313),inference(split_conjunct,[status(thm)],[c259])).
% 1.32/1.55  cnf(c336,plain,organism(skolem0001,skolem0003),inference(resolution,[status(thm)],[c260, c334])).
% 1.32/1.55  fof(ax6,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax6)).
% 1.32/1.55  fof(c261,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 1.32/1.55  fof(c262,plain,(![X130]:(![X131]:(~organism(X130,X131)|entity(X130,X131)))),inference(variable_rename,[status(thm)],[c261])).
% 1.32/1.55  cnf(c263,plain,~organism(X316,X315)|entity(X316,X315),inference(split_conjunct,[status(thm)],[c262])).
% 1.32/1.55  cnf(c338,plain,entity(skolem0001,skolem0003),inference(resolution,[status(thm)],[c263, c336])).
% 1.32/1.55  cnf(c344,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c338, c227])).
% 1.32/1.55  cnf(c347,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c344, c164])).
% 1.32/1.55  cnf(c479,plain,skolem0001!=X709|skolem0003!=X708|singleton(X709,X708),inference(resolution,[status(thm)],[c36, c347])).
% 1.32/1.55  cnf(c745,plain,skolem0001!=X710|singleton(X710,skolem0003),inference(resolution,[status(thm)],[c479, reflexivity])).
% 1.32/1.55  cnf(c62,negated_conjecture,event(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  cnf(c288,plain,eventuality(skolem0001,skolem0006),inference(resolution,[status(thm)],[c188, c62])).
% 1.32/1.55  cnf(c289,plain,thing(skolem0001,skolem0006),inference(resolution,[status(thm)],[c191, c288])).
% 1.32/1.55  cnf(c290,plain,singleton(skolem0001,skolem0006),inference(resolution,[status(thm)],[c289, c164])).
% 1.32/1.55  cnf(c478,plain,skolem0001!=X706|skolem0006!=X705|singleton(X706,X705),inference(resolution,[status(thm)],[c36, c290])).
% 1.32/1.55  cnf(c743,plain,skolem0001!=X707|singleton(X707,skolem0006),inference(resolution,[status(thm)],[c478, reflexivity])).
% 1.32/1.55  cnf(c323,plain,nonhuman(skolem0001,skolem0004),inference(resolution,[status(thm)],[c322, c167])).
% 1.32/1.55  cnf(c463,plain,skolem0001!=X700|skolem0004!=X701|nonhuman(X700,X701),inference(resolution,[status(thm)],[c35, c323])).
% 1.32/1.55  cnf(c740,plain,skolem0001!=X702|nonhuman(X702,skolem0004),inference(resolution,[status(thm)],[c463, reflexivity])).
% 1.32/1.55  cnf(c56,negated_conjecture,nonhuman(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  cnf(c459,plain,skolem0001!=X695|skolem0002!=X696|nonhuman(X695,X696),inference(resolution,[status(thm)],[c35, c56])).
% 1.32/1.55  cnf(c737,plain,skolem0001!=X699|nonhuman(X699,skolem0002),inference(resolution,[status(thm)],[c459, reflexivity])).
% 1.32/1.55  cnf(c324,plain,general(skolem0001,skolem0004),inference(resolution,[status(thm)],[c322, c170])).
% 1.32/1.55  cnf(c445,plain,skolem0001!=X692|skolem0004!=X693|general(X692,X693),inference(resolution,[status(thm)],[c34, c324])).
% 1.32/1.55  cnf(c735,plain,skolem0001!=X694|general(X694,skolem0004),inference(resolution,[status(thm)],[c445, reflexivity])).
% 1.32/1.55  cnf(c75,negated_conjecture,group(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  fof(ax35,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax35)).
% 1.32/1.55  fof(c174,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 1.32/1.55  fof(c175,plain,(![X72]:(![X73]:(~group(X72,X73)|set(X72,X73)))),inference(variable_rename,[status(thm)],[c174])).
% 1.32/1.55  cnf(c176,plain,~group(X205,X206)|set(X205,X206),inference(split_conjunct,[status(thm)],[c175])).
% 1.32/1.55  cnf(c284,plain,set(skolem0001,skolem0007),inference(resolution,[status(thm)],[c176, c75])).
% 1.32/1.55  fof(ax34,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax34)).
% 1.32/1.55  fof(c177,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 1.32/1.55  fof(c178,plain,(![X74]:(![X75]:(~set(X74,X75)|multiple(X74,X75)))),inference(variable_rename,[status(thm)],[c177])).
% 1.32/1.55  cnf(c179,plain,~set(X208,X207)|multiple(X208,X207),inference(split_conjunct,[status(thm)],[c178])).
% 1.32/1.55  cnf(c285,plain,multiple(skolem0001,skolem0007),inference(resolution,[status(thm)],[c179, c284])).
% 1.32/1.55  cnf(c33,axiom,X405!=X406|X407!=X404|~multiple(X405,X407)|multiple(X406,X404),theory(equality)).
% 1.32/1.55  cnf(c439,plain,skolem0001!=X688|skolem0007!=X687|multiple(X688,X687),inference(resolution,[status(thm)],[c33, c285])).
% 1.32/1.55  cnf(c732,plain,skolem0001!=X689|multiple(X689,skolem0007),inference(resolution,[status(thm)],[c439, reflexivity])).
% 1.32/1.55  cnf(c32,axiom,X401!=X402|X403!=X400|~set(X401,X403)|set(X402,X400),theory(equality)).
% 1.32/1.55  cnf(c434,plain,skolem0001!=X684|skolem0007!=X685|set(X684,X685),inference(resolution,[status(thm)],[c32, c284])).
% 1.32/1.55  cnf(c730,plain,skolem0001!=X686|set(X686,skolem0007),inference(resolution,[status(thm)],[c434, reflexivity])).
% 1.32/1.55  cnf(c31,axiom,X397!=X398|X399!=X396|~group(X397,X399)|group(X398,X396),theory(equality)).
% 1.32/1.55  cnf(c424,plain,skolem0001!=X680|skolem0007!=X679|group(X680,X679),inference(resolution,[status(thm)],[c31, c75])).
% 1.32/1.55  cnf(c727,plain,skolem0001!=X681|group(X681,skolem0007),inference(resolution,[status(thm)],[c424, reflexivity])).
% 1.32/1.55  cnf(c30,axiom,X393!=X394|X395!=X392|~five(X393,X395)|five(X394,X392),theory(equality)).
% 1.32/1.55  cnf(c419,plain,skolem0001!=X675|skolem0007!=X674|five(X675,X674),inference(resolution,[status(thm)],[c30, c74])).
% 1.32/1.55  cnf(c724,plain,skolem0001!=X678|five(X678,skolem0007),inference(resolution,[status(thm)],[c419, reflexivity])).
% 1.32/1.55  cnf(c292,plain,nonexistent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c197, c288])).
% 1.32/1.55  cnf(c407,plain,skolem0001!=X671|skolem0006!=X672|nonexistent(X671,X672),inference(resolution,[status(thm)],[c28, c292])).
% 1.32/1.55  cnf(c722,plain,skolem0001!=X673|nonexistent(X673,skolem0006),inference(resolution,[status(thm)],[c407, reflexivity])).
% 1.32/1.55  cnf(c397,plain,skolem0001!=X667|skolem0006!=X666|eventuality(X667,X666),inference(resolution,[status(thm)],[c27, c288])).
% 1.32/1.55  cnf(c719,plain,skolem0001!=X668|eventuality(X668,skolem0006),inference(resolution,[status(thm)],[c397, reflexivity])).
% 1.32/1.55  cnf(c67,negated_conjecture,order(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  fof(ax26,axiom,(![U]:(![V]:(order(U,V)=>act(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax26)).
% 1.32/1.55  fof(c201,plain,(![U]:(![V]:(~order(U,V)|act(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 1.32/1.55  fof(c202,plain,(![X90]:(![X91]:(~order(X90,X91)|act(X90,X91)))),inference(variable_rename,[status(thm)],[c201])).
% 1.32/1.55  cnf(c203,plain,~order(X240,X239)|act(X240,X239),inference(split_conjunct,[status(thm)],[c202])).
% 1.32/1.55  cnf(c295,plain,act(skolem0001,skolem0006),inference(resolution,[status(thm)],[c203, c67])).
% 1.32/1.55  cnf(c26,axiom,X377!=X378|X379!=X376|~act(X377,X379)|act(X378,X376),theory(equality)).
% 1.32/1.55  cnf(c391,plain,skolem0001!=X663|skolem0006!=X664|act(X663,X664),inference(resolution,[status(thm)],[c26, c295])).
% 1.32/1.55  cnf(c717,plain,skolem0001!=X665|act(X665,skolem0006),inference(resolution,[status(thm)],[c391, reflexivity])).
% 1.32/1.55  cnf(c386,plain,skolem0001!=X659|skolem0006!=X658|event(X659,X658),inference(resolution,[status(thm)],[c25, c62])).
% 1.32/1.55  cnf(c714,plain,skolem0001!=X660|event(X660,skolem0006),inference(resolution,[status(thm)],[c386, reflexivity])).
% 1.32/1.55  cnf(c24,axiom,X369!=X370|X371!=X368|~order(X369,X371)|order(X370,X368),theory(equality)).
% 1.32/1.55  cnf(c377,plain,skolem0001!=X653|skolem0006!=X654|order(X653,X654),inference(resolution,[status(thm)],[c24, c67])).
% 1.32/1.55  cnf(c711,plain,skolem0001!=X657|order(X657,skolem0006),inference(resolution,[status(thm)],[c377, reflexivity])).
% 1.32/1.55  cnf(c23,axiom,X359!=X360|X361!=X358|~shake_beverage(X359,X361)|shake_beverage(X360,X358),theory(equality)).
% 1.32/1.55  cnf(c371,plain,skolem0001!=X650|skolem0005!=X649|shake_beverage(X650,X649),inference(resolution,[status(thm)],[c23, c61])).
% 1.32/1.55  cnf(c708,plain,skolem0001!=X652|shake_beverage(X652,skolem0005),inference(resolution,[status(thm)],[c371, reflexivity])).
% 1.32/1.55  cnf(c22,axiom,X347!=X348|X349!=X346|~beverage(X347,X349)|beverage(X348,X346),theory(equality)).
% 1.32/1.55  cnf(c367,plain,skolem0001!=X648|skolem0005!=X647|beverage(X648,X647),inference(resolution,[status(thm)],[c22, c299])).
% 1.32/1.55  cnf(c707,plain,skolem0001!=X651|beverage(X651,skolem0005),inference(resolution,[status(thm)],[c367, reflexivity])).
% 1.32/1.55  cnf(c1,axiom,X160!=X161|X162!=X159|~female(X160,X162)|female(X161,X159),theory(equality)).
% 1.32/1.55  fof(ax1,axiom,(![U]:(![V]:(woman(U,V)=>female(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 1.32/1.55  fof(c276,plain,(![U]:(![V]:(~woman(U,V)|female(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 1.32/1.55  fof(c277,plain,(![X140]:(![X141]:(~woman(X140,X141)|female(X140,X141)))),inference(variable_rename,[status(thm)],[c276])).
% 1.32/1.55  cnf(c278,plain,~woman(X341,X342)|female(X341,X342),inference(split_conjunct,[status(thm)],[c277])).
% 1.32/1.55  cnf(c364,plain,female(skolem0001,skolem0003),inference(resolution,[status(thm)],[c278, c58])).
% 1.32/1.55  cnf(c365,plain,skolem0001!=X644|skolem0003!=X643|female(X644,X643),inference(resolution,[status(thm)],[c364, c1])).
% 1.32/1.55  cnf(c704,plain,skolem0001!=X646|female(X646,skolem0003),inference(resolution,[status(thm)],[c365, reflexivity])).
% 1.32/1.55  cnf(c21,axiom,X338!=X339|X340!=X337|~food(X338,X340)|food(X339,X337),theory(equality)).
% 1.32/1.55  cnf(c363,plain,skolem0001!=X641|skolem0005!=X642|food(X641,X642),inference(resolution,[status(thm)],[c21, c300])).
% 1.32/1.55  cnf(c703,plain,skolem0001!=X645|food(X645,skolem0005),inference(resolution,[status(thm)],[c363, reflexivity])).
% 1.32/1.55  cnf(c3,axiom,X186!=X187|X188!=X185|~animate(X186,X188)|animate(X187,X185),theory(equality)).
% 1.32/1.55  fof(ax2,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 1.32/1.55  fof(c273,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 1.32/1.55  fof(c274,plain,(![X138]:(![X139]:(~human_person(X138,X139)|animate(X138,X139)))),inference(variable_rename,[status(thm)],[c273])).
% 1.32/1.55  cnf(c275,plain,~human_person(X336,X335)|animate(X336,X335),inference(split_conjunct,[status(thm)],[c274])).
% 1.32/1.55  cnf(c361,plain,animate(skolem0001,skolem0003),inference(resolution,[status(thm)],[c275, c334])).
% 1.32/1.55  cnf(c362,plain,skolem0001!=X637|skolem0003!=X638|animate(X637,X638),inference(resolution,[status(thm)],[c361, c3])).
% 1.32/1.55  cnf(c700,plain,skolem0001!=X640|animate(X640,skolem0003),inference(resolution,[status(thm)],[c362, reflexivity])).
% 1.32/1.55  cnf(c4,axiom,X200!=X201|X202!=X199|~human(X200,X202)|human(X201,X199),theory(equality)).
% 1.32/1.55  fof(ax3,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 1.32/1.55  fof(c270,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 1.32/1.55  fof(c271,plain,(![X136]:(![X137]:(~human_person(X136,X137)|human(X136,X137)))),inference(variable_rename,[status(thm)],[c270])).
% 1.32/1.55  cnf(c272,plain,~human_person(X333,X334)|human(X333,X334),inference(split_conjunct,[status(thm)],[c271])).
% 1.32/1.55  cnf(c358,plain,human(skolem0001,skolem0003),inference(resolution,[status(thm)],[c272, c334])).
% 1.32/1.55  cnf(c360,plain,skolem0001!=X636|skolem0003!=X635|human(X636,X635),inference(resolution,[status(thm)],[c358, c4])).
% 1.32/1.55  cnf(c699,plain,skolem0001!=X639|human(X639,skolem0003),inference(resolution,[status(thm)],[c360, reflexivity])).
% 1.32/1.55  cnf(c20,axiom,X330!=X331|X332!=X329|~substance_matter(X330,X332)|substance_matter(X331,X329),theory(equality)).
% 1.32/1.55  cnf(c357,plain,skolem0001!=X631|skolem0005!=X632|substance_matter(X631,X632),inference(resolution,[status(thm)],[c20, c302])).
% 1.32/1.55  cnf(c696,plain,skolem0001!=X634|substance_matter(X634,skolem0005),inference(resolution,[status(thm)],[c357, reflexivity])).
% 1.32/1.55  cnf(c6,axiom,X220!=X221|X222!=X219|~living(X220,X222)|living(X221,X219),theory(equality)).
% 1.32/1.55  fof(ax4,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 1.32/1.55  fof(c267,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 1.32/1.55  fof(c268,plain,(![X134]:(![X135]:(~organism(X134,X135)|living(X134,X135)))),inference(variable_rename,[status(thm)],[c267])).
% 1.32/1.55  cnf(c269,plain,~organism(X328,X327)|living(X328,X327),inference(split_conjunct,[status(thm)],[c268])).
% 1.32/1.55  cnf(c354,plain,living(skolem0001,skolem0003),inference(resolution,[status(thm)],[c269, c336])).
% 1.32/1.55  cnf(c355,plain,skolem0001!=X629|skolem0003!=X630|living(X629,X630),inference(resolution,[status(thm)],[c354, c6])).
% 1.32/1.55  cnf(c695,plain,skolem0001!=X633|living(X633,skolem0003),inference(resolution,[status(thm)],[c355, reflexivity])).
% 1.32/1.55  cnf(c7,axiom,X228!=X229|X230!=X227|~impartial(X228,X230)|impartial(X229,X227),theory(equality)).
% 1.32/1.55  fof(ax5,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax5)).
% 1.32/1.55  fof(c264,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 1.32/1.55  fof(c265,plain,(![X132]:(![X133]:(~organism(X132,X133)|impartial(X132,X133)))),inference(variable_rename,[status(thm)],[c264])).
% 1.32/1.55  cnf(c266,plain,~organism(X325,X326)|impartial(X325,X326),inference(split_conjunct,[status(thm)],[c265])).
% 1.32/1.55  cnf(c352,plain,impartial(skolem0001,skolem0003),inference(resolution,[status(thm)],[c266, c336])).
% 1.32/1.55  cnf(c353,plain,skolem0001!=X626|skolem0003!=X625|impartial(X626,X625),inference(resolution,[status(thm)],[c352, c7])).
% 1.32/1.55  cnf(c692,plain,skolem0001!=X628|impartial(X628,skolem0003),inference(resolution,[status(thm)],[c353, reflexivity])).
% 1.32/1.55  cnf(c351,plain,skolem0001!=X623|skolem0004!=X624|thing(X623,X624),inference(resolution,[status(thm)],[c19, c325])).
% 1.32/1.55  cnf(c691,plain,skolem0001!=X627|thing(X627,skolem0004),inference(resolution,[status(thm)],[c351, reflexivity])).
% 1.32/1.55  cnf(c350,plain,skolem0001!=X619|skolem0006!=X620|thing(X619,X620),inference(resolution,[status(thm)],[c19, c289])).
% 1.32/1.55  cnf(c688,plain,skolem0001!=X622|thing(X622,skolem0006),inference(resolution,[status(thm)],[c350, reflexivity])).
% 1.32/1.55  cnf(c349,plain,skolem0001!=X617|skolem0005!=X618|thing(X617,X618),inference(resolution,[status(thm)],[c19, c306])).
% 1.32/1.55  cnf(c687,plain,skolem0001!=X621|thing(X621,skolem0005),inference(resolution,[status(thm)],[c349, reflexivity])).
% 1.32/1.55  cnf(c348,plain,skolem0001!=X613|skolem0003!=X614|thing(X613,X614),inference(resolution,[status(thm)],[c19, c344])).
% 1.32/1.55  cnf(c684,plain,skolem0001!=X616|thing(X616,skolem0003),inference(resolution,[status(thm)],[c348, reflexivity])).
% 1.32/1.55  cnf(c17,axiom,X308!=X309|X310!=X307|~existent(X308,X310)|existent(X309,X307),theory(equality)).
% 1.32/1.55  fof(ax16,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax16)).
% 1.32/1.55  fof(c231,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 1.32/1.55  fof(c232,plain,(![X110]:(![X111]:(~entity(X110,X111)|existent(X110,X111)))),inference(variable_rename,[status(thm)],[c231])).
% 1.32/1.55  cnf(c233,plain,~entity(X276,X275)|existent(X276,X275),inference(split_conjunct,[status(thm)],[c232])).
% 1.32/1.55  cnf(c343,plain,existent(skolem0001,skolem0003),inference(resolution,[status(thm)],[c338, c233])).
% 1.32/1.55  cnf(c346,plain,skolem0001!=X612|skolem0003!=X611|existent(X612,X611),inference(resolution,[status(thm)],[c343, c17])).
% 1.32/1.55  cnf(c683,plain,skolem0001!=X615|existent(X615,skolem0003),inference(resolution,[status(thm)],[c346, reflexivity])).
% 1.32/1.55  fof(ax17,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax17)).
% 1.32/1.55  fof(c228,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 1.32/1.55  fof(c229,plain,(![X108]:(![X109]:(~entity(X108,X109)|specific(X108,X109)))),inference(variable_rename,[status(thm)],[c228])).
% 1.32/1.55  cnf(c230,plain,~entity(X274,X273)|specific(X274,X273),inference(split_conjunct,[status(thm)],[c229])).
% 1.32/1.55  cnf(c342,plain,specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c338, c230])).
% 1.32/1.55  cnf(c345,plain,skolem0001!=X607|skolem0003!=X608|specific(X607,X608),inference(resolution,[status(thm)],[c342, c18])).
% 1.32/1.55  cnf(c680,plain,skolem0001!=X610|specific(X610,skolem0003),inference(resolution,[status(thm)],[c345, reflexivity])).
% 1.32/1.55  cnf(c8,axiom,X236!=X237|X238!=X235|~entity(X236,X238)|entity(X237,X235),theory(equality)).
% 1.32/1.55  cnf(c341,plain,skolem0001!=X606|skolem0003!=X605|entity(X606,X605),inference(resolution,[status(thm)],[c338, c8])).
% 1.32/1.55  cnf(c679,plain,skolem0001!=X609|entity(X609,skolem0003),inference(resolution,[status(thm)],[c341, reflexivity])).
% 1.32/1.55  cnf(c308,plain,specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c230, c304])).
% 1.32/1.55  cnf(c340,plain,skolem0001!=X601|skolem0005!=X602|specific(X601,X602),inference(resolution,[status(thm)],[c18, c308])).
% 1.32/1.55  cnf(c676,plain,skolem0001!=X604|specific(X604,skolem0005),inference(resolution,[status(thm)],[c340, reflexivity])).
% 1.32/1.55  cnf(c291,plain,specific(skolem0001,skolem0006),inference(resolution,[status(thm)],[c194, c288])).
% 1.32/1.55  cnf(c339,plain,skolem0001!=X599|skolem0006!=X600|specific(X599,X600),inference(resolution,[status(thm)],[c18, c291])).
% 1.32/1.55  cnf(c675,plain,skolem0001!=X603|specific(X603,skolem0006),inference(resolution,[status(thm)],[c339, reflexivity])).
% 1.32/1.55  cnf(c5,axiom,X210!=X211|X212!=X209|~organism(X210,X212)|organism(X211,X209),theory(equality)).
% 1.32/1.55  cnf(c337,plain,skolem0001!=X597|skolem0003!=X596|organism(X597,X596),inference(resolution,[status(thm)],[c336, c5])).
% 1.32/1.55  cnf(c673,plain,skolem0001!=X598|organism(X598,skolem0003),inference(resolution,[status(thm)],[c337, reflexivity])).
% 1.32/1.55  cnf(c2,axiom,X172!=X173|X174!=X171|~human_person(X172,X174)|human_person(X173,X171),theory(equality)).
% 1.32/1.55  cnf(c335,plain,skolem0001!=X589|skolem0003!=X590|human_person(X589,X590),inference(resolution,[status(thm)],[c334, c2])).
% 1.32/1.55  cnf(c669,plain,skolem0001!=X591|human_person(X591,skolem0003),inference(resolution,[status(thm)],[c335, reflexivity])).
% 1.32/1.55  cnf(c309,plain,existent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c233, c304])).
% 1.32/1.55  cnf(c333,plain,skolem0001!=X587|skolem0005!=X586|existent(X587,X586),inference(resolution,[status(thm)],[c17, c309])).
% 1.32/1.55  cnf(c667,plain,skolem0001!=X588|existent(X588,skolem0005),inference(resolution,[status(thm)],[c333, reflexivity])).
% 1.32/1.55  cnf(c326,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c322, c173])).
% 1.32/1.55  cnf(c331,plain,skolem0001!=X579|skolem0004!=X580|unisex(X579,X580),inference(resolution,[status(thm)],[c326, c15])).
% 1.32/1.55  cnf(c664,plain,skolem0001!=X581|unisex(X581,skolem0004),inference(resolution,[status(thm)],[c331, reflexivity])).
% 1.32/1.55  fof(ax15,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax15)).
% 1.32/1.55  fof(c234,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 1.32/1.55  fof(c235,plain,(![X112]:(![X113]:(~object(X112,X113)|nonliving(X112,X113)))),inference(variable_rename,[status(thm)],[c234])).
% 1.32/1.55  cnf(c236,plain,~object(X277,X278)|nonliving(X277,X278),inference(split_conjunct,[status(thm)],[c235])).
% 1.32/1.55  cnf(c310,plain,nonliving(skolem0001,skolem0005),inference(resolution,[status(thm)],[c236, c303])).
% 1.32/1.55  cnf(c16,axiom,X302!=X303|X304!=X301|~nonliving(X302,X304)|nonliving(X303,X301),theory(equality)).
% 1.32/1.55  cnf(c330,plain,skolem0001!=X569|skolem0005!=X570|nonliving(X569,X570),inference(resolution,[status(thm)],[c16, c310])).
% 1.32/1.55  cnf(c662,plain,skolem0001!=X578|nonliving(X578,skolem0005),inference(resolution,[status(thm)],[c330, reflexivity])).
% 1.32/1.55  cnf(c107,plain,~member(X575,X573,X571)|~member(X575,X576,X571)|X576=X573|~member(X575,X577,X571)|X577=X576|X577=X573|~member(X575,X572,X571)|X572=X577|X572=X576|X572=X573|~member(X575,X574,X571)|X574=X572|X574=X577|X574=X576|X574=X573|skolem0014(X575,X571,X573,X576,X577,X572,X574)!=X573|five(X575,X571),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c327,plain,skolem0001!=X567|skolem0004!=X566|abstraction(X567,X566),inference(resolution,[status(thm)],[c322, c12])).
% 1.32/1.55  cnf(c660,plain,skolem0001!=X568|abstraction(X568,skolem0004),inference(resolution,[status(thm)],[c327, reflexivity])).
% 1.32/1.55  cnf(c106,plain,~member(X563,X561,X559)|~member(X563,X564,X559)|X564=X561|~member(X563,X565,X559)|X565=X564|X565=X561|~member(X563,X560,X559)|X560=X565|X560=X564|X560=X561|~member(X563,X562,X559)|X562=X560|X562=X565|X562=X564|X562=X561|skolem0014(X563,X559,X561,X564,X565,X560,X562)!=X564|five(X563,X559),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c294,plain,unisex(skolem0001,skolem0006),inference(resolution,[status(thm)],[c200, c288])).
% 1.32/1.55  cnf(c321,plain,skolem0001!=X556|skolem0006!=X557|unisex(X556,X557),inference(resolution,[status(thm)],[c15, c294])).
% 1.32/1.55  cnf(c658,plain,skolem0001!=X558|unisex(X558,skolem0006),inference(resolution,[status(thm)],[c321, reflexivity])).
% 1.32/1.55  fof(ax13,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax13)).
% 1.32/1.55  fof(c240,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 1.32/1.55  fof(c241,plain,(![X116]:(![X117]:(~object(X116,X117)|unisex(X116,X117)))),inference(variable_rename,[status(thm)],[c240])).
% 1.32/1.55  cnf(c242,plain,~object(X285,X286)|unisex(X285,X286),inference(split_conjunct,[status(thm)],[c241])).
% 1.32/1.55  cnf(c314,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c242, c303])).
% 1.32/1.55  cnf(c320,plain,skolem0001!=X553|skolem0005!=X554|unisex(X553,X554),inference(resolution,[status(thm)],[c15, c314])).
% 1.32/1.55  cnf(c656,plain,skolem0001!=X555|unisex(X555,skolem0005),inference(resolution,[status(thm)],[c320, reflexivity])).
% 1.32/1.55  cnf(c105,plain,~member(X550,X548,X546)|~member(X550,X551,X546)|X551=X548|~member(X550,X552,X546)|X552=X551|X552=X548|~member(X550,X547,X546)|X547=X552|X547=X551|X547=X548|~member(X550,X549,X546)|X549=X547|X549=X552|X549=X551|X549=X548|skolem0014(X550,X546,X548,X551,X552,X547,X549)!=X552|five(X550,X546),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c11,axiom,X262!=X263|X264!=X261|~relation(X262,X264)|relation(X263,X261),theory(equality)).
% 1.32/1.55  cnf(c319,plain,skolem0001!=X544|skolem0004!=X543|relation(X544,X543),inference(resolution,[status(thm)],[c318, c11])).
% 1.32/1.55  cnf(c654,plain,skolem0001!=X545|relation(X545,skolem0004),inference(resolution,[status(thm)],[c319, reflexivity])).
% 1.32/1.55  cnf(c13,axiom,X280!=X281|X282!=X279|~relname(X280,X282)|relname(X281,X279),theory(equality)).
% 1.32/1.55  cnf(c317,plain,skolem0001!=X533|skolem0004!=X534|relname(X533,X534),inference(resolution,[status(thm)],[c316, c13])).
% 1.32/1.55  cnf(c652,plain,skolem0001!=X542|relname(X542,skolem0004),inference(resolution,[status(thm)],[c317, reflexivity])).
% 1.32/1.55  cnf(c104,plain,~member(X539,X537,X535)|~member(X539,X540,X535)|X540=X537|~member(X539,X541,X535)|X541=X540|X541=X537|~member(X539,X536,X535)|X536=X541|X536=X540|X536=X537|~member(X539,X538,X535)|X538=X536|X538=X541|X538=X540|X538=X537|skolem0014(X539,X535,X537,X540,X541,X536,X538)!=X536|five(X539,X535),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c14,axiom,X288!=X289|X290!=X287|~object(X288,X290)|object(X289,X287),theory(equality)).
% 1.32/1.55  cnf(c315,plain,skolem0001!=X530|skolem0005!=X531|object(X530,X531),inference(resolution,[status(thm)],[c14, c303])).
% 1.32/1.55  cnf(c650,plain,skolem0001!=X532|object(X532,skolem0005),inference(resolution,[status(thm)],[c315, reflexivity])).
% 1.32/1.55  cnf(c103,plain,~member(X527,X525,X523)|~member(X527,X528,X523)|X528=X525|~member(X527,X529,X523)|X529=X528|X529=X525|~member(X527,X524,X523)|X524=X529|X524=X528|X524=X525|~member(X527,X526,X523)|X526=X524|X526=X529|X526=X528|X526=X525|skolem0014(X527,X523,X525,X528,X529,X524,X526)!=X526|five(X527,X523),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  fof(ax14,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax14)).
% 1.32/1.55  fof(c237,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 1.32/1.55  fof(c238,plain,(![X114]:(![X115]:(~object(X114,X115)|impartial(X114,X115)))),inference(variable_rename,[status(thm)],[c237])).
% 1.32/1.55  cnf(c239,plain,~object(X284,X283)|impartial(X284,X283),inference(split_conjunct,[status(thm)],[c238])).
% 1.32/1.55  cnf(c312,plain,impartial(skolem0001,skolem0005),inference(resolution,[status(thm)],[c239, c303])).
% 1.32/1.55  cnf(c313,plain,skolem0001!=X521|skolem0005!=X520|impartial(X521,X520),inference(resolution,[status(thm)],[c312, c7])).
% 1.32/1.55  cnf(c648,plain,skolem0001!=X522|impartial(X522,skolem0005),inference(resolution,[status(thm)],[c313, reflexivity])).
% 1.32/1.55  cnf(c305,plain,skolem0001!=X518|skolem0005!=X517|entity(X518,X517),inference(resolution,[status(thm)],[c304, c8])).
% 1.32/1.55  cnf(c646,plain,skolem0001!=X519|entity(X519,skolem0005),inference(resolution,[status(thm)],[c305, reflexivity])).
% 1.32/1.55  cnf(c102,plain,~member(X514,X512,X510)|~member(X514,X515,X510)|X515=X512|~member(X514,X516,X510)|X516=X515|X516=X512|~member(X514,X511,X510)|X511=X516|X511=X515|X511=X512|~member(X514,X513,X510)|X513=X511|X513=X516|X513=X515|X513=X512|member(X514,skolem0014(X514,X510,X512,X515,X516,X511,X513),X510)|five(X514,X510),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c10,axiom,X254!=X255|X256!=X253|~forename(X254,X256)|forename(X255,X253),theory(equality)).
% 1.32/1.55  cnf(c301,plain,skolem0001!=X507|skolem0004!=X508|forename(X507,X508),inference(resolution,[status(thm)],[c10, c60])).
% 1.32/1.55  cnf(c635,plain,skolem0001!=X509|forename(X509,skolem0004),inference(resolution,[status(thm)],[c301, reflexivity])).
% 1.32/1.55  cnf(c59,negated_conjecture,mia_forename(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  cnf(c9,axiom,X244!=X245|X246!=X243|~mia_forename(X244,X246)|mia_forename(X245,X243),theory(equality)).
% 1.32/1.55  cnf(c297,plain,skolem0001!=X501|skolem0004!=X502|mia_forename(X501,X502),inference(resolution,[status(thm)],[c9, c59])).
% 1.32/1.55  cnf(c628,plain,skolem0001!=X506|mia_forename(X506,skolem0004),inference(resolution,[status(thm)],[c297, reflexivity])).
% 1.32/1.55  cnf(c101,plain,~five(X503,X505)|~member(X503,X504,X505)|X504=skolem0013(X503,X505)|X504=skolem0012(X503,X505)|X504=skolem0011(X503,X505)|X504=skolem0010(X503,X505)|X504=skolem0009(X503,X505),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c0,axiom,X152!=X153|X154!=X151|~woman(X152,X154)|woman(X153,X151),theory(equality)).
% 1.32/1.55  cnf(c282,plain,skolem0001!=X498|skolem0003!=X499|woman(X498,X499),inference(resolution,[status(thm)],[c0, c58])).
% 1.32/1.55  cnf(c626,plain,skolem0001!=X500|woman(X500,skolem0003),inference(resolution,[status(thm)],[c282, reflexivity])).
% 1.32/1.55  cnf(c100,plain,~five(X496,X497)|skolem0013(X496,X497)!=skolem0009(X496,X497),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c99,plain,~five(X494,X495)|skolem0013(X494,X495)!=skolem0010(X494,X495),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c98,plain,~five(X492,X493)|skolem0013(X492,X493)!=skolem0011(X492,X493),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c97,plain,~five(X490,X491)|skolem0013(X490,X491)!=skolem0012(X490,X491),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c95,plain,~five(X488,X489)|skolem0012(X488,X489)!=skolem0009(X488,X489),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c94,plain,~five(X486,X487)|skolem0012(X486,X487)!=skolem0010(X486,X487),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c93,plain,~five(X484,X485)|skolem0012(X484,X485)!=skolem0011(X484,X485),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c91,plain,~five(X481,X482)|skolem0011(X481,X482)!=skolem0009(X481,X482),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c90,plain,~five(X479,X480)|skolem0011(X479,X480)!=skolem0010(X479,X480),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  cnf(c88,plain,~five(X477,X478)|skolem0010(X477,X478)!=skolem0009(X477,X478),inference(split_conjunct,[status(thm)],[c85])).
% 1.32/1.55  fof(ax46,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax46)).
% 1.32/1.55  fof(c139,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax46])).
% 1.32/1.55  fof(c140,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c139])).
% 1.32/1.55  fof(c141,plain,(![X50]:(![X51]:(~existent(X50,X51)|~nonexistent(X50,X51)))),inference(variable_rename,[status(thm)],[c140])).
% 1.32/1.55  cnf(c142,plain,~existent(X176,X175)|~nonexistent(X176,X175),inference(split_conjunct,[status(thm)],[c141])).
% 1.32/1.55  cnf(c561,plain,~existent(skolem0001,skolem0008(skolem0009(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c516, c142])).
% 1.32/1.55  cnf(c555,plain,~existent(skolem0001,skolem0008(skolem0013(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c511, c142])).
% 1.32/1.55  cnf(c544,plain,~existent(skolem0001,skolem0008(skolem0011(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c506, c142])).
% 1.32/1.55  cnf(c533,plain,~existent(skolem0001,skolem0008(skolem0012(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c501, c142])).
% 1.32/1.55  cnf(c522,plain,~existent(skolem0001,skolem0008(skolem0010(skolem0001,skolem0007))),inference(resolution,[status(thm)],[c491, c142])).
% 1.32/1.55  fof(ax51,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax51)).
% 1.32/1.55  fof(c119,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax51])).
% 1.32/1.55  fof(c120,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c119])).
% 1.32/1.55  fof(c121,plain,(![X40]:(![X41]:(~specific(X40,X41)|~general(X40,X41)))),inference(variable_rename,[status(thm)],[c120])).
% 1.32/1.55  cnf(c122,plain,~specific(X158,X157)|~general(X158,X157),inference(split_conjunct,[status(thm)],[c121])).
% 1.32/1.55  cnf(c456,plain,~specific(skolem0001,skolem0013(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c451, c122])).
% 1.32/1.55  cnf(c435,plain,~specific(skolem0001,skolem0012(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c430, c122])).
% 1.32/1.55  cnf(c418,plain,~specific(skolem0001,skolem0011(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c414, c122])).
% 1.32/1.55  cnf(c403,plain,~specific(skolem0001,skolem0010(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c399, c122])).
% 1.32/1.55  cnf(c387,plain,~specific(skolem0001,skolem0009(skolem0001,skolem0007)),inference(resolution,[status(thm)],[c382, c122])).
% 1.32/1.55  cnf(c48,axiom,X350!=X351|~actual_world(X350)|actual_world(X351),theory(equality)).
% 1.32/1.55  fof(ax52,axiom,(![U]:(![V]:(unisex(U,V)=>(~female(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax52)).
% 1.32/1.55  fof(c115,plain,(![U]:(![V]:(unisex(U,V)=>~female(U,V)))),inference(fof_simplification,[status(thm)],[ax52])).
% 1.32/1.55  fof(c116,plain,(![U]:(![V]:(~unisex(U,V)|~female(U,V)))),inference(fof_nnf,[status(thm)],[c115])).
% 1.32/1.55  fof(c117,plain,(![X38]:(![X39]:(~unisex(X38,X39)|~female(X38,X39)))),inference(variable_rename,[status(thm)],[c116])).
% 1.32/1.55  cnf(c118,plain,~unisex(X156,X155)|~female(X156,X155),inference(split_conjunct,[status(thm)],[c117])).
% 1.32/1.55  cnf(c366,plain,~unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c364, c118])).
% 1.32/1.55  fof(ax47,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax47)).
% 1.32/1.55  fof(c135,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax47])).
% 1.32/1.55  fof(c136,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c135])).
% 1.32/1.55  fof(c137,plain,(![X48]:(![X49]:(~nonhuman(X48,X49)|~human(X48,X49)))),inference(variable_rename,[status(thm)],[c136])).
% 1.32/1.55  cnf(c138,plain,~nonhuman(X169,X170)|~human(X169,X170),inference(split_conjunct,[status(thm)],[c137])).
% 1.32/1.55  cnf(c359,plain,~nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c358, c138])).
% 1.32/1.55  fof(ax48,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 1.32/1.55  fof(c131,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax48])).
% 1.32/1.55  fof(c132,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c131])).
% 1.32/1.55  fof(c133,plain,(![X46]:(![X47]:(~nonliving(X46,X47)|~living(X46,X47)))),inference(variable_rename,[status(thm)],[c132])).
% 1.32/1.55  cnf(c134,plain,~nonliving(X167,X168)|~living(X167,X168),inference(split_conjunct,[status(thm)],[c133])).
% 1.32/1.55  cnf(c356,plain,~nonliving(skolem0001,skolem0003),inference(resolution,[status(thm)],[c354, c134])).
% 1.32/1.55  fof(ax9,axiom,(![U]:(![V]:(mia_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax9)).
% 1.32/1.55  fof(c252,plain,(![U]:(![V]:(~mia_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 1.32/1.55  fof(c253,plain,(![X124]:(![X125]:(~mia_forename(X124,X125)|forename(X124,X125)))),inference(variable_rename,[status(thm)],[c252])).
% 1.32/1.55  cnf(c254,plain,~mia_forename(X306,X305)|forename(X306,X305),inference(split_conjunct,[status(thm)],[c253])).
% 1.32/1.55  cnf(c328,plain,~specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c324, c122])).
% 1.32/1.55  fof(ax45,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax45)).
% 1.32/1.55  fof(c143,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax45])).
% 1.32/1.55  fof(c144,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c143])).
% 1.32/1.55  fof(c145,plain,(![X52]:(![X53]:(~animate(X52,X53)|~nonliving(X52,X53)))),inference(variable_rename,[status(thm)],[c144])).
% 1.32/1.55  cnf(c146,plain,~animate(X177,X178)|~nonliving(X177,X178),inference(split_conjunct,[status(thm)],[c145])).
% 1.32/1.55  cnf(c311,plain,~animate(skolem0001,skolem0005),inference(resolution,[status(thm)],[c310, c146])).
% 1.32/1.55  fof(ax24,axiom,(![U]:(![V]:(order(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax24)).
% 1.32/1.55  fof(c207,plain,(![U]:(![V]:(~order(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 1.32/1.55  fof(c208,plain,(![X94]:(![X95]:(~order(X94,X95)|event(X94,X95)))),inference(variable_rename,[status(thm)],[c207])).
% 1.32/1.55  cnf(c209,plain,~order(X248,X247)|event(X248,X247),inference(split_conjunct,[status(thm)],[c208])).
% 1.32/1.55  fof(ax25,axiom,(![U]:(![V]:(act(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax25)).
% 1.32/1.55  fof(c204,plain,(![U]:(![V]:(~act(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 1.32/1.55  fof(c205,plain,(![X92]:(![X93]:(~act(X92,X93)|event(X92,X93)))),inference(variable_rename,[status(thm)],[c204])).
% 1.32/1.55  cnf(c206,plain,~act(X242,X241)|event(X242,X241),inference(split_conjunct,[status(thm)],[c205])).
% 1.32/1.55  cnf(c293,plain,~existent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c292, c142])).
% 1.32/1.55  fof(ax32,axiom,(![U]:(![V]:(cost(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax32)).
% 1.32/1.55  fof(c183,plain,(![U]:(![V]:(~cost(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 1.32/1.55  fof(c184,plain,(![X78]:(![X79]:(~cost(X78,X79)|event(X78,X79)))),inference(variable_rename,[status(thm)],[c183])).
% 1.32/1.55  cnf(c185,plain,~cost(X215,X216)|event(X215,X216),inference(split_conjunct,[status(thm)],[c184])).
% 1.32/1.55  fof(ax33,axiom,(![U]:(![V]:(five(U,V)=>group(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax33)).
% 1.32/1.55  fof(c180,plain,(![U]:(![V]:(~five(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 1.32/1.55  fof(c181,plain,(![X76]:(![X77]:(~five(X76,X77)|group(X76,X77)))),inference(variable_rename,[status(thm)],[c180])).
% 1.32/1.55  cnf(c182,plain,~five(X213,X214)|group(X213,X214),inference(split_conjunct,[status(thm)],[c181])).
% 1.32/1.55  fof(ax50,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax50)).
% 1.32/1.55  fof(c123,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax50])).
% 1.32/1.55  fof(c124,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c123])).
% 1.32/1.55  fof(c125,plain,(![X42]:(![X43]:(~singleton(X42,X43)|~multiple(X42,X43)))),inference(variable_rename,[status(thm)],[c124])).
% 1.32/1.55  cnf(c126,plain,~singleton(X164,X163)|~multiple(X164,X163),inference(split_conjunct,[status(thm)],[c125])).
% 1.32/1.55  cnf(c286,plain,~singleton(skolem0001,skolem0007),inference(resolution,[status(thm)],[c285, c126])).
% 1.32/1.55  fof(ax49,axiom,(![U]:(![V]:(present(U,V)=>(~past(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 1.32/1.55  fof(c127,plain,(![U]:(![V]:(present(U,V)=>~past(U,V)))),inference(fof_simplification,[status(thm)],[ax49])).
% 1.32/1.55  fof(c128,plain,(![U]:(![V]:(~present(U,V)|~past(U,V)))),inference(fof_nnf,[status(thm)],[c127])).
% 1.32/1.55  fof(c129,plain,(![X44]:(![X45]:(~present(X44,X45)|~past(X44,X45)))),inference(variable_rename,[status(thm)],[c128])).
% 1.32/1.55  cnf(c130,plain,~present(X165,X166)|~past(X165,X166),inference(split_conjunct,[status(thm)],[c129])).
% 1.32/1.55  cnf(c283,plain,~present(skolem0001,skolem0006),inference(resolution,[status(thm)],[c130, c65])).
% 1.32/1.55  cnf(transitivity,axiom,X149!=X148|X148!=X150|X149=X150,theory(equality)).
% 1.32/1.55  cnf(symmetry,axiom,X146!=X145|X145=X146,theory(equality)).
% 1.32/1.55  fof(ax56,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax56)).
% 1.32/1.55  fof(c77,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax56])).
% 1.32/1.55  fof(c78,plain,(![X12]:(![X13]:~member(X12,X13,X13))),inference(variable_rename,[status(thm)],[c77])).
% 1.32/1.55  cnf(c79,plain,~member(X143,X144,X144),inference(split_conjunct,[status(thm)],[c78])).
% 1.32/1.55  cnf(c55,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c54])).
% 1.32/1.55  % SZS output end Saturation
% 1.32/1.55  
% 1.32/1.55  % Initial clauses    : 151
% 1.32/1.55  % Processed clauses  : 701
% 1.32/1.55  % Factors computed   : 6
% 1.32/1.55  % Resolvents computed: 743
% 1.32/1.55  % Tautologies deleted: 3
% 1.32/1.55  % Forward subsumed   : 196
% 1.32/1.55  % Backward subsumed  : 5
% 1.32/1.55  % -------- CPU Time ---------
% 1.32/1.55  % User time          : 1.125 s
% 1.32/1.55  % System time        : 0.021 s
% 1.32/1.55  % Total time         : 1.146 s
%------------------------------------------------------------------------------