PyRes---1.5.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : NLP220+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n007.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:40 EDT 2024

% Result   : CounterSatisfiable 0.88s 1.12s
% Output   : Saturation 0.96s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP220+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33  % Computer : n007.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 300
% 0.13/0.33  % DateTime : Wed May  8 13:36:37 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 0.88/1.12  % Version:  1.5
% 0.88/1.12  % SZS status CounterSatisfiable
% 0.88/1.12  % SZS output start Saturation
% 0.88/1.12  fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![Z]:(man(Y,Z)=>(?[X1]:(((event(Y,X1)&agent(Y,X1,Z))&present(Y,X1))&smoke(Y,X1))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.88/1.12  fof(c33,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![Z]:(man(Y,Z)=>(?[X1]:(((event(Y,X1)&agent(Y,X1,Z))&present(Y,X1))&smoke(Y,X1)))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.88/1.12  fof(c34,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((of(U,W,V)&man(U,V))&vincent_forename(U,W))&forename(U,W))&proposition(U,Y))&agent(U,X,V))&theme(U,X,Y))&event(U,X))&present(U,X))&think_believe_consider(U,X))&accessible_world(U,Y))&(![Z]:(~man(Y,Z)|(?[X1]:(((event(Y,X1)&agent(Y,X1,Z))&present(Y,X1))&smoke(Y,X1)))))))))))),inference(fof_nnf,[status(thm)],[c33])).
% 0.88/1.12  fof(c35,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((of(X2,X4,X3)&man(X2,X3))&vincent_forename(X2,X4))&forename(X2,X4))&proposition(X2,X6))&agent(X2,X5,X3))&theme(X2,X5,X6))&event(X2,X5))&present(X2,X5))&think_believe_consider(X2,X5))&accessible_world(X2,X6))&(![X7]:(~man(X6,X7)|(?[X8]:(((event(X6,X8)&agent(X6,X8,X7))&present(X6,X8))&smoke(X6,X8)))))))))))),inference(variable_rename,[status(thm)],[c34])).
% 0.88/1.12  fof(c37,negated_conjecture,(![X7]:(actual_world(skolem0001)&(((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&(~man(skolem0005,X7)|(((event(skolem0005,skolem0006(X7))&agent(skolem0005,skolem0006(X7),X7))&present(skolem0005,skolem0006(X7)))&smoke(skolem0005,skolem0006(X7))))))),inference(shift_quantors,[status(thm)],[fof(c36,negated_conjecture,(actual_world(skolem0001)&(((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&(![X7]:(~man(skolem0005,X7)|(((event(skolem0005,skolem0006(X7))&agent(skolem0005,skolem0006(X7),X7))&present(skolem0005,skolem0006(X7)))&smoke(skolem0005,skolem0006(X7))))))),inference(skolemize,[status(esa)],[c35])).])).
% 0.88/1.12  fof(c38,negated_conjecture,(![X7]:(actual_world(skolem0001)&(((((((((((of(skolem0001,skolem0003,skolem0002)&man(skolem0001,skolem0002))&vincent_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&proposition(skolem0001,skolem0005))&agent(skolem0001,skolem0004,skolem0002))&theme(skolem0001,skolem0004,skolem0005))&event(skolem0001,skolem0004))&present(skolem0001,skolem0004))&think_believe_consider(skolem0001,skolem0004))&accessible_world(skolem0001,skolem0005))&((((~man(skolem0005,X7)|event(skolem0005,skolem0006(X7)))&(~man(skolem0005,X7)|agent(skolem0005,skolem0006(X7),X7)))&(~man(skolem0005,X7)|present(skolem0005,skolem0006(X7))))&(~man(skolem0005,X7)|smoke(skolem0005,skolem0006(X7))))))),inference(distribute,[status(thm)],[c37])).
% 0.88/1.12  cnf(c50,negated_conjecture,accessible_world(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.12  cnf(c41,negated_conjecture,man(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.12  fof(ax52,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&man(V,U))=>man(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax52)).
% 0.88/1.12  fof(c92,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~man(V,U))|man(W,U))))),inference(fof_nnf,[status(thm)],[ax52])).
% 0.88/1.12  fof(c93,plain,(![X50]:(![X51]:(![X52]:((~accessible_world(X51,X52)|~man(X51,X50))|man(X52,X50))))),inference(variable_rename,[status(thm)],[c92])).
% 0.88/1.12  cnf(c94,plain,~accessible_world(X441,X442)|~man(X441,X440)|man(X442,X440),inference(split_conjunct,[status(thm)],[c93])).
% 0.88/1.12  cnf(c414,plain,~accessible_world(skolem0001,X443)|man(X443,skolem0002),inference(resolution,[status(thm)],[c94, c41])).
% 0.88/1.12  cnf(c415,plain,man(skolem0005,skolem0002),inference(resolution,[status(thm)],[c414, c50])).
% 0.88/1.12  cnf(c52,negated_conjecture,~man(skolem0005,X454)|agent(skolem0005,skolem0006(X454),X454),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.12  cnf(c445,plain,agent(skolem0005,skolem0006(skolem0002),skolem0002),inference(resolution,[status(thm)],[c52, c415])).
% 0.88/1.12  cnf(c46,negated_conjecture,theme(skolem0001,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.12  fof(ax41,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&theme(W,U,V))=>theme(X,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax41)).
% 0.88/1.12  fof(c125,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~theme(W,U,V))|theme(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax41])).
% 0.88/1.12  fof(c126,plain,(![X83]:(![X84]:(![X85]:(![X86]:((~accessible_world(X85,X86)|~theme(X85,X83,X84))|theme(X86,X83,X84)))))),inference(variable_rename,[status(thm)],[c125])).
% 0.88/1.12  cnf(c127,plain,~accessible_world(X523,X524)|~theme(X523,X525,X526)|theme(X524,X525,X526),inference(split_conjunct,[status(thm)],[c126])).
% 0.88/1.12  cnf(c513,plain,~accessible_world(skolem0001,X607)|theme(X607,skolem0004,skolem0005),inference(resolution,[status(thm)],[c127, c46])).
% 0.88/1.12  cnf(c596,plain,theme(skolem0005,skolem0004,skolem0005),inference(resolution,[status(thm)],[c513, c50])).
% 0.88/1.12  fof(ax64,axiom,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:((((((((think_believe_consider(U,V)&proposition(U,Y))&theme(U,V,Y))&agent(U,V,X))&think_believe_consider(U,W))&proposition(U,Z))&theme(U,W,Z))&agent(U,W,X))=>Y=Z))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax64)).
% 0.88/1.12  fof(c55,plain,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:((((((((~think_believe_consider(U,V)|~proposition(U,Y))|~theme(U,V,Y))|~agent(U,V,X))|~think_believe_consider(U,W))|~proposition(U,Z))|~theme(U,W,Z))|~agent(U,W,X))|Y=Z))))))),inference(fof_nnf,[status(thm)],[ax64])).
% 0.88/1.12  fof(c56,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((((((((~think_believe_consider(X9,X10)|~proposition(X9,X13))|~theme(X9,X10,X13))|~agent(X9,X10,X12))|~think_believe_consider(X9,X11))|~proposition(X9,X14))|~theme(X9,X11,X14))|~agent(X9,X11,X12))|X13=X14))))))),inference(variable_rename,[status(thm)],[c55])).
% 0.88/1.12  cnf(c57,plain,~think_believe_consider(X459,X457)|~proposition(X459,X458)|~theme(X459,X457,X458)|~agent(X459,X457,X455)|~think_believe_consider(X459,X460)|~proposition(X459,X456)|~theme(X459,X460,X456)|~agent(X459,X460,X455)|X458=X456,inference(split_conjunct,[status(thm)],[c56])).
% 0.88/1.12  cnf(c45,negated_conjecture,agent(skolem0001,skolem0004,skolem0002),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.12  fof(ax53,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&agent(W,U,V))=>agent(X,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax53)).
% 0.88/1.12  fof(c89,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~agent(W,U,V))|agent(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax53])).
% 0.88/1.12  fof(c90,plain,(![X46]:(![X47]:(![X48]:(![X49]:((~accessible_world(X48,X49)|~agent(X48,X46,X47))|agent(X49,X46,X47)))))),inference(variable_rename,[status(thm)],[c89])).
% 0.88/1.12  cnf(c91,plain,~accessible_world(X469,X467)|~agent(X469,X466,X468)|agent(X467,X466,X468),inference(split_conjunct,[status(thm)],[c90])).
% 0.88/1.12  cnf(c480,plain,~accessible_world(skolem0001,X603)|agent(X603,skolem0004,skolem0002),inference(resolution,[status(thm)],[c91, c45])).
% 0.88/1.12  cnf(c590,plain,agent(skolem0005,skolem0004,skolem0002),inference(resolution,[status(thm)],[c480, c50])).
% 0.88/1.12  cnf(c592,plain,~think_believe_consider(skolem0005,X915)|~proposition(skolem0005,X916)|~theme(skolem0005,X915,X916)|~agent(skolem0005,X915,skolem0002)|~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,X914)|~theme(skolem0005,skolem0004,X914)|X916=X914,inference(resolution,[status(thm)],[c590, c57])).
% 0.88/1.12  cnf(c807,plain,~think_believe_consider(skolem0005,X950)|~proposition(skolem0005,X951)|~theme(skolem0005,X950,X951)|~agent(skolem0005,X950,skolem0002)|~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,skolem0005)|X951=skolem0005,inference(resolution,[status(thm)],[c592, c596])).
% 0.88/1.12  cnf(c824,plain,~think_believe_consider(skolem0005,skolem0006(skolem0002))|~proposition(skolem0005,X953)|~theme(skolem0005,skolem0006(skolem0002),X953)|~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,skolem0005)|X953=skolem0005,inference(resolution,[status(thm)],[c807, c445])).
% 0.88/1.12  cnf(c456,plain,~think_believe_consider(skolem0001,X837)|~proposition(skolem0001,X838)|~theme(skolem0001,X837,X838)|~agent(skolem0001,X837,skolem0002)|~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,X836)|~theme(skolem0001,skolem0004,X836)|X838=X836,inference(resolution,[status(thm)],[c57, c45])).
% 0.88/1.12  cnf(c757,plain,~think_believe_consider(skolem0001,X946)|~proposition(skolem0001,X947)|~theme(skolem0001,X946,X947)|~agent(skolem0001,X946,skolem0002)|~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,skolem0005)|X947=skolem0005,inference(resolution,[status(thm)],[c456, c46])).
% 0.88/1.12  cnf(c455,plain,~think_believe_consider(X827,X831)|~proposition(X827,X828)|~theme(X827,X831,X828)|~agent(X827,X831,X830)|~proposition(X827,X829)|~theme(X827,X831,X829)|X828=X829,inference(factor,[status(thm)],[c57])).
% 0.88/1.12  cnf(c751,plain,~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,X944)|~theme(skolem0005,skolem0004,X944)|~agent(skolem0005,skolem0004,X943)|~proposition(skolem0005,skolem0005)|X944=skolem0005,inference(resolution,[status(thm)],[c455, c596])).
% 0.88/1.12  cnf(c821,plain,~think_believe_consider(skolem0005,skolem0004)|~proposition(skolem0005,X945)|~theme(skolem0005,skolem0004,X945)|~proposition(skolem0005,skolem0005)|X945=skolem0005,inference(resolution,[status(thm)],[c751, c590])).
% 0.88/1.12  cnf(c750,plain,~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,X940)|~theme(skolem0001,skolem0004,X940)|~agent(skolem0001,skolem0004,X939)|~proposition(skolem0001,skolem0005)|X940=skolem0005,inference(resolution,[status(thm)],[c455, c46])).
% 0.88/1.12  cnf(c819,plain,~think_believe_consider(skolem0001,skolem0004)|~proposition(skolem0001,X941)|~theme(skolem0001,skolem0004,X941)|~proposition(skolem0001,skolem0005)|X941=skolem0005,inference(resolution,[status(thm)],[c750, c45])).
% 0.88/1.12  cnf(reflexivity,axiom,X177=X177,theory(equality)).
% 0.88/1.12  cnf(c26,axiom,X406!=X410|X408!=X405|X409!=X407|~of(X406,X408,X409)|of(X410,X405,X407),theory(equality)).
% 0.88/1.12  cnf(c40,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.12  fof(ax32,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&of(W,U,V))=>of(X,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax32)).
% 0.88/1.12  fof(c152,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~of(W,U,V))|of(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.88/1.12  fof(c153,plain,(![X111]:(![X112]:(![X113]:(![X114]:((~accessible_world(X113,X114)|~of(X113,X111,X112))|of(X114,X111,X112)))))),inference(variable_rename,[status(thm)],[c152])).
% 0.88/1.12  cnf(c154,plain,~accessible_world(X569,X568)|~of(X569,X566,X567)|of(X568,X566,X567),inference(split_conjunct,[status(thm)],[c153])).
% 0.88/1.12  cnf(c565,plain,~accessible_world(skolem0001,X608)|of(X608,skolem0003,skolem0002),inference(resolution,[status(thm)],[c154, c40])).
% 0.88/1.12  cnf(c599,plain,of(skolem0005,skolem0003,skolem0002),inference(resolution,[status(thm)],[c565, c50])).
% 0.88/1.12  cnf(c601,plain,skolem0005!=X925|skolem0003!=X926|skolem0002!=X924|of(X925,X926,X924),inference(resolution,[status(thm)],[c599, c26])).
% 0.88/1.12  cnf(c813,plain,skolem0005!=X931|skolem0003!=X930|of(X931,X930,skolem0002),inference(resolution,[status(thm)],[c601, reflexivity])).
% 0.88/1.12  cnf(c816,plain,skolem0005!=X933|of(X933,skolem0003,skolem0002),inference(resolution,[status(thm)],[c813, reflexivity])).
% 0.88/1.12  fof(ax63,axiom,(![U]:(![V]:(![W]:(((entity(U,V)&forename(U,W))&of(U,W,V))=>(~(?[X]:((forename(U,X)&X!=W)&of(U,X,V)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax63)).
% 0.88/1.12  fof(c58,plain,(![U]:(![V]:(![W]:(((~entity(U,V)|~forename(U,W))|~of(U,W,V))|(![X]:((~forename(U,X)|X=W)|~of(U,X,V))))))),inference(fof_nnf,[status(thm)],[ax63])).
% 0.88/1.12  fof(c60,plain,(![X15]:(![X16]:(![X17]:(![X18]:(((~entity(X15,X16)|~forename(X15,X17))|~of(X15,X17,X16))|((~forename(X15,X18)|X18=X17)|~of(X15,X18,X16))))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,(![X15]:(![X16]:(![X17]:(((~entity(X15,X16)|~forename(X15,X17))|~of(X15,X17,X16))|(![X18]:((~forename(X15,X18)|X18=X17)|~of(X15,X18,X16))))))),inference(variable_rename,[status(thm)],[c58])).])).
% 0.88/1.12  cnf(c61,plain,~entity(X463,X462)|~forename(X463,X464)|~of(X463,X464,X462)|~forename(X463,X461)|X461=X464|~of(X463,X461,X462),inference(split_conjunct,[status(thm)],[c60])).
% 0.88/1.12  cnf(c603,plain,~entity(skolem0005,skolem0002)|~forename(skolem0005,X932)|~of(skolem0005,X932,skolem0002)|~forename(skolem0005,skolem0003)|skolem0003=X932,inference(resolution,[status(thm)],[c599, c61])).
% 0.88/1.12  cnf(c28,axiom,X424!=X428|X426!=X423|X427!=X425|~theme(X424,X426,X427)|theme(X428,X423,X425),theory(equality)).
% 0.88/1.12  cnf(c598,plain,skolem0005!=X918|skolem0004!=X920|skolem0005!=X919|theme(X918,X920,X919),inference(resolution,[status(thm)],[c596, c28])).
% 0.88/1.12  cnf(c810,plain,skolem0005!=X927|skolem0004!=X928|theme(X927,X928,skolem0005),inference(resolution,[status(thm)],[c598, reflexivity])).
% 0.88/1.12  cnf(c814,plain,skolem0005!=X929|theme(X929,skolem0004,skolem0005),inference(resolution,[status(thm)],[c810, reflexivity])).
% 0.88/1.12  cnf(c809,plain,skolem0005!=X922|skolem0004!=X921|theme(X922,X921,X922),inference(factor,[status(thm)],[c598])).
% 0.88/1.12  cnf(c811,plain,skolem0005!=X923|theme(X923,skolem0004,X923),inference(resolution,[status(thm)],[c809, reflexivity])).
% 0.88/1.12  cnf(c30,axiom,X445!=X449|X447!=X444|X448!=X446|~agent(X445,X447,X448)|agent(X449,X444,X446),theory(equality)).
% 0.88/1.12  cnf(c477,plain,skolem0005!=X892|skolem0006(skolem0002)!=X891|skolem0002!=X893|agent(X892,X891,X893),inference(resolution,[status(thm)],[c445, c30])).
% 0.88/1.12  cnf(c794,plain,skolem0005!=X912|skolem0002!=X913|agent(X912,skolem0006(skolem0002),X913),inference(resolution,[status(thm)],[c477, reflexivity])).
% 0.88/1.12  cnf(c805,plain,skolem0005!=X917|agent(X917,skolem0006(skolem0002),skolem0002),inference(resolution,[status(thm)],[c794, reflexivity])).
% 0.88/1.12  cnf(c591,plain,skolem0005!=X907|skolem0004!=X906|skolem0002!=X908|agent(X907,X906,X908),inference(resolution,[status(thm)],[c590, c30])).
% 0.88/1.12  cnf(c802,plain,skolem0005!=X910|skolem0004!=X909|agent(X910,X909,skolem0002),inference(resolution,[status(thm)],[c591, reflexivity])).
% 0.88/1.12  cnf(c803,plain,skolem0005!=X911|agent(X911,skolem0004,skolem0002),inference(resolution,[status(thm)],[c802, reflexivity])).
% 0.88/1.12  cnf(c425,plain,skolem0001!=X778|skolem0004!=X777|skolem0002!=X779|agent(X778,X777,X779),inference(resolution,[status(thm)],[c30, c45])).
% 0.88/1.12  cnf(c715,plain,skolem0001!=X903|skolem0004!=X904|agent(X903,X904,skolem0002),inference(resolution,[status(thm)],[c425, reflexivity])).
% 0.88/1.12  cnf(c800,plain,skolem0001!=X905|agent(X905,skolem0004,skolem0002),inference(resolution,[status(thm)],[c715, reflexivity])).
% 0.88/1.12  cnf(c409,plain,skolem0001!=X764|skolem0004!=X766|skolem0005!=X765|theme(X764,X766,X765),inference(resolution,[status(thm)],[c28, c46])).
% 0.88/1.12  cnf(c707,plain,skolem0001!=X898|skolem0004!=X897|theme(X898,X897,skolem0005),inference(resolution,[status(thm)],[c409, reflexivity])).
% 0.88/1.12  cnf(c797,plain,skolem0001!=X902|theme(X902,skolem0004,skolem0005),inference(resolution,[status(thm)],[c707, reflexivity])).
% 0.88/1.12  cnf(c478,plain,~think_believe_consider(skolem0005,X900)|~proposition(skolem0005,X901)|~theme(skolem0005,X900,X901)|~agent(skolem0005,X900,skolem0002)|~think_believe_consider(skolem0005,skolem0006(skolem0002))|~proposition(skolem0005,X899)|~theme(skolem0005,skolem0006(skolem0002),X899)|X901=X899,inference(resolution,[status(thm)],[c445, c57])).
% 0.88/1.12  cnf(c396,plain,skolem0001!=X752|skolem0003!=X753|skolem0002!=X751|of(X752,X753,X751),inference(resolution,[status(thm)],[c26, c40])).
% 0.88/1.13  cnf(c698,plain,skolem0001!=X895|skolem0003!=X894|of(X895,X894,skolem0002),inference(resolution,[status(thm)],[c396, reflexivity])).
% 0.88/1.13  cnf(c795,plain,skolem0001!=X896|of(X896,skolem0003,skolem0002),inference(resolution,[status(thm)],[c698, reflexivity])).
% 0.88/1.13  cnf(c0,axiom,X188!=X186|X189!=X187|~vincent_forename(X188,X189)|vincent_forename(X186,X187),theory(equality)).
% 0.88/1.13  cnf(c42,negated_conjecture,vincent_forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.13  fof(ax33,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&vincent_forename(V,U))=>vincent_forename(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax33)).
% 0.88/1.13  fof(c149,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~vincent_forename(V,U))|vincent_forename(W,U))))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.88/1.13  fof(c150,plain,(![X108]:(![X109]:(![X110]:((~accessible_world(X109,X110)|~vincent_forename(X109,X108))|vincent_forename(X110,X108))))),inference(variable_rename,[status(thm)],[c149])).
% 0.88/1.13  cnf(c151,plain,~accessible_world(X561,X560)|~vincent_forename(X561,X562)|vincent_forename(X560,X562),inference(split_conjunct,[status(thm)],[c150])).
% 0.88/1.13  cnf(c562,plain,~accessible_world(skolem0001,X574)|vincent_forename(X574,skolem0003),inference(resolution,[status(thm)],[c151, c42])).
% 0.88/1.13  cnf(c575,plain,vincent_forename(skolem0005,skolem0003),inference(resolution,[status(thm)],[c562, c50])).
% 0.88/1.13  cnf(c578,plain,skolem0005!=X889|skolem0003!=X888|vincent_forename(X889,X888),inference(resolution,[status(thm)],[c575, c0])).
% 0.88/1.13  cnf(c792,plain,skolem0005!=X890|vincent_forename(X890,skolem0003),inference(resolution,[status(thm)],[c578, reflexivity])).
% 0.88/1.13  cnf(c23,axiom,X380!=X378|X381!=X379|~singleton(X380,X381)|singleton(X378,X379),theory(equality)).
% 0.88/1.13  fof(ax24,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax24)).
% 0.88/1.13  fof(c180,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.88/1.13  fof(c181,plain,(![X129]:(![X130]:(~thing(X129,X130)|singleton(X129,X130)))),inference(variable_rename,[status(thm)],[c180])).
% 0.88/1.13  cnf(c182,plain,~thing(X207,X206)|singleton(X207,X206),inference(split_conjunct,[status(thm)],[c181])).
% 0.88/1.13  fof(ax25,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax25)).
% 0.88/1.13  fof(c177,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.88/1.13  fof(c178,plain,(![X127]:(![X128]:(~eventuality(X127,X128)|thing(X127,X128)))),inference(variable_rename,[status(thm)],[c177])).
% 0.88/1.13  cnf(c179,plain,~eventuality(X204,X205)|thing(X204,X205),inference(split_conjunct,[status(thm)],[c178])).
% 0.88/1.13  fof(ax26,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax26)).
% 0.88/1.13  fof(c174,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.88/1.13  fof(c175,plain,(![X125]:(![X126]:(~event(X125,X126)|eventuality(X125,X126)))),inference(variable_rename,[status(thm)],[c174])).
% 0.88/1.13  cnf(c176,plain,~event(X198,X199)|eventuality(X198,X199),inference(split_conjunct,[status(thm)],[c175])).
% 0.88/1.13  cnf(c51,negated_conjecture,~man(skolem0005,X312)|event(skolem0005,skolem0006(X312)),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.13  cnf(c417,plain,event(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c415, c51])).
% 0.88/1.13  cnf(c448,plain,eventuality(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c417, c176])).
% 0.88/1.13  cnf(c459,plain,thing(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c448, c179])).
% 0.88/1.13  cnf(c467,plain,singleton(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c459, c182])).
% 0.88/1.13  cnf(c475,plain,skolem0005!=X885|skolem0006(skolem0002)!=X886|singleton(X885,X886),inference(resolution,[status(thm)],[c467, c23])).
% 0.88/1.13  cnf(c790,plain,skolem0005!=X887|singleton(X887,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c475, reflexivity])).
% 0.88/1.13  cnf(c2,axiom,X210!=X208|X211!=X209|~relname(X210,X211)|relname(X208,X209),theory(equality)).
% 0.88/1.13  fof(ax3,axiom,(![U]:(![V]:(forename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 0.88/1.13  fof(c243,plain,(![U]:(![V]:(~forename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.88/1.13  fof(c244,plain,(![X171]:(![X172]:(~forename(X171,X172)|relname(X171,X172)))),inference(variable_rename,[status(thm)],[c243])).
% 0.88/1.13  cnf(c245,plain,~forename(X288,X289)|relname(X288,X289),inference(split_conjunct,[status(thm)],[c244])).
% 0.88/1.13  cnf(c43,negated_conjecture,forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.13  fof(ax35,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&forename(V,U))=>forename(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax35)).
% 0.88/1.13  fof(c143,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~forename(V,U))|forename(W,U))))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.88/1.13  fof(c144,plain,(![X102]:(![X103]:(![X104]:((~accessible_world(X103,X104)|~forename(X103,X102))|forename(X104,X102))))),inference(variable_rename,[status(thm)],[c143])).
% 0.88/1.13  cnf(c145,plain,~accessible_world(X547,X548)|~forename(X547,X549)|forename(X548,X549),inference(split_conjunct,[status(thm)],[c144])).
% 0.88/1.13  cnf(c558,plain,~accessible_world(skolem0001,X570)|forename(X570,skolem0003),inference(resolution,[status(thm)],[c145, c43])).
% 0.88/1.13  cnf(c566,plain,forename(skolem0005,skolem0003),inference(resolution,[status(thm)],[c558, c50])).
% 0.88/1.13  cnf(c568,plain,relname(skolem0005,skolem0003),inference(resolution,[status(thm)],[c566, c245])).
% 0.88/1.13  cnf(c572,plain,skolem0005!=X883|skolem0003!=X882|relname(X883,X882),inference(resolution,[status(thm)],[c568, c2])).
% 0.88/1.13  cnf(c788,plain,skolem0005!=X884|relname(X884,skolem0003),inference(resolution,[status(thm)],[c572, reflexivity])).
% 0.88/1.13  cnf(c22,axiom,X373!=X371|X374!=X372|~nonexistent(X373,X374)|nonexistent(X371,X372),theory(equality)).
% 0.88/1.13  fof(ax22,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax22)).
% 0.88/1.13  fof(c186,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.88/1.13  fof(c187,plain,(![X133]:(![X134]:(~eventuality(X133,X134)|nonexistent(X133,X134)))),inference(variable_rename,[status(thm)],[c186])).
% 0.88/1.13  cnf(c188,plain,~eventuality(X214,X215)|nonexistent(X214,X215),inference(split_conjunct,[status(thm)],[c187])).
% 0.88/1.13  cnf(c462,plain,nonexistent(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c448, c188])).
% 0.88/1.13  cnf(c474,plain,skolem0005!=X879|skolem0006(skolem0002)!=X880|nonexistent(X879,X880),inference(resolution,[status(thm)],[c462, c22])).
% 0.88/1.13  cnf(c786,plain,skolem0005!=X881|nonexistent(X881,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c474, reflexivity])).
% 0.88/1.13  cnf(c1,axiom,X202!=X200|X203!=X201|~forename(X202,X203)|forename(X200,X201),theory(equality)).
% 0.88/1.13  cnf(c567,plain,skolem0005!=X877|skolem0003!=X876|forename(X877,X876),inference(resolution,[status(thm)],[c566, c1])).
% 0.88/1.13  cnf(c784,plain,skolem0005!=X878|forename(X878,skolem0003),inference(resolution,[status(thm)],[c567, reflexivity])).
% 0.88/1.13  cnf(c6,axiom,X244!=X242|X245!=X243|~general(X244,X245)|general(X242,X243),theory(equality)).
% 0.88/1.13  fof(ax5,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax5)).
% 0.88/1.13  fof(c237,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.88/1.13  fof(c238,plain,(![X167]:(![X168]:(~abstraction(X167,X168)|general(X167,X168)))),inference(variable_rename,[status(thm)],[c237])).
% 0.88/1.13  cnf(c239,plain,~abstraction(X280,X281)|general(X280,X281),inference(split_conjunct,[status(thm)],[c238])).
% 0.88/1.13  fof(ax8,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax8)).
% 0.88/1.13  fof(c228,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.88/1.13  fof(c229,plain,(![X161]:(![X162]:(~relation(X161,X162)|abstraction(X161,X162)))),inference(variable_rename,[status(thm)],[c228])).
% 0.88/1.13  cnf(c230,plain,~relation(X266,X267)|abstraction(X266,X267),inference(split_conjunct,[status(thm)],[c229])).
% 0.88/1.13  cnf(c298,plain,relname(skolem0001,skolem0003),inference(resolution,[status(thm)],[c245, c43])).
% 0.88/1.13  fof(ax2,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 0.88/1.13  fof(c246,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.88/1.13  fof(c247,plain,(![X173]:(![X174]:(~relname(X173,X174)|relation(X173,X174)))),inference(variable_rename,[status(thm)],[c246])).
% 0.88/1.13  cnf(c248,plain,~relname(X291,X290)|relation(X291,X290),inference(split_conjunct,[status(thm)],[c247])).
% 0.88/1.13  cnf(c300,plain,relation(skolem0001,skolem0003),inference(resolution,[status(thm)],[c248, c298])).
% 0.88/1.13  fof(ax39,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relation(V,U))=>relation(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax39)).
% 0.88/1.13  fof(c131,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relation(V,U))|relation(W,U))))),inference(fof_nnf,[status(thm)],[ax39])).
% 0.88/1.13  fof(c132,plain,(![X90]:(![X91]:(![X92]:((~accessible_world(X91,X92)|~relation(X91,X90))|relation(X92,X90))))),inference(variable_rename,[status(thm)],[c131])).
% 0.88/1.13  cnf(c133,plain,~accessible_world(X530,X528)|~relation(X530,X529)|relation(X528,X529),inference(split_conjunct,[status(thm)],[c132])).
% 0.88/1.13  cnf(c527,plain,~accessible_world(skolem0001,X536)|relation(X536,skolem0003),inference(resolution,[status(thm)],[c133, c300])).
% 0.88/1.13  cnf(c535,plain,relation(skolem0005,skolem0003),inference(resolution,[status(thm)],[c527, c50])).
% 0.88/1.13  cnf(c536,plain,abstraction(skolem0005,skolem0003),inference(resolution,[status(thm)],[c535, c230])).
% 0.88/1.13  cnf(c540,plain,general(skolem0005,skolem0003),inference(resolution,[status(thm)],[c536, c239])).
% 0.88/1.13  cnf(c551,plain,skolem0005!=X873|skolem0003!=X874|general(X873,X874),inference(resolution,[status(thm)],[c540, c6])).
% 0.88/1.13  cnf(c782,plain,skolem0005!=X875|general(X875,skolem0003),inference(resolution,[status(thm)],[c551, reflexivity])).
% 0.88/1.13  cnf(c471,plain,~entity(skolem0001,skolem0002)|~forename(skolem0001,X872)|~of(skolem0001,X872,skolem0002)|~forename(skolem0001,skolem0003)|skolem0003=X872,inference(resolution,[status(thm)],[c61, c40])).
% 0.88/1.13  cnf(c7,axiom,X254!=X252|X255!=X253|~nonhuman(X254,X255)|nonhuman(X252,X253),theory(equality)).
% 0.88/1.13  fof(ax6,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax6)).
% 0.88/1.13  fof(c234,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.88/1.13  fof(c235,plain,(![X165]:(![X166]:(~abstraction(X165,X166)|nonhuman(X165,X166)))),inference(variable_rename,[status(thm)],[c234])).
% 0.88/1.13  cnf(c236,plain,~abstraction(X275,X274)|nonhuman(X275,X274),inference(split_conjunct,[status(thm)],[c235])).
% 0.88/1.13  cnf(c539,plain,nonhuman(skolem0005,skolem0003),inference(resolution,[status(thm)],[c536, c236])).
% 0.88/1.13  cnf(c548,plain,skolem0005!=X869|skolem0003!=X870|nonhuman(X869,X870),inference(resolution,[status(thm)],[c539, c7])).
% 0.88/1.13  cnf(c779,plain,skolem0005!=X871|nonhuman(X871,skolem0003),inference(resolution,[status(thm)],[c548, reflexivity])).
% 0.88/1.13  cnf(c4,axiom,X228!=X226|X229!=X227|~abstraction(X228,X229)|abstraction(X226,X227),theory(equality)).
% 0.88/1.13  cnf(c543,plain,skolem0005!=X864|skolem0003!=X863|abstraction(X864,X863),inference(resolution,[status(thm)],[c536, c4])).
% 0.88/1.13  cnf(c777,plain,skolem0005!=X868|abstraction(X868,skolem0003),inference(resolution,[status(thm)],[c543, reflexivity])).
% 0.88/1.13  cnf(c5,axiom,X236!=X234|X237!=X235|~unisex(X236,X237)|unisex(X234,X235),theory(equality)).
% 0.88/1.13  fof(ax21,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 0.88/1.13  fof(c189,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.88/1.13  fof(c190,plain,(![X135]:(![X136]:(~eventuality(X135,X136)|unisex(X135,X136)))),inference(variable_rename,[status(thm)],[c189])).
% 0.88/1.13  cnf(c191,plain,~eventuality(X220,X221)|unisex(X220,X221),inference(split_conjunct,[status(thm)],[c190])).
% 0.88/1.13  cnf(c461,plain,unisex(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c448, c191])).
% 0.88/1.13  cnf(c468,plain,skolem0005!=X860|skolem0006(skolem0002)!=X859|unisex(X860,X859),inference(resolution,[status(thm)],[c461, c5])).
% 0.88/1.13  cnf(c774,plain,skolem0005!=X862|unisex(X862,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c468, reflexivity])).
% 0.88/1.13  cnf(c3,axiom,X218!=X216|X219!=X217|~relation(X218,X219)|relation(X216,X217),theory(equality)).
% 0.88/1.13  cnf(c538,plain,skolem0005!=X857|skolem0003!=X858|relation(X857,X858),inference(resolution,[status(thm)],[c535, c3])).
% 0.88/1.13  cnf(c773,plain,skolem0005!=X861|relation(X861,skolem0003),inference(resolution,[status(thm)],[c538, reflexivity])).
% 0.88/1.13  cnf(c8,axiom,X262!=X260|X263!=X261|~thing(X262,X263)|thing(X260,X261),theory(equality)).
% 0.88/1.13  cnf(c466,plain,skolem0005!=X854|skolem0006(skolem0002)!=X853|thing(X854,X853),inference(resolution,[status(thm)],[c459, c8])).
% 0.88/1.13  cnf(c770,plain,skolem0005!=X856|thing(X856,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c466, reflexivity])).
% 0.88/1.13  fof(ax9,axiom,(![U]:(![V]:(proposition(U,V)=>relation(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax9)).
% 0.88/1.13  fof(c225,plain,(![U]:(![V]:(~proposition(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.88/1.13  fof(c226,plain,(![X159]:(![X160]:(~proposition(X159,X160)|relation(X159,X160)))),inference(variable_rename,[status(thm)],[c225])).
% 0.88/1.13  cnf(c227,plain,~proposition(X265,X264)|relation(X265,X264),inference(split_conjunct,[status(thm)],[c226])).
% 0.88/1.13  cnf(c44,negated_conjecture,proposition(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.13  fof(ax40,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&proposition(V,U))=>proposition(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax40)).
% 0.88/1.13  fof(c128,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~proposition(V,U))|proposition(W,U))))),inference(fof_nnf,[status(thm)],[ax40])).
% 0.88/1.13  fof(c129,plain,(![X87]:(![X88]:(![X89]:((~accessible_world(X88,X89)|~proposition(X88,X87))|proposition(X89,X87))))),inference(variable_rename,[status(thm)],[c128])).
% 0.88/1.13  cnf(c130,plain,~accessible_world(X521,X522)|~proposition(X521,X520)|proposition(X522,X520),inference(split_conjunct,[status(thm)],[c129])).
% 0.88/1.13  cnf(c512,plain,~accessible_world(skolem0001,X527)|proposition(X527,skolem0005),inference(resolution,[status(thm)],[c130, c44])).
% 0.88/1.13  cnf(c514,plain,proposition(skolem0005,skolem0005),inference(resolution,[status(thm)],[c512, c50])).
% 0.88/1.13  cnf(c517,plain,relation(skolem0005,skolem0005),inference(resolution,[status(thm)],[c514, c227])).
% 0.88/1.13  cnf(c518,plain,abstraction(skolem0005,skolem0005),inference(resolution,[status(thm)],[c517, c230])).
% 0.88/1.13  cnf(c521,plain,general(skolem0005,skolem0005),inference(resolution,[status(thm)],[c518, c239])).
% 0.88/1.13  cnf(c530,plain,skolem0005!=X850|skolem0005!=X851|general(X850,X851),inference(resolution,[status(thm)],[c521, c6])).
% 0.88/1.13  cnf(c768,plain,skolem0005!=X855|general(X855,skolem0005),inference(resolution,[status(thm)],[c530, reflexivity])).
% 0.88/1.13  cnf(c767,plain,skolem0005!=X852|general(X852,X852),inference(factor,[status(thm)],[c530])).
% 0.88/1.13  cnf(c20,axiom,X356!=X354|X357!=X355|~specific(X356,X357)|specific(X354,X355),theory(equality)).
% 0.88/1.13  fof(ax23,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax23)).
% 0.88/1.13  fof(c183,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.88/1.13  fof(c184,plain,(![X131]:(![X132]:(~eventuality(X131,X132)|specific(X131,X132)))),inference(variable_rename,[status(thm)],[c183])).
% 0.88/1.13  cnf(c185,plain,~eventuality(X213,X212)|specific(X213,X212),inference(split_conjunct,[status(thm)],[c184])).
% 0.88/1.13  cnf(c458,plain,specific(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c448, c185])).
% 0.88/1.13  cnf(c464,plain,skolem0005!=X848|skolem0006(skolem0002)!=X847|specific(X848,X847),inference(resolution,[status(thm)],[c458, c20])).
% 0.88/1.13  cnf(c765,plain,skolem0005!=X849|specific(X849,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c464, reflexivity])).
% 0.88/1.13  cnf(c21,axiom,X362!=X360|X363!=X361|~eventuality(X362,X363)|eventuality(X360,X361),theory(equality)).
% 0.88/1.13  cnf(c457,plain,skolem0005!=X844|skolem0006(skolem0002)!=X843|eventuality(X844,X843),inference(resolution,[status(thm)],[c448, c21])).
% 0.88/1.13  cnf(c762,plain,skolem0005!=X846|eventuality(X846,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c457, reflexivity])).
% 0.88/1.13  cnf(c520,plain,nonhuman(skolem0005,skolem0005),inference(resolution,[status(thm)],[c518, c236])).
% 0.88/1.13  cnf(c525,plain,skolem0005!=X840|skolem0005!=X841|nonhuman(X840,X841),inference(resolution,[status(thm)],[c520, c7])).
% 0.88/1.13  cnf(c760,plain,skolem0005!=X845|nonhuman(X845,skolem0005),inference(resolution,[status(thm)],[c525, reflexivity])).
% 0.88/1.13  cnf(c759,plain,skolem0005!=X842|nonhuman(X842,X842),inference(factor,[status(thm)],[c525])).
% 0.88/1.13  cnf(c523,plain,skolem0005!=X834|skolem0005!=X833|abstraction(X834,X833),inference(resolution,[status(thm)],[c518, c4])).
% 0.88/1.13  cnf(c754,plain,skolem0005!=X839|abstraction(X839,skolem0005),inference(resolution,[status(thm)],[c523, reflexivity])).
% 0.88/1.13  cnf(c753,plain,skolem0005!=X835|abstraction(X835,X835),inference(factor,[status(thm)],[c523])).
% 0.88/1.13  cnf(c519,plain,skolem0005!=X824|skolem0005!=X825|relation(X824,X825),inference(resolution,[status(thm)],[c517, c3])).
% 0.88/1.13  cnf(c747,plain,skolem0005!=X832|relation(X832,skolem0005),inference(resolution,[status(thm)],[c519, reflexivity])).
% 0.88/1.13  cnf(c746,plain,skolem0005!=X826|relation(X826,X826),inference(factor,[status(thm)],[c519])).
% 0.88/1.13  cnf(c25,axiom,X397!=X395|X398!=X396|~smoke(X397,X398)|smoke(X395,X396),theory(equality)).
% 0.88/1.13  cnf(c54,negated_conjecture,~man(skolem0005,X318)|smoke(skolem0005,skolem0006(X318)),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.13  cnf(c419,plain,smoke(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c415, c54])).
% 0.88/1.13  cnf(c454,plain,skolem0005!=X821|skolem0006(skolem0002)!=X822|smoke(X821,X822),inference(resolution,[status(thm)],[c419, c25])).
% 0.88/1.13  cnf(c744,plain,skolem0005!=X823|smoke(X823,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c454, reflexivity])).
% 0.88/1.13  cnf(c31,axiom,X452!=X450|X453!=X451|~present(X452,X453)|present(X450,X451),theory(equality)).
% 0.88/1.13  cnf(c53,negated_conjecture,~man(skolem0005,X313)|present(skolem0005,skolem0006(X313)),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.13  cnf(c418,plain,present(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c415, c53])).
% 0.88/1.13  cnf(c451,plain,skolem0005!=X816|skolem0006(skolem0002)!=X817|present(X816,X817),inference(resolution,[status(thm)],[c418, c31])).
% 0.88/1.13  cnf(c740,plain,skolem0005!=X820|present(X820,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c451, reflexivity])).
% 0.88/1.13  cnf(c9,axiom,X270!=X268|X271!=X269|~proposition(X270,X271)|proposition(X268,X269),theory(equality)).
% 0.88/1.13  cnf(c515,plain,skolem0005!=X815|skolem0005!=X814|proposition(X815,X814),inference(resolution,[status(thm)],[c514, c9])).
% 0.88/1.13  cnf(c739,plain,skolem0005!=X819|proposition(X819,skolem0005),inference(resolution,[status(thm)],[c515, reflexivity])).
% 0.88/1.13  cnf(c738,plain,skolem0005!=X818|proposition(X818,X818),inference(factor,[status(thm)],[c515])).
% 0.88/1.13  cnf(c24,axiom,X387!=X385|X388!=X386|~event(X387,X388)|event(X385,X386),theory(equality)).
% 0.88/1.13  cnf(c447,plain,skolem0005!=X811|skolem0006(skolem0002)!=X810|event(X811,X810),inference(resolution,[status(thm)],[c417, c24])).
% 0.88/1.13  cnf(c735,plain,skolem0005!=X813|event(X813,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c447, reflexivity])).
% 0.88/1.13  cnf(c29,axiom,X437!=X435|X438!=X436|~think_believe_consider(X437,X438)|think_believe_consider(X435,X436),theory(equality)).
% 0.88/1.13  cnf(c49,negated_conjecture,think_believe_consider(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.13  fof(ax42,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&think_believe_consider(V,U))=>think_believe_consider(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax42)).
% 0.88/1.13  fof(c122,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~think_believe_consider(V,U))|think_believe_consider(W,U))))),inference(fof_nnf,[status(thm)],[ax42])).
% 0.88/1.13  fof(c123,plain,(![X80]:(![X81]:(![X82]:((~accessible_world(X81,X82)|~think_believe_consider(X81,X80))|think_believe_consider(X82,X80))))),inference(variable_rename,[status(thm)],[c122])).
% 0.88/1.13  cnf(c124,plain,~accessible_world(X516,X514)|~think_believe_consider(X516,X515)|think_believe_consider(X514,X515),inference(split_conjunct,[status(thm)],[c123])).
% 0.88/1.13  cnf(c508,plain,~accessible_world(skolem0001,X518)|think_believe_consider(X518,skolem0004),inference(resolution,[status(thm)],[c124, c49])).
% 0.88/1.13  cnf(c509,plain,think_believe_consider(skolem0005,skolem0004),inference(resolution,[status(thm)],[c508, c50])).
% 0.88/1.13  cnf(c510,plain,skolem0005!=X809|skolem0004!=X808|think_believe_consider(X809,X808),inference(resolution,[status(thm)],[c509, c29])).
% 0.88/1.13  cnf(c734,plain,skolem0005!=X812|think_believe_consider(X812,skolem0004),inference(resolution,[status(thm)],[c510, reflexivity])).
% 0.88/1.13  cnf(c479,plain,~accessible_world(skolem0005,X807)|agent(X807,skolem0006(skolem0002),skolem0002),inference(resolution,[status(thm)],[c91, c445])).
% 0.88/1.13  cnf(c19,axiom,X351!=X349|X352!=X350|~existent(X351,X352)|existent(X349,X350),theory(equality)).
% 0.88/1.13  fof(ax15,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax15)).
% 0.88/1.13  fof(c207,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.88/1.13  fof(c208,plain,(![X147]:(![X148]:(~entity(X147,X148)|existent(X147,X148)))),inference(variable_rename,[status(thm)],[c207])).
% 0.88/1.13  cnf(c209,plain,~entity(X241,X240)|existent(X241,X240),inference(split_conjunct,[status(thm)],[c208])).
% 0.88/1.13  fof(ax18,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 0.88/1.13  fof(c198,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.88/1.13  fof(c199,plain,(![X141]:(![X142]:(~organism(X141,X142)|entity(X141,X142)))),inference(variable_rename,[status(thm)],[c198])).
% 0.88/1.13  cnf(c200,plain,~organism(X231,X230)|entity(X231,X230),inference(split_conjunct,[status(thm)],[c199])).
% 0.88/1.13  fof(ax19,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax19)).
% 0.88/1.13  fof(c195,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.88/1.13  fof(c196,plain,(![X139]:(![X140]:(~human_person(X139,X140)|organism(X139,X140)))),inference(variable_rename,[status(thm)],[c195])).
% 0.88/1.13  cnf(c197,plain,~human_person(X224,X225)|organism(X224,X225),inference(split_conjunct,[status(thm)],[c196])).
% 0.88/1.13  fof(ax20,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 0.88/1.13  fof(c192,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.88/1.13  fof(c193,plain,(![X137]:(![X138]:(~man(X137,X138)|human_person(X137,X138)))),inference(variable_rename,[status(thm)],[c192])).
% 0.88/1.13  cnf(c194,plain,~man(X223,X222)|human_person(X223,X222),inference(split_conjunct,[status(thm)],[c193])).
% 0.88/1.13  cnf(c420,plain,human_person(skolem0005,skolem0002),inference(resolution,[status(thm)],[c415, c194])).
% 0.88/1.13  cnf(c429,plain,organism(skolem0005,skolem0002),inference(resolution,[status(thm)],[c420, c197])).
% 0.88/1.13  cnf(c433,plain,entity(skolem0005,skolem0002),inference(resolution,[status(thm)],[c429, c200])).
% 0.88/1.13  cnf(c442,plain,existent(skolem0005,skolem0002),inference(resolution,[status(thm)],[c433, c209])).
% 0.88/1.13  cnf(c446,plain,skolem0005!=X805|skolem0002!=X804|existent(X805,X804),inference(resolution,[status(thm)],[c442, c19])).
% 0.88/1.13  cnf(c732,plain,skolem0005!=X806|existent(X806,skolem0002),inference(resolution,[status(thm)],[c446, reflexivity])).
% 0.88/1.13  cnf(c17,axiom,X332!=X330|X333!=X331|~impartial(X332,X333)|impartial(X330,X331),theory(equality)).
% 0.88/1.13  fof(ax14,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax14)).
% 0.88/1.13  fof(c210,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.88/1.13  fof(c211,plain,(![X149]:(![X150]:(~organism(X149,X150)|impartial(X149,X150)))),inference(variable_rename,[status(thm)],[c210])).
% 0.88/1.13  cnf(c212,plain,~organism(X246,X247)|impartial(X246,X247),inference(split_conjunct,[status(thm)],[c211])).
% 0.88/1.13  cnf(c435,plain,impartial(skolem0005,skolem0002),inference(resolution,[status(thm)],[c429, c212])).
% 0.88/1.13  cnf(c444,plain,skolem0005!=X802|skolem0002!=X801|impartial(X802,X801),inference(resolution,[status(thm)],[c435, c17])).
% 0.88/1.13  cnf(c730,plain,skolem0005!=X803|impartial(X803,skolem0002),inference(resolution,[status(thm)],[c444, reflexivity])).
% 0.88/1.13  cnf(c16,axiom,X328!=X326|X329!=X327|~living(X328,X329)|living(X326,X327),theory(equality)).
% 0.88/1.13  fof(ax13,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax13)).
% 0.88/1.13  fof(c213,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.88/1.14  fof(c214,plain,(![X151]:(![X152]:(~organism(X151,X152)|living(X151,X152)))),inference(variable_rename,[status(thm)],[c213])).
% 0.88/1.14  cnf(c215,plain,~organism(X249,X248)|living(X249,X248),inference(split_conjunct,[status(thm)],[c214])).
% 0.88/1.14  cnf(c434,plain,living(skolem0005,skolem0002),inference(resolution,[status(thm)],[c429, c215])).
% 0.88/1.14  cnf(c443,plain,skolem0005!=X799|skolem0002!=X798|living(X799,X798),inference(resolution,[status(thm)],[c434, c16])).
% 0.88/1.14  cnf(c728,plain,skolem0005!=X800|living(X800,skolem0002),inference(resolution,[status(thm)],[c443, reflexivity])).
% 0.88/1.14  cnf(c18,axiom,X341!=X339|X342!=X340|~entity(X341,X342)|entity(X339,X340),theory(equality)).
% 0.88/1.14  cnf(c440,plain,skolem0005!=X795|skolem0002!=X796|entity(X795,X796),inference(resolution,[status(thm)],[c433, c18])).
% 0.88/1.14  cnf(c726,plain,skolem0005!=X797|entity(X797,skolem0002),inference(resolution,[status(thm)],[c440, reflexivity])).
% 0.88/1.14  cnf(c48,negated_conjecture,present(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c38])).
% 0.88/1.14  cnf(c438,plain,skolem0001!=X792|skolem0004!=X793|present(X792,X793),inference(resolution,[status(thm)],[c31, c48])).
% 0.88/1.14  cnf(c724,plain,skolem0001!=X794|present(X794,skolem0004),inference(resolution,[status(thm)],[c438, reflexivity])).
% 0.88/1.14  fof(ax54,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&present(V,U))=>present(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax54)).
% 0.88/1.14  fof(c86,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~present(V,U))|present(W,U))))),inference(fof_nnf,[status(thm)],[ax54])).
% 0.88/1.14  fof(c87,plain,(![X43]:(![X44]:(![X45]:((~accessible_world(X44,X45)|~present(X44,X43))|present(X45,X43))))),inference(variable_rename,[status(thm)],[c86])).
% 0.88/1.14  cnf(c88,plain,~accessible_world(X433,X431)|~present(X433,X432)|present(X431,X432),inference(split_conjunct,[status(thm)],[c87])).
% 0.88/1.14  cnf(c410,plain,~accessible_world(skolem0001,X434)|present(X434,skolem0004),inference(resolution,[status(thm)],[c88, c48])).
% 0.88/1.14  cnf(c411,plain,present(skolem0005,skolem0004),inference(resolution,[status(thm)],[c410, c50])).
% 0.88/1.14  cnf(c437,plain,skolem0005!=X789|skolem0004!=X790|present(X789,X790),inference(resolution,[status(thm)],[c31, c411])).
% 0.88/1.14  cnf(c722,plain,skolem0005!=X791|present(X791,skolem0004),inference(resolution,[status(thm)],[c437, reflexivity])).
% 0.88/1.14  cnf(c15,axiom,X316!=X314|X317!=X315|~organism(X316,X317)|organism(X314,X315),theory(equality)).
% 0.88/1.14  cnf(c436,plain,skolem0005!=X786|skolem0002!=X787|organism(X786,X787),inference(resolution,[status(thm)],[c429, c15])).
% 0.88/1.14  cnf(c720,plain,skolem0005!=X788|organism(X788,skolem0002),inference(resolution,[status(thm)],[c436, reflexivity])).
% 0.88/1.14  cnf(c13,axiom,X298!=X296|X299!=X297|~animate(X298,X299)|animate(X296,X297),theory(equality)).
% 0.88/1.14  fof(ax11,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax11)).
% 0.88/1.14  fof(c219,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.88/1.14  fof(c220,plain,(![X155]:(![X156]:(~human_person(X155,X156)|animate(X155,X156)))),inference(variable_rename,[status(thm)],[c219])).
% 0.88/1.14  cnf(c221,plain,~human_person(X257,X256)|animate(X257,X256),inference(split_conjunct,[status(thm)],[c220])).
% 0.88/1.14  cnf(c427,plain,animate(skolem0005,skolem0002),inference(resolution,[status(thm)],[c420, c221])).
% 0.88/1.14  cnf(c432,plain,skolem0005!=X784|skolem0002!=X783|animate(X784,X783),inference(resolution,[status(thm)],[c427, c13])).
% 0.88/1.14  cnf(c718,plain,skolem0005!=X785|animate(X785,skolem0002),inference(resolution,[status(thm)],[c432, reflexivity])).
% 0.88/1.14  cnf(c14,axiom,X305!=X303|X306!=X304|~human(X305,X306)|human(X303,X304),theory(equality)).
% 0.88/1.14  fof(ax12,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax12)).
% 0.88/1.14  fof(c216,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.88/1.14  fof(c217,plain,(![X153]:(![X154]:(~human_person(X153,X154)|human(X153,X154)))),inference(variable_rename,[status(thm)],[c216])).
% 0.88/1.14  cnf(c218,plain,~human_person(X250,X251)|human(X250,X251),inference(split_conjunct,[status(thm)],[c217])).
% 0.88/1.14  cnf(c426,plain,human(skolem0005,skolem0002),inference(resolution,[status(thm)],[c420, c218])).
% 0.96/1.14  cnf(c431,plain,skolem0005!=X780|skolem0002!=X781|human(X780,X781),inference(resolution,[status(thm)],[c426, c14])).
% 0.96/1.14  cnf(c716,plain,skolem0005!=X782|human(X782,skolem0002),inference(resolution,[status(thm)],[c431, reflexivity])).
% 0.96/1.14  cnf(c12,axiom,X294!=X292|X295!=X293|~human_person(X294,X295)|human_person(X292,X293),theory(equality)).
% 0.96/1.14  cnf(c428,plain,skolem0005!=X774|skolem0002!=X775|human_person(X774,X775),inference(resolution,[status(thm)],[c420, c12])).
% 0.96/1.14  cnf(c713,plain,skolem0005!=X776|human_person(X776,skolem0002),inference(resolution,[status(thm)],[c428, reflexivity])).
% 0.96/1.14  cnf(c11,axiom,X286!=X284|X287!=X285|~male(X286,X287)|male(X284,X285),theory(equality)).
% 0.96/1.14  fof(ax10,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax10)).
% 0.96/1.14  fof(c222,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.96/1.14  fof(c223,plain,(![X157]:(![X158]:(~man(X157,X158)|male(X157,X158)))),inference(variable_rename,[status(thm)],[c222])).
% 0.96/1.14  cnf(c224,plain,~man(X259,X258)|male(X259,X258),inference(split_conjunct,[status(thm)],[c223])).
% 0.96/1.14  cnf(c416,plain,male(skolem0005,skolem0002),inference(resolution,[status(thm)],[c415, c224])).
% 0.96/1.14  cnf(c424,plain,skolem0005!=X772|skolem0002!=X771|male(X772,X771),inference(resolution,[status(thm)],[c416, c11])).
% 0.96/1.14  cnf(c711,plain,skolem0005!=X773|male(X773,skolem0002),inference(resolution,[status(thm)],[c424, reflexivity])).
% 0.96/1.14  cnf(c10,axiom,X278!=X276|X279!=X277|~man(X278,X279)|man(X276,X277),theory(equality)).
% 0.96/1.14  cnf(c421,plain,skolem0005!=X769|skolem0002!=X768|man(X769,X768),inference(resolution,[status(thm)],[c415, c10])).
% 0.96/1.14  cnf(c709,plain,skolem0005!=X770|man(X770,skolem0002),inference(resolution,[status(thm)],[c421, reflexivity])).
% 0.96/1.14  cnf(c413,plain,skolem0001!=X763|skolem0004!=X762|think_believe_consider(X763,X762),inference(resolution,[status(thm)],[c29, c49])).
% 0.96/1.14  cnf(c706,plain,skolem0001!=X767|think_believe_consider(X767,skolem0004),inference(resolution,[status(thm)],[c413, reflexivity])).
% 0.96/1.14  cnf(c281,plain,relation(skolem0001,skolem0005),inference(resolution,[status(thm)],[c227, c44])).
% 0.96/1.14  cnf(c283,plain,abstraction(skolem0001,skolem0005),inference(resolution,[status(thm)],[c230, c281])).
% 0.96/1.14  fof(ax4,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 0.96/1.14  fof(c240,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.96/1.14  fof(c241,plain,(![X169]:(![X170]:(~abstraction(X169,X170)|unisex(X169,X170)))),inference(variable_rename,[status(thm)],[c240])).
% 0.96/1.14  cnf(c242,plain,~abstraction(X282,X283)|unisex(X282,X283),inference(split_conjunct,[status(thm)],[c241])).
% 0.96/1.14  cnf(c295,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c242, c283])).
% 0.96/1.14  fof(ax55,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&unisex(V,U))=>unisex(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax55)).
% 0.96/1.14  fof(c83,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~unisex(V,U))|unisex(W,U))))),inference(fof_nnf,[status(thm)],[ax55])).
% 0.96/1.14  fof(c84,plain,(![X40]:(![X41]:(![X42]:((~accessible_world(X41,X42)|~unisex(X41,X40))|unisex(X42,X40))))),inference(variable_rename,[status(thm)],[c83])).
% 0.96/1.14  cnf(c85,plain,~accessible_world(X412,X414)|~unisex(X412,X413)|unisex(X414,X413),inference(split_conjunct,[status(thm)],[c84])).
% 0.96/1.14  cnf(c399,plain,~accessible_world(skolem0001,X421)|unisex(X421,skolem0005),inference(resolution,[status(thm)],[c85, c295])).
% 0.96/1.14  cnf(c406,plain,unisex(skolem0005,skolem0005),inference(resolution,[status(thm)],[c399, c50])).
% 0.96/1.14  cnf(c407,plain,skolem0005!=X759|skolem0005!=X758|unisex(X759,X758),inference(resolution,[status(thm)],[c406, c5])).
% 0.96/1.14  cnf(c703,plain,skolem0005!=X761|unisex(X761,skolem0005),inference(resolution,[status(thm)],[c407, reflexivity])).
% 0.96/1.14  cnf(c702,plain,skolem0005!=X760|unisex(X760,X760),inference(factor,[status(thm)],[c407])).
% 0.96/1.14  cnf(c27,axiom,X418!=X416|X419!=X417|~accessible_world(X418,X419)|accessible_world(X416,X417),theory(equality)).
% 0.96/1.14  cnf(c404,plain,skolem0001!=X755|skolem0005!=X756|accessible_world(X755,X756),inference(resolution,[status(thm)],[c27, c50])).
% 0.96/1.14  cnf(c700,plain,skolem0001!=X757|accessible_world(X757,skolem0005),inference(resolution,[status(thm)],[c404, reflexivity])).
% 0.96/1.14  cnf(c301,plain,abstraction(skolem0001,skolem0003),inference(resolution,[status(thm)],[c300, c230])).
% 0.96/1.14  cnf(c306,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c301, c242])).
% 0.96/1.14  cnf(c397,plain,~accessible_world(skolem0001,X415)|unisex(X415,skolem0003),inference(resolution,[status(thm)],[c85, c306])).
% 0.96/1.14  cnf(c401,plain,unisex(skolem0005,skolem0003),inference(resolution,[status(thm)],[c397, c50])).
% 0.96/1.14  cnf(c402,plain,skolem0005!=X750|skolem0003!=X749|unisex(X750,X749),inference(resolution,[status(thm)],[c401, c5])).
% 0.96/1.14  cnf(c697,plain,skolem0005!=X754|unisex(X754,skolem0003),inference(resolution,[status(thm)],[c402, reflexivity])).
% 0.96/1.14  cnf(c264,plain,human_person(skolem0001,skolem0002),inference(resolution,[status(thm)],[c194, c41])).
% 0.96/1.14  cnf(c265,plain,organism(skolem0001,skolem0002),inference(resolution,[status(thm)],[c197, c264])).
% 0.96/1.14  cnf(c266,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c200, c265])).
% 0.96/1.14  fof(ax16,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax16)).
% 0.96/1.14  fof(c204,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.96/1.14  fof(c205,plain,(![X145]:(![X146]:(~entity(X145,X146)|specific(X145,X146)))),inference(variable_rename,[status(thm)],[c204])).
% 0.96/1.14  cnf(c206,plain,~entity(X238,X239)|specific(X238,X239),inference(split_conjunct,[status(thm)],[c205])).
% 0.96/1.14  cnf(c270,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c206, c266])).
% 0.96/1.14  fof(ax57,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&specific(V,U))=>specific(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax57)).
% 0.96/1.14  fof(c77,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~specific(V,U))|specific(W,U))))),inference(fof_nnf,[status(thm)],[ax57])).
% 0.96/1.14  fof(c78,plain,(![X34]:(![X35]:(![X36]:((~accessible_world(X35,X36)|~specific(X35,X34))|specific(X36,X34))))),inference(variable_rename,[status(thm)],[c77])).
% 0.96/1.14  cnf(c79,plain,~accessible_world(X392,X390)|~specific(X392,X391)|specific(X390,X391),inference(split_conjunct,[status(thm)],[c78])).
% 0.96/1.14  cnf(c387,plain,~accessible_world(skolem0001,X394)|specific(X394,skolem0002),inference(resolution,[status(thm)],[c79, c270])).
% 0.96/1.14  cnf(c390,plain,specific(skolem0005,skolem0002),inference(resolution,[status(thm)],[c387, c50])).
% 0.96/1.14  cnf(c392,plain,skolem0005!=X746|skolem0002!=X745|specific(X746,X745),inference(resolution,[status(thm)],[c390, c20])).
% 0.96/1.14  cnf(c694,plain,skolem0005!=X748|specific(X748,skolem0002),inference(resolution,[status(thm)],[c392, reflexivity])).
% 0.96/1.14  cnf(c47,negated_conjecture,event(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c38])).
% 0.96/1.14  cnf(c385,plain,skolem0001!=X744|skolem0004!=X743|event(X744,X743),inference(resolution,[status(thm)],[c24, c47])).
% 0.96/1.14  cnf(c693,plain,skolem0001!=X747|event(X747,skolem0004),inference(resolution,[status(thm)],[c385, reflexivity])).
% 0.96/1.14  fof(ax61,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&event(V,U))=>event(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax61)).
% 0.96/1.14  fof(c65,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~event(V,U))|event(W,U))))),inference(fof_nnf,[status(thm)],[ax61])).
% 0.96/1.14  fof(c66,plain,(![X22]:(![X23]:(![X24]:((~accessible_world(X23,X24)|~event(X23,X22))|event(X24,X22))))),inference(variable_rename,[status(thm)],[c65])).
% 0.96/1.14  cnf(c67,plain,~accessible_world(X323,X322)|~event(X323,X324)|event(X322,X324),inference(split_conjunct,[status(thm)],[c66])).
% 0.96/1.14  cnf(c320,plain,~accessible_world(skolem0001,X325)|event(X325,skolem0004),inference(resolution,[status(thm)],[c67, c47])).
% 0.96/1.14  cnf(c321,plain,event(skolem0005,skolem0004),inference(resolution,[status(thm)],[c320, c50])).
% 0.96/1.14  cnf(c384,plain,skolem0005!=X740|skolem0004!=X739|event(X740,X739),inference(resolution,[status(thm)],[c24, c321])).
% 0.96/1.14  cnf(c690,plain,skolem0005!=X742|event(X742,skolem0004),inference(resolution,[status(thm)],[c384, reflexivity])).
% 0.96/1.14  fof(ax17,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax17)).
% 0.96/1.14  fof(c201,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.96/1.14  fof(c202,plain,(![X143]:(![X144]:(~entity(X143,X144)|thing(X143,X144)))),inference(variable_rename,[status(thm)],[c201])).
% 0.96/1.14  cnf(c203,plain,~entity(X233,X232)|thing(X233,X232),inference(split_conjunct,[status(thm)],[c202])).
% 0.96/1.14  cnf(c267,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c203, c266])).
% 0.96/1.14  fof(ax59,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&thing(V,U))=>thing(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax59)).
% 0.96/1.14  fof(c71,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~thing(V,U))|thing(W,U))))),inference(fof_nnf,[status(thm)],[ax59])).
% 0.96/1.14  fof(c72,plain,(![X28]:(![X29]:(![X30]:((~accessible_world(X29,X30)|~thing(X29,X28))|thing(X30,X28))))),inference(variable_rename,[status(thm)],[c71])).
% 0.96/1.14  cnf(c73,plain,~accessible_world(X344,X345)|~thing(X344,X346)|thing(X345,X346),inference(split_conjunct,[status(thm)],[c72])).
% 0.96/1.14  cnf(c341,plain,~accessible_world(skolem0001,X358)|thing(X358,skolem0002),inference(resolution,[status(thm)],[c73, c267])).
% 0.96/1.14  cnf(c355,plain,thing(skolem0005,skolem0002),inference(resolution,[status(thm)],[c341, c50])).
% 0.96/1.14  cnf(c358,plain,singleton(skolem0005,skolem0002),inference(resolution,[status(thm)],[c355, c182])).
% 0.96/1.14  cnf(c382,plain,skolem0005!=X737|skolem0002!=X738|singleton(X737,X738),inference(resolution,[status(thm)],[c23, c358])).
% 0.96/1.14  cnf(c689,plain,skolem0005!=X741|singleton(X741,skolem0002),inference(resolution,[status(thm)],[c382, reflexivity])).
% 0.96/1.14  cnf(c322,plain,eventuality(skolem0005,skolem0004),inference(resolution,[status(thm)],[c321, c176])).
% 0.96/1.14  cnf(c328,plain,thing(skolem0005,skolem0004),inference(resolution,[status(thm)],[c322, c179])).
% 0.96/1.14  cnf(c332,plain,singleton(skolem0005,skolem0004),inference(resolution,[status(thm)],[c328, c182])).
% 0.96/1.14  cnf(c381,plain,skolem0005!=X733|skolem0004!=X734|singleton(X733,X734),inference(resolution,[status(thm)],[c23, c332])).
% 0.96/1.14  cnf(c686,plain,skolem0005!=X736|singleton(X736,skolem0004),inference(resolution,[status(thm)],[c381, reflexivity])).
% 0.96/1.14  fof(ax7,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax7)).
% 0.96/1.14  fof(c231,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.96/1.14  fof(c232,plain,(![X163]:(![X164]:(~abstraction(X163,X164)|thing(X163,X164)))),inference(variable_rename,[status(thm)],[c231])).
% 0.96/1.14  cnf(c233,plain,~abstraction(X272,X273)|thing(X272,X273),inference(split_conjunct,[status(thm)],[c232])).
% 0.96/1.14  cnf(c308,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c301, c233])).
% 0.96/1.14  cnf(c339,plain,~accessible_world(skolem0001,X348)|thing(X348,skolem0003),inference(resolution,[status(thm)],[c73, c308])).
% 0.96/1.14  cnf(c343,plain,thing(skolem0005,skolem0003),inference(resolution,[status(thm)],[c339, c50])).
% 0.96/1.14  cnf(c347,plain,singleton(skolem0005,skolem0003),inference(resolution,[status(thm)],[c343, c182])).
% 0.96/1.14  cnf(c380,plain,skolem0005!=X731|skolem0003!=X732|singleton(X731,X732),inference(resolution,[status(thm)],[c23, c347])).
% 0.96/1.14  cnf(c685,plain,skolem0005!=X735|singleton(X735,skolem0003),inference(resolution,[status(thm)],[c380, reflexivity])).
% 0.96/1.14  cnf(c286,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c233, c283])).
% 0.96/1.14  cnf(c288,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c286, c182])).
% 0.96/1.14  cnf(c379,plain,skolem0001!=X727|skolem0005!=X728|singleton(X727,X728),inference(resolution,[status(thm)],[c23, c288])).
% 0.96/1.14  cnf(c682,plain,skolem0001!=X730|singleton(X730,skolem0005),inference(resolution,[status(thm)],[c379, reflexivity])).
% 0.96/1.14  cnf(c314,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c308, c182])).
% 0.96/1.14  cnf(c378,plain,skolem0001!=X725|skolem0003!=X726|singleton(X725,X726),inference(resolution,[status(thm)],[c23, c314])).
% 0.96/1.14  cnf(c681,plain,skolem0001!=X729|singleton(X729,skolem0003),inference(resolution,[status(thm)],[c378, reflexivity])).
% 0.96/1.14  cnf(c256,plain,eventuality(skolem0001,skolem0004),inference(resolution,[status(thm)],[c176, c47])).
% 0.96/1.14  cnf(c258,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c179, c256])).
% 0.96/1.14  cnf(c259,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c182, c258])).
% 0.96/1.14  cnf(c377,plain,skolem0001!=X721|skolem0004!=X722|singleton(X721,X722),inference(resolution,[status(thm)],[c23, c259])).
% 0.96/1.14  cnf(c678,plain,skolem0001!=X724|singleton(X724,skolem0004),inference(resolution,[status(thm)],[c377, reflexivity])).
% 0.96/1.14  cnf(c340,plain,~accessible_world(skolem0001,X353)|thing(X353,skolem0005),inference(resolution,[status(thm)],[c73, c286])).
% 0.96/1.14  cnf(c348,plain,thing(skolem0005,skolem0005),inference(resolution,[status(thm)],[c340, c50])).
% 0.96/1.14  cnf(c351,plain,singleton(skolem0005,skolem0005),inference(resolution,[status(thm)],[c348, c182])).
% 0.96/1.14  cnf(c376,plain,skolem0005!=X718|skolem0005!=X719|singleton(X718,X719),inference(resolution,[status(thm)],[c23, c351])).
% 0.96/1.14  cnf(c676,plain,skolem0005!=X723|singleton(X723,skolem0005),inference(resolution,[status(thm)],[c376, reflexivity])).
% 0.96/1.14  cnf(c675,plain,skolem0005!=X720|singleton(X720,X720),inference(factor,[status(thm)],[c376])).
% 0.96/1.14  cnf(c268,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c267, c182])).
% 0.96/1.14  cnf(c375,plain,skolem0001!=X715|skolem0002!=X716|singleton(X715,X716),inference(resolution,[status(thm)],[c23, c268])).
% 0.96/1.14  cnf(c673,plain,skolem0001!=X717|singleton(X717,skolem0002),inference(resolution,[status(thm)],[c375, reflexivity])).
% 0.96/1.14  cnf(c327,plain,nonexistent(skolem0005,skolem0004),inference(resolution,[status(thm)],[c322, c188])).
% 0.96/1.14  cnf(c372,plain,skolem0005!=X712|skolem0004!=X713|nonexistent(X712,X713),inference(resolution,[status(thm)],[c22, c327])).
% 0.96/1.14  cnf(c671,plain,skolem0005!=X714|nonexistent(X714,skolem0004),inference(resolution,[status(thm)],[c372, reflexivity])).
% 0.96/1.14  cnf(c261,plain,nonexistent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c188, c256])).
% 0.96/1.14  cnf(c371,plain,skolem0001!=X709|skolem0004!=X710|nonexistent(X709,X710),inference(resolution,[status(thm)],[c22, c261])).
% 0.96/1.14  cnf(c669,plain,skolem0001!=X711|nonexistent(X711,skolem0004),inference(resolution,[status(thm)],[c371, reflexivity])).
% 0.96/1.14  cnf(c361,plain,skolem0005!=X707|skolem0004!=X706|eventuality(X707,X706),inference(resolution,[status(thm)],[c21, c322])).
% 0.96/1.14  cnf(c667,plain,skolem0005!=X708|eventuality(X708,skolem0004),inference(resolution,[status(thm)],[c361, reflexivity])).
% 0.96/1.14  cnf(c360,plain,skolem0001!=X704|skolem0004!=X703|eventuality(X704,X703),inference(resolution,[status(thm)],[c21, c256])).
% 0.96/1.14  cnf(c665,plain,skolem0001!=X705|eventuality(X705,skolem0004),inference(resolution,[status(thm)],[c360, reflexivity])).
% 0.96/1.14  cnf(c357,plain,skolem0005!=X701|skolem0002!=X700|thing(X701,X700),inference(resolution,[status(thm)],[c355, c8])).
% 0.96/1.14  cnf(c663,plain,skolem0005!=X702|thing(X702,skolem0002),inference(resolution,[status(thm)],[c357, reflexivity])).
% 0.96/1.14  cnf(c326,plain,specific(skolem0005,skolem0004),inference(resolution,[status(thm)],[c322, c185])).
% 0.96/1.14  cnf(c354,plain,skolem0005!=X698|skolem0004!=X697|specific(X698,X697),inference(resolution,[status(thm)],[c20, c326])).
% 0.96/1.14  cnf(c661,plain,skolem0005!=X699|specific(X699,skolem0004),inference(resolution,[status(thm)],[c354, reflexivity])).
% 0.96/1.14  cnf(c353,plain,skolem0001!=X695|skolem0002!=X694|specific(X695,X694),inference(resolution,[status(thm)],[c20, c270])).
% 0.96/1.14  cnf(c659,plain,skolem0001!=X696|specific(X696,skolem0002),inference(resolution,[status(thm)],[c353, reflexivity])).
% 0.96/1.14  cnf(c260,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c185, c256])).
% 0.96/1.14  cnf(c352,plain,skolem0001!=X692|skolem0004!=X691|specific(X692,X691),inference(resolution,[status(thm)],[c20, c260])).
% 0.96/1.14  cnf(c657,plain,skolem0001!=X693|specific(X693,skolem0004),inference(resolution,[status(thm)],[c352, reflexivity])).
% 0.96/1.14  cnf(c350,plain,skolem0005!=X688|skolem0005!=X687|thing(X688,X687),inference(resolution,[status(thm)],[c348, c8])).
% 0.96/1.14  cnf(c654,plain,skolem0005!=X690|thing(X690,skolem0005),inference(resolution,[status(thm)],[c350, reflexivity])).
% 0.96/1.14  cnf(c653,plain,skolem0005!=X689|thing(X689,X689),inference(factor,[status(thm)],[c350])).
% 0.96/1.14  cnf(c346,plain,skolem0005!=X685|skolem0003!=X684|thing(X685,X684),inference(resolution,[status(thm)],[c343, c8])).
% 0.96/1.14  cnf(c651,plain,skolem0005!=X686|thing(X686,skolem0003),inference(resolution,[status(thm)],[c346, reflexivity])).
% 0.96/1.14  cnf(c271,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c209, c266])).
% 0.96/1.14  cnf(c344,plain,skolem0001!=X682|skolem0002!=X681|existent(X682,X681),inference(resolution,[status(thm)],[c19, c271])).
% 0.96/1.14  cnf(c649,plain,skolem0001!=X683|existent(X683,skolem0002),inference(resolution,[status(thm)],[c344, reflexivity])).
% 0.96/1.14  cnf(c337,plain,skolem0001!=X678|skolem0002!=X679|entity(X678,X679),inference(resolution,[status(thm)],[c18, c266])).
% 0.96/1.14  cnf(c647,plain,skolem0001!=X680|entity(X680,skolem0002),inference(resolution,[status(thm)],[c337, reflexivity])).
% 0.96/1.14  cnf(c272,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c212, c265])).
% 0.96/1.14  cnf(c333,plain,skolem0001!=X676|skolem0002!=X675|impartial(X676,X675),inference(resolution,[status(thm)],[c17, c272])).
% 0.96/1.14  cnf(c645,plain,skolem0001!=X677|impartial(X677,skolem0002),inference(resolution,[status(thm)],[c333, reflexivity])).
% 0.96/1.14  cnf(c331,plain,skolem0005!=X673|skolem0004!=X672|thing(X673,X672),inference(resolution,[status(thm)],[c328, c8])).
% 0.96/1.14  cnf(c643,plain,skolem0005!=X674|thing(X674,skolem0004),inference(resolution,[status(thm)],[c331, reflexivity])).
% 0.96/1.14  cnf(c325,plain,unisex(skolem0005,skolem0004),inference(resolution,[status(thm)],[c322, c191])).
% 0.96/1.14  cnf(c329,plain,skolem0005!=X670|skolem0004!=X669|unisex(X670,X669),inference(resolution,[status(thm)],[c325, c5])).
% 0.96/1.14  cnf(c641,plain,skolem0005!=X671|unisex(X671,skolem0004),inference(resolution,[status(thm)],[c329, reflexivity])).
% 0.96/1.14  cnf(c273,plain,living(skolem0001,skolem0002),inference(resolution,[status(thm)],[c215, c265])).
% 0.96/1.14  cnf(c324,plain,skolem0001!=X667|skolem0002!=X666|living(X667,X666),inference(resolution,[status(thm)],[c16, c273])).
% 0.96/1.14  cnf(c639,plain,skolem0001!=X668|living(X668,skolem0002),inference(resolution,[status(thm)],[c324, reflexivity])).
% 0.96/1.14  cnf(c319,plain,skolem0001!=X663|skolem0002!=X664|organism(X663,X664),inference(resolution,[status(thm)],[c15, c265])).
% 0.96/1.14  cnf(c637,plain,skolem0001!=X665|organism(X665,skolem0002),inference(resolution,[status(thm)],[c319, reflexivity])).
% 0.96/1.14  cnf(c274,plain,human(skolem0001,skolem0002),inference(resolution,[status(thm)],[c218, c264])).
% 0.96/1.14  cnf(c317,plain,skolem0001!=X660|skolem0002!=X661|human(X660,X661),inference(resolution,[status(thm)],[c14, c274])).
% 0.96/1.14  cnf(c635,plain,skolem0001!=X662|human(X662,skolem0002),inference(resolution,[status(thm)],[c317, reflexivity])).
% 0.96/1.14  cnf(c276,plain,animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c221, c264])).
% 0.96/1.14  cnf(c315,plain,skolem0001!=X658|skolem0002!=X657|animate(X658,X657),inference(resolution,[status(thm)],[c13, c276])).
% 0.96/1.14  cnf(c633,plain,skolem0001!=X659|animate(X659,skolem0002),inference(resolution,[status(thm)],[c315, reflexivity])).
% 0.96/1.14  cnf(c313,plain,skolem0001!=X655|skolem0003!=X654|thing(X655,X654),inference(resolution,[status(thm)],[c308, c8])).
% 0.96/1.14  cnf(c631,plain,skolem0001!=X656|thing(X656,skolem0003),inference(resolution,[status(thm)],[c313, reflexivity])).
% 0.96/1.14  cnf(c312,plain,skolem0001!=X652|skolem0003!=X651|unisex(X652,X651),inference(resolution,[status(thm)],[c306, c5])).
% 0.96/1.14  cnf(c629,plain,skolem0001!=X653|unisex(X653,skolem0003),inference(resolution,[status(thm)],[c312, reflexivity])).
% 0.96/1.14  cnf(c305,plain,general(skolem0001,skolem0003),inference(resolution,[status(thm)],[c301, c239])).
% 0.96/1.14  cnf(c311,plain,skolem0001!=X648|skolem0003!=X649|general(X648,X649),inference(resolution,[status(thm)],[c305, c6])).
% 0.96/1.14  cnf(c627,plain,skolem0001!=X650|general(X650,skolem0003),inference(resolution,[status(thm)],[c311, reflexivity])).
% 0.96/1.14  cnf(c304,plain,nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c301, c236])).
% 0.96/1.14  cnf(c309,plain,skolem0001!=X645|skolem0003!=X646|nonhuman(X645,X646),inference(resolution,[status(thm)],[c304, c7])).
% 0.96/1.14  cnf(c625,plain,skolem0001!=X647|nonhuman(X647,skolem0003),inference(resolution,[status(thm)],[c309, reflexivity])).
% 0.96/1.14  cnf(c307,plain,skolem0001!=X643|skolem0003!=X642|abstraction(X643,X642),inference(resolution,[status(thm)],[c301, c4])).
% 0.96/1.14  cnf(c623,plain,skolem0001!=X644|abstraction(X644,skolem0003),inference(resolution,[status(thm)],[c307, reflexivity])).
% 0.96/1.14  cnf(c303,plain,skolem0001!=X639|skolem0002!=X640|human_person(X639,X640),inference(resolution,[status(thm)],[c12, c264])).
% 0.96/1.15  cnf(c621,plain,skolem0001!=X641|human_person(X641,skolem0002),inference(resolution,[status(thm)],[c303, reflexivity])).
% 0.96/1.15  cnf(c302,plain,skolem0001!=X636|skolem0003!=X637|relation(X636,X637),inference(resolution,[status(thm)],[c300, c3])).
% 0.96/1.15  cnf(c619,plain,skolem0001!=X638|relation(X638,skolem0003),inference(resolution,[status(thm)],[c302, reflexivity])).
% 0.96/1.15  cnf(c299,plain,skolem0001!=X634|skolem0003!=X633|relname(X634,X633),inference(resolution,[status(thm)],[c298, c2])).
% 0.96/1.15  cnf(c617,plain,skolem0001!=X635|relname(X635,skolem0003),inference(resolution,[status(thm)],[c299, reflexivity])).
% 0.96/1.15  cnf(c297,plain,skolem0001!=X631|skolem0005!=X630|unisex(X631,X630),inference(resolution,[status(thm)],[c295, c5])).
% 0.96/1.15  cnf(c615,plain,skolem0001!=X632|unisex(X632,skolem0005),inference(resolution,[status(thm)],[c297, reflexivity])).
% 0.96/1.15  cnf(c277,plain,male(skolem0001,skolem0002),inference(resolution,[status(thm)],[c224, c41])).
% 0.96/1.15  cnf(c296,plain,skolem0001!=X628|skolem0002!=X627|male(X628,X627),inference(resolution,[status(thm)],[c11, c277])).
% 0.96/1.15  cnf(c613,plain,skolem0001!=X629|male(X629,skolem0002),inference(resolution,[status(thm)],[c296, reflexivity])).
% 0.96/1.15  cnf(c292,plain,general(skolem0001,skolem0005),inference(resolution,[status(thm)],[c239, c283])).
% 0.96/1.15  cnf(c294,plain,skolem0001!=X624|skolem0005!=X625|general(X624,X625),inference(resolution,[status(thm)],[c292, c6])).
% 0.96/1.15  cnf(c611,plain,skolem0001!=X626|general(X626,skolem0005),inference(resolution,[status(thm)],[c294, reflexivity])).
% 0.96/1.15  cnf(c289,plain,nonhuman(skolem0001,skolem0005),inference(resolution,[status(thm)],[c236, c283])).
% 0.96/1.15  cnf(c291,plain,skolem0001!=X621|skolem0005!=X622|nonhuman(X621,X622),inference(resolution,[status(thm)],[c289, c7])).
% 0.96/1.15  cnf(c609,plain,skolem0001!=X623|nonhuman(X623,skolem0005),inference(resolution,[status(thm)],[c291, reflexivity])).
% 0.96/1.15  cnf(c290,plain,skolem0001!=X619|skolem0002!=X618|man(X619,X618),inference(resolution,[status(thm)],[c10, c41])).
% 0.96/1.15  cnf(c607,plain,skolem0001!=X620|man(X620,skolem0002),inference(resolution,[status(thm)],[c290, reflexivity])).
% 0.96/1.15  cnf(c602,plain,~accessible_world(skolem0005,X617)|of(X617,skolem0003,skolem0002),inference(resolution,[status(thm)],[c599, c154])).
% 0.96/1.15  cnf(c287,plain,skolem0001!=X615|skolem0005!=X614|thing(X615,X614),inference(resolution,[status(thm)],[c286, c8])).
% 0.96/1.15  cnf(c605,plain,skolem0001!=X616|thing(X616,skolem0005),inference(resolution,[status(thm)],[c287, reflexivity])).
% 0.96/1.15  cnf(c597,plain,~accessible_world(skolem0005,X613)|theme(X613,skolem0004,skolem0005),inference(resolution,[status(thm)],[c596, c127])).
% 0.96/1.15  cnf(c593,plain,~accessible_world(skolem0005,X612)|agent(X612,skolem0004,skolem0002),inference(resolution,[status(thm)],[c590, c91])).
% 0.96/1.15  cnf(c285,plain,skolem0001!=X610|skolem0005!=X609|abstraction(X610,X609),inference(resolution,[status(thm)],[c283, c4])).
% 0.96/1.15  cnf(c600,plain,skolem0001!=X611|abstraction(X611,skolem0005),inference(resolution,[status(thm)],[c285, reflexivity])).
% 0.96/1.15  cnf(c284,plain,skolem0001!=X605|skolem0005!=X604|proposition(X605,X604),inference(resolution,[status(thm)],[c9, c44])).
% 0.96/1.15  cnf(c594,plain,skolem0001!=X606|proposition(X606,skolem0005),inference(resolution,[status(thm)],[c284, reflexivity])).
% 0.96/1.15  fof(ax58,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&singleton(V,U))=>singleton(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax58)).
% 0.96/1.15  fof(c74,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~singleton(V,U))|singleton(W,U))))),inference(fof_nnf,[status(thm)],[ax58])).
% 0.96/1.15  fof(c75,plain,(![X31]:(![X32]:(![X33]:((~accessible_world(X32,X33)|~singleton(X32,X31))|singleton(X33,X31))))),inference(variable_rename,[status(thm)],[c74])).
% 0.96/1.15  cnf(c76,plain,~accessible_world(X367,X368)|~singleton(X367,X369)|singleton(X368,X369),inference(split_conjunct,[status(thm)],[c75])).
% 0.96/1.15  cnf(c476,plain,~accessible_world(skolem0005,X602)|singleton(X602,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c467, c76])).
% 0.96/1.15  cnf(c282,plain,skolem0001!=X599|skolem0005!=X600|relation(X599,X600),inference(resolution,[status(thm)],[c281, c3])).
% 0.96/1.15  cnf(c588,plain,skolem0001!=X601|relation(X601,skolem0005),inference(resolution,[status(thm)],[c282, reflexivity])).
% 0.96/1.15  fof(ax56,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonexistent(V,U))=>nonexistent(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax56)).
% 0.96/1.15  fof(c80,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonexistent(V,U))|nonexistent(W,U))))),inference(fof_nnf,[status(thm)],[ax56])).
% 0.96/1.15  fof(c81,plain,(![X37]:(![X38]:(![X39]:((~accessible_world(X38,X39)|~nonexistent(X38,X37))|nonexistent(X39,X37))))),inference(variable_rename,[status(thm)],[c80])).
% 0.96/1.15  cnf(c82,plain,~accessible_world(X403,X402)|~nonexistent(X403,X401)|nonexistent(X402,X401),inference(split_conjunct,[status(thm)],[c81])).
% 0.96/1.15  cnf(c473,plain,~accessible_world(skolem0005,X598)|nonexistent(X598,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c462, c82])).
% 0.96/1.15  cnf(c469,plain,~accessible_world(skolem0005,X597)|unisex(X597,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c461, c85])).
% 0.96/1.15  cnf(c465,plain,~accessible_world(skolem0005,X596)|thing(X596,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c459, c73])).
% 0.96/1.15  cnf(c279,plain,skolem0001!=X594|skolem0002!=X593|thing(X594,X593),inference(resolution,[status(thm)],[c8, c267])).
% 0.96/1.15  cnf(c586,plain,skolem0001!=X595|thing(X595,skolem0002),inference(resolution,[status(thm)],[c279, reflexivity])).
% 0.96/1.15  cnf(c463,plain,~accessible_world(skolem0005,X592)|specific(X592,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c458, c79])).
% 0.96/1.15  fof(ax60,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&eventuality(V,U))=>eventuality(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax60)).
% 0.96/1.15  fof(c68,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~eventuality(V,U))|eventuality(W,U))))),inference(fof_nnf,[status(thm)],[ax60])).
% 0.96/1.15  fof(c69,plain,(![X25]:(![X26]:(![X27]:((~accessible_world(X26,X27)|~eventuality(X26,X25))|eventuality(X27,X25))))),inference(variable_rename,[status(thm)],[c68])).
% 0.96/1.15  cnf(c70,plain,~accessible_world(X337,X335)|~eventuality(X337,X336)|eventuality(X335,X336),inference(split_conjunct,[status(thm)],[c69])).
% 0.96/1.15  cnf(c460,plain,~accessible_world(skolem0005,X591)|eventuality(X591,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c448, c70])).
% 0.96/1.15  fof(ax62,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&smoke(V,U))=>smoke(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax62)).
% 0.96/1.15  fof(c62,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~smoke(V,U))|smoke(W,U))))),inference(fof_nnf,[status(thm)],[ax62])).
% 0.96/1.15  fof(c63,plain,(![X19]:(![X20]:(![X21]:((~accessible_world(X20,X21)|~smoke(X20,X19))|smoke(X21,X19))))),inference(variable_rename,[status(thm)],[c62])).
% 0.96/1.15  cnf(c64,plain,~accessible_world(X321,X320)|~smoke(X321,X319)|smoke(X320,X319),inference(split_conjunct,[status(thm)],[c63])).
% 0.96/1.15  cnf(c452,plain,~accessible_world(skolem0005,X590)|smoke(X590,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c419, c64])).
% 0.96/1.15  cnf(c278,plain,skolem0001!=X588|skolem0004!=X587|thing(X588,X587),inference(resolution,[status(thm)],[c8, c258])).
% 0.96/1.15  cnf(c584,plain,skolem0001!=X589|thing(X589,skolem0004),inference(resolution,[status(thm)],[c278, reflexivity])).
% 0.96/1.15  cnf(c450,plain,~accessible_world(skolem0005,X586)|present(X586,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c418, c88])).
% 0.96/1.15  cnf(c449,plain,~accessible_world(skolem0005,X585)|event(X585,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c417, c67])).
% 0.96/1.15  cnf(c263,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c191, c256])).
% 0.96/1.15  cnf(c269,plain,skolem0001!=X583|skolem0004!=X582|unisex(X583,X582),inference(resolution,[status(thm)],[c5, c263])).
% 0.96/1.15  cnf(c582,plain,skolem0001!=X584|unisex(X584,skolem0004),inference(resolution,[status(thm)],[c269, reflexivity])).
% 0.96/1.15  cnf(c257,plain,skolem0001!=X577|skolem0003!=X576|forename(X577,X576),inference(resolution,[status(thm)],[c1, c43])).
% 0.96/1.15  cnf(c579,plain,skolem0001!=X581|forename(X581,skolem0003),inference(resolution,[status(thm)],[c257, reflexivity])).
% 0.96/1.15  cnf(c576,plain,~accessible_world(skolem0005,X580)|vincent_forename(X580,skolem0003),inference(resolution,[status(thm)],[c575, c151])).
% 0.96/1.15  cnf(c255,plain,skolem0001!=X573|skolem0003!=X572|vincent_forename(X573,X572),inference(resolution,[status(thm)],[c0, c42])).
% 0.96/1.15  cnf(c574,plain,skolem0001!=X579|vincent_forename(X579,skolem0003),inference(resolution,[status(thm)],[c255, reflexivity])).
% 0.96/1.15  fof(ax34,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relname(V,U))=>relname(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax34)).
% 0.96/1.15  fof(c146,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relname(V,U))|relname(W,U))))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.96/1.15  fof(c147,plain,(![X105]:(![X106]:(![X107]:((~accessible_world(X106,X107)|~relname(X106,X105))|relname(X107,X105))))),inference(variable_rename,[status(thm)],[c146])).
% 0.96/1.15  cnf(c148,plain,~accessible_world(X555,X554)|~relname(X555,X553)|relname(X554,X553),inference(split_conjunct,[status(thm)],[c147])).
% 0.96/1.15  cnf(c571,plain,~accessible_world(skolem0005,X578)|relname(X578,skolem0003),inference(resolution,[status(thm)],[c568, c148])).
% 0.96/1.15  cnf(c569,plain,~accessible_world(skolem0005,X575)|forename(X575,skolem0003),inference(resolution,[status(thm)],[c566, c145])).
% 0.96/1.15  cnf(c560,plain,~accessible_world(skolem0001,X571)|relname(X571,skolem0003),inference(resolution,[status(thm)],[c148, c298])).
% 0.96/1.15  fof(ax36,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&general(V,U))=>general(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax36)).
% 0.96/1.15  fof(c140,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~general(V,U))|general(W,U))))),inference(fof_nnf,[status(thm)],[ax36])).
% 0.96/1.15  fof(c141,plain,(![X99]:(![X100]:(![X101]:((~accessible_world(X100,X101)|~general(X100,X99))|general(X101,X99))))),inference(variable_rename,[status(thm)],[c140])).
% 0.96/1.15  cnf(c142,plain,~accessible_world(X542,X541)|~general(X542,X540)|general(X541,X540),inference(split_conjunct,[status(thm)],[c141])).
% 0.96/1.15  cnf(c555,plain,~accessible_world(skolem0005,X565)|general(X565,skolem0005),inference(resolution,[status(thm)],[c142, c521])).
% 0.96/1.15  cnf(c554,plain,~accessible_world(skolem0001,X564)|general(X564,skolem0003),inference(resolution,[status(thm)],[c142, c305])).
% 0.96/1.15  cnf(c553,plain,~accessible_world(skolem0001,X563)|general(X563,skolem0005),inference(resolution,[status(thm)],[c142, c292])).
% 0.96/1.15  cnf(c552,plain,~accessible_world(skolem0005,X559)|general(X559,skolem0003),inference(resolution,[status(thm)],[c142, c540])).
% 0.96/1.15  fof(ax37,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonhuman(V,U))=>nonhuman(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax37)).
% 0.96/1.15  fof(c137,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonhuman(V,U))|nonhuman(W,U))))),inference(fof_nnf,[status(thm)],[ax37])).
% 0.96/1.15  fof(c138,plain,(![X96]:(![X97]:(![X98]:((~accessible_world(X97,X98)|~nonhuman(X97,X96))|nonhuman(X98,X96))))),inference(variable_rename,[status(thm)],[c137])).
% 0.96/1.15  cnf(c139,plain,~accessible_world(X538,X539)|~nonhuman(X538,X537)|nonhuman(X539,X537),inference(split_conjunct,[status(thm)],[c138])).
% 0.96/1.15  cnf(c549,plain,~accessible_world(skolem0005,X558)|nonhuman(X558,skolem0003),inference(resolution,[status(thm)],[c539, c139])).
% 0.96/1.15  cnf(c547,plain,~accessible_world(skolem0005,X557)|nonhuman(X557,skolem0005),inference(resolution,[status(thm)],[c139, c520])).
% 0.96/1.15  cnf(c546,plain,~accessible_world(skolem0001,X556)|nonhuman(X556,skolem0005),inference(resolution,[status(thm)],[c139, c289])).
% 0.96/1.15  cnf(c545,plain,~accessible_world(skolem0001,X552)|nonhuman(X552,skolem0003),inference(resolution,[status(thm)],[c139, c304])).
% 0.96/1.15  fof(ax38,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&abstraction(V,U))=>abstraction(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax38)).
% 0.96/1.15  fof(c134,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~abstraction(V,U))|abstraction(W,U))))),inference(fof_nnf,[status(thm)],[ax38])).
% 0.96/1.15  fof(c135,plain,(![X93]:(![X94]:(![X95]:((~accessible_world(X94,X95)|~abstraction(X94,X93))|abstraction(X95,X93))))),inference(variable_rename,[status(thm)],[c134])).
% 0.96/1.15  cnf(c136,plain,~accessible_world(X532,X533)|~abstraction(X532,X534)|abstraction(X533,X534),inference(split_conjunct,[status(thm)],[c135])).
% 0.96/1.15  cnf(c541,plain,~accessible_world(skolem0005,X551)|abstraction(X551,skolem0003),inference(resolution,[status(thm)],[c536, c136])).
% 0.96/1.15  cnf(c537,plain,~accessible_world(skolem0005,X550)|relation(X550,skolem0003),inference(resolution,[status(thm)],[c535, c133])).
% 0.96/1.15  cnf(c533,plain,~accessible_world(skolem0001,X546)|abstraction(X546,skolem0005),inference(resolution,[status(thm)],[c136, c283])).
% 0.96/1.15  cnf(c532,plain,~accessible_world(skolem0001,X545)|abstraction(X545,skolem0003),inference(resolution,[status(thm)],[c136, c301])).
% 0.96/1.15  cnf(c531,plain,~accessible_world(skolem0005,X544)|abstraction(X544,skolem0005),inference(resolution,[status(thm)],[c136, c518])).
% 0.96/1.15  cnf(c528,plain,~accessible_world(skolem0005,X543)|relation(X543,skolem0005),inference(resolution,[status(thm)],[c133, c517])).
% 0.96/1.15  fof(ax30,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax30)).
% 0.96/1.15  fof(c159,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax30])).
% 0.96/1.15  fof(c160,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c159])).
% 0.96/1.15  fof(c161,plain,(![X117]:(![X118]:(~specific(X117,X118)|~general(X117,X118)))),inference(variable_rename,[status(thm)],[c160])).
% 0.96/1.15  cnf(c162,plain,~specific(X190,X191)|~general(X190,X191),inference(split_conjunct,[status(thm)],[c161])).
% 0.96/1.15  cnf(c550,plain,~specific(skolem0005,skolem0003),inference(resolution,[status(thm)],[c540, c162])).
% 0.96/1.15  cnf(c526,plain,~accessible_world(skolem0001,X535)|relation(X535,skolem0005),inference(resolution,[status(thm)],[c133, c281])).
% 0.96/1.15  cnf(c516,plain,~accessible_world(skolem0005,X531)|proposition(X531,skolem0005),inference(resolution,[status(thm)],[c514, c130])).
% 0.96/1.15  cnf(c529,plain,~specific(skolem0005,skolem0005),inference(resolution,[status(thm)],[c521, c162])).
% 0.96/1.15  cnf(c511,plain,~accessible_world(skolem0005,X519)|think_believe_consider(X519,skolem0004),inference(resolution,[status(thm)],[c509, c124])).
% 0.96/1.15  fof(ax43,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&male(V,U))=>male(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax43)).
% 0.96/1.15  fof(c119,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~male(V,U))|male(W,U))))),inference(fof_nnf,[status(thm)],[ax43])).
% 0.96/1.15  fof(c120,plain,(![X77]:(![X78]:(![X79]:((~accessible_world(X78,X79)|~male(X78,X77))|male(X79,X77))))),inference(variable_rename,[status(thm)],[c119])).
% 0.96/1.15  cnf(c121,plain,~accessible_world(X509,X510)|~male(X509,X508)|male(X510,X508),inference(split_conjunct,[status(thm)],[c120])).
% 0.96/1.15  cnf(c505,plain,~accessible_world(skolem0005,X517)|male(X517,skolem0002),inference(resolution,[status(thm)],[c121, c416])).
% 0.96/1.15  cnf(c504,plain,~accessible_world(skolem0001,X513)|male(X513,skolem0002),inference(resolution,[status(thm)],[c121, c277])).
% 0.96/1.15  fof(ax44,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&animate(V,U))=>animate(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax44)).
% 0.96/1.15  fof(c116,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~animate(V,U))|animate(W,U))))),inference(fof_nnf,[status(thm)],[ax44])).
% 0.96/1.15  fof(c117,plain,(![X74]:(![X75]:(![X76]:((~accessible_world(X75,X76)|~animate(X75,X74))|animate(X76,X74))))),inference(variable_rename,[status(thm)],[c116])).
% 0.96/1.15  cnf(c118,plain,~accessible_world(X506,X507)|~animate(X506,X505)|animate(X507,X505),inference(split_conjunct,[status(thm)],[c117])).
% 0.96/1.15  cnf(c503,plain,~accessible_world(skolem0005,X512)|animate(X512,skolem0002),inference(resolution,[status(thm)],[c118, c427])).
% 0.96/1.15  cnf(c502,plain,~accessible_world(skolem0001,X511)|animate(X511,skolem0002),inference(resolution,[status(thm)],[c118, c276])).
% 0.96/1.15  fof(ax45,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human(V,U))=>human(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax45)).
% 0.96/1.15  fof(c113,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~human(V,U))|human(W,U))))),inference(fof_nnf,[status(thm)],[ax45])).
% 0.96/1.15  fof(c114,plain,(![X71]:(![X72]:(![X73]:((~accessible_world(X72,X73)|~human(X72,X71))|human(X73,X71))))),inference(variable_rename,[status(thm)],[c113])).
% 0.96/1.15  cnf(c115,plain,~accessible_world(X501,X499)|~human(X501,X500)|human(X499,X500),inference(split_conjunct,[status(thm)],[c114])).
% 0.96/1.15  cnf(c500,plain,~accessible_world(skolem0001,X504)|human(X504,skolem0002),inference(resolution,[status(thm)],[c115, c274])).
% 0.96/1.15  cnf(c499,plain,~accessible_world(skolem0005,X503)|human(X503,skolem0002),inference(resolution,[status(thm)],[c115, c426])).
% 0.96/1.15  fof(ax46,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&living(V,U))=>living(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax46)).
% 0.96/1.15  fof(c110,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~living(V,U))|living(W,U))))),inference(fof_nnf,[status(thm)],[ax46])).
% 0.96/1.15  fof(c111,plain,(![X68]:(![X69]:(![X70]:((~accessible_world(X69,X70)|~living(X69,X68))|living(X70,X68))))),inference(variable_rename,[status(thm)],[c110])).
% 0.96/1.15  cnf(c112,plain,~accessible_world(X495,X493)|~living(X495,X494)|living(X493,X494),inference(split_conjunct,[status(thm)],[c111])).
% 0.96/1.15  cnf(c496,plain,~accessible_world(skolem0005,X502)|living(X502,skolem0002),inference(resolution,[status(thm)],[c112, c434])).
% 0.96/1.15  cnf(c495,plain,~accessible_world(skolem0001,X498)|living(X498,skolem0002),inference(resolution,[status(thm)],[c112, c273])).
% 0.96/1.15  fof(ax47,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&impartial(V,U))=>impartial(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax47)).
% 0.96/1.15  fof(c107,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~impartial(V,U))|impartial(W,U))))),inference(fof_nnf,[status(thm)],[ax47])).
% 0.96/1.15  fof(c108,plain,(![X65]:(![X66]:(![X67]:((~accessible_world(X66,X67)|~impartial(X66,X65))|impartial(X67,X65))))),inference(variable_rename,[status(thm)],[c107])).
% 0.96/1.15  cnf(c109,plain,~accessible_world(X492,X491)|~impartial(X492,X490)|impartial(X491,X490),inference(split_conjunct,[status(thm)],[c108])).
% 0.96/1.15  cnf(c494,plain,~accessible_world(skolem0005,X497)|impartial(X497,skolem0002),inference(resolution,[status(thm)],[c109, c435])).
% 0.96/1.15  cnf(c493,plain,~accessible_world(skolem0001,X496)|impartial(X496,skolem0002),inference(resolution,[status(thm)],[c109, c272])).
% 0.96/1.15  fof(ax48,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&existent(V,U))=>existent(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 0.96/1.15  fof(c104,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~existent(V,U))|existent(W,U))))),inference(fof_nnf,[status(thm)],[ax48])).
% 0.96/1.15  fof(c105,plain,(![X62]:(![X63]:(![X64]:((~accessible_world(X63,X64)|~existent(X63,X62))|existent(X64,X62))))),inference(variable_rename,[status(thm)],[c104])).
% 0.96/1.15  cnf(c106,plain,~accessible_world(X487,X486)|~existent(X487,X485)|existent(X486,X485),inference(split_conjunct,[status(thm)],[c105])).
% 0.96/1.15  cnf(c491,plain,~accessible_world(skolem0005,X489)|existent(X489,skolem0002),inference(resolution,[status(thm)],[c106, c442])).
% 0.96/1.15  cnf(c490,plain,~accessible_world(skolem0001,X488)|existent(X488,skolem0002),inference(resolution,[status(thm)],[c106, c271])).
% 0.96/1.15  fof(ax49,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&entity(V,U))=>entity(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 0.96/1.15  fof(c101,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~entity(V,U))|entity(W,U))))),inference(fof_nnf,[status(thm)],[ax49])).
% 0.96/1.15  fof(c102,plain,(![X59]:(![X60]:(![X61]:((~accessible_world(X60,X61)|~entity(X60,X59))|entity(X61,X59))))),inference(variable_rename,[status(thm)],[c101])).
% 0.96/1.15  cnf(c103,plain,~accessible_world(X478,X479)|~entity(X478,X480)|entity(X479,X480),inference(split_conjunct,[status(thm)],[c102])).
% 0.96/1.15  cnf(c487,plain,~accessible_world(skolem0001,X484)|entity(X484,skolem0002),inference(resolution,[status(thm)],[c103, c266])).
% 0.96/1.15  cnf(c486,plain,~accessible_world(skolem0005,X483)|entity(X483,skolem0002),inference(resolution,[status(thm)],[c103, c433])).
% 0.96/1.15  fof(ax50,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&organism(V,U))=>organism(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax50)).
% 0.96/1.15  fof(c98,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~organism(V,U))|organism(W,U))))),inference(fof_nnf,[status(thm)],[ax50])).
% 0.96/1.15  fof(c99,plain,(![X56]:(![X57]:(![X58]:((~accessible_world(X57,X58)|~organism(X57,X56))|organism(X58,X56))))),inference(variable_rename,[status(thm)],[c98])).
% 0.96/1.15  cnf(c100,plain,~accessible_world(X477,X475)|~organism(X477,X476)|organism(X475,X476),inference(split_conjunct,[status(thm)],[c99])).
% 0.96/1.15  cnf(c485,plain,~accessible_world(skolem0001,X482)|organism(X482,skolem0002),inference(resolution,[status(thm)],[c100, c265])).
% 0.96/1.15  cnf(c484,plain,~accessible_world(skolem0005,X481)|organism(X481,skolem0002),inference(resolution,[status(thm)],[c100, c429])).
% 0.96/1.15  fof(ax51,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human_person(V,U))=>human_person(W,U))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax51)).
% 0.96/1.15  fof(c95,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~human_person(V,U))|human_person(W,U))))),inference(fof_nnf,[status(thm)],[ax51])).
% 0.96/1.15  fof(c96,plain,(![X53]:(![X54]:(![X55]:((~accessible_world(X54,X55)|~human_person(X54,X53))|human_person(X55,X53))))),inference(variable_rename,[status(thm)],[c95])).
% 0.96/1.15  cnf(c97,plain,~accessible_world(X472,X470)|~human_person(X472,X471)|human_person(X470,X471),inference(split_conjunct,[status(thm)],[c96])).
% 0.96/1.15  cnf(c482,plain,~accessible_world(skolem0001,X474)|human_person(X474,skolem0002),inference(resolution,[status(thm)],[c97, c264])).
% 0.96/1.15  cnf(c481,plain,~accessible_world(skolem0005,X473)|human_person(X473,skolem0002),inference(resolution,[status(thm)],[c97, c420])).
% 0.96/1.15  cnf(c422,plain,~accessible_world(skolem0005,X465)|man(X465,skolem0002),inference(resolution,[status(thm)],[c415, c94])).
% 0.96/1.15  fof(ax28,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax28)).
% 0.96/1.15  fof(c167,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax28])).
% 0.96/1.15  fof(c168,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c167])).
% 0.96/1.15  fof(c169,plain,(![X121]:(![X122]:(~existent(X121,X122)|~nonexistent(X121,X122)))),inference(variable_rename,[status(thm)],[c168])).
% 0.96/1.15  cnf(c170,plain,~existent(X194,X195)|~nonexistent(X194,X195),inference(split_conjunct,[status(thm)],[c169])).
% 0.96/1.15  cnf(c472,plain,~existent(skolem0005,skolem0006(skolem0002)),inference(resolution,[status(thm)],[c462, c170])).
% 0.96/1.15  fof(ax29,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax29)).
% 0.96/1.15  fof(c163,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax29])).
% 0.96/1.15  fof(c164,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c163])).
% 0.96/1.15  fof(c165,plain,(![X119]:(![X120]:(~nonhuman(X119,X120)|~human(X119,X120)))),inference(variable_rename,[status(thm)],[c164])).
% 0.96/1.15  cnf(c166,plain,~nonhuman(X192,X193)|~human(X192,X193),inference(split_conjunct,[status(thm)],[c165])).
% 0.96/1.15  cnf(c430,plain,~nonhuman(skolem0005,skolem0002),inference(resolution,[status(thm)],[c426, c166])).
% 0.96/1.15  fof(ax31,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 0.96/1.15  fof(c155,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax31])).
% 0.96/1.15  fof(c156,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c155])).
% 0.96/1.15  fof(c157,plain,(![X115]:(![X116]:(~unisex(X115,X116)|~male(X115,X116)))),inference(variable_rename,[status(thm)],[c156])).
% 0.96/1.15  cnf(c158,plain,~unisex(X185,X184)|~male(X185,X184),inference(split_conjunct,[status(thm)],[c157])).
% 0.96/1.15  cnf(c423,plain,~unisex(skolem0005,skolem0002),inference(resolution,[status(thm)],[c416, c158])).
% 0.96/1.15  cnf(c412,plain,~accessible_world(skolem0005,X439)|present(X439,skolem0004),inference(resolution,[status(thm)],[c411, c88])).
% 0.96/1.15  cnf(c408,plain,~accessible_world(skolem0005,X430)|unisex(X430,skolem0005),inference(resolution,[status(thm)],[c406, c85])).
% 0.96/1.15  cnf(c403,plain,~accessible_world(skolem0005,X429)|unisex(X429,skolem0003),inference(resolution,[status(thm)],[c401, c85])).
% 0.96/1.15  cnf(c400,plain,~accessible_world(skolem0005,X422)|unisex(X422,skolem0004),inference(resolution,[status(thm)],[c85, c325])).
% 0.96/1.15  cnf(c398,plain,~accessible_world(skolem0001,X420)|unisex(X420,skolem0004),inference(resolution,[status(thm)],[c85, c263])).
% 0.96/1.15  cnf(c394,plain,~accessible_world(skolem0005,X411)|nonexistent(X411,skolem0004),inference(resolution,[status(thm)],[c82, c327])).
% 0.96/1.15  cnf(c393,plain,~accessible_world(skolem0001,X404)|nonexistent(X404,skolem0004),inference(resolution,[status(thm)],[c82, c261])).
% 0.96/1.15  cnf(c391,plain,~accessible_world(skolem0005,X400)|specific(X400,skolem0002),inference(resolution,[status(thm)],[c390, c79])).
% 0.96/1.15  cnf(c388,plain,~accessible_world(skolem0005,X399)|specific(X399,skolem0004),inference(resolution,[status(thm)],[c79, c326])).
% 0.96/1.15  cnf(c386,plain,~accessible_world(skolem0001,X393)|specific(X393,skolem0004),inference(resolution,[status(thm)],[c79, c260])).
% 0.96/1.15  cnf(c369,plain,~accessible_world(skolem0005,X389)|singleton(X389,skolem0002),inference(resolution,[status(thm)],[c76, c358])).
% 0.96/1.15  cnf(c368,plain,~accessible_world(skolem0005,X384)|singleton(X384,skolem0004),inference(resolution,[status(thm)],[c76, c332])).
% 0.96/1.15  cnf(c367,plain,~accessible_world(skolem0005,X383)|singleton(X383,skolem0003),inference(resolution,[status(thm)],[c76, c347])).
% 0.96/1.15  cnf(c366,plain,~accessible_world(skolem0001,X382)|singleton(X382,skolem0005),inference(resolution,[status(thm)],[c76, c288])).
% 0.96/1.15  cnf(c365,plain,~accessible_world(skolem0001,X377)|singleton(X377,skolem0003),inference(resolution,[status(thm)],[c76, c314])).
% 0.96/1.15  cnf(c364,plain,~accessible_world(skolem0001,X376)|singleton(X376,skolem0004),inference(resolution,[status(thm)],[c76, c259])).
% 0.96/1.15  cnf(c363,plain,~accessible_world(skolem0005,X375)|singleton(X375,skolem0005),inference(resolution,[status(thm)],[c76, c351])).
% 0.96/1.15  cnf(c362,plain,~accessible_world(skolem0001,X370)|singleton(X370,skolem0002),inference(resolution,[status(thm)],[c76, c268])).
% 0.96/1.15  cnf(c356,plain,~accessible_world(skolem0005,X366)|thing(X366,skolem0002),inference(resolution,[status(thm)],[c355, c73])).
% 0.96/1.15  cnf(c349,plain,~accessible_world(skolem0005,X365)|thing(X365,skolem0005),inference(resolution,[status(thm)],[c348, c73])).
% 0.96/1.15  cnf(c345,plain,~accessible_world(skolem0005,X364)|thing(X364,skolem0003),inference(resolution,[status(thm)],[c343, c73])).
% 0.96/1.15  cnf(c342,plain,~accessible_world(skolem0001,X359)|thing(X359,skolem0004),inference(resolution,[status(thm)],[c73, c258])).
% 0.96/1.15  cnf(c338,plain,~accessible_world(skolem0005,X347)|thing(X347,skolem0004),inference(resolution,[status(thm)],[c73, c328])).
% 0.96/1.15  cnf(c335,plain,~accessible_world(skolem0005,X343)|eventuality(X343,skolem0004),inference(resolution,[status(thm)],[c70, c322])).
% 0.96/1.15  cnf(c334,plain,~accessible_world(skolem0001,X338)|eventuality(X338,skolem0004),inference(resolution,[status(thm)],[c70, c256])).
% 0.96/1.15  cnf(c323,plain,~accessible_world(skolem0005,X334)|event(X334,skolem0004),inference(resolution,[status(thm)],[c321, c67])).
% 0.96/1.15  cnf(c330,plain,~existent(skolem0005,skolem0004),inference(resolution,[status(thm)],[c327, c170])).
% 0.96/1.15  cnf(c32,axiom,X310!=X309|~actual_world(X310)|actual_world(X309),theory(equality)).
% 0.96/1.15  fof(ax1,axiom,(![U]:(![V]:(vincent_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 0.96/1.15  fof(c249,plain,(![U]:(![V]:(~vincent_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.96/1.15  fof(c250,plain,(![X175]:(![X176]:(~vincent_forename(X175,X176)|forename(X175,X176)))),inference(variable_rename,[status(thm)],[c249])).
% 0.96/1.15  cnf(c251,plain,~vincent_forename(X300,X301)|forename(X300,X301),inference(split_conjunct,[status(thm)],[c250])).
% 0.96/1.15  cnf(c310,plain,~specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c305, c162])).
% 0.96/1.15  cnf(c293,plain,~specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c292, c162])).
% 0.96/1.15  cnf(c280,plain,~unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c277, c158])).
% 0.96/1.15  cnf(c275,plain,~nonhuman(skolem0001,skolem0002),inference(resolution,[status(thm)],[c274, c166])).
% 0.96/1.15  cnf(c262,plain,~existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c261, c170])).
% 0.96/1.15  fof(ax27,axiom,(![U]:(![V]:(smoke(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax27)).
% 0.96/1.15  fof(c171,plain,(![U]:(![V]:(~smoke(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.96/1.15  fof(c172,plain,(![X123]:(![X124]:(~smoke(X123,X124)|event(X123,X124)))),inference(variable_rename,[status(thm)],[c171])).
% 0.96/1.15  cnf(c173,plain,~smoke(X196,X197)|event(X196,X197),inference(split_conjunct,[status(thm)],[c172])).
% 0.96/1.15  cnf(transitivity,axiom,X182!=X181|X181!=X183|X182=X183,theory(equality)).
% 0.96/1.15  cnf(symmetry,axiom,X179!=X178|X178=X179,theory(equality)).
% 0.96/1.15  cnf(c39,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c38])).
% 0.96/1.15  % SZS output end Saturation
% 0.96/1.15  
% 0.96/1.15  % Initial clauses    : 116
% 0.96/1.15  % Processed clauses  : 533
% 0.96/1.15  % Factors computed   : 16
% 0.96/1.15  % Resolvents computed: 558
% 0.96/1.15  % Tautologies deleted: 3
% 0.96/1.15  % Forward subsumed   : 154
% 0.96/1.15  % Backward subsumed  : 2
% 0.96/1.15  % -------- CPU Time ---------
% 0.96/1.15  % User time          : 0.779 s
% 0.96/1.15  % System time        : 0.015 s
% 0.96/1.15  % Total time         : 0.794 s
%------------------------------------------------------------------------------