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