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