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