%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP090+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:34:00 EDT 2024
% Result : CounterSatisfiable 2.26s 2.49s
% Output : Saturation 2.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : NLP090+1 : TPTP v8.1.2. Released v2.4.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n013.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 13:28:38 EDT 2024
% 0.21/0.36 % CPUTime :
% 2.26/2.49 % Version: 1.5
% 2.26/2.49 % SZS status CounterSatisfiable
% 2.26/2.49 % SZS output start Saturation
% 2.26/2.49 fof(co1,conjecture,(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(((((((male(U,V)&man(U,V))&of(U,W,V))&cannon(U,W))&(![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,W))))))&six(U,X))&group(U,X))&(![X1]:(member(U,X1,X)=>shot(U,X1)))))))))&(~(?[X2]:(actual_world(X2)&(?[V]:(?[W]:(?[X]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((((male(X2,X)&male(X2,V))&man(X2,V))&of(X2,W,V))&cannon(X2,W))&(![Y]:(member(X2,Y,X)=>(?[Z]:((((((event(X2,Z)&agent(X2,Z,V))&patient(X2,Z,Y))&present(X2,Z))&nonreflexive(X2,Z))&fire(X2,Z))&from_loc(X2,Z,W))))))&six(X2,X))&group(X2,X))&(![X1]:(member(X2,X1,X)=>shot(X2,X1))))&cry(X2,X3))&revenge(X2,X4))&event(X2,X5))&agent(X2,X5,X))&patient(X2,X5,X3))&present(X2,X5))&nonreflexive(X2,X5))&scream(X2,X5))&of(X2,X5,X4))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 2.26/2.49 fof(c44,negated_conjecture,(~(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(((((((male(U,V)&man(U,V))&of(U,W,V))&cannon(U,W))&(![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,W))))))&six(U,X))&group(U,X))&(![X1]:(member(U,X1,X)=>shot(U,X1)))))))))&(~(?[X2]:(actual_world(X2)&(?[V]:(?[W]:(?[X]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((((male(X2,X)&male(X2,V))&man(X2,V))&of(X2,W,V))&cannon(X2,W))&(![Y]:(member(X2,Y,X)=>(?[Z]:((((((event(X2,Z)&agent(X2,Z,V))&patient(X2,Z,Y))&present(X2,Z))&nonreflexive(X2,Z))&fire(X2,Z))&from_loc(X2,Z,W))))))&six(X2,X))&group(X2,X))&(![X1]:(member(X2,X1,X)=>shot(X2,X1))))&cry(X2,X3))&revenge(X2,X4))&event(X2,X5))&agent(X2,X5,X))&patient(X2,X5,X3))&present(X2,X5))&nonreflexive(X2,X5))&scream(X2,X5))&of(X2,X5,X4)))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 2.26/2.49 fof(c45,negated_conjecture,((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(((((((male(U,V)&man(U,V))&of(U,W,V))&cannon(U,W))&(![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,W))))))&six(U,X))&group(U,X))&(![X1]:(~member(U,X1,X)|shot(U,X1)))))))))&(![X2]:(~actual_world(X2)|(![V]:(![W]:(![X]:(![X3]:(![X4]:(![X5]:(((((((((((((((((~male(X2,X)|~male(X2,V))|~man(X2,V))|~of(X2,W,V))|~cannon(X2,W))|(?[Y]:(member(X2,Y,X)&(![Z]:((((((~event(X2,Z)|~agent(X2,Z,V))|~patient(X2,Z,Y))|~present(X2,Z))|~nonreflexive(X2,Z))|~fire(X2,Z))|~from_loc(X2,Z,W))))))|~six(X2,X))|~group(X2,X))|(?[X1]:(member(X2,X1,X)&~shot(X2,X1))))|~cry(X2,X3))|~revenge(X2,X4))|~event(X2,X5))|~agent(X2,X5,X))|~patient(X2,X5,X3))|~present(X2,X5))|~nonreflexive(X2,X5))|~scream(X2,X5))|~of(X2,X5,X4))))))))))),inference(fof_nnf,[status(thm)],[c44])).
% 2.26/2.49 fof(c46,negated_conjecture,((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(((((((male(X2,X3)&man(X2,X3))&of(X2,X4,X3))&cannon(X2,X4))&(![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,X4))))))&six(X2,X5))&group(X2,X5))&(![X8]:(~member(X2,X8,X5)|shot(X2,X8)))))))))&(![X9]:(~actual_world(X9)|(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(((((((((((((((((~male(X9,X12)|~male(X9,X10))|~man(X9,X10))|~of(X9,X11,X10))|~cannon(X9,X11))|(?[X16]:(member(X9,X16,X12)&(![X17]:((((((~event(X9,X17)|~agent(X9,X17,X10))|~patient(X9,X17,X16))|~present(X9,X17))|~nonreflexive(X9,X17))|~fire(X9,X17))|~from_loc(X9,X17,X11))))))|~six(X9,X12))|~group(X9,X12))|(?[X18]:(member(X9,X18,X12)&~shot(X9,X18))))|~cry(X9,X13))|~revenge(X9,X14))|~event(X9,X15))|~agent(X9,X15,X12))|~patient(X9,X15,X13))|~present(X9,X15))|~nonreflexive(X9,X15))|~scream(X9,X15))|~of(X9,X15,X14))))))))))),inference(variable_rename,[status(thm)],[c45])).
% 2.26/2.49 fof(c48,negated_conjecture,(![X6]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X17]:((actual_world(skolem0001)&(((((((male(skolem0001,skolem0002)&man(skolem0001,skolem0002))&of(skolem0001,skolem0003,skolem0002))&cannon(skolem0001,skolem0003))&(~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),skolem0003))))&six(skolem0001,skolem0004))&group(skolem0001,skolem0004))&(~member(skolem0001,X8,skolem0004)|shot(skolem0001,X8))))&(~actual_world(X9)|(((((((((((((((((~male(X9,X12)|~male(X9,X10))|~man(X9,X10))|~of(X9,X11,X10))|~cannon(X9,X11))|(member(X9,skolem0006(X9,X10,X11,X12,X13,X14,X15),X12)&((((((~event(X9,X17)|~agent(X9,X17,X10))|~patient(X9,X17,skolem0006(X9,X10,X11,X12,X13,X14,X15)))|~present(X9,X17))|~nonreflexive(X9,X17))|~fire(X9,X17))|~from_loc(X9,X17,X11))))|~six(X9,X12))|~group(X9,X12))|(member(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15),X12)&~shot(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15))))|~cry(X9,X13))|~revenge(X9,X14))|~event(X9,X15))|~agent(X9,X15,X12))|~patient(X9,X15,X13))|~present(X9,X15))|~nonreflexive(X9,X15))|~scream(X9,X15))|~of(X9,X15,X14)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c47,negated_conjecture,((actual_world(skolem0001)&(((((((male(skolem0001,skolem0002)&man(skolem0001,skolem0002))&of(skolem0001,skolem0003,skolem0002))&cannon(skolem0001,skolem0003))&(![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),skolem0003)))))&six(skolem0001,skolem0004))&group(skolem0001,skolem0004))&(![X8]:(~member(skolem0001,X8,skolem0004)|shot(skolem0001,X8)))))&(![X9]:(~actual_world(X9)|(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(((((((((((((((((~male(X9,X12)|~male(X9,X10))|~man(X9,X10))|~of(X9,X11,X10))|~cannon(X9,X11))|(member(X9,skolem0006(X9,X10,X11,X12,X13,X14,X15),X12)&(![X17]:((((((~event(X9,X17)|~agent(X9,X17,X10))|~patient(X9,X17,skolem0006(X9,X10,X11,X12,X13,X14,X15)))|~present(X9,X17))|~nonreflexive(X9,X17))|~fire(X9,X17))|~from_loc(X9,X17,X11)))))|~six(X9,X12))|~group(X9,X12))|(member(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15),X12)&~shot(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15))))|~cry(X9,X13))|~revenge(X9,X14))|~event(X9,X15))|~agent(X9,X15,X12))|~patient(X9,X15,X13))|~present(X9,X15))|~nonreflexive(X9,X15))|~scream(X9,X15))|~of(X9,X15,X14))))))))))),inference(skolemize,[status(esa)],[c46])).])).
% 2.26/2.49 fof(c49,negated_conjecture,(![X6]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X17]:((actual_world(skolem0001)&(((((((male(skolem0001,skolem0002)&man(skolem0001,skolem0002))&of(skolem0001,skolem0003,skolem0002))&cannon(skolem0001,skolem0003))&(((((((~member(skolem0001,X6,skolem0004)|event(skolem0001,skolem0005(X6)))&(~member(skolem0001,X6,skolem0004)|agent(skolem0001,skolem0005(X6),skolem0002)))&(~member(skolem0001,X6,skolem0004)|patient(skolem0001,skolem0005(X6),X6)))&(~member(skolem0001,X6,skolem0004)|present(skolem0001,skolem0005(X6))))&(~member(skolem0001,X6,skolem0004)|nonreflexive(skolem0001,skolem0005(X6))))&(~member(skolem0001,X6,skolem0004)|fire(skolem0001,skolem0005(X6))))&(~member(skolem0001,X6,skolem0004)|from_loc(skolem0001,skolem0005(X6),skolem0003))))&six(skolem0001,skolem0004))&group(skolem0001,skolem0004))&(~member(skolem0001,X8,skolem0004)|shot(skolem0001,X8))))&(((~actual_world(X9)|(((((((((((((((((~male(X9,X12)|~male(X9,X10))|~man(X9,X10))|~of(X9,X11,X10))|~cannon(X9,X11))|member(X9,skolem0006(X9,X10,X11,X12,X13,X14,X15),X12))|~six(X9,X12))|~group(X9,X12))|member(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15),X12))|~cry(X9,X13))|~revenge(X9,X14))|~event(X9,X15))|~agent(X9,X15,X12))|~patient(X9,X15,X13))|~present(X9,X15))|~nonreflexive(X9,X15))|~scream(X9,X15))|~of(X9,X15,X14)))&(~actual_world(X9)|(((((((((((((((((~male(X9,X12)|~male(X9,X10))|~man(X9,X10))|~of(X9,X11,X10))|~cannon(X9,X11))|member(X9,skolem0006(X9,X10,X11,X12,X13,X14,X15),X12))|~six(X9,X12))|~group(X9,X12))|~shot(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15)))|~cry(X9,X13))|~revenge(X9,X14))|~event(X9,X15))|~agent(X9,X15,X12))|~patient(X9,X15,X13))|~present(X9,X15))|~nonreflexive(X9,X15))|~scream(X9,X15))|~of(X9,X15,X14))))&((~actual_world(X9)|(((((((((((((((((~male(X9,X12)|~male(X9,X10))|~man(X9,X10))|~of(X9,X11,X10))|~cannon(X9,X11))|((((((~event(X9,X17)|~agent(X9,X17,X10))|~patient(X9,X17,skolem0006(X9,X10,X11,X12,X13,X14,X15)))|~present(X9,X17))|~nonreflexive(X9,X17))|~fire(X9,X17))|~from_loc(X9,X17,X11)))|~six(X9,X12))|~group(X9,X12))|member(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15),X12))|~cry(X9,X13))|~revenge(X9,X14))|~event(X9,X15))|~agent(X9,X15,X12))|~patient(X9,X15,X13))|~present(X9,X15))|~nonreflexive(X9,X15))|~scream(X9,X15))|~of(X9,X15,X14)))&(~actual_world(X9)|(((((((((((((((((~male(X9,X12)|~male(X9,X10))|~man(X9,X10))|~of(X9,X11,X10))|~cannon(X9,X11))|((((((~event(X9,X17)|~agent(X9,X17,X10))|~patient(X9,X17,skolem0006(X9,X10,X11,X12,X13,X14,X15)))|~present(X9,X17))|~nonreflexive(X9,X17))|~fire(X9,X17))|~from_loc(X9,X17,X11)))|~six(X9,X12))|~group(X9,X12))|~shot(X9,skolem0007(X9,X10,X11,X12,X13,X14,X15)))|~cry(X9,X13))|~revenge(X9,X14))|~event(X9,X15))|~agent(X9,X15,X12))|~patient(X9,X15,X13))|~present(X9,X15))|~nonreflexive(X9,X15))|~scream(X9,X15))|~of(X9,X15,X14)))))))))))))))),inference(distribute,[status(thm)],[c48])).
% 2.26/2.49 cnf(c62,negated_conjecture,six(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.49 fof(ax44,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', ax44)).
% 2.26/2.49 fof(c75,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)],[ax44])).
% 2.26/2.49 fof(c76,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)],[c75])).
% 2.26/2.49 fof(c77,plain,((![X25]:(![X26]:(~six(X25,X26)|(?[X27]:(member(X25,X27,X26)&(?[X28]:((member(X25,X28,X26)&X28!=X27)&(?[X29]:(((member(X25,X29,X26)&X29!=X28)&X29!=X27)&(?[X30]:((((member(X25,X30,X26)&X30!=X29)&X30!=X28)&X30!=X27)&(?[X31]:(((((member(X25,X31,X26)&X31!=X30)&X31!=X29)&X31!=X28)&X31!=X27)&(?[X32]:((((((member(X25,X32,X26)&X32!=X31)&X32!=X30)&X32!=X29)&X32!=X28)&X32!=X27)&(![X33]:(~member(X25,X33,X26)|(((((X33=X32|X33=X31)|X33=X30)|X33=X29)|X33=X28)|X33=X27))))))))))))))))))&(![X34]:(![X35]:((![X36]:(~member(X34,X36,X35)|(![X37]:((~member(X34,X37,X35)|X37=X36)|(![X38]:(((~member(X34,X38,X35)|X38=X37)|X38=X36)|(![X39]:((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(![X40]:(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|(![X41]:((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|(?[X42]:(member(X34,X42,X35)&(((((X42!=X41&X42!=X40)&X42!=X39)&X42!=X38)&X42!=X37)&X42!=X36)))))))))))))))|six(X34,X35))))),inference(variable_rename,[status(thm)],[c76])).
% 2.26/2.49 fof(c79,plain,(![X25]:(![X26]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:((~six(X25,X26)|(member(X25,skolem0008(X25,X26),X26)&((member(X25,skolem0009(X25,X26),X26)&skolem0009(X25,X26)!=skolem0008(X25,X26))&(((member(X25,skolem0010(X25,X26),X26)&skolem0010(X25,X26)!=skolem0009(X25,X26))&skolem0010(X25,X26)!=skolem0008(X25,X26))&((((member(X25,skolem0011(X25,X26),X26)&skolem0011(X25,X26)!=skolem0010(X25,X26))&skolem0011(X25,X26)!=skolem0009(X25,X26))&skolem0011(X25,X26)!=skolem0008(X25,X26))&(((((member(X25,skolem0012(X25,X26),X26)&skolem0012(X25,X26)!=skolem0011(X25,X26))&skolem0012(X25,X26)!=skolem0010(X25,X26))&skolem0012(X25,X26)!=skolem0009(X25,X26))&skolem0012(X25,X26)!=skolem0008(X25,X26))&((((((member(X25,skolem0013(X25,X26),X26)&skolem0013(X25,X26)!=skolem0012(X25,X26))&skolem0013(X25,X26)!=skolem0011(X25,X26))&skolem0013(X25,X26)!=skolem0010(X25,X26))&skolem0013(X25,X26)!=skolem0009(X25,X26))&skolem0013(X25,X26)!=skolem0008(X25,X26))&(~member(X25,X33,X26)|(((((X33=skolem0013(X25,X26)|X33=skolem0012(X25,X26))|X33=skolem0011(X25,X26))|X33=skolem0010(X25,X26))|X33=skolem0009(X25,X26))|X33=skolem0008(X25,X26))))))))))&((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|(member(X34,skolem0014(X34,X35,X36,X37,X38,X39,X40,X41),X35)&(((((skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X41&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X40)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X39)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X38)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X37)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X36))))))))|six(X34,X35)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,((![X25]:(![X26]:(~six(X25,X26)|(member(X25,skolem0008(X25,X26),X26)&((member(X25,skolem0009(X25,X26),X26)&skolem0009(X25,X26)!=skolem0008(X25,X26))&(((member(X25,skolem0010(X25,X26),X26)&skolem0010(X25,X26)!=skolem0009(X25,X26))&skolem0010(X25,X26)!=skolem0008(X25,X26))&((((member(X25,skolem0011(X25,X26),X26)&skolem0011(X25,X26)!=skolem0010(X25,X26))&skolem0011(X25,X26)!=skolem0009(X25,X26))&skolem0011(X25,X26)!=skolem0008(X25,X26))&(((((member(X25,skolem0012(X25,X26),X26)&skolem0012(X25,X26)!=skolem0011(X25,X26))&skolem0012(X25,X26)!=skolem0010(X25,X26))&skolem0012(X25,X26)!=skolem0009(X25,X26))&skolem0012(X25,X26)!=skolem0008(X25,X26))&((((((member(X25,skolem0013(X25,X26),X26)&skolem0013(X25,X26)!=skolem0012(X25,X26))&skolem0013(X25,X26)!=skolem0011(X25,X26))&skolem0013(X25,X26)!=skolem0010(X25,X26))&skolem0013(X25,X26)!=skolem0009(X25,X26))&skolem0013(X25,X26)!=skolem0008(X25,X26))&(![X33]:(~member(X25,X33,X26)|(((((X33=skolem0013(X25,X26)|X33=skolem0012(X25,X26))|X33=skolem0011(X25,X26))|X33=skolem0010(X25,X26))|X33=skolem0009(X25,X26))|X33=skolem0008(X25,X26)))))))))))))&(![X34]:(![X35]:((![X36]:(~member(X34,X36,X35)|(![X37]:((~member(X34,X37,X35)|X37=X36)|(![X38]:(((~member(X34,X38,X35)|X38=X37)|X38=X36)|(![X39]:((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(![X40]:(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|(![X41]:((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|(member(X34,skolem0014(X34,X35,X36,X37,X38,X39,X40,X41),X35)&(((((skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X41&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X40)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X39)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X38)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X37)&skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X36))))))))))))))|six(X34,X35))))),inference(skolemize,[status(esa)],[c77])).])).
% 2.26/2.49 fof(c80,plain,(![X25]:(![X26]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:(((~six(X25,X26)|member(X25,skolem0008(X25,X26),X26))&(((~six(X25,X26)|member(X25,skolem0009(X25,X26),X26))&(~six(X25,X26)|skolem0009(X25,X26)!=skolem0008(X25,X26)))&((((~six(X25,X26)|member(X25,skolem0010(X25,X26),X26))&(~six(X25,X26)|skolem0010(X25,X26)!=skolem0009(X25,X26)))&(~six(X25,X26)|skolem0010(X25,X26)!=skolem0008(X25,X26)))&(((((~six(X25,X26)|member(X25,skolem0011(X25,X26),X26))&(~six(X25,X26)|skolem0011(X25,X26)!=skolem0010(X25,X26)))&(~six(X25,X26)|skolem0011(X25,X26)!=skolem0009(X25,X26)))&(~six(X25,X26)|skolem0011(X25,X26)!=skolem0008(X25,X26)))&((((((~six(X25,X26)|member(X25,skolem0012(X25,X26),X26))&(~six(X25,X26)|skolem0012(X25,X26)!=skolem0011(X25,X26)))&(~six(X25,X26)|skolem0012(X25,X26)!=skolem0010(X25,X26)))&(~six(X25,X26)|skolem0012(X25,X26)!=skolem0009(X25,X26)))&(~six(X25,X26)|skolem0012(X25,X26)!=skolem0008(X25,X26)))&(((((((~six(X25,X26)|member(X25,skolem0013(X25,X26),X26))&(~six(X25,X26)|skolem0013(X25,X26)!=skolem0012(X25,X26)))&(~six(X25,X26)|skolem0013(X25,X26)!=skolem0011(X25,X26)))&(~six(X25,X26)|skolem0013(X25,X26)!=skolem0010(X25,X26)))&(~six(X25,X26)|skolem0013(X25,X26)!=skolem0009(X25,X26)))&(~six(X25,X26)|skolem0013(X25,X26)!=skolem0008(X25,X26)))&(~six(X25,X26)|(~member(X25,X33,X26)|(((((X33=skolem0013(X25,X26)|X33=skolem0012(X25,X26))|X33=skolem0011(X25,X26))|X33=skolem0010(X25,X26))|X33=skolem0009(X25,X26))|X33=skolem0008(X25,X26))))))))))&(((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|member(X34,skolem0014(X34,X35,X36,X37,X38,X39,X40,X41),X35)))))))|six(X34,X35))&(((((((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X41))))))|six(X34,X35))&((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X40))))))|six(X34,X35)))&((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X39))))))|six(X34,X35)))&((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X38))))))|six(X34,X35)))&((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X37))))))|six(X34,X35)))&((~member(X34,X36,X35)|((~member(X34,X37,X35)|X37=X36)|(((~member(X34,X38,X35)|X38=X37)|X38=X36)|((((~member(X34,X39,X35)|X39=X38)|X39=X37)|X39=X36)|(((((~member(X34,X40,X35)|X40=X39)|X40=X38)|X40=X37)|X40=X36)|((((((~member(X34,X41,X35)|X41=X40)|X41=X39)|X41=X38)|X41=X37)|X41=X36)|skolem0014(X34,X35,X36,X37,X38,X39,X40,X41)!=X36))))))|six(X34,X35)))))))))))))))),inference(distribute,[status(thm)],[c79])).
% 2.26/2.49 cnf(c91,plain,~six(X304,X303)|member(X304,skolem0012(X304,X303),X303),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.49 cnf(c305,plain,member(skolem0001,skolem0012(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c91, c62])).
% 2.26/2.49 cnf(c56,negated_conjecture,~member(skolem0001,X428,skolem0004)|agent(skolem0001,skolem0005(X428),skolem0002),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.49 cnf(c565,plain,agent(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c56, c305])).
% 2.26/2.49 cnf(c57,negated_conjecture,~member(skolem0001,X430,skolem0004)|patient(skolem0001,skolem0005(X430),X430),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.49 cnf(c584,plain,patient(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c57, c305])).
% 2.26/2.49 cnf(c65,negated_conjecture,~actual_world(X437)|~male(X437,X434)|~male(X437,X436)|~man(X437,X436)|~of(X437,X435,X436)|~cannon(X437,X435)|member(X437,skolem0006(X437,X436,X435,X434,X440,X439,X438),X434)|~six(X437,X434)|~group(X437,X434)|member(X437,skolem0007(X437,X436,X435,X434,X440,X439,X438),X434)|~cry(X437,X440)|~revenge(X437,X439)|~event(X437,X438)|~agent(X437,X438,X434)|~patient(X437,X438,X440)|~present(X437,X438)|~nonreflexive(X437,X438)|~scream(X437,X438)|~of(X437,X438,X439),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.49 cnf(c600,plain,~actual_world(X1035)|~male(X1035,X1036)|~male(X1035,X1037)|~man(X1035,X1037)|~of(X1035,X1038,X1037)|~cannon(X1035,X1038)|member(X1035,skolem0006(X1035,X1037,X1038,X1036,X1039,X1037,X1038),X1036)|~six(X1035,X1036)|~group(X1035,X1036)|member(X1035,skolem0007(X1035,X1037,X1038,X1036,X1039,X1037,X1038),X1036)|~cry(X1035,X1039)|~revenge(X1035,X1037)|~event(X1035,X1038)|~agent(X1035,X1038,X1036)|~patient(X1035,X1038,X1039)|~present(X1035,X1038)|~nonreflexive(X1035,X1038)|~scream(X1035,X1038),inference(factor,[status(thm)],[c65])).
% 2.26/2.49 cnf(c961,plain,~actual_world(skolem0001)|~male(skolem0001,X1254)|~male(skolem0001,X1253)|~man(skolem0001,X1253)|~of(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)),X1253)|~cannon(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1253,skolem0005(skolem0012(skolem0001,skolem0004)),X1254,skolem0012(skolem0001,skolem0004),X1253,skolem0005(skolem0012(skolem0001,skolem0004))),X1254)|~six(skolem0001,X1254)|~group(skolem0001,X1254)|member(skolem0001,skolem0007(skolem0001,X1253,skolem0005(skolem0012(skolem0001,skolem0004)),X1254,skolem0012(skolem0001,skolem0004),X1253,skolem0005(skolem0012(skolem0001,skolem0004))),X1254)|~cry(skolem0001,skolem0012(skolem0001,skolem0004))|~revenge(skolem0001,X1253)|~event(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)),X1254)|~present(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c600, c584])).
% 2.26/2.49 cnf(c1043,plain,~actual_world(skolem0001)|~male(skolem0001,skolem0002)|~male(skolem0001,X1255)|~man(skolem0001,X1255)|~of(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)),X1255)|~cannon(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1255,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0002,skolem0012(skolem0001,skolem0004),X1255,skolem0005(skolem0012(skolem0001,skolem0004))),skolem0002)|~six(skolem0001,skolem0002)|~group(skolem0001,skolem0002)|member(skolem0001,skolem0007(skolem0001,X1255,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0002,skolem0012(skolem0001,skolem0004),X1255,skolem0005(skolem0012(skolem0001,skolem0004))),skolem0002)|~cry(skolem0001,skolem0012(skolem0001,skolem0004))|~revenge(skolem0001,X1255)|~event(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|~present(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c961, c565])).
% 2.26/2.49 cnf(c96,plain,~six(X310,X309)|member(X310,skolem0013(X310,X309),X309),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.49 cnf(c307,plain,member(skolem0001,skolem0013(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c96, c62])).
% 2.26/2.49 cnf(c567,plain,agent(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c56, c307])).
% 2.26/2.49 cnf(c586,plain,patient(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c57, c307])).
% 2.26/2.49 cnf(c960,plain,~actual_world(skolem0001)|~male(skolem0001,X1250)|~male(skolem0001,X1249)|~man(skolem0001,X1249)|~of(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)),X1249)|~cannon(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1249,skolem0005(skolem0013(skolem0001,skolem0004)),X1250,skolem0013(skolem0001,skolem0004),X1249,skolem0005(skolem0013(skolem0001,skolem0004))),X1250)|~six(skolem0001,X1250)|~group(skolem0001,X1250)|member(skolem0001,skolem0007(skolem0001,X1249,skolem0005(skolem0013(skolem0001,skolem0004)),X1250,skolem0013(skolem0001,skolem0004),X1249,skolem0005(skolem0013(skolem0001,skolem0004))),X1250)|~cry(skolem0001,skolem0013(skolem0001,skolem0004))|~revenge(skolem0001,X1249)|~event(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)),X1250)|~present(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c600, c586])).
% 2.26/2.49 cnf(c1042,plain,~actual_world(skolem0001)|~male(skolem0001,skolem0002)|~male(skolem0001,X1252)|~man(skolem0001,X1252)|~of(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)),X1252)|~cannon(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1252,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0002,skolem0013(skolem0001,skolem0004),X1252,skolem0005(skolem0013(skolem0001,skolem0004))),skolem0002)|~six(skolem0001,skolem0002)|~group(skolem0001,skolem0002)|member(skolem0001,skolem0007(skolem0001,X1252,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0002,skolem0013(skolem0001,skolem0004),X1252,skolem0005(skolem0013(skolem0001,skolem0004))),skolem0002)|~cry(skolem0001,skolem0013(skolem0001,skolem0004))|~revenge(skolem0001,X1252)|~event(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|~present(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c960, c567])).
% 2.26/2.49 cnf(c81,plain,~six(X296,X295)|member(X296,skolem0008(X296,X295),X295),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.49 cnf(c301,plain,member(skolem0001,skolem0008(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c81, c62])).
% 2.26/2.49 cnf(c566,plain,agent(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c56, c301])).
% 2.26/2.49 cnf(c585,plain,patient(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c57, c301])).
% 2.26/2.49 cnf(c959,plain,~actual_world(skolem0001)|~male(skolem0001,X1248)|~male(skolem0001,X1247)|~man(skolem0001,X1247)|~of(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)),X1247)|~cannon(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1247,skolem0005(skolem0008(skolem0001,skolem0004)),X1248,skolem0008(skolem0001,skolem0004),X1247,skolem0005(skolem0008(skolem0001,skolem0004))),X1248)|~six(skolem0001,X1248)|~group(skolem0001,X1248)|member(skolem0001,skolem0007(skolem0001,X1247,skolem0005(skolem0008(skolem0001,skolem0004)),X1248,skolem0008(skolem0001,skolem0004),X1247,skolem0005(skolem0008(skolem0001,skolem0004))),X1248)|~cry(skolem0001,skolem0008(skolem0001,skolem0004))|~revenge(skolem0001,X1247)|~event(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)),X1248)|~present(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c600, c585])).
% 2.26/2.50 cnf(c1041,plain,~actual_world(skolem0001)|~male(skolem0001,skolem0002)|~male(skolem0001,X1251)|~man(skolem0001,X1251)|~of(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)),X1251)|~cannon(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1251,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0002,skolem0008(skolem0001,skolem0004),X1251,skolem0005(skolem0008(skolem0001,skolem0004))),skolem0002)|~six(skolem0001,skolem0002)|~group(skolem0001,skolem0002)|member(skolem0001,skolem0007(skolem0001,X1251,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0002,skolem0008(skolem0001,skolem0004),X1251,skolem0005(skolem0008(skolem0001,skolem0004))),skolem0002)|~cry(skolem0001,skolem0008(skolem0001,skolem0004))|~revenge(skolem0001,X1251)|~event(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|~present(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c959, c566])).
% 2.26/2.50 cnf(c82,plain,~six(X298,X297)|member(X298,skolem0009(X298,X297),X297),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.50 cnf(c302,plain,member(skolem0001,skolem0009(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c82, c62])).
% 2.26/2.50 cnf(c563,plain,agent(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c56, c302])).
% 2.26/2.50 cnf(c582,plain,patient(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c57, c302])).
% 2.26/2.50 cnf(c958,plain,~actual_world(skolem0001)|~male(skolem0001,X1245)|~male(skolem0001,X1244)|~man(skolem0001,X1244)|~of(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)),X1244)|~cannon(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1244,skolem0005(skolem0009(skolem0001,skolem0004)),X1245,skolem0009(skolem0001,skolem0004),X1244,skolem0005(skolem0009(skolem0001,skolem0004))),X1245)|~six(skolem0001,X1245)|~group(skolem0001,X1245)|member(skolem0001,skolem0007(skolem0001,X1244,skolem0005(skolem0009(skolem0001,skolem0004)),X1245,skolem0009(skolem0001,skolem0004),X1244,skolem0005(skolem0009(skolem0001,skolem0004))),X1245)|~cry(skolem0001,skolem0009(skolem0001,skolem0004))|~revenge(skolem0001,X1244)|~event(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)),X1245)|~present(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c600, c582])).
% 2.26/2.50 cnf(c1040,plain,~actual_world(skolem0001)|~male(skolem0001,skolem0002)|~male(skolem0001,X1246)|~man(skolem0001,X1246)|~of(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)),X1246)|~cannon(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1246,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0002,skolem0009(skolem0001,skolem0004),X1246,skolem0005(skolem0009(skolem0001,skolem0004))),skolem0002)|~six(skolem0001,skolem0002)|~group(skolem0001,skolem0002)|member(skolem0001,skolem0007(skolem0001,X1246,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0002,skolem0009(skolem0001,skolem0004),X1246,skolem0005(skolem0009(skolem0001,skolem0004))),skolem0002)|~cry(skolem0001,skolem0009(skolem0001,skolem0004))|~revenge(skolem0001,X1246)|~event(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|~present(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c958, c563])).
% 2.26/2.50 cnf(c84,plain,~six(X300,X299)|member(X300,skolem0010(X300,X299),X299),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.50 cnf(c303,plain,member(skolem0001,skolem0010(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c84, c62])).
% 2.26/2.50 cnf(c564,plain,agent(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c56, c303])).
% 2.26/2.50 cnf(c583,plain,patient(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c57, c303])).
% 2.26/2.50 cnf(c957,plain,~actual_world(skolem0001)|~male(skolem0001,X1241)|~male(skolem0001,X1240)|~man(skolem0001,X1240)|~of(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)),X1240)|~cannon(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1240,skolem0005(skolem0010(skolem0001,skolem0004)),X1241,skolem0010(skolem0001,skolem0004),X1240,skolem0005(skolem0010(skolem0001,skolem0004))),X1241)|~six(skolem0001,X1241)|~group(skolem0001,X1241)|member(skolem0001,skolem0007(skolem0001,X1240,skolem0005(skolem0010(skolem0001,skolem0004)),X1241,skolem0010(skolem0001,skolem0004),X1240,skolem0005(skolem0010(skolem0001,skolem0004))),X1241)|~cry(skolem0001,skolem0010(skolem0001,skolem0004))|~revenge(skolem0001,X1240)|~event(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)),X1241)|~present(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c600, c583])).
% 2.26/2.50 cnf(c1039,plain,~actual_world(skolem0001)|~male(skolem0001,skolem0002)|~male(skolem0001,X1243)|~man(skolem0001,X1243)|~of(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)),X1243)|~cannon(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1243,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0002,skolem0010(skolem0001,skolem0004),X1243,skolem0005(skolem0010(skolem0001,skolem0004))),skolem0002)|~six(skolem0001,skolem0002)|~group(skolem0001,skolem0002)|member(skolem0001,skolem0007(skolem0001,X1243,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0002,skolem0010(skolem0001,skolem0004),X1243,skolem0005(skolem0010(skolem0001,skolem0004))),skolem0002)|~cry(skolem0001,skolem0010(skolem0001,skolem0004))|~revenge(skolem0001,X1243)|~event(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|~present(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c957, c564])).
% 2.26/2.50 cnf(c87,plain,~six(X302,X301)|member(X302,skolem0011(X302,X301),X301),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.50 cnf(c304,plain,member(skolem0001,skolem0011(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c87, c62])).
% 2.26/2.50 cnf(c568,plain,agent(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c56, c304])).
% 2.26/2.50 cnf(c587,plain,patient(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c57, c304])).
% 2.26/2.50 cnf(c956,plain,~actual_world(skolem0001)|~male(skolem0001,X1239)|~male(skolem0001,X1238)|~man(skolem0001,X1238)|~of(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)),X1238)|~cannon(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1238,skolem0005(skolem0011(skolem0001,skolem0004)),X1239,skolem0011(skolem0001,skolem0004),X1238,skolem0005(skolem0011(skolem0001,skolem0004))),X1239)|~six(skolem0001,X1239)|~group(skolem0001,X1239)|member(skolem0001,skolem0007(skolem0001,X1238,skolem0005(skolem0011(skolem0001,skolem0004)),X1239,skolem0011(skolem0001,skolem0004),X1238,skolem0005(skolem0011(skolem0001,skolem0004))),X1239)|~cry(skolem0001,skolem0011(skolem0001,skolem0004))|~revenge(skolem0001,X1238)|~event(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)),X1239)|~present(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c600, c587])).
% 2.26/2.50 cnf(c1038,plain,~actual_world(skolem0001)|~male(skolem0001,skolem0002)|~male(skolem0001,X1242)|~man(skolem0001,X1242)|~of(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)),X1242)|~cannon(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|member(skolem0001,skolem0006(skolem0001,X1242,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0002,skolem0011(skolem0001,skolem0004),X1242,skolem0005(skolem0011(skolem0001,skolem0004))),skolem0002)|~six(skolem0001,skolem0002)|~group(skolem0001,skolem0002)|member(skolem0001,skolem0007(skolem0001,X1242,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0002,skolem0011(skolem0001,skolem0004),X1242,skolem0005(skolem0011(skolem0001,skolem0004))),skolem0002)|~cry(skolem0001,skolem0011(skolem0001,skolem0004))|~revenge(skolem0001,X1242)|~event(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|~present(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|~nonreflexive(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|~scream(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c956, c568])).
% 2.26/2.50 cnf(c59,negated_conjecture,~member(skolem0001,X423,skolem0004)|nonreflexive(skolem0001,skolem0005(X423)),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.50 cnf(c551,plain,nonreflexive(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c59, c304])).
% 2.26/2.50 fof(ax46,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', ax46)).
% 2.26/2.50 fof(c69,plain,(![U]:(![V]:(![W]:(![X]:(((~nonreflexive(U,V)|~agent(U,V,W))|~patient(U,V,X))|W!=X))))),inference(fof_nnf,[status(thm)],[ax46])).
% 2.26/2.50 fof(c70,plain,(![X19]:(![X20]:(![X21]:(![X22]:(((~nonreflexive(X19,X20)|~agent(X19,X20,X21))|~patient(X19,X20,X22))|X21!=X22))))),inference(variable_rename,[status(thm)],[c69])).
% 2.26/2.50 cnf(c71,plain,~nonreflexive(X501,X498)|~agent(X501,X498,X499)|~patient(X501,X498,X500)|X499!=X500,inference(split_conjunct,[status(thm)],[c70])).
% 2.26/2.50 cnf(c860,plain,~nonreflexive(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)),X1237)|X1237!=skolem0011(skolem0001,skolem0004),inference(resolution,[status(thm)],[c587, c71])).
% 2.26/2.50 cnf(c1035,plain,~nonreflexive(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)))|skolem0002!=skolem0011(skolem0001,skolem0004),inference(resolution,[status(thm)],[c860, c568])).
% 2.26/2.50 cnf(c1037,plain,skolem0002!=skolem0011(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1035, c551])).
% 2.26/2.50 cnf(c550,plain,nonreflexive(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c59, c307])).
% 2.26/2.50 cnf(c858,plain,~nonreflexive(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)),X1236)|X1236!=skolem0013(skolem0001,skolem0004),inference(resolution,[status(thm)],[c586, c71])).
% 2.26/2.50 cnf(c1034,plain,~nonreflexive(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)))|skolem0002!=skolem0013(skolem0001,skolem0004),inference(resolution,[status(thm)],[c858, c567])).
% 2.26/2.50 cnf(c1036,plain,skolem0002!=skolem0013(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1034, c550])).
% 2.26/2.50 cnf(c549,plain,nonreflexive(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c59, c301])).
% 2.26/2.50 cnf(c856,plain,~nonreflexive(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)),X1235)|X1235!=skolem0008(skolem0001,skolem0004),inference(resolution,[status(thm)],[c585, c71])).
% 2.26/2.50 cnf(c1031,plain,~nonreflexive(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)))|skolem0002!=skolem0008(skolem0001,skolem0004),inference(resolution,[status(thm)],[c856, c566])).
% 2.26/2.50 cnf(c1033,plain,skolem0002!=skolem0008(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1031, c549])).
% 2.26/2.50 cnf(c548,plain,nonreflexive(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c59, c305])).
% 2.26/2.50 cnf(c852,plain,~nonreflexive(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)),X1234)|X1234!=skolem0012(skolem0001,skolem0004),inference(resolution,[status(thm)],[c584, c71])).
% 2.26/2.50 cnf(c1030,plain,~nonreflexive(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)))|skolem0002!=skolem0012(skolem0001,skolem0004),inference(resolution,[status(thm)],[c852, c565])).
% 2.26/2.50 cnf(c1032,plain,skolem0002!=skolem0012(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1030, c548])).
% 2.26/2.50 cnf(c547,plain,nonreflexive(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c59, c303])).
% 2.26/2.50 cnf(c850,plain,~nonreflexive(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)),X1233)|X1233!=skolem0010(skolem0001,skolem0004),inference(resolution,[status(thm)],[c583, c71])).
% 2.26/2.50 cnf(c1028,plain,~nonreflexive(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)))|skolem0002!=skolem0010(skolem0001,skolem0004),inference(resolution,[status(thm)],[c850, c564])).
% 2.26/2.50 cnf(c1029,plain,skolem0002!=skolem0010(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1028, c547])).
% 2.26/2.50 cnf(c546,plain,nonreflexive(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c59, c302])).
% 2.26/2.50 cnf(c848,plain,~nonreflexive(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|~agent(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)),X1227)|X1227!=skolem0009(skolem0001,skolem0004),inference(resolution,[status(thm)],[c582, c71])).
% 2.26/2.50 cnf(c1026,plain,~nonreflexive(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)))|skolem0002!=skolem0009(skolem0001,skolem0004),inference(resolution,[status(thm)],[c848, c563])).
% 2.26/2.50 cnf(c1027,plain,skolem0002!=skolem0009(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1026, c546])).
% 2.26/2.50 cnf(reflexivity,axiom,X129=X129,theory(equality)).
% 2.26/2.50 cnf(c37,axiom,X399!=X396|X397!=X394|X395!=X398|~patient(X399,X397,X395)|patient(X396,X394,X398),theory(equality)).
% 2.26/2.50 cnf(c859,plain,skolem0001!=X1217|skolem0005(skolem0011(skolem0001,skolem0004))!=X1216|skolem0011(skolem0001,skolem0004)!=X1218|patient(X1217,X1216,X1218),inference(resolution,[status(thm)],[c587, c37])).
% 2.26/2.50 cnf(c1023,plain,skolem0001!=X1225|skolem0011(skolem0001,skolem0004)!=X1224|patient(X1225,skolem0005(skolem0011(skolem0001,skolem0004)),X1224),inference(resolution,[status(thm)],[c859, reflexivity])).
% 2.26/2.50 cnf(c1024,plain,skolem0001!=X1226|patient(X1226,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c1023, reflexivity])).
% 2.26/2.50 cnf(c857,plain,skolem0001!=X1211|skolem0005(skolem0013(skolem0001,skolem0004))!=X1210|skolem0013(skolem0001,skolem0004)!=X1212|patient(X1211,X1210,X1212),inference(resolution,[status(thm)],[c586, c37])).
% 2.26/2.50 cnf(c1020,plain,skolem0001!=X1214|skolem0013(skolem0001,skolem0004)!=X1213|patient(X1214,skolem0005(skolem0013(skolem0001,skolem0004)),X1213),inference(resolution,[status(thm)],[c857, reflexivity])).
% 2.26/2.50 cnf(c1021,plain,skolem0001!=X1215|patient(X1215,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c1020, reflexivity])).
% 2.26/2.50 cnf(c855,plain,skolem0001!=X1200|skolem0005(skolem0008(skolem0001,skolem0004))!=X1199|skolem0008(skolem0001,skolem0004)!=X1201|patient(X1200,X1199,X1201),inference(resolution,[status(thm)],[c585, c37])).
% 2.26/2.50 cnf(c1017,plain,skolem0001!=X1202|skolem0008(skolem0001,skolem0004)!=X1203|patient(X1202,skolem0005(skolem0008(skolem0001,skolem0004)),X1203),inference(resolution,[status(thm)],[c855, reflexivity])).
% 2.26/2.50 cnf(c1018,plain,skolem0001!=X1204|patient(X1204,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c1017, reflexivity])).
% 2.26/2.50 cnf(c851,plain,skolem0001!=X1189|skolem0005(skolem0012(skolem0001,skolem0004))!=X1188|skolem0012(skolem0001,skolem0004)!=X1190|patient(X1189,X1188,X1190),inference(resolution,[status(thm)],[c584, c37])).
% 2.26/2.50 cnf(c1014,plain,skolem0001!=X1192|skolem0012(skolem0001,skolem0004)!=X1191|patient(X1192,skolem0005(skolem0012(skolem0001,skolem0004)),X1191),inference(resolution,[status(thm)],[c851, reflexivity])).
% 2.26/2.50 cnf(c1015,plain,skolem0001!=X1193|patient(X1193,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c1014, reflexivity])).
% 2.26/2.50 cnf(c849,plain,skolem0001!=X1178|skolem0005(skolem0010(skolem0001,skolem0004))!=X1177|skolem0010(skolem0001,skolem0004)!=X1179|patient(X1178,X1177,X1179),inference(resolution,[status(thm)],[c583, c37])).
% 2.26/2.50 cnf(c1011,plain,skolem0001!=X1181|skolem0010(skolem0001,skolem0004)!=X1180|patient(X1181,skolem0005(skolem0010(skolem0001,skolem0004)),X1180),inference(resolution,[status(thm)],[c849, reflexivity])).
% 2.26/2.50 cnf(c1012,plain,skolem0001!=X1187|patient(X1187,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c1011, reflexivity])).
% 2.26/2.50 cnf(c847,plain,skolem0001!=X1167|skolem0005(skolem0009(skolem0001,skolem0004))!=X1166|skolem0009(skolem0001,skolem0004)!=X1168|patient(X1167,X1166,X1168),inference(resolution,[status(thm)],[c582, c37])).
% 2.26/2.50 cnf(c1008,plain,skolem0001!=X1174|skolem0009(skolem0001,skolem0004)!=X1175|patient(X1174,skolem0005(skolem0009(skolem0001,skolem0004)),X1175),inference(resolution,[status(thm)],[c847, reflexivity])).
% 2.26/2.50 cnf(c1009,plain,skolem0001!=X1176|patient(X1176,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c1008, reflexivity])).
% 2.26/2.50 cnf(c42,axiom,X422!=X419|X420!=X417|X418!=X421|~from_loc(X422,X420,X418)|from_loc(X419,X417,X421),theory(equality)).
% 2.26/2.50 cnf(c61,negated_conjecture,~member(skolem0001,X431,skolem0004)|from_loc(skolem0001,skolem0005(X431),skolem0003),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.50 cnf(c599,plain,from_loc(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c61, c304])).
% 2.26/2.50 cnf(c700,plain,skolem0001!=X1160|skolem0005(skolem0011(skolem0001,skolem0004))!=X1161|skolem0003!=X1162|from_loc(X1160,X1161,X1162),inference(resolution,[status(thm)],[c599, c42])).
% 2.26/2.50 cnf(c1005,plain,skolem0001!=X1163|skolem0003!=X1164|from_loc(X1163,skolem0005(skolem0011(skolem0001,skolem0004)),X1164),inference(resolution,[status(thm)],[c700, reflexivity])).
% 2.26/2.50 cnf(c1006,plain,skolem0001!=X1165|from_loc(X1165,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c1005, reflexivity])).
% 2.26/2.50 cnf(c598,plain,from_loc(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c61, c307])).
% 2.26/2.50 cnf(c698,plain,skolem0001!=X1147|skolem0005(skolem0013(skolem0001,skolem0004))!=X1148|skolem0003!=X1149|from_loc(X1147,X1148,X1149),inference(resolution,[status(thm)],[c598, c42])).
% 2.26/2.50 cnf(c1002,plain,skolem0001!=X1151|skolem0003!=X1150|from_loc(X1151,skolem0005(skolem0013(skolem0001,skolem0004)),X1150),inference(resolution,[status(thm)],[c698, reflexivity])).
% 2.26/2.50 cnf(c1003,plain,skolem0001!=X1152|from_loc(X1152,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c1002, reflexivity])).
% 2.26/2.50 cnf(c597,plain,from_loc(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c61, c301])).
% 2.26/2.50 cnf(c697,plain,skolem0001!=X1134|skolem0005(skolem0008(skolem0001,skolem0004))!=X1135|skolem0003!=X1136|from_loc(X1134,X1135,X1136),inference(resolution,[status(thm)],[c597, c42])).
% 2.26/2.50 cnf(c999,plain,skolem0001!=X1138|skolem0003!=X1137|from_loc(X1138,skolem0005(skolem0008(skolem0001,skolem0004)),X1137),inference(resolution,[status(thm)],[c697, reflexivity])).
% 2.26/2.50 cnf(c1000,plain,skolem0001!=X1139|from_loc(X1139,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c999, reflexivity])).
% 2.26/2.50 cnf(c596,plain,from_loc(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c61, c305])).
% 2.26/2.50 cnf(c696,plain,skolem0001!=X1121|skolem0005(skolem0012(skolem0001,skolem0004))!=X1122|skolem0003!=X1123|from_loc(X1121,X1122,X1123),inference(resolution,[status(thm)],[c596, c42])).
% 2.26/2.50 cnf(c996,plain,skolem0001!=X1124|skolem0003!=X1125|from_loc(X1124,skolem0005(skolem0012(skolem0001,skolem0004)),X1125),inference(resolution,[status(thm)],[c696, reflexivity])).
% 2.26/2.50 cnf(c997,plain,skolem0001!=X1133|from_loc(X1133,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c996, reflexivity])).
% 2.26/2.50 cnf(c595,plain,from_loc(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c61, c303])).
% 2.26/2.50 cnf(c695,plain,skolem0001!=X1108|skolem0005(skolem0010(skolem0001,skolem0004))!=X1109|skolem0003!=X1110|from_loc(X1108,X1109,X1110),inference(resolution,[status(thm)],[c595, c42])).
% 2.26/2.50 cnf(c993,plain,skolem0001!=X1119|skolem0003!=X1118|from_loc(X1119,skolem0005(skolem0010(skolem0001,skolem0004)),X1118),inference(resolution,[status(thm)],[c695, reflexivity])).
% 2.26/2.50 cnf(c994,plain,skolem0001!=X1120|from_loc(X1120,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c993, reflexivity])).
% 2.26/2.50 cnf(c594,plain,from_loc(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c61, c302])).
% 2.26/2.50 cnf(c694,plain,skolem0001!=X1102|skolem0005(skolem0009(skolem0001,skolem0004))!=X1103|skolem0003!=X1104|from_loc(X1102,X1103,X1104),inference(resolution,[status(thm)],[c594, c42])).
% 2.26/2.50 cnf(c990,plain,skolem0001!=X1106|skolem0003!=X1105|from_loc(X1106,skolem0005(skolem0009(skolem0001,skolem0004)),X1105),inference(resolution,[status(thm)],[c694, reflexivity])).
% 2.26/2.50 cnf(c991,plain,skolem0001!=X1107|from_loc(X1107,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0003),inference(resolution,[status(thm)],[c990, reflexivity])).
% 2.26/2.50 cnf(c39,axiom,X409!=X406|X407!=X404|X405!=X408|~agent(X409,X407,X405)|agent(X406,X404,X408),theory(equality)).
% 2.26/2.50 cnf(c692,plain,skolem0001!=X1091|skolem0005(skolem0011(skolem0001,skolem0004))!=X1089|skolem0002!=X1090|agent(X1091,X1089,X1090),inference(resolution,[status(thm)],[c568, c39])).
% 2.26/2.50 cnf(c987,plain,skolem0001!=X1093|skolem0002!=X1092|agent(X1093,skolem0005(skolem0011(skolem0001,skolem0004)),X1092),inference(resolution,[status(thm)],[c692, reflexivity])).
% 2.26/2.50 cnf(c988,plain,skolem0001!=X1094|agent(X1094,skolem0005(skolem0011(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c987, reflexivity])).
% 2.26/2.50 cnf(c691,plain,skolem0001!=X1085|skolem0005(skolem0013(skolem0001,skolem0004))!=X1083|skolem0002!=X1084|agent(X1085,X1083,X1084),inference(resolution,[status(thm)],[c567, c39])).
% 2.26/2.50 cnf(c984,plain,skolem0001!=X1087|skolem0002!=X1086|agent(X1087,skolem0005(skolem0013(skolem0001,skolem0004)),X1086),inference(resolution,[status(thm)],[c691, reflexivity])).
% 2.26/2.50 cnf(c985,plain,skolem0001!=X1088|agent(X1088,skolem0005(skolem0013(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c984, reflexivity])).
% 2.26/2.50 cnf(c690,plain,skolem0001!=X1079|skolem0005(skolem0008(skolem0001,skolem0004))!=X1077|skolem0002!=X1078|agent(X1079,X1077,X1078),inference(resolution,[status(thm)],[c566, c39])).
% 2.26/2.50 cnf(c981,plain,skolem0001!=X1081|skolem0002!=X1080|agent(X1081,skolem0005(skolem0008(skolem0001,skolem0004)),X1080),inference(resolution,[status(thm)],[c690, reflexivity])).
% 2.26/2.50 cnf(c982,plain,skolem0001!=X1082|agent(X1082,skolem0005(skolem0008(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c981, reflexivity])).
% 2.26/2.50 cnf(c689,plain,skolem0001!=X1073|skolem0005(skolem0012(skolem0001,skolem0004))!=X1071|skolem0002!=X1072|agent(X1073,X1071,X1072),inference(resolution,[status(thm)],[c565, c39])).
% 2.26/2.50 cnf(c978,plain,skolem0001!=X1075|skolem0002!=X1074|agent(X1075,skolem0005(skolem0012(skolem0001,skolem0004)),X1074),inference(resolution,[status(thm)],[c689, reflexivity])).
% 2.26/2.50 cnf(c979,plain,skolem0001!=X1076|agent(X1076,skolem0005(skolem0012(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c978, reflexivity])).
% 2.26/2.50 cnf(c688,plain,skolem0001!=X1067|skolem0005(skolem0010(skolem0001,skolem0004))!=X1065|skolem0002!=X1066|agent(X1067,X1065,X1066),inference(resolution,[status(thm)],[c564, c39])).
% 2.26/2.50 cnf(c975,plain,skolem0001!=X1068|skolem0002!=X1069|agent(X1068,skolem0005(skolem0010(skolem0001,skolem0004)),X1069),inference(resolution,[status(thm)],[c688, reflexivity])).
% 2.26/2.50 cnf(c976,plain,skolem0001!=X1070|agent(X1070,skolem0005(skolem0010(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c975, reflexivity])).
% 2.26/2.50 cnf(c686,plain,skolem0001!=X1061|skolem0005(skolem0009(skolem0001,skolem0004))!=X1059|skolem0002!=X1060|agent(X1061,X1059,X1060),inference(resolution,[status(thm)],[c563, c39])).
% 2.26/2.50 cnf(c972,plain,skolem0001!=X1062|skolem0002!=X1063|agent(X1062,skolem0005(skolem0009(skolem0001,skolem0004)),X1063),inference(resolution,[status(thm)],[c686, reflexivity])).
% 2.26/2.50 cnf(c973,plain,skolem0001!=X1064|agent(X1064,skolem0005(skolem0009(skolem0001,skolem0004)),skolem0002),inference(resolution,[status(thm)],[c972, reflexivity])).
% 2.26/2.50 cnf(c36,axiom,X393!=X390|X391!=X388|X389!=X392|~member(X393,X391,X389)|member(X390,X388,X392),theory(equality)).
% 2.26/2.50 cnf(c518,plain,skolem0001!=X947|skolem0011(skolem0001,skolem0004)!=X949|skolem0004!=X948|member(X947,X949,X948),inference(resolution,[status(thm)],[c36, c304])).
% 2.26/2.50 cnf(c899,plain,skolem0001!=X1056|skolem0004!=X1057|member(X1056,skolem0011(skolem0001,skolem0004),X1057),inference(resolution,[status(thm)],[c518, reflexivity])).
% 2.26/2.50 cnf(c970,plain,skolem0001!=X1058|member(X1058,skolem0011(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c899, reflexivity])).
% 2.26/2.50 cnf(c517,plain,skolem0001!=X939|skolem0013(skolem0001,skolem0004)!=X941|skolem0004!=X940|member(X939,X941,X940),inference(resolution,[status(thm)],[c36, c307])).
% 2.26/2.50 cnf(c895,plain,skolem0001!=X1054|skolem0004!=X1053|member(X1054,skolem0013(skolem0001,skolem0004),X1053),inference(resolution,[status(thm)],[c517, reflexivity])).
% 2.26/2.50 cnf(c968,plain,skolem0001!=X1055|member(X1055,skolem0013(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c895, reflexivity])).
% 2.26/2.50 cnf(c516,plain,skolem0001!=X930|skolem0008(skolem0001,skolem0004)!=X932|skolem0004!=X931|member(X930,X932,X931),inference(resolution,[status(thm)],[c36, c301])).
% 2.26/2.50 cnf(c890,plain,skolem0001!=X1050|skolem0004!=X1051|member(X1050,skolem0008(skolem0001,skolem0004),X1051),inference(resolution,[status(thm)],[c516, reflexivity])).
% 2.26/2.50 cnf(c966,plain,skolem0001!=X1052|member(X1052,skolem0008(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c890, reflexivity])).
% 2.26/2.50 cnf(c515,plain,skolem0001!=X923|skolem0012(skolem0001,skolem0004)!=X925|skolem0004!=X924|member(X923,X925,X924),inference(resolution,[status(thm)],[c36, c305])).
% 2.26/2.50 cnf(c886,plain,skolem0001!=X1044|skolem0004!=X1043|member(X1044,skolem0012(skolem0001,skolem0004),X1043),inference(resolution,[status(thm)],[c515, reflexivity])).
% 2.26/2.50 cnf(c964,plain,skolem0001!=X1049|member(X1049,skolem0012(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c886, reflexivity])).
% 2.26/2.50 cnf(c53,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.50 cnf(c601,plain,~actual_world(skolem0001)|~male(skolem0001,X1045)|~male(skolem0001,X1047)|~man(skolem0001,X1047)|~of(skolem0001,X1048,X1047)|~cannon(skolem0001,X1048)|member(skolem0001,skolem0006(skolem0001,X1047,X1048,X1045,X1046,skolem0002,skolem0003),X1045)|~six(skolem0001,X1045)|~group(skolem0001,X1045)|member(skolem0001,skolem0007(skolem0001,X1047,X1048,X1045,X1046,skolem0002,skolem0003),X1045)|~cry(skolem0001,X1046)|~revenge(skolem0001,skolem0002)|~event(skolem0001,skolem0003)|~agent(skolem0001,skolem0003,X1045)|~patient(skolem0001,skolem0003,X1046)|~present(skolem0001,skolem0003)|~nonreflexive(skolem0001,skolem0003)|~scream(skolem0001,skolem0003),inference(resolution,[status(thm)],[c65, c53])).
% 2.26/2.50 cnf(c514,plain,skolem0001!=X915|skolem0010(skolem0001,skolem0004)!=X917|skolem0004!=X916|member(X915,X917,X916),inference(resolution,[status(thm)],[c36, c303])).
% 2.26/2.50 cnf(c882,plain,skolem0001!=X1041|skolem0004!=X1040|member(X1041,skolem0010(skolem0001,skolem0004),X1040),inference(resolution,[status(thm)],[c514, reflexivity])).
% 2.26/2.50 cnf(c962,plain,skolem0001!=X1042|member(X1042,skolem0010(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c882, reflexivity])).
% 2.26/2.50 cnf(c513,plain,skolem0001!=X906|skolem0009(skolem0001,skolem0004)!=X908|skolem0004!=X907|member(X906,X908,X907),inference(resolution,[status(thm)],[c36, c302])).
% 2.26/2.50 cnf(c877,plain,skolem0001!=X1032|skolem0004!=X1033|member(X1032,skolem0009(skolem0001,skolem0004),X1033),inference(resolution,[status(thm)],[c513, reflexivity])).
% 2.26/2.50 cnf(c954,plain,skolem0001!=X1034|member(X1034,skolem0009(skolem0001,skolem0004),skolem0004),inference(resolution,[status(thm)],[c877, reflexivity])).
% 2.26/2.50 cnf(c20,axiom,X326!=X325|X324!=X323|~fire(X326,X324)|fire(X325,X323),theory(equality)).
% 2.26/2.50 cnf(c60,negated_conjecture,~member(skolem0001,X429,skolem0004)|fire(skolem0001,skolem0005(X429)),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.50 cnf(c575,plain,fire(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c60, c304])).
% 2.26/2.50 cnf(c592,plain,skolem0001!=X1029|skolem0005(skolem0011(skolem0001,skolem0004))!=X1030|fire(X1029,X1030),inference(resolution,[status(thm)],[c575, c20])).
% 2.26/2.50 cnf(c952,plain,skolem0001!=X1031|fire(X1031,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c592, reflexivity])).
% 2.26/2.50 cnf(c574,plain,fire(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c60, c307])).
% 2.26/2.50 cnf(c590,plain,skolem0001!=X1026|skolem0005(skolem0013(skolem0001,skolem0004))!=X1027|fire(X1026,X1027),inference(resolution,[status(thm)],[c574, c20])).
% 2.26/2.50 cnf(c950,plain,skolem0001!=X1028|fire(X1028,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c590, reflexivity])).
% 2.26/2.50 cnf(c573,plain,fire(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c60, c301])).
% 2.26/2.50 cnf(c588,plain,skolem0001!=X1023|skolem0005(skolem0008(skolem0001,skolem0004))!=X1024|fire(X1023,X1024),inference(resolution,[status(thm)],[c573, c20])).
% 2.26/2.50 cnf(c948,plain,skolem0001!=X1025|fire(X1025,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c588, reflexivity])).
% 2.26/2.50 cnf(c572,plain,fire(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c60, c305])).
% 2.26/2.50 cnf(c580,plain,skolem0001!=X1020|skolem0005(skolem0012(skolem0001,skolem0004))!=X1021|fire(X1020,X1021),inference(resolution,[status(thm)],[c572, c20])).
% 2.26/2.50 cnf(c946,plain,skolem0001!=X1022|fire(X1022,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c580, reflexivity])).
% 2.26/2.50 cnf(c571,plain,fire(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c60, c303])).
% 2.26/2.50 cnf(c578,plain,skolem0001!=X1017|skolem0005(skolem0010(skolem0001,skolem0004))!=X1018|fire(X1017,X1018),inference(resolution,[status(thm)],[c571, c20])).
% 2.26/2.50 cnf(c944,plain,skolem0001!=X1019|fire(X1019,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c578, reflexivity])).
% 2.26/2.50 cnf(c570,plain,fire(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c60, c302])).
% 2.26/2.50 cnf(c576,plain,skolem0001!=X1014|skolem0005(skolem0009(skolem0001,skolem0004))!=X1015|fire(X1014,X1015),inference(resolution,[status(thm)],[c570, c20])).
% 2.26/2.50 cnf(c942,plain,skolem0001!=X1016|fire(X1016,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c576, reflexivity])).
% 2.26/2.50 cnf(c38,axiom,X403!=X402|X401!=X400|~nonreflexive(X403,X401)|nonreflexive(X402,X400),theory(equality)).
% 2.26/2.50 cnf(c569,plain,skolem0001!=X1012|skolem0005(skolem0011(skolem0001,skolem0004))!=X1011|nonreflexive(X1012,X1011),inference(resolution,[status(thm)],[c551, c38])).
% 2.26/2.50 cnf(c940,plain,skolem0001!=X1013|nonreflexive(X1013,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c569, reflexivity])).
% 2.26/2.50 cnf(c562,plain,skolem0001!=X1009|skolem0005(skolem0013(skolem0001,skolem0004))!=X1008|nonreflexive(X1009,X1008),inference(resolution,[status(thm)],[c550, c38])).
% 2.26/2.50 cnf(c938,plain,skolem0001!=X1010|nonreflexive(X1010,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c562, reflexivity])).
% 2.26/2.50 cnf(c561,plain,skolem0001!=X1006|skolem0005(skolem0008(skolem0001,skolem0004))!=X1005|nonreflexive(X1006,X1005),inference(resolution,[status(thm)],[c549, c38])).
% 2.26/2.50 cnf(c936,plain,skolem0001!=X1007|nonreflexive(X1007,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c561, reflexivity])).
% 2.26/2.50 cnf(c560,plain,skolem0001!=X1003|skolem0005(skolem0012(skolem0001,skolem0004))!=X1002|nonreflexive(X1003,X1002),inference(resolution,[status(thm)],[c548, c38])).
% 2.26/2.50 cnf(c934,plain,skolem0001!=X1004|nonreflexive(X1004,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c560, reflexivity])).
% 2.26/2.50 cnf(c559,plain,skolem0001!=X1000|skolem0005(skolem0010(skolem0001,skolem0004))!=X999|nonreflexive(X1000,X999),inference(resolution,[status(thm)],[c547, c38])).
% 2.26/2.50 cnf(c932,plain,skolem0001!=X1001|nonreflexive(X1001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c559, reflexivity])).
% 2.26/2.50 cnf(c558,plain,skolem0001!=X997|skolem0005(skolem0009(skolem0001,skolem0004))!=X996|nonreflexive(X997,X996),inference(resolution,[status(thm)],[c546, c38])).
% 2.26/2.50 cnf(c930,plain,skolem0001!=X998|nonreflexive(X998,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c558, reflexivity])).
% 2.26/2.50 cnf(c58,negated_conjecture,~member(skolem0001,X416,skolem0004)|present(skolem0001,skolem0005(X416)),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.50 cnf(c544,plain,present(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c58, c307])).
% 2.26/2.50 cnf(c43,axiom,X427!=X426|X425!=X424|~present(X427,X425)|present(X426,X424),theory(equality)).
% 2.26/2.50 cnf(c557,plain,skolem0001!=X993|skolem0005(skolem0013(skolem0001,skolem0004))!=X994|present(X993,X994),inference(resolution,[status(thm)],[c43, c544])).
% 2.26/2.50 cnf(c928,plain,skolem0001!=X995|present(X995,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c557, reflexivity])).
% 2.26/2.50 cnf(c543,plain,present(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c58, c301])).
% 2.26/2.50 cnf(c556,plain,skolem0001!=X990|skolem0005(skolem0008(skolem0001,skolem0004))!=X991|present(X990,X991),inference(resolution,[status(thm)],[c43, c543])).
% 2.26/2.50 cnf(c926,plain,skolem0001!=X992|present(X992,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c556, reflexivity])).
% 2.26/2.50 cnf(c541,plain,present(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c58, c303])).
% 2.26/2.50 cnf(c555,plain,skolem0001!=X987|skolem0005(skolem0010(skolem0001,skolem0004))!=X988|present(X987,X988),inference(resolution,[status(thm)],[c43, c541])).
% 2.26/2.50 cnf(c924,plain,skolem0001!=X989|present(X989,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c555, reflexivity])).
% 2.26/2.50 cnf(c540,plain,present(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c58, c302])).
% 2.26/2.50 cnf(c554,plain,skolem0001!=X984|skolem0005(skolem0009(skolem0001,skolem0004))!=X985|present(X984,X985),inference(resolution,[status(thm)],[c43, c540])).
% 2.26/2.50 cnf(c922,plain,skolem0001!=X986|present(X986,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c554, reflexivity])).
% 2.26/2.50 cnf(c545,plain,present(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c58, c304])).
% 2.26/2.50 cnf(c553,plain,skolem0001!=X981|skolem0005(skolem0011(skolem0001,skolem0004))!=X982|present(X981,X982),inference(resolution,[status(thm)],[c43, c545])).
% 2.26/2.50 cnf(c920,plain,skolem0001!=X983|present(X983,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c553, reflexivity])).
% 2.26/2.50 cnf(c542,plain,present(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c58, c305])).
% 2.26/2.50 cnf(c552,plain,skolem0001!=X978|skolem0005(skolem0012(skolem0001,skolem0004))!=X979|present(X978,X979),inference(resolution,[status(thm)],[c43, c542])).
% 2.26/2.50 cnf(c918,plain,skolem0001!=X980|present(X980,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c552, reflexivity])).
% 2.26/2.50 cnf(c34,axiom,X383!=X382|X381!=X380|~singleton(X383,X381)|singleton(X382,X380),theory(equality)).
% 2.26/2.50 fof(ax34,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 2.26/2.50 fof(c142,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 2.26/2.50 fof(c143,plain,(![X61]:(![X62]:(~thing(X61,X62)|singleton(X61,X62)))),inference(variable_rename,[status(thm)],[c142])).
% 2.26/2.50 cnf(c144,plain,~thing(X164,X165)|singleton(X164,X165),inference(split_conjunct,[status(thm)],[c143])).
% 2.26/2.50 fof(ax35,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 2.26/2.50 fof(c139,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 2.26/2.50 fof(c140,plain,(![X59]:(![X60]:(~eventuality(X59,X60)|thing(X59,X60)))),inference(variable_rename,[status(thm)],[c139])).
% 2.26/2.50 cnf(c141,plain,~eventuality(X159,X158)|thing(X159,X158),inference(split_conjunct,[status(thm)],[c140])).
% 2.26/2.50 fof(ax36,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 2.26/2.50 fof(c136,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax36])).
% 2.26/2.50 fof(c137,plain,(![X57]:(![X58]:(~event(X57,X58)|eventuality(X57,X58)))),inference(variable_rename,[status(thm)],[c136])).
% 2.26/2.50 cnf(c138,plain,~event(X156,X157)|eventuality(X156,X157),inference(split_conjunct,[status(thm)],[c137])).
% 2.26/2.50 cnf(c55,negated_conjecture,~member(skolem0001,X367,skolem0004)|event(skolem0001,skolem0005(X367)),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.50 cnf(c428,plain,event(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c55, c304])).
% 2.26/2.50 cnf(c439,plain,eventuality(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c428, c138])).
% 2.26/2.50 cnf(c478,plain,thing(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c439, c141])).
% 2.26/2.50 cnf(c527,plain,singleton(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c478, c144])).
% 2.26/2.50 cnf(c539,plain,skolem0001!=X976|skolem0005(skolem0011(skolem0001,skolem0004))!=X975|singleton(X976,X975),inference(resolution,[status(thm)],[c527, c34])).
% 2.26/2.50 cnf(c916,plain,skolem0001!=X977|singleton(X977,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c539, reflexivity])).
% 2.26/2.50 cnf(c41,axiom,X415!=X412|X413!=X410|X411!=X414|~of(X415,X413,X411)|of(X412,X410,X414),theory(equality)).
% 2.26/2.50 cnf(c538,plain,skolem0001!=X969|skolem0003!=X970|skolem0002!=X971|of(X969,X970,X971),inference(resolution,[status(thm)],[c41, c53])).
% 2.26/2.50 cnf(c913,plain,skolem0001!=X972|skolem0003!=X973|of(X972,X973,skolem0002),inference(resolution,[status(thm)],[c538, reflexivity])).
% 2.26/2.50 cnf(c914,plain,skolem0001!=X974|of(X974,skolem0003,skolem0002),inference(resolution,[status(thm)],[c913, reflexivity])).
% 2.26/2.50 cnf(c427,plain,event(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c55, c307])).
% 2.26/2.50 cnf(c437,plain,eventuality(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c427, c138])).
% 2.26/2.50 cnf(c467,plain,thing(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c437, c141])).
% 2.26/2.50 cnf(c521,plain,singleton(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c467, c144])).
% 2.26/2.50 cnf(c537,plain,skolem0001!=X967|skolem0005(skolem0013(skolem0001,skolem0004))!=X966|singleton(X967,X966),inference(resolution,[status(thm)],[c521, c34])).
% 2.26/2.50 cnf(c911,plain,skolem0001!=X968|singleton(X968,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c537, reflexivity])).
% 2.26/2.50 cnf(c426,plain,event(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c55, c301])).
% 2.26/2.50 cnf(c435,plain,eventuality(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c426, c138])).
% 2.26/2.50 cnf(c462,plain,thing(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c435, c141])).
% 2.26/2.50 cnf(c509,plain,singleton(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c462, c144])).
% 2.26/2.50 cnf(c536,plain,skolem0001!=X964|skolem0005(skolem0008(skolem0001,skolem0004))!=X963|singleton(X964,X963),inference(resolution,[status(thm)],[c509, c34])).
% 2.26/2.50 cnf(c909,plain,skolem0001!=X965|singleton(X965,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c536, reflexivity])).
% 2.26/2.50 cnf(c425,plain,event(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c55, c305])).
% 2.26/2.50 cnf(c433,plain,eventuality(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c425, c138])).
% 2.26/2.50 cnf(c457,plain,thing(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c433, c141])).
% 2.26/2.50 cnf(c503,plain,singleton(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c457, c144])).
% 2.26/2.50 cnf(c535,plain,skolem0001!=X961|skolem0005(skolem0012(skolem0001,skolem0004))!=X960|singleton(X961,X960),inference(resolution,[status(thm)],[c503, c34])).
% 2.26/2.50 cnf(c907,plain,skolem0001!=X962|singleton(X962,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c535, reflexivity])).
% 2.26/2.50 cnf(c424,plain,event(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c55, c303])).
% 2.26/2.50 cnf(c431,plain,eventuality(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c424, c138])).
% 2.26/2.50 cnf(c452,plain,thing(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c431, c141])).
% 2.26/2.50 cnf(c497,plain,singleton(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c452, c144])).
% 2.26/2.50 cnf(c534,plain,skolem0001!=X958|skolem0005(skolem0010(skolem0001,skolem0004))!=X957|singleton(X958,X957),inference(resolution,[status(thm)],[c497, c34])).
% 2.26/2.50 cnf(c905,plain,skolem0001!=X959|singleton(X959,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c534, reflexivity])).
% 2.26/2.50 cnf(c423,plain,event(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c55, c302])).
% 2.26/2.50 cnf(c429,plain,eventuality(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c423, c138])).
% 2.26/2.50 cnf(c447,plain,thing(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c429, c141])).
% 2.26/2.50 cnf(c483,plain,singleton(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c447, c144])).
% 2.26/2.50 cnf(c533,plain,skolem0001!=X955|skolem0005(skolem0009(skolem0001,skolem0004))!=X954|singleton(X955,X954),inference(resolution,[status(thm)],[c483, c34])).
% 2.26/2.50 cnf(c903,plain,skolem0001!=X956|singleton(X956,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c533, reflexivity])).
% 2.26/2.50 cnf(c10,axiom,X253!=X252|X251!=X250|~unisex(X253,X251)|unisex(X252,X250),theory(equality)).
% 2.26/2.50 fof(ax31,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 2.26/2.50 fof(c151,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 2.26/2.50 fof(c152,plain,(![X67]:(![X68]:(~eventuality(X67,X68)|unisex(X67,X68)))),inference(variable_rename,[status(thm)],[c151])).
% 2.26/2.50 cnf(c153,plain,~eventuality(X171,X170)|unisex(X171,X170),inference(split_conjunct,[status(thm)],[c152])).
% 2.26/2.50 cnf(c482,plain,unisex(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c439, c153])).
% 2.26/2.50 cnf(c532,plain,skolem0001!=X952|skolem0005(skolem0011(skolem0001,skolem0004))!=X951|unisex(X952,X951),inference(resolution,[status(thm)],[c482, c10])).
% 2.26/2.50 cnf(c901,plain,skolem0001!=X953|unisex(X953,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c532, reflexivity])).
% 2.26/2.50 cnf(c13,axiom,X275!=X274|X273!=X272|~specific(X275,X273)|specific(X274,X272),theory(equality)).
% 2.26/2.50 fof(ax33,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 2.26/2.50 fof(c145,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 2.26/2.50 fof(c146,plain,(![X63]:(![X64]:(~eventuality(X63,X64)|specific(X63,X64)))),inference(variable_rename,[status(thm)],[c145])).
% 2.26/2.50 cnf(c147,plain,~eventuality(X167,X166)|specific(X167,X166),inference(split_conjunct,[status(thm)],[c146])).
% 2.26/2.50 cnf(c481,plain,specific(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c439, c147])).
% 2.26/2.50 cnf(c531,plain,skolem0001!=X946|skolem0005(skolem0011(skolem0001,skolem0004))!=X945|specific(X946,X945),inference(resolution,[status(thm)],[c481, c13])).
% 2.26/2.50 cnf(c898,plain,skolem0001!=X950|specific(X950,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c531, reflexivity])).
% 2.26/2.50 cnf(c33,axiom,X379!=X378|X377!=X376|~nonexistent(X379,X377)|nonexistent(X378,X376),theory(equality)).
% 2.26/2.50 fof(ax32,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 2.26/2.50 fof(c148,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 2.26/2.50 fof(c149,plain,(![X65]:(![X66]:(~eventuality(X65,X66)|nonexistent(X65,X66)))),inference(variable_rename,[status(thm)],[c148])).
% 2.26/2.50 cnf(c150,plain,~eventuality(X169,X168)|nonexistent(X169,X168),inference(split_conjunct,[status(thm)],[c149])).
% 2.26/2.50 cnf(c480,plain,nonexistent(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c439, c150])).
% 2.26/2.50 cnf(c530,plain,skolem0001!=X942|skolem0005(skolem0011(skolem0001,skolem0004))!=X943|nonexistent(X942,X943),inference(resolution,[status(thm)],[c480, c33])).
% 2.26/2.50 cnf(c896,plain,skolem0001!=X944|nonexistent(X944,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c530, reflexivity])).
% 2.26/2.50 cnf(c14,axiom,X283!=X282|X281!=X280|~thing(X283,X281)|thing(X282,X280),theory(equality)).
% 2.26/2.50 cnf(c528,plain,skolem0001!=X936|skolem0005(skolem0011(skolem0001,skolem0004))!=X937|thing(X936,X937),inference(resolution,[status(thm)],[c478, c14])).
% 2.26/2.50 cnf(c893,plain,skolem0001!=X938|thing(X938,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c528, reflexivity])).
% 2.26/2.50 cnf(c471,plain,unisex(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c437, c153])).
% 2.26/2.50 cnf(c526,plain,skolem0001!=X934|skolem0005(skolem0013(skolem0001,skolem0004))!=X933|unisex(X934,X933),inference(resolution,[status(thm)],[c471, c10])).
% 2.26/2.50 cnf(c891,plain,skolem0001!=X935|unisex(X935,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c526, reflexivity])).
% 2.26/2.50 cnf(c470,plain,specific(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c437, c147])).
% 2.26/2.50 cnf(c525,plain,skolem0001!=X928|skolem0005(skolem0013(skolem0001,skolem0004))!=X927|specific(X928,X927),inference(resolution,[status(thm)],[c470, c13])).
% 2.26/2.50 cnf(c888,plain,skolem0001!=X929|specific(X929,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c525, reflexivity])).
% 2.26/2.50 cnf(c469,plain,nonexistent(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c437, c150])).
% 2.26/2.50 cnf(c524,plain,skolem0001!=X921|skolem0005(skolem0013(skolem0001,skolem0004))!=X922|nonexistent(X921,X922),inference(resolution,[status(thm)],[c469, c33])).
% 2.26/2.50 cnf(c885,plain,skolem0001!=X926|nonexistent(X926,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c524, reflexivity])).
% 2.26/2.50 cnf(c522,plain,skolem0001!=X918|skolem0005(skolem0013(skolem0001,skolem0004))!=X919|thing(X918,X919),inference(resolution,[status(thm)],[c467, c14])).
% 2.26/2.50 cnf(c883,plain,skolem0001!=X920|thing(X920,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c522, reflexivity])).
% 2.26/2.50 cnf(c466,plain,unisex(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c435, c153])).
% 2.26/2.50 cnf(c520,plain,skolem0001!=X913|skolem0005(skolem0008(skolem0001,skolem0004))!=X912|unisex(X913,X912),inference(resolution,[status(thm)],[c466, c10])).
% 2.26/2.50 cnf(c880,plain,skolem0001!=X914|unisex(X914,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c520, reflexivity])).
% 2.26/2.50 cnf(c465,plain,specific(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c435, c147])).
% 2.26/2.50 cnf(c519,plain,skolem0001!=X910|skolem0005(skolem0008(skolem0001,skolem0004))!=X909|specific(X910,X909),inference(resolution,[status(thm)],[c465, c13])).
% 2.26/2.50 cnf(c878,plain,skolem0001!=X911|specific(X911,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c519, reflexivity])).
% 2.26/2.50 cnf(c464,plain,nonexistent(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c435, c150])).
% 2.26/2.50 cnf(c512,plain,skolem0001!=X903|skolem0005(skolem0008(skolem0001,skolem0004))!=X904|nonexistent(X903,X904),inference(resolution,[status(thm)],[c464, c33])).
% 2.26/2.50 cnf(c875,plain,skolem0001!=X905|nonexistent(X905,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c512, reflexivity])).
% 2.26/2.50 cnf(c510,plain,skolem0001!=X900|skolem0005(skolem0008(skolem0001,skolem0004))!=X901|thing(X900,X901),inference(resolution,[status(thm)],[c462, c14])).
% 2.26/2.50 cnf(c873,plain,skolem0001!=X902|thing(X902,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c510, reflexivity])).
% 2.26/2.50 cnf(c461,plain,unisex(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c433, c153])).
% 2.26/2.50 cnf(c508,plain,skolem0001!=X898|skolem0005(skolem0012(skolem0001,skolem0004))!=X897|unisex(X898,X897),inference(resolution,[status(thm)],[c461, c10])).
% 2.26/2.50 cnf(c871,plain,skolem0001!=X899|unisex(X899,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c508, reflexivity])).
% 2.26/2.50 cnf(c460,plain,specific(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c433, c147])).
% 2.26/2.50 cnf(c507,plain,skolem0001!=X895|skolem0005(skolem0012(skolem0001,skolem0004))!=X894|specific(X895,X894),inference(resolution,[status(thm)],[c460, c13])).
% 2.26/2.50 cnf(c869,plain,skolem0001!=X896|specific(X896,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c507, reflexivity])).
% 2.26/2.50 cnf(c459,plain,nonexistent(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c433, c150])).
% 2.26/2.50 cnf(c506,plain,skolem0001!=X891|skolem0005(skolem0012(skolem0001,skolem0004))!=X892|nonexistent(X891,X892),inference(resolution,[status(thm)],[c459, c33])).
% 2.26/2.50 cnf(c867,plain,skolem0001!=X893|nonexistent(X893,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c506, reflexivity])).
% 2.26/2.50 cnf(c504,plain,skolem0001!=X888|skolem0005(skolem0012(skolem0001,skolem0004))!=X889|thing(X888,X889),inference(resolution,[status(thm)],[c457, c14])).
% 2.26/2.50 cnf(c865,plain,skolem0001!=X890|thing(X890,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c504, reflexivity])).
% 2.26/2.50 cnf(c456,plain,unisex(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c431, c153])).
% 2.26/2.50 cnf(c502,plain,skolem0001!=X886|skolem0005(skolem0010(skolem0001,skolem0004))!=X885|unisex(X886,X885),inference(resolution,[status(thm)],[c456, c10])).
% 2.26/2.50 cnf(c863,plain,skolem0001!=X887|unisex(X887,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c502, reflexivity])).
% 2.26/2.50 cnf(c455,plain,specific(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c431, c147])).
% 2.26/2.50 cnf(c501,plain,skolem0001!=X883|skolem0005(skolem0010(skolem0001,skolem0004))!=X882|specific(X883,X882),inference(resolution,[status(thm)],[c455, c13])).
% 2.26/2.50 cnf(c861,plain,skolem0001!=X884|specific(X884,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c501, reflexivity])).
% 2.26/2.50 cnf(c454,plain,nonexistent(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c431, c150])).
% 2.26/2.50 cnf(c500,plain,skolem0001!=X879|skolem0005(skolem0010(skolem0001,skolem0004))!=X880|nonexistent(X879,X880),inference(resolution,[status(thm)],[c454, c33])).
% 2.26/2.50 cnf(c853,plain,skolem0001!=X881|nonexistent(X881,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c500, reflexivity])).
% 2.26/2.50 cnf(c498,plain,skolem0001!=X876|skolem0005(skolem0010(skolem0001,skolem0004))!=X877|thing(X876,X877),inference(resolution,[status(thm)],[c452, c14])).
% 2.26/2.50 cnf(c845,plain,skolem0001!=X878|thing(X878,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c498, reflexivity])).
% 2.26/2.50 fof(ax26,axiom,(![U]:(![V]:(act(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 2.26/2.50 fof(c166,plain,(![U]:(![V]:(~act(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 2.26/2.50 fof(c167,plain,(![X77]:(![X78]:(~act(X77,X78)|event(X77,X78)))),inference(variable_rename,[status(thm)],[c166])).
% 2.26/2.50 cnf(c168,plain,~act(X185,X184)|event(X185,X184),inference(split_conjunct,[status(thm)],[c167])).
% 2.26/2.50 fof(ax27,axiom,(![U]:(![V]:(action(U,V)=>act(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 2.26/2.50 fof(c163,plain,(![U]:(![V]:(~action(U,V)|act(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 2.26/2.50 fof(c164,plain,(![X75]:(![X76]:(~action(X75,X76)|act(X75,X76)))),inference(variable_rename,[status(thm)],[c163])).
% 2.26/2.50 cnf(c165,plain,~action(X183,X182)|act(X183,X182),inference(split_conjunct,[status(thm)],[c164])).
% 2.26/2.50 fof(ax25,axiom,(![U]:(![V]:(shot(U,V)=>action(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 2.26/2.50 fof(c169,plain,(![U]:(![V]:(~shot(U,V)|action(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 2.26/2.51 fof(c170,plain,(![X79]:(![X80]:(~shot(X79,X80)|action(X79,X80)))),inference(variable_rename,[status(thm)],[c169])).
% 2.26/2.51 cnf(c171,plain,~shot(X187,X186)|action(X187,X186),inference(split_conjunct,[status(thm)],[c170])).
% 2.26/2.51 cnf(c64,negated_conjecture,~member(skolem0001,X290,skolem0004)|shot(skolem0001,X290),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.51 cnf(c405,plain,shot(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c307, c64])).
% 2.26/2.51 cnf(c406,plain,action(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c405, c171])).
% 2.26/2.51 cnf(c409,plain,act(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c406, c165])).
% 2.26/2.51 cnf(c411,plain,event(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c409, c168])).
% 2.26/2.51 cnf(c412,plain,eventuality(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c411, c138])).
% 2.26/2.51 cnf(c415,plain,thing(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c412, c141])).
% 2.26/2.51 cnf(c419,plain,singleton(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c415, c144])).
% 2.26/2.51 cnf(c496,plain,skolem0001!=X874|skolem0013(skolem0001,skolem0004)!=X873|singleton(X874,X873),inference(resolution,[status(thm)],[c34, c419])).
% 2.26/2.51 cnf(c843,plain,skolem0001!=X875|singleton(X875,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c496, reflexivity])).
% 2.26/2.51 cnf(c451,plain,unisex(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c429, c153])).
% 2.26/2.51 cnf(c488,plain,skolem0001!=X871|skolem0005(skolem0009(skolem0001,skolem0004))!=X870|unisex(X871,X870),inference(resolution,[status(thm)],[c451, c10])).
% 2.26/2.51 cnf(c841,plain,skolem0001!=X872|unisex(X872,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c488, reflexivity])).
% 2.26/2.51 cnf(c358,plain,shot(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c304, c64])).
% 2.26/2.51 cnf(c359,plain,action(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c358, c171])).
% 2.26/2.51 cnf(c360,plain,act(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c359, c165])).
% 2.26/2.51 cnf(c362,plain,event(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c360, c168])).
% 2.26/2.51 cnf(c363,plain,eventuality(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c362, c138])).
% 2.26/2.51 cnf(c366,plain,thing(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c363, c141])).
% 2.26/2.51 cnf(c370,plain,singleton(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c366, c144])).
% 2.26/2.51 cnf(c495,plain,skolem0001!=X868|skolem0011(skolem0001,skolem0004)!=X867|singleton(X868,X867),inference(resolution,[status(thm)],[c34, c370])).
% 2.26/2.51 cnf(c839,plain,skolem0001!=X869|singleton(X869,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c495, reflexivity])).
% 2.26/2.51 cnf(c450,plain,specific(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c429, c147])).
% 2.26/2.51 cnf(c487,plain,skolem0001!=X865|skolem0005(skolem0009(skolem0001,skolem0004))!=X864|specific(X865,X864),inference(resolution,[status(thm)],[c450, c13])).
% 2.26/2.51 cnf(c837,plain,skolem0001!=X866|specific(X866,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c487, reflexivity])).
% 2.26/2.51 cnf(c324,plain,shot(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c302, c64])).
% 2.26/2.51 cnf(c325,plain,action(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c324, c171])).
% 2.26/2.51 cnf(c327,plain,act(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c325, c165])).
% 2.26/2.51 cnf(c328,plain,event(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c327, c168])).
% 2.26/2.51 cnf(c329,plain,eventuality(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c328, c138])).
% 2.26/2.51 cnf(c331,plain,thing(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c329, c141])).
% 2.26/2.51 cnf(c335,plain,singleton(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c331, c144])).
% 2.26/2.51 cnf(c494,plain,skolem0001!=X862|skolem0009(skolem0001,skolem0004)!=X861|singleton(X862,X861),inference(resolution,[status(thm)],[c34, c335])).
% 2.26/2.51 cnf(c835,plain,skolem0001!=X863|singleton(X863,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c494, reflexivity])).
% 2.26/2.51 cnf(c449,plain,nonexistent(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c429, c150])).
% 2.26/2.51 cnf(c486,plain,skolem0001!=X858|skolem0005(skolem0009(skolem0001,skolem0004))!=X859|nonexistent(X858,X859),inference(resolution,[status(thm)],[c449, c33])).
% 2.26/2.51 cnf(c833,plain,skolem0001!=X860|nonexistent(X860,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c486, reflexivity])).
% 2.26/2.51 cnf(c308,plain,shot(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c301, c64])).
% 2.26/2.51 cnf(c309,plain,action(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c308, c171])).
% 2.26/2.51 cnf(c310,plain,act(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c309, c165])).
% 2.26/2.51 cnf(c311,plain,event(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c310, c168])).
% 2.26/2.51 cnf(c313,plain,eventuality(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c311, c138])).
% 2.26/2.51 cnf(c315,plain,thing(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c313, c141])).
% 2.26/2.51 cnf(c319,plain,singleton(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c315, c144])).
% 2.26/2.51 cnf(c493,plain,skolem0001!=X856|skolem0008(skolem0001,skolem0004)!=X855|singleton(X856,X855),inference(resolution,[status(thm)],[c34, c319])).
% 2.26/2.51 cnf(c831,plain,skolem0001!=X857|singleton(X857,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c493, reflexivity])).
% 2.26/2.51 cnf(c484,plain,skolem0001!=X852|skolem0005(skolem0009(skolem0001,skolem0004))!=X853|thing(X852,X853),inference(resolution,[status(thm)],[c447, c14])).
% 2.26/2.51 cnf(c829,plain,skolem0001!=X854|thing(X854,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c484, reflexivity])).
% 2.26/2.51 cnf(c375,plain,shot(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c305, c64])).
% 2.26/2.51 cnf(c380,plain,action(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c375, c171])).
% 2.26/2.51 cnf(c382,plain,act(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c380, c165])).
% 2.26/2.51 cnf(c383,plain,event(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c382, c168])).
% 2.26/2.51 cnf(c384,plain,eventuality(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c383, c138])).
% 2.26/2.51 cnf(c387,plain,thing(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c384, c141])).
% 2.26/2.51 cnf(c396,plain,singleton(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c387, c144])).
% 2.26/2.51 cnf(c492,plain,skolem0001!=X850|skolem0012(skolem0001,skolem0004)!=X849|singleton(X850,X849),inference(resolution,[status(thm)],[c34, c396])).
% 2.26/2.51 cnf(c827,plain,skolem0001!=X851|singleton(X851,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c492, reflexivity])).
% 2.26/2.51 cnf(c32,axiom,X375!=X374|X373!=X372|~eventuality(X375,X373)|eventuality(X374,X372),theory(equality)).
% 2.26/2.51 cnf(c479,plain,skolem0001!=X847|skolem0005(skolem0011(skolem0001,skolem0004))!=X846|eventuality(X847,X846),inference(resolution,[status(thm)],[c439, c32])).
% 2.26/2.51 cnf(c825,plain,skolem0001!=X848|eventuality(X848,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c479, reflexivity])).
% 2.26/2.51 cnf(c341,plain,shot(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c303, c64])).
% 2.26/2.51 cnf(c342,plain,action(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c341, c171])).
% 2.26/2.51 cnf(c343,plain,act(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c342, c165])).
% 2.26/2.51 cnf(c344,plain,event(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c343, c168])).
% 2.26/2.51 cnf(c345,plain,eventuality(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c344, c138])).
% 2.26/2.51 cnf(c349,plain,thing(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c345, c141])).
% 2.26/2.51 cnf(c353,plain,singleton(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c349, c144])).
% 2.26/2.51 cnf(c489,plain,skolem0001!=X844|skolem0010(skolem0001,skolem0004)!=X843|singleton(X844,X843),inference(resolution,[status(thm)],[c34, c353])).
% 2.26/2.51 cnf(c823,plain,skolem0001!=X845|singleton(X845,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c489, reflexivity])).
% 2.26/2.51 cnf(c333,plain,nonexistent(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c329, c150])).
% 2.26/2.51 cnf(c477,plain,skolem0001!=X840|skolem0009(skolem0001,skolem0004)!=X841|nonexistent(X840,X841),inference(resolution,[status(thm)],[c33, c333])).
% 2.26/2.51 cnf(c821,plain,skolem0001!=X842|nonexistent(X842,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c477, reflexivity])).
% 2.26/2.51 cnf(c389,plain,nonexistent(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c384, c150])).
% 2.26/2.51 cnf(c476,plain,skolem0001!=X837|skolem0012(skolem0001,skolem0004)!=X838|nonexistent(X837,X838),inference(resolution,[status(thm)],[c33, c389])).
% 2.26/2.51 cnf(c819,plain,skolem0001!=X839|nonexistent(X839,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c476, reflexivity])).
% 2.26/2.51 cnf(c468,plain,skolem0001!=X835|skolem0005(skolem0013(skolem0001,skolem0004))!=X834|eventuality(X835,X834),inference(resolution,[status(thm)],[c437, c32])).
% 2.26/2.51 cnf(c817,plain,skolem0001!=X836|eventuality(X836,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c468, reflexivity])).
% 2.26/2.51 cnf(c317,plain,nonexistent(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c313, c150])).
% 2.26/2.51 cnf(c475,plain,skolem0001!=X831|skolem0008(skolem0001,skolem0004)!=X832|nonexistent(X831,X832),inference(resolution,[status(thm)],[c33, c317])).
% 2.26/2.51 cnf(c815,plain,skolem0001!=X833|nonexistent(X833,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c475, reflexivity])).
% 2.26/2.51 cnf(c463,plain,skolem0001!=X829|skolem0005(skolem0008(skolem0001,skolem0004))!=X828|eventuality(X829,X828),inference(resolution,[status(thm)],[c435, c32])).
% 2.26/2.51 cnf(c813,plain,skolem0001!=X830|eventuality(X830,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c463, reflexivity])).
% 2.26/2.51 cnf(c351,plain,nonexistent(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c345, c150])).
% 2.26/2.51 cnf(c474,plain,skolem0001!=X825|skolem0010(skolem0001,skolem0004)!=X826|nonexistent(X825,X826),inference(resolution,[status(thm)],[c33, c351])).
% 2.26/2.51 cnf(c811,plain,skolem0001!=X827|nonexistent(X827,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c474, reflexivity])).
% 2.26/2.51 cnf(c458,plain,skolem0001!=X823|skolem0005(skolem0012(skolem0001,skolem0004))!=X822|eventuality(X823,X822),inference(resolution,[status(thm)],[c433, c32])).
% 2.26/2.51 cnf(c809,plain,skolem0001!=X824|eventuality(X824,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c458, reflexivity])).
% 2.26/2.51 cnf(c417,plain,nonexistent(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c412, c150])).
% 2.26/2.51 cnf(c473,plain,skolem0001!=X819|skolem0013(skolem0001,skolem0004)!=X820|nonexistent(X819,X820),inference(resolution,[status(thm)],[c33, c417])).
% 2.26/2.51 cnf(c807,plain,skolem0001!=X821|nonexistent(X821,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c473, reflexivity])).
% 2.26/2.51 cnf(c453,plain,skolem0001!=X817|skolem0005(skolem0010(skolem0001,skolem0004))!=X816|eventuality(X817,X816),inference(resolution,[status(thm)],[c431, c32])).
% 2.26/2.51 cnf(c805,plain,skolem0001!=X818|eventuality(X818,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c453, reflexivity])).
% 2.26/2.51 cnf(c368,plain,nonexistent(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c363, c150])).
% 2.26/2.51 cnf(c472,plain,skolem0001!=X813|skolem0011(skolem0001,skolem0004)!=X814|nonexistent(X813,X814),inference(resolution,[status(thm)],[c33, c368])).
% 2.26/2.51 cnf(c803,plain,skolem0001!=X815|nonexistent(X815,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c472, reflexivity])).
% 2.26/2.51 cnf(c448,plain,skolem0001!=X811|skolem0005(skolem0009(skolem0001,skolem0004))!=X810|eventuality(X811,X810),inference(resolution,[status(thm)],[c429, c32])).
% 2.26/2.51 cnf(c801,plain,skolem0001!=X812|eventuality(X812,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c448, reflexivity])).
% 2.26/2.51 cnf(c446,plain,skolem0001!=X808|skolem0011(skolem0001,skolem0004)!=X807|eventuality(X808,X807),inference(resolution,[status(thm)],[c32, c363])).
% 2.26/2.51 cnf(c799,plain,skolem0001!=X809|eventuality(X809,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c446, reflexivity])).
% 2.26/2.51 cnf(c21,axiom,X330!=X329|X328!=X327|~event(X330,X328)|event(X329,X327),theory(equality)).
% 2.26/2.51 cnf(c440,plain,skolem0001!=X805|skolem0005(skolem0011(skolem0001,skolem0004))!=X804|event(X805,X804),inference(resolution,[status(thm)],[c428, c21])).
% 2.26/2.51 cnf(c797,plain,skolem0001!=X806|event(X806,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c440, reflexivity])).
% 2.26/2.51 cnf(c445,plain,skolem0001!=X802|skolem0009(skolem0001,skolem0004)!=X801|eventuality(X802,X801),inference(resolution,[status(thm)],[c32, c329])).
% 2.26/2.51 cnf(c795,plain,skolem0001!=X803|eventuality(X803,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c445, reflexivity])).
% 2.26/2.51 cnf(c438,plain,skolem0001!=X799|skolem0005(skolem0013(skolem0001,skolem0004))!=X798|event(X799,X798),inference(resolution,[status(thm)],[c427, c21])).
% 2.26/2.51 cnf(c793,plain,skolem0001!=X800|event(X800,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c438, reflexivity])).
% 2.26/2.51 cnf(c444,plain,skolem0001!=X796|skolem0012(skolem0001,skolem0004)!=X795|eventuality(X796,X795),inference(resolution,[status(thm)],[c32, c384])).
% 2.26/2.51 cnf(c791,plain,skolem0001!=X797|eventuality(X797,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c444, reflexivity])).
% 2.26/2.51 cnf(c436,plain,skolem0001!=X793|skolem0005(skolem0008(skolem0001,skolem0004))!=X792|event(X793,X792),inference(resolution,[status(thm)],[c426, c21])).
% 2.26/2.51 cnf(c789,plain,skolem0001!=X794|event(X794,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c436, reflexivity])).
% 2.26/2.51 cnf(c443,plain,skolem0001!=X790|skolem0008(skolem0001,skolem0004)!=X789|eventuality(X790,X789),inference(resolution,[status(thm)],[c32, c313])).
% 2.26/2.51 cnf(c787,plain,skolem0001!=X791|eventuality(X791,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c443, reflexivity])).
% 2.26/2.51 cnf(c434,plain,skolem0001!=X787|skolem0005(skolem0012(skolem0001,skolem0004))!=X786|event(X787,X786),inference(resolution,[status(thm)],[c425, c21])).
% 2.26/2.51 cnf(c785,plain,skolem0001!=X788|event(X788,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c434, reflexivity])).
% 2.26/2.51 cnf(c442,plain,skolem0001!=X784|skolem0013(skolem0001,skolem0004)!=X783|eventuality(X784,X783),inference(resolution,[status(thm)],[c32, c412])).
% 2.26/2.51 cnf(c783,plain,skolem0001!=X785|eventuality(X785,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c442, reflexivity])).
% 2.26/2.51 cnf(c432,plain,skolem0001!=X781|skolem0005(skolem0010(skolem0001,skolem0004))!=X780|event(X781,X780),inference(resolution,[status(thm)],[c424, c21])).
% 2.26/2.51 cnf(c781,plain,skolem0001!=X782|event(X782,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c432, reflexivity])).
% 2.26/2.51 cnf(c441,plain,skolem0001!=X778|skolem0010(skolem0001,skolem0004)!=X777|eventuality(X778,X777),inference(resolution,[status(thm)],[c32, c345])).
% 2.26/2.51 cnf(c779,plain,skolem0001!=X779|eventuality(X779,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c441, reflexivity])).
% 2.26/2.51 cnf(c430,plain,skolem0001!=X775|skolem0005(skolem0009(skolem0001,skolem0004))!=X774|event(X775,X774),inference(resolution,[status(thm)],[c423, c21])).
% 2.26/2.51 cnf(c777,plain,skolem0001!=X776|event(X776,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c430, reflexivity])).
% 2.26/2.51 cnf(c416,plain,unisex(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c412, c153])).
% 2.26/2.51 cnf(c421,plain,skolem0001!=X772|skolem0013(skolem0001,skolem0004)!=X771|unisex(X772,X771),inference(resolution,[status(thm)],[c416, c10])).
% 2.26/2.51 cnf(c775,plain,skolem0001!=X773|unisex(X773,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c421, reflexivity])).
% 2.26/2.51 cnf(c420,plain,skolem0001!=X768|skolem0013(skolem0001,skolem0004)!=X769|thing(X768,X769),inference(resolution,[status(thm)],[c415, c14])).
% 2.26/2.51 cnf(c773,plain,skolem0001!=X770|thing(X770,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c420, reflexivity])).
% 2.26/2.51 cnf(c414,plain,specific(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c412, c147])).
% 2.26/2.51 cnf(c418,plain,skolem0001!=X766|skolem0013(skolem0001,skolem0004)!=X765|specific(X766,X765),inference(resolution,[status(thm)],[c414, c13])).
% 2.26/2.51 cnf(c771,plain,skolem0001!=X767|specific(X767,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c418, reflexivity])).
% 2.26/2.51 cnf(c413,plain,skolem0001!=X763|skolem0013(skolem0001,skolem0004)!=X762|event(X763,X762),inference(resolution,[status(thm)],[c411, c21])).
% 2.26/2.51 cnf(c769,plain,skolem0001!=X764|event(X764,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c413, reflexivity])).
% 2.26/2.51 cnf(c28,axiom,X358!=X357|X356!=X355|~act(X358,X356)|act(X357,X355),theory(equality)).
% 2.26/2.51 cnf(c410,plain,skolem0001!=X760|skolem0013(skolem0001,skolem0004)!=X759|act(X760,X759),inference(resolution,[status(thm)],[c409, c28])).
% 2.26/2.51 cnf(c767,plain,skolem0001!=X761|act(X761,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c410, reflexivity])).
% 2.26/2.51 cnf(c27,axiom,X354!=X353|X352!=X351|~action(X354,X352)|action(X353,X351),theory(equality)).
% 2.26/2.51 cnf(c408,plain,skolem0001!=X757|skolem0013(skolem0001,skolem0004)!=X756|action(X757,X756),inference(resolution,[status(thm)],[c406, c27])).
% 2.26/2.51 cnf(c765,plain,skolem0001!=X758|action(X758,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c408, reflexivity])).
% 2.26/2.51 cnf(c26,axiom,X350!=X349|X348!=X347|~shot(X350,X348)|shot(X349,X347),theory(equality)).
% 2.26/2.51 cnf(c407,plain,skolem0001!=X753|skolem0013(skolem0001,skolem0004)!=X754|shot(X753,X754),inference(resolution,[status(thm)],[c405, c26])).
% 2.26/2.51 cnf(c763,plain,skolem0001!=X755|shot(X755,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c407, reflexivity])).
% 2.26/2.51 cnf(c404,plain,skolem0001!=X751|skolem0012(skolem0001,skolem0004)!=X750|act(X751,X750),inference(resolution,[status(thm)],[c28, c382])).
% 2.26/2.51 cnf(c761,plain,skolem0001!=X752|act(X752,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c404, reflexivity])).
% 2.26/2.51 cnf(c403,plain,skolem0001!=X748|skolem0010(skolem0001,skolem0004)!=X747|act(X748,X747),inference(resolution,[status(thm)],[c28, c343])).
% 2.26/2.51 cnf(c759,plain,skolem0001!=X749|act(X749,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c403, reflexivity])).
% 2.26/2.51 cnf(c402,plain,skolem0001!=X745|skolem0011(skolem0001,skolem0004)!=X744|act(X745,X744),inference(resolution,[status(thm)],[c28, c360])).
% 2.26/2.51 cnf(c757,plain,skolem0001!=X746|act(X746,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c402, reflexivity])).
% 2.26/2.51 cnf(c401,plain,skolem0001!=X742|skolem0008(skolem0001,skolem0004)!=X741|act(X742,X741),inference(resolution,[status(thm)],[c28, c310])).
% 2.26/2.51 cnf(c755,plain,skolem0001!=X743|act(X743,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c401, reflexivity])).
% 2.26/2.51 cnf(c400,plain,skolem0001!=X739|skolem0009(skolem0001,skolem0004)!=X738|act(X739,X738),inference(resolution,[status(thm)],[c28, c327])).
% 2.26/2.51 cnf(c753,plain,skolem0001!=X740|act(X740,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c400, reflexivity])).
% 2.26/2.51 cnf(c388,plain,unisex(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c384, c153])).
% 2.26/2.51 cnf(c398,plain,skolem0001!=X736|skolem0012(skolem0001,skolem0004)!=X735|unisex(X736,X735),inference(resolution,[status(thm)],[c388, c10])).
% 2.26/2.51 cnf(c751,plain,skolem0001!=X737|unisex(X737,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c398, reflexivity])).
% 2.26/2.51 cnf(c397,plain,skolem0001!=X732|skolem0012(skolem0001,skolem0004)!=X733|thing(X732,X733),inference(resolution,[status(thm)],[c387, c14])).
% 2.26/2.51 cnf(c749,plain,skolem0001!=X734|thing(X734,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c397, reflexivity])).
% 2.26/2.51 cnf(c386,plain,specific(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c384, c147])).
% 2.26/2.51 cnf(c395,plain,skolem0001!=X730|skolem0012(skolem0001,skolem0004)!=X729|specific(X730,X729),inference(resolution,[status(thm)],[c386, c13])).
% 2.26/2.51 cnf(c747,plain,skolem0001!=X731|specific(X731,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c395, reflexivity])).
% 2.26/2.51 cnf(c394,plain,skolem0001!=X727|skolem0008(skolem0001,skolem0004)!=X726|action(X727,X726),inference(resolution,[status(thm)],[c27, c309])).
% 2.26/2.51 cnf(c745,plain,skolem0001!=X728|action(X728,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c394, reflexivity])).
% 2.26/2.51 cnf(c393,plain,skolem0001!=X724|skolem0009(skolem0001,skolem0004)!=X723|action(X724,X723),inference(resolution,[status(thm)],[c27, c325])).
% 2.26/2.51 cnf(c743,plain,skolem0001!=X725|action(X725,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c393, reflexivity])).
% 2.26/2.51 cnf(c392,plain,skolem0001!=X721|skolem0011(skolem0001,skolem0004)!=X720|action(X721,X720),inference(resolution,[status(thm)],[c27, c359])).
% 2.26/2.51 cnf(c741,plain,skolem0001!=X722|action(X722,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c392, reflexivity])).
% 2.26/2.51 cnf(c391,plain,skolem0001!=X718|skolem0012(skolem0001,skolem0004)!=X717|action(X718,X717),inference(resolution,[status(thm)],[c27, c380])).
% 2.26/2.51 cnf(c739,plain,skolem0001!=X719|action(X719,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c391, reflexivity])).
% 2.26/2.51 cnf(c390,plain,skolem0001!=X715|skolem0010(skolem0001,skolem0004)!=X714|action(X715,X714),inference(resolution,[status(thm)],[c27, c342])).
% 2.26/2.51 cnf(c737,plain,skolem0001!=X716|action(X716,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c390, reflexivity])).
% 2.26/2.51 cnf(c385,plain,skolem0001!=X712|skolem0012(skolem0001,skolem0004)!=X711|event(X712,X711),inference(resolution,[status(thm)],[c383, c21])).
% 2.26/2.51 cnf(c735,plain,skolem0001!=X713|event(X713,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c385, reflexivity])).
% 2.26/2.51 cnf(c381,plain,skolem0001!=X708|skolem0012(skolem0001,skolem0004)!=X709|shot(X708,X709),inference(resolution,[status(thm)],[c375, c26])).
% 2.26/2.51 cnf(c733,plain,skolem0001!=X710|shot(X710,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c381, reflexivity])).
% 2.26/2.51 cnf(c379,plain,skolem0001!=X705|skolem0008(skolem0001,skolem0004)!=X706|shot(X705,X706),inference(resolution,[status(thm)],[c26, c308])).
% 2.26/2.51 cnf(c731,plain,skolem0001!=X707|shot(X707,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c379, reflexivity])).
% 2.26/2.51 cnf(c378,plain,skolem0001!=X702|skolem0011(skolem0001,skolem0004)!=X703|shot(X702,X703),inference(resolution,[status(thm)],[c26, c358])).
% 2.26/2.51 cnf(c729,plain,skolem0001!=X704|shot(X704,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c378, reflexivity])).
% 2.26/2.51 cnf(c377,plain,skolem0001!=X699|skolem0010(skolem0001,skolem0004)!=X700|shot(X699,X700),inference(resolution,[status(thm)],[c26, c341])).
% 2.26/2.51 cnf(c727,plain,skolem0001!=X701|shot(X701,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c377, reflexivity])).
% 2.26/2.51 cnf(c376,plain,skolem0001!=X696|skolem0009(skolem0001,skolem0004)!=X697|shot(X696,X697),inference(resolution,[status(thm)],[c26, c324])).
% 2.26/2.51 cnf(c725,plain,skolem0001!=X698|shot(X698,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c376, reflexivity])).
% 2.26/2.51 cnf(c367,plain,unisex(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c363, c153])).
% 2.26/2.51 cnf(c373,plain,skolem0001!=X694|skolem0011(skolem0001,skolem0004)!=X693|unisex(X694,X693),inference(resolution,[status(thm)],[c367, c10])).
% 2.26/2.51 cnf(c723,plain,skolem0001!=X695|unisex(X695,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c373, reflexivity])).
% 2.26/2.51 cnf(c371,plain,skolem0001!=X690|skolem0011(skolem0001,skolem0004)!=X691|thing(X690,X691),inference(resolution,[status(thm)],[c366, c14])).
% 2.26/2.51 cnf(c721,plain,skolem0001!=X692|thing(X692,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c371, reflexivity])).
% 2.26/2.51 cnf(c365,plain,specific(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c363, c147])).
% 2.26/2.51 cnf(c369,plain,skolem0001!=X688|skolem0011(skolem0001,skolem0004)!=X687|specific(X688,X687),inference(resolution,[status(thm)],[c365, c13])).
% 2.26/2.51 cnf(c719,plain,skolem0001!=X689|specific(X689,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c369, reflexivity])).
% 2.26/2.51 cnf(c364,plain,skolem0001!=X685|skolem0011(skolem0001,skolem0004)!=X684|event(X685,X684),inference(resolution,[status(thm)],[c362, c21])).
% 2.26/2.51 cnf(c717,plain,skolem0001!=X686|event(X686,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c364, reflexivity])).
% 2.26/2.51 cnf(c350,plain,unisex(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c345, c153])).
% 2.26/2.51 cnf(c355,plain,skolem0001!=X681|skolem0010(skolem0001,skolem0004)!=X680|unisex(X681,X680),inference(resolution,[status(thm)],[c350, c10])).
% 2.26/2.51 cnf(c714,plain,skolem0001!=X683|unisex(X683,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c355, reflexivity])).
% 2.26/2.51 cnf(c354,plain,skolem0001!=X675|skolem0010(skolem0001,skolem0004)!=X676|thing(X675,X676),inference(resolution,[status(thm)],[c349, c14])).
% 2.26/2.51 cnf(c710,plain,skolem0001!=X682|thing(X682,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c354, reflexivity])).
% 2.26/2.51 cnf(c348,plain,specific(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c345, c147])).
% 2.26/2.51 cnf(c352,plain,skolem0001!=X672|skolem0010(skolem0001,skolem0004)!=X671|specific(X672,X671),inference(resolution,[status(thm)],[c348, c13])).
% 2.26/2.51 cnf(c707,plain,skolem0001!=X679|specific(X679,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c352, reflexivity])).
% 2.26/2.51 cnf(c346,plain,skolem0001!=X667|skolem0010(skolem0001,skolem0004)!=X666|event(X667,X666),inference(resolution,[status(thm)],[c344, c21])).
% 2.26/2.51 cnf(c703,plain,skolem0001!=X678|event(X678,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c346, reflexivity])).
% 2.26/2.51 cnf(c340,plain,skolem0001!=X663|skolem0008(skolem0001,skolem0004)!=X662|event(X663,X662),inference(resolution,[status(thm)],[c21, c311])).
% 2.26/2.51 cnf(c699,plain,skolem0001!=X677|event(X677,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c340, reflexivity])).
% 2.26/2.51 cnf(c339,plain,skolem0001!=X661|skolem0009(skolem0001,skolem0004)!=X660|event(X661,X660),inference(resolution,[status(thm)],[c21, c328])).
% 2.26/2.51 cnf(c693,plain,skolem0001!=X674|event(X674,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c339, reflexivity])).
% 2.26/2.51 cnf(c332,plain,unisex(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c329, c153])).
% 2.26/2.51 cnf(c337,plain,skolem0001!=X659|skolem0009(skolem0001,skolem0004)!=X658|unisex(X659,X658),inference(resolution,[status(thm)],[c332, c10])).
% 2.26/2.51 cnf(c687,plain,skolem0001!=X673|unisex(X673,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c337, reflexivity])).
% 2.26/2.51 cnf(c336,plain,skolem0001!=X653|skolem0009(skolem0001,skolem0004)!=X654|thing(X653,X654),inference(resolution,[status(thm)],[c331, c14])).
% 2.26/2.51 cnf(c683,plain,skolem0001!=X670|thing(X670,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c336, reflexivity])).
% 2.26/2.51 cnf(c330,plain,specific(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c329, c147])).
% 2.26/2.51 cnf(c334,plain,skolem0001!=X646|skolem0009(skolem0001,skolem0004)!=X645|specific(X646,X645),inference(resolution,[status(thm)],[c330, c13])).
% 2.26/2.51 cnf(c678,plain,skolem0001!=X669|specific(X669,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c334, reflexivity])).
% 2.26/2.51 cnf(c316,plain,unisex(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c313, c153])).
% 2.26/2.51 cnf(c321,plain,skolem0001!=X640|skolem0008(skolem0001,skolem0004)!=X639|unisex(X640,X639),inference(resolution,[status(thm)],[c316, c10])).
% 2.26/2.51 cnf(c674,plain,skolem0001!=X668|unisex(X668,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c321, reflexivity])).
% 2.26/2.51 cnf(c320,plain,skolem0001!=X632|skolem0008(skolem0001,skolem0004)!=X633|thing(X632,X633),inference(resolution,[status(thm)],[c315, c14])).
% 2.26/2.51 cnf(c670,plain,skolem0001!=X665|thing(X665,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c320, reflexivity])).
% 2.26/2.51 cnf(c314,plain,specific(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c313, c147])).
% 2.26/2.51 cnf(c318,plain,skolem0001!=X625|skolem0008(skolem0001,skolem0004)!=X624|specific(X625,X624),inference(resolution,[status(thm)],[c314, c13])).
% 2.26/2.51 cnf(c665,plain,skolem0001!=X664|specific(X664,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c318, reflexivity])).
% 2.26/2.51 fof(ax14,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 2.26/2.51 fof(c202,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 2.26/2.51 fof(c203,plain,(![X101]:(![X102]:(~entity(X101,X102)|thing(X101,X102)))),inference(variable_rename,[status(thm)],[c202])).
% 2.26/2.51 cnf(c204,plain,~entity(X229,X228)|thing(X229,X228),inference(split_conjunct,[status(thm)],[c203])).
% 2.26/2.51 cnf(c52,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.51 fof(ax8,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 2.26/2.51 fof(c220,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 2.26/2.51 fof(c221,plain,(![X113]:(![X114]:(~man(X113,X114)|human_person(X113,X114)))),inference(variable_rename,[status(thm)],[c220])).
% 2.26/2.51 cnf(c222,plain,~man(X248,X249)|human_person(X248,X249),inference(split_conjunct,[status(thm)],[c221])).
% 2.26/2.51 cnf(c271,plain,human_person(skolem0001,skolem0002),inference(resolution,[status(thm)],[c222, c52])).
% 2.26/2.51 fof(ax7,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 2.26/2.51 fof(c223,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 2.26/2.51 fof(c224,plain,(![X115]:(![X116]:(~human_person(X115,X116)|organism(X115,X116)))),inference(variable_rename,[status(thm)],[c223])).
% 2.26/2.51 cnf(c225,plain,~human_person(X255,X254)|organism(X255,X254),inference(split_conjunct,[status(thm)],[c224])).
% 2.26/2.51 cnf(c274,plain,organism(skolem0001,skolem0002),inference(resolution,[status(thm)],[c225, c271])).
% 2.26/2.51 fof(ax6,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 2.26/2.51 fof(c226,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 2.26/2.51 fof(c227,plain,(![X117]:(![X118]:(~organism(X117,X118)|entity(X117,X118)))),inference(variable_rename,[status(thm)],[c226])).
% 2.26/2.51 cnf(c228,plain,~organism(X256,X257)|entity(X256,X257),inference(split_conjunct,[status(thm)],[c227])).
% 2.26/2.51 cnf(c276,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c228, c274])).
% 2.26/2.51 cnf(c278,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c276, c204])).
% 2.26/2.51 cnf(c282,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c278, c144])).
% 2.26/2.51 cnf(c491,plain,skolem0001!=X656|skolem0002!=X655|singleton(X656,X655),inference(resolution,[status(thm)],[c34, c282])).
% 2.26/2.51 cnf(c684,plain,skolem0001!=X657|singleton(X657,skolem0002),inference(resolution,[status(thm)],[c491, reflexivity])).
% 2.26/2.51 cnf(c54,negated_conjecture,cannon(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.51 fof(ax20,axiom,(![U]:(![V]:(cannon(U,V)=>weapon(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 2.26/2.51 fof(c184,plain,(![U]:(![V]:(~cannon(U,V)|weapon(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 2.26/2.51 fof(c185,plain,(![X89]:(![X90]:(~cannon(X89,X90)|weapon(X89,X90)))),inference(variable_rename,[status(thm)],[c184])).
% 2.26/2.51 cnf(c186,plain,~cannon(X204,X205)|weapon(X204,X205),inference(split_conjunct,[status(thm)],[c185])).
% 2.26/2.51 cnf(c254,plain,weapon(skolem0001,skolem0003),inference(resolution,[status(thm)],[c186, c54])).
% 2.26/2.51 fof(ax19,axiom,(![U]:(![V]:(weapon(U,V)=>weaponry(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 2.26/2.51 fof(c187,plain,(![U]:(![V]:(~weapon(U,V)|weaponry(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 2.26/2.51 fof(c188,plain,(![X91]:(![X92]:(~weapon(X91,X92)|weaponry(X91,X92)))),inference(variable_rename,[status(thm)],[c187])).
% 2.26/2.51 cnf(c189,plain,~weapon(X211,X210)|weaponry(X211,X210),inference(split_conjunct,[status(thm)],[c188])).
% 2.26/2.51 cnf(c255,plain,weaponry(skolem0001,skolem0003),inference(resolution,[status(thm)],[c189, c254])).
% 2.26/2.51 fof(ax18,axiom,(![U]:(![V]:(weaponry(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 2.26/2.51 fof(c190,plain,(![U]:(![V]:(~weaponry(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 2.26/2.51 fof(c191,plain,(![X93]:(![X94]:(~weaponry(X93,X94)|instrumentality(X93,X94)))),inference(variable_rename,[status(thm)],[c190])).
% 2.26/2.51 cnf(c192,plain,~weaponry(X212,X213)|instrumentality(X212,X213),inference(split_conjunct,[status(thm)],[c191])).
% 2.26/2.51 cnf(c256,plain,instrumentality(skolem0001,skolem0003),inference(resolution,[status(thm)],[c192, c255])).
% 2.26/2.51 fof(ax17,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 2.26/2.51 fof(c193,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 2.26/2.51 fof(c194,plain,(![X95]:(![X96]:(~instrumentality(X95,X96)|artifact(X95,X96)))),inference(variable_rename,[status(thm)],[c193])).
% 2.26/2.51 cnf(c195,plain,~instrumentality(X214,X215)|artifact(X214,X215),inference(split_conjunct,[status(thm)],[c194])).
% 2.26/2.51 cnf(c257,plain,artifact(skolem0001,skolem0003),inference(resolution,[status(thm)],[c195, c256])).
% 2.26/2.51 fof(ax16,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 2.26/2.51 fof(c196,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 2.26/2.51 fof(c197,plain,(![X97]:(![X98]:(~artifact(X97,X98)|object(X97,X98)))),inference(variable_rename,[status(thm)],[c196])).
% 2.26/2.51 cnf(c198,plain,~artifact(X221,X220)|object(X221,X220),inference(split_conjunct,[status(thm)],[c197])).
% 2.26/2.51 cnf(c258,plain,object(skolem0001,skolem0003),inference(resolution,[status(thm)],[c198, c257])).
% 2.26/2.51 fof(ax15,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 2.26/2.51 fof(c199,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 2.26/2.51 fof(c200,plain,(![X99]:(![X100]:(~object(X99,X100)|entity(X99,X100)))),inference(variable_rename,[status(thm)],[c199])).
% 2.26/2.51 cnf(c201,plain,~object(X223,X222)|entity(X223,X222),inference(split_conjunct,[status(thm)],[c200])).
% 2.26/2.51 cnf(c259,plain,entity(skolem0001,skolem0003),inference(resolution,[status(thm)],[c201, c258])).
% 2.26/2.51 cnf(c260,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c204, c259])).
% 2.26/2.51 cnf(c261,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c260, c144])).
% 2.26/2.51 cnf(c490,plain,skolem0001!=X651|skolem0003!=X650|singleton(X651,X650),inference(resolution,[status(thm)],[c34, c261])).
% 2.26/2.51 cnf(c681,plain,skolem0001!=X652|singleton(X652,skolem0003),inference(resolution,[status(thm)],[c490, reflexivity])).
% 2.26/2.51 cnf(c63,negated_conjecture,group(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.51 fof(ax24,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 2.26/2.51 fof(c172,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 2.26/2.51 fof(c173,plain,(![X81]:(![X82]:(~group(X81,X82)|set(X81,X82)))),inference(variable_rename,[status(thm)],[c172])).
% 2.26/2.51 cnf(c174,plain,~group(X192,X193)|set(X192,X193),inference(split_conjunct,[status(thm)],[c173])).
% 2.26/2.51 cnf(c250,plain,set(skolem0001,skolem0004),inference(resolution,[status(thm)],[c174, c63])).
% 2.26/2.51 fof(ax23,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 2.26/2.51 fof(c175,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 2.26/2.51 fof(c176,plain,(![X83]:(![X84]:(~set(X83,X84)|multiple(X83,X84)))),inference(variable_rename,[status(thm)],[c175])).
% 2.26/2.51 cnf(c177,plain,~set(X194,X195)|multiple(X194,X195),inference(split_conjunct,[status(thm)],[c176])).
% 2.26/2.51 cnf(c251,plain,multiple(skolem0001,skolem0004),inference(resolution,[status(thm)],[c177, c250])).
% 2.26/2.51 cnf(c25,axiom,X346!=X345|X344!=X343|~multiple(X346,X344)|multiple(X345,X343),theory(equality)).
% 2.26/2.51 cnf(c372,plain,skolem0001!=X647|skolem0004!=X648|multiple(X647,X648),inference(resolution,[status(thm)],[c25, c251])).
% 2.26/2.51 cnf(c679,plain,skolem0001!=X649|multiple(X649,skolem0004),inference(resolution,[status(thm)],[c372, reflexivity])).
% 2.26/2.51 cnf(c24,axiom,X342!=X341|X340!=X339|~set(X342,X340)|set(X341,X339),theory(equality)).
% 2.26/2.51 cnf(c361,plain,skolem0001!=X642|skolem0004!=X643|set(X642,X643),inference(resolution,[status(thm)],[c24, c250])).
% 2.26/2.51 cnf(c676,plain,skolem0001!=X644|set(X644,skolem0004),inference(resolution,[status(thm)],[c361, reflexivity])).
% 2.26/2.51 cnf(c23,axiom,X338!=X337|X336!=X335|~group(X338,X336)|group(X337,X335),theory(equality)).
% 2.26/2.51 cnf(c357,plain,skolem0001!=X637|skolem0004!=X638|group(X637,X638),inference(resolution,[status(thm)],[c23, c63])).
% 2.26/2.51 cnf(c673,plain,skolem0001!=X641|group(X641,skolem0004),inference(resolution,[status(thm)],[c357, reflexivity])).
% 2.26/2.51 cnf(c22,axiom,X334!=X333|X332!=X331|~six(X334,X332)|six(X333,X331),theory(equality)).
% 2.26/2.51 cnf(c347,plain,skolem0001!=X634|skolem0004!=X635|six(X634,X635),inference(resolution,[status(thm)],[c22, c62])).
% 2.26/2.51 cnf(c671,plain,skolem0001!=X636|six(X636,skolem0004),inference(resolution,[status(thm)],[c347, reflexivity])).
% 2.26/2.51 cnf(c19,axiom,X322!=X321|X320!=X319|~cannon(X322,X320)|cannon(X321,X319),theory(equality)).
% 2.26/2.51 cnf(c326,plain,skolem0001!=X629|skolem0003!=X630|cannon(X629,X630),inference(resolution,[status(thm)],[c19, c54])).
% 2.26/2.51 cnf(c668,plain,skolem0001!=X631|cannon(X631,skolem0003),inference(resolution,[status(thm)],[c326, reflexivity])).
% 2.26/2.51 cnf(c18,axiom,X318!=X317|X316!=X315|~weapon(X318,X316)|weapon(X317,X315),theory(equality)).
% 2.26/2.51 cnf(c322,plain,skolem0001!=X627|skolem0003!=X626|weapon(X627,X626),inference(resolution,[status(thm)],[c18, c254])).
% 2.26/2.51 cnf(c666,plain,skolem0001!=X628|weapon(X628,skolem0003),inference(resolution,[status(thm)],[c322, reflexivity])).
% 2.26/2.51 cnf(c17,axiom,X314!=X313|X312!=X311|~weaponry(X314,X312)|weaponry(X313,X311),theory(equality)).
% 2.26/2.51 cnf(c312,plain,skolem0001!=X622|skolem0003!=X621|weaponry(X622,X621),inference(resolution,[status(thm)],[c17, c255])).
% 2.26/2.51 cnf(c663,plain,skolem0001!=X623|weaponry(X623,skolem0003),inference(resolution,[status(thm)],[c312, reflexivity])).
% 2.26/2.51 cnf(c16,axiom,X308!=X307|X306!=X305|~instrumentality(X308,X306)|instrumentality(X307,X305),theory(equality)).
% 2.26/2.51 cnf(c306,plain,skolem0001!=X618|skolem0003!=X619|instrumentality(X618,X619),inference(resolution,[status(thm)],[c16, c256])).
% 2.26/2.51 cnf(c661,plain,skolem0001!=X620|instrumentality(X620,skolem0003),inference(resolution,[status(thm)],[c306, reflexivity])).
% 2.26/2.51 cnf(c15,axiom,X294!=X293|X292!=X291|~artifact(X294,X292)|artifact(X293,X291),theory(equality)).
% 2.26/2.51 cnf(c300,plain,skolem0001!=X615|skolem0003!=X616|artifact(X615,X616),inference(resolution,[status(thm)],[c15, c257])).
% 2.26/2.51 cnf(c659,plain,skolem0001!=X617|artifact(X617,skolem0003),inference(resolution,[status(thm)],[c300, reflexivity])).
% 2.26/2.51 cnf(c298,plain,skolem0001!=X612|skolem0002!=X613|thing(X612,X613),inference(resolution,[status(thm)],[c14, c278])).
% 2.26/2.51 cnf(c657,plain,skolem0001!=X614|thing(X614,skolem0002),inference(resolution,[status(thm)],[c298, reflexivity])).
% 2.26/2.51 cnf(c297,plain,skolem0001!=X609|skolem0003!=X610|thing(X609,X610),inference(resolution,[status(thm)],[c14, c260])).
% 2.26/2.51 cnf(c655,plain,skolem0001!=X611|thing(X611,skolem0003),inference(resolution,[status(thm)],[c297, reflexivity])).
% 2.26/2.51 cnf(c3,axiom,X191!=X190|X189!=X188|~animate(X191,X189)|animate(X190,X188),theory(equality)).
% 2.26/2.51 fof(ax2,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 2.26/2.51 fof(c238,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 2.26/2.51 fof(c239,plain,(![X125]:(![X126]:(~human_person(X125,X126)|animate(X125,X126)))),inference(variable_rename,[status(thm)],[c238])).
% 2.26/2.51 cnf(c240,plain,~human_person(X277,X276)|animate(X277,X276),inference(split_conjunct,[status(thm)],[c239])).
% 2.26/2.51 cnf(c294,plain,animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c240, c271])).
% 2.26/2.51 cnf(c295,plain,skolem0001!=X607|skolem0002!=X606|animate(X607,X606),inference(resolution,[status(thm)],[c294, c3])).
% 2.26/2.51 cnf(c653,plain,skolem0001!=X608|animate(X608,skolem0002),inference(resolution,[status(thm)],[c295, reflexivity])).
% 2.26/2.51 cnf(c4,axiom,X199!=X198|X197!=X196|~human(X199,X197)|human(X198,X196),theory(equality)).
% 2.26/2.51 fof(ax3,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 2.26/2.51 fof(c235,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 2.26/2.51 fof(c236,plain,(![X123]:(![X124]:(~human_person(X123,X124)|human(X123,X124)))),inference(variable_rename,[status(thm)],[c235])).
% 2.26/2.51 cnf(c237,plain,~human_person(X270,X271)|human(X270,X271),inference(split_conjunct,[status(thm)],[c236])).
% 2.26/2.51 cnf(c290,plain,human(skolem0001,skolem0002),inference(resolution,[status(thm)],[c237, c271])).
% 2.26/2.51 cnf(c293,plain,skolem0001!=X604|skolem0002!=X603|human(X604,X603),inference(resolution,[status(thm)],[c290, c4])).
% 2.26/2.51 cnf(c651,plain,skolem0001!=X605|human(X605,skolem0002),inference(resolution,[status(thm)],[c293, reflexivity])).
% 2.26/2.51 fof(ax13,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 2.26/2.51 fof(c205,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 2.26/2.51 fof(c206,plain,(![X103]:(![X104]:(~entity(X103,X104)|specific(X103,X104)))),inference(variable_rename,[status(thm)],[c205])).
% 2.26/2.51 cnf(c207,plain,~entity(X230,X231)|specific(X230,X231),inference(split_conjunct,[status(thm)],[c206])).
% 2.26/2.51 cnf(c262,plain,specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c207, c259])).
% 2.26/2.51 cnf(c292,plain,skolem0001!=X593|skolem0003!=X592|specific(X593,X592),inference(resolution,[status(thm)],[c13, c262])).
% 2.26/2.51 cnf(c649,plain,skolem0001!=X602|specific(X602,skolem0003),inference(resolution,[status(thm)],[c292, reflexivity])).
% 2.26/2.51 cnf(c109,plain,~member(X597,X598,X595)|~member(X597,X599,X595)|X599=X598|~member(X597,X596,X595)|X596=X599|X596=X598|~member(X597,X600,X595)|X600=X596|X600=X599|X600=X598|~member(X597,X601,X595)|X601=X600|X601=X596|X601=X599|X601=X598|~member(X597,X594,X595)|X594=X601|X594=X600|X594=X596|X594=X599|X594=X598|skolem0014(X597,X595,X598,X599,X596,X600,X601,X594)!=X598|six(X597,X595),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.51 cnf(c279,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c276, c207])).
% 2.26/2.51 cnf(c291,plain,skolem0001!=X590|skolem0002!=X589|specific(X590,X589),inference(resolution,[status(thm)],[c13, c279])).
% 2.26/2.51 cnf(c647,plain,skolem0001!=X591|specific(X591,skolem0002),inference(resolution,[status(thm)],[c291, reflexivity])).
% 2.26/2.51 cnf(c108,plain,~member(X584,X585,X582)|~member(X584,X586,X582)|X586=X585|~member(X584,X583,X582)|X583=X586|X583=X585|~member(X584,X587,X582)|X587=X583|X587=X586|X587=X585|~member(X584,X588,X582)|X588=X587|X588=X583|X588=X586|X588=X585|~member(X584,X581,X582)|X581=X588|X581=X587|X581=X583|X581=X586|X581=X585|skolem0014(X584,X582,X585,X586,X583,X587,X588,X581)!=X586|six(X584,X582),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.51 cnf(c6,axiom,X219!=X218|X217!=X216|~living(X219,X217)|living(X218,X216),theory(equality)).
% 2.26/2.51 fof(ax4,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 2.26/2.51 fof(c232,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 2.26/2.51 fof(c233,plain,(![X121]:(![X122]:(~organism(X121,X122)|living(X121,X122)))),inference(variable_rename,[status(thm)],[c232])).
% 2.26/2.51 cnf(c234,plain,~organism(X268,X269)|living(X268,X269),inference(split_conjunct,[status(thm)],[c233])).
% 2.26/2.51 cnf(c287,plain,living(skolem0001,skolem0002),inference(resolution,[status(thm)],[c234, c274])).
% 2.26/2.51 cnf(c289,plain,skolem0001!=X579|skolem0002!=X578|living(X579,X578),inference(resolution,[status(thm)],[c287, c6])).
% 2.26/2.51 cnf(c645,plain,skolem0001!=X580|living(X580,skolem0002),inference(resolution,[status(thm)],[c289, reflexivity])).
% 2.26/2.51 cnf(c7,axiom,X227!=X226|X225!=X224|~impartial(X227,X225)|impartial(X226,X224),theory(equality)).
% 2.26/2.51 fof(ax5,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 2.26/2.51 fof(c229,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 2.26/2.51 fof(c230,plain,(![X119]:(![X120]:(~organism(X119,X120)|impartial(X119,X120)))),inference(variable_rename,[status(thm)],[c229])).
% 2.26/2.51 cnf(c231,plain,~organism(X262,X263)|impartial(X262,X263),inference(split_conjunct,[status(thm)],[c230])).
% 2.26/2.51 cnf(c283,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c231, c274])).
% 2.26/2.51 cnf(c286,plain,skolem0001!=X575|skolem0002!=X576|impartial(X575,X576),inference(resolution,[status(thm)],[c283, c7])).
% 2.26/2.51 cnf(c643,plain,skolem0001!=X577|impartial(X577,skolem0002),inference(resolution,[status(thm)],[c286, reflexivity])).
% 2.26/2.51 cnf(c107,plain,~member(X570,X571,X568)|~member(X570,X572,X568)|X572=X571|~member(X570,X569,X568)|X569=X572|X569=X571|~member(X570,X573,X568)|X573=X569|X573=X572|X573=X571|~member(X570,X574,X568)|X574=X573|X574=X569|X574=X572|X574=X571|~member(X570,X567,X568)|X567=X574|X567=X573|X567=X569|X567=X572|X567=X571|skolem0014(X570,X568,X571,X572,X569,X573,X574,X567)!=X569|six(X570,X568),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.51 fof(ax12,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 2.26/2.51 fof(c208,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 2.26/2.51 fof(c209,plain,(![X105]:(![X106]:(~entity(X105,X106)|existent(X105,X106)))),inference(variable_rename,[status(thm)],[c208])).
% 2.26/2.51 cnf(c210,plain,~entity(X236,X237)|existent(X236,X237),inference(split_conjunct,[status(thm)],[c209])).
% 2.26/2.51 cnf(c280,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c276, c210])).
% 2.26/2.51 cnf(c12,axiom,X267!=X266|X265!=X264|~existent(X267,X265)|existent(X266,X264),theory(equality)).
% 2.26/2.51 cnf(c285,plain,skolem0001!=X564|skolem0002!=X565|existent(X564,X565),inference(resolution,[status(thm)],[c12, c280])).
% 2.26/2.51 cnf(c641,plain,skolem0001!=X566|existent(X566,skolem0002),inference(resolution,[status(thm)],[c285, reflexivity])).
% 2.26/2.51 cnf(c264,plain,existent(skolem0001,skolem0003),inference(resolution,[status(thm)],[c210, c259])).
% 2.26/2.51 cnf(c284,plain,skolem0001!=X553|skolem0003!=X554|existent(X553,X554),inference(resolution,[status(thm)],[c12, c264])).
% 2.26/2.51 cnf(c639,plain,skolem0001!=X563|existent(X563,skolem0003),inference(resolution,[status(thm)],[c284, reflexivity])).
% 2.26/2.51 cnf(c106,plain,~member(X558,X559,X556)|~member(X558,X560,X556)|X560=X559|~member(X558,X557,X556)|X557=X560|X557=X559|~member(X558,X561,X556)|X561=X557|X561=X560|X561=X559|~member(X558,X562,X556)|X562=X561|X562=X557|X562=X560|X562=X559|~member(X558,X555,X556)|X555=X562|X555=X561|X555=X557|X555=X560|X555=X559|skolem0014(X558,X556,X559,X560,X557,X561,X562,X555)!=X561|six(X558,X556),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.51 fof(ax11,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 2.26/2.51 fof(c211,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 2.26/2.51 fof(c212,plain,(![X107]:(![X108]:(~object(X107,X108)|nonliving(X107,X108)))),inference(variable_rename,[status(thm)],[c211])).
% 2.26/2.51 cnf(c213,plain,~object(X238,X239)|nonliving(X238,X239),inference(split_conjunct,[status(thm)],[c212])).
% 2.26/2.51 cnf(c265,plain,nonliving(skolem0001,skolem0003),inference(resolution,[status(thm)],[c213, c258])).
% 2.26/2.51 cnf(c11,axiom,X261!=X260|X259!=X258|~nonliving(X261,X259)|nonliving(X260,X258),theory(equality)).
% 2.26/2.51 cnf(c281,plain,skolem0001!=X551|skolem0003!=X550|nonliving(X551,X550),inference(resolution,[status(thm)],[c11, c265])).
% 2.26/2.51 cnf(c637,plain,skolem0001!=X552|nonliving(X552,skolem0003),inference(resolution,[status(thm)],[c281, reflexivity])).
% 2.26/2.51 cnf(c105,plain,~member(X545,X546,X543)|~member(X545,X547,X543)|X547=X546|~member(X545,X544,X543)|X544=X547|X544=X546|~member(X545,X548,X543)|X548=X544|X548=X547|X548=X546|~member(X545,X549,X543)|X549=X548|X549=X544|X549=X547|X549=X546|~member(X545,X542,X543)|X542=X549|X542=X548|X542=X544|X542=X547|X542=X546|skolem0014(X545,X543,X546,X547,X544,X548,X549,X542)!=X549|six(X545,X543),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.51 cnf(c8,axiom,X235!=X234|X233!=X232|~entity(X235,X233)|entity(X234,X232),theory(equality)).
% 2.26/2.51 cnf(c277,plain,skolem0001!=X540|skolem0002!=X539|entity(X540,X539),inference(resolution,[status(thm)],[c276, c8])).
% 2.26/2.51 cnf(c635,plain,skolem0001!=X541|entity(X541,skolem0002),inference(resolution,[status(thm)],[c277, reflexivity])).
% 2.26/2.51 cnf(c5,axiom,X209!=X208|X207!=X206|~organism(X209,X207)|organism(X208,X206),theory(equality)).
% 2.26/2.51 cnf(c275,plain,skolem0001!=X536|skolem0002!=X537|organism(X536,X537),inference(resolution,[status(thm)],[c274, c5])).
% 2.26/2.51 cnf(c633,plain,skolem0001!=X538|organism(X538,skolem0002),inference(resolution,[status(thm)],[c275, reflexivity])).
% 2.26/2.51 cnf(c104,plain,~member(X531,X532,X529)|~member(X531,X533,X529)|X533=X532|~member(X531,X530,X529)|X530=X533|X530=X532|~member(X531,X534,X529)|X534=X530|X534=X533|X534=X532|~member(X531,X535,X529)|X535=X534|X535=X530|X535=X533|X535=X532|~member(X531,X528,X529)|X528=X535|X528=X534|X528=X530|X528=X533|X528=X532|skolem0014(X531,X529,X532,X533,X530,X534,X535,X528)!=X528|six(X531,X529),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.51 cnf(c2,axiom,X177!=X176|X175!=X174|~human_person(X177,X175)|human_person(X176,X174),theory(equality)).
% 2.26/2.51 cnf(c273,plain,skolem0001!=X525|skolem0002!=X526|human_person(X525,X526),inference(resolution,[status(thm)],[c271, c2])).
% 2.26/2.51 cnf(c631,plain,skolem0001!=X527|human_person(X527,skolem0002),inference(resolution,[status(thm)],[c273, reflexivity])).
% 2.26/2.51 fof(ax9,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 2.26/2.51 fof(c217,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 2.26/2.51 fof(c218,plain,(![X111]:(![X112]:(~object(X111,X112)|unisex(X111,X112)))),inference(variable_rename,[status(thm)],[c217])).
% 2.26/2.51 cnf(c219,plain,~object(X246,X247)|unisex(X246,X247),inference(split_conjunct,[status(thm)],[c218])).
% 2.26/2.51 cnf(c270,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c219, c258])).
% 2.26/2.51 cnf(c272,plain,skolem0001!=X515|skolem0003!=X514|unisex(X515,X514),inference(resolution,[status(thm)],[c10, c270])).
% 2.26/2.51 cnf(c618,plain,skolem0001!=X524|unisex(X524,skolem0003),inference(resolution,[status(thm)],[c272, reflexivity])).
% 2.26/2.51 cnf(c103,plain,~member(X519,X520,X517)|~member(X519,X521,X517)|X521=X520|~member(X519,X518,X517)|X518=X521|X518=X520|~member(X519,X522,X517)|X522=X518|X522=X521|X522=X520|~member(X519,X523,X517)|X523=X522|X523=X518|X523=X521|X523=X520|~member(X519,X516,X517)|X516=X523|X516=X522|X516=X518|X516=X521|X516=X520|member(X519,skolem0014(X519,X517,X520,X521,X518,X522,X523,X516),X517)|six(X519,X517),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 fof(ax10,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 2.26/2.52 fof(c214,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 2.26/2.52 fof(c215,plain,(![X109]:(![X110]:(~object(X109,X110)|impartial(X109,X110)))),inference(variable_rename,[status(thm)],[c214])).
% 2.26/2.52 cnf(c216,plain,~object(X245,X244)|impartial(X245,X244),inference(split_conjunct,[status(thm)],[c215])).
% 2.26/2.52 cnf(c268,plain,impartial(skolem0001,skolem0003),inference(resolution,[status(thm)],[c216, c258])).
% 2.26/2.52 cnf(c269,plain,skolem0001!=X511|skolem0003!=X512|impartial(X511,X512),inference(resolution,[status(thm)],[c268, c7])).
% 2.26/2.52 cnf(c616,plain,skolem0001!=X513|impartial(X513,skolem0003),inference(resolution,[status(thm)],[c269, reflexivity])).
% 2.26/2.52 cnf(c102,plain,~six(X510,X509)|~member(X510,X508,X509)|X508=skolem0013(X510,X509)|X508=skolem0012(X510,X509)|X508=skolem0011(X510,X509)|X508=skolem0010(X510,X509)|X508=skolem0009(X510,X509)|X508=skolem0008(X510,X509),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c9,axiom,X243!=X242|X241!=X240|~object(X243,X241)|object(X242,X240),theory(equality)).
% 2.26/2.52 cnf(c267,plain,skolem0001!=X505|skolem0003!=X506|object(X505,X506),inference(resolution,[status(thm)],[c9, c258])).
% 2.26/2.52 cnf(c608,plain,skolem0001!=X507|object(X507,skolem0003),inference(resolution,[status(thm)],[c267, reflexivity])).
% 2.26/2.52 cnf(c263,plain,skolem0001!=X503|skolem0003!=X502|entity(X503,X502),inference(resolution,[status(thm)],[c8, c259])).
% 2.26/2.52 cnf(c606,plain,skolem0001!=X504|entity(X504,skolem0003),inference(resolution,[status(thm)],[c263, reflexivity])).
% 2.26/2.52 cnf(c51,negated_conjecture,male(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.52 cnf(c1,axiom,X163!=X162|X161!=X160|~male(X163,X161)|male(X162,X160),theory(equality)).
% 2.26/2.52 cnf(c249,plain,skolem0001!=X495|skolem0002!=X496|male(X495,X496),inference(resolution,[status(thm)],[c1, c51])).
% 2.26/2.52 cnf(c604,plain,skolem0001!=X497|male(X497,skolem0002),inference(resolution,[status(thm)],[c249, reflexivity])).
% 2.26/2.52 cnf(c0,axiom,X149!=X148|X147!=X146|~man(X149,X147)|man(X148,X146),theory(equality)).
% 2.26/2.52 cnf(c248,plain,skolem0001!=X485|skolem0002!=X484|man(X485,X484),inference(resolution,[status(thm)],[c0, c52])).
% 2.26/2.52 cnf(c602,plain,skolem0001!=X494|man(X494,skolem0002),inference(resolution,[status(thm)],[c248, reflexivity])).
% 2.26/2.52 cnf(c68,negated_conjecture,~actual_world(X490)|~male(X490,X487)|~male(X490,X489)|~man(X490,X489)|~of(X490,X488,X489)|~cannon(X490,X488)|~event(X490,X486)|~agent(X490,X486,X489)|~patient(X490,X486,skolem0006(X490,X489,X488,X487,X493,X492,X491))|~present(X490,X486)|~nonreflexive(X490,X486)|~fire(X490,X486)|~from_loc(X490,X486,X488)|~six(X490,X487)|~group(X490,X487)|~shot(X490,skolem0007(X490,X489,X488,X487,X493,X492,X491))|~cry(X490,X493)|~revenge(X490,X492)|~event(X490,X491)|~agent(X490,X491,X487)|~patient(X490,X491,X493)|~present(X490,X491)|~nonreflexive(X490,X491)|~scream(X490,X491)|~of(X490,X491,X492),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.52 cnf(c101,plain,~six(X483,X482)|skolem0013(X483,X482)!=skolem0008(X483,X482),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c100,plain,~six(X481,X480)|skolem0013(X481,X480)!=skolem0009(X481,X480),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c99,plain,~six(X479,X478)|skolem0013(X479,X478)!=skolem0010(X479,X478),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c98,plain,~six(X477,X476)|skolem0013(X477,X476)!=skolem0011(X477,X476),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c67,negated_conjecture,~actual_world(X472)|~male(X472,X469)|~male(X472,X471)|~man(X472,X471)|~of(X472,X470,X471)|~cannon(X472,X470)|~event(X472,X468)|~agent(X472,X468,X471)|~patient(X472,X468,skolem0006(X472,X471,X470,X469,X475,X474,X473))|~present(X472,X468)|~nonreflexive(X472,X468)|~fire(X472,X468)|~from_loc(X472,X468,X470)|~six(X472,X469)|~group(X472,X469)|member(X472,skolem0007(X472,X471,X470,X469,X475,X474,X473),X469)|~cry(X472,X475)|~revenge(X472,X474)|~event(X472,X473)|~agent(X472,X473,X469)|~patient(X472,X473,X475)|~present(X472,X473)|~nonreflexive(X472,X473)|~scream(X472,X473)|~of(X472,X473,X474),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.52 cnf(c97,plain,~six(X467,X466)|skolem0013(X467,X466)!=skolem0012(X467,X466),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c95,plain,~six(X465,X464)|skolem0012(X465,X464)!=skolem0008(X465,X464),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c94,plain,~six(X463,X462)|skolem0012(X463,X462)!=skolem0009(X463,X462),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c93,plain,~six(X461,X460)|skolem0012(X461,X460)!=skolem0010(X461,X460),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c92,plain,~six(X459,X458)|skolem0012(X459,X458)!=skolem0011(X459,X458),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c66,negated_conjecture,~actual_world(X454)|~male(X454,X451)|~male(X454,X453)|~man(X454,X453)|~of(X454,X452,X453)|~cannon(X454,X452)|member(X454,skolem0006(X454,X453,X452,X451,X457,X456,X455),X451)|~six(X454,X451)|~group(X454,X451)|~shot(X454,skolem0007(X454,X453,X452,X451,X457,X456,X455))|~cry(X454,X457)|~revenge(X454,X456)|~event(X454,X455)|~agent(X454,X455,X451)|~patient(X454,X455,X457)|~present(X454,X455)|~nonreflexive(X454,X455)|~scream(X454,X455)|~of(X454,X455,X456),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.52 cnf(c90,plain,~six(X450,X449)|skolem0011(X450,X449)!=skolem0008(X450,X449),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c89,plain,~six(X448,X447)|skolem0011(X448,X447)!=skolem0009(X448,X447),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c88,plain,~six(X446,X445)|skolem0011(X446,X445)!=skolem0010(X446,X445),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c86,plain,~six(X444,X443)|skolem0010(X444,X443)!=skolem0008(X444,X443),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c85,plain,~six(X442,X441)|skolem0010(X442,X441)!=skolem0009(X442,X441),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 cnf(c83,plain,~six(X433,X432)|skolem0009(X433,X432)!=skolem0008(X433,X432),inference(split_conjunct,[status(thm)],[c80])).
% 2.26/2.52 fof(ax40,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 2.26/2.52 fof(c122,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax40])).
% 2.26/2.52 fof(c123,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c122])).
% 2.26/2.52 fof(c124,plain,(![X49]:(![X50]:(~existent(X49,X50)|~nonexistent(X49,X50)))),inference(variable_rename,[status(thm)],[c123])).
% 2.26/2.52 cnf(c125,plain,~existent(X145,X144)|~nonexistent(X145,X144),inference(split_conjunct,[status(thm)],[c124])).
% 2.26/2.52 cnf(c529,plain,~existent(skolem0001,skolem0005(skolem0011(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c480, c125])).
% 2.26/2.52 cnf(c523,plain,~existent(skolem0001,skolem0005(skolem0013(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c469, c125])).
% 2.26/2.52 cnf(c511,plain,~existent(skolem0001,skolem0005(skolem0008(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c464, c125])).
% 2.26/2.52 cnf(c505,plain,~existent(skolem0001,skolem0005(skolem0012(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c459, c125])).
% 2.26/2.52 cnf(c499,plain,~existent(skolem0001,skolem0005(skolem0010(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c454, c125])).
% 2.26/2.52 cnf(c485,plain,~existent(skolem0001,skolem0005(skolem0009(skolem0001,skolem0004))),inference(resolution,[status(thm)],[c449, c125])).
% 2.26/2.52 cnf(c35,axiom,X387!=X386|X385!=X384|~sound(X387,X385)|sound(X386,X384),theory(equality)).
% 2.26/2.52 cnf(c31,axiom,X371!=X370|X369!=X368|~scream(X371,X369)|scream(X370,X368),theory(equality)).
% 2.26/2.52 cnf(c422,plain,~existent(skolem0001,skolem0013(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c417, c125])).
% 2.26/2.52 cnf(c30,axiom,X366!=X365|X364!=X363|~cry(X366,X364)|cry(X365,X363),theory(equality)).
% 2.26/2.52 cnf(c29,axiom,X362!=X361|X360!=X359|~revenge(X362,X360)|revenge(X361,X359),theory(equality)).
% 2.26/2.52 cnf(c399,plain,~existent(skolem0001,skolem0012(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c389, c125])).
% 2.26/2.52 cnf(c374,plain,~existent(skolem0001,skolem0011(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c368, c125])).
% 2.26/2.52 cnf(c356,plain,~existent(skolem0001,skolem0010(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c351, c125])).
% 2.26/2.52 cnf(c338,plain,~existent(skolem0001,skolem0009(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c333, c125])).
% 2.26/2.52 cnf(c323,plain,~existent(skolem0001,skolem0008(skolem0001,skolem0004)),inference(resolution,[status(thm)],[c317, c125])).
% 2.26/2.52 cnf(c40,axiom,X288!=X287|~actual_world(X288)|actual_world(X287),theory(equality)).
% 2.26/2.52 fof(ax1,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 2.26/2.52 fof(c241,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 2.26/2.52 fof(c242,plain,(![X127]:(![X128]:(~man(X127,X128)|male(X127,X128)))),inference(variable_rename,[status(thm)],[c241])).
% 2.26/2.52 cnf(c243,plain,~man(X278,X279)|male(X278,X279),inference(split_conjunct,[status(thm)],[c242])).
% 2.26/2.52 fof(ax41,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 2.26/2.52 fof(c118,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax41])).
% 2.26/2.52 fof(c119,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c118])).
% 2.26/2.52 fof(c120,plain,(![X47]:(![X48]:(~nonliving(X47,X48)|~living(X47,X48)))),inference(variable_rename,[status(thm)],[c119])).
% 2.26/2.52 cnf(c121,plain,~nonliving(X143,X142)|~living(X143,X142),inference(split_conjunct,[status(thm)],[c120])).
% 2.26/2.52 cnf(c288,plain,~nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c287, c121])).
% 2.26/2.52 fof(ax39,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 2.26/2.52 fof(c126,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax39])).
% 2.26/2.52 fof(c127,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c126])).
% 2.26/2.52 fof(c128,plain,(![X51]:(![X52]:(~animate(X51,X52)|~nonliving(X51,X52)))),inference(variable_rename,[status(thm)],[c127])).
% 2.26/2.52 cnf(c129,plain,~animate(X151,X150)|~nonliving(X151,X150),inference(split_conjunct,[status(thm)],[c128])).
% 2.26/2.52 cnf(c266,plain,~animate(skolem0001,skolem0003),inference(resolution,[status(thm)],[c265, c129])).
% 2.26/2.52 fof(ax21,axiom,(![U]:(![V]:(fire(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 2.26/2.52 fof(c181,plain,(![U]:(![V]:(~fire(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 2.26/2.52 fof(c182,plain,(![X87]:(![X88]:(~fire(X87,X88)|event(X87,X88)))),inference(variable_rename,[status(thm)],[c181])).
% 2.26/2.52 cnf(c183,plain,~fire(X203,X202)|event(X203,X202),inference(split_conjunct,[status(thm)],[c182])).
% 2.26/2.52 fof(ax22,axiom,(![U]:(![V]:(six(U,V)=>group(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 2.26/2.52 fof(c178,plain,(![U]:(![V]:(~six(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 2.26/2.52 fof(c179,plain,(![X85]:(![X86]:(~six(X85,X86)|group(X85,X86)))),inference(variable_rename,[status(thm)],[c178])).
% 2.26/2.52 cnf(c180,plain,~six(X201,X200)|group(X201,X200),inference(split_conjunct,[status(thm)],[c179])).
% 2.26/2.52 fof(ax42,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 2.26/2.52 fof(c114,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax42])).
% 2.26/2.52 fof(c115,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c114])).
% 2.26/2.52 fof(c116,plain,(![X45]:(![X46]:(~singleton(X45,X46)|~multiple(X45,X46)))),inference(variable_rename,[status(thm)],[c115])).
% 2.26/2.52 cnf(c117,plain,~singleton(X141,X140)|~multiple(X141,X140),inference(split_conjunct,[status(thm)],[c116])).
% 2.26/2.52 cnf(c252,plain,~singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c251, c117])).
% 2.26/2.52 fof(ax28,axiom,(![U]:(![V]:(revenge(U,V)=>action(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 2.26/2.52 fof(c160,plain,(![U]:(![V]:(~revenge(U,V)|action(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 2.26/2.52 fof(c161,plain,(![X73]:(![X74]:(~revenge(X73,X74)|action(X73,X74)))),inference(variable_rename,[status(thm)],[c160])).
% 2.26/2.52 cnf(c162,plain,~revenge(X180,X181)|action(X180,X181),inference(split_conjunct,[status(thm)],[c161])).
% 2.26/2.52 fof(ax29,axiom,(![U]:(![V]:(cry(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 2.26/2.52 fof(c157,plain,(![U]:(![V]:(~cry(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 2.26/2.52 fof(c158,plain,(![X71]:(![X72]:(~cry(X71,X72)|event(X71,X72)))),inference(variable_rename,[status(thm)],[c157])).
% 2.26/2.52 cnf(c159,plain,~cry(X178,X179)|event(X178,X179),inference(split_conjunct,[status(thm)],[c158])).
% 2.26/2.52 fof(ax30,axiom,(![U]:(![V]:(scream(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 2.26/2.52 fof(c154,plain,(![U]:(![V]:(~scream(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 2.26/2.52 fof(c155,plain,(![X69]:(![X70]:(~scream(X69,X70)|event(X69,X70)))),inference(variable_rename,[status(thm)],[c154])).
% 2.26/2.52 cnf(c156,plain,~scream(X172,X173)|event(X172,X173),inference(split_conjunct,[status(thm)],[c155])).
% 2.26/2.52 fof(ax37,axiom,(![U]:(![V]:(sound(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 2.26/2.52 fof(c133,plain,(![U]:(![V]:(~sound(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax37])).
% 2.26/2.52 fof(c134,plain,(![X55]:(![X56]:(~sound(X55,X56)|event(X55,X56)))),inference(variable_rename,[status(thm)],[c133])).
% 2.26/2.52 cnf(c135,plain,~sound(X154,X155)|event(X154,X155),inference(split_conjunct,[status(thm)],[c134])).
% 2.26/2.52 fof(ax38,axiom,(![U]:(![V]:(scream(U,V)=>sound(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 2.26/2.52 fof(c130,plain,(![U]:(![V]:(~scream(U,V)|sound(U,V)))),inference(fof_nnf,[status(thm)],[ax38])).
% 2.26/2.52 fof(c131,plain,(![X53]:(![X54]:(~scream(X53,X54)|sound(X53,X54)))),inference(variable_rename,[status(thm)],[c130])).
% 2.26/2.52 cnf(c132,plain,~scream(X152,X153)|sound(X152,X153),inference(split_conjunct,[status(thm)],[c131])).
% 2.26/2.52 fof(ax43,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax43)).
% 2.26/2.52 fof(c110,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax43])).
% 2.26/2.52 fof(c111,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c110])).
% 2.26/2.52 fof(c112,plain,(![X43]:(![X44]:(~unisex(X43,X44)|~male(X43,X44)))),inference(variable_rename,[status(thm)],[c111])).
% 2.26/2.52 cnf(c113,plain,~unisex(X139,X138)|~male(X139,X138),inference(split_conjunct,[status(thm)],[c112])).
% 2.26/2.52 cnf(c247,plain,~unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c113, c51])).
% 2.26/2.52 cnf(transitivity,axiom,X137!=X135|X135!=X136|X137=X136,theory(equality)).
% 2.26/2.52 cnf(symmetry,axiom,X133!=X132|X132=X133,theory(equality)).
% 2.26/2.52 fof(ax45,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax45)).
% 2.26/2.52 fof(c72,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax45])).
% 2.26/2.52 fof(c73,plain,(![X23]:(![X24]:~member(X23,X24,X24))),inference(variable_rename,[status(thm)],[c72])).
% 2.26/2.52 cnf(c74,plain,~member(X130,X131,X131),inference(split_conjunct,[status(thm)],[c73])).
% 2.26/2.52 cnf(c50,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c49])).
% 2.26/2.52 % SZS output end Saturation
% 2.26/2.52
% 2.26/2.52 % Initial clauses : 140
% 2.26/2.52 % Processed clauses : 735
% 2.26/2.52 % Factors computed : 7
% 2.26/2.52 % Resolvents computed: 793
% 2.26/2.52 % Tautologies deleted: 3
% 2.26/2.52 % Forward subsumed : 202
% 2.26/2.52 % Backward subsumed : 6
% 2.26/2.52 % -------- CPU Time ---------
% 2.26/2.52 % User time : 2.136 s
% 2.26/2.52 % System time : 0.017 s
% 2.26/2.52 % Total time : 2.153 s
%------------------------------------------------------------------------------