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