%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP077+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:57 EDT 2024
% Result : CounterSatisfiable 1.67s 1.83s
% Output : Saturation 1.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NLP077+1 : TPTP v8.1.2. Released v2.4.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 13:31:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.67/1.83 % Version: 1.5
% 1.67/1.83 % SZS status CounterSatisfiable
% 1.67/1.83 % SZS output start Saturation
% 1.67/1.83 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:((((![W]:(![X]:(((((male(U,W)&man(U,W))&of(U,X,W))&cannon(U,X))&member(U,X,V))=>(?[Y]:((((((event(U,Y)&agent(U,Y,W))&patient(U,Y,X))&present(U,Y))&nonreflexive(U,Y))&fire(U,Y))&from_loc(U,Y,X))))))&six(U,V))&group(U,V))&(![Z]:(member(U,Z,V)=>shot(U,Z)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 1.67/1.83 fof(c40,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:((((![W]:(![X]:(((((male(U,W)&man(U,W))&of(U,X,W))&cannon(U,X))&member(U,X,V))=>(?[Y]:((((((event(U,Y)&agent(U,Y,W))&patient(U,Y,X))&present(U,Y))&nonreflexive(U,Y))&fire(U,Y))&from_loc(U,Y,X))))))&six(U,V))&group(U,V))&(![Z]:(member(U,Z,V)=>shot(U,Z))))))))),inference(assume_negation,[status(cth)],[co1])).
% 1.67/1.83 fof(c41,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:((((![W]:(![X]:(((((~male(U,W)|~man(U,W))|~of(U,X,W))|~cannon(U,X))|~member(U,X,V))|(?[Y]:((((((event(U,Y)&agent(U,Y,W))&patient(U,Y,X))&present(U,Y))&nonreflexive(U,Y))&fire(U,Y))&from_loc(U,Y,X))))))&six(U,V))&group(U,V))&(![Z]:(~member(U,Z,V)|shot(U,Z))))))),inference(fof_nnf,[status(thm)],[c40])).
% 1.67/1.83 fof(c42,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:((((![X4]:(![X5]:(((((~male(X2,X4)|~man(X2,X4))|~of(X2,X5,X4))|~cannon(X2,X5))|~member(X2,X5,X3))|(?[X6]:((((((event(X2,X6)&agent(X2,X6,X4))&patient(X2,X6,X5))&present(X2,X6))&nonreflexive(X2,X6))&fire(X2,X6))&from_loc(X2,X6,X5))))))&six(X2,X3))&group(X2,X3))&(![X7]:(~member(X2,X7,X3)|shot(X2,X7))))))),inference(variable_rename,[status(thm)],[c41])).
% 1.67/1.83 fof(c44,negated_conjecture,(![X4]:(![X5]:(![X7]:(actual_world(skolem0001)&((((((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|((((((event(skolem0001,skolem0003(X4,X5))&agent(skolem0001,skolem0003(X4,X5),X4))&patient(skolem0001,skolem0003(X4,X5),X5))&present(skolem0001,skolem0003(X4,X5)))&nonreflexive(skolem0001,skolem0003(X4,X5)))&fire(skolem0001,skolem0003(X4,X5)))&from_loc(skolem0001,skolem0003(X4,X5),X5)))&six(skolem0001,skolem0002))&group(skolem0001,skolem0002))&(~member(skolem0001,X7,skolem0002)|shot(skolem0001,X7))))))),inference(shift_quantors,[status(thm)],[fof(c43,negated_conjecture,(actual_world(skolem0001)&((((![X4]:(![X5]:(((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|((((((event(skolem0001,skolem0003(X4,X5))&agent(skolem0001,skolem0003(X4,X5),X4))&patient(skolem0001,skolem0003(X4,X5),X5))&present(skolem0001,skolem0003(X4,X5)))&nonreflexive(skolem0001,skolem0003(X4,X5)))&fire(skolem0001,skolem0003(X4,X5)))&from_loc(skolem0001,skolem0003(X4,X5),X5)))))&six(skolem0001,skolem0002))&group(skolem0001,skolem0002))&(![X7]:(~member(skolem0001,X7,skolem0002)|shot(skolem0001,X7))))),inference(skolemize,[status(esa)],[c42])).])).
% 1.67/1.83 fof(c45,negated_conjecture,(![X4]:(![X5]:(![X7]:(actual_world(skolem0001)&((((((((((((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|event(skolem0001,skolem0003(X4,X5)))&(((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|agent(skolem0001,skolem0003(X4,X5),X4)))&(((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|patient(skolem0001,skolem0003(X4,X5),X5)))&(((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|present(skolem0001,skolem0003(X4,X5))))&(((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|nonreflexive(skolem0001,skolem0003(X4,X5))))&(((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|fire(skolem0001,skolem0003(X4,X5))))&(((((~male(skolem0001,X4)|~man(skolem0001,X4))|~of(skolem0001,X5,X4))|~cannon(skolem0001,X5))|~member(skolem0001,X5,skolem0002))|from_loc(skolem0001,skolem0003(X4,X5),X5)))&six(skolem0001,skolem0002))&group(skolem0001,skolem0002))&(~member(skolem0001,X7,skolem0002)|shot(skolem0001,X7))))))),inference(distribute,[status(thm)],[c44])).
% 1.67/1.83 cnf(c54,negated_conjecture,six(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.83 fof(ax40,axiom,(![U]:(![V]:(six(U,V)<=>(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(?[Z]:((((member(U,Z,V)&Z!=Y)&Z!=X)&Z!=W)&(?[X1]:(((((member(U,X1,V)&X1!=Z)&X1!=Y)&X1!=X)&X1!=W)&(?[X2]:((((((member(U,X2,V)&X2!=X1)&X2!=Z)&X2!=Y)&X2!=X)&X2!=W)&(![X3]:(member(U,X3,V)=>(((((X3=X2|X3=X1)|X3=Z)|X3=Y)|X3=X)|X3=W)))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 1.67/1.83 fof(c60,plain,(![U]:(![V]:((~six(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(?[Z]:((((member(U,Z,V)&Z!=Y)&Z!=X)&Z!=W)&(?[X1]:(((((member(U,X1,V)&X1!=Z)&X1!=Y)&X1!=X)&X1!=W)&(?[X2]:((((((member(U,X2,V)&X2!=X1)&X2!=Z)&X2!=Y)&X2!=X)&X2!=W)&(![X3]:(~member(U,X3,V)|(((((X3=X2|X3=X1)|X3=Z)|X3=Y)|X3=X)|X3=W))))))))))))))))&((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(![Y]:(((~member(U,Y,V)|Y=X)|Y=W)|(![Z]:((((~member(U,Z,V)|Z=Y)|Z=X)|Z=W)|(![X1]:(((((~member(U,X1,V)|X1=Z)|X1=Y)|X1=X)|X1=W)|(![X2]:((((((~member(U,X2,V)|X2=X1)|X2=Z)|X2=Y)|X2=X)|X2=W)|(?[X3]:(member(U,X3,V)&(((((X3!=X2&X3!=X1)&X3!=Z)&X3!=Y)&X3!=X)&X3!=W)))))))))))))))|six(U,V))))),inference(fof_nnf,[status(thm)],[ax40])).
% 1.67/1.83 fof(c61,plain,((![U]:(![V]:(~six(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(?[Z]:((((member(U,Z,V)&Z!=Y)&Z!=X)&Z!=W)&(?[X1]:(((((member(U,X1,V)&X1!=Z)&X1!=Y)&X1!=X)&X1!=W)&(?[X2]:((((((member(U,X2,V)&X2!=X1)&X2!=Z)&X2!=Y)&X2!=X)&X2!=W)&(![X3]:(~member(U,X3,V)|(((((X3=X2|X3=X1)|X3=Z)|X3=Y)|X3=X)|X3=W))))))))))))))))))&(![U]:(![V]:((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(![Y]:(((~member(U,Y,V)|Y=X)|Y=W)|(![Z]:((((~member(U,Z,V)|Z=Y)|Z=X)|Z=W)|(![X1]:(((((~member(U,X1,V)|X1=Z)|X1=Y)|X1=X)|X1=W)|(![X2]:((((((~member(U,X2,V)|X2=X1)|X2=Z)|X2=Y)|X2=X)|X2=W)|(?[X3]:(member(U,X3,V)&(((((X3!=X2&X3!=X1)&X3!=Z)&X3!=Y)&X3!=X)&X3!=W)))))))))))))))|six(U,V))))),inference(shift_quantors,[status(thm)],[c60])).
% 1.67/1.83 fof(c62,plain,((![X10]:(![X11]:(~six(X10,X11)|(?[X12]:(member(X10,X12,X11)&(?[X13]:((member(X10,X13,X11)&X13!=X12)&(?[X14]:(((member(X10,X14,X11)&X14!=X13)&X14!=X12)&(?[X15]:((((member(X10,X15,X11)&X15!=X14)&X15!=X13)&X15!=X12)&(?[X16]:(((((member(X10,X16,X11)&X16!=X15)&X16!=X14)&X16!=X13)&X16!=X12)&(?[X17]:((((((member(X10,X17,X11)&X17!=X16)&X17!=X15)&X17!=X14)&X17!=X13)&X17!=X12)&(![X18]:(~member(X10,X18,X11)|(((((X18=X17|X18=X16)|X18=X15)|X18=X14)|X18=X13)|X18=X12))))))))))))))))))&(![X19]:(![X20]:((![X21]:(~member(X19,X21,X20)|(![X22]:((~member(X19,X22,X20)|X22=X21)|(![X23]:(((~member(X19,X23,X20)|X23=X22)|X23=X21)|(![X24]:((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(![X25]:(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|(![X26]:((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|(?[X27]:(member(X19,X27,X20)&(((((X27!=X26&X27!=X25)&X27!=X24)&X27!=X23)&X27!=X22)&X27!=X21)))))))))))))))|six(X19,X20))))),inference(variable_rename,[status(thm)],[c61])).
% 1.67/1.83 fof(c64,plain,(![X10]:(![X11]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((~six(X10,X11)|(member(X10,skolem0004(X10,X11),X11)&((member(X10,skolem0005(X10,X11),X11)&skolem0005(X10,X11)!=skolem0004(X10,X11))&(((member(X10,skolem0006(X10,X11),X11)&skolem0006(X10,X11)!=skolem0005(X10,X11))&skolem0006(X10,X11)!=skolem0004(X10,X11))&((((member(X10,skolem0007(X10,X11),X11)&skolem0007(X10,X11)!=skolem0006(X10,X11))&skolem0007(X10,X11)!=skolem0005(X10,X11))&skolem0007(X10,X11)!=skolem0004(X10,X11))&(((((member(X10,skolem0008(X10,X11),X11)&skolem0008(X10,X11)!=skolem0007(X10,X11))&skolem0008(X10,X11)!=skolem0006(X10,X11))&skolem0008(X10,X11)!=skolem0005(X10,X11))&skolem0008(X10,X11)!=skolem0004(X10,X11))&((((((member(X10,skolem0009(X10,X11),X11)&skolem0009(X10,X11)!=skolem0008(X10,X11))&skolem0009(X10,X11)!=skolem0007(X10,X11))&skolem0009(X10,X11)!=skolem0006(X10,X11))&skolem0009(X10,X11)!=skolem0005(X10,X11))&skolem0009(X10,X11)!=skolem0004(X10,X11))&(~member(X10,X18,X11)|(((((X18=skolem0009(X10,X11)|X18=skolem0008(X10,X11))|X18=skolem0007(X10,X11))|X18=skolem0006(X10,X11))|X18=skolem0005(X10,X11))|X18=skolem0004(X10,X11))))))))))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|(member(X19,skolem0010(X19,X20,X21,X22,X23,X24,X25,X26),X20)&(((((skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X26&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X25)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X24)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X23)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X22)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X21))))))))|six(X19,X20)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X10]:(![X11]:(~six(X10,X11)|(member(X10,skolem0004(X10,X11),X11)&((member(X10,skolem0005(X10,X11),X11)&skolem0005(X10,X11)!=skolem0004(X10,X11))&(((member(X10,skolem0006(X10,X11),X11)&skolem0006(X10,X11)!=skolem0005(X10,X11))&skolem0006(X10,X11)!=skolem0004(X10,X11))&((((member(X10,skolem0007(X10,X11),X11)&skolem0007(X10,X11)!=skolem0006(X10,X11))&skolem0007(X10,X11)!=skolem0005(X10,X11))&skolem0007(X10,X11)!=skolem0004(X10,X11))&(((((member(X10,skolem0008(X10,X11),X11)&skolem0008(X10,X11)!=skolem0007(X10,X11))&skolem0008(X10,X11)!=skolem0006(X10,X11))&skolem0008(X10,X11)!=skolem0005(X10,X11))&skolem0008(X10,X11)!=skolem0004(X10,X11))&((((((member(X10,skolem0009(X10,X11),X11)&skolem0009(X10,X11)!=skolem0008(X10,X11))&skolem0009(X10,X11)!=skolem0007(X10,X11))&skolem0009(X10,X11)!=skolem0006(X10,X11))&skolem0009(X10,X11)!=skolem0005(X10,X11))&skolem0009(X10,X11)!=skolem0004(X10,X11))&(![X18]:(~member(X10,X18,X11)|(((((X18=skolem0009(X10,X11)|X18=skolem0008(X10,X11))|X18=skolem0007(X10,X11))|X18=skolem0006(X10,X11))|X18=skolem0005(X10,X11))|X18=skolem0004(X10,X11)))))))))))))&(![X19]:(![X20]:((![X21]:(~member(X19,X21,X20)|(![X22]:((~member(X19,X22,X20)|X22=X21)|(![X23]:(((~member(X19,X23,X20)|X23=X22)|X23=X21)|(![X24]:((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(![X25]:(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|(![X26]:((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|(member(X19,skolem0010(X19,X20,X21,X22,X23,X24,X25,X26),X20)&(((((skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X26&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X25)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X24)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X23)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X22)&skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X21))))))))))))))|six(X19,X20))))),inference(skolemize,[status(esa)],[c62])).])).
% 1.67/1.83 fof(c65,plain,(![X10]:(![X11]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(((~six(X10,X11)|member(X10,skolem0004(X10,X11),X11))&(((~six(X10,X11)|member(X10,skolem0005(X10,X11),X11))&(~six(X10,X11)|skolem0005(X10,X11)!=skolem0004(X10,X11)))&((((~six(X10,X11)|member(X10,skolem0006(X10,X11),X11))&(~six(X10,X11)|skolem0006(X10,X11)!=skolem0005(X10,X11)))&(~six(X10,X11)|skolem0006(X10,X11)!=skolem0004(X10,X11)))&(((((~six(X10,X11)|member(X10,skolem0007(X10,X11),X11))&(~six(X10,X11)|skolem0007(X10,X11)!=skolem0006(X10,X11)))&(~six(X10,X11)|skolem0007(X10,X11)!=skolem0005(X10,X11)))&(~six(X10,X11)|skolem0007(X10,X11)!=skolem0004(X10,X11)))&((((((~six(X10,X11)|member(X10,skolem0008(X10,X11),X11))&(~six(X10,X11)|skolem0008(X10,X11)!=skolem0007(X10,X11)))&(~six(X10,X11)|skolem0008(X10,X11)!=skolem0006(X10,X11)))&(~six(X10,X11)|skolem0008(X10,X11)!=skolem0005(X10,X11)))&(~six(X10,X11)|skolem0008(X10,X11)!=skolem0004(X10,X11)))&(((((((~six(X10,X11)|member(X10,skolem0009(X10,X11),X11))&(~six(X10,X11)|skolem0009(X10,X11)!=skolem0008(X10,X11)))&(~six(X10,X11)|skolem0009(X10,X11)!=skolem0007(X10,X11)))&(~six(X10,X11)|skolem0009(X10,X11)!=skolem0006(X10,X11)))&(~six(X10,X11)|skolem0009(X10,X11)!=skolem0005(X10,X11)))&(~six(X10,X11)|skolem0009(X10,X11)!=skolem0004(X10,X11)))&(~six(X10,X11)|(~member(X10,X18,X11)|(((((X18=skolem0009(X10,X11)|X18=skolem0008(X10,X11))|X18=skolem0007(X10,X11))|X18=skolem0006(X10,X11))|X18=skolem0005(X10,X11))|X18=skolem0004(X10,X11))))))))))&(((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|member(X19,skolem0010(X19,X20,X21,X22,X23,X24,X25,X26),X20)))))))|six(X19,X20))&(((((((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X26))))))|six(X19,X20))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X25))))))|six(X19,X20)))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X24))))))|six(X19,X20)))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X23))))))|six(X19,X20)))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X22))))))|six(X19,X20)))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|((((~member(X19,X24,X20)|X24=X23)|X24=X22)|X24=X21)|(((((~member(X19,X25,X20)|X25=X24)|X25=X23)|X25=X22)|X25=X21)|((((((~member(X19,X26,X20)|X26=X25)|X26=X24)|X26=X23)|X26=X22)|X26=X21)|skolem0010(X19,X20,X21,X22,X23,X24,X25,X26)!=X21))))))|six(X19,X20)))))))))))))))),inference(distribute,[status(thm)],[c64])).
% 1.67/1.83 cnf(c72,plain,~six(X242,X243)|member(X242,skolem0007(X242,X243),X243),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.83 cnf(c228,plain,member(skolem0001,skolem0007(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c72, c54])).
% 1.67/1.83 cnf(c53,negated_conjecture,~male(skolem0001,X493)|~man(skolem0001,X493)|~of(skolem0001,X494,X493)|~cannon(skolem0001,X494)|~member(skolem0001,X494,skolem0002)|from_loc(skolem0001,skolem0003(X493,X494),X494),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.83 cnf(c454,plain,~male(skolem0001,X754)|~man(skolem0001,X754)|~of(skolem0001,skolem0007(skolem0001,skolem0002),X754)|~cannon(skolem0001,skolem0007(skolem0001,skolem0002))|from_loc(skolem0001,skolem0003(X754,skolem0007(skolem0001,skolem0002)),skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c53, c228])).
% 1.67/1.83 cnf(c69,plain,~six(X240,X241)|member(X240,skolem0006(X240,X241),X241),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.83 cnf(c227,plain,member(skolem0001,skolem0006(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c69, c54])).
% 1.67/1.83 cnf(c453,plain,~male(skolem0001,X753)|~man(skolem0001,X753)|~of(skolem0001,skolem0006(skolem0001,skolem0002),X753)|~cannon(skolem0001,skolem0006(skolem0001,skolem0002))|from_loc(skolem0001,skolem0003(X753,skolem0006(skolem0001,skolem0002)),skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c53, c227])).
% 1.67/1.83 cnf(c67,plain,~six(X234,X235)|member(X234,skolem0005(X234,X235),X235),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.83 cnf(c226,plain,member(skolem0001,skolem0005(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c67, c54])).
% 1.67/1.83 cnf(c452,plain,~male(skolem0001,X752)|~man(skolem0001,X752)|~of(skolem0001,skolem0005(skolem0001,skolem0002),X752)|~cannon(skolem0001,skolem0005(skolem0001,skolem0002))|from_loc(skolem0001,skolem0003(X752,skolem0005(skolem0001,skolem0002)),skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c53, c226])).
% 1.67/1.83 cnf(c76,plain,~six(X244,X245)|member(X244,skolem0008(X244,X245),X245),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.83 cnf(c229,plain,member(skolem0001,skolem0008(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c76, c54])).
% 1.67/1.83 cnf(c451,plain,~male(skolem0001,X751)|~man(skolem0001,X751)|~of(skolem0001,skolem0008(skolem0001,skolem0002),X751)|~cannon(skolem0001,skolem0008(skolem0001,skolem0002))|from_loc(skolem0001,skolem0003(X751,skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c53, c229])).
% 1.67/1.83 cnf(c66,plain,~six(X232,X233)|member(X232,skolem0004(X232,X233),X233),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.83 cnf(c225,plain,member(skolem0001,skolem0004(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c66, c54])).
% 1.67/1.83 cnf(c450,plain,~male(skolem0001,X750)|~man(skolem0001,X750)|~of(skolem0001,skolem0004(skolem0001,skolem0002),X750)|~cannon(skolem0001,skolem0004(skolem0001,skolem0002))|from_loc(skolem0001,skolem0003(X750,skolem0004(skolem0001,skolem0002)),skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c53, c225])).
% 1.67/1.83 cnf(c81,plain,~six(X246,X247)|member(X246,skolem0009(X246,X247),X247),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.83 cnf(c230,plain,member(skolem0001,skolem0009(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c81, c54])).
% 1.67/1.83 cnf(c449,plain,~male(skolem0001,X749)|~man(skolem0001,X749)|~of(skolem0001,skolem0009(skolem0001,skolem0002),X749)|~cannon(skolem0001,skolem0009(skolem0001,skolem0002))|from_loc(skolem0001,skolem0003(X749,skolem0009(skolem0001,skolem0002)),skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c53, c230])).
% 1.67/1.83 cnf(c49,negated_conjecture,~male(skolem0001,X466)|~man(skolem0001,X466)|~of(skolem0001,X467,X466)|~cannon(skolem0001,X467)|~member(skolem0001,X467,skolem0002)|patient(skolem0001,skolem0003(X466,X467),X467),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.83 cnf(c417,plain,~male(skolem0001,X748)|~man(skolem0001,X748)|~of(skolem0001,skolem0007(skolem0001,skolem0002),X748)|~cannon(skolem0001,skolem0007(skolem0001,skolem0002))|patient(skolem0001,skolem0003(X748,skolem0007(skolem0001,skolem0002)),skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c49, c228])).
% 1.67/1.84 cnf(c416,plain,~male(skolem0001,X747)|~man(skolem0001,X747)|~of(skolem0001,skolem0006(skolem0001,skolem0002),X747)|~cannon(skolem0001,skolem0006(skolem0001,skolem0002))|patient(skolem0001,skolem0003(X747,skolem0006(skolem0001,skolem0002)),skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c49, c227])).
% 1.67/1.84 cnf(c415,plain,~male(skolem0001,X746)|~man(skolem0001,X746)|~of(skolem0001,skolem0005(skolem0001,skolem0002),X746)|~cannon(skolem0001,skolem0005(skolem0001,skolem0002))|patient(skolem0001,skolem0003(X746,skolem0005(skolem0001,skolem0002)),skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c49, c226])).
% 1.67/1.84 cnf(c414,plain,~male(skolem0001,X745)|~man(skolem0001,X745)|~of(skolem0001,skolem0008(skolem0001,skolem0002),X745)|~cannon(skolem0001,skolem0008(skolem0001,skolem0002))|patient(skolem0001,skolem0003(X745,skolem0008(skolem0001,skolem0002)),skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c49, c229])).
% 1.67/1.84 cnf(c413,plain,~male(skolem0001,X744)|~man(skolem0001,X744)|~of(skolem0001,skolem0004(skolem0001,skolem0002),X744)|~cannon(skolem0001,skolem0004(skolem0001,skolem0002))|patient(skolem0001,skolem0003(X744,skolem0004(skolem0001,skolem0002)),skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c49, c225])).
% 1.67/1.84 cnf(c412,plain,~male(skolem0001,X743)|~man(skolem0001,X743)|~of(skolem0001,skolem0009(skolem0001,skolem0002),X743)|~cannon(skolem0001,skolem0009(skolem0001,skolem0002))|patient(skolem0001,skolem0003(X743,skolem0009(skolem0001,skolem0002)),skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c49, c230])).
% 1.67/1.84 cnf(c48,negated_conjecture,~male(skolem0001,X459)|~man(skolem0001,X459)|~of(skolem0001,X460,X459)|~cannon(skolem0001,X460)|~member(skolem0001,X460,skolem0002)|agent(skolem0001,skolem0003(X459,X460),X459),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.84 cnf(c408,plain,~male(skolem0001,X742)|~man(skolem0001,X742)|~of(skolem0001,skolem0007(skolem0001,skolem0002),X742)|~cannon(skolem0001,skolem0007(skolem0001,skolem0002))|agent(skolem0001,skolem0003(X742,skolem0007(skolem0001,skolem0002)),X742),inference(resolution,[status(thm)],[c48, c228])).
% 1.67/1.84 cnf(c407,plain,~male(skolem0001,X741)|~man(skolem0001,X741)|~of(skolem0001,skolem0006(skolem0001,skolem0002),X741)|~cannon(skolem0001,skolem0006(skolem0001,skolem0002))|agent(skolem0001,skolem0003(X741,skolem0006(skolem0001,skolem0002)),X741),inference(resolution,[status(thm)],[c48, c227])).
% 1.67/1.84 cnf(c52,negated_conjecture,~male(skolem0001,X487)|~man(skolem0001,X487)|~of(skolem0001,X488,X487)|~cannon(skolem0001,X488)|~member(skolem0001,X488,skolem0002)|fire(skolem0001,skolem0003(X487,X488)),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.84 cnf(c445,plain,~male(skolem0001,X740)|~man(skolem0001,X740)|~of(skolem0001,skolem0007(skolem0001,skolem0002),X740)|~cannon(skolem0001,skolem0007(skolem0001,skolem0002))|fire(skolem0001,skolem0003(X740,skolem0007(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c52, c228])).
% 1.67/1.84 cnf(c444,plain,~male(skolem0001,X739)|~man(skolem0001,X739)|~of(skolem0001,skolem0006(skolem0001,skolem0002),X739)|~cannon(skolem0001,skolem0006(skolem0001,skolem0002))|fire(skolem0001,skolem0003(X739,skolem0006(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c52, c227])).
% 1.67/1.84 cnf(c443,plain,~male(skolem0001,X738)|~man(skolem0001,X738)|~of(skolem0001,skolem0005(skolem0001,skolem0002),X738)|~cannon(skolem0001,skolem0005(skolem0001,skolem0002))|fire(skolem0001,skolem0003(X738,skolem0005(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c52, c226])).
% 1.67/1.84 cnf(c406,plain,~male(skolem0001,X737)|~man(skolem0001,X737)|~of(skolem0001,skolem0005(skolem0001,skolem0002),X737)|~cannon(skolem0001,skolem0005(skolem0001,skolem0002))|agent(skolem0001,skolem0003(X737,skolem0005(skolem0001,skolem0002)),X737),inference(resolution,[status(thm)],[c48, c226])).
% 1.67/1.84 cnf(c442,plain,~male(skolem0001,X736)|~man(skolem0001,X736)|~of(skolem0001,skolem0008(skolem0001,skolem0002),X736)|~cannon(skolem0001,skolem0008(skolem0001,skolem0002))|fire(skolem0001,skolem0003(X736,skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c52, c229])).
% 1.67/1.84 cnf(c441,plain,~male(skolem0001,X735)|~man(skolem0001,X735)|~of(skolem0001,skolem0004(skolem0001,skolem0002),X735)|~cannon(skolem0001,skolem0004(skolem0001,skolem0002))|fire(skolem0001,skolem0003(X735,skolem0004(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c52, c225])).
% 1.67/1.84 cnf(c440,plain,~male(skolem0001,X734)|~man(skolem0001,X734)|~of(skolem0001,skolem0009(skolem0001,skolem0002),X734)|~cannon(skolem0001,skolem0009(skolem0001,skolem0002))|fire(skolem0001,skolem0003(X734,skolem0009(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c52, c230])).
% 1.67/1.84 cnf(c51,negated_conjecture,~male(skolem0001,X480)|~man(skolem0001,X480)|~of(skolem0001,X481,X480)|~cannon(skolem0001,X481)|~member(skolem0001,X481,skolem0002)|nonreflexive(skolem0001,skolem0003(X480,X481)),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.84 cnf(c436,plain,~male(skolem0001,X733)|~man(skolem0001,X733)|~of(skolem0001,skolem0007(skolem0001,skolem0002),X733)|~cannon(skolem0001,skolem0007(skolem0001,skolem0002))|nonreflexive(skolem0001,skolem0003(X733,skolem0007(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c51, c228])).
% 1.67/1.84 cnf(c435,plain,~male(skolem0001,X732)|~man(skolem0001,X732)|~of(skolem0001,skolem0006(skolem0001,skolem0002),X732)|~cannon(skolem0001,skolem0006(skolem0001,skolem0002))|nonreflexive(skolem0001,skolem0003(X732,skolem0006(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c51, c227])).
% 1.67/1.84 cnf(c405,plain,~male(skolem0001,X731)|~man(skolem0001,X731)|~of(skolem0001,skolem0008(skolem0001,skolem0002),X731)|~cannon(skolem0001,skolem0008(skolem0001,skolem0002))|agent(skolem0001,skolem0003(X731,skolem0008(skolem0001,skolem0002)),X731),inference(resolution,[status(thm)],[c48, c229])).
% 1.67/1.84 cnf(c434,plain,~male(skolem0001,X730)|~man(skolem0001,X730)|~of(skolem0001,skolem0005(skolem0001,skolem0002),X730)|~cannon(skolem0001,skolem0005(skolem0001,skolem0002))|nonreflexive(skolem0001,skolem0003(X730,skolem0005(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c51, c226])).
% 1.67/1.84 cnf(c433,plain,~male(skolem0001,X729)|~man(skolem0001,X729)|~of(skolem0001,skolem0008(skolem0001,skolem0002),X729)|~cannon(skolem0001,skolem0008(skolem0001,skolem0002))|nonreflexive(skolem0001,skolem0003(X729,skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c51, c229])).
% 1.67/1.84 cnf(c432,plain,~male(skolem0001,X728)|~man(skolem0001,X728)|~of(skolem0001,skolem0004(skolem0001,skolem0002),X728)|~cannon(skolem0001,skolem0004(skolem0001,skolem0002))|nonreflexive(skolem0001,skolem0003(X728,skolem0004(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c51, c225])).
% 1.67/1.84 cnf(c431,plain,~male(skolem0001,X727)|~man(skolem0001,X727)|~of(skolem0001,skolem0009(skolem0001,skolem0002),X727)|~cannon(skolem0001,skolem0009(skolem0001,skolem0002))|nonreflexive(skolem0001,skolem0003(X727,skolem0009(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c51, c230])).
% 1.67/1.84 cnf(c50,negated_conjecture,~male(skolem0001,X472)|~man(skolem0001,X472)|~of(skolem0001,X473,X472)|~cannon(skolem0001,X473)|~member(skolem0001,X473,skolem0002)|present(skolem0001,skolem0003(X472,X473)),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.84 cnf(c426,plain,~male(skolem0001,X726)|~man(skolem0001,X726)|~of(skolem0001,skolem0007(skolem0001,skolem0002),X726)|~cannon(skolem0001,skolem0007(skolem0001,skolem0002))|present(skolem0001,skolem0003(X726,skolem0007(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c50, c228])).
% 1.67/1.84 cnf(c404,plain,~male(skolem0001,X725)|~man(skolem0001,X725)|~of(skolem0001,skolem0004(skolem0001,skolem0002),X725)|~cannon(skolem0001,skolem0004(skolem0001,skolem0002))|agent(skolem0001,skolem0003(X725,skolem0004(skolem0001,skolem0002)),X725),inference(resolution,[status(thm)],[c48, c225])).
% 1.67/1.84 cnf(c425,plain,~male(skolem0001,X724)|~man(skolem0001,X724)|~of(skolem0001,skolem0006(skolem0001,skolem0002),X724)|~cannon(skolem0001,skolem0006(skolem0001,skolem0002))|present(skolem0001,skolem0003(X724,skolem0006(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c50, c227])).
% 1.67/1.84 cnf(c424,plain,~male(skolem0001,X723)|~man(skolem0001,X723)|~of(skolem0001,skolem0005(skolem0001,skolem0002),X723)|~cannon(skolem0001,skolem0005(skolem0001,skolem0002))|present(skolem0001,skolem0003(X723,skolem0005(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c50, c226])).
% 1.67/1.84 cnf(c423,plain,~male(skolem0001,X722)|~man(skolem0001,X722)|~of(skolem0001,skolem0008(skolem0001,skolem0002),X722)|~cannon(skolem0001,skolem0008(skolem0001,skolem0002))|present(skolem0001,skolem0003(X722,skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c50, c229])).
% 1.67/1.84 cnf(c422,plain,~male(skolem0001,X721)|~man(skolem0001,X721)|~of(skolem0001,skolem0004(skolem0001,skolem0002),X721)|~cannon(skolem0001,skolem0004(skolem0001,skolem0002))|present(skolem0001,skolem0003(X721,skolem0004(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c50, c225])).
% 1.67/1.84 cnf(c421,plain,~male(skolem0001,X720)|~man(skolem0001,X720)|~of(skolem0001,skolem0009(skolem0001,skolem0002),X720)|~cannon(skolem0001,skolem0009(skolem0001,skolem0002))|present(skolem0001,skolem0003(X720,skolem0009(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c50, c230])).
% 1.67/1.84 cnf(c403,plain,~male(skolem0001,X719)|~man(skolem0001,X719)|~of(skolem0001,skolem0009(skolem0001,skolem0002),X719)|~cannon(skolem0001,skolem0009(skolem0001,skolem0002))|agent(skolem0001,skolem0003(X719,skolem0009(skolem0001,skolem0002)),X719),inference(resolution,[status(thm)],[c48, c230])).
% 1.67/1.84 cnf(c47,negated_conjecture,~male(skolem0001,X451)|~man(skolem0001,X451)|~of(skolem0001,X452,X451)|~cannon(skolem0001,X452)|~member(skolem0001,X452,skolem0002)|event(skolem0001,skolem0003(X451,X452)),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.84 cnf(c398,plain,~male(skolem0001,X718)|~man(skolem0001,X718)|~of(skolem0001,skolem0007(skolem0001,skolem0002),X718)|~cannon(skolem0001,skolem0007(skolem0001,skolem0002))|event(skolem0001,skolem0003(X718,skolem0007(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c47, c228])).
% 1.67/1.84 cnf(c397,plain,~male(skolem0001,X717)|~man(skolem0001,X717)|~of(skolem0001,skolem0006(skolem0001,skolem0002),X717)|~cannon(skolem0001,skolem0006(skolem0001,skolem0002))|event(skolem0001,skolem0003(X717,skolem0006(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c47, c227])).
% 1.67/1.84 cnf(c396,plain,~male(skolem0001,X716)|~man(skolem0001,X716)|~of(skolem0001,skolem0005(skolem0001,skolem0002),X716)|~cannon(skolem0001,skolem0005(skolem0001,skolem0002))|event(skolem0001,skolem0003(X716,skolem0005(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c47, c226])).
% 1.67/1.84 cnf(c395,plain,~male(skolem0001,X715)|~man(skolem0001,X715)|~of(skolem0001,skolem0008(skolem0001,skolem0002),X715)|~cannon(skolem0001,skolem0008(skolem0001,skolem0002))|event(skolem0001,skolem0003(X715,skolem0008(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c47, c229])).
% 1.67/1.84 cnf(c394,plain,~male(skolem0001,X714)|~man(skolem0001,X714)|~of(skolem0001,skolem0004(skolem0001,skolem0002),X714)|~cannon(skolem0001,skolem0004(skolem0001,skolem0002))|event(skolem0001,skolem0003(X714,skolem0004(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c47, c225])).
% 1.67/1.84 cnf(c393,plain,~male(skolem0001,X713)|~man(skolem0001,X713)|~of(skolem0001,skolem0009(skolem0001,skolem0002),X713)|~cannon(skolem0001,skolem0009(skolem0001,skolem0002))|event(skolem0001,skolem0003(X713,skolem0009(skolem0001,skolem0002))),inference(resolution,[status(thm)],[c47, c230])).
% 1.67/1.84 cnf(reflexivity,axiom,X108=X108,theory(equality)).
% 1.67/1.84 cnf(c35,axiom,X421!=X420|X423!=X422|X418!=X419|~member(X421,X423,X418)|member(X420,X422,X419),theory(equality)).
% 1.67/1.84 cnf(c382,plain,skolem0001!=X706|skolem0007(skolem0001,skolem0002)!=X708|skolem0002!=X707|member(X706,X708,X707),inference(resolution,[status(thm)],[c35, c228])).
% 1.67/1.84 cnf(c568,plain,skolem0001!=X711|skolem0002!=X710|member(X711,skolem0007(skolem0001,skolem0002),X710),inference(resolution,[status(thm)],[c382, reflexivity])).
% 1.67/1.84 cnf(c570,plain,skolem0001!=X712|member(X712,skolem0007(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c568, reflexivity])).
% 1.67/1.84 cnf(c381,plain,skolem0001!=X701|skolem0006(skolem0001,skolem0002)!=X703|skolem0002!=X702|member(X701,X703,X702),inference(resolution,[status(thm)],[c35, c227])).
% 1.67/1.84 cnf(c566,plain,skolem0001!=X704|skolem0002!=X705|member(X704,skolem0006(skolem0001,skolem0002),X705),inference(resolution,[status(thm)],[c381, reflexivity])).
% 1.67/1.84 cnf(c567,plain,skolem0001!=X709|member(X709,skolem0006(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c566, reflexivity])).
% 1.67/1.84 cnf(c380,plain,skolem0001!=X695|skolem0005(skolem0001,skolem0002)!=X697|skolem0002!=X696|member(X695,X697,X696),inference(resolution,[status(thm)],[c35, c226])).
% 1.67/1.84 cnf(c563,plain,skolem0001!=X698|skolem0002!=X699|member(X698,skolem0005(skolem0001,skolem0002),X699),inference(resolution,[status(thm)],[c380, reflexivity])).
% 1.67/1.84 cnf(c564,plain,skolem0001!=X700|member(X700,skolem0005(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c563, reflexivity])).
% 1.67/1.84 cnf(c379,plain,skolem0001!=X688|skolem0008(skolem0001,skolem0002)!=X690|skolem0002!=X689|member(X688,X690,X689),inference(resolution,[status(thm)],[c35, c229])).
% 1.67/1.84 cnf(c559,plain,skolem0001!=X693|skolem0002!=X692|member(X693,skolem0008(skolem0001,skolem0002),X692),inference(resolution,[status(thm)],[c379, reflexivity])).
% 1.67/1.84 cnf(c561,plain,skolem0001!=X694|member(X694,skolem0008(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c559, reflexivity])).
% 1.67/1.84 cnf(c378,plain,skolem0001!=X683|skolem0004(skolem0001,skolem0002)!=X685|skolem0002!=X684|member(X683,X685,X684),inference(resolution,[status(thm)],[c35, c225])).
% 1.67/1.84 cnf(c557,plain,skolem0001!=X686|skolem0002!=X687|member(X686,skolem0004(skolem0001,skolem0002),X687),inference(resolution,[status(thm)],[c378, reflexivity])).
% 1.67/1.84 cnf(c558,plain,skolem0001!=X691|member(X691,skolem0004(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c557, reflexivity])).
% 1.67/1.84 cnf(c377,plain,skolem0001!=X677|skolem0009(skolem0001,skolem0002)!=X679|skolem0002!=X678|member(X677,X679,X678),inference(resolution,[status(thm)],[c35, c230])).
% 1.67/1.84 cnf(c554,plain,skolem0001!=X681|skolem0002!=X680|member(X681,skolem0009(skolem0001,skolem0002),X680),inference(resolution,[status(thm)],[c377, reflexivity])).
% 1.67/1.84 cnf(c555,plain,skolem0001!=X682|member(X682,skolem0009(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c554, reflexivity])).
% 1.67/1.84 cnf(c56,negated_conjecture,~member(skolem0001,X231,skolem0002)|shot(skolem0001,X231),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.84 cnf(c243,plain,shot(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c226, c56])).
% 1.67/1.84 cnf(c31,axiom,X378!=X379|X381!=X380|~shot(X378,X381)|shot(X379,X380),theory(equality)).
% 1.67/1.84 cnf(c368,plain,skolem0001!=X674|skolem0005(skolem0001,skolem0002)!=X675|shot(X674,X675),inference(resolution,[status(thm)],[c31, c243])).
% 1.67/1.84 cnf(c552,plain,skolem0001!=X676|shot(X676,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c368, reflexivity])).
% 1.67/1.84 cnf(c273,plain,shot(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c228, c56])).
% 1.67/1.84 cnf(c367,plain,skolem0001!=X671|skolem0007(skolem0001,skolem0002)!=X672|shot(X671,X672),inference(resolution,[status(thm)],[c31, c273])).
% 1.67/1.84 cnf(c550,plain,skolem0001!=X673|shot(X673,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c367, reflexivity])).
% 1.67/1.84 cnf(c231,plain,shot(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c225, c56])).
% 1.67/1.84 cnf(c366,plain,skolem0001!=X668|skolem0004(skolem0001,skolem0002)!=X669|shot(X668,X669),inference(resolution,[status(thm)],[c31, c231])).
% 1.67/1.84 cnf(c548,plain,skolem0001!=X670|shot(X670,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c366, reflexivity])).
% 1.67/1.84 cnf(c257,plain,shot(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c227, c56])).
% 1.67/1.84 cnf(c365,plain,skolem0001!=X665|skolem0006(skolem0001,skolem0002)!=X666|shot(X665,X666),inference(resolution,[status(thm)],[c31, c257])).
% 1.67/1.84 cnf(c546,plain,skolem0001!=X667|shot(X667,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c365, reflexivity])).
% 1.67/1.84 cnf(c301,plain,shot(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c230, c56])).
% 1.67/1.84 cnf(c364,plain,skolem0001!=X662|skolem0009(skolem0001,skolem0002)!=X663|shot(X662,X663),inference(resolution,[status(thm)],[c31, c301])).
% 1.67/1.84 cnf(c544,plain,skolem0001!=X664|shot(X664,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c364, reflexivity])).
% 1.67/1.84 cnf(c287,plain,shot(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c229, c56])).
% 1.67/1.84 cnf(c363,plain,skolem0001!=X659|skolem0008(skolem0001,skolem0002)!=X660|shot(X659,X660),inference(resolution,[status(thm)],[c31, c287])).
% 1.67/1.84 cnf(c542,plain,skolem0001!=X661|shot(X661,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c363, reflexivity])).
% 1.67/1.84 fof(ax33,axiom,(![U]:(![V]:(shot(U,V)=>action(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 1.67/1.84 fof(c118,plain,(![U]:(![V]:(~shot(U,V)|action(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 1.67/1.84 fof(c119,plain,(![X42]:(![X43]:(~shot(X42,X43)|action(X42,X43)))),inference(variable_rename,[status(thm)],[c118])).
% 1.67/1.84 cnf(c120,plain,~shot(X128,X127)|action(X128,X127),inference(split_conjunct,[status(thm)],[c119])).
% 1.67/1.84 cnf(c232,plain,action(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c231, c120])).
% 1.67/1.84 cnf(c30,axiom,X374!=X375|X377!=X376|~action(X374,X377)|action(X375,X376),theory(equality)).
% 1.67/1.84 cnf(c362,plain,skolem0001!=X656|skolem0004(skolem0001,skolem0002)!=X657|action(X656,X657),inference(resolution,[status(thm)],[c30, c232])).
% 1.67/1.84 cnf(c540,plain,skolem0001!=X658|action(X658,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c362, reflexivity])).
% 1.67/1.84 cnf(c274,plain,action(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c273, c120])).
% 1.67/1.84 cnf(c361,plain,skolem0001!=X653|skolem0007(skolem0001,skolem0002)!=X654|action(X653,X654),inference(resolution,[status(thm)],[c30, c274])).
% 1.67/1.84 cnf(c538,plain,skolem0001!=X655|action(X655,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c361, reflexivity])).
% 1.67/1.84 cnf(c258,plain,action(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c257, c120])).
% 1.67/1.84 cnf(c360,plain,skolem0001!=X650|skolem0006(skolem0001,skolem0002)!=X651|action(X650,X651),inference(resolution,[status(thm)],[c30, c258])).
% 1.67/1.84 cnf(c536,plain,skolem0001!=X652|action(X652,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c360, reflexivity])).
% 1.67/1.84 cnf(c307,plain,action(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c301, c120])).
% 1.67/1.84 cnf(c359,plain,skolem0001!=X647|skolem0009(skolem0001,skolem0002)!=X648|action(X647,X648),inference(resolution,[status(thm)],[c30, c307])).
% 1.67/1.84 cnf(c534,plain,skolem0001!=X649|action(X649,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c359, reflexivity])).
% 1.67/1.84 cnf(c288,plain,action(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c287, c120])).
% 1.67/1.84 cnf(c358,plain,skolem0001!=X644|skolem0008(skolem0001,skolem0002)!=X645|action(X644,X645),inference(resolution,[status(thm)],[c30, c288])).
% 1.67/1.84 cnf(c532,plain,skolem0001!=X646|action(X646,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c358, reflexivity])).
% 1.67/1.84 cnf(c244,plain,action(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c243, c120])).
% 1.67/1.84 cnf(c357,plain,skolem0001!=X641|skolem0005(skolem0001,skolem0002)!=X642|action(X641,X642),inference(resolution,[status(thm)],[c30, c244])).
% 1.67/1.84 cnf(c530,plain,skolem0001!=X643|action(X643,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c357, reflexivity])).
% 1.67/1.84 fof(ax32,axiom,(![U]:(![V]:(action(U,V)=>act(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 1.67/1.84 fof(c121,plain,(![U]:(![V]:(~action(U,V)|act(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 1.67/1.84 fof(c122,plain,(![X44]:(![X45]:(~action(X44,X45)|act(X44,X45)))),inference(variable_rename,[status(thm)],[c121])).
% 1.67/1.84 cnf(c123,plain,~action(X130,X129)|act(X130,X129),inference(split_conjunct,[status(thm)],[c122])).
% 1.67/1.84 cnf(c275,plain,act(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c274, c123])).
% 1.67/1.84 cnf(c29,axiom,X370!=X371|X373!=X372|~act(X370,X373)|act(X371,X372),theory(equality)).
% 1.67/1.84 cnf(c356,plain,skolem0001!=X639|skolem0007(skolem0001,skolem0002)!=X638|act(X639,X638),inference(resolution,[status(thm)],[c29, c275])).
% 1.67/1.84 cnf(c528,plain,skolem0001!=X640|act(X640,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c356, reflexivity])).
% 1.67/1.84 cnf(c289,plain,act(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c288, c123])).
% 1.67/1.84 cnf(c355,plain,skolem0001!=X636|skolem0008(skolem0001,skolem0002)!=X635|act(X636,X635),inference(resolution,[status(thm)],[c29, c289])).
% 1.67/1.84 cnf(c526,plain,skolem0001!=X637|act(X637,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c355, reflexivity])).
% 1.67/1.84 cnf(c245,plain,act(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c244, c123])).
% 1.67/1.84 cnf(c354,plain,skolem0001!=X633|skolem0005(skolem0001,skolem0002)!=X632|act(X633,X632),inference(resolution,[status(thm)],[c29, c245])).
% 1.67/1.84 cnf(c524,plain,skolem0001!=X634|act(X634,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c354, reflexivity])).
% 1.67/1.84 cnf(c261,plain,act(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c258, c123])).
% 1.67/1.84 cnf(c353,plain,skolem0001!=X630|skolem0006(skolem0001,skolem0002)!=X629|act(X630,X629),inference(resolution,[status(thm)],[c29, c261])).
% 1.67/1.84 cnf(c522,plain,skolem0001!=X631|act(X631,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c353, reflexivity])).
% 1.67/1.84 cnf(c233,plain,act(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c232, c123])).
% 1.67/1.84 cnf(c352,plain,skolem0001!=X627|skolem0004(skolem0001,skolem0002)!=X626|act(X627,X626),inference(resolution,[status(thm)],[c29, c233])).
% 1.67/1.84 cnf(c520,plain,skolem0001!=X628|act(X628,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c352, reflexivity])).
% 1.67/1.84 cnf(c308,plain,act(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c307, c123])).
% 1.67/1.84 cnf(c351,plain,skolem0001!=X624|skolem0009(skolem0001,skolem0002)!=X623|act(X624,X623),inference(resolution,[status(thm)],[c29, c308])).
% 1.67/1.84 cnf(c518,plain,skolem0001!=X625|act(X625,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c351, reflexivity])).
% 1.67/1.84 fof(ax28,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 1.67/1.84 fof(c133,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 1.67/1.84 fof(c134,plain,(![X52]:(![X53]:(~thing(X52,X53)|singleton(X52,X53)))),inference(variable_rename,[status(thm)],[c133])).
% 1.67/1.84 cnf(c135,plain,~thing(X141,X142)|singleton(X141,X142),inference(split_conjunct,[status(thm)],[c134])).
% 1.67/1.84 fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 1.67/1.84 fof(c130,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 1.67/1.84 fof(c131,plain,(![X50]:(![X51]:(~eventuality(X50,X51)|thing(X50,X51)))),inference(variable_rename,[status(thm)],[c130])).
% 1.67/1.84 cnf(c132,plain,~eventuality(X140,X139)|thing(X140,X139),inference(split_conjunct,[status(thm)],[c131])).
% 1.67/1.84 fof(ax30,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 1.67/1.84 fof(c127,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 1.67/1.84 fof(c128,plain,(![X48]:(![X49]:(~event(X48,X49)|eventuality(X48,X49)))),inference(variable_rename,[status(thm)],[c127])).
% 1.67/1.84 cnf(c129,plain,~event(X134,X133)|eventuality(X134,X133),inference(split_conjunct,[status(thm)],[c128])).
% 1.67/1.84 fof(ax31,axiom,(![U]:(![V]:(act(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 1.67/1.84 fof(c124,plain,(![U]:(![V]:(~act(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 1.67/1.84 fof(c125,plain,(![X46]:(![X47]:(~act(X46,X47)|event(X46,X47)))),inference(variable_rename,[status(thm)],[c124])).
% 1.67/1.84 cnf(c126,plain,~act(X132,X131)|event(X132,X131),inference(split_conjunct,[status(thm)],[c125])).
% 1.67/1.84 cnf(c262,plain,event(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c261, c126])).
% 1.67/1.84 cnf(c263,plain,eventuality(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c262, c129])).
% 1.67/1.84 cnf(c264,plain,thing(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c263, c132])).
% 1.67/1.84 cnf(c269,plain,singleton(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c264, c135])).
% 1.67/1.84 cnf(c28,axiom,X363!=X364|X366!=X365|~singleton(X363,X366)|singleton(X364,X365),theory(equality)).
% 1.67/1.84 cnf(c348,plain,skolem0001!=X621|skolem0006(skolem0001,skolem0002)!=X620|singleton(X621,X620),inference(resolution,[status(thm)],[c28, c269])).
% 1.67/1.84 cnf(c516,plain,skolem0001!=X622|singleton(X622,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c348, reflexivity])).
% 1.67/1.84 cnf(c290,plain,event(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c289, c126])).
% 1.67/1.84 cnf(c291,plain,eventuality(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c290, c129])).
% 1.67/1.84 cnf(c292,plain,thing(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c291, c132])).
% 1.67/1.84 cnf(c297,plain,singleton(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c292, c135])).
% 1.67/1.84 cnf(c347,plain,skolem0001!=X618|skolem0008(skolem0001,skolem0002)!=X617|singleton(X618,X617),inference(resolution,[status(thm)],[c28, c297])).
% 1.67/1.84 cnf(c514,plain,skolem0001!=X619|singleton(X619,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c347, reflexivity])).
% 1.67/1.84 cnf(c309,plain,event(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c308, c126])).
% 1.67/1.84 cnf(c310,plain,eventuality(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c309, c129])).
% 1.67/1.84 cnf(c312,plain,thing(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c310, c132])).
% 1.67/1.84 cnf(c318,plain,singleton(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c312, c135])).
% 1.67/1.84 cnf(c346,plain,skolem0001!=X615|skolem0009(skolem0001,skolem0002)!=X614|singleton(X615,X614),inference(resolution,[status(thm)],[c28, c318])).
% 1.67/1.84 cnf(c512,plain,skolem0001!=X616|singleton(X616,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c346, reflexivity])).
% 1.67/1.84 cnf(c234,plain,event(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c233, c126])).
% 1.67/1.84 cnf(c235,plain,eventuality(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c234, c129])).
% 1.67/1.84 cnf(c236,plain,thing(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c235, c132])).
% 1.67/1.84 cnf(c240,plain,singleton(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c236, c135])).
% 1.67/1.84 cnf(c345,plain,skolem0001!=X612|skolem0004(skolem0001,skolem0002)!=X611|singleton(X612,X611),inference(resolution,[status(thm)],[c28, c240])).
% 1.67/1.84 cnf(c510,plain,skolem0001!=X613|singleton(X613,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c345, reflexivity])).
% 1.67/1.84 cnf(c276,plain,event(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c275, c126])).
% 1.67/1.84 cnf(c277,plain,eventuality(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c276, c129])).
% 1.67/1.84 cnf(c278,plain,thing(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c277, c132])).
% 1.67/1.84 cnf(c283,plain,singleton(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c278, c135])).
% 1.67/1.84 cnf(c344,plain,skolem0001!=X609|skolem0007(skolem0001,skolem0002)!=X608|singleton(X609,X608),inference(resolution,[status(thm)],[c28, c283])).
% 1.67/1.84 cnf(c508,plain,skolem0001!=X610|singleton(X610,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c344, reflexivity])).
% 1.67/1.84 cnf(c246,plain,event(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c245, c126])).
% 1.67/1.84 cnf(c247,plain,eventuality(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c246, c129])).
% 1.67/1.84 cnf(c248,plain,thing(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c247, c132])).
% 1.67/1.84 cnf(c252,plain,singleton(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c248, c135])).
% 1.67/1.84 cnf(c343,plain,skolem0001!=X606|skolem0005(skolem0001,skolem0002)!=X605|singleton(X606,X605),inference(resolution,[status(thm)],[c28, c252])).
% 1.67/1.84 cnf(c506,plain,skolem0001!=X607|singleton(X607,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c343, reflexivity])).
% 1.67/1.84 fof(ax26,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 1.67/1.84 fof(c139,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 1.67/1.84 fof(c140,plain,(![X56]:(![X57]:(~eventuality(X56,X57)|nonexistent(X56,X57)))),inference(variable_rename,[status(thm)],[c139])).
% 1.67/1.84 cnf(c141,plain,~eventuality(X146,X145)|nonexistent(X146,X145),inference(split_conjunct,[status(thm)],[c140])).
% 1.67/1.84 cnf(c314,plain,nonexistent(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c310, c141])).
% 1.67/1.84 cnf(c27,axiom,X355!=X356|X358!=X357|~nonexistent(X355,X358)|nonexistent(X356,X357),theory(equality)).
% 1.67/1.84 cnf(c339,plain,skolem0001!=X602|skolem0009(skolem0001,skolem0002)!=X603|nonexistent(X602,X603),inference(resolution,[status(thm)],[c27, c314])).
% 1.67/1.84 cnf(c504,plain,skolem0001!=X604|nonexistent(X604,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c339, reflexivity])).
% 1.67/1.84 cnf(c238,plain,nonexistent(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c235, c141])).
% 1.67/1.84 cnf(c338,plain,skolem0001!=X599|skolem0004(skolem0001,skolem0002)!=X600|nonexistent(X599,X600),inference(resolution,[status(thm)],[c27, c238])).
% 1.67/1.84 cnf(c502,plain,skolem0001!=X601|nonexistent(X601,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c338, reflexivity])).
% 1.67/1.84 cnf(c294,plain,nonexistent(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c291, c141])).
% 1.67/1.84 cnf(c337,plain,skolem0001!=X596|skolem0008(skolem0001,skolem0002)!=X597|nonexistent(X596,X597),inference(resolution,[status(thm)],[c27, c294])).
% 1.67/1.84 cnf(c500,plain,skolem0001!=X598|nonexistent(X598,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c337, reflexivity])).
% 1.67/1.84 cnf(c280,plain,nonexistent(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c277, c141])).
% 1.67/1.84 cnf(c336,plain,skolem0001!=X585|skolem0007(skolem0001,skolem0002)!=X586|nonexistent(X585,X586),inference(resolution,[status(thm)],[c27, c280])).
% 1.67/1.84 cnf(c498,plain,skolem0001!=X595|nonexistent(X595,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c336, reflexivity])).
% 1.67/1.84 cnf(c94,plain,~member(X594,X590,X592)|~member(X594,X593,X592)|X593=X590|~member(X594,X589,X592)|X589=X593|X589=X590|~member(X594,X588,X592)|X588=X589|X588=X593|X588=X590|~member(X594,X587,X592)|X587=X588|X587=X589|X587=X593|X587=X590|~member(X594,X591,X592)|X591=X587|X591=X588|X591=X589|X591=X593|X591=X590|skolem0010(X594,X592,X590,X593,X589,X588,X587,X591)!=X590|six(X594,X592),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c266,plain,nonexistent(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c263, c141])).
% 1.67/1.84 cnf(c335,plain,skolem0001!=X582|skolem0006(skolem0001,skolem0002)!=X583|nonexistent(X582,X583),inference(resolution,[status(thm)],[c27, c266])).
% 1.67/1.84 cnf(c496,plain,skolem0001!=X584|nonexistent(X584,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c335, reflexivity])).
% 1.67/1.84 cnf(c93,plain,~member(X581,X577,X579)|~member(X581,X580,X579)|X580=X577|~member(X581,X576,X579)|X576=X580|X576=X577|~member(X581,X575,X579)|X575=X576|X575=X580|X575=X577|~member(X581,X574,X579)|X574=X575|X574=X576|X574=X580|X574=X577|~member(X581,X578,X579)|X578=X574|X578=X575|X578=X576|X578=X580|X578=X577|skolem0010(X581,X579,X577,X580,X576,X575,X574,X578)!=X580|six(X581,X579),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c250,plain,nonexistent(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c247, c141])).
% 1.67/1.84 cnf(c334,plain,skolem0001!=X571|skolem0005(skolem0001,skolem0002)!=X572|nonexistent(X571,X572),inference(resolution,[status(thm)],[c27, c250])).
% 1.67/1.84 cnf(c494,plain,skolem0001!=X573|nonexistent(X573,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c334, reflexivity])).
% 1.67/1.84 cnf(c26,axiom,X344!=X345|X347!=X346|~eventuality(X344,X347)|eventuality(X345,X346),theory(equality)).
% 1.67/1.84 cnf(c330,plain,skolem0001!=X569|skolem0006(skolem0001,skolem0002)!=X568|eventuality(X569,X568),inference(resolution,[status(thm)],[c26, c263])).
% 1.67/1.84 cnf(c492,plain,skolem0001!=X570|eventuality(X570,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c330, reflexivity])).
% 1.67/1.84 cnf(c92,plain,~member(X567,X563,X565)|~member(X567,X566,X565)|X566=X563|~member(X567,X562,X565)|X562=X566|X562=X563|~member(X567,X561,X565)|X561=X562|X561=X566|X561=X563|~member(X567,X560,X565)|X560=X561|X560=X562|X560=X566|X560=X563|~member(X567,X564,X565)|X564=X560|X564=X561|X564=X562|X564=X566|X564=X563|skolem0010(X567,X565,X563,X566,X562,X561,X560,X564)!=X562|six(X567,X565),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c329,plain,skolem0001!=X558|skolem0005(skolem0001,skolem0002)!=X557|eventuality(X558,X557),inference(resolution,[status(thm)],[c26, c247])).
% 1.67/1.84 cnf(c490,plain,skolem0001!=X559|eventuality(X559,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c329, reflexivity])).
% 1.67/1.84 cnf(c328,plain,skolem0001!=X547|skolem0004(skolem0001,skolem0002)!=X546|eventuality(X547,X546),inference(resolution,[status(thm)],[c26, c235])).
% 1.67/1.84 cnf(c488,plain,skolem0001!=X556|eventuality(X556,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c328, reflexivity])).
% 1.67/1.84 cnf(c91,plain,~member(X555,X551,X553)|~member(X555,X554,X553)|X554=X551|~member(X555,X550,X553)|X550=X554|X550=X551|~member(X555,X549,X553)|X549=X550|X549=X554|X549=X551|~member(X555,X548,X553)|X548=X549|X548=X550|X548=X554|X548=X551|~member(X555,X552,X553)|X552=X548|X552=X549|X552=X550|X552=X554|X552=X551|skolem0010(X555,X553,X551,X554,X550,X549,X548,X552)!=X549|six(X555,X553),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c327,plain,skolem0001!=X544|skolem0008(skolem0001,skolem0002)!=X543|eventuality(X544,X543),inference(resolution,[status(thm)],[c26, c291])).
% 1.67/1.84 cnf(c486,plain,skolem0001!=X545|eventuality(X545,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c327, reflexivity])).
% 1.67/1.84 cnf(c90,plain,~member(X542,X538,X540)|~member(X542,X541,X540)|X541=X538|~member(X542,X537,X540)|X537=X541|X537=X538|~member(X542,X536,X540)|X536=X537|X536=X541|X536=X538|~member(X542,X535,X540)|X535=X536|X535=X537|X535=X541|X535=X538|~member(X542,X539,X540)|X539=X535|X539=X536|X539=X537|X539=X541|X539=X538|skolem0010(X542,X540,X538,X541,X537,X536,X535,X539)!=X535|six(X542,X540),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c326,plain,skolem0001!=X533|skolem0007(skolem0001,skolem0002)!=X532|eventuality(X533,X532),inference(resolution,[status(thm)],[c26, c277])).
% 1.67/1.84 cnf(c484,plain,skolem0001!=X534|eventuality(X534,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c326, reflexivity])).
% 1.67/1.84 cnf(c325,plain,skolem0001!=X530|skolem0009(skolem0001,skolem0002)!=X529|eventuality(X530,X529),inference(resolution,[status(thm)],[c26, c310])).
% 1.67/1.84 cnf(c482,plain,skolem0001!=X531|eventuality(X531,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c325, reflexivity])).
% 1.67/1.84 cnf(c89,plain,~member(X528,X524,X526)|~member(X528,X527,X526)|X527=X524|~member(X528,X523,X526)|X523=X527|X523=X524|~member(X528,X522,X526)|X522=X523|X522=X527|X522=X524|~member(X528,X521,X526)|X521=X522|X521=X523|X521=X527|X521=X524|~member(X528,X525,X526)|X525=X521|X525=X522|X525=X523|X525=X527|X525=X524|skolem0010(X528,X526,X524,X527,X523,X522,X521,X525)!=X525|six(X528,X526),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c13,axiom,X264!=X265|X267!=X266|~specific(X264,X267)|specific(X265,X266),theory(equality)).
% 1.67/1.84 fof(ax27,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 1.67/1.84 fof(c136,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 1.67/1.84 fof(c137,plain,(![X54]:(![X55]:(~eventuality(X54,X55)|specific(X54,X55)))),inference(variable_rename,[status(thm)],[c136])).
% 1.67/1.84 cnf(c138,plain,~eventuality(X144,X143)|specific(X144,X143),inference(split_conjunct,[status(thm)],[c137])).
% 1.67/1.84 cnf(c315,plain,specific(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c310, c138])).
% 1.67/1.84 cnf(c321,plain,skolem0001!=X518|skolem0009(skolem0001,skolem0002)!=X519|specific(X518,X519),inference(resolution,[status(thm)],[c315, c13])).
% 1.67/1.84 cnf(c480,plain,skolem0001!=X520|specific(X520,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c321, reflexivity])).
% 1.67/1.84 cnf(c10,axiom,X252!=X253|X255!=X254|~unisex(X252,X255)|unisex(X253,X254),theory(equality)).
% 1.67/1.84 fof(ax25,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 1.67/1.84 fof(c142,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 1.67/1.84 fof(c143,plain,(![X58]:(![X59]:(~eventuality(X58,X59)|unisex(X58,X59)))),inference(variable_rename,[status(thm)],[c142])).
% 1.67/1.84 cnf(c144,plain,~eventuality(X148,X147)|unisex(X148,X147),inference(split_conjunct,[status(thm)],[c143])).
% 1.67/1.84 cnf(c313,plain,unisex(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c310, c144])).
% 1.67/1.84 cnf(c319,plain,skolem0001!=X507|skolem0009(skolem0001,skolem0002)!=X508|unisex(X507,X508),inference(resolution,[status(thm)],[c313, c10])).
% 1.67/1.84 cnf(c467,plain,skolem0001!=X517|unisex(X517,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c319, reflexivity])).
% 1.67/1.84 cnf(c88,plain,~member(X516,X512,X514)|~member(X516,X515,X514)|X515=X512|~member(X516,X511,X514)|X511=X515|X511=X512|~member(X516,X510,X514)|X510=X511|X510=X515|X510=X512|~member(X516,X509,X514)|X509=X510|X509=X511|X509=X515|X509=X512|~member(X516,X513,X514)|X513=X509|X513=X510|X513=X511|X513=X515|X513=X512|member(X516,skolem0010(X516,X514,X512,X515,X511,X510,X509,X513),X514)|six(X516,X514),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c14,axiom,X268!=X269|X271!=X270|~thing(X268,X271)|thing(X269,X270),theory(equality)).
% 1.67/1.84 cnf(c317,plain,skolem0001!=X505|skolem0009(skolem0001,skolem0002)!=X504|thing(X505,X504),inference(resolution,[status(thm)],[c312, c14])).
% 1.67/1.84 cnf(c465,plain,skolem0001!=X506|thing(X506,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c317, reflexivity])).
% 1.67/1.84 cnf(c87,plain,~six(X502,X503)|~member(X502,X501,X503)|X501=skolem0009(X502,X503)|X501=skolem0008(X502,X503)|X501=skolem0007(X502,X503)|X501=skolem0006(X502,X503)|X501=skolem0005(X502,X503)|X501=skolem0004(X502,X503),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c21,axiom,X296!=X297|X299!=X298|~event(X296,X299)|event(X297,X298),theory(equality)).
% 1.67/1.84 cnf(c311,plain,skolem0001!=X498|skolem0009(skolem0001,skolem0002)!=X499|event(X498,X499),inference(resolution,[status(thm)],[c309, c21])).
% 1.67/1.84 cnf(c457,plain,skolem0001!=X500|event(X500,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c311, reflexivity])).
% 1.67/1.84 cnf(c306,plain,skolem0001!=X495|skolem0004(skolem0001,skolem0002)!=X496|event(X495,X496),inference(resolution,[status(thm)],[c21, c234])).
% 1.67/1.84 cnf(c455,plain,skolem0001!=X497|event(X497,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c306, reflexivity])).
% 1.67/1.84 cnf(c305,plain,skolem0001!=X490|skolem0006(skolem0001,skolem0002)!=X491|event(X490,X491),inference(resolution,[status(thm)],[c21, c262])).
% 1.67/1.84 cnf(c447,plain,skolem0001!=X492|event(X492,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c305, reflexivity])).
% 1.67/1.84 cnf(c304,plain,skolem0001!=X485|skolem0005(skolem0001,skolem0002)!=X486|event(X485,X486),inference(resolution,[status(thm)],[c21, c246])).
% 1.67/1.84 cnf(c439,plain,skolem0001!=X489|event(X489,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c304, reflexivity])).
% 1.67/1.84 cnf(c303,plain,skolem0001!=X482|skolem0007(skolem0001,skolem0002)!=X483|event(X482,X483),inference(resolution,[status(thm)],[c21, c276])).
% 1.67/1.84 cnf(c437,plain,skolem0001!=X484|event(X484,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c303, reflexivity])).
% 1.67/1.84 cnf(c302,plain,skolem0001!=X477|skolem0008(skolem0001,skolem0002)!=X478|event(X477,X478),inference(resolution,[status(thm)],[c21, c290])).
% 1.67/1.84 cnf(c429,plain,skolem0001!=X479|event(X479,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c302, reflexivity])).
% 1.67/1.84 cnf(c295,plain,specific(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c291, c138])).
% 1.67/1.84 cnf(c300,plain,skolem0001!=X474|skolem0008(skolem0001,skolem0002)!=X475|specific(X474,X475),inference(resolution,[status(thm)],[c295, c13])).
% 1.67/1.84 cnf(c427,plain,skolem0001!=X476|specific(X476,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c300, reflexivity])).
% 1.67/1.84 cnf(c293,plain,unisex(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c291, c144])).
% 1.67/1.84 cnf(c298,plain,skolem0001!=X469|skolem0008(skolem0001,skolem0002)!=X470|unisex(X469,X470),inference(resolution,[status(thm)],[c293, c10])).
% 1.67/1.84 cnf(c419,plain,skolem0001!=X471|unisex(X471,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c298, reflexivity])).
% 1.67/1.84 cnf(c296,plain,skolem0001!=X465|skolem0008(skolem0001,skolem0002)!=X464|thing(X465,X464),inference(resolution,[status(thm)],[c292, c14])).
% 1.67/1.84 cnf(c411,plain,skolem0001!=X468|thing(X468,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c296, reflexivity])).
% 1.67/1.84 cnf(c281,plain,specific(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c277, c138])).
% 1.67/1.84 cnf(c286,plain,skolem0001!=X461|skolem0007(skolem0001,skolem0002)!=X462|specific(X461,X462),inference(resolution,[status(thm)],[c281, c13])).
% 1.67/1.84 cnf(c409,plain,skolem0001!=X463|specific(X463,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c286, reflexivity])).
% 1.67/1.84 cnf(c279,plain,unisex(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c277, c144])).
% 1.67/1.84 cnf(c284,plain,skolem0001!=X456|skolem0007(skolem0001,skolem0002)!=X457|unisex(X456,X457),inference(resolution,[status(thm)],[c279, c10])).
% 1.67/1.84 cnf(c401,plain,skolem0001!=X458|unisex(X458,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c284, reflexivity])).
% 1.67/1.84 cnf(c282,plain,skolem0001!=X454|skolem0007(skolem0001,skolem0002)!=X453|thing(X454,X453),inference(resolution,[status(thm)],[c278, c14])).
% 1.67/1.84 cnf(c399,plain,skolem0001!=X455|thing(X455,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c282, reflexivity])).
% 1.67/1.84 cnf(c267,plain,specific(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c263, c138])).
% 1.67/1.84 cnf(c272,plain,skolem0001!=X448|skolem0006(skolem0001,skolem0002)!=X449|specific(X448,X449),inference(resolution,[status(thm)],[c267, c13])).
% 1.67/1.84 cnf(c391,plain,skolem0001!=X450|specific(X450,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c272, reflexivity])).
% 1.67/1.84 cnf(c265,plain,unisex(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c263, c144])).
% 1.67/1.84 cnf(c270,plain,skolem0001!=X439|skolem0006(skolem0001,skolem0002)!=X440|unisex(X439,X440),inference(resolution,[status(thm)],[c265, c10])).
% 1.67/1.84 cnf(c389,plain,skolem0001!=X447|unisex(X447,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c270, reflexivity])).
% 1.67/1.84 cnf(c38,axiom,X444!=X443|X446!=X445|X441!=X442|~of(X444,X446,X441)|of(X443,X445,X442),theory(equality)).
% 1.67/1.84 cnf(c268,plain,skolem0001!=X437|skolem0006(skolem0001,skolem0002)!=X436|thing(X437,X436),inference(resolution,[status(thm)],[c264, c14])).
% 1.67/1.84 cnf(c387,plain,skolem0001!=X438|thing(X438,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c268, reflexivity])).
% 1.67/1.84 cnf(c37,axiom,X433!=X432|X435!=X434|X430!=X431|~from_loc(X433,X435,X430)|from_loc(X432,X434,X431),theory(equality)).
% 1.67/1.84 cnf(c260,plain,skolem0001!=X428|skolem0004(skolem0001,skolem0002)!=X427|thing(X428,X427),inference(resolution,[status(thm)],[c14, c236])).
% 1.67/1.84 cnf(c385,plain,skolem0001!=X429|thing(X429,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c260, reflexivity])).
% 1.67/1.84 cnf(c259,plain,skolem0001!=X425|skolem0005(skolem0001,skolem0002)!=X424|thing(X425,X424),inference(resolution,[status(thm)],[c14, c248])).
% 1.67/1.84 cnf(c383,plain,skolem0001!=X426|thing(X426,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c259, reflexivity])).
% 1.67/1.84 cnf(c251,plain,specific(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c247, c138])).
% 1.67/1.84 cnf(c256,plain,skolem0001!=X415|skolem0005(skolem0001,skolem0002)!=X416|specific(X415,X416),inference(resolution,[status(thm)],[c251, c13])).
% 1.67/1.84 cnf(c375,plain,skolem0001!=X417|specific(X417,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c256, reflexivity])).
% 1.67/1.84 cnf(c239,plain,specific(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c235, c138])).
% 1.67/1.84 cnf(c255,plain,skolem0001!=X406|skolem0004(skolem0001,skolem0002)!=X407|specific(X406,X407),inference(resolution,[status(thm)],[c13, c239])).
% 1.67/1.84 cnf(c373,plain,skolem0001!=X414|specific(X414,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c255, reflexivity])).
% 1.67/1.84 cnf(c34,axiom,X411!=X410|X413!=X412|X408!=X409|~agent(X411,X413,X408)|agent(X410,X412,X409),theory(equality)).
% 1.67/1.84 cnf(c249,plain,unisex(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c247, c144])).
% 1.67/1.84 cnf(c253,plain,skolem0001!=X403|skolem0005(skolem0001,skolem0002)!=X404|unisex(X403,X404),inference(resolution,[status(thm)],[c249, c10])).
% 1.67/1.84 cnf(c371,plain,skolem0001!=X405|unisex(X405,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c253, reflexivity])).
% 1.67/1.84 cnf(c32,axiom,X400!=X399|X402!=X401|X397!=X398|~patient(X400,X402,X397)|patient(X399,X401,X398),theory(equality)).
% 1.67/1.84 cnf(c237,plain,unisex(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c235, c144])).
% 1.67/1.84 cnf(c241,plain,skolem0001!=X394|skolem0004(skolem0001,skolem0002)!=X395|unisex(X394,X395),inference(resolution,[status(thm)],[c237, c10])).
% 1.67/1.84 cnf(c369,plain,skolem0001!=X396|unisex(X396,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c241, reflexivity])).
% 1.67/1.84 fof(ax39,axiom,(![U]:(![V]:(![W]:(![X]:(((nonreflexive(U,V)&agent(U,V,W))&patient(U,V,X))=>W!=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 1.67/1.84 fof(c95,plain,(![U]:(![V]:(![W]:(![X]:(((~nonreflexive(U,V)|~agent(U,V,W))|~patient(U,V,X))|W!=X))))),inference(fof_nnf,[status(thm)],[ax39])).
% 1.67/1.84 fof(c96,plain,(![X28]:(![X29]:(![X30]:(![X31]:(((~nonreflexive(X28,X29)|~agent(X28,X29,X30))|~patient(X28,X29,X31))|X30!=X31))))),inference(variable_rename,[status(thm)],[c95])).
% 1.67/1.84 cnf(c97,plain,~nonreflexive(X393,X391)|~agent(X393,X391,X390)|~patient(X393,X391,X392)|X390!=X392,inference(split_conjunct,[status(thm)],[c96])).
% 1.67/1.84 cnf(c39,axiom,X386!=X387|X389!=X388|~present(X386,X389)|present(X387,X388),theory(equality)).
% 1.67/1.84 cnf(c33,axiom,X382!=X383|X385!=X384|~nonreflexive(X382,X385)|nonreflexive(X383,X384),theory(equality)).
% 1.67/1.84 cnf(c55,negated_conjecture,group(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.84 fof(ax24,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 1.67/1.84 fof(c145,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 1.67/1.84 fof(c146,plain,(![X60]:(![X61]:(~group(X60,X61)|set(X60,X61)))),inference(variable_rename,[status(thm)],[c145])).
% 1.67/1.84 cnf(c147,plain,~group(X153,X154)|set(X153,X154),inference(split_conjunct,[status(thm)],[c146])).
% 1.67/1.84 cnf(c220,plain,set(skolem0001,skolem0002),inference(resolution,[status(thm)],[c147, c55])).
% 1.67/1.84 fof(ax23,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 1.67/1.84 fof(c148,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 1.67/1.84 fof(c149,plain,(![X62]:(![X63]:(~set(X62,X63)|multiple(X62,X63)))),inference(variable_rename,[status(thm)],[c148])).
% 1.67/1.84 cnf(c150,plain,~set(X155,X156)|multiple(X155,X156),inference(split_conjunct,[status(thm)],[c149])).
% 1.67/1.84 cnf(c221,plain,multiple(skolem0001,skolem0002),inference(resolution,[status(thm)],[c150, c220])).
% 1.67/1.84 cnf(c25,axiom,X330!=X331|X333!=X332|~multiple(X330,X333)|multiple(X331,X332),theory(equality)).
% 1.67/1.84 cnf(c324,plain,skolem0001!=X367|skolem0002!=X368|multiple(X367,X368),inference(resolution,[status(thm)],[c25, c221])).
% 1.67/1.84 cnf(c349,plain,skolem0001!=X369|multiple(X369,skolem0002),inference(resolution,[status(thm)],[c324, reflexivity])).
% 1.67/1.84 cnf(c24,axiom,X316!=X317|X319!=X318|~set(X316,X319)|set(X317,X318),theory(equality)).
% 1.67/1.84 cnf(c323,plain,skolem0001!=X360|skolem0002!=X361|set(X360,X361),inference(resolution,[status(thm)],[c24, c220])).
% 1.67/1.84 cnf(c341,plain,skolem0001!=X362|set(X362,skolem0002),inference(resolution,[status(thm)],[c323, reflexivity])).
% 1.67/1.84 cnf(c23,axiom,X304!=X305|X307!=X306|~group(X304,X307)|group(X305,X306),theory(equality)).
% 1.67/1.84 cnf(c322,plain,skolem0001!=X353|skolem0002!=X354|group(X353,X354),inference(resolution,[status(thm)],[c23, c55])).
% 1.67/1.84 cnf(c333,plain,skolem0001!=X359|group(X359,skolem0002),inference(resolution,[status(thm)],[c322, reflexivity])).
% 1.67/1.84 cnf(c22,axiom,X300!=X301|X303!=X302|~six(X300,X303)|six(X301,X302),theory(equality)).
% 1.67/1.84 cnf(c316,plain,skolem0001!=X351|skolem0002!=X350|six(X351,X350),inference(resolution,[status(thm)],[c22, c54])).
% 1.67/1.84 cnf(c331,plain,skolem0001!=X352|six(X352,skolem0002),inference(resolution,[status(thm)],[c316, reflexivity])).
% 1.67/1.84 cnf(c86,plain,~six(X348,X349)|skolem0009(X348,X349)!=skolem0004(X348,X349),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c85,plain,~six(X342,X343)|skolem0009(X342,X343)!=skolem0005(X342,X343),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c84,plain,~six(X340,X341)|skolem0009(X340,X341)!=skolem0006(X340,X341),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c83,plain,~six(X338,X339)|skolem0009(X338,X339)!=skolem0007(X338,X339),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c82,plain,~six(X336,X337)|skolem0009(X336,X337)!=skolem0008(X336,X337),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c80,plain,~six(X334,X335)|skolem0008(X334,X335)!=skolem0004(X334,X335),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c79,plain,~six(X328,X329)|skolem0008(X328,X329)!=skolem0005(X328,X329),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c78,plain,~six(X326,X327)|skolem0008(X326,X327)!=skolem0006(X326,X327),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c77,plain,~six(X324,X325)|skolem0008(X324,X325)!=skolem0007(X324,X325),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c75,plain,~six(X322,X323)|skolem0007(X322,X323)!=skolem0004(X322,X323),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c74,plain,~six(X320,X321)|skolem0007(X320,X321)!=skolem0005(X320,X321),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c73,plain,~six(X314,X315)|skolem0007(X314,X315)!=skolem0006(X314,X315),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c71,plain,~six(X312,X313)|skolem0006(X312,X313)!=skolem0004(X312,X313),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c70,plain,~six(X310,X311)|skolem0006(X310,X311)!=skolem0005(X310,X311),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 cnf(c68,plain,~six(X308,X309)|skolem0005(X308,X309)!=skolem0004(X308,X309),inference(split_conjunct,[status(thm)],[c65])).
% 1.67/1.84 fof(ax35,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 1.67/1.84 fof(c110,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax35])).
% 1.67/1.84 fof(c111,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c110])).
% 1.67/1.84 fof(c112,plain,(![X38]:(![X39]:(~existent(X38,X39)|~nonexistent(X38,X39)))),inference(variable_rename,[status(thm)],[c111])).
% 1.67/1.84 cnf(c113,plain,~existent(X121,X120)|~nonexistent(X121,X120),inference(split_conjunct,[status(thm)],[c112])).
% 1.67/1.84 cnf(c320,plain,~existent(skolem0001,skolem0009(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c314, c113])).
% 1.67/1.84 cnf(c299,plain,~existent(skolem0001,skolem0008(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c294, c113])).
% 1.67/1.84 cnf(c20,axiom,X292!=X293|X295!=X294|~fire(X292,X295)|fire(X293,X294),theory(equality)).
% 1.67/1.84 cnf(c19,axiom,X288!=X289|X291!=X290|~cannon(X288,X291)|cannon(X289,X290),theory(equality)).
% 1.67/1.84 cnf(c285,plain,~existent(skolem0001,skolem0007(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c280, c113])).
% 1.67/1.84 cnf(c18,axiom,X284!=X285|X287!=X286|~weapon(X284,X287)|weapon(X285,X286),theory(equality)).
% 1.67/1.84 cnf(c17,axiom,X280!=X281|X283!=X282|~weaponry(X280,X283)|weaponry(X281,X282),theory(equality)).
% 1.67/1.84 cnf(c16,axiom,X276!=X277|X279!=X278|~instrumentality(X276,X279)|instrumentality(X277,X278),theory(equality)).
% 1.67/1.84 cnf(c271,plain,~existent(skolem0001,skolem0006(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c266, c113])).
% 1.67/1.84 cnf(c15,axiom,X272!=X273|X275!=X274|~artifact(X272,X275)|artifact(X273,X274),theory(equality)).
% 1.67/1.84 cnf(c254,plain,~existent(skolem0001,skolem0005(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c250, c113])).
% 1.67/1.84 cnf(c12,axiom,X260!=X261|X263!=X262|~existent(X260,X263)|existent(X261,X262),theory(equality)).
% 1.67/1.84 cnf(c242,plain,~existent(skolem0001,skolem0004(skolem0001,skolem0002)),inference(resolution,[status(thm)],[c238, c113])).
% 1.67/1.84 cnf(c11,axiom,X256!=X257|X259!=X258|~nonliving(X256,X259)|nonliving(X257,X258),theory(equality)).
% 1.67/1.84 cnf(c9,axiom,X248!=X249|X251!=X250|~object(X248,X251)|object(X249,X250),theory(equality)).
% 1.67/1.84 cnf(c8,axiom,X236!=X237|X239!=X238|~entity(X236,X239)|entity(X237,X238),theory(equality)).
% 1.67/1.84 cnf(c36,axiom,X228!=X229|~actual_world(X228)|actual_world(X229),theory(equality)).
% 1.67/1.84 cnf(c7,axiom,X224!=X225|X227!=X226|~impartial(X224,X227)|impartial(X225,X226),theory(equality)).
% 1.67/1.84 fof(ax1,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 1.67/1.84 fof(c214,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 1.67/1.84 fof(c215,plain,(![X106]:(![X107]:(~man(X106,X107)|male(X106,X107)))),inference(variable_rename,[status(thm)],[c214])).
% 1.67/1.84 cnf(c216,plain,~man(X219,X220)|male(X219,X220),inference(split_conjunct,[status(thm)],[c215])).
% 1.67/1.84 fof(ax2,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 1.67/1.84 fof(c211,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 1.67/1.84 fof(c212,plain,(![X104]:(![X105]:(~human_person(X104,X105)|animate(X104,X105)))),inference(variable_rename,[status(thm)],[c211])).
% 1.67/1.84 cnf(c213,plain,~human_person(X218,X217)|animate(X218,X217),inference(split_conjunct,[status(thm)],[c212])).
% 1.67/1.84 fof(ax3,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 1.67/1.84 fof(c208,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 1.67/1.84 fof(c209,plain,(![X102]:(![X103]:(~human_person(X102,X103)|human(X102,X103)))),inference(variable_rename,[status(thm)],[c208])).
% 1.67/1.84 cnf(c210,plain,~human_person(X215,X216)|human(X215,X216),inference(split_conjunct,[status(thm)],[c209])).
% 1.67/1.84 cnf(c6,axiom,X211!=X212|X214!=X213|~living(X211,X214)|living(X212,X213),theory(equality)).
% 1.67/1.84 fof(ax4,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 1.67/1.84 fof(c205,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 1.67/1.84 fof(c206,plain,(![X100]:(![X101]:(~organism(X100,X101)|living(X100,X101)))),inference(variable_rename,[status(thm)],[c205])).
% 1.67/1.84 cnf(c207,plain,~organism(X210,X209)|living(X210,X209),inference(split_conjunct,[status(thm)],[c206])).
% 1.67/1.84 fof(ax5,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 1.67/1.84 fof(c202,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 1.67/1.84 fof(c203,plain,(![X98]:(![X99]:(~organism(X98,X99)|impartial(X98,X99)))),inference(variable_rename,[status(thm)],[c202])).
% 1.67/1.84 cnf(c204,plain,~organism(X207,X208)|impartial(X207,X208),inference(split_conjunct,[status(thm)],[c203])).
% 1.67/1.84 fof(ax6,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 1.67/1.84 fof(c199,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 1.67/1.84 fof(c200,plain,(![X96]:(![X97]:(~organism(X96,X97)|entity(X96,X97)))),inference(variable_rename,[status(thm)],[c199])).
% 1.67/1.84 cnf(c201,plain,~organism(X205,X206)|entity(X205,X206),inference(split_conjunct,[status(thm)],[c200])).
% 1.67/1.84 fof(ax7,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 1.67/1.84 fof(c196,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 1.67/1.84 fof(c197,plain,(![X94]:(![X95]:(~human_person(X94,X95)|organism(X94,X95)))),inference(variable_rename,[status(thm)],[c196])).
% 1.67/1.85 cnf(c198,plain,~human_person(X203,X204)|organism(X203,X204),inference(split_conjunct,[status(thm)],[c197])).
% 1.67/1.85 fof(ax8,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 1.67/1.85 fof(c193,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 1.67/1.85 fof(c194,plain,(![X92]:(![X93]:(~man(X92,X93)|human_person(X92,X93)))),inference(variable_rename,[status(thm)],[c193])).
% 1.67/1.85 cnf(c195,plain,~man(X201,X202)|human_person(X201,X202),inference(split_conjunct,[status(thm)],[c194])).
% 1.67/1.85 cnf(c5,axiom,X197!=X198|X200!=X199|~organism(X197,X200)|organism(X198,X199),theory(equality)).
% 1.67/1.85 fof(ax9,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 1.67/1.85 fof(c190,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 1.67/1.85 fof(c191,plain,(![X90]:(![X91]:(~object(X90,X91)|unisex(X90,X91)))),inference(variable_rename,[status(thm)],[c190])).
% 1.67/1.85 cnf(c192,plain,~object(X196,X195)|unisex(X196,X195),inference(split_conjunct,[status(thm)],[c191])).
% 1.67/1.85 fof(ax10,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 1.67/1.85 fof(c187,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 1.67/1.85 fof(c188,plain,(![X88]:(![X89]:(~object(X88,X89)|impartial(X88,X89)))),inference(variable_rename,[status(thm)],[c187])).
% 1.67/1.85 cnf(c189,plain,~object(X194,X193)|impartial(X194,X193),inference(split_conjunct,[status(thm)],[c188])).
% 1.67/1.85 fof(ax11,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 1.67/1.85 fof(c184,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 1.67/1.85 fof(c185,plain,(![X86]:(![X87]:(~object(X86,X87)|nonliving(X86,X87)))),inference(variable_rename,[status(thm)],[c184])).
% 1.67/1.85 cnf(c186,plain,~object(X192,X191)|nonliving(X192,X191),inference(split_conjunct,[status(thm)],[c185])).
% 1.67/1.85 fof(ax12,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 1.67/1.85 fof(c181,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 1.67/1.85 fof(c182,plain,(![X84]:(![X85]:(~entity(X84,X85)|existent(X84,X85)))),inference(variable_rename,[status(thm)],[c181])).
% 1.67/1.85 cnf(c183,plain,~entity(X189,X190)|existent(X189,X190),inference(split_conjunct,[status(thm)],[c182])).
% 1.67/1.85 fof(ax13,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 1.67/1.85 fof(c178,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 1.67/1.85 fof(c179,plain,(![X82]:(![X83]:(~entity(X82,X83)|specific(X82,X83)))),inference(variable_rename,[status(thm)],[c178])).
% 1.67/1.85 cnf(c180,plain,~entity(X187,X188)|specific(X187,X188),inference(split_conjunct,[status(thm)],[c179])).
% 1.67/1.85 cnf(c4,axiom,X183!=X184|X186!=X185|~human(X183,X186)|human(X184,X185),theory(equality)).
% 1.67/1.85 fof(ax14,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 1.67/1.85 fof(c175,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 1.67/1.85 fof(c176,plain,(![X80]:(![X81]:(~entity(X80,X81)|thing(X80,X81)))),inference(variable_rename,[status(thm)],[c175])).
% 1.67/1.85 cnf(c177,plain,~entity(X182,X181)|thing(X182,X181),inference(split_conjunct,[status(thm)],[c176])).
% 1.67/1.85 fof(ax15,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 1.67/1.85 fof(c172,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 1.67/1.85 fof(c173,plain,(![X78]:(![X79]:(~object(X78,X79)|entity(X78,X79)))),inference(variable_rename,[status(thm)],[c172])).
% 1.67/1.85 cnf(c174,plain,~object(X179,X180)|entity(X179,X180),inference(split_conjunct,[status(thm)],[c173])).
% 1.67/1.85 fof(ax16,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 1.67/1.85 fof(c169,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 1.67/1.85 fof(c170,plain,(![X76]:(![X77]:(~artifact(X76,X77)|object(X76,X77)))),inference(variable_rename,[status(thm)],[c169])).
% 1.67/1.85 cnf(c171,plain,~artifact(X178,X177)|object(X178,X177),inference(split_conjunct,[status(thm)],[c170])).
% 1.67/1.85 fof(ax17,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 1.67/1.85 fof(c166,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 1.67/1.85 fof(c167,plain,(![X74]:(![X75]:(~instrumentality(X74,X75)|artifact(X74,X75)))),inference(variable_rename,[status(thm)],[c166])).
% 1.67/1.85 cnf(c168,plain,~instrumentality(X176,X175)|artifact(X176,X175),inference(split_conjunct,[status(thm)],[c167])).
% 1.67/1.85 fof(ax18,axiom,(![U]:(![V]:(weaponry(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 1.67/1.85 fof(c163,plain,(![U]:(![V]:(~weaponry(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 1.67/1.85 fof(c164,plain,(![X72]:(![X73]:(~weaponry(X72,X73)|instrumentality(X72,X73)))),inference(variable_rename,[status(thm)],[c163])).
% 1.67/1.85 cnf(c165,plain,~weaponry(X173,X174)|instrumentality(X173,X174),inference(split_conjunct,[status(thm)],[c164])).
% 1.67/1.85 cnf(c3,axiom,X169!=X170|X172!=X171|~animate(X169,X172)|animate(X170,X171),theory(equality)).
% 1.67/1.85 fof(ax19,axiom,(![U]:(![V]:(weapon(U,V)=>weaponry(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 1.67/1.85 fof(c160,plain,(![U]:(![V]:(~weapon(U,V)|weaponry(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 1.67/1.85 fof(c161,plain,(![X70]:(![X71]:(~weapon(X70,X71)|weaponry(X70,X71)))),inference(variable_rename,[status(thm)],[c160])).
% 1.67/1.85 cnf(c162,plain,~weapon(X168,X167)|weaponry(X168,X167),inference(split_conjunct,[status(thm)],[c161])).
% 1.67/1.85 fof(ax20,axiom,(![U]:(![V]:(cannon(U,V)=>weapon(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 1.67/1.85 fof(c157,plain,(![U]:(![V]:(~cannon(U,V)|weapon(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 1.67/1.85 fof(c158,plain,(![X68]:(![X69]:(~cannon(X68,X69)|weapon(X68,X69)))),inference(variable_rename,[status(thm)],[c157])).
% 1.67/1.85 cnf(c159,plain,~cannon(X166,X165)|weapon(X166,X165),inference(split_conjunct,[status(thm)],[c158])).
% 1.67/1.85 fof(ax21,axiom,(![U]:(![V]:(fire(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 1.67/1.85 fof(c154,plain,(![U]:(![V]:(~fire(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 1.67/1.85 fof(c155,plain,(![X66]:(![X67]:(~fire(X66,X67)|event(X66,X67)))),inference(variable_rename,[status(thm)],[c154])).
% 1.67/1.85 cnf(c156,plain,~fire(X163,X164)|event(X163,X164),inference(split_conjunct,[status(thm)],[c155])).
% 1.67/1.85 fof(ax22,axiom,(![U]:(![V]:(six(U,V)=>group(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 1.67/1.85 fof(c151,plain,(![U]:(![V]:(~six(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 1.67/1.85 fof(c152,plain,(![X64]:(![X65]:(~six(X64,X65)|group(X64,X65)))),inference(variable_rename,[status(thm)],[c151])).
% 1.67/1.85 cnf(c153,plain,~six(X161,X162)|group(X161,X162),inference(split_conjunct,[status(thm)],[c152])).
% 1.67/1.85 cnf(c2,axiom,X157!=X158|X160!=X159|~human_person(X157,X160)|human_person(X158,X159),theory(equality)).
% 1.67/1.85 fof(ax37,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 1.67/1.85 fof(c102,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax37])).
% 1.67/1.85 fof(c103,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c102])).
% 1.67/1.85 fof(c104,plain,(![X34]:(![X35]:(~singleton(X34,X35)|~multiple(X34,X35)))),inference(variable_rename,[status(thm)],[c103])).
% 1.67/1.85 cnf(c105,plain,~singleton(X117,X116)|~multiple(X117,X116),inference(split_conjunct,[status(thm)],[c104])).
% 1.67/1.85 cnf(c222,plain,~singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c221, c105])).
% 1.67/1.85 cnf(c1,axiom,X149!=X150|X152!=X151|~male(X149,X152)|male(X150,X151),theory(equality)).
% 1.67/1.85 cnf(c0,axiom,X135!=X136|X138!=X137|~man(X135,X138)|man(X136,X137),theory(equality)).
% 1.67/1.85 fof(ax34,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 1.67/1.85 fof(c114,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax34])).
% 1.67/1.85 fof(c115,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c114])).
% 1.67/1.85 fof(c116,plain,(![X40]:(![X41]:(~animate(X40,X41)|~nonliving(X40,X41)))),inference(variable_rename,[status(thm)],[c115])).
% 1.67/1.85 cnf(c117,plain,~animate(X125,X126)|~nonliving(X125,X126),inference(split_conjunct,[status(thm)],[c116])).
% 1.67/1.85 cnf(transitivity,axiom,X122!=X123|X123!=X124|X122=X124,theory(equality)).
% 1.67/1.85 fof(ax36,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 1.67/1.85 fof(c106,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax36])).
% 1.67/1.85 fof(c107,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c106])).
% 1.67/1.85 fof(c108,plain,(![X36]:(![X37]:(~nonliving(X36,X37)|~living(X36,X37)))),inference(variable_rename,[status(thm)],[c107])).
% 1.67/1.85 cnf(c109,plain,~nonliving(X119,X118)|~living(X119,X118),inference(split_conjunct,[status(thm)],[c108])).
% 1.67/1.85 fof(ax38,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 1.67/1.85 fof(c98,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax38])).
% 1.67/1.85 fof(c99,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c98])).
% 1.67/1.85 fof(c100,plain,(![X32]:(![X33]:(~unisex(X32,X33)|~male(X32,X33)))),inference(variable_rename,[status(thm)],[c99])).
% 1.67/1.85 cnf(c101,plain,~unisex(X114,X115)|~male(X114,X115),inference(split_conjunct,[status(thm)],[c100])).
% 1.67/1.85 cnf(symmetry,axiom,X111!=X112|X112=X111,theory(equality)).
% 1.67/1.85 fof(ax41,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 1.67/1.85 fof(c57,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax41])).
% 1.67/1.85 fof(c58,plain,(![X8]:(![X9]:~member(X8,X9,X9))),inference(variable_rename,[status(thm)],[c57])).
% 1.67/1.85 cnf(c59,plain,~member(X109,X110,X110),inference(split_conjunct,[status(thm)],[c58])).
% 1.67/1.85 cnf(c46,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c45])).
% 1.67/1.85 % SZS output end Saturation
% 1.67/1.85
% 1.67/1.85 % Initial clauses : 123
% 1.67/1.85 % Processed clauses : 386
% 1.67/1.85 % Factors computed : 6
% 1.67/1.85 % Resolvents computed: 349
% 1.67/1.85 % Tautologies deleted: 3
% 1.67/1.85 % Forward subsumed : 89
% 1.67/1.85 % Backward subsumed : 0
% 1.67/1.85 % -------- CPU Time ---------
% 1.67/1.85 % User time : 1.472 s
% 1.67/1.85 % System time : 0.025 s
% 1.67/1.85 % Total time : 1.497 s
%------------------------------------------------------------------------------