PyRes---1.5.CSA-Sat.s

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

% Computer : n002.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:42 EDT 2024

% Result   : CounterSatisfiable 1.49s 1.66s
% Output   : Saturation 1.53s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12  % Problem  : NLP225+1 : TPTP v8.1.2. Released v2.4.0.
% 0.08/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34  % Computer : n002.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Wed May  8 13:37:23 EDT 2024
% 0.12/0.34  % CPUTime  : 
% 1.49/1.66  % Version:  1.5
% 1.49/1.66  % SZS status CounterSatisfiable
% 1.49/1.66  % SZS output start Saturation
% 1.49/1.66  fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((((((of(U,V,W)&jules_forename(U,V))&forename(U,V))&of(U,X,W))&man(U,W))&vincent_forename(U,X))&forename(U,X))&proposition(U,Z))&agent(U,Y,W))&theme(U,Y,Z))&event(U,Y))&present(U,Y))&think_believe_consider(U,Y))&accessible_world(U,Z))&(![X3]:(man(Z,X3)=>(?[X4]:(((event(Z,X4)&agent(Z,X4,X3))&present(Z,X4))&smoke(Z,X4))))))&man(U,X1))&state(U,X2))&be(U,X2,W,X1)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 1.49/1.66  fof(c36,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((((((of(U,V,W)&jules_forename(U,V))&forename(U,V))&of(U,X,W))&man(U,W))&vincent_forename(U,X))&forename(U,X))&proposition(U,Z))&agent(U,Y,W))&theme(U,Y,Z))&event(U,Y))&present(U,Y))&think_believe_consider(U,Y))&accessible_world(U,Z))&(![X3]:(man(Z,X3)=>(?[X4]:(((event(Z,X4)&agent(Z,X4,X3))&present(Z,X4))&smoke(Z,X4))))))&man(U,X1))&state(U,X2))&be(U,X2,W,X1))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 1.49/1.66  fof(c37,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((((((of(U,V,W)&jules_forename(U,V))&forename(U,V))&of(U,X,W))&man(U,W))&vincent_forename(U,X))&forename(U,X))&proposition(U,Z))&agent(U,Y,W))&theme(U,Y,Z))&event(U,Y))&present(U,Y))&think_believe_consider(U,Y))&accessible_world(U,Z))&(![X3]:(~man(Z,X3)|(?[X4]:(((event(Z,X4)&agent(Z,X4,X3))&present(Z,X4))&smoke(Z,X4))))))&man(U,X1))&state(U,X2))&be(U,X2,W,X1))))))))))),inference(fof_nnf,[status(thm)],[c36])).
% 1.49/1.66  fof(c38,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:(((((((((((((((((of(X2,X3,X4)&jules_forename(X2,X3))&forename(X2,X3))&of(X2,X5,X4))&man(X2,X4))&vincent_forename(X2,X5))&forename(X2,X5))&proposition(X2,X7))&agent(X2,X6,X4))&theme(X2,X6,X7))&event(X2,X6))&present(X2,X6))&think_believe_consider(X2,X6))&accessible_world(X2,X7))&(![X10]:(~man(X7,X10)|(?[X11]:(((event(X7,X11)&agent(X7,X11,X10))&present(X7,X11))&smoke(X7,X11))))))&man(X2,X8))&state(X2,X9))&be(X2,X9,X4,X8))))))))))),inference(variable_rename,[status(thm)],[c37])).
% 1.49/1.66  fof(c40,negated_conjecture,(![X10]:(actual_world(skolem0001)&(((((((((((((((((of(skolem0001,skolem0002,skolem0003)&jules_forename(skolem0001,skolem0002))&forename(skolem0001,skolem0002))&of(skolem0001,skolem0004,skolem0003))&man(skolem0001,skolem0003))&vincent_forename(skolem0001,skolem0004))&forename(skolem0001,skolem0004))&proposition(skolem0001,skolem0006))&agent(skolem0001,skolem0005,skolem0003))&theme(skolem0001,skolem0005,skolem0006))&event(skolem0001,skolem0005))&present(skolem0001,skolem0005))&think_believe_consider(skolem0001,skolem0005))&accessible_world(skolem0001,skolem0006))&(~man(skolem0006,X10)|(((event(skolem0006,skolem0009(X10))&agent(skolem0006,skolem0009(X10),X10))&present(skolem0006,skolem0009(X10)))&smoke(skolem0006,skolem0009(X10)))))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0003,skolem0007)))),inference(shift_quantors,[status(thm)],[fof(c39,negated_conjecture,(actual_world(skolem0001)&(((((((((((((((((of(skolem0001,skolem0002,skolem0003)&jules_forename(skolem0001,skolem0002))&forename(skolem0001,skolem0002))&of(skolem0001,skolem0004,skolem0003))&man(skolem0001,skolem0003))&vincent_forename(skolem0001,skolem0004))&forename(skolem0001,skolem0004))&proposition(skolem0001,skolem0006))&agent(skolem0001,skolem0005,skolem0003))&theme(skolem0001,skolem0005,skolem0006))&event(skolem0001,skolem0005))&present(skolem0001,skolem0005))&think_believe_consider(skolem0001,skolem0005))&accessible_world(skolem0001,skolem0006))&(![X10]:(~man(skolem0006,X10)|(((event(skolem0006,skolem0009(X10))&agent(skolem0006,skolem0009(X10),X10))&present(skolem0006,skolem0009(X10)))&smoke(skolem0006,skolem0009(X10))))))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0003,skolem0007))),inference(skolemize,[status(esa)],[c38])).])).
% 1.49/1.66  fof(c41,negated_conjecture,(![X10]:(actual_world(skolem0001)&(((((((((((((((((of(skolem0001,skolem0002,skolem0003)&jules_forename(skolem0001,skolem0002))&forename(skolem0001,skolem0002))&of(skolem0001,skolem0004,skolem0003))&man(skolem0001,skolem0003))&vincent_forename(skolem0001,skolem0004))&forename(skolem0001,skolem0004))&proposition(skolem0001,skolem0006))&agent(skolem0001,skolem0005,skolem0003))&theme(skolem0001,skolem0005,skolem0006))&event(skolem0001,skolem0005))&present(skolem0001,skolem0005))&think_believe_consider(skolem0001,skolem0005))&accessible_world(skolem0001,skolem0006))&((((~man(skolem0006,X10)|event(skolem0006,skolem0009(X10)))&(~man(skolem0006,X10)|agent(skolem0006,skolem0009(X10),X10)))&(~man(skolem0006,X10)|present(skolem0006,skolem0009(X10))))&(~man(skolem0006,X10)|smoke(skolem0006,skolem0009(X10)))))&man(skolem0001,skolem0007))&state(skolem0001,skolem0008))&be(skolem0001,skolem0008,skolem0003,skolem0007)))),inference(distribute,[status(thm)],[c40])).
% 1.49/1.66  cnf(c56,negated_conjecture,accessible_world(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.66  cnf(c52,negated_conjecture,theme(skolem0001,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.66  fof(ax37,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&theme(W,U,V))=>theme(X,U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 1.49/1.66  fof(c167,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~theme(W,U,V))|theme(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax37])).
% 1.49/1.66  fof(c168,plain,(![X123]:(![X124]:(![X125]:(![X126]:((~accessible_world(X125,X126)|~theme(X125,X123,X124))|theme(X126,X123,X124)))))),inference(variable_rename,[status(thm)],[c167])).
% 1.49/1.66  cnf(c169,plain,~accessible_world(X627,X626)|~theme(X627,X629,X628)|theme(X626,X629,X628),inference(split_conjunct,[status(thm)],[c168])).
% 1.49/1.66  cnf(c778,plain,~accessible_world(skolem0001,X892)|theme(X892,skolem0005,skolem0006),inference(resolution,[status(thm)],[c169, c52])).
% 1.49/1.66  cnf(c1010,plain,theme(skolem0006,skolem0005,skolem0006),inference(resolution,[status(thm)],[c778, c56])).
% 1.49/1.66  fof(ax69,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/sandbox2/benchmark/theBenchmark.p', ax69)).
% 1.49/1.66  fof(c71,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)],[ax69])).
% 1.49/1.66  fof(c72,plain,(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:((((((((~think_believe_consider(X20,X21)|~proposition(X20,X24))|~theme(X20,X21,X24))|~agent(X20,X21,X23))|~think_believe_consider(X20,X22))|~proposition(X20,X25))|~theme(X20,X22,X25))|~agent(X20,X22,X23))|X24=X25))))))),inference(variable_rename,[status(thm)],[c71])).
% 1.49/1.66  cnf(c73,plain,~think_believe_consider(X482,X480)|~proposition(X482,X483)|~theme(X482,X480,X483)|~agent(X482,X480,X479)|~think_believe_consider(X482,X481)|~proposition(X482,X484)|~theme(X482,X481,X484)|~agent(X482,X481,X479)|X483=X484,inference(split_conjunct,[status(thm)],[c72])).
% 1.49/1.66  fof(ax39,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&agent(W,U,V))=>agent(X,U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 1.49/1.66  fof(c161,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~agent(W,U,V))|agent(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax39])).
% 1.49/1.66  fof(c162,plain,(![X116]:(![X117]:(![X118]:(![X119]:((~accessible_world(X118,X119)|~agent(X118,X116,X117))|agent(X119,X116,X117)))))),inference(variable_rename,[status(thm)],[c161])).
% 1.49/1.66  cnf(c163,plain,~accessible_world(X615,X614)|~agent(X615,X616,X613)|agent(X614,X616,X613),inference(split_conjunct,[status(thm)],[c162])).
% 1.49/1.66  cnf(reflexivity,axiom,X201=X201,theory(equality)).
% 1.49/1.66  cnf(c63,negated_conjecture,be(skolem0001,skolem0008,skolem0003,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.66  fof(ax71,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax71)).
% 1.49/1.67  fof(c64,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax71])).
% 1.49/1.67  fof(c65,plain,(![X12]:(![X13]:(![X14]:(![X15]:(~be(X12,X13,X14,X15)|X14=X15))))),inference(variable_rename,[status(thm)],[c64])).
% 1.49/1.67  cnf(c66,plain,~be(X378,X380,X381,X379)|X381=X379,inference(split_conjunct,[status(thm)],[c65])).
% 1.49/1.67  cnf(c415,plain,skolem0003=skolem0007,inference(resolution,[status(thm)],[c66, c63])).
% 1.49/1.67  cnf(c51,negated_conjecture,agent(skolem0001,skolem0005,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c31,axiom,X430!=X431|X429!=X428|X432!=X433|~agent(X430,X429,X432)|agent(X431,X428,X433),theory(equality)).
% 1.49/1.67  cnf(c479,plain,skolem0001!=X1011|skolem0005!=X1012|skolem0003!=X1013|agent(X1011,X1012,X1013),inference(resolution,[status(thm)],[c31, c51])).
% 1.49/1.67  cnf(c1090,plain,skolem0001!=X1322|skolem0005!=X1323|agent(X1322,X1323,skolem0007),inference(resolution,[status(thm)],[c479, c415])).
% 1.49/1.67  cnf(c1315,plain,skolem0001!=X1324|agent(X1324,skolem0005,skolem0007),inference(resolution,[status(thm)],[c1090, reflexivity])).
% 1.49/1.67  cnf(c1316,plain,agent(skolem0001,skolem0005,skolem0007),inference(resolution,[status(thm)],[c1315, reflexivity])).
% 1.49/1.67  cnf(c1317,plain,~accessible_world(skolem0001,X1325)|agent(X1325,skolem0005,skolem0007),inference(resolution,[status(thm)],[c1316, c163])).
% 1.49/1.67  cnf(c1320,plain,agent(skolem0006,skolem0005,skolem0007),inference(resolution,[status(thm)],[c1317, c56])).
% 1.49/1.67  cnf(c1323,plain,~think_believe_consider(skolem0006,X1457)|~proposition(skolem0006,X1458)|~theme(skolem0006,X1457,X1458)|~agent(skolem0006,X1457,skolem0007)|~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,X1459)|~theme(skolem0006,skolem0005,X1459)|X1458=X1459,inference(resolution,[status(thm)],[c1320, c73])).
% 1.49/1.67  cnf(c1496,plain,~think_believe_consider(skolem0006,X1716)|~proposition(skolem0006,X1717)|~theme(skolem0006,X1716,X1717)|~agent(skolem0006,X1716,skolem0007)|~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,skolem0006)|X1717=skolem0006,inference(resolution,[status(thm)],[c1323, c1010])).
% 1.49/1.67  cnf(c58,negated_conjecture,~man(skolem0006,X464)|agent(skolem0006,skolem0009(X464),X464),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c47,negated_conjecture,man(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  fof(ax59,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&man(V,U))=>man(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax59)).
% 1.49/1.67  fof(c101,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~man(V,U))|man(W,U))))),inference(fof_nnf,[status(thm)],[ax59])).
% 1.49/1.67  fof(c102,plain,(![X55]:(![X56]:(![X57]:((~accessible_world(X56,X57)|~man(X56,X55))|man(X57,X55))))),inference(variable_rename,[status(thm)],[c101])).
% 1.49/1.67  cnf(c103,plain,~accessible_world(X523,X522)|~man(X523,X521)|man(X522,X521),inference(split_conjunct,[status(thm)],[c102])).
% 1.49/1.67  cnf(c576,plain,~accessible_world(skolem0001,X571)|man(X571,skolem0003),inference(resolution,[status(thm)],[c103, c47])).
% 1.49/1.67  cnf(c677,plain,man(skolem0006,skolem0003),inference(resolution,[status(thm)],[c576, c56])).
% 1.49/1.67  cnf(c683,plain,agent(skolem0006,skolem0009(skolem0003),skolem0003),inference(resolution,[status(thm)],[c677, c58])).
% 1.49/1.67  cnf(c770,plain,~accessible_world(skolem0001,X883)|agent(X883,skolem0005,skolem0003),inference(resolution,[status(thm)],[c163, c51])).
% 1.49/1.67  cnf(c1000,plain,agent(skolem0006,skolem0005,skolem0003),inference(resolution,[status(thm)],[c770, c56])).
% 1.49/1.67  cnf(c1005,plain,~think_believe_consider(skolem0006,X1348)|~proposition(skolem0006,X1349)|~theme(skolem0006,X1348,X1349)|~agent(skolem0006,X1348,skolem0003)|~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,X1350)|~theme(skolem0006,skolem0005,X1350)|X1349=X1350,inference(resolution,[status(thm)],[c1000, c73])).
% 1.49/1.67  cnf(c1346,plain,~think_believe_consider(skolem0006,X1493)|~proposition(skolem0006,X1494)|~theme(skolem0006,X1493,X1494)|~agent(skolem0006,X1493,skolem0003)|~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,skolem0006)|X1494=skolem0006,inference(resolution,[status(thm)],[c1005, c1010])).
% 1.49/1.67  cnf(c1525,plain,~think_believe_consider(skolem0006,skolem0009(skolem0003))|~proposition(skolem0006,X1715)|~theme(skolem0006,skolem0009(skolem0003),X1715)|~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,skolem0006)|X1715=skolem0006,inference(resolution,[status(thm)],[c1346, c683])).
% 1.49/1.67  cnf(c1319,plain,~think_believe_consider(skolem0001,X1442)|~proposition(skolem0001,X1443)|~theme(skolem0001,X1442,X1443)|~agent(skolem0001,X1442,skolem0007)|~think_believe_consider(skolem0001,skolem0005)|~proposition(skolem0001,X1444)|~theme(skolem0001,skolem0005,X1444)|X1443=X1444,inference(resolution,[status(thm)],[c1316, c73])).
% 1.49/1.67  cnf(c1490,plain,~think_believe_consider(skolem0001,X1712)|~proposition(skolem0001,X1713)|~theme(skolem0001,X1712,X1713)|~agent(skolem0001,X1712,skolem0007)|~think_believe_consider(skolem0001,skolem0005)|~proposition(skolem0001,skolem0006)|X1713=skolem0006,inference(resolution,[status(thm)],[c1319, c52])).
% 1.49/1.67  cnf(symmetry,axiom,X203!=X202|X202=X203,theory(equality)).
% 1.49/1.67  cnf(c416,plain,skolem0007=skolem0003,inference(resolution,[status(thm)],[c415, symmetry])).
% 1.49/1.67  cnf(c61,negated_conjecture,man(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c575,plain,~accessible_world(skolem0001,X555)|man(X555,skolem0007),inference(resolution,[status(thm)],[c103, c61])).
% 1.49/1.67  cnf(c605,plain,man(skolem0006,skolem0007),inference(resolution,[status(thm)],[c575, c56])).
% 1.49/1.67  cnf(c611,plain,agent(skolem0006,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c605, c58])).
% 1.49/1.67  cnf(c773,plain,skolem0006!=X1263|skolem0009(skolem0007)!=X1264|skolem0007!=X1265|agent(X1263,X1264,X1265),inference(resolution,[status(thm)],[c611, c31])).
% 1.49/1.67  cnf(c1273,plain,skolem0006!=X1394|skolem0007!=X1393|agent(X1394,skolem0009(skolem0007),X1393),inference(resolution,[status(thm)],[c773, reflexivity])).
% 1.49/1.67  cnf(c1381,plain,skolem0006!=X1395|agent(X1395,skolem0009(skolem0007),skolem0003),inference(resolution,[status(thm)],[c1273, c416])).
% 1.49/1.67  cnf(c1383,plain,agent(skolem0006,skolem0009(skolem0007),skolem0003),inference(resolution,[status(thm)],[c1381, reflexivity])).
% 1.49/1.67  cnf(c1523,plain,~think_believe_consider(skolem0006,skolem0009(skolem0007))|~proposition(skolem0006,X1711)|~theme(skolem0006,skolem0009(skolem0007),X1711)|~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,skolem0006)|X1711=skolem0006,inference(resolution,[status(thm)],[c1346, c1383])).
% 1.49/1.67  cnf(c34,axiom,X456!=X459|X455!=X454|X460!=X461|X457!=X458|~be(X456,X455,X460,X457)|be(X459,X454,X461,X458),theory(equality)).
% 1.49/1.67  fof(ax68,axiom,(![U]:(![V]:(![W]:(![X]:(![Y]:((accessible_world(X,Y)&be(X,U,V,W))=>be(Y,U,V,W))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax68)).
% 1.49/1.67  fof(c74,plain,(![U]:(![V]:(![W]:(![X]:(![Y]:((~accessible_world(X,Y)|~be(X,U,V,W))|be(Y,U,V,W))))))),inference(fof_nnf,[status(thm)],[ax68])).
% 1.49/1.67  fof(c75,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:((~accessible_world(X29,X30)|~be(X29,X26,X27,X28))|be(X30,X26,X27,X28))))))),inference(variable_rename,[status(thm)],[c74])).
% 1.49/1.67  cnf(c76,plain,~accessible_world(X488,X491)|~be(X488,X492,X490,X489)|be(X491,X492,X490,X489),inference(split_conjunct,[status(thm)],[c75])).
% 1.49/1.67  cnf(c508,plain,skolem0001!=X1048|skolem0008!=X1051|skolem0003!=X1049|skolem0007!=X1050|be(X1048,X1051,X1049,X1050),inference(resolution,[status(thm)],[c34, c63])).
% 1.49/1.67  cnf(c1121,plain,skolem0001!=X1371|skolem0008!=X1372|skolem0003!=X1373|be(X1371,X1372,X1373,skolem0007),inference(resolution,[status(thm)],[c508, reflexivity])).
% 1.49/1.67  cnf(c1366,plain,skolem0001!=X1424|skolem0008!=X1425|be(X1424,X1425,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1121, c415])).
% 1.49/1.67  cnf(c1419,plain,skolem0001!=X1426|be(X1426,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1366, reflexivity])).
% 1.49/1.67  cnf(c1420,plain,be(skolem0001,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1419, reflexivity])).
% 1.49/1.67  cnf(c1421,plain,~accessible_world(skolem0001,X1428)|be(X1428,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1420, c76])).
% 1.49/1.67  cnf(c1424,plain,be(skolem0006,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1421, c56])).
% 1.49/1.67  cnf(c1426,plain,skolem0006!=X1689|skolem0008!=X1692|skolem0007!=X1690|skolem0007!=X1691|be(X1689,X1692,X1690,X1691),inference(resolution,[status(thm)],[c1424, c34])).
% 1.49/1.67  cnf(c1593,plain,skolem0006!=X1695|skolem0008!=X1693|skolem0007!=X1694|be(X1695,X1693,X1694,X1694),inference(factor,[status(thm)],[c1426])).
% 1.49/1.67  cnf(c1422,plain,skolem0001!=X1672|skolem0008!=X1675|skolem0007!=X1673|skolem0007!=X1674|be(X1672,X1675,X1673,X1674),inference(resolution,[status(thm)],[c1420, c34])).
% 1.49/1.67  cnf(c1588,plain,skolem0001!=X1678|skolem0008!=X1677|skolem0007!=X1676|be(X1678,X1677,X1676,X1676),inference(factor,[status(thm)],[c1422])).
% 1.49/1.67  cnf(c1120,plain,skolem0001!=X1362|skolem0008!=X1363|skolem0003!=X1364|be(X1362,X1363,X1364,skolem0003),inference(resolution,[status(thm)],[c508, c416])).
% 1.49/1.67  cnf(c1360,plain,skolem0001!=X1409|skolem0008!=X1410|be(X1409,X1410,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1120, c415])).
% 1.49/1.67  cnf(c1398,plain,skolem0001!=X1411|be(X1411,skolem0008,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1360, reflexivity])).
% 1.49/1.67  cnf(c1399,plain,be(skolem0001,skolem0008,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1398, reflexivity])).
% 1.49/1.67  cnf(c1400,plain,~accessible_world(skolem0001,X1414)|be(X1414,skolem0008,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1399, c76])).
% 1.49/1.67  cnf(c1405,plain,be(skolem0006,skolem0008,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1400, c56])).
% 1.49/1.67  cnf(c1407,plain,skolem0006!=X1619|skolem0008!=X1622|skolem0007!=X1620|skolem0003!=X1621|be(X1619,X1622,X1620,X1621),inference(resolution,[status(thm)],[c1405, c34])).
% 1.49/1.67  cnf(c1573,plain,skolem0006!=X1653|skolem0008!=X1652|skolem0007!=X1654|be(X1653,X1652,X1654,skolem0007),inference(resolution,[status(thm)],[c1407, c415])).
% 1.49/1.67  cnf(c1361,plain,skolem0001!=X1416|skolem0008!=X1417|be(X1416,X1417,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1120, reflexivity])).
% 1.49/1.67  cnf(c1409,plain,skolem0001!=X1419|be(X1419,skolem0008,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1361, reflexivity])).
% 1.49/1.67  cnf(c1410,plain,be(skolem0001,skolem0008,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1409, reflexivity])).
% 1.49/1.67  cnf(c1411,plain,~accessible_world(skolem0001,X1420)|be(X1420,skolem0008,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1410, c76])).
% 1.49/1.67  cnf(c1414,plain,be(skolem0006,skolem0008,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1411, c56])).
% 1.49/1.67  cnf(c1416,plain,skolem0006!=X1641|skolem0008!=X1644|skolem0003!=X1642|skolem0003!=X1643|be(X1641,X1644,X1642,X1643),inference(resolution,[status(thm)],[c1414, c34])).
% 1.49/1.67  cnf(c1581,plain,skolem0006!=X1646|skolem0008!=X1647|skolem0003!=X1645|be(X1646,X1647,X1645,X1645),inference(factor,[status(thm)],[c1416])).
% 1.49/1.67  cnf(c1412,plain,skolem0001!=X1626|skolem0008!=X1629|skolem0003!=X1627|skolem0003!=X1628|be(X1626,X1629,X1627,X1628),inference(resolution,[status(thm)],[c1410, c34])).
% 1.49/1.67  cnf(c1576,plain,skolem0001!=X1636|skolem0008!=X1635|skolem0003!=X1634|be(X1636,X1635,X1634,X1634),inference(factor,[status(thm)],[c1412])).
% 1.49/1.67  cnf(c1572,plain,skolem0006!=X1624|skolem0008!=X1623|skolem0007!=X1625|be(X1624,X1623,X1625,skolem0003),inference(resolution,[status(thm)],[c1407, reflexivity])).
% 1.49/1.67  cnf(c1401,plain,skolem0001!=X1598|skolem0008!=X1601|skolem0007!=X1599|skolem0003!=X1600|be(X1598,X1601,X1599,X1600),inference(resolution,[status(thm)],[c1399, c34])).
% 1.49/1.67  cnf(c1566,plain,skolem0001!=X1612|skolem0008!=X1613|skolem0007!=X1611|be(X1612,X1613,X1611,skolem0007),inference(resolution,[status(thm)],[c1401, c415])).
% 1.49/1.67  cnf(c538,plain,~think_believe_consider(X1086,X1083)|~proposition(X1086,X1087)|~theme(X1086,X1083,X1087)|~agent(X1086,X1083,X1084)|~proposition(X1086,X1085)|~theme(X1086,X1083,X1085)|X1087=X1085,inference(factor,[status(thm)],[c73])).
% 1.49/1.67  cnf(c1149,plain,~think_believe_consider(skolem0001,skolem0005)|~proposition(skolem0001,X1413)|~theme(skolem0001,skolem0005,X1413)|~agent(skolem0001,skolem0005,X1412)|~proposition(skolem0001,skolem0006)|X1413=skolem0006,inference(resolution,[status(thm)],[c538, c52])).
% 1.49/1.67  cnf(c1403,plain,~think_believe_consider(skolem0001,skolem0005)|~proposition(skolem0001,X1610)|~theme(skolem0001,skolem0005,X1610)|~proposition(skolem0001,skolem0006)|X1610=skolem0006,inference(resolution,[status(thm)],[c1149, c51])).
% 1.49/1.67  cnf(c1565,plain,skolem0001!=X1604|skolem0008!=X1605|skolem0007!=X1603|be(X1604,X1605,X1603,skolem0003),inference(resolution,[status(thm)],[c1401, reflexivity])).
% 1.49/1.67  cnf(c835,plain,skolem0006!=X1279|skolem0009(skolem0003)!=X1280|skolem0003!=X1281|agent(X1279,X1280,X1281),inference(resolution,[status(thm)],[c683, c31])).
% 1.49/1.67  cnf(c1282,plain,skolem0006!=X1398|skolem0003!=X1399|agent(X1398,skolem0009(skolem0003),X1399),inference(resolution,[status(thm)],[c835, reflexivity])).
% 1.49/1.67  cnf(c1389,plain,skolem0006!=X1400|agent(X1400,skolem0009(skolem0003),skolem0007),inference(resolution,[status(thm)],[c1282, c415])).
% 1.49/1.67  cnf(c1391,plain,agent(skolem0006,skolem0009(skolem0003),skolem0007),inference(resolution,[status(thm)],[c1389, reflexivity])).
% 1.49/1.67  cnf(c1393,plain,skolem0006!=X1571|skolem0009(skolem0003)!=X1572|skolem0007!=X1573|agent(X1571,X1572,X1573),inference(resolution,[status(thm)],[c1391, c31])).
% 1.49/1.67  cnf(c1550,plain,skolem0006!=X1595|skolem0007!=X1596|agent(X1595,skolem0009(skolem0003),X1596),inference(resolution,[status(thm)],[c1393, reflexivity])).
% 1.49/1.67  cnf(c1385,plain,skolem0006!=X1551|skolem0009(skolem0007)!=X1552|skolem0003!=X1553|agent(X1551,X1552,X1553),inference(resolution,[status(thm)],[c1383, c31])).
% 1.49/1.67  cnf(c1548,plain,skolem0006!=X1591|skolem0003!=X1592|agent(X1591,skolem0009(skolem0007),X1592),inference(resolution,[status(thm)],[c1385, reflexivity])).
% 1.49/1.67  cnf(c541,plain,~accessible_world(skolem0001,X1063)|be(X1063,skolem0008,skolem0003,skolem0007),inference(resolution,[status(thm)],[c76, c63])).
% 1.49/1.67  cnf(c1128,plain,be(skolem0006,skolem0008,skolem0003,skolem0007),inference(resolution,[status(thm)],[c541, c56])).
% 1.49/1.67  cnf(c1130,plain,skolem0006!=X1379|skolem0008!=X1382|skolem0003!=X1380|skolem0007!=X1381|be(X1379,X1382,X1380,X1381),inference(resolution,[status(thm)],[c1128, c34])).
% 1.49/1.67  cnf(c1372,plain,skolem0006!=X1538|skolem0008!=X1539|skolem0003!=X1540|be(X1538,X1539,X1540,skolem0007),inference(resolution,[status(thm)],[c1130, reflexivity])).
% 1.49/1.67  cnf(c1547,plain,skolem0006!=X1588|skolem0008!=X1587|be(X1588,X1587,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1372, c415])).
% 1.49/1.67  cnf(c1559,plain,skolem0006!=X1589|be(X1589,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1547, reflexivity])).
% 1.49/1.67  cnf(c1546,plain,skolem0006!=X1584|skolem0008!=X1583|be(X1584,X1583,skolem0003,skolem0007),inference(resolution,[status(thm)],[c1372, reflexivity])).
% 1.49/1.67  cnf(c1556,plain,skolem0006!=X1586|be(X1586,skolem0008,skolem0003,skolem0007),inference(resolution,[status(thm)],[c1546, reflexivity])).
% 1.49/1.67  cnf(c1148,plain,~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,X1408)|~theme(skolem0006,skolem0005,X1408)|~agent(skolem0006,skolem0005,X1407)|~proposition(skolem0006,skolem0006)|X1408=skolem0006,inference(resolution,[status(thm)],[c538, c1010])).
% 1.49/1.67  cnf(c1396,plain,~think_believe_consider(skolem0006,skolem0005)|~proposition(skolem0006,X1585)|~theme(skolem0006,skolem0005,X1585)|~proposition(skolem0006,skolem0006)|X1585=skolem0006,inference(resolution,[status(thm)],[c1148, c1000])).
% 1.49/1.67  cnf(c1371,plain,skolem0006!=X1529|skolem0008!=X1530|skolem0003!=X1531|be(X1529,X1530,X1531,skolem0003),inference(resolution,[status(thm)],[c1130, c416])).
% 1.49/1.67  cnf(c1543,plain,skolem0006!=X1580|skolem0008!=X1581|be(X1580,X1581,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1371, c415])).
% 1.49/1.67  cnf(c1554,plain,skolem0006!=X1582|be(X1582,skolem0008,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1543, reflexivity])).
% 1.49/1.67  cnf(c1394,plain,~think_believe_consider(skolem0006,X1577)|~proposition(skolem0006,X1578)|~theme(skolem0006,X1577,X1578)|~agent(skolem0006,X1577,skolem0007)|~think_believe_consider(skolem0006,skolem0009(skolem0003))|~proposition(skolem0006,X1579)|~theme(skolem0006,skolem0009(skolem0003),X1579)|X1578=X1579,inference(resolution,[status(thm)],[c1391, c73])).
% 1.49/1.67  cnf(c1542,plain,skolem0006!=X1574|skolem0008!=X1575|be(X1574,X1575,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1371, reflexivity])).
% 1.49/1.67  cnf(c1551,plain,skolem0006!=X1576|be(X1576,skolem0008,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1542, reflexivity])).
% 1.49/1.67  cnf(c1386,plain,~think_believe_consider(skolem0006,X1564)|~proposition(skolem0006,X1565)|~theme(skolem0006,X1564,X1565)|~agent(skolem0006,X1564,skolem0003)|~think_believe_consider(skolem0006,skolem0009(skolem0007))|~proposition(skolem0006,X1566)|~theme(skolem0006,skolem0009(skolem0007),X1566)|X1565=X1566,inference(resolution,[status(thm)],[c1383, c73])).
% 1.49/1.67  cnf(c0,axiom,X210!=X211|X209!=X208|~vincent_forename(X210,X209)|vincent_forename(X211,X208),theory(equality)).
% 1.49/1.67  cnf(c48,negated_conjecture,vincent_forename(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  fof(ax35,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&vincent_forename(V,U))=>vincent_forename(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 1.49/1.67  fof(c173,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~vincent_forename(V,U))|vincent_forename(W,U))))),inference(fof_nnf,[status(thm)],[ax35])).
% 1.49/1.67  fof(c174,plain,(![X130]:(![X131]:(![X132]:((~accessible_world(X131,X132)|~vincent_forename(X131,X130))|vincent_forename(X132,X130))))),inference(variable_rename,[status(thm)],[c173])).
% 1.49/1.67  cnf(c175,plain,~accessible_world(X642,X643)|~vincent_forename(X642,X641)|vincent_forename(X643,X641),inference(split_conjunct,[status(thm)],[c174])).
% 1.49/1.67  cnf(c782,plain,~accessible_world(skolem0001,X711)|vincent_forename(X711,skolem0004),inference(resolution,[status(thm)],[c175, c48])).
% 1.49/1.67  cnf(c895,plain,vincent_forename(skolem0006,skolem0004),inference(resolution,[status(thm)],[c782, c56])).
% 1.49/1.67  cnf(c898,plain,skolem0006!=X1309|skolem0004!=X1310|vincent_forename(X1309,X1310),inference(resolution,[status(thm)],[c895, c0])).
% 1.49/1.67  fof(ax22,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 1.49/1.67  fof(c216,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 1.49/1.67  fof(c217,plain,(![X157]:(![X158]:(~man(X157,X158)|human_person(X157,X158)))),inference(variable_rename,[status(thm)],[c216])).
% 1.49/1.67  cnf(c218,plain,~man(X260,X261)|human_person(X260,X261),inference(split_conjunct,[status(thm)],[c217])).
% 1.49/1.67  cnf(c309,plain,human_person(skolem0001,skolem0003),inference(resolution,[status(thm)],[c218, c47])).
% 1.49/1.67  fof(ax21,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 1.49/1.67  fof(c219,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 1.49/1.67  fof(c220,plain,(![X159]:(![X160]:(~human_person(X159,X160)|organism(X159,X160)))),inference(variable_rename,[status(thm)],[c219])).
% 1.49/1.67  cnf(c221,plain,~human_person(X267,X266)|organism(X267,X266),inference(split_conjunct,[status(thm)],[c220])).
% 1.49/1.67  cnf(c311,plain,organism(skolem0001,skolem0003),inference(resolution,[status(thm)],[c221, c309])).
% 1.49/1.67  fof(ax20,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 1.49/1.67  fof(c222,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 1.49/1.67  fof(c223,plain,(![X161]:(![X162]:(~organism(X161,X162)|entity(X161,X162)))),inference(variable_rename,[status(thm)],[c222])).
% 1.49/1.67  cnf(c224,plain,~organism(X268,X269)|entity(X268,X269),inference(split_conjunct,[status(thm)],[c223])).
% 1.49/1.67  cnf(c312,plain,entity(skolem0001,skolem0003),inference(resolution,[status(thm)],[c224, c311])).
% 1.49/1.67  cnf(c49,negated_conjecture,forename(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c45,negated_conjecture,forename(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c46,negated_conjecture,of(skolem0001,skolem0004,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c43,negated_conjecture,of(skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  fof(ax70,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/sandbox2/benchmark/theBenchmark.p', ax70)).
% 1.49/1.67  fof(c67,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)],[ax70])).
% 1.49/1.67  fof(c69,plain,(![X16]:(![X17]:(![X18]:(![X19]:(((~entity(X16,X17)|~forename(X16,X18))|~of(X16,X18,X17))|((~forename(X16,X19)|X19=X18)|~of(X16,X19,X17))))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,(![X16]:(![X17]:(![X18]:(((~entity(X16,X17)|~forename(X16,X18))|~of(X16,X18,X17))|(![X19]:((~forename(X16,X19)|X19=X18)|~of(X16,X19,X17))))))),inference(variable_rename,[status(thm)],[c67])).])).
% 1.49/1.67  cnf(c70,plain,~entity(X469,X471)|~forename(X469,X470)|~of(X469,X470,X471)|~forename(X469,X468)|X468=X470|~of(X469,X468,X471),inference(split_conjunct,[status(thm)],[c69])).
% 1.49/1.67  cnf(c521,plain,~entity(skolem0001,skolem0003)|~forename(skolem0001,X1071)|~of(skolem0001,X1071,skolem0003)|~forename(skolem0001,skolem0002)|skolem0002=X1071,inference(resolution,[status(thm)],[c70, c43])).
% 1.49/1.67  cnf(c1137,plain,~entity(skolem0001,skolem0003)|~forename(skolem0001,skolem0004)|~forename(skolem0001,skolem0002)|skolem0002=skolem0004,inference(resolution,[status(thm)],[c521, c46])).
% 1.49/1.67  cnf(c1380,plain,~entity(skolem0001,skolem0003)|~forename(skolem0001,skolem0004)|skolem0002=skolem0004,inference(resolution,[status(thm)],[c1137, c45])).
% 1.49/1.67  cnf(c1430,plain,~entity(skolem0001,skolem0003)|skolem0002=skolem0004,inference(resolution,[status(thm)],[c1380, c49])).
% 1.49/1.67  cnf(c1431,plain,skolem0002=skolem0004,inference(resolution,[status(thm)],[c1430, c312])).
% 1.49/1.67  cnf(c1444,plain,skolem0004=skolem0002,inference(resolution,[status(thm)],[c1431, symmetry])).
% 1.49/1.67  cnf(c1472,plain,skolem0006!=X1487|vincent_forename(X1487,skolem0002),inference(resolution,[status(thm)],[c1444, c898])).
% 1.49/1.67  cnf(c1517,plain,vincent_forename(skolem0006,skolem0002),inference(resolution,[status(thm)],[c1472, reflexivity])).
% 1.49/1.67  cnf(c1518,plain,skolem0006!=X1534|skolem0002!=X1535|vincent_forename(X1534,X1535),inference(resolution,[status(thm)],[c1517, c0])).
% 1.49/1.67  cnf(c285,plain,skolem0001!=X647|skolem0004!=X648|vincent_forename(X647,X648),inference(resolution,[status(thm)],[c0, c48])).
% 1.49/1.67  cnf(c1471,plain,skolem0001!=X1485|vincent_forename(X1485,skolem0002),inference(resolution,[status(thm)],[c1444, c285])).
% 1.49/1.67  cnf(c1511,plain,vincent_forename(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1471, reflexivity])).
% 1.49/1.67  cnf(c1512,plain,skolem0001!=X1527|skolem0002!=X1528|vincent_forename(X1527,X1528),inference(resolution,[status(thm)],[c1511, c0])).
% 1.49/1.67  cnf(c6,axiom,X258!=X259|X257!=X256|~jules_forename(X258,X257)|jules_forename(X259,X256),theory(equality)).
% 1.49/1.67  cnf(c44,negated_conjecture,jules_forename(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c307,plain,skolem0001!=X668|skolem0002!=X667|jules_forename(X668,X667),inference(resolution,[status(thm)],[c6, c44])).
% 1.49/1.67  cnf(c1455,plain,skolem0001!=X1462|jules_forename(X1462,skolem0004),inference(resolution,[status(thm)],[c1431, c307])).
% 1.49/1.67  cnf(c1501,plain,jules_forename(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1455, reflexivity])).
% 1.49/1.67  cnf(c1503,plain,skolem0001!=X1524|skolem0004!=X1523|jules_forename(X1524,X1523),inference(resolution,[status(thm)],[c1501, c6])).
% 1.49/1.67  fof(ax42,axiom,(![U]:(![V]:(![W]:(![X]:((accessible_world(W,X)&of(W,U,V))=>of(X,U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 1.49/1.67  fof(c152,plain,(![U]:(![V]:(![W]:(![X]:((~accessible_world(W,X)|~of(W,U,V))|of(X,U,V)))))),inference(fof_nnf,[status(thm)],[ax42])).
% 1.49/1.67  fof(c153,plain,(![X106]:(![X107]:(![X108]:(![X109]:((~accessible_world(X108,X109)|~of(X108,X106,X107))|of(X109,X106,X107)))))),inference(variable_rename,[status(thm)],[c152])).
% 1.49/1.67  cnf(c154,plain,~accessible_world(X597,X594)|~of(X597,X596,X595)|of(X594,X596,X595),inference(split_conjunct,[status(thm)],[c153])).
% 1.49/1.67  cnf(c33,axiom,X447!=X448|X446!=X445|X449!=X450|~of(X447,X446,X449)|of(X448,X445,X450),theory(equality)).
% 1.49/1.67  cnf(c502,plain,skolem0001!=X1042|skolem0004!=X1041|skolem0003!=X1043|of(X1042,X1041,X1043),inference(resolution,[status(thm)],[c33, c46])).
% 1.49/1.67  cnf(c1115,plain,skolem0001!=X1345|skolem0004!=X1346|of(X1345,X1346,skolem0007),inference(resolution,[status(thm)],[c502, c415])).
% 1.49/1.67  cnf(c1343,plain,skolem0001!=X1347|of(X1347,skolem0004,skolem0007),inference(resolution,[status(thm)],[c1115, reflexivity])).
% 1.49/1.67  cnf(c1344,plain,of(skolem0001,skolem0004,skolem0007),inference(resolution,[status(thm)],[c1343, reflexivity])).
% 1.49/1.67  cnf(c1349,plain,~accessible_world(skolem0001,X1351)|of(X1351,skolem0004,skolem0007),inference(resolution,[status(thm)],[c1344, c154])).
% 1.49/1.67  cnf(c1350,plain,of(skolem0006,skolem0004,skolem0007),inference(resolution,[status(thm)],[c1349, c56])).
% 1.49/1.67  cnf(c1352,plain,~entity(skolem0006,skolem0007)|~forename(skolem0006,X1521)|~of(skolem0006,X1521,skolem0007)|~forename(skolem0006,skolem0004)|skolem0004=X1521,inference(resolution,[status(thm)],[c1350, c70])).
% 1.49/1.67  fof(ax43,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&jules_forename(V,U))=>jules_forename(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax43)).
% 1.49/1.67  fof(c149,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~jules_forename(V,U))|jules_forename(W,U))))),inference(fof_nnf,[status(thm)],[ax43])).
% 1.49/1.67  fof(c150,plain,(![X103]:(![X104]:(![X105]:((~accessible_world(X104,X105)|~jules_forename(X104,X103))|jules_forename(X105,X103))))),inference(variable_rename,[status(thm)],[c149])).
% 1.49/1.67  cnf(c151,plain,~accessible_world(X590,X588)|~jules_forename(X590,X589)|jules_forename(X588,X589),inference(split_conjunct,[status(thm)],[c150])).
% 1.49/1.67  cnf(c754,plain,~accessible_world(skolem0001,X703)|jules_forename(X703,skolem0002),inference(resolution,[status(thm)],[c151, c44])).
% 1.49/1.67  cnf(c877,plain,jules_forename(skolem0006,skolem0002),inference(resolution,[status(thm)],[c754, c56])).
% 1.49/1.67  cnf(c881,plain,skolem0006!=X1298|skolem0002!=X1297|jules_forename(X1298,X1297),inference(resolution,[status(thm)],[c877, c6])).
% 1.49/1.67  cnf(c1450,plain,skolem0006!=X1460|jules_forename(X1460,skolem0004),inference(resolution,[status(thm)],[c1431, c881])).
% 1.49/1.67  cnf(c1497,plain,jules_forename(skolem0006,skolem0004),inference(resolution,[status(thm)],[c1450, reflexivity])).
% 1.49/1.67  cnf(c1499,plain,skolem0006!=X1519|skolem0004!=X1518|jules_forename(X1519,X1518),inference(resolution,[status(thm)],[c1497, c6])).
% 1.49/1.67  cnf(c1351,plain,skolem0006!=X1513|skolem0004!=X1512|skolem0007!=X1514|of(X1513,X1512,X1514),inference(resolution,[status(thm)],[c1350, c33])).
% 1.49/1.67  cnf(c1348,plain,~entity(skolem0001,skolem0007)|~forename(skolem0001,X1506)|~of(skolem0001,X1506,skolem0007)|~forename(skolem0001,skolem0004)|skolem0004=X1506,inference(resolution,[status(thm)],[c1344, c70])).
% 1.49/1.67  cnf(c1519,plain,~accessible_world(skolem0006,X1505)|vincent_forename(X1505,skolem0002),inference(resolution,[status(thm)],[c1517, c175])).
% 1.49/1.67  cnf(c1513,plain,~accessible_world(skolem0001,X1504)|vincent_forename(X1504,skolem0002),inference(resolution,[status(thm)],[c1511, c175])).
% 1.49/1.67  cnf(c1504,plain,~accessible_world(skolem0001,X1503)|jules_forename(X1503,skolem0004),inference(resolution,[status(thm)],[c1501, c151])).
% 1.49/1.67  cnf(c1347,plain,skolem0001!=X1501|skolem0004!=X1500|skolem0007!=X1502|of(X1501,X1500,X1502),inference(resolution,[status(thm)],[c1344, c33])).
% 1.49/1.67  cnf(c1500,plain,~accessible_world(skolem0006,X1499)|jules_forename(X1499,skolem0004),inference(resolution,[status(thm)],[c1497, c151])).
% 1.49/1.67  cnf(transitivity,axiom,X207!=X205|X205!=X206|X207=X206,theory(equality)).
% 1.49/1.67  cnf(c1479,plain,X1492!=skolem0004|X1492=skolem0002,inference(resolution,[status(thm)],[c1444, transitivity])).
% 1.49/1.67  cnf(c501,plain,skolem0001!=X1035|skolem0002!=X1034|skolem0003!=X1036|of(X1035,X1034,X1036),inference(resolution,[status(thm)],[c33, c43])).
% 1.49/1.67  cnf(c1109,plain,skolem0001!=X1332|skolem0002!=X1331|of(X1332,X1331,skolem0007),inference(resolution,[status(thm)],[c501, c415])).
% 1.49/1.67  cnf(c1328,plain,skolem0001!=X1336|of(X1336,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1109, reflexivity])).
% 1.49/1.67  cnf(c1331,plain,of(skolem0001,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1328, reflexivity])).
% 1.49/1.67  cnf(c1334,plain,~accessible_world(skolem0001,X1337)|of(X1337,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1331, c154])).
% 1.49/1.67  cnf(c1335,plain,of(skolem0006,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1334, c56])).
% 1.49/1.67  cnf(c1337,plain,~entity(skolem0006,skolem0007)|~forename(skolem0006,X1486)|~of(skolem0006,X1486,skolem0007)|~forename(skolem0006,skolem0002)|skolem0002=X1486,inference(resolution,[status(thm)],[c1335, c70])).
% 1.49/1.67  cnf(c1336,plain,skolem0006!=X1480|skolem0002!=X1479|skolem0007!=X1481|of(X1480,X1479,X1481),inference(resolution,[status(thm)],[c1335, c33])).
% 1.49/1.67  cnf(c1333,plain,~entity(skolem0001,skolem0007)|~forename(skolem0001,X1473)|~of(skolem0001,X1473,skolem0007)|~forename(skolem0001,skolem0002)|skolem0002=X1473,inference(resolution,[status(thm)],[c1331, c70])).
% 1.49/1.67  cnf(c1332,plain,skolem0001!=X1466|skolem0002!=X1465|skolem0007!=X1467|of(X1466,X1465,X1467),inference(resolution,[status(thm)],[c1331, c33])).
% 1.49/1.67  cnf(c1449,plain,X1456!=skolem0002|X1456=skolem0004,inference(resolution,[status(thm)],[c1431, transitivity])).
% 1.49/1.67  cnf(c1322,plain,skolem0006!=X1450|skolem0005!=X1451|skolem0007!=X1452|agent(X1450,X1451,X1452),inference(resolution,[status(thm)],[c1320, c31])).
% 1.49/1.67  cnf(c1318,plain,skolem0001!=X1434|skolem0005!=X1435|skolem0007!=X1436|agent(X1434,X1435,X1436),inference(resolution,[status(thm)],[c1316, c31])).
% 1.49/1.67  cnf(c35,axiom,X371!=X372|~actual_world(X371)|actual_world(X372),theory(equality)).
% 1.49/1.67  cnf(c1482,plain,~actual_world(skolem0004)|actual_world(skolem0002),inference(resolution,[status(thm)],[c1444, c35])).
% 1.49/1.67  cnf(c1454,plain,~actual_world(skolem0002)|actual_world(skolem0004),inference(resolution,[status(thm)],[c1431, c35])).
% 1.49/1.67  cnf(c1367,plain,skolem0001!=X1431|skolem0008!=X1432|be(X1431,X1432,skolem0003,skolem0007),inference(resolution,[status(thm)],[c1121, reflexivity])).
% 1.49/1.67  cnf(c1428,plain,skolem0001!=X1433|be(X1433,skolem0008,skolem0003,skolem0007),inference(resolution,[status(thm)],[c1367, reflexivity])).
% 1.49/1.67  cnf(c1425,plain,~accessible_world(skolem0006,X1429)|be(X1429,skolem0008,skolem0007,skolem0007),inference(resolution,[status(thm)],[c1424, c76])).
% 1.49/1.67  cnf(c1415,plain,~accessible_world(skolem0006,X1423)|be(X1423,skolem0008,skolem0003,skolem0003),inference(resolution,[status(thm)],[c1414, c76])).
% 1.49/1.67  cnf(c539,plain,~think_believe_consider(skolem0001,X1092)|~proposition(skolem0001,X1093)|~theme(skolem0001,X1092,X1093)|~agent(skolem0001,X1092,skolem0003)|~think_believe_consider(skolem0001,skolem0005)|~proposition(skolem0001,X1094)|~theme(skolem0001,skolem0005,X1094)|X1093=X1094,inference(resolution,[status(thm)],[c73, c51])).
% 1.49/1.67  cnf(c1154,plain,~think_believe_consider(skolem0001,X1421)|~proposition(skolem0001,X1422)|~theme(skolem0001,X1421,X1422)|~agent(skolem0001,X1421,skolem0003)|~think_believe_consider(skolem0001,skolem0005)|~proposition(skolem0001,skolem0006)|X1422=skolem0006,inference(resolution,[status(thm)],[c539, c52])).
% 1.49/1.67  cnf(c1406,plain,~accessible_world(skolem0006,X1415)|be(X1415,skolem0008,skolem0007,skolem0003),inference(resolution,[status(thm)],[c1405, c76])).
% 1.49/1.67  cnf(c1392,plain,~accessible_world(skolem0006,X1406)|agent(X1406,skolem0009(skolem0003),skolem0007),inference(resolution,[status(thm)],[c1391, c163])).
% 1.49/1.67  cnf(c1390,plain,skolem0006!=X1405|agent(X1405,skolem0009(skolem0003),skolem0003),inference(resolution,[status(thm)],[c1282, reflexivity])).
% 1.49/1.67  cnf(c1384,plain,~accessible_world(skolem0006,X1397)|agent(X1397,skolem0009(skolem0007),skolem0003),inference(resolution,[status(thm)],[c1383, c163])).
% 1.49/1.67  cnf(c1382,plain,skolem0006!=X1396|agent(X1396,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c1273, reflexivity])).
% 1.49/1.67  cnf(c29,axiom,X418!=X419|X417!=X416|X420!=X421|~theme(X418,X417,X420)|theme(X419,X416,X421),theory(equality)).
% 1.49/1.67  cnf(c1012,plain,skolem0006!=X1355|skolem0005!=X1356|skolem0006!=X1357|theme(X1355,X1356,X1357),inference(resolution,[status(thm)],[c1010, c29])).
% 1.49/1.67  cnf(c1356,plain,skolem0006!=X1391|skolem0005!=X1390|theme(X1391,X1390,skolem0006),inference(resolution,[status(thm)],[c1012, reflexivity])).
% 1.49/1.67  cnf(c1378,plain,skolem0006!=X1392|theme(X1392,skolem0005,skolem0006),inference(resolution,[status(thm)],[c1356, reflexivity])).
% 1.49/1.67  cnf(c1004,plain,skolem0006!=X1339|skolem0005!=X1340|skolem0003!=X1341|agent(X1339,X1340,X1341),inference(resolution,[status(thm)],[c1000, c31])).
% 1.49/1.67  cnf(c1340,plain,skolem0006!=X1388|skolem0005!=X1387|agent(X1388,X1387,skolem0003),inference(resolution,[status(thm)],[c1004, reflexivity])).
% 1.49/1.67  cnf(c1376,plain,skolem0006!=X1389|agent(X1389,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1340, reflexivity])).
% 1.49/1.67  cnf(c1339,plain,skolem0006!=X1385|skolem0005!=X1384|agent(X1385,X1384,skolem0007),inference(resolution,[status(thm)],[c1004, c415])).
% 1.49/1.67  cnf(c1374,plain,skolem0006!=X1386|agent(X1386,skolem0005,skolem0007),inference(resolution,[status(thm)],[c1339, reflexivity])).
% 1.49/1.67  cnf(c759,plain,~accessible_world(skolem0001,X872)|of(X872,skolem0004,skolem0003),inference(resolution,[status(thm)],[c154, c46])).
% 1.49/1.67  cnf(c992,plain,of(skolem0006,skolem0004,skolem0003),inference(resolution,[status(thm)],[c759, c56])).
% 1.49/1.67  cnf(c996,plain,skolem0006!=X1334|skolem0004!=X1333|skolem0003!=X1335|of(X1334,X1333,X1335),inference(resolution,[status(thm)],[c992, c33])).
% 1.49/1.67  cnf(c1330,plain,skolem0006!=X1378|skolem0004!=X1377|of(X1378,X1377,skolem0003),inference(resolution,[status(thm)],[c996, reflexivity])).
% 1.49/1.67  cnf(c1370,plain,skolem0006!=X1383|of(X1383,skolem0004,skolem0003),inference(resolution,[status(thm)],[c1330, reflexivity])).
% 1.49/1.67  cnf(c1329,plain,skolem0006!=X1375|skolem0004!=X1374|of(X1375,X1374,skolem0007),inference(resolution,[status(thm)],[c996, c415])).
% 1.49/1.67  cnf(c1368,plain,skolem0006!=X1376|of(X1376,skolem0004,skolem0007),inference(resolution,[status(thm)],[c1329, reflexivity])).
% 1.49/1.67  cnf(c758,plain,~accessible_world(skolem0001,X871)|of(X871,skolem0002,skolem0003),inference(resolution,[status(thm)],[c154, c43])).
% 1.49/1.67  cnf(c988,plain,of(skolem0006,skolem0002,skolem0003),inference(resolution,[status(thm)],[c758, c56])).
% 1.49/1.67  cnf(c991,plain,skolem0006!=X1320|skolem0002!=X1319|skolem0003!=X1321|of(X1320,X1319,X1321),inference(resolution,[status(thm)],[c988, c33])).
% 1.49/1.67  cnf(c1314,plain,skolem0006!=X1369|skolem0002!=X1368|of(X1369,X1368,skolem0003),inference(resolution,[status(thm)],[c991, reflexivity])).
% 1.49/1.67  cnf(c1364,plain,skolem0006!=X1370|of(X1370,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1314, reflexivity])).
% 1.49/1.67  cnf(c1313,plain,skolem0006!=X1366|skolem0002!=X1365|of(X1366,X1365,skolem0007),inference(resolution,[status(thm)],[c991, c415])).
% 1.49/1.67  cnf(c1362,plain,skolem0006!=X1367|of(X1367,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1313, reflexivity])).
% 1.49/1.67  cnf(c1355,plain,skolem0006!=X1359|skolem0005!=X1360|theme(X1359,X1360,X1359),inference(factor,[status(thm)],[c1012])).
% 1.49/1.67  cnf(c1358,plain,skolem0006!=X1361|theme(X1361,skolem0005,X1361),inference(resolution,[status(thm)],[c1355, reflexivity])).
% 1.49/1.67  cnf(c1116,plain,skolem0001!=X1353|skolem0004!=X1354|of(X1353,X1354,skolem0003),inference(resolution,[status(thm)],[c502, reflexivity])).
% 1.49/1.67  cnf(c1354,plain,skolem0001!=X1358|of(X1358,skolem0004,skolem0003),inference(resolution,[status(thm)],[c1116, reflexivity])).
% 1.49/1.67  cnf(c1353,plain,~accessible_world(skolem0006,X1352)|of(X1352,skolem0004,skolem0007),inference(resolution,[status(thm)],[c1350, c154])).
% 1.49/1.67  cnf(c1110,plain,skolem0001!=X1343|skolem0002!=X1342|of(X1343,X1342,skolem0003),inference(resolution,[status(thm)],[c501, reflexivity])).
% 1.49/1.67  cnf(c1341,plain,skolem0001!=X1344|of(X1344,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1110, reflexivity])).
% 1.49/1.67  cnf(c1338,plain,~accessible_world(skolem0006,X1338)|of(X1338,skolem0002,skolem0007),inference(resolution,[status(thm)],[c1335, c154])).
% 1.49/1.67  cnf(c1091,plain,skolem0001!=X1328|skolem0005!=X1329|agent(X1328,X1329,skolem0003),inference(resolution,[status(thm)],[c479, reflexivity])).
% 1.49/1.67  cnf(c1326,plain,skolem0001!=X1330|agent(X1330,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1091, reflexivity])).
% 1.49/1.67  cnf(c1321,plain,~accessible_world(skolem0006,X1327)|agent(X1327,skolem0005,skolem0007),inference(resolution,[status(thm)],[c1320, c163])).
% 1.49/1.67  cnf(c994,plain,~entity(skolem0006,skolem0003)|~forename(skolem0006,X1326)|~of(skolem0006,X1326,skolem0003)|~forename(skolem0006,skolem0004)|skolem0004=X1326,inference(resolution,[status(thm)],[c992, c70])).
% 1.49/1.67  cnf(c463,plain,skolem0001!=X990|skolem0005!=X991|skolem0006!=X992|theme(X990,X991,X992),inference(resolution,[status(thm)],[c29, c52])).
% 1.49/1.67  cnf(c1077,plain,skolem0001!=X1317|skolem0005!=X1316|theme(X1317,X1316,skolem0006),inference(resolution,[status(thm)],[c463, reflexivity])).
% 1.49/1.67  cnf(c1311,plain,skolem0001!=X1318|theme(X1318,skolem0005,skolem0006),inference(resolution,[status(thm)],[c1077, reflexivity])).
% 1.49/1.67  cnf(c1129,plain,~accessible_world(skolem0006,X1315)|be(X1315,skolem0008,skolem0003,skolem0007),inference(resolution,[status(thm)],[c1128, c76])).
% 1.49/1.67  cnf(c989,plain,~entity(skolem0006,skolem0003)|~forename(skolem0006,X1314)|~of(skolem0006,X1314,skolem0003)|~forename(skolem0006,skolem0002)|skolem0002=X1314,inference(resolution,[status(thm)],[c988, c70])).
% 1.49/1.67  cnf(c1305,plain,skolem0006!=X1313|vincent_forename(X1313,skolem0004),inference(resolution,[status(thm)],[c898, reflexivity])).
% 1.49/1.67  cnf(c2,axiom,X228!=X229|X227!=X226|~proposition(X228,X227)|proposition(X229,X226),theory(equality)).
% 1.49/1.67  cnf(c50,negated_conjecture,proposition(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  fof(ax36,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&proposition(V,U))=>proposition(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 1.49/1.67  fof(c170,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~proposition(V,U))|proposition(W,U))))),inference(fof_nnf,[status(thm)],[ax36])).
% 1.49/1.67  fof(c171,plain,(![X127]:(![X128]:(![X129]:((~accessible_world(X128,X129)|~proposition(X128,X127))|proposition(X129,X127))))),inference(variable_rename,[status(thm)],[c170])).
% 1.49/1.67  cnf(c172,plain,~accessible_world(X635,X634)|~proposition(X635,X633)|proposition(X634,X633),inference(split_conjunct,[status(thm)],[c171])).
% 1.49/1.67  cnf(c781,plain,~accessible_world(skolem0001,X710)|proposition(X710,skolem0006),inference(resolution,[status(thm)],[c172, c50])).
% 1.49/1.67  cnf(c891,plain,proposition(skolem0006,skolem0006),inference(resolution,[status(thm)],[c781, c56])).
% 1.49/1.67  cnf(c893,plain,skolem0006!=X1308|skolem0006!=X1307|proposition(X1308,X1307),inference(resolution,[status(thm)],[c891, c2])).
% 1.49/1.67  cnf(c1304,plain,skolem0006!=X1312|proposition(X1312,skolem0006),inference(resolution,[status(thm)],[c893, reflexivity])).
% 1.49/1.67  cnf(c1303,plain,skolem0006!=X1311|proposition(X1311,X1311),inference(factor,[status(thm)],[c893])).
% 1.49/1.67  cnf(c30,axiom,X424!=X425|X423!=X422|~think_believe_consider(X424,X423)|think_believe_consider(X425,X422),theory(equality)).
% 1.49/1.67  cnf(c55,negated_conjecture,think_believe_consider(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  fof(ax38,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&think_believe_consider(V,U))=>think_believe_consider(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 1.49/1.67  fof(c164,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~think_believe_consider(V,U))|think_believe_consider(W,U))))),inference(fof_nnf,[status(thm)],[ax38])).
% 1.49/1.67  fof(c165,plain,(![X120]:(![X121]:(![X122]:((~accessible_world(X121,X122)|~think_believe_consider(X121,X120))|think_believe_consider(X122,X120))))),inference(variable_rename,[status(thm)],[c164])).
% 1.49/1.67  cnf(c166,plain,~accessible_world(X620,X621)|~think_believe_consider(X620,X622)|think_believe_consider(X621,X622),inference(split_conjunct,[status(thm)],[c165])).
% 1.49/1.67  cnf(c775,plain,~accessible_world(skolem0001,X707)|think_believe_consider(X707,skolem0005),inference(resolution,[status(thm)],[c166, c55])).
% 1.49/1.67  cnf(c886,plain,think_believe_consider(skolem0006,skolem0005),inference(resolution,[status(thm)],[c775, c56])).
% 1.49/1.67  cnf(c889,plain,skolem0006!=X1303|skolem0005!=X1304|think_believe_consider(X1303,X1304),inference(resolution,[status(thm)],[c886, c30])).
% 1.49/1.67  cnf(c1300,plain,skolem0006!=X1306|think_believe_consider(X1306,skolem0005),inference(resolution,[status(thm)],[c889, reflexivity])).
% 1.49/1.67  cnf(c32,axiom,X441!=X442|X440!=X439|~present(X441,X440)|present(X442,X439),theory(equality)).
% 1.49/1.67  cnf(c54,negated_conjecture,present(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  fof(ax40,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&present(V,U))=>present(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 1.49/1.67  fof(c158,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~present(V,U))|present(W,U))))),inference(fof_nnf,[status(thm)],[ax40])).
% 1.49/1.67  fof(c159,plain,(![X113]:(![X114]:(![X115]:((~accessible_world(X114,X115)|~present(X114,X113))|present(X115,X113))))),inference(variable_rename,[status(thm)],[c158])).
% 1.49/1.67  cnf(c160,plain,~accessible_world(X609,X607)|~present(X609,X608)|present(X607,X608),inference(split_conjunct,[status(thm)],[c159])).
% 1.49/1.67  cnf(c765,plain,~accessible_world(skolem0001,X706)|present(X706,skolem0005),inference(resolution,[status(thm)],[c160, c54])).
% 1.49/1.67  cnf(c883,plain,present(skolem0006,skolem0005),inference(resolution,[status(thm)],[c765, c56])).
% 1.49/1.67  cnf(c885,plain,skolem0006!=X1301|skolem0005!=X1302|present(X1301,X1302),inference(resolution,[status(thm)],[c883, c32])).
% 1.49/1.67  cnf(c1299,plain,skolem0006!=X1305|present(X1305,skolem0005),inference(resolution,[status(thm)],[c885, reflexivity])).
% 1.49/1.67  cnf(c1296,plain,skolem0006!=X1300|jules_forename(X1300,skolem0002),inference(resolution,[status(thm)],[c881, reflexivity])).
% 1.49/1.67  cnf(c10,axiom,X286!=X287|X285!=X284|~nonhuman(X286,X285)|nonhuman(X287,X284),theory(equality)).
% 1.49/1.67  fof(ax7,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 1.49/1.67  fof(c261,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 1.49/1.67  fof(c262,plain,(![X187]:(![X188]:(~abstraction(X187,X188)|nonhuman(X187,X188)))),inference(variable_rename,[status(thm)],[c261])).
% 1.49/1.67  cnf(c263,plain,~abstraction(X334,X335)|nonhuman(X334,X335),inference(split_conjunct,[status(thm)],[c262])).
% 1.49/1.67  fof(ax9,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 1.49/1.67  fof(c255,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 1.49/1.67  fof(c256,plain,(![X183]:(![X184]:(~relation(X183,X184)|abstraction(X183,X184)))),inference(variable_rename,[status(thm)],[c255])).
% 1.49/1.67  cnf(c257,plain,~relation(X322,X323)|abstraction(X322,X323),inference(split_conjunct,[status(thm)],[c256])).
% 1.49/1.67  fof(ax2,axiom,(![U]:(![V]:(proposition(U,V)=>relation(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 1.49/1.67  fof(c276,plain,(![U]:(![V]:(~proposition(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 1.49/1.67  fof(c277,plain,(![X197]:(![X198]:(~proposition(X197,X198)|relation(X197,X198)))),inference(variable_rename,[status(thm)],[c276])).
% 1.49/1.67  cnf(c278,plain,~proposition(X352,X353)|relation(X352,X353),inference(split_conjunct,[status(thm)],[c277])).
% 1.49/1.67  cnf(c389,plain,relation(skolem0001,skolem0006),inference(resolution,[status(thm)],[c278, c50])).
% 1.49/1.67  fof(ax47,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relation(V,U))=>relation(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax47)).
% 1.49/1.67  fof(c137,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relation(V,U))|relation(W,U))))),inference(fof_nnf,[status(thm)],[ax47])).
% 1.49/1.67  fof(c138,plain,(![X91]:(![X92]:(![X93]:((~accessible_world(X92,X93)|~relation(X92,X91))|relation(X93,X91))))),inference(variable_rename,[status(thm)],[c137])).
% 1.49/1.67  cnf(c139,plain,~accessible_world(X577,X575)|~relation(X577,X576)|relation(X575,X576),inference(split_conjunct,[status(thm)],[c138])).
% 1.49/1.67  cnf(c707,plain,~accessible_world(skolem0001,X676)|relation(X676,skolem0006),inference(resolution,[status(thm)],[c139, c389])).
% 1.49/1.67  cnf(c843,plain,relation(skolem0006,skolem0006),inference(resolution,[status(thm)],[c707, c56])).
% 1.49/1.67  cnf(c846,plain,abstraction(skolem0006,skolem0006),inference(resolution,[status(thm)],[c843, c257])).
% 1.49/1.67  cnf(c852,plain,nonhuman(skolem0006,skolem0006),inference(resolution,[status(thm)],[c846, c263])).
% 1.49/1.67  cnf(c857,plain,skolem0006!=X1294|skolem0006!=X1293|nonhuman(X1294,X1293),inference(resolution,[status(thm)],[c852, c10])).
% 1.49/1.67  cnf(c1293,plain,skolem0006!=X1299|nonhuman(X1299,skolem0006),inference(resolution,[status(thm)],[c857, reflexivity])).
% 1.49/1.67  cnf(c9,axiom,X278!=X279|X277!=X276|~general(X278,X277)|general(X279,X276),theory(equality)).
% 1.49/1.67  fof(ax6,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 1.49/1.67  fof(c264,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 1.49/1.67  fof(c265,plain,(![X189]:(![X190]:(~abstraction(X189,X190)|general(X189,X190)))),inference(variable_rename,[status(thm)],[c264])).
% 1.49/1.67  cnf(c266,plain,~abstraction(X337,X336)|general(X337,X336),inference(split_conjunct,[status(thm)],[c265])).
% 1.49/1.67  cnf(c848,plain,general(skolem0006,skolem0006),inference(resolution,[status(thm)],[c846, c266])).
% 1.49/1.67  cnf(c855,plain,skolem0006!=X1290|skolem0006!=X1291|general(X1290,X1291),inference(resolution,[status(thm)],[c848, c9])).
% 1.49/1.67  cnf(c1290,plain,skolem0006!=X1296|general(X1296,skolem0006),inference(resolution,[status(thm)],[c855, reflexivity])).
% 1.49/1.67  cnf(c1292,plain,skolem0006!=X1295|nonhuman(X1295,X1295),inference(factor,[status(thm)],[c857])).
% 1.49/1.67  cnf(c1289,plain,skolem0006!=X1292|general(X1292,X1292),inference(factor,[status(thm)],[c855])).
% 1.49/1.67  cnf(c7,axiom,X264!=X265|X263!=X262|~abstraction(X264,X263)|abstraction(X265,X262),theory(equality)).
% 1.49/1.67  cnf(c849,plain,skolem0006!=X1284|skolem0006!=X1283|abstraction(X1284,X1283),inference(resolution,[status(thm)],[c846, c7])).
% 1.49/1.67  cnf(c1285,plain,skolem0006!=X1289|abstraction(X1289,skolem0006),inference(resolution,[status(thm)],[c849, reflexivity])).
% 1.49/1.67  cnf(c836,plain,~think_believe_consider(skolem0006,X1286)|~proposition(skolem0006,X1287)|~theme(skolem0006,X1286,X1287)|~agent(skolem0006,X1286,skolem0003)|~think_believe_consider(skolem0006,skolem0009(skolem0003))|~proposition(skolem0006,X1288)|~theme(skolem0006,skolem0009(skolem0003),X1288)|X1287=X1288,inference(resolution,[status(thm)],[c683, c73])).
% 1.49/1.67  cnf(c1284,plain,skolem0006!=X1285|abstraction(X1285,X1285),inference(factor,[status(thm)],[c849])).
% 1.49/1.67  cnf(c3,axiom,X238!=X239|X237!=X236|~relation(X238,X237)|relation(X239,X236),theory(equality)).
% 1.49/1.67  cnf(c844,plain,skolem0006!=X1276|skolem0006!=X1277|relation(X1276,X1277),inference(resolution,[status(thm)],[c843, c3])).
% 1.49/1.67  cnf(c1280,plain,skolem0006!=X1282|relation(X1282,skolem0006),inference(resolution,[status(thm)],[c844, reflexivity])).
% 1.49/1.67  cnf(c1279,plain,skolem0006!=X1278|relation(X1278,X1278),inference(factor,[status(thm)],[c844])).
% 1.49/1.67  cnf(c834,plain,~accessible_world(skolem0006,X1275)|agent(X1275,skolem0009(skolem0003),skolem0003),inference(resolution,[status(thm)],[c683, c163])).
% 1.49/1.67  fof(ax10,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 1.49/1.67  fof(c252,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 1.49/1.67  fof(c253,plain,(![X181]:(![X182]:(~relname(X181,X182)|relation(X181,X182)))),inference(variable_rename,[status(thm)],[c252])).
% 1.49/1.67  cnf(c254,plain,~relname(X317,X316)|relation(X317,X316),inference(split_conjunct,[status(thm)],[c253])).
% 1.49/1.67  fof(ax11,axiom,(![U]:(![V]:(forename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 1.49/1.67  fof(c249,plain,(![U]:(![V]:(~forename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 1.49/1.67  fof(c250,plain,(![X179]:(![X180]:(~forename(X179,X180)|relname(X179,X180)))),inference(variable_rename,[status(thm)],[c249])).
% 1.49/1.67  cnf(c251,plain,~forename(X315,X314)|relname(X315,X314),inference(split_conjunct,[status(thm)],[c250])).
% 1.49/1.67  fof(ax49,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&forename(V,U))=>forename(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax49)).
% 1.49/1.67  fof(c131,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~forename(V,U))|forename(W,U))))),inference(fof_nnf,[status(thm)],[ax49])).
% 1.49/1.67  fof(c132,plain,(![X85]:(![X86]:(![X87]:((~accessible_world(X86,X87)|~forename(X86,X85))|forename(X87,X85))))),inference(variable_rename,[status(thm)],[c131])).
% 1.49/1.67  cnf(c133,plain,~accessible_world(X569,X568)|~forename(X569,X570)|forename(X568,X570),inference(split_conjunct,[status(thm)],[c132])).
% 1.49/1.67  cnf(c674,plain,~accessible_world(skolem0001,X656)|forename(X656,skolem0002),inference(resolution,[status(thm)],[c133, c45])).
% 1.49/1.67  cnf(c811,plain,forename(skolem0006,skolem0002),inference(resolution,[status(thm)],[c674, c56])).
% 1.49/1.67  cnf(c815,plain,relname(skolem0006,skolem0002),inference(resolution,[status(thm)],[c811, c251])).
% 1.49/1.67  cnf(c816,plain,relation(skolem0006,skolem0002),inference(resolution,[status(thm)],[c815, c254])).
% 1.49/1.67  cnf(c821,plain,abstraction(skolem0006,skolem0002),inference(resolution,[status(thm)],[c816, c257])).
% 1.49/1.67  cnf(c827,plain,nonhuman(skolem0006,skolem0002),inference(resolution,[status(thm)],[c821, c263])).
% 1.49/1.67  cnf(c832,plain,skolem0006!=X1270|skolem0002!=X1269|nonhuman(X1270,X1269),inference(resolution,[status(thm)],[c827, c10])).
% 1.49/1.67  cnf(c1276,plain,skolem0006!=X1274|nonhuman(X1274,skolem0002),inference(resolution,[status(thm)],[c832, reflexivity])).
% 1.49/1.67  cnf(c774,plain,~think_believe_consider(skolem0006,X1271)|~proposition(skolem0006,X1272)|~theme(skolem0006,X1271,X1272)|~agent(skolem0006,X1271,skolem0007)|~think_believe_consider(skolem0006,skolem0009(skolem0007))|~proposition(skolem0006,X1273)|~theme(skolem0006,skolem0009(skolem0007),X1273)|X1272=X1273,inference(resolution,[status(thm)],[c611, c73])).
% 1.49/1.67  cnf(c823,plain,general(skolem0006,skolem0002),inference(resolution,[status(thm)],[c821, c266])).
% 1.49/1.67  cnf(c830,plain,skolem0006!=X1266|skolem0002!=X1267|general(X1266,X1267),inference(resolution,[status(thm)],[c823, c9])).
% 1.49/1.67  cnf(c1274,plain,skolem0006!=X1268|general(X1268,skolem0002),inference(resolution,[status(thm)],[c830, reflexivity])).
% 1.49/1.67  cnf(c824,plain,skolem0006!=X1261|skolem0002!=X1260|abstraction(X1261,X1260),inference(resolution,[status(thm)],[c821, c7])).
% 1.49/1.67  cnf(c1271,plain,skolem0006!=X1262|abstraction(X1262,skolem0002),inference(resolution,[status(thm)],[c824, reflexivity])).
% 1.49/1.67  cnf(c27,axiom,X405!=X406|X404!=X403|~singleton(X405,X404)|singleton(X406,X403),theory(equality)).
% 1.49/1.67  fof(ax28,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 1.49/1.67  fof(c198,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 1.49/1.67  fof(c199,plain,(![X145]:(![X146]:(~thing(X145,X146)|singleton(X145,X146)))),inference(variable_rename,[status(thm)],[c198])).
% 1.49/1.67  cnf(c200,plain,~thing(X233,X232)|singleton(X233,X232),inference(split_conjunct,[status(thm)],[c199])).
% 1.49/1.67  fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 1.49/1.67  fof(c195,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 1.49/1.67  fof(c196,plain,(![X143]:(![X144]:(~eventuality(X143,X144)|thing(X143,X144)))),inference(variable_rename,[status(thm)],[c195])).
% 1.49/1.67  cnf(c197,plain,~eventuality(X230,X231)|thing(X230,X231),inference(split_conjunct,[status(thm)],[c196])).
% 1.49/1.67  fof(ax23,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 1.49/1.67  fof(c213,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 1.49/1.67  fof(c214,plain,(![X155]:(![X156]:(~event(X155,X156)|eventuality(X155,X156)))),inference(variable_rename,[status(thm)],[c213])).
% 1.49/1.67  cnf(c215,plain,~event(X250,X251)|eventuality(X250,X251),inference(split_conjunct,[status(thm)],[c214])).
% 1.49/1.67  cnf(c57,negated_conjecture,~man(skolem0006,X392)|event(skolem0006,skolem0009(X392)),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.67  cnf(c679,plain,event(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c677, c57])).
% 1.49/1.67  cnf(c725,plain,eventuality(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c679, c215])).
% 1.49/1.67  cnf(c735,plain,thing(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c725, c197])).
% 1.49/1.67  cnf(c744,plain,singleton(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c735, c200])).
% 1.49/1.67  cnf(c751,plain,skolem0006!=X1257|skolem0009(skolem0003)!=X1258|singleton(X1257,X1258),inference(resolution,[status(thm)],[c744, c27])).
% 1.49/1.67  cnf(c1269,plain,skolem0006!=X1259|singleton(X1259,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c751, reflexivity])).
% 1.49/1.67  cnf(c819,plain,skolem0006!=X1254|skolem0002!=X1255|relation(X1254,X1255),inference(resolution,[status(thm)],[c816, c3])).
% 1.49/1.67  cnf(c1267,plain,skolem0006!=X1256|relation(X1256,skolem0002),inference(resolution,[status(thm)],[c819, reflexivity])).
% 1.49/1.67  cnf(c8,axiom,X272!=X273|X271!=X270|~unisex(X272,X271)|unisex(X273,X270),theory(equality)).
% 1.49/1.67  fof(ax25,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 1.49/1.67  fof(c207,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 1.49/1.67  fof(c208,plain,(![X151]:(![X152]:(~eventuality(X151,X152)|unisex(X151,X152)))),inference(variable_rename,[status(thm)],[c207])).
% 1.49/1.67  cnf(c209,plain,~eventuality(X243,X242)|unisex(X243,X242),inference(split_conjunct,[status(thm)],[c208])).
% 1.49/1.67  cnf(c736,plain,unisex(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c725, c209])).
% 1.49/1.67  cnf(c750,plain,skolem0006!=X1252|skolem0009(skolem0003)!=X1251|unisex(X1252,X1251),inference(resolution,[status(thm)],[c736, c8])).
% 1.49/1.67  cnf(c1265,plain,skolem0006!=X1253|unisex(X1253,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c750, reflexivity])).
% 1.49/1.67  cnf(c12,axiom,X300!=X301|X299!=X298|~relname(X300,X299)|relname(X301,X298),theory(equality)).
% 1.49/1.67  cnf(c817,plain,skolem0006!=X1249|skolem0002!=X1248|relname(X1249,X1248),inference(resolution,[status(thm)],[c815, c12])).
% 1.49/1.67  cnf(c1263,plain,skolem0006!=X1250|relname(X1250,skolem0002),inference(resolution,[status(thm)],[c817, reflexivity])).
% 1.49/1.67  cnf(c11,axiom,X292!=X293|X291!=X290|~thing(X292,X291)|thing(X293,X290),theory(equality)).
% 1.49/1.67  cnf(c743,plain,skolem0006!=X1246|skolem0009(skolem0003)!=X1245|thing(X1246,X1245),inference(resolution,[status(thm)],[c735, c11])).
% 1.49/1.67  cnf(c1261,plain,skolem0006!=X1247|thing(X1247,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c743, reflexivity])).
% 1.49/1.67  cnf(c1,axiom,X216!=X217|X215!=X214|~forename(X216,X215)|forename(X217,X214),theory(equality)).
% 1.49/1.67  cnf(c814,plain,skolem0006!=X1242|skolem0002!=X1243|forename(X1242,X1243),inference(resolution,[status(thm)],[c811, c1])).
% 1.49/1.67  cnf(c1259,plain,skolem0006!=X1244|forename(X1244,skolem0002),inference(resolution,[status(thm)],[c814, reflexivity])).
% 1.49/1.67  cnf(c23,axiom,X376!=X377|X375!=X374|~specific(X376,X375)|specific(X377,X374),theory(equality)).
% 1.49/1.67  fof(ax27,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 1.49/1.67  fof(c201,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 1.49/1.67  fof(c202,plain,(![X147]:(![X148]:(~eventuality(X147,X148)|specific(X147,X148)))),inference(variable_rename,[status(thm)],[c201])).
% 1.49/1.67  cnf(c203,plain,~eventuality(X234,X235)|specific(X234,X235),inference(split_conjunct,[status(thm)],[c202])).
% 1.49/1.67  cnf(c734,plain,specific(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c725, c203])).
% 1.49/1.67  cnf(c741,plain,skolem0006!=X1239|skolem0009(skolem0003)!=X1240|specific(X1239,X1240),inference(resolution,[status(thm)],[c734, c23])).
% 1.49/1.67  cnf(c1257,plain,skolem0006!=X1241|specific(X1241,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c741, reflexivity])).
% 1.49/1.67  cnf(c673,plain,~accessible_world(skolem0001,X651)|forename(X651,skolem0004),inference(resolution,[status(thm)],[c133, c49])).
% 1.49/1.67  cnf(c788,plain,forename(skolem0006,skolem0004),inference(resolution,[status(thm)],[c673, c56])).
% 1.49/1.67  cnf(c792,plain,relname(skolem0006,skolem0004),inference(resolution,[status(thm)],[c788, c251])).
% 1.49/1.67  cnf(c793,plain,relation(skolem0006,skolem0004),inference(resolution,[status(thm)],[c792, c254])).
% 1.49/1.67  cnf(c798,plain,abstraction(skolem0006,skolem0004),inference(resolution,[status(thm)],[c793, c257])).
% 1.49/1.67  cnf(c804,plain,nonhuman(skolem0006,skolem0004),inference(resolution,[status(thm)],[c798, c263])).
% 1.49/1.67  cnf(c809,plain,skolem0006!=X1237|skolem0004!=X1236|nonhuman(X1237,X1236),inference(resolution,[status(thm)],[c804, c10])).
% 1.49/1.67  cnf(c1255,plain,skolem0006!=X1238|nonhuman(X1238,skolem0004),inference(resolution,[status(thm)],[c809, reflexivity])).
% 1.49/1.67  cnf(c26,axiom,X397!=X398|X396!=X395|~nonexistent(X397,X396)|nonexistent(X398,X395),theory(equality)).
% 1.49/1.67  fof(ax26,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 1.49/1.67  fof(c204,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 1.49/1.67  fof(c205,plain,(![X149]:(![X150]:(~eventuality(X149,X150)|nonexistent(X149,X150)))),inference(variable_rename,[status(thm)],[c204])).
% 1.49/1.67  cnf(c206,plain,~eventuality(X241,X240)|nonexistent(X241,X240),inference(split_conjunct,[status(thm)],[c205])).
% 1.49/1.67  cnf(c733,plain,nonexistent(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c725, c206])).
% 1.49/1.67  cnf(c738,plain,skolem0006!=X1233|skolem0009(skolem0003)!=X1234|nonexistent(X1233,X1234),inference(resolution,[status(thm)],[c733, c26])).
% 1.49/1.67  cnf(c1253,plain,skolem0006!=X1235|nonexistent(X1235,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c738, reflexivity])).
% 1.49/1.68  cnf(c800,plain,general(skolem0006,skolem0004),inference(resolution,[status(thm)],[c798, c266])).
% 1.49/1.68  cnf(c807,plain,skolem0006!=X1230|skolem0004!=X1231|general(X1230,X1231),inference(resolution,[status(thm)],[c800, c9])).
% 1.49/1.68  cnf(c1251,plain,skolem0006!=X1232|general(X1232,skolem0004),inference(resolution,[status(thm)],[c807, reflexivity])).
% 1.49/1.68  cnf(c24,axiom,X384!=X385|X383!=X382|~eventuality(X384,X383)|eventuality(X385,X382),theory(equality)).
% 1.49/1.68  cnf(c737,plain,skolem0006!=X1228|skolem0009(skolem0003)!=X1227|eventuality(X1228,X1227),inference(resolution,[status(thm)],[c725, c24])).
% 1.49/1.68  cnf(c1249,plain,skolem0006!=X1229|eventuality(X1229,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c737, reflexivity])).
% 1.49/1.68  cnf(c801,plain,skolem0006!=X1225|skolem0004!=X1224|abstraction(X1225,X1224),inference(resolution,[status(thm)],[c798, c7])).
% 1.49/1.68  cnf(c1247,plain,skolem0006!=X1226|abstraction(X1226,skolem0004),inference(resolution,[status(thm)],[c801, reflexivity])).
% 1.49/1.68  cnf(c59,negated_conjecture,~man(skolem0006,X393)|present(skolem0006,skolem0009(X393)),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.68  cnf(c682,plain,present(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c677, c59])).
% 1.49/1.68  cnf(c728,plain,skolem0006!=X1221|skolem0009(skolem0003)!=X1222|present(X1221,X1222),inference(resolution,[status(thm)],[c682, c32])).
% 1.49/1.68  cnf(c1245,plain,skolem0006!=X1223|present(X1223,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c728, reflexivity])).
% 1.49/1.68  cnf(c796,plain,skolem0006!=X1218|skolem0004!=X1219|relation(X1218,X1219),inference(resolution,[status(thm)],[c793, c3])).
% 1.49/1.68  cnf(c1243,plain,skolem0006!=X1220|relation(X1220,skolem0004),inference(resolution,[status(thm)],[c796, reflexivity])).
% 1.49/1.68  cnf(c4,axiom,X246!=X247|X245!=X244|~smoke(X246,X245)|smoke(X247,X244),theory(equality)).
% 1.49/1.68  cnf(c60,negated_conjecture,~man(skolem0006,X394)|smoke(skolem0006,skolem0009(X394)),inference(split_conjunct,[status(thm)],[c41])).
% 1.49/1.68  cnf(c681,plain,smoke(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c677, c60])).
% 1.49/1.68  cnf(c727,plain,skolem0006!=X1215|skolem0009(skolem0003)!=X1216|smoke(X1215,X1216),inference(resolution,[status(thm)],[c681, c4])).
% 1.53/1.68  cnf(c1241,plain,skolem0006!=X1217|smoke(X1217,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c727, reflexivity])).
% 1.53/1.68  cnf(c794,plain,skolem0006!=X1213|skolem0004!=X1212|relname(X1213,X1212),inference(resolution,[status(thm)],[c792, c12])).
% 1.53/1.68  cnf(c1239,plain,skolem0006!=X1214|relname(X1214,skolem0004),inference(resolution,[status(thm)],[c794, reflexivity])).
% 1.53/1.68  cnf(c5,axiom,X254!=X255|X253!=X252|~event(X254,X253)|event(X255,X252),theory(equality)).
% 1.53/1.68  cnf(c724,plain,skolem0006!=X1209|skolem0009(skolem0003)!=X1210|event(X1209,X1210),inference(resolution,[status(thm)],[c679, c5])).
% 1.53/1.68  cnf(c1237,plain,skolem0006!=X1211|event(X1211,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c724, reflexivity])).
% 1.53/1.68  cnf(c791,plain,skolem0006!=X1206|skolem0004!=X1207|forename(X1206,X1207),inference(resolution,[status(thm)],[c788, c1])).
% 1.53/1.68  cnf(c1235,plain,skolem0006!=X1208|forename(X1208,skolem0004),inference(resolution,[status(thm)],[c791, reflexivity])).
% 1.53/1.68  cnf(c772,plain,~accessible_world(skolem0006,X1205)|agent(X1205,skolem0009(skolem0007),skolem0007),inference(resolution,[status(thm)],[c611, c163])).
% 1.53/1.68  cnf(c22,axiom,X366!=X367|X365!=X364|~existent(X366,X365)|existent(X367,X364),theory(equality)).
% 1.53/1.68  fof(ax17,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 1.53/1.68  fof(c231,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 1.53/1.68  fof(c232,plain,(![X167]:(![X168]:(~entity(X167,X168)|existent(X167,X168)))),inference(variable_rename,[status(thm)],[c231])).
% 1.53/1.68  cnf(c233,plain,~entity(X282,X283)|existent(X282,X283),inference(split_conjunct,[status(thm)],[c232])).
% 1.53/1.68  cnf(c684,plain,human_person(skolem0006,skolem0003),inference(resolution,[status(thm)],[c677, c218])).
% 1.53/1.68  cnf(c691,plain,organism(skolem0006,skolem0003),inference(resolution,[status(thm)],[c684, c221])).
% 1.53/1.68  cnf(c698,plain,entity(skolem0006,skolem0003),inference(resolution,[status(thm)],[c691, c224])).
% 1.53/1.68  cnf(c709,plain,existent(skolem0006,skolem0003),inference(resolution,[status(thm)],[c698, c233])).
% 1.53/1.68  cnf(c718,plain,skolem0006!=X1202|skolem0003!=X1201|existent(X1202,X1201),inference(resolution,[status(thm)],[c709, c22])).
% 1.53/1.68  cnf(c19,axiom,X346!=X347|X345!=X344|~living(X346,X345)|living(X347,X344),theory(equality)).
% 1.53/1.68  fof(ax15,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 1.53/1.68  fof(c237,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 1.53/1.68  fof(c238,plain,(![X171]:(![X172]:(~organism(X171,X172)|living(X171,X172)))),inference(variable_rename,[status(thm)],[c237])).
% 1.53/1.68  cnf(c239,plain,~organism(X295,X294)|living(X295,X294),inference(split_conjunct,[status(thm)],[c238])).
% 1.53/1.68  cnf(c700,plain,living(skolem0006,skolem0003),inference(resolution,[status(thm)],[c691, c239])).
% 1.53/1.68  cnf(c716,plain,skolem0006!=X1198|skolem0003!=X1197|living(X1198,X1197),inference(resolution,[status(thm)],[c700, c19])).
% 1.53/1.68  cnf(c607,plain,event(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c605, c57])).
% 1.53/1.68  cnf(c650,plain,eventuality(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c607, c215])).
% 1.53/1.68  cnf(c657,plain,thing(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c650, c197])).
% 1.53/1.68  cnf(c669,plain,singleton(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c657, c200])).
% 1.53/1.68  cnf(c675,plain,skolem0006!=X1194|skolem0009(skolem0007)!=X1195|singleton(X1194,X1195),inference(resolution,[status(thm)],[c669, c27])).
% 1.53/1.68  cnf(c1229,plain,skolem0006!=X1196|singleton(X1196,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c675, reflexivity])).
% 1.53/1.68  cnf(c20,axiom,X356!=X357|X355!=X354|~impartial(X356,X355)|impartial(X357,X354),theory(equality)).
% 1.53/1.68  fof(ax16,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 1.53/1.68  fof(c234,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 1.53/1.68  fof(c235,plain,(![X169]:(![X170]:(~organism(X169,X170)|impartial(X169,X170)))),inference(variable_rename,[status(thm)],[c234])).
% 1.53/1.68  cnf(c236,plain,~organism(X288,X289)|impartial(X288,X289),inference(split_conjunct,[status(thm)],[c235])).
% 1.53/1.68  cnf(c699,plain,impartial(skolem0006,skolem0003),inference(resolution,[status(thm)],[c691, c236])).
% 1.53/1.68  cnf(c715,plain,skolem0006!=X1191|skolem0003!=X1190|impartial(X1191,X1190),inference(resolution,[status(thm)],[c699, c20])).
% 1.53/1.68  cnf(c658,plain,unisex(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c650, c209])).
% 1.53/1.68  cnf(c672,plain,skolem0006!=X1188|skolem0009(skolem0007)!=X1187|unisex(X1188,X1187),inference(resolution,[status(thm)],[c658, c8])).
% 1.53/1.68  cnf(c1225,plain,skolem0006!=X1189|unisex(X1189,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c672, reflexivity])).
% 1.53/1.68  cnf(c21,axiom,X360!=X361|X359!=X358|~entity(X360,X359)|entity(X361,X358),theory(equality)).
% 1.53/1.68  cnf(c712,plain,skolem0006!=X1183|skolem0003!=X1184|entity(X1183,X1184),inference(resolution,[status(thm)],[c698, c21])).
% 1.53/1.68  cnf(c668,plain,skolem0006!=X1181|skolem0009(skolem0007)!=X1180|thing(X1181,X1180),inference(resolution,[status(thm)],[c657, c11])).
% 1.53/1.68  cnf(c1221,plain,skolem0006!=X1182|thing(X1182,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c668, reflexivity])).
% 1.53/1.68  cnf(c16,axiom,X326!=X327|X325!=X324|~animate(X326,X325)|animate(X327,X324),theory(equality)).
% 1.53/1.68  fof(ax13,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 1.53/1.68  fof(c243,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 1.53/1.68  fof(c244,plain,(![X175]:(![X176]:(~human_person(X175,X176)|animate(X175,X176)))),inference(variable_rename,[status(thm)],[c243])).
% 1.53/1.68  cnf(c245,plain,~human_person(X303,X302)|animate(X303,X302),inference(split_conjunct,[status(thm)],[c244])).
% 1.53/1.68  cnf(c694,plain,animate(skolem0006,skolem0003),inference(resolution,[status(thm)],[c684, c245])).
% 1.53/1.68  cnf(c704,plain,skolem0006!=X1176|skolem0003!=X1177|animate(X1176,X1177),inference(resolution,[status(thm)],[c694, c16])).
% 1.53/1.68  cnf(c656,plain,specific(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c650, c203])).
% 1.53/1.68  cnf(c666,plain,skolem0006!=X1173|skolem0009(skolem0007)!=X1174|specific(X1173,X1174),inference(resolution,[status(thm)],[c656, c23])).
% 1.53/1.68  cnf(c1217,plain,skolem0006!=X1175|specific(X1175,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c666, reflexivity])).
% 1.53/1.68  cnf(c17,axiom,X332!=X333|X331!=X330|~human(X332,X331)|human(X333,X330),theory(equality)).
% 1.53/1.68  fof(ax14,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 1.53/1.68  fof(c240,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 1.53/1.68  fof(c241,plain,(![X173]:(![X174]:(~human_person(X173,X174)|human(X173,X174)))),inference(variable_rename,[status(thm)],[c240])).
% 1.53/1.68  cnf(c242,plain,~human_person(X296,X297)|human(X296,X297),inference(split_conjunct,[status(thm)],[c241])).
% 1.53/1.68  cnf(c692,plain,human(skolem0006,skolem0003),inference(resolution,[status(thm)],[c684, c242])).
% 1.53/1.68  cnf(c702,plain,skolem0006!=X1169|skolem0003!=X1170|human(X1169,X1170),inference(resolution,[status(thm)],[c692, c17])).
% 1.53/1.68  cnf(c655,plain,nonexistent(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c650, c206])).
% 1.53/1.68  cnf(c663,plain,skolem0006!=X1166|skolem0009(skolem0007)!=X1167|nonexistent(X1166,X1167),inference(resolution,[status(thm)],[c655, c26])).
% 1.53/1.68  cnf(c1213,plain,skolem0006!=X1168|nonexistent(X1168,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c663, reflexivity])).
% 1.53/1.68  cnf(c18,axiom,X340!=X341|X339!=X338|~organism(X340,X339)|organism(X341,X338),theory(equality)).
% 1.53/1.68  cnf(c697,plain,skolem0006!=X1163|skolem0003!=X1162|organism(X1163,X1162),inference(resolution,[status(thm)],[c691, c18])).
% 1.53/1.68  cnf(c659,plain,skolem0006!=X1160|skolem0009(skolem0007)!=X1159|eventuality(X1160,X1159),inference(resolution,[status(thm)],[c650, c24])).
% 1.53/1.68  cnf(c1209,plain,skolem0006!=X1161|eventuality(X1161,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c659, reflexivity])).
% 1.53/1.68  cnf(c15,axiom,X320!=X321|X319!=X318|~human_person(X320,X319)|human_person(X321,X318),theory(equality)).
% 1.53/1.68  cnf(c693,plain,skolem0006!=X1156|skolem0003!=X1155|human_person(X1156,X1155),inference(resolution,[status(thm)],[c684, c15])).
% 1.53/1.68  cnf(c610,plain,present(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c605, c59])).
% 1.53/1.68  cnf(c653,plain,skolem0006!=X1152|skolem0009(skolem0007)!=X1153|present(X1152,X1153),inference(resolution,[status(thm)],[c610, c32])).
% 1.53/1.68  cnf(c1205,plain,skolem0006!=X1154|present(X1154,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c653, reflexivity])).
% 1.53/1.68  cnf(c14,axiom,X312!=X313|X311!=X310|~male(X312,X311)|male(X313,X310),theory(equality)).
% 1.53/1.68  fof(ax12,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 1.53/1.68  fof(c246,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 1.53/1.68  fof(c247,plain,(![X177]:(![X178]:(~man(X177,X178)|male(X177,X178)))),inference(variable_rename,[status(thm)],[c246])).
% 1.53/1.68  cnf(c248,plain,~man(X309,X308)|male(X309,X308),inference(split_conjunct,[status(thm)],[c247])).
% 1.53/1.68  cnf(c678,plain,male(skolem0006,skolem0003),inference(resolution,[status(thm)],[c677, c248])).
% 1.53/1.68  cnf(c687,plain,skolem0006!=X1149|skolem0003!=X1148|male(X1149,X1148),inference(resolution,[status(thm)],[c678, c14])).
% 1.53/1.68  cnf(c609,plain,smoke(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c605, c60])).
% 1.53/1.68  cnf(c652,plain,skolem0006!=X1145|skolem0009(skolem0007)!=X1146|smoke(X1145,X1146),inference(resolution,[status(thm)],[c609, c4])).
% 1.53/1.68  cnf(c1201,plain,skolem0006!=X1147|smoke(X1147,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c652, reflexivity])).
% 1.53/1.68  cnf(c13,axiom,X306!=X307|X305!=X304|~man(X306,X305)|man(X307,X304),theory(equality)).
% 1.53/1.68  cnf(c680,plain,skolem0006!=X1141|skolem0003!=X1142|man(X1141,X1142),inference(resolution,[status(thm)],[c677, c13])).
% 1.53/1.68  cnf(c649,plain,skolem0006!=X1138|skolem0009(skolem0007)!=X1139|event(X1138,X1139),inference(resolution,[status(thm)],[c607, c5])).
% 1.53/1.68  cnf(c1197,plain,skolem0006!=X1140|event(X1140,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c649, reflexivity])).
% 1.53/1.68  cnf(c612,plain,human_person(skolem0006,skolem0007),inference(resolution,[status(thm)],[c605, c218])).
% 1.53/1.68  cnf(c616,plain,organism(skolem0006,skolem0007),inference(resolution,[status(thm)],[c612, c221])).
% 1.53/1.68  cnf(c625,plain,entity(skolem0006,skolem0007),inference(resolution,[status(thm)],[c616, c224])).
% 1.53/1.68  cnf(c631,plain,existent(skolem0006,skolem0007),inference(resolution,[status(thm)],[c625, c233])).
% 1.53/1.68  cnf(c643,plain,skolem0006!=X1135|skolem0007!=X1134|existent(X1135,X1134),inference(resolution,[status(thm)],[c631, c22])).
% 1.53/1.68  cnf(c1194,plain,skolem0006!=X1137|existent(X1137,skolem0007),inference(resolution,[status(thm)],[c643, reflexivity])).
% 1.53/1.68  cnf(c1193,plain,skolem0006!=X1136|existent(X1136,skolem0003),inference(resolution,[status(thm)],[c643, c416])).
% 1.53/1.68  cnf(c627,plain,living(skolem0006,skolem0007),inference(resolution,[status(thm)],[c616, c239])).
% 1.53/1.68  cnf(c641,plain,skolem0006!=X1130|skolem0007!=X1129|living(X1130,X1129),inference(resolution,[status(thm)],[c627, c19])).
% 1.53/1.68  cnf(c1189,plain,skolem0006!=X1133|living(X1133,skolem0007),inference(resolution,[status(thm)],[c641, reflexivity])).
% 1.53/1.68  cnf(c1188,plain,skolem0006!=X1132|living(X1132,skolem0003),inference(resolution,[status(thm)],[c641, c416])).
% 1.53/1.68  cnf(c626,plain,impartial(skolem0006,skolem0007),inference(resolution,[status(thm)],[c616, c236])).
% 1.53/1.68  cnf(c640,plain,skolem0006!=X1126|skolem0007!=X1125|impartial(X1126,X1125),inference(resolution,[status(thm)],[c626, c20])).
% 1.53/1.68  cnf(c1185,plain,skolem0006!=X1131|impartial(X1131,skolem0007),inference(resolution,[status(thm)],[c640, reflexivity])).
% 1.53/1.68  cnf(c1184,plain,skolem0006!=X1128|impartial(X1128,skolem0003),inference(resolution,[status(thm)],[c640, c416])).
% 1.53/1.68  cnf(c634,plain,skolem0006!=X1120|skolem0007!=X1121|entity(X1120,X1121),inference(resolution,[status(thm)],[c625, c21])).
% 1.53/1.68  cnf(c1180,plain,skolem0006!=X1127|entity(X1127,skolem0007),inference(resolution,[status(thm)],[c634, reflexivity])).
% 1.53/1.68  cnf(c1179,plain,skolem0006!=X1124|entity(X1124,skolem0003),inference(resolution,[status(thm)],[c634, c416])).
% 1.53/1.68  cnf(c619,plain,animate(skolem0006,skolem0007),inference(resolution,[status(thm)],[c612, c245])).
% 1.53/1.68  cnf(c630,plain,skolem0006!=X1118|skolem0007!=X1119|animate(X1118,X1119),inference(resolution,[status(thm)],[c619, c16])).
% 1.53/1.68  cnf(c1178,plain,skolem0006!=X1123|animate(X1123,skolem0007),inference(resolution,[status(thm)],[c630, reflexivity])).
% 1.53/1.68  cnf(c1177,plain,skolem0006!=X1122|animate(X1122,skolem0003),inference(resolution,[status(thm)],[c630, c416])).
% 1.53/1.68  cnf(c617,plain,human(skolem0006,skolem0007),inference(resolution,[status(thm)],[c612, c242])).
% 1.53/1.68  cnf(c629,plain,skolem0006!=X1114|skolem0007!=X1115|human(X1114,X1115),inference(resolution,[status(thm)],[c617, c17])).
% 1.53/1.68  cnf(c1174,plain,skolem0006!=X1117|human(X1117,skolem0007),inference(resolution,[status(thm)],[c629, reflexivity])).
% 1.53/1.68  cnf(c1173,plain,skolem0006!=X1116|human(X1116,skolem0003),inference(resolution,[status(thm)],[c629, c416])).
% 1.53/1.68  cnf(c624,plain,skolem0006!=X1111|skolem0007!=X1110|organism(X1111,X1110),inference(resolution,[status(thm)],[c616, c18])).
% 1.53/1.68  cnf(c1170,plain,skolem0006!=X1113|organism(X1113,skolem0007),inference(resolution,[status(thm)],[c624, reflexivity])).
% 1.53/1.68  cnf(c1169,plain,skolem0006!=X1112|organism(X1112,skolem0003),inference(resolution,[status(thm)],[c624, c416])).
% 1.53/1.68  cnf(c618,plain,skolem0006!=X1106|skolem0007!=X1105|human_person(X1106,X1105),inference(resolution,[status(thm)],[c612, c15])).
% 1.53/1.68  cnf(c1165,plain,skolem0006!=X1109|human_person(X1109,skolem0007),inference(resolution,[status(thm)],[c618, reflexivity])).
% 1.53/1.68  cnf(c1164,plain,skolem0006!=X1108|human_person(X1108,skolem0003),inference(resolution,[status(thm)],[c618, c416])).
% 1.53/1.68  cnf(c606,plain,male(skolem0006,skolem0007),inference(resolution,[status(thm)],[c605, c248])).
% 1.53/1.68  cnf(c615,plain,skolem0006!=X1102|skolem0007!=X1101|male(X1102,X1101),inference(resolution,[status(thm)],[c606, c14])).
% 1.53/1.68  cnf(c1161,plain,skolem0006!=X1107|male(X1107,skolem0007),inference(resolution,[status(thm)],[c615, reflexivity])).
% 1.53/1.68  cnf(c1160,plain,skolem0006!=X1104|male(X1104,skolem0003),inference(resolution,[status(thm)],[c615, c416])).
% 1.53/1.68  cnf(c608,plain,skolem0006!=X1098|skolem0007!=X1099|man(X1098,X1099),inference(resolution,[status(thm)],[c605, c13])).
% 1.53/1.68  cnf(c1158,plain,skolem0006!=X1103|man(X1103,skolem0007),inference(resolution,[status(thm)],[c608, reflexivity])).
% 1.53/1.68  cnf(c1157,plain,skolem0006!=X1100|man(X1100,skolem0003),inference(resolution,[status(thm)],[c608, c416])).
% 1.53/1.68  cnf(c53,negated_conjecture,event(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 1.53/1.68  fof(ax60,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&event(V,U))=>event(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax60)).
% 1.53/1.68  fof(c98,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~event(V,U))|event(W,U))))),inference(fof_nnf,[status(thm)],[ax60])).
% 1.53/1.68  fof(c99,plain,(![X52]:(![X53]:(![X54]:((~accessible_world(X53,X54)|~event(X53,X52))|event(X54,X52))))),inference(variable_rename,[status(thm)],[c98])).
% 1.53/1.68  cnf(c100,plain,~accessible_world(X516,X517)|~event(X516,X518)|event(X517,X518),inference(split_conjunct,[status(thm)],[c99])).
% 1.53/1.68  cnf(c568,plain,~accessible_world(skolem0001,X545)|event(X545,skolem0005),inference(resolution,[status(thm)],[c100, c53])).
% 1.53/1.68  cnf(c596,plain,event(skolem0006,skolem0005),inference(resolution,[status(thm)],[c568, c56])).
% 1.53/1.68  cnf(c600,plain,skolem0006!=X1095|skolem0005!=X1096|event(X1095,X1096),inference(resolution,[status(thm)],[c596, c5])).
% 1.53/1.68  cnf(c1155,plain,skolem0006!=X1097|event(X1097,skolem0005),inference(resolution,[status(thm)],[c600, reflexivity])).
% 1.53/1.68  cnf(c346,plain,relname(skolem0001,skolem0004),inference(resolution,[status(thm)],[c251, c49])).
% 1.53/1.68  cnf(c350,plain,relation(skolem0001,skolem0004),inference(resolution,[status(thm)],[c254, c346])).
% 1.53/1.68  cnf(c356,plain,abstraction(skolem0001,skolem0004),inference(resolution,[status(thm)],[c257, c350])).
% 1.53/1.68  fof(ax5,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 1.53/1.68  fof(c267,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 1.53/1.68  fof(c268,plain,(![X191]:(![X192]:(~abstraction(X191,X192)|unisex(X191,X192)))),inference(variable_rename,[status(thm)],[c267])).
% 1.53/1.68  cnf(c269,plain,~abstraction(X343,X342)|unisex(X343,X342),inference(split_conjunct,[status(thm)],[c268])).
% 1.53/1.68  cnf(c382,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c269, c356])).
% 1.53/1.68  fof(ax61,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&unisex(V,U))=>unisex(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax61)).
% 1.53/1.68  fof(c95,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~unisex(V,U))|unisex(W,U))))),inference(fof_nnf,[status(thm)],[ax61])).
% 1.53/1.68  fof(c96,plain,(![X49]:(![X50]:(![X51]:((~accessible_world(X50,X51)|~unisex(X50,X49))|unisex(X51,X49))))),inference(variable_rename,[status(thm)],[c95])).
% 1.53/1.68  cnf(c97,plain,~accessible_world(X510,X511)|~unisex(X510,X509)|unisex(X511,X509),inference(split_conjunct,[status(thm)],[c96])).
% 1.53/1.68  cnf(c563,plain,~accessible_world(skolem0001,X543)|unisex(X543,skolem0004),inference(resolution,[status(thm)],[c97, c382])).
% 1.53/1.68  cnf(c593,plain,unisex(skolem0006,skolem0004),inference(resolution,[status(thm)],[c563, c56])).
% 1.53/1.68  cnf(c595,plain,skolem0006!=X1090|skolem0004!=X1089|unisex(X1090,X1089),inference(resolution,[status(thm)],[c593, c8])).
% 1.53/1.68  cnf(c1151,plain,skolem0006!=X1091|unisex(X1091,skolem0004),inference(resolution,[status(thm)],[c595, reflexivity])).
% 1.53/1.68  cnf(c393,plain,abstraction(skolem0001,skolem0006),inference(resolution,[status(thm)],[c389, c257])).
% 1.53/1.68  cnf(c394,plain,unisex(skolem0001,skolem0006),inference(resolution,[status(thm)],[c393, c269])).
% 1.53/1.68  cnf(c561,plain,~accessible_world(skolem0001,X538)|unisex(X538,skolem0006),inference(resolution,[status(thm)],[c97, c394])).
% 1.53/1.68  cnf(c588,plain,unisex(skolem0006,skolem0006),inference(resolution,[status(thm)],[c561, c56])).
% 1.53/1.68  cnf(c590,plain,skolem0006!=X1081|skolem0006!=X1080|unisex(X1081,X1080),inference(resolution,[status(thm)],[c588, c8])).
% 1.53/1.68  cnf(c1145,plain,skolem0006!=X1088|unisex(X1088,skolem0006),inference(resolution,[status(thm)],[c590, reflexivity])).
% 1.53/1.68  cnf(c1144,plain,skolem0006!=X1082|unisex(X1082,X1082),inference(factor,[status(thm)],[c590])).
% 1.53/1.68  cnf(c347,plain,relname(skolem0001,skolem0002),inference(resolution,[status(thm)],[c251, c45])).
% 1.53/1.68  cnf(c351,plain,relation(skolem0001,skolem0002),inference(resolution,[status(thm)],[c254, c347])).
% 1.53/1.68  cnf(c357,plain,abstraction(skolem0001,skolem0002),inference(resolution,[status(thm)],[c257, c351])).
% 1.53/1.68  cnf(c383,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c269, c357])).
% 1.53/1.68  cnf(c559,plain,~accessible_world(skolem0001,X536)|unisex(X536,skolem0002),inference(resolution,[status(thm)],[c97, c383])).
% 1.53/1.68  cnf(c585,plain,unisex(skolem0006,skolem0002),inference(resolution,[status(thm)],[c559, c56])).
% 1.53/1.68  cnf(c587,plain,skolem0006!=X1077|skolem0002!=X1076|unisex(X1077,X1076),inference(resolution,[status(thm)],[c585, c8])).
% 1.53/1.68  cnf(c1140,plain,skolem0006!=X1079|unisex(X1079,skolem0002),inference(resolution,[status(thm)],[c587, reflexivity])).
% 1.53/1.68  cnf(c522,plain,~entity(skolem0001,skolem0003)|~forename(skolem0001,X1078)|~of(skolem0001,X1078,skolem0003)|~forename(skolem0001,skolem0004)|skolem0004=X1078,inference(resolution,[status(thm)],[c70, c46])).
% 1.53/1.68  fof(ax18,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 1.53/1.68  fof(c228,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 1.53/1.68  fof(c229,plain,(![X165]:(![X166]:(~entity(X165,X166)|specific(X165,X166)))),inference(variable_rename,[status(thm)],[c228])).
% 1.53/1.68  cnf(c230,plain,~entity(X281,X280)|specific(X281,X280),inference(split_conjunct,[status(thm)],[c229])).
% 1.53/1.68  cnf(c321,plain,specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c230, c312])).
% 1.53/1.68  fof(ax63,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&specific(V,U))=>specific(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax63)).
% 1.53/1.68  fof(c89,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~specific(V,U))|specific(W,U))))),inference(fof_nnf,[status(thm)],[ax63])).
% 1.53/1.68  fof(c90,plain,(![X43]:(![X44]:(![X45]:((~accessible_world(X44,X45)|~specific(X44,X43))|specific(X45,X43))))),inference(variable_rename,[status(thm)],[c89])).
% 1.53/1.68  cnf(c91,plain,~accessible_world(X499,X497)|~specific(X499,X498)|specific(X497,X498),inference(split_conjunct,[status(thm)],[c90])).
% 1.53/1.68  cnf(c548,plain,~accessible_world(skolem0001,X520)|specific(X520,skolem0003),inference(resolution,[status(thm)],[c91, c321])).
% 1.53/1.68  cnf(c572,plain,specific(skolem0006,skolem0003),inference(resolution,[status(thm)],[c548, c56])).
% 1.53/1.68  cnf(c573,plain,skolem0006!=X1072|skolem0003!=X1073|specific(X1072,X1073),inference(resolution,[status(thm)],[c572, c23])).
% 1.53/1.68  cnf(c308,plain,human_person(skolem0001,skolem0007),inference(resolution,[status(thm)],[c218, c61])).
% 1.53/1.68  cnf(c310,plain,organism(skolem0001,skolem0007),inference(resolution,[status(thm)],[c221, c308])).
% 1.53/1.68  cnf(c313,plain,entity(skolem0001,skolem0007),inference(resolution,[status(thm)],[c224, c310])).
% 1.53/1.68  cnf(c320,plain,specific(skolem0001,skolem0007),inference(resolution,[status(thm)],[c230, c313])).
% 1.53/1.68  cnf(c543,plain,~accessible_world(skolem0001,X512)|specific(X512,skolem0007),inference(resolution,[status(thm)],[c91, c320])).
% 1.53/1.68  cnf(c564,plain,specific(skolem0006,skolem0007),inference(resolution,[status(thm)],[c543, c56])).
% 1.53/1.68  cnf(c565,plain,skolem0006!=X1067|skolem0007!=X1068|specific(X1067,X1068),inference(resolution,[status(thm)],[c564, c23])).
% 1.53/1.68  cnf(c1133,plain,skolem0006!=X1070|specific(X1070,skolem0007),inference(resolution,[status(thm)],[c565, reflexivity])).
% 1.53/1.68  cnf(c1132,plain,skolem0006!=X1069|specific(X1069,skolem0003),inference(resolution,[status(thm)],[c565, c416])).
% 1.53/1.68  fof(ax19,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 1.53/1.68  fof(c225,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 1.53/1.68  fof(c226,plain,(![X163]:(![X164]:(~entity(X163,X164)|thing(X163,X164)))),inference(variable_rename,[status(thm)],[c225])).
% 1.53/1.68  cnf(c227,plain,~entity(X275,X274)|thing(X275,X274),inference(split_conjunct,[status(thm)],[c226])).
% 1.53/1.68  cnf(c317,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c227, c312])).
% 1.53/1.68  fof(ax65,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&thing(V,U))=>thing(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax65)).
% 1.53/1.68  fof(c83,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~thing(V,U))|thing(W,U))))),inference(fof_nnf,[status(thm)],[ax65])).
% 1.53/1.68  fof(c84,plain,(![X37]:(![X38]:(![X39]:((~accessible_world(X38,X39)|~thing(X38,X37))|thing(X39,X37))))),inference(variable_rename,[status(thm)],[c83])).
% 1.53/1.68  cnf(c85,plain,~accessible_world(X435,X437)|~thing(X435,X436)|thing(X437,X436),inference(split_conjunct,[status(thm)],[c84])).
% 1.53/1.68  cnf(c488,plain,~accessible_world(skolem0001,X465)|thing(X465,skolem0003),inference(resolution,[status(thm)],[c85, c317])).
% 1.53/1.68  cnf(c515,plain,thing(skolem0006,skolem0003),inference(resolution,[status(thm)],[c488, c56])).
% 1.53/1.68  cnf(c517,plain,singleton(skolem0006,skolem0003),inference(resolution,[status(thm)],[c515, c200])).
% 1.53/1.68  cnf(c519,plain,skolem0006!=X1058|skolem0003!=X1059|singleton(X1058,X1059),inference(resolution,[status(thm)],[c517, c27])).
% 1.53/1.68  cnf(c516,plain,skolem0006!=X1056|skolem0003!=X1055|thing(X1056,X1055),inference(resolution,[status(thm)],[c515, c11])).
% 1.53/1.68  fof(ax8,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 1.53/1.68  fof(c258,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 1.53/1.68  fof(c259,plain,(![X185]:(![X186]:(~abstraction(X185,X186)|thing(X185,X186)))),inference(variable_rename,[status(thm)],[c258])).
% 1.53/1.68  cnf(c260,plain,~abstraction(X329,X328)|thing(X329,X328),inference(split_conjunct,[status(thm)],[c259])).
% 1.53/1.68  cnf(c363,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c260, c357])).
% 1.53/1.68  cnf(c487,plain,~accessible_world(skolem0001,X463)|thing(X463,skolem0002),inference(resolution,[status(thm)],[c85, c363])).
% 1.53/1.68  cnf(c510,plain,thing(skolem0006,skolem0002),inference(resolution,[status(thm)],[c487, c56])).
% 1.53/1.68  cnf(c512,plain,singleton(skolem0006,skolem0002),inference(resolution,[status(thm)],[c510, c200])).
% 1.53/1.68  cnf(c514,plain,skolem0006!=X1052|skolem0002!=X1053|singleton(X1052,X1053),inference(resolution,[status(thm)],[c512, c27])).
% 1.53/1.68  cnf(c1122,plain,skolem0006!=X1054|singleton(X1054,skolem0002),inference(resolution,[status(thm)],[c514, reflexivity])).
% 1.53/1.68  cnf(c511,plain,skolem0006!=X1046|skolem0002!=X1045|thing(X1046,X1045),inference(resolution,[status(thm)],[c510, c11])).
% 1.53/1.68  cnf(c1118,plain,skolem0006!=X1047|thing(X1047,skolem0002),inference(resolution,[status(thm)],[c511, reflexivity])).
% 1.53/1.68  cnf(c397,plain,thing(skolem0001,skolem0006),inference(resolution,[status(thm)],[c393, c260])).
% 1.53/1.68  cnf(c483,plain,~accessible_world(skolem0001,X451)|thing(X451,skolem0006),inference(resolution,[status(thm)],[c85, c397])).
% 1.53/1.68  cnf(c503,plain,thing(skolem0006,skolem0006),inference(resolution,[status(thm)],[c483, c56])).
% 1.53/1.68  cnf(c505,plain,singleton(skolem0006,skolem0006),inference(resolution,[status(thm)],[c503, c200])).
% 1.53/1.68  cnf(c507,plain,skolem0006!=X1038|skolem0006!=X1039|singleton(X1038,X1039),inference(resolution,[status(thm)],[c505, c27])).
% 1.53/1.68  cnf(c1113,plain,skolem0006!=X1044|singleton(X1044,skolem0006),inference(resolution,[status(thm)],[c507, reflexivity])).
% 1.53/1.68  cnf(c1112,plain,skolem0006!=X1040|singleton(X1040,X1040),inference(factor,[status(thm)],[c507])).
% 1.53/1.68  cnf(c504,plain,skolem0006!=X1032|skolem0006!=X1031|thing(X1032,X1031),inference(resolution,[status(thm)],[c503, c11])).
% 1.53/1.68  cnf(c1107,plain,skolem0006!=X1037|thing(X1037,skolem0006),inference(resolution,[status(thm)],[c504, reflexivity])).
% 1.53/1.68  cnf(c1106,plain,skolem0006!=X1033|thing(X1033,X1033),inference(factor,[status(thm)],[c504])).
% 1.53/1.68  cnf(c362,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c260, c356])).
% 1.53/1.68  cnf(c482,plain,~accessible_world(skolem0001,X444)|thing(X444,skolem0004),inference(resolution,[status(thm)],[c85, c362])).
% 1.53/1.68  cnf(c496,plain,thing(skolem0006,skolem0004),inference(resolution,[status(thm)],[c482, c56])).
% 1.53/1.68  cnf(c498,plain,singleton(skolem0006,skolem0004),inference(resolution,[status(thm)],[c496, c200])).
% 1.53/1.68  cnf(c500,plain,skolem0006!=X1028|skolem0004!=X1029|singleton(X1028,X1029),inference(resolution,[status(thm)],[c498, c27])).
% 1.53/1.68  cnf(c1104,plain,skolem0006!=X1030|singleton(X1030,skolem0004),inference(resolution,[status(thm)],[c500, reflexivity])).
% 1.53/1.68  cnf(c497,plain,skolem0006!=X1026|skolem0004!=X1025|thing(X1026,X1025),inference(resolution,[status(thm)],[c496, c11])).
% 1.53/1.68  cnf(c1102,plain,skolem0006!=X1027|thing(X1027,skolem0004),inference(resolution,[status(thm)],[c497, reflexivity])).
% 1.53/1.68  cnf(c494,plain,skolem0001!=X1022|skolem0005!=X1023|present(X1022,X1023),inference(resolution,[status(thm)],[c32, c54])).
% 1.53/1.68  cnf(c1100,plain,skolem0001!=X1024|present(X1024,skolem0005),inference(resolution,[status(thm)],[c494, reflexivity])).
% 1.53/1.68  cnf(c316,plain,thing(skolem0001,skolem0007),inference(resolution,[status(thm)],[c227, c313])).
% 1.53/1.68  cnf(c480,plain,~accessible_world(skolem0001,X438)|thing(X438,skolem0007),inference(resolution,[status(thm)],[c85, c316])).
% 1.53/1.68  cnf(c489,plain,thing(skolem0006,skolem0007),inference(resolution,[status(thm)],[c480, c56])).
% 1.53/1.68  cnf(c491,plain,singleton(skolem0006,skolem0007),inference(resolution,[status(thm)],[c489, c200])).
% 1.53/1.68  cnf(c493,plain,skolem0006!=X1018|skolem0007!=X1019|singleton(X1018,X1019),inference(resolution,[status(thm)],[c491, c27])).
% 1.53/1.68  cnf(c1097,plain,skolem0006!=X1021|singleton(X1021,skolem0007),inference(resolution,[status(thm)],[c493, reflexivity])).
% 1.53/1.68  cnf(c1096,plain,skolem0006!=X1020|singleton(X1020,skolem0003),inference(resolution,[status(thm)],[c493, c416])).
% 1.53/1.68  cnf(c490,plain,skolem0006!=X1015|skolem0007!=X1014|thing(X1015,X1014),inference(resolution,[status(thm)],[c489, c11])).
% 1.53/1.68  cnf(c1093,plain,skolem0006!=X1017|thing(X1017,skolem0007),inference(resolution,[status(thm)],[c490, reflexivity])).
% 1.53/1.68  cnf(c1092,plain,skolem0006!=X1016|thing(X1016,skolem0003),inference(resolution,[status(thm)],[c490, c416])).
% 1.53/1.68  cnf(c297,plain,eventuality(skolem0001,skolem0005),inference(resolution,[status(thm)],[c215, c53])).
% 1.53/1.68  fof(ax66,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&eventuality(V,U))=>eventuality(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax66)).
% 1.53/1.68  fof(c80,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~eventuality(V,U))|eventuality(W,U))))),inference(fof_nnf,[status(thm)],[ax66])).
% 1.53/1.68  fof(c81,plain,(![X34]:(![X35]:(![X36]:((~accessible_world(X35,X36)|~eventuality(X35,X34))|eventuality(X36,X34))))),inference(variable_rename,[status(thm)],[c80])).
% 1.53/1.68  cnf(c82,plain,~accessible_world(X413,X414)|~eventuality(X413,X412)|eventuality(X414,X412),inference(split_conjunct,[status(thm)],[c81])).
% 1.53/1.68  cnf(c459,plain,~accessible_world(skolem0001,X415)|eventuality(X415,skolem0005),inference(resolution,[status(thm)],[c82, c297])).
% 1.53/1.68  cnf(c462,plain,eventuality(skolem0006,skolem0005),inference(resolution,[status(thm)],[c459, c56])).
% 1.53/1.68  cnf(c467,plain,thing(skolem0006,skolem0005),inference(resolution,[status(thm)],[c462, c197])).
% 1.53/1.68  cnf(c474,plain,singleton(skolem0006,skolem0005),inference(resolution,[status(thm)],[c467, c200])).
% 1.53/1.68  cnf(c477,plain,skolem0006!=X1008|skolem0005!=X1009|singleton(X1008,X1009),inference(resolution,[status(thm)],[c474, c27])).
% 1.53/1.68  cnf(c1088,plain,skolem0006!=X1010|singleton(X1010,skolem0005),inference(resolution,[status(thm)],[c477, reflexivity])).
% 1.53/1.68  cnf(c476,plain,skolem0001!=X1005|skolem0005!=X1006|think_believe_consider(X1005,X1006),inference(resolution,[status(thm)],[c30, c55])).
% 1.53/1.68  cnf(c1086,plain,skolem0001!=X1007|think_believe_consider(X1007,skolem0005),inference(resolution,[status(thm)],[c476, reflexivity])).
% 1.53/1.68  cnf(c468,plain,unisex(skolem0006,skolem0005),inference(resolution,[status(thm)],[c462, c209])).
% 1.53/1.68  cnf(c475,plain,skolem0006!=X1003|skolem0005!=X1002|unisex(X1003,X1002),inference(resolution,[status(thm)],[c468, c8])).
% 1.53/1.68  cnf(c1084,plain,skolem0006!=X1004|unisex(X1004,skolem0005),inference(resolution,[status(thm)],[c475, reflexivity])).
% 1.53/1.68  cnf(c473,plain,skolem0006!=X1000|skolem0005!=X999|thing(X1000,X999),inference(resolution,[status(thm)],[c467, c11])).
% 1.53/1.68  cnf(c1082,plain,skolem0006!=X1001|thing(X1001,skolem0005),inference(resolution,[status(thm)],[c473, reflexivity])).
% 1.53/1.68  cnf(c466,plain,specific(skolem0006,skolem0005),inference(resolution,[status(thm)],[c462, c203])).
% 1.53/1.68  cnf(c472,plain,skolem0006!=X996|skolem0005!=X997|specific(X996,X997),inference(resolution,[status(thm)],[c466, c23])).
% 1.53/1.68  cnf(c1080,plain,skolem0006!=X998|specific(X998,skolem0005),inference(resolution,[status(thm)],[c472, reflexivity])).
% 1.53/1.68  cnf(c465,plain,nonexistent(skolem0006,skolem0005),inference(resolution,[status(thm)],[c462, c206])).
% 1.53/1.68  cnf(c470,plain,skolem0006!=X993|skolem0005!=X994|nonexistent(X993,X994),inference(resolution,[status(thm)],[c465, c26])).
% 1.53/1.68  cnf(c1078,plain,skolem0006!=X995|nonexistent(X995,skolem0005),inference(resolution,[status(thm)],[c470, reflexivity])).
% 1.53/1.68  cnf(c469,plain,skolem0006!=X988|skolem0005!=X987|eventuality(X988,X987),inference(resolution,[status(thm)],[c462, c24])).
% 1.53/1.68  cnf(c1075,plain,skolem0006!=X989|eventuality(X989,skolem0005),inference(resolution,[status(thm)],[c469, reflexivity])).
% 1.53/1.68  fof(ax30,axiom,(![U]:(![V]:(state(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 1.53/1.68  fof(c192,plain,(![U]:(![V]:(~state(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 1.53/1.68  fof(c193,plain,(![X141]:(![X142]:(~state(X141,X142)|eventuality(X141,X142)))),inference(variable_rename,[status(thm)],[c192])).
% 1.53/1.68  cnf(c194,plain,~state(X224,X225)|eventuality(X224,X225),inference(split_conjunct,[status(thm)],[c193])).
% 1.53/1.68  cnf(c62,negated_conjecture,state(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c41])).
% 1.53/1.68  fof(ax67,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&state(V,U))=>state(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax67)).
% 1.53/1.68  fof(c77,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~state(V,U))|state(W,U))))),inference(fof_nnf,[status(thm)],[ax67])).
% 1.53/1.68  fof(c78,plain,(![X31]:(![X32]:(![X33]:((~accessible_world(X32,X33)|~state(X32,X31))|state(X33,X31))))),inference(variable_rename,[status(thm)],[c77])).
% 1.53/1.68  cnf(c79,plain,~accessible_world(X401,X400)|~state(X401,X399)|state(X400,X399),inference(split_conjunct,[status(thm)],[c78])).
% 1.53/1.68  cnf(c431,plain,~accessible_world(skolem0001,X402)|state(X402,skolem0008),inference(resolution,[status(thm)],[c79, c62])).
% 1.53/1.68  cnf(c432,plain,state(skolem0006,skolem0008),inference(resolution,[status(thm)],[c431, c56])).
% 1.53/1.68  cnf(c433,plain,eventuality(skolem0006,skolem0008),inference(resolution,[status(thm)],[c432, c194])).
% 1.53/1.68  cnf(c439,plain,thing(skolem0006,skolem0008),inference(resolution,[status(thm)],[c433, c197])).
% 1.53/1.68  cnf(c455,plain,singleton(skolem0006,skolem0008),inference(resolution,[status(thm)],[c439, c200])).
% 1.53/1.68  cnf(c458,plain,skolem0006!=X984|skolem0008!=X985|singleton(X984,X985),inference(resolution,[status(thm)],[c455, c27])).
% 1.53/1.68  cnf(c1073,plain,skolem0006!=X986|singleton(X986,skolem0008),inference(resolution,[status(thm)],[c458, reflexivity])).
% 1.53/1.68  cnf(c28,axiom,X409!=X410|X408!=X407|~accessible_world(X409,X408)|accessible_world(X410,X407),theory(equality)).
% 1.53/1.68  cnf(c457,plain,skolem0001!=X982|skolem0006!=X981|accessible_world(X982,X981),inference(resolution,[status(thm)],[c28, c56])).
% 1.53/1.68  cnf(c1071,plain,skolem0001!=X983|accessible_world(X983,skolem0006),inference(resolution,[status(thm)],[c457, reflexivity])).
% 1.53/1.68  cnf(c440,plain,unisex(skolem0006,skolem0008),inference(resolution,[status(thm)],[c433, c209])).
% 1.53/1.68  cnf(c456,plain,skolem0006!=X979|skolem0008!=X978|unisex(X979,X978),inference(resolution,[status(thm)],[c440, c8])).
% 1.53/1.68  cnf(c1069,plain,skolem0006!=X980|unisex(X980,skolem0008),inference(resolution,[status(thm)],[c456, reflexivity])).
% 1.53/1.68  cnf(c454,plain,skolem0006!=X976|skolem0008!=X975|thing(X976,X975),inference(resolution,[status(thm)],[c439, c11])).
% 1.53/1.68  cnf(c1067,plain,skolem0006!=X977|thing(X977,skolem0008),inference(resolution,[status(thm)],[c454, reflexivity])).
% 1.53/1.68  cnf(c438,plain,specific(skolem0006,skolem0008),inference(resolution,[status(thm)],[c433, c203])).
% 1.53/1.68  cnf(c453,plain,skolem0006!=X972|skolem0008!=X973|specific(X972,X973),inference(resolution,[status(thm)],[c438, c23])).
% 1.53/1.68  cnf(c1065,plain,skolem0006!=X974|specific(X974,skolem0008),inference(resolution,[status(thm)],[c453, reflexivity])).
% 1.53/1.68  cnf(c437,plain,nonexistent(skolem0006,skolem0008),inference(resolution,[status(thm)],[c433, c206])).
% 1.53/1.68  cnf(c451,plain,skolem0006!=X969|skolem0008!=X970|nonexistent(X969,X970),inference(resolution,[status(thm)],[c437, c26])).
% 1.53/1.68  cnf(c1063,plain,skolem0006!=X971|nonexistent(X971,skolem0008),inference(resolution,[status(thm)],[c451, reflexivity])).
% 1.53/1.68  cnf(c403,plain,singleton(skolem0001,skolem0006),inference(resolution,[status(thm)],[c397, c200])).
% 1.53/1.68  cnf(c450,plain,skolem0001!=X966|skolem0006!=X967|singleton(X966,X967),inference(resolution,[status(thm)],[c27, c403])).
% 1.53/1.68  cnf(c1061,plain,skolem0001!=X968|singleton(X968,skolem0006),inference(resolution,[status(thm)],[c450, reflexivity])).
% 1.53/1.68  cnf(c367,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c363, c200])).
% 1.53/1.68  cnf(c449,plain,skolem0001!=X963|skolem0002!=X964|singleton(X963,X964),inference(resolution,[status(thm)],[c27, c367])).
% 1.53/1.68  cnf(c1059,plain,skolem0001!=X965|singleton(X965,skolem0002),inference(resolution,[status(thm)],[c449, reflexivity])).
% 1.53/1.68  cnf(c319,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c317, c200])).
% 1.53/1.68  cnf(c448,plain,skolem0001!=X959|skolem0003!=X960|singleton(X959,X960),inference(resolution,[status(thm)],[c27, c319])).
% 1.53/1.68  cnf(c365,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c362, c200])).
% 1.53/1.68  cnf(c447,plain,skolem0001!=X956|skolem0004!=X957|singleton(X956,X957),inference(resolution,[status(thm)],[c27, c365])).
% 1.53/1.68  cnf(c1055,plain,skolem0001!=X958|singleton(X958,skolem0004),inference(resolution,[status(thm)],[c447, reflexivity])).
% 1.53/1.68  cnf(c301,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c297, c197])).
% 1.53/1.68  cnf(c306,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c301, c200])).
% 1.53/1.68  cnf(c446,plain,skolem0001!=X953|skolem0005!=X954|singleton(X953,X954),inference(resolution,[status(thm)],[c27, c306])).
% 1.53/1.68  cnf(c1053,plain,skolem0001!=X955|singleton(X955,skolem0005),inference(resolution,[status(thm)],[c446, reflexivity])).
% 1.53/1.68  cnf(c288,plain,eventuality(skolem0001,skolem0008),inference(resolution,[status(thm)],[c194, c62])).
% 1.53/1.68  cnf(c290,plain,thing(skolem0001,skolem0008),inference(resolution,[status(thm)],[c197, c288])).
% 1.53/1.68  cnf(c291,plain,singleton(skolem0001,skolem0008),inference(resolution,[status(thm)],[c200, c290])).
% 1.53/1.68  cnf(c445,plain,skolem0001!=X949|skolem0008!=X950|singleton(X949,X950),inference(resolution,[status(thm)],[c27, c291])).
% 1.53/1.68  cnf(c1050,plain,skolem0001!=X952|singleton(X952,skolem0008),inference(resolution,[status(thm)],[c445, reflexivity])).
% 1.53/1.68  cnf(c318,plain,singleton(skolem0001,skolem0007),inference(resolution,[status(thm)],[c316, c200])).
% 1.53/1.68  cnf(c444,plain,skolem0001!=X946|skolem0007!=X947|singleton(X946,X947),inference(resolution,[status(thm)],[c27, c318])).
% 1.53/1.68  cnf(c1048,plain,skolem0001!=X951|singleton(X951,skolem0007),inference(resolution,[status(thm)],[c444, reflexivity])).
% 1.53/1.68  cnf(c1047,plain,skolem0001!=X948|singleton(X948,skolem0003),inference(resolution,[status(thm)],[c444, c416])).
% 1.53/1.68  fof(ax24,axiom,(![U]:(![V]:(state(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 1.53/1.68  fof(c210,plain,(![U]:(![V]:(~state(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 1.53/1.68  fof(c211,plain,(![X153]:(![X154]:(~state(X153,X154)|event(X153,X154)))),inference(variable_rename,[status(thm)],[c210])).
% 1.53/1.68  cnf(c212,plain,~state(X248,X249)|event(X248,X249),inference(split_conjunct,[status(thm)],[c211])).
% 1.53/1.68  cnf(c434,plain,event(skolem0006,skolem0008),inference(resolution,[status(thm)],[c432, c212])).
% 1.53/1.68  cnf(c442,plain,skolem0006!=X943|skolem0008!=X944|event(X943,X944),inference(resolution,[status(thm)],[c434, c5])).
% 1.53/1.68  cnf(c1045,plain,skolem0006!=X945|event(X945,skolem0008),inference(resolution,[status(thm)],[c442, reflexivity])).
% 1.53/1.68  cnf(c441,plain,skolem0006!=X941|skolem0008!=X940|eventuality(X941,X940),inference(resolution,[status(thm)],[c433, c24])).
% 1.53/1.68  cnf(c1043,plain,skolem0006!=X942|eventuality(X942,skolem0008),inference(resolution,[status(thm)],[c441, reflexivity])).
% 1.53/1.68  cnf(c25,axiom,X390!=X391|X389!=X388|~state(X390,X389)|state(X391,X388),theory(equality)).
% 1.53/1.68  cnf(c435,plain,skolem0006!=X938|skolem0008!=X937|state(X938,X937),inference(resolution,[status(thm)],[c432, c25])).
% 1.53/1.68  cnf(c1041,plain,skolem0006!=X939|state(X939,skolem0008),inference(resolution,[status(thm)],[c435, reflexivity])).
% 1.53/1.68  cnf(c293,plain,nonexistent(skolem0001,skolem0008),inference(resolution,[status(thm)],[c206, c288])).
% 1.53/1.68  cnf(c430,plain,skolem0001!=X934|skolem0008!=X935|nonexistent(X934,X935),inference(resolution,[status(thm)],[c26, c293])).
% 1.53/1.68  cnf(c1039,plain,skolem0001!=X936|nonexistent(X936,skolem0008),inference(resolution,[status(thm)],[c430, reflexivity])).
% 1.53/1.68  cnf(c299,plain,nonexistent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c297, c206])).
% 1.53/1.68  cnf(c429,plain,skolem0001!=X931|skolem0005!=X932|nonexistent(X931,X932),inference(resolution,[status(thm)],[c26, c299])).
% 1.53/1.68  cnf(c1037,plain,skolem0001!=X933|nonexistent(X933,skolem0005),inference(resolution,[status(thm)],[c429, reflexivity])).
% 1.53/1.68  cnf(c428,plain,skolem0001!=X929|skolem0008!=X928|state(X929,X928),inference(resolution,[status(thm)],[c25, c62])).
% 1.53/1.68  cnf(c1035,plain,skolem0001!=X930|state(X930,skolem0008),inference(resolution,[status(thm)],[c428, reflexivity])).
% 1.53/1.68  cnf(c423,plain,skolem0001!=X926|skolem0008!=X925|eventuality(X926,X925),inference(resolution,[status(thm)],[c24, c288])).
% 1.53/1.68  cnf(c1033,plain,skolem0001!=X927|eventuality(X927,skolem0008),inference(resolution,[status(thm)],[c423, reflexivity])).
% 1.53/1.68  cnf(c422,plain,skolem0001!=X923|skolem0005!=X922|eventuality(X923,X922),inference(resolution,[status(thm)],[c24, c297])).
% 1.53/1.68  cnf(c1031,plain,skolem0001!=X924|eventuality(X924,skolem0005),inference(resolution,[status(thm)],[c422, reflexivity])).
% 1.53/1.68  cnf(c300,plain,specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c297, c203])).
% 1.53/1.68  cnf(c414,plain,skolem0001!=X918|skolem0005!=X919|specific(X918,X919),inference(resolution,[status(thm)],[c23, c300])).
% 1.53/1.68  cnf(c1029,plain,skolem0001!=X921|specific(X921,skolem0005),inference(resolution,[status(thm)],[c414, reflexivity])).
% 1.53/1.68  cnf(c413,plain,skolem0001!=X915|skolem0003!=X916|specific(X915,X916),inference(resolution,[status(thm)],[c23, c321])).
% 1.53/1.68  cnf(c292,plain,specific(skolem0001,skolem0008),inference(resolution,[status(thm)],[c203, c288])).
% 1.53/1.68  cnf(c412,plain,skolem0001!=X912|skolem0008!=X913|specific(X912,X913),inference(resolution,[status(thm)],[c23, c292])).
% 1.53/1.68  cnf(c1025,plain,skolem0001!=X914|specific(X914,skolem0008),inference(resolution,[status(thm)],[c412, reflexivity])).
% 1.53/1.68  cnf(c411,plain,skolem0001!=X906|skolem0007!=X907|specific(X906,X907),inference(resolution,[status(thm)],[c23, c320])).
% 1.53/1.68  cnf(c1022,plain,skolem0001!=X911|specific(X911,skolem0007),inference(resolution,[status(thm)],[c411, reflexivity])).
% 1.53/1.68  cnf(c1021,plain,skolem0001!=X910|specific(X910,skolem0003),inference(resolution,[status(thm)],[c411, c416])).
% 1.53/1.68  cnf(c322,plain,existent(skolem0001,skolem0007),inference(resolution,[status(thm)],[c233, c313])).
% 1.53/1.68  cnf(c409,plain,skolem0001!=X905|skolem0007!=X904|existent(X905,X904),inference(resolution,[status(thm)],[c22, c322])).
% 1.53/1.68  cnf(c323,plain,existent(skolem0001,skolem0003),inference(resolution,[status(thm)],[c233, c312])).
% 1.53/1.68  cnf(c408,plain,skolem0001!=X901|skolem0003!=X900|existent(X901,X900),inference(resolution,[status(thm)],[c22, c323])).
% 1.53/1.68  cnf(c1016,plain,skolem0001!=X903|existent(X903,skolem0003),inference(resolution,[status(thm)],[c408, reflexivity])).
% 1.53/1.68  cnf(c1015,plain,skolem0001!=X902|existent(X902,skolem0007),inference(resolution,[status(thm)],[c408, c415])).
% 1.53/1.68  cnf(c1011,plain,~accessible_world(skolem0006,X899)|theme(X899,skolem0005,skolem0006),inference(resolution,[status(thm)],[c1010, c169])).
% 1.53/1.68  cnf(c1003,plain,~accessible_world(skolem0006,X898)|agent(X898,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1000, c163])).
% 1.53/1.68  cnf(c995,plain,~accessible_world(skolem0006,X897)|of(X897,skolem0004,skolem0003),inference(resolution,[status(thm)],[c992, c154])).
% 1.53/1.68  cnf(c398,plain,nonhuman(skolem0001,skolem0006),inference(resolution,[status(thm)],[c393, c263])).
% 1.53/1.68  cnf(c406,plain,skolem0001!=X895|skolem0006!=X894|nonhuman(X895,X894),inference(resolution,[status(thm)],[c398, c10])).
% 1.53/1.68  cnf(c1013,plain,skolem0001!=X896|nonhuman(X896,skolem0006),inference(resolution,[status(thm)],[c406, reflexivity])).
% 1.53/1.68  cnf(c990,plain,~accessible_world(skolem0006,X893)|of(X893,skolem0002,skolem0003),inference(resolution,[status(thm)],[c988, c154])).
% 1.53/1.68  cnf(c405,plain,skolem0001!=X888|skolem0003!=X889|entity(X888,X889),inference(resolution,[status(thm)],[c21, c312])).
% 1.53/1.68  cnf(c404,plain,skolem0001!=X884|skolem0007!=X885|entity(X884,X885),inference(resolution,[status(thm)],[c21, c313])).
% 1.53/1.68  cnf(c1002,plain,skolem0001!=X887|entity(X887,skolem0007),inference(resolution,[status(thm)],[c404, reflexivity])).
% 1.53/1.68  cnf(c1001,plain,skolem0001!=X886|entity(X886,skolem0003),inference(resolution,[status(thm)],[c404, c416])).
% 1.53/1.68  cnf(c767,plain,~accessible_world(skolem0006,X882)|present(X882,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c160, c682])).
% 1.53/1.68  cnf(c766,plain,~accessible_world(skolem0006,X881)|present(X881,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c160, c610])).
% 1.53/1.68  cnf(c402,plain,skolem0001!=X879|skolem0006!=X878|thing(X879,X878),inference(resolution,[status(thm)],[c397, c11])).
% 1.53/1.68  cnf(c998,plain,skolem0001!=X880|thing(X880,skolem0006),inference(resolution,[status(thm)],[c402, reflexivity])).
% 1.53/1.68  fof(ax41,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&smoke(V,U))=>smoke(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 1.53/1.68  fof(c155,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~smoke(V,U))|smoke(W,U))))),inference(fof_nnf,[status(thm)],[ax41])).
% 1.53/1.68  fof(c156,plain,(![X110]:(![X111]:(![X112]:((~accessible_world(X111,X112)|~smoke(X111,X110))|smoke(X112,X110))))),inference(variable_rename,[status(thm)],[c155])).
% 1.53/1.68  cnf(c157,plain,~accessible_world(X601,X602)|~smoke(X601,X603)|smoke(X602,X603),inference(split_conjunct,[status(thm)],[c156])).
% 1.53/1.68  cnf(c762,plain,~accessible_world(skolem0006,X877)|smoke(X877,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c157, c609])).
% 1.53/1.68  cnf(c761,plain,~accessible_world(skolem0006,X876)|smoke(X876,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c157, c681])).
% 1.53/1.68  cnf(c395,plain,general(skolem0001,skolem0006),inference(resolution,[status(thm)],[c393, c266])).
% 1.53/1.68  cnf(c400,plain,skolem0001!=X873|skolem0006!=X874|general(X873,X874),inference(resolution,[status(thm)],[c395, c9])).
% 1.53/1.68  cnf(c993,plain,skolem0001!=X875|general(X875,skolem0006),inference(resolution,[status(thm)],[c400, reflexivity])).
% 1.53/1.68  cnf(c399,plain,skolem0001!=X869|skolem0006!=X868|unisex(X869,X868),inference(resolution,[status(thm)],[c394, c8])).
% 1.53/1.68  cnf(c986,plain,skolem0001!=X870|unisex(X870,skolem0006),inference(resolution,[status(thm)],[c399, reflexivity])).
% 1.53/1.68  fof(ax64,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&singleton(V,U))=>singleton(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax64)).
% 1.53/1.68  fof(c86,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~singleton(V,U))|singleton(W,U))))),inference(fof_nnf,[status(thm)],[ax64])).
% 1.53/1.68  fof(c87,plain,(![X40]:(![X41]:(![X42]:((~accessible_world(X41,X42)|~singleton(X41,X40))|singleton(X42,X40))))),inference(variable_rename,[status(thm)],[c86])).
% 1.53/1.68  cnf(c88,plain,~accessible_world(X476,X475)|~singleton(X476,X477)|singleton(X475,X477),inference(split_conjunct,[status(thm)],[c87])).
% 1.53/1.68  cnf(c752,plain,~accessible_world(skolem0006,X867)|singleton(X867,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c744, c88])).
% 1.53/1.68  cnf(c749,plain,~accessible_world(skolem0006,X866)|unisex(X866,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c736, c97])).
% 1.53/1.68  cnf(c745,plain,~accessible_world(skolem0006,X865)|thing(X865,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c735, c85])).
% 1.53/1.68  cnf(c396,plain,skolem0001!=X863|skolem0006!=X862|abstraction(X863,X862),inference(resolution,[status(thm)],[c393, c7])).
% 1.53/1.68  cnf(c984,plain,skolem0001!=X864|abstraction(X864,skolem0006),inference(resolution,[status(thm)],[c396, reflexivity])).
% 1.53/1.68  cnf(c742,plain,~accessible_world(skolem0006,X861)|specific(X861,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c734, c91])).
% 1.53/1.68  fof(ax62,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonexistent(V,U))=>nonexistent(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax62)).
% 1.53/1.68  fof(c92,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonexistent(V,U))|nonexistent(W,U))))),inference(fof_nnf,[status(thm)],[ax62])).
% 1.53/1.68  fof(c93,plain,(![X46]:(![X47]:(![X48]:((~accessible_world(X47,X48)|~nonexistent(X47,X46))|nonexistent(X48,X46))))),inference(variable_rename,[status(thm)],[c92])).
% 1.53/1.68  cnf(c94,plain,~accessible_world(X505,X503)|~nonexistent(X505,X504)|nonexistent(X503,X504),inference(split_conjunct,[status(thm)],[c93])).
% 1.53/1.68  cnf(c740,plain,~accessible_world(skolem0006,X860)|nonexistent(X860,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c733, c94])).
% 1.53/1.68  cnf(c732,plain,~accessible_world(skolem0006,X859)|eventuality(X859,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c725, c82])).
% 1.53/1.68  cnf(c392,plain,skolem0001!=X856|skolem0006!=X857|relation(X856,X857),inference(resolution,[status(thm)],[c389, c3])).
% 1.53/1.68  cnf(c982,plain,skolem0001!=X858|relation(X858,skolem0006),inference(resolution,[status(thm)],[c392, reflexivity])).
% 1.53/1.68  cnf(c723,plain,~accessible_world(skolem0006,X855)|event(X855,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c679, c100])).
% 1.53/1.68  cnf(c676,plain,~accessible_world(skolem0006,X854)|singleton(X854,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c669, c88])).
% 1.53/1.68  cnf(c671,plain,~accessible_world(skolem0006,X853)|unisex(X853,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c658, c97])).
% 1.53/1.68  cnf(c325,plain,impartial(skolem0001,skolem0007),inference(resolution,[status(thm)],[c236, c310])).
% 1.53/1.68  cnf(c391,plain,skolem0001!=X850|skolem0007!=X849|impartial(X850,X849),inference(resolution,[status(thm)],[c20, c325])).
% 1.53/1.68  cnf(c670,plain,~accessible_world(skolem0006,X848)|thing(X848,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c657, c85])).
% 1.53/1.68  cnf(c324,plain,impartial(skolem0001,skolem0003),inference(resolution,[status(thm)],[c236, c311])).
% 1.53/1.68  cnf(c390,plain,skolem0001!=X845|skolem0003!=X844|impartial(X845,X844),inference(resolution,[status(thm)],[c20, c324])).
% 1.53/1.68  cnf(c977,plain,skolem0001!=X847|impartial(X847,skolem0003),inference(resolution,[status(thm)],[c390, reflexivity])).
% 1.53/1.68  cnf(c976,plain,skolem0001!=X846|impartial(X846,skolem0007),inference(resolution,[status(thm)],[c390, c415])).
% 1.53/1.68  cnf(c667,plain,~accessible_world(skolem0006,X843)|specific(X843,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c656, c91])).
% 1.53/1.68  cnf(c665,plain,~accessible_world(skolem0006,X842)|nonexistent(X842,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c655, c94])).
% 1.53/1.68  cnf(c654,plain,~accessible_world(skolem0006,X841)|eventuality(X841,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c650, c82])).
% 1.53/1.68  cnf(c387,plain,skolem0001!=X839|skolem0002!=X838|unisex(X839,X838),inference(resolution,[status(thm)],[c383, c8])).
% 1.53/1.68  cnf(c974,plain,skolem0001!=X840|unisex(X840,skolem0002),inference(resolution,[status(thm)],[c387, reflexivity])).
% 1.53/1.68  cnf(c648,plain,~accessible_world(skolem0006,X837)|event(X837,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c607, c100])).
% 1.53/1.68  cnf(c331,plain,living(skolem0001,skolem0007),inference(resolution,[status(thm)],[c239, c310])).
% 1.53/1.68  cnf(c385,plain,skolem0001!=X829|skolem0007!=X828|living(X829,X828),inference(resolution,[status(thm)],[c19, c331])).
% 1.53/1.68  cnf(c968,plain,skolem0001!=X834|living(X834,skolem0007),inference(resolution,[status(thm)],[c385, reflexivity])).
% 1.53/1.68  cnf(c330,plain,living(skolem0001,skolem0003),inference(resolution,[status(thm)],[c239, c311])).
% 1.53/1.68  cnf(c386,plain,skolem0001!=X833|skolem0003!=X832|living(X833,X832),inference(resolution,[status(thm)],[c19, c330])).
% 1.53/1.68  cnf(c967,plain,skolem0001!=X831|living(X831,skolem0003),inference(resolution,[status(thm)],[c385, c416])).
% 1.53/1.68  cnf(c384,plain,skolem0001!=X823|skolem0004!=X822|unisex(X823,X822),inference(resolution,[status(thm)],[c382, c8])).
% 1.53/1.68  cnf(c964,plain,skolem0001!=X830|unisex(X830,skolem0004),inference(resolution,[status(thm)],[c384, reflexivity])).
% 1.53/1.68  cnf(c375,plain,general(skolem0001,skolem0002),inference(resolution,[status(thm)],[c266, c357])).
% 1.53/1.68  cnf(c380,plain,skolem0001!=X818|skolem0002!=X819|general(X818,X819),inference(resolution,[status(thm)],[c375, c9])).
% 1.53/1.68  cnf(c961,plain,skolem0001!=X827|general(X827,skolem0002),inference(resolution,[status(thm)],[c380, reflexivity])).
% 1.53/1.68  cnf(c378,plain,skolem0001!=X809|skolem0003!=X808|organism(X809,X808),inference(resolution,[status(thm)],[c18, c311])).
% 1.53/1.68  cnf(c954,plain,skolem0001!=X824|organism(X824,skolem0003),inference(resolution,[status(thm)],[c378, reflexivity])).
% 1.53/1.68  cnf(c953,plain,skolem0001!=X821|organism(X821,skolem0007),inference(resolution,[status(thm)],[c378, c415])).
% 1.53/1.68  cnf(c374,plain,general(skolem0001,skolem0004),inference(resolution,[status(thm)],[c266, c356])).
% 1.53/1.68  cnf(c376,plain,skolem0001!=X802|skolem0004!=X803|general(X802,X803),inference(resolution,[status(thm)],[c374, c9])).
% 1.53/1.68  cnf(c950,plain,skolem0001!=X820|general(X820,skolem0004),inference(resolution,[status(thm)],[c376, reflexivity])).
% 1.53/1.68  cnf(c371,plain,nonhuman(skolem0001,skolem0002),inference(resolution,[status(thm)],[c263, c357])).
% 1.53/1.68  cnf(c373,plain,skolem0001!=X799|skolem0002!=X798|nonhuman(X799,X798),inference(resolution,[status(thm)],[c371, c10])).
% 1.53/1.68  cnf(c947,plain,skolem0001!=X817|nonhuman(X817,skolem0002),inference(resolution,[status(thm)],[c373, reflexivity])).
% 1.53/1.68  cnf(c370,plain,nonhuman(skolem0001,skolem0004),inference(resolution,[status(thm)],[c263, c356])).
% 1.53/1.68  cnf(c372,plain,skolem0001!=X794|skolem0004!=X793|nonhuman(X794,X793),inference(resolution,[status(thm)],[c370, c10])).
% 1.53/1.68  cnf(c943,plain,skolem0001!=X816|nonhuman(X816,skolem0004),inference(resolution,[status(thm)],[c372, reflexivity])).
% 1.53/1.68  cnf(c379,plain,skolem0001!=X813|skolem0007!=X812|organism(X813,X812),inference(resolution,[status(thm)],[c18, c310])).
% 1.53/1.68  cnf(c332,plain,human(skolem0001,skolem0007),inference(resolution,[status(thm)],[c242, c308])).
% 1.53/1.68  cnf(c368,plain,skolem0001!=X783|skolem0007!=X784|human(X783,X784),inference(resolution,[status(thm)],[c17, c332])).
% 1.53/1.68  cnf(c936,plain,skolem0001!=X811|human(X811,skolem0007),inference(resolution,[status(thm)],[c368, reflexivity])).
% 1.53/1.68  cnf(c935,plain,skolem0001!=X810|human(X810,skolem0003),inference(resolution,[status(thm)],[c368, c416])).
% 1.53/1.68  cnf(c366,plain,skolem0001!=X778|skolem0002!=X777|thing(X778,X777),inference(resolution,[status(thm)],[c363, c11])).
% 1.53/1.68  cnf(c933,plain,skolem0001!=X807|thing(X807,skolem0002),inference(resolution,[status(thm)],[c366, reflexivity])).
% 1.53/1.68  cnf(c364,plain,skolem0001!=X773|skolem0004!=X772|thing(X773,X772),inference(resolution,[status(thm)],[c362, c11])).
% 1.53/1.68  cnf(c931,plain,skolem0001!=X806|thing(X806,skolem0004),inference(resolution,[status(thm)],[c364, reflexivity])).
% 1.53/1.68  cnf(c336,plain,animate(skolem0001,skolem0007),inference(resolution,[status(thm)],[c245, c308])).
% 1.53/1.68  cnf(c360,plain,skolem0001!=X761|skolem0007!=X762|animate(X761,X762),inference(resolution,[status(thm)],[c16, c336])).
% 1.53/1.68  cnf(c925,plain,skolem0001!=X801|animate(X801,skolem0007),inference(resolution,[status(thm)],[c360, reflexivity])).
% 1.53/1.68  cnf(c924,plain,skolem0001!=X800|animate(X800,skolem0003),inference(resolution,[status(thm)],[c360, c416])).
% 1.53/1.68  cnf(c359,plain,skolem0001!=X756|skolem0002!=X755|abstraction(X756,X755),inference(resolution,[status(thm)],[c357, c7])).
% 1.53/1.68  cnf(c921,plain,skolem0001!=X797|abstraction(X797,skolem0002),inference(resolution,[status(thm)],[c359, reflexivity])).
% 1.53/1.68  cnf(c358,plain,skolem0001!=X751|skolem0004!=X750|abstraction(X751,X750),inference(resolution,[status(thm)],[c356, c7])).
% 1.53/1.68  cnf(c918,plain,skolem0001!=X796|abstraction(X796,skolem0004),inference(resolution,[status(thm)],[c358, reflexivity])).
% 1.53/1.68  cnf(c355,plain,skolem0001!=X744|skolem0002!=X745|relation(X744,X745),inference(resolution,[status(thm)],[c351, c3])).
% 1.53/1.68  cnf(c916,plain,skolem0001!=X795|relation(X795,skolem0002),inference(resolution,[status(thm)],[c355, reflexivity])).
% 1.53/1.68  cnf(c354,plain,skolem0001!=X740|skolem0004!=X741|relation(X740,X741),inference(resolution,[status(thm)],[c350, c3])).
% 1.53/1.68  cnf(c913,plain,skolem0001!=X792|relation(X792,skolem0004),inference(resolution,[status(thm)],[c354, reflexivity])).
% 1.53/1.68  cnf(c333,plain,human(skolem0001,skolem0003),inference(resolution,[status(thm)],[c242, c309])).
% 1.53/1.68  cnf(c369,plain,skolem0001!=X788|skolem0003!=X789|human(X788,X789),inference(resolution,[status(thm)],[c17, c333])).
% 1.53/1.68  cnf(c352,plain,skolem0001!=X729|skolem0007!=X728|human_person(X729,X728),inference(resolution,[status(thm)],[c15, c308])).
% 1.53/1.68  cnf(c908,plain,skolem0001!=X787|human_person(X787,skolem0007),inference(resolution,[status(thm)],[c352, reflexivity])).
% 1.53/1.68  cnf(c907,plain,skolem0001!=X786|human_person(X786,skolem0003),inference(resolution,[status(thm)],[c352, c416])).
% 1.53/1.68  cnf(c349,plain,skolem0001!=X723|skolem0002!=X722|relname(X723,X722),inference(resolution,[status(thm)],[c347, c12])).
% 1.53/1.68  cnf(c904,plain,skolem0001!=X785|relname(X785,skolem0002),inference(resolution,[status(thm)],[c349, reflexivity])).
% 1.53/1.68  cnf(c348,plain,skolem0001!=X717|skolem0004!=X716|relname(X717,X716),inference(resolution,[status(thm)],[c346, c12])).
% 1.53/1.69  cnf(c903,plain,skolem0001!=X782|relname(X782,skolem0004),inference(resolution,[status(thm)],[c348, reflexivity])).
% 1.53/1.69  cnf(c899,plain,~accessible_world(skolem0006,X781)|vincent_forename(X781,skolem0004),inference(resolution,[status(thm)],[c895, c175])).
% 1.53/1.69  cnf(c892,plain,~accessible_world(skolem0006,X776)|proposition(X776,skolem0006),inference(resolution,[status(thm)],[c891, c172])).
% 1.53/1.69  cnf(c890,plain,~accessible_world(skolem0006,X775)|think_believe_consider(X775,skolem0005),inference(resolution,[status(thm)],[c886, c166])).
% 1.53/1.69  cnf(c340,plain,male(skolem0001,skolem0007),inference(resolution,[status(thm)],[c248, c61])).
% 1.53/1.69  cnf(c344,plain,skolem0001!=X709|skolem0007!=X708|male(X709,X708),inference(resolution,[status(thm)],[c14, c340])).
% 1.53/1.69  cnf(c888,plain,skolem0001!=X774|male(X774,skolem0007),inference(resolution,[status(thm)],[c344, reflexivity])).
% 1.53/1.69  cnf(c887,plain,skolem0001!=X771|male(X771,skolem0003),inference(resolution,[status(thm)],[c344, c416])).
% 1.53/1.69  cnf(c884,plain,~accessible_world(skolem0006,X770)|present(X770,skolem0005),inference(resolution,[status(thm)],[c883, c160])).
% 1.53/1.69  cnf(c882,plain,~accessible_world(skolem0006,X769)|jules_forename(X769,skolem0002),inference(resolution,[status(thm)],[c877, c151])).
% 1.53/1.69  cnf(c337,plain,animate(skolem0001,skolem0003),inference(resolution,[status(thm)],[c245, c309])).
% 1.53/1.69  cnf(c361,plain,skolem0001!=X765|skolem0003!=X766|animate(X765,X766),inference(resolution,[status(thm)],[c16, c337])).
% 1.53/1.69  cnf(c338,plain,skolem0001!=X699|skolem0007!=X700|man(X699,X700),inference(resolution,[status(thm)],[c13, c61])).
% 1.53/1.69  cnf(c874,plain,skolem0001!=X764|man(X764,skolem0007),inference(resolution,[status(thm)],[c338, reflexivity])).
% 1.53/1.69  cnf(c873,plain,skolem0001!=X763|man(X763,skolem0003),inference(resolution,[status(thm)],[c338, c416])).
% 1.53/1.69  cnf(c329,plain,skolem0001!=X696|skolem0005!=X695|thing(X696,X695),inference(resolution,[status(thm)],[c11, c301])).
% 1.53/1.69  cnf(c870,plain,skolem0001!=X760|thing(X760,skolem0005),inference(resolution,[status(thm)],[c329, reflexivity])).
% 1.53/1.69  cnf(c327,plain,skolem0001!=X686|skolem0008!=X685|thing(X686,X685),inference(resolution,[status(thm)],[c11, c290])).
% 1.53/1.69  cnf(c862,plain,skolem0001!=X757|thing(X757,skolem0008),inference(resolution,[status(thm)],[c327, reflexivity])).
% 1.53/1.69  cnf(c326,plain,skolem0001!=X680|skolem0007!=X679|thing(X680,X679),inference(resolution,[status(thm)],[c11, c316])).
% 1.53/1.69  cnf(c860,plain,skolem0001!=X754|thing(X754,skolem0007),inference(resolution,[status(thm)],[c326, reflexivity])).
% 1.53/1.69  cnf(c859,plain,skolem0001!=X753|thing(X753,skolem0003),inference(resolution,[status(thm)],[c326, c416])).
% 1.53/1.69  fof(ax45,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&nonhuman(V,U))=>nonhuman(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax45)).
% 1.53/1.69  fof(c143,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~nonhuman(V,U))|nonhuman(W,U))))),inference(fof_nnf,[status(thm)],[ax45])).
% 1.53/1.69  fof(c144,plain,(![X97]:(![X98]:(![X99]:((~accessible_world(X98,X99)|~nonhuman(X98,X97))|nonhuman(X99,X97))))),inference(variable_rename,[status(thm)],[c143])).
% 1.53/1.69  cnf(c145,plain,~accessible_world(X582,X583)|~nonhuman(X582,X581)|nonhuman(X583,X581),inference(split_conjunct,[status(thm)],[c144])).
% 1.53/1.69  cnf(c858,plain,~accessible_world(skolem0006,X752)|nonhuman(X752,skolem0006),inference(resolution,[status(thm)],[c852, c145])).
% 1.53/1.69  fof(ax44,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&general(V,U))=>general(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax44)).
% 1.53/1.69  fof(c146,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~general(V,U))|general(W,U))))),inference(fof_nnf,[status(thm)],[ax44])).
% 1.53/1.69  fof(c147,plain,(![X100]:(![X101]:(![X102]:((~accessible_world(X101,X102)|~general(X101,X100))|general(X102,X100))))),inference(variable_rename,[status(thm)],[c146])).
% 1.53/1.69  cnf(c148,plain,~accessible_world(X586,X584)|~general(X586,X585)|general(X584,X585),inference(split_conjunct,[status(thm)],[c147])).
% 1.53/1.69  cnf(c854,plain,~accessible_world(skolem0006,X749)|general(X749,skolem0006),inference(resolution,[status(thm)],[c848, c148])).
% 1.53/1.69  cnf(c295,plain,unisex(skolem0001,skolem0008),inference(resolution,[status(thm)],[c209, c288])).
% 1.53/1.69  cnf(c315,plain,skolem0001!=X678|skolem0008!=X677|unisex(X678,X677),inference(resolution,[status(thm)],[c8, c295])).
% 1.53/1.69  cnf(c853,plain,skolem0001!=X748|unisex(X748,skolem0008),inference(resolution,[status(thm)],[c315, reflexivity])).
% 1.53/1.69  fof(ax46,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&abstraction(V,U))=>abstraction(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax46)).
% 1.53/1.69  fof(c140,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~abstraction(V,U))|abstraction(W,U))))),inference(fof_nnf,[status(thm)],[ax46])).
% 1.53/1.69  fof(c141,plain,(![X94]:(![X95]:(![X96]:((~accessible_world(X95,X96)|~abstraction(X95,X94))|abstraction(X96,X94))))),inference(variable_rename,[status(thm)],[c140])).
% 1.53/1.69  cnf(c142,plain,~accessible_world(X580,X579)|~abstraction(X580,X578)|abstraction(X579,X578),inference(split_conjunct,[status(thm)],[c141])).
% 1.53/1.69  cnf(c851,plain,~accessible_world(skolem0006,X747)|abstraction(X747,skolem0006),inference(resolution,[status(thm)],[c846, c142])).
% 1.53/1.69  cnf(c845,plain,~accessible_world(skolem0006,X746)|relation(X746,skolem0006),inference(resolution,[status(thm)],[c843, c139])).
% 1.53/1.69  cnf(c302,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c297, c209])).
% 1.53/1.69  cnf(c314,plain,skolem0001!=X674|skolem0005!=X673|unisex(X674,X673),inference(resolution,[status(thm)],[c8, c302])).
% 1.53/1.69  cnf(c841,plain,skolem0001!=X743|unisex(X743,skolem0005),inference(resolution,[status(thm)],[c314, reflexivity])).
% 1.53/1.69  cnf(c840,plain,skolem0001!=X742|jules_forename(X742,skolem0002),inference(resolution,[status(thm)],[c307, reflexivity])).
% 1.53/1.69  cnf(c296,plain,event(skolem0001,skolem0008),inference(resolution,[status(thm)],[c212, c62])).
% 1.53/1.69  cnf(c304,plain,skolem0001!=X661|skolem0008!=X662|event(X661,X662),inference(resolution,[status(thm)],[c5, c296])).
% 1.53/1.69  cnf(c837,plain,skolem0001!=X739|event(X739,skolem0008),inference(resolution,[status(thm)],[c304, reflexivity])).
% 1.53/1.69  cnf(c833,plain,~accessible_world(skolem0006,X738)|nonhuman(X738,skolem0002),inference(resolution,[status(thm)],[c827, c145])).
% 1.53/1.69  cnf(c829,plain,~accessible_world(skolem0006,X737)|general(X737,skolem0002),inference(resolution,[status(thm)],[c823, c148])).
% 1.53/1.69  cnf(c303,plain,skolem0001!=X659|skolem0005!=X660|event(X659,X660),inference(resolution,[status(thm)],[c5, c53])).
% 1.53/1.69  cnf(c828,plain,skolem0001!=X736|event(X736,skolem0005),inference(resolution,[status(thm)],[c303, reflexivity])).
% 1.53/1.69  cnf(c353,plain,skolem0001!=X735|skolem0003!=X734|human_person(X735,X734),inference(resolution,[status(thm)],[c15, c309])).
% 1.53/1.69  cnf(c826,plain,~accessible_world(skolem0006,X733)|abstraction(X733,skolem0002),inference(resolution,[status(thm)],[c821, c142])).
% 1.53/1.69  cnf(c820,plain,~accessible_world(skolem0006,X732)|relation(X732,skolem0002),inference(resolution,[status(thm)],[c816, c139])).
% 1.53/1.69  fof(ax48,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&relname(V,U))=>relname(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax48)).
% 1.53/1.69  fof(c134,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~relname(V,U))|relname(W,U))))),inference(fof_nnf,[status(thm)],[ax48])).
% 1.53/1.69  fof(c135,plain,(![X88]:(![X89]:(![X90]:((~accessible_world(X89,X90)|~relname(X89,X88))|relname(X90,X88))))),inference(variable_rename,[status(thm)],[c134])).
% 1.53/1.69  cnf(c136,plain,~accessible_world(X573,X572)|~relname(X573,X574)|relname(X572,X574),inference(split_conjunct,[status(thm)],[c135])).
% 1.53/1.69  cnf(c818,plain,~accessible_world(skolem0006,X731)|relname(X731,skolem0002),inference(resolution,[status(thm)],[c815, c136])).
% 1.53/1.69  cnf(c813,plain,~accessible_world(skolem0006,X730)|forename(X730,skolem0002),inference(resolution,[status(thm)],[c811, c133])).
% 1.53/1.69  cnf(c289,plain,skolem0001!=X658|skolem0006!=X657|proposition(X658,X657),inference(resolution,[status(thm)],[c2, c50])).
% 1.53/1.69  cnf(c812,plain,skolem0001!=X727|proposition(X727,skolem0006),inference(resolution,[status(thm)],[c289, reflexivity])).
% 1.53/1.69  cnf(c810,plain,~accessible_world(skolem0006,X726)|nonhuman(X726,skolem0004),inference(resolution,[status(thm)],[c804, c145])).
% 1.53/1.69  cnf(c806,plain,~accessible_world(skolem0006,X725)|general(X725,skolem0004),inference(resolution,[status(thm)],[c800, c148])).
% 1.53/1.69  cnf(c287,plain,skolem0001!=X654|skolem0002!=X655|forename(X654,X655),inference(resolution,[status(thm)],[c1, c45])).
% 1.53/1.69  cnf(c805,plain,skolem0001!=X724|forename(X724,skolem0002),inference(resolution,[status(thm)],[c287, reflexivity])).
% 1.53/1.69  cnf(c803,plain,~accessible_world(skolem0006,X721)|abstraction(X721,skolem0004),inference(resolution,[status(thm)],[c798, c142])).
% 1.53/1.69  cnf(c797,plain,~accessible_world(skolem0006,X720)|relation(X720,skolem0004),inference(resolution,[status(thm)],[c793, c139])).
% 1.53/1.69  cnf(c795,plain,~accessible_world(skolem0006,X719)|relname(X719,skolem0004),inference(resolution,[status(thm)],[c792, c136])).
% 1.53/1.69  cnf(c790,plain,~accessible_world(skolem0006,X718)|forename(X718,skolem0004),inference(resolution,[status(thm)],[c788, c133])).
% 1.53/1.69  cnf(c286,plain,skolem0001!=X652|skolem0004!=X653|forename(X652,X653),inference(resolution,[status(thm)],[c1, c49])).
% 1.53/1.69  cnf(c789,plain,skolem0001!=X715|forename(X715,skolem0004),inference(resolution,[status(thm)],[c286, reflexivity])).
% 1.53/1.69  cnf(c785,plain,skolem0001!=X714|vincent_forename(X714,skolem0004),inference(resolution,[status(thm)],[c285, reflexivity])).
% 1.53/1.69  cnf(c341,plain,male(skolem0001,skolem0003),inference(resolution,[status(thm)],[c248, c47])).
% 1.53/1.69  cnf(c345,plain,skolem0001!=X713|skolem0003!=X712|male(X713,X712),inference(resolution,[status(thm)],[c14, c341])).
% 1.53/1.69  cnf(c339,plain,skolem0001!=X704|skolem0003!=X705|man(X704,X705),inference(resolution,[status(thm)],[c13, c47])).
% 1.53/1.69  cnf(c748,plain,~accessible_world(skolem0001,X702)|general(X702,skolem0002),inference(resolution,[status(thm)],[c148, c375])).
% 1.53/1.69  cnf(c747,plain,~accessible_world(skolem0001,X701)|general(X701,skolem0004),inference(resolution,[status(thm)],[c148, c374])).
% 1.53/1.69  cnf(c746,plain,~accessible_world(skolem0001,X698)|general(X698,skolem0006),inference(resolution,[status(thm)],[c148, c395])).
% 1.53/1.69  cnf(c731,plain,~accessible_world(skolem0001,X697)|nonhuman(X697,skolem0004),inference(resolution,[status(thm)],[c145, c370])).
% 1.53/1.69  cnf(c730,plain,~accessible_world(skolem0001,X694)|nonhuman(X694,skolem0002),inference(resolution,[status(thm)],[c145, c371])).
% 1.53/1.69  cnf(c729,plain,~accessible_world(skolem0001,X693)|nonhuman(X693,skolem0006),inference(resolution,[status(thm)],[c145, c398])).
% 1.53/1.69  cnf(c722,plain,~accessible_world(skolem0001,X692)|abstraction(X692,skolem0002),inference(resolution,[status(thm)],[c142, c357])).
% 1.53/1.69  cnf(c328,plain,skolem0001!=X691|skolem0003!=X690|thing(X691,X690),inference(resolution,[status(thm)],[c11, c317])).
% 1.53/1.69  cnf(c721,plain,~accessible_world(skolem0001,X689)|abstraction(X689,skolem0006),inference(resolution,[status(thm)],[c142, c393])).
% 1.53/1.69  cnf(c720,plain,~accessible_world(skolem0001,X688)|abstraction(X688,skolem0004),inference(resolution,[status(thm)],[c142, c356])).
% 1.53/1.69  fof(ax55,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&existent(V,U))=>existent(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax55)).
% 1.53/1.69  fof(c113,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~existent(V,U))|existent(W,U))))),inference(fof_nnf,[status(thm)],[ax55])).
% 1.53/1.69  fof(c114,plain,(![X67]:(![X68]:(![X69]:((~accessible_world(X68,X69)|~existent(X68,X67))|existent(X69,X67))))),inference(variable_rename,[status(thm)],[c113])).
% 1.53/1.69  cnf(c115,plain,~accessible_world(X548,X547)|~existent(X548,X546)|existent(X547,X546),inference(split_conjunct,[status(thm)],[c114])).
% 1.53/1.69  cnf(c719,plain,~accessible_world(skolem0006,X687)|existent(X687,skolem0003),inference(resolution,[status(thm)],[c709, c115])).
% 1.53/1.69  fof(ax53,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&living(V,U))=>living(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax53)).
% 1.53/1.69  fof(c119,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~living(V,U))|living(W,U))))),inference(fof_nnf,[status(thm)],[ax53])).
% 1.53/1.69  fof(c120,plain,(![X73]:(![X74]:(![X75]:((~accessible_world(X74,X75)|~living(X74,X73))|living(X75,X73))))),inference(variable_rename,[status(thm)],[c119])).
% 1.53/1.69  cnf(c121,plain,~accessible_world(X556,X558)|~living(X556,X557)|living(X558,X557),inference(split_conjunct,[status(thm)],[c120])).
% 1.53/1.69  cnf(c717,plain,~accessible_world(skolem0006,X684)|living(X684,skolem0003),inference(resolution,[status(thm)],[c700, c121])).
% 1.53/1.69  fof(ax54,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&impartial(V,U))=>impartial(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax54)).
% 1.53/1.69  fof(c116,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~impartial(V,U))|impartial(W,U))))),inference(fof_nnf,[status(thm)],[ax54])).
% 1.53/1.69  fof(c117,plain,(![X70]:(![X71]:(![X72]:((~accessible_world(X71,X72)|~impartial(X71,X70))|impartial(X72,X70))))),inference(variable_rename,[status(thm)],[c116])).
% 1.53/1.69  cnf(c118,plain,~accessible_world(X553,X551)|~impartial(X553,X552)|impartial(X551,X552),inference(split_conjunct,[status(thm)],[c117])).
% 1.53/1.69  cnf(c714,plain,~accessible_world(skolem0006,X683)|impartial(X683,skolem0003),inference(resolution,[status(thm)],[c699, c118])).
% 1.53/1.69  fof(ax56,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&entity(V,U))=>entity(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax56)).
% 1.53/1.69  fof(c110,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~entity(V,U))|entity(W,U))))),inference(fof_nnf,[status(thm)],[ax56])).
% 1.53/1.69  fof(c111,plain,(![X64]:(![X65]:(![X66]:((~accessible_world(X65,X66)|~entity(X65,X64))|entity(X66,X64))))),inference(variable_rename,[status(thm)],[c110])).
% 1.53/1.69  cnf(c112,plain,~accessible_world(X541,X540)|~entity(X541,X539)|entity(X540,X539),inference(split_conjunct,[status(thm)],[c111])).
% 1.53/1.69  cnf(c713,plain,~accessible_world(skolem0006,X682)|entity(X682,skolem0003),inference(resolution,[status(thm)],[c698, c112])).
% 1.53/1.69  cnf(c708,plain,~accessible_world(skolem0001,X681)|relation(X681,skolem0002),inference(resolution,[status(thm)],[c139, c351])).
% 1.53/1.69  fof(ax33,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 1.53/1.69  fof(c180,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax33])).
% 1.53/1.69  fof(c181,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c180])).
% 1.53/1.69  fof(c182,plain,(![X135]:(![X136]:(~specific(X135,X136)|~general(X135,X136)))),inference(variable_rename,[status(thm)],[c181])).
% 1.53/1.69  cnf(c183,plain,~specific(X218,X219)|~general(X218,X219),inference(split_conjunct,[status(thm)],[c182])).
% 1.53/1.69  cnf(c856,plain,~specific(skolem0006,skolem0006),inference(resolution,[status(thm)],[c848, c183])).
% 1.53/1.69  cnf(c706,plain,~accessible_world(skolem0001,X675)|relation(X675,skolem0004),inference(resolution,[status(thm)],[c139, c350])).
% 1.53/1.69  fof(ax51,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&animate(V,U))=>animate(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax51)).
% 1.53/1.69  fof(c125,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~animate(V,U))|animate(W,U))))),inference(fof_nnf,[status(thm)],[ax51])).
% 1.53/1.69  fof(c126,plain,(![X79]:(![X80]:(![X81]:((~accessible_world(X80,X81)|~animate(X80,X79))|animate(X81,X79))))),inference(variable_rename,[status(thm)],[c125])).
% 1.53/1.69  cnf(c127,plain,~accessible_world(X562,X564)|~animate(X562,X563)|animate(X564,X563),inference(split_conjunct,[status(thm)],[c126])).
% 1.53/1.69  cnf(c705,plain,~accessible_world(skolem0006,X672)|animate(X672,skolem0003),inference(resolution,[status(thm)],[c694, c127])).
% 1.53/1.69  fof(ax52,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human(V,U))=>human(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax52)).
% 1.53/1.69  fof(c122,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~human(V,U))|human(W,U))))),inference(fof_nnf,[status(thm)],[ax52])).
% 1.53/1.69  fof(c123,plain,(![X76]:(![X77]:(![X78]:((~accessible_world(X77,X78)|~human(X77,X76))|human(X78,X76))))),inference(variable_rename,[status(thm)],[c122])).
% 1.53/1.69  cnf(c124,plain,~accessible_world(X559,X561)|~human(X559,X560)|human(X561,X560),inference(split_conjunct,[status(thm)],[c123])).
% 1.53/1.69  cnf(c703,plain,~accessible_world(skolem0006,X671)|human(X671,skolem0003),inference(resolution,[status(thm)],[c692, c124])).
% 1.53/1.69  fof(ax57,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&organism(V,U))=>organism(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax57)).
% 1.53/1.69  fof(c107,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~organism(V,U))|organism(W,U))))),inference(fof_nnf,[status(thm)],[ax57])).
% 1.53/1.69  fof(c108,plain,(![X61]:(![X62]:(![X63]:((~accessible_world(X62,X63)|~organism(X62,X61))|organism(X63,X61))))),inference(variable_rename,[status(thm)],[c107])).
% 1.53/1.69  cnf(c109,plain,~accessible_world(X535,X533)|~organism(X535,X534)|organism(X533,X534),inference(split_conjunct,[status(thm)],[c108])).
% 1.53/1.69  cnf(c696,plain,~accessible_world(skolem0006,X670)|organism(X670,skolem0003),inference(resolution,[status(thm)],[c691, c109])).
% 1.53/1.69  fof(ax58,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&human_person(V,U))=>human_person(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax58)).
% 1.53/1.69  fof(c104,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~human_person(V,U))|human_person(W,U))))),inference(fof_nnf,[status(thm)],[ax58])).
% 1.53/1.69  fof(c105,plain,(![X58]:(![X59]:(![X60]:((~accessible_world(X59,X60)|~human_person(X59,X58))|human_person(X60,X58))))),inference(variable_rename,[status(thm)],[c104])).
% 1.53/1.69  cnf(c106,plain,~accessible_world(X529,X530)|~human_person(X529,X528)|human_person(X530,X528),inference(split_conjunct,[status(thm)],[c105])).
% 1.53/1.69  cnf(c695,plain,~accessible_world(skolem0006,X669)|human_person(X669,skolem0003),inference(resolution,[status(thm)],[c684, c106])).
% 1.53/1.69  cnf(c690,plain,~accessible_world(skolem0001,X666)|relname(X666,skolem0002),inference(resolution,[status(thm)],[c136, c347])).
% 1.53/1.69  cnf(c689,plain,~accessible_world(skolem0001,X665)|relname(X665,skolem0004),inference(resolution,[status(thm)],[c136, c346])).
% 1.53/1.69  fof(ax50,axiom,(![U]:(![V]:(![W]:((accessible_world(V,W)&male(V,U))=>male(W,U))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax50)).
% 1.53/1.69  fof(c128,plain,(![U]:(![V]:(![W]:((~accessible_world(V,W)|~male(V,U))|male(W,U))))),inference(fof_nnf,[status(thm)],[ax50])).
% 1.53/1.69  fof(c129,plain,(![X82]:(![X83]:(![X84]:((~accessible_world(X83,X84)|~male(X83,X82))|male(X84,X82))))),inference(variable_rename,[status(thm)],[c128])).
% 1.53/1.69  cnf(c130,plain,~accessible_world(X567,X566)|~male(X567,X565)|male(X566,X565),inference(split_conjunct,[status(thm)],[c129])).
% 1.53/1.69  cnf(c688,plain,~accessible_world(skolem0006,X664)|male(X664,skolem0003),inference(resolution,[status(thm)],[c678, c130])).
% 1.53/1.69  cnf(c685,plain,~accessible_world(skolem0006,X663)|man(X663,skolem0003),inference(resolution,[status(thm)],[c677, c103])).
% 1.53/1.69  cnf(c831,plain,~specific(skolem0006,skolem0002),inference(resolution,[status(thm)],[c823, c183])).
% 1.53/1.69  cnf(c808,plain,~specific(skolem0006,skolem0004),inference(resolution,[status(thm)],[c800, c183])).
% 1.53/1.69  cnf(c662,plain,~accessible_world(skolem0001,X650)|male(X650,skolem0003),inference(resolution,[status(thm)],[c130, c341])).
% 1.53/1.69  cnf(c661,plain,~accessible_world(skolem0001,X649)|male(X649,skolem0007),inference(resolution,[status(thm)],[c130, c340])).
% 1.53/1.69  cnf(c660,plain,~accessible_world(skolem0006,X646)|male(X646,skolem0007),inference(resolution,[status(thm)],[c130, c606])).
% 1.53/1.69  cnf(c647,plain,~accessible_world(skolem0001,X645)|animate(X645,skolem0003),inference(resolution,[status(thm)],[c127, c337])).
% 1.53/1.69  cnf(c646,plain,~accessible_world(skolem0001,X644)|animate(X644,skolem0007),inference(resolution,[status(thm)],[c127, c336])).
% 1.53/1.69  cnf(c645,plain,~accessible_world(skolem0006,X640)|animate(X640,skolem0007),inference(resolution,[status(thm)],[c127, c619])).
% 1.53/1.69  cnf(c644,plain,~accessible_world(skolem0006,X639)|existent(X639,skolem0007),inference(resolution,[status(thm)],[c631, c115])).
% 1.53/1.69  cnf(c642,plain,~accessible_world(skolem0006,X638)|living(X638,skolem0007),inference(resolution,[status(thm)],[c627, c121])).
% 1.53/1.69  cnf(c639,plain,~accessible_world(skolem0006,X637)|impartial(X637,skolem0007),inference(resolution,[status(thm)],[c626, c118])).
% 1.53/1.69  cnf(c638,plain,~accessible_world(skolem0006,X636)|human(X636,skolem0007),inference(resolution,[status(thm)],[c124, c617])).
% 1.53/1.69  cnf(c637,plain,~accessible_world(skolem0001,X632)|human(X632,skolem0003),inference(resolution,[status(thm)],[c124, c333])).
% 1.53/1.69  cnf(c636,plain,~accessible_world(skolem0001,X631)|human(X631,skolem0007),inference(resolution,[status(thm)],[c124, c332])).
% 1.53/1.69  cnf(c635,plain,~accessible_world(skolem0006,X630)|entity(X630,skolem0007),inference(resolution,[status(thm)],[c625, c112])).
% 1.53/1.69  cnf(c623,plain,~accessible_world(skolem0006,X625)|organism(X625,skolem0007),inference(resolution,[status(thm)],[c616, c109])).
% 1.53/1.69  cnf(c622,plain,~accessible_world(skolem0001,X624)|living(X624,skolem0003),inference(resolution,[status(thm)],[c121, c330])).
% 1.53/1.69  cnf(c621,plain,~accessible_world(skolem0001,X623)|living(X623,skolem0007),inference(resolution,[status(thm)],[c121, c331])).
% 1.53/1.69  cnf(c620,plain,~accessible_world(skolem0006,X619)|human_person(X619,skolem0007),inference(resolution,[status(thm)],[c612, c106])).
% 1.53/1.69  cnf(c613,plain,~accessible_world(skolem0006,X618)|man(X618,skolem0007),inference(resolution,[status(thm)],[c605, c103])).
% 1.53/1.69  cnf(c604,plain,~accessible_world(skolem0001,X617)|impartial(X617,skolem0007),inference(resolution,[status(thm)],[c118, c325])).
% 1.53/1.69  cnf(c603,plain,~accessible_world(skolem0001,X612)|impartial(X612,skolem0003),inference(resolution,[status(thm)],[c118, c324])).
% 1.53/1.69  cnf(c599,plain,~accessible_world(skolem0006,X611)|event(X611,skolem0005),inference(resolution,[status(thm)],[c596, c100])).
% 1.53/1.69  cnf(c598,plain,~accessible_world(skolem0001,X610)|existent(X610,skolem0007),inference(resolution,[status(thm)],[c115, c322])).
% 1.53/1.69  cnf(c597,plain,~accessible_world(skolem0001,X606)|existent(X606,skolem0003),inference(resolution,[status(thm)],[c115, c323])).
% 1.53/1.69  cnf(c594,plain,~accessible_world(skolem0006,X605)|unisex(X605,skolem0004),inference(resolution,[status(thm)],[c593, c97])).
% 1.53/1.69  cnf(c592,plain,~accessible_world(skolem0001,X604)|entity(X604,skolem0003),inference(resolution,[status(thm)],[c112, c312])).
% 1.53/1.69  cnf(c591,plain,~accessible_world(skolem0001,X600)|entity(X600,skolem0007),inference(resolution,[status(thm)],[c112, c313])).
% 1.53/1.69  cnf(c589,plain,~accessible_world(skolem0006,X599)|unisex(X599,skolem0006),inference(resolution,[status(thm)],[c588, c97])).
% 1.53/1.69  cnf(c586,plain,~accessible_world(skolem0006,X598)|unisex(X598,skolem0002),inference(resolution,[status(thm)],[c585, c97])).
% 1.53/1.69  cnf(c584,plain,~accessible_world(skolem0001,X593)|organism(X593,skolem0007),inference(resolution,[status(thm)],[c109, c310])).
% 1.53/1.69  cnf(c583,plain,~accessible_world(skolem0001,X592)|organism(X592,skolem0003),inference(resolution,[status(thm)],[c109, c311])).
% 1.53/1.69  cnf(c580,plain,~accessible_world(skolem0001,X591)|human_person(X591,skolem0003),inference(resolution,[status(thm)],[c106, c309])).
% 1.53/1.69  cnf(c579,plain,~accessible_world(skolem0001,X587)|human_person(X587,skolem0007),inference(resolution,[status(thm)],[c106, c308])).
% 1.53/1.69  fof(ax31,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 1.53/1.69  fof(c188,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax31])).
% 1.53/1.69  fof(c189,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c188])).
% 1.53/1.69  fof(c190,plain,(![X139]:(![X140]:(~existent(X139,X140)|~nonexistent(X139,X140)))),inference(variable_rename,[status(thm)],[c189])).
% 1.53/1.69  cnf(c191,plain,~existent(X223,X222)|~nonexistent(X223,X222),inference(split_conjunct,[status(thm)],[c190])).
% 1.53/1.69  cnf(c739,plain,~existent(skolem0006,skolem0009(skolem0003)),inference(resolution,[status(thm)],[c733, c191])).
% 1.53/1.69  fof(ax32,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 1.53/1.69  fof(c184,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax32])).
% 1.53/1.69  fof(c185,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c184])).
% 1.53/1.69  fof(c186,plain,(![X137]:(![X138]:(~nonhuman(X137,X138)|~human(X137,X138)))),inference(variable_rename,[status(thm)],[c185])).
% 1.53/1.69  cnf(c187,plain,~nonhuman(X220,X221)|~human(X220,X221),inference(split_conjunct,[status(thm)],[c186])).
% 1.53/1.69  cnf(c701,plain,~nonhuman(skolem0006,skolem0003),inference(resolution,[status(thm)],[c692, c187])).
% 1.53/1.69  fof(ax34,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 1.53/1.69  fof(c176,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax34])).
% 1.53/1.69  fof(c177,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c176])).
% 1.53/1.69  fof(c178,plain,(![X133]:(![X134]:(~unisex(X133,X134)|~male(X133,X134)))),inference(variable_rename,[status(thm)],[c177])).
% 1.53/1.69  cnf(c179,plain,~unisex(X213,X212)|~male(X213,X212),inference(split_conjunct,[status(thm)],[c178])).
% 1.53/1.69  cnf(c686,plain,~unisex(skolem0006,skolem0003),inference(resolution,[status(thm)],[c678, c179])).
% 1.53/1.69  cnf(c664,plain,~existent(skolem0006,skolem0009(skolem0007)),inference(resolution,[status(thm)],[c655, c191])).
% 1.53/1.69  cnf(c628,plain,~nonhuman(skolem0006,skolem0007),inference(resolution,[status(thm)],[c617, c187])).
% 1.53/1.69  cnf(c614,plain,~unisex(skolem0006,skolem0007),inference(resolution,[status(thm)],[c606, c179])).
% 1.53/1.69  cnf(c574,plain,~accessible_world(skolem0006,X554)|specific(X554,skolem0003),inference(resolution,[status(thm)],[c572, c91])).
% 1.53/1.69  cnf(c570,plain,~accessible_world(skolem0001,X550)|event(X550,skolem0008),inference(resolution,[status(thm)],[c100, c296])).
% 1.53/1.69  cnf(c569,plain,~accessible_world(skolem0006,X549)|event(X549,skolem0008),inference(resolution,[status(thm)],[c100, c434])).
% 1.53/1.69  cnf(c566,plain,~accessible_world(skolem0006,X544)|specific(X544,skolem0007),inference(resolution,[status(thm)],[c564, c91])).
% 1.53/1.69  cnf(c562,plain,~accessible_world(skolem0006,X542)|unisex(X542,skolem0008),inference(resolution,[status(thm)],[c97, c440])).
% 1.53/1.69  cnf(c560,plain,~accessible_world(skolem0006,X537)|unisex(X537,skolem0005),inference(resolution,[status(thm)],[c97, c468])).
% 1.53/1.69  cnf(c558,plain,~accessible_world(skolem0001,X532)|unisex(X532,skolem0005),inference(resolution,[status(thm)],[c97, c302])).
% 1.53/1.69  cnf(c557,plain,~accessible_world(skolem0001,X531)|unisex(X531,skolem0008),inference(resolution,[status(thm)],[c97, c295])).
% 1.53/1.69  cnf(c554,plain,~accessible_world(skolem0001,X527)|nonexistent(X527,skolem0008),inference(resolution,[status(thm)],[c94, c293])).
% 1.53/1.69  cnf(c553,plain,~accessible_world(skolem0001,X526)|nonexistent(X526,skolem0005),inference(resolution,[status(thm)],[c94, c299])).
% 1.53/1.69  cnf(c552,plain,~accessible_world(skolem0006,X525)|nonexistent(X525,skolem0008),inference(resolution,[status(thm)],[c94, c437])).
% 1.53/1.69  cnf(c551,plain,~accessible_world(skolem0006,X524)|nonexistent(X524,skolem0005),inference(resolution,[status(thm)],[c94, c465])).
% 1.53/1.69  cnf(c547,plain,~accessible_world(skolem0001,X519)|specific(X519,skolem0005),inference(resolution,[status(thm)],[c91, c300])).
% 1.53/1.69  cnf(c546,plain,~accessible_world(skolem0001,X515)|specific(X515,skolem0008),inference(resolution,[status(thm)],[c91, c292])).
% 1.53/1.69  cnf(c545,plain,~accessible_world(skolem0006,X514)|specific(X514,skolem0008),inference(resolution,[status(thm)],[c91, c438])).
% 1.53/1.69  cnf(c544,plain,~accessible_world(skolem0006,X513)|specific(X513,skolem0005),inference(resolution,[status(thm)],[c91, c466])).
% 1.53/1.69  cnf(c536,plain,~accessible_world(skolem0001,X508)|singleton(X508,skolem0006),inference(resolution,[status(thm)],[c88, c403])).
% 1.53/1.69  cnf(c535,plain,~accessible_world(skolem0006,X507)|singleton(X507,skolem0002),inference(resolution,[status(thm)],[c88, c512])).
% 1.53/1.69  cnf(c534,plain,~accessible_world(skolem0001,X506)|singleton(X506,skolem0002),inference(resolution,[status(thm)],[c88, c367])).
% 1.53/1.69  cnf(c533,plain,~accessible_world(skolem0001,X502)|singleton(X502,skolem0003),inference(resolution,[status(thm)],[c88, c319])).
% 1.53/1.69  cnf(c532,plain,~accessible_world(skolem0006,X501)|singleton(X501,skolem0004),inference(resolution,[status(thm)],[c88, c498])).
% 1.53/1.69  cnf(c531,plain,~accessible_world(skolem0001,X500)|singleton(X500,skolem0004),inference(resolution,[status(thm)],[c88, c365])).
% 1.53/1.69  cnf(c530,plain,~accessible_world(skolem0006,X496)|singleton(X496,skolem0007),inference(resolution,[status(thm)],[c88, c491])).
% 1.53/1.69  cnf(c529,plain,~accessible_world(skolem0001,X495)|singleton(X495,skolem0005),inference(resolution,[status(thm)],[c88, c306])).
% 1.53/1.69  cnf(c528,plain,~accessible_world(skolem0006,X494)|singleton(X494,skolem0003),inference(resolution,[status(thm)],[c88, c517])).
% 1.53/1.69  cnf(c527,plain,~accessible_world(skolem0006,X493)|singleton(X493,skolem0005),inference(resolution,[status(thm)],[c88, c474])).
% 1.53/1.69  cnf(c526,plain,~accessible_world(skolem0001,X487)|singleton(X487,skolem0008),inference(resolution,[status(thm)],[c88, c291])).
% 1.53/1.69  cnf(c525,plain,~accessible_world(skolem0006,X486)|singleton(X486,skolem0006),inference(resolution,[status(thm)],[c88, c505])).
% 1.53/1.69  cnf(c524,plain,~accessible_world(skolem0006,X485)|singleton(X485,skolem0008),inference(resolution,[status(thm)],[c88, c455])).
% 1.53/1.69  cnf(c523,plain,~accessible_world(skolem0001,X478)|singleton(X478,skolem0007),inference(resolution,[status(thm)],[c88, c318])).
% 1.53/1.69  cnf(c518,plain,~accessible_world(skolem0006,X474)|thing(X474,skolem0003),inference(resolution,[status(thm)],[c515, c85])).
% 1.53/1.69  cnf(c513,plain,~accessible_world(skolem0006,X473)|thing(X473,skolem0002),inference(resolution,[status(thm)],[c510, c85])).
% 1.53/1.69  cnf(c506,plain,~accessible_world(skolem0006,X472)|thing(X472,skolem0006),inference(resolution,[status(thm)],[c503, c85])).
% 1.53/1.69  cnf(c499,plain,~accessible_world(skolem0006,X467)|thing(X467,skolem0004),inference(resolution,[status(thm)],[c496, c85])).
% 1.53/1.69  cnf(c492,plain,~accessible_world(skolem0006,X466)|thing(X466,skolem0007),inference(resolution,[status(thm)],[c489, c85])).
% 1.53/1.69  cnf(c486,plain,~accessible_world(skolem0001,X462)|thing(X462,skolem0005),inference(resolution,[status(thm)],[c85, c301])).
% 1.53/1.69  cnf(c485,plain,~accessible_world(skolem0006,X453)|thing(X453,skolem0008),inference(resolution,[status(thm)],[c85, c439])).
% 1.53/1.69  cnf(c484,plain,~accessible_world(skolem0006,X452)|thing(X452,skolem0005),inference(resolution,[status(thm)],[c85, c467])).
% 1.53/1.69  cnf(c481,plain,~accessible_world(skolem0001,X443)|thing(X443,skolem0008),inference(resolution,[status(thm)],[c85, c290])).
% 1.53/1.69  cnf(c464,plain,~accessible_world(skolem0006,X434)|eventuality(X434,skolem0005),inference(resolution,[status(thm)],[c462, c82])).
% 1.53/1.69  cnf(c461,plain,~accessible_world(skolem0006,X427)|eventuality(X427,skolem0008),inference(resolution,[status(thm)],[c82, c433])).
% 1.53/1.69  cnf(c460,plain,~accessible_world(skolem0001,X426)|eventuality(X426,skolem0008),inference(resolution,[status(thm)],[c82, c288])).
% 1.53/1.69  cnf(c471,plain,~existent(skolem0006,skolem0005),inference(resolution,[status(thm)],[c465, c191])).
% 1.53/1.69  cnf(c436,plain,~accessible_world(skolem0006,X411)|state(X411,skolem0008),inference(resolution,[status(thm)],[c432, c79])).
% 1.53/1.69  cnf(c452,plain,~existent(skolem0006,skolem0008),inference(resolution,[status(thm)],[c437, c191])).
% 1.53/1.69  cnf(c420,plain,X387!=skolem0007|X387=skolem0003,inference(resolution,[status(thm)],[c416, transitivity])).
% 1.53/1.69  cnf(c417,plain,X386!=skolem0003|X386=skolem0007,inference(resolution,[status(thm)],[c415, transitivity])).
% 1.53/1.69  cnf(c421,plain,~actual_world(skolem0007)|actual_world(skolem0003),inference(resolution,[status(thm)],[c416, c35])).
% 1.53/1.69  cnf(c418,plain,~actual_world(skolem0003)|actual_world(skolem0007),inference(resolution,[status(thm)],[c415, c35])).
% 1.53/1.69  fof(ax1,axiom,(![U]:(![V]:(vincent_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 1.53/1.69  fof(c279,plain,(![U]:(![V]:(~vincent_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 1.53/1.69  fof(c280,plain,(![X199]:(![X200]:(~vincent_forename(X199,X200)|forename(X199,X200)))),inference(variable_rename,[status(thm)],[c279])).
% 1.53/1.69  cnf(c281,plain,~vincent_forename(X363,X362)|forename(X363,X362),inference(split_conjunct,[status(thm)],[c280])).
% 1.53/1.69  cnf(c401,plain,~specific(skolem0001,skolem0006),inference(resolution,[status(thm)],[c395, c183])).
% 1.53/1.69  fof(ax3,axiom,(![U]:(![V]:(smoke(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 1.53/1.69  fof(c273,plain,(![U]:(![V]:(~smoke(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 1.53/1.69  fof(c274,plain,(![X195]:(![X196]:(~smoke(X195,X196)|event(X195,X196)))),inference(variable_rename,[status(thm)],[c273])).
% 1.53/1.69  cnf(c275,plain,~smoke(X351,X350)|event(X351,X350),inference(split_conjunct,[status(thm)],[c274])).
% 1.53/1.69  fof(ax4,axiom,(![U]:(![V]:(jules_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 1.53/1.69  fof(c270,plain,(![U]:(![V]:(~jules_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 1.53/1.69  fof(c271,plain,(![X193]:(![X194]:(~jules_forename(X193,X194)|forename(X193,X194)))),inference(variable_rename,[status(thm)],[c270])).
% 1.53/1.69  cnf(c272,plain,~jules_forename(X349,X348)|forename(X349,X348),inference(split_conjunct,[status(thm)],[c271])).
% 1.53/1.69  cnf(c381,plain,~specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c375, c183])).
% 1.53/1.69  cnf(c377,plain,~specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c374, c183])).
% 1.53/1.69  cnf(c343,plain,~unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c341, c179])).
% 1.53/1.69  cnf(c342,plain,~unisex(skolem0001,skolem0007),inference(resolution,[status(thm)],[c340, c179])).
% 1.53/1.69  cnf(c335,plain,~nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c333, c187])).
% 1.53/1.69  cnf(c334,plain,~nonhuman(skolem0001,skolem0007),inference(resolution,[status(thm)],[c332, c187])).
% 1.53/1.69  cnf(c305,plain,~existent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c299, c191])).
% 1.53/1.69  cnf(c294,plain,~existent(skolem0001,skolem0008),inference(resolution,[status(thm)],[c293, c191])).
% 1.53/1.69  cnf(c42,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 1.53/1.69  % SZS output end Saturation
% 1.53/1.69  
% 1.53/1.69  % Initial clauses    : 132
% 1.53/1.69  % Processed clauses  : 990
% 1.53/1.69  % Factors computed   : 25
% 1.53/1.69  % Resolvents computed: 1295
% 1.53/1.69  % Tautologies deleted: 3
% 1.53/1.69  % Forward subsumed   : 459
% 1.53/1.69  % Backward subsumed  : 7
% 1.53/1.69  % -------- CPU Time ---------
% 1.53/1.69  % User time          : 1.333 s
% 1.53/1.69  % System time        : 0.015 s
% 1.53/1.69  % Total time         : 1.348 s
%------------------------------------------------------------------------------