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