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